From b0e22dcfbf5db27f958e1b38dc37cd7c03f0aae2 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 26 Jan 2018 13:36:53 +0000
Subject: Shebang must be first line of file. Fixes RISCV test failing on
 jenkins due to non-bash default shell.

---
 test/riscv/run_tests.sh | 1 -
 1 file changed, 1 deletion(-)

diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index 9f1aa007..32f6f091 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -1,4 +1,3 @@
-
 #!/usr/bin/env bash
 set -e
 
-- 
cgit v1.2.3


From d9d064c0d91cc072e300f6ca7b6c12ca640c7712 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 26 Jan 2018 13:45:18 +0000
Subject: Give LEM test suite a more useful name for benefit of jenkins.

---
 test/lem/run_tests.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/lem/run_tests.sh b/test/lem/run_tests.sh
index 5d435950..c53ec189 100755
--- a/test/lem/run_tests.sh
+++ b/test/lem/run_tests.sh
@@ -61,6 +61,6 @@ do
     fi
 done
 
-finish_suite "Expecting pass"
+finish_suite "LEM tests"
 
 printf "</testsuites>\n" >> $DIR/tests.xml
-- 
cgit v1.2.3


From cba3932176946e69a25d16e0e32527563faed71f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 26 Jan 2018 11:16:12 +0000
Subject: Preserve more typing info in monomorphisation for later stages

---
 src/monomorphise.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 2e7ad08f..59052c24 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1504,8 +1504,9 @@ let split_defs continue_anyway splits defs =
            | Some (Some (pats,l)) ->
               Some (List.mapi (fun i p ->
                 match p with
-                | P_aux (P_lit lit,_) when (match lit with L_aux (L_undef,_) -> false | _ -> true) ->
-                   p,[id,E_aux (E_lit lit,(Generated Unknown,None))],[l,(i,[])]
+                | P_aux (P_lit lit,(pl,pannot))
+                    when (match lit with L_aux (L_undef,_) -> false | _ -> true) ->
+                   p,[id,E_aux (E_lit lit,(Generated pl,pannot))],[l,(i,[])]
                 | _ ->
                    let p',subst = freshen_pat_bindings p in
                    P_aux (P_as (p',id),(l,annot)),[],[l,(i,subst)])
@@ -2664,8 +2665,8 @@ let initial_env fn_id (TypQ_aux (tq,_)) pat set_assertions =
        (match KBindings.find kid set_assertions with
        | (l,is) ->
           let l' = Generated l in
-          let pats = List.map (fun n -> P_aux (P_lit (L_aux (L_num n,l')),(l',None))) is in
-          let pats = pats @ [P_aux (P_wild,(l',None))] in
+          let pats = List.map (fun n -> P_aux (P_lit (L_aux (L_num n,l')),(l',snd annot))) is in
+          let pats = pats @ [P_aux (P_wild,(l',snd annot))] in
           Partial (pats,l)
        | exception Not_found -> Total)
     | _ -> Total
-- 
cgit v1.2.3


From 41f4066a2eb5798b546499ade9712792b096b85c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 26 Jan 2018 17:18:41 +0000
Subject: Add replacement of complex nexp sizes by equivalent variables in mono

---
 src/monomorphise.ml | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 59052c24..cd2c419f 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -2227,6 +2227,7 @@ let merge rs rs' = {
 }
 
 type env = {
+  top_kids : kid list;
   var_deps : dependencies Bindings.t;
   kid_deps : dependencies KBindings.t
 }
@@ -2249,7 +2250,7 @@ let update_env env deps pat =
   let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in
   let kbound = kids_bound_by_pat pat in
   let kid_deps = KidSet.fold (fun v ds -> KBindings.add v deps ds) kbound env.kid_deps in
-  { var_deps = var_deps; kid_deps = kid_deps }
+  { env with var_deps = var_deps; kid_deps = kid_deps }
 
 let assigned_vars_exps es =
   List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp))
@@ -2385,6 +2386,18 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps =
      | None -> None)
   | _ -> None
 
+let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) =
+  let is_equal kid =
+    prove typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown))
+  in
+  match ne with
+  | Nexp_var _
+  | Nexp_constant _ -> nexp
+  | _ ->
+     match List.find is_equal env.top_kids with
+     | kid -> Nexp_aux (Nexp_var kid,Generated l)
+     | exception Not_found -> nexp
+
 (* Takes an environment of dependencies on vars, type vars, and flow control,
    and dependencies on mutable variables.  The latter are quite conservative,
    we currently drop variables assigned inside loops, for example. *)
@@ -2601,6 +2614,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
        let typ = Env.expand_synonyms tenv typ in
        if is_bitvector_typ typ then
          let _,size,_,_ = vector_typ_args_of typ in
+         let size = simplify_size_nexp env tenv size in
          match deps_of_nexp env.kid_deps [] size with
          | Have (args,caller,caller_kids) ->
             { r with
@@ -2737,7 +2751,8 @@ let initial_env fn_id (TypQ_aux (tq,_)) pat set_assertions =
   let _,var_deps,kid_deps = split3 (List.mapi arg pats) in
   let var_deps = List.fold_left dep_bindings_merge Bindings.empty var_deps in
   let kid_deps = List.fold_left dep_kbindings_merge kid_quant_deps kid_deps in
-  { var_deps = var_deps; kid_deps = kid_deps }
+  let top_kids = List.map fst (KBindings.bindings kid_quant_deps) in
+  { top_kids = top_kids; var_deps = var_deps; kid_deps = kid_deps }
 
 (* When there's more than one pick the first *)
 let merge_set_asserts _ x y =
-- 
cgit v1.2.3


From 36e95d3af78bf8b6e11b1939e605a735285e3183 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 26 Jan 2018 17:22:12 +0000
Subject: Missing -ocamlfind

---
 src/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Makefile b/src/Makefile
index 325cbec6..85c5abba 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -270,4 +270,4 @@ doc:
 	ocamlbuild -use-ocamlfind sail.docdir/index.html
 
 lib:
-	ocamlbuild pretty_print.cmxa pretty_print.cma
+	ocamlbuild -use-ocamlfind pretty_print.cmxa pretty_print.cma
-- 
cgit v1.2.3


From 481f492ecc3179f5ea8293dab45c3712871c219e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 26 Jan 2018 17:52:16 +0000
Subject: One more mono rewrite

---
 lib/mono_rewrites.sail | 7 +++++++
 src/monomorphise.ml    | 4 ++++
 2 files changed, 11 insertions(+)

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/src/monomorphise.ml b/src/monomorphise.ml
index cd2c419f..745b40e4 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3075,6 +3075,10 @@ let rewrite_app env typ (id,args) =
         when is_slice slice1 && not (is_constant length1) ->
        E_app (mk_id "zext_slice", [vector1; start1; length1])
 
+    | [E_aux (E_app (ones, [len1]),_);
+       _ (* unnecessary ZeroExtend length *)] ->
+       E_app (mk_id "zext_ones", [len1])
+
     | _ -> E_app (id,args)
 
   else if is_id env (Id "SignExtend") id then
-- 
cgit v1.2.3


From 3ea0add3e9b0e6c5ba9c74d533d7c44874d95beb Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 26 Jan 2018 22:53:22 +0000
Subject: Fixed loading ARM elf files

Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib
---
 aarch64/main.sail    | 16 +++++++++-------
 aarch64/prelude.sail | 31 ++++---------------------------
 lib/elf.sail         |  8 ++++++++
 lib/flow.sail        | 42 ++++++++++++++++++++++++++++++++++++++++++
 lib/smt.sail         | 30 ++++++++++++++++++++++++++++++
 src/elf_loader.ml    |  6 +++---
 6 files changed, 96 insertions(+), 37 deletions(-)
 create mode 100644 lib/elf.sail
 create mode 100644 lib/flow.sail
 create mode 100644 lib/smt.sail

diff --git a/aarch64/main.sail b/aarch64/main.sail
index b48f84d9..eaaf4f7f 100644
--- a/aarch64/main.sail
+++ b/aarch64/main.sail
@@ -1,12 +1,14 @@
-val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+$include <elf.sail>
 
-function fetch_and_execute () = while true do {
-  let instr = aget_Mem(_PC, 4, AccType_IFETCH);
-  decode(instr);
-  if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
-}
+// Simple top level fetch and execute loop.
+val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
+function fetch_and_execute () =
+  while true do {
+    let instr = aget_Mem(_PC, 4, AccType_IFETCH);
+    decode(instr);
+    if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
+  }
 
 val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index da98b495..ab916e27 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -1,25 +1,12 @@
 default Order dec
 
+$include <smt.sail>
+$include <flow.sail>
+
 type bits ('n : Int) = vector('n, dec, bit)
 
 infix 4 ==
 
-val div = {
-  smt : "div",
-  lem : "integerDiv"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm))
-
-val mod = {
-  smt : "mod",
-  lem : "integerMod"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm))
-
-val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-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 eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
 
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
@@ -86,16 +73,10 @@ val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('
 
 overload append = {bitvector_concat, vector_concat}
 
-val not_bool = "not" : bool -> bool
-
 val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
 
-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 neq_int = {lem: "neq"} : (int, int) -> bool
 
 function neq_int (x, y) = not_bool(eq_int(x, y))
@@ -110,8 +91,6 @@ function neq_anything (x, y) = not_bool(x == y)
 
 overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
-val and_bool = "and_bool" : (bool, bool) -> bool
-
 val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -120,8 +99,6 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
 overload operator & = {and_bool, and_vec}
 
-val or_bool = "or_bool" : (bool, bool) -> bool
-
 val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -263,7 +240,7 @@ val abs_int = "abs_int" : int -> int
 
 val abs_real = "abs_real" : real -> real
 
-overload abs = {abs_int, abs_real}
+overload abs = {abs, abs_int, abs_real}
 
 val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
 
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
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index feacdf3d..83c36821 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -118,9 +118,9 @@ let load_segment seg =
 let load_elf name =
   let segments, e_entry, symbol_map = read name in
   opt_elf_entry := e_entry;
-  if List.mem_assoc "tohost" symbol_map then
-    let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
-    opt_elf_tohost := tohost_addr;
+  (if List.mem_assoc "tohost" symbol_map then
+     let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
+     opt_elf_tohost := tohost_addr);
   List.iter load_segment segments
 
 (* The sail model can access this by externing a unit -> int function
-- 
cgit v1.2.3


From f6b35a7dba6acad62afb9d481e2bf2dfdbc312b4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 27 Jan 2018 11:41:26 +0000
Subject: Add Makefile for RISC-V

---
 riscv/Makefile | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 riscv/Makefile

diff --git a/riscv/Makefile b/riscv/Makefile
new file mode 100644
index 00000000..fabaaafc
--- /dev/null
+++ b/riscv/Makefile
@@ -0,0 +1,24 @@
+SAIL_SRCS = prelude.sail riscv_types.sail riscv.sail
+SAIL_DIR ?= $(realpath ..)
+
+export SAIL_DIR
+
+all: riscv Riscv_embed_sequential.thy
+
+riscv: $(SAIL_SRCS) main.sail
+	$(SAIL_DIR)/sail -ocaml -o riscv $^
+
+Riscv_embed_sequential.thy: riscv_embed_sequential.lem riscv_extras_embed_sequential.lem
+	lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
+		riscv_extras_embed_sequential.lem \
+		riscv_embed_types_sequential.lem \
+		riscv_embed_sequential.lem
+
+riscv_embed_sequential.lem: $(SAIL_SRCS)
+	$(SAIL_DIR)/sail -lem -o riscv -lem_sequential -lem_mwords -lem_lib Riscv_extras_embed $^
+
+clean:
+	-rm -rf riscv _sbuild
+	-rm -f riscv_embed_sequential.lem riscv_embed_types_sequential.lem
+	-rm -f Riscv_embed_sequential.thy Riscv_embed_types_sequential.thy \
+		Riscv_extras_embed_sequential.thy
-- 
cgit v1.2.3


From 4e4420f00984c11782445210709e665370e99358 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 29 Jan 2018 09:00:26 +0000
Subject: Avoid generating (_ as n) in mono, broke atom type rewriting

---
 src/monomorphise.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 745b40e4..d911e537 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1509,7 +1509,11 @@ let split_defs continue_anyway splits defs =
                    p,[id,E_aux (E_lit lit,(Generated pl,pannot))],[l,(i,[])]
                 | _ ->
                    let p',subst = freshen_pat_bindings p in
-                   P_aux (P_as (p',id),(l,annot)),[],[l,(i,subst)])
+                   match p' with
+                   | P_aux (P_wild,_) ->
+                      P_aux (P_id id,(l,annot)),[],[l,(i,subst)]
+                   | _ ->
+                      P_aux (P_as (p',id),(l,annot)),[],[l,(i,subst)])
                       pats)
            )
         | P_app (id,ps) ->
-- 
cgit v1.2.3


From 3adfbd69df79862bb9ac8b57f4777a30dac24ff3 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 29 Jan 2018 09:18:08 +0000
Subject: Turn off warnings when rechecking after mono

---
 src/monomorphise.ml  | 27 +++++++++++++++++++--------
 src/monomorphise.mli |  5 +++--
 src/process_file.ml  |  8 +++-----
 3 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d911e537..5177a1a1 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3123,15 +3123,23 @@ type options = {
   debug_analysis : int;
   rewrites : bool;
   rewrite_size_parameters : bool;
-  all_split_errors : bool
+  all_split_errors : bool;
+  dump_raw: bool
 }
 
+let recheck defs =
+  let w = !Util.opt_warnings in
+  let () = Util.opt_warnings := false in
+  let r = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
+  let () = Util.opt_warnings := w in
+  r
+
 let monomorphise opts splits env defs =
   let (defs,env) =
     if opts.rewrites then
       let defs = MonoRewrites.mono_rewrite defs in
     (* TODO: is this necessary? *)
-      Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs
+      recheck defs
     else (defs,env)
   in
 (*let _ = Pretty_print.pp_defs stdout defs in*)
@@ -3145,9 +3153,12 @@ let monomorphise opts splits env defs =
   (* TODO: currently doing this because constant propagation leaves numeric literals as
      int, try to avoid this later; also use final env for DEF_spec case above, because the
      type checker doesn't store the env at that point :( *)
-  if opts.rewrite_size_parameters then
-    let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
-    let defs = AtomToItself.rewrite_size_parameters env defs in
-    defs
-  else
-    defs
+  let defs = if opts.rewrite_size_parameters then
+      let (defs,env) = recheck defs in
+      let defs = AtomToItself.rewrite_size_parameters env defs in
+      defs
+    else
+      defs
+  in
+  let () = if opts.dump_raw then Pretty_print_sail.pp_defs stdout defs else () in
+  recheck defs
diff --git a/src/monomorphise.mli b/src/monomorphise.mli
index 8e0c1ede..11713511 100644
--- a/src/monomorphise.mli
+++ b/src/monomorphise.mli
@@ -53,7 +53,8 @@ type options = {
   debug_analysis : int;           (* Debug output level for the automatic analysis *)
   rewrites : bool;                (* Experimental rewrites for variable-sized operations *)
   rewrite_size_parameters : bool; (* Make implicit type parameters explicit for (e.g.) lem *)
-  all_split_errors : bool
+  all_split_errors : bool;
+  dump_raw: bool
 }
 
 val monomorphise :
@@ -61,4 +62,4 @@ val monomorphise :
   ((string * int) * string) list -> (* List of splits from the command line *)
   Type_check.Env.t ->
   Type_check.tannot Ast.defs ->
-  Type_check.tannot Ast.defs
+  Type_check.tannot Ast.defs * Type_check.Env.t
diff --git a/src/process_file.ml b/src/process_file.ml
index cb8c8011..1ba8069f 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -196,12 +196,10 @@ let monomorphise_ast locs type_env ast =
     debug_analysis = !opt_dmono_analysis;
     rewrites = !opt_mono_rewrites;
     rewrite_size_parameters = !Pretty_print_lem.opt_mwords;
-    all_split_errors = !opt_dall_split_errors
+    all_split_errors = !opt_dall_split_errors;
+    dump_raw = !opt_ddump_raw_mono_ast
   } in
-  let ast = monomorphise opts locs type_env ast in
-  let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail.pp_defs stdout ast else () in
-  let ienv = Type_check.Env.no_casts Type_check.initial_env in
-  Type_check.check ienv ast
+  monomorphise opts locs type_env ast
 
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
-- 
cgit v1.2.3


From cb0a994d5156b5765712ff90b28105e2ba7dcd04 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 29 Jan 2018 11:23:00 +0000
Subject: Use fresh variables when dealing with (multiple) literal patterns

---
 src/type_check.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/type_check.ml b/src/type_check.ml
index 41438592..a49807ce 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2020,6 +2020,12 @@ let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -
 let strip_pexp : 'a pexp -> unit pexp = function pexp -> map_pexp_annot (fun (l, _) -> (l, ())) pexp
 let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp
 
+let fresh_var =
+  let counter = ref 0 in
+  fun () -> let n = !counter in
+            let () = counter := n+1 in
+            mk_id ("v#" ^ string_of_int n)
+
 let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
   let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
   let add_effect exp eff = match exp with
@@ -2470,8 +2476,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
      | exception (Type_error _ as typ_exn) ->
         match pat_aux with
         | P_lit lit ->
-           let guard = mk_exp (E_app_infix (mk_exp (E_id (mk_id "p#")), mk_id "==", mk_exp (E_lit lit))) in
-           let (typed_pat, env, guards) = bind_pat env (mk_pat (P_id (mk_id "p#"))) typ in
+           let var = fresh_var () in
+           let guard = mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit))) in
+           let (typed_pat, env, guards) = bind_pat env (mk_pat (P_id var)) typ in
            typed_pat, env, guard::guards
         | _ -> raise typ_exn
 
-- 
cgit v1.2.3


From 8475527be0c7cf6d4412c432d3c63cfba38176a7 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 29 Jan 2018 11:23:56 +0000
Subject: Turn off constraint substitution in mono (Type checker doesn't seem
 to use false aggressively enough for this)

---
 src/monomorphise.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 5177a1a1..0baaf139 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -899,7 +899,8 @@ let rec freshen_pat_bindings p =
 (* Use the location pairs in choices to reduce case expressions at the first
    location to the given case at the second. *)
 let apply_pat_choices choices =
-  let rewrite_constraint (NC_aux (nc,l) as nconstr) =
+  let rewrite_constraint (NC_aux (nc,l) as nconstr) = E_constraint nconstr (*
+    Not right now - false cases may not type check
     match List.assoc l choices with
     | choice,_ -> begin
        match nc with
@@ -907,7 +908,7 @@ let apply_pat_choices choices =
           E_constraint (NC_aux ((if choice < List.length is then NC_true else NC_false), Generated l))
        | _ -> E_constraint nconstr
     end
-    | exception Not_found -> E_constraint nconstr
+    | exception Not_found -> E_constraint nconstr*)
   in
   let rewrite_case (e,cases) =
     match List.assoc (exp_loc e) choices with
-- 
cgit v1.2.3


From 605c4f71d0549fcbe1b9ccbb517fcd162bfd0c06 Mon Sep 17 00:00:00 2001
From: Shaked Flur
Date: Mon, 29 Jan 2018 13:07:34 +0000
Subject: Linksem does not use uint anymore

---
 src/lem_interp/run_with_elf.ml          | 2 +-
 src/lem_interp/run_with_elf_cheri.ml    | 2 +-
 src/lem_interp/run_with_elf_cheri128.ml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 8533827b..bb56c8a9 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -727,7 +727,7 @@ let initial_system_state_of_elf_file name =
            aarch64_register_data_all) *)
         | 8 (* EM_MIPS *) ->
           let startaddr =
-            let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+            let e_entry = Uint64_wrapper.of_bigint e_entry in
             match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
             | Error.Fail s -> failwith "Failed computing entry point"
             | Error.Success s -> s
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 46bc92fb..3d187aa9 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
         match Nat_big_num.to_int e_machine with
         | 8 (* EM_MIPS *) ->
           let startaddr =
-            let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+            let e_entry = Uint64_wrapper.of_bigint e_entry in
             match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
             | Error.Fail s -> failwith "Failed computing entry point"
             | Error.Success s -> s
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 5e5bee21..6b12ebbb 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
         match Nat_big_num.to_int e_machine with
         | 8 (* EM_MIPS *) ->
           let startaddr =
-            let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+            let e_entry = Uint64_wrapper.of_bigint e_entry in
             match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
             | Error.Fail s -> failwith "Failed computing entry point"
             | Error.Success s -> s
-- 
cgit v1.2.3


From 36f086ce2b3506e2a81ef77ad03f3b339b8f0518 Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Mon, 29 Jan 2018 13:18:14 +0000
Subject: Shaked removing generation of now-uncessary uint dependency

---
 lib/_tags | 4 ++--
 1 file changed, 2 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
-- 
cgit v1.2.3