diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 10 | ||||
| -rw-r--r-- | src/constraint.ml | 8 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 6 | ||||
| -rw-r--r-- | src/process_file.ml | 4 | ||||
| -rw-r--r-- | src/profile.ml | 91 | ||||
| -rw-r--r-- | src/rewrites.ml | 7 | ||||
| -rw-r--r-- | src/sail.ml | 7 |
7 files changed, 124 insertions, 9 deletions
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/process_file.ml b/src/process_file.ml index bb789d0a..53293849 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -364,8 +364,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 3505ecf4..df095e0e 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 |