From 668ae1bc10fc1d9ea4d62ae0a2708a52cd83e211 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 21 Jun 2018 03:19:11 +0100
Subject: Constant folding improvements

---
 src/constant_fold.ml | 101 ++++++++++++++++++++++++++++++++++++++-------------
 src/interpreter.ml   |   2 -
 src/process_file.ml  |   2 +-
 src/type_check.ml    |  17 ---------
 src/value2.lem       |  20 ++++------
 5 files changed, 84 insertions(+), 58 deletions(-)

(limited to 'src')

diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 7a35226e..45d3efe0 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -59,10 +59,25 @@ module StringMap = Map.Make(String);;
    false = no folding, true = perform constant folding. *)
 let optimize_constant_fold = ref false
 
-let exp_of_value =
+let rec fexp_of_ctor (field, value) =
+  FE_aux (FE_Fexp (mk_id field, exp_of_value value), no_annot)
+  
+and exp_of_value =
   let open Value in
   function
   | V_int n -> mk_lit_exp (L_num n)
+  | V_bit Sail_lib.B0 -> mk_lit_exp L_zero
+  | V_bit Sail_lib.B1 -> mk_lit_exp L_one
+  | V_bool true -> mk_lit_exp L_true
+  | V_bool false -> mk_lit_exp L_false
+  | V_string str -> mk_lit_exp (L_string str)
+  | V_record ctors ->
+     mk_exp (E_record (FES_aux (FES_Fexps (List.map fexp_of_ctor (StringMap.bindings ctors), false), no_annot)))
+  | V_vector vs ->
+     mk_exp (E_vector (List.map exp_of_value vs))
+  | V_tuple vs ->
+     mk_exp (E_tuple (List.map exp_of_value vs))
+  | V_unit -> mk_lit_exp L_unit
   | _ -> failwith "No expression for value"
 
 (* We want to avoid evaluating things like print statements at compile
@@ -85,15 +100,23 @@ let safe_primops =
       "Elf_loader.elf_tohost"
     ]
 
-let is_literal = function
-  | E_aux (E_lit _, _) -> true
+let rec is_constant (E_aux (e_aux, _)) =
+  match e_aux with
+  | E_lit _ -> true
+  | E_vector exps -> List.for_all is_constant exps
+  | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> List.for_all is_constant_fexp fexps
+  | E_cast (_, exp) -> is_constant exp
+  | E_tuple exps -> List.for_all is_constant exps
   | _ -> false
 
+and is_constant_fexp (FE_aux (FE_Fexp (_, exp), _)) = is_constant exp
+
 (* Wrapper around interpreter that repeatedly steps until done. *)
 let rec run ast frame =
   match frame with
   | Interpreter.Done (state, v) -> v
-  | Interpreter.Step _ ->
+  | Interpreter.Step (lazy_str, _, _, _) ->
+     prerr_endline (Lazy.force lazy_str);
      run ast (Interpreter.eval_frame ast frame)
   | Interpreter.Break frame ->
      run ast (Interpreter.eval_frame ast frame)
@@ -115,35 +138,57 @@ let rec run ast frame =
    - Throws an exception that isn't caught.
  *)
 
-let rewrite_constant_function_calls' ast =
+let rec rewrite_constant_function_calls' ast =
+  let rewrite_count = ref 0 in
+  let ok () = incr rewrite_count in
+  let not_ok () = decr rewrite_count in
+  
   let lstate, gstate =
     Interpreter.initial_state ast safe_primops
   in
   let gstate = { gstate with Interpreter.allow_registers = false } in
 
+  let evaluate e_aux annot =
+    let initial_monad = Interpreter.return (E_aux (e_aux, annot)) in
+    try
+      begin
+        let v = run ast (Interpreter.Step (lazy "", (lstate, gstate), initial_monad, [])) in
+        let exp = exp_of_value v in
+        try (ok (); Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)) with
+        | Type_error (l, err) ->
+           (* A type error here would be unexpected, so don't ignore it! *)
+           Util.warn ("Type error when folding constants in "
+                      ^ string_of_exp (E_aux (e_aux, annot))
+                      ^ "\n" ^ Type_error.string_of_type_error err);
+           not_ok ();
+           E_aux (e_aux, annot)
+      end
+    with
+    (* Otherwise if anything goes wrong when trying to constant
+       fold, just continue without optimising. *)
+    | _ -> E_aux (e_aux, annot)
+  in
+    
   let rw_funcall e_aux annot =
     match e_aux with
-    | E_app (id, args) when List.for_all is_literal args ->
-       begin
-         let initial_monad = Interpreter.return (E_aux (e_aux, annot)) in
-         try
-           begin
-             let v = run ast (Interpreter.Step (lazy "", (lstate, gstate), initial_monad, [])) in
-             let exp = exp_of_value v in
-             try Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot) with
-             | Type_error (l, err) ->
-                (* A type error here would be unexpected, so don't ignore it! *)
-                Util.warn ("Type error when folding constants in "
-                           ^ string_of_exp (E_aux (e_aux, annot))
-                           ^ "\n" ^ Type_error.string_of_type_error err);
-                E_aux (e_aux, annot)
-           end
-         with
-         (* Otherwise if anything goes wrong when trying to constant
-            fold, just continue without optimising. *)
-         | _ -> E_aux (e_aux, annot)
-       end
+    | E_app (id, args) when List.for_all is_constant args ->
+       evaluate e_aux annot
+
+    | E_field (exp, id) when is_constant exp ->
+       evaluate e_aux annot      
+
+    | E_if (E_aux (E_lit (L_aux (L_true, _)), _), then_exp, _) -> ok (); then_exp
+    | E_if (E_aux (E_lit (L_aux (L_false, _)), _), _, else_exp) -> ok (); else_exp
+
+    | E_let (LB_aux (LB_val (P_aux (P_id id, _), bind), _), exp) when is_constant bind ->
+       ok ();
+       subst id bind exp
 
+    | E_let (LB_aux (LB_val (P_aux (P_typ (typ, P_aux (P_id id, _)), annot), bind), _), exp)
+         when is_constant bind ->
+       ok ();
+       subst id (E_aux (E_cast (typ, bind), annot)) exp
+       
     | _ -> E_aux (e_aux, annot)
   in
   let rw_exp = {
@@ -151,7 +196,11 @@ let rewrite_constant_function_calls' ast =
       e_aux = (fun (e_aux, annot) -> rw_funcall e_aux annot)
     } in
   let rw_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) } in
-  rewrite_defs_base rw_defs ast
+  let ast = rewrite_defs_base rw_defs ast in
+  (* We keep iterating until we have no more re-writes to do *)
+  if !rewrite_count > 0
+  then rewrite_constant_function_calls' ast
+  else ast
 
 let rewrite_constant_function_calls ast =
   if !optimize_constant_fold then
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 00846d73..99d5889a 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -232,7 +232,6 @@ let is_value_fexp (FE_aux (FE_Fexp (id, exp), _)) = is_value exp
 let value_of_fexp (FE_aux (FE_Fexp (id, exp), _)) = (string_of_id id, value_of_exp exp)
 
 let rec build_letchain id lbs (E_aux (_, annot) as exp) =
-  (* print_endline ("LETCHAIN " ^ string_of_exp exp); *)
   match lbs with
   | [] -> exp
   | lb :: lbs when IdSet.mem id (letbind_pat_ids lb)->
@@ -311,7 +310,6 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      else
        failwith "Match failure"
 
-
   | E_vector_subrange (vec, n, m) ->
      wrap (E_app (mk_id "vector_subrange_dec", [vec; n; m]))
   | E_vector_access (vec, n) ->
diff --git a/src/process_file.ml b/src/process_file.ml
index 9603e986..9ed52e8d 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -403,7 +403,7 @@ let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
 let rewrite_ast_c ast =
   ast
   |> rewrite Rewrites.rewrite_defs_c
-  |> Constant_fold.rewrite_constant_function_calls
+  |> rewrite [("constant_fold", Constant_fold.rewrite_constant_function_calls)]
 
 let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter
 let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check
diff --git a/src/type_check.ml b/src/type_check.ml
index 0a29b6d6..afdf41c9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -132,28 +132,11 @@ let is_unknown_type = function
   | (Typ_aux (Typ_internal_unknown, _)) -> true
   | _ -> false
 
-(* An index_sort is a more general form of range type: it can either
-   be IS_int, which represents every natural number, or some set of
-   natural numbers given by an IS_prop expression of the form
-   {'n. f('n) <= g('n) /\ ...} *)
-type index_sort =
-  | IS_int
-  | IS_prop of kid * (nexp * nexp) list
-
-let string_of_index_sort = function
-  | IS_int -> "INT"
-  | IS_prop (kid, constraints) ->
-     "{" ^ string_of_kid kid ^ " | "
-     ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints
-     ^ "}"
-
 let is_atom (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_app (f, [_]) when string_of_id f = "atom" -> true
   | _ -> false
 
-
-
 let rec strip_id = function
   | Id_aux (Id x, _) -> Id_aux (Id x, Parse_ast.Unknown)
   | Id_aux (DeIid x, _) -> Id_aux (DeIid x, Parse_ast.Unknown)
diff --git a/src/value2.lem b/src/value2.lem
index 33416503..d9fd1263 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -70,17 +70,13 @@ type vl =
   | V_record of list (string * vl)
   | V_null (* Used for unitialized values and null pointers in C compilation *)
 
-let primops extern args =
-  match (extern, args) with
-  | ("and_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 && b2)
-  | ("and_bool", [V_nondet; V_bool false]) -> V_bool false
-  | ("and_bool", [V_bool false; V_nondet]) -> V_bool false
-  | ("and_bool", _) -> V_nondet
 
-  | ("or_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 || b2)
-  | ("or_bool", [V_nondet; V_bool true]) -> V_bool true
-  | ("or_bool", [V_bool true; V_nondet]) -> V_bool true
-  | ("or_bool", _) -> V_nondet
+let value_int_op_int op = function
+  | [V_int v1; V_int v2] -> V_int (op v1 v2)
+  | _ -> V_null
+end
 
-  | _ -> failwith ("Unimplemented primitive operation " ^ extern)
-  end
+let value_bool_op_int op = function
+  | [V_int v1; V_int v2] -> V_bool (op v1 v2)
+  | _ -> V_null
+end
-- 
cgit v1.2.3


From e0059c15e282c98bc227962a1df6ae0ad34de477 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 2 Jul 2018 13:00:58 +0100
Subject: Work around Coq issue with pattern binders

---
 src/pretty_print_coq.ml | 51 +++++++++++++++++++++++++++++++++----------------
 1 file changed, 35 insertions(+), 16 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index ffe376e0..8d9dd881 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -537,9 +537,9 @@ let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) =
 let doc_typquant_items_separate ctx delimit (TypQ_aux (tq,_)) =
   match tq with
   | TypQ_tq qis ->
-     separate_opt space (doc_quant_item_id ctx delimit) qis,
-     separate_opt space (doc_quant_item_constr ctx delimit) qis
-  | TypQ_no_forall -> empty, empty
+     Util.map_filter (doc_quant_item_id ctx delimit) qis,
+     Util.map_filter (doc_quant_item_constr ctx delimit) qis
+  | TypQ_no_forall -> [], []
 
 let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with
 | TypQ_tq ((_ :: _) as qs) ->
@@ -1485,14 +1485,6 @@ let merge_kids_atoms pats =
   let gone,map,_ = List.fold_left try_eliminate (KidSet.empty, KBindings.empty, KidSet.empty) pats in
   gone,map
 
-let doc_binder ctxt (P_aux (p,ann) as pat, typ) =
-  let env = env_of_annot ann in
-  let exp_typ = Env.expand_synonyms env typ in
-  match p with
-  | P_id id
-  | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) ->
-     parens (separate space [doc_id id; colon; doc_typ ctxt typ])
-  | _ -> squote ^^ parens (separate space [doc_pat ctxt true (pat, exp_typ); colon; doc_typ ctxt typ])
 
 let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in
@@ -1516,22 +1508,48 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
      been replaced by one of the term-level arguments is bound. *)
   let quantspp, constrspp = doc_typquant_items_separate ctxt braces tq in
   let exp = List.fold_left (fun body f -> f body) (bind exp) binds in
-  let patspp = separate_map space (doc_binder ctxt) pats in
-  let atom_constr_pp = separate_opt space (atom_constraint ctxt) pats in
+  let used_a_pattern = ref false in
+  let doc_binder (P_aux (p,ann) as pat, typ) =
+    let env = env_of_annot ann in
+    let exp_typ = Env.expand_synonyms env typ in
+    match p with
+    | P_id id
+    | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) ->
+       parens (separate space [doc_id id; colon; doc_typ ctxt typ])
+    | _ ->
+       (used_a_pattern := true;
+        squote ^^ parens (separate space [doc_pat ctxt true (pat, exp_typ); colon; doc_typ ctxt typ]))
+  in
+  let patspp = separate_map space doc_binder pats in
+  let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in
+  let atom_constr_pp = separate space atom_constrs in
   let retpp =
     if effectful eff
     then string "M" ^^ space ^^ parens (doc_typ ctxt ret_typ)
     else doc_typ ctxt ret_typ
   in
+  let idpp = doc_id id in
+  (* Work around Coq bug 7975 about pattern binders followed by implicit arguments *)
+  let implicitargs =
+    if !used_a_pattern && List.length constrspp + List.length atom_constrs > 0 then
+      separate space
+        ([string "Arguments"; idpp;] @
+            List.map (fun _ -> string "{_}") quantspp @
+            List.map (fun _ -> string "_") pats @
+            List.map (fun _ -> string "{_}") constrspp @
+            List.map (fun _ -> string "{_}") atom_constrs)
+      ^^ dot
+    else empty
+  in
   let _ = match guard with
     | None -> ()
     | _ ->
        raise (Reporting_basic.err_unreachable l
                 "guarded pattern expression should have been rewritten before pretty-printing") in
   group (prefix 3 1
-    (separate space [doc_id id; quantspp; patspp; constrspp; atom_constr_pp] ^/^
+    (separate space ([idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp]) ^/^
        colon ^^ space ^^ retpp ^^ coloneq)
-    (doc_fun_body ctxt exp ^^ dot))
+    (doc_fun_body ctxt exp ^^ dot)) ^/^ implicitargs
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -1660,7 +1678,8 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
      let arg_typs_pp = separate space (List.map doc_typ' typs) in
      let ret_typ_pp = doc_typ empty_ctxt ret_ty in
      let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in
-     string "forall" ^/^ tyvars_pp ^/^ arg_typs_pp ^/^ constrs_pp ^^ comma ^/^ ret_typ_pp
+     string "forall" ^/^ separate space tyvars_pp ^/^
+       arg_typs_pp ^/^ separate space constrs_pp ^^ comma ^/^ ret_typ_pp
   | _ -> doc_typschm empty_ctxt true ts
 
 let doc_val_spec unimplemented (VS_aux (VS_val_spec(tys,id,_,_),ann)) =
-- 
cgit v1.2.3


From 02923ba7a62b7b383a02fb04c40be31ffbdb75a4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 2 Jul 2018 17:18:48 +0100
Subject: Coq: multiple record field updates Uses simple method of printing the
 entire record, in lieu of any decent record update syntax.

---
 src/pretty_print_coq.ml | 26 +++++++++++++++++++++++---
 src/type_check.ml       |  3 +++
 src/type_check.mli      |  3 +++
 3 files changed, 29 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 8d9dd881..6d9cbfc1 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1048,13 +1048,33 @@ let doc_exp_lem, doc_let_lem =
                                           (doc_fexp ctxt recordtyp) fexps)) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-       let recordtyp = match annot with
+       let recordtyp, env = match annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _)
            when Env.is_record tid env ->
-           tid
+           tid, env
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
-       enclose_record_update (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps))
+       if List.length fexps > 1 then
+         let _,fields = Env.get_record recordtyp env in
+         let var, let_pp =
+           match e with
+           | E_aux (E_id id,_) -> id, empty
+           | _ -> let v = mk_id "_record" in (* TODO: collision avoid *)
+                  v, separate space [string "let "; doc_id v; coloneq; top_exp ctxt true e; string "in"] ^^ break 1
+         in
+         let doc_field (_,id) =
+           match List.find (fun (FE_aux (FE_Fexp (id',_),_)) -> Id.compare id id' == 0) fexps with
+           | fexp -> doc_fexp ctxt recordtyp fexp
+           | exception Not_found ->
+               let fname =
+                 if prefix_recordtype && string_of_id recordtyp <> "regstate"
+                 then (string (string_of_id recordtyp ^ "_")) ^^ doc_id id
+                 else doc_id id in
+               doc_op coloneq fname (doc_id var ^^ dot ^^ parens fname)
+         in let_pp ^^ enclose_record (align (separate_map (semi_sp ^^ break 1)
+                                               doc_field fields))
+       else
+         enclose_record_update (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let start, (len, order, etyp) =
diff --git a/src/type_check.ml b/src/type_check.ml
index afdf41c9..db85bf33 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -355,6 +355,7 @@ module Env : sig
   val is_mapping : id -> t -> bool
   val add_record : id -> typquant -> (typ * id) list -> t -> t
   val is_record : id -> t -> bool
+  val get_record : id -> t -> typquant * (typ * id) list
   val get_accessor_fn : id -> id -> t -> typquant * typ
   val get_accessor : id -> id -> t -> typquant * typ * typ * effect
   val add_local : id -> mut * typ -> t -> t
@@ -917,6 +918,8 @@ end = struct
 
   let is_record id env = Bindings.mem id env.records
 
+  let get_record id env = Bindings.find id env.records
+
   let add_record id typq fields env =
     if bound_typ_id env id
     then typ_error (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound")
diff --git a/src/type_check.mli b/src/type_check.mli
index 4f87e4e6..fd1ddb92 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -136,6 +136,9 @@ module Env : sig
 
   val is_record : id -> t -> bool
 
+  (** Returns record quantifiers and fields *)
+  val get_record : id -> t -> typquant * (typ * id) list
+
   (** Return type is: quantifier, argument type, return type, effect *)
   val get_accessor : id -> id -> t -> typquant * typ * typ * effect
 
-- 
cgit v1.2.3


From 1f323e30d1e476e234ccfdaff9f9583d714e8854 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 2 Jul 2018 17:56:39 +0100
Subject: Coq: tidy up a bit of printing

---
 src/pretty_print_coq.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 6d9cbfc1..78507577 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1552,7 +1552,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   (* Work around Coq bug 7975 about pattern binders followed by implicit arguments *)
   let implicitargs =
     if !used_a_pattern && List.length constrspp + List.length atom_constrs > 0 then
-      separate space
+      break 1 ^^ separate space
         ([string "Arguments"; idpp;] @
             List.map (fun _ -> string "{_}") quantspp @
             List.map (fun _ -> string "_") pats @
@@ -1568,8 +1568,8 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
                 "guarded pattern expression should have been rewritten before pretty-printing") in
   group (prefix 3 1
     (separate space ([idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp]) ^/^
-       colon ^^ space ^^ retpp ^^ coloneq)
-    (doc_fun_body ctxt exp ^^ dot)) ^/^ implicitargs
+       separate space [colon; retpp; coloneq])
+    (doc_fun_body ctxt exp ^^ dot)) ^^ implicitargs
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
-- 
cgit v1.2.3


From e4101799eebec8a13c8bb4588c8f7d9663858902 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 2 Jul 2018 18:56:14 +0100
Subject: Fix get_recursive_functions to not only pick up non-mutually
 recursive functions

The code to do this is rather ugly. It would be nice to have a generic
callgraph representation we could just query and not use the rewriter
in a weird way to extract this info.
---
 src/c_backend.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index d18ca354..8a41df67 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2684,6 +2684,26 @@ let rec get_recursive_functions (Defs defs) =
   match defs with
   | DEF_internal_mutrec fundefs :: defs ->
      IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs))
+
+  | (DEF_fundef fdef as def) :: defs ->
+     let open Rewriter in
+     let ids = ref IdSet.empty in
+     let collect_funcalls e_aux annot =
+       match e_aux with
+       | E_app (id, args) -> (ids := IdSet.add id !ids; E_aux (e_aux, annot))
+       | _ -> E_aux (e_aux, annot)
+     in
+     let map_exp = {
+         id_exp_alg with
+         e_aux = (fun (e_aux, annot) -> collect_funcalls e_aux annot)
+       } in
+     let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in
+     let _ = rewrite_def map_defs def in
+     if IdSet.mem (id_of_fundef fdef) !ids then
+       IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs))
+     else
+       get_recursive_functions (Defs defs)
+
   | _ :: defs -> get_recursive_functions (Defs defs)
   | [] -> IdSet.empty
 
-- 
cgit v1.2.3


From c369d0897230bec405fc6cce7144d4f9f2956ed6 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 3 Jul 2018 14:19:48 +0100
Subject: Fix letbind_effects on LEXP_deref with an effectful subexpression

---
 src/rewrites.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 214ca571..c2bf0835 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2606,7 +2606,7 @@ let rewrite_defs_letbind_effects =
     match lexp_aux with
     | LEXP_id _ -> k lexp
     | LEXP_deref exp ->
-       n_exp exp (fun exp ->
+       n_exp_name exp (fun exp ->
        k (fix_eff_lexp (LEXP_aux (LEXP_deref exp, annot))))
     | LEXP_memory (id,es) ->
        n_exp_nameL es (fun es -> 
-- 
cgit v1.2.3


From 53959905b8e4bfd4877c1e052195391d89bdb0d6 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 3 Jul 2018 19:06:03 +0100
Subject: Fix a bug in foreach loops

We should test before the first iteration in case 'to' starts out as
less than 'from'.
---
 src/c_backend.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 8a41df67..4335e98e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1215,6 +1215,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      in
 
      let loop_start_label = label "for_start_" in
+     let loop_end_label = label "for_end_" in
      let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in
      let body_gs = gensym () in
 
@@ -1223,17 +1224,15 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      @ variable_init step_gs step_setup step_ctyp step_call step_cleanup
      @ [iblock ([idecl CT_int64 loop_var;
                  icopy (CL_id loop_var) (F_id from_gs, CT_int64);
-                 ilabel loop_start_label;
                  idecl CT_unit body_gs;
-                 iblock (body_setup
+                 iblock ([ilabel loop_start_label]
+                         @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label]
+                         @ body_setup
                          @ [body_call (CL_id body_gs)]
                          @ body_cleanup
-                         @ if is_inc then
-                             [icopy (CL_id loop_var) (F_op (F_id loop_var, "+", F_id step_gs), CT_int64);
-                              ijump (F_op (F_id loop_var, "<=", F_id to_gs), CT_bool) loop_start_label]
-                           else
-                             [icopy (CL_id loop_var) (F_op (F_id loop_var, "-", F_id step_gs), CT_int64);
-                              ijump (F_op (F_id loop_var, ">=", F_id to_gs), CT_bool) loop_start_label])])],
+                         @ [icopy (CL_id loop_var) (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)]
+                         @ [igoto loop_start_label]);
+                 ilabel loop_end_label])],
      CT_unit,
      (fun clexp -> icopy clexp unit_fragment),
      []
-- 
cgit v1.2.3


From c080665a6fbd8c88b66440a7bddc31a9634741cf Mon Sep 17 00:00:00 2001
From: Jon French
Date: Thu, 5 Jul 2018 13:09:41 +0100
Subject: restore missing RISC-V fence types in sail2; ignore io bits in fences
 more cleanly

---
 src/lem_interp/sail2_instr_kinds.lem | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index 13e5304e..938b693d 100644
--- a/src/lem_interp/sail2_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
@@ -151,6 +151,10 @@ type barrier_kind =
   | Barrier_RISCV_r_r
   | Barrier_RISCV_rw_w
   | Barrier_RISCV_w_w
+  | Barrier_RISCV_w_rw
+  | Barrier_RISCV_rw_r
+  | Barrier_RISCV_r_w
+  | Barrier_RISCV_w_r
   | Barrier_RISCV_i
   (* X86 *)
   | Barrier_x86_MFENCE
@@ -176,6 +180,10 @@ instance (Show barrier_kind)
     | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
     | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
     | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
+    | Barrier_RISCV_w_rw  -> "Barrier_RISCV_w_rw"
+    | Barrier_RISCV_rw_r  -> "Barrier_RISCV_rw_r"
+    | Barrier_RISCV_r_w   -> "Barrier_RISCV_r_w"
+    | Barrier_RISCV_w_r   -> "Barrier_RISCV_w_r"
     | Barrier_RISCV_i     -> "Barrier_RISCV_i"
     | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
   end
@@ -288,7 +296,11 @@ instance (EnumerationType barrier_kind)
     | Barrier_RISCV_r_r -> 15
     | Barrier_RISCV_rw_w -> 16
     | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_i -> 18
-    | Barrier_x86_MFENCE -> 19
+    | Barrier_RISCV_w_rw -> 18
+    | Barrier_RISCV_rw_r -> 19
+    | Barrier_RISCV_r_w -> 20
+    | Barrier_RISCV_w_r -> 21
+    | Barrier_RISCV_i -> 22
+    | Barrier_x86_MFENCE -> 23
   end
 end
-- 
cgit v1.2.3


From 86194c561fbb9ea24b28f413f16211d5920bb362 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 5 Jul 2018 16:17:01 +0100
Subject: make many generated c functions static -- this gives the compiler a
 chance to notice if they are dead or inline them if appropriate, cleaning up
 coverage reports and potentially improving execution speed.

---
 src/c_backend.ml | 66 ++++++++++++++++++++++++++++----------------------------
 1 file changed, 33 insertions(+), 33 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 4335e98e..eeb3390e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2086,7 +2086,7 @@ let codegen_type_def ctx = function
   | CTD_enum (id, ids) ->
      let codegen_eq =
        let name = sgen_id id in
-       string (Printf.sprintf "bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name)
+       string (Printf.sprintf "static bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name)
      in
      string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline
      ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) upper_codegen_id ids; rbrace ^^ semi]
@@ -2102,7 +2102,7 @@ let codegen_type_def ctx = function
          string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
      in
      let codegen_setter id ctors =
-       string (let n = sgen_id id in Printf.sprintf "void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space
+       string (let n = sgen_id id in Printf.sprintf "static void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space
        ^^ surround 2 0 lbrace
                    (separate_map hardline codegen_set (Bindings.bindings ctors))
                    rbrace
@@ -2114,13 +2114,13 @@ let codegen_type_def ctx = function
        else []
      in
      let codegen_init f id ctors =
-       string (let n = sgen_id id in Printf.sprintf "void %s(%s)(struct %s *op)" f n n) ^^ space
+       string (let n = sgen_id id in Printf.sprintf "static void %s(%s)(struct %s *op)" f n n) ^^ space
        ^^ surround 2 0 lbrace
                    (separate hardline (Bindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat))
                    rbrace
      in
      let codegen_eq =
-       string (Printf.sprintf "bool eq_%s(struct %s op1, struct %s op2) { return true; }" (sgen_id id) (sgen_id id) (sgen_id id))
+       string (Printf.sprintf "static bool eq_%s(struct %s op1, struct %s op2) { return true; }" (sgen_id id) (sgen_id id) (sgen_id id))
      in
      (* Generate the struct and add the generated functions *)
      let codegen_ctor (id, ctyp) =
@@ -2161,7 +2161,7 @@ let codegen_type_def ctx = function
      let codegen_init =
        let n = sgen_id id in
        let ctor_id, ctyp = List.hd tus in
-       string (Printf.sprintf "void CREATE(%s)(struct %s *op)" n n)
+       string (Printf.sprintf "static void CREATE(%s)(struct %s *op)" n n)
        ^^ hardline
        ^^ surround 2 0 lbrace
                    (string (Printf.sprintf "op->kind = Kind_%s;" (sgen_id ctor_id)) ^^ hardline
@@ -2172,7 +2172,7 @@ let codegen_type_def ctx = function
      in
      let codegen_reinit =
        let n = sgen_id id in
-       string (Printf.sprintf "void RECREATE(%s)(struct %s *op) {}" n n)
+       string (Printf.sprintf "static void RECREATE(%s)(struct %s *op) {}" n n)
      in
      let clear_field v ctor_id ctyp =
        if is_stack_ctyp ctyp then
@@ -2182,7 +2182,7 @@ let codegen_type_def ctx = function
      in
      let codegen_clear =
        let n = sgen_id id in
-       string (Printf.sprintf "void KILL(%s)(struct %s *op)" n n) ^^ hardline
+       string (Printf.sprintf "static void KILL(%s)(struct %s *op)" n n) ^^ hardline
        ^^ surround 2 0 lbrace
                    (each_ctor "op->" (clear_field "op") tus ^^ semi)
                    rbrace
@@ -2203,7 +2203,7 @@ let codegen_type_def ctx = function
             ^^ separate hardline (List.mapi tuple_set ctyps) ^^ hardline
          | ctyp -> Printf.sprintf "%s op" (sgen_ctyp ctyp), empty
        in
-       string (Printf.sprintf "void %s(struct %s *rop, %s)" (sgen_id ctor_id) (sgen_id id) ctor_args) ^^ hardline
+       string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_id ctor_id) (sgen_id id) ctor_args) ^^ hardline
        ^^ surround 2 0 lbrace
                    (tuple
                     ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline
@@ -2224,7 +2224,7 @@ let codegen_type_def ctx = function
            string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))
            ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id))
        in
-       string (Printf.sprintf "void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline
+       string (Printf.sprintf "static void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline
        ^^ surround 2 0 lbrace
                    (each_ctor "rop->" (clear_field "rop") tus
                     ^^ semi ^^ hardline
@@ -2306,10 +2306,10 @@ let codegen_node id ctyp =
   ^^ string (Printf.sprintf "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id))
 
 let codegen_list_init id =
-  string (Printf.sprintf "void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id))
+  string (Printf.sprintf "static void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id))
 
 let codegen_list_clear id ctyp =
-  string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
+  string (Printf.sprintf "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
   ^^ string (Printf.sprintf "  if (*rop == NULL) return;")
   ^^ (if is_stack_ctyp ctyp then empty
       else string (Printf.sprintf "  KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)))
@@ -2318,7 +2318,7 @@ let codegen_list_clear id ctyp =
   ^^ string "}"
 
 let codegen_list_set id ctyp =
-  string (Printf.sprintf "void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+  string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
   ^^ string "  if (op == NULL) { *rop = NULL; return; };\n"
   ^^ string (Printf.sprintf "  *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id))
   ^^ (if is_stack_ctyp ctyp then
@@ -2329,14 +2329,14 @@ let codegen_list_set id ctyp =
   ^^ string (Printf.sprintf "  internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id))
   ^^ string "}"
   ^^ twice hardline
-  ^^ string (Printf.sprintf "void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+  ^^ string (Printf.sprintf "static void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
   ^^ string (Printf.sprintf "  KILL(%s)(rop);\n" (sgen_id id))
   ^^ string (Printf.sprintf "  internal_set_%s(rop, op);\n" (sgen_id id))
   ^^ string "}"
 
 let codegen_cons id ctyp =
   let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in
-  string (Printf.sprintf "void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
+  string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
   ^^ string (Printf.sprintf "  *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id))
   ^^ (if is_stack_ctyp ctyp then
         string "  (*rop)->hd = x;\n"
@@ -2348,9 +2348,9 @@ let codegen_cons id ctyp =
 
 let codegen_pick id ctyp =
   if is_stack_ctyp ctyp then
-    string (Printf.sprintf "%s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id))
+    string (Printf.sprintf "static %s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id))
   else
-    string (Printf.sprintf "void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
+    string (Printf.sprintf "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp))
 
 let codegen_list ctx ctyp =
   let id = mk_id (string_of_ctyp (CT_list ctyp)) in
@@ -2378,10 +2378,10 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id))
     in
     let vector_init =
-      string (Printf.sprintf "void CREATE(%s)(%s *rop) {\n  rop->len = 0;\n  rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
+      string (Printf.sprintf "static void CREATE(%s)(%s *rop) {\n  rop->len = 0;\n  rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
     in
     let vector_set =
-      string (Printf.sprintf "void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+      string (Printf.sprintf "static void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
       ^^ string (Printf.sprintf "  KILL(%s)(rop);\n" (sgen_id id))
       ^^ string "  rop->len = op.len;\n"
       ^^ string (Printf.sprintf "  rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
@@ -2394,7 +2394,7 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string "}"
     in
     let vector_clear =
-      string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
+      string (Printf.sprintf "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
       ^^ (if is_stack_ctyp ctyp then empty
          else
            string "  for (int i = 0; i < (rop->len); i++) {\n"
@@ -2404,7 +2404,7 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string "}"
     in
     let vector_update =
-      string (Printf.sprintf "void vector_update_%s(%s *rop, %s op, mpz_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+      string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, mpz_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
       ^^ string "  int m = mpz_get_ui(n);\n"
       ^^ string "  if (rop->data == op.data) {\n"
       ^^ string (if is_stack_ctyp ctyp then
@@ -2421,7 +2421,7 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string "}"
     in
     let internal_vector_update =
-      string (Printf.sprintf "void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+      string (Printf.sprintf "static void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
       ^^ string (if is_stack_ctyp ctyp then
                    "  rop->data[n] = elem;\n"
                  else
@@ -2430,24 +2430,24 @@ let codegen_vector ctx (direction, ctyp) =
     in
     let vector_access =
       if is_stack_ctyp ctyp then
-        string (Printf.sprintf "%s vector_access_%s(%s op, mpz_t n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id))
+        string (Printf.sprintf "static %s vector_access_%s(%s op, mpz_t n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id))
         ^^ string "  int m = mpz_get_ui(n);\n"
         ^^ string "  return op.data[m];\n"
         ^^ string "}"
       else
-        string (Printf.sprintf "void vector_access_%s(%s *rop, %s op, mpz_t n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
+        string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, mpz_t n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
         ^^ string "  int m = mpz_get_ui(n);\n"
         ^^ string (Printf.sprintf "  COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp))
         ^^ string "}"
     in
     let internal_vector_init =
-      string (Printf.sprintf "void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id))
+      string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id))
       ^^ string "  rop->len = len;\n"
       ^^ string (Printf.sprintf "  rop->data = malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp))
       ^^ string "}"
     in
     let vector_undefined =
-      string (Printf.sprintf "void undefined_vector_%s(%s *rop, mpz_t len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+      string (Printf.sprintf "static void undefined_vector_%s(%s *rop, mpz_t len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
       ^^ string (Printf.sprintf "  rop->len = mpz_get_ui(len);\n")
       ^^ string (Printf.sprintf "  rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
       ^^ string "  for (int i = 0; i < (rop->len); i++) {\n"
@@ -2495,9 +2495,9 @@ let codegen_def' ctx = function
      if Env.is_extern id ctx.tc_env "c" then
        empty
      else if is_stack_ctyp ret_ctyp then
-       string (Printf.sprintf "%s %s(%s);" (sgen_ctyp ret_ctyp) (sgen_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "static %s %s(%s);" (sgen_ctyp ret_ctyp) (sgen_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
      else
-       string (Printf.sprintf "void %s(%s *rop, %s);" (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "static void %s(%s *rop, %s);" (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
 
   | CDEF_fundef (id, ret_arg, args, instrs) as def ->
      if !opt_ddump_flow_graphs then make_dot id (instrs_graph instrs) else ();
@@ -2521,10 +2521,10 @@ let codegen_def' ctx = function
        match ret_arg with
        | None ->
           assert (is_stack_ctyp ret_ctyp);
-          string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline
+          string "static " ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline
        | Some gs ->
           assert (not (is_stack_ctyp ret_ctyp));
-          string "void" ^^ space ^^ codegen_id id
+          string "static void" ^^ space ^^ codegen_id id
           ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
           ^^ hardline
      in
@@ -2537,7 +2537,7 @@ let codegen_def' ctx = function
      codegen_type_def ctx ctype_def
 
   | CDEF_startup (id, instrs) ->
-     let startup_header = string (Printf.sprintf "void startup_%s(void)" (sgen_id id)) in
+     let startup_header = string (Printf.sprintf "static void startup_%s(void)" (sgen_id id)) in
      separate_map hardline codegen_decl instrs
      ^^ twice hardline
      ^^ startup_header ^^ hardline
@@ -2546,7 +2546,7 @@ let codegen_def' ctx = function
      ^^ string "}"
 
   | CDEF_finish (id, instrs) ->
-     let finish_header = string (Printf.sprintf "void finish_%s(void)" (sgen_id id)) in
+     let finish_header = string (Printf.sprintf "static void finish_%s(void)" (sgen_id id)) in
      separate_map hardline codegen_decl (List.filter is_decl instrs)
      ^^ twice hardline
      ^^ finish_header ^^ hardline
@@ -2563,12 +2563,12 @@ let codegen_def' ctx = function
        List.concat (List.map (fun (id, ctyp) -> [iclear ctyp id]) bindings)
      in
      separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings
-     ^^ hardline ^^ string (Printf.sprintf "void create_letbind_%d(void) " number)
+     ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number)
      ^^ string "{"
      ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline
      ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") { ctx with no_raw = true }) instrs) ^^ hardline
      ^^ string "}"
-     ^^ hardline ^^ string (Printf.sprintf "void kill_letbind_%d(void) " number)
+     ^^ hardline ^^ string (Printf.sprintf "static void kill_letbind_%d(void) " number)
      ^^ string "{"
      ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) cleanup) ^^ hardline
      ^^ string "}"
-- 
cgit v1.2.3


From 9a0cbbedbe281807f70bf2206756624315096642 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 5 Jul 2018 19:09:26 +0100
Subject: Fix CHERI test that was failing when compiled to C

Non bitvector literals for decreasing vectors were not being reversed
correctly, so the list of capability registers was effectively in
reverse order.

Added a test case to test/c/ based on this aspect of CHERI
---
 src/c_backend.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index eeb3390e..6f1379e3 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -691,7 +691,7 @@ let rec compile_aval ctx = function
      in
      [idecl vector_ctyp gs;
       iextern (CL_id gs) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)] vector_ctyp]
-     @ List.concat (List.mapi aval_set avals),
+     @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)),
      (F_id gs, vector_ctyp),
      [iclear vector_ctyp gs]
 
-- 
cgit v1.2.3


From f62edee6988476ed8ba78424c870461ac8d44256 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 5 Jul 2018 20:57:44 +0100
Subject: Fix equality comparisons for structs

Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any
builtin type in sail.h.
---
 src/c_backend.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 6f1379e3..6097e996 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2120,7 +2120,19 @@ let codegen_type_def ctx = function
                    rbrace
      in
      let codegen_eq =
-       string (Printf.sprintf "static bool eq_%s(struct %s op1, struct %s op2) { return true; }" (sgen_id id) (sgen_id id) (sgen_id id))
+       let codegen_eq_test (id, ctyp) =
+         if is_stack_ctyp ctyp then
+           string (Printf.sprintf "op1.%s == op2.%s" (sgen_id id) (sgen_id id))
+         else
+           string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
+       in
+       string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2)" (sgen_id id) (sgen_id id) (sgen_id id))
+       ^^ space
+       ^^ surround 2 0 lbrace
+            (string "return" ^^ space
+             ^^ separate_map (string " && ") codegen_eq_test ctors
+             ^^ string ";")
+            rbrace
      in
      (* Generate the struct and add the generated functions *)
      let codegen_ctor (id, ctyp) =
-- 
cgit v1.2.3


From 79c9c884536cb522ac54c51aad70ab810ea4a420 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 5 Jul 2018 21:34:23 +0100
Subject: Fix equality comparisons for variants in C

Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing
variants. Also make sure that struct equality works for structs containing other structs.
---
 src/c_backend.ml | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 6097e996..09501ce9 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2121,10 +2121,7 @@ let codegen_type_def ctx = function
      in
      let codegen_eq =
        let codegen_eq_test (id, ctyp) =
-         if is_stack_ctyp ctyp then
-           string (Printf.sprintf "op1.%s == op2.%s" (sgen_id id) (sgen_id id))
-         else
-           string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
+         string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id))
        in
        string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2)" (sgen_id id) (sgen_id id) (sgen_id id))
        ^^ space
@@ -2245,6 +2242,21 @@ let codegen_type_def ctx = function
                     ^^ each_ctor "op." set_field tus)
                    rbrace
      in
+     let codegen_eq =
+       let codegen_eq_test ctor_id ctyp =
+         string (Printf.sprintf "return EQUAL(%s)(op1.%s, op2.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id))
+       in
+       let rec codegen_eq_tests = function
+         | [] -> string "return false;"
+         | (ctor_id, ctyp) :: ctors ->
+            string (Printf.sprintf "if (op1.kind == Kind_%s && op2.kind == Kind_%s) " (sgen_id ctor_id) (sgen_id ctor_id)) ^^ lbrace ^^ hardline
+            ^^ jump 0 2 (codegen_eq_test ctor_id ctyp)
+            ^^ hardline ^^ rbrace ^^ string " else " ^^ codegen_eq_tests ctors
+       in
+       let n = sgen_id id in
+       string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2) " n n n)
+       ^^ surround 2 0 lbrace (codegen_eq_tests tus) rbrace
+     in
      string (Printf.sprintf "// union %s" (string_of_id id)) ^^ hardline
      ^^ string "enum" ^^ space
      ^^ string ("kind_" ^ sgen_id id) ^^ space
@@ -2272,6 +2284,8 @@ let codegen_type_def ctx = function
      ^^ twice hardline
      ^^ codegen_setter
      ^^ twice hardline
+     ^^ codegen_eq
+     ^^ twice hardline
      ^^ separate_map (twice hardline) codegen_ctor tus
      (* If this is the exception type, then we setup up some global variables to deal with exceptions. *)
      ^^ if string_of_id id = "exception" then
-- 
cgit v1.2.3


From d2ddaad22f25a152d5fd53c11b3e1698747bd9c5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 4 Jul 2018 11:43:06 +0100
Subject: Coq: turn off partial support for dropping true constraints, fix
 strings

---
 src/pretty_print_coq.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 78507577..6df8c5df 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -424,7 +424,7 @@ let doc_typ, doc_atomic_typ =
            List.fold_left add_tyvar tpp kids
         | None ->
            match nc with
-           | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids)
+(*           | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids)*)
            | _ -> List.fold_left add_tyvar (doc_arithfact ctx nc) kids
       end
     and doc_typ_arg (Typ_arg_aux(t,_)) = match t with
@@ -1839,6 +1839,8 @@ try
           (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline;
         string "Import ListNotations.";
         hardline;
+        string "Open Scope string.";
+        hardline;
         (* Put the body into a Section so that we can define some values with
            Let to put them into the local context, where tactics can see them *)
         string "Section Content.";
-- 
cgit v1.2.3


From e4c43d45c6fe5267ad72a1be64d6328470f2a18e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 5 Jul 2018 17:02:03 +0100
Subject: Coq: missing existential building for ranges

---
 src/pretty_print_coq.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 6df8c5df..5f4d349c 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -946,6 +946,9 @@ let doc_exp_lem, doc_let_lem =
               (* TODO: more sophisticated check *)
               match destruct_exist env arg_ty, destruct_exist env typ_from_fn with
               | Some _, None -> parens (string "projT1 " ^^ arg_pp)
+              (* Usually existentials have already been built elsewhere, but this
+                 is useful for (e.g.) ranges *)
+              | None, Some _ -> parens (string "build_ex " ^^ arg_pp)
               | _, _ -> arg_pp
             in
             let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in
-- 
cgit v1.2.3


From cd3a1f9a5ac8c7e64489a1d92dc4dea595ed8a2b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 6 Jul 2018 10:14:51 +0100
Subject: Coq: reduce use of sumbool_of_bool to relevant constraints

---
 src/pretty_print_coq.ml | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5f4d349c..dc0b5036 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -708,6 +708,21 @@ let similar_nexps n1 n2 =
     | _ -> false
   in if same_nexp_shape n1 n2 then true else false
 
+let constraint_fns = ["Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"]
+
+let condition_produces_constraint exp =
+  (* Cheat a little - this isn't quite the right environment for subexpressions
+     but will have all of the relevant functions in it. *)
+  let env = env_of exp in
+  Rewriter.fold_exp
+    { (Rewriter.pure_exp_alg false (||)) with
+      Rewriter.e_app = fun (f,bs) ->
+        List.exists (fun x -> x) bs ||
+        (Env.is_extern f env "coq" &&
+           let f' = Env.get_extern f env "coq" in
+           List.exists (fun id -> String.compare f' id == 0) constraint_fns)
+    } exp
+
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
@@ -1191,7 +1206,9 @@ let doc_exp_lem, doc_let_lem =
       | _ -> prefix 2 1 (string "else") (top_exp ctxt false e)
     in
     (prefix 2 1
-      (soft_surround 2 1 if_pp (string "sumbool_of_bool" ^^ space ^^ parens (top_exp ctxt true c)) (string "then"))
+      (soft_surround 2 1 if_pp
+         ((if condition_produces_constraint c then string "sumbool_of_bool" ^^ space else empty)
+          ^^ parens (top_exp ctxt true c)) (string "then"))
       (top_exp ctxt false t)) ^^
     break 1 ^^
     else_pp
-- 
cgit v1.2.3


From f1f3c68878406ae5029881e20b839d2b6f535280 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 6 Jul 2018 17:00:05 +0100
Subject: Coq: feed assertions into the context

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index dc0b5036..9cc85601 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1149,7 +1149,7 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> liftR (separate space [string "exit"; expY e])
     | E_assert (e1,e2) ->
-       let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
+       let epp = liftR (separate space [string "assert_exp'"; expY e1; expY e2]) in
        if aexp_needed then parens (align epp) else align epp
     | E_app_infix (e1,id,e2) ->
        raise (Reporting_basic.err_unreachable l
@@ -1161,6 +1161,9 @@ let doc_exp_lem, doc_let_lem =
          let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
          let middle =
            match fst (untyp_pat pat) with
+           | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)
+             when (match e1 with E_aux (E_assert _,_) -> true | _ -> false) ->
+              string ">>= fun _ =>"
            | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
               string ">>"
            | P_aux (P_id id,_) ->
-- 
cgit v1.2.3


From a41ca0c0ed6acdb17362886c4c9650c4c353afef Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 6 Jul 2018 17:36:33 +0100
Subject: Coq: Avoid clashes with the monad name, M

---
 src/pretty_print_coq.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 9cc85601..1eb62193 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -136,6 +136,7 @@ let rec fix_id remove_tick name = match name with
   | "EQ"
   | "Z"
   | "mod"
+  | "M"
     -> name ^ "'"
   | _ ->
      if String.contains name '#' then
@@ -146,7 +147,7 @@ let rec fix_id remove_tick name = match name with
        fix_id remove_tick (String.concat "__" (Util.split_on_char '^' name))
      else if name.[0] = '\'' then
        let var = String.sub name 1 (String.length name - 1) in
-       if remove_tick then var else (var ^ "'")
+       if remove_tick then fix_id remove_tick var else (var ^ "'")
      else if is_number_char(name.[0]) then
        ("v" ^ name ^ "'")
      else name
-- 
cgit v1.2.3


From 3c5d11d7536c1f0f1d3c899b5daac7e35f1f369a Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 6 Jul 2018 18:26:41 +0100
Subject: Coq: avoid nexp simplification when deciding whether a cast is needed

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 1eb62193..a85e8782 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -987,9 +987,11 @@ let doc_exp_lem, doc_let_lem =
                 | t1, t2 -> false,false,t1,t2
               in
               let autocast =
-                match destruct_vector env in_typ, destruct_vector env out_typ with
-                | Some (n1,_,t1), Some (n2,_,t2) 
-                  when is_bit_typ t1 && is_bit_typ t2 ->
+                (* Avoid using helper functions which simplify the nexps *)
+                is_bitvector_typ in_typ && is_bitvector_typ out_typ &&
+                match in_typ, out_typ with
+                | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_),
+                  Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) ->
                    not (similar_nexps n1 n2)
                 | _ -> false
               in unpack,build_ex,autocast
-- 
cgit v1.2.3


From 7c36a2c621ce64e3a181bf72f7b0434f42450092 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 6 Jul 2018 21:28:35 +0100
Subject: Coq: support assertions inside and outside of blocks

---
 src/pretty_print_coq.ml | 46 ++++++++++++++++++++++++++--------------------
 1 file changed, 26 insertions(+), 20 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index a85e8782..7d8d0e5a 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1152,7 +1152,7 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> liftR (separate space [string "exit"; expY e])
     | E_assert (e1,e2) ->
-       let epp = liftR (separate space [string "assert_exp'"; expY e1; expY e2]) in
+       let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
        if aexp_needed then parens (align epp) else align epp
     | E_app_infix (e1,id,e2) ->
        raise (Reporting_basic.err_unreachable l
@@ -1160,25 +1160,31 @@ let doc_exp_lem, doc_let_lem =
     | E_var(lexp, eq_exp, in_exp) ->
        raise (report l "E_vars should have been removed before pretty-printing")
     | E_internal_plet (pat,e1,e2) ->
-       let epp =
-         let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
-         let middle =
-           match fst (untyp_pat pat) with
-           | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)
-             when (match e1 with E_aux (E_assert _,_) -> true | _ -> false) ->
-              string ">>= fun _ =>"
-           | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
-              string ">>"
-           | P_aux (P_id id,_) ->
-              separate space [string ">>= fun"; doc_id id; bigarrow]
-           | P_aux (P_typ (typ, P_aux (P_id id,_)),_) ->
-              separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]
-           | _ ->
-              separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow]
-         in
-         infix 0 1 middle (expV b e1) (expN e2)
-       in
-       if aexp_needed then parens (align epp) else epp
+       begin
+         match pat, e1 with
+         | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)),
+           (E_aux (E_assert (assert_e1,assert_e2),_)) ->
+            let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in
+            let epp = infix 0 1 (string ">>= fun _ =>") epp (expN e2) in
+            if aexp_needed then parens (align epp) else align epp
+         | _ ->
+            let epp =
+              let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
+              let middle =
+                match fst (untyp_pat pat) with
+                | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
+                   string ">>"
+                | P_aux (P_id id,_) ->
+                   separate space [string ">>= fun"; doc_id id; bigarrow]
+                | P_aux (P_typ (typ, P_aux (P_id id,_)),_) ->
+                   separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]
+                | _ ->
+                   separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow]
+              in
+              infix 0 1 middle (expV b e1) (expN e2)
+            in
+            if aexp_needed then parens (align epp) else epp
+       end
     | E_internal_return (e1) ->
        wrap_parens (align (separate space [string "returnm"; expY e1]))
     | E_sizeof nexp ->
-- 
cgit v1.2.3


From a7e3bad39b771cb18b989da05528e6e6f2788147 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sat, 7 Jul 2018 16:34:42 +0100
Subject: Coq: supply index constraint in for loops

---
 src/pretty_print_coq.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 7d8d0e5a..38395b07 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -831,7 +831,7 @@ let doc_exp_lem, doc_let_lem =
        | Id_aux (Id "foreach", _) ->
           begin
             match args with
-            | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
+            | [from_exp; to_exp; step_exp; ord_exp; vartuple; body] ->
                let loopvar, body = match body with
                  | E_aux (E_let (LB_aux (LB_val (_, _), _),
                    E_aux (E_let (LB_aux (LB_val (_, _), _),
@@ -842,13 +842,13 @@ let doc_exp_lem, doc_let_lem =
                      | (P_aux (P_id id, _))), _), _),
                      body), _), _), _)), _)), _) -> id, body
                  | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
-               let step = match ord_exp with
-                 | E_aux (E_lit (L_aux (L_false, _)), _) ->
-                    parens (separate space [string "integerNegate"; expY exp3])
-                 | _ -> expY exp3
+               let dir = match ord_exp with
+                 | E_aux (E_lit (L_aux (L_false, _)), _) -> "_down"
+                 | E_aux (E_lit (L_aux (L_true, _)), _) -> "_up"
+                 | _ -> raise (Reporting_basic.err_unreachable l ("Unexpected loop direction " ^ string_of_exp ord_exp))
                in
-               let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in
-               let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in
+               let combinator = if effectful (effect_of body) then "foreach_ZM" else "foreach_Z" in
+               let combinator = combinator ^ dir in
                let used_vars_body = find_e_ids body in
                let body_lambda =
                  (* Work around indentation issues in Lem when translating
@@ -856,18 +856,20 @@ let doc_exp_lem, doc_let_lem =
                  match fst (uncast_exp vartuple) with
                    | E_aux (E_tuple _, _)
                      when not (IdSet.mem (mk_id "varstup") used_vars_body)->
-                      separate space [string "fun"; doc_id loopvar; string "varstup"; bigarrow]
+                      separate space [string "fun"; doc_id loopvar; string "_"; string "varstup"; bigarrow]
                       ^^ break 1 ^^
                       separate space [string "let"; expY vartuple; string ":= varstup in"]
                    | E_aux (E_lit (L_aux (L_unit, _)), _)
                      when not (IdSet.mem (mk_id "unit_var") used_vars_body) ->
-                      separate space [string "fun"; doc_id loopvar; string "unit_var"; bigarrow]
+                      separate space [string "fun"; doc_id loopvar; string "_"; string "unit_var"; bigarrow]
                    | _ ->
-                      separate space [string "fun"; doc_id loopvar; expY vartuple; bigarrow]
+                      separate space [string "fun"; doc_id loopvar; string "_"; expY vartuple; bigarrow]
                in
                parens (
                    (prefix 2 1)
-                     ((separate space) [string combinator; indices_pp; expY vartuple])
+                     ((separate space) [string combinator;
+                                        expY from_exp; expY to_exp; expY step_exp;
+                                        expY vartuple])
                      (parens
                         (prefix 2 1 (group body_lambda) (expN body))
                      )
-- 
cgit v1.2.3


From 979d88fec8a5c611ee61be15ce45ae81b4a52317 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sat, 7 Jul 2018 16:36:04 +0100
Subject: Coq: precise generic vectors (probably still some pattern matching to
 do, but I don't think the models use that)

---
 src/pretty_print_coq.ml | 6 ++++--
 src/state.ml            | 8 ++++----
 2 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 38395b07..e68a6dd9 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -382,7 +382,7 @@ let doc_typ, doc_atomic_typ =
          let tpp = match elem_typ with
            | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
              string "mword " ^^ doc_nexp ctx (nexp_simp m)
-           | _ -> string "list" ^^ space ^^ typ elem_typ in
+           | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx (nexp_simp m) in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
          let tpp = string "register_ref regstate register_value " ^^ typ etyp in
@@ -1122,7 +1122,9 @@ let doc_exp_lem, doc_let_lem =
          if is_bit_typ etyp then
            let bepp = string "vec_of_bits" ^^ space ^^ align epp in
            (align (group (prefix 0 1 bepp (doc_tannot_lem ctxt (env_of full_exp) false t))), true)
-         else (epp,aexp_needed) in
+         else
+           let vepp = string "vec_of_list_len" ^^ space ^^ align epp in
+           (vepp,aexp_needed) in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update(v,e1,e2) ->
        raise (Reporting_basic.err_unreachable l
diff --git a/src/state.ml b/src/state.ml
index c591f753..e788ab6a 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -411,7 +411,7 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with
      let size = string_of_nexp (nexp_simp size) in
      let is_inc = if is_order_inc ord then "true" else "false" in
      let etyp_of, of_etyp = regval_convs_coq etyp in
-     "(fun v => vector_of_regval " ^ etyp_of ^ " v)",
+     "(fun v => vector_of_regval " ^ size ^ " " ^ etyp_of ^ " v)",
      "(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)"
   | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
     when string_of_id id = "list" ->
@@ -430,12 +430,12 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with
 let register_refs_coq registers =
   let generic_convs =
     separate_map hardline string [
-      "Definition vector_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
-      "  | Regval_vector (_, _, v) => just_list (List.map of_regval v)";
+      "Definition vector_of_regval {a} n (of_regval : register_value -> option a) (rv : register_value) : option (vec a n) := match rv with";
+      "  | Regval_vector (n', _, v) => if n =? n' then map_bind (vec_of_list n) (just_list (List.map of_regval v)) else None";
       "  | _ => None";
       "end.";
       "";
-      "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : list a) : register_value := Regval_vector (size, is_inc, List.map regval_of xs).";
+      "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : vec a size) : register_value := Regval_vector (size, is_inc, List.map regval_of (list_of_vec xs)).";
       "";
       "Definition list_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
       "  | Regval_list v => just_list (List.map of_regval v)";
-- 
cgit v1.2.3


From 8286993fe02b151dc1daa808b422f1ba97e05602 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Sun, 8 Jul 2018 14:19:23 +0100
Subject: Add -static flag that controls whether generated C functions are
 static

By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
---
 src/c_backend.ml | 7 +++++--
 src/sail.ml      | 3 +++
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 09501ce9..e92ca1a6 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -63,6 +63,7 @@ module Big_int = Nat_big_num
 let c_verbosity = ref 0
 let opt_ddump_flow_graphs = ref false
 let opt_trace = ref false
+let opt_static = ref false
 
 (* Optimization flags *)
 let optimize_primops = ref false
@@ -2547,10 +2548,12 @@ let codegen_def' ctx = function
        match ret_arg with
        | None ->
           assert (is_stack_ctyp ret_ctyp);
-          string "static " ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline
+          (if !opt_static then string "static " else empty)
+          ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline
        | Some gs ->
           assert (not (is_stack_ctyp ret_ctyp));
-          string "static void" ^^ space ^^ codegen_id id
+          (if !opt_static then string "static " else empty)
+          ^^ string "void" ^^ space ^^ codegen_id id
           ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
           ^^ hardline
      in
diff --git a/src/sail.ml b/src/sail.ml
index 046445d1..64e60c23 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -121,6 +121,9 @@ let options = Arg.align ([
   ( "-Oconstant_fold",
     Arg.Set Constant_fold.optimize_constant_fold,
     " Apply constant folding optimizations");
+  ( "-static",
+    Arg.Set C_backend.opt_static,
+    " Make generated C functions static");
   ( "-trace",
     Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml],
     " Instrument ouput with tracing");
-- 
cgit v1.2.3


From edc2be164fcf53c333796e55b93f94bf6c9ed152 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 22 Jun 2018 19:03:02 +0100
Subject: Simplify treating of undefined_bool in Lem library

Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
---
 src/gen_lib/sail2_operators_bitlists.lem | 56 ++++++++++++++---------------
 src/gen_lib/sail2_operators_mwords.lem   | 62 ++++++++++++++++----------------
 src/gen_lib/sail2_prompt.lem             | 32 +++++++++++------
 src/gen_lib/sail2_prompt_monad.lem       |  1 +
 src/gen_lib/sail2_state.lem              | 32 +++++++++++------
 src/gen_lib/sail2_state_monad.lem        | 18 +++-------
 6 files changed, 107 insertions(+), 94 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 3f8b7510..0c833e90 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -10,16 +10,16 @@ open import Sail2_prompt
 val uint_maybe : list bitU -> maybe integer
 let uint_maybe v = unsigned v
 let uint_fail v = maybe_fail "uint" (unsigned v)
-let uint_oracle v =
-  bools_of_bits_oracle v >>= (fun bs ->
+let uint_nondet v =
+  bools_of_bits_nondet v >>= (fun bs ->
   return (int_of_bools false bs))
 let uint v = maybe_failwith (uint_maybe v)
 
 val sint_maybe : list bitU -> maybe integer
 let sint_maybe v = signed v
 let sint_fail v = maybe_fail "sint" (signed v)
-let sint_oracle v =
-  bools_of_bits_oracle v >>= (fun bs ->
+let sint_nondet v =
+  bools_of_bits_nondet v >>= (fun bs ->
   return (int_of_bools true bs))
 let sint v = maybe_failwith (sint_maybe v)
 
@@ -43,13 +43,13 @@ let vector_truncate bs len = extz_bv len bs
 
 val vec_of_bits_maybe    : list bitU -> maybe (list bitU)
 val vec_of_bits_fail     : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
-val vec_of_bits_oracle   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
+val vec_of_bits_nondet   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
 val vec_of_bits_failwith : list bitU -> list bitU
 val vec_of_bits          : list bitU -> list bitU
 let inline vec_of_bits bits = bits
 let inline vec_of_bits_maybe bits = Just bits
 let inline vec_of_bits_fail bits = return bits
-let inline vec_of_bits_oracle bits = return bits
+let inline vec_of_bits_nondet bits = return bits
 let inline vec_of_bits_failwith bits = bits
 
 val access_vec_inc : list bitU -> integer -> bitU
@@ -62,13 +62,13 @@ val update_vec_inc : list bitU -> integer -> bitU -> list bitU
 let update_vec_inc = update_bv_inc
 let update_vec_inc_maybe v i b = Just (update_vec_inc v i b)
 let update_vec_inc_fail v i b = return (update_vec_inc v i b)
-let update_vec_inc_oracle v i b = return (update_vec_inc v i b)
+let update_vec_inc_nondet v i b = return (update_vec_inc v i b)
 
 val update_vec_dec : list bitU -> integer -> bitU -> list bitU
 let update_vec_dec = update_bv_dec
 let update_vec_dec_maybe v i b = Just (update_vec_dec v i b)
 let update_vec_dec_fail v i b = return (update_vec_dec v i b)
-let update_vec_dec_oracle v i b = return (update_vec_dec v i b)
+let update_vec_dec_nondet v i b = return (update_vec_dec v i b)
 
 val subrange_vec_inc : list bitU -> integer -> integer -> list bitU
 let subrange_vec_inc = subrange_bv_inc
@@ -89,19 +89,19 @@ val cons_vec : bitU -> list bitU -> list bitU
 let cons_vec = cons_bv
 let cons_vec_maybe b v = Just (cons_vec b v)
 let cons_vec_fail b v = return (cons_vec b v)
-let cons_vec_oracle b v = return (cons_vec b v)
+let cons_vec_nondet b v = return (cons_vec b v)
 
 val cast_unit_vec : bitU -> list bitU
 let cast_unit_vec = cast_unit_bv
 let cast_unit_vec_maybe b = Just (cast_unit_vec b)
 let cast_unit_vec_fail b = return (cast_unit_vec b)
-let cast_unit_vec_oracle b = return (cast_unit_vec b)
+let cast_unit_vec_nondet b = return (cast_unit_vec b)
 
 val vec_of_bit : integer -> bitU -> list bitU
 let vec_of_bit = bv_of_bit
 let vec_of_bit_maybe len b = Just (vec_of_bit len b)
 let vec_of_bit_fail len b = return (vec_of_bit len b)
-let vec_of_bit_oracle len b = return (vec_of_bit len b)
+let vec_of_bit_nondet len b = return (vec_of_bit len b)
 
 val msb : list bitU -> bitU
 let msb = most_significant
@@ -109,7 +109,7 @@ let msb = most_significant
 val int_of_vec_maybe : bool -> list bitU -> maybe integer
 let int_of_vec_maybe = int_of_bv
 let int_of_vec_fail sign v = maybe_fail "int_of_vec" (int_of_vec_maybe sign v)
-let int_of_vec_oracle sign v = bools_of_bits_oracle v >>= (fun v -> return (int_of_bools sign v))
+let int_of_vec_nondet sign v = bools_of_bits_nondet v >>= (fun v -> return (int_of_bools sign v))
 let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v)
 
 val string_of_bits : list bitU -> string
@@ -179,25 +179,25 @@ val subs_vec_bit     : list bitU -> bitU -> list bitU
 let add_vec_bool       l r = arith_op_bv_bool integerAdd false l r
 let add_vec_bit_maybe  l r = arith_op_bv_bit integerAdd false l r
 let add_vec_bit_fail   l r = maybe_fail "add_vec_bit" (add_vec_bit_maybe l r)
-let add_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r))
+let add_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (add_vec_bool l r))
 let add_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (add_vec_bit_maybe l r)
 
 let adds_vec_bool       l r = arith_op_bv_bool integerAdd true l r
 let adds_vec_bit_maybe  l r = arith_op_bv_bit integerAdd true l r
 let adds_vec_bit_fail   l r = maybe_fail "adds_vec_bit" (adds_vec_bit_maybe l r)
-let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r))
+let adds_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (adds_vec_bool l r))
 let adds_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (adds_vec_bit_maybe l r)
 
 let sub_vec_bool        l r = arith_op_bv_bool integerMinus false l r
 let sub_vec_bit_maybe   l r = arith_op_bv_bit integerMinus false l r
 let sub_vec_bit_fail    l r = maybe_fail "sub_vec_bit" (sub_vec_bit_maybe l r)
-let sub_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r))
+let sub_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (sub_vec_bool l r))
 let sub_vec_bit         l r = fromMaybe (repeat [BU] (length l)) (sub_vec_bit_maybe l r)
 
 let subs_vec_bool       l r = arith_op_bv_bool integerMinus true l r
 let subs_vec_bit_maybe  l r = arith_op_bv_bit integerMinus true l r
 let subs_vec_bit_fail   l r = maybe_fail "sub_vec_bit" (subs_vec_bit_maybe l r)
-let subs_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (subs_vec_bool l r))
+let subs_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (subs_vec_bool l r))
 let subs_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (subs_vec_bit_maybe l r)
 
 (*val add_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
@@ -236,47 +236,47 @@ let rotr         = rotr_bv
 val mod_vec        : list bitU -> list bitU -> list bitU
 val mod_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
 val mod_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
-val mod_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val mod_vec_nondet : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
 let mod_vec        l r = fromMaybe (repeat [BU] (length l)) (mod_bv l r)
 let mod_vec_maybe  l r = mod_bv l r
 let mod_vec_fail   l r = maybe_fail "mod_vec" (mod_bv l r)
-let mod_vec_oracle l r = of_bits_oracle (mod_vec l r)
+let mod_vec_nondet l r = of_bits_nondet (mod_vec l r)
 
 val quot_vec        : list bitU -> list bitU -> list bitU
 val quot_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
 val quot_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
-val quot_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val quot_vec_nondet : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
 let quot_vec        l r = fromMaybe (repeat [BU] (length l)) (quot_bv l r)
 let quot_vec_maybe  l r = quot_bv l r
 let quot_vec_fail   l r = maybe_fail "quot_vec" (quot_bv l r)
-let quot_vec_oracle l r = of_bits_oracle (quot_vec l r)
+let quot_vec_nondet l r = of_bits_nondet (quot_vec l r)
 
 val quots_vec        : list bitU -> list bitU -> list bitU
 val quots_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)
 val quots_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
-val quots_vec_oracle : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
+val quots_vec_nondet : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e
 let quots_vec        l r = fromMaybe (repeat [BU] (length l)) (quots_bv l r)
 let quots_vec_maybe  l r = quots_bv l r
 let quots_vec_fail   l r = maybe_fail "quots_vec" (quots_bv l r)
-let quots_vec_oracle l r = of_bits_oracle (quots_vec l r)
+let quots_vec_nondet l r = of_bits_nondet (quots_vec l r)
 
 val mod_vec_int        : list bitU -> integer -> list bitU
 val mod_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)
 val mod_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
-val mod_vec_int_oracle : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val mod_vec_int_nondet : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
 let mod_vec_int        l r = fromMaybe (repeat [BU] (length l)) (mod_bv_int l r)
 let mod_vec_int_maybe  l r = mod_bv_int l r
 let mod_vec_int_fail   l r = maybe_fail "mod_vec_int" (mod_bv_int l r)
-let mod_vec_int_oracle l r = of_bits_oracle (mod_vec_int l r)
+let mod_vec_int_nondet l r = of_bits_nondet (mod_vec_int l r)
 
 val quot_vec_int        : list bitU -> integer -> list bitU
 val quot_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)
 val quot_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
-val quot_vec_int_oracle : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
+val quot_vec_int_nondet : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e
 let quot_vec_int        l r = fromMaybe (repeat [BU] (length l)) (quot_bv_int l r)
 let quot_vec_int_maybe  l r = quot_bv_int l r
 let quot_vec_int_fail   l r = maybe_fail "quot_vec_int" (quot_bv_int l r)
-let quot_vec_int_oracle l r = of_bits_oracle (quot_vec_int l r)
+let quot_vec_int_nondet l r = of_bits_nondet (quot_vec_int l r)
 
 val replicate_bits : list bitU -> integer -> list bitU
 let replicate_bits = replicate_bits_bv
@@ -285,8 +285,8 @@ val duplicate : bitU -> integer -> list bitU
 let duplicate = duplicate_bit_bv
 let duplicate_maybe b n = Just (duplicate b n)
 let duplicate_fail b n = return (duplicate b n)
-let duplicate_oracle b n =
-  bool_of_bitU_oracle b >>= (fun b ->
+let duplicate_nondet b n =
+  bool_of_bitU_nondet b >>= (fun b ->
   return (duplicate (bitU_of_bool b) n))
 
 val reverse_endianness : list bitU -> list bitU
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index 1e4d63ba..61048ac5 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -10,21 +10,21 @@ open import Sail2_prompt
 let inline uint v = unsignedIntegerFromWord v
 let uint_maybe v = Just (uint v)
 let uint_fail v = return (uint v)
-let uint_oracle v = return (uint v)
+let uint_nondet v = return (uint v)
 
 let inline sint v = signedIntegerFromWord v
 let sint_maybe v = Just (sint v)
 let sint_fail v = return (sint v)
-let sint_oracle v = return (sint v)
+let sint_nondet v = return (sint v)
 
 val vec_of_bits_maybe    : forall 'a. Size 'a => list bitU -> maybe (mword 'a)
 val vec_of_bits_fail     : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
-val vec_of_bits_oracle   : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
+val vec_of_bits_nondet   : forall 'rv 'a 'e. Size 'a => list bitU -> monad 'rv (mword 'a) 'e
 val vec_of_bits_failwith : forall 'a. Size 'a => list bitU -> mword 'a
 val vec_of_bits          : forall 'a. Size 'a => list bitU -> mword 'a
 let vec_of_bits_maybe bits = of_bits bits
 let vec_of_bits_fail bits = of_bits_fail bits
-let vec_of_bits_oracle bits = of_bits_oracle bits
+let vec_of_bits_nondet bits = of_bits_nondet bits
 let vec_of_bits_failwith bits = of_bits_failwith bits
 let vec_of_bits bits = of_bits_failwith bits
 
@@ -38,8 +38,8 @@ let update_vec_dec_maybe w i b = update_mword_dec w i b
 let update_vec_dec_fail w i b =
   bool_of_bitU_fail b >>= (fun b ->
   return (update_mword_bool_dec w i b))
-let update_vec_dec_oracle w i b =
-  bool_of_bitU_oracle b >>= (fun b ->
+let update_vec_dec_nondet w i b =
+  bool_of_bitU_nondet b >>= (fun b ->
   return (update_mword_bool_dec w i b))
 let update_vec_dec w i b = maybe_failwith (update_vec_dec_maybe w i b)
 
@@ -47,8 +47,8 @@ let update_vec_inc_maybe w i b = update_mword_inc w i b
 let update_vec_inc_fail w i b =
   bool_of_bitU_fail b >>= (fun b ->
   return (update_mword_bool_inc w i b))
-let update_vec_inc_oracle w i b =
-  bool_of_bitU_oracle b >>= (fun b ->
+let update_vec_inc_nondet w i b =
+  bool_of_bitU_nondet b >>= (fun b ->
   return (update_mword_bool_inc w i b))
 let update_vec_inc w i b = maybe_failwith (update_vec_inc_maybe w i b)
 
@@ -89,21 +89,21 @@ val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> mword 'a -> mwo
 let cons_vec_bool b w = wordFromBitlist (b :: bitlistFromWord w)
 let cons_vec_maybe b w = Maybe.map (fun b -> cons_vec_bool b w) (bool_of_bitU b)
 let cons_vec_fail b w = bool_of_bitU_fail b >>= (fun b -> return (cons_vec_bool b w))
-let cons_vec_oracle b w = bool_of_bitU_oracle b >>= (fun b -> return (cons_vec_bool b w))
+let cons_vec_nondet b w = bool_of_bitU_nondet b >>= (fun b -> return (cons_vec_bool b w))
 let cons_vec b w = maybe_failwith (cons_vec_maybe b w)
 
 val vec_of_bool : forall 'a. Size 'a => integer -> bool -> mword 'a
 let vec_of_bool _ b = wordFromBitlist [b]
 let vec_of_bit_maybe len b = Maybe.map (vec_of_bool len) (bool_of_bitU b)
 let vec_of_bit_fail len b = bool_of_bitU_fail b >>= (fun b -> return (vec_of_bool len b))
-let vec_of_bit_oracle len b = bool_of_bitU_oracle b >>= (fun b -> return (vec_of_bool len b))
+let vec_of_bit_nondet len b = bool_of_bitU_nondet b >>= (fun b -> return (vec_of_bool len b))
 let vec_of_bit len b = maybe_failwith (vec_of_bit_maybe len b)
 
 val cast_bool_vec : bool -> mword ty1
 let cast_bool_vec b = vec_of_bool 1 b
 let cast_unit_vec_maybe b = vec_of_bit_maybe 1 b
 let cast_unit_vec_fail b = bool_of_bitU_fail b >>= (fun b -> return (cast_bool_vec b))
-let cast_unit_vec_oracle b = bool_of_bitU_oracle b >>= (fun b -> return (cast_bool_vec b))
+let cast_unit_vec_nondet b = bool_of_bitU_nondet b >>= (fun b -> return (cast_bool_vec b))
 let cast_unit_vec b = maybe_failwith (cast_unit_vec_maybe b)
 
 val msb : forall 'a. Size 'a => mword 'a -> bitU
@@ -176,25 +176,25 @@ val subs_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 let add_vec_bool        l r = arith_op_bv_bool integerAdd false l r
 let add_vec_bit_maybe   l r = Maybe.map (add_vec_bool l) (bool_of_bitU r)
 let add_vec_bit_fail    l r = bool_of_bitU_fail r >>= (fun r -> return (add_vec_bool l r))
-let add_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r))
+let add_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (add_vec_bool l r))
 let add_vec_bit         l r = maybe_failwith (add_vec_bit_maybe  l r)
 
 let adds_vec_bool       l r = arith_op_bv_bool integerAdd true  l r
 let adds_vec_bit_maybe  l r = Maybe.map (adds_vec_bool l) (bool_of_bitU r)
 let adds_vec_bit_fail   l r = bool_of_bitU_fail r >>= (fun r -> return (adds_vec_bool l r))
-let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r))
+let adds_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (adds_vec_bool l r))
 let adds_vec_bit        l r = maybe_failwith (adds_vec_bit_maybe l r)
 
 let sub_vec_bool        l r = arith_op_bv_bool integerMinus false l r
 let sub_vec_bit_maybe   l r = Maybe.map (sub_vec_bool l) (bool_of_bitU r)
 let sub_vec_bit_fail    l r = bool_of_bitU_fail r >>= (fun r -> return (sub_vec_bool l r))
-let sub_vec_bit_oracle  l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r))
+let sub_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (sub_vec_bool l r))
 let sub_vec_bit         l r = maybe_failwith (sub_vec_bit_maybe  l r)
 
 let subs_vec_bool       l r = arith_op_bv_bool integerMinus true  l r
 let subs_vec_bit_maybe  l r = Maybe.map (subs_vec_bool l) (bool_of_bitU r)
 let subs_vec_bit_fail   l r = bool_of_bitU_fail r >>= (fun r -> return (subs_vec_bool l r))
-let subs_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (subs_vec_bool l r))
+let subs_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (subs_vec_bool l r))
 let subs_vec_bit        l r = maybe_failwith (subs_vec_bit_maybe  l r)
 
 (* TODO
@@ -238,66 +238,66 @@ let rotr         = rotr_mword
 val mod_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val mod_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
 val mod_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
-val mod_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val mod_vec_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
 let mod_vec        l r = mod_mword l r
 let mod_vec_maybe  l r = mod_bv l r
 let mod_vec_fail   l r = maybe_fail "mod_vec" (mod_bv l r)
-let mod_vec_oracle l r =
+let mod_vec_nondet l r =
   match (mod_bv l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val quot_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val quot_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
 val quot_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
-val quot_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val quot_vec_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
 let quot_vec        l r = quot_mword l r
 let quot_vec_maybe  l r = quot_bv l r
 let quot_vec_fail   l r = maybe_fail "quot_vec" (quot_bv l r)
-let quot_vec_oracle l r =
+let quot_vec_nondet l r =
   match (quot_bv l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val quots_vec        : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val quots_vec_maybe  : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a)
 val quots_vec_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
-val quots_vec_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
+val quots_vec_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> mword 'a -> monad 'rv (mword 'a) 'e
 let quots_vec        l r = quots_mword l r
 let quots_vec_maybe  l r = quots_bv l r
 let quots_vec_fail   l r = maybe_fail "quots_vec" (quots_bv l r)
-let quots_vec_oracle l r =
+let quots_vec_nondet l r =
   match (quots_bv l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val mod_vec_int        : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val mod_vec_int_maybe  : forall 'a. Size 'a => mword 'a -> integer -> maybe (mword 'a)
 val mod_vec_int_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
-val mod_vec_int_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+val mod_vec_int_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
 let mod_vec_int        l r = mod_mword_int l r
 let mod_vec_int_maybe  l r = mod_bv_int l r
 let mod_vec_int_fail   l r = maybe_fail "mod_vec_int" (mod_bv_int l r)
-let mod_vec_int_oracle l r =
+let mod_vec_int_nondet l r =
   match (mod_bv_int l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val quot_vec_int        : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val quot_vec_int_maybe  : forall 'a. Size 'a => mword 'a -> integer -> maybe (mword 'a)
 val quot_vec_int_fail   : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
-val quot_vec_int_oracle : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
+val quot_vec_int_nondet : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv (mword 'a) 'e
 let quot_vec_int        l r = quot_mword_int l r
 let quot_vec_int_maybe  l r = quot_bv_int l r
 let quot_vec_int_fail   l r = maybe_fail "quot_vec_int" (quot_bv_int l r)
-let quot_vec_int_oracle l r =
+let quot_vec_int_nondet l r =
   match (quot_bv_int l r) with
     | Just w -> return w
-    | Nothing -> mword_oracle ()
+    | Nothing -> mword_nondet ()
   end
 
 val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
@@ -307,7 +307,7 @@ val duplicate_bool : forall 'a. Size 'a => bool -> integer -> mword 'a
 let duplicate_bool   b n = wordFromBitlist (repeat [b] n)
 let duplicate_maybe  b n = Maybe.map (fun b -> duplicate_bool b n) (bool_of_bitU b)
 let duplicate_fail   b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_bool b n))
-let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n))
+let duplicate_nondet b n = bool_of_bitU_nondet b >>= (fun b -> return (duplicate_bool b n))
 let duplicate        b n = maybe_failwith (duplicate_maybe b n)
 
 val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem
index 08a47052..e01cc051 100644
--- a/src/gen_lib/sail2_prompt.lem
+++ b/src/gen_lib/sail2_prompt.lem
@@ -51,31 +51,31 @@ let bool_of_bitU_fail = function
   | BU -> Fail "bool_of_bitU"
 end
 
-val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e
-let bool_of_bitU_oracle = function
+val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
+let bool_of_bitU_nondet = function
   | B0 -> return false
   | B1 -> return true
   | BU -> undefined_bool ()
 end
 
-val bools_of_bits_oracle : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
-let bools_of_bits_oracle bits =
+val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
+let bools_of_bits_nondet bits =
   foreachM bits []
     (fun b bools ->
-      bool_of_bitU_oracle b >>= (fun b ->
+      bool_of_bitU_nondet b >>= (fun b ->
       return (bools ++ [b])))
 
-val of_bits_oracle : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
-let of_bits_oracle bits =
-  bools_of_bits_oracle bits >>= (fun bs ->
+val of_bits_nondet : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
+let of_bits_nondet bits =
+  bools_of_bits_nondet bits >>= (fun bs ->
   return (of_bools bs))
 
 val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
 let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits)
 
-val mword_oracle : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
-let mword_oracle () =
-  bools_of_bits_oracle (repeat [BU] (integerFromNat size)) >>= (fun bs ->
+val mword_nondet : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
+let mword_nondet () =
+  bools_of_bits_nondet (repeat [BU] (integerFromNat size)) >>= (fun bs ->
   return (wordFromBitlist bs))
 
 val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
@@ -93,6 +93,16 @@ let rec untilM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then return vars else untilM vars cond body
 
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs =
+  (* Use sufficiently many undefined bits and convert into an index into the list *)
+  bools_of_bits_nondet (repeat [BU] (length_list xs)) >>= fun bs ->
+  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
+  match index xs idx with
+    | Just x -> return x
+    | Nothing -> Fail "internal_pick"
+  end
+
 (*let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 745589e2..78b1615e 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -29,6 +29,7 @@ type monad 'regval 'a 'e =
   | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
   (* Request to write register *)
   | Write_reg of register_name * 'regval * monad 'regval 'a 'e
+  (* Request to choose a Boolean, e.g. to resolve an undefined bit *)
   | Undefined of (bool -> monad 'regval 'a 'e)
   (* Print debugging or tracing information *)
   | Print of string * monad 'regval 'a 'e
diff --git a/src/gen_lib/sail2_state.lem b/src/gen_lib/sail2_state.lem
index 82ac35d8..f703dead 100644
--- a/src/gen_lib/sail2_state.lem
+++ b/src/gen_lib/sail2_state.lem
@@ -41,31 +41,31 @@ let bool_of_bitU_fail = function
   | BU -> failS "bool_of_bitU"
 end
 
-val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
-let bool_of_bitU_oracleS = function
+val bool_of_bitU_nondetS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_nondetS = function
   | B0 -> returnS false
   | B1 -> returnS true
   | BU -> undefined_boolS ()
 end
 
-val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
-let bools_of_bits_oracleS bits =
+val bools_of_bits_nondetS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
+let bools_of_bits_nondetS bits =
   foreachS bits []
     (fun b bools ->
-      bool_of_bitU_oracleS b >>$= (fun b ->
+      bool_of_bitU_nondetS b >>$= (fun b ->
       returnS (bools ++ [b])))
 
-val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
-let of_bits_oracleS bits =
-  bools_of_bits_oracleS bits >>$= (fun bs ->
+val of_bits_nondetS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_nondetS bits =
+  bools_of_bits_nondetS bits >>$= (fun bs ->
   returnS (of_bools bs))
 
 val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
 let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits)
 
-val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
-let mword_oracleS () =
-  bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
+val mword_nondetS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
+let mword_nondetS () =
+  bools_of_bits_nondetS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
   returnS (wordFromBitlist bs))
 
 
@@ -83,3 +83,13 @@ let rec untilS vars cond body s =
   (body vars >>$= (fun vars s' ->
   (cond vars >>$= (fun cond_val s'' ->
   if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
+
+val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e
+let internal_pickS xs =
+  (* Use sufficiently many undefined bits and convert into an index into the list *)
+  bools_of_bits_nondetS (repeat [BU] (length_list xs)) >>$= fun bs ->
+  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
+  match index xs idx with
+    | Just x -> returnS x
+    | Nothing -> failS "internal_pick"
+  end
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index f207699f..30b296cc 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -13,20 +13,15 @@ type sequential_state 'regs =
      memstate : memstate;
      tagstate : tagstate;
      write_ea : maybe (write_kind * integer * integer);
-     last_exclusive_operation_was_load : bool;
-     (* Random bool generator for use as an undefined bit oracle *)
-     next_bool : nat -> (bool * nat);
-     seed : nat |>
+     last_exclusive_operation_was_load : bool |>
 
-val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs
-let init_state regs o s =
+val init_state : forall 'regs. 'regs -> sequential_state 'regs
+let init_state regs =
   <| regstate = regs;
      memstate = Map.empty;
      tagstate = Map.empty;
      write_ea = Nothing;
-     last_exclusive_operation_was_load = false;
-     next_bool = o;
-     seed = s |>
+     last_exclusive_operation_was_load = false |>
 
 type ex 'e =
   | Failure of string
@@ -69,10 +64,7 @@ val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
 let failS msg s = {(Ex (Failure msg), s)}
 
 val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () =
-  readS (fun s -> s.next_bool (s.seed)) >>$= (fun (b, seed) ->
-  updateS (fun s -> <| s with seed = seed |>) >>$
-  returnS b)
+let undefined_boolS () = chooseS {false; true}
 
 val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
 let exitS () = failS "exit"
-- 
cgit v1.2.3


From 2529f5a65d70dfffe40ead73ae49aaa4d78fefb4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 7 Jul 2018 22:47:28 +0100
Subject: Add some syntactic sugar for Isabelle

---
 src/state.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/state.ml b/src/state.ml
index e788ab6a..245d450c 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -367,15 +367,15 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) =
     let id' = remove_trailing_underscores id in
     separate_map hardline string [
       "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\"";
+      "  \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = readS (" ^ id' ^ " \\<circ> regstate)\"";
       "  by (auto simp: liftState_read_reg_readS register_defs)";
       "";
       "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:";
-      "  \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
+      "  \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\"";
       "  by (auto simp: liftState_write_reg_updateS register_defs)"
     ]
   in
-  string "abbreviation \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
+  string "abbreviation liftS (\"\\<lbrakk>_\\<rbrakk>\\<^sub>S\") where \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^
   hardline ^^ hardline ^^
   register_defs ^^
   hardline ^^ hardline ^^
-- 
cgit v1.2.3


From 946898cca35080989e88c14d7d6028d580ee6836 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 7 Jul 2018 22:48:39 +0100
Subject: Add explanatory comment to guard rewriting

---
 src/rewrites.ml | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index c2bf0835..67fb807e 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1168,6 +1168,25 @@ let case_exp e t cs =
     (* let efr = union_effs (List.map effect_of_pexp ps) in *)
     fix_eff_exp (annot_exp (E_case (e,ps)) l env t)
 
+(* Rewrite guarded patterns into a combination of if-expressions and
+   unguarded pattern matches
+
+   Strategy:
+   - Split clauses into groups where the first pattern subsumes all the
+     following ones
+   - Translate the groups in reverse order, using the next group as a
+     fall-through target, if there is one
+   - Within a group,
+     - translate the sequence of clauses to an if-then-else cascade using the
+       guards as long as the patterns are equivalent modulo substitution, or
+     - recursively translate the remaining clauses to a pattern match if
+       there is a difference in the patterns.
+
+  TODO: Compare this more closely with the algorithm in the CPP'18 paper of
+  Spector-Zabusky et al, who seem to use the opposite grouping and merging
+  strategy to ours: group *mutually exclusive* clauses, and try to merge them
+  into a pattern match first instead of an if-then-else cascade.
+*)
 let rewrite_guarded_clauses l cs =
   let rec group fallthrough clauses =
     let add_clause (pat,cls,annot) c = (pat,cls @ [c],annot) in
-- 
cgit v1.2.3


From 4eab8dcb613e5eb07414930d715d8b9340fa99f9 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 7 Jul 2018 22:49:19 +0100
Subject: Tweak rewriting of literal patterns for Lem

---
 src/rewrites.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 67fb807e..481a1c25 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3324,8 +3324,15 @@ let rewrite_defs_mapping_patterns =
   in
   pexp_rewriters rewrite_pexp
 
+let rewrite_lit_lem (L_aux (lit, _)) = match lit with
+  | L_num _ | L_string _ | L_hex _ | L_bin _ | L_real _ -> true
+  | _ -> false
+
+let rewrite_no_strings (L_aux (lit, _)) = match lit with
+  | L_string _ -> false
+  | _ -> true
 
-let rewrite_defs_pat_lits =
+let rewrite_defs_pat_lits rewrite_lit =
   let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) =
     let guards = ref [] in
     let counter = ref 0 in
@@ -3333,7 +3340,7 @@ let rewrite_defs_pat_lits =
     let rewrite_pat = function
       (* HACK: ignore strings for now *)
       | P_lit (L_aux (L_string _, _)) as p_aux, p_annot -> P_aux (p_aux, p_annot)
-      | P_lit lit, p_annot ->
+      | P_lit lit, p_annot when rewrite_lit lit ->
          let env = env_of_annot p_annot in
          let typ = typ_of_annot p_annot in
          let id = mk_id ("p" ^ string_of_int !counter ^ "#") in
@@ -4004,7 +4011,7 @@ let rewrite_defs_lem = [
   ("remove_mapping_valspecs", remove_mapping_valspecs);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("mapping_builtins", rewrite_defs_mapping_patterns);
-  ("pat_lits", rewrite_defs_pat_lits);
+  ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
@@ -4042,7 +4049,7 @@ let rewrite_defs_ocaml = [
   ("realise_mappings", rewrite_defs_realise_mappings);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("mapping_builtins", rewrite_defs_mapping_patterns);
-  ("pat_lits", rewrite_defs_pat_lits);
+  ("pat_lits", rewrite_defs_pat_lits rewrite_no_strings);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
@@ -4064,7 +4071,7 @@ let rewrite_defs_c = [
   ("realise_mappings", rewrite_defs_realise_mappings);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("mapping_builtins", rewrite_defs_mapping_patterns);
-  ("pat_lits", rewrite_defs_pat_lits);
+  ("pat_lits", rewrite_defs_pat_lits rewrite_no_strings);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
-- 
cgit v1.2.3


From 3334e0f9de700ed918e5f8c461f8cf08d23e7fd3 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 7 Jul 2018 22:49:42 +0100
Subject: Fix bug in rewriting of try-catch-blocks with variable updates

---
 src/rewrites.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 481a1c25..fad1f4d2 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3539,11 +3539,12 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          let eff = union_eff_exps [c;e1;e2] in
          let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
          Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
-    | E_case (e1,ps) ->
-       (* after rewrite_defs_letbind_effects e1 needs no rewriting *)
+    | E_case (e1,ps) | E_try (e1, ps) ->
+       let is_case = match expaux with E_case _ -> true | _ -> false in
        let vars, varpats =
-         ps
-         |> List.map (fun (Pat_aux ((Pat_exp (_,e)|Pat_when (_,_,e)),_)) -> e)
+         (* for E_case, e1 needs no rewriting after rewrite_defs_letbind_effects *)
+         ((if is_case then [] else [e1]) @
+         List.map (fun (Pat_aux ((Pat_exp (_,e)|Pat_when (_,_,e)),_)) -> e) ps)
          |> List.map find_updated_vars
          |> List.fold_left IdSet.union IdSet.empty
          |> IdSet.inter used_vars
@@ -3554,8 +3555,10 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
              Pat_aux (Pat_exp (p,rewrite_var_updates e),a)
            | Pat_aux (Pat_when (p,g,e),a) ->
              Pat_aux (Pat_when (p,g,rewrite_var_updates e),a)) ps in
-         Same_vars (E_aux (E_case (e1,ps),annot))
+         let expaux = if is_case then E_case (e1, ps) else E_try (e1, ps) in
+         Same_vars (E_aux (expaux, annot))
        else
+         let e1 = if is_case then e1 else rewrite_var_updates (add_vars overwrite e1 vars) in
          let rewrite_pexp (Pat_aux (pexp, (l, _))) = match pexp with
            | Pat_exp (pat, exp) ->
              let exp = rewrite_var_updates (add_vars overwrite exp vars) in
@@ -3564,10 +3567,12 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
            | Pat_when _ ->
              raise (Reporting_basic.err_unreachable l
                "Guarded patterns should have been rewritten already") in
+         let ps = List.map rewrite_pexp ps in
+         let expaux = if is_case then E_case (e1, ps) else E_try (e1, ps) in
          let typ = match ps with
            | Pat_aux ((Pat_exp (_,first)|Pat_when (_,_,first)),_) :: _ -> typ_of first
            | _ -> unit_typ in
-         let v = fix_eff_exp (annot_exp (E_case (e1, List.map rewrite_pexp ps)) pl env typ) in
+         let v = fix_eff_exp (annot_exp expaux pl env typ) in
          Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
     | E_assign (lexp,vexp) ->
        let mk_id_pat id = match Env.lookup_id id env with
-- 
cgit v1.2.3


From 0bb45311868aff5ce34d29ec4b0a410bc1e319dd Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 9 Jul 2018 15:35:25 +0100
Subject: Coq: remove some unnecessary casts

---
 src/pretty_print_coq.ml | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index e68a6dd9..efcf3851 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -688,6 +688,27 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
   | Typ_app (id, _) -> id
   | _ -> raise (Reporting_basic.err_unreachable l "failed to get type id")
 
+(* TODO: maybe Nexp_exp, division? *)
+(* Evaluation of constant nexp subexpressions, because Coq will be able to do those itself *)
+let rec nexp_const_eval (Nexp_aux (n,l) as nexp) =
+  let binop f re l n1 n2 =
+  match nexp_const_eval n1, nexp_const_eval n2 with
+  | Nexp_aux (Nexp_constant c1,_), Nexp_aux (Nexp_constant c2,_) ->
+     Nexp_aux (Nexp_constant (f c1 c2),l)
+  | n1', n2' -> Nexp_aux (re n1' n2',l)
+  in
+  let unop f re l n1 =
+  match nexp_const_eval n1 with
+  | Nexp_aux (Nexp_constant c1,_) -> Nexp_aux (Nexp_constant (f c1),l)
+  | n1' -> Nexp_aux (re n1',l)
+  in
+  match n with
+  | Nexp_times (n1,n2) -> binop Big_int.mul (fun n1 n2 -> Nexp_times (n1,n2)) l n1 n2
+  | Nexp_sum (n1,n2) -> binop Big_int.add (fun n1 n2 -> Nexp_sum (n1,n2)) l n1 n2
+  | Nexp_minus (n1,n2) -> binop Big_int.sub (fun n1 n2 -> Nexp_minus (n1,n2)) l n1 n2
+  | Nexp_neg n1 -> unop Big_int.negate (fun n -> Nexp_neg n) l n1
+  | _ -> nexp
+
 (* Decide whether two nexps used in a vector size are similar; if not
    a cast will be inserted *)
 let similar_nexps n1 n2 =
@@ -707,7 +728,7 @@ let similar_nexps n1 n2 =
     | Nexp_neg n1, Nexp_neg n2
       -> same_nexp_shape n1 n2
     | _ -> false
-  in if same_nexp_shape n1 n2 then true else false
+  in if same_nexp_shape (nexp_const_eval n1) (nexp_const_eval n2) then true else false
 
 let constraint_fns = ["Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"]
 
-- 
cgit v1.2.3


From 936f1beb2bbc9db6182ba8b706668e146c3657d9 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 9 Jul 2018 16:30:06 +0100
Subject: Changes for anonymisation. Ensure headers are in correct format.
 Remove some redundant files.

---
 src/test/lib/run_test_interp.ml | 51 -----------------------------------------
 src/value2.lem                  |  4 ++--
 2 files changed, 2 insertions(+), 53 deletions(-)
 delete mode 100644 src/test/lib/run_test_interp.ml

(limited to 'src')

diff --git a/src/test/lib/run_test_interp.ml b/src/test/lib/run_test_interp.ml
deleted file mode 100644
index 5f2ace1b..00000000
--- a/src/test/lib/run_test_interp.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-(**************************************************************************)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*                                                                        *)
-(*  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 Interp_interface ;;
-open Interp_inter_imp ;;
-open Sail_impl_base ;;
-
-let doit () =
-  let context = build_context false Test_lem_ast.defs [] [] [] [] [] [] [] None [] in
-  translate_address context E_little_endian "run" None (address_of_integer (Nat_big_num.of_int 0));;
-
-doit () ;;
diff --git a/src/value2.lem b/src/value2.lem
index d9fd1263..e8a8262a 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -1,4 +1,4 @@
-(**************************************************************************)
+(*========================================================================*)
 (*     Sail                                                               *)
 (*                                                                        *)
 (*  Copyright (c) 2013-2017                                               *)
@@ -46,7 +46,7 @@
 (*  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 import Pervasives
 open import Assert_extra
-- 
cgit v1.2.3


From 53ce89769a10be9a47af72b5fb440afa74bb4d02 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 9 Jul 2018 18:48:17 +0100
Subject: Lem: prefer type variables to constants when looking for equivalent
 nexps If we have an nexp that we can't print, look for an equivalent type
 variable before looking for a constant - the constant may only be valid
 locally (e.g., under an if) while the type variable will be valid throughout
 the function. Fixes a problem with aget_Mem on aarch64.

---
 src/pretty_print_lem.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c872d420..9897bb7c 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -334,14 +334,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp = 
          Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       match Type_check.solve env size with
-       | Some n -> mk_typ (nconstant n)
-       | None ->
-          let is_equal nexp =
-            prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
-          in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
-          | nexp -> mk_typ nexp
-          | exception Not_found -> None
+       let is_equal nexp =
+         prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+       in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+       | nexp -> mk_typ nexp
+       | exception Not_found ->
+          match Type_check.solve env size with
+          | Some n -> mk_typ (nconstant n)
+          | None -> None
      end
   | _ -> None
 
-- 
cgit v1.2.3


From 85def9a2d488cc2d74394663f9f6323258e5fa59 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 9 Jul 2018 16:49:31 -0700
Subject: Initialize fresh memory to 0 in the OCaml backend. This makes it
 consistent with the C backend, and also makes it easier to compare traces
 across execution re-runs.

---
 src/sail_lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index ab621342..63260c17 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -419,7 +419,7 @@ let get_mem_page p =
   try
     Mem.find p !mem_pages
   with Not_found -> 
-    let new_page = Bytes.create page_size_bytes in
+    let new_page = Bytes.make page_size_bytes '\000' in
     mem_pages := Mem.add p new_page !mem_pages;
     new_page
 
-- 
cgit v1.2.3


From 58836205da846571afdb7994a9d5915f6fbae09f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 10 Jul 2018 11:40:28 +0100
Subject: Aarch64 mono script update

---
 src/gen_lib/sail2_values.lem | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src')

diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 0f384cab..003eedc7 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -53,6 +53,8 @@ val prerr_endline : string -> unit
 let prerr_endline _ = ()
 declare ocaml target_rep function prerr_endline = `prerr_endline`
 
+let prerr x = prerr_endline x
+
 val print_int : string -> integer -> unit
 let print_int msg i = print_endline (msg ^ (stringFromInteger i))
 
-- 
cgit v1.2.3


From 472097b3fb486d474a427427c1c38298a2ee1fc3 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Tue, 10 Jul 2018 15:00:25 +0100
Subject: disable printing when compiling to Lem to keep rmem happy

---
 src/gen_lib/sail2_values.lem | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 003eedc7..fd742fb1 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -47,7 +47,7 @@ let power_real b e = realPowInteger b e*)
 
 val print_endline : string -> unit
 let print_endline _ = ()
-declare ocaml target_rep function print_endline = `print_endline`
+(* declare ocaml target_rep function print_endline = `print_endline` *)
 
 val prerr_endline : string -> unit
 let prerr_endline _ = ()
-- 
cgit v1.2.3


From b34725b4d168984c505bb691735be96961499830 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 10 Jul 2018 15:48:17 +0100
Subject: Only put static qualifier on valspecs when -static flag is used

---
 src/c_backend.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index e92ca1a6..e4bbd393 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2519,12 +2519,13 @@ let codegen_def' ctx = function
      ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))
 
   | CDEF_spec (id, arg_ctyps, ret_ctyp) ->
+     let static = if !opt_static then "static " else "" in
      if Env.is_extern id ctx.tc_env "c" then
        empty
      else if is_stack_ctyp ret_ctyp then
-       string (Printf.sprintf "static %s %s(%s);" (sgen_ctyp ret_ctyp) (sgen_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
      else
-       string (Printf.sprintf "static void %s(%s *rop, %s);" (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
 
   | CDEF_fundef (id, ret_arg, args, instrs) as def ->
      if !opt_ddump_flow_graphs then make_dot id (instrs_graph instrs) else ();
@@ -2566,7 +2567,8 @@ let codegen_def' ctx = function
      codegen_type_def ctx ctype_def
 
   | CDEF_startup (id, instrs) ->
-     let startup_header = string (Printf.sprintf "static void startup_%s(void)" (sgen_id id)) in
+     let static = if !opt_static then "static " else "" in
+     let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_id id)) in
      separate_map hardline codegen_decl instrs
      ^^ twice hardline
      ^^ startup_header ^^ hardline
@@ -2575,7 +2577,8 @@ let codegen_def' ctx = function
      ^^ string "}"
 
   | CDEF_finish (id, instrs) ->
-     let finish_header = string (Printf.sprintf "static void finish_%s(void)" (sgen_id id)) in
+     let static = if !opt_static then "static " else "" in
+     let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_id id)) in
      separate_map hardline codegen_decl (List.filter is_decl instrs)
      ^^ twice hardline
      ^^ finish_header ^^ hardline
-- 
cgit v1.2.3


From 115c33129aa7dc3f0f0f6232c8e5fd892c79eb87 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Tue, 10 Jul 2018 16:35:18 +0100
Subject: fix constructor typo

---
 src/lem_interp/sail2_instr_kinds.lem | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index 938b693d..3d238676 100644
--- a/src/lem_interp/sail2_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
@@ -219,7 +219,7 @@ instance (Show instruction_kind)
     | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
     | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
     | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
-    | IK_branch               -> "IK_branch"
+    | IK_branch ()            -> "IK_branch"
     | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
     | IK_simple ()            -> "IK_simple"
   end
-- 
cgit v1.2.3


From d559aefa947c53f84a6aeb2dc67106a21d4cfb68 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 10 Jul 2018 22:44:27 +0100
Subject: Fix some signedness bugs

add_vec_int and similar functions in the Lem library used unsigned instead of
signed conversion.
---
 src/gen_lib/sail2_operators_bitlists.lem | 38 +++++++++++---------------------
 src/gen_lib/sail2_operators_mwords.lem   | 38 +++++++++++---------------------
 2 files changed, 26 insertions(+), 50 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 0c833e90..b9a2fa86 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -145,31 +145,19 @@ let subs_vec  = arith_op_bv integerMinus true
 let mult_vec  = arith_op_double_bl integerMult false
 let mults_vec = arith_op_double_bl integerMult true
 
-val add_vec_int       : list bitU -> integer -> list bitU
-val adds_vec_int      : list bitU -> integer -> list bitU
-val sub_vec_int       : list bitU -> integer -> list bitU
-val subs_vec_int      : list bitU -> integer -> list bitU
-val mult_vec_int      : list bitU -> integer -> list bitU
-val mults_vec_int     : list bitU -> integer -> list bitU
-let add_vec_int   l r = arith_op_bv_int integerAdd false l r
-let adds_vec_int  l r = arith_op_bv_int integerAdd true l r
-let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
-let subs_vec_int  l r = arith_op_bv_int integerMinus true l r
-let mult_vec_int  l r = arith_op_double_bl integerMult false l (of_int (length l) r)
-let mults_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r)
-
-val add_int_vec       : integer -> list bitU -> list bitU
-val adds_int_vec      : integer -> list bitU -> list bitU
-val sub_int_vec       : integer -> list bitU -> list bitU
-val subs_int_vec      : integer -> list bitU -> list bitU
-val mult_int_vec      : integer -> list bitU -> list bitU
-val mults_int_vec     : integer -> list bitU -> list bitU
-let add_int_vec   l r = arith_op_int_bv integerAdd false l r
-let adds_int_vec  l r = arith_op_int_bv integerAdd true l r
-let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
-let subs_int_vec  l r = arith_op_int_bv integerMinus true l r
-let mult_int_vec  l r = arith_op_double_bl integerMult false (of_int (length r) l) r
-let mults_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r
+val add_vec_int      : list bitU -> integer -> list bitU
+val sub_vec_int      : list bitU -> integer -> list bitU
+val mult_vec_int     : list bitU -> integer -> list bitU
+let add_vec_int  l r = arith_op_bv_int integerAdd true l r
+let sub_vec_int  l r = arith_op_bv_int integerMinus true l r
+let mult_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r)
+
+val add_int_vec      : integer -> list bitU -> list bitU
+val sub_int_vec      : integer -> list bitU -> list bitU
+val mult_int_vec     : integer -> list bitU -> list bitU
+let add_int_vec  l r = arith_op_int_bv integerAdd true l r
+let sub_int_vec  l r = arith_op_int_bv integerMinus true l r
+let mult_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r
 
 val add_vec_bit      : list bitU -> bitU -> list bitU
 val adds_vec_bit     : list bitU -> bitU -> list bitU
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index 61048ac5..c0b7f2d1 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -142,31 +142,19 @@ let subs_vec  l r = arith_op_bv integerMinus true  l r
 let mult_vec  l r = arith_op_bv integerMult  false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b)
 let mults_vec l r = arith_op_bv integerMult  true  (signExtend l : mword 'b) (signExtend r : mword 'b)
 
-val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val adds_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val subs_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-let add_vec_int   l r = arith_op_bv_int integerAdd   false l r
-let adds_vec_int  l r = arith_op_bv_int integerAdd   true  l r
-let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
-let subs_vec_int  l r = arith_op_bv_int integerMinus true  l r
-let mult_vec_int  l r = arith_op_bv_int integerMult  false (zeroExtend l : mword 'b) r
-let mults_vec_int l r = arith_op_bv_int integerMult  true  (signExtend l : mword 'b) r
-
-val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val adds_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val subs_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
-val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
-let add_int_vec   l r = arith_op_int_bv integerAdd   false l r
-let adds_int_vec  l r = arith_op_int_bv integerAdd   true  l r
-let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
-let subs_int_vec  l r = arith_op_int_bv integerMinus true  l r
-let mult_int_vec  l r = arith_op_int_bv integerMult  false l (zeroExtend r : mword 'b)
-let mults_int_vec l r = arith_op_int_bv integerMult  true  l (signExtend r : mword 'b)
+val add_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sub_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let add_vec_int  l r = arith_op_bv_int integerAdd   true  l r
+let sub_vec_int  l r = arith_op_bv_int integerMinus true  l r
+let mult_vec_int l r = arith_op_bv_int integerMult  true  (signExtend l : mword 'b) r
+
+val add_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sub_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let add_int_vec  l r = arith_op_int_bv integerAdd   true  l r
+let sub_int_vec  l r = arith_op_int_bv integerMinus true  l r
+let mult_int_vec l r = arith_op_int_bv integerMult  true  l (signExtend r : mword 'b)
 
 val add_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
-- 
cgit v1.2.3


From 7e79a2adde6a75e33973a1cd559f85a47551b18a Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 11 Jul 2018 12:59:59 +0100
Subject: Partially revert change to add_vec_int et al

On second thought, this change should not really make a difference; the CHERI
test suite still passes without it.  Moreover, using unsigned conversion of the
vector argument leads to more convenient lemmas for the provers.
---
 src/gen_lib/sail2_operators_bitlists.lem | 26 +++++++++++++-------------
 src/gen_lib/sail2_operators_mwords.lem   | 26 +++++++++++++-------------
 2 files changed, 26 insertions(+), 26 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index b9a2fa86..186e0a09 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -145,19 +145,19 @@ let subs_vec  = arith_op_bv integerMinus true
 let mult_vec  = arith_op_double_bl integerMult false
 let mults_vec = arith_op_double_bl integerMult true
 
-val add_vec_int      : list bitU -> integer -> list bitU
-val sub_vec_int      : list bitU -> integer -> list bitU
-val mult_vec_int     : list bitU -> integer -> list bitU
-let add_vec_int  l r = arith_op_bv_int integerAdd true l r
-let sub_vec_int  l r = arith_op_bv_int integerMinus true l r
-let mult_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r)
-
-val add_int_vec      : integer -> list bitU -> list bitU
-val sub_int_vec      : integer -> list bitU -> list bitU
-val mult_int_vec     : integer -> list bitU -> list bitU
-let add_int_vec  l r = arith_op_int_bv integerAdd true l r
-let sub_int_vec  l r = arith_op_int_bv integerMinus true l r
-let mult_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r
+val add_vec_int       : list bitU -> integer -> list bitU
+val sub_vec_int       : list bitU -> integer -> list bitU
+val mult_vec_int      : list bitU -> integer -> list bitU
+let add_vec_int   l r = arith_op_bv_int integerAdd false l r
+let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
+let mult_vec_int  l r = arith_op_double_bl integerMult false l (of_int (length l) r)
+
+val add_int_vec       : integer -> list bitU -> list bitU
+val sub_int_vec       : integer -> list bitU -> list bitU
+val mult_int_vec      : integer -> list bitU -> list bitU
+let add_int_vec   l r = arith_op_int_bv integerAdd false l r
+let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
+let mult_int_vec  l r = arith_op_double_bl integerMult false (of_int (length r) l) r
 
 val add_vec_bit      : list bitU -> bitU -> list bitU
 val adds_vec_bit     : list bitU -> bitU -> list bitU
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index c0b7f2d1..a7fb7c50 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -142,19 +142,19 @@ let subs_vec  l r = arith_op_bv integerMinus true  l r
 let mult_vec  l r = arith_op_bv integerMult  false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b)
 let mults_vec l r = arith_op_bv integerMult  true  (signExtend l : mword 'b) (signExtend r : mword 'b)
 
-val add_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val sub_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-let add_vec_int  l r = arith_op_bv_int integerAdd   true  l r
-let sub_vec_int  l r = arith_op_bv_int integerMinus true  l r
-let mult_vec_int l r = arith_op_bv_int integerMult  true  (signExtend l : mword 'b) r
-
-val add_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val sub_int_vec  : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
-let add_int_vec  l r = arith_op_int_bv integerAdd   true  l r
-let sub_int_vec  l r = arith_op_int_bv integerMinus true  l r
-let mult_int_vec l r = arith_op_int_bv integerMult  true  l (signExtend r : mword 'b)
+val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sub_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val mult_vec_int  : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let add_vec_int   l r = arith_op_bv_int integerAdd   false l r
+let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
+let mult_vec_int  l r = arith_op_bv_int integerMult  false (zeroExtend l : mword 'b) r
+
+val add_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sub_int_vec   : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val mult_int_vec  : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+let add_int_vec   l r = arith_op_int_bv integerAdd   false l r
+let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
+let mult_int_vec  l r = arith_op_int_bv integerMult  false l (zeroExtend r : mword 'b)
 
 val add_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
 val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a
-- 
cgit v1.2.3


From 2a89faec667fdf24b93360d3da5f14eab161983b Mon Sep 17 00:00:00 2001
From: Jon French
Date: Wed, 11 Jul 2018 18:13:15 +0100
Subject: RISC-V model fixes for RMEM

---
 src/sail_lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 63260c17..16b1d3cc 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -457,7 +457,7 @@ let write_ram' (data_size, addr, data) =
   end
 
 let write_ram (addr_size, data_size, hex_ram, addr, data) =
-  write_ram' (data_size, uint addr, data)
+  write_ram' (data_size, uint addr, data); true
 
 let wram addr byte =
   let bytes = Bytes.make 1 (char_of_int byte) in
-- 
cgit v1.2.3


From e3e2f7137be43771aace42694c8d5112f6849039 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 12 Jul 2018 00:37:54 +0100
Subject: Fixes for ARM Sail tests, and get_time_ns for interpreter

---
 src/value.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src')

diff --git a/src/value.ml b/src/value.ml
index 41b52720..1d2346af 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -561,6 +561,7 @@ let primops =
       ("write_ram", value_write_ram);
       ("trace_memory_read", fun _ -> V_unit);
       ("trace_memory_write", fun _ -> V_unit);
+      ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns()));
       ("load_raw", value_load_raw);
       ("to_real", value_to_real);
       ("eq_real", value_eq_real);
-- 
cgit v1.2.3


From d4c2a2d51e16cf483c67dfc4d589ded9a2e29417 Mon Sep 17 00:00:00 2001
From: Shaked Flur
Date: Thu, 12 Jul 2018 09:19:01 +0100
Subject: Minor fix to support OCaml 4.02.3

---
 src/gen_lib/sail2_string.lem | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index d0e40ad4..ba3a2d51 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -31,7 +31,7 @@ let string_append = stringAppend
 
 val maybeIntegerOfString : string -> maybe integer
 let maybeIntegerOfString _ = Nothing (* TODO FIXME *)
-declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string_opt s with None -> None | Some i -> Some (Nat_big_num.of_int i))`
+declare ocaml target_rep function maybeIntegerOfString = `(fun s -> match int_of_string s with i -> Some (Nat_big_num.of_int i) | exception Failure _ -> None )`
 
 (***********************************************
  * end stuff that should be in Lem Num_extra   *
-- 
cgit v1.2.3


From 870f918d3f6e3e9ed8c8367ce19d1991a8bf40b7 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 11 Jul 2018 20:32:22 +0100
Subject: Fix bug for large integers in OCaml compilation

---
 src/c_backend.ml     |  3 ++-
 src/ocaml_backend.ml | 15 +++++++++++----
 src/rewrites.ml      |  1 +
 3 files changed, 14 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index e4bbd393..cb732e2d 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2655,7 +2655,8 @@ let instrument_tracing ctx =
   let module StringSet = Set.Make(String) in
   let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in
   let rec instrument = function
-    | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs ->
+    | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs when not (Env.is_extern id ctx.tc_env "c") ->
+
        let trace_start =
          iraw (Printf.sprintf "trace_start(\"%s\");" (String.escaped (string_of_id id)))
        in
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 5ffb1647..236c4222 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -167,10 +167,13 @@ let ocaml_lit (L_aux (lit_aux, _)) =
   | L_one -> string "B1"
   | L_true -> string "true"
   | L_false -> string "false"
-  | L_num n -> if Big_int.equal n Big_int.zero
-               then string "Big_int.zero"
-               else parens (string "Big_int.of_int" ^^ space
-                            ^^ string "(" ^^ string (Big_int.to_string n) ^^ string ")")
+  | L_num n ->
+     if Big_int.equal n Big_int.zero then
+       string "Big_int.zero"
+     else if Big_int.less_equal (Big_int.of_int min_int) n && Big_int.less_equal n (Big_int.of_int max_int) then
+       parens (string "Big_int.of_int" ^^ space ^^ parens (string (Big_int.to_string n)))
+     else
+       parens (string "Big_int.of_string" ^^ space ^^ dquotes (string (Big_int.to_string n)))
   | L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
   | L_string str -> string_lit str
   | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str)))
@@ -389,6 +392,10 @@ let ocaml_dec_spec ctx (DEC_aux (reg, _)) =
      separate space [string "let"; zencode ctx id; colon;
                      parens (ocaml_typ ctx typ); string "ref"; equals;
                      string "ref"; parens (ocaml_exp ctx (initial_value_for id ctx.register_inits))]
+  | DEC_config (id, typ, exp) ->
+     separate space [string "let"; zencode ctx id; colon;
+                     parens (ocaml_typ ctx typ); string "ref"; equals;
+                     string "ref"; parens (ocaml_exp ctx exp)]
   | _ -> failwith "Unsupported register declaration"
 
 let first_function = ref true
diff --git a/src/rewrites.ml b/src/rewrites.ml
index fad1f4d2..8fe30d6b 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2304,6 +2304,7 @@ let rewrite_type_def_typs rw_typ rw_typquant rw_typschm (TD_aux (td, annot)) =
 let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) =
   match ds with
   | DEC_reg (typ, id) -> DEC_aux (DEC_reg (rw_typ typ, id), annot)
+  | DEC_config (id, typ, exp) -> DEC_aux (DEC_config (id, rw_typ typ, exp), annot)
   | _ -> assert false
 
 (* Remove overload definitions and cast val specs from the
-- 
cgit v1.2.3


From fb33182ec89cfc4307ce5f04aa5e46d1c3c2716d Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 12 Jul 2018 12:35:48 +0100
Subject: Coq: more accurate autocast insertion

---
 src/pretty_print_coq.ml | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index efcf3851..e57238f6 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -991,10 +991,21 @@ let doc_exp_lem, doc_let_lem =
               | _, _ -> arg_pp
             in
             let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in
-            (* Unpack existential result *)
-            let inst = instantiation_of full_exp in
-            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
-            let ret_typ_inst = subst_unifiers inst ret_typ in
+            (* Decide whether to unpack an existential result, pack one, or cast.
+               To do this we compare the expected type stored in the checked expression
+               with the inferred type. *)
+            let ret_typ_inst =
+              match infer_exp (env_of full_exp) (strip_exp full_exp) with
+              | typed_exp -> typ_of typed_exp
+              (* Not all function applications can be inferred, so try falling back to the
+                 type inferred when we know the target type.
+                 TODO: there are probably some edge cases where this won't pick up a need
+                 to cast. *)
+              | exception _ ->
+                 let inst = instantiation_of full_exp in
+                 let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+                 subst_unifiers inst ret_typ
+            in
             let unpack,build_ex,autocast =
               let ann_typ = Env.expand_synonyms env (typ_of_annot (l,annot)) in
               let ann_typ = expand_range_type ann_typ in
-- 
cgit v1.2.3


From 4f939658df5f45026d42491b8bf78aaa44f76e7b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 12 Jul 2018 13:41:07 +0100
Subject: Coq: tuple matching in loops

---
 src/pretty_print_coq.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index e57238f6..6cb97d5b 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -879,7 +879,7 @@ let doc_exp_lem, doc_let_lem =
                      when not (IdSet.mem (mk_id "varstup") used_vars_body)->
                       separate space [string "fun"; doc_id loopvar; string "_"; string "varstup"; bigarrow]
                       ^^ break 1 ^^
-                      separate space [string "let"; expY vartuple; string ":= varstup in"]
+                      separate space [string "let"; squote ^^ expY vartuple; string ":= varstup in"]
                    | E_aux (E_lit (L_aux (L_unit, _)), _)
                      when not (IdSet.mem (mk_id "unit_var") used_vars_body) ->
                       separate space [string "fun"; doc_id loopvar; string "_"; string "unit_var"; bigarrow]
@@ -918,7 +918,7 @@ let doc_exp_lem, doc_let_lem =
                    | E_aux (E_tuple _, _)
                      when not (IdSet.mem (mk_id "varstup") used_vars_body)->
                       separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^
-                      separate space [string "let"; expY varstuple; string ":= varstup in"]
+                      separate space [string "let"; squote ^^ expY varstuple; string ":= varstup in"]
                    | E_aux (E_lit (L_aux (L_unit, _)), _)
                      when not (IdSet.mem (mk_id "unit_var") used_vars_body) ->
                       separate space [string "fun unit_var"; bigarrow]
-- 
cgit v1.2.3


From f3d480d3fee8c28c1dd1975117149ddcd47d989f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 12 Jul 2018 14:45:34 +0100
Subject: Coq: more autocast insertion

---
 src/pretty_print_coq.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 6cb97d5b..8c345cd6 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -711,12 +711,11 @@ let rec nexp_const_eval (Nexp_aux (n,l) as nexp) =
 
 (* Decide whether two nexps used in a vector size are similar; if not
    a cast will be inserted *)
-let similar_nexps n1 n2 =
+let similar_nexps env n1 n2 =
   let rec same_nexp_shape (Nexp_aux (n1,_)) (Nexp_aux (n2,_)) =
     match n1, n2 with
-    | Nexp_id _, Nexp_id _
-    | Nexp_var _, Nexp_var _
-      -> true
+    | Nexp_id _, Nexp_id _ -> true
+    | Nexp_var k1, Nexp_var k2 -> prove env (nc_eq (nvar k1) (nvar k2))
     | Nexp_constant c1, Nexp_constant c2 -> Nat_big_num.equal c1 c2
     | Nexp_app (f1,args1), Nexp_app (f2,args2) ->
        Id.compare f1 f2 == 0 && List.for_all2 same_nexp_shape args1 args2
@@ -995,7 +994,7 @@ let doc_exp_lem, doc_let_lem =
                To do this we compare the expected type stored in the checked expression
                with the inferred type. *)
             let ret_typ_inst =
-              match infer_exp (env_of full_exp) (strip_exp full_exp) with
+              match infer_exp env (strip_exp full_exp) with
               | typed_exp -> typ_of typed_exp
               (* Not all function applications can be inferred, so try falling back to the
                  type inferred when we know the target type.
@@ -1026,7 +1025,7 @@ let doc_exp_lem, doc_let_lem =
                 match in_typ, out_typ with
                 | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_),
                   Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) ->
-                   not (similar_nexps n1 n2)
+                   not (similar_nexps env n1 n2)
                 | _ -> false
               in unpack,build_ex,autocast
             in
-- 
cgit v1.2.3


From 3e8afd335d1648b700fa04c80312326aec49c9c0 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 12 Jul 2018 15:36:33 +0100
Subject: Coq: handle all bool conjunctions/disjunctions

---
 src/pretty_print_coq.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 8c345cd6..28289241 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -152,10 +152,12 @@ let rec fix_id remove_tick name = match name with
        ("v" ^ name ^ "'")
      else name
 
-let doc_id (Id_aux(i,_)) =
+let string_id (Id_aux(i,_)) =
   match i with
-  | Id i -> string (fix_id false i)
-  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+  | Id i -> fix_id false i
+  | DeIid x -> Util.zencode_string ("op " ^ x)
+
+let doc_id id = string (string_id id)
 
 let doc_id_type (Id_aux(i,_)) =
   match i with
@@ -729,7 +731,7 @@ let similar_nexps env n1 n2 =
     | _ -> false
   in if same_nexp_shape (nexp_const_eval n1) (nexp_const_eval n2) then true else false
 
-let constraint_fns = ["Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"]
+let constraint_fns = ["Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"; "neq_atom"]
 
 let condition_produces_constraint exp =
   (* Cheat a little - this isn't quite the right environment for subexpressions
@@ -739,9 +741,10 @@ let condition_produces_constraint exp =
     { (Rewriter.pure_exp_alg false (||)) with
       Rewriter.e_app = fun (f,bs) ->
         List.exists (fun x -> x) bs ||
-        (Env.is_extern f env "coq" &&
-           let f' = Env.get_extern f env "coq" in
-           List.exists (fun id -> String.compare f' id == 0) constraint_fns)
+        (let name = if Env.is_extern f env "coq"
+          then Env.get_extern f env "coq"
+          else string_id f in
+         List.exists (fun id -> String.compare name id == 0) constraint_fns)
     } exp
 
 let prefix_recordtype = true
-- 
cgit v1.2.3


From 06c20157840425fb367feb186f009858a3a00448 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 12 Jul 2018 15:52:40 +0100
Subject: Coq: get rid of syntax error on exception handling

---
 src/pretty_print_coq.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 28289241..52ecc715 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1179,7 +1179,8 @@ let doc_exp_lem, doc_let_lem =
        if effectful (effect_of e) then
          let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in
          let epp =
-           group ((separate space [string try_catch; expY e; string "(function "]) ^/^
+           (* TODO capture avoidance for __catch_val *)
+           group ((separate space [string try_catch; expY e; string "(fun __catch_val => match __catch_val with "]) ^/^
                     (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^
                       (string "end)")) in
          if aexp_needed then parens (align epp) else align epp
-- 
cgit v1.2.3


From 79ecf8b83b06a6bd1330e1f243826cbe951a9e7d Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 12 Jul 2018 15:54:11 +0100
Subject: update arm and mips models for new type of write_ram builtin. Also
 fix c and interpreter implementations of same.

---
 src/value.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/value.ml b/src/value.ml
index 1d2346af..dccb216e 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -406,8 +406,8 @@ let value_read_ram = function
 
 let value_write_ram = function
   | [v1; v2; v3; v4; v5] ->
-     Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5);
-     V_unit
+     let b = Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5) in
+     V_bool(b)
   | _ -> failwith "value write_ram"
 
 let value_load_raw = function
-- 
cgit v1.2.3


From d482dcd0152b1f44faf1ad3b1ae06c029a048dab Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 12 Jul 2018 16:14:13 +0100
Subject: Handle failures during interpreting better

Changes to the interpreter to better support constant folding during
compilation mean it can now throw exceptions to the caller, allow the
caller to handle the error, rather than simply printing an error. This
broke the ARM interpreter test because exit() is handled by throwing
an Exit exception in the interpreter.
---
 src/isail.ml | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/isail.ml b/src/isail.ml
index 593167f9..4adc1cd2 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -127,7 +127,12 @@ let rec run () =
           print_endline ("Result = " ^ Value.string_of_value v);
           current_mode := Normal
        | Step (out, state, _, stack) ->
-          current_mode := Evaluation (eval_frame !interactive_ast frame);
+          begin
+            try
+              current_mode := Evaluation (eval_frame !interactive_ast frame)
+            with
+            | Failure str -> print_endline str; current_mode := Normal
+          end;
           run ()
        | Break frame ->
           print_endline "Breakpoint";
@@ -147,7 +152,12 @@ let rec run_steps n =
           print_endline ("Result = " ^ Value.string_of_value v);
           current_mode := Normal
        | Step (out, state, _, stack) ->
-          current_mode := Evaluation (eval_frame !interactive_ast frame);
+          begin
+            try
+              current_mode := Evaluation (eval_frame !interactive_ast frame)
+            with
+            | Failure str -> print_endline str; current_mode := Normal
+          end;
           run_steps (n - 1)
        | Break frame ->
           print_endline "Breakpoint";
@@ -352,9 +362,14 @@ let handle_input' input =
                print_endline ("Result = " ^ Value.string_of_value v);
                current_mode := Normal
             | Step (out, state, _, stack) ->
-               interactive_state := state;
-               current_mode := Evaluation (eval_frame !interactive_ast frame);
-               print_program ()
+               begin
+                 try
+                   interactive_state := state;
+                   current_mode := Evaluation (eval_frame !interactive_ast frame);
+                   print_program ()
+                 with
+                 | Failure str -> print_endline str; current_mode := Normal
+               end
             | Break frame ->
                print_endline "Breakpoint";
                current_mode := Evaluation frame
-- 
cgit v1.2.3


From 6586abcc185fa4e0f3853a73d91f097fbde16aca Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 13 Jul 2018 10:14:57 +0100
Subject: Coq: avoid a couple of common identifiers

---
 src/pretty_print_coq.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 52ecc715..aaef83cb 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -135,6 +135,8 @@ let rec fix_id remove_tick name = match name with
   | "GT"
   | "EQ"
   | "Z"
+  | "O"
+  | "S"
   | "mod"
   | "M"
     -> name ^ "'"
-- 
cgit v1.2.3


From a48dad8232a7db82c74a72157249a27ce25d326e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 16 Jul 2018 15:59:23 +0100
Subject: Coq: add support for more complex atom types As a result, add proof
 to pow2.

---
 src/pretty_print_coq.ml | 47 +++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 41 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index aaef83cb..95b3fb68 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -749,6 +749,28 @@ let condition_produces_constraint exp =
          List.exists (fun id -> String.compare name id == 0) constraint_fns)
     } exp
 
+(* For most functions whose return types are non-trivial atoms we return a
+   dependent pair with a proof that the result is the expected integer.  This
+   is redundant for basic arithmetic functions and functions which we unfold
+   in the constraint solver. *)
+let no_Z_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"]
+
+let is_no_Z_proof_fn env id =
+  if Env.is_extern id env "coq"
+  then
+    let s = Env.get_extern id env "coq" in
+    List.exists (fun x -> String.compare x s == 0) no_Z_proof_fns
+  else false
+
+let replace_atom_return_type ret_typ =
+  (* TODO: more complex uses of atom *)
+  match ret_typ with
+  | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) ->
+     let kid = mk_kid "_retval" in (* TODO: collision avoidance *)
+     true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Generated l)
+  | _ -> false, ret_typ
+
+
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
@@ -1014,6 +1036,9 @@ let doc_exp_lem, doc_let_lem =
               let ann_typ = Env.expand_synonyms env (typ_of_annot (l,annot)) in
               let ann_typ = expand_range_type ann_typ in
               let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in
+              let ret_typ_inst =
+                if is_no_Z_proof_fn env f then ret_typ_inst
+                else snd (replace_atom_return_type ret_typ_inst) in
               let unpack, build_ex, in_typ, out_typ =
                 match ret_typ_inst, ann_typ with
                 | Typ_aux (Typ_exist (_,_,t1),_), Typ_aux (Typ_exist (_,_,t2),_) ->
@@ -1497,17 +1522,23 @@ let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) =
       E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann)
   else (pat,typ), fun e -> e
 
-(* Ideally we'd remove the duplication between type variables and atom
-   arguments, but for now we just add an equality constraint. *)
+(* Add equality constraints between arguments and nexps, except in the case
+   that they've been merged. *)
 
 let atom_constraint ctxt (pat, typ) =
   let typ = Env.base_typ_of (pat_env_of pat) typ in
   match pat, typ with
   | P_aux (P_id id, _),
       Typ_aux (Typ_app (Id_aux (Id "atom",_),
-                        [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_) ->
-     Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
-                               parens (doc_op equals (doc_id id) (doc_var_lem ctxt kid))))
+                        [Typ_arg_aux (Typ_arg_nexp nexp,_)]),_) ->
+     (match nexp with
+       (* When the kid is mapped to the id, we don't need a constraint *)
+     | Nexp_aux (Nexp_var kid,_)
+         when (try Id.compare (KBindings.find kid ctxt.kid_id_renames) id == 0 with _ -> false) ->
+           None
+     | _ ->
+        Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
+                                  parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp)))))
   | _ -> None
 
 let all_ids pexp =
@@ -1616,6 +1647,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let patspp = separate_map space doc_binder pats in
   let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in
   let atom_constr_pp = separate space atom_constrs in
+  let build_ex, ret_typ = replace_atom_return_type ret_typ in
   let retpp =
     if effectful eff
     then string "M" ^^ space ^^ parens (doc_typ ctxt ret_typ)
@@ -1639,10 +1671,12 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     | _ ->
        raise (Reporting_basic.err_unreachable l
                 "guarded pattern expression should have been rewritten before pretty-printing") in
+  let bodypp = doc_fun_body ctxt exp in
+  let bodypp = if build_ex then string "build_ex" ^^ space ^^ parens bodypp else bodypp in
   group (prefix 3 1
     (separate space ([idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp]) ^/^
        separate space [colon; retpp; coloneq])
-    (doc_fun_body ctxt exp ^^ dot)) ^^ implicitargs
+    (bodypp ^^ dot)) ^^ implicitargs
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -1769,6 +1803,7 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
        | _ -> parens (underscore ^^ string " : " ^^ doc_typ empty_ctxt typ)
      in
      let arg_typs_pp = separate space (List.map doc_typ' typs) in
+     let _, ret_ty = replace_atom_return_type ret_ty in
      let ret_typ_pp = doc_typ empty_ctxt ret_ty in
      let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in
      string "forall" ^/^ separate space tyvars_pp ^/^
-- 
cgit v1.2.3


From 786ff327752c7fd26550d96ed2ba328f0facdb4a Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 16 Jul 2018 17:07:24 +0100
Subject: Coq: handle simple type variable matches properly and nat type

---
 src/pretty_print_coq.ml | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 95b3fb68..62ff2b3b 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -768,6 +768,9 @@ let replace_atom_return_type ret_typ =
   | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) ->
      let kid = mk_kid "_retval" in (* TODO: collision avoidance *)
      true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Generated l)
+  | Typ_aux (Typ_id (Id_aux (Id "nat",_)),l) ->
+     let kid = mk_kid "_retval" in
+     true, Typ_aux (Typ_exist ([kid], nc_gteq (nvar kid) (nconstant Nat_big_num.zero), atom_typ (nvar kid)),Generated l)
   | _ -> false, ret_typ
 
 
@@ -1525,7 +1528,7 @@ let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) =
 (* Add equality constraints between arguments and nexps, except in the case
    that they've been merged. *)
 
-let atom_constraint ctxt (pat, typ) =
+let rec atom_constraint ctxt (pat, typ) =
   let typ = Env.base_typ_of (pat_env_of pat) typ in
   match pat, typ with
   | P_aux (P_id id, _),
@@ -1539,6 +1542,11 @@ let atom_constraint ctxt (pat, typ) =
      | _ ->
         Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
                                   parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp)))))
+  | P_aux (P_id id, _),
+        Typ_aux (Typ_id (Id_aux (Id "nat",_)),_) ->
+     Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
+                                  parens (doc_op (string ">=") (doc_id id) (string "0"))))
+  | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ)
   | _ -> None
 
 let all_ids pexp =
@@ -1609,6 +1617,13 @@ let merge_kids_atoms pats =
   let gone,map,_ = List.fold_left try_eliminate (KidSet.empty, KBindings.empty, KidSet.empty) pats in
   gone,map
 
+let merge_var_patterns map pats =
+  let map,pats = List.fold_left (fun (map,pats) (pat, typ) ->
+    match pat with
+    | P_aux (P_var (P_aux (P_id id,_), TP_aux (TP_var kid,_)),ann) ->
+       KBindings.add kid id map, (P_aux (P_id id,ann), typ) :: pats
+    | _ -> map, (pat,typ)::pats) (map,[]) pats
+  in map, List.rev pats
 
 let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in
@@ -1622,6 +1637,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let pats, bind = untuple_args_pat arg_typ pat in
   let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in
   let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in
+  let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in
   let kids_used = KidSet.diff kids_used eliminated_kids in
   let ctxt =
     { early_ret = contains_early_return exp;
-- 
cgit v1.2.3


From 0effbdd2468859924363fe00f29c0afcb727f065 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 16 Jul 2018 18:02:09 +0100
Subject: Coq: we also unfold length

---
 src/pretty_print_coq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 62ff2b3b..7a31465d 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -753,7 +753,7 @@ let condition_produces_constraint exp =
    dependent pair with a proof that the result is the expected integer.  This
    is redundant for basic arithmetic functions and functions which we unfold
    in the constraint solver. *)
-let no_Z_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"]
+let no_Z_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "length_mword"; "length"]
 
 let is_no_Z_proof_fn env id =
   if Env.is_extern id env "coq"
-- 
cgit v1.2.3


From eec725af3dbfc0e8c0ccb79cf8eb457ff5cf68a4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 16 Jul 2018 18:29:18 +0100
Subject: Coq: fix false existential problem

---
 src/pretty_print_coq.ml | 13 +++++++------
 src/type_check.ml       |  6 ++++++
 src/type_check.mli      |  4 ++++
 3 files changed, 17 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 7a31465d..32a560ea 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1023,16 +1023,17 @@ let doc_exp_lem, doc_let_lem =
             (* Decide whether to unpack an existential result, pack one, or cast.
                To do this we compare the expected type stored in the checked expression
                with the inferred type. *)
-            let ret_typ_inst =
-              match infer_exp env (strip_exp full_exp) with
-              | typed_exp -> typ_of typed_exp
+            let inst =
+              match instantiation_of_without_type full_exp with
+              | x -> x
               (* Not all function applications can be inferred, so try falling back to the
                  type inferred when we know the target type.
                  TODO: there are probably some edge cases where this won't pick up a need
                  to cast. *)
-              | exception _ ->
-                 let inst = instantiation_of full_exp in
-                 let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+              | exception _ -> instantiation_of full_exp
+            in
+            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+            let ret_typ_inst =
                  subst_unifiers inst ret_typ
             in
             let unpack,build_ex,autocast =
diff --git a/src/type_check.ml b/src/type_check.ml
index db85bf33..2d1241b9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3302,6 +3302,12 @@ and instantiation_of (E_aux (exp_aux, (l, _)) as exp) =
   | E_app (f, xs) -> snd (infer_funapp' l (Env.no_casts env) f (Env.get_val_spec f env) (List.map strip_exp xs) (Some (typ_of exp)))
   | _ -> invalid_arg ("instantiation_of expected application,  got " ^ string_of_exp exp)
 
+and instantiation_of_without_type (E_aux (exp_aux, (l, _)) as exp) =
+  let env = env_of exp in
+  match exp_aux with
+  | E_app (f, xs) -> snd (infer_funapp' l (Env.no_casts env) f (Env.get_val_spec f env) (List.map strip_exp xs) None)
+  | _ -> invalid_arg ("instantiation_of expected application,  got " ^ string_of_exp exp)
+
 and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
   let annot_exp exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
   let switch_annot env typ = function
diff --git a/src/type_check.mli b/src/type_check.mli
index fd1ddb92..665981e9 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -355,6 +355,10 @@ val alpha_equivalent : Env.t -> typ -> typ -> bool
 (** Throws Invalid_argument if the argument is not a E_app expression *)
 val instantiation_of : tannot exp -> uvar KBindings.t
 
+(** Doesn't use the type of the expression when calculating instantiations.
+    May fail if the arguments aren't sufficient to calculate all unifiers. *)
+val instantiation_of_without_type : tannot exp -> uvar KBindings.t
+
 (* Type variable instantiations that inference will extract from constraints *)
 val instantiate_simple_equations : quant_item list -> uvar KBindings.t
 
-- 
cgit v1.2.3


From 48c73e33a621034ba020b9b1bc83c5f70a19314f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 17 Jul 2018 12:19:15 +0100
Subject: Coq: handle E_constraint properly Adds missing constraints for
 aarch64

---
 src/pretty_print_coq.ml | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 32a560ea..5c4e4e54 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -323,7 +323,7 @@ let drop_duplicate_atoms kids ty =
   in aux_typ ty
 
 (* TODO: parens *)
-let rec doc_nc ctx (NC_aux (nc,_)) =
+let rec doc_nc_prop ctx (NC_aux (nc,_)) =
   match nc with
   | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2)
   | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
@@ -333,11 +333,27 @@ let rec doc_nc ctx (NC_aux (nc,_)) =
      separate space [string "In"; doc_var_lem ctx kid;
                      brackets (separate (string "; ")
                                  (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
-  | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc ctx nc1) (doc_nc ctx nc2)
-  | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc ctx nc1) (doc_nc ctx nc2)
+  | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
+  | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
   | NC_true -> string "True"
   | NC_false -> string "False"
 
+(* TODO: parens *)
+let rec doc_nc_exp ctx (NC_aux (nc,_)) =
+  match nc with
+  | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+  | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+  | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+  | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2))
+  | NC_set (kid, is) -> (* TODO: is this a good translation? *)
+     separate space [string "member_Z_list"; doc_var_lem ctx kid;
+                     brackets (separate (string "; ")
+                                 (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
+  | NC_or (nc1, nc2) -> doc_op (string "||") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2)
+  | NC_and (nc1, nc2) -> doc_op (string "&&") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2)
+  | NC_true -> string "true"
+  | NC_false -> string "false"
+
 let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) =
   match typ with
   | Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_);
@@ -352,7 +368,7 @@ let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) =
 let expand_range_type typ = Util.option_default typ (maybe_expand_range_type typ)
 
 let doc_arithfact ctxt nc =
-  string "ArithFact" ^^ space ^^ parens (doc_nc ctxt nc)
+  string "ArithFact" ^^ space ^^ parens (doc_nc_prop ctxt nc)
 
 (* When making changes here, check whether they affect lem_tyvars_of_typ *)
 let doc_typ, doc_atomic_typ =
@@ -1273,7 +1289,7 @@ let doc_exp_lem, doc_let_lem =
           parens (doc_typ ctxt (typ_of full_exp));
           parens (doc_typ ctxt (typ_of r))] in
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
-    | E_constraint _ -> string "true"
+    | E_constraint nc -> wrap_parens (doc_nc_exp ctxt nc)
     | E_comment _ | E_comment_struc _ -> empty
     | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _
     | E_internal_exp_user _ | E_internal_value _ ->
@@ -1964,8 +1980,8 @@ try
           (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline;
         string "Import ListNotations.";
         hardline;
-        string "Open Scope string.";
-        hardline;
+        string "Open Scope string."; hardline;
+        string "Open Scope bool."; hardline;
         (* Put the body into a Section so that we can define some values with
            Let to put them into the local context, where tactics can see them *)
         string "Section Content.";
-- 
cgit v1.2.3


From ba4250ac585a247ab71656f57aced6857b98ecea Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 17 Jul 2018 15:50:08 +0100
Subject: Coq: support returning rich integer types from effectful functions
 (e.g., coerce_int_nat in aarch64)

---
 src/pretty_print_coq.ml | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5c4e4e54..44670277 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -96,12 +96,14 @@ type context = {
   kid_renames : kid KBindings.t; (* Plain tyvar -> tyvar renames *)
   kid_id_renames : id KBindings.t; (* tyvar -> argument renames *)
   bound_nexps : NexpSet.t;
+  build_ex_return : bool;
 }
 let empty_ctxt = {
   early_ret = false;
   kid_renames = KBindings.empty;
   kid_id_renames = KBindings.empty;
-  bound_nexps = NexpSet.empty
+  bound_nexps = NexpSet.empty;
+  build_ex_return = false;
 }
 
 let langlebar = string "<|"
@@ -1272,7 +1274,11 @@ let doc_exp_lem, doc_let_lem =
             if aexp_needed then parens (align epp) else epp
        end
     | E_internal_return (e1) ->
-       wrap_parens (align (separate space [string "returnm"; expY e1]))
+       let e1pp = expY e1 in
+       let valpp = if ctxt.build_ex_return
+         then parens (string "build_ex" ^^ space ^^ e1pp)
+         else e1pp in
+       wrap_parens (align (separate space [string "returnm"; valpp]))
     | E_sizeof nexp ->
       (match nexp_simp nexp with
         | Nexp_aux (Nexp_constant i, _) -> doc_lit (L_aux (L_num i, l))
@@ -1648,6 +1654,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     | Typ_aux (Typ_fn (arg_typ, ret_typ, eff),_) -> arg_typ, ret_typ, eff
     | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type")
   in
+  let build_ex, ret_typ = replace_atom_return_type ret_typ in
   let ids_to_avoid = all_ids pexp in
   let kids_used = tyvars_of_typquant tq in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
@@ -1660,7 +1667,9 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     { early_ret = contains_early_return exp;
       kid_renames = mk_kid_renames ids_to_avoid kids_used;
       kid_id_renames = kid_to_arg_rename;
-      bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ) } in
+      bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ);
+      build_ex_return = effectful eff && build_ex;
+    } in
   (* Put the constraints after pattern matching so that any type variable that's
      been replaced by one of the term-level arguments is bound. *)
   let quantspp, constrspp = doc_typquant_items_separate ctxt braces tq in
@@ -1680,7 +1689,6 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let patspp = separate_map space doc_binder pats in
   let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in
   let atom_constr_pp = separate space atom_constrs in
-  let build_ex, ret_typ = replace_atom_return_type ret_typ in
   let retpp =
     if effectful eff
     then string "M" ^^ space ^^ parens (doc_typ ctxt ret_typ)
@@ -1705,7 +1713,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
        raise (Reporting_basic.err_unreachable l
                 "guarded pattern expression should have been rewritten before pretty-printing") in
   let bodypp = doc_fun_body ctxt exp in
-  let bodypp = if build_ex then string "build_ex" ^^ space ^^ parens bodypp else bodypp in
+  let bodypp = if effectful eff || not build_ex then bodypp else string "build_ex" ^^ parens bodypp in
   group (prefix 3 1
     (separate space ([idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp]) ^/^
        separate space [colon; retpp; coloneq])
-- 
cgit v1.2.3


From 0c5ff0aa6cd611ab40233b284b0a6054bc27166e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 17 Jul 2018 16:06:27 +0100
Subject: Coq: support effectful function signatures in axiom generation

---
 src/pretty_print_coq.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 44670277..74e97a29 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1846,6 +1846,11 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
      let arg_typs_pp = separate space (List.map doc_typ' typs) in
      let _, ret_ty = replace_atom_return_type ret_ty in
      let ret_typ_pp = doc_typ empty_ctxt ret_ty in
+     let ret_typ_pp =
+       if effectful eff
+       then string "M" ^^ space ^^ parens ret_typ_pp
+       else ret_typ_pp
+     in
      let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in
      string "forall" ^/^ separate space tyvars_pp ^/^
        arg_typs_pp ^/^ separate space constrs_pp ^^ comma ^/^ ret_typ_pp
-- 
cgit v1.2.3


From f3ef82fee78d40c628d319dab4cc35a41c638e8e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 23 Jul 2018 16:14:12 +0100
Subject: Coq: make all pattern matches in the output exhaustive Uses previous
 stage to deal with (e.g.) guards. New option -dcoq_warn_nonex tells you where
 all of the extra default cases were added.

---
 src/process_file.ml |   2 +-
 src/rewrites.ml     | 296 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/rewrites.mli    |   7 ++
 src/sail.ml         |   3 +
 src/type_check.mli  |   1 +
 5 files changed, 308 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/process_file.ml b/src/process_file.ml
index 9ed52e8d..c3e1b510 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -398,7 +398,7 @@ let rewrite rewriters defs =
 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
 let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined bitvectors x)]
 let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
-let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_lem
+let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_coq
 let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
 let rewrite_ast_c ast =
   ast
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8fe30d6b..246a2670 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4001,6 +4001,263 @@ let rewrite_defs_realise_mappings (Defs defs) =
   in
   Defs (List.map rewrite_def defs |> List.flatten)
 
+
+(* Rewrite to make all pattern matches in Coq output exhaustive.
+   Assumes that guards, vector patterns, etc have been rewritten already. *)
+
+let opt_coq_warn_nonexhaustive = ref false
+
+module MakeExhaustive =
+struct
+
+type rlit =
+  | RL_unit
+  | RL_zero
+  | RL_one
+  | RL_true
+  | RL_false
+  | RL_inf
+
+let string_of_rlit = function
+  | RL_unit -> "()"
+  | RL_zero -> "bitzero"
+  | RL_one -> "bitone"
+  | RL_true -> "true"
+  | RL_false -> "false"
+  | RL_inf -> "..."
+
+let rlit_of_lit (L_aux (l,_)) =
+  match l with
+  | L_unit -> RL_unit
+  | L_zero -> RL_zero
+  | L_one -> RL_one
+  | L_true -> RL_true
+  | L_false -> RL_false
+  | L_num _ | L_hex _ | L_bin _ | L_string _ | L_real _ -> RL_inf
+  | L_undef -> assert false
+
+let inv_rlit_of_lit (L_aux (l,_)) =
+  match l with
+  | L_unit -> []
+  | L_zero -> [RL_one]
+  | L_one -> [RL_zero]
+  | L_true -> [RL_false]
+  | L_false -> [RL_true]
+  | L_num _ | L_hex _ | L_bin _ | L_string _ | L_real _ -> [RL_inf]
+  | L_undef -> assert false
+
+type residual_pattern =
+  | RP_any
+  | RP_lit of rlit
+  | RP_enum of id
+  | RP_app of id * residual_pattern list
+  | RP_tup of residual_pattern list
+  | RP_nil
+  | RP_cons of residual_pattern * residual_pattern
+
+let rec string_of_rp = function
+  | RP_any -> "_"
+  | RP_lit rlit -> string_of_rlit rlit
+  | RP_enum id -> string_of_id id
+  | RP_app (f,args) -> string_of_id f ^ "(" ^ String.concat "," (List.map string_of_rp args) ^ ")"
+  | RP_tup rps -> "(" ^ String.concat "," (List.map string_of_rp rps) ^ ")"
+  | RP_nil -> "[| |]"
+  | RP_cons (rp1,rp2) -> string_of_rp rp1 ^ "::" ^ string_of_rp rp2
+
+type ctx = {
+  env : Env.t;
+  enum_to_rest: (residual_pattern list) Bindings.t;
+  constructor_to_rest: (residual_pattern list) Bindings.t
+}
+
+let make_enum_mappings ids m =
+  IdSet.fold (fun id m ->
+    Bindings.add id
+      (List.map (fun e -> RP_enum e) (IdSet.elements (IdSet.remove id ids))) m)
+    ids
+    m
+
+let make_cstr_mappings env ids m =
+  let ids = IdSet.elements ids in
+  let constructors = List.map
+    (fun id ->
+      let _,ty = Env.get_val_spec id env in
+      let args = match ty with
+        | Typ_aux (Typ_fn (Typ_aux (Typ_tup tys,_),_,_),_) -> List.map (fun _ -> RP_any) tys
+        | _ -> [RP_any]
+      in RP_app (id,args)) ids in
+  let rec aux ids acc l =
+    match ids, l with
+    | [], [] -> m
+    | id::ids, rp::t ->
+       let m = aux ids (acc@[rp]) t in
+       Bindings.add id (acc@t) m
+    | _ -> assert false
+  in aux ids [] constructors
+
+let ctx_from_pattern_completeness_ctx env =
+  let ctx = Env.pattern_completeness_ctx env in
+  { env = env;
+    enum_to_rest = Bindings.fold (fun _ ids m -> make_enum_mappings ids m) 
+      ctx.Pattern_completeness.enums Bindings.empty;
+    constructor_to_rest = Bindings.fold (fun _ ids m -> make_cstr_mappings env ids m)
+      ctx.Pattern_completeness.variants Bindings.empty
+  }
+
+let printprefix = ref "  "
+
+let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
+  let subpats rm_pats res_pats =
+    let res_pats' = List.map2 (remove_clause_from_pattern ctx) rm_pats res_pats in
+    let rec aux acc fixed residual =
+      match fixed, residual with
+      | [], [] -> []
+      | (fh::ft), (rh::rt) ->
+         let rt' = aux (acc@[fh]) ft rt in
+         let newr = List.map (fun x -> acc @ (x::ft)) rh in
+         newr @ rt'
+      | _,_ -> assert false (* impossible because we managed map2 above *)
+    in aux [] res_pats res_pats'
+  in
+  let inconsistent () =
+    raise (Reporting_basic.err_unreachable (fst ann)
+             ("Inconsistency during exhaustiveness analysis with " ^
+                 string_of_rp res_pat))
+  in
+  (*let _ = print_endline (!printprefix ^ "pat: " ^string_of_pat (P_aux (rm_pat,ann))) in
+  let _ = print_endline (!printprefix ^ "res_pat: " ^string_of_rp res_pat) in
+  let _ = printprefix := "  " ^ !printprefix in*)
+  let rp' =
+  match rm_pat with
+  | P_wild -> []
+  | P_id id when (match Env.lookup_id id ctx.env with Unbound | Local _ -> true | _ -> false) -> []
+  | P_lit lit ->
+     (match res_pat with
+     | RP_any -> List.map (fun l -> RP_lit l) (inv_rlit_of_lit lit)
+     | RP_lit RL_inf -> [res_pat]
+     | RP_lit lit' -> if lit' = rlit_of_lit lit then [] else [res_pat]
+     | _ -> inconsistent ())
+  | P_as (p,_) 
+  | P_typ (_,p)
+  | P_var (p,_) 
+    -> remove_clause_from_pattern ctx p res_pat
+  | P_id id ->
+     (match Env.lookup_id id ctx.env with
+     | Enum enum ->
+        (match res_pat with
+        | RP_any -> Bindings.find id ctx.enum_to_rest
+        | RP_enum id' -> if Id.compare id id' == 0 then [] else [res_pat]
+        | _ -> inconsistent ())
+     | _ -> assert false)
+  | P_tup rm_pats ->
+     let previous_res_pats = 
+       match res_pat with
+       | RP_tup res_pats -> res_pats
+       | RP_any -> List.map (fun _ -> RP_any) rm_pats
+       | _ -> inconsistent ()
+     in
+     let res_pats' = subpats rm_pats previous_res_pats in
+     List.map (fun rps -> RP_tup rps) res_pats'
+  | P_app (id,args) ->
+     (match res_pat with
+     | RP_app (id',residual_args) ->
+        if Id.compare id id' == 0 then
+          let res_pats' = subpats args residual_args in
+          List.map (fun rps -> RP_app (id,rps)) res_pats'
+        else [res_pat]
+     | RP_any ->
+        let res_args = subpats args (List.map (fun _ -> RP_any) args) in
+        (List.map (fun l -> (RP_app (id,l))) res_args) @
+          (Bindings.find id ctx.constructor_to_rest)
+     | _ -> inconsistent ()
+     )
+  | P_list ps ->
+     (match ps with
+     | p1::ptl -> remove_clause_from_pattern ctx (P_aux (P_cons (p1,P_aux (P_list ptl,ann)),ann)) res_pat
+     | [] ->
+        match res_pat with
+        | RP_any -> [RP_cons (RP_any,RP_any)]
+        | RP_cons _ -> [res_pat]
+        | RP_nil -> []
+        | _ -> inconsistent ())
+  | P_cons (p1,p2) -> begin
+     let rp',rps = 
+       match res_pat with
+       | RP_cons (rp1,rp2) -> [], Some [rp1;rp2]
+       | RP_any -> [RP_nil], Some [RP_any;RP_any]
+       | RP_nil -> [RP_nil], None
+       | _ -> inconsistent ()
+     in
+     match rps with
+     | None -> rp'
+     | Some rps ->
+        let res_pats = subpats [p1;p2] rps in
+        rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
+  end
+  | P_record _ ->
+     raise (Reporting_basic.err_unreachable (fst ann)
+              "Record pattern not supported")
+  | P_vector _
+  | P_vector_concat _
+  | P_string_append _ ->
+     raise (Reporting_basic.err_unreachable (fst ann)
+              "Found pattern that should have been rewritten away in earlier stage")
+
+  (*in let _ = printprefix := String.sub (!printprefix) 0 (String.length !printprefix - 2)
+  in let _ = print_endline (!printprefix ^ "res_pats': " ^ String.concat "; " (List.map string_of_rp rp'))*)
+  in rp'
+
+let process_pexp env =
+  let ctx = ctx_from_pattern_completeness_ctx env in
+  fun rps patexp ->
+  (*let _ = print_endline ("res_pats: " ^ String.concat "; " (List.map string_of_rp rps)) in
+    let _ = print_endline ("pat: " ^ string_of_pexp patexp) in*)
+  match patexp with
+  | Pat_aux (Pat_exp (p,_),_) -> 
+     List.concat (List.map (remove_clause_from_pattern ctx p) rps)
+  | Pat_aux (Pat_when _,(l,_)) ->
+     raise (Reporting_basic.err_unreachable l
+              "Guarded pattern should have been rewritten away")
+
+let rewrite_case (e,ann) =
+  match e with
+  | E_case (e1,cases) ->
+     begin
+     let env = env_of_annot ann in
+     let rps = List.fold_left (process_pexp env) [RP_any] cases in
+     match rps with
+     | [] -> E_aux (E_case (e1,cases),ann)
+     | (example::_) ->
+
+        let _ =
+          if !opt_coq_warn_nonexhaustive
+          then Reporting_basic.print_err false false
+            (fst ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
+
+        let l = Parse_ast.Generated Parse_ast.Unknown in
+        let p = P_aux (P_wild, (l, None)) in
+        let ann' = Some (env, typ_of_annot ann, mk_effect [BE_escape]) in
+        (* TODO: use an expression that specifically indicates a failed pattern match *)
+        let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,None))),(l,ann')) in
+        E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,None))]),ann)
+     end
+  | _ -> E_aux (e,ann)
+
+let rewrite =
+  let alg = { id_exp_alg with e_aux = rewrite_case } in
+  rewrite_defs_base
+    { rewrite_exp = (fun _ -> fold_exp alg)
+    ; rewrite_pat = rewrite_pat
+    ; rewrite_let = rewrite_let
+    ; rewrite_lexp = rewrite_lexp
+    ; rewrite_fun = rewrite_fun
+    ; rewrite_def = rewrite_def
+    ; rewrite_defs = rewrite_defs_base
+    }
+
+
+end
+
 let recheck_defs defs = fst (Type_error.check initial_env defs)
 
 let remove_mapping_valspecs (Defs defs) =
@@ -4049,6 +4306,45 @@ let rewrite_defs_lem = [
   ("recheck_defs", recheck_defs)
   ]
 
+let rewrite_defs_coq = [
+  ("realise_mappings", rewrite_defs_realise_mappings);
+  ("remove_mapping_valspecs", remove_mapping_valspecs);
+  ("pat_string_append", rewrite_defs_pat_string_append);
+  ("mapping_builtins", rewrite_defs_mapping_patterns);
+  ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem);
+  ("vector_concat_assignments", rewrite_vector_concat_assignments);
+  ("tuple_assignments", rewrite_tuple_assignments);
+  ("simple_assignments", rewrite_simple_assignments);
+  ("remove_vector_concat", rewrite_defs_remove_vector_concat);
+  ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
+  ("remove_numeral_pats", rewrite_defs_remove_numeral_pats);
+  ("guarded_pats", rewrite_defs_guarded_pats);
+  ("bitvector_exps", rewrite_bitvector_exps);
+  (* ("register_ref_writes", rewrite_register_ref_writes); *)
+  ("nexp_ids", rewrite_defs_nexp_ids);
+  ("fix_val_specs", rewrite_fix_val_specs);
+  ("split_execute", rewrite_split_fun_constr_pats "execute");
+  ("recheck_defs", recheck_defs);
+  ("exp_lift_assign", rewrite_defs_exp_lift_assign);
+  (* ("constraint", rewrite_constraint); *)
+  (* ("remove_assert", rewrite_defs_remove_assert); *)
+  ("top_sort_defs", top_sort_defs);
+  ("trivial_sizeof", rewrite_trivial_sizeof);
+  ("sizeof", rewrite_sizeof);
+  ("early_return", rewrite_defs_early_return);
+  ("make_cases_exhaustive", MakeExhaustive.rewrite);
+  ("fix_val_specs", rewrite_fix_val_specs);
+  ("recheck_defs", recheck_defs);
+  ("remove_blocks", rewrite_defs_remove_blocks);
+  ("letbind_effects", rewrite_defs_letbind_effects);
+  ("remove_e_assign", rewrite_defs_remove_e_assign);
+  ("internal_lets", rewrite_defs_internal_lets);
+  ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds);
+  ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns);
+  ("merge function clauses", merge_funcls);
+  ("recheck_defs", recheck_defs)
+  ]
+
 let rewrite_defs_ocaml = [
     (* ("undefined", rewrite_undefined); *)
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
diff --git a/src/rewrites.mli b/src/rewrites.mli
index 70cb75af..7d6bc0b2 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -66,6 +66,13 @@ val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list
 (* Perform rewrites to exclude AST nodes not supported for lem out*)
 val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list
 
+(* Perform rewrites to exclude AST nodes not supported for coq out*)
+val rewrite_defs_coq : (string * (tannot defs -> tannot defs)) list
+
+(* Warn about matches where we add a default case for Coq because they're not
+   exhaustive *)
+val opt_coq_warn_nonexhaustive : bool ref
+
 (* Perform rewrites to exclude AST nodes not supported for C compilation *)
 val rewrite_defs_c : (string * (tannot defs -> tannot defs)) list
 
diff --git a/src/sail.ml b/src/sail.ml
index 64e60c23..f0903146 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -151,6 +151,9 @@ let options = Arg.align ([
   ( "-dcoq_undef_axioms",
     Arg.Set Pretty_print_coq.opt_undef_axioms,
     "Generate axioms for functions that are declared but not defined");
+  ( "-dcoq_warn_nonex",
+    Arg.Set Rewrites.opt_coq_warn_nonexhaustive,
+    "Generate warnings for non-exhaustive pattern matches in the Coq backend");
   ( "-latex_prefix",
     Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix),
     " set a custom prefix for generated latex command (default sail)");
diff --git a/src/type_check.mli b/src/type_check.mli
index 665981e9..31a5a8dd 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -197,6 +197,7 @@ module Env : sig
 
   val empty : t
 
+  val pattern_completeness_ctx : t -> Pattern_completeness.ctx
 end
 
 (** Push all the type variables and constraints from a typquant into
-- 
cgit v1.2.3