[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: diem#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