Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2

5 files changed, 89 insertions, 2 deletions

diff --git a/lib/_tags b/lib/_tags
index b1a8186f..916a546b 100644
--- a/lib/_tags
+++ b/lib/_tags
@@ -1,2 +1,2 @@
-<*.m{l,li}>: package(lem), package(linksem), package(zarith), package(uint)
-<main.native>: package(lem), package(linksem), package(zarith), package(uint)
\ No newline at end of file
+<*.m{l,li}>: package(lem), package(linksem), package(zarith)
+<main.native>: package(lem), package(linksem), package(zarith)
\ No newline at end of file
diff --git a/lib/elf.sail b/lib/elf.sail
new file mode 100644
index 00000000..f158fbad
--- /dev/null
+++ b/lib/elf.sail
@@ -0,0 +1,8 @@
+$ifndef _ELF
+$define _ELF
+
+val elf_entry = "Elf_loader.elf_entry" : unit -> int
+
+val elf_tohost = "Elf_loader.elf_tohost" : unit -> int
+
+$endif
diff --git a/lib/flow.sail b/lib/flow.sail
new file mode 100644
index 00000000..cb7b1b99
--- /dev/null
+++ b/lib/flow.sail
@@ -0,0 +1,42 @@
+$ifndef _FLOW
+$define _FLOW
+
+val not_bool = "not" : bool -> bool
+val and_bool = "and_bool" : (bool, bool) -> bool
+val or_bool = "or_bool" : (bool, bool) -> bool
+
+val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+function neq_atom (x, y) = not_bool(eq_atom(x, y))
+
+val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lt_atom = "lt"     : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gt_atom = "gt"     : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+val lt_range_atom = "lt"     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val lteq_range_atom = "lteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val gt_range_atom = "gt"     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val gteq_range_atom = "gteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val lt_atom_range = "lt"     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val lteq_atom_range = "lteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val gt_atom_range = "gt"     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+
+$ifdef TEST
+
+val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit
+
+function __flow_test (x, y) = {
+  if lteq_atom(x, y) then {
+    _prove(constraint('n <= 'm))
+  } else {
+    _prove(constraint('n > 'm))
+  }
+}
+
+$endif
+
+$endif
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index fd1d1b23..a69dc379 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -122,3 +122,10 @@ function UInt_slice(xs,i,l) = {
   let xs = (xs & slice_mask(i,l)) >> i in
   UInt(xs)
 }
+
+val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure
+
+function zext_ones(m) = {
+  let v : bits('n) = extsv(0b1) in
+  v >> ('n - m)
+}
diff --git a/lib/smt.sail b/lib/smt.sail
new file mode 100644
index 00000000..702b82c6
--- /dev/null
+++ b/lib/smt.sail
@@ -0,0 +1,30 @@
+$ifndef _SMT
+$define _SMT
+
+// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
+
+val div = {
+  smt: "div",
+  ocaml: "quotient",
+  lem: "integerDiv"
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
+
+val mod = {
+  smt: "mod",
+  ocaml: "modulus",
+  lem: "integerMod"
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
+
+val abs = {
+  smt : "abs",
+  ocaml: "abs_int",
+  lem: "abs_int"
+} : forall 'n. atom('n) -> {'o, 'o = abs('n). atom('o)}
+
+$ifdef TEST
+
+let __smt_x : atom(div(4, 2)) = div(8, 4)
+
+$endif
+
+$endif