Merge remote-tracking branch 'origin/sail2' into separate_bv

1 files changed, 54 insertions, 8 deletions

diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index bb1bc952..ce7080c4 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -21,6 +21,13 @@ val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect p
 val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
 overload length = {bitvector_length}
 overload __size = {length}
+val add_bits = {ocaml: "add_vec", lem: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+overload operator + = {add_bits}
+val vector_update_subrange = {
+  ocaml: "update_subrange",
+  lem: "update_subrange_vec_dec"
+} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
 
 /* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */
 
@@ -33,6 +40,14 @@ function foo(n, x) =
     64 => let z = y@y@y@y in let dfsf = 4 in z
   }
 
+val foo_if : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure
+
+function foo_if(n, x) =
+  let y : bits(16) = extzv(x) in
+  if n == 32
+  then y@y
+  else /* 64 */ let z = y@y@y@y in let dfsf = 4 in z
+
 val use : bits(16) -> unit effect pure
 
 function use(x) = ()
@@ -45,6 +60,13 @@ function bar(x) =
    16 => use(x)
   }
 
+val bar_if : forall 'n, 'n in {8,16}. bits('n) -> unit effect pure
+
+function bar_if(x) =
+  if 'n == 8
+  then use(x@x)
+  else /* 16 */ use(x)
+
 val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef}
 
 function ret(n, x) =
@@ -54,11 +76,9 @@ function ret(n, x) =
     64 => let z = y@y@y@y in { dfsf = 4; return z; undefined }
   }
 
-/* TODO: Assignments need more plumbing
-
-val assign : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect {undef}
+val assign : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef}
 
-function assign(x) = {
+function assign(n, x) = {
   let y : bits(16) = extzv(x);
   r : bits('n) = undefined;
   match 'n {
@@ -67,7 +87,29 @@ function assign(x) = {
   };
   r
 }
-*/
+
+val assign2 : forall 'm, 'm in {8,16}. bits('m) -> bits(32)
+
+function assign2(x) = {
+  y : bits('m) = x;
+  r : bits(32) = 0x00000000;
+  match 'm {
+     8 => { y = y + 0x01; r = extzv(y) },
+    16 => r = extzv(y)
+  };
+  r
+}
+
+val assign3 : forall 'm, 'm in {8,16}. bits('m) -> bits('m)
+
+function assign3(x) = {
+  y : bits('m) = x;
+  match 'm {
+    8 => y = y + 0x01,
+   16 => y[7..0] = 0x89
+  };
+  y
+}
 
 /* Adding casts for top-level pattern matches */
 
@@ -108,12 +150,16 @@ function run () = {
     assert((ret(0x34) : bits(64)) == 0x0034003400340034);
     assert((ret(0x3456) : bits(32)) == 0x34563456);
     assert((ret(0x3456) : bits(64)) == 0x3456345634563456);
-/*    assert((assign(0x12) : bits(32)) == 0x00120012);
+    assert((assign(0x12) : bits(32)) == 0x00120012);
     assert((assign(0x1234) : bits(32)) == 0x12341234);
     assert((assign(0x12) : bits(64)) == 0x0012001200120012);
-    assert((assign(0x1234) : bits(64)) == 0x1234123412341234);*/
+    assert((assign(0x1234) : bits(64)) == 0x1234123412341234);
+    assert(assign2(0x12) == 0x00000013);
+    assert(assign2(0x1234) == 0x00001234);
+    assert(assign3(0x12) == 0x13);
+    assert(assign3(0x1234) == 0x1289);
     assert(foo2(32,0x12) == 0x00120012);
     assert(foo2(64,0x12) == 0x0012001200120012);
     assert(foo3(4,0x12) == 0x00120012);
     assert(foo3(8,0x12) == 0x0012001200120012);
-}
\ No newline at end of file
+}