motoko-san: add option encoding into prelude & update tests

serokell · May 18, 2024 · 8782033 · 8782033
1 parent 1c3267b
commit 8782033
Show file tree

Hide file tree

Showing 34 changed files with 191 additions and 20 deletions.
diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml
@@ -17,10 +17,19 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */|prelude}
diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@46.1)
diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) (((((true && (acc(($Self).immut_arr,write) && ($array_acc(

diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok
@@ -1,2 +1,2 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@37.13--37.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@55.15--55.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@46.13--46.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@64.15--64.44)
diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 field $message_async: Int

diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@60.15--60.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@69.15--69.42)
diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 field $message_async_4: Int

diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok
@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@58.20--58.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@67.20--67.47)
diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 field $message_async: Int

diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))

diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@38.1)
diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))

diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 field $message_async: Int

diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@38.1)
diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) ((true && acc(($Self).count,write)))

diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok
@@ -1 +1 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@34.13--34.24)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@43.13--43.24)
diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))

diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@28.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@29.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@38.1)
diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) (true)

diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@38.1)
diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) ((true && acc(($Self).boolFld,write)))

diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@29.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@38.1)
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) ((true && acc(($Self).x,write)))

diff --git a/test/viper/ok/polymono.silicon.ok b/test/viper/ok/polymono.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@28.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@29.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@38.1)
diff --git a/test/viper/ok/polymono.vpr.ok b/test/viper/ok/polymono.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) (true)

diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))

diff --git a/test/viper/ok/reverse.silicon.ok b/test/viper/ok/reverse.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@32.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@41.1)
diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok
@@ -17,12 +17,21 @@ domain Tuple {
   function $prj_inv2(r: Ref): Int
   axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
 }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
 /* Typed references */
 field $int: Int
 field $bool: Bool
 field $ref: Ref
 field $array: Array
 field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
 /* END PRELUDE */
 
 define $Perm($Self) ((true && (acc(($Self).xarray,write) && ($array_acc(

diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok
@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@28.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@29.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@37.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@38.1)