fix-constant-and-ghost-mem (#11101)

aptos-labs · Nov 29, 2023 · afe4703 · afe4703
1 parent fc04dcc
commit afe4703
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 15 deletions.
diff --git a/aptos-move/framework/aptos-stdlib/tests/fixedpoint64_tests.move b/aptos-move/framework/aptos-stdlib/tests/fixedpoint64_tests.move
@@ -2,7 +2,9 @@
 module aptos_std::fixed_point64_tests {
     use aptos_std::fixed_point64;
 
-    const POW2_64: u128 = 1 << 64;
+    fun POW2_64(): u128 {
+        1 << 64 // TODO(#9330)
+    }
     const MAX_U128: u128 = 340282366920938463463374607431768211455;
 
     #[test]
@@ -17,15 +19,15 @@ module aptos_std::fixed_point64_tests {
     fun create_overflow() {
         // The maximum value is 2^32 - 1. Check that anything larger aborts
         // with an overflow.
-        fixed_point64::create_from_rational(POW2_64, 1); // 2^64
+        fixed_point64::create_from_rational(POW2_64(), 1); // 2^64
     }
 
     #[test]
     #[expected_failure(abort_code = fixed_point64::ERATIO_OUT_OF_RANGE)]
     fun create_underflow() {
         // The minimum non-zero value is 2^-32. Check that anything smaller
         // aborts.
-        fixed_point64::create_from_rational(1, 2 * POW2_64); // 2^-65
+        fixed_point64::create_from_rational(1, 2 * POW2_64()); // 2^-65
     }
 
     #[test]
@@ -47,7 +49,7 @@ module aptos_std::fixed_point64_tests {
     fun divide_overflow_small_divisore() {
         let f = fixed_point64::create_from_raw_value(1); // 2^-64
         // Divide 2^64 by the minimum fractional value. This should overflow.
-        fixed_point64::divide_u128(POW2_64, f);
+        fixed_point64::divide_u128(POW2_64(), f);
     }
 
     #[test]
@@ -71,7 +73,7 @@ module aptos_std::fixed_point64_tests {
     fun multiply_overflow_large_multiplier() {
         let f = fixed_point64::create_from_raw_value(MAX_U128);
         // Multiply 2^65 by the maximum fixed-point value. This should overflow.
-        fixed_point64::multiply_u128(2 * POW2_64, f);
+        fixed_point64::multiply_u128(2 * POW2_64(), f);
     }
 
     #[test]
@@ -107,7 +109,7 @@ module aptos_std::fixed_point64_tests {
         // Test creating a 1.0 fraction from the maximum u64 value.
         let f = fixed_point64::create_from_rational(MAX_U128, MAX_U128);
         let one = fixed_point64::get_raw_value(f);
-        assert!(one == POW2_64, 0); // 0x1.00000000
+        assert!(one == POW2_64(), 0); // 0x1.00000000
     }
 
     #[test]
@@ -116,10 +118,10 @@ module aptos_std::fixed_point64_tests {
         let two = fixed_point64::create_from_rational(2, 1);
         let smaller_number1 = fixed_point64::min(one, two);
         let val1 = fixed_point64::get_raw_value(smaller_number1);
-        assert!(val1 == POW2_64, 0);  // 0x1.00000000
+        assert!(val1 == POW2_64(), 0);  // 0x1.00000000
         let smaller_number2 = fixed_point64::min(two, one);
         let val2 = fixed_point64::get_raw_value(smaller_number2);
-        assert!(val2 == POW2_64, 0);  // 0x1.00000000
+        assert!(val2 == POW2_64(), 0);  // 0x1.00000000
     }
 
     #[test]
@@ -129,9 +131,9 @@ module aptos_std::fixed_point64_tests {
         let larger_number1 = fixed_point64::max(one, two);
         let larger_number2 = fixed_point64::max(two, one);
         let val1 = fixed_point64::get_raw_value(larger_number1);
-        assert!(val1 == 2 * POW2_64, 0);  // 0x2.00000000
+        assert!(val1 == 2 * POW2_64(), 0);  // 0x2.00000000
         let val2 = fixed_point64::get_raw_value(larger_number2);
-        assert!(val2 == 2 * POW2_64, 0);  // 0x2.00000000
+        assert!(val2 == 2 * POW2_64(), 0);  // 0x2.00000000
     }
 
     #[test]
@@ -145,13 +147,13 @@ module aptos_std::fixed_point64_tests {
     fun create_from_u128_create_correct_fixed_point_number() {
         let one = fixed_point64::create_from_u128(1);
         let val = fixed_point64::get_raw_value(one);
-        assert!(val == POW2_64, 0);
+        assert!(val == POW2_64(), 0);
     }
 
     #[test]
     #[expected_failure(abort_code = fixed_point64::ERATIO_OUT_OF_RANGE)]
     fun create_from_u128_throw_error_when_number_too_large() {
-        fixed_point64::create_from_u128(POW2_64);
+        fixed_point64::create_from_u128(POW2_64());
     }
 
     #[test]

diff --git a/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs b/third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs
@@ -155,6 +155,9 @@ impl ModuleGenerator {
 
     /// Generate information for a struct.
     fn gen_struct(&mut self, ctx: &ModuleContext, struct_env: &StructEnv<'_>) {
+        if struct_env.is_ghost_memory() {
+            return;
+        }
         let loc = &struct_env.get_loc();
         let struct_handle = self.struct_index(ctx, loc, struct_env);
         let field_information = FF::StructFieldInformation::Declared(

diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/with_spec.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/with_spec.exp
@@ -2,7 +2,7 @@
 
 [variant baseline]
 fun m::bar() {
-  0: assert true
+  0: assume 1
   1: return ()
 }
 
@@ -28,7 +28,7 @@ public fun m::foo($t0: &m::S): u8 {
 [variant baseline]
 fun m::bar() {
      # live vars:
-  0: assert true
+  0: assume 1
      # live vars:
   1: return ()
 }

diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/with_spec.move b/third_party/move/move-compiler-v2/tests/file-format-generator/with_spec.move
@@ -1,5 +1,8 @@
 module 0x42::m {
     use std::vector;
+    spec module {
+        global var: num;
+    }
     struct S {
         data: vector<E>,
     }
@@ -14,7 +17,7 @@ module 0x42::m {
 
     fun bar() {
         spec {
-            assert true;
+            update var = 1;
         };
     }
 }