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, &parameter_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 = &parameter_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, &parameter_name)} else {"".to_string()},
-        "    let result = self.env.set_field(".to_string(),
+        generate_parameter_type_check(type_signature, &parameter_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);
             }
         }