From 9ac293b1fb67f191006cff22050afd80a423e4e0 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <shrabec@student.ethz.ch> Date: Tue, 7 Feb 2023 00:35:12 +0900 Subject: [PATCH 01/33] Add prusti_refute! macro --- 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 +++++++ .../src/encoder/errors/error_manager.rs | 2 + .../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 | 3 ++ viper/src/ast_factory/statement.rs | 21 +++++++++ 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 +++++++++ 19 files changed, 232 insertions(+), 3 deletions(-) diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index f09d9dc9062..161a6a26569 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -177,6 +177,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 2edd74c80cc..a65d08efb63 100644 --- a/prusti-contracts/prusti-contracts-proc-macros/src/lib.rs +++ b/prusti-contracts/prusti-contracts-proc-macros/src/lib.rs @@ -64,6 +64,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 { @@ -183,6 +189,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 6fe66caae8f..43597b102b8 100644 --- a/prusti-contracts/prusti-contracts/src/lib.rs +++ b/prusti-contracts/prusti-contracts/src/lib.rs @@ -30,6 +30,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 e2387b80582..80d91e4cb0d 100644 --- a/prusti-contracts/prusti-specs/src/lib.rs +++ b/prusti-contracts/prusti-specs/src/lib.rs @@ -409,6 +409,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 e1dced3a032..994fa867c51 100644 --- a/prusti-contracts/prusti-specs/src/rewriter.rs +++ b/prusti-contracts/prusti-specs/src/rewriter.rs @@ -225,6 +225,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<TokenStream> { + 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 f959a2566a9..2356e0585f0 100644 --- a/prusti-interface/src/specs/mod.rs +++ b/prusti-interface/src/specs/mod.rs @@ -80,6 +80,7 @@ pub struct SpecCollector<'a, 'tcx> { type_specs: HashMap<LocalDefId, TypeSpecRefs>, prusti_assertions: Vec<LocalDefId>, prusti_assumptions: Vec<LocalDefId>, + prusti_refutations: Vec<LocalDefId>, ghost_begin: Vec<LocalDefId>, ghost_end: Vec<LocalDefId>, } @@ -96,6 +97,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { type_specs: HashMap::new(), prusti_assertions: vec![], prusti_assumptions: vec![], + prusti_refutations: vec![], ghost_begin: vec![], ghost_end: vec![], } @@ -109,6 +111,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 @@ -269,6 +272,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( @@ -477,6 +490,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 d1fcefa526f..5c3c36ac3b8 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -18,6 +18,7 @@ pub struct DefSpecificationMap { pub type_specs: FxHashMap<DefId, TypeSpecification>, pub prusti_assertions: FxHashMap<DefId, PrustiAssertion>, pub prusti_assumptions: FxHashMap<DefId, PrustiAssumption>, + pub prusti_refutations: FxHashMap<DefId, PrustiRefutation>, pub ghost_begin: FxHashMap<DefId, GhostBegin>, pub ghost_end: FxHashMap<DefId, GhostEnd>, } @@ -47,6 +48,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) } @@ -167,12 +172,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(); @@ -291,6 +302,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-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 9ad741859fe..fd19eb37c28 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -24,6 +24,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!() diff --git a/prusti-viper/src/encoder/foldunfold/requirements.rs b/prusti-viper/src/encoder/foldunfold/requirements.rs index bbb5c96d099..b75e9c77757 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 50bdf995694..76c6e291ec4 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 87c88c29917..e4b4d93e1ce 100644 --- a/prusti-viper/src/encoder/mir/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/specifications/interface.rs @@ -98,6 +98,9 @@ pub(crate) trait SpecificationsInterface<'tcx> { /// Get the prusti assumption fn get_prusti_assumption(&self, def_id: DefId) -> Option<typed::PrustiAssumption>; + /// Get the prusti refutation + fn get_prusti_refutation(&self, def_id: DefId) -> Option<typed::PrustiRefutation>; + /// Get the begin marker of the ghost block fn get_ghost_begin(&self, def_id: DefId) -> Option<typed::GhostBegin>; @@ -241,6 +244,14 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode .cloned() } + fn get_prusti_refutation(&self, def_id: DefId) -> Option<typed::PrustiRefutation> { + self.specifications_state + .specs + .borrow() + .get_refutation(&def_id) + .cloned() + } + fn get_ghost_begin(&self, def_id: DefId) -> Option<typed::GhostBegin> { 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 acc47eafd9a..02faf674b8f 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, Refinable, SpecificationItem, TypeSpecification, PrustiRefutation, }, PrustiError, }; @@ -91,6 +91,11 @@ impl<'tcx> Specifications<'tcx> { self.user_typed_specs.get_assumption(def_id) } + pub(super) fn get_refutation(&self, def_id: &DefId) -> Option<&PrustiRefutation> { + trace!("Get refutation specs of {:?}", def_id); + self.user_typed_specs.get_refutation(def_id) + } + pub(super) fn get_ghost_begin(&self, def_id: &DefId) -> Option<&GhostBegin> { trace!("Get begin ghost block specs of {:?}", def_id); 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 07903f0084f..b3ef7012f2b 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -221,7 +221,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(()) } @@ -294,6 +295,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<vir::Stmt>, + ) -> SpannedEncodingResult<bool> { + 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.to_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 44fab0c2ea2..9e000e99d7a 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -198,6 +198,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..ace101842be 100644 --- a/viper/src/ast_factory/statement.rs +++ b/viper/src/ast_factory/statement.rs @@ -8,6 +8,7 @@ use crate::ast_factory::{ }; use jni::objects::JObject; use viper_sys::wrappers::viper::silver::ast; +use viper_sys::wrappers::viper::silver::plugin::standard::refute; impl<'a> AstFactory<'a> { pub fn new_stmt(&self, lhs: Expr, fields: &[Field]) -> Stmt<'a> { @@ -133,6 +134,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 +154,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/vir/defs/polymorphic/ast/stmt.rs b/vir/defs/polymorphic/ast/stmt.rs index 694ff64b7c8..43b9727bdaa 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, @@ -542,6 +556,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), @@ -595,6 +610,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, @@ -746,6 +769,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), @@ -803,6 +827,14 @@ pub trait FallibleStmtFolder { })) } + fn fallible_fold_refute(&mut self, statement: Refute) -> Result<Stmt, Self::Error> { + 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<Stmt, Self::Error> { let MethodCall { method_name, @@ -983,6 +1015,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), @@ -1024,6 +1057,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, .. @@ -1133,6 +1171,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), @@ -1189,6 +1228,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 d2215f9645c..ea9f81fad8a 100644 --- a/vir/src/converter/polymorphic_to_legacy.rs +++ b/vir/src/converter/polymorphic_to_legacy.rs @@ -567,6 +567,9 @@ impl From<polymorphic::Stmt> 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 4c0cd4d451a..009ec0c1deb 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<TypeVar, Type>) -> Self { + let mut refute = self; + refute.expr = refute.expr.substitute(map); + refute + } +} + impl Generic for MethodCall { fn substitute(self, map: &FxHashMap<TypeVar, Type>) -> Self { let mut method_call = self; diff --git a/vir/src/legacy/ast/stmt.rs b/vir/src/legacy/ast/stmt.rs index 3317170256a..23590248e4d 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<Expr>, Vec<LocalVar>), /// 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, "{} := {}({})", @@ -300,6 +305,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) @@ -312,6 +318,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) @@ -381,6 +388,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), @@ -421,6 +429,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<Expr>, targets: Vec<LocalVar>) -> Stmt { Stmt::MethodCall( name, @@ -529,6 +541,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), @@ -571,6 +584,10 @@ pub trait FallibleStmtFolder { Ok(Stmt::Assert(self.fallible_fold_expr(expr)?, pos)) } + fn fallible_fold_refute(&mut self, expr: Expr, pos: Position) -> Result<Stmt, Self::Error> { + Ok(Stmt::Refute(self.fallible_fold_expr(expr)?, pos)) + } + fn fallible_fold_method_call( &mut self, name: String, @@ -721,6 +738,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), @@ -757,6 +775,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); From c49f9a76ef1e53efecce4cf5537c5bccddf29971 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <shrabec@student.ethz.ch> Date: Tue, 21 Feb 2023 17:10:58 +0900 Subject: [PATCH 02/33] Add macro to generate getters/setters for fields via JNI --- jni-gen/src/generators/class.rs | 8 +- jni-gen/src/generators/field_getter_setter.rs | 126 ++++++++++++++++++ jni-gen/src/generators/method.rs | 18 ++- jni-gen/src/generators/mod.rs | 1 + jni-gen/src/utils.rs | 13 +- jni-gen/src/wrapper_spec.rs | 14 ++ 6 files changed, 162 insertions(+), 18 deletions(-) create mode 100644 jni-gen/src/generators/field_getter_setter.rs diff --git a/jni-gen/src/generators/class.rs b/jni-gen/src/generators/class.rs index 1a74c26683f..1c09f88aef8 100644 --- a/jni-gen/src/generators/class.rs +++ b/jni-gen/src/generators/class.rs @@ -7,7 +7,7 @@ use crate::{ class_name::*, errors::*, - generators::{constructor::*, method::*, scala_object_getter::*}, + generators::{constructor::*, method::*, scala_object_getter::*, field_getter_setter::*}, wrapper_spec::*, }; use jni::JNIEnv; @@ -130,6 +130,12 @@ impl<'a> ClassGenerator<'a> { signature.clone(), suffix.clone(), )?, + ItemWrapperSpec::FieldGetterSetter { + ref field_name, + ref signature, + } => { + generate_field_getter_setter(self.env, &self.class, field_name, signature)? + } }; gen_items.push(gen) } diff --git a/jni-gen/src/generators/field_getter_setter.rs b/jni-gen/src/generators/field_getter_setter.rs new file mode 100644 index 00000000000..78d62adf15e --- /dev/null +++ b/jni-gen/src/generators/field_getter_setter.rs @@ -0,0 +1,126 @@ +// © 2019, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use crate::{class_name::*, errors::*, utils::*}; +use jni::JNIEnv; + +fn generate_type_check(type_signature: &str, type_name: &str, prefix: &str) -> String { + let type_class = &type_signature[1..(type_signature.len() - 1)]; + vec![ + " debug_assert!(".to_string(), + " self.env.is_instance_of(".to_string(), + format!(" {},", type_name), + format!(" self.env.find_class(\"{}\")?,", type_class), + " )?".to_string(), + " );".to_string(), + ].iter().map(|x| format!("{}{}", prefix, x)).collect::<Vec<_>>().join("\n") +} + +fn generate_result_type_check(return_signature: &str) -> String { + vec![ + " if let Ok(result) = result {".to_string(), + generate_type_check(return_signature, "result", " "), + " }".to_string(), + "".to_string(), + ].join("\n") +} + +fn generate_parameter_type_check(type_signature: &str, type_name: &str) -> String { + generate_type_check(type_signature, type_name, "")+"\n" +} + +fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signature: &str) -> String { + let rust_getter_name = format!("call_getter_{}", java_identifier_to_rust(field_name)); + let parameter_type = generate_jni_type(type_signature); + + vec![ + format!("/// Returns the field `{}` of the scala class `{}`.", field_name, class_name.full_name()), + "///".to_string(), + format!("/// Return type and Java signature: `{}` (`{}`)", parameter_type, type_signature), + format!("pub fn {rust_getter_name}("), + " &self,".to_string(), + " receiver: JObject<'a>,".to_string(), + ") -> JNIResult<JObject> {".to_string(), + format!(" let class_name = \"{}\";", class_name.path()), + format!(" let field_name = \"{}\";", field_name), + format!(" let return_signature = \"{}\";", type_signature), + "".to_string(), + " debug_assert!(".to_string(), + " self.env.is_instance_of(".to_string(), + " receiver,".to_string(), + " self.env.find_class(class_name)?,".to_string(), + " )?".to_string(), + " );".to_string(), + "".to_string(), + " let result = self.env.get_field(".to_string(), + " receiver,".to_string(), + " field_name,".to_string(), + " return_signature,".to_string(), + format!(" ).and_then(|x| x.{}());", generate_jni_type_char(&type_signature)), + "".to_string(), + if type_signature.starts_with('L') {generate_result_type_check(&type_signature)} else {"".to_string()}, + " result".to_string(), + "}".to_string(), + ] + .join("\n")+"\n" +} + +fn generate_field_setter(class_name: &ClassName, field_name: &str, type_signature: &str) -> String { + let rust_setter_name = format!("call_setter_{}", java_identifier_to_rust(field_name)); + let parameter_name = format!("new_{}", field_name); + let parameter_type = generate_jni_type(type_signature); + + vec![ + format!("/// Sets the field `{}` of the scala class `{}`.", field_name, class_name.full_name()), + "///".to_string(), + "/// Type and Java signature of parameters:".to_string(), + "///".to_string(), + format!("/// - `{}`: `{}` (`{}`)", parameter_name, parameter_type, type_signature), + "/// ".to_string(), + "/// Return type and Java signature: `()` (`V`)".to_string(), + format!("pub fn {rust_setter_name}("), + " &self,".to_string(), + " receiver: JObject<'a>,".to_string(), + format!(" {}: {},", parameter_name, parameter_type), + ") -> JNIResult<()> {".to_string(), + format!(" let class_name = \"{}\";", class_name.path()), + format!(" let field_name = \"{}\";", field_name), + format!(" let return_signature = \"{}\";", type_signature), + "".to_string(), + " debug_assert!(".to_string(), + " self.env.is_instance_of(".to_string(), + " receiver,".to_string(), + " self.env.find_class(class_name)?,".to_string(), + " )?".to_string(), + " );".to_string(), + "".to_string(), + if type_signature.starts_with('L') {generate_parameter_type_check(&type_signature, ¶meter_name)} else {"".to_string()}, + " let result = self.env.set_field(".to_string(), + " receiver,".to_string(), + " field_name,".to_string(), + " return_signature,".to_string(), + format!(" JValue::from({})", parameter_name), + " );".to_string(), + "".to_string(), + " result".to_string(), + "}".to_string(), + ] + .join("\n")+"\n" +} + +pub fn generate_field_getter_setter(env: &JNIEnv, class_name: &ClassName, field_name: &str, type_signature: &str) -> Result<String> { + env.get_field_id( + class_name.path(), + field_name, + type_signature, + ) + .map(|_| ())?; + + let setter_code = generate_field_getter(class_name, field_name, type_signature); + let getter_code = generate_field_setter(class_name, field_name, type_signature); + + Ok(format!("{}\n{}", setter_code, getter_code)) +} diff --git a/jni-gen/src/generators/method.rs b/jni-gen/src/generators/method.rs index a110d9ae788..709c6a96d2f 100644 --- a/jni-gen/src/generators/method.rs +++ b/jni-gen/src/generators/method.rs @@ -147,8 +147,8 @@ pub fn generate_method( } let rust_method_name = match suffix { - None => format!("call_{}", java_method_to_rust(method_name)), - Some(s) => format!("call_{}_{}", java_method_to_rust(method_name), s), + None => format!("call_{}", java_identifier_to_rust(method_name)), + Some(s) => format!("call_{}_{}", java_identifier_to_rust(method_name), s), }; if is_static { @@ -190,9 +190,12 @@ fn generate( method_name, class.full_name() )); - code.push("///".to_string()); - code.push("/// Type and Java signature of parameters:".to_string()); - code.push("///".to_string()); + + if !parameter_names.is_empty() { + code.push("///".to_string()); + code.push("/// Type and Java signature of parameters:".to_string()); + code.push("///".to_string()); + } for i in 0..parameter_names.len() { let par_name = ¶meter_names[i]; @@ -451,8 +454,3 @@ fn generate_static( code.join("\n") + "\n" } - -fn java_method_to_rust(method_name: &str) -> String { - method_name.replace('_', "__").replace('$', "_dollar_") - // If needed, replace other charachters with "_{something}_" -} diff --git a/jni-gen/src/generators/mod.rs b/jni-gen/src/generators/mod.rs index 417ac6e7443..48008fa73ea 100644 --- a/jni-gen/src/generators/mod.rs +++ b/jni-gen/src/generators/mod.rs @@ -9,3 +9,4 @@ mod constructor; mod method; pub mod module; mod scala_object_getter; +mod field_getter_setter; diff --git a/jni-gen/src/utils.rs b/jni-gen/src/utils.rs index 5af7330b5de..a7b64f50e83 100644 --- a/jni-gen/src/utils.rs +++ b/jni-gen/src/utils.rs @@ -72,11 +72,10 @@ pub fn java_str_to_string(string: &JavaStr) -> Result<String> { } pub fn java_str_to_valid_rust_argument_name(string: &JavaStr) -> Result<String> { - let mut res = "arg_".to_string(); - res.push_str( - &java_str_to_string(string)? - .replace('_', "___") - .replace('$', "_d_"), - ); - Ok(res) + Ok(format!("arg_{}", java_identifier_to_rust(&java_str_to_string(string)?))) } + +pub fn java_identifier_to_rust(name: &str) -> String { + // identifier can only be composed of [a-zA-Z&_] characters - https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8 + name.replace('_', "__").replace('$', "_dollar_") +} \ No newline at end of file diff --git a/jni-gen/src/wrapper_spec.rs b/jni-gen/src/wrapper_spec.rs index c80a7676d1f..eb187175512 100644 --- a/jni-gen/src/wrapper_spec.rs +++ b/jni-gen/src/wrapper_spec.rs @@ -41,6 +41,10 @@ pub enum ItemWrapperSpec { signature: Option<String>, suffix: Option<String>, }, + FieldGetterSetter { + field_name: String, + signature: String, + }, } #[macro_export] @@ -106,3 +110,13 @@ macro_rules! method { } }; } + +#[macro_export] +macro_rules! field_getter_setter { + ($name:expr, $signature:expr) => { + ItemWrapperSpec::FieldGetterSetter { + field_name: $name.into(), + signature: $signature.into(), + } + }; +} From 6c3d955e2c749bcac88f9b87fc5bb10b33e50ac1 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <shrabec@student.ethz.ch> Date: Wed, 22 Feb 2023 03:48:25 +0900 Subject: [PATCH 03/33] Resolve fmt-check and clippy errors, simplify naming, small refactoring --- jni-gen/src/generators/class.rs | 6 +- jni-gen/src/generators/field_getter_setter.rs | 114 +++++++++++------- jni-gen/src/utils.rs | 7 +- jni-gen/src/wrapper_spec.rs | 2 +- 4 files changed, 80 insertions(+), 49 deletions(-) diff --git a/jni-gen/src/generators/class.rs b/jni-gen/src/generators/class.rs index 1c09f88aef8..7f303b2b909 100644 --- a/jni-gen/src/generators/class.rs +++ b/jni-gen/src/generators/class.rs @@ -7,7 +7,7 @@ use crate::{ class_name::*, errors::*, - generators::{constructor::*, method::*, scala_object_getter::*, field_getter_setter::*}, + generators::{constructor::*, field_getter_setter::*, method::*, scala_object_getter::*}, wrapper_spec::*, }; use jni::JNIEnv; @@ -133,9 +133,7 @@ impl<'a> ClassGenerator<'a> { ItemWrapperSpec::FieldGetterSetter { ref field_name, ref signature, - } => { - generate_field_getter_setter(self.env, &self.class, field_name, signature)? - } + } => generate_field_getter_setter(self.env, &self.class, field_name, signature)?, }; gen_items.push(gen) } diff --git a/jni-gen/src/generators/field_getter_setter.rs b/jni-gen/src/generators/field_getter_setter.rs index 78d62adf15e..2df48f64df1 100644 --- a/jni-gen/src/generators/field_getter_setter.rs +++ b/jni-gen/src/generators/field_getter_setter.rs @@ -7,46 +7,68 @@ use crate::{class_name::*, errors::*, utils::*}; use jni::JNIEnv; -fn generate_type_check(type_signature: &str, type_name: &str, prefix: &str) -> String { +fn generate_type_check(type_signature: &str, type_name: &str, is_result: bool) -> String { + if !type_signature.starts_with('L') { + return "".to_string(); + } + let type_class = &type_signature[1..(type_signature.len() - 1)]; - vec![ + + let type_check = vec![ " debug_assert!(".to_string(), " self.env.is_instance_of(".to_string(), - format!(" {},", type_name), - format!(" self.env.find_class(\"{}\")?,", type_class), + format!(" {type_name},"), + format!(" self.env.find_class(\"{type_class}\")?,"), " )?".to_string(), " );".to_string(), - ].iter().map(|x| format!("{}{}", prefix, x)).collect::<Vec<_>>().join("\n") + ]; + + if is_result { + let indented_type_check = type_check + .iter() + .map(|x| format!(" {x}")) + .collect::<Vec<_>>() + .join("\n"); + + vec![ + " if let Ok(result) = result {".to_string(), + indented_type_check, + " }".to_string(), + ] + } else { + type_check + } + .join("\n") + + "\n" } fn generate_result_type_check(return_signature: &str) -> String { - vec![ - " if let Ok(result) = result {".to_string(), - generate_type_check(return_signature, "result", " "), - " }".to_string(), - "".to_string(), - ].join("\n") + generate_type_check(return_signature, "result", true) } fn generate_parameter_type_check(type_signature: &str, type_name: &str) -> String { - generate_type_check(type_signature, type_name, "")+"\n" + generate_type_check(type_signature, type_name, false) } fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signature: &str) -> String { - let rust_getter_name = format!("call_getter_{}", java_identifier_to_rust(field_name)); + let rust_getter_name = format!("get_{}", java_identifier_to_rust(field_name)); let parameter_type = generate_jni_type(type_signature); vec![ - format!("/// Returns the field `{}` of the scala class `{}`.", field_name, class_name.full_name()), + format!( + "/// Returns the field `{}` of the scala class `{}`.", + field_name, + class_name.full_name() + ), "///".to_string(), - format!("/// Return type and Java signature: `{}` (`{}`)", parameter_type, type_signature), + format!("/// Return type and Java signature: `{parameter_type}` (`{type_signature}`)"), format!("pub fn {rust_getter_name}("), " &self,".to_string(), " receiver: JObject<'a>,".to_string(), ") -> JNIResult<JObject> {".to_string(), format!(" let class_name = \"{}\";", class_name.path()), - format!(" let field_name = \"{}\";", field_name), - format!(" let return_signature = \"{}\";", type_signature), + format!(" let field_name = \"{field_name}\";"), + format!(" let return_signature = \"{type_signature}\";"), "".to_string(), " debug_assert!(".to_string(), " self.env.is_instance_of(".to_string(), @@ -59,36 +81,44 @@ fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signatur " receiver,".to_string(), " field_name,".to_string(), " return_signature,".to_string(), - format!(" ).and_then(|x| x.{}());", generate_jni_type_char(&type_signature)), + format!( + " ).and_then(|x| x.{}());", + generate_jni_type_char(type_signature) + ), "".to_string(), - if type_signature.starts_with('L') {generate_result_type_check(&type_signature)} else {"".to_string()}, + generate_result_type_check(type_signature), " result".to_string(), "}".to_string(), ] - .join("\n")+"\n" + .join("\n") + + "\n" } fn generate_field_setter(class_name: &ClassName, field_name: &str, type_signature: &str) -> String { - let rust_setter_name = format!("call_setter_{}", java_identifier_to_rust(field_name)); - let parameter_name = format!("new_{}", field_name); + let rust_setter_name = format!("set_{}", java_identifier_to_rust(field_name)); + let parameter_name = format!("new_{field_name}"); let parameter_type = generate_jni_type(type_signature); vec![ - format!("/// Sets the field `{}` of the scala class `{}`.", field_name, class_name.full_name()), + format!( + "/// Sets the field `{}` of the scala class `{}`.", + field_name, + class_name.full_name() + ), "///".to_string(), "/// Type and Java signature of parameters:".to_string(), "///".to_string(), - format!("/// - `{}`: `{}` (`{}`)", parameter_name, parameter_type, type_signature), + format!("/// - `{parameter_name}`: `{parameter_type}` (`{type_signature}`)"), "/// ".to_string(), "/// Return type and Java signature: `()` (`V`)".to_string(), format!("pub fn {rust_setter_name}("), " &self,".to_string(), " receiver: JObject<'a>,".to_string(), - format!(" {}: {},", parameter_name, parameter_type), + format!(" {parameter_name}: {parameter_type},"), ") -> JNIResult<()> {".to_string(), format!(" let class_name = \"{}\";", class_name.path()), - format!(" let field_name = \"{}\";", field_name), - format!(" let return_signature = \"{}\";", type_signature), + format!(" let field_name = \"{field_name}\";"), + format!(" let return_signature = \"{type_signature}\";"), "".to_string(), " debug_assert!(".to_string(), " self.env.is_instance_of(".to_string(), @@ -97,30 +127,30 @@ fn generate_field_setter(class_name: &ClassName, field_name: &str, type_signatur " )?".to_string(), " );".to_string(), "".to_string(), - if type_signature.starts_with('L') {generate_parameter_type_check(&type_signature, ¶meter_name)} else {"".to_string()}, - " let result = self.env.set_field(".to_string(), + generate_parameter_type_check(type_signature, ¶meter_name), + " self.env.set_field(".to_string(), " receiver,".to_string(), " field_name,".to_string(), " return_signature,".to_string(), - format!(" JValue::from({})", parameter_name), - " );".to_string(), - "".to_string(), - " result".to_string(), + format!(" JValue::from({parameter_name})"), + " )".to_string(), "}".to_string(), ] - .join("\n")+"\n" + .join("\n") + + "\n" } -pub fn generate_field_getter_setter(env: &JNIEnv, class_name: &ClassName, field_name: &str, type_signature: &str) -> Result<String> { - env.get_field_id( - class_name.path(), - field_name, - type_signature, - ) - .map(|_| ())?; +pub fn generate_field_getter_setter( + env: &JNIEnv, + class_name: &ClassName, + field_name: &str, + type_signature: &str, +) -> Result<String> { + env.get_field_id(class_name.path(), field_name, type_signature) + .map(|_| ())?; let setter_code = generate_field_getter(class_name, field_name, type_signature); let getter_code = generate_field_setter(class_name, field_name, type_signature); - Ok(format!("{}\n{}", setter_code, getter_code)) + Ok(format!("{setter_code}\n{getter_code}")) } diff --git a/jni-gen/src/utils.rs b/jni-gen/src/utils.rs index a7b64f50e83..beefc773ba1 100644 --- a/jni-gen/src/utils.rs +++ b/jni-gen/src/utils.rs @@ -72,10 +72,13 @@ pub fn java_str_to_string(string: &JavaStr) -> Result<String> { } pub fn java_str_to_valid_rust_argument_name(string: &JavaStr) -> Result<String> { - Ok(format!("arg_{}", java_identifier_to_rust(&java_str_to_string(string)?))) + Ok(format!( + "arg_{}", + java_identifier_to_rust(&java_str_to_string(string)?) + )) } pub fn java_identifier_to_rust(name: &str) -> String { // identifier can only be composed of [a-zA-Z&_] characters - https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8 name.replace('_', "__").replace('$', "_dollar_") -} \ No newline at end of file +} diff --git a/jni-gen/src/wrapper_spec.rs b/jni-gen/src/wrapper_spec.rs index eb187175512..0d2c22e97fb 100644 --- a/jni-gen/src/wrapper_spec.rs +++ b/jni-gen/src/wrapper_spec.rs @@ -112,7 +112,7 @@ macro_rules! method { } #[macro_export] -macro_rules! field_getter_setter { +macro_rules! field { ($name:expr, $signature:expr) => { ItemWrapperSpec::FieldGetterSetter { field_name: $name.into(), From a896d5a422bc37e32eae9c997cff56b501660531 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <shrabec@student.ethz.ch> Date: Sun, 26 Feb 2023 15:27:53 +0900 Subject: [PATCH 04/33] Add test for field! macro --- jni-gen/src/generators/field_getter_setter.rs | 2 +- jni-gen/systest/build.rs | 20 +++++---- jni-gen/systest/tests/jvm_builtin_classes.rs | 45 +++++++++++++++++++ 3 files changed, 58 insertions(+), 9 deletions(-) diff --git a/jni-gen/src/generators/field_getter_setter.rs b/jni-gen/src/generators/field_getter_setter.rs index 2df48f64df1..e0f7a4ddf60 100644 --- a/jni-gen/src/generators/field_getter_setter.rs +++ b/jni-gen/src/generators/field_getter_setter.rs @@ -65,7 +65,7 @@ fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signatur format!("pub fn {rust_getter_name}("), " &self,".to_string(), " receiver: JObject<'a>,".to_string(), - ") -> JNIResult<JObject> {".to_string(), + format!(") -> JNIResult<{parameter_type}> {{"), format!(" let class_name = \"{}\";", class_name.path()), format!(" let field_name = \"{field_name}\";"), format!(" let return_signature = \"{type_signature}\";"), diff --git a/jni-gen/systest/build.rs b/jni-gen/systest/build.rs index 22ed1d9c12a..0e4b382dc88 100644 --- a/jni-gen/systest/build.rs +++ b/jni-gen/systest/build.rs @@ -28,14 +28,18 @@ fn main() { .use_jar(&asm_jar) .wrap(java_class!("java.lang.Object")) .wrap_all(vec![ - java_class!("java.lang.Integer", vec![constructor!("(I)V")]), - java_class!( - "java.util.Arrays", - vec![method!( - "binarySearch", - "([Ljava/lang/Object;Ljava/lang/Object;)I" - ),] - ), + java_class!("java.lang.Integer", vec![ + constructor!("(I)V"), + field!("value", "I") + ]), + java_class!("java.util.Arrays", vec![ + method!("binarySearch", "([Ljava/lang/Object;Ljava/lang/Object;)I"), + ]), + java_class!("java.lang.Error", vec![ + constructor!("(Ljava/lang/String;)V"), + method!("getMessage"), + field!("detailMessage", "Ljava/lang/String;"), + ]), ]) .generate(&generated_dir) .unwrap_or_else(|e| { diff --git a/jni-gen/systest/tests/jvm_builtin_classes.rs b/jni-gen/systest/tests/jvm_builtin_classes.rs index c1ad07848d4..b6f0fc962e8 100644 --- a/jni-gen/systest/tests/jvm_builtin_classes.rs +++ b/jni-gen/systest/tests/jvm_builtin_classes.rs @@ -2,9 +2,20 @@ use jni::objects::JObject; use jni::InitArgsBuilder; use jni::JNIVersion; use jni::JavaVM; +use jni::JNIEnv; +use jni::objects::JString; +use jni::errors::Result as JNIResult; use systest::print_exception; use systest::wrappers::*; +fn string_to_jobject<'a>(env: &JNIEnv<'a>, string: &str) -> JNIResult<JObject<'a>> { + Ok(JObject::from(env.new_string(string.to_owned())?)) +} + +fn jobject_to_string<'a>(env: &JNIEnv<'a>, obj: JObject) -> JNIResult<String> { + Ok(String::from(env.get_string(JString::from(obj))?)) +} + #[test] fn test_jvm_builtin_classes() { let jvm_args = InitArgsBuilder::new() @@ -52,4 +63,38 @@ fn test_jvm_builtin_classes() { }); } } + + for int_value in -10..10 { + env.with_local_frame(16, || { + let integer_value = java::lang::Integer::with(&env).new(int_value)?; + assert!(java::lang::Integer::with(&env).get_value(integer_value)? == int_value); + let new_wal = int_value + 2; + java::lang::Integer::with(&env).set_value(integer_value, new_wal)?; + assert!(java::lang::Integer::with(&env).get_value(integer_value)? == new_wal); + + Ok(JObject::null()) + }).unwrap_or_else(|e| { + print_exception(&env); + panic!("{} source: {:?}", e, std::error::Error::source(&e)); + }); + } + + env.with_local_frame(16, || { + let error_wrapper = java::lang::Error::with(&env); + + // Initalize error and check its content + let innitial_message = "First error message".to_string(); + let error = error_wrapper.new(string_to_jobject(&env, &innitial_message)?)?; + assert!(jobject_to_string(&env, error_wrapper.get_detailMessage(error)?)? == innitial_message); + + // Update the error object and check that the content has changed accordingly + let another_message = "Second message".to_string(); + error_wrapper.set_detailMessage(error, string_to_jobject(&env, &another_message)?)?; + assert!(jobject_to_string(&env, error_wrapper.get_detailMessage(error)?)? == another_message); + + Ok(JObject::null()) + }).unwrap_or_else(|e| { + print_exception(&env); + panic!("{} source: {:?}", e, std::error::Error::source(&e)); + }); } From ec17da5e7f8ccc12168750e0d19df8e4f437f6e0 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <shrabec@student.ethz.ch> Date: Sun, 26 Feb 2023 17:16:07 +0900 Subject: [PATCH 05/33] Update field! macro to not ask for signature (WIP) --- jni-gen/src/generators/class.rs | 7 +++---- jni-gen/src/generators/field_getter_setter.rs | 19 +++++++++++++++---- jni-gen/src/wrapper_spec.rs | 4 +--- jni-gen/systest/build.rs | 4 ++-- 4 files changed, 21 insertions(+), 13 deletions(-) diff --git a/jni-gen/src/generators/class.rs b/jni-gen/src/generators/class.rs index 7f303b2b909..63942e37cdc 100644 --- a/jni-gen/src/generators/class.rs +++ b/jni-gen/src/generators/class.rs @@ -130,10 +130,9 @@ impl<'a> ClassGenerator<'a> { signature.clone(), suffix.clone(), )?, - ItemWrapperSpec::FieldGetterSetter { - ref field_name, - ref signature, - } => generate_field_getter_setter(self.env, &self.class, field_name, signature)?, + ItemWrapperSpec::FieldGetterSetter { ref field_name } => { + generate_field_getter_setter(self.env, &self.class, field_name)? + } }; gen_items.push(gen) } diff --git a/jni-gen/src/generators/field_getter_setter.rs b/jni-gen/src/generators/field_getter_setter.rs index e0f7a4ddf60..c5944edbb9b 100644 --- a/jni-gen/src/generators/field_getter_setter.rs +++ b/jni-gen/src/generators/field_getter_setter.rs @@ -4,8 +4,10 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. +// use core::num::flt2dec::Sign; + use crate::{class_name::*, errors::*, utils::*}; -use jni::JNIEnv; +use jni::{objects::JObject, JNIEnv}; fn generate_type_check(type_signature: &str, type_name: &str, is_result: bool) -> String { if !type_signature.starts_with('L') { @@ -144,10 +146,19 @@ pub fn generate_field_getter_setter( env: &JNIEnv, class_name: &ClassName, field_name: &str, - type_signature: &str, ) -> Result<String> { - env.get_field_id(class_name.path(), field_name, type_signature) - .map(|_| ())?; + let clazz = env.find_class(class_name.path())?; + + let field = env + .call_method( + clazz, + "getField", + "(Ljava/lang/String;)Ljava/lang/reflect/Field;", + &[JObject::from(env.new_string(field_name.to_owned())?).into()], + )? + .l()?; + + let type_signature = ""; // TODO Generate the signature in a proper format let setter_code = generate_field_getter(class_name, field_name, type_signature); let getter_code = generate_field_setter(class_name, field_name, type_signature); diff --git a/jni-gen/src/wrapper_spec.rs b/jni-gen/src/wrapper_spec.rs index 0d2c22e97fb..ee86531507e 100644 --- a/jni-gen/src/wrapper_spec.rs +++ b/jni-gen/src/wrapper_spec.rs @@ -43,7 +43,6 @@ pub enum ItemWrapperSpec { }, FieldGetterSetter { field_name: String, - signature: String, }, } @@ -113,10 +112,9 @@ macro_rules! method { #[macro_export] macro_rules! field { - ($name:expr, $signature:expr) => { + ($name:expr) => { ItemWrapperSpec::FieldGetterSetter { field_name: $name.into(), - signature: $signature.into(), } }; } diff --git a/jni-gen/systest/build.rs b/jni-gen/systest/build.rs index 0e4b382dc88..cb8886a0006 100644 --- a/jni-gen/systest/build.rs +++ b/jni-gen/systest/build.rs @@ -30,7 +30,7 @@ fn main() { .wrap_all(vec![ java_class!("java.lang.Integer", vec![ constructor!("(I)V"), - field!("value", "I") + field!("value") ]), java_class!("java.util.Arrays", vec![ method!("binarySearch", "([Ljava/lang/Object;Ljava/lang/Object;)I"), @@ -38,7 +38,7 @@ fn main() { java_class!("java.lang.Error", vec![ constructor!("(Ljava/lang/String;)V"), method!("getMessage"), - field!("detailMessage", "Ljava/lang/String;"), + field!("detailMessage"), ]), ]) .generate(&generated_dir) From dc8642c340a4d0e0b3fde0ac6cd44153131dfb42 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <shrabec@student.ethz.ch> Date: Mon, 27 Feb 2023 14:13:02 +0900 Subject: [PATCH 06/33] Update field! macro to search all the class hierarchy for the field to determine its signature --- jni-gen/src/errors.rs | 5 + jni-gen/src/generators/field_getter_setter.rs | 110 ++++++++++++++---- 2 files changed, 92 insertions(+), 23 deletions(-) diff --git a/jni-gen/src/errors.rs b/jni-gen/src/errors.rs index e66bf117e2c..ef078696a96 100644 --- a/jni-gen/src/errors.rs +++ b/jni-gen/src/errors.rs @@ -54,5 +54,10 @@ error_chain::error_chain! { description("no matching method") display("no method '{}' with signature '{}' in class '{}'", method, signature, class) } + + NoField(class: String, field: String) { + description("no field") + display("no field '{}' in class'{}'", field, class) + } } } diff --git a/jni-gen/src/generators/field_getter_setter.rs b/jni-gen/src/generators/field_getter_setter.rs index c5944edbb9b..110e4f6dc95 100644 --- a/jni-gen/src/generators/field_getter_setter.rs +++ b/jni-gen/src/generators/field_getter_setter.rs @@ -7,7 +7,62 @@ // use core::num::flt2dec::Sign; use crate::{class_name::*, errors::*, utils::*}; -use jni::{objects::JObject, JNIEnv}; +use jni::{ + objects::{JClass, JObject, JValue}, + JNIEnv, +}; + +fn hierarchy_field_lookup<'a>( + env: &JNIEnv<'a>, + class: &ClassName, + lookup_name: &str, +) -> Result<Option<JObject<'a>>> { + let mut clazz = env.find_class(class.path())?; + while !clazz.is_null() { + if let Some(field) = class_field_lookup(env, clazz, lookup_name)? { + return Ok(Some(field)); + } + + clazz = env.get_superclass(clazz)?; + } + + Ok(None) +} + +fn class_field_lookup<'a>( + env: &JNIEnv<'a>, + clazz: JClass<'a>, + lookup_name: &str, +) -> Result<Option<JObject<'a>>> { + let fields = env + .call_method( + clazz, + "getDeclaredFields", + "()[Ljava/lang/reflect/Field;", + &[], + )? + .l()?; + + let num_fields = env.get_array_length(*fields)?; + + for field_index in 0..num_fields { + let field = env.get_object_array_element(*fields, field_index)?; + + let field_name = java_str_to_string( + &env.get_string( + env.call_method(field, "getName", "()Ljava/lang/String;", &[])? + .l()? + .into(), + )?, + )?; + + if field_name == lookup_name { + return Ok(Some(field)); + } + } + + Ok(None) +} fn generate_type_check(type_signature: &str, type_name: &str, is_result: bool) -> String { if !type_signature.starts_with('L') { @@ -52,7 +107,7 @@ fn generate_parameter_type_check(type_signature: &str, type_name: &str) -> Strin generate_type_check(type_signature, type_name, false) } -fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signature: &str) -> String { +fn generate_field_getter(class: &ClassName, field_name: &str, type_signature: &str) -> String { let rust_getter_name = format!("get_{}", java_identifier_to_rust(field_name)); let parameter_type = generate_jni_type(type_signature); @@ -60,7 +115,7 @@ fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signatur format!( "/// Returns the field `{}` of the scala class `{}`.", field_name, - class_name.full_name() + class.full_name() ), "///".to_string(), format!("/// Return type and Java signature: `{parameter_type}` (`{type_signature}`)"), @@ -68,7 +123,7 @@ fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signatur " &self,".to_string(), " receiver: JObject<'a>,".to_string(), format!(") -> JNIResult<{parameter_type}> {{"), - format!(" let class_name = \"{}\";", class_name.path()), + format!(" let class_name = \"{}\";", class.path()), format!(" let field_name = \"{field_name}\";"), format!(" let return_signature = \"{type_signature}\";"), "".to_string(), @@ -96,7 +151,7 @@ fn generate_field_getter(class_name: &ClassName, field_name: &str, type_signatur + "\n" } -fn generate_field_setter(class_name: &ClassName, field_name: &str, type_signature: &str) -> String { +fn generate_field_setter(class: &ClassName, field_name: &str, type_signature: &str) -> String { let rust_setter_name = format!("set_{}", java_identifier_to_rust(field_name)); let parameter_name = format!("new_{field_name}"); let parameter_type = generate_jni_type(type_signature); @@ -105,7 +160,7 @@ fn generate_field_setter(class_name: &ClassName, field_name: &str, type_signatur format!( "/// Sets the field `{}` of the scala class `{}`.", field_name, - class_name.full_name() + class.full_name() ), "///".to_string(), "/// Type and Java signature of parameters:".to_string(), @@ -118,7 +173,7 @@ fn generate_field_setter(class_name: &ClassName, field_name: &str, type_signatur " receiver: JObject<'a>,".to_string(), format!(" {parameter_name}: {parameter_type},"), ") -> JNIResult<()> {".to_string(), - format!(" let class_name = \"{}\";", class_name.path()), + format!(" let class_name = \"{}\";", class.path()), format!(" let field_name = \"{field_name}\";"), format!(" let return_signature = \"{type_signature}\";"), "".to_string(), @@ -144,24 +199,33 @@ fn generate_field_setter(class_name: &ClassName, field_name: &str, type_signatur pub fn generate_field_getter_setter( env: &JNIEnv, - class_name: &ClassName, + class: &ClassName, field_name: &str, ) -> Result<String> { - let clazz = env.find_class(class_name.path())?; - - let field = env - .call_method( - clazz, - "getField", - "(Ljava/lang/String;)Ljava/lang/reflect/Field;", - &[JObject::from(env.new_string(field_name.to_owned())?).into()], - )? - .l()?; - - let type_signature = ""; // TODO Generate the signature in a proper format - - let setter_code = generate_field_getter(class_name, field_name, type_signature); - let getter_code = generate_field_setter(class_name, field_name, type_signature); + let field_signature = match hierarchy_field_lookup(env, class, field_name)? { + Some(field) => { + let field_type = env + .call_method(field, "getType", "()Ljava/lang/Class;", &[])? + .l()?; + + java_str_to_string( + &env.get_string( + env.call_static_method( + "org/objectweb/asm/Type", + "getDescriptor", + "(Ljava/lang/Class;)Ljava/lang/String;", + &[JValue::Object(field_type)], + )? + .l()? + .into(), + )?, + )? + } + _ => return Err(ErrorKind::NoField(class.full_name(), field_name.into()).into()), + }; + + let setter_code = generate_field_getter(class, field_name, &field_signature); + let getter_code = generate_field_setter(class, field_name, &field_signature); Ok(format!("{setter_code}\n{getter_code}")) } From 608c4aa712157d2cc0a80fab7397241dc59b3c27 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <shrabec@student.ethz.ch> Date: Mon, 27 Feb 2023 16:56:12 +0900 Subject: [PATCH 07/33] Rename variables, add comments, delete leftover commented code --- jni-gen/src/generators/field_getter_setter.rs | 24 +++++++++++++------ 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/jni-gen/src/generators/field_getter_setter.rs b/jni-gen/src/generators/field_getter_setter.rs index 110e4f6dc95..8047af4ad8e 100644 --- a/jni-gen/src/generators/field_getter_setter.rs +++ b/jni-gen/src/generators/field_getter_setter.rs @@ -4,8 +4,6 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -// use core::num::flt2dec::Sign; - use crate::{class_name::*, errors::*, utils::*}; use jni::{ objects::{JClass, JObject, JValue}, @@ -64,18 +62,20 @@ fn class_field_lookup<'a>( Ok(None) } -fn generate_type_check(type_signature: &str, type_name: &str, is_result: bool) -> String { - if !type_signature.starts_with('L') { +// Generates a runtine check that the object is of the expected class - applies only to object types (starting with L) +// If this value is also the returned value in the setter, unwrap it first (since it is of type Result<T>) +fn generate_type_check(expected_variable_signature: &str, variable_name: &str, is_result: bool) -> String { + if !expected_variable_signature.starts_with('L') { return "".to_string(); } - let type_class = &type_signature[1..(type_signature.len() - 1)]; + let variable_type = &expected_variable_signature[1..(expected_variable_signature.len() - 1)]; let type_check = vec![ " debug_assert!(".to_string(), " self.env.is_instance_of(".to_string(), - format!(" {type_name},"), - format!(" self.env.find_class(\"{type_class}\")?,"), + format!(" {variable_name},"), + format!(" self.env.find_class(\"{variable_type}\")?,"), " )?".to_string(), " );".to_string(), ]; @@ -197,6 +197,16 @@ fn generate_field_setter(class: &ClassName, field_name: &str, type_signature: &s + "\n" } +/// Generates Rust code to both retrieve and modify a value of +/// the specified field of a given object of the specified class +/// +/// It works also for private fields and for inherited fields +/// +/// It determines the type of the field by iterating over the +/// inheritance hierarchy and checking for a field with matching name +/// +/// For class type fields it also generates runtime checks verifying +/// that the given object is of the specified class (or its descendant) pub fn generate_field_getter_setter( env: &JNIEnv, class: &ClassName, From 667c3b62974f03e3aee988233751f9f1c8b822c7 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 28 Feb 2023 03:35:48 +0900 Subject: [PATCH 08/33] Follow update in master branch --- prusti-viper/src/encoder/procedure_encoder.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 5c682edb299..637a1db5427 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -307,7 +307,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { 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.to_def_id()) { + let refutation = match self.encoder.get_prusti_refutation(cl_def_id) { Some(spec) => spec, None => return Ok(false), }; From 864c8969c3e28bb2819d64a8b8d27b4ab83a542b Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 6 Mar 2023 19:38:43 +0900 Subject: [PATCH 09/33] current code, just a snapshot of my working dir --- Cargo.lock | 379 +----------------- Cargo.toml | 2 +- jni-gen/src/generators/class.rs | 2 + jni-gen/src/generators/method.rs | 23 ++ jni-gen/src/generators/scala_object_getter.rs | 34 +- jni-gen/src/lib.rs | 4 +- jni-gen/src/utils.rs | 4 + jni-gen/systest/Cargo.toml | 1 + prusti/src/driver.rs | 18 +- viper-sys/Cargo.toml | 1 + viper-sys/build.rs | 30 ++ viper/src/verification_context.rs | 11 +- viper/src/verifier.rs | 123 ++++-- 13 files changed, 206 insertions(+), 426 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index a625edefcd5..85d24c43045 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -134,7 +134,7 @@ dependencies = [ "slab", "socket2", "waker-fn", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -162,7 +162,7 @@ dependencies = [ "futures-lite", "libc", "signal-hook", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -216,21 +216,6 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "065374052e7df7ee4047b1160cca5e1467a12351a40b3da123c870ba0b8eda2a" -[[package]] -name = "attohttpc" -version = "0.16.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fdb8867f378f33f78a811a8eb9bf108ad99430d7aad43315dd9319c827ef6247" -dependencies = [ - "flate2", - "http", - "log", - "native-tls", - "openssl", - "url", - "wildmatch", -] - [[package]] name = "atty" version = "0.2.14" @@ -378,7 +363,7 @@ dependencies = [ "glob", "itertools", "lazy_static", - "remove_dir_all 0.5.3", + "remove_dir_all", "serde_json", "snapbox", "tar", @@ -488,17 +473,6 @@ dependencies = [ "unicode-width", ] -[[package]] -name = "color-backtrace" -version = "0.5.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cd6c04463c99389fff045d2b90ce84f5131332712c7ffbede020f5e9ad1ed685" -dependencies = [ - "atty", - "backtrace", - "termcolor", -] - [[package]] name = "combine" version = "4.6.6" @@ -643,40 +617,6 @@ dependencies = [ "cfg-if", ] -[[package]] -name = "crossbeam-channel" -version = "0.5.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2dd04ddaf88237dc3b8d8f9a3c1004b506b54b3313403944054d23c0870c521" -dependencies = [ - "cfg-if", - "crossbeam-utils", -] - -[[package]] -name = "crossbeam-deque" -version = "0.8.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "715e8152b692bba2d374b53d4875445368fdf21a94751410af607a5ac677d1fc" -dependencies = [ - "cfg-if", - "crossbeam-epoch", - "crossbeam-utils", -] - -[[package]] -name = "crossbeam-epoch" -version = "0.9.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "01a9af1f4c2ef74bb8aa1f7e19706bc72d03598c8a570bb5de72243c7a9d9d5a" -dependencies = [ - "autocfg", - "cfg-if", - "crossbeam-utils", - "memoffset 0.7.1", - "scopeguard", -] - [[package]] name = "crossbeam-utils" version = "0.8.14" @@ -746,8 +686,8 @@ version = "3.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1631ca6e3c59112501a9d87fd86f21591ff77acd31331e8a73f8d80a65bbdd71" dependencies = [ - "nix 0.26.1", - "windows-sys 0.42.0", + "nix", + "windows-sys", ] [[package]] @@ -947,28 +887,6 @@ version = "2.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0206175f82b8d6bf6652ff7d71a1e27fd2e4efde587fd368662814d6ec1d9ce0" -[[package]] -name = "failure" -version = "0.1.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d32e9bd16cc02eae7db7ef620b392808b89f6a5e16bb3497d159c6b92a0f4f86" -dependencies = [ - "backtrace", - "failure_derive", -] - -[[package]] -name = "failure_derive" -version = "0.1.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aa4da3c766cd7a0db8242e326e9e4e081edd567072893ed320008189715366a4" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "synstructure", -] - [[package]] name = "fastrand" version = "1.8.0" @@ -987,7 +905,7 @@ dependencies = [ "cfg-if", "libc", "redox_syscall", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -1031,16 +949,6 @@ dependencies = [ "percent-encoding", ] -[[package]] -name = "fs2" -version = "0.4.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9564fc758e15025b46aa6643b1b77d047d1a56a1aea6e01002ac0c7026876213" -dependencies = [ - "libc", - "winapi", -] - [[package]] name = "futures" version = "0.3.25" @@ -1449,7 +1357,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "46112a93252b123d31a119a8d1a1ac19deac4fac6e0e8b0df58f0d4e5870e63c" dependencies = [ "libc", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -1467,7 +1375,7 @@ dependencies = [ "hermit-abi 0.2.6", "io-lifetimes", "rustix", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -1658,15 +1566,6 @@ version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" -[[package]] -name = "memoffset" -version = "0.6.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5aa361d4faea93603064a027415f07bd8e1d5c88c9fbf68bf56a285428fd79ce" -dependencies = [ - "autocfg", -] - [[package]] name = "memoffset" version = "0.7.1" @@ -1716,7 +1615,7 @@ dependencies = [ "libc", "log", "wasi", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -1746,38 +1645,6 @@ dependencies = [ "twoway", ] -[[package]] -name = "native-tls" -version = "0.2.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07226173c32f2926027b63cce4bcd8076c3552846cbe7925f3aaffeac0a3b92e" -dependencies = [ - "lazy_static", - "libc", - "log", - "openssl", - "openssl-probe", - "openssl-sys", - "schannel", - "security-framework", - "security-framework-sys", - "tempfile", -] - -[[package]] -name = "nix" -version = "0.25.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f346ff70e7dbfd675fe90590b92d59ef2de15a8779ae305ebcbfd3f0caf59be4" -dependencies = [ - "autocfg", - "bitflags", - "cfg-if", - "libc", - "memoffset 0.6.5", - "pin-utils", -] - [[package]] name = "nix" version = "0.26.1" @@ -1787,7 +1654,7 @@ dependencies = [ "bitflags", "cfg-if", "libc", - "memoffset 0.7.1", + "memoffset", "pin-utils", "static_assertions", ] @@ -2040,7 +1907,7 @@ dependencies = [ "libc", "log", "wepoll-ffi", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -2147,7 +2014,7 @@ version = "0.1.0" dependencies = [ "ctrlc", "glob", - "nix 0.26.1", + "nix", "prusti-utils", ] @@ -2221,7 +2088,7 @@ dependencies = [ "itertools", "lazy_static", "log", - "nix 0.26.1", + "nix", "rustc-hash", "serde", "toml", @@ -2298,28 +2165,6 @@ dependencies = [ "getrandom", ] -[[package]] -name = "rayon" -version = "1.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6db3a213adf02b3bcfd2d3846bb41cb22857d131789e01df434fb7e7bc0759b7" -dependencies = [ - "either", - "rayon-core", -] - -[[package]] -name = "rayon-core" -version = "1.10.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cac410af5d00ab6884528b4ab69d1e8e146e8d471201800fa1b4524126de6ad3" -dependencies = [ - "crossbeam-channel", - "crossbeam-deque", - "crossbeam-utils", - "num_cpus", -] - [[package]] name = "redox_syscall" version = "0.2.16" @@ -2372,19 +2217,6 @@ dependencies = [ "winapi", ] -[[package]] -name = "remove_dir_all" -version = "0.7.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "882f368737489ea543bc5c340e6f3d34a28c39980bd9a979e47322b26f60ac40" -dependencies = [ - "libc", - "log", - "num_cpus", - "rayon", - "winapi", -] - [[package]] name = "reqwest" version = "0.11.13" @@ -2504,7 +2336,7 @@ dependencies = [ "io-lifetimes", "libc", "linux-raw-sys", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -2543,39 +2375,6 @@ version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5583e89e108996506031660fe09baa5011b9dd0341b89029313006d1fb508d70" -[[package]] -name = "rustwide" -version = "0.15.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1b0070cdf593a5b66ba6160974bbfb504a837f8c06f3357a623c9a7b6619c64" -dependencies = [ - "attohttpc", - "base64 0.13.1", - "failure", - "flate2", - "fs2", - "futures-util", - "getrandom", - "git2", - "http", - "lazy_static", - "log", - "nix 0.25.1", - "percent-encoding", - "remove_dir_all 0.7.0", - "scopeguard", - "serde", - "serde_json", - "tar", - "tempfile", - "thiserror", - "tokio", - "tokio-stream", - "toml", - "walkdir", - "windows-sys 0.36.1", -] - [[package]] name = "ryu" version = "1.0.12" @@ -2597,28 +2396,12 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "schannel" -version = "0.1.20" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88d6731146462ea25d9244b2ed5fd1d716d25c52e4d54aa4fb0f3c4e9854dbe2" -dependencies = [ - "lazy_static", - "windows-sys 0.36.1", -] - [[package]] name = "scoped-tls" version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e1cf6437eb19a8f4a6cc0f7dca544973b0b78843adbfeb3683d1a94a0024a294" -[[package]] -name = "scopeguard" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" - [[package]] name = "scratch" version = "1.0.3" @@ -2635,29 +2418,6 @@ dependencies = [ "untrusted", ] -[[package]] -name = "security-framework" -version = "2.7.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2bc1bb97804af6631813c55739f771071e0f2ed33ee20b68c86ec505d906356c" -dependencies = [ - "bitflags", - "core-foundation", - "core-foundation-sys", - "libc", - "security-framework-sys", -] - -[[package]] -name = "security-framework-sys" -version = "2.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0160a13a177a45bfb43ce71c01580998474f556ad854dcbca936dd2841a5c556" -dependencies = [ - "core-foundation-sys", - "libc", -] - [[package]] name = "semver" version = "1.0.16" @@ -2840,18 +2600,6 @@ dependencies = [ "unicode-ident", ] -[[package]] -name = "synstructure" -version = "0.12.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "unicode-xid", -] - [[package]] name = "systest" version = "0.1.0" @@ -2873,7 +2621,6 @@ checksum = "4b55807c0344e1e6c04d7c965f5289c39a8d94ae23ed5c0b57aabac549f871c6" dependencies = [ "filetime", "libc", - "xattr", ] [[package]] @@ -2886,7 +2633,7 @@ dependencies = [ "fastrand", "libc", "redox_syscall", - "remove_dir_all 0.5.3", + "remove_dir_all", "winapi", ] @@ -2910,24 +2657,6 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "test-crates" -version = "0.1.0" -dependencies = [ - "clap", - "color-backtrace", - "csv", - "env_logger", - "failure", - "glob", - "log", - "prusti", - "prusti-launch", - "rustwide", - "serde", - "toml", -] - [[package]] name = "tester" version = "0.9.0" @@ -2987,11 +2716,9 @@ dependencies = [ "libc", "memchr", "mio", - "num_cpus", "pin-project-lite", - "signal-hook-registry", "socket2", - "windows-sys 0.42.0", + "windows-sys", ] [[package]] @@ -3173,12 +2900,6 @@ version = "0.1.10" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" -[[package]] -name = "unicode-xid" -version = "0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f962df74c8c05a667b5ee8bcf162993134c104e96440b663c8daa176dc772d8c" - [[package]] name = "untrusted" version = "0.7.1" @@ -3491,12 +3212,6 @@ dependencies = [ "cc", ] -[[package]] -name = "wildmatch" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7f44b95f62d34113cf558c93511ac93027e03e9c29a60dd0fd70e6e025c7270a" - [[package]] name = "winapi" version = "0.3.9" @@ -3528,19 +3243,6 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-sys" -version = "0.36.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ea04155a16a59f9eab786fe12a4a450e75cdb175f9e0d80da1e17db09f55b8d2" -dependencies = [ - "windows_aarch64_msvc 0.36.1", - "windows_i686_gnu 0.36.1", - "windows_i686_msvc 0.36.1", - "windows_x86_64_gnu 0.36.1", - "windows_x86_64_msvc 0.36.1", -] - [[package]] name = "windows-sys" version = "0.42.0" @@ -3548,12 +3250,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5a3e1820f08b8513f676f7ab6c1f99ff312fb97b553d30ff4dd86f9f15728aa7" dependencies = [ "windows_aarch64_gnullvm", - "windows_aarch64_msvc 0.42.0", - "windows_i686_gnu 0.42.0", - "windows_i686_msvc 0.42.0", - "windows_x86_64_gnu 0.42.0", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", "windows_x86_64_gnullvm", - "windows_x86_64_msvc 0.42.0", + "windows_x86_64_msvc", ] [[package]] @@ -3562,48 +3264,24 @@ version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "41d2aa71f6f0cbe00ae5167d90ef3cfe66527d6f613ca78ac8024c3ccab9a19e" -[[package]] -name = "windows_aarch64_msvc" -version = "0.36.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9bb8c3fd39ade2d67e9874ac4f3db21f0d710bee00fe7cab16949ec184eeaa47" - [[package]] name = "windows_aarch64_msvc" version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dd0f252f5a35cac83d6311b2e795981f5ee6e67eb1f9a7f64eb4500fbc4dcdb4" -[[package]] -name = "windows_i686_gnu" -version = "0.36.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "180e6ccf01daf4c426b846dfc66db1fc518f074baa793aa7d9b9aaeffad6a3b6" - [[package]] name = "windows_i686_gnu" version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fbeae19f6716841636c28d695375df17562ca208b2b7d0dc47635a50ae6c5de7" -[[package]] -name = "windows_i686_msvc" -version = "0.36.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2e7917148b2812d1eeafaeb22a97e4813dfa60a3f8f78ebe204bcc88f12f024" - [[package]] name = "windows_i686_msvc" version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "84c12f65daa39dd2babe6e442988fc329d6243fdce47d7d2d155b8d874862246" -[[package]] -name = "windows_x86_64_gnu" -version = "0.36.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4dcd171b8776c41b97521e5da127a2d86ad280114807d0b2ab1e462bc764d9e1" - [[package]] name = "windows_x86_64_gnu" version = "0.42.0" @@ -3616,12 +3294,6 @@ version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09d525d2ba30eeb3297665bd434a54297e4170c7f1a44cad4ef58095b4cd2028" -[[package]] -name = "windows_x86_64_msvc" -version = "0.36.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c811ca4a8c853ef420abd8592ba53ddbbac90410fab6903b3e79972a631f7680" - [[package]] name = "windows_x86_64_msvc" version = "0.42.0" @@ -3637,15 +3309,6 @@ dependencies = [ "winapi", ] -[[package]] -name = "xattr" -version = "0.2.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d1526bbe5aaeb5eb06885f4d987bcdfa5e23187055de9b83fe00156a821fabc" -dependencies = [ - "libc", -] - [[package]] name = "yaml-rust" version = "0.4.5" diff --git a/Cargo.toml b/Cargo.toml index bd8815e5a9d..6f6264ac99e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,7 +13,7 @@ members = [ "prusti-smt-solver", "prusti-rustc-interface", "smt-log-analyzer", - "test-crates", + #"test-crates", "viper", "viper-sys", "vir", diff --git a/jni-gen/src/generators/class.rs b/jni-gen/src/generators/class.rs index 63942e37cdc..68a719c2d28 100644 --- a/jni-gen/src/generators/class.rs +++ b/jni-gen/src/generators/class.rs @@ -56,6 +56,7 @@ impl<'a> ClassGenerator<'a> { fn generate_imports(&self) -> String { vec![ + "use jni_gen::{class_name::*, errors::*, utils::*};", "use jni::JNIEnv;", "use jni::objects::GlobalRef;", "use jni::objects::JObject;", @@ -65,6 +66,7 @@ impl<'a> ClassGenerator<'a> { "use jni::objects::JValue;", "use jni::objects::JClass;", "use jni::errors::Result as JNIResult;", + "use jni::errors::*;", "use jni::sys::*;", "use jni::signature::*;", "use once_cell::sync::OnceCell;", diff --git a/jni-gen/src/generators/method.rs b/jni-gen/src/generators/method.rs index 3886653a6d9..c787118c33e 100644 --- a/jni-gen/src/generators/method.rs +++ b/jni-gen/src/generators/method.rs @@ -250,6 +250,29 @@ fn generate( } code.push("".to_string()); + + + + + // let reciever_class = env.get_object_class(receiver)?; + // let receiver_class_name = java_str_to_string( + // self.env.get_string( + // self.env.call_method(receiver, "getName", "()Ljava/lang/String;", &[])? + // .l()? + // .into(), + // )?, + // )?; + // println!("Function 'call_stop', receiver is of type '{}'", receiver_class_name); + code.push("let reciever_class = self.env.get_object_class(receiver)?;".to_string()); + code.push("let receiver_class_name = java_str_to_string_simple(".to_string()); + code.push(" &self.env.get_string(".to_string()); + code.push(" self.env.call_method(reciever_class, \"getName\", \"()Ljava/lang/String;\", &[])?".to_string()); + code.push(" .l()?".to_string()); + code.push(" .into(),".to_string()); + code.push(" )?,".to_string()); + code.push(");".to_string()); + code.push(format!("println!(\"Function '{rust_method_name}', receiver is of type '{{}}'\", receiver_class_name);")); + // Generate dynamic type check for `receiver` code.push(" debug_assert!(".to_string()); code.push(" self.env.is_instance_of(".to_string()); diff --git a/jni-gen/src/generators/scala_object_getter.rs b/jni-gen/src/generators/scala_object_getter.rs index 6374f7910fc..bfaa18d315b 100644 --- a/jni-gen/src/generators/scala_object_getter.rs +++ b/jni-gen/src/generators/scala_object_getter.rs @@ -30,23 +30,23 @@ pub fn generate_scala_object_getter(env: &JNIEnv, class_name: &ClassName) -> Res " let field_name = \"MODULE$\";".to_string(), format!(" let field_signature = \"L{};\";", class_name.path()), "".to_string(), - "static CLASS: OnceCell<GlobalRef> = OnceCell::new();".to_string(), - "static STATIC_FIELD_ID: OnceCell<JStaticFieldID> = OnceCell::new();".to_string(), - "static FIELD_TYPE: OnceCell<JavaType> = OnceCell::new();".to_string(), - "let class = CLASS.get_or_try_init(|| {".to_string(), - " let class = self.env.find_class(class_name)?;".to_string(), - " self.env.new_global_ref(class)".to_string(), - "})?;".to_string(), - "let static_field_id = *STATIC_FIELD_ID.get_or_try_init(|| {".to_string(), - " self.env.get_static_field_id(".to_string(), - " class_name,".to_string(), - " field_name,".to_string(), - " field_signature,".to_string(), - " )".to_string(), - "})?;".to_string(), - "let field_type = FIELD_TYPE.get_or_try_init(|| {".to_string(), - " JavaType::from_str(field_signature)".to_string(), - "})?.clone();".to_string(), + " static CLASS: OnceCell<GlobalRef> = OnceCell::new();".to_string(), + " static STATIC_FIELD_ID: OnceCell<JStaticFieldID> = OnceCell::new();".to_string(), + " static FIELD_TYPE: OnceCell<JavaType> = OnceCell::new();".to_string(), + " let class = CLASS.get_or_try_init(|| {".to_string(), + " let class = self.env.find_class(class_name)?;".to_string(), + " self.env.new_global_ref(class)".to_string(), + " })?;".to_string(), + " let static_field_id = *STATIC_FIELD_ID.get_or_try_init(|| {".to_string(), + " self.env.get_static_field_id(".to_string(), + " class_name,".to_string(), + " field_name,".to_string(), + " field_signature,".to_string(), + " )".to_string(), + " })?;".to_string(), + " let field_type = FIELD_TYPE.get_or_try_init(|| {".to_string(), + " JavaType::from_str(field_signature)".to_string(), + " })?.clone();".to_string(), "".to_string(), " let result = self.env.get_static_field_unchecked(".to_string(), " JClass::from(class.as_obj()),".to_string(), diff --git a/jni-gen/src/lib.rs b/jni-gen/src/lib.rs index 8123bc22e91..91a82835431 100644 --- a/jni-gen/src/lib.rs +++ b/jni-gen/src/lib.rs @@ -6,12 +6,12 @@ #![warn(clippy::disallowed_types)] -mod class_name; +pub mod class_name; pub mod errors; mod generators; mod module_tree; mod unordered_set_eq; -mod utils; +pub mod utils; mod wrapper_generator; mod wrapper_spec; diff --git a/jni-gen/src/utils.rs b/jni-gen/src/utils.rs index beefc773ba1..fd2b8c96a33 100644 --- a/jni-gen/src/utils.rs +++ b/jni-gen/src/utils.rs @@ -71,6 +71,10 @@ pub fn java_str_to_string(string: &JavaStr) -> Result<String> { unsafe { Ok(CStr::from_ptr(string.get_raw()).to_str()?.to_string()) } } +pub fn java_str_to_string_simple(string: &JavaStr) -> String { + java_str_to_string(string).unwrap() +} + pub fn java_str_to_valid_rust_argument_name(string: &JavaStr) -> Result<String> { Ok(format!( "arg_{}", diff --git a/jni-gen/systest/Cargo.toml b/jni-gen/systest/Cargo.toml index 833309c0871..b7b22cd7639 100644 --- a/jni-gen/systest/Cargo.toml +++ b/jni-gen/systest/Cargo.toml @@ -15,3 +15,4 @@ tempfile = "3.3" error-chain = "0.12" jni = { version = "0.20", features = ["invocation"] } once_cell = "1.16" +jni-gen = { path = ".." } diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index 9ab010b1277..e6bad1c2c20 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -25,13 +25,13 @@ use std::{borrow::Cow, env, panic}; /// Link to report Prusti bugs const BUG_REPORT_URL: &str = "https://github.com/viperproject/prusti-dev/issues/new"; -lazy_static! { - static ref ICE_HOOK: Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static> = { - let hook = panic::take_hook(); - panic::set_hook(box |info| report_prusti_ice(info, BUG_REPORT_URL)); - hook - }; -} +// lazy_static! { +// static ref ICE_HOOK: Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static> = { +// let hook = panic::take_hook(); +// // panic::set_hook(box |info| report_prusti_ice(info, BUG_REPORT_URL)); +// hook +// }; +// } fn get_prusti_version_info() -> String { format!( @@ -46,7 +46,7 @@ fn get_prusti_version_info() -> String { /// Report a readable error message in case of panic, with a link to open a new Prusti issue. fn report_prusti_ice(info: &panic::PanicInfo<'_>, bug_report_url: &str) { // Invoke our ICE handler, which prints the actual panic message and optionally a backtrace - (*ICE_HOOK)(info); + // (*ICE_HOOK)(info); // Separate the output with an empty line eprintln!(); @@ -140,7 +140,7 @@ fn main() { config::set_no_verify(true); } - lazy_static::initialize(&ICE_HOOK); + // lazy_static::initialize(&ICE_HOOK); init_loggers(); // Disable incremental compilation because it causes mir_borrowck not to diff --git a/viper-sys/Cargo.toml b/viper-sys/Cargo.toml index 28bd2675d1c..716daa66279 100644 --- a/viper-sys/Cargo.toml +++ b/viper-sys/Cargo.toml @@ -21,3 +21,4 @@ env_logger = "0.10" jni = { version = "0.20", features = ["invocation"] } log = { version = "0.4", features = ["release_max_level_info"] } once_cell = "1.16" +jni-gen = { path = "../jni-gen" } diff --git a/viper-sys/build.rs b/viper-sys/build.rs index ef161097b8e..43b85b59612 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -128,6 +128,36 @@ fn main() { object_getter!(), method!("apply"), ]), + + java_class!("viper.silver.frontend.DefaultStates", vec![ + method!("ConsistencyCheck"), + method!("Verification"), + ]), + + // Logger + java_class!("viper.silver.logger.SilentLogger$", vec![ + object_getter!(), + method!("apply"), + ]), + java_class!("viper.silver.logger.ViperLogger", vec![ + method!("get"), + ]), + + // SiliconFrontend + java_class!("viper.silicon.SiliconFrontend", vec![ + constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"), + method!("setVerifier"), + method!("_program"), + method!("verification"), + method!("getVerificationResult"), + method!("setState"), + method!("verifier"), + // field!("_program", "Lscala/Option;"), + // field!("_verifier", "Lscala/Option;"), + field!("_program"), + field!("_verifier"), + ]), + // Silicon java_class!("viper.silicon.Silicon", vec![ constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"), diff --git a/viper/src/verification_context.rs b/viper/src/verification_context.rs index b2e557d5463..07088e78a71 100644 --- a/viper/src/verification_context.rs +++ b/viper/src/verification_context.rs @@ -94,8 +94,13 @@ impl<'a> VerificationContext<'a> { debug!("Verifier arguments: '{}'", verifier_args.to_vec().join(" ")); - Verifier::new(&self.env, backend, report_path, smt_manager) - .parse_command_line(&verifier_args) - .start() + let ver = Verifier::new(&self.env, backend, report_path, smt_manager); + + ver.frontend_wrapper.call___program(ver.frontend_instance).expect("fail 3"); + ver.verifier_wrapper.call_name(ver.verifier_instance).expect("fail 5"); + + ver.parse_command_line(&verifier_args); + ver.start(); + ver } } diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index 60241be0eec..d8e06a56c2c 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -19,12 +19,14 @@ use std::path::PathBuf; use viper_sys::wrappers::{scala, viper::*}; pub struct Verifier<'a> { - env: &'a JNIEnv<'a>, - verifier_wrapper: silver::verifier::Verifier<'a>, - verifier_instance: JObject<'a>, - jni: JniUtils<'a>, - ast_utils: AstUtils<'a>, - smt_manager: SmtManager, + pub env: &'a JNIEnv<'a>, + pub verifier_wrapper: silver::verifier::Verifier<'a>, + pub verifier_instance: JObject<'a>, + pub frontend_wrapper: silicon::SiliconFrontend<'a>, + pub frontend_instance: JObject<'a>, + pub jni: JniUtils<'a>, + pub ast_utils: AstUtils<'a>, + pub smt_manager: SmtManager, } impl<'a> Verifier<'a> { @@ -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 = silicon::SiliconFrontend::with(env); + // let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || { + let frontend_instance = jni.unwrap_result(env.with_local_frame(128, || { 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,59 +52,96 @@ impl<'a> Verifier<'a> { }; let debug_info = jni.new_seq(&[]); - match backend { + let backend_unwrapped = match backend { VerificationBackend::Silicon => { + println!("Created a new silicon backend"); silicon::Silicon::with(env).new(reporter, debug_info) } VerificationBackend::Carbon => { - carbon::CarbonVerifier::with(env).new(reporter, debug_info) - } - } + panic!("Trying to use Carbon backend - now made compatible just with Silicon"); + } // VerificationBackend::Carbon => { + // carbon::CarbonVerifier::with(env).new(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 = silicon::SiliconFrontend::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.set___verifier(frontend_instance, verifier_option).unwrap(); + + Ok(frontend_instance) + + // match backend { + // VerificationBackend::Silicon => { + // silicon::Silicon::with(env).new(reporter, debug_info) + // } + // VerificationBackend::Carbon => { + // carbon::CarbonVerifier::with(env).new(reporter, debug_info) + // } + // } })); - ast_utils.with_local_frame(16, || { - 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)), - ); + let verifier_instance = jni.unwrap_result(ast_utils.with_local_frame(128, || { + 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(); + println!("Set state"); + + 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) + })); + + let _x = verifier_wrapper.call_name(verifier_instance).expect("fail1"); + let _y = frontend_wrapper.call___program(frontend_instance).expect("fail2"); + + println!("THIS IS PASSING"); Verifier { env, verifier_wrapper, verifier_instance, + frontend_wrapper, + frontend_instance, jni, ast_utils, smt_manager, } } - #[must_use] - pub fn parse_command_line(self, args: &[String]) -> Self { - self.ast_utils.with_local_frame(16, || { - let args = self.jni.new_seq( - &args - .iter() - .map(|x| self.jni.new_string(x)) - .collect::<Vec<JObject>>(), - ); + pub fn parse_command_line(&self, args: &[String]) { + self.verifier_wrapper.call_name(self.verifier_instance).expect("fail 6"); + // self.verifier_wrapper.call_parseCommandLine(self.verifier_instance, args).expect("fail 7"); + self.ast_utils.with_local_frame(128, || { + self.verifier_wrapper.call_name(self.verifier_instance).expect("fail 7"); + // let args = self.jni.new_seq(&args.iter().map(|x| self.jni.new_string(x)).collect::<Vec<JObject>>()); + // let args = self.jni.new_seq(&args.iter().map(|x| self.jni.new_string(x)).collect::<Vec<JObject>>()); + let a = &args.iter().map(|x| self.jni.new_string(x)).collect::<Vec<JObject>>(); + self.verifier_wrapper.call_name(self.verifier_instance).expect("fail 8"); + let b = self.jni.new_seq(a); + self.verifier_wrapper.call_name(self.verifier_instance).expect("fail 9"); self.jni.unwrap_result( self.verifier_wrapper - .call_parseCommandLine(self.verifier_instance, args), + .call_parseCommandLine(self.verifier_instance, b), ); }); - self } - #[must_use] - pub fn start(self) -> Self { + pub fn start(&self) { self.ast_utils.with_local_frame(16, || { self.jni .unwrap_result(self.verifier_wrapper.call_start(self.verifier_instance)); }); - self } pub fn verify(&mut self, program: Program) -> VerificationResult { @@ -132,11 +173,20 @@ impl<'a> Verifier<'a> { ); } + // set program + println!("set program"); + let program_option = self.jni.new_option(Some(program.to_jobject())); + self.jni.unwrap_result(self.frontend_wrapper.set___program(self.frontend_instance, program_option)); + run_timed!("Viper verification", debug, - let viper_result = self.jni.unwrap_result( - self.verifier_wrapper - .call_verify(self.verifier_instance, program.to_jobject()), - ); + // let viper_result = self.jni.unwrap_result( + // self.verifier_wrapper + // .call_verify(self.verifier_instance, program.to_jobject()), + // ); + println!("calling verification"); + 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: {}", @@ -337,6 +387,7 @@ impl<'a> Verifier<'a> { impl<'a> Drop for Verifier<'a> { fn drop(&mut self) { + println!("DROPVERIFIER"); // Tell the verifier to stop its threads. self.jni .unwrap_result(self.verifier_wrapper.call_stop(self.verifier_instance)); From b9796a6b227bdffc27bc2800baef9963f6c4728d Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 13 Mar 2023 15:13:39 +0900 Subject: [PATCH 10/33] fix bug with env/ast_utils with_local_frame - calling wrong function --- viper/src/verifier.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index d8e06a56c2c..2a33a114d7d 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -88,7 +88,7 @@ impl<'a> Verifier<'a> { // } })); - let verifier_instance = jni.unwrap_result(ast_utils.with_local_frame(128, || { + let verifier_instance = jni.unwrap_result(env.with_local_frame(128, || { let verifier_instance = jni.unwrap_result(frontend_wrapper.call_verifier(frontend_instance)); From 0d48d5a46d55b6a4671e60116c228d176072edcf Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 13 Mar 2023 15:46:09 +0900 Subject: [PATCH 11/33] add --- prusti/src/driver.rs | 14 +++++++------- viper/src/verification_context.rs | 4 +--- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index 6f9dffabc91..e82fa3ca20a 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -27,13 +27,13 @@ use tracing_subscriber::{filter::EnvFilter, prelude::*}; /// Link to report Prusti bugs const BUG_REPORT_URL: &str = "https://github.com/viperproject/prusti-dev/issues/new"; -// lazy_static! { -// static ref ICE_HOOK: Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static> = { -// let hook = panic::take_hook(); -// // panic::set_hook(box |info| report_prusti_ice(info, BUG_REPORT_URL)); -// hook -// }; -// } +lazy_static! { + static ref ICE_HOOK: Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static> = { + let hook = panic::take_hook(); + panic::set_hook(box |info| report_prusti_ice(info, BUG_REPORT_URL)); + hook + }; +} fn get_prusti_version_info() -> String { format!( diff --git a/viper/src/verification_context.rs b/viper/src/verification_context.rs index ee33ba37500..85d02b7c8ed 100644 --- a/viper/src/verification_context.rs +++ b/viper/src/verification_context.rs @@ -100,8 +100,6 @@ impl<'a> VerificationContext<'a> { ver.frontend_wrapper.call___program(ver.frontend_instance).expect("fail 3"); ver.verifier_wrapper.call_name(ver.verifier_instance).expect("fail 5"); - ver.parse_command_line(&verifier_args); - ver.start(); - ver + ver.parse_command_line(&verifier_args).start() } } From ea965ab1ecabf1b9c5e061f55e04014e6949ebec Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 13 Mar 2023 16:48:06 +0900 Subject: [PATCH 12/33] Remove unecessary changes --- Cargo.toml | 2 +- jni-gen/src/generators/class.rs | 2 -- jni-gen/src/generators/method.rs | 23 ----------------------- jni-gen/src/lib.rs | 4 ++-- jni-gen/src/utils.rs | 4 ---- jni-gen/systest/Cargo.toml | 1 - prusti/src/driver.rs | 2 +- viper-sys/Cargo.toml | 1 - viper-sys/build.rs | 8 -------- 9 files changed, 4 insertions(+), 43 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index ebd2e50d4d5..6175322a7f3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,7 +14,7 @@ members = [ "prusti-smt-solver", "prusti-rustc-interface", "smt-log-analyzer", - #"test-crates", + "test-crates", "viper", "viper-sys", "vir", diff --git a/jni-gen/src/generators/class.rs b/jni-gen/src/generators/class.rs index eb3cded03e9..3862546b782 100644 --- a/jni-gen/src/generators/class.rs +++ b/jni-gen/src/generators/class.rs @@ -56,7 +56,6 @@ impl<'a> ClassGenerator<'a> { fn generate_imports(&self) -> String { vec![ - "use jni_gen::{class_name::*, errors::*, utils::*};", "use jni::JNIEnv;", "use jni::objects::GlobalRef;", "use jni::objects::JObject;", @@ -66,7 +65,6 @@ impl<'a> ClassGenerator<'a> { "use jni::objects::JValue;", "use jni::objects::JClass;", "use jni::errors::Result as JNIResult;", - "use jni::errors::*;", "use jni::sys::*;", "use jni::signature::*;", "use once_cell::sync::OnceCell;", diff --git a/jni-gen/src/generators/method.rs b/jni-gen/src/generators/method.rs index 6298c9a634d..42135b63bc7 100644 --- a/jni-gen/src/generators/method.rs +++ b/jni-gen/src/generators/method.rs @@ -258,29 +258,6 @@ fn generate( } } - - - - - // let reciever_class = env.get_object_class(receiver)?; - // let receiver_class_name = java_str_to_string( - // self.env.get_string( - // self.env.call_method(receiver, "getName", "()Ljava/lang/String;", &[])? - // .l()? - // .into(), - // )?, - // )?; - // println!("Function 'call_stop', receiver is of type '{}'", receiver_class_name); - code.push("let reciever_class = self.env.get_object_class(receiver)?;".to_string()); - code.push("let receiver_class_name = java_str_to_string_simple(".to_string()); - code.push(" &self.env.get_string(".to_string()); - code.push(" self.env.call_method(reciever_class, \"getName\", \"()Ljava/lang/String;\", &[])?".to_string()); - code.push(" .l()?".to_string()); - code.push(" .into(),".to_string()); - code.push(" )?,".to_string()); - code.push(");".to_string()); - code.push(format!("println!(\"Function '{rust_method_name}', receiver is of type '{{}}'\", receiver_class_name);")); - // Generate dynamic type check for `receiver` code.push(generate_variable_type_check("receiver", "class_name")); diff --git a/jni-gen/src/lib.rs b/jni-gen/src/lib.rs index 91a82835431..8123bc22e91 100644 --- a/jni-gen/src/lib.rs +++ b/jni-gen/src/lib.rs @@ -6,12 +6,12 @@ #![warn(clippy::disallowed_types)] -pub mod class_name; +mod class_name; pub mod errors; mod generators; mod module_tree; mod unordered_set_eq; -pub mod utils; +mod utils; mod wrapper_generator; mod wrapper_spec; diff --git a/jni-gen/src/utils.rs b/jni-gen/src/utils.rs index 6b9be5e0a06..2d17be940f3 100644 --- a/jni-gen/src/utils.rs +++ b/jni-gen/src/utils.rs @@ -71,10 +71,6 @@ pub fn java_str_to_string(string: &JavaStr) -> Result<String> { unsafe { Ok(CStr::from_ptr(string.get_raw()).to_str()?.to_string()) } } -pub fn java_str_to_string_simple(string: &JavaStr) -> String { - java_str_to_string(string).unwrap() -} - pub fn java_str_to_valid_rust_argument_name(string: &JavaStr) -> Result<String> { Ok(format!( "arg_{}", diff --git a/jni-gen/systest/Cargo.toml b/jni-gen/systest/Cargo.toml index b7b22cd7639..833309c0871 100644 --- a/jni-gen/systest/Cargo.toml +++ b/jni-gen/systest/Cargo.toml @@ -15,4 +15,3 @@ tempfile = "3.3" error-chain = "0.12" jni = { version = "0.20", features = ["invocation"] } once_cell = "1.16" -jni-gen = { path = ".." } diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index e82fa3ca20a..d8271f23e2d 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -48,7 +48,7 @@ fn get_prusti_version_info() -> String { /// Report a readable error message in case of panic, with a link to open a new Prusti issue. fn report_prusti_ice(info: &panic::PanicInfo<'_>, bug_report_url: &str) { // Invoke our ICE handler, which prints the actual panic message and optionally a backtrace - // (*ICE_HOOK)(info); + (*ICE_HOOK)(info); // Separate the output with an empty line eprintln!(); diff --git a/viper-sys/Cargo.toml b/viper-sys/Cargo.toml index 716daa66279..28bd2675d1c 100644 --- a/viper-sys/Cargo.toml +++ b/viper-sys/Cargo.toml @@ -21,4 +21,3 @@ env_logger = "0.10" jni = { version = "0.20", features = ["invocation"] } log = { version = "0.4", features = ["release_max_level_info"] } once_cell = "1.16" -jni-gen = { path = "../jni-gen" } diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 43b85b59612..c7d0b3809d4 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -128,13 +128,10 @@ fn main() { object_getter!(), method!("apply"), ]), - java_class!("viper.silver.frontend.DefaultStates", vec![ method!("ConsistencyCheck"), method!("Verification"), ]), - - // Logger java_class!("viper.silver.logger.SilentLogger$", vec![ object_getter!(), method!("apply"), @@ -142,8 +139,6 @@ fn main() { java_class!("viper.silver.logger.ViperLogger", vec![ method!("get"), ]), - - // SiliconFrontend java_class!("viper.silicon.SiliconFrontend", vec![ constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"), method!("setVerifier"), @@ -152,12 +147,9 @@ fn main() { method!("getVerificationResult"), method!("setState"), method!("verifier"), - // field!("_program", "Lscala/Option;"), - // field!("_verifier", "Lscala/Option;"), field!("_program"), field!("_verifier"), ]), - // Silicon java_class!("viper.silicon.Silicon", vec![ constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"), From 76e03762824f9fef521eff92505355f225cab428 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 13 Mar 2023 17:31:05 +0900 Subject: [PATCH 13/33] additional temporary code removal --- viper/src/verification_context.rs | 9 +++------ viper/src/verifier.rs | 16 +++------------- 2 files changed, 6 insertions(+), 19 deletions(-) diff --git a/viper/src/verification_context.rs b/viper/src/verification_context.rs index 85d02b7c8ed..2537431c837 100644 --- a/viper/src/verification_context.rs +++ b/viper/src/verification_context.rs @@ -95,11 +95,8 @@ impl<'a> VerificationContext<'a> { debug!("Verifier arguments: '{}'", verifier_args.to_vec().join(" ")); - let ver = Verifier::new(&self.env, backend, report_path, smt_manager); - - ver.frontend_wrapper.call___program(ver.frontend_instance).expect("fail 3"); - ver.verifier_wrapper.call_name(ver.verifier_instance).expect("fail 5"); - - ver.parse_command_line(&verifier_args).start() + Verifier::new(&self.env, backend, report_path, smt_manager) + .parse_command_line(&verifier_args) + .start() } } diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index 4116762271c..a382a2b68dc 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -40,8 +40,8 @@ impl<'a> Verifier<'a> { let ast_utils = AstUtils::new(env); let verifier_wrapper = silver::verifier::Verifier::with(env); let frontend_wrapper = silicon::SiliconFrontend::with(env); - // let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || { - let frontend_instance = jni.unwrap_result(env.with_local_frame(128, || { + + 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"), @@ -70,13 +70,12 @@ impl<'a> Verifier<'a> { Ok(frontend_instance) })); - let verifier_instance = jni.unwrap_result(env.with_local_frame(128, || { + 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(); - println!("Set state"); 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)),); @@ -84,11 +83,6 @@ impl<'a> Verifier<'a> { Ok(verifier_instance) })); - let _x = verifier_wrapper.call_name(verifier_instance).expect("fail1"); - let _y = frontend_wrapper.call___program(frontend_instance).expect("fail2"); - - println!("THIS IS PASSING"); - Verifier { env, verifier_wrapper, @@ -175,13 +169,10 @@ impl<'a> Verifier<'a> { ); } - // set program - println!("set program"); let program_option = self.jni.new_option(Some(program.to_jobject())); self.jni.unwrap_result(self.frontend_wrapper.set___program(self.frontend_instance, program_option)); run_timed!("Viper verification", debug, - println!("calling verification"); 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)); @@ -392,7 +383,6 @@ impl<'a> Verifier<'a> { impl<'a> Drop for Verifier<'a> { fn drop(&mut self) { - println!("DROPVERIFIER"); // Tell the verifier to stop its threads. self.jni .unwrap_result(self.verifier_wrapper.call_stop(self.verifier_instance)); From 8117694805ef00a65899db65fdba251467678538 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 14 Mar 2023 03:36:26 +0900 Subject: [PATCH 14/33] Add "refute.failed:refutation.true" into error_manager --- prusti-viper/src/encoder/errors/error_manager.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index be1ee27faff..53d5e0e6c3d 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -698,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!( From e6b5692ea1812290705e48406d9a7a53d14b3107 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 14 Mar 2023 04:01:16 +0900 Subject: [PATCH 15/33] Remove unnecessary code, fmt-all --- prusti-interface/src/specs/typed.rs | 2 +- .../src/encoder/mir/specifications/specs.rs | 2 +- viper-sys/build.rs | 2 - viper/src/ast_factory/statement.rs | 3 +- viper/src/verifier.rs | 60 ++++++++++++------- vir/src/legacy/ast/stmt.rs | 2 +- 6 files changed, 42 insertions(+), 29 deletions(-) diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index b1d5879725d..2041266c555 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -174,7 +174,7 @@ impl DefSpecificationMap { let refutations: Vec<_> = self .prusti_refutations .values() - .map(|spec| format!("{:?}", spec)) + .map(|spec| format!("{spec:?}")) .collect(); let mut values = Vec::new(); values.extend(loop_specs); diff --git a/prusti-viper/src/encoder/mir/specifications/specs.rs b/prusti-viper/src/encoder/mir/specifications/specs.rs index cbc7c7e7fdf..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, PrustiRefutation, + PrustiAssumption, PrustiRefutation, Refinable, SpecificationItem, TypeSpecification, }, PrustiError, }; diff --git a/viper-sys/build.rs b/viper-sys/build.rs index c7d0b3809d4..e6abf26ad04 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -130,7 +130,6 @@ fn main() { ]), java_class!("viper.silver.frontend.DefaultStates", vec![ method!("ConsistencyCheck"), - method!("Verification"), ]), java_class!("viper.silver.logger.SilentLogger$", vec![ object_getter!(), @@ -142,7 +141,6 @@ fn main() { java_class!("viper.silicon.SiliconFrontend", vec![ constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"), method!("setVerifier"), - method!("_program"), method!("verification"), method!("getVerificationResult"), method!("setState"), diff --git a/viper/src/ast_factory/statement.rs b/viper/src/ast_factory/statement.rs index ace101842be..a2592f3539c 100644 --- a/viper/src/ast_factory/statement.rs +++ b/viper/src/ast_factory/statement.rs @@ -7,8 +7,7 @@ use crate::ast_factory::{ AstFactory, }; use jni::objects::JObject; -use viper_sys::wrappers::viper::silver::ast; -use viper_sys::wrappers::viper::silver::plugin::standard::refute; +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> { diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index a382a2b68dc..ffab5535211 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -19,14 +19,14 @@ use std::path::PathBuf; use viper_sys::wrappers::{scala, viper::*}; pub struct Verifier<'a> { - pub env: &'a JNIEnv<'a>, - pub verifier_wrapper: silver::verifier::Verifier<'a>, - pub verifier_instance: JObject<'a>, - pub frontend_wrapper: silicon::SiliconFrontend<'a>, - pub frontend_instance: JObject<'a>, - pub jni: JniUtils<'a>, - pub ast_utils: AstUtils<'a>, - pub smt_manager: SmtManager, + env: &'a JNIEnv<'a>, + verifier_wrapper: silver::verifier::Verifier<'a>, + verifier_instance: JObject<'a>, + frontend_wrapper: silicon::SiliconFrontend<'a>, + frontend_instance: JObject<'a>, + jni: JniUtils<'a>, + ast_utils: AstUtils<'a>, + smt_manager: SmtManager, } impl<'a> Verifier<'a> { @@ -40,7 +40,7 @@ impl<'a> Verifier<'a> { let ast_utils = AstUtils::new(env); let verifier_wrapper = silver::verifier::Verifier::with(env); let frontend_wrapper = silicon::SiliconFrontend::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( @@ -56,29 +56,45 @@ impl<'a> Verifier<'a> { 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 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 = silicon::SiliconFrontend::with(env).new(reporter, logger); + let unwrapped_frontend_instance = + silicon::SiliconFrontend::with(env).new(reporter, logger); let frontend_instance = jni.unwrap_result(unwrapped_frontend_instance); - frontend_wrapper.call_setVerifier(frontend_instance, backend_instance).unwrap(); + frontend_wrapper + .call_setVerifier(frontend_instance, backend_instance) + .unwrap(); let verifier_option = jni.new_option(Some(backend_instance)); - frontend_wrapper.set___verifier(frontend_instance, verifier_option).unwrap(); + frontend_wrapper + .set___verifier(frontend_instance, verifier_option) + .unwrap(); Ok(frontend_instance) })); 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)),); + 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) })); diff --git a/vir/src/legacy/ast/stmt.rs b/vir/src/legacy/ast/stmt.rs index d1529ceefc0..444bbe4988d 100644 --- a/vir/src/legacy/ast/stmt.rs +++ b/vir/src/legacy/ast/stmt.rs @@ -136,7 +136,7 @@ impl fmt::Display for Stmt { write!(f, "assert {expr}") } Stmt::Refute(ref expr, _) => { - write!(f, "refute {}", expr) + write!(f, "refute {expr}") } Stmt::MethodCall(ref name, ref args, ref vars) => write!( f, From cc7bb62dbfce6c33c5d59c1a7ef1da6a0e91ccb7 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 14 Mar 2023 04:08:16 +0900 Subject: [PATCH 16/33] cargo lock update --- Cargo.lock | 370 +++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 348 insertions(+), 22 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 2c6c8f3d5a1..201291ebd58 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -135,7 +135,7 @@ dependencies = [ "slab", "socket2", "waker-fn", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -163,7 +163,7 @@ dependencies = [ "futures-lite", "libc", "signal-hook", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -217,6 +217,21 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "065374052e7df7ee4047b1160cca5e1467a12351a40b3da123c870ba0b8eda2a" +[[package]] +name = "attohttpc" +version = "0.16.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fdb8867f378f33f78a811a8eb9bf108ad99430d7aad43315dd9319c827ef6247" +dependencies = [ + "flate2", + "http", + "log", + "native-tls", + "openssl", + "url", + "wildmatch", +] + [[package]] name = "atty" version = "0.2.14" @@ -364,7 +379,7 @@ dependencies = [ "glob", "itertools", "lazy_static", - "remove_dir_all", + "remove_dir_all 0.5.3", "serde_json", "snapbox", "tar", @@ -474,6 +489,17 @@ dependencies = [ "unicode-width", ] +[[package]] +name = "color-backtrace" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cd6c04463c99389fff045d2b90ce84f5131332712c7ffbede020f5e9ad1ed685" +dependencies = [ + "atty", + "backtrace", + "termcolor", +] + [[package]] name = "combine" version = "4.6.6" @@ -620,14 +646,38 @@ dependencies = [ [[package]] name = "crossbeam-channel" -version = "0.5.7" +version = "0.5.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2dd04ddaf88237dc3b8d8f9a3c1004b506b54b3313403944054d23c0870c521" +dependencies = [ + "cfg-if", + "crossbeam-utils", +] + +[[package]] +name = "crossbeam-deque" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf2b3e8478797446514c91ef04bafcb59faba183e621ad488df88983cc14128c" +checksum = "715e8152b692bba2d374b53d4875445368fdf21a94751410af607a5ac677d1fc" dependencies = [ "cfg-if", + "crossbeam-epoch", "crossbeam-utils", ] +[[package]] +name = "crossbeam-epoch" +version = "0.9.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "01a9af1f4c2ef74bb8aa1f7e19706bc72d03598c8a570bb5de72243c7a9d9d5a" +dependencies = [ + "autocfg", + "cfg-if", + "crossbeam-utils", + "memoffset 0.7.1", + "scopeguard", +] + [[package]] name = "crossbeam-utils" version = "0.8.14" @@ -697,8 +747,8 @@ version = "3.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1631ca6e3c59112501a9d87fd86f21591ff77acd31331e8a73f8d80a65bbdd71" dependencies = [ - "nix", - "windows-sys", + "nix 0.26.1", + "windows-sys 0.42.0", ] [[package]] @@ -898,6 +948,28 @@ version = "2.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0206175f82b8d6bf6652ff7d71a1e27fd2e4efde587fd368662814d6ec1d9ce0" +[[package]] +name = "failure" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d32e9bd16cc02eae7db7ef620b392808b89f6a5e16bb3497d159c6b92a0f4f86" +dependencies = [ + "backtrace", + "failure_derive", +] + +[[package]] +name = "failure_derive" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aa4da3c766cd7a0db8242e326e9e4e081edd567072893ed320008189715366a4" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "synstructure", +] + [[package]] name = "fastrand" version = "1.8.0" @@ -916,7 +988,7 @@ dependencies = [ "cfg-if", "libc", "redox_syscall", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -960,6 +1032,16 @@ dependencies = [ "percent-encoding", ] +[[package]] +name = "fs2" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9564fc758e15025b46aa6643b1b77d047d1a56a1aea6e01002ac0c7026876213" +dependencies = [ + "libc", + "winapi", +] + [[package]] name = "futures" version = "0.3.25" @@ -1368,7 +1450,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "46112a93252b123d31a119a8d1a1ac19deac4fac6e0e8b0df58f0d4e5870e63c" dependencies = [ "libc", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -1386,7 +1468,7 @@ dependencies = [ "hermit-abi 0.2.6", "io-lifetimes", "rustix", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -1593,6 +1675,15 @@ version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" +[[package]] +name = "memoffset" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5aa361d4faea93603064a027415f07bd8e1d5c88c9fbf68bf56a285428fd79ce" +dependencies = [ + "autocfg", +] + [[package]] name = "memoffset" version = "0.7.1" @@ -1642,7 +1733,7 @@ dependencies = [ "libc", "log", "wasi", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -1672,6 +1763,38 @@ dependencies = [ "twoway", ] +[[package]] +name = "native-tls" +version = "0.2.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "07226173c32f2926027b63cce4bcd8076c3552846cbe7925f3aaffeac0a3b92e" +dependencies = [ + "lazy_static", + "libc", + "log", + "openssl", + "openssl-probe", + "openssl-sys", + "schannel", + "security-framework", + "security-framework-sys", + "tempfile", +] + +[[package]] +name = "nix" +version = "0.25.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f346ff70e7dbfd675fe90590b92d59ef2de15a8779ae305ebcbfd3f0caf59be4" +dependencies = [ + "autocfg", + "bitflags", + "cfg-if", + "libc", + "memoffset 0.6.5", + "pin-utils", +] + [[package]] name = "nix" version = "0.26.1" @@ -1681,7 +1804,7 @@ dependencies = [ "bitflags", "cfg-if", "libc", - "memoffset", + "memoffset 0.7.1", "pin-utils", "static_assertions", ] @@ -1934,7 +2057,7 @@ dependencies = [ "libc", "log", "wepoll-ffi", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -2129,7 +2252,7 @@ dependencies = [ "itertools", "lazy_static", "log", - "nix", + "nix 0.26.1", "rustc-hash", "serde", "toml", @@ -2208,6 +2331,28 @@ dependencies = [ "getrandom", ] +[[package]] +name = "rayon" +version = "1.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6db3a213adf02b3bcfd2d3846bb41cb22857d131789e01df434fb7e7bc0759b7" +dependencies = [ + "either", + "rayon-core", +] + +[[package]] +name = "rayon-core" +version = "1.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "356a0625f1954f730c0201cdab48611198dc6ce21f4acff55089b5a78e6e835b" +dependencies = [ + "crossbeam-channel", + "crossbeam-deque", + "crossbeam-utils", + "num_cpus", +] + [[package]] name = "redox_syscall" version = "0.2.16" @@ -2263,6 +2408,19 @@ dependencies = [ "winapi", ] +[[package]] +name = "remove_dir_all" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "882f368737489ea543bc5c340e6f3d34a28c39980bd9a979e47322b26f60ac40" +dependencies = [ + "libc", + "log", + "num_cpus", + "rayon", + "winapi", +] + [[package]] name = "reqwest" version = "0.11.13" @@ -2382,7 +2540,7 @@ dependencies = [ "io-lifetimes", "libc", "linux-raw-sys", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -2421,6 +2579,39 @@ version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5583e89e108996506031660fe09baa5011b9dd0341b89029313006d1fb508d70" +[[package]] +name = "rustwide" +version = "0.15.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1b0070cdf593a5b66ba6160974bbfb504a837f8c06f3357a623c9a7b6619c64" +dependencies = [ + "attohttpc", + "base64 0.13.1", + "failure", + "flate2", + "fs2", + "futures-util", + "getrandom", + "git2", + "http", + "lazy_static", + "log", + "nix 0.25.1", + "percent-encoding", + "remove_dir_all 0.7.0", + "scopeguard", + "serde", + "serde_json", + "tar", + "tempfile", + "thiserror", + "tokio", + "tokio-stream", + "toml", + "walkdir", + "windows-sys 0.36.1", +] + [[package]] name = "ryu" version = "1.0.12" @@ -2442,12 +2633,27 @@ dependencies = [ "winapi-util", ] +[[package]] +name = "schannel" +version = "0.1.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "713cfb06c7059f3588fb8044c0fad1d09e3c01d225e25b9220dbfdcf16dbb1b3" +dependencies = [ + "windows-sys 0.42.0", +] + [[package]] name = "scoped-tls" version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e1cf6437eb19a8f4a6cc0f7dca544973b0b78843adbfeb3683d1a94a0024a294" +[[package]] +name = "scopeguard" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" + [[package]] name = "scratch" version = "1.0.3" @@ -2464,6 +2670,29 @@ dependencies = [ "untrusted", ] +[[package]] +name = "security-framework" +version = "2.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a332be01508d814fed64bf28f798a146d73792121129962fdf335bb3c49a4254" +dependencies = [ + "bitflags", + "core-foundation", + "core-foundation-sys", + "libc", + "security-framework-sys", +] + +[[package]] +name = "security-framework-sys" +version = "2.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "31c9bb296072e961fcbd8853511dd39c2d8be2deb1e17c6860b1d30732b323b4" +dependencies = [ + "core-foundation-sys", + "libc", +] + [[package]] name = "semver" version = "1.0.16" @@ -2661,6 +2890,18 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "synstructure" +version = "0.12.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "unicode-xid", +] + [[package]] name = "systest" version = "0.1.0" @@ -2682,6 +2923,7 @@ checksum = "4b55807c0344e1e6c04d7c965f5289c39a8d94ae23ed5c0b57aabac549f871c6" dependencies = [ "filetime", "libc", + "xattr", ] [[package]] @@ -2694,7 +2936,7 @@ dependencies = [ "fastrand", "libc", "redox_syscall", - "remove_dir_all", + "remove_dir_all 0.5.3", "winapi", ] @@ -2718,6 +2960,24 @@ dependencies = [ "winapi-util", ] +[[package]] +name = "test-crates" +version = "0.1.0" +dependencies = [ + "clap", + "color-backtrace", + "csv", + "env_logger", + "failure", + "glob", + "log", + "prusti", + "prusti-launch", + "rustwide", + "serde", + "toml", +] + [[package]] name = "tester" version = "0.9.0" @@ -2787,9 +3047,11 @@ dependencies = [ "libc", "memchr", "mio", + "num_cpus", "pin-project-lite", + "signal-hook-registry", "socket2", - "windows-sys", + "windows-sys 0.42.0", ] [[package]] @@ -3033,6 +3295,12 @@ version = "0.1.10" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" +[[package]] +name = "unicode-xid" +version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f962df74c8c05a667b5ee8bcf162993134c104e96440b663c8daa176dc772d8c" + [[package]] name = "untrusted" version = "0.7.1" @@ -3353,6 +3621,12 @@ dependencies = [ "cc", ] +[[package]] +name = "wildmatch" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7f44b95f62d34113cf558c93511ac93027e03e9c29a60dd0fd70e6e025c7270a" + [[package]] name = "winapi" version = "0.3.9" @@ -3384,6 +3658,19 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-sys" +version = "0.36.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ea04155a16a59f9eab786fe12a4a450e75cdb175f9e0d80da1e17db09f55b8d2" +dependencies = [ + "windows_aarch64_msvc 0.36.1", + "windows_i686_gnu 0.36.1", + "windows_i686_msvc 0.36.1", + "windows_x86_64_gnu 0.36.1", + "windows_x86_64_msvc 0.36.1", +] + [[package]] name = "windows-sys" version = "0.42.0" @@ -3391,12 +3678,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5a3e1820f08b8513f676f7ab6c1f99ff312fb97b553d30ff4dd86f9f15728aa7" dependencies = [ "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_msvc", - "windows_x86_64_gnu", + "windows_aarch64_msvc 0.42.0", + "windows_i686_gnu 0.42.0", + "windows_i686_msvc 0.42.0", + "windows_x86_64_gnu 0.42.0", "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_x86_64_msvc 0.42.0", ] [[package]] @@ -3405,24 +3692,48 @@ version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "41d2aa71f6f0cbe00ae5167d90ef3cfe66527d6f613ca78ac8024c3ccab9a19e" +[[package]] +name = "windows_aarch64_msvc" +version = "0.36.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9bb8c3fd39ade2d67e9874ac4f3db21f0d710bee00fe7cab16949ec184eeaa47" + [[package]] name = "windows_aarch64_msvc" version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dd0f252f5a35cac83d6311b2e795981f5ee6e67eb1f9a7f64eb4500fbc4dcdb4" +[[package]] +name = "windows_i686_gnu" +version = "0.36.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "180e6ccf01daf4c426b846dfc66db1fc518f074baa793aa7d9b9aaeffad6a3b6" + [[package]] name = "windows_i686_gnu" version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fbeae19f6716841636c28d695375df17562ca208b2b7d0dc47635a50ae6c5de7" +[[package]] +name = "windows_i686_msvc" +version = "0.36.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2e7917148b2812d1eeafaeb22a97e4813dfa60a3f8f78ebe204bcc88f12f024" + [[package]] name = "windows_i686_msvc" version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "84c12f65daa39dd2babe6e442988fc329d6243fdce47d7d2d155b8d874862246" +[[package]] +name = "windows_x86_64_gnu" +version = "0.36.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4dcd171b8776c41b97521e5da127a2d86ad280114807d0b2ab1e462bc764d9e1" + [[package]] name = "windows_x86_64_gnu" version = "0.42.0" @@ -3435,6 +3746,12 @@ version = "0.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09d525d2ba30eeb3297665bd434a54297e4170c7f1a44cad4ef58095b4cd2028" +[[package]] +name = "windows_x86_64_msvc" +version = "0.36.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c811ca4a8c853ef420abd8592ba53ddbbac90410fab6903b3e79972a631f7680" + [[package]] name = "windows_x86_64_msvc" version = "0.42.0" @@ -3450,6 +3767,15 @@ dependencies = [ "winapi", ] +[[package]] +name = "xattr" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d1526bbe5aaeb5eb06885f4d987bcdfa5e23187055de9b83fe00156a821fabc" +dependencies = [ + "libc", +] + [[package]] name = "yaml-rust" version = "0.4.5" From fc2bda88e0b7a16b6c998f5731a1a54a340cce6f Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Fri, 17 Mar 2023 17:03:07 +0900 Subject: [PATCH 17/33] add frotend support also for carbon --- viper-sys/build.rs | 10 +++++++ viper/src/verifier.rs | 68 +++++++++++++++++++++++++++++-------------- 2 files changed, 56 insertions(+), 22 deletions(-) diff --git a/viper-sys/build.rs b/viper-sys/build.rs index e6abf26ad04..3666bcf5d3a 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -148,6 +148,16 @@ fn main() { field!("_program"), field!("_verifier"), ]), + java_class!("viper.carbon.CarbonFrontend", vec![ + constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"), + method!("setVerifier"), + method!("verification"), + method!("getVerificationResult"), + method!("setState"), + method!("verifier"), + field!("_program"), + field!("_verifier"), + ]), // Silicon java_class!("viper.silicon.Silicon", vec![ constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"), diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index ffab5535211..9038ad5b8ba 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -22,11 +22,13 @@ pub struct Verifier<'a> { env: &'a JNIEnv<'a>, verifier_wrapper: silver::verifier::Verifier<'a>, verifier_instance: JObject<'a>, - frontend_wrapper: silicon::SiliconFrontend<'a>, + frontend_silicon_wrapper: silicon::SiliconFrontend<'a>, + frontend_carbon_wrapper: carbon::CarbonFrontend<'a>, frontend_instance: JObject<'a>, jni: JniUtils<'a>, ast_utils: AstUtils<'a>, smt_manager: SmtManager, + backend: VerificationBackend, } impl<'a> Verifier<'a> { @@ -39,7 +41,8 @@ impl<'a> Verifier<'a> { let jni = JniUtils::new(env); let ast_utils = AstUtils::new(env); let verifier_wrapper = silver::verifier::Verifier::with(env); - let frontend_wrapper = silicon::SiliconFrontend::with(env); + let frontend_silicon_wrapper = silicon::SiliconFrontend::with(env); + let frontend_carbon_wrapper = carbon::CarbonFrontend::with(env); let frontend_instance = jni.unwrap_result(env.with_local_frame(16, || { let reporter = if let Some(real_report_path) = report_path { @@ -64,31 +67,42 @@ impl<'a> Verifier<'a> { let logger = jni.unwrap_result(silver::logger::ViperLogger::with(env).call_get(logger_factory)); - let unwrapped_frontend_instance = - silicon::SiliconFrontend::with(env).new(reporter, logger); + 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(); + match backend { + VerificationBackend::Silicon => frontend_silicon_wrapper.call_setVerifier(frontend_instance, backend_instance).unwrap(), + VerificationBackend::Carbon => frontend_carbon_wrapper.call_setVerifier(frontend_instance, backend_instance).unwrap(), + } let verifier_option = jni.new_option(Some(backend_instance)); - frontend_wrapper - .set___verifier(frontend_instance, verifier_option) - .unwrap(); + + match backend { + VerificationBackend::Silicon => frontend_silicon_wrapper.set___verifier(frontend_instance, verifier_option).unwrap(), + VerificationBackend::Carbon => frontend_carbon_wrapper.set___verifier(frontend_instance, verifier_option).unwrap(), + } Ok(frontend_instance) })); let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || { - let verifier_instance = - jni.unwrap_result(frontend_wrapper.call_verifier(frontend_instance)); + let verifier_instance = match backend { + VerificationBackend::Silicon => jni.unwrap_result(frontend_silicon_wrapper.call_verifier(frontend_instance)), + VerificationBackend::Carbon => jni.unwrap_result(frontend_carbon_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(); + + match backend { + VerificationBackend::Silicon => frontend_silicon_wrapper.call_setState(frontend_instance, consistency_check_state).unwrap(), + VerificationBackend::Carbon => frontend_carbon_wrapper.call_setState(frontend_instance, consistency_check_state).unwrap(), + } let name = jni.to_string(jni.unwrap_result(verifier_wrapper.call_name(verifier_instance))); @@ -103,11 +117,13 @@ impl<'a> Verifier<'a> { env, verifier_wrapper, verifier_instance, - frontend_wrapper, + frontend_silicon_wrapper, + frontend_carbon_wrapper, frontend_instance, jni, ast_utils, smt_manager, + backend, } } @@ -120,9 +136,7 @@ impl<'a> Verifier<'a> { ) -> Result<JObject<'a>> { match backend { VerificationBackend::Silicon => silicon::Silicon::with(env).new(reporter, debug_info), - VerificationBackend::Carbon => { - panic!("Trying to use Carbon backend - now made compatible just with Silicon"); - } + VerificationBackend::Carbon => carbon::CarbonVerifier::with(env).new(reporter, debug_info) } } @@ -156,6 +170,7 @@ impl<'a> Verifier<'a> { #[tracing::instrument(name = "viper::verify", level = "debug", skip_all)] pub fn verify(&mut self, program: Program) -> VerificationResult { + let ast_utils = self.ast_utils; ast_utils.with_local_frame(16, || { debug!( @@ -186,11 +201,20 @@ impl<'a> Verifier<'a> { } let program_option = self.jni.new_option(Some(program.to_jobject())); - self.jni.unwrap_result(self.frontend_wrapper.set___program(self.frontend_instance, program_option)); + match self.backend { + VerificationBackend::Silicon => self.jni.unwrap_result(self.frontend_silicon_wrapper.set___program(self.frontend_instance, program_option)), + VerificationBackend::Carbon => self.jni.unwrap_result(self.frontend_carbon_wrapper.set___program(self.frontend_instance, program_option)), + }; run_timed!("Viper verification", debug, - 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)); + match self.backend { + VerificationBackend::Silicon => self.jni.unwrap_result(self.frontend_silicon_wrapper.call_verification(self.frontend_instance)), + VerificationBackend::Carbon => self.jni.unwrap_result(self.frontend_carbon_wrapper.call_verification(self.frontend_instance)), + }; + let viper_result_option = match self.backend { + VerificationBackend::Silicon => self.jni.unwrap_result(self.frontend_silicon_wrapper.call_getVerificationResult(self.frontend_instance)), + VerificationBackend::Carbon => self.jni.unwrap_result(self.frontend_carbon_wrapper.call_getVerificationResult(self.frontend_instance)), + }; let viper_result = self.jni.unwrap_result(scala::Some::with(self.env).call_get(viper_result_option)); ); From d0ad6a6fef3dc16301a3d9dbfbb2ae5b769c4ee2 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Sun, 19 Mar 2023 14:55:02 +0900 Subject: [PATCH 18/33] add assert.failed:assertion.false-PanicCause::Refute entry to the error manager --- prusti-viper/src/encoder/errors/error_manager.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 53d5e0e6c3d..5d9e6cc0a67 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -705,6 +705,13 @@ impl<'tcx> ErrorManager<'tcx> { ) } + ("assert.failed:assertion.false", 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!( From 6867a3bf03ba89a6da7558195e41302f961ee52e Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 21 Mar 2023 02:41:07 +0900 Subject: [PATCH 19/33] Add field access via Scala methods, use SilFrontend wrapper and remove unecessary dispatch --- viper-sys/build.rs | 49 +++++++++++++++----------------- viper/src/verifier.rs | 65 +++++++++++++++++-------------------------- 2 files changed, 48 insertions(+), 66 deletions(-) diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 3666bcf5d3a..7433cbe5348 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -128,45 +128,30 @@ fn main() { object_getter!(), method!("apply"), ]), - 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"), + // Silicon + 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"), - method!("setVerifier"), - method!("verification"), - method!("getVerificationResult"), - method!("setState"), - method!("verifier"), - field!("_program"), - field!("_verifier"), + ]), + // 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"), - field!("_program"), - field!("_verifier"), - ]), - // Silicon - java_class!("viper.silicon.Silicon", vec![ - constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"), + method!("_verifier_$eq"), + method!("_program_$eq"), ]), - // Carbon - java_class!("viper.carbon.CarbonVerifier", vec![ - constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"), - ]), - // Silver java_class!("viper.silver.reporter.CSVReporter", vec![ constructor!("(Ljava/lang/String;Ljava/lang/String;)V"), ]), @@ -181,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;") diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index 9038ad5b8ba..eb41ff5bb9a 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -22,13 +22,11 @@ pub struct Verifier<'a> { env: &'a JNIEnv<'a>, verifier_wrapper: silver::verifier::Verifier<'a>, verifier_instance: JObject<'a>, - frontend_silicon_wrapper: silicon::SiliconFrontend<'a>, - frontend_carbon_wrapper: carbon::CarbonFrontend<'a>, + frontend_wrapper: silver::frontend::SilFrontend<'a>, frontend_instance: JObject<'a>, jni: JniUtils<'a>, ast_utils: AstUtils<'a>, smt_manager: SmtManager, - backend: VerificationBackend, } impl<'a> Verifier<'a> { @@ -41,8 +39,7 @@ impl<'a> Verifier<'a> { let jni = JniUtils::new(env); let ast_utils = AstUtils::new(env); let verifier_wrapper = silver::verifier::Verifier::with(env); - let frontend_silicon_wrapper = silicon::SiliconFrontend::with(env); - let frontend_carbon_wrapper = carbon::CarbonFrontend::with(env); + 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 { @@ -69,40 +66,39 @@ impl<'a> Verifier<'a> { let unwrapped_frontend_instance = { match backend { - VerificationBackend::Silicon => silicon::SiliconFrontend::with(env).new(reporter, logger), - VerificationBackend::Carbon => carbon::CarbonFrontend::with(env).new(reporter, logger), + 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); - match backend { - VerificationBackend::Silicon => frontend_silicon_wrapper.call_setVerifier(frontend_instance, backend_instance).unwrap(), - VerificationBackend::Carbon => frontend_carbon_wrapper.call_setVerifier(frontend_instance, backend_instance).unwrap(), - } + frontend_wrapper + .call_setVerifier(frontend_instance, backend_instance) + .unwrap(); let verifier_option = jni.new_option(Some(backend_instance)); - match backend { - VerificationBackend::Silicon => frontend_silicon_wrapper.set___verifier(frontend_instance, verifier_option).unwrap(), - VerificationBackend::Carbon => frontend_carbon_wrapper.set___verifier(frontend_instance, verifier_option).unwrap(), - } + frontend_wrapper + .call___verifier___dollar_eq(frontend_instance, verifier_option) + .unwrap(); Ok(frontend_instance) })); let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || { - let verifier_instance = match backend { - VerificationBackend::Silicon => jni.unwrap_result(frontend_silicon_wrapper.call_verifier(frontend_instance)), - VerificationBackend::Carbon => jni.unwrap_result(frontend_carbon_wrapper.call_verifier(frontend_instance)), - }; + let verifier_instance = + jni.unwrap_result(frontend_wrapper.call_verifier(frontend_instance)); let consistency_check_state = silver::frontend::DefaultStates::with(env) .call_ConsistencyCheck() .unwrap(); - match backend { - VerificationBackend::Silicon => frontend_silicon_wrapper.call_setState(frontend_instance, consistency_check_state).unwrap(), - VerificationBackend::Carbon => frontend_carbon_wrapper.call_setState(frontend_instance, consistency_check_state).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))); @@ -117,13 +113,11 @@ impl<'a> Verifier<'a> { env, verifier_wrapper, verifier_instance, - frontend_silicon_wrapper, - frontend_carbon_wrapper, + frontend_wrapper, frontend_instance, jni, ast_utils, smt_manager, - backend, } } @@ -136,7 +130,9 @@ impl<'a> Verifier<'a> { ) -> Result<JObject<'a>> { match backend { VerificationBackend::Silicon => silicon::Silicon::with(env).new(reporter, debug_info), - VerificationBackend::Carbon => carbon::CarbonVerifier::with(env).new(reporter, debug_info) + VerificationBackend::Carbon => { + carbon::CarbonVerifier::with(env).new(reporter, debug_info) + } } } @@ -201,20 +197,11 @@ impl<'a> Verifier<'a> { } let program_option = self.jni.new_option(Some(program.to_jobject())); - match self.backend { - VerificationBackend::Silicon => self.jni.unwrap_result(self.frontend_silicon_wrapper.set___program(self.frontend_instance, program_option)), - VerificationBackend::Carbon => self.jni.unwrap_result(self.frontend_carbon_wrapper.set___program(self.frontend_instance, program_option)), - }; + self.jni.unwrap_result(self.frontend_wrapper.call___program___dollar_eq(self.frontend_instance, program_option)); run_timed!("Viper verification", debug, - match self.backend { - VerificationBackend::Silicon => self.jni.unwrap_result(self.frontend_silicon_wrapper.call_verification(self.frontend_instance)), - VerificationBackend::Carbon => self.jni.unwrap_result(self.frontend_carbon_wrapper.call_verification(self.frontend_instance)), - }; - let viper_result_option = match self.backend { - VerificationBackend::Silicon => self.jni.unwrap_result(self.frontend_silicon_wrapper.call_getVerificationResult(self.frontend_instance)), - VerificationBackend::Carbon => self.jni.unwrap_result(self.frontend_carbon_wrapper.call_getVerificationResult(self.frontend_instance)), - }; + 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)); ); From 04153957a6b993532b99e11408e3304374653f2f Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 21 Mar 2023 03:21:38 +0900 Subject: [PATCH 20/33] Remove empty line - fmt-all error --- viper/src/verifier.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index eb41ff5bb9a..2be37927853 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -166,7 +166,6 @@ impl<'a> Verifier<'a> { #[tracing::instrument(name = "viper::verify", level = "debug", skip_all)] pub fn verify(&mut self, program: Program) -> VerificationResult { - let ast_utils = self.ast_utils; ast_utils.with_local_frame(16, || { debug!( From 2695bafef4060527f5f19334419bbfaf947fae0b Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 21 Mar 2023 18:23:55 +0900 Subject: [PATCH 21/33] add tests for prusti_refute! --- .../prusti_assert.rs | 0 .../assert_assume_refute/prusti_refute.rs | 30 +++++++++++++++++++ .../simple_assert.rs | 0 3 files changed, 30 insertions(+) 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/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..bf27239cf4e --- /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() {} \ No newline at end of file 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 From a207e107679f47fb0b9e7bc0347c81a6f09e9e7c Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 21 Mar 2023 19:15:43 +0900 Subject: [PATCH 22/33] update docs (user guide) - add mention to refute --- docs/user-guide/src/SUMMARY.md | 2 +- ...sert_assume.md => assert_refute_assume.md} | 35 ++++++++++++++++++- docs/user-guide/src/verify/summary.md | 2 +- 3 files changed, 36 insertions(+), 3 deletions(-) rename docs/user-guide/src/verify/{assert_assume.md => assert_refute_assume.md} (65%) 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 65% rename from docs/user-guide/src/verify/assert_assume.md rename to docs/user-guide/src/verify/assert_refute_assume.md index 1bfd7da2339..fa4f3812a3d 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,39 @@ 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 + +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) From e6897da33702ecbae024252cffde8ab13f582c9b Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 27 Mar 2023 16:55:00 +0900 Subject: [PATCH 23/33] trying to figure out positions for added refutes --- docs/dev-guide/src/config/flags.md | 5 ++ prusti-utils/src/config.rs | 5 ++ prusti-viper/src/encoder/procedure_encoder.rs | 75 ++++++++++++++++++- 3 files changed, 84 insertions(+), 1 deletion(-) diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index b3ef1913dc9..b8abb82c915 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -15,6 +15,7 @@ | [`CHECK_TIMEOUT`](#check_timeout) | `Option<u32>` | `None` | A | | [`COUNTEREXAMPLE`](#counterexample) | `bool` | `false` | A | | [`DELETE_BASIC_BLOCKS`](#delete_basic_blocks) | `Vec<String>` | `vec![]` | A | +| [`DETECT_UNREACHABLE_CODE`](#detect_unreachable_code) | `bool` | `false` | A | | [`DISABLE_NAME_MANGLING`](#disable_name_mangling) | `bool` | `false` | A | | [`DUMP_BORROWCK_INFO`](#dump_borrowck_info) | `bool` | `false` | A | | [`DUMP_DEBUG_INFO`](#dump_debug_info) | `bool` | `false` | A | @@ -146,6 +147,10 @@ When enabled, Prusti will try to find and print a counterexample for any failed The given basic blocks will be replaced with `assume false`. +## `DETECT_UNREACHABLE_CODE` + +When enabled, Viper will issue warning for code that cannot be reached. + ## `DISABLE_NAME_MANGLING` When enabled, Viper name mangling will be disabled. diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 65a6bc9e624..aef6985a9dc 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -129,6 +129,7 @@ lazy_static::lazy_static! { settings.set_default("use_new_encoder", true).unwrap(); settings.set_default::<Option<u8>>("number_of_parallel_verifiers", None).unwrap(); settings.set_default::<Option<String>>("min_prusti_version", None).unwrap(); + settings.set_default("detect_unreachable_code", false).unwrap(); settings.set_default("print_desugared_specs", false).unwrap(); settings.set_default("print_typeckd_specs", false).unwrap(); @@ -958,6 +959,10 @@ pub fn delete_basic_blocks() -> Vec<String> { read_setting("delete_basic_blocks") } +pub fn detect_unreachable_code() -> bool { + read_setting("detect_unreachable_code") +} + /// When enabled, features not supported by Prusti will be reported as warnings /// rather than errors. pub fn skip_unsupported_features() -> bool { diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 944af6051da..60e55bef1e0 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -66,7 +66,7 @@ use prusti_interface::environment::borrowck::regions::PlaceRegionsError; use crate::encoder::errors::EncodingErrorKind; use std::convert::TryInto; use prusti_interface::specs::typed::{Pledge, SpecificationItem}; -use vir_crate::polymorphic::Float; +use vir_crate::polymorphic::{Float, Position, Stmt, Expr}; use crate::utils::is_reference; use crate::encoder::mir::{ sequences::MirSequencesEncoderInterface, @@ -135,6 +135,78 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { substs: SubstsRef<'tcx>, } +fn get_first_position(statements: &Vec<Stmt>) -> Option<Position> { + for statement in statements { + match statement { + Stmt::Comment(_) => (), + Stmt::Label(_) => (), + Stmt::Inhale(inhale) => return Some(inhale.expr.pos()), + Stmt::Exhale(exhale) => return Some(exhale.position), + Stmt::Assert(assert) => return Some(assert.position), + Stmt::Refute(refute) => return Some(refute.position), + // Stmt::MethodCall(method_call) => { + // for expression in method_call.arguments { + // if expression.pos() != Position::default() { + // return Some(expression.pos()); + // } + // } + // None + // }, + Stmt::Assign(assign) => return Some(assign.target.pos()), + Stmt::Fold(fold) => return Some(fold.position), + // Stmt::Unfold(_) => todo!(), + // Stmt::Obtain(_) => todo!(), + // Stmt::BeginFrame(_) => todo!(), + // Stmt::EndFrame(_) => todo!(), + // Stmt::TransferPerm(_) => todo!(), + // Stmt::PackageMagicWand(_) => todo!(), + // Stmt::ApplyMagicWand(_) => todo!(), + // Stmt::ExpireBorrows(_) => todo!(), + // Stmt::If(_) => todo!(), + // Stmt::Downcast(_) => todo!(), + _ => (), + } + } + None +} + +// fn add_unreachable_code_check(&mut self) { +fn add_unreachable_code_check(mut method: vir::CfgMethod, encoder: &Encoder, mir_encorder: &MirEncoder) -> vir::CfgMethod { + for block in method.basic_blocks.iter_mut() { + if let Some(position) = get_first_position(&block.stmts) { + // let span: Span = encoder.error_manager().position_manager().get_span(position).unwrap().primary_span().unwrap(); + // let position = Position::new(4, 17, 11); + let position = encoder.error_manager().duplicate_position(position); + encoder.error_manager().set_error(position, ErrorCtxt::Panic(PanicCause::Refute)); + // let a = self.encoder.error_manager(); + // let b = a.position_manager(); + // let c = b.duplicate(position); + // let position_copy = self.encoder.error_manager().position_manager().duplicate(position); + + // let position = mir_encorder.register_error(span, ErrorCtxt::Panic(PanicCause::Refute)); + let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{ + value: vir::ast::expr::Const::Bool(false), + position, + }); + + let refute_stmt = vir::Stmt::Refute( + vir::Refute { + expr: refute_expr, + position, + } + ); + + block.stmts.reverse(); + let comment = block.stmts.pop().unwrap(); + block.stmts.push(refute_stmt); + block.stmts.push(comment); + block.stmts.reverse(); + println!("After reverse {:?}\n", block.stmts); + } + } + method +} + impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { #[tracing::instrument(name = "ProcedureEncoder::new", level = "debug", skip_all, fields(proc_def_id = ?procedure.get_id()))] pub fn new( @@ -584,6 +656,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // Fix variable declarations. let method_with_fold_unfold = fix_ghost_vars(method_with_fold_unfold); + let method_with_fold_unfold = add_unreachable_code_check(method_with_fold_unfold, &self.encoder, &self.mir_encoder); // Dump final CFG if config::dump_debug_info() { prusti_common::report::log::report_with_writer( From e71787af1047cf2ed85f2664e4254605cf935a79 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 28 Mar 2023 17:25:31 +0900 Subject: [PATCH 24/33] use terminator span --- prusti-viper/src/encoder/procedure_encoder.rs | 286 +++++++++++++----- 1 file changed, 216 insertions(+), 70 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 60e55bef1e0..41c8569acee 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -135,77 +135,188 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { substs: SubstsRef<'tcx>, } -fn get_first_position(statements: &Vec<Stmt>) -> Option<Position> { - for statement in statements { - match statement { - Stmt::Comment(_) => (), - Stmt::Label(_) => (), - Stmt::Inhale(inhale) => return Some(inhale.expr.pos()), - Stmt::Exhale(exhale) => return Some(exhale.position), - Stmt::Assert(assert) => return Some(assert.position), - Stmt::Refute(refute) => return Some(refute.position), - // Stmt::MethodCall(method_call) => { - // for expression in method_call.arguments { - // if expression.pos() != Position::default() { - // return Some(expression.pos()); - // } - // } - // None - // }, - Stmt::Assign(assign) => return Some(assign.target.pos()), - Stmt::Fold(fold) => return Some(fold.position), - // Stmt::Unfold(_) => todo!(), - // Stmt::Obtain(_) => todo!(), - // Stmt::BeginFrame(_) => todo!(), - // Stmt::EndFrame(_) => todo!(), - // Stmt::TransferPerm(_) => todo!(), - // Stmt::PackageMagicWand(_) => todo!(), - // Stmt::ApplyMagicWand(_) => todo!(), - // Stmt::ExpireBorrows(_) => todo!(), - // Stmt::If(_) => todo!(), - // Stmt::Downcast(_) => todo!(), - _ => (), - } - } - None -} - -// fn add_unreachable_code_check(&mut self) { -fn add_unreachable_code_check(mut method: vir::CfgMethod, encoder: &Encoder, mir_encorder: &MirEncoder) -> vir::CfgMethod { - for block in method.basic_blocks.iter_mut() { - if let Some(position) = get_first_position(&block.stmts) { - // let span: Span = encoder.error_manager().position_manager().get_span(position).unwrap().primary_span().unwrap(); - // let position = Position::new(4, 17, 11); - let position = encoder.error_manager().duplicate_position(position); - encoder.error_manager().set_error(position, ErrorCtxt::Panic(PanicCause::Refute)); - // let a = self.encoder.error_manager(); - // let b = a.position_manager(); - // let c = b.duplicate(position); - // let position_copy = self.encoder.error_manager().position_manager().duplicate(position); +// fn statement_position(statement: &Stmt) -> Option<Position> { +// match statement { +// vir::Stmt::Comment(_) => None, +// vir::Stmt::Label(_) => None, +// vir::Stmt::Inhale(inhale) => Some(inhale.expr.pos()), +// vir::Stmt::Exhale(exhale) => Some(exhale.position), +// vir::Stmt::Assert(assert) => Some(assert.position), +// vir::Stmt::Refute(refute) => Some(refute.position), +// // vir::Stmt::MethodCall(method_call) => { +// // for expression in method_call.arguments { +// // if expression.pos() != Position::default() { +// // return Some(expression.pos()); +// // } +// // } +// // None +// // }, +// vir::Stmt::Assign(assign) => Some(assign.target.pos()), +// vir::Stmt::Fold(fold) => Some(fold.position), +// // vir::Stmt::Unfold(_) => todo!(), +// // vir::Stmt::Obtain(_) => todo!(), +// // vir::Stmt::BeginFrame(_) => todo!(), +// // vir::Stmt::EndFrame(_) => todo!(), +// // vir::Stmt::TransferPerm(_) => todo!(), +// // vir::Stmt::PackageMagicWand(_) => todo!(), +// // vir::Stmt::ApplyMagicWand(_) => todo!(), +// // vir::Stmt::ExpireBorrows(_) => todo!(), +// // vir::Stmt::If(_) => todo!(), +// // vir::Stmt::Downcast(_) => todo!(), +// _ => None, +// } +// } + + +// 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)?; +// println!("refute expression: {:?}", refute_expr); + +// 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); + +// pub fn insert_refutes(mut method: vir::CfgMethod) -> vir::CfgMethod { +// let mut first_position: Option<Position> = None; +// for block in method.basic_blocks.iter_mut() { +// // for statement in block.stmts { +// // if let Some(pos) = statement_position(&statement) { +// // first_position = Some(pos); +// // } +// // } +// // if first_position == None { +// // continue; +// // } +// // let first_position = first_position.unwrap(); + +// println!("Before reverse {:?}", block.stmts); +// block.stmts.reverse(); + +// let comment = block.stmts.pop().unwrap(); + +// // let xxx :vir_crate::polymorphic::ast::Stmt = vir_crate::polymorphic::ast::Stmt::Refute(); +// // let yyy: vir::Expr::Const() +// // let zzz: +// let expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{ +// value: vir::ast::expr::Const::Bool(false), +// position: vir::ast::common::Position::new(23, 17, 61), +// // position: vir::ast::common::Position::default(), +// }); + + + +// // Expr::Const(ConstExpr { +// // value: val.into(), +// // position: Position::default(), +// // }) +// let refute_stmt = vir::Stmt::Refute( +// vir::Refute { +// expr, +// position: vir::ast::common::Position::new(23, 17, 61), +// // position: vir::ast::common::Position::default(), +// } +// ); + +// // refute_stmt. +// block.stmts.push(refute_stmt); +// // let mut vvv = vec![refute_stmt]; +// // block.stmts.append(&mut vvv); +// block.stmts.push(comment); +// // println!("After append {:?}", block.stmts); + + +// block.stmts.reverse(); +// // println!("Dereversed {:?}", block.stmts); + +// // let vir_create::gen::polymorphic::ast::stmt::Stmt x = ; +// // vir::gen::polymorphic::ast::stmt::Stmt +// // vir::gen::polymorphic::ast::stmt +// // block.stmts.append(other) +// } +// method +// } + +// fn get_first_position(statements: &Vec<Stmt>) -> Option<Position> { +// for statement in statements { +// match statement { +// Stmt::Comment(_) => (), +// Stmt::Label(_) => (), +// Stmt::Inhale(inhale) => return Some(inhale.expr.pos()), +// Stmt::Exhale(exhale) => return Some(exhale.position), +// Stmt::Assert(assert) => return Some(assert.position), +// Stmt::Refute(refute) => return Some(refute.position), +// // Stmt::MethodCall(method_call) => { +// // for expression in method_call.arguments { +// // if expression.pos() != Position::default() { +// // return Some(expression.pos()); +// // } +// // } +// // None +// // }, +// Stmt::Assign(assign) => return Some(assign.target.pos()), +// Stmt::Fold(fold) => return Some(fold.position), +// // Stmt::Unfold(_) => todo!(), +// // Stmt::Obtain(_) => todo!(), +// // Stmt::BeginFrame(_) => todo!(), +// // Stmt::EndFrame(_) => todo!(), +// // Stmt::TransferPerm(_) => todo!(), +// // Stmt::PackageMagicWand(_) => todo!(), +// // Stmt::ApplyMagicWand(_) => todo!(), +// // Stmt::ExpireBorrows(_) => todo!(), +// // Stmt::If(_) => todo!(), +// // Stmt::Downcast(_) => todo!(), +// _ => (), +// } +// } +// None +// } + +// // fn add_unreachable_code_check(&mut self) { +// fn add_unreachable_code_check(mut method: vir::CfgMethod, encoder: &Encoder, mir_encorder: &MirEncoder) -> vir::CfgMethod { +// for block in method.basic_blocks.iter_mut() { +// if let Some(position) = get_first_position(&block.stmts) { +// // let span: Span = encoder.error_manager().position_manager().get_span(position).unwrap().primary_span().unwrap(); +// // let position = Position::new(4, 17, 11); +// let position = encoder.error_manager().duplicate_position(position); +// encoder.error_manager().set_error(position, ErrorCtxt::Panic(PanicCause::Refute)); +// // let a = self.encoder.error_manager(); +// // let b = a.position_manager(); +// // let c = b.duplicate(position); +// // let position_copy = self.encoder.error_manager().position_manager().duplicate(position); - // let position = mir_encorder.register_error(span, ErrorCtxt::Panic(PanicCause::Refute)); - let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{ - value: vir::ast::expr::Const::Bool(false), - position, - }); - - let refute_stmt = vir::Stmt::Refute( - vir::Refute { - expr: refute_expr, - position, - } - ); +// // let position = mir_encorder.register_error(span, ErrorCtxt::Panic(PanicCause::Refute)); +// let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{ +// value: vir::ast::expr::Const::Bool(false), +// position, +// }); + +// let refute_stmt = vir::Stmt::Refute( +// vir::Refute { +// expr: refute_expr, +// position, +// } +// ); - block.stmts.reverse(); - let comment = block.stmts.pop().unwrap(); - block.stmts.push(refute_stmt); - block.stmts.push(comment); - block.stmts.reverse(); - println!("After reverse {:?}\n", block.stmts); - } - } - method -} +// block.stmts.reverse(); +// let comment = block.stmts.pop().unwrap(); +// block.stmts.push(refute_stmt); +// block.stmts.push(comment); +// block.stmts.reverse(); +// println!("After reverse {:?}\n", block.stmts); +// } +// } +// method +// } impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { #[tracing::instrument(name = "ProcedureEncoder::new", level = "debug", skip_all, fields(proc_def_id = ?procedure.get_id()))] @@ -571,6 +682,28 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { )); } + if config::detect_unreachable_code() { + for bbi in self.procedure.get_reachable_nonspec_cfg_blocks() { + let cfg_block_indices = &self.cfg_blocks_map[&bbi]; + for cfg_block_index in cfg_block_indices { + let span = self.mir_encoder.get_span_of_basic_block(bbi); + // let bb_pos_expr = self.mir_encoder.register_span(span); + let bb_pos_expr = self.register_error(span, ErrorCtxt::UnreachableCode("Err 1".to_string())); + let bb_pos_stmt = self.register_error(span, ErrorCtxt::UnreachableCode("Err 2".to_string())); + // let bb_pos_stmt = self.mir_encoder.register_span(); + + let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{value: vir::ast::expr::Const::Bool(false), position: bb_pos_expr}); + let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); + + self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.reverse(); + let comment = self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.pop().unwrap(); + self.cfg_method.add_stmt(*cfg_block_index, refute_stmt); + self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.push(comment); + self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.reverse(); + } + } + } + // Set the first CFG block self.cfg_method.set_successor( start_cfg_block, @@ -620,6 +753,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { self.cfg_method = self.encoder.patch_snapshots_method(self.cfg_method) .with_span(mir_span)?; + // let method_with_fold_unfold = self.add_unreachable_code_check(method_with_fold_unfold); + // add_unreachable_code_check(&mut self.cfg_method, &self.encoder, &self.mir_encoder); + // Add fold/unfold let loan_locations = self .polonius_info() @@ -656,7 +792,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // Fix variable declarations. let method_with_fold_unfold = fix_ghost_vars(method_with_fold_unfold); - let method_with_fold_unfold = add_unreachable_code_check(method_with_fold_unfold, &self.encoder, &self.mir_encoder); + // let method_with_fold_unfold = add_unreachable_code_check(method_with_fold_unfold, &self.encoder, &self.mir_encoder); + + // let x = self.add_unreachable_code_check(method_with_fold_unfold); + // let method_with_fold_unfold = if config::detect_unreachable_code() { + // method_with_fold_unfold + // } else { + // self.add_unreachable_code_check(method_with_fold_unfold) + // }; + + // let method_with_fold_unfold = insert_refutes(method_with_fold_unfold); + // Dump final CFG if config::dump_debug_info() { prusti_common::report::log::report_with_writer( From 31bc7d9370bea3d0321df2f58927ca4c559ed0ea Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Wed, 29 Mar 2023 16:29:25 +0900 Subject: [PATCH 25/33] Update unreachable message --- .../src/encoder/errors/error_manager.rs | 6 + prusti-viper/src/encoder/procedure_encoder.rs | 229 ++---------------- 2 files changed, 29 insertions(+), 206 deletions(-) diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 5d9e6cc0a67..b5721771e1d 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -188,6 +188,8 @@ pub enum ErrorCtxt { /// The state that fold-unfold algorithm deduced as unreachable, is actually /// reachable. UnreachableFoldingState, + /// Raised when DETECT_UNREACHABLE_CODE is enabled and an code is determined as unreachable. + UnreachableCode, } /// The error manager @@ -712,6 +714,10 @@ impl<'tcx> ErrorManager<'tcx> { ) } + ("refute.failed:refutation.true", ErrorCtxt::UnreachableCode) => { + PrustiError::verification("Detected unreachable code", error_span) + } + (full_err_id, ErrorCtxt::Unexpected) => { PrustiError::internal( format!( diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 41c8569acee..4d2b844901c 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -66,7 +66,7 @@ use prusti_interface::environment::borrowck::regions::PlaceRegionsError; use crate::encoder::errors::EncodingErrorKind; use std::convert::TryInto; use prusti_interface::specs::typed::{Pledge, SpecificationItem}; -use vir_crate::polymorphic::{Float, Position, Stmt, Expr}; +use vir_crate::polymorphic::Float; use crate::utils::is_reference; use crate::encoder::mir::{ sequences::MirSequencesEncoderInterface, @@ -133,191 +133,9 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { /// Type substitutions inside this procedure. Most likely identity for the /// given proc_def_id. substs: SubstsRef<'tcx>, + reachibility_used_positions: FxHashSet<(i32, i32)>, } -// fn statement_position(statement: &Stmt) -> Option<Position> { -// match statement { -// vir::Stmt::Comment(_) => None, -// vir::Stmt::Label(_) => None, -// vir::Stmt::Inhale(inhale) => Some(inhale.expr.pos()), -// vir::Stmt::Exhale(exhale) => Some(exhale.position), -// vir::Stmt::Assert(assert) => Some(assert.position), -// vir::Stmt::Refute(refute) => Some(refute.position), -// // vir::Stmt::MethodCall(method_call) => { -// // for expression in method_call.arguments { -// // if expression.pos() != Position::default() { -// // return Some(expression.pos()); -// // } -// // } -// // None -// // }, -// vir::Stmt::Assign(assign) => Some(assign.target.pos()), -// vir::Stmt::Fold(fold) => Some(fold.position), -// // vir::Stmt::Unfold(_) => todo!(), -// // vir::Stmt::Obtain(_) => todo!(), -// // vir::Stmt::BeginFrame(_) => todo!(), -// // vir::Stmt::EndFrame(_) => todo!(), -// // vir::Stmt::TransferPerm(_) => todo!(), -// // vir::Stmt::PackageMagicWand(_) => todo!(), -// // vir::Stmt::ApplyMagicWand(_) => todo!(), -// // vir::Stmt::ExpireBorrows(_) => todo!(), -// // vir::Stmt::If(_) => todo!(), -// // vir::Stmt::Downcast(_) => todo!(), -// _ => None, -// } -// } - - -// 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)?; -// println!("refute expression: {:?}", refute_expr); - -// 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); - -// pub fn insert_refutes(mut method: vir::CfgMethod) -> vir::CfgMethod { -// let mut first_position: Option<Position> = None; -// for block in method.basic_blocks.iter_mut() { -// // for statement in block.stmts { -// // if let Some(pos) = statement_position(&statement) { -// // first_position = Some(pos); -// // } -// // } -// // if first_position == None { -// // continue; -// // } -// // let first_position = first_position.unwrap(); - -// println!("Before reverse {:?}", block.stmts); -// block.stmts.reverse(); - -// let comment = block.stmts.pop().unwrap(); - -// // let xxx :vir_crate::polymorphic::ast::Stmt = vir_crate::polymorphic::ast::Stmt::Refute(); -// // let yyy: vir::Expr::Const() -// // let zzz: -// let expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{ -// value: vir::ast::expr::Const::Bool(false), -// position: vir::ast::common::Position::new(23, 17, 61), -// // position: vir::ast::common::Position::default(), -// }); - - - -// // Expr::Const(ConstExpr { -// // value: val.into(), -// // position: Position::default(), -// // }) -// let refute_stmt = vir::Stmt::Refute( -// vir::Refute { -// expr, -// position: vir::ast::common::Position::new(23, 17, 61), -// // position: vir::ast::common::Position::default(), -// } -// ); - -// // refute_stmt. -// block.stmts.push(refute_stmt); -// // let mut vvv = vec![refute_stmt]; -// // block.stmts.append(&mut vvv); -// block.stmts.push(comment); -// // println!("After append {:?}", block.stmts); - - -// block.stmts.reverse(); -// // println!("Dereversed {:?}", block.stmts); - -// // let vir_create::gen::polymorphic::ast::stmt::Stmt x = ; -// // vir::gen::polymorphic::ast::stmt::Stmt -// // vir::gen::polymorphic::ast::stmt -// // block.stmts.append(other) -// } -// method -// } - -// fn get_first_position(statements: &Vec<Stmt>) -> Option<Position> { -// for statement in statements { -// match statement { -// Stmt::Comment(_) => (), -// Stmt::Label(_) => (), -// Stmt::Inhale(inhale) => return Some(inhale.expr.pos()), -// Stmt::Exhale(exhale) => return Some(exhale.position), -// Stmt::Assert(assert) => return Some(assert.position), -// Stmt::Refute(refute) => return Some(refute.position), -// // Stmt::MethodCall(method_call) => { -// // for expression in method_call.arguments { -// // if expression.pos() != Position::default() { -// // return Some(expression.pos()); -// // } -// // } -// // None -// // }, -// Stmt::Assign(assign) => return Some(assign.target.pos()), -// Stmt::Fold(fold) => return Some(fold.position), -// // Stmt::Unfold(_) => todo!(), -// // Stmt::Obtain(_) => todo!(), -// // Stmt::BeginFrame(_) => todo!(), -// // Stmt::EndFrame(_) => todo!(), -// // Stmt::TransferPerm(_) => todo!(), -// // Stmt::PackageMagicWand(_) => todo!(), -// // Stmt::ApplyMagicWand(_) => todo!(), -// // Stmt::ExpireBorrows(_) => todo!(), -// // Stmt::If(_) => todo!(), -// // Stmt::Downcast(_) => todo!(), -// _ => (), -// } -// } -// None -// } - -// // fn add_unreachable_code_check(&mut self) { -// fn add_unreachable_code_check(mut method: vir::CfgMethod, encoder: &Encoder, mir_encorder: &MirEncoder) -> vir::CfgMethod { -// for block in method.basic_blocks.iter_mut() { -// if let Some(position) = get_first_position(&block.stmts) { -// // let span: Span = encoder.error_manager().position_manager().get_span(position).unwrap().primary_span().unwrap(); -// // let position = Position::new(4, 17, 11); -// let position = encoder.error_manager().duplicate_position(position); -// encoder.error_manager().set_error(position, ErrorCtxt::Panic(PanicCause::Refute)); -// // let a = self.encoder.error_manager(); -// // let b = a.position_manager(); -// // let c = b.duplicate(position); -// // let position_copy = self.encoder.error_manager().position_manager().duplicate(position); - -// // let position = mir_encorder.register_error(span, ErrorCtxt::Panic(PanicCause::Refute)); -// let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{ -// value: vir::ast::expr::Const::Bool(false), -// position, -// }); - -// let refute_stmt = vir::Stmt::Refute( -// vir::Refute { -// expr: refute_expr, -// position, -// } -// ); - -// block.stmts.reverse(); -// let comment = block.stmts.pop().unwrap(); -// block.stmts.push(refute_stmt); -// block.stmts.push(comment); -// block.stmts.reverse(); -// println!("After reverse {:?}\n", block.stmts); -// } -// } -// method -// } - impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { #[tracing::instrument(name = "ProcedureEncoder::new", level = "debug", skip_all, fields(proc_def_id = ?procedure.get_id()))] pub fn new( @@ -375,6 +193,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { old_ghost_vars: FxHashMap::default(), cached_loop_invariant_block: FxHashMap::default(), substs, + reachibility_used_positions: FxHashSet::default(), }) } @@ -682,28 +501,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { )); } - if config::detect_unreachable_code() { - for bbi in self.procedure.get_reachable_nonspec_cfg_blocks() { - let cfg_block_indices = &self.cfg_blocks_map[&bbi]; - for cfg_block_index in cfg_block_indices { - let span = self.mir_encoder.get_span_of_basic_block(bbi); - // let bb_pos_expr = self.mir_encoder.register_span(span); - let bb_pos_expr = self.register_error(span, ErrorCtxt::UnreachableCode("Err 1".to_string())); - let bb_pos_stmt = self.register_error(span, ErrorCtxt::UnreachableCode("Err 2".to_string())); - // let bb_pos_stmt = self.mir_encoder.register_span(); - - let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{value: vir::ast::expr::Const::Bool(false), position: bb_pos_expr}); - let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); - - self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.reverse(); - let comment = self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.pop().unwrap(); - self.cfg_method.add_stmt(*cfg_block_index, refute_stmt); - self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.push(comment); - self.cfg_method.basic_blocks[cfg_block_index.block_index].stmts.reverse(); - } - } - } - // Set the first CFG block self.cfg_method.set_successor( start_cfg_block, @@ -1476,6 +1273,26 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { ); } + if config::detect_unreachable_code() { + let bb_data = &self.mir.basic_blocks[bbi]; + let statements: &Vec<mir::Statement<'tcx>> = &bb_data.statements; + if !statements.is_empty() { + let location = mir::Location { + block: bbi, + statement_index: 0, + }; + let span = self.mir_encoder.get_span_of_location(location); + let bb_pos_expr = self.mir_encoder.register_span(span); + if !self.reachibility_used_positions.contains(&(bb_pos_expr.line(), bb_pos_expr.column())) { + self.reachibility_used_positions.insert((bb_pos_expr.line(), bb_pos_expr.column())); + let bb_pos_stmt = self.register_error(span, ErrorCtxt::UnreachableCode); + let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{value: vir::ast::expr::Const::Bool(false), position: bb_pos_expr}); + let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); + self.cfg_method.add_stmt(curr_block, refute_stmt); + } + } + } + self.encode_execution_flag(bbi, curr_block)?; let opt_successor = self.encode_block_statements(bbi, curr_block)?; let mir_successor: MirSuccessor = if let Some(successor) = opt_successor { From bdfcd24ed980367352199c0e2bfd2daef4c3bc28 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Wed, 29 Mar 2023 16:32:51 +0900 Subject: [PATCH 26/33] delete lefrover code --- prusti-viper/src/encoder/procedure_encoder.rs | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 4d2b844901c..9b45c5b97b6 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -550,9 +550,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { self.cfg_method = self.encoder.patch_snapshots_method(self.cfg_method) .with_span(mir_span)?; - // let method_with_fold_unfold = self.add_unreachable_code_check(method_with_fold_unfold); - // add_unreachable_code_check(&mut self.cfg_method, &self.encoder, &self.mir_encoder); - // Add fold/unfold let loan_locations = self .polonius_info() @@ -589,17 +586,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // Fix variable declarations. let method_with_fold_unfold = fix_ghost_vars(method_with_fold_unfold); - // let method_with_fold_unfold = add_unreachable_code_check(method_with_fold_unfold, &self.encoder, &self.mir_encoder); - - // let x = self.add_unreachable_code_check(method_with_fold_unfold); - // let method_with_fold_unfold = if config::detect_unreachable_code() { - // method_with_fold_unfold - // } else { - // self.add_unreachable_code_check(method_with_fold_unfold) - // }; - - // let method_with_fold_unfold = insert_refutes(method_with_fold_unfold); - // Dump final CFG if config::dump_debug_info() { prusti_common::report::log::report_with_writer( From b66210eb77c52408638d2867bf98d923379e71a5 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 3 Apr 2023 15:35:41 +0900 Subject: [PATCH 27/33] make code unreachable errors just warnings --- prusti-viper/src/encoder/errors/error_manager.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index b5721771e1d..1966a362229 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -715,7 +715,7 @@ impl<'tcx> ErrorManager<'tcx> { } ("refute.failed:refutation.true", ErrorCtxt::UnreachableCode) => { - PrustiError::verification("Detected unreachable code", error_span) + PrustiError::warning("Detected unreachable code", error_span) } (full_err_id, ErrorCtxt::Unexpected) => { From 7592282931e5904ec8b7ccfa53c4fc242ad1dab7 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Mon, 3 Apr 2023 18:04:26 +0900 Subject: [PATCH 28/33] change detection of assert/panic terminators --- prusti-viper/src/encoder/procedure_encoder.rs | 28 +++++++++++++++++-- prusti/src/verifier.rs | 3 +- 2 files changed, 28 insertions(+), 3 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 9b45c5b97b6..93c62471b81 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1262,7 +1262,31 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { if config::detect_unreachable_code() { let bb_data = &self.mir.basic_blocks[bbi]; let statements: &Vec<mir::Statement<'tcx>> = &bb_data.statements; - if !statements.is_empty() { + + let panic_free = match &bb_data.terminator().kind { + TerminatorKind::Unreachable => false, + TerminatorKind::Assert { .. } => false, + TerminatorKind::Call { + func: + mir::Operand::Constant(box mir::Constant { + literal, + .. + }), + .. + } => { + if let ty::TyKind::FnDef(called_def_id, _call_substs) = literal.ty().kind() { + let full_func_proc_name: &str = + &self.encoder.env().name.get_absolute_item_name(*called_def_id); + + !matches!(full_func_proc_name, "std::rt::begin_panic" | "core::panicking::panic" | "core::panicking::panic_fmt") + } else { + true + } + } + _ => true, + }; + + if !statements.is_empty() && panic_free { let location = mir::Location { block: bbi, statement_index: 0, @@ -1272,7 +1296,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { if !self.reachibility_used_positions.contains(&(bb_pos_expr.line(), bb_pos_expr.column())) { self.reachibility_used_positions.insert((bb_pos_expr.line(), bb_pos_expr.column())); let bb_pos_stmt = self.register_error(span, ErrorCtxt::UnreachableCode); - let refute_expr = vir::ast::Expr::Const(vir::ast::expr::ConstExpr{value: vir::ast::expr::Const::Bool(false), position: bb_pos_expr}); + let refute_expr = vir::ast::Expr::Const(vir_crate::polymorphic::ConstExpr{value: vir_crate::polymorphic::Const::Bool(false), position: bb_pos_expr}); let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); self.cfg_method.add_stmt(curr_block, refute_stmt); } diff --git a/prusti/src/verifier.rs b/prusti/src/verifier.rs index 74775f0d628..0e19ff5f344 100644 --- a/prusti/src/verifier.rs +++ b/prusti/src/verifier.rs @@ -77,7 +77,8 @@ pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) { env.diagnostic.has_errors() || config::internal_errors_as_warnings() || (config::skip_unsupported_features() - && config::allow_unreachable_unsupported_code()) + && config::allow_unreachable_unsupported_code() + || config::detect_unreachable_code()) ); } }; From ca94f92a15b10304fb15dd794f5d1cdf4dbda096 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Tue, 4 Apr 2023 00:41:29 +0900 Subject: [PATCH 29/33] remove unecessary case in the error manager --- prusti-viper/src/encoder/errors/error_manager.rs | 7 ------- 1 file changed, 7 deletions(-) diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 1966a362229..6fb46a2082b 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -707,13 +707,6 @@ impl<'tcx> ErrorManager<'tcx> { ) } - ("assert.failed:assertion.false", ErrorCtxt::Panic(PanicCause::Refute)) => { - PrustiError::verification( - "the refuted expression holds in all cases or could not be reached", - error_span, - ) - } - ("refute.failed:refutation.true", ErrorCtxt::UnreachableCode) => { PrustiError::warning("Detected unreachable code", error_span) } From 27ecb2ed860b9dca98f04ce7de648f64236b7b67 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Wed, 5 Apr 2023 01:33:16 +0900 Subject: [PATCH 30/33] make line/column numbers unique for code reachability refute statements --- prusti-viper/src/encoder/procedure_encoder.rs | 27 ++++++++++++------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 93c62471b81..89d11201743 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -31,6 +31,7 @@ use prusti_common::{ }; use vir_crate::{ polymorphic::{ + Position, self as vir, compute_identifier, borrows::Borrow, @@ -133,7 +134,9 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { /// Type substitutions inside this procedure. Most likely identity for the /// given proc_def_id. substs: SubstsRef<'tcx>, - reachibility_used_positions: FxHashSet<(i32, i32)>, + /// Used in unreachable code detecetion to get positions without + /// colliding line/column numbers + uniquie_line_column_number: i32, } impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { @@ -193,10 +196,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { old_ghost_vars: FxHashMap::default(), cached_loop_invariant_block: FxHashMap::default(), substs, - reachibility_used_positions: FxHashSet::default(), + uniquie_line_column_number: 0, }) } + fn generate_unique_line_column_number(&mut self) -> i32 { + self.uniquie_line_column_number -= 1; + self.uniquie_line_column_number + } + #[tracing::instrument(level = "trace", skip_all)] fn encode_specification_blocks(&mut self) -> SpannedEncodingResult<()> { // Collect the entry points into the specification blocks. @@ -1292,14 +1300,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { statement_index: 0, }; let span = self.mir_encoder.get_span_of_location(location); - let bb_pos_expr = self.mir_encoder.register_span(span); - if !self.reachibility_used_positions.contains(&(bb_pos_expr.line(), bb_pos_expr.column())) { - self.reachibility_used_positions.insert((bb_pos_expr.line(), bb_pos_expr.column())); - let bb_pos_stmt = self.register_error(span, ErrorCtxt::UnreachableCode); - let refute_expr = vir::ast::Expr::Const(vir_crate::polymorphic::ConstExpr{value: vir_crate::polymorphic::Const::Bool(false), position: bb_pos_expr}); - let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); - self.cfg_method.add_stmt(curr_block, refute_stmt); - } + let bb_pos_expr_id = self.mir_encoder.register_span(span).id(); + let bb_pos_expr = Position::new(self.generate_unique_line_column_number(), self.generate_unique_line_column_number(), bb_pos_expr_id); + let bb_pos_stmt_id = self.register_error(span, ErrorCtxt::UnreachableCode).id(); + let bb_pos_stmt = Position::new(self.generate_unique_line_column_number(), self.generate_unique_line_column_number(), bb_pos_stmt_id); + let refute_expr = vir::ast::Expr::Const(vir_crate::polymorphic::ConstExpr{value: vir_crate::polymorphic::Const::Bool(false), position: bb_pos_expr}); + let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); + self.cfg_method.add_stmt(curr_block, refute_stmt); } } From b9cb939e9c91420d5f66a68795454f13d8884174 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Wed, 5 Apr 2023 01:46:48 +0900 Subject: [PATCH 31/33] remove unecessary member variable, use just position id --- prusti-viper/src/encoder/procedure_encoder.rs | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 89d11201743..dc07bd00e63 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -134,9 +134,6 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { /// Type substitutions inside this procedure. Most likely identity for the /// given proc_def_id. substs: SubstsRef<'tcx>, - /// Used in unreachable code detecetion to get positions without - /// colliding line/column numbers - uniquie_line_column_number: i32, } impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { @@ -196,15 +193,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { old_ghost_vars: FxHashMap::default(), cached_loop_invariant_block: FxHashMap::default(), substs, - uniquie_line_column_number: 0, }) } - fn generate_unique_line_column_number(&mut self) -> i32 { - self.uniquie_line_column_number -= 1; - self.uniquie_line_column_number - } - #[tracing::instrument(level = "trace", skip_all)] fn encode_specification_blocks(&mut self) -> SpannedEncodingResult<()> { // Collect the entry points into the specification blocks. @@ -1301,9 +1292,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { }; let span = self.mir_encoder.get_span_of_location(location); let bb_pos_expr_id = self.mir_encoder.register_span(span).id(); - let bb_pos_expr = Position::new(self.generate_unique_line_column_number(), self.generate_unique_line_column_number(), bb_pos_expr_id); + let bb_pos_expr = Position::new(-(bb_pos_expr_id as i32), 0, bb_pos_expr_id); let bb_pos_stmt_id = self.register_error(span, ErrorCtxt::UnreachableCode).id(); - let bb_pos_stmt = Position::new(self.generate_unique_line_column_number(), self.generate_unique_line_column_number(), bb_pos_stmt_id); + let bb_pos_stmt = Position::new(-(bb_pos_stmt_id as i32), 0, bb_pos_stmt_id); let refute_expr = vir::ast::Expr::Const(vir_crate::polymorphic::ConstExpr{value: vir_crate::polymorphic::Const::Bool(false), position: bb_pos_expr}); let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); self.cfg_method.add_stmt(curr_block, refute_stmt); From 5cd88f5a9bd20f01dc8f1491bf41f0ce80d70aaf Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Wed, 5 Apr 2023 19:08:21 +0900 Subject: [PATCH 32/33] make position manager return positions with unique line/column --- prusti-viper/src/encoder/encoder.rs | 6 +-- .../src/encoder/errors/error_manager.rs | 17 ++------ .../src/encoder/errors/position_manager.rs | 42 ++++--------------- prusti-viper/src/encoder/procedure_encoder.rs | 1 - 4 files changed, 14 insertions(+), 52 deletions(-) diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index 08e5966d17f..28f239dfe06 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -67,7 +67,7 @@ use super::high::to_typed::types::HighToTypedTypeEncoderState; pub struct Encoder<'v, 'tcx: 'v> { env: &'v Environment<'tcx>, - error_manager: RefCell<ErrorManager<'tcx>>, + error_manager: RefCell<ErrorManager>, /// A map containing all functions: identifier → function definition. functions: RefCell<FxHashMap<vir::FunctionIdentifier, Rc<vir::Function>>>, builtin_domains: RefCell<FxHashMap<BuiltinDomainKind, vir::Domain>>, @@ -151,7 +151,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { Encoder { env, - error_manager: RefCell::new(ErrorManager::new(env.query.codemap())), + error_manager: RefCell::new(ErrorManager::default()), functions: RefCell::new(FxHashMap::default()), builtin_domains: RefCell::new(FxHashMap::default()), builtin_domains_in_progress: RefCell::new(FxHashSet::default()), @@ -228,7 +228,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { self.env } - pub fn error_manager(&self) -> RefMut<ErrorManager<'tcx>> { + pub fn error_manager(&self) -> RefMut<ErrorManager> { self.error_manager.borrow_mut() } diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 6fb46a2082b..7cbc06a1f66 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -8,7 +8,6 @@ use std::fmt::Debug; use vir_crate::polymorphic::Position; use rustc_hash::FxHashMap; -use prusti_rustc_interface::span::source_map::SourceMap; use prusti_rustc_interface::errors::MultiSpan; use viper::VerificationError; use prusti_interface::PrustiError; @@ -193,22 +192,14 @@ pub enum ErrorCtxt { } /// The error manager -#[derive(Clone)] -pub struct ErrorManager<'tcx> { - position_manager: PositionManager<'tcx>, +#[derive(Clone, Default)] +pub struct ErrorManager { + position_manager: PositionManager, error_contexts: FxHashMap<u64, ErrorCtxt>, inner_positions: FxHashMap<u64, Position>, } -impl<'tcx> ErrorManager<'tcx> { - pub fn new(codemap: &'tcx SourceMap) -> Self { - ErrorManager { - position_manager: PositionManager::new(codemap), - error_contexts: FxHashMap::default(), - inner_positions: FxHashMap::default(), - } - } - +impl ErrorManager { pub fn position_manager(&self) -> &PositionManager { &self.position_manager } diff --git a/prusti-viper/src/encoder/errors/position_manager.rs b/prusti-viper/src/encoder/errors/position_manager.rs index b1575ec0e0f..2e58b677cb9 100644 --- a/prusti-viper/src/encoder/errors/position_manager.rs +++ b/prusti-viper/src/encoder/errors/position_manager.rs @@ -8,17 +8,14 @@ use std::fmt::Debug; use vir_crate::polymorphic::Position; use rustc_hash::FxHashMap; -use prusti_rustc_interface::span::source_map::SourceMap; use prusti_rustc_interface::errors::MultiSpan; -use log::debug; use prusti_interface::data::ProcedureDefId; /// Mapping from VIR positions to the source code that generated them. /// One VIR position can be involved in multiple errors. If an error needs to refer to a special /// span, that should be done by adding the span to `ErrorCtxt`, not by registering a new span. #[derive(Clone)] -pub struct PositionManager<'tcx> { - codemap: &'tcx SourceMap, +pub struct PositionManager { next_pos_id: u64, /// The def_id of the procedure that generated the given VIR position. pub(crate) def_id: FxHashMap<u64, ProcedureDefId>, @@ -26,51 +23,26 @@ pub struct PositionManager<'tcx> { pub(crate) source_span: FxHashMap<u64, MultiSpan>, } -impl<'tcx> PositionManager<'tcx> -{ - pub fn new(codemap: &'tcx SourceMap) -> Self { +impl Default for PositionManager { + fn default() -> Self { PositionManager { - codemap, next_pos_id: 1, def_id: FxHashMap::default(), source_span: FxHashMap::default(), } } +} +impl PositionManager +{ #[tracing::instrument(level = "trace", skip(self), ret)] pub fn register_span<T: Into<MultiSpan> + Debug>(&mut self, def_id: ProcedureDefId, span: T) -> Position { let span = span.into(); let pos_id = self.next_pos_id; self.next_pos_id += 1; - - let pos = if let Some(primary_span) = span.primary_span() { - let lines_info_res = self - .codemap - .span_to_lines(primary_span.source_callsite()); - match lines_info_res { - Ok(lines_info) => { - if let Some(first_line_info) = lines_info.lines.get(0) { - let line = first_line_info.line_index as i32 + 1; - let column = first_line_info.start_col.0 as i32 + 1; - Position::new(line, column, pos_id) - } else { - debug!("Primary span of position id {} has no lines", pos_id); - Position::new(0, 0, pos_id) - } - } - Err(e) => { - debug!("Error converting primary span of position id {} to lines: {:?}", pos_id, e); - Position::new(0, 0, pos_id) - } - } - } else { - debug!("Position id {} has no primary span", pos_id); - Position::new(0, 0, pos_id) - }; - self.def_id.insert(pos_id, def_id); self.source_span.insert(pos_id, span); - pos + Position::new(pos_id as i32, 0, pos_id) } pub fn duplicate(&mut self, pos: Position) -> Position { diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index f3cf020bba8..c21aed06b19 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -31,7 +31,6 @@ use prusti_common::{ }; use vir_crate::{ polymorphic::{ - Position, self as vir, compute_identifier, borrows::Borrow, From 8433a89dc972ec8fa2cd52132c6828a7d6899ea9 Mon Sep 17 00:00:00 2001 From: Simon Hrabec <simon.hrabec@gmail.com> Date: Thu, 6 Apr 2023 15:47:54 +0900 Subject: [PATCH 33/33] rely on the change in position manager for unique line/column numbers in positions --- prusti-viper/src/encoder/procedure_encoder.rs | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index c21aed06b19..68a146ddf84 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1290,12 +1290,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { statement_index: 0, }; let span = self.mir_encoder.get_span_of_location(location); - let bb_pos_expr_id = self.mir_encoder.register_span(span).id(); - let bb_pos_expr = Position::new(-(bb_pos_expr_id as i32), 0, bb_pos_expr_id); - let bb_pos_stmt_id = self.register_error(span, ErrorCtxt::UnreachableCode).id(); - let bb_pos_stmt = Position::new(-(bb_pos_stmt_id as i32), 0, bb_pos_stmt_id); - let refute_expr = vir::ast::Expr::Const(vir_crate::polymorphic::ConstExpr{value: vir_crate::polymorphic::Const::Bool(false), position: bb_pos_expr}); - let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: bb_pos_stmt}); + let expr_position = self.mir_encoder.register_span(span); + let stmt_position = self.register_error(span, ErrorCtxt::UnreachableCode); + let refute_expr = vir::ast::Expr::Const(vir_crate::polymorphic::ConstExpr{value: vir_crate::polymorphic::Const::Bool(false), position: expr_position}); + let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: stmt_position}); self.cfg_method.add_stmt(curr_block, refute_stmt); } }