Merge branch 'sail2' into rmem_interpreter

22 files changed, 324 insertions, 114 deletions

diff --git a/test/c/cfold_reg.expect b/test/c/cfold_reg.expect
new file mode 100644
index 00000000..27ba77dd
--- /dev/null
+++ b/test/c/cfold_reg.expect
@@ -0,0 +1 @@
+true
diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail
new file mode 100644
index 00000000..a5090e91
--- /dev/null
+++ b/test/c/cfold_reg.sail
@@ -0,0 +1,30 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "eq_string" : (string, string) -> bool
+
+overload operator == = {eq_string}
+
+register R : bool
+
+val "print_endline" : string -> unit
+
+function IMPDEF(str : string) -> bool = {
+  if str == "A" then {
+    return(R)
+  } else if str == "B" then {
+    true
+  } else {
+    false
+  }
+}
+
+function main(() : unit) -> unit = {
+  R = true;
+  if IMPDEF("A") then {
+    print_endline("true")
+  } else {
+    print_endline("false")
+  }
+}
\ No newline at end of file
diff --git a/test/c/cheri128_hsb.expect b/test/c/cheri128_hsb.expect
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/test/c/cheri128_hsb.expect
diff --git a/test/c/cheri128_hsb.sail b/test/c/cheri128_hsb.sail
new file mode 100644
index 00000000..d8501d88
--- /dev/null
+++ b/test/c/cheri128_hsb.sail
@@ -0,0 +1,62 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <option.sail>
+$include <vector_dec.sail>
+$include <exception_basic.sail>
+
+val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
+
+val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
+
+val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
+  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
+
+val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c == 'a | 'c == 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
+
+overload operator + = {add_range}
+overload operator - = {sub_range}
+
+infix 1 >>
+infix 1 <<
+
+val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) effect {undef}
+
+val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m)
+
+overload operator >> = {shift_bits_right, shiftr}
+overload operator << = {shift_bits_left, shiftl}
+
+val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))}
+
+function HighestSetBit x = {
+  foreach (i from ('N - 1) to 0 by 1 in dec)
+    if [x[i]] == 0b1 then return (true, i);
+  return (false, 0)
+}
+
+/* hw rounds up E to multiple of 4 */
+function roundUp(e) : range(0, 45) -> range(0, 48) =
+    let 'r = modulus(e, 4) in
+    if (r == 0)
+    then e
+    else (e - r + 4)
+
+function computeE (rlength) : bits(65) -> range(0, 48) =
+    let (nonzero, 'msb) = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
+    if nonzero then
+      /* above will always return <= 45 because 19 bits of zero are shifted in from right */
+      {assert(0 <= msb & msb <= 45); roundUp (min(msb,45)) }
+    else
+      0
+
+val main : unit -> unit effect {escape}
+
+function main() = {
+  let _ = computeE(0xFFFF_FFFF_FFFF_FFFF @ 0b1);
+  ()
+}
\ No newline at end of file
diff --git a/test/c/cheri_capstruct_order.expect b/test/c/cheri_capstruct_order.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/cheri_capstruct_order.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/cheri_capstruct_order.sail b/test/c/cheri_capstruct_order.sail
new file mode 100644
index 00000000..6eb774dd
--- /dev/null
+++ b/test/c/cheri_capstruct_order.sail
@@ -0,0 +1,32 @@
+default Order dec
+
+val SignalException : unit -> unit effect {rreg}
+
+val SignalExceptionBadAddr : unit -> unit effect {rreg}
+
+function SignalExceptionBadAddr() = {
+    SignalException();
+}
+
+struct CapStruct = {
+    base : bool,
+}
+
+type CapReg = CapStruct
+
+function getCapBase(c)   : CapStruct -> bool = c.base
+
+register KCC : CapReg
+
+function SignalException () = {
+    base = getCapBase(KCC);
+    ();
+}
+
+val "print_endline" : string -> unit
+
+val main : unit -> unit
+
+function main() = {
+  print_endline("ok")
+}
\ No newline at end of file
diff --git a/test/c/config.expect b/test/c/config.expect
new file mode 100644
index 00000000..059a413f
--- /dev/null
+++ b/test/c/config.expect
@@ -0,0 +1,6 @@
+x = 3
+Hello
+z = 0xFF
+x = 4
+World
+z = 0xAA
diff --git a/test/c/config.sail b/test/c/config.sail
new file mode 100644
index 00000000..2902d259
--- /dev/null
+++ b/test/c/config.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <arith.sail>
+$include <vector_dec.sail>
+
+val "print" : string -> unit
+
+register q : int
+
+register configuration x : int = 3
+
+register configuration y : string = "Hello\n"
+
+register configuration z : bits(8) = 0xFF
+
+val init : unit -> unit effect {configuration}
+
+function init() = {
+  x = 4;
+  y = "World\n";
+  z = 0xAA;
+}
+
+val main : unit -> unit effect {configuration}
+
+function main() = {
+  print_int("x = ", x);
+  print(y);
+  print_bits("z = ", z);
+  init();
+  print_int("x = ", x);
+  print(y);
+  print_bits("z = ", z);
+}
\ No newline at end of file
diff --git a/test/c/config_register.expect b/test/c/config_register.expect
new file mode 100644
index 00000000..8d164b5c
--- /dev/null
+++ b/test/c/config_register.expect
@@ -0,0 +1 @@
+R = 0x00000000
diff --git a/test/c/config_register.sail b/test/c/config_register.sail
new file mode 100644
index 00000000..f4831ca5
--- /dev/null
+++ b/test/c/config_register.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+function zeros forall 'n. (() : unit) -> bits('n) = {
+  sail_zeros('n)
+}
+
+register configuration R : bits(32) = zeros()
+
+register S : bits(32)
+
+function main(() : unit) -> unit = {
+    R = zeros();
+    print_bits("R = ", R)
+}
\ No newline at end of file
diff --git a/test/c/custom_flow.expect b/test/c/custom_flow.expect
new file mode 100644
index 00000000..cf275436
--- /dev/null
+++ b/test/c/custom_flow.expect
@@ -0,0 +1,5 @@
+1
+2
+3
+4
+4
diff --git a/test/c/custom_flow.sail b/test/c/custom_flow.sail
new file mode 100644
index 00000000..43c980d6
--- /dev/null
+++ b/test/c/custom_flow.sail
@@ -0,0 +1,43 @@
+val "print_endline" : string -> unit
+
+val operator <= = {
+  coq: "Z.leb",
+  _: "lteq"
+} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+function test1 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  if n <= m then {
+    _prove(constraint('n <= 'm));
+    print_endline("1");
+  } else {
+    print_endline("2");
+    _prove(constraint('n > 'm));
+  }
+}
+
+val and_bool = {
+  coq: "andb",
+  _: "and_bool"
+} : forall ('p: Bool) ('q: Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+overload operator & = {and_bool}
+
+function test2 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  let x = n <= m & n <= 20;
+  if x then {
+    _prove(constraint('n <= 20));
+    _prove(constraint('n <= 'm));
+    print_endline("3")
+  } else {
+    _prove(constraint('n > 'm | 'n > 20));
+    print_endline("4")
+  }
+}
+
+function main((): unit) -> unit = {
+  test1(1, 2);
+  test1(2, 1);
+  test2(1, 2);
+  test2(2, 1);
+  test2(21, 0)
+}
\ No newline at end of file
diff --git a/test/c/list_test.sail b/test/c/list_test.sail
index c315d3bf..b89e0f47 100644
--- a/test/c/list_test.sail
+++ b/test/c/list_test.sail
@@ -20,8 +20,8 @@ val main : unit -> unit
 
 function main () = {
   let x : list(int) = [|1, 2, 3|];
-  let y = hd(0 : int, x);
+  let y : int = hd(0, x);
   print_int("y = ", y);
-  print_int("hd(tl(x)) = ", hd(0, tl(x)));
-  print_int("hd(tl(tl(x))) = ", hd(0, tl(tl(x))));
+  print_int("hd(tl(x)) = ", hd(0, tl(x)) : int);
+  print_int("hd(tl(tl(x))) = ", hd(0, tl(tl(x))) : int);
 }
\ No newline at end of file
diff --git a/test/c/non_unique.expect b/test/c/non_unique.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/non_unique.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/non_unique.sail b/test/c/non_unique.sail
new file mode 100644
index 00000000..eda7720d
--- /dev/null
+++ b/test/c/non_unique.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function f(_: int) -> unit = ()
+function g(_: bits(1)) -> unit = ()
+
+function main(() : unit) -> unit = {
+  let y : int = {
+    let x : int = 3;
+    x
+  };
+  {
+    let x : bits(1) = 0b0;
+    g(x)
+  };
+  print_endline("ok");
+}
\ No newline at end of file
diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail
index 6d0bdaad..c4989829 100644
--- a/test/c/poly_pair.sail
+++ b/test/c/poly_pair.sail
@@ -4,7 +4,7 @@ val print = "print_endline" : string -> unit
 
 val "eq_int" : (int, int) -> bool
 
-union test ('a : Type) ('b : Type) = {
+union test('a : Type, 'b : Type) = {
   Ctor1 : ('a, 'b),
   Ctor2 : int
 }
diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index 6cd75981..4f221636 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -13,9 +13,10 @@ from sailtest import *
 
 def test_c(name, c_opts, sail_opts, valgrind):
     banner('Testing {} with C options: {} Sail options: {} valgrind: {}'.format(name, c_opts, sail_opts, valgrind))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -27,13 +28,15 @@ def test_c(name, c_opts, sail_opts, valgrind):
                     step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=1 ./{}".format(basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
-    return collect_results(name, tests)
+        results.collect(tests)
+    return results.finish()
 
 def test_interpreter(name):
     banner('Testing {}'.format(name))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -41,13 +44,15 @@ def test_interpreter(name):
                 step('diff {}.iresult {}.expect'.format(basename, basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
-    return collect_results(name, tests)
+        results.collect(tests)
+    return results.finish()
 
 def test_ocaml(name):
     banner('Testing {}'.format(name))
-    tests = {}
-    for filename in os.listdir('.'):
-        if re.match('.+\.sail', filename):
+    results = Results(name)
+    for filenames in chunks(os.listdir('.'), parallel()):
+        tests = {}
+        for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
             tests[filename] = os.fork()
             if tests[filename] == 0:
@@ -56,13 +61,15 @@ def test_ocaml(name):
                 step('diff {}.oresult {}.expect'.format(basename, basename))
                 print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
                 sys.exit()
-    return collect_results(name, tests)
+        results.collect(tests)
+    return results.finish()
 
 xml = '<testsuites>\n'
 
 xml += test_c('unoptimized C', '', '', True)
 xml += test_c('optimized C', '-O2', '-O', True)
 xml += test_c('constant folding', '', '-Oconstant_fold', True)
+xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True)
 xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False)
 
 xml += test_interpreter('interpreter')
diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh
deleted file mode 100755
index 37787605..00000000
--- a/test/c/run_tests.sh
+++ /dev/null
@@ -1,98 +0,0 @@
-
-#!/usr/bin/env bash
-set -e
-
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
-cd $DIR
-SAILDIR="$DIR/../.."
-
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
-NC='\033[0m'
-
-rm -f $DIR/tests.xml
-
-pass=0
-fail=0
-XML=""
-
-function green {
-    (( pass += 1 ))
-    printf "$1: ${GREEN}$2${NC}\n"
-    XML+="    <testcase name=\"$1\"/>\n"
-}
-
-function yellow {
-    (( fail += 1 ))
-    printf "$1: ${YELLOW}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function red {
-    (( fail += 1 ))
-    printf "$1: ${RED}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function finish_suite {
-    printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n"
-    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
-    printf "$XML" >> $DIR/tests.xml
-    XML=""
-    pass=0
-    fail=0
-}
-
-printf "<testsuites>\n" >> $DIR/tests.xml
-
-shopt -s nullglob;
-
-function run_c_tests {
-    for file in $DIR/*.sail;
-    do
-	if $SAILDIR/sail -no_warn -c $SAIL_OPTS $file 1> ${file%.sail}.c 2> /dev/null;
-	then
-	    green "compiling $(basename $file) ($SAIL_OPTS)" "ok";
-	    if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -lz -I $SAILDIR/lib;
-	    then
-		green "compiling $(basename ${file%.sail}.c) ($CC_OPTS)" "ok";
-		$DIR/a.out 1> ${file%.sail}.result 2> /dev/null;
-		if diff ${file%.sail}.result ${file%.sail}.expect;
-		then
-		    green "executing $(basename ${file%.sail})" "ok"
-		else
-		    red "executing $(basename ${file%.sail})" "fail"
-		fi;
-		if valgrind -q --leak-check=full --errors-for-leak-kinds=all --error-exitcode=1 $DIR/a.out 1> /dev/null 2> /dev/null;
-		then
-		    green "executing $(basename ${file%.sail}) with valgrind" "ok"
-		else
-		    red "executing $(basename ${file%.sail}) with valgrind" "fail"
-		fi
-	    else
-		red "compiling generated C" "fail"
-	    fi
-	else
-	    red "compiling $file" "fail"
-	fi;
-	rm -f ${file%.sail}.c
-	rm -f ${file%.sail}.result
-    done
-}
-
-SAIL_OPTS=""
-CC_OPTS="-O0"
-run_c_tests
-
-SAIL_OPTS="-O"
-CC_OPTS="-O2"
-run_c_tests
-
-SAIL_OPTS="-O"
-CC_OPTS="-O2 -fsanitize=undefined"
-run_c_tests
-
-finish_suite "C testing"
-
-printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/c/small_slice.expect b/test/c/small_slice.expect
new file mode 100644
index 00000000..64d39581
--- /dev/null
+++ b/test/c/small_slice.expect
@@ -0,0 +1,2 @@
+v1 = 0x1234
+v2 = 0x34
diff --git a/test/c/small_slice.sail b/test/c/small_slice.sail
new file mode 100644
index 00000000..80878a80
--- /dev/null
+++ b/test/c/small_slice.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+function get_16((): unit) -> range(0, 16) = 16
+function get_8((): unit) -> range(0, 16) = 8
+
+function main((): unit) -> unit = {
+  let x = get_16();
+  let y = get_8();
+  let addr = 0x1234_ABCD;
+  let v1 = slice(addr, 16, x);
+  let v2 = slice(addr, 16, y);
+  print_bits("v1 = ", v1);
+  print_bits("v2 = ", v2);
+}
\ No newline at end of file
diff --git a/test/c/string_of_bits.expect b/test/c/string_of_bits.expect
new file mode 100644
index 00000000..e373cf38
--- /dev/null
+++ b/test/c/string_of_bits.expect
@@ -0,0 +1,6 @@
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
+HelloWorld0b11110000111 0xFF
diff --git a/test/c/string_of_bits.sail b/test/c/string_of_bits.sail
new file mode 100644
index 00000000..fcaeb3e1
--- /dev/null
+++ b/test/c/string_of_bits.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "concat_str" : (string, string) -> string
+
+infixl 1 ++
+
+overload operator ++ = {concat_str}
+
+val "print_endline" : string -> unit
+
+val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
+
+val DecStr = "decimal_string_of_bits" : forall 'n. bits('n) -> string
+
+function main(() : unit) -> unit = {
+  foreach (i from 0 to 5) {
+    let x = "Hello";
+    let y = "World";
+    let z = 0b1111_0000_111;
+    let w = 0xFF;
+    print_endline(x ++ y ++ BitStr(z) ++ " " ++ BitStr(w))
+  }
+}
\ No newline at end of file