Fixed loading ARM elf files

Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib

3 files changed, 80 insertions, 0 deletions

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/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