[read/write set analysis] adding some useful tests

Adding tests for: - reading an address from a vector stored in a struct (credit Daniel Perez) - reading from secondary indexes - reading nested fields Closes: aptos-labs#8706
IDxtc · Jul 8, 2021 · 9a2cfd3 · 9a2cfd3
1 parent e3daba1
commit 9a2cfd3
Show file tree

Hide file tree

Showing 8 changed files with 928 additions and 10 deletions.
diff --git a/language/move-prover/bytecode/tests/read_write_set/borrow.exp b/language/move-prover/bytecode/tests/read_write_set/borrow.exp
@@ -1,5 +1,82 @@
 ============ initial translation from Move ================
 
+[variant baseline]
+public intrinsic fun Vector::contains<#0>($t0|v: &vector<#0>, $t1|e: &#0): bool;
+
+
+[variant baseline]
+public intrinsic fun Vector::index_of<#0>($t0|v: &vector<#0>, $t1|e: &#0): (bool, u64);
+
+
+[variant baseline]
+public intrinsic fun Vector::append<#0>($t0|lhs: &mut vector<#0>, $t1|other: vector<#0>);
+
+
+[variant baseline]
+public native fun Vector::borrow<#0>($t0|v: &vector<#0>, $t1|i: u64): &#0;
+
+
+[variant baseline]
+public native fun Vector::borrow_mut<#0>($t0|v: &mut vector<#0>, $t1|i: u64): &mut #0;
+
+
+[variant baseline]
+public native fun Vector::destroy_empty<#0>($t0|v: vector<#0>);
+
+
+[variant baseline]
+public native fun Vector::empty<#0>(): vector<#0>;
+
+
+[variant baseline]
+public intrinsic fun Vector::is_empty<#0>($t0|v: &vector<#0>): bool;
+
+
+[variant baseline]
+public native fun Vector::length<#0>($t0|v: &vector<#0>): u64;
+
+
+[variant baseline]
+public native fun Vector::pop_back<#0>($t0|v: &mut vector<#0>): #0;
+
+
+[variant baseline]
+public native fun Vector::push_back<#0>($t0|v: &mut vector<#0>, $t1|e: #0);
+
+
+[variant baseline]
+public intrinsic fun Vector::remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0;
+
+
+[variant baseline]
+public intrinsic fun Vector::reverse<#0>($t0|v: &mut vector<#0>);
+
+
+[variant baseline]
+public fun Vector::singleton<#0>($t0|e: #0): vector<#0> {
+     var $t1|v: vector<#0>
+     var $t2: vector<#0>
+     var $t3: &mut vector<#0>
+     var $t4: #0
+     var $t5: vector<#0>
+  0: $t2 := Vector::empty<#0>()
+  1: $t1 := $t2
+  2: $t3 := borrow_local($t1)
+  3: $t4 := move($t0)
+  4: Vector::push_back<#0>($t3, $t4)
+  5: $t5 := move($t1)
+  6: return $t5
+}
+
+
+[variant baseline]
+public native fun Vector::swap<#0>($t0|v: &mut vector<#0>, $t1|i: u64, $t2|j: u64);
+
+
+[variant baseline]
+public intrinsic fun Vector::swap_remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0;
+
+
 [variant baseline]
 fun Borrow::borrow_s($t0|a: address) {
      var $t1: address
@@ -21,8 +98,116 @@ fun Borrow::borrow_s_mut($t0|a: address) {
   3: return ()
 }
 
+
+[variant baseline]
+fun Borrow::borrow_vec($t0|v: &vector<u64>) {
+     var $t1: &vector<u64>
+     var $t2: u64
+     var $t3: &u64
+  0: $t1 := move($t0)
+  1: $t2 := 7
+  2: $t3 := Vector::borrow<u64>($t1, $t2)
+  3: destroy($t3)
+  4: return ()
+}
+
+
+[variant baseline]
+fun Borrow::borrow_vec_mut($t0|v: &mut vector<u64>) {
+     var $t1: &mut vector<u64>
+     var $t2: u64
+     var $t3: &mut u64
+  0: $t1 := move($t0)
+  1: $t2 := 7
+  2: $t3 := Vector::borrow_mut<u64>($t1, $t2)
+  3: destroy($t3)
+  4: return ()
+}
+
 ============ after pipeline `read_write_set` ================
 
+[variant baseline]
+public intrinsic fun Vector::contains<#0>($t0|v: &vector<#0>, $t1|e: &#0): bool;
+
+
+[variant baseline]
+public intrinsic fun Vector::index_of<#0>($t0|v: &vector<#0>, $t1|e: &#0): (bool, u64);
+
+
+[variant baseline]
+public intrinsic fun Vector::append<#0>($t0|lhs: &mut vector<#0>, $t1|other: vector<#0>);
+
+
+[variant baseline]
+public native fun Vector::borrow<#0>($t0|v: &vector<#0>, $t1|i: u64): &#0;
+
+
+[variant baseline]
+public native fun Vector::borrow_mut<#0>($t0|v: &mut vector<#0>, $t1|i: u64): &mut #0;
+
+
+[variant baseline]
+public native fun Vector::destroy_empty<#0>($t0|v: vector<#0>);
+
+
+[variant baseline]
+public native fun Vector::empty<#0>(): vector<#0>;
+
+
+[variant baseline]
+public intrinsic fun Vector::is_empty<#0>($t0|v: &vector<#0>): bool;
+
+
+[variant baseline]
+public native fun Vector::length<#0>($t0|v: &vector<#0>): u64;
+
+
+[variant baseline]
+public native fun Vector::pop_back<#0>($t0|v: &mut vector<#0>): #0;
+
+
+[variant baseline]
+public native fun Vector::push_back<#0>($t0|v: &mut vector<#0>, $t1|e: #0);
+
+
+[variant baseline]
+public intrinsic fun Vector::remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0;
+
+
+[variant baseline]
+public intrinsic fun Vector::reverse<#0>($t0|v: &mut vector<#0>);
+
+
+[variant baseline]
+public fun Vector::singleton<#0>($t0|e: #0): vector<#0> {
+     var $t1|v: vector<#0>
+     var $t2: vector<#0>
+     var $t3: &mut vector<#0>
+     var $t4: #0
+     var $t5: vector<#0>
+     # Accesses:
+     # Formal(0): Read
+     #
+     # Locals:
+     #
+  0: $t2 := Vector::empty<#0>()
+  1: $t1 := $t2
+  2: $t3 := borrow_local($t1)
+  3: $t4 := move($t0)
+  4: Vector::push_back<#0>($t3, $t4)
+  5: $t5 := move($t1)
+  6: return $t5
+}
+
+
+[variant baseline]
+public native fun Vector::swap<#0>($t0|v: &mut vector<#0>, $t1|i: u64, $t2|j: u64);
+
+
+[variant baseline]
+public intrinsic fun Vector::swap_remove<#0>($t0|v: &mut vector<#0>, $t1|i: u64): #0;
+
+
 [variant baseline]
 fun Borrow::borrow_s($t0|a: address) {
      var $t1: address
@@ -53,3 +238,41 @@ fun Borrow::borrow_s_mut($t0|a: address) {
   2: destroy($t2)
   3: return ()
 }
+
+
+[variant baseline]
+fun Borrow::borrow_vec($t0|v: &vector<u64>) {
+     var $t1: &vector<u64>
+     var $t2: u64
+     var $t3: &u64
+     # Accesses:
+     # Formal(0): Read
+     # Formal(0)/[_]: Read
+     #
+     # Locals:
+     #
+  0: $t1 := move($t0)
+  1: $t2 := 7
+  2: $t3 := Vector::borrow<u64>($t1, $t2)
+  3: destroy($t3)
+  4: return ()
+}
+
+
+[variant baseline]
+fun Borrow::borrow_vec_mut($t0|v: &mut vector<u64>) {
+     var $t1: &mut vector<u64>
+     var $t2: u64
+     var $t3: &mut u64
+     # Accesses:
+     # Formal(0): Read
+     # Formal(0)/[_]: Read
+     #
+     # Locals:
+     #
+  0: $t1 := move($t0)
+  1: $t2 := 7
+  2: $t3 := Vector::borrow_mut<u64>($t1, $t2)
+  3: destroy($t3)
+  4: return ()
+}
diff --git a/language/move-prover/bytecode/tests/read_write_set/borrow.move b/language/move-prover/bytecode/tests/read_write_set/borrow.move
@@ -1,8 +1,8 @@
-address 0x1 {
-module Borrow {
-    // TODO: figure out how to allow this dependency
+// dep: ../../move-stdlib/modules/Vector.move
+
+module 0x1::Borrow {
     // ensure that borrows get counted as reads when appropriate
-    //use 0x1::Vector;
+    use 0x1::Vector;
 
     struct S has key { }
 
@@ -16,15 +16,13 @@ module Borrow {
         _ = borrow_global_mut<S>(a)
     }
 
-    /*// expected: read v/size
+    // expected: read v/size
     fun borrow_vec(v: &vector<u64>) {
         let _ = Vector::borrow(v, 7);
     }
 
     // expected: read v/size
-    fun borrow_vec_mut(v: &vector<u64>) {
-        let _ = Vector::borrow_mut(v, 7);
-    }*/
-
-}
+    fun borrow_vec_mut(v: &mut vector<u64>) {
+        let _ = Vector::borrow_mut<u64>(v, 7);
+    }
 }