From b3ea287bcf8be43714595b6921a0c47d25a67eee Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 16 Nov 2018 16:26:35 +0000 Subject: Various bugfixes and a simple profiling feature for rewrites --- lib/arith.sail | 4 +-- lib/rts.c | 4 +++ lib/sail.c | 11 +++++++ lib/sail.h | 3 ++ src/c_backend.ml | 10 ++++-- src/constraint.ml | 8 ++++- src/ocaml_backend.ml | 6 ++-- src/process_file.ml | 4 ++- src/profile.ml | 91 ++++++++++++++++++++++++++++++++++++++++++++++++++++ src/rewrites.ml | 7 ++-- src/sail.ml | 7 ++++ 11 files changed, 144 insertions(+), 11 deletions(-) create mode 100644 src/profile.ml diff --git a/lib/arith.sail b/lib/arith.sail index e61ec473..db011f14 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -57,13 +57,13 @@ let elsize = shl_int(8, UInt(size)) ``` THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` */ -val _shl8 = "shl_int" : +val _shl8 = {c: "shl_mach_int", _: "shl_int"} : forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64} /*! Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` */ -val _shl32 = "shl_int" : +val _shl32 = {c: "shl_mach_int", _: "shl_int"} : forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64} val _shl_int = "shl_int" : (int, int) -> int diff --git a/lib/rts.c b/lib/rts.c index 6bd97934..2f594ff8 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -94,6 +94,10 @@ void write_mem(uint64_t address, uint64_t byte) uint64_t mask = address & ~MASK; uint64_t offset = address & MASK; + //if ((byte >= 97 && byte <= 122) || (byte >= 64 && byte <= 90) || (byte >= 48 && byte <= 57) || byte == 10 || byte == 32) { + // fprintf(stderr, "%c", (char) byte); + //} + struct block *current = sail_memory; while (current != NULL) { diff --git a/lib/sail.c b/lib/sail.c index 94cd5c2c..fc11a40d 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -290,6 +290,12 @@ void shl_int(sail_int *rop, const sail_int op1, const sail_int op2) mpz_mul_2exp(*rop, op1, mpz_get_ui(op2)); } +inline +mach_int shl_mach_int(const mach_int op1, const mach_int op2) +{ + return op1 << op2; +} + inline void shr_int(sail_int *rop, const sail_int op1, const sail_int op2) { @@ -446,6 +452,11 @@ void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const ui mpz_init_set_ui(*rop->bits, op); } +mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits op) +{ + return mpz_get_ui(*op.bits); +} + void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction) { rop->len = len; diff --git a/lib/sail.h b/lib/sail.h index 4ccd8b93..b3386198 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -131,6 +131,7 @@ bool gteq(const sail_int, const sail_int); /* * Left and right shift for integers */ +mach_int shl_mach_int(const mach_int, const mach_int); SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int); @@ -192,6 +193,8 @@ void RECREATE_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits len, const bool direction); +mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits); + mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool); void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool); 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 -- cgit v1.2.3