From 33c27c9a4e30f6b3532aeeed0d72b0331c943d8b Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 13 Feb 2019 16:57:00 +0000
Subject: Attempt to parse sail version from opam file for manifest.ml. Update
 version in opam file in anticipation of release and add yojson dependency.

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

(limited to 'src')

diff --git a/src/Makefile b/src/Makefile
index b0b22f77..beba66df 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -96,7 +96,7 @@ else
 	echo let dir=\"$(SHARE_DIR)\" >> manifest.ml
 	echo let commit=\"opam\" >> manifest.ml
 	echo let branch=\"sail2\" >> manifest.ml
-	echo let version=\"0.8\" >> manifest.ml
+	echo let version=\"$(shell grep '^version:' ../opam | grep -o -E '"[^"]+"')\" >> manifest.ml
 endif
 
 sail: ast.ml bytecode.ml manifest.ml
-- 
cgit v1.2.3


From b8fa1b62c114e030f2dcdc58d7df01ae2308b6d4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 14 Feb 2019 11:31:35 +0000
Subject: Coq: special case printing of bind-if-then-else trees for decoding
 Reduces the current arm model output from 268MB to 15MB.

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 4596f23f..27484560 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1775,6 +1775,10 @@ let doc_exp, doc_let =
       | E_aux (E_if (c', t', e'), _)
       | E_aux (E_cast (_, E_aux (E_if (c', t', e'), _)), _) ->
          if_exp ctxt true c' t' e'
+      (* Special case to prevent current arm decoder becoming a staircase *)
+      (* TODO: replace with smarter pretty printing *)
+      | E_aux (E_internal_plet (pat,exp1,E_aux (E_cast (typ, (E_aux (E_if (_, _, _), _) as exp2)),_)),ann) when Typ.compare typ unit_typ == 0 ->
+         string "else" ^/^ top_exp ctxt false (E_aux (E_internal_plet (pat,exp1,exp2),ann))
       | _ -> prefix 2 1 (string "else") (top_exp ctxt false e)
     in
     (prefix 2 1
-- 
cgit v1.2.3


From cf7eb8b83ecf7278c84f6e22b5659261ee1eddbc Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 14 Feb 2019 15:10:29 +0000
Subject: Don't do any rewrites when checking files for Emacs

This makes sure we don't do any kind of re-writing or de-scatter any
definitions when loading files into emacs. The difference here is that
normally all files are processed together, but the emacs mode loads
each file one by one. This is probably what we want to be doing
anyway, so location information stays accurate for scattered
functions for things like type-at-cursor commands and similar.

Also fix some warnings.

Fixes #32
---
 src/ast_util.ml          |  1 +
 src/isail.ml             |  4 ++--
 src/ocaml_backend.ml     |  8 ++++----
 src/pretty_print_sail.ml |  9 +++++++--
 src/rewrites.ml          | 13 ++++++++++---
 src/sail.ml              | 23 +++++++++++++----------
 src/specialize.ml        |  2 ++
 7 files changed, 39 insertions(+), 21 deletions(-)

(limited to 'src')

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 5746a242..11873690 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1355,6 +1355,7 @@ and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) =
   match typ_arg_aux with
   | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
   | A_typ typ -> [undefined_of_typ mwords l annot typ]
+  | A_bool nc -> [E_aux (E_constraint nc, (l, annot (atom_bool_typ nc)))]
   | A_order _ -> []
 
 let destruct_pexp (Pat_aux (pexp,ann)) =
diff --git a/src/isail.ml b/src/isail.ml
index 7d009791..4cfb2c6f 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -276,7 +276,7 @@ let load_session upto file =
   | Some upto_file when Filename.basename upto_file = file -> None
   | Some upto_file ->
      let (_, ast, env) =
-       load_files ~generate:false !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
+       load_files ~check:true !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
      in
      Interactive.ast := append_ast !Interactive.ast ast;
      Interactive.env := env;
@@ -464,7 +464,7 @@ let handle_input' input =
            begin
              try
                load_into_session arg;
-               let (_, ast, env) = load_files !Interactive.env [arg] in
+               let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in
                Interactive.ast := append_ast !Interactive.ast ast;
                interactive_state := initial_state !Interactive.ast Value.primops;
                Interactive.env := env;
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index d51aba75..05406413 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -710,13 +710,12 @@ let ocaml_pp_generators ctx defs orig_types required =
   and add_req_from_typarg required (A_aux (arg,_)) =
     match arg with
     | A_typ typ -> add_req_from_typ required typ
-    | A_nexp _
-    | A_order _
-      -> required
+    | A_nexp _ | A_order _ | A_bool _ -> required
   and add_req_from_td required (TD_aux (td,(l,_))) =
     match td with
     | TD_abbrev (_, _, A_aux (A_typ typ, _)) ->
        add_req_from_typ required typ
+    | TD_abbrev _ -> required
     | TD_record (_, _, fields, _) ->
        List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields
     | TD_variant (_, _, variants, _) ->
@@ -787,7 +786,7 @@ let ocaml_pp_generators ctx defs orig_types required =
                                        | _ -> space ^^ separate space args_pp
         in
         string ("g.gen_" ^ typ_str) ^^ args_pp
-      and typearg (A_aux (arg,_)) =
+      and typearg (A_aux (arg,l)) =
         match arg with
         | A_nexp (Nexp_aux (nexp,l) as full_nexp) ->
            (match nexp with
@@ -801,6 +800,7 @@ let ocaml_pp_generators ctx defs orig_types required =
             | Ord_inc -> string "true"
             | Ord_dec -> string "false")
         | A_typ typ -> parens (string "fun g -> " ^^ gen_type typ)
+        | A_bool nc -> raise (Reporting.err_todo l ("Unsupported constraint for generators: " ^ string_of_n_constraint nc))
       in
       let make_subgen (Typ_aux (typ,l) as full_typ) =
         let typ_str, args_pp =
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index f30d5135..9a374275 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -619,8 +619,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | TD_variant (id, TypQ_aux (TypQ_tq qs, _), unions, _) ->
      separate space [string "union"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
-  | _ -> string "TYPEDEF"
-
+  | TD_bitfield _ -> string "BITFIELD" (* should be rewritten *)
 
 let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) =
   let doc_extern ext =
@@ -656,6 +655,12 @@ let rec doc_scattered (SD_aux (sd_aux, _)) =
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id
   | SD_variant (id, TypQ_aux (TypQ_tq quants, _)) ->
      string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants
+  | SD_mapcl (id, mapcl) ->
+     separate space [string "mapping clause"; doc_id id; equals; doc_mapcl mapcl]
+  | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_none, _)) ->
+     separate space [string "scattered mapping"; doc_id id]
+  | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_some (_, typ), _)) ->
+     separate space [string "scattered mapping"; doc_id id; string ":"; doc_typ typ]
   | SD_unioncl (id, tu) ->
      separate space [string "union clause"; doc_id id; equals; doc_union tu]
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5a70a721..31117f33 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3525,7 +3525,11 @@ let rewrite_defs_mapping_patterns env =
        let mapping_in_typ = typ_of_annot p_annot in
 
        let x = Env.get_val_spec mapping_id env in
-       let (_, Typ_aux(Typ_bidir(typ1, typ2), _)) = x in
+
+       let typ1, typ2 = match x with
+         | (_, Typ_aux(Typ_bidir(typ1, typ2), _)) -> typ1, typ2
+         | (_, typ) -> raise (Reporting.err_unreachable (fst p_annot) __POS__ ("Must be bi-directional mapping: " ^ string_of_typ typ))
+       in
 
        let mapping_direction =
          if mapping_in_typ = typ1 then
@@ -4642,8 +4646,11 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
         rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
   end
   | P_record _ ->
-     raise (Reporting.err_unreachable (fst ann) __POS__
-              "Record pattern not supported")
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Record pattern not supported")
+  | P_or _ ->
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Or pattern not supported")
+  | P_not _ ->
+     raise (Reporting.err_unreachable (fst ann) __POS__ "Negated pattern not supported")
   | P_vector _
   | P_vector_concat _
   | P_string_append _ ->
diff --git a/src/sail.ml b/src/sail.ml
index 06bd618e..28c5db0a 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -311,7 +311,7 @@ let _ =
       opt_file_arguments := (!opt_file_arguments) @ [s])
     usage_msg
 
-let load_files ?generate:(generate=true) type_envs files =
+let load_files ?check:(check=false) type_envs files =
   if !opt_memo_z3 then Constraint.load_digests () else ();
 
   let t = Profile.start () in
@@ -320,24 +320,27 @@ let load_files ?generate:(generate=true) type_envs files =
     List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes)
                      -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
   let ast = Process_file.preprocess_ast options ast in
-  let ast = Initial_check.process_ast ~generate:generate ast in
+  let ast = Initial_check.process_ast ~generate:(not check) ast in
   Profile.finish "parsing" t;
 
   let t = Profile.start () in
   let (ast, type_envs) = check_ast type_envs ast in
   Profile.finish "type checking" t;
 
-  let ast = Scattered.descatter ast in
-  let ast = rewrite_ast type_envs ast in
+  if !opt_memo_z3 then Constraint.save_digests () else ();
 
-  let out_name = match !opt_file_out with
-    | None when parsed = [] -> "out.sail"
-    | None -> fst (List.hd parsed)
-    | Some f -> f ^ ".sail" in
+  if check then
+    ("out.sail", ast, type_envs)
+  else
+    let ast = Scattered.descatter ast in
+    let ast = rewrite_ast type_envs ast in
 
-  if !opt_memo_z3 then Constraint.save_digests () else ();
+    let out_name = match !opt_file_out with
+      | None when parsed = [] -> "out.sail"
+      | None -> fst (List.hd parsed)
+      | Some f -> f ^ ".sail" in
 
-  (out_name, ast, type_envs)
+    (out_name, ast, type_envs)
 
 let main() =
   if !opt_print_version then
diff --git a/src/specialize.ml b/src/specialize.ml
index 00357557..9f6af6d6 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -160,6 +160,8 @@ let string_of_instantiation instantiation =
        kid_name (mk_kopt K_int kid) ^ " in {" ^ Util.string_of_list ", " Big_int.to_string ns ^ "}"
     | NC_aux (NC_true, _) -> "true"
     | NC_aux (NC_false, _) -> "false"
+    | NC_aux (NC_var kid, _) -> kid_name (mk_kopt K_bool kid)
+    | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
   in
 
   let string_of_binding (kid, arg) = string_of_kid kid ^ " => " ^ string_of_typ_arg arg in
-- 
cgit v1.2.3


From 5a51f3f958bd66fd305af4268e43568474f34ac9 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 14 Feb 2019 17:46:29 +0000
Subject: Fix a bug that caused constant propagation option to fail for v8.5

Make type-at-cursor work for scattered function clauses in emacs
---
 src/ast_util.ml      | 35 +++++++++++++++++++++++++++--------
 src/constant_fold.ml |  2 ++
 2 files changed, 29 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 11873690..fcfa619e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -1862,6 +1862,12 @@ let rec find_annot_exp sl (E_aux (aux, (l, annot)) as exp) =
          option_chain (find_annot_lexp sl lexp) (find_annot_exp sl exp)
       | E_var (lexp, exp1, exp2) ->
          option_chain (find_annot_lexp sl lexp) (option_mapm (find_annot_exp sl) [exp1; exp2])
+      | E_if (cond_exp, then_exp, else_exp) ->
+         option_mapm (find_annot_exp sl) [cond_exp; then_exp; else_exp]
+      | E_case (exp, cases) | E_try (exp, cases) ->
+         option_chain (find_annot_exp sl exp) (option_mapm (find_annot_pexp sl) cases)
+      | E_return exp | E_cast (_, exp) ->
+         find_annot_exp sl exp
       | _ -> None
     in
     match result with
@@ -1888,6 +1894,8 @@ and find_annot_lexp sl (LEXP_aux (aux, (l, annot))) =
 and find_annot_pat sl (P_aux (aux, (l, annot))) =
   if not (subloc sl l) then None else
     let result = match aux with
+      | P_vector_concat pats ->
+         option_mapm (find_annot_pat sl) pats
       | _ -> None
     in
     match result with
@@ -1898,32 +1906,43 @@ and find_annot_pexp sl (Pat_aux (aux, (l, annot))) =
   if not (subloc sl l) then None else
     match aux with
     | Pat_exp (pat, exp) ->
-       find_annot_exp sl exp
+       option_chain (find_annot_pat sl pat) (find_annot_exp sl exp)
     | Pat_when (pat, guard, exp) ->
-       None
+       option_chain (find_annot_pat sl pat) (option_mapm (find_annot_exp sl) [guard; exp])
 
 let find_annot_funcl sl (FCL_aux (FCL_Funcl (id, pexp), (l, annot))) =
-  if not (subloc sl l) then
-    None
-  else
+  if not (subloc sl l) then None else
     match find_annot_pexp sl pexp with
     | None -> Some (l, annot)
     | result -> result
 
 let find_annot_fundef sl (FD_aux (FD_function (_, _, _, funcls), (l, annot))) =
-  if not (subloc sl l) then
-    None
-  else
+  if not (subloc sl l) then None else
     match option_mapm (find_annot_funcl sl) funcls with
     | None -> Some (l, annot)
     | result -> result
 
+let find_annot_scattered sl (SD_aux (aux, (l, annot))) =
+  if not (subloc sl l) then None else
+    let result = match aux with
+      | SD_funcl fcl -> find_annot_funcl sl fcl
+      | _ -> None
+    in
+    match result with
+    | None -> Some (l, annot)
+    | _ -> result
+
 let rec find_annot_defs sl = function
   | DEF_fundef fdef :: defs ->
      begin match find_annot_fundef sl fdef with
      | None -> find_annot_defs sl defs
      | result -> result
      end
+  | DEF_scattered sdef :: defs ->
+     begin match find_annot_scattered sl sdef with
+     | None -> find_annot_defs sl defs
+     | result -> result
+     end
   | _ :: defs ->
      find_annot_defs sl defs
   | [] -> None
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 7321a801..6ad1f663 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -180,6 +180,8 @@ let rec rewrite_constant_function_calls' ast =
     | E_app (id, args) when List.for_all is_constant args ->
        evaluate e_aux annot
 
+    | E_cast (typ, (E_aux (E_lit _, _) as lit)) -> ok (); lit
+
     | E_field (exp, id) when is_constant exp ->
        evaluate e_aux annot
 
-- 
cgit v1.2.3


From 7d34e41566f9c6a22debdcadc3a54c4b3b016b80 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 14 Feb 2019 20:14:31 +0000
Subject: Fix issues for versions of z3 confused by 2^n

Some versions of z3 do not like any constraints with the form 2^f(n),
even when such constraints are completely trivial, or only exist in
the environment yet no bearing on the current goal. Unfortunately the
z3 in Ubuntu LTS has these issues.

We can mitigate these issues somewhat by removing any 2^f(n)
containing conjuncts from the environment when z3 returns unknown, and
attempting to reprove the goal. In practice Type_check.prove only
guarantees that the goal is provable when it returns true, and does
not guarantee that it is false when it returns false, only that it
wasn't provable in the specified timeout. Similarly for
Type_check.solve. Mostly this is fine, because prove returning false
usually triggers a type error, or e.g. in the C optimizer always has a
sensible fallback (where it just won't optimize that specific
case). What is slightly concerning is that this z3 issues means that
Sail written using the latest z3 from git may not compile using Ubuntu
LTS z3.

We could if we wanted to put additional restrictions on Nexp_exp to
avoid this issue. We should also look over uses of Type_check.prove in
Sail to make sure callers are using it correctly.
---
 src/type_check.ml  | 82 +++++++++++++++++++++++++++++++++++-------------------
 src/type_check.mli |  5 ++++
 2 files changed, 58 insertions(+), 29 deletions(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index a8251e97..11b58a8c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1322,6 +1322,32 @@ and simp_typ_aux = function
 
   | typ_aux -> typ_aux
 
+let rec typ_nexps (Typ_aux (typ_aux, l)) =
+  match typ_aux with
+  | Typ_internal_unknown -> []
+  | Typ_id v -> []
+  | Typ_var kid -> []
+  | Typ_tup typs -> List.concat (List.map typ_nexps typs)
+  | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
+  | Typ_exist (kids, nc, typ) -> typ_nexps typ
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
+  | Typ_bidir (typ1, typ2) ->
+     typ_nexps typ1 @ typ_nexps typ2
+and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
+  match typ_arg_aux with
+  | A_nexp n -> [n]
+  | A_typ typ -> typ_nexps typ
+  | A_bool nc -> constraint_nexps nc
+  | A_order ord -> []
+and constraint_nexps (NC_aux (nc_aux, l)) =
+  match nc_aux with
+  | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_not_equal (n1, n2) ->
+     [n1; n2]
+  | NC_set _ | NC_true | NC_false | NC_var _ -> []
+  | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2
+  | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args)
+
 (* Here's how the constraint generation works for subtyping
 
 X(b,c...) --> {a. Y(a,b,c...)} \subseteq {a. Z(a,b,c...)}
@@ -1343,6 +1369,22 @@ this is equivalent to
 which is then a problem we can feed to the constraint solver expecting unsat.
  *)
 
+let rec nexp_variable_power (Nexp_aux (aux, _)) =
+  match aux with
+  | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) ->
+     nexp_variable_power n1 || nexp_variable_power n2
+  | Nexp_neg n ->
+     nexp_variable_power n
+  | Nexp_id _ | Nexp_var _ | Nexp_constant _ ->
+     false
+  | Nexp_app (_, ns) ->
+     List.exists nexp_variable_power ns
+  | Nexp_exp n ->
+     not (KidSet.is_empty (tyvars_of_nexp n))
+
+let constraint_variable_power nc =
+  List.exists nexp_variable_power (constraint_nexps nc)
+
 let prove_z3 env (NC_aux (_, l) as nc) =
   let vars = Env.get_typ_vars env in
   let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
@@ -1350,7 +1392,15 @@ let prove_z3 env (NC_aux (_, l) as nc) =
   match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs) with
   | Constraint.Unsat -> typ_debug (lazy "unsat"); true
   | Constraint.Sat -> typ_debug (lazy "sat"); false
-  | Constraint.Unknown -> typ_debug (lazy "unknown"); false
+  | Constraint.Unknown ->
+     (* Work around versions of z3 that are confused by 2^n in
+        constraints, even when such constraints are irrelevant *)
+     let ncs = List.concat (List.map constraint_conj ncs) in
+     let ncs = List.filter (fun nc -> not (constraint_variable_power nc)) ncs in
+     match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs) with
+     | Constraint.Unsat -> typ_debug (lazy "unsat"); true
+     | Constraint.Sat -> typ_debug (lazy "sat"); false
+     | Constraint.Unknown -> typ_debug (lazy "unknown"); false
 
 let solve env (Nexp_aux (_, l) as nexp) =
   typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
@@ -1393,32 +1443,6 @@ let rec nexp_frees ?exs:(exs=KidSet.empty) (Nexp_aux (nexp, l)) =
   | Nexp_exp n -> nexp_frees ~exs:exs n
   | Nexp_neg n -> nexp_frees ~exs:exs n
 
-let rec typ_nexps (Typ_aux (typ_aux, l)) =
-  match typ_aux with
-  | Typ_internal_unknown -> []
-  | Typ_id v -> []
-  | Typ_var kid -> []
-  | Typ_tup typs -> List.concat (List.map typ_nexps typs)
-  | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
-  | Typ_exist (kids, nc, typ) -> typ_nexps typ
-  | Typ_fn (arg_typs, ret_typ, _) ->
-     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
-  | Typ_bidir (typ1, typ2) ->
-     typ_nexps typ1 @ typ_nexps typ2
-and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
-  match typ_arg_aux with
-  | A_nexp n -> [n]
-  | A_typ typ -> typ_nexps typ
-  | A_bool nc -> constraint_nexps nc
-  | A_order ord -> []
-and constraint_nexps (NC_aux (nc_aux, l)) =
-  match nc_aux with
-  | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_not_equal (n1, n2) ->
-     [n1; n2]
-  | NC_set _ | NC_true | NC_false | NC_var _ -> []
-  | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2
-  | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args)
-
 let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
   match nexp1, nexp2 with
   | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 = 0
@@ -1709,13 +1733,13 @@ let rec ambiguous_vars (Typ_aux (aux, _)) =
   match aux with
   | Typ_app (_, args) -> List.fold_left KidSet.union KidSet.empty (List.map ambiguous_arg_vars args)
   | _ -> KidSet.empty
-  
+
 and ambiguous_arg_vars (A_aux (aux, _)) =
   match aux with
   | A_bool nc -> ambiguous_nc_vars nc
   | A_nexp nexp -> ambiguous_nexp_vars nexp
   | _ -> KidSet.empty
-               
+
 and ambiguous_nc_vars (NC_aux (aux, _)) =
   match aux with
   | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2)
diff --git a/src/type_check.mli b/src/type_check.mli
index eab96b07..8ea0b3e2 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -309,6 +309,11 @@ val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t
 
 val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t
 
+(** Attempt to prove a constraint using z3. Returns true if z3 can
+   prove that the constraint is true, returns false if z3 cannot prove
+   the constraint true. Note that this does not guarantee that the
+   constraint is actually false, as the constraint solver is somewhat
+   untrustworthy. *)
 val prove : (string * int * int * int) -> Env.t -> n_constraint -> bool
 
 val solve : Env.t -> nexp -> Big_int.num option
-- 
cgit v1.2.3


From 96f0df85a129666e3b960d6d17df165de13b3024 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 14 Feb 2019 23:54:13 +0000
Subject: Improve sizeof-rewriting performance

Simple heuristic to try local variables with the same name as type
variables first, roughly doubles typechecking speed.
---
 src/type_check.ml | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index 11b58a8c..37f2cee7 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1395,12 +1395,11 @@ let prove_z3 env (NC_aux (_, l) as nc) =
   | Constraint.Unknown ->
      (* Work around versions of z3 that are confused by 2^n in
         constraints, even when such constraints are irrelevant *)
-     let ncs = List.concat (List.map constraint_conj ncs) in
-     let ncs = List.filter (fun nc -> not (constraint_variable_power nc)) ncs in
-     match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs) with
+     let ncs' = List.concat (List.map constraint_conj ncs) in
+     let ncs' = List.filter (fun nc -> not (constraint_variable_power nc)) ncs' in
+     match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs') with
      | Constraint.Unsat -> typ_debug (lazy "unsat"); true
-     | Constraint.Sat -> typ_debug (lazy "sat"); false
-     | Constraint.Unknown -> typ_debug (lazy "unknown"); false
+     | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false
 
 let solve env (Nexp_aux (_, l) as nexp) =
   typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
@@ -2007,11 +2006,24 @@ let subtype_check env typ1 typ2 =
 
 exception No_simple_rewrite;;
 
+let rec move_to_front p ys = function
+  | x :: xs when p x -> x :: (ys @ xs)
+  | x :: xs -> move_to_front p (x :: ys) xs
+  | [] -> ys
+
 let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) =
   let mk_exp exp = mk_exp ~loc:l exp in
   match aux with
   | Nexp_var v ->
+     (* Use a simple heuristic to find the most likely local we can
+        use, and move it to the front of the list. *)
+     let str = string_of_kid v in
+     let likely =
+       try let n = if str.[1] = '_' then 2 else 1 in String.sub str n (String.length str - n) with
+       | Invalid_argument _ -> str
+     in
      let locals = Env.get_locals env |> Bindings.bindings in
+     let locals = move_to_front (fun local -> likely = string_of_id (fst local)) [] locals in
      let same_size (local, (_, Typ_aux (aux, _))) =
        match aux with
        | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)])
-- 
cgit v1.2.3


From 65599f14b3ecac193529caafbee7672b38ed367e Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Fri, 15 Feb 2019 03:04:37 +0000
Subject: Use multiple solvers

Useful to see what constraints we are generating that are particularly
hard, and which of our specs work with different solvers.

Refactor code to use smt in names rather than specifically z3
---
 src/c_backend.ml   |  16 +++---
 src/constraint.ml  | 156 +++++++++++++++++++++++++++++++++++++++--------------
 src/constraint.mli |   6 ++-
 src/profile.ml     |  18 +++----
 src/sail.ml        |   9 ++--
 src/type_check.ml  |  14 ++---
 6 files changed, 151 insertions(+), 68 deletions(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index a1050972..2981660e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -110,7 +110,7 @@ type ctx =
     letbinds : int list;
     recursive_functions : IdSet.t;
     no_raw : bool;
-    optimize_z3 : bool;
+    optimize_smt : bool;
   }
 
 let initial_ctx env =
@@ -123,13 +123,13 @@ let initial_ctx env =
     letbinds = [];
     recursive_functions = IdSet.empty;
     no_raw = false;
-    optimize_z3 = true;
+    optimize_smt = true;
   }
 
 (** Convert a sail type into a C-type. This function can be quite
-   slow, because it uses ctx.local_env and Z3 to analyse the Sail
+   slow, because it uses ctx.local_env and SMT to analyse the Sail
    types and attempts to fit them into the smallest possible C
-   types, provided ctx.optimize_z3 is true (default) **)
+   types, provided ctx.optimize_smt is true (default) **)
 let rec ctyp_of_typ ctx typ =
   let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
   match typ_aux with
@@ -151,7 +151,7 @@ let rec ctyp_of_typ ctx typ =
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
              when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
            CT_int64
-        | n, m when ctx.optimize_z3 ->
+        | n, m when ctx.optimize_smt ->
            if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
              CT_int64
            else
@@ -173,7 +173,7 @@ let rec ctyp_of_typ ctx typ =
      let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
      begin match nexp_simp n with
      | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
-     | n when ctx.optimize_z3 && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
+     | n when ctx.optimize_smt && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
      | _ -> CT_lbits direction
      end
 
@@ -193,8 +193,8 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs)
 
-  | Typ_exist _ when ctx.optimize_z3 ->
-     (* Use Type_check.destruct_exist when optimising with z3, to
+  | Typ_exist _ when ctx.optimize_smt ->
+     (* Use Type_check.destruct_exist when optimising with SMT, to
         ensure that we don't cause any type variable clashes in
         local_env, and that we can optimize the existential based upon
         it's constraints. *)
diff --git a/src/constraint.ml b/src/constraint.ml
index b7fa50c3..09091655 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -55,6 +55,76 @@ open Util
 
 let opt_smt_verbose = ref false
 
+type solver = {
+    command : string;
+    header : string;
+    footer : string;
+    negative_literals : bool;
+    uninterpret_power : bool
+  }
+
+let cvc4_solver = {
+    command = "cvc4 -L smtlib2 --tlimit=2000";
+    header = "(set-logic QF_UFNIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let mathsat_solver = {
+    command = "mathsat";
+    header = "(set-logic QF_UFLIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let z3_solver = {
+    command = "z3 -t:1000 -T:10";
+    (* Using push and pop is much faster, I believe because
+       incremental mode uses a different solver. *)
+    header = "(push)\n";
+    footer = "(pop)\n";
+    negative_literals = true;
+    uninterpret_power = false;
+  }
+
+let yices_solver = {
+    command = "yices-smt2 --timeout=2";
+    header = "(set-logic QF_UFLIA)\n";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let vampire_solver = {
+    (* vampire sometimes likes to ignore its time limit *)
+    command = "timeout -s SIGKILL 3s vampire --time_limit 2s --input_syntax smtlib2 --mode smtcomp";
+    header = "";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let alt_ergo_solver ={
+    command = "alt-ergo";
+    header = "";
+    footer = "";
+    negative_literals = false;
+    uninterpret_power = true
+  }
+
+let opt_solver = ref z3_solver
+
+let set_solver = function
+  | "z3" -> opt_solver := z3_solver
+  | "alt-ergo" -> opt_solver := alt_ergo_solver
+  | "cvc4" -> opt_solver := cvc4_solver
+  | "mathsat" -> opt_solver := mathsat_solver
+  | "vampire" -> opt_solver := vampire_solver
+  | "yices" -> opt_solver := yices_solver
+  | unknown -> prerr_endline ("Unrecognised SMT solver " ^ unknown)
+
 (* SMTLIB v2.0 format is based on S-expressions so we have a
    lightweight representation of those here. *)
 type sexpr = List of (sexpr list) | Atom of string
@@ -101,6 +171,9 @@ let to_smt l vars constr =
     match aux with
     | Nexp_id id -> Atom (Util.zencode_string (string_of_id id))
     | Nexp_var v -> smt_var v
+    | Nexp_constant c
+         when Big_int.less_equal c (Big_int.of_int (-1)) && not !opt_solver.negative_literals ->
+       sfun "-" [Atom "0"; Atom (Big_int.to_string (Big_int.abs c))]
     | Nexp_constant c -> Atom (Big_int.to_string c)
     | Nexp_app (id, nexps) -> sfun (string_of_id id) (List.map smt_nexp nexps)
     | Nexp_times (nexp1, nexp2) -> sfun "*" [smt_nexp nexp1; smt_nexp nexp2]
@@ -108,6 +181,7 @@ let to_smt l vars constr =
     | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2]
     | Nexp_exp (Nexp_aux (Nexp_constant c, _)) when Big_int.greater c Big_int.zero ->
        Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c)))
+    | Nexp_exp nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp]
     | Nexp_exp nexp -> sfun "^" [Atom "2"; smt_nexp nexp]
     | Nexp_neg nexp -> sfun "-" [smt_nexp nexp]
   in
@@ -137,12 +211,13 @@ let to_smt l vars constr =
 
 let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string * (kid -> sexpr) =
   let variables, problem, var_map = to_smt l vars constr in
-  "(push)\n"
+  !opt_solver.header
   ^ variables ^ "\n"
+  ^ (if !opt_solver.uninterpret_power then "(declare-fun sailexp (Int) Int)\n" else "")
   ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem])
   ^ "\n(assert constraint)\n(check-sat)"
-  ^ (if get_model then "\n(get-model)" else "")
-  ^ "\n(pop)",
+  ^ (if get_model then "\n(get-model)\n" else "\n")
+  ^ !opt_solver.footer,
   var_map
 
 type smt_result = Unknown | Sat | Unsat
@@ -184,12 +259,12 @@ let save_digests () =
   DigestMap.iter output !known_problems;
   close_out out_chan
 
-let call_z3' l vars constraints : smt_result =
+let call_smt' l vars constraints : smt_result =
   let problems = [constraints] in
-  let z3_file, _ = smtlib_of_constraints l vars constraints in
+  let smt_file, _ = smtlib_of_constraints l vars constraints in
 
   if !opt_smt_verbose then
-    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file)
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file)
   else ();
 
   let rec input_lines chan = function
@@ -202,7 +277,7 @@ let call_z3' l vars constraints : smt_result =
        end
   in
 
-  let digest = Digest.string z3_file in
+  let digest = Digest.string smt_file in
   try
     let result = DigestMap.find digest !known_problems in
     result
@@ -210,45 +285,48 @@ let call_z3' l vars constraints : smt_result =
   | Not_found ->
     begin
       let (input_file, tmp_chan) =
-        try Filename.open_temp_file "constraint_" ".sat" with
-        | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling Z3: " ^ msg))
+        try Filename.open_temp_file "constraint_" ".smt2" with
+        | Sys_error msg -> raise (Reporting.err_general l ("Could not open temp file when calling SMT: " ^ msg))
       in
-      output_string tmp_chan z3_file;
+      output_string tmp_chan smt_file;
       close_out tmp_chan;
-      let z3_output =
+      let smt_output =
         try
-          let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-          let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
-          let _ = Unix.close_process_in z3_chan in
-          z3_output
+          let smt_out, smt_in, smt_err = Unix.open_process_full (!opt_solver.command ^ " " ^ input_file) (Unix.environment ()) in
+          let smt_output =
+            try List.combine problems (input_lines smt_out (List.length problems)) with
+            | End_of_file -> List.combine problems ["unknown"]
+          in
+          let _ = Unix.close_process_full (smt_out, smt_in, smt_err) in
+          smt_output
         with
-        | exn -> raise (Reporting.err_general l ("Error when calling z3: " ^ Printexc.to_string exn))
+        | exn -> raise (Reporting.err_general l ("Error when calling smt: " ^ Printexc.to_string exn))
       in
       Sys.remove input_file;
       try
-        let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
+        let (problem, _) = List.find (fun (_, result) -> result = "unsat") smt_output in
         known_problems := DigestMap.add digest Unsat !known_problems;
         Unsat
       with
       | Not_found ->
-         let unsolved = List.filter (fun (_, result) -> result = "unknown") z3_output in
+         let unsolved = List.filter (fun (_, result) -> result = "unknown") smt_output in
          if unsolved == []
          then (known_problems := DigestMap.add digest Sat !known_problems; Sat)
          else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
     end
 
-let call_z3 l vars constraints =
-  let t = Profile.start_z3 () in
-  let result = call_z3' l vars constraints in
-  Profile.finish_z3 t;
+let call_smt l vars constraints =
+  let t = Profile.start_smt () in
+  let result = call_smt' l vars constraints in
+  Profile.finish_smt t;
   result
 
-let rec solve_z3 l vars constraints var =
-  let z3_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
-  let z3_var = pp_sexpr (smt_var var) in
+let rec solve_smt l vars constraints var =
+  let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
+  let smt_var = pp_sexpr (smt_var var) in
 
-  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file);
-     prerr_endline ("Solving for " ^ z3_var); *)
+  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file);
+     prerr_endline ("Solving for " ^ smt_var); *)
 
   let rec input_all chan =
     try
@@ -259,25 +337,25 @@ let rec solve_z3 l vars constraints var =
       End_of_file -> []
   in
 
-  let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
-  output_string tmp_chan z3_file;
+  let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".smt2" in
+  output_string tmp_chan smt_file;
   close_out tmp_chan;
-  let z3_output =
+  let smt_output =
     try
-      let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-      let z3_output = String.concat " " (input_all z3_chan) in
-      let _ = Unix.close_process_in z3_chan in
-      z3_output
+      let smt_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+      let smt_output = String.concat " " (input_all smt_chan) in
+      let _ = Unix.close_process_in smt_chan in
+      smt_output
     with
     | exn ->
-       raise (Reporting.err_general l ("Got error when calling z3: " ^ Printexc.to_string exn))
+       raise (Reporting.err_general l ("Got error when calling smt: " ^ Printexc.to_string exn))
   in
   Sys.remove input_file;
-  let regexp = {|(define-fun |} ^ z3_var ^ {| () Int[ ]+\([0-9]+\))|} in
+  let regexp = {|(define-fun |} ^ smt_var ^ {| () Int[ ]+\([0-9]+\))|} in
   try
-    let _ = Str.search_forward (Str.regexp regexp) z3_output 0 in
-    let result = Big_int.of_string (Str.matched_group 1 z3_output) in
-    begin match call_z3 l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
+    let _ = Str.search_forward (Str.regexp regexp) smt_output 0 in
+    let result = Big_int.of_string (Str.matched_group 1 smt_output) in
+    begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
     | Unsat -> Some result
     | _ -> None
     end
diff --git a/src/constraint.mli b/src/constraint.mli
index fa318c35..e86c764a 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -54,11 +54,13 @@ open Ast_util
 
 val opt_smt_verbose : bool ref
 
+val set_solver : string -> unit
+
 type smt_result = Unknown | Sat | Unsat
 
 val load_digests : unit -> unit
 val save_digests : unit -> unit
 
-val call_z3 : l -> kind_aux KBindings.t -> n_constraint -> smt_result
+val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result
 
-val solve_z3 : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
+val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
diff --git a/src/profile.ml b/src/profile.ml
index 1a8bd30b..f64bdfe0 100644
--- a/src/profile.ml
+++ b/src/profile.ml
@@ -51,13 +51,13 @@
 let opt_profile = ref false
 
 type profile = {
-    z3_calls : int;
-    z3_time : float
+    smt_calls : int;
+    smt_time : float
   }
 
 let new_profile = {
-    z3_calls = 0;
-    z3_time = 0.0
+    smt_calls = 0;
+    smt_time = 0.0
   }
 
 let profile_stack = ref []
@@ -68,12 +68,12 @@ let update_profile f =
   | (p :: ps) ->
      profile_stack := f p :: ps
 
-let start_z3 () =
-  update_profile (fun p -> { p with z3_calls = p.z3_calls + 1 });
+let start_smt () =
+  update_profile (fun p -> { p with smt_calls = p.smt_calls + 1 });
   Sys.time ()
 
-let finish_z3 t =
-  update_profile (fun p -> { p with z3_time = p.z3_time +. (Sys.time () -. t) })
+let finish_smt t =
+  update_profile (fun p -> { p with smt_time = p.smt_time +. (Sys.time () -. t) })
 
 let start () =
   profile_stack := new_profile :: !profile_stack;
@@ -84,7 +84,7 @@ let finish msg t =
     begin match !profile_stack with
     | p :: ps ->
        prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profiled" |> magenta |> clear) msg (Sys.time () -. t));
-       prerr_endline (Printf.sprintf "  Z3 calls: %d, Z3 time: %fs" p.z3_calls p.z3_time);
+       prerr_endline (Printf.sprintf "  SMT calls: %d, SMT time: %fs" p.smt_calls p.smt_time);
        profile_stack := ps
     | [] -> ()
     end
diff --git a/src/sail.ml b/src/sail.ml
index 28c5db0a..9cf87af8 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -64,7 +64,7 @@ let opt_print_c = ref false
 let opt_print_latex = ref false
 let opt_print_coq = ref false
 let opt_print_cgen = ref false
-let opt_memo_z3 = ref true
+let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
 let opt_libs_lem = ref ([]:string list)
@@ -112,6 +112,9 @@ let options = Arg.align ([
   ( "-ocaml_generators",
     Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators),
     "<types> produce random generators for the given types");
+  ( "-smt_solver",
+    Arg.String (fun s -> Constraint.set_solver (String.trim s)),
+    "<solver> choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices.");
   ( "-latex",
     Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
     " pretty print the input to LaTeX");
@@ -208,7 +211,7 @@ let options = Arg.align ([
     " memoize calls to z3, improving performance when typechecking repeatedly (default)");
   ( "-no_memo_z3",
     Arg.Clear opt_memo_z3,
-    " do not memoize calls to z3");
+    " do not memoize calls to z3 (default)");
   ( "-memo",
     Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache],
     " memoize calls to z3, and intermediate compilation results");
@@ -268,7 +271,7 @@ let options = Arg.align ([
     "<verbosity> (debug) verbose typechecker output: 0 is silent");
   ( "-dsmt_verbose",
     Arg.Set Constraint.opt_smt_verbose,
-    " (debug) print SMTLIB constraints sent to Z3");
+    " (debug) print SMTLIB constraints sent to SMT solver");
   ( "-dno_cast",
     Arg.Set opt_dno_cast,
     " (debug) typecheck without any implicit casting");
diff --git a/src/type_check.ml b/src/type_check.ml
index 37f2cee7..65e13a19 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -401,7 +401,7 @@ module Env : sig
   val wf_nexp : ?exs:KidSet.t -> t -> nexp -> unit
   val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit
 
-  (* Some of the code in the environment needs to use the Z3 prover,
+  (* Some of the code in the environment needs to use the smt solver,
      which is defined below. To break the circularity this would cause
      (as the prove code depends on the environment), we add a
      reference to the prover to the initial environment. *)
@@ -1299,7 +1299,7 @@ and simp_typ_aux = function
      would become {('s:Bool) ('r: Bool), nc('r). bool('s & 'r)},
      wherein all the redundant boolean variables have been combined
      into a single one. Making this simplification allows us to avoid
-     having to pass large numbers of pointless variables to Z3 if we
+     having to pass large numbers of pointless variables to SMT if we
      ever bind this existential. *)
   | Typ_exist (vars, nc, Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool b, _)]), _)) ->
      let kids = KidSet.of_list (List.map kopt_kid vars) in
@@ -1385,11 +1385,11 @@ let rec nexp_variable_power (Nexp_aux (aux, _)) =
 let constraint_variable_power nc =
   List.exists nexp_variable_power (constraint_nexps nc)
 
-let prove_z3 env (NC_aux (_, l) as nc) =
+let prove_smt env (NC_aux (_, l) as nc) =
   let vars = Env.get_typ_vars env in
   let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
   let ncs = Env.get_constraints env in
-  match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs) with
+  match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs) with
   | Constraint.Unsat -> typ_debug (lazy "unsat"); true
   | Constraint.Sat -> typ_debug (lazy "sat"); false
   | Constraint.Unknown ->
@@ -1397,7 +1397,7 @@ let prove_z3 env (NC_aux (_, l) as nc) =
         constraints, even when such constraints are irrelevant *)
      let ncs' = List.concat (List.map constraint_conj ncs) in
      let ncs' = List.filter (fun nc -> not (constraint_variable_power nc)) ncs' in
-     match Constraint.call_z3 l vars (List.fold_left nc_and (nc_not nc) ncs') with
+     match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs') with
      | Constraint.Unsat -> typ_debug (lazy "unsat"); true
      | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false
 
@@ -1411,7 +1411,7 @@ let solve env (Nexp_aux (_, l) as nexp) =
     let vars = Env.get_typ_vars env in
     let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
     let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in
-    Constraint.solve_z3 l vars constr (mk_kid "solve#")
+    Constraint.solve_smt l vars constr (mk_kid "solve#")
 
 let debug_pos (file, line, _, _) =
   "(" ^ file ^ "/" ^ string_of_int line ^ ") "
@@ -1424,7 +1424,7 @@ let prove pos env nc =
   else ();
   match nc_aux with
   | NC_true -> true
-  | _ -> prove_z3 env nc
+  | _ -> prove_smt env nc
 
 (**************************************************************************)
 (* 3. Unification                                                         *)
-- 
cgit v1.2.3


From 18b38f6495ea8836f332e9b5da8525caac338e28 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 14 Feb 2019 17:09:58 +0000
Subject: Coq: Partial simplification of rich bool types This uses the SMT
 solver to spot rich `atom_bool` types which don't contain any information,
 replaces them with bool, and handles most of the construction and projection
 of them. The SMT part will be replaced by a simplification procedure soon,
 because it can't handle some important cases.

---
 src/pretty_print_coq.ml | 152 ++++++++++++++++++++++++++++++------------------
 1 file changed, 95 insertions(+), 57 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 27484560..501c610e 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -370,6 +370,34 @@ let doc_nc_fn id =
   | "not" -> string "negb"
   | s -> string s
 
+type ex_atom_bool = ExBool_simple | ExBool_val of bool | ExBool_complex
+
+let non_trivial_ex_atom_bool l kopts nc atom_nc =
+  let vars = KOptSet.union (kopts_of_constraint nc) (kopts_of_constraint atom_nc) in
+  let exists = KOptSet.of_list kopts in
+  if KOptSet.subset vars exists then
+    let kenv = List.fold_left (fun kenv kopt -> KBindings.add (kopt_kid kopt) (unaux_kind (kopt_kind kopt)) kenv) KBindings.empty kopts in
+    match Constraint.call_smt l kenv (nc_and nc atom_nc),
+          Constraint.call_smt l kenv (nc_and nc (nc_not atom_nc)) with
+    | Sat, Sat -> ExBool_simple
+    | Sat, Unsat -> ExBool_val true
+    | Unsat, Sat -> ExBool_val false
+    | _ -> ExBool_complex
+  else ExBool_complex
+
+type ex_kind = ExNone | ExBool | ExGeneral
+
+let classify_ex_type (Typ_aux (t,l) as t0) =
+  match t with
+  | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin
+      match non_trivial_ex_atom_bool l kopts nc atom_nc with
+      | ExBool_simple -> ExNone, t1
+      | ExBool_val _ -> ExBool, t1
+      | ExBool_complex -> ExGeneral, t1
+    end
+  | Typ_exist (_,_,t1) -> ExGeneral,t1
+  | _ -> ExNone,t0
+
 (* When making changes here, check whether they affect coq_nvars_of_typ *)
 let rec doc_typ_fns ctx =
   (* following the structure of parser for precedence *)
@@ -476,13 +504,18 @@ let rec doc_typ_fns ctx =
                        [doc_var ctx var; colon; tpp;
                         ampersand;
                         doc_arithfact ctx ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc])
-          | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) ->
-             let var = mk_kid "_bool" in (* TODO collision avoid *)
-             let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in
-             braces (separate space
-                       [doc_var ctx var; colon; string "bool";
-                        ampersand;
-                        doc_arithfact ctx ~exists:(List.map kopt_kid kopts) nc])
+          | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin
+             match non_trivial_ex_atom_bool l kopts nc atom_nc with
+             | ExBool_simple -> string "bool"
+             | ExBool_val t -> string "Bool(" ^^ if t then string "True)" else string "False)"
+             | ExBool_complex ->
+                let var = mk_kid "_bool" in (* TODO collision avoid *)
+                let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in
+                braces (separate space
+                          [doc_var ctx var; colon; string "bool";
+                           ampersand;
+                           doc_arithfact ctx ~exists:(List.map kopt_kid kopts) nc])
+            end
           | _ ->
              raise (Reporting.err_todo l
                   ("Non-atom existential type not yet supported in Coq: " ^
@@ -1034,9 +1067,14 @@ let doc_exp, doc_let =
       let typ = expand_range_type typ in
       match destruct_exist_plain typ with
       | None -> epp
+      | Some (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l)) -> begin
+          match non_trivial_ex_atom_bool l kopts nc atom_nc with
+          | ExBool_simple -> epp
+          | ExBool_val t -> wrap_parens (string "build_Bool" ^/^ epp)
+          | ExBool_complex -> wrap_parens (string "build_ex" ^/^ epp)
+        end
       | Some _ ->
-         let epp = string "build_ex" ^/^ epp in
-         if aexp_needed then parens epp else epp
+         wrap_parens (string "build_ex" ^/^ epp)
     in
     let rec construct_dep_pairs env =
       let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) =
@@ -1049,8 +1087,14 @@ let doc_exp, doc_let =
            let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in
            let build_ex, out_typ =
              match destruct_exist_plain typ' with
-             | Some (_,_,t) -> true, t
-             | None -> false, typ'
+             | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin
+                 match non_trivial_ex_atom_bool l kopts nc atom_nc with
+                 | ExBool_simple -> None, t
+                 | ExBool_val _ -> Some "build_Bool", t
+                 | ExBool_complex -> Some "build_ex", t
+               end
+             | Some (_,_,t) -> Some "build_ex", t
+             | None -> None, typ'
            in
            let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in
            let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in
@@ -1063,16 +1107,17 @@ let doc_exp, doc_let =
                   not (similar_nexps ctxt (env_of exp) n1 n2)
                | _ -> false
            in
-           let exp_pp = expV (want_parens || autocast || build_ex) exp in
+           let exp_pp = expV (want_parens || autocast || Util.is_some build_ex) exp in
            let exp_pp =
              if autocast then
                let exp_pp = string "autocast" ^^ space ^^ exp_pp in
-               if want_parens || build_ex then parens exp_pp else exp_pp
+               if want_parens || Util.is_some build_ex then parens exp_pp else exp_pp
              else exp_pp
-           in if build_ex then
-                let exp_pp = string "build_ex" ^^ space ^^ exp_pp in
+           in match build_ex with
+              | Some s ->
+                let exp_pp = string s ^^ space ^^ exp_pp in
                 if want_parens then parens exp_pp else exp_pp
-              else exp_pp
+              | None -> exp_pp
       in aux
     in
     let liftR doc =
@@ -1499,21 +1544,9 @@ let doc_exp, doc_let =
          debug ctxt (lazy (" on expr of type " ^ string_of_typ inner_typ));
          debug ctxt (lazy (" where type expected is " ^ string_of_typ outer_typ))
        in
-       let outer_ex,outer_typ' =
-         match outer_typ with
-         | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
-         | t1 -> false,t1
-       in
-       let cast_ex,cast_typ' =
-         match cast_typ with
-         | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
-         | t1 -> false,t1
-       in
-       let inner_ex,inner_typ' =
-         match inner_typ with
-         | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1
-         | t1 -> false,t1
-       in
+       let outer_ex,outer_typ' = classify_ex_type outer_typ in
+       let cast_ex,cast_typ' = classify_ex_type cast_typ in
+       let inner_ex,inner_typ' = classify_ex_type inner_typ in
        let autocast =
                 (* Avoid using helper functions which simplify the nexps *)
          is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' &&
@@ -1526,30 +1559,34 @@ let doc_exp, doc_let =
        let effects = effectful (effect_of e) in
        let epp =
          if effects then
-           if inner_ex then
-             if cast_ex
-             (* If the types are the same use the cast as a hint to Coq,
-                otherwise derive the new type from the old one. *)
-             then if alpha_equivalent env inner_typ cast_typ
-                  then epp
-                  else string "derive_m" ^^ space ^^ epp
-             else string "projT1_m" ^^ space ^^ epp
-           else if cast_ex
-           then string "build_ex_m" ^^ space ^^ epp
-           else epp
-         else if cast_ex
-         then string "build_ex" ^^ space ^^ epp
-         else epp
+           match inner_ex, cast_ex with
+           | ExGeneral, ExGeneral ->
+              (* If the types are the same use the cast as a hint to Coq,
+                 otherwise derive the new type from the old one. *)
+              if alpha_equivalent env inner_typ cast_typ
+              then epp
+              else string "derive_m" ^^ space ^^ epp
+           | ExGeneral, ExNone ->
+              string "projT1_m" ^^ space ^^ epp
+           | ExNone, ExGeneral ->
+              string "build_ex_m" ^^ space ^^ epp
+           | ExNone, ExNone -> epp
+         else match cast_ex with
+              | ExGeneral -> string "build_ex" ^^ space ^^ epp
+              | ExBool -> string "build_Bool" ^^ space ^^ epp
+              | ExNone -> epp
        in
        let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in
        let epp =
          if effects then
-           if cast_ex && not outer_ex
-           then string "projT1_m" ^^ space ^^ parens epp
-           else epp
-         else if cast_ex
-         then string "projT1" ^^ space ^^ parens epp
-         else epp
+           match cast_ex, outer_ex with
+           | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp
+           | ExBool, ExNone -> string "projBool_m" ^^ space ^^ parens epp
+           | _ -> epp
+         else match cast_ex with
+              | ExGeneral -> string "projT1" ^^ space ^^ parens epp
+              | ExBool -> string "projBool" ^^ space ^^ parens epp
+              | ExNone -> epp
        in
        let epp =
          if autocast then
@@ -1718,10 +1755,10 @@ let doc_exp, doc_let =
                 | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_)
                     when not (is_enum (env_of e1) id) ->
                       let full_typ = (expand_range_type typ) in
-                      let binder = match destruct_exist_plain (Env.expand_synonyms (env_of e1) full_typ) with
-                        | Some _ ->
+                      let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with
+                        | ExGeneral, _ ->
                            squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
-                        | _ ->
+                        | (ExBool | ExNone), _ ->
                            parens (separate space [doc_id id; colon; doc_typ ctxt typ])
                       in separate space [string ">>= fun"; binder; bigarrow]
                 | _ ->
@@ -2204,9 +2241,10 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     | _ -> 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 build_ex = match destruct_exist_plain (Env.expand_synonyms env (expand_range_type ret_typ)) with
-    | Some _ -> Some "build_ex"
-    | _ -> build_ex
+  let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with
+    | ExGeneral, _ -> Some "build_ex"
+    | ExBool, _ -> Some "build_Bool"
+    | ExNone, _ -> build_ex
   in
   let ids_to_avoid = all_ids pexp in
   let bound_kids = tyvars_of_typquant tq in
-- 
cgit v1.2.3


From a62061fd64d3fb8a31f115a3d059da4346a13d85 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 15 Feb 2019 18:09:33 +0000
Subject: Tweak intermediate language names for loop combinators to allow
 reparsing This should produce identical Lem and Coq output, but allow dumped
 Sail ASTs from the final stages of rewriting to be reread with -dmagic_hash.

---
 src/pretty_print_coq.ml |  5 +++--
 src/pretty_print_lem.ml |  5 +++--
 src/rewrites.ml         | 12 ++++++------
 3 files changed, 12 insertions(+), 10 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 501c610e..c321cb26 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1207,7 +1207,7 @@ let doc_exp, doc_let =
           wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
        (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "None", _) as none -> doc_id_ctor none
-       | Id_aux (Id "foreach", _) ->
+       | Id_aux (Id "foreach#", _) ->
           begin
             match args with
             | [from_exp; to_exp; step_exp; ord_exp; vartuple; body] ->
@@ -1254,7 +1254,8 @@ let doc_exp, doc_let =
           | _ -> raise (Reporting.err_unreachable l __POS__
              "Unexpected number of arguments for loop combinator")
           end
-       | Id_aux (Id (("while" | "until") as combinator), _) ->
+       | Id_aux (Id (("while#" | "until#") as combinator), _) ->
+          let combinator = String.sub combinator 0 (String.length combinator - 1) in
           begin
             match args with
             | [cond; varstuple; body] ->
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index dee0a29f..3e7911fe 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -668,7 +668,7 @@ let doc_exp_lem, doc_let_lem =
           let call = doc_id_lem (append_id f "M") in
           wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
        (* temporary hack to make the loop body a function of the temporary variables *)
-       | Id_aux (Id "foreach", _) ->
+       | Id_aux (Id "foreach#", _) ->
           begin
             match args with
             | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
@@ -713,7 +713,8 @@ let doc_exp_lem, doc_let_lem =
           | _ -> raise (Reporting.err_unreachable l __POS__
             "Unexpected number of arguments for loop combinator")
           end
-       | Id_aux (Id (("while" | "until") as combinator), _) ->
+       | Id_aux (Id (("while#" | "until#") as combinator), _) ->
+          let combinator = String.sub combinator 0 (String.length combinator - 1) in
           begin
             match args with
             | [cond; varstuple; body] ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 31117f33..e40b7387 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3826,7 +3826,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
        let v =
          fix_eff_exp (annot_exp (E_let (lb_lower,
            fix_eff_exp (annot_exp (E_let (lb_upper,
-             fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body]))
+             fix_eff_exp (annot_exp (E_app (mk_id "foreach#", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body]))
                el env (typ_of exp4))))
              el env (typ_of exp4))))
            el env (typ_of exp4)) in
@@ -3842,8 +3842,8 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
         let body = rewrite_var_updates (add_vars overwrite body vars) in
         let (E_aux (_,(_,bannot))) = body in
         let fname = match loop with
-          | While -> "while"
-          | Until -> "until" in
+          | While -> "while#"
+          | Until -> "until#" in
         let funcl = Id_aux (Id fname,gen_loc el) in
         let v = E_aux (E_app (funcl,[cond;tuple_exp vars;body]), (gen_loc el, bannot)) in
         Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
@@ -4144,9 +4144,9 @@ let rewrite_defs_remove_superfluous_returns env =
 
 let rewrite_defs_remove_e_assign env (Defs defs) =
   let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
-    [("foreach", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
-     ("while", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
-     ("until", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
+    [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
+     ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
+     ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
   let rewrite_exp _ e =
     replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in
   rewrite_defs_base
-- 
cgit v1.2.3


From 962b584da179b8737a67172d15d8cc58bb538fd6 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 15 Feb 2019 18:19:26 +0000
Subject: Fix bug in Int-synonym expansion

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

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index 65e13a19..0c936860 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -548,6 +548,10 @@ end = struct
     match aux with
     | NC_or (nc1, nc2) -> NC_aux (NC_or (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
     | NC_and (nc1, nc2) -> NC_aux (NC_and (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
+    | NC_equal (n1, n2) -> NC_aux (NC_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
+    | NC_not_equal (n1, n2) -> NC_aux (NC_not_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
+    | NC_bounded_le (n1, n2) -> NC_aux (NC_bounded_le (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
+    | NC_bounded_ge (n1, n2) -> NC_aux (NC_bounded_ge (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
     | NC_app (id, args) ->
        (try
           begin match Bindings.find id env.typ_synonyms l env args with
@@ -555,7 +559,7 @@ end = struct
           | arg -> typ_error env l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
           end
         with Not_found -> NC_aux (NC_app (id, List.map (expand_synonyms_arg env) args), l))
-    | NC_true | NC_false | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _ | NC_var _ | NC_set _ -> nc
+    | NC_true | NC_false | NC_var _ | NC_set _ -> nc
 
   and expand_nexp_synonyms env (Nexp_aux (aux, l) as nexp) =
     typ_debug ~level:2 (lazy ("Expanding " ^ string_of_nexp nexp));
-- 
cgit v1.2.3


From 112f02934f30c631996ff837dd7687039d274e97 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 18 Feb 2019 15:24:58 +0000
Subject: Fix latex output

Fixes #33
---
 src/latex.ml | 67 +++++++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 46 insertions(+), 21 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index a0660daa..1806da47 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -71,20 +71,23 @@ type latex_state =
   { mutable noindent : bool;
     mutable this : id option;
     mutable norefs : StringSet.t;
-    mutable generated_names : string Bindings.t
+    mutable generated_names : string Bindings.t;
+    mutable commands : StringSet.t
   }
 
 let reset_state state =
   state.noindent <- false;
   state.this <- None;
   state.norefs <- StringSet.empty;
-  state.generated_names <- Bindings.empty
+  state.generated_names <- Bindings.empty;
+  state.commands <- StringSet.empty
 
 let state =
   { noindent = false;
     this = None;
     norefs = StringSet.empty;
-    generated_names = Bindings.empty
+    generated_names = Bindings.empty;
+    commands = StringSet.empty
   }
 
 let rec unique_postfix n =
@@ -285,24 +288,39 @@ let add_links str =
   in
   Str.global_substitute r subst str
 
+let rec skip_lines in_chan = function
+  | n when n <= 0 -> ()
+  | n -> ignore (input_line in_chan); skip_lines in_chan (n - 1)
+
+let rec read_lines in_chan = function
+  | n when n <= 0 -> []
+  | n ->
+     let l = input_line in_chan in
+     let ls = read_lines in_chan (n - 1) in
+     l :: ls
+
 let latex_loc no_loc l =
-  match l with
-  | Parse_ast.Range (_, _) | Parse_ast.Documented (_, Parse_ast.Range (_, _)) ->
+  match simp_loc l with
+  | Some (p1, p2) ->
      begin
-       let using_color = !Util.opt_colors in
-       Util.opt_colors := false;
-       let code = Util.split_on_char '\n' (Reporting.loc_to_string l) in
-       let doc = match code with
-         | _ :: _ :: code -> string (add_links (String.concat "\n" code))
-         | _ -> empty
-       in
-       Util.opt_colors := using_color;
-       doc ^^ hardline
+       let open Lexing in
+       try
+         let in_chan = open_in p1.pos_fname in
+         try
+           skip_lines in_chan (p1.pos_lnum - 3);
+           let code = read_lines in_chan ((p2.pos_lnum - p1.pos_lnum) + 3) in
+           close_in in_chan;
+           let doc = match code with
+             | _ :: _ :: code -> string (add_links (String.concat "\n" code))
+             | _ -> empty
+           in
+           doc ^^ hardline
+         with
+         | _ -> close_in_noerr in_chan; docstring l ^^ no_loc
+       with
+       | _ -> docstring l ^^ no_loc
      end
-
-  | _ -> docstring l ^^ no_loc
-
-let commands = ref StringSet.empty
+  | None -> docstring l ^^ no_loc
 
 let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) =
   Pretty_print_sail.doc_id id ^^ space
@@ -322,10 +340,17 @@ let rec latex_command cat id no_loc ((l, _) as annot) =
   let doc = if cat = Val then no_loc else latex_loc no_loc l in
   output_string chan (Pretty_print_sail.to_string doc);
   close_out chan;
+  let command = sprintf "\\%s%s%s" !opt_prefix (category_name cat) (latex_id id) in
+  if StringSet.mem command state.commands then
+    (Util.warn ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty)
+  else
+    begin
+      state.commands <- StringSet.add command state.commands;
 
-  ksprintf string "\\newcommand{\\%s%s%s}{\\phantomsection%s\\saildoc%s{" !opt_prefix (category_name cat) (latex_id id) labelling (category_name_simple cat)
-  ^^ docstring l ^^ string "}{"
-  ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file)
+      ksprintf string "\\newcommand{%s}{\\phantomsection%s\\saildoc%s{" command labelling (category_name_simple cat)
+      ^^ docstring l ^^ string "}{"
+      ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file)
+    end
 
 let latex_label str id =
   string (Printf.sprintf "\\label{%s:%s}" str (Util.zencode_string (string_of_id id)))
-- 
cgit v1.2.3


From 9de3f45de277d8a8f264a425d9121fe91ad80345 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 18 Feb 2019 17:47:37 +0000
Subject: Make sure we remove bitvector patterns within guards

Fixes #34
---
 src/rewrites.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index e40b7387..3c000f17 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1549,10 +1549,11 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_ex
        | None -> Pat_aux (Pat_exp (pat', body'), annot'))
      | Pat_aux (Pat_when (pat,guard,body),annot') ->
        let (pat',(guard',decls,_)) = remove_bitvector_pat pat in
+       let guard'' = rewrite_rec guard in
        let body' = decls (rewrite_rec body) in
        (match guard' with
-       | Some guard' -> Pat_aux (Pat_when (pat', bitwise_and_exp (decls guard) guard', body'), annot')
-       | None -> Pat_aux (Pat_when (pat', (decls guard), body'), annot')) in
+       | Some guard' -> Pat_aux (Pat_when (pat', bitwise_and_exp (decls guard'') guard', body'), annot')
+       | None -> Pat_aux (Pat_when (pat', (decls guard''), body'), annot')) in
     rewrap (E_case (e, List.map rewrite_pexp ps))
   | E_let (LB_aux (LB_val (pat,v),annot'),body) ->
      let (pat,(_,decls,_)) = remove_bitvector_pat pat in
-- 
cgit v1.2.3


From 66e6585b9696ffc91a8609e5d52bfe6d5adff1b6 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 18 Feb 2019 19:12:17 +0000
Subject: Rename Type_check.solve -> Type_check.solve_unique

---
 src/constraint.ml       |  2 +-
 src/constraint.mli      |  2 +-
 src/monomorphise.ml     | 16 ++++++++--------
 src/pretty_print_lem.ml |  2 +-
 src/type_check.ml       |  4 ++--
 src/type_check.mli      |  2 +-
 6 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'src')

diff --git a/src/constraint.ml b/src/constraint.ml
index 09091655..2c5150a5 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -321,7 +321,7 @@ let call_smt l vars constraints =
   Profile.finish_smt t;
   result
 
-let rec solve_smt l vars constraints var =
+let rec solve_unique_smt l vars constraints var =
   let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
   let smt_var = pp_sexpr (smt_var var) in
 
diff --git a/src/constraint.mli b/src/constraint.mli
index e86c764a..fb6e0fcd 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -63,4 +63,4 @@ val save_digests : unit -> unit
 
 val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result
 
-val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
+val solve_unique_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 8c52fce1..acc31456 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -2263,7 +2263,7 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) =
       prove __POS__ env (NC_aux (NC_equal (size,nexp), Parse_ast.Unknown))
     in
     if is_nexp_constant size then size else
-      match solve env size with
+      match solve_unique env size with
       | Some n -> nconstant n
       | None ->
          match List.find is_equal bound_nexps with
@@ -2930,7 +2930,7 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps =
   | _ -> None
 
 let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) =
-  match solve typ_env nexp with
+  match solve_unique typ_env nexp with
   | Some n -> nconstant n
   | None ->
      let is_equal kid =
@@ -3691,7 +3691,7 @@ let rec rewrite_app env typ (id,args) =
     let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
     match size with
     | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp)
-    | _ -> match solve env size with
+    | _ -> match solve_unique env size with
       | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp)
       | None -> e
   in
@@ -3711,7 +3711,7 @@ let rec rewrite_app env typ (id,args) =
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in begin
-         match solve env midsize with
+         match solve_unique env midsize with
          | Some c ->
             let midtyp = vector_typ (nconstant c) order bittyp in
             E_app (append,
@@ -3739,7 +3739,7 @@ let rec rewrite_app env typ (id,args) =
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in begin
-         match solve env midsize with
+         match solve_unique env midsize with
          | Some c ->
             let midtyp = vector_typ (nconstant c) order bittyp in
             E_app (append,
@@ -3797,7 +3797,7 @@ let rec rewrite_app env typ (id,args) =
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in begin
-         match solve env midsize with
+         match solve_unique env midsize with
          | Some c ->
             let midtyp = vector_typ (nconstant c) order bittyp in
             try_cast_to_typ
@@ -4000,7 +4000,7 @@ struct
 
 let simplify_size_nexp env quant_kids nexp =
   let rec aux (Nexp_aux (ne,l) as nexp) =
-    match solve env nexp with
+    match solve_unique env nexp with
     | Some n -> Some (nconstant n)
     | None ->
        let is_equal kid =
@@ -4191,7 +4191,7 @@ let fill_in_type env typ =
     | K_order
     | K_bool -> subst
     | K_int ->
-       (match solve env (nvar kid) with
+       (match solve_unique env (nvar kid) with
        | None -> subst
        | Some n -> KBindings.add kid (nconstant n) subst)) tyvars KBindings.empty in
   subst_src_typ subst typ
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 3e7911fe..9d472e15 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -359,7 +359,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp =
          Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       match Type_check.solve env size with
+       match Type_check.solve_unique env size with
        | Some n -> mk_typ (nconstant n)
        | None ->
           let is_equal nexp =
diff --git a/src/type_check.ml b/src/type_check.ml
index 0c936860..ada04c24 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1405,7 +1405,7 @@ let prove_smt env (NC_aux (_, l) as nc) =
      | Constraint.Unsat -> typ_debug (lazy "unsat"); true
      | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false
 
-let solve env (Nexp_aux (_, l) as nexp) =
+let solve_unique env (Nexp_aux (_, l) as nexp) =
   typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
                    ^ " |- " ^ string_of_nexp nexp ^ " = ?"));
   match nexp with
@@ -1415,7 +1415,7 @@ let solve env (Nexp_aux (_, l) as nexp) =
     let vars = Env.get_typ_vars env in
     let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
     let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in
-    Constraint.solve_smt l vars constr (mk_kid "solve#")
+    Constraint.solve_unique_smt l vars constr (mk_kid "solve#")
 
 let debug_pos (file, line, _, _) =
   "(" ^ file ^ "/" ^ string_of_int line ^ ") "
diff --git a/src/type_check.mli b/src/type_check.mli
index 8ea0b3e2..00439412 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -316,7 +316,7 @@ val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t
    untrustworthy. *)
 val prove : (string * int * int * int) -> Env.t -> n_constraint -> bool
 
-val solve : Env.t -> nexp -> Big_int.num option
+val solve_unique : Env.t -> nexp -> Big_int.num option
 
 val canonicalize : Env.t -> typ -> typ
 
-- 
cgit v1.2.3


From 1234d5404cea88a92e1fd89cc419173f8ca2e7c5 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 18 Feb 2019 20:25:01 +0000
Subject: Add option to linearize constraints containing exponentials

When adding a constraint such as `x <= 2^n-1` to an environment
containing e.g. `n in {32, 64}` or similar, we can enumerate all
values of n and add `n == 32 & x <= 2^32-1 | n == 64 & x <= 2^64-1`
instead. The exponentials then get simplified away, which means that
we stay on the SMT solver's happy path.

This is enabled by the (experimental, name subject to change) flag
-smt_linearize, as this both allows some things to typecheck that
didn't before (see pow_32_64.sail in test/typecheck/pass), but also
may potentially cause some things that typecheck to no longer
typecheck for SMT solvers like z3 that have some support for reasoning
with power functions, or where we could simply treat the exponential
as a uninterpreted function.

Also make the -dsmt_verbose option print the smtlib2 files for the
solve functions in constraint.ml. We currently ignore the -smt_solver
option for these, because smtlib does not guarantee a standard format
for the output of get-model, so we always use z3 in this case.

Following the last commit where solve got renamed solve_unique, there
are now 3 functions for solving constraints:

* Constraint.solve_smt, which finds a solution if one exists

* Constraint.solve_all_smt, which returns all possible
  solutions. Currently there's no bound, so this could loop forever if
  there are infinite solutions.

* Constraint.solve_unique, which returns a unique solution if one exists

Fix a bug where $option pragmas were dropped unnecessarily.
---
 src/ast_util.ml     |   9 +++-
 src/constraint.ml   |  35 ++++++++++----
 src/constraint.mli  |   4 ++
 src/process_file.ml |   4 +-
 src/sail.ml         |   5 +-
 src/type_check.ml   | 129 ++++++++++++++++++++++++++++++++--------------------
 src/type_check.mli  |   5 ++
 7 files changed, 128 insertions(+), 63 deletions(-)

(limited to 'src')

diff --git a/src/ast_util.ml b/src/ast_util.ml
index fcfa619e..e4287249 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -417,11 +417,16 @@ let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
 let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
 let nc_lt n1 n2 = nc_lteq (nsum n1 (nint 1)) n2
 let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1))
-let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
 let nc_var kid = mk_nc (NC_var kid)
 let nc_true = mk_nc NC_true
 let nc_false = mk_nc NC_false
 
+let nc_or nc1 nc2 =
+  match nc1, nc2 with
+  | _, NC_aux (NC_false, _) -> nc1
+  | NC_aux (NC_false, _), _ -> nc2
+  | _, _ -> mk_nc (NC_or (nc1, nc2))
+
 let nc_and nc1 nc2 =
   match nc1, nc2 with
   | _, NC_aux (NC_true, _) -> nc1
@@ -439,7 +444,7 @@ let arg_kopt (KOpt_aux (KOpt_kind (K_aux (k, _), v), l)) =
   | K_order -> arg_order (Ord_aux (Ord_var v, l))
   | K_bool -> arg_bool (nc_var v)
   | K_type -> arg_typ (mk_typ (Typ_var v))
-           
+
 let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc]))
 
 let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
diff --git a/src/constraint.ml b/src/constraint.ml
index 2c5150a5..5402f6f7 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -321,12 +321,13 @@ let call_smt l vars constraints =
   Profile.finish_smt t;
   result
 
-let rec solve_unique_smt l vars constraints var =
+let solve_smt l vars constraints var =
   let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
   let smt_var = pp_sexpr (smt_var var) in
 
-  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file);
-     prerr_endline ("Solving for " ^ smt_var); *)
+  if !opt_smt_verbose then
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are (solve for %s): \n%s%!" smt_var smt_file)
+  else ();
 
   let rec input_all chan =
     try
@@ -355,9 +356,27 @@ let rec solve_unique_smt l vars constraints var =
   try
     let _ = Str.search_forward (Str.regexp regexp) smt_output 0 in
     let result = Big_int.of_string (Str.matched_group 1 smt_output) in
-    begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
-    | Unsat -> Some result
-    | _ -> None
-    end
+    Some result
   with
-    Not_found -> None
+  | Not_found -> None
+
+let solve_all_smt l vars constraints var =
+  let rec aux results =
+    let constraints = List.fold_left (fun ncs r -> (nc_and ncs (nc_neq (nconstant r) (nvar var)))) constraints results in
+    match solve_smt l vars constraints var with
+    | Some result -> aux (result :: results)
+    | None ->
+       match call_smt l vars constraints with
+       | Unsat -> Some results
+       | _ -> None
+  in
+  aux []
+
+let solve_unique_smt l vars constraints var =
+  match solve_smt l vars constraints var with
+  | Some result ->
+     begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
+     | Unsat -> Some result
+     | _ -> None
+     end
+  | None -> None
diff --git a/src/constraint.mli b/src/constraint.mli
index fb6e0fcd..b5d6ff6b 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -63,4 +63,8 @@ val save_digests : unit -> unit
 
 val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result
 
+val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
+
+val solve_all_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num list option
+
 val solve_unique_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option
diff --git a/src/process_file.ml b/src/process_file.ml
index 52e0cd08..e7bf8d30 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -159,7 +159,7 @@ let rec preprocess opts = function
      symbols := StringSet.add symbol !symbols;
      preprocess opts defs
 
-  | Parse_ast.DEF_pragma ("option", command, l) :: defs ->
+  | (Parse_ast.DEF_pragma ("option", command, l) as opt_pragma) :: defs ->
      begin
        try
          let args = Str.split (Str.regexp " +") command in
@@ -167,7 +167,7 @@ let rec preprocess opts = function
        with
        | Arg.Bad message | Arg.Help message -> raise (Reporting.err_general l message)
      end;
-     preprocess opts defs
+     opt_pragma :: preprocess opts defs
 
   | Parse_ast.DEF_pragma ("ifndef", symbol, l) :: defs ->
      let then_defs, else_defs, defs = cond_pragma l defs in
diff --git a/src/sail.ml b/src/sail.ml
index 9cf87af8..64ccd341 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -115,8 +115,11 @@ let options = Arg.align ([
   ( "-smt_solver",
     Arg.String (fun s -> Constraint.set_solver (String.trim s)),
     "<solver> choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices.");
+  ( "-smt_linearize",
+    Arg.Set Type_check.opt_smt_linearize,
+    "(experimental) force linearization for constraints involving exponentials");
   ( "-latex",
-    Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ],
+    Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec],
     " pretty print the input to LaTeX");
   ( "-latex_prefix",
     Arg.String (fun prefix -> Latex.opt_prefix := prefix),
diff --git a/src/type_check.ml b/src/type_check.ml
index ada04c24..0da7f753 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -72,6 +72,10 @@ let opt_no_lexp_bounds_check = ref false
    We prefer not to do it for latex output but it is otherwise a good idea. *)
 let opt_expand_valspec = ref true
 
+(* Linearize cases involving power where we would otherwise require
+   the SMT solver to use non-linear arithmetic. *)
+let opt_smt_linearize = ref false
+
 let depth = ref 0
 
 let rec indent n = match n with
@@ -247,6 +251,50 @@ and strip_kinded_id_aux = function
 and strip_kind = function
   | K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown)
 
+let rec typ_nexps (Typ_aux (typ_aux, l)) =
+  match typ_aux with
+  | Typ_internal_unknown -> []
+  | Typ_id v -> []
+  | Typ_var kid -> []
+  | Typ_tup typs -> List.concat (List.map typ_nexps typs)
+  | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
+  | Typ_exist (kids, nc, typ) -> typ_nexps typ
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
+  | Typ_bidir (typ1, typ2) ->
+     typ_nexps typ1 @ typ_nexps typ2
+and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
+  match typ_arg_aux with
+  | A_nexp n -> [n]
+  | A_typ typ -> typ_nexps typ
+  | A_bool nc -> constraint_nexps nc
+  | A_order ord -> []
+and constraint_nexps (NC_aux (nc_aux, l)) =
+  match nc_aux with
+  | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_not_equal (n1, n2) ->
+     [n1; n2]
+  | NC_set _ | NC_true | NC_false | NC_var _ -> []
+  | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2
+  | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args)
+
+(* Return a KidSet containing all the type variables appearing in
+   nexp, where nexp occurs underneath a Nexp_exp, i.e. 2^nexp *)
+let rec nexp_power_variables (Nexp_aux (aux, _)) =
+  match aux with
+  | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) ->
+     KidSet.union (nexp_power_variables n1) (nexp_power_variables n2)
+  | Nexp_neg n ->
+     nexp_power_variables n
+  | Nexp_id _ | Nexp_var _ | Nexp_constant _ ->
+     KidSet.empty
+  | Nexp_app (_, ns) ->
+     List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables ns)
+  | Nexp_exp n ->
+     tyvars_of_nexp n
+
+let constraint_power_variables nc =
+  List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables (constraint_nexps nc))
+
 let rec name_pat (P_aux (aux, _)) =
   match aux with
   | P_id id | P_as (_, id) -> Some ("_" ^ string_of_id id)
@@ -262,7 +310,7 @@ let fresh_existential k =
 let named_existential k = function
   | Some n -> mk_kopt k (mk_kid n)
   | None -> fresh_existential k
- 
+
 let destruct_exist_plain ?name:(name=None) typ =
   match typ with
   | Typ_aux (Typ_exist ([kopt], nc, typ), _) ->
@@ -1089,7 +1137,7 @@ end = struct
   let add_typ_var l (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) env =
     if KBindings.mem v env.typ_vars then begin
         let n = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0 in
-        let s_l, s_k = KBindings.find v env.typ_vars in 
+        let s_l, s_k = KBindings.find v env.typ_vars in
         let s_v = Kid_aux (Var (string_of_kid v ^ "#" ^ string_of_int n), l) in
         typ_print (lazy (Printf.sprintf "%stype variable (shadowing %s) %s : %s" adding (string_of_kid s_v) (string_of_kid v) (string_of_kind_aux k)));
         { env with
@@ -1108,11 +1156,34 @@ end = struct
   let add_constraint constr env =
     wf_constraint env constr;
     let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in
-    match nc_aux with
-    | NC_true -> env
-    | _ ->
-       typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr));
-       { env with constraints = constr :: env.constraints }
+    let power_vars = constraint_power_variables constr in
+    if KidSet.cardinal power_vars > 1 && !opt_smt_linearize then
+      typ_error env l ("Cannot add constraint " ^ string_of_n_constraint constr
+                       ^ " where more than two variables appear within an exponential")
+    else if KidSet.cardinal power_vars = 1 && !opt_smt_linearize then
+      let v = KidSet.choose power_vars in
+      let constrs = List.fold_left nc_and nc_true (get_constraints env) in
+      begin match Constraint.solve_all_smt l (get_typ_vars env) constrs v with
+      | Some solutions ->
+         typ_print (lazy (Util.("Linearizing " |> red |> clear) ^ string_of_n_constraint constr
+                          ^ " for " ^ string_of_kid v ^ " in " ^ Util.string_of_list ", " Big_int.to_string solutions));
+         let linearized =
+           List.fold_left
+             (fun c s -> nc_or c (nc_and (nc_eq (nvar v) (nconstant s)) (constraint_subst v (arg_nexp (nconstant s)) constr)))
+             nc_false solutions
+         in
+         typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint linearized));
+         { env with constraints = linearized :: env.constraints }
+      | None ->
+         typ_error env l ("Type variable " ^ string_of_kid v
+                          ^ " must have a finite number of solutions to add " ^ string_of_n_constraint constr)
+      end
+    else
+      match nc_aux with
+      | NC_true -> env
+      | _ ->
+         typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr));
+         { env with constraints = constr :: env.constraints }
 
   let get_ret_typ env = env.ret_typ
 
@@ -1326,32 +1397,6 @@ and simp_typ_aux = function
 
   | typ_aux -> typ_aux
 
-let rec typ_nexps (Typ_aux (typ_aux, l)) =
-  match typ_aux with
-  | Typ_internal_unknown -> []
-  | Typ_id v -> []
-  | Typ_var kid -> []
-  | Typ_tup typs -> List.concat (List.map typ_nexps typs)
-  | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
-  | Typ_exist (kids, nc, typ) -> typ_nexps typ
-  | Typ_fn (arg_typs, ret_typ, _) ->
-     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
-  | Typ_bidir (typ1, typ2) ->
-     typ_nexps typ1 @ typ_nexps typ2
-and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
-  match typ_arg_aux with
-  | A_nexp n -> [n]
-  | A_typ typ -> typ_nexps typ
-  | A_bool nc -> constraint_nexps nc
-  | A_order ord -> []
-and constraint_nexps (NC_aux (nc_aux, l)) =
-  match nc_aux with
-  | NC_equal (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_le (n1, n2) | NC_not_equal (n1, n2) ->
-     [n1; n2]
-  | NC_set _ | NC_true | NC_false | NC_var _ -> []
-  | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2
-  | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args)
-
 (* Here's how the constraint generation works for subtyping
 
 X(b,c...) --> {a. Y(a,b,c...)} \subseteq {a. Z(a,b,c...)}
@@ -1373,22 +1418,6 @@ this is equivalent to
 which is then a problem we can feed to the constraint solver expecting unsat.
  *)
 
-let rec nexp_variable_power (Nexp_aux (aux, _)) =
-  match aux with
-  | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) ->
-     nexp_variable_power n1 || nexp_variable_power n2
-  | Nexp_neg n ->
-     nexp_variable_power n
-  | Nexp_id _ | Nexp_var _ | Nexp_constant _ ->
-     false
-  | Nexp_app (_, ns) ->
-     List.exists nexp_variable_power ns
-  | Nexp_exp n ->
-     not (KidSet.is_empty (tyvars_of_nexp n))
-
-let constraint_variable_power nc =
-  List.exists nexp_variable_power (constraint_nexps nc)
-
 let prove_smt env (NC_aux (_, l) as nc) =
   let vars = Env.get_typ_vars env in
   let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) vars in
@@ -1400,7 +1429,7 @@ let prove_smt env (NC_aux (_, l) as nc) =
      (* Work around versions of z3 that are confused by 2^n in
         constraints, even when such constraints are irrelevant *)
      let ncs' = List.concat (List.map constraint_conj ncs) in
-     let ncs' = List.filter (fun nc -> not (constraint_variable_power nc)) ncs' in
+     let ncs' = List.filter (fun nc -> KidSet.is_empty (constraint_power_variables nc)) ncs' in
      match Constraint.call_smt l vars (List.fold_left nc_and (nc_not nc) ncs') with
      | Constraint.Unsat -> typ_debug (lazy "unsat"); true
      | Constraint.Sat | Constraint.Unknown -> typ_debug (lazy "sat/unknown"); false
diff --git a/src/type_check.mli b/src/type_check.mli
index 00439412..cfdfa2c6 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -71,6 +71,10 @@ val opt_no_lexp_bounds_check : bool ref
    We prefer not to do it for latex output but it is otherwise a good idea. *)
 val opt_expand_valspec : bool ref
 
+(** Linearize cases involving power where we would otherwise require
+   the SMT solver to use non-linear arithmetic. *)
+val opt_smt_linearize : bool ref
+
 (** {2 Type errors} *)
 
 type type_error =
@@ -316,6 +320,7 @@ val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t
    untrustworthy. *)
 val prove : (string * int * int * int) -> Env.t -> n_constraint -> bool
 
+(** Returns Some c if there is a unique c such that nexp = c *)
 val solve_unique : Env.t -> nexp -> Big_int.num option
 
 val canonicalize : Env.t -> typ -> typ
-- 
cgit v1.2.3


From fc7d360e9442ab2e945e0d2da97faaf0eefec66f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 19 Feb 2019 17:02:19 +0000
Subject: Refactor specialization

specialize functions now take a 'specialization' parameter that
specifies how they will specialize the AST. typ_ord_specialization
gives the previous behaviour, whereas int_specialization allows
specializing on Int-kinded arguments. Note that this can loop forever
unless the appropriate case splits are inserted beforehand, presumably
by monomorphisation.

rename is_nat_kopt -> is_int_kopt for consistency
---
 src/ast_util.ml          |   2 +-
 src/ast_util.mli         |   2 +-
 src/initial_check.ml     |   6 +--
 src/isail.ml             |   6 +--
 src/monomorphise.ml      |   2 +-
 src/ocaml_backend.ml     |   4 +-
 src/pretty_print_coq.ml  |   2 +-
 src/pretty_print_lem.ml  |   2 +-
 src/pretty_print_sail.ml |   6 +--
 src/sail.ml              |   2 +-
 src/specialize.ml        | 101 +++++++++++++++++++++++++++++++----------------
 src/specialize.mli       |  18 +++++++--
 src/type_check.ml        |   6 +--
 13 files changed, 101 insertions(+), 58 deletions(-)

(limited to 'src')

diff --git a/src/ast_util.ml b/src/ast_util.ml
index e4287249..8942b3b1 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -129,7 +129,7 @@ let mk_val_spec vs_aux =
 let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid
 let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k
 
-let is_nat_kopt = function
+let is_int_kopt = function
   | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true
   | _ -> false
 
diff --git a/src/ast_util.mli b/src/ast_util.mli
index fe722f5e..823fcebb 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -109,7 +109,7 @@ val dec_ord : order
 (* Utilites for working with kinded_ids *)
 val kopt_kid : kinded_id -> kid
 val kopt_kind : kinded_id -> kind
-val is_nat_kopt : kinded_id -> bool
+val is_int_kopt : kinded_id -> bool
 val is_order_kopt : kinded_id -> bool
 val is_typ_kopt : kinded_id -> bool
 val is_bool_kopt : kinded_id -> bool
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 07316c6d..003da64e 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -824,15 +824,15 @@ let val_spec_ids (Defs defs) =
   IdSet.of_list (vs_ids defs)
 
 let quant_item_param = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))]
   | _ -> []
 let quant_item_typ = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))]
   | _ -> []
 let quant_item_arg = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))]
   | _ -> []
 let undefined_typschm id typq =
diff --git a/src/isail.ml b/src/isail.ml
index 4cfb2c6f..252b21b8 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -358,7 +358,7 @@ let handle_input' input =
         List.iter print_endline commands
      | ":poly" ->
         let is_kopt = match arg with
-          | "Int" -> is_nat_kopt
+          | "Int" -> is_int_kopt
           | "Type" -> is_typ_kopt
           | "Order" -> is_order_kopt
           | _ -> failwith "Invalid kind"
@@ -374,7 +374,7 @@ let handle_input' input =
           | Arg.Bad message | Arg.Help message -> print_endline message
         end;
      | ":spec" ->
-        let ast, env = Specialize.specialize !Interactive.ast !Interactive.env in
+        let ast, env = Specialize.(specialize int_specialization !Interactive.ast !Interactive.env) in
         Interactive.ast := ast;
         Interactive.env := env;
         interactive_state := initial_state !Interactive.ast Value.primops
@@ -384,7 +384,7 @@ let handle_input' input =
         let open PPrint in
         let open C_backend in
         let ast = Process_file.rewrite_ast_c !Interactive.env !Interactive.ast in
-        let ast, env = Specialize.specialize ast !Interactive.env in
+        let ast, env = Specialize.(specialize typ_ord_specialization ast !Interactive.env) in
         let ctx = initial_ctx env in
         interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast
      | ":ir" ->
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index acc31456..856e36d5 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -4300,7 +4300,7 @@ let add_bitvector_casts (Defs defs) =
   let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann)) =
     let fcl_env = env_of_annot fcl_ann in
     let (tq,typ) = Env.get_val_spec_orig id fcl_env in
-    let quant_kids = List.map kopt_kid (List.filter is_nat_kopt (quant_kopts tq)) in
+    let quant_kids = List.map kopt_kid (List.filter is_int_kopt (quant_kopts tq)) in
     let ret_typ =
       match typ with
       | Typ_aux (Typ_fn (_,ret,_),_) -> ret
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 05406413..894d028f 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -744,13 +744,13 @@ let ocaml_pp_generators ctx defs orig_types required =
     let gen_tyvars = List.map (fun k -> kopt_kid k |> zencode_kid)
                        (List.filter is_typ_kopt tquants) in
     let print_quant kindedid =
-      if is_nat_kopt kindedid then string "int" else
+      if is_int_kopt kindedid then string "int" else
       if is_order_kopt kindedid then string "bool" else
       parens (separate space [string "generators"; string "->"; zencode_kid (kopt_kid kindedid)])
     in
     let name = "gen_" ^ type_name id in
     let make_tyarg kindedid =
-      if is_nat_kopt kindedid
+      if is_int_kopt kindedid
       then mk_typ_arg (A_nexp (nvar (kopt_kid kindedid)))
       else if is_order_kopt kindedid
       then mk_typ_arg (A_order (mk_ord (Ord_var (kopt_kid kindedid))))
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index c321cb26..430eb40d 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2512,7 +2512,7 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
      let used = if is_number ret_ty then used else KidSet.union used (tyvars_of_typ ret_ty) in
      let tqs = match tqs with
        | TypQ_aux (TypQ_tq qs,l) -> TypQ_aux (TypQ_tq (List.filter (function
-         | QI_aux (QI_id kopt,_) when is_nat_kopt kopt ->
+         | QI_aux (QI_id kopt,_) when is_int_kopt kopt ->
             let kid = kopt_kid kopt in
             KidSet.mem kid used && not (KidSet.mem kid args)
          | _ -> true) qs),l)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 9d472e15..1c30e06e 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -316,7 +316,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
           * if we add a new Typ constructor *)
          let tpp = typ ty in
          if atyp_needed then parens tpp else tpp
-      | Typ_exist (kopts,_,ty) when List.for_all is_nat_kopt kopts -> begin
+      | Typ_exist (kopts,_,ty) when List.for_all is_int_kopt kopts -> begin
          let kids = List.map kopt_kid kopts in
          let tpp = typ ty in
          let visible_vars = lem_tyvars_of_typ ty in
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 9a374275..27f626ea 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -66,7 +66,7 @@ let doc_id (Id_aux (id_aux, _)) =
 let doc_kid kid = string (Ast_util.string_of_kid kid)
 
 let doc_kopt = function
-  | kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt)
+  | kopt when is_int_kopt kopt -> doc_kid (kopt_kid kopt)
   | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
   | kopt when is_order_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
   | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])
@@ -213,7 +213,7 @@ and doc_arg_typs = function
 let doc_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
+    | QI_id kopt when is_int_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
     | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
     | QI_id kopt when is_bool_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])]
     | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
@@ -234,7 +234,7 @@ let doc_quants quants =
 let doc_param_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
+    | QI_id kopt when is_int_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
     | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
     | QI_id kopt when is_bool_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"]
     | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
diff --git a/src/sail.ml b/src/sail.ml
index 64ccd341..eaf96eb4 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -406,7 +406,7 @@ let main() =
       (if !(opt_print_c)
        then
          let ast_c = rewrite_ast_c type_envs ast in
-         let ast_c, type_envs = Specialize.specialize ast_c type_envs in
+         let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
          (* let ast_c = Spec_analysis.top_sort_defs ast_c in *)
          Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
diff --git a/src/specialize.ml b/src/specialize.ml
index 9f6af6d6..eaef1231 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -52,11 +52,26 @@ open Ast
 open Ast_util
 open Rewriter
 
-let is_typ_ord_uvar = function
+let is_typ_ord_arg = function
   | A_aux (A_typ _, _) -> true
   | A_aux (A_order _, _) -> true
   | _ -> false
 
+type specialization = {
+    is_polymorphic : kinded_id -> bool;
+    instantiation_filter : kid -> typ_arg -> bool
+  }
+
+let typ_ord_specialization = {
+    is_polymorphic = (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt);
+    instantiation_filter = (fun _ -> is_typ_ord_arg)
+  }
+
+let int_specialization = {
+    is_polymorphic = is_int_kopt;
+    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false)
+  }
+
 let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
   let typ_aux = match typ_aux with
     | Typ_id v -> Typ_id v
@@ -81,34 +96,43 @@ and nexp_simp_typ_arg (A_aux (typ_arg_aux, l)) =
 
 (* We have to be careful about whether the typechecker has renamed anything returned by instantiation_of.
    This part of the typechecker API is a bit ugly. *)
-let fix_instantiation instantiation =
-  let instantiation = KBindings.bindings (KBindings.filter (fun _ arg -> is_typ_ord_uvar arg) instantiation) in
+let fix_instantiation spec instantiation =
+  let instantiation = KBindings.bindings (KBindings.filter spec.instantiation_filter instantiation) in
   let instantiation = List.map (fun (kid, arg) -> Type_check.orig_kid kid, nexp_simp_typ_arg arg) instantiation in
   List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty instantiation
 
+(* polymorphic_functions returns all functions that are polymorphic
+   for some set of kinded-identifiers, specified by the is_kopt
+   predicate. For example, polymorphic_functions is_int_kopt will
+   return all Int-polymorphic functions. *)
 let rec polymorphic_functions is_kopt (Defs defs) =
   match defs with
   | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ) , _), id, _, externs), _)) :: defs ->
-     let is_type_polymorphic = List.exists is_kopt (quant_kopts typq) in
-     if is_type_polymorphic then
+     let is_polymorphic = List.exists is_kopt (quant_kopts typq) in
+     if is_polymorphic then
        IdSet.add id (polymorphic_functions is_kopt (Defs defs))
      else
        polymorphic_functions is_kopt (Defs defs)
   | _ :: defs -> polymorphic_functions is_kopt (Defs defs)
   | [] -> IdSet.empty
 
+(* When we specialize a function, we need to generate new name. To do
+   this we take the instantiation that the new function is specialized
+   for and turn that into a string in such a way that alpha-equivalent
+   instantiations always get the same name. We then zencode that
+   string so it is a valid identifier name, and prepend it to the
+   previous function name. *)
 let string_of_instantiation instantiation =
   let open Type_check in
   let kid_names = ref KOptMap.empty in
   let kid_counter = ref 0 in
   let kid_name kid =
     try KOptMap.find kid !kid_names with
-    | Not_found -> begin
-        let n = string_of_int !kid_counter in
-        kid_names := KOptMap.add kid n !kid_names;
-        incr kid_counter;
-        n
-      end
+    | Not_found ->
+       let n = string_of_int !kid_counter in
+       kid_names := KOptMap.add kid n !kid_names;
+       incr kid_counter;
+       n
   in
 
   (* We need custom string_of functions to ensure that alpha-equivalent definitions get the same name *)
@@ -121,7 +145,7 @@ let string_of_instantiation instantiation =
     | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")"
     | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")"
     | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")"
-    | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")"
+    | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_nexp nexps ^ ")"
     | Nexp_exp n -> "2 ^ " ^ string_of_nexp n
     | Nexp_neg n -> "- " ^ string_of_nexp n
   in
@@ -132,7 +156,7 @@ let string_of_instantiation instantiation =
     | Typ_id id -> string_of_id id
     | Typ_var kid -> kid_name (mk_kopt K_type kid)
     | Typ_tup typs -> "(" ^ Util.string_of_list ", " string_of_typ typs ^ ")"
-    | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
+    | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_typ_arg args ^ ")"
     | Typ_fn (arg_typs, ret_typ, eff) ->
        "(" ^ Util.string_of_list ", " string_of_typ arg_typs ^ ") -> " ^ string_of_typ ret_typ ^ " effect " ^ string_of_effect eff
     | Typ_bidir (t1, t2) ->
@@ -161,10 +185,10 @@ let string_of_instantiation instantiation =
     | NC_aux (NC_true, _) -> "true"
     | NC_aux (NC_false, _) -> "false"
     | NC_aux (NC_var kid, _) -> kid_name (mk_kopt K_bool kid)
-    | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
+    | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_typ_arg args ^ ")"
   in
 
-  let string_of_binding (kid, arg) = string_of_kid kid ^ " => " ^ string_of_typ_arg arg in
+  let string_of_binding (kid, arg) = string_of_kid kid ^ "=>" ^ string_of_typ_arg arg in
   Util.zencode_string (Util.string_of_list ", " string_of_binding (KBindings.bindings instantiation))
 
 let id_of_instantiation id instantiation =
@@ -181,12 +205,12 @@ let rec variant_generic_typ id (Defs defs) =
 (* Returns a list of all the instantiations of a function id in an
    ast. Also works with union constructors, and searches for them in
    patterns. *)
-let rec instantiations_of id ast =
+let rec instantiations_of spec id ast =
   let instantiations = ref [] in
 
   let inspect_exp = function
     | E_aux (E_app (id', _), _) as exp when Id.compare id id' = 0 ->
-       let instantiation = fix_instantiation (Type_check.instantiation_of exp) in
+       let instantiation = fix_instantiation spec (Type_check.instantiation_of exp) in
        instantiations := instantiation :: !instantiations;
        exp
     | exp -> exp
@@ -204,7 +228,7 @@ let rec instantiations_of id ast =
                                 (variant_generic_typ variant_id ast)
                                 typ
           in
-          instantiations := fix_instantiation instantiation :: !instantiations;
+          instantiations := fix_instantiation spec instantiation :: !instantiations;
           pat
        | Typ_aux (Typ_id variant_id, _) -> pat
        | _ -> failwith ("Union constructor " ^ string_of_pat pat ^ " has non-union type")
@@ -220,12 +244,12 @@ let rec instantiations_of id ast =
 
   !instantiations
 
-let rec rewrite_polymorphic_calls id ast =
+let rec rewrite_polymorphic_calls spec id ast =
   let vs_ids = Initial_check.val_spec_ids ast in
 
   let rewrite_e_aux = function
     | E_aux (E_app (id', args), annot) as exp when Id.compare id id' = 0 ->
-       let instantiation = fix_instantiation (Type_check.instantiation_of exp) in
+       let instantiation = fix_instantiation spec (Type_check.instantiation_of exp) in
        let spec_id = id_of_instantiation id instantiation in
        (* Make sure we only generate specialized calls when we've
           specialized the valspec. The valspec may not be generated if
@@ -280,7 +304,7 @@ and typ_arg_int_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
   | A_order ord -> KidSet.empty
   | A_bool _ -> KidSet.empty
 
-let specialize_id_valspec instantiations id ast =
+let specialize_id_valspec spec instantiations id ast =
   match split_defs (is_valspec id) ast with
   | None -> failwith ("Valspec " ^ string_of_id id ^ " does not exist!")
   | Some (pre_ast, vs, post_ast) ->
@@ -304,7 +328,8 @@ let specialize_id_valspec instantiations id ast =
 
        (* Remove type variables from the type quantifier. *)
        let kopts, constraints = quant_split typq in
-       let kopts = List.filter (fun kopt -> not (is_typ_kopt kopt || is_order_kopt kopt)) kopts in
+       let constraints = List.map (fun c -> List.fold_left (fun c (v, a) -> constraint_subst v a c) c (KBindings.bindings instantiation)) constraints in
+       let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in
        let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees
                                @ List.map (mk_qi_id K_int) int_frees
                                @ List.map mk_qi_kopt kopts
@@ -344,7 +369,7 @@ let specialize_annotations instantiation =
       rewrite_exp = (fun _ -> fold_exp rw_exp);
       rewrite_pat = (fun _ -> fold_pat rw_pat)
     }
-     
+
 let specialize_id_fundef instantiations id ast =
   match split_defs (is_fundef id) ast with
   | None -> ast
@@ -382,7 +407,15 @@ let specialize_id_overloads instantiations id (Defs defs) =
    valspecs are then re-specialized. This process is iterated until
    the whole spec is specialized. *)
 
-let initial_calls = (IdSet.of_list [mk_id "main"; mk_id "__SetConfig"; mk_id "__ListConfig"; mk_id "execute"; mk_id "decode"; mk_id "initialize_registers"; mk_id "append_64"])
+let initial_calls = IdSet.of_list
+  [ mk_id "main";
+    mk_id "__SetConfig";
+    mk_id "__ListConfig";
+    mk_id "execute";
+    mk_id "decode";
+    mk_id "initialize_registers";
+    mk_id "append_64" (* used to construct bitvector literals in C backend *)
+  ]
 
 let remove_unused_valspecs ?(initial_calls=initial_calls) env ast =
   let calls = ref initial_calls in
@@ -426,9 +459,9 @@ let slice_defs env (Defs defs) keep_ids =
   let defs = List.filter keep defs in
   remove_unused_valspecs env (Defs defs) ~initial_calls:keep_ids
 
-let specialize_id id ast =
-  let instantiations = instantiations_of id ast in
-  let ast = specialize_id_valspec instantiations id ast in
+let specialize_id spec id ast =
+  let instantiations = instantiations_of spec id ast in
+  let ast = specialize_id_valspec spec instantiations id ast in
   let ast = specialize_id_fundef instantiations id ast in
   specialize_id_overloads instantiations id ast
 
@@ -450,21 +483,21 @@ let reorder_typedefs (Defs defs) =
   let others = filter_typedefs defs in
   Defs (List.rev !tdefs @ others)
 
-let specialize_ids ids ast =
-  let ast = List.fold_left (fun ast id -> specialize_id id ast) ast (IdSet.elements ids) in
+let specialize_ids spec ids ast =
+  let ast = List.fold_left (fun ast id -> specialize_id spec id ast) ast (IdSet.elements ids) in
   let ast = reorder_typedefs ast in
   let ast, _ = Type_error.check Type_check.initial_env ast in
   let ast =
-    List.fold_left (fun ast id -> rewrite_polymorphic_calls id ast) ast (IdSet.elements ids)
+    List.fold_left (fun ast id -> rewrite_polymorphic_calls spec id ast) ast (IdSet.elements ids)
   in
   let ast, env = Type_error.check Type_check.initial_env ast in
   let ast = remove_unused_valspecs env ast in
   ast, env
 
-let rec specialize ast env =
-  let ids = polymorphic_functions (fun kopt -> is_typ_kopt kopt || is_order_kopt kopt) ast in
+let rec specialize spec ast env =
+  let ids = polymorphic_functions spec.is_polymorphic ast in
   if IdSet.is_empty ids then
     ast, env
   else
-    let ast, env = specialize_ids ids ast in
-    specialize ast env
+    let ast, env = specialize_ids spec ids ast in
+    specialize spec ast env
diff --git a/src/specialize.mli b/src/specialize.mli
index 28029747..269f2340 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -54,10 +54,18 @@ open Ast
 open Ast_util
 open Type_check
 
+type specialization
+
+(** Only specialize Type- and Ord- kinded polymorphism. *)
+val typ_ord_specialization : specialization
+
+(** (experimental) specialise Int-kinded definitions *)
+val int_specialization : specialization
+
 (** Returns an IdSet with the function ids that have X-kinded
    parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first
    argument specifies what X should be - it should be one of:
-   [is_nat_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
+   [is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
    or some combination of those. *)
 val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
 
@@ -66,11 +74,13 @@ val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
    AST with [Type_check.initial_env]. The env parameter is the
    environment to return if there is no polymorphism to remove, in
    which case specialize returns the AST unmodified. *)
-val specialize : tannot defs -> Env.t -> tannot defs * Env.t
+val specialize : specialization -> tannot defs -> Env.t -> tannot defs * Env.t
 
-val instantiations_of : id -> tannot defs -> typ_arg KBindings.t list
+(** return all instantiations of a function id, with the
+   instantiations filtered according to the specialization. *)
+val instantiations_of : specialization -> id -> tannot defs -> typ_arg KBindings.t list
 
 val string_of_instantiation : typ_arg KBindings.t -> string
 
-(* Remove all function definitions except for the given set *)
+(** Remove all function definitions except for the given set *)
 val slice_defs : Env.t -> tannot defs -> IdSet.t -> tannot defs
diff --git a/src/type_check.ml b/src/type_check.ml
index 0da7f753..3d0f38a6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -574,7 +574,7 @@ end = struct
     let kopts, ncs = quant_split typq in
     let rec subst_args kopts args =
       match kopts, args with
-      | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_nat_kopt kopt ->
+      | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt ->
          List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args)
       | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
          subst_args kopts args
@@ -992,7 +992,7 @@ end = struct
         typ_print (lazy (adding ^ "record " ^ string_of_id id));
         let rec record_typ_args = function
           | [] -> []
-          | ((QI_aux (QI_id kopt, _)) :: qis) when is_nat_kopt kopt ->
+          | ((QI_aux (QI_id kopt, _)) :: qis) when is_int_kopt kopt ->
              mk_typ_arg (A_nexp (nvar (kopt_kid kopt))) :: record_typ_args qis
           | ((QI_aux (QI_id kopt, _)) :: qis) when is_typ_kopt kopt ->
              mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt)))) :: record_typ_args qis
@@ -4817,7 +4817,7 @@ let mk_synonym typq typ_arg =
   let kopts = List.map snd kopts in
   let rec subst_args env l kopts args =
     match kopts, args with
-    | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_nat_kopt kopt ->
+    | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt ->
        let typ_arg, ncs = subst_args env l kopts args in
        typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
        List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
-- 
cgit v1.2.3


From a45ce2aecdd27de565dd32d42c8c79d10e2edd0a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 20 Feb 2019 14:18:49 +0000
Subject: Remove dead branches when compiling to C

Specifically remove branches where flow-typing implies false, as this
allows the optimizer to prove anything, which can result in nonsense
code. This does incur something of a performance hit.
---
 src/anf.ml       |  2 ++
 src/anf.mli      |  2 ++
 src/c_backend.ml | 36 ++++++++++++++++++++++--------------
 3 files changed, 26 insertions(+), 14 deletions(-)

(limited to 'src')

diff --git a/src/anf.ml b/src/anf.ml
index 38c77e0b..5db836e9 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -436,6 +436,8 @@ and pp_aval = function
 
 let ae_lit lit typ = AE_val (AV_lit (lit, typ))
 
+let is_dead_aexp (AE_aux (_, env, _)) = prove __POS__ env nc_false
+
 (** GLOBAL: gensym_counter is used to generate fresh identifiers where
    needed. It should be safe to reset between top level
    definitions. **)
diff --git a/src/anf.mli b/src/anf.mli
index 5e162b7c..6b9c9b51 100644
--- a/src/anf.mli
+++ b/src/anf.mli
@@ -112,6 +112,8 @@ val apat_globals : 'a apat -> (id * 'a) list
 
 val apat_types : 'a apat -> 'a Bindings.t
 
+val is_dead_aexp : 'a aexp -> bool
+
 (* Compiling to ANF expressions *)
 
 val anf_pat : ?global:bool -> tannot pat -> typ apat
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 2981660e..fd728111 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1083,7 +1083,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
          | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _)
-         | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
+           | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true
          | _ -> false
        in
        let case_label = label "case_" in
@@ -1103,7 +1103,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
          @ [igoto finish_match_label]
        in
-       [iblock case_instrs; ilabel case_label]
+       if is_dead_aexp body then
+         [ilabel case_label]
+       else
+         [iblock case_instrs; ilabel case_label]
      in
      [icomment "begin match"]
      @ aval_setup @ [idecl ctyp case_return_id]
@@ -1159,18 +1162,23 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      []
 
   | AE_if (aval, then_aexp, else_aexp, if_typ) ->
-     let if_ctyp = ctyp_of_typ ctx if_typ in
-     let compile_branch aexp =
-       let setup, call, cleanup = compile_aexp ctx aexp in
-       fun clexp -> setup @ [call clexp] @ cleanup
-     in
-     let setup, cval, cleanup = compile_aval l ctx aval in
-     setup,
-     (fun clexp -> iif cval
-                       (compile_branch then_aexp clexp)
-                       (compile_branch else_aexp clexp)
-                       if_ctyp),
-     cleanup
+     if is_dead_aexp then_aexp then
+       compile_aexp ctx else_aexp
+     else if is_dead_aexp else_aexp then
+       compile_aexp ctx then_aexp
+     else
+       let if_ctyp = ctyp_of_typ ctx if_typ in
+       let compile_branch aexp =
+         let setup, call, cleanup = compile_aexp ctx aexp in
+         fun clexp -> setup @ [call clexp] @ cleanup
+       in
+       let setup, cval, cleanup = compile_aval l ctx aval in
+       setup,
+       (fun clexp -> iif cval
+                         (compile_branch then_aexp clexp)
+                         (compile_branch else_aexp clexp)
+                         if_ctyp),
+       cleanup
 
   (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *)
   | AE_record_update (aval, fields, typ) ->
-- 
cgit v1.2.3


From cf01543fa352d136f56e4acd94c448bc48217572 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Wed, 20 Feb 2019 10:05:28 -0800
Subject: Support 32-bit ELF in OCaml loader.

---
 src/elf_loader.ml | 71 +++++++++++++++++++++++++++++++++++--------------------
 1 file changed, 45 insertions(+), 26 deletions(-)

(limited to 'src')

diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index 88fcfddb..23d19f22 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -66,14 +66,16 @@ let break n xs =
     | (_ :: _ as xs) -> helper ([Lem_list.take n xs] @ acc) (Lem_list.drop n xs)
   in helper [] xs
 
-let print_segment seg =
-  let bs = seg.Elf_interpreted_segment.elf64_segment_body in
+let print_segment bs =
   prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";
   List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs))
 
+type elf_segs =
+  | ELF64 of Elf_interpreted_segment.elf64_interpreted_segment list
+  | ELF32 of Elf_interpreted_segment.elf32_interpreted_segment list
+
 let read name =
   let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in
-
   prerr_endline "Elf read:";
   let (elf_file, elf_epi, symbol_map) =
     begin match info with
@@ -87,20 +89,18 @@ let read name =
        (elf_file, elf_epi, symbol_map)
     end
   in
-
   prerr_endline "\nElf segments:";
+
+  (* remove all the auto generated segments (they contain only 0s) *)
+  let prune_segments segs =
+    Lem_list.mapMaybe (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None) segs in
   let (segments, e_entry, e_machine) =
     begin match elf_epi, elf_file with
-    | (Sail_interface.ELF_Class_32 _, _) -> failwith "cannot handle ELF_Class_32"
-    | (_, Elf_file.ELF_File_32 _)  -> failwith "cannot handle ELF_File_32"
-    | (Sail_interface.ELF_Class_64 (segments, e_entry, e_machine), Elf_file.ELF_File_64 f1) ->
-       (* remove all the auto generated segments (they contain only 0s) *)
-       let segments =
-         Lem_list.mapMaybe
-           (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None)
-           segments
-       in
-       (segments, e_entry, e_machine)
+    | (Sail_interface.ELF_Class_32 (segments, e_entry, e_machine), Elf_file.ELF_File_32 _) ->
+          (ELF32 (prune_segments segments), e_entry, e_machine)
+    | (Sail_interface.ELF_Class_64 (segments, e_entry, e_machine), Elf_file.ELF_File_64 _) ->
+          (ELF64 (prune_segments segments), e_entry, e_machine)
+    | (_, _) -> failwith "cannot handle ELF file"
     end
   in
   (segments, e_entry, symbol_map)
@@ -120,24 +120,20 @@ let write_file chan paddr i byte =
   output_string chan (Big_int.to_string (Big_int.add paddr (Big_int.of_int i)) ^ "\n");
   output_string chan (string_of_int byte ^ "\n")
 
-let load_segment ?writer:(writer=write_sail_lib) seg =
-  let open Elf_interpreted_segment in
-  let bs = seg.elf64_segment_body in
-  let paddr = seg.elf64_segment_paddr in
-  let base = seg.elf64_segment_base in
-  let offset = seg.elf64_segment_offset in
-  let size = seg.elf64_segment_size in
-  let memsz = seg.elf64_segment_memsz in
+let print_seg_info offset base paddr size memsz =
   prerr_endline "\nLoading Segment";
   prerr_endline ("Segment offset: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 offset)));
   prerr_endline ("Segment base address: " ^ (Big_int.to_string base));
   (* NB don't attempt to convert paddr to int64 because on MIPS it is quite likely to exceed signed
-     64-bit range e.g. addresses beginning 0x9.... Really need to_uint64 or to_string_hex but lem 
+     64-bit range e.g. addresses beginning 0x9.... Really need to_uint64 or to_string_hex but lem
      doesn't have them. *)
   prerr_endline ("Segment physical address: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 paddr)));
   prerr_endline ("Segment size: " ^  (Printf.sprintf "0x%Lx" (Big_int.to_int64 size)));
-  prerr_endline ("Segment memsz: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 memsz)));
-  print_segment seg;
+  prerr_endline ("Segment memsz: " ^ (Printf.sprintf "0x%Lx" (Big_int.to_int64 memsz)))
+
+let load_segment ?writer:(writer=write_sail_lib) bs paddr base offset size memsz =
+  print_seg_info offset base paddr size memsz;
+  print_segment bs;
   List.iteri (writer paddr) (List.rev_map int_of_char (List.rev (Byte_sequence.char_list_of_byte_sequence bs)));
   write_mem_zeros (Big_int.add paddr size) (Big_int.sub memsz size)
 
@@ -147,7 +143,30 @@ let load_elf ?writer:(writer=write_sail_lib) name =
   (if List.mem_assoc "tohost" symbol_map then
      let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
      opt_elf_tohost := tohost_addr);
-  List.iter (load_segment ~writer:writer) segments
+  (match segments with
+     | ELF64 segs ->
+           List.iter (fun seg ->
+                      let open Elf_interpreted_segment in
+                      let bs = seg.elf64_segment_body in
+                      let paddr = seg.elf64_segment_paddr in
+                      let base = seg.elf64_segment_base in
+                      let offset = seg.elf64_segment_offset in
+                      let size = seg.elf64_segment_size in
+                      let memsz = seg.elf64_segment_memsz in
+                      load_segment ~writer:writer bs paddr base offset size memsz)
+                     segs
+     | ELF32 segs ->
+           List.iter (fun seg ->
+                      let open Elf_interpreted_segment in
+                      let bs = seg.elf32_segment_body in
+                      let paddr = seg.elf32_segment_paddr in
+                      let base = seg.elf32_segment_base in
+                      let offset = seg.elf32_segment_offset in
+                      let size = seg.elf32_segment_size in
+                      let memsz = seg.elf32_segment_memsz in
+                      load_segment ~writer:writer bs paddr base offset size memsz)
+                     segs
+  )
 
 (* The sail model can access this by externing a unit -> int function
    as Elf_loader.elf_entry. *)
-- 
cgit v1.2.3


From 09c8c3e212e5959461312d28240f2ae843a19e81 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Wed, 20 Feb 2019 13:34:29 -0800
Subject: Record the type of loaded ELF for sanity checks.

---
 src/elf_loader.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index 23d19f22..2f63087f 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -47,6 +47,10 @@ let opt_elf_threads = ref 1
 let opt_elf_entry = ref Big_int.zero
 let opt_elf_tohost = ref Big_int.zero
 
+(* the type of elf last loaded *)
+type elf_class = ELF_Class_64 | ELF_Class_32
+let opt_elf_class = ref ELF_Class_64 (* default *)
+
 type word8 = int
 
 let escape_char c =
@@ -154,7 +158,8 @@ let load_elf ?writer:(writer=write_sail_lib) name =
                       let size = seg.elf64_segment_size in
                       let memsz = seg.elf64_segment_memsz in
                       load_segment ~writer:writer bs paddr base offset size memsz)
-                     segs
+                     segs;
+           opt_elf_class := ELF_Class_64
      | ELF32 segs ->
            List.iter (fun seg ->
                       let open Elf_interpreted_segment in
@@ -165,7 +170,8 @@ let load_elf ?writer:(writer=write_sail_lib) name =
                       let size = seg.elf32_segment_size in
                       let memsz = seg.elf32_segment_memsz in
                       load_segment ~writer:writer bs paddr base offset size memsz)
-                     segs
+                     segs;
+           opt_elf_class := ELF_Class_32
   )
 
 (* The sail model can access this by externing a unit -> int function
@@ -173,3 +179,5 @@ let load_elf ?writer:(writer=write_sail_lib) name =
 let elf_entry () = !opt_elf_entry
 (* Used by RISCV sail model test harness for exiting test *)
 let elf_tohost () = !opt_elf_tohost
+(* Used to check last loaded elf class. *)
+let elf_class () = !opt_elf_class
-- 
cgit v1.2.3


From 7253269fb62712e7e8fd94d5d0264d5bed9e8406 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Wed, 20 Feb 2019 22:31:51 +0000
Subject: Fix bug with missing satisfiablity check in subtyping

Thanks to Mark for finding this bug. Regression test is
complex_exist_sat in test/typecheck/pass/
---
 src/type_check.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index 3d0f38a6..8de4a904 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1976,9 +1976,17 @@ let rec subtyp l env typ1 typ2 =
      let env = add_typ_vars l (List.map (mk_kopt K_int) (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2)))) env in
      let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in
      if not (kids2 = []) then typ_error env l ("Universally quantified constraint generated: " ^ Util.string_of_list ", " string_of_kid kids2) else ();
-     let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
-     if prove __POS__ env nc2 then ()
-     else typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+     let vars = KBindings.filter (fun _ k -> match k with K_int | K_bool -> true | _ -> false) (Env.get_typ_vars env) in
+     begin match Constraint.call_smt l vars (nc_eq nexp1 nexp2) with
+     | Constraint.Sat ->
+        let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
+        if prove __POS__ env nc2 then
+          ()
+        else
+          typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+     | _ ->
+        typ_error env l ("Constraint " ^ string_of_n_constraint (nc_eq nexp1 nexp2) ^ " is not satisfiable")
+     end
   | _, _ ->
   match typ_aux1, typ_aux2 with
   | _, Typ_internal_unknown when Env.allow_unknowns env -> ()
-- 
cgit v1.2.3


From c0de36691f70867bbe1f9cd01f0ee4340b7fb2d5 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 21 Feb 2019 00:51:12 +0000
Subject: Fix specialization bug involving function annotations not matching
 valspecs

Perhaps suprisingly to some, this did not mean that Sail was
unable to typecheck the identify function.

While doing this rename Effect_opt_pure to Effect_opt_none - as
Effect_opt_pure was the effect equivalent of Typ_annot_opt_none,
and actually means that the function definition lacks an effect
annnotation, not that the function is actually pure, so this was
*extremely* misleading. The effect_opt that actually indicated a
function is pure was (and still is) the succinct:

Effect_opt_aux (Effect_opt_effect (Effect_aux (Effect_set [], _)), _)

In fact because in the grammar we only specify effects on
valspecs (they can always be inferred for fundefs in the absence
of a valspec) effect_opts are basically vestigial and are always
Effect_opt_none.

What might actually be super nice would be to remove rec_opt,
effect_opt and typ_annot_opt from fundefs in ast.ml altogether
and if we want them in the syntax just have them in parse_ast.ml
and pull them into a valspec during the initial check.
---
 src/ast_util.ml      |  2 +-
 src/initial_check.ml |  2 +-
 src/monomorphise.ml  |  2 +-
 src/parse_ast.ml     |  2 +-
 src/parser.mly       |  2 +-
 src/rewrites.ml      | 20 ++++++++++----------
 src/scattered.ml     |  6 +++---
 src/specialize.ml    | 24 +++++++++++++++++-------
 8 files changed, 35 insertions(+), 25 deletions(-)

(limited to 'src')

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 8942b3b1..158b40a8 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -116,7 +116,7 @@ let mk_qi_kopt kopt = QI_aux (QI_id kopt, Parse_ast.Unknown)
 
 let mk_fundef funcls =
   let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
-  let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in
+  let effect_opt = Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown) in
   let rec_opt = Rec_aux (Rec_nonrec, Parse_ast.Unknown) in
   DEF_fundef
    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 003da64e..5893563b 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -595,7 +595,7 @@ let to_ast_typschm_opt ctx (P.TypSchm_opt_aux(aux,l)) : tannot_opt ctx_out =
 
 let to_ast_effects_opt (P.Effect_opt_aux(e,l)) : effect_opt =
   match e with
-  | P.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l)
+  | P.Effect_opt_none -> Effect_opt_aux(Effect_opt_none,l)
   | P.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects typ),l)
 
 let to_ast_funcl ctx (P.FCL_aux(fcl,l) : P.funcl) : (unit funcl) =
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 856e36d5..92a0ae01 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -201,7 +201,7 @@ let rec is_value (E_aux (e,(l,annot))) =
 
 let is_pure (Effect_opt_aux (e,_)) =
   match e with
-  | Effect_opt_pure -> true
+  | Effect_opt_none -> true
   | Effect_opt_effect (Effect_aux (Effect_set [],_)) -> true
   | _ -> false
 
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index eb5c3dc6..2ff7b5e2 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -324,7 +324,7 @@ typschm_opt =
 
 type 
 effect_opt_aux =  (* Optional effect annotation for functions *)
-   Effect_opt_pure (* sugar for empty effect set *)
+   Effect_opt_none (* sugar for empty effect set *)
  | Effect_opt_effect of atyp
 
 
diff --git a/src/parser.mly b/src/parser.mly
index bd832d28..4004f53d 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -133,7 +133,7 @@ let mk_recn = (Rec_aux((Rec_nonrec), Unknown))
 let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
 let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m)
-let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
+let mk_eannotn = Effect_opt_aux(Effect_opt_none,Unknown)
 
 let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m)
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 3c000f17..c78c9aee 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3106,7 +3106,7 @@ let construct_toplevel_string_append_func env f_id pat =
   let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
   let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
   let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
-  let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+  let effect_none = (Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown)) in
   let s_id = fresh_stringappend_id () in
   let arg_pat = mk_pat (P_id s_id) in
   (* We can ignore guards here because we've already removed them *)
@@ -3211,7 +3211,7 @@ let construct_toplevel_string_append_func env f_id pat =
   in
   let wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit])))) in
   let new_match = mk_exp (E_case (mk_exp (E_id s_id), [strip_pexp new_pexp; wildcard])) in
-  let new_fun_def = FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl f_id arg_pat new_match]), (unk,())) in
+  let new_fun_def = FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl f_id arg_pat new_match]), (unk,())) in
   let new_fun_def, env = Type_check.check_fundef env new_fun_def in
   List.flatten [new_val_spec; new_fun_def]
 
@@ -4339,7 +4339,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
 
     let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
-    let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+    let effect_none = (Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown)) in
     (* We need to make sure we get the environment for the last mapping clause *)
     let env = match List.rev mapcls with
       | MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot
@@ -4373,10 +4373,10 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let forwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl true forwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
     let backwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl false backwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
 
-    let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
-    let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
-    let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in
-    let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in
+    let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
+    let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
+    let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in
+    let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in
 
     typ_debug (lazy (Printf.sprintf "forwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string)));
     typ_debug (lazy (Printf.sprintf "backwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string)));
@@ -4395,7 +4395,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
               let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
               let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
-              let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
+              let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
               typ_debug (lazy (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string)));
               let forwards_prefix_fun, _ = Type_check.check_fundef env forwards_prefix_fun in
               forwards_prefix_spec @ forwards_prefix_fun
@@ -4405,7 +4405,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
                 let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
                 let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
-                let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
+                let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
                 typ_debug (lazy (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string)));
                 let backwards_prefix_fun, _ = Type_check.check_fundef env backwards_prefix_fun in
                 backwards_prefix_spec @ backwards_prefix_fun
@@ -4937,7 +4937,7 @@ let rewrite_explicit_measure env (Defs defs) =
         match Bindings.find id measures with
         | (measure_pat, measure_exp) ->
            let e = match e with
-             | Effect_opt_aux (Effect_opt_pure, _) ->
+             | Effect_opt_aux (Effect_opt_none, _) ->
                 Effect_opt_aux (Effect_opt_effect (mk_effect [BE_escape]), loc)
              | Effect_opt_aux (Effect_opt_effect eff,_) ->
                 Effect_opt_aux (Effect_opt_effect (add_escape eff), loc)
diff --git a/src/scattered.ml b/src/scattered.ml
index de286e3f..92cb3561 100644
--- a/src/scattered.ml
+++ b/src/scattered.ml
@@ -66,8 +66,8 @@ let rec last_scattered_mapcl id = function
   | [] -> true
 
 (* Nothing cares about these and the AST should be changed *)
-let fake_effect_opt l = Effect_opt_aux (Effect_opt_pure, gen_loc l)
-let fake_rec_opt l = Rec_aux (Rec_rec, gen_loc l)
+let no_effect_opt l = Effect_opt_aux (Effect_opt_none, gen_loc l)
+let fake_rec_opt l = Rec_aux (Rec_nonrec, gen_loc l)
 
 let no_tannot_opt l = Typ_annot_opt_aux (Typ_annot_opt_none, gen_loc l)
 
@@ -95,7 +95,7 @@ let rec descatter' funcls mapcls = function
        | Some clauses -> List.rev (funcl :: clauses)
        | None -> [funcl]
      in
-     DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, fake_effect_opt l, clauses),
+     DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, no_effect_opt l, clauses),
                          (gen_loc l, Type_check.empty_tannot)))
      :: descatter' funcls mapcls defs
 
diff --git a/src/specialize.ml b/src/specialize.ml
index eaef1231..646b92f7 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -351,8 +351,9 @@ let specialize_id_valspec spec instantiations id ast =
 
 (* When we specialize a function definition we also need to specialize
    all the types that appear as annotations within the function
-   body. *)
-let specialize_annotations instantiation =
+   body. Also remove any type-annotation from the fundef itself,
+   because at this point we have that as a separate valspec.*)
+let specialize_annotations instantiation fdef =
   let open Type_check in
   let rw_pat = {
       id_pat_alg with
@@ -364,11 +365,20 @@ let specialize_annotations instantiation =
       lEXP_cast = (fun (typ, lexp) -> LEXP_cast (subst_unifiers instantiation typ, lexp));
       pat_alg = rw_pat
     } in
-  rewrite_fun {
-      rewriters_base with
-      rewrite_exp = (fun _ -> fold_exp rw_exp);
-      rewrite_pat = (fun _ -> fold_pat rw_pat)
-    }
+  let fdef =
+    rewrite_fun {
+        rewriters_base with
+        rewrite_exp = (fun _ -> fold_exp rw_exp);
+        rewrite_pat = (fun _ -> fold_pat rw_pat)
+      } fdef
+  in
+  match fdef with
+  | FD_aux (FD_function (rec_opt, _, eff_opt, funcls), annot) ->
+     FD_aux (FD_function (rec_opt,
+                          Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown),
+                          eff_opt,
+                          funcls),
+             annot)
 
 let specialize_id_fundef instantiations id ast =
   match split_defs (is_fundef id) ast with
-- 
cgit v1.2.3


From 084fb032de3495671d557e31dbc55dc8400f9d81 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 21 Feb 2019 23:15:15 +0000
Subject: Allow monomorphisation with C generation

Run C tests with -O -Oconstant_fold -auto_mono
---
 src/c_backend.ml |  2 ++
 src/rewrites.ml  | 11 +++++++++++
 2 files changed, 13 insertions(+)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index fd728111..3b289572 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -143,6 +143,8 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
 
+  | Typ_app (id, args) when string_of_id id = "itself" ->
+     ctyp_of_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
   | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
      begin match destruct_range Env.empty typ with
      | None -> assert false (* Checked if range type in guard *)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c78c9aee..f14d423c 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5172,10 +5172,21 @@ let rewrite_defs_ocaml = [
 
 let rewrite_defs_c = [
   ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
+
+  (* Remove bidirectional mappings *)
   ("realise_mappings", rewrite_defs_realise_mappings);
   ("toplevel_string_append", rewrite_defs_toplevel_string_append);
   ("pat_string_append", rewrite_defs_pat_string_append);
   ("mapping_builtins", rewrite_defs_mapping_patterns);
+
+  (* Monomorphisation *)
+  ("mono_rewrites", if_mono mono_rewrites);
+  ("recheck_defs", if_mono recheck_defs);
+  ("rewrite_toplevel_nexps", if_mono rewrite_toplevel_nexps);
+  ("monomorphise", if_mono monomorphise);
+  ("rewrite_atoms_to_singletons", if_mono (fun _ -> Monomorphise.rewrite_atoms_to_singletons));
+  ("recheck_defs", if_mono recheck_defs);
+
   ("rewrite_undefined", rewrite_undefined_if_gen false);
   ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
   ("remove_not_pats", rewrite_defs_not_pats);
-- 
cgit v1.2.3


From a5bf7345a1d279d00f58820459ab4ea497749cc3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 22 Feb 2019 14:46:17 +0000
Subject: Fix some bugs in int-specialization

---
 src/isail.ml       |  2 +-
 src/specialize.ml  | 73 +++++++++++++++++++++++++++++++++++++++++++++++-------
 src/specialize.mli |  2 ++
 3 files changed, 67 insertions(+), 10 deletions(-)

(limited to 'src')

diff --git a/src/isail.ml b/src/isail.ml
index 252b21b8..35350291 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -374,7 +374,7 @@ let handle_input' input =
           | Arg.Bad message | Arg.Help message -> print_endline message
         end;
      | ":spec" ->
-        let ast, env = Specialize.(specialize int_specialization !Interactive.ast !Interactive.env) in
+        let ast, env = Specialize.(specialize' 1 int_specialization !Interactive.ast !Interactive.env) in
         Interactive.ast := ast;
         Interactive.env := env;
         interactive_state := initial_state !Interactive.ast Value.primops
diff --git a/src/specialize.ml b/src/specialize.ml
index 646b92f7..f34dc85f 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -304,13 +304,61 @@ and typ_arg_int_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
   | A_order ord -> KidSet.empty
   | A_bool _ -> KidSet.empty
 
+(* Implicit arguments have restrictions that won't hold
+   post-specialisation, but we can just remove them and turn them into
+   regular arguments. *)
+let rec remove_implicit (Typ_aux (aux, l) as t) =
+  match aux with
+  | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
+  | Typ_tup typs -> Typ_aux (Typ_tup (List.map remove_implicit typs), l)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map remove_implicit arg_typs, remove_implicit ret_typ, effs), l)
+  | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (remove_implicit typ1, remove_implicit typ2), l)
+  | Typ_app (Id_aux (Id "implicit", _), args) -> Typ_aux (Typ_app (mk_id "atom", List.map remove_implicit_arg args), l)
+  | Typ_app (id, args) -> Typ_aux (Typ_app (id, List.map remove_implicit_arg args), l)
+  | Typ_id id -> Typ_aux (Typ_id id, l)
+  | Typ_exist (kopts, nc, typ) -> Typ_aux (Typ_exist (kopts, nc, remove_implicit typ), l)
+  | Typ_var v -> Typ_aux (Typ_var v, l)
+and remove_implicit_arg (A_aux (aux, l)) =
+  match aux with
+  | A_typ typ -> A_aux (A_typ (remove_implicit typ), l)
+  | arg -> A_aux (arg, l)
+
+let kopt_arg = function
+  | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> arg_nexp (nvar kid)
+  | KOpt_aux (KOpt_kind (K_aux (K_type,_), kid), _) -> arg_typ (mk_typ (Typ_var kid))
+  | _ -> failwith "oh no"
+
+(* For numeric type arguments we have to be careful not to run into a
+   situation where we have an instantiation like
+
+   'n => 'm, 'm => 8
+
+   and end up re-writing 'n to 8. This function turns an instantition
+   like the above into two,
+
+   'n => 'i#m, 'm => 8 and 'i#m => 'm
+
+   so we can do the substitution in two steps. *)
+let safe_instantiation instantiation =
+  let args =
+    List.map (fun (_, arg) -> kopts_of_typ_arg arg) (KBindings.bindings instantiation)
+    |> List.fold_left KOptSet.union KOptSet.empty
+    |> KOptSet.elements
+  in
+  List.fold_left (fun (i, r) v -> KBindings.map (fun arg -> subst_kid typ_arg_subst (kopt_kid v) (prepend_kid "i#" (kopt_kid v)) arg) i,
+                                  KBindings.add (prepend_kid "i#" (kopt_kid v)) (kopt_arg v) r)
+                 (instantiation, KBindings.empty) args
+
+let instantiate_constraints instantiation ncs =
+  List.map (fun c -> List.fold_left (fun c (v, a) -> constraint_subst v a c) c (KBindings.bindings instantiation)) ncs
+
 let specialize_id_valspec spec instantiations id ast =
   match split_defs (is_valspec id) ast with
-  | None -> failwith ("Valspec " ^ string_of_id id ^ " does not exist!")
+  | None -> Reporting.unreachable (id_loc id) __POS__ ("Valspec " ^ string_of_id id ^ " does not exist!")
   | Some (pre_ast, vs, post_ast) ->
      let typschm, externs, is_cast, annot = match vs with
        | DEF_spec (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) -> typschm, externs, is_cast, annot
-       | _ -> assert false (* unreachable *)
+       | _ -> Reporting.unreachable (id_loc id) __POS__ "val-spec is not actually a val-spec"
      in
      let TypSchm_aux (TypSchm_ts (typq, typ), _) = typschm in
 
@@ -318,8 +366,9 @@ let specialize_id_valspec spec instantiations id ast =
      let spec_ids = ref IdSet.empty in
 
      let specialize_instance instantiation =
+       let safe_instantiation, reverse = safe_instantiation instantiation in
        (* Replace the polymorphic type variables in the type with their concrete instantiation. *)
-       let typ = Type_check.subst_unifiers instantiation typ in
+       let typ = remove_implicit (Type_check.subst_unifiers reverse (Type_check.subst_unifiers safe_instantiation typ)) in
 
        (* Collect any new type variables introduced by the instantiation *)
        let collect_kids kidsets = KidSet.elements (List.fold_left KidSet.union KidSet.empty kidsets) in
@@ -328,7 +377,8 @@ let specialize_id_valspec spec instantiations id ast =
 
        (* Remove type variables from the type quantifier. *)
        let kopts, constraints = quant_split typq in
-       let constraints = List.map (fun c -> List.fold_left (fun c (v, a) -> constraint_subst v a c) c (KBindings.bindings instantiation)) constraints in
+       let constraints = instantiate_constraints safe_instantiation constraints in
+       let constraints = instantiate_constraints reverse constraints in
        let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in
        let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees
                                @ List.map (mk_qi_id K_int) int_frees
@@ -504,10 +554,15 @@ let specialize_ids spec ids ast =
   let ast = remove_unused_valspecs env ast in
   ast, env
 
-let rec specialize spec ast env =
-  let ids = polymorphic_functions spec.is_polymorphic ast in
-  if IdSet.is_empty ids then
+let rec specialize' n spec ast env =
+  if n = 0 then
     ast, env
   else
-    let ast, env = specialize_ids spec ids ast in
-    specialize spec ast env
+    let ids = polymorphic_functions spec.is_polymorphic ast in
+    if IdSet.is_empty ids then
+      ast, env
+    else
+      let ast, env = specialize_ids spec ids ast in
+      specialize' (n - 1) spec ast env
+
+let specialize = specialize' (-1)
diff --git a/src/specialize.mli b/src/specialize.mli
index 269f2340..93dec239 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -76,6 +76,8 @@ val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
    which case specialize returns the AST unmodified. *)
 val specialize : specialization -> tannot defs -> Env.t -> tannot defs * Env.t
 
+val specialize' : int -> specialization -> tannot defs -> Env.t -> tannot defs * Env.t
+
 (** return all instantiations of a function id, with the
    instantiations filtered according to the specialization. *)
 val instantiations_of : specialization -> id -> tannot defs -> typ_arg KBindings.t list
-- 
cgit v1.2.3


From fc9e071bb633fd7c7241db79146934e4ab2b33b5 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 22 Feb 2019 16:58:58 +0000
Subject: Fix more bugs in int-specialization

---
 src/sail.ml       |  1 +
 src/specialize.ml | 12 ++++++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/sail.ml b/src/sail.ml
index eaf96eb4..bd953992 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -407,6 +407,7 @@ let main() =
        then
          let ast_c = rewrite_ast_c type_envs ast in
          let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
+         (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization ast_c type_envs) in *)
          (* let ast_c = Spec_analysis.top_sort_defs ast_c in *)
          Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
diff --git a/src/specialize.ml b/src/specialize.ml
index f34dc85f..591a415a 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -380,10 +380,14 @@ let specialize_id_valspec spec instantiations id ast =
        let constraints = instantiate_constraints safe_instantiation constraints in
        let constraints = instantiate_constraints reverse constraints in
        let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in
-       let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees
-                               @ List.map (mk_qi_id K_int) int_frees
-                               @ List.map mk_qi_kopt kopts
-                               @ List.map mk_qi_nc constraints) in
+       let typq =
+         if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then
+           mk_typquant []
+         else
+           mk_typquant (List.map (mk_qi_id K_type) typ_frees
+                        @ List.map (mk_qi_id K_int) int_frees
+                        @ List.map mk_qi_kopt kopts
+                        @ List.map mk_qi_nc constraints) in
        let typschm = mk_typschm typq typ in
 
        let spec_id = id_of_instantiation id instantiation in
-- 
cgit v1.2.3


From 38656b50ad24df6a29f3a84e50adfcf409131fb0 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Fri, 22 Feb 2019 20:50:16 +0000
Subject: Generalize CT_int64 for arbitrary fixed size integers

If we want to use our low-level intermediate representation to generate
SMT, then we want to be more precise than just splitting integers into
64-bits and larger. This commit changes CT_int and CT_int64 into CT_lint
for large integers and CT_fint n for (signed) fixed precision integers
that fit within n bits. This follows the convention for bitvectors where
we have CT_fbits for fixed-length bitvectors and CT_lbits for large
arbitrary precision bitvectors.
---
 src/bytecode_util.ml | 22 ++++++++--------
 src/c_backend.ml     | 73 ++++++++++++++++++++++++++--------------------------
 2 files changed, 48 insertions(+), 47 deletions(-)

(limited to 'src')

diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 3ced48b6..489bcc64 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -252,14 +252,14 @@ and string_of_fragment' ?zencode:(zencode=true) f =
 (* String representation of ctyps here is only for debugging and
    intermediate language pretty-printer. *)
 and string_of_ctyp = function
-  | CT_int -> "int"
+  | CT_lint -> "int"
   | CT_lbits true -> "lbits(dec)"
   | CT_lbits false -> "lbits(inc)"
   | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
   | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
   | CT_sbits true -> "sbits(dec)"
   | CT_sbits false -> "sbits(inc)"
-  | CT_int64 -> "int64"
+  | CT_fint n -> "int(" ^ string_of_int n ^ ")"
   | CT_bit -> "bit"
   | CT_unit -> "unit"
   | CT_bool -> "bool"
@@ -276,14 +276,14 @@ and string_of_ctyp = function
 (** This function is like string_of_ctyp, but recursively prints all
    constructors in variants and structs. Used for debug output. *)
 and full_string_of_ctyp = function
-  | CT_int -> "int"
+  | CT_lint -> "int"
   | CT_lbits true -> "lbits(dec)"
   | CT_lbits false -> "lbits(inc)"
   | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)"
   | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)"
   | CT_sbits true -> "sbits(dec)"
   | CT_sbits false -> "sbits(inc)"
-  | CT_int64 -> "int64"
+  | CT_fint n -> "int(" ^ string_of_int n ^ ")"
   | CT_bit -> "bit"
   | CT_unit -> "unit"
   | CT_bool -> "bool"
@@ -303,7 +303,7 @@ and full_string_of_ctyp = function
   | CT_poly -> "*"
 
 let rec map_ctyp f = function
-  | (CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _
+  | (CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _
      | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp
   | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps))
   | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp))
@@ -314,12 +314,12 @@ let rec map_ctyp f = function
 
 let rec ctyp_equal ctyp1 ctyp2 =
   match ctyp1, ctyp2 with
-  | CT_int, CT_int -> true
+  | CT_lint, CT_lint -> true
   | CT_lbits d1, CT_lbits d2 -> d1 = d2
   | CT_sbits d1, CT_sbits d2 -> d1 = d2
   | CT_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2
   | CT_bit, CT_bit -> true
-  | CT_int64, CT_int64 -> true
+  | CT_fint n, CT_fint m -> n = m
   | CT_unit, CT_unit -> true
   | CT_bool, CT_bool -> true
   | CT_struct (id1, _), CT_struct (id2, _) -> Id.compare id1 id2 = 0
@@ -353,11 +353,11 @@ let rec ctyp_unify ctyp1 ctyp2 =
   | _, _ -> raise (Invalid_argument "ctyp_unify")
 
 let rec ctyp_suprema = function
-  | CT_int -> CT_int
+  | CT_lint -> CT_lint
   | CT_lbits d -> CT_lbits d
   | CT_fbits (_, d) -> CT_lbits d
   | CT_sbits d -> CT_lbits d
-  | CT_int64 -> CT_int
+  | CT_fint _ -> CT_lint
   | CT_unit -> CT_unit
   | CT_bool -> CT_bool
   | CT_real -> CT_real
@@ -382,7 +382,7 @@ let rec ctyp_ids = function
      IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors)
   | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps
   | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
-  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
     | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
 
 let rec unpoly = function
@@ -394,7 +394,7 @@ let rec unpoly = function
   | f -> f
 
 let rec is_polymorphic = function
-  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false
   | CT_tup ctyps -> List.exists is_polymorphic ctyps
   | CT_enum _ -> false
   | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 3b289572..aff2d49e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -135,8 +135,8 @@ let rec ctyp_of_typ ctx typ =
   match typ_aux with
   | Typ_id id when string_of_id id = "bit"    -> CT_bit
   | Typ_id id when string_of_id id = "bool"   -> CT_bool
-  | Typ_id id when string_of_id id = "int"    -> CT_int
-  | Typ_id id when string_of_id id = "nat"    -> CT_int
+  | Typ_id id when string_of_id id = "int"    -> CT_lint
+  | Typ_id id when string_of_id id = "nat"    -> CT_lint
   | Typ_id id when string_of_id id = "unit"   -> CT_unit
   | Typ_id id when string_of_id id = "string" -> CT_string
   | Typ_id id when string_of_id id = "real"   -> CT_real
@@ -152,13 +152,13 @@ let rec ctyp_of_typ ctx typ =
         match nexp_simp n, nexp_simp m with
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
              when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
-           CT_int64
+           CT_fint 64
         | n, m when ctx.optimize_smt ->
            if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
-             CT_int64
+             CT_fint 64
            else
-             CT_int
-        | _ -> CT_int
+             CT_lint
+        | _ -> CT_lint
      end
 
   | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
@@ -214,8 +214,9 @@ let rec ctyp_of_typ ctx typ =
   | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
 
 let rec is_stack_ctyp ctyp = match ctyp with
-  | CT_fbits _ | CT_sbits _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
-  | CT_lbits _ | CT_int | CT_real | CT_string | CT_list _ | CT_vector _ -> false
+  | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
+  | CT_fint n -> n <= 64
+  | CT_lbits _ | CT_lint | CT_real | CT_string | CT_list _ | CT_vector _ -> false
   | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
   | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *)
   | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
@@ -264,7 +265,7 @@ let hex_char =
 let literal_to_fragment (L_aux (l_aux, _) as lit) =
   match l_aux with
   | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
-     Some (F_lit (V_int n), CT_int64)
+     Some (F_lit (V_int n), CT_fint 64)
   | L_hex str when String.length str <= 16 ->
      let padding = 16 - String.length str in
      let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in
@@ -399,7 +400,7 @@ let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
        let aexp3 = analyze_functions ctx f aexp3 in
        let aexp4 = analyze_functions ctx f aexp4 in
        (* Currently we assume that loop indexes are always safe to put into an int64 *)
-       let ctx = { ctx with locals = Bindings.add id (Immutable, CT_int64) ctx.locals } in
+       let ctx = { ctx with locals = Bindings.add id (Immutable, CT_fint 64) ctx.locals } in
        AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
 
     | AE_case (aval, cases, typ) ->
@@ -544,14 +545,14 @@ let analyze_primop' ctx id args typ =
         match nexp_simp n, nexp_simp m with
         | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
                when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
-           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
+           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
         | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) ->
-           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
+           AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64))
         | _ -> no_change
      end
 
   | "neg_int", [AV_C_fragment (frag, _, _)] ->
-     AE_val (AV_C_fragment (F_op (v_int 0, "-", frag), typ, CT_int64))
+     AE_val (AV_C_fragment (F_op (v_int 0, "-", frag), typ, CT_fint 64))
 
   | "replicate_bits", [AV_C_fragment (vec, vtyp, _); AV_C_fragment (times, _, _)] ->
      begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with
@@ -738,15 +739,15 @@ let rec compile_aval l ctx = function
 
   | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 ->
      let gs = gensym () in
-     [iinit CT_int gs (F_lit (V_int n), CT_int64)],
-     (F_id gs, CT_int),
-     [iclear CT_int gs]
+     [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)],
+     (F_id gs, CT_lint),
+     [iclear CT_lint gs]
 
   | AV_lit (L_aux (L_num n, _), typ) ->
      let gs = gensym () in
-     [iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
-     (F_id gs, CT_int),
-     [iclear CT_int gs]
+     [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
+     (F_id gs, CT_lint),
+     [iclear CT_lint gs]
 
   | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), []
   | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), []
@@ -870,11 +871,11 @@ let rec compile_aval l ctx = function
        setup
        @ [iextern (CL_id (gs, vector_ctyp))
                   (mk_id "internal_vector_update")
-                  [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_int64); cval]]
+                  [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_fint 64); cval]]
        @ cleanup
      in
      [idecl vector_ctyp gs;
-      iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)]]
+      iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]]
      @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)),
      (F_id gs, vector_ctyp),
      [iclear vector_ctyp gs]
@@ -1342,8 +1343,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      cleanup
 
   | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) ->
-     (* We assume that all loop indices are safe to put in a CT_int64. *)
-     let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_int64) ctx.locals } in
+     (* We assume that all loop indices are safe to put in a CT_fint. *)
+     let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_fint 64) ctx.locals } in
 
      let is_inc = match ord with
        | Ord_inc -> true
@@ -1359,8 +1360,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in
      let step_gs = gensym () in
      let variable_init gs setup call cleanup =
-       [idecl CT_int64 gs;
-        iblock (setup @ [call (CL_id (gs, CT_int64))] @ cleanup)]
+       [idecl (CT_fint 64) gs;
+        iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)]
      in
 
      let loop_start_label = label "for_start_" in
@@ -1371,16 +1372,16 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      variable_init from_gs from_setup from_call from_cleanup
      @ variable_init to_gs to_setup to_call to_cleanup
      @ variable_init step_gs step_setup step_call step_cleanup
-     @ [iblock ([idecl CT_int64 loop_var;
-                 icopy l (CL_id (loop_var, CT_int64)) (F_id from_gs, CT_int64);
+     @ [iblock ([idecl (CT_fint 64) loop_var;
+                 icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64));
                  idecl CT_unit body_gs;
                  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, CT_unit))]
                          @ body_cleanup
-                         @ [icopy l (CL_id (loop_var, CT_int64))
-                                  (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)]
+                         @ [icopy l (CL_id (loop_var, (CT_fint 64)))
+                                  (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))]
                          @ [igoto loop_start_label]);
                  ilabel loop_end_label])],
      (fun clexp -> icopy l clexp unit_fragment),
@@ -1888,7 +1889,7 @@ let rec instrs_rename from_id to_id =
   | [] -> []
 
 let hoist_ctyp = function
-  | CT_int | CT_lbits _ | CT_struct _ -> true
+  | CT_lint | CT_lbits _ | CT_struct _ -> true
   | _ -> false
 
 let hoist_counter = ref 0
@@ -2420,8 +2421,8 @@ let rec sgen_ctyp = function
   | CT_bool -> "bool"
   | CT_fbits _ -> "fbits"
   | CT_sbits _ -> "sbits"
-  | CT_int64 -> "mach_int"
-  | CT_int -> "sail_int"
+  | CT_fint _ -> "mach_int"
+  | CT_lint -> "sail_int"
   | CT_lbits _ -> "lbits"
   | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
   | CT_struct (id, _) -> "struct " ^ sgen_id id
@@ -2440,8 +2441,8 @@ let rec sgen_ctyp_name = function
   | CT_bool -> "bool"
   | CT_fbits _ -> "fbits"
   | CT_sbits _ -> "sbits"
-  | CT_int64 -> "mach_int"
-  | CT_int -> "sail_int"
+  | CT_fint _ -> "mach_int"
+  | CT_lint -> "sail_int"
   | CT_lbits _ -> "lbits"
   | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
   | CT_struct (id, _) -> sgen_id id
@@ -2657,7 +2658,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        match ctyp with
        | CT_unit -> "UNIT", []
        | CT_bit -> "UINT64_C(0)", []
-       | CT_int64 -> "INT64_C(0xdeadc0de)", []
+       | CT_fint _ -> "INT64_C(0xdeadc0de)", []
        | CT_fbits _ -> "UINT64_C(0xdeadc0de)", []
        | CT_sbits _ -> "undefined_sbits()", []
        | CT_bool -> "false", []
@@ -3275,7 +3276,7 @@ let rec ctyp_dependencies = function
   | CT_ref ctyp -> ctyp_dependencies ctyp
   | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
   | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
-  | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> []
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> []
 
 let codegen_ctg ctx = function
   | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp)
-- 
cgit v1.2.3