From c1d3447652c675e40884039c6b83489a7188892d Mon Sep 17 00:00:00 2001 From: simon-hrabec Date: Tue, 4 Apr 2023 02:45:34 +0900 Subject: [PATCH] Add prusti_refute! macro (#1365) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add prusti_refute! macro * Add macro to generate getters/setters for fields via JNI * Resolve fmt-check and clippy errors, simplify naming, small refactoring * Add test for field! macro * Update field! macro to not ask for signature (WIP) * Update field! macro to search all the class hierarchy for the field to determine its signature * Rename variables, add comments, delete leftover commented code * Follow update in master branch * current code, just a snapshot of my working dir * fix bug with env/ast_utils with_local_frame - calling wrong function * add * Remove unecessary changes * additional temporary code removal * Add "refute.failed:refutation.true" into error_manager * Remove unnecessary code, fmt-all * cargo lock update * add frotend support also for carbon * add assert.failed:assertion.false-PanicCause::Refute entry to the error manager * Add field access via Scala methods, use SilFrontend wrapper and remove unecessary dispatch * Remove empty line - fmt-all error * add tests for prusti_refute! * update docs (user guide) - add mention to refute * Add disclaimer about soundness, formatting * remove unecessary case in the error manager * typo - remove blank line --------- Co-authored-by: Simon Hrabec Co-authored-by: Jonáš Fiala --- docs/user-guide/src/SUMMARY.md | 2 +- ...sert_assume.md => assert_refute_assume.md} | 37 +++++++++- docs/user-guide/src/verify/summary.md | 2 +- prusti-common/src/vir/to_viper.rs | 3 + .../prusti-contracts-proc-macros/src/lib.rs | 12 ++++ prusti-contracts/prusti-contracts/src/lib.rs | 3 + prusti-contracts/prusti-specs/src/lib.rs | 4 ++ prusti-contracts/prusti-specs/src/rewriter.rs | 9 +++ prusti-interface/src/specs/mod.rs | 17 +++++ prusti-interface/src/specs/typed.rs | 16 +++++ .../prusti_assert.rs | 0 .../assert_assume_refute/prusti_refute.rs | 30 ++++++++ .../simple_assert.rs | 0 .../src/encoder/errors/error_manager.rs | 9 +++ .../src/encoder/foldunfold/requirements.rs | 6 +- .../src/encoder/foldunfold/semantics.rs | 1 + .../encoder/mir/specifications/interface.rs | 11 +++ .../src/encoder/mir/specifications/specs.rs | 7 +- prusti-viper/src/encoder/procedure_encoder.rs | 41 ++++++++++- viper-sys/build.rs | 28 ++++++++ viper/src/ast_factory/statement.rs | 22 +++++- viper/src/verifier.rs | 68 +++++++++++++++++-- vir/defs/polymorphic/ast/stmt.rs | 45 ++++++++++++ vir/src/converter/polymorphic_to_legacy.rs | 3 + vir/src/converter/type_substitution.rs | 9 +++ vir/src/legacy/ast/stmt.rs | 22 ++++++ 26 files changed, 393 insertions(+), 14 deletions(-) rename docs/user-guide/src/verify/{assert_assume.md => assert_refute_assume.md} (59%) rename prusti-tests/tests/verify_overflow/fail/{assert_assume => assert_assume_refute}/prusti_assert.rs (100%) create mode 100644 prusti-tests/tests/verify_overflow/fail/assert_assume_refute/prusti_refute.rs rename prusti-tests/tests/verify_overflow/fail/{assert_assume => assert_assume_refute}/simple_assert.rs (100%) diff --git a/docs/user-guide/src/SUMMARY.md b/docs/user-guide/src/SUMMARY.md index baf9cde630d..1c60f9b4678 100644 --- a/docs/user-guide/src/SUMMARY.md +++ b/docs/user-guide/src/SUMMARY.md @@ -19,7 +19,7 @@ - [Absence of panics](verify/panic.md) - [Overflow checks](verify/overflow.md) - [Pre- and postconditions](verify/prepost.md) - - [Assertions and assumptions](verify/assert_assume.md) + - [Assertions, refutations and assumptions](verify/assert_refute_assume.md) - [Trusted functions](verify/trusted.md) - [Pure functions](verify/pure.md) - [Predicates](verify/predicate.md) diff --git a/docs/user-guide/src/verify/assert_assume.md b/docs/user-guide/src/verify/assert_refute_assume.md similarity index 59% rename from docs/user-guide/src/verify/assert_assume.md rename to docs/user-guide/src/verify/assert_refute_assume.md index 1bfd7da2339..714921bc1ce 100644 --- a/docs/user-guide/src/verify/assert_assume.md +++ b/docs/user-guide/src/verify/assert_refute_assume.md @@ -1,4 +1,4 @@ -# Assertions and Assumptions +# Assertions, Refutations and Assumptions You can use Prusti to verify that a certain property holds at a certain point within the body of a function (via an assertion). It is also possible to @@ -35,6 +35,41 @@ prusti_assert!(map.insert(5)); // error `assert_eq!` and `assert_ne!`, but the check is made for [snapshot equality](../syntax.md#snapshot-equality), resp. snapshot inequality. +## Refutations + +> Refutation **should not be relied upon for soundness** as it may succeed even when it should fail; Prusti may not be able to prove the property being refuted and thus won't complain even though the property actually holds (e.g. if the property is difficult to prove). + +The `prusti_refute!` macro is similar to `prusti_assert!` in its format, conditions of use and what expressions it accepts. It instructs Prusti to verify that a certain property at a specific point within the body of a function might hold in some, but not all cases. For example the following code will verify: + +```rust,noplaypen +#[ensures(val < 0 ==> result == -1)] +#[ensures(val == 0 ==> result == 0)] +#[ensures(val > 0 ==> result == 1)] +fn sign(val: i32) -> i32 { + prusti_refute!(val <= 0); + prusti_refute!(val >= 0); + if val < 0 { + -1 + } else if val > 0 { + 1 + } else { + prusti_refute!(false); + 0 + } +} +``` + +But the following function would not: + +```rust,noplaypen +#[requires(val < 0 && val > 0)] +#[ensures(result == val/2)] +fn half(val: i32) -> i32 { + prusti_refute!(false); + val/2 +} +``` + ## Assumptions The `prusti_assume!` macro instructs Prusti to assume that a certain property diff --git a/docs/user-guide/src/verify/summary.md b/docs/user-guide/src/verify/summary.md index 7bf7be4a336..2465182237b 100644 --- a/docs/user-guide/src/verify/summary.md +++ b/docs/user-guide/src/verify/summary.md @@ -10,7 +10,7 @@ More intricate properties require users to write suitable [specifications](../sy The following features are either currently supported or planned to be supported in Prusti: - [Pre- and postconditions](prepost.md) -- [Assertions and assumptions](assert_assume.md) +- [Assertions, refutations and assumptions](assert_refute_assume.md) - [Trusted functions](trusted.md) - [Pure functions](pure.md) - [Predicates](predicate.md) diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index 034628c5696..3d0d814e6e7 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -178,6 +178,9 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for Stmt { Stmt::Assert(ref expr, ref pos) => { ast.assert(expr.to_viper(context, ast), pos.to_viper(context, ast)) } + Stmt::Refute(ref expr, ref pos) => { + ast.refute(expr.to_viper(context, ast), pos.to_viper(context, ast)) + } Stmt::MethodCall(ref method_name, ref args, ref targets) => { let fake_position = Position::default(); ast.method_call( diff --git a/prusti-contracts/prusti-contracts-proc-macros/src/lib.rs b/prusti-contracts/prusti-contracts-proc-macros/src/lib.rs index a6b2b89f5f9..9a50a2f3f8c 100644 --- a/prusti-contracts/prusti-contracts-proc-macros/src/lib.rs +++ b/prusti-contracts/prusti-contracts-proc-macros/src/lib.rs @@ -70,6 +70,12 @@ pub fn prusti_assume(_tokens: TokenStream) -> TokenStream { TokenStream::new() } +#[cfg(not(feature = "prusti"))] +#[proc_macro] +pub fn prusti_refute(_tokens: TokenStream) -> TokenStream { + TokenStream::new() +} + #[cfg(not(feature = "prusti"))] #[proc_macro_attribute] pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream { @@ -195,6 +201,12 @@ pub fn prusti_assume(tokens: TokenStream) -> TokenStream { prusti_specs::prusti_assume(tokens.into()).into() } +#[cfg(feature = "prusti")] +#[proc_macro] +pub fn prusti_refute(tokens: TokenStream) -> TokenStream { + prusti_specs::prusti_refutation(tokens.into()).into() +} + #[cfg(feature = "prusti")] #[proc_macro] pub fn closure(tokens: TokenStream) -> TokenStream { diff --git a/prusti-contracts/prusti-contracts/src/lib.rs b/prusti-contracts/prusti-contracts/src/lib.rs index b7e40364743..28ab1bce27d 100644 --- a/prusti-contracts/prusti-contracts/src/lib.rs +++ b/prusti-contracts/prusti-contracts/src/lib.rs @@ -33,6 +33,9 @@ pub use prusti_contracts_proc_macros::prusti_assert; /// A macro for writing assumptions using prusti syntax pub use prusti_contracts_proc_macros::prusti_assume; +/// A macro for writing refutations using prusti syntax +pub use prusti_contracts_proc_macros::prusti_refute; + /// A macro for impl blocks that refine trait specifications. pub use prusti_contracts_proc_macros::refine_trait_spec; diff --git a/prusti-contracts/prusti-specs/src/lib.rs b/prusti-contracts/prusti-specs/src/lib.rs index 16330a4c57c..6f124f4cb01 100644 --- a/prusti-contracts/prusti-specs/src/lib.rs +++ b/prusti-contracts/prusti-specs/src/lib.rs @@ -431,6 +431,10 @@ pub fn prusti_assume(tokens: TokenStream) -> TokenStream { generate_expression_closure(&AstRewriter::process_prusti_assumption, tokens) } +pub fn prusti_refutation(tokens: TokenStream) -> TokenStream { + generate_expression_closure(&AstRewriter::process_prusti_refutation, tokens) +} + /// Generates the TokenStream encoding an expression using prusti syntax /// Used for body invariants, assertions, and assumptions fn generate_expression_closure( diff --git a/prusti-contracts/prusti-specs/src/rewriter.rs b/prusti-contracts/prusti-specs/src/rewriter.rs index a9df02429d8..16128256439 100644 --- a/prusti-contracts/prusti-specs/src/rewriter.rs +++ b/prusti-contracts/prusti-specs/src/rewriter.rs @@ -255,6 +255,15 @@ impl AstRewriter { self.process_prusti_expression(quote! {prusti_assumption}, spec_id, tokens) } + /// Parse a prusti refute into a Rust expression + pub fn process_prusti_refutation( + &mut self, + spec_id: SpecificationId, + tokens: TokenStream, + ) -> syn::Result { + self.process_prusti_expression(quote! {prusti_refutation}, spec_id, tokens) + } + fn process_prusti_expression( &mut self, kind: TokenStream, diff --git a/prusti-interface/src/specs/mod.rs b/prusti-interface/src/specs/mod.rs index 25b70c57e22..d7125c83353 100644 --- a/prusti-interface/src/specs/mod.rs +++ b/prusti-interface/src/specs/mod.rs @@ -83,6 +83,7 @@ pub struct SpecCollector<'a, 'tcx> { type_specs: FxHashMap, prusti_assertions: Vec, prusti_assumptions: Vec, + prusti_refutations: Vec, ghost_begin: Vec, ghost_end: Vec, } @@ -99,6 +100,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { type_specs: FxHashMap::default(), prusti_assertions: vec![], prusti_assumptions: vec![], + prusti_refutations: vec![], ghost_begin: vec![], ghost_end: vec![], } @@ -119,6 +121,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { self.determine_type_specs(&mut def_spec); self.determine_prusti_assertions(&mut def_spec); self.determine_prusti_assumptions(&mut def_spec); + self.determine_prusti_refutations(&mut def_spec); self.determine_ghost_begin_ends(&mut def_spec); // TODO: remove spec functions (make sure none are duplicated or left over) // Load all local spec MIR bodies, for export and later use @@ -275,6 +278,16 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { ); } } + fn determine_prusti_refutations(&self, def_spec: &mut typed::DefSpecificationMap) { + for local_id in self.prusti_refutations.iter() { + def_spec.prusti_refutations.insert( + local_id.to_def_id(), + typed::PrustiRefutation { + refutation: *local_id, + }, + ); + } + } fn determine_ghost_begin_ends(&self, def_spec: &mut typed::DefSpecificationMap) { for local_id in self.ghost_begin.iter() { def_spec.ghost_begin.insert( @@ -526,6 +539,10 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> { self.prusti_assumptions.push(local_id); } + if has_prusti_attr(attrs, "prusti_refutation") { + self.prusti_refutations.push(local_id); + } + if has_prusti_attr(attrs, "ghost_begin") { self.ghost_begin.push(local_id); } diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index 0811293421a..2041266c555 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -17,6 +17,7 @@ pub struct DefSpecificationMap { pub type_specs: FxHashMap, pub prusti_assertions: FxHashMap, pub prusti_assumptions: FxHashMap, + pub prusti_refutations: FxHashMap, pub ghost_begin: FxHashMap, pub ghost_end: FxHashMap, } @@ -46,6 +47,10 @@ impl DefSpecificationMap { self.prusti_assumptions.get(def_id) } + pub fn get_refutation(&self, def_id: &DefId) -> Option<&PrustiRefutation> { + self.prusti_refutations.get(def_id) + } + pub fn get_ghost_begin(&self, def_id: &DefId) -> Option<&GhostBegin> { self.ghost_begin.get(def_id) } @@ -166,12 +171,18 @@ impl DefSpecificationMap { .values() .map(|spec| format!("{spec:?}")) .collect(); + let refutations: Vec<_> = self + .prusti_refutations + .values() + .map(|spec| format!("{spec:?}")) + .collect(); let mut values = Vec::new(); values.extend(loop_specs); values.extend(proc_specs); values.extend(type_specs); values.extend(asserts); values.extend(assumptions); + values.extend(refutations); if hide_uuids { let uuid = Regex::new("[a-z0-9]{8}-[a-z0-9]{4}-[a-z0-9]{4}-[a-z0-9]{4}-[a-z0-9]{12}").unwrap(); @@ -292,6 +303,11 @@ pub struct PrustiAssumption { pub assumption: LocalDefId, } +#[derive(Debug, Clone)] +pub struct PrustiRefutation { + pub refutation: LocalDefId, +} + #[derive(Debug, Clone)] pub struct GhostBegin { pub marker: LocalDefId, diff --git a/prusti-tests/tests/verify_overflow/fail/assert_assume/prusti_assert.rs b/prusti-tests/tests/verify_overflow/fail/assert_assume_refute/prusti_assert.rs similarity index 100% rename from prusti-tests/tests/verify_overflow/fail/assert_assume/prusti_assert.rs rename to prusti-tests/tests/verify_overflow/fail/assert_assume_refute/prusti_assert.rs diff --git a/prusti-tests/tests/verify_overflow/fail/assert_assume_refute/prusti_refute.rs b/prusti-tests/tests/verify_overflow/fail/assert_assume_refute/prusti_refute.rs new file mode 100644 index 00000000000..45cdb9b660c --- /dev/null +++ b/prusti-tests/tests/verify_overflow/fail/assert_assume_refute/prusti_refute.rs @@ -0,0 +1,30 @@ +#![allow(unused)] + +use prusti_contracts::*; + +fn refute1() { + prusti_refute!(false); +} + +fn failing_refute() { + prusti_refute!(true); //~ ERROR +} + +fn unreachable_branch_sign(val: i32) -> i32 { + if val <= 0 { + -1 + } else if val >= 0 { + 1 + } else { + prusti_refute!(false); //~ ERROR + 0 + } +} + +#[requires(val < 0 && val > 0)] +fn no_valid_input(val: i32) -> i32 { + prusti_refute!(false); //~ ERROR + 42 +} + +fn main() {} diff --git a/prusti-tests/tests/verify_overflow/fail/assert_assume/simple_assert.rs b/prusti-tests/tests/verify_overflow/fail/assert_assume_refute/simple_assert.rs similarity index 100% rename from prusti-tests/tests/verify_overflow/fail/assert_assume/simple_assert.rs rename to prusti-tests/tests/verify_overflow/fail/assert_assume_refute/simple_assert.rs diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index e4d3d9ea01b..53d5e0e6c3d 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -30,6 +30,8 @@ pub enum PanicCause { Panic, /// Caused by an assert!() Assert, + /// Caused by an refute!() + Refute, /// Caused by an debug_assert!() DebugAssert, /// Caused by an unreachable!() @@ -696,6 +698,13 @@ impl<'tcx> ErrorManager<'tcx> { ) } + ("refute.failed:refutation.true", ErrorCtxt::Panic(PanicCause::Refute)) => { + PrustiError::verification( + "the refuted expression holds in all cases or could not be reached", + error_span, + ) + } + (full_err_id, ErrorCtxt::Unexpected) => { PrustiError::internal( format!( diff --git a/prusti-viper/src/encoder/foldunfold/requirements.rs b/prusti-viper/src/encoder/foldunfold/requirements.rs index 32c984acd4c..ba63e01139a 100644 --- a/prusti-viper/src/encoder/foldunfold/requirements.rs +++ b/prusti-viper/src/encoder/foldunfold/requirements.rs @@ -71,7 +71,11 @@ impl RequiredStmtPermissionsGetter for vir::Stmt { .collect() } - &vir::Stmt::Assert(vir::Assert { + &vir::Stmt::Refute(vir::Refute { + ref expr, + ref position, + }) + | &vir::Stmt::Assert(vir::Assert { ref expr, ref position, }) diff --git a/prusti-viper/src/encoder/foldunfold/semantics.rs b/prusti-viper/src/encoder/foldunfold/semantics.rs index a7136f36d29..a35c6cba526 100644 --- a/prusti-viper/src/encoder/foldunfold/semantics.rs +++ b/prusti-viper/src/encoder/foldunfold/semantics.rs @@ -61,6 +61,7 @@ impl ApplyOnState for vir::Stmt { &vir::Stmt::Comment(_) | &vir::Stmt::Label(_) | &vir::Stmt::Assert(_) + | &vir::Stmt::Refute(_) | &vir::Stmt::Obtain(_) => {} &vir::Stmt::Inhale(vir::Inhale { ref expr }) => { diff --git a/prusti-viper/src/encoder/mir/specifications/interface.rs b/prusti-viper/src/encoder/mir/specifications/interface.rs index 8c91fd44baa..73a829e7e60 100644 --- a/prusti-viper/src/encoder/mir/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/specifications/interface.rs @@ -97,6 +97,9 @@ pub(crate) trait SpecificationsInterface<'tcx> { /// Get the prusti assumption fn get_prusti_assumption(&self, def_id: DefId) -> Option; + /// Get the prusti refutation + fn get_prusti_refutation(&self, def_id: DefId) -> Option; + /// Get the begin marker of the ghost block fn get_ghost_begin(&self, def_id: DefId) -> Option; @@ -234,6 +237,14 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode .cloned() } + fn get_prusti_refutation(&self, def_id: DefId) -> Option { + self.specifications_state + .specs + .borrow() + .get_refutation(&def_id) + .cloned() + } + fn get_ghost_begin(&self, def_id: DefId) -> Option { self.specifications_state .specs diff --git a/prusti-viper/src/encoder/mir/specifications/specs.rs b/prusti-viper/src/encoder/mir/specifications/specs.rs index 58c81921c7a..ce904970f15 100644 --- a/prusti-viper/src/encoder/mir/specifications/specs.rs +++ b/prusti-viper/src/encoder/mir/specifications/specs.rs @@ -11,7 +11,7 @@ use prusti_interface::{ specs::typed::{ DefSpecificationMap, GhostBegin, GhostEnd, LoopSpecification, ProcedureSpecification, ProcedureSpecificationKind, ProcedureSpecificationKindError, PrustiAssertion, - PrustiAssumption, Refinable, SpecificationItem, TypeSpecification, + PrustiAssumption, PrustiRefutation, Refinable, SpecificationItem, TypeSpecification, }, PrustiError, }; @@ -91,6 +91,11 @@ impl<'tcx> Specifications<'tcx> { self.user_typed_specs.get_assumption(def_id) } + #[tracing::instrument(level = "trace", skip(self))] + pub(super) fn get_refutation(&self, def_id: &DefId) -> Option<&PrustiRefutation> { + self.user_typed_specs.get_refutation(def_id) + } + #[tracing::instrument(level = "trace", skip(self))] pub(super) fn get_ghost_begin(&self, def_id: &DefId) -> Option<&GhostBegin> { self.user_typed_specs.get_ghost_begin(def_id) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index c671915b6cc..6d823998555 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -222,7 +222,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { ) -> SpannedEncodingResult<()> { let block = &self.mir[bb]; let _ = self.try_encode_assert(bb, block, encoded_statements)? - || self.try_encode_assume(bb, block, encoded_statements)?; + || self.try_encode_assume(bb, block, encoded_statements)? + || self.try_encode_refute(bb, block, encoded_statements)?; Ok(()) } @@ -295,6 +296,44 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { Ok(false) } + fn try_encode_refute( + &mut self, + bb: mir::BasicBlock, + block: &mir::BasicBlockData<'tcx>, + encoded_statements: &mut Vec, + ) -> SpannedEncodingResult { + for stmt in &block.statements { + if let mir::StatementKind::Assign(box ( + _, + mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _), + )) = stmt.kind + { + let refutation = match self.encoder.get_prusti_refutation(cl_def_id) { + Some(spec) => spec, + None => return Ok(false), + }; + + let span = self + .encoder + .get_definition_span(refutation.refutation.to_def_id()); + + let refute_expr = self.encoder.encode_invariant(self.mir, bb, self.proc_def_id, cl_substs)?; + + let refute_stmt = vir::Stmt::Refute( + vir::Refute { + expr: refute_expr, + position: self.register_error(span, ErrorCtxt::Panic(PanicCause::Refute)) + } + ); + + encoded_statements.push(refute_stmt); + + return Ok(true); + } + } + Ok(false) + } + fn translate_polonius_error(&self, error: PoloniusInfoError) -> SpannedEncodingError { match error { PoloniusInfoError::UnsupportedLoanInLoop { diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 84622597571..78d1d021483 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -132,11 +132,26 @@ fn main() { java_class!("viper.silicon.Silicon", vec![ constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"), ]), + java_class!("viper.silicon.SiliconFrontend", vec![ + constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"), + ]), // Carbon java_class!("viper.carbon.CarbonVerifier", vec![ constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"), ]), + java_class!("viper.carbon.CarbonFrontend", vec![ + constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"), + ]), // Silver + java_class!("viper.silver.frontend.SilFrontend", vec![ + method!("setVerifier"), + method!("verification"), + method!("getVerificationResult"), + method!("setState"), + method!("verifier"), + method!("_verifier_$eq"), + method!("_program_$eq"), + ]), java_class!("viper.silver.reporter.CSVReporter", vec![ constructor!("(Ljava/lang/String;Ljava/lang/String;)V"), ]), @@ -151,6 +166,16 @@ fn main() { method!("stop"), method!("verify"), ]), + java_class!("viper.silver.frontend.DefaultStates", vec![ + method!("ConsistencyCheck"), + ]), + java_class!("viper.silver.logger.SilentLogger$", vec![ + object_getter!(), + method!("apply"), + ]), + java_class!("viper.silver.logger.ViperLogger", vec![ + method!("get"), + ]), java_class!("viper.silver.ast.pretty.FastPrettyPrinter$", vec![ object_getter!(), method!("pretty", "(Lviper/silver/ast/Node;)Ljava/lang/String;") @@ -198,6 +223,9 @@ fn main() { java_class!("viper.silver.ast.Assert", vec![ constructor!(), ]), + java_class!("viper.silver.plugin.standard.refute.Refute", vec![ + constructor!(), + ]), java_class!("viper.silver.ast.Bool$", vec![ object_getter!(), ]), diff --git a/viper/src/ast_factory/statement.rs b/viper/src/ast_factory/statement.rs index fafb83ac94b..a2592f3539c 100644 --- a/viper/src/ast_factory/statement.rs +++ b/viper/src/ast_factory/statement.rs @@ -7,7 +7,7 @@ use crate::ast_factory::{ AstFactory, }; use jni::objects::JObject; -use viper_sys::wrappers::viper::silver::ast; +use viper_sys::wrappers::viper::silver::{ast, plugin::standard::refute}; impl<'a> AstFactory<'a> { pub fn new_stmt(&self, lhs: Expr, fields: &[Field]) -> Stmt<'a> { @@ -133,6 +133,16 @@ impl<'a> AstFactory<'a> { Stmt::new(obj) } + pub fn refute(&self, expr: Expr, pos: Position) -> Stmt<'a> { + let obj = self.jni.unwrap_result(refute::Refute::with(self.env).new( + expr.to_jobject(), + pos.to_jobject(), + self.no_info(), + self.no_trafos(), + )); + Stmt::new(obj) + } + pub fn assert_with_comment(&self, expr: Expr, pos: Position, comment: &str) -> Stmt<'a> { let obj = self.jni.unwrap_result(ast::Assert::with(self.env).new( expr.to_jobject(), @@ -143,6 +153,16 @@ impl<'a> AstFactory<'a> { Stmt::new(obj) } + pub fn refute_with_comment(&self, expr: Expr, pos: Position, comment: &str) -> Stmt<'a> { + let obj = self.jni.unwrap_result(refute::Refute::with(self.env).new( + expr.to_jobject(), + pos.to_jobject(), + self.simple_info(&[comment, ""]), + self.no_trafos(), + )); + Stmt::new(obj) + } + pub fn fold(&self, acc: Expr) -> Stmt<'a> { build_ast_node!(self, Stmt, ast::Fold, acc.to_jobject()) } diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index 14ab105bea9..b05df9aadc4 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -22,6 +22,8 @@ pub struct Verifier<'a> { env: &'a JNIEnv<'a>, verifier_wrapper: silver::verifier::Verifier<'a>, verifier_instance: JObject<'a>, + frontend_wrapper: silver::frontend::SilFrontend<'a>, + frontend_instance: JObject<'a>, jni: JniUtils<'a>, ast_utils: AstUtils<'a>, smt_manager: SmtManager, @@ -37,7 +39,9 @@ impl<'a> Verifier<'a> { let jni = JniUtils::new(env); let ast_utils = AstUtils::new(env); let verifier_wrapper = silver::verifier::Verifier::with(env); - let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || { + let frontend_wrapper = silver::frontend::SilFrontend::with(env); + + let frontend_instance = jni.unwrap_result(env.with_local_frame(16, || { let reporter = if let Some(real_report_path) = report_path { jni.unwrap_result(silver::reporter::CSVReporter::with(env).new( jni.new_string("csv_reporter"), @@ -48,22 +52,69 @@ impl<'a> Verifier<'a> { }; let debug_info = jni.new_seq(&[]); - Self::instantiate_verifier(backend, env, reporter, debug_info) + + let backend_unwrapped = Self::instantiate_verifier(backend, env, reporter, debug_info); + let backend_instance = jni.unwrap_result(backend_unwrapped); + + let logger_singleton = + jni.unwrap_result(silver::logger::SilentLogger_object::with(env).singleton()); + let logger_factory = jni.unwrap_result( + silver::logger::SilentLogger_object::with(env).call_apply(logger_singleton), + ); + let logger = + jni.unwrap_result(silver::logger::ViperLogger::with(env).call_get(logger_factory)); + + let unwrapped_frontend_instance = { + match backend { + VerificationBackend::Silicon => { + silicon::SiliconFrontend::with(env).new(reporter, logger) + } + VerificationBackend::Carbon => { + carbon::CarbonFrontend::with(env).new(reporter, logger) + } + } + }; + let frontend_instance = jni.unwrap_result(unwrapped_frontend_instance); + + frontend_wrapper + .call_setVerifier(frontend_instance, backend_instance) + .unwrap(); + let verifier_option = jni.new_option(Some(backend_instance)); + + frontend_wrapper + .call___verifier___dollar_eq(frontend_instance, verifier_option) + .unwrap(); + + Ok(frontend_instance) })); - ast_utils.with_local_frame(16, || { + let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || { + let verifier_instance = + jni.unwrap_result(frontend_wrapper.call_verifier(frontend_instance)); + + let consistency_check_state = silver::frontend::DefaultStates::with(env) + .call_ConsistencyCheck() + .unwrap(); + + frontend_wrapper + .call_setState(frontend_instance, consistency_check_state) + .unwrap(); + let name = jni.to_string(jni.unwrap_result(verifier_wrapper.call_name(verifier_instance))); let build_version = jni.to_string( jni.unwrap_result(verifier_wrapper.call_buildVersion(verifier_instance)), ); info!("Using backend {} version {}", name, build_version); - }); + Ok(verifier_instance) + })); Verifier { env, verifier_wrapper, verifier_instance, + frontend_wrapper, + frontend_instance, jni, ast_utils, smt_manager, @@ -144,10 +195,13 @@ impl<'a> Verifier<'a> { ); } + let program_option = self.jni.new_option(Some(program.to_jobject())); + self.jni.unwrap_result(self.frontend_wrapper.call___program___dollar_eq(self.frontend_instance, program_option)); + run_timed!("Viper verification", debug, - let viper_result = self.jni.unwrap_result( - self.call_verify(program) - ); + self.jni.unwrap_result(self.frontend_wrapper.call_verification(self.frontend_instance)); + let viper_result_option = self.jni.unwrap_result(self.frontend_wrapper.call_getVerificationResult(self.frontend_instance)); + let viper_result = self.jni.unwrap_result(scala::Some::with(self.env).call_get(viper_result_option)); ); debug!( "Viper verification result: {}", diff --git a/vir/defs/polymorphic/ast/stmt.rs b/vir/defs/polymorphic/ast/stmt.rs index e6d25ce2434..39de9ff181b 100644 --- a/vir/defs/polymorphic/ast/stmt.rs +++ b/vir/defs/polymorphic/ast/stmt.rs @@ -21,6 +21,7 @@ pub enum Stmt { Inhale(Inhale), Exhale(Exhale), Assert(Assert), + Refute(Refute), /// MethodCall: method_name, args, targets MethodCall(MethodCall), /// Target, source, kind @@ -73,6 +74,7 @@ impl fmt::Display for Stmt { Stmt::Inhale(inhale) => inhale.fmt(f), Stmt::Exhale(exhale) => exhale.fmt(f), Stmt::Assert(assert) => assert.fmt(f), + Stmt::Refute(refute) => refute.fmt(f), Stmt::MethodCall(method_call) => method_call.fmt(f), Stmt::Assign(assign) => assign.fmt(f), Stmt::Fold(fold) => fold.fmt(f), @@ -161,12 +163,24 @@ pub struct Assert { pub position: Position, } +#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct Refute { + pub expr: Expr, + pub position: Position, +} + impl fmt::Display for Assert { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { write!(f, "assert {}", self.expr) } } +impl fmt::Display for Refute { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "refute {}", self.expr) + } +} + #[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct MethodCall { pub method_name: String, @@ -546,6 +560,7 @@ pub trait StmtFolder { Stmt::Inhale(inhale) => self.fold_inhale(inhale), Stmt::Exhale(exhale) => self.fold_exhale(exhale), Stmt::Assert(assert) => self.fold_assert(assert), + Stmt::Refute(refute) => self.fold_refute(refute), Stmt::MethodCall(method_call) => self.fold_method_call(method_call), Stmt::Assign(assign) => self.fold_assign(assign), Stmt::Fold(fold) => self.fold_fold(fold), @@ -599,6 +614,14 @@ pub trait StmtFolder { }) } + fn fold_refute(&mut self, statement: Refute) -> Stmt { + let Refute { expr, position } = statement; + Stmt::Refute(Refute { + expr: self.fold_expr(expr), + position, + }) + } + fn fold_method_call(&mut self, statement: MethodCall) -> Stmt { let MethodCall { method_name, @@ -750,6 +773,7 @@ pub trait FallibleStmtFolder { Stmt::Inhale(inhale) => self.fallible_fold_inhale(inhale), Stmt::Exhale(exhale) => self.fallible_fold_exhale(exhale), Stmt::Assert(assert) => self.fallible_fold_assert(assert), + Stmt::Refute(refute) => self.fallible_fold_refute(refute), Stmt::MethodCall(method_call) => self.fallible_fold_method_call(method_call), Stmt::Assign(assign) => self.fallible_fold_assign(assign), Stmt::Fold(fold) => self.fallible_fold_fold(fold), @@ -807,6 +831,14 @@ pub trait FallibleStmtFolder { })) } + fn fallible_fold_refute(&mut self, statement: Refute) -> Result { + let Refute { expr, position } = statement; + Ok(Stmt::Refute(Refute { + expr: self.fallible_fold_expr(expr)?, + position, + })) + } + fn fallible_fold_method_call(&mut self, statement: MethodCall) -> Result { let MethodCall { method_name, @@ -987,6 +1019,7 @@ pub trait StmtWalker { Stmt::Inhale(inhale) => self.walk_inhale(inhale), Stmt::Exhale(exhale) => self.walk_exhale(exhale), Stmt::Assert(assert) => self.walk_assert(assert), + Stmt::Refute(refute) => self.walk_refute(refute), Stmt::MethodCall(method_call) => self.walk_method_call(method_call), Stmt::Assign(assign) => self.walk_assign(assign), Stmt::Fold(fold) => self.walk_fold(fold), @@ -1028,6 +1061,11 @@ pub trait StmtWalker { self.walk_expr(expr); } + fn walk_refute(&mut self, statement: &Refute) { + let Refute { expr, .. } = statement; + self.walk_expr(expr); + } + fn walk_method_call(&mut self, statement: &MethodCall) { let MethodCall { arguments, targets, .. @@ -1137,6 +1175,7 @@ pub trait FallibleStmtWalker { Stmt::Inhale(inhale) => self.fallible_walk_inhale(inhale), Stmt::Exhale(exhale) => self.fallible_walk_exhale(exhale), Stmt::Assert(assert) => self.fallible_walk_assert(assert), + Stmt::Refute(refute) => self.fallible_walk_refute(refute), Stmt::MethodCall(method_call) => self.fallible_walk_method_call(method_call), Stmt::Assign(assign) => self.fallible_walk_assign(assign), Stmt::Fold(fold) => self.fallible_walk_fold(fold), @@ -1193,6 +1232,12 @@ pub trait FallibleStmtWalker { Ok(()) } + fn fallible_walk_refute(&mut self, statement: &Refute) -> Result<(), Self::Error> { + let Refute { expr, .. } = statement; + self.fallible_walk_expr(expr)?; + Ok(()) + } + fn fallible_walk_method_call(&mut self, statement: &MethodCall) -> Result<(), Self::Error> { let MethodCall { arguments, targets, .. diff --git a/vir/src/converter/polymorphic_to_legacy.rs b/vir/src/converter/polymorphic_to_legacy.rs index 912aa5de3f1..6d47a6bd0e3 100644 --- a/vir/src/converter/polymorphic_to_legacy.rs +++ b/vir/src/converter/polymorphic_to_legacy.rs @@ -599,6 +599,9 @@ impl From for legacy::Stmt { polymorphic::Stmt::Assert(assert) => { legacy::Stmt::Assert(assert.expr.into(), assert.position.into()) } + polymorphic::Stmt::Refute(refute) => { + legacy::Stmt::Refute(refute.expr.into(), refute.position.into()) + } polymorphic::Stmt::MethodCall(method_call) => legacy::Stmt::MethodCall( method_call.method_name, method_call diff --git a/vir/src/converter/type_substitution.rs b/vir/src/converter/type_substitution.rs index 24f2a36ef5e..d580d9e0900 100644 --- a/vir/src/converter/type_substitution.rs +++ b/vir/src/converter/type_substitution.rs @@ -522,6 +522,7 @@ impl Generic for Stmt { Stmt::Inhale(inhale) => Stmt::Inhale(inhale.substitute(map)), Stmt::Exhale(exhale) => Stmt::Exhale(exhale.substitute(map)), Stmt::Assert(assert) => Stmt::Assert(assert.substitute(map)), + Stmt::Refute(refute) => Stmt::Refute(refute.substitute(map)), Stmt::MethodCall(method_call) => Stmt::MethodCall(method_call.substitute(map)), Stmt::Assign(assign) => Stmt::Assign(assign.substitute(map)), Stmt::Fold(fold) => Stmt::Fold(fold.substitute(map)), @@ -594,6 +595,14 @@ impl Generic for Assert { } } +impl Generic for Refute { + fn substitute(self, map: &FxHashMap) -> Self { + let mut refute = self; + refute.expr = refute.expr.substitute(map); + refute + } +} + impl Generic for MethodCall { fn substitute(self, map: &FxHashMap) -> Self { let mut method_call = self; diff --git a/vir/src/legacy/ast/stmt.rs b/vir/src/legacy/ast/stmt.rs index d9bfaff4bf6..444bbe4988d 100644 --- a/vir/src/legacy/ast/stmt.rs +++ b/vir/src/legacy/ast/stmt.rs @@ -23,6 +23,7 @@ pub enum Stmt { Inhale(Expr), Exhale(Expr, Position), Assert(Expr, Position), + Refute(Expr, Position), /// MethodCall: method_name, args, targets MethodCall(String, Vec, Vec), /// Target, source, kind @@ -84,6 +85,7 @@ impl Hash for Stmt { Stmt::Inhale(e) => e.hash(state), Stmt::Exhale(e, p) => (e, p).hash(state), Stmt::Assert(e, p) => (e, p).hash(state), + Stmt::Refute(e, p) => (e, p).hash(state), Stmt::MethodCall(s, v1, v2) => (s, v1, v2).hash(state), Stmt::Assign(e1, e2, ak) => (e1, e2, ak).hash(state), Stmt::Fold(s, v, pa, mevi, p) => (s, v, pa, mevi, p).hash(state), @@ -133,6 +135,9 @@ impl fmt::Display for Stmt { Stmt::Assert(ref expr, _) => { write!(f, "assert {expr}") } + Stmt::Refute(ref expr, _) => { + write!(f, "refute {expr}") + } Stmt::MethodCall(ref name, ref args, ref vars) => write!( f, "{} := {}({})", @@ -298,6 +303,7 @@ impl Stmt { match self { Stmt::Exhale(_, ref p) | Stmt::Assert(_, ref p) + | Stmt::Refute(_, ref p) | Stmt::Fold(_, _, _, _, ref p) | Stmt::Obtain(_, ref p) | Stmt::PackageMagicWand(_, _, _, _, ref p) @@ -310,6 +316,7 @@ impl Stmt { match self { Stmt::Exhale(_, ref mut p) | Stmt::Assert(_, ref mut p) + | Stmt::Refute(_, ref mut p) | Stmt::Fold(_, _, _, _, ref mut p) | Stmt::Obtain(_, ref mut p) | Stmt::PackageMagicWand(_, _, _, _, ref mut p) @@ -379,6 +386,7 @@ pub trait StmtFolder { Stmt::Inhale(expr) => self.fold_inhale(expr), Stmt::Exhale(e, p) => self.fold_exhale(e, p), Stmt::Assert(expr, pos) => self.fold_assert(expr, pos), + Stmt::Refute(expr, pos) => self.fold_refute(expr, pos), Stmt::MethodCall(s, ve, vv) => self.fold_method_call(s, ve, vv), Stmt::Assign(p, e, k) => self.fold_assign(p, e, k), Stmt::Fold(s, ve, perm, variant, p) => self.fold_fold(s, ve, perm, variant, p), @@ -419,6 +427,10 @@ pub trait StmtFolder { Stmt::Assert(self.fold_expr(expr), pos) } + fn fold_refute(&mut self, expr: Expr, pos: Position) -> Stmt { + Stmt::Refute(self.fold_expr(expr), pos) + } + fn fold_method_call(&mut self, name: String, args: Vec, targets: Vec) -> Stmt { Stmt::MethodCall( name, @@ -527,6 +539,7 @@ pub trait FallibleStmtFolder { Stmt::Inhale(expr) => self.fallible_fold_inhale(expr), Stmt::Exhale(e, p) => self.fallible_fold_exhale(e, p), Stmt::Assert(expr, pos) => self.fallible_fold_assert(expr, pos), + Stmt::Refute(expr, pos) => self.fallible_fold_refute(expr, pos), Stmt::MethodCall(s, ve, vv) => self.fallible_fold_method_call(s, ve, vv), Stmt::Assign(p, e, k) => self.fallible_fold_assign(p, e, k), Stmt::Fold(s, ve, perm, variant, p) => self.fallible_fold_fold(s, ve, perm, variant, p), @@ -569,6 +582,10 @@ pub trait FallibleStmtFolder { Ok(Stmt::Assert(self.fallible_fold_expr(expr)?, pos)) } + fn fallible_fold_refute(&mut self, expr: Expr, pos: Position) -> Result { + Ok(Stmt::Refute(self.fallible_fold_expr(expr)?, pos)) + } + fn fallible_fold_method_call( &mut self, name: String, @@ -719,6 +736,7 @@ pub trait StmtWalker { Stmt::Inhale(expr) => self.walk_inhale(expr), Stmt::Exhale(e, p) => self.walk_exhale(e, p), Stmt::Assert(expr, pos) => self.walk_assert(expr, pos), + Stmt::Refute(expr, pos) => self.walk_refute(expr, pos), Stmt::MethodCall(s, ve, vv) => self.walk_method_call(s, ve, vv), Stmt::Assign(p, e, k) => self.walk_assign(p, e, k), Stmt::Fold(s, ve, perm, variant, pos) => self.walk_fold(s, ve, perm, variant, pos), @@ -755,6 +773,10 @@ pub trait StmtWalker { self.walk_expr(expr); } + fn walk_refute(&mut self, expr: &Expr, _pos: &Position) { + self.walk_expr(expr); + } + fn walk_method_call(&mut self, _method_name: &str, args: &[Expr], targets: &[LocalVar]) { for arg in args { self.walk_expr(arg);