Merge branch 'mono-tweaks' into sail2

8 files changed, 89 insertions, 16 deletions

diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index ff9aa952..28a4d28d 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -21,12 +21,12 @@ def test_c(name, c_opts, sail_opts, valgrind):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('sail -no_warn -c {} {} 1> {}.c'.format(sail_opts, filename, basename))
-                step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, sail_dir, sail_dir, basename))
-                step('./{} 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0)
+                step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}.bin'.format(c_opts, basename, sail_dir, sail_dir, basename))
+                step('./{}.bin 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0)
                 step('diff {}.result {}.expect'.format(basename, basename))
                 if valgrind:
-                    step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0)
-                step('rm {}.c {} {}.result'.format(basename, basename, basename))
+                    step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}.bin".format(basename), expected_status = 1 if basename == "exception" else 0)
+                step('rm {}.c {}.bin {}.result'.format(basename, basename, basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
         results.collect(tests)
@@ -62,7 +62,7 @@ def test_interpreter(name):
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
-                step('sail -is execute.isail -iout {}.iresult {}'.format(basename, filename))
+                step('sail -undefined_gen -is execute.isail -iout {}.iresult {}'.format(basename, filename))
                 step('diff {}.iresult {}.expect'.format(basename, basename))
                 step('rm {}.iresult'.format(basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
@@ -79,11 +79,11 @@ def test_ocaml(name):
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
-                step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {} {}'.format(basename, basename, filename))
-                step('./{} 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0)
+                step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {}_ocaml {}'.format(basename, basename, filename))
+                step('./{}_ocaml 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0)
                 step('diff {}.oresult {}.expect'.format(basename, basename))
                 step('rm -r _sbuild_{}'.format(basename))
-                step('rm {}.oresult {}'.format(basename, basename))
+                step('rm {}.oresult {}_ocaml'.format(basename, basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
         results.collect(tests)
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
index db73580f..da6bce69 100755
--- a/test/coq/run_tests.sh
+++ b/test/coq/run_tests.sh
@@ -5,7 +5,7 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 SAILDIR="$DIR/../.."
 TYPECHECKTESTSDIR="$DIR/../typecheck/pass"
 EXTRATESTSDIR="$DIR/pass"
-BBVDIR="$DIR/../../../bbv/theories"
+BBVDIR="$DIR/../../../bbv/src/bbv"
 
 RED='\033[0;31m'
 GREEN='\033[0;32m'
diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail
index 0501cf1e..4540f1a5 100644
--- a/test/mono/itself_rewriting.sail
+++ b/test/mono/itself_rewriting.sail
@@ -1,5 +1,6 @@
 $include <smt.sail>
 $include <flow.sail>
+$include <arith.sail>
 default Order dec
 type bits ('n : Int) = bitvector('n, dec)
 val operator & = "and_bool" : (bool, bool) -> bool
@@ -67,10 +68,43 @@ function willsplit(x) = {
   shadowed(n);
 }
 
+val execute : forall 'datasize. int('datasize) -> unit
+
+function execute(datasize) = {
+  let x : bits('datasize) = replicate_bits(0b1, datasize);
+  ()
+}
+
+val test_execute : unit -> unit
+
+function test_execute() = {
+  let exp = 4;
+  let 'datasize = shl_int(1, exp);
+  execute(datasize)
+}
+
+val transitive_itself : forall 'n. int('n) -> unit
+
+function transitive_itself(n) = {
+  needs_size_in_guard(n);
+  ()
+}
+
+val transitive_split : bool -> unit
+
+function transitive_split(x) = {
+  let n = if x then 8 else 16;
+  transitive_itself(n);
+}
+
 val run : unit -> unit effect {escape}
 
 function run () = {
   assert(true); /* To force us into the monad */
+  test_execute();
   willsplit(true);
   willsplit(false);
-}
\ No newline at end of file
+  transitive_itself(16);
+  transitive_split(true);
+  transitive_split(false);
+}
diff --git a/test/typecheck/pass/floor_pow2.sail b/test/typecheck/pass/floor_pow2.sail
new file mode 100644
index 00000000..fa8680cf
--- /dev/null
+++ b/test/typecheck/pass/floor_pow2.sail
@@ -0,0 +1,17 @@
+$include <arith.sail>
+
+val "pow2" : forall 'n, 'n >= 0. int('n) -> int(2 ^ 'n)
+
+val floor_pow2 : forall ('x : Int), 'x >= 0. int('x) -> int
+
+function floor_pow2 x = {
+    if x == 0 then {
+        return(0);
+    } else {
+        n : {'n, 'n >= 1. int('n)} = 1;
+        while x >= pow2(n) do {
+            n = n + 1
+        };
+        return(pow2(n - 1))
+    }
+}
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
index 90166904..8854282d 100644
--- a/test/typecheck/pass/reg_32_64/v2.expect
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -1,13 +1,11 @@
 Type error:
-[reg_32_64/v2.sail]:21:18-22
+[reg_32_64/v2.sail]:21:2-15
 21 |  (*R)['d .. 0] = data
-   |                  ^--^
-   | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data
-   | Coercion failed because:
-   | Mismatched argument types in subtype check
+   |  ^-----------^
+   | Bounds check failed for l-expression: ((0 <= 0 & 0 <= 'd) & 'd < 64)
    | This error was caused by:
    | [reg_32_64/v2.sail]:21:2-15
    | 21 |  (*R)['d .. 0] = data
    |    |  ^-----------^
-   |    | Mismatched argument types in subtype check
+   |    | Bounds check failed for l-expression: ((0 <= 0 & 0 <= 'd) & 'd < 64)
    | 
diff --git a/test/typecheck/pass/repeat_constraint.sail b/test/typecheck/pass/repeat_constraint.sail
new file mode 100644
index 00000000..6d63f2e8
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _not_prove(constraint(false));
+  } until (false);
+}
diff --git a/test/typecheck/pass/repeat_constraint/v1.expect b/test/typecheck/pass/repeat_constraint/v1.expect
new file mode 100644
index 00000000..9d561e11
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[repeat_constraint/v1.sail]:7:4-29
+7 |    _prove(constraint(false));
+  |    ^-----------------------^
+  | Cannot prove false
+  | 
diff --git a/test/typecheck/pass/repeat_constraint/v1.sail b/test/typecheck/pass/repeat_constraint/v1.sail
new file mode 100644
index 00000000..5dd2f513
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _prove(constraint(false));
+  } until (false);
+}