[move-prover] fix crash in read/write set analysis

The transfer functions for read_ref used an outdated version of the assignment logic that predated support for addresses flowing into/out of structs. Using the modern version and deleting the old one. Added E2E test that exercises the crash + passes now.

Closes: aptos-labs#9320

language/move-prover/bytecode/src/access_path_trie.rs

@@ -367,7 +367,12 @@ impl<T: FootprintDomain> AccessPathTrie<T> {
         node: TrieNode<T>,
         fun_env: &FunctionEnv,
     ) {
-        self.0.insert(Root::from_index(local_index, fun_env), node);
+        self.bind_node(Root::from_index(local_index, fun_env), node);
+    }
+
+    /// Bind `node` to `lhs` in the trie, overwriting the old value of `lhs`
+    pub fn bind_node(&mut self, lhs: Root, node: TrieNode<T>) {
+        self.0.insert(lhs, node);
     }
 
     /// Remove the value bound to the local variable `local_index`
@@ -380,7 +385,8 @@ impl<T: FootprintDomain> AccessPathTrie<T> {
         self.bind_root(Root::ret(return_index), data)
     }
 
-    fn bind_root(&mut self, root: Root, data: T) {
+    /// Bind `root` to `data`
+    pub fn bind_root(&mut self, root: Root, data: T) {
         self.0.insert(root, TrieNode::new(data));
     }
 

language/move-prover/bytecode/src/read_write_set_analysis.rs

@@ -190,32 +190,21 @@ impl ReadWriteSetState {
         self.accesses.join(&new_callee_accesses);
     }
 
-    /// Copy the contents of `rhs_index` into `lhs_index`. Fails if `rhs_index` is not bound
-    pub fn copy_local(
-        &mut self,
-        lhs_index: TempIndex,
-        rhs_index: TempIndex,
-        fun_env: &FunctionEnv,
-    ) {
-        let rhs_value = self
-            .locals
-            .get_local(rhs_index, fun_env)
-            .unwrap_or_else(|| panic!("Unbound local {:?}", rhs_index))
-            .clone();
-        self.locals.bind_local(lhs_index, rhs_value, fun_env)
-    }
-
     pub fn assign_local(
         &mut self,
         lhs_index: TempIndex,
         rhs_index: TempIndex,
         func_env: &FunctionEnv,
     ) {
+        self.assign_root(Root::from_index(lhs_index, func_env), rhs_index, func_env)
+    }
+
+    pub fn assign_root(&mut self, lhs: Root, rhs_index: TempIndex, func_env: &FunctionEnv) {
         if let Some(rhs_data) = self.locals.get_local(rhs_index, func_env).cloned() {
-            self.locals.bind_local(lhs_index, rhs_data, func_env);
+            self.locals.bind_root(lhs, rhs_data);
             self.record_access(rhs_index, Access::Read, func_env)
         } else if let Some(rhs_node) = self.locals.get_local_node(rhs_index, func_env).cloned() {
-            self.locals.bind_local_node(lhs_index, rhs_node, func_env);
+            self.locals.bind_node(lhs, rhs_node);
         }
     }
 
@@ -274,7 +263,7 @@ impl ReadWriteSetState {
         for p in self
             .locals
             .get_local(local_idx, fun_env)
-            .expect("Unbound local")
+            .unwrap_or_else(|| panic!("Unbound local {:?}", local_idx))
             .iter()
         {
             if let Addr::Footprint(ap) = p {
@@ -295,7 +284,7 @@ impl ReadWriteSetState {
         let borrowed = self
             .locals
             .get_local(base, fun_env)
-            .expect("Unbound local")
+            .unwrap_or_else(|| panic!("Unbound local {:?}", base))
             .clone();
         let extended_aps = borrowed.add_offset(offset);
         for ap in extended_aps.footprint_paths() {
@@ -440,7 +429,6 @@ impl<'a> TransferFunctions for ReadWriteSetAnalysis<'a> {
         use Operation::*;
 
         let func_env = &self.func_env;
-
         match instr {
             Call(_, rets, oper, args, _abort_action) => match oper {
                 BorrowField(_mid, _sid, _types, fld) => {
@@ -450,9 +438,8 @@ impl<'a> TransferFunctions for ReadWriteSetAnalysis<'a> {
                 }
                 ReadRef => {
                     if state.locals.local_exists(args[0], func_env) {
-                        state.record_access(args[0], Access::Read, func_env);
                         // rets[0] = args[0]
-                        state.copy_local(rets[0], args[0], func_env)
+                        state.assign_local(rets[0], args[0], func_env)
                     }
                 }
                 WriteRef => {
@@ -505,7 +492,6 @@ impl<'a> TransferFunctions for ReadWriteSetAnalysis<'a> {
                     let fun_id = mid.qualified(*fid);
                     let global_env = self.cache.global_env();
                     let callee_fun_env = global_env.get_function(fun_id);
-                    // TODO: fix crash here
                     if let Some(callee_summary) = self
                         .cache
                         .get::<ReadWriteSetState>(fun_id, &FunctionVariant::Baseline)
@@ -606,22 +592,8 @@ impl<'a> TransferFunctions for ReadWriteSetAnalysis<'a> {
             }
             Assign(_attr_id, lhs, rhs, _assign_kind) => state.assign_local(*lhs, *rhs, func_env),
             Ret(_attr_id, rets) => {
-                let ret_vals: Vec<Option<AbsAddr>> = rets
-                    .iter()
-                    .map(|ret| state.locals.get_local(*ret, func_env).cloned())
-                    .collect();
-                for (ret_index, ret_val_opt) in ret_vals.iter().enumerate() {
-                    if let Some(ret_val) = ret_val_opt {
-                        /*assert!(
-                            !ret_val.is_empty(),
-                            "empty return value bound to ret index {:?}",
-                            ret_index
-                        );*/
-                        // TODO: replace with assertion above
-                        if !ret_val.is_empty() {
-                            state.locals.bind_return(ret_index, ret_val.clone())
-                        }
-                    }
+                for (ret_index, ret_val) in rets.iter().enumerate() {
+                    state.assign_root(Root::Return(ret_index), *ret_val, func_env)
                 }
             }
             Abort(..) => {}
@@ -650,7 +622,7 @@ fn call_native_function(
         ("Signer", "borrow_address") => {
             if state.locals.local_exists(args[0], func_env) {
                 // treat as identity function
-                state.copy_local(rets[0], args[0], func_env)
+                state.assign_local(rets[0], args[0], func_env)
             }
         }
         ("Vector", "borrow_mut") | ("Vector", "borrow") => {
@@ -696,7 +668,7 @@ fn call_native_function(
             if state.locals.local_exists(args[0], func_env) {
                 state.record_access(args[0], Access::Read, func_env); // reads the input address
                                                                       // treat as assignment
-                state.copy_local(rets[0], args[0], func_env)
+                state.assign_local(rets[0], args[0], func_env)
             }
         }
         ("Vector", "empty") | ("Vector", "destroy_empty") | ("Vector", "reverse") => (),

language/move-prover/bytecode/tests/read_write_set/copy_struct.exp

@@ -0,0 +1,158 @@
+============ initial translation from Move ================
+
+[variant baseline]
+public fun CopyStruct::g() {
+     var $t0|s1: CopyStruct::S
+     var $t1|s2: CopyStruct::S
+     var $t2: address
+     var $t3: CopyStruct::S
+     var $t4: u64
+     var $t5: &CopyStruct::S
+     var $t6: &address
+     var $t7: address
+     var $t8: &mut CopyStruct::G
+     var $t9: &mut u64
+     var $t10: address
+     var $t11: CopyStruct::S
+     var $t12: u64
+     var $t13: &CopyStruct::S
+     var $t14: &address
+     var $t15: address
+     var $t16: &mut CopyStruct::G
+     var $t17: &mut u64
+  0: $t2 := 0x7
+  1: $t3 := CopyStruct::ret_struct_copy($t2)
+  2: $t0 := $t3
+  3: $t4 := 1
+  4: $t5 := borrow_local($t0)
+  5: $t6 := borrow_field<CopyStruct::S>.a($t5)
+  6: $t7 := read_ref($t6)
+  7: $t8 := borrow_global<CopyStruct::G>($t7)
+  8: $t9 := borrow_field<CopyStruct::G>.f($t8)
+  9: write_ref($t9, $t4)
+ 10: $t10 := 0x7
+ 11: $t11 := CopyStruct::ret_struct($t10)
+ 12: $t1 := $t11
+ 13: $t12 := 2
+ 14: $t13 := borrow_local($t1)
+ 15: $t14 := borrow_field<CopyStruct::S>.a($t13)
+ 16: $t15 := read_ref($t14)
+ 17: $t16 := borrow_global<CopyStruct::G>($t15)
+ 18: $t17 := borrow_field<CopyStruct::G>.f($t16)
+ 19: write_ref($t17, $t12)
+ 20: return ()
+}
+
+
+[variant baseline]
+public fun CopyStruct::ret_struct($t0|a: address): CopyStruct::S {
+     var $t1: address
+     var $t2: CopyStruct::S
+  0: $t1 := copy($t0)
+  1: $t2 := pack CopyStruct::S($t1)
+  2: return $t2
+}
+
+
+[variant baseline]
+public fun CopyStruct::ret_struct_copy($t0|a: address): CopyStruct::S {
+     var $t1|s: CopyStruct::S
+     var $t2: address
+     var $t3: CopyStruct::S
+     var $t4: &CopyStruct::S
+     var $t5: CopyStruct::S
+  0: $t2 := copy($t0)
+  1: $t3 := pack CopyStruct::S($t2)
+  2: $t1 := $t3
+  3: $t4 := borrow_local($t1)
+  4: $t5 := read_ref($t4)
+  5: return $t5
+}
+
+============ after pipeline `read_write_set` ================
+
+[variant baseline]
+public fun CopyStruct::g() {
+     var $t0|s1: CopyStruct::S
+     var $t1|s2: CopyStruct::S
+     var $t2: address
+     var $t3: CopyStruct::S
+     var $t4: u64
+     var $t5: &CopyStruct::S
+     var $t6: &address
+     var $t7: address
+     var $t8: &mut CopyStruct::G
+     var $t9: &mut u64
+     var $t10: address
+     var $t11: CopyStruct::S
+     var $t12: u64
+     var $t13: &CopyStruct::S
+     var $t14: &address
+     var $t15: address
+     var $t16: &mut CopyStruct::G
+     var $t17: &mut u64
+     # Accesses:
+     # 0x7/0x1::CopyStruct::G/f: Write
+     #
+     # Locals:
+     #
+  0: $t2 := 0x7
+  1: $t3 := CopyStruct::ret_struct_copy($t2)
+  2: $t0 := $t3
+  3: $t4 := 1
+  4: $t5 := borrow_local($t0)
+  5: $t6 := borrow_field<CopyStruct::S>.a($t5)
+  6: $t7 := read_ref($t6)
+  7: $t8 := borrow_global<CopyStruct::G>($t7)
+  8: $t9 := borrow_field<CopyStruct::G>.f($t8)
+  9: write_ref($t9, $t4)
+ 10: $t10 := 0x7
+ 11: $t11 := CopyStruct::ret_struct($t10)
+ 12: $t1 := $t11
+ 13: $t12 := 2
+ 14: $t13 := borrow_local($t1)
+ 15: $t14 := borrow_field<CopyStruct::S>.a($t13)
+ 16: $t15 := read_ref($t14)
+ 17: $t16 := borrow_global<CopyStruct::G>($t15)
+ 18: $t17 := borrow_field<CopyStruct::G>.f($t16)
+ 19: write_ref($t17, $t12)
+ 20: return ()
+}
+
+
+[variant baseline]
+public fun CopyStruct::ret_struct($t0|a: address): CopyStruct::S {
+     var $t1: address
+     var $t2: CopyStruct::S
+     # Accesses:
+     # Formal(0): Read
+     #
+     # Locals:
+     # Ret(0)/a: Formal(0)
+     #
+  0: $t1 := copy($t0)
+  1: $t2 := pack CopyStruct::S($t1)
+  2: return $t2
+}
+
+
+[variant baseline]
+public fun CopyStruct::ret_struct_copy($t0|a: address): CopyStruct::S {
+     var $t1|s: CopyStruct::S
+     var $t2: address
+     var $t3: CopyStruct::S
+     var $t4: &CopyStruct::S
+     var $t5: CopyStruct::S
+     # Accesses:
+     # Formal(0): Read
+     #
+     # Locals:
+     # Ret(0)/a: Formal(0)
+     #
+  0: $t2 := copy($t0)
+  1: $t3 := pack CopyStruct::S($t2)
+  2: $t1 := $t3
+  3: $t4 := borrow_local($t1)
+  4: $t5 := read_ref($t4)
+  5: return $t5
+}

language/move-prover/bytecode/tests/read_write_set/copy_struct.move

@@ -0,0 +1,23 @@
+module 0x1::CopyStruct {
+    struct S has copy, drop { a: address }
+
+    struct G has key { f: u64 }
+
+    public fun ret_struct(a: address): S {
+        S { a }
+    }
+
+    // returning a copy of S should behave the same as returning S
+    public fun ret_struct_copy(a: address): S {
+        let s = S { a };
+        *&s
+    }
+
+    public fun g() acquires G {
+        let s1 = ret_struct_copy(@0x7);
+        borrow_global_mut<G>(s1.a).f = 1;
+
+        let s2 = ret_struct(@0x7);
+        borrow_global_mut<G>(s2.a).f = 2;
+    }
+}

language/move-prover/bytecode/tests/read_write_set/secondary_index.exp

@@ -228,6 +228,7 @@ fun SecondaryIndex::read_secondary_index_from_formal_interproc($t0|a_addr: addre
      var $t5: address
      # Accesses:
      # Formal(0): Read
+     # Formal(0)/0x1::SecondaryIndex::B/b_addr: Read
      #
      # Locals:
      # Ret(0): Formal(0)/0x1::SecondaryIndex::B/b_addr