run bv in inter-procedure mode

third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs

@@ -17,13 +17,14 @@ use itertools::Either;
 use move_binary_format::file_format::CodeOffset;
 use move_model::{
     ast::{Exp, ExpData, Operation as ASTOperation, TempIndex},
-    model::{FieldId, FunId, GlobalEnv, ModuleId, Parameter, StructId},
+    model::{FieldId, FunId, FunctionEnv, GlobalEnv, ModuleId, Parameter, StructId},
     ty::{PrimitiveType, Type},
 };
 use move_stackless_bytecode::{
     dataflow_analysis::{DataflowAnalysis, TransferFunctions},
     dataflow_domains::{AbstractDomain, JoinResult},
     function_target::FunctionTarget,
+    function_target::FunctionData,
     function_target_pipeline::{
         FunctionTargetPipeline, FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant,
     },
@@ -46,13 +47,13 @@ impl NumberOperationProcessor {
 
     /// Create initial number operation state for expressions
     pub fn create_initial_exp_oper_state(&self, env: &GlobalEnv) {
-        let mut default_exp = BTreeMap::new();
+        let mut global_state = env.get_cloned_extension::<GlobalNumberOperationState>();
         let exp_info_map = env.get_nodes();
         for id in exp_info_map {
-            default_exp.insert(id, Bottom);
+            if !global_state.exp_operation_map.contains_key(&id) {
+                global_state.exp_operation_map.insert(id, Bottom);
+            }
         }
-        let mut global_state = env.get_cloned_extension::<GlobalNumberOperationState>();
-        global_state.exp_operation_map = default_exp;
         env.set_extension(global_state);
     }
 
@@ -96,7 +97,7 @@ impl NumberOperationProcessor {
         if !target.func_env.is_native_or_intrinsic() {
             let cfg = StacklessControlFlowGraph::one_block(target.get_bytecode());
             let analyzer = NumberOperationAnalysis {
-                func_target: target,
+                func_target: target.clone(),
                 ban_int_2_bv_conversion: ProverOptions::get(env).ban_int_2_bv,
             };
             analyzer.analyze_function(
@@ -110,7 +111,7 @@ impl NumberOperationProcessor {
 
 impl FunctionTargetProcessor for NumberOperationProcessor {
     fn is_single_run(&self) -> bool {
-        true
+        false
     }
 
     fn run(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
@@ -120,6 +121,18 @@ impl FunctionTargetProcessor for NumberOperationProcessor {
     fn name(&self) -> String {
         "number_operation_analysis".to_string()
     }
+
+    fn process(
+        &self,
+        _targets: &mut FunctionTargetsHolder,
+        _fun_env: &FunctionEnv,
+        _data: FunctionData,
+        _scc_opt: Option<&[FunctionEnv]>,
+    ) -> FunctionData {
+        self.analyze(_fun_env.module_env.env, _targets);
+        _data
+    }
+
 }
 
 struct NumberOperationAnalysis<'a> {

third_party/move/move-prover/tests/sources/functional/bitwise_operators.move

@@ -2,6 +2,7 @@
 address 0x123 {
 
   module M {
+    // use std::fixed_point32;
 
     public fun foo(): u64 {
       let a = A {
@@ -77,6 +78,17 @@ address 0x123 {
       if (e == (0 as u64)) { int2bv((1 as u64)) } else { n & spec_bv_and(n, e - int2bv((1 as u64))) }
     }
 
+    fun test_2(x1: u64, x2: u64): u64 {
+       x1 + x2
+    }
+
+    fun test_1(x: u64): u64 {
+       let y = x ^ (x - 2);
+       let fix = fixed_point32::create_from_rational(2, 3);
+       // this does not work for now
+       // fixed_point32::divide_u64(2, fix) + y
+       test_2(x1, x2) + y
+    }
   }
 
 }

third_party/move/move-prover/tests/testsuite.rs

@@ -244,6 +244,8 @@ fn get_flags_and_baseline(
     // Add flags specified via environment variable.
     flags.extend(shell_words::split(&read_env_var(ENV_FLAGS))?);
 
+    flags.push("--keep".to_string());
+
     // Create a temporary file for output. We inject the modifier to potentially prevent
     // any races between similar named files in different directories, as it appears TempPath
     // isn't working always.