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(-)

(limited to 'src')

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(-)

(limited to 'src')

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(-)

(limited to 'src')

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

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

(limited to 'src')

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
---
 src/elf_loader.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src')

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 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(-)

(limited to 'src')

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(-)

(limited to 'src')

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(-)

(limited to 'src')

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(-)

(limited to 'src')

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(-)

(limited to 'src')

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