Merge branch 'main' into cut-tables

Author: andrii-a8c

Cargo.lock

@@ -81,14 +81,14 @@ datatest-stable = "0.3.2"
 sha2 = "0.10.9"
 dir-test = "0.4.1"
 
-move-stdlib = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-docgen = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-package = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-compiler = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-ir-types = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-core-types = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-symbol-pool = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-disassembler = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-binary-format = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-bytecode-source-map = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
-move-command-line-common = { git = "https://github.com/asymptotic-code/sui", branch = "next" }
+move-stdlib = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-docgen = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-package = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-compiler = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-ir-types = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-core-types = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-symbol-pool = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-disassembler = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-binary-format = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-bytecode-source-map = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }
+move-command-line-common = { git = "https://github.com/asymptotic-code/sui", branch = "spec_only_loop_inv" }

Cargo.toml

@@ -21,7 +21,7 @@ const DEFAULT_BOOGIE_FLAGS: &[&str] = &[
     "-printModel:1",
     "-enhancedErrorMessages:1",
     "-useArrayAxioms",
-    "-proverOpt:O:smt.QI.EAGER_THRESHOLD=100",
+    "-proverOpt:O:smt.QI.EAGER_THRESHOLD=10",
     "-proverOpt:O:smt.QI.LAZY_THRESHOLD=100",
     "-proverOpt:O:model_validate=true",
     "-vcsCores:4",
@@ -118,6 +118,23 @@ impl ProverHandler {
         Ok(())
     }
 
+    fn get_option_key(option: &str) -> &str {
+        if let Some(eq_pos) = option.find('=') {
+            &option[..eq_pos]
+        } else if let Some(colon_pos) = option.rfind(':') {
+            let after_colon = &option[colon_pos + 1..];
+            if after_colon.chars().next().map_or(false, |c| {
+                c.is_ascii_digit() || after_colon.starts_with('/') || after_colon.starts_with('.')
+            }) {
+                &option[..colon_pos]
+            } else {
+                option
+            }
+        } else {
+            option
+        }
+    }
+
     fn get_boogie_command(
         &self,
         boogie_file_name: &str,
@@ -131,7 +148,11 @@ impl ProverHandler {
         result.extend(DEFAULT_BOOGIE_FLAGS.iter().map(|s| s.to_string()));
 
         if let Some(options) = individual_options {
-            result.extend(options.split_whitespace().map(|s| s.to_string()));
+            for option in options.split_whitespace().map(|s| format!("-{}", s)) {
+                let key = Self::get_option_key(&option);
+                result.retain(|existing: &String| Self::get_option_key(existing) != key);
+                result.push(option);
+            }
         }
 
         result.push(format!("-proverOpt:PROVER_PATH={z3_exe}"));

crates/lambda-boogie-handler/handler.rs

@@ -340,6 +340,7 @@ impl<'env> BoogieTranslator<'env> {
                 if self.options.func_abort_check_only
                     && self.targets.is_spec(&fun_env.get_qualified_id())
                 {
+                    self.translate_function_style(fun_env, FunctionTranslationStyle::Aborts);
                     self.translate_function_style(fun_env, FunctionTranslationStyle::Opaque);
                     continue;
                 }

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs

@@ -216,7 +216,7 @@ impl Default for BoogieOptions {
             proc_cores: 4,
             vc_timeout: 40,
             keep_artifacts: true,
-            eager_threshold: 100,
+            eager_threshold: 10,
             lazy_threshold: 100,
             stable_test_output: false,
             num_instances: 1,
@@ -250,6 +250,26 @@ impl BoogieOptions {
         }
     }
 
+    /// Extracts the key part of a boogie option (everything except the value).
+    /// For "-proverOpt:O:smt.QI.EAGER_THRESHOLD=100", returns "-proverOpt:O:smt.QI.EAGER_THRESHOLD"
+    /// For "-vcsCores:4", returns "-vcsCores"
+    fn get_option_key(option: &str) -> &str {
+        if let Some(eq_pos) = option.find('=') {
+            &option[..eq_pos]
+        } else if let Some(colon_pos) = option.rfind(':') {
+            let after_colon = &option[colon_pos + 1..];
+            if after_colon.chars().next().map_or(false, |c| {
+                c.is_ascii_digit() || after_colon.starts_with('/') || after_colon.starts_with('.')
+            }) {
+                &option[..colon_pos]
+            } else {
+                option
+            }
+        } else {
+            option
+        }
+    }
+
     /// Returns command line to call boogie.
     pub fn get_boogie_command(
         &self,
@@ -272,6 +292,8 @@ impl BoogieOptions {
         let mut seen_options = HashSet::new();
         let mut add = |sl: &[&str]| {
             for s in sl {
+                let key = Self::get_option_key(s);
+                seen_options.retain(|existing: &String| Self::get_option_key(existing) != key);
                 seen_options.insert(s.to_string());
             }
         };