summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml7
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/c_backend.ml10
-rw-r--r--src/constraint.ml8
-rw-r--r--src/ocaml_backend.ml6
-rw-r--r--src/pretty_print_sail.ml22
-rw-r--r--src/process_file.ml4
-rw-r--r--src/profile.ml91
-rw-r--r--src/rewrites.ml7
-rw-r--r--src/sail.ml7
-rw-r--r--src/type_check.ml75
11 files changed, 207 insertions, 32 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 71b3299a..d61c96ed 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -402,6 +402,13 @@ let mk_effect effs =
let no_effect = mk_effect []
+let quant_add qi typq =
+ match qi, typq with
+ | QI_aux (QI_const (NC_aux (NC_true, _)), _), _ -> typq
+ | QI_aux (QI_id _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qi :: qis), l)
+ | QI_aux (QI_const nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l)
+ | _, TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_tq [qi], l)
+
let quant_items : typquant -> quant_item list = function
| TypQ_aux (TypQ_tq qis, _) -> qis
| TypQ_aux (TypQ_no_forall, _) -> []
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 2a303475..8f555744 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -175,6 +175,8 @@ val nc_int_set : kid -> int list -> n_constraint
de-morgans to switch and to or and vice versa. *)
val nc_negate : n_constraint -> n_constraint
+(* Functions for working with type quantifiers *)
+val quant_add : quant_item -> typquant -> typquant
val quant_items : typquant -> quant_item list
val quant_kopts : typquant -> kinded_id list
val quant_split : typquant -> kinded_id list * n_constraint list
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 0c4ae87d..97477163 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -306,7 +306,9 @@ let rec c_aval ctx = function
else
v (* id's type went from heap -> stack due to flow typing, so it's really still heap allocated! *)
with
- Not_found -> failwith ("could not find " ^ string_of_id id ^ " in local variables")
+ (* Hack: Assuming global letbindings don't change from flow typing... *)
+ Not_found -> AV_C_fragment (F_id id, typ)
+ (* failwith ("could not find " ^ string_of_id id ^ " in local variables") *)
end
| Register (_, _, typ) when is_stack_typ ctx typ ->
AV_C_fragment (F_id id, typ)
@@ -427,9 +429,11 @@ let analyze_primop' ctx id args typ =
| _ -> no_change
end
+ (*
| "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] when is_stack_typ ctx typ ->
let len = F_op (f, "-", F_op (t, "-", v_one)) in
AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ))
+ *)
| "vector_access", [AV_C_fragment (vec, _); AV_C_fragment (n, _)] ->
AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ))
@@ -437,8 +441,10 @@ let analyze_primop' ctx id args typ =
| "eq_bit", [AV_C_fragment (a, _); AV_C_fragment (b, _)] ->
AE_val (AV_C_fragment (F_op (a, "==", b), typ))
+ (*
| "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] ->
AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", start)), typ))
+ *)
| "undefined_bit", _ ->
AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ))
@@ -2727,7 +2733,7 @@ let codegen_vector ctx (direction, ctyp) =
^^ string (Printf.sprintf " rop->data = malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp))
^^ (if not (is_stack_ctyp ctyp) then
string " for (int i = 0; i < len; i++) {\n"
- ^^ string (Printf.sprintf " CREATE(%s)((rop->data) + i);\n" (sgen_ctyp ctyp))
+ ^^ string (Printf.sprintf " CREATE(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp))
^^ string " }\n"
else empty)
^^ string "}"
diff --git a/src/constraint.ml b/src/constraint.ml
index d66705b6..cf861423 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -219,7 +219,7 @@ let save_digests () =
DigestMap.iter output !known_problems;
close_out out_chan
-let rec call_z3 constraints : smt_result =
+let call_z3' constraints : smt_result =
let problems = [constraints] in
let z3_file = smtlib_of_constraints constraints in
@@ -261,6 +261,12 @@ let rec call_z3 constraints : smt_result =
else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
end
+let call_z3 constraints =
+ let t = Profile.start_z3 () in
+ let result = call_z3' constraints in
+ Profile.finish_z3 t;
+ result
+
let rec solve_z3 constraints var =
let problems = [constraints] in
let z3_file = smtlib_of_constraints ~get_model:true constraints in
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 3ad4c07f..9a48421a 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -359,10 +359,10 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp =
else ocaml_atomic_exp ctx exp
in
separate space [zencode ctx id; string ":="; traced_exp]
- | _ -> separate space [zencode ctx id; string ":="; ocaml_exp ctx exp]
+ | _ -> separate space [zencode ctx id; string ":="; parens (ocaml_exp ctx exp)]
end
| LEXP_deref ref_exp ->
- separate space [ocaml_atomic_exp ctx ref_exp; string ":="; ocaml_exp ctx exp]
+ separate space [ocaml_atomic_exp ctx ref_exp; string ":="; parens (ocaml_exp ctx exp)]
| _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
match lexp_aux with
@@ -933,7 +933,7 @@ let ocaml_main spec sail_dir =
@ [ " zinitializze_registers ();";
if !opt_trace_ocaml then " Sail_lib.opt_trace := true;" else " ();";
" Printexc.record_backtrace true;";
- " try zmain () with _ -> prerr_endline(\"Exiting due to uncaught exception\")\n";])
+ " try zmain () with exn -> prerr_endline(\"Exiting due to uncaught exception:\\n\" ^ Printexc.to_string exn)\n";])
|> String.concat "\n"
let ocaml_pp_defs f defs generator_types =
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7608f78b..792c3d23 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -68,7 +68,7 @@ let doc_kid kid = string (Ast_util.string_of_kid kid)
let doc_int n = string (Big_int.to_string n)
let docstring (l, _) = match l with
- | Parse_ast.Documented (str, _) -> string "/**" ^^ string str ^^ string "*/" ^^ hardline
+ | Parse_ast.Documented (str, _) -> string "/*!" ^^ string str ^^ string "*/" ^^ hardline
| _ -> empty
let doc_ord (Ord_aux(o,_)) = match o with
@@ -119,7 +119,7 @@ let doc_nc nc =
match nc_aux with
| NC_true -> string "true"
| NC_false -> string "false"
- | NC_equal (n1, n2) -> nc_op "=" n1 n2
+ | NC_equal (n1, n2) -> nc_op "==" n1 n2
| NC_not_equal (n1, n2) -> nc_op "!=" n1 n2
| NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2
| NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
@@ -321,7 +321,8 @@ let fixities =
let rec doc_exp (E_aux (e_aux, _) as exp) =
match e_aux with
| E_block [] -> string "()"
- | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace
+ | E_block exps ->
+ group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace)
| E_nondet exps -> assert false
(* This is mostly for the -convert option *)
| E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
@@ -485,13 +486,14 @@ let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) =
let doc_default (DT_aux (DT_order ord, _)) = separate space [string "default"; string "Order"; doc_ord ord]
-let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) =
- match funcls with
- | [] -> failwith "Empty function list"
- | _ ->
- let sep = hardline ^^ string "and" ^^ space in
- let clauses = separate_map sep doc_funcl funcls in
- string "function" ^^ space ^^ clauses
+let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), annot)) =
+ docstring annot
+ ^^ match funcls with
+ | [] -> failwith "Empty function list"
+ | _ ->
+ let sep = hardline ^^ string "and" ^^ space in
+ let clauses = separate_map sep doc_funcl funcls in
+ string "function" ^^ space ^^ clauses
let rec doc_mpat (MP_aux (mp_aux, _) as mpat) =
match mp_aux with
diff --git a/src/process_file.ml b/src/process_file.ml
index 3788d269..c3d0be0e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -365,8 +365,10 @@ let output libpath out_arg files =
output1 libpath out_arg f defs)
files
-let rewrite_step defs (name,rewriter) =
+let rewrite_step defs (name, rewriter) =
+ let t = Profile.start () in
let defs = rewriter defs in
+ Profile.finish ("rewrite " ^ name) t;
let _ = match !(opt_ddump_rewrite_ast) with
| Some (f, i) ->
begin
diff --git a/src/profile.ml b/src/profile.ml
new file mode 100644
index 00000000..cb374403
--- /dev/null
+++ b/src/profile.ml
@@ -0,0 +1,91 @@
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+let opt_profile = ref false
+
+type profile = {
+ z3_calls : int;
+ z3_time : float
+ }
+
+let new_profile = {
+ z3_calls = 0;
+ z3_time = 0.0
+ }
+
+let profile_stack = ref []
+
+let update_profile f =
+ match !profile_stack with
+ | [] -> ()
+ | (p :: ps) ->
+ profile_stack := f p :: ps
+
+let start_z3 () =
+ update_profile (fun p -> { p with z3_calls = p.z3_calls + 1 });
+ Sys.time ()
+
+let finish_z3 t =
+ update_profile (fun p -> { p with z3_time = p.z3_time +. (Sys.time () -. t) })
+
+let start () =
+ profile_stack := new_profile :: !profile_stack;
+ Sys.time ()
+
+let finish msg t =
+ if !opt_profile then
+ begin match !profile_stack with
+ | p :: ps ->
+ prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profile" |> magenta |> clear) msg (Sys.time () -. t));
+ prerr_endline (Printf.sprintf " Z3 calls: %d, Z3 time: %fs" p.z3_calls p.z3_time);
+ profile_stack := ps
+ | [] -> ()
+ end
+ else ()
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c274ded4..591b86a7 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2591,7 +2591,10 @@ let rewrite_tuple_assignments defs =
let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in
let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in
let block = mk_exp (E_block (List.mapi block_assign lexps)) in
- let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in
+ let letbind = mk_letbind (mk_pat (P_typ (Type_check.typ_of exp,
+ mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids)))))
+ (strip_exp exp)
+ in
let let_exp = mk_exp (E_let (letbind, block)) in
begin
try check_exp env let_exp unit_typ with
@@ -2641,7 +2644,7 @@ let rewrite_defs_remove_blocks =
let e_aux = function
| (E_block es,(l,_)) -> f l es
| (e,annot) -> E_aux (e,annot) in
-
+
let alg = { id_exp_alg with e_aux = e_aux } in
rewrite_defs_base
diff --git a/src/sail.ml b/src/sail.ml
index 9208190d..c9cead2a 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -240,6 +240,9 @@ let options = Arg.align ([
( "-dfunction",
Arg.String (fun f -> C_backend.opt_debug_function := f),
" (debug) print debugging output for a single function");
+ ( "-dprofile",
+ Arg.Set Profile.opt_profile,
+ " (debug) provides basic profiling information for rewriting passes within Sail");
( "-Xconstraint_synonyms",
Arg.Set Type_check.opt_constraint_synonyms,
" (extension) allow constraint synonyms");
@@ -265,14 +268,18 @@ let interactive_env = ref Type_check.initial_env
let load_files type_envs files =
if !opt_memo_z3 then Constraint.load_digests () else ();
+ let t = Profile.start () in
let parsed = List.map (fun f -> (f, parse_file f)) files in
let ast =
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 = convert_ast Ast_util.inc_ord 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 = rewrite_ast ast in
diff --git a/src/type_check.ml b/src/type_check.ml
index 4ad93a0c..0079d59f 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -758,17 +758,52 @@ end = struct
with
| Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
+ let ex_counter = ref 0
+
+ (* TODO: Currently this is duplicated with destruct_exist outside of Env and deals with val spec arguments only. *)
+ let fresh_existential ?name:(n="") () =
+ let fresh = Kid_aux (Var ("'all" ^ string_of_int !ex_counter ^ "#" ^ n), Parse_ast.Unknown) in
+ incr ex_counter; fresh
+
+ let destruct_exist env typ =
+ match expand_synonyms env typ with
+ | Typ_aux (Typ_exist (kids, nc, typ), _) ->
+ let fresh_kids = List.map (fun kid -> (kid, fresh_existential ~name:(string_of_id (id_of_kid kid)) ())) kids in
+ let nc = List.fold_left (fun nc (kid, fresh) -> nc_subst_nexp kid (Nexp_var fresh) nc) nc fresh_kids in
+ let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst_nexp kid (Nexp_var fresh) typ) typ fresh_kids in
+ Some (List.map snd fresh_kids, nc, typ)
+ | _ -> None
+
let rec update_val_spec id (typq, typ) env =
- begin
- let typ = expand_synonyms env typ in
- let typq = expand_typquant_synonyms env typq in
- typ_print (lazy (adding ^ "val spec " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
- let env = match typ with
- | Typ_aux (Typ_bidir (typ1, typ2), _) -> add_mapping id (typq, typ1, typ2) env
- | _ -> env
- in
- { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
+ begin match expand_synonyms env typ with
+ | Typ_aux (Typ_fn (arg_typs, ret_typ, effect), l) ->
+ (* We perform some canonicalisation for function types where existentials appear on the left, so
+ ({'n, 'n >= 2, int('n)}, foo) -> bar
+ would become
+ forall 'n, 'n >= 2. (int('n), foo) -> bar
+ this enforces the invariant that all things on the left of functions are 'base types' (i.e. without existentials)
+ *)
+ let typq = expand_typquant_synonyms env typq in
+ let base_args = List.map (destruct_exist env) arg_typs in
+ let existential_arg typq = function
+ | None -> typq
+ | Some (exs, nc, _) ->
+ List.fold_left (fun typq kid -> quant_add (mk_qi_id BK_int kid) typq) (quant_add (mk_qi_nc nc) typq) exs
+ in
+ let typq = List.fold_left existential_arg typq base_args in
+ let arg_typs = List.map2 (fun typ -> function Some (_, _, typ) -> typ | None -> typ) arg_typs base_args in
+ let typ = Typ_aux (Typ_fn (arg_typs, ret_typ, effect), l) in
+ typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
+ { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
+
+ | Typ_aux (Typ_bidir (typ1, typ2), l) ->
+ let env = add_mapping id (typq, typ1, typ2) env in
+ typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
+ { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
+
+ | _ -> typ_error (id_loc id) "val definition must have a mapping or function type"
end
+
and add_val_spec id (bind_typq, bind_typ) env =
if not (Bindings.mem id env.top_val_specs)
then update_val_spec id (bind_typq, bind_typ) env
@@ -780,6 +815,7 @@ end = struct
typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound as " ^ string_of_bind (existing_typq, existing_typ) ^ ", cannot rebind as " ^ string_of_bind (bind_typq, bind_typ))
else
env
+
and add_mapping id (typq, typ1, typ2) env =
begin
typ_print (lazy (adding ^ "mapping " ^ string_of_id id));
@@ -2955,9 +2991,19 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
| _ -> assert false
end
| _ ->
- let inferred_exp = irule infer_exp env exp in
- let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in
- annot_assign tlexp inferred_exp, env'
+ (* Here we have two options, we can infer the type from the
+ expression, or we can infer the type from the
+ l-expression. Both are useful in different cases, so try
+ both. *)
+ try
+ let inferred_exp = irule infer_exp env exp in
+ let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in
+ annot_assign tlexp inferred_exp, env'
+ with
+ | Type_error (_, _) ->
+ let inferred_lexp = infer_lexp env lexp in
+ let checked_exp = crule check_exp env exp (lexp_typ_of inferred_lexp) in
+ annot_assign inferred_lexp checked_exp, env
and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^ " to " ^ string_of_typ typ));
@@ -3099,7 +3145,10 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
in
let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in
annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ weff
- | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp)
+ | LEXP_tup lexps ->
+ let inferred_lexps = List.map (infer_lexp env) lexps in
+ annot_lexp (LEXP_tup inferred_lexps) (tuple_typ (List.map lexp_typ_of inferred_lexps))
+ | _ -> typ_error l ("Could not infer the type of " ^ string_of_lexp lexp)
and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let annot_exp_effect exp typ eff = E_aux (exp, (l, Some ((env, typ, eff),None))) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 02:49:03 +0000