Add table/dynamic_field in pure functions. (#441)

Author: andreistefanescu

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

@@ -2750,7 +2750,13 @@ impl<'env> FunctionTranslator<'env> {
                             let native_fn =
                                 self.parent.env.should_be_used_as_func(&mid.qualified(*fid));
                             // Handle function calls for functions that can be emitted as Boogie functions
-                            if self.can_callee_be_function(mid, fid) || native_fn {
+                            if self.can_callee_be_function(mid, fid)
+                                || PureFunctionAnalysisProcessor::native_pure_variants(
+                                    self.parent.env,
+                                )
+                                .contains(&mid.qualified(*fid))
+                                || native_fn
+                            {
                                 let inst = &self.inst_slice(inst);
                                 let fun_name = boogie_function_name(
                                     &callee_env,
@@ -2763,14 +2769,6 @@ impl<'env> FunctionTranslator<'env> {
                                 );
                                 let args = srcs.iter().map(|s| fmt_temp(*s)).join(", ");
                                 format!("{}({})", fun_name, args)
-                            } else if let Some(fun_name) =
-                                PureFunctionAnalysisProcessor::special_pure_functions_map(
-                                    self.parent.env,
-                                )
-                                .get(&mid.qualified(*fid))
-                            {
-                                let args = srcs.iter().map(|s| fmt_temp(*s)).join(", ");
-                                format!("{}({})", fun_name, args)
                             } else {
                                 unreachable!(
                                     "Cannot emit function call to {:?} as pure function",

crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl

@@ -254,7 +254,7 @@ procedure {:inline 1} $1_vector_borrow{{S}}(v: Vec ({{T}}), i: int) returns (dst
     dst := ReadVec(v, i);
 }
 
-function {:inline} $1_vector_$borrow{{S}}(v: Vec ({{T}}), i: int): {{T}} {
+function {:inline} $1_vector_borrow{{S}}$pure(v: Vec ({{T}}), i: int): {{T}} {
     ReadVec(v, i)
 }
 
@@ -271,10 +271,6 @@ returns (dst: $Mutation ({{T}}), m': $Mutation (Vec ({{T}})))
     m' := m;
 }
 
-function {:inline} $1_vector_$borrow_mut{{S}}(v: Vec ({{T}}), i: int): {{T}} {
-    ReadVec(v, i)
-}
-
 procedure {:inline 1} $1_vector_destroy_empty{{S}}(v: Vec ({{T}})) {
     if (!IsEmptyVec(v)) {
       call $ExecFailureAbort();
@@ -774,6 +770,9 @@ procedure {:inline 2} {{impl.fun_borrow}}{{S}}(t: {{Type}}{{S}}, k: {{K}}) retur
         v := GetTable(t->$contents, {{ENC}}(k));
     }
 }
+function {:inline} {{impl.fun_borrow}}{{S}}$pure(t: {{Type}}{{S}}, k: {{K}}): {{V}} {
+    GetTable(t->$contents, {{ENC}}(k))
+}
 {%- endif %}
 
 {%- if impl.fun_borrow_mut != "" %}
@@ -880,6 +879,9 @@ procedure {:inline 2} {{impl.fun_borrow}}{{DF_S}}(t: {{Type}}, k: {{K}}) returns
         v := GetTable(t->$dynamic_fields{{S}}, {{ENC}}(k));
     }
 }
+function {:inline} {{impl.fun_borrow}}{{DF_S}}$pure(t: {{Type}}, k: {{K}}): {{V}} {
+    GetTable(t->$dynamic_fields{{S}}, {{ENC}}(k))
+}
 {%- endif %}
 
 {%- if impl.fun_borrow_mut != "" %}

crates/move-stackless-bytecode/src/pure_function_analysis.rs

@@ -1,6 +1,6 @@
 use codespan_reporting::diagnostic::Severity;
 use move_model::model::{FunId, FunctionEnv, GlobalEnv, ModuleId, QualifiedId};
-use std::collections::BTreeMap;
+use std::collections::BTreeSet;
 
 use crate::{
     deterministic_analysis,
@@ -16,10 +16,14 @@ impl PureFunctionAnalysisProcessor {
         Box::new(Self())
     }
 
-    pub fn special_pure_functions_map(env: &GlobalEnv) -> BTreeMap<QualifiedId<FunId>, String> {
-        let mut special_funcs = BTreeMap::new();
-        special_funcs.insert(env.std_vector_borrow_qid().unwrap(), "ReadVec".to_string());
-        special_funcs
+    pub fn native_pure_variants(env: &GlobalEnv) -> BTreeSet<QualifiedId<FunId>> {
+        BTreeSet::from([
+            env.std_vector_borrow_qid().unwrap(),
+            env.table_borrow_qid().unwrap(),
+            env.object_table_borrow_qid().unwrap(),
+            env.dynamic_field_borrow_qid().unwrap(),
+            env.dynamic_object_field_borrow_qid().unwrap(),
+        ])
     }
 
     fn check_function(
@@ -32,7 +36,7 @@ impl PureFunctionAnalysisProcessor {
         let func_env = env.get_function(qid);
         if targets.is_pure_fun(&func_env.get_qualified_id())
             || env.should_be_used_as_func(&qid)
-            || Self::special_pure_functions_map(env).contains_key(&qid)
+            || Self::native_pure_variants(env).contains(&qid)
         {
             return None;
         } else {

crates/sui-prover/tests/snapshots/multiple_specs/include_external.fail.move.snap

@@ -3,5 +3,5 @@ source: crates/sui-prover/tests/integration.rs
 expression: output
 ---
 [internal] boogie exited with compilation errors:
-output/multiple_specs/include_external.fail/bar_specs_double_foo_imported_module::bar_spec_Assume.bpl(4368,4): Error: call to undeclared procedure: $42_fb_foo
+output/multiple_specs/include_external.fail/bar_specs_double_foo_imported_module::bar_spec_Assume.bpl(4364,4): Error: call to undeclared procedure: $42_fb_foo
 1 name resolution errors detected in output/multiple_specs/include_external.fail/bar_specs_double_foo_imported_module::bar_spec_Assume.bpl