Merge branch 'sail2' into rmem_interpreter

18 files changed, 271 insertions, 9 deletions

diff --git a/test/c/bool_bits_mapping.expect b/test/c/bool_bits_mapping.expect
new file mode 100644
index 00000000..79ebd086
--- /dev/null
+++ b/test/c/bool_bits_mapping.expect
@@ -0,0 +1,2 @@
+ok
+ok
diff --git a/test/c/bool_bits_mapping.sail b/test/c/bool_bits_mapping.sail
new file mode 100644
index 00000000..1a104186
--- /dev/null
+++ b/test/c/bool_bits_mapping.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+$include <prelude.sail>
+
+mapping bool_bits : bool <-> bits(1) = {
+  true   <-> 0b1,
+  false  <-> 0b0
+}
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  if bool_bits(0b1) then {
+    print_endline("ok")
+  } else {
+    print_endline("fail")
+  };
+  if bool_bits(true) == 0b1 then {
+    print_endline("ok")
+  } else {
+    print_endline("fail")
+  }
+}
\ No newline at end of file
diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail
index a5090e91..53066bf5 100644
--- a/test/c/cfold_reg.sail
+++ b/test/c/cfold_reg.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-val "eq_string" : (string, string) -> bool
+val eq_string = { lem: "eq", _: "eq_string" } : (string, string) -> bool
 
 overload operator == = {eq_string}
 
diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail
index e8890a4a..a9480ab6 100644
--- a/test/c/cheri_capreg.sail
+++ b/test/c/cheri_capreg.sail
@@ -13,11 +13,11 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 val zeros_0 = "zeros" : forall 'n. int('n) -> bits('n)
 
-val zeros : forall 'n. unit -> bits('n)
-function zeros() = zeros_0('n)
+val zeros : forall 'n. (implicit('n), unit) -> bits('n)
+function zeros(n, _) = zeros_0(n)
 
-val ones : forall 'n, 'n >= 0 . unit -> bits('n)
-function ones() = replicate_bits (0b1,'n)
+val ones : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n)
+function ones(n, _) = replicate_bits(0b1, n)
 
 val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
diff --git a/test/c/config_register.sail b/test/c/config_register.sail
index f4831ca5..8b41a3f4 100644
--- a/test/c/config_register.sail
+++ b/test/c/config_register.sail
@@ -2,8 +2,9 @@ default Order dec
 
 $include <prelude.sail>
 
-function zeros forall 'n. (() : unit) -> bits('n) = {
-  sail_zeros('n)
+val zeros : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n)
+function zeros(n, _) = {
+  sail_zeros(n)
 }
 
 register configuration R : bits(32) = zeros()
diff --git a/test/c/eq_struct.sail b/test/c/eq_struct.sail
index b4258569..9da12aae 100644
--- a/test/c/eq_struct.sail
+++ b/test/c/eq_struct.sail
@@ -3,7 +3,7 @@ default Order dec
 $include <flow.sail>
 $include <exception_basic.sail>
 
-val eq = "eq_anything" : forall ('a : Type). ('a, 'a) -> bool
+val eq = { lem: "eq", _: "eq_anything" } : forall ('a : Type). ('a, 'a) -> bool
 
 overload operator == = {eq}
 
diff --git a/test/c/fallthrough_exception.expect b/test/c/fallthrough_exception.expect
new file mode 100644
index 00000000..6d9de85e
--- /dev/null
+++ b/test/c/fallthrough_exception.expect
@@ -0,0 +1 @@
+E2
diff --git a/test/c/fallthrough_exception.sail b/test/c/fallthrough_exception.sail
new file mode 100644
index 00000000..6260a603
--- /dev/null
+++ b/test/c/fallthrough_exception.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <prelude.sail>
+
+val print = "print_endline" : string -> unit
+
+union exception = {
+  E1 : unit,
+  E2 : unit
+}
+
+function main((): unit) -> unit = {
+  try {
+    try throw(E2()) catch {
+      E1() => print("E1")
+    }
+  } catch {
+    E2() => print("E2")
+  }
+}
\ No newline at end of file
diff --git a/test/c/implicits.expect b/test/c/implicits.expect
new file mode 100644
index 00000000..3d770e7d
--- /dev/null
+++ b/test/c/implicits.expect
@@ -0,0 +1,11 @@
+a = 0x00000000000000FF
+b = 0xFFFFFFFFFFFFFFFF
+c = 0xFFFFFFFFFFFFFFFF
+d = 0x0000000000000000
+e = 0x0000000000000000
+f = 0x0000000000000000
+g = 0x00000000
+h = 0x0000
+i = 0x00
+j = 0x0
+k = 0b00
diff --git a/test/c/implicits.sail b/test/c/implicits.sail
new file mode 100644
index 00000000..2923fab4
--- /dev/null
+++ b/test/c/implicits.sail
@@ -0,0 +1,45 @@
+default Order dec
+
+$include <prelude.sail>
+
+val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m)
+
+function EXTZ(m, x) = sail_zero_extend(x, m)
+
+val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m)
+
+function EXTS(m, x) = sail_sign_extend(x, m)
+
+val zeros : forall 'n, 'n >= 0. implicit('n) -> bits('n)
+
+function zeros(n) = replicate_bits(0b0, n)
+
+val dzeros : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m)) -> (bits('n), bits('m))
+
+function dzeros(n, m) = (zeros(n), zeros(m))
+
+val dzeros2 : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m), unit) -> (bits('n), bits('m))
+
+function dzeros2(n, m, _) = (zeros(n), zeros(m))
+
+function main((): unit) -> unit = {
+  let a: bits(64) = EXTZ(0xFF);
+  let b: bits(64) = EXTS(0xFF);
+  let c: bits(64) = EXTS(64, 0xFF);
+  let d: bits(64) = zeros();
+  let e: bits(64) = zeros(64);
+  let (f, g): (bits(64), bits(32)) = dzeros();
+  let (h, i) = dzeros(16, 8);
+  let (j, k): (bits(4), bits(2)) = dzeros2();
+  print_bits("a = ", a);
+  print_bits("b = ", b);
+  print_bits("c = ", c);
+  print_bits("d = ", d);
+  print_bits("e = ", e);
+  print_bits("f = ", f);
+  print_bits("g = ", g);
+  print_bits("h = ", h);
+  print_bits("i = ", i);
+  print_bits("j = ", j);
+  print_bits("k = ", k)
+}
\ No newline at end of file
diff --git a/test/c/lbuild/_tags b/test/c/lbuild/_tags
new file mode 100644
index 00000000..ced67350
--- /dev/null
+++ b/test/c/lbuild/_tags
@@ -0,0 +1,3 @@
+true: debug
+<*.m{l,li}>: package(lem), package(linksem), package(zarith)
+<main.native>: package(lem), package(linksem), package(zarith)
diff --git a/test/c/lbuild/myocamlbuild.ml b/test/c/lbuild/myocamlbuild.ml
new file mode 100644
index 00000000..cc65b03a
--- /dev/null
+++ b/test/c/lbuild/myocamlbuild.ml
@@ -0,0 +1,77 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ocamlbuild_plugin ;;
+open Command ;;
+open Pathname ;;
+open Outcome ;;
+
+(* paths relative to _build *)
+let lem = "lem" ;;
+
+(* All -wl ignores should be removed if you want to see the pattern compilation, exhaustive, and unused var warnings *)
+let lem_opts = [A "-lib"; P "..";
+                A "-wl_pat_comp"; P "ign";
+                A "-wl_pat_exh";  P "ign";
+                A "-wl_pat_fail"; P "ign";
+                A "-wl_unused_vars";   P "ign";
+               ] ;;
+
+dispatch begin function
+| After_rules ->
+    rule "lem -> ml"
+    ~prod: "%.ml"
+    ~dep: "%.lem"
+    (fun env builder -> Seq [
+      Cmd (S ([ P lem] @ lem_opts @ [ A "-ocaml"; P (env "%.lem") ]));
+      ]);
+
+| _ -> ()
+end ;;
diff --git a/test/c/nexp_synonym.expect b/test/c/nexp_synonym.expect
new file mode 100644
index 00000000..880c3ee3
--- /dev/null
+++ b/test/c/nexp_synonym.expect
@@ -0,0 +1 @@
+v = 0xFFFFFFFF
diff --git a/test/c/nexp_synonym.sail b/test/c/nexp_synonym.sail
new file mode 100644
index 00000000..b908b265
--- /dev/null
+++ b/test/c/nexp_synonym.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+type LEN : Int = 32
+
+let v : bits(LEN) = 0xFFFF_FFFF
+
+function main((): unit) -> unit = {
+  print_bits("v = ", v)
+}
\ No newline at end of file
diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail
index c4989829..7c86062d 100644
--- a/test/c/poly_pair.sail
+++ b/test/c/poly_pair.sail
@@ -2,7 +2,7 @@ default Order dec
 
 val print = "print_endline" : string -> unit
 
-val "eq_int" : (int, int) -> bool
+val eq_int = { lem: "eq", _: "eq_int" } : (int, int) -> bool
 
 union test('a : Type, 'b : Type) = {
   Ctor1 : ('a, 'b),
diff --git a/test/c/reg_32_64.expect b/test/c/reg_32_64.expect
new file mode 100644
index 00000000..c381486c
--- /dev/null
+++ b/test/c/reg_32_64.expect
@@ -0,0 +1,2 @@
+R = 0xCAFECAFEFFFFFFFF
+R = 0xFFFFFFFF
diff --git a/test/c/reg_32_64.sail b/test/c/reg_32_64.sail
new file mode 100644
index 00000000..79dfc862
--- /dev/null
+++ b/test/c/reg_32_64.sail
@@ -0,0 +1,39 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
+register R0 : bits(64)
+register R1 : bits(64)
+register R2 : bits(64)
+register R3 : bits(64)
+
+let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0]
+
+type regno('r: Int) -> Bool = 0 <= 'r <= 3
+
+val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (int('r), bits('d)) -> unit effect {wreg}
+
+function set_R(r, data) = {
+  let R = GPRs[r];
+  (*R)['d - 1 .. 0] = data
+}
+
+val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}.
+  (implicit('d), int('r)) -> bits('d) effect {rreg}
+
+function get_R(datasize, r) = {
+  let R = GPRs[r];
+  reg_deref(R)[datasize - 1 .. 0]
+}
+
+overload R = {set_R, get_R}
+
+function main() -> unit = {
+  R(0) = 0xCAFE_CAFE_0000_0000;
+  R(0) = 0xFFFF_FFFF;
+  print_bits("R = ", R(0) : bits(64));
+  print_bits("R = ", R(0) : bits(32))
+}
diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index 4f221636..4927e281 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -64,6 +64,30 @@ def test_ocaml(name):
         results.collect(tests)
     return results.finish()
 
+def test_lem(name):
+    banner('Testing {}'.format(name))
+    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:
+                step('sail -lem {}'.format(filename))
+                step('mkdir -p _lbuild_{}'.format(basename))
+                step('cp {}*.lem _lbuild_{}'.format(basename, basename))
+                step('cp lbuild/* _lbuild_{}'.format(basename))
+                step('cp ../../src/gen_lib/*.lem _lbuild_{}'.format(basename))
+                os.chdir('_lbuild_{}'.format(basename))
+                step('echo "let _ = {}.main ()" > main.ml'.format(basename.capitalize()))
+                step('ocamlbuild -use-ocamlfind main.native'.format(basename, basename))
+                step('./main.native 1> {}.lresult'.format(basename))
+                step('diff ../{}.expect {}.lresult'.format(basename, basename))
+                print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
+                sys.exit()
+        results.collect(tests)
+    return results.finish()
+
 xml = '<testsuites>\n'
 
 xml += test_c('unoptimized C', '', '', True)
@@ -76,6 +100,8 @@ xml += test_interpreter('interpreter')
 
 xml += test_ocaml('OCaml')
 
+#xml += test_lem('lem')
+
 xml += '</testsuites>\n'
 
 output = open('tests.xml', 'w')