From 26510d7798daac30a400e8d04278a86ea8b83983 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 14 Apr 2020 17:16:29 +0100 Subject: Add add_symbol to the API of Process_file Allows clients of sail as a library to define custom symbols for $ifdef and $ifndef Iterate vector concat assignment and tuple assignment to handle unusual nesting cases when compiling to C. These rewrites should really be one rewrite anyway though! Don't add type annotations when introducing tuple patterns during rewriting. I guess not adding them could also cause an error in some circumstances, but if that's the case it could probably be fixed by tweaking some rules in the type-checker. --- src/process_file.ml | 2 ++ src/process_file.mli | 1 + src/rewrites.ml | 5 +++-- 3 files changed, 6 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/process_file.ml b/src/process_file.ml index d2a86595..116788b9 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -108,6 +108,8 @@ let have_symbol symbol = let clear_symbols () = symbols := default_symbols +let add_symbol str = symbols := StringSet.add str !symbols + let cond_pragma l defs = let depth = ref 0 in let in_then = ref true in diff --git a/src/process_file.mli b/src/process_file.mli index d1fa2cb8..c9eb5e9e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -54,6 +54,7 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs val clear_symbols : unit -> unit val have_symbol : string -> bool +val add_symbol : string -> unit val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t diff --git a/src/rewrites.ml b/src/rewrites.ml index 863f8115..e622d620 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2114,8 +2114,7 @@ let rewrite_tuple_assignments env 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_typ (Type_check.typ_of exp, - mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))))) + let letbind = mk_letbind (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 @@ -5033,6 +5032,8 @@ let rewrites_c = [ ("pattern_literals", [Literal_arg "all"]); ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); + ("tuple_assignments", []); ("simple_assignments", []); ("exp_lift_assign", []); ("merge_function_clauses", []); -- cgit v1.2.3 From b727e02d59c130b6b6d1eb969a0e4fa8cc156e51 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 15 Apr 2020 15:57:38 +0100 Subject: Add more intuitive defaults to interactive toplevel sail -i now starts an interactive toplevel with a few additional options set by default: - It applies the "interpreter" rewrites to any files passed on the command line. - It also applies those rewrites after the :l/:load command - Registers previously started in a disabled state, as the interactive shell made no default decision as to how to handle undefined (which is the initial value for all registers). Now -i implies -undefined_gen - Better help text for :fix_registers - Nullary interactive actions generate Sail functions that round-trip through pretty printing and parsing (bugfix) The -interact_custom flag has the same behavior as the previous -i flag This commit also improves the c/ocaml/interpreter test harness so it cleans up temporary files which could cause issues with stale files when switching ocaml versions --- src/constant_fold.ml | 8 +++++++- src/interactive.ml | 5 ++++- src/interactive.mli | 1 + src/interpreter.ml | 2 +- src/isail.ml | 22 +++++++++++++++++++--- src/sail.ml | 14 ++++++++++++-- 6 files changed, 44 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 35417ac8..1c273df1 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -374,4 +374,10 @@ let () = ~name:"fix_registers" ~help:"Fix the value of specified registers, specified as a \ list of =. Can also fix a specific \ - register field as .=." + register field as .=. Note that \ + this is not used to set registers normally, but instead \ + fixes their value such that the constant folding rewrite \ + (which is subsequently invoked by this command) will \ + replace register reads with the fixed values. Requires a \ + target (c, lem, etc.), as the set of functions that can \ + be constant folded can differ on a per-target basis." diff --git a/src/interactive.ml b/src/interactive.ml index 2cca944c..93df1dc0 100644 --- a/src/interactive.ml +++ b/src/interactive.ml @@ -55,6 +55,7 @@ open Printf let opt_interactive = ref false let opt_emacs_mode = ref false let opt_suppress_banner = ref false +let opt_auto_interpreter_rewrites = ref false let env = ref Type_check.initial_env @@ -80,7 +81,9 @@ let reflect_typ action = | ArgInt (_, next) -> int_typ :: arg_typs (next 0) | Action _ -> [] in - function_typ (arg_typs action) unit_typ no_effect + match action with + | Action _ -> function_typ [unit_typ] unit_typ no_effect + | _ -> function_typ (arg_typs action) unit_typ no_effect let generate_help name help action = let rec args = function diff --git a/src/interactive.mli b/src/interactive.mli index 933d0a46..b0cce425 100644 --- a/src/interactive.mli +++ b/src/interactive.mli @@ -54,6 +54,7 @@ open Type_check val opt_interactive : bool ref val opt_emacs_mode : bool ref val opt_suppress_banner : bool ref +val opt_auto_interpreter_rewrites : bool ref val ast : tannot defs ref diff --git a/src/interpreter.ml b/src/interpreter.ml index a30e90bc..b3e8fe31 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -961,7 +961,7 @@ let rec initialize_registers allow_registers gstate = begin let env = Type_check.env_of_annot annot in let typ = Type_check.Env.expand_synonyms env typ in - let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit (L_undef))))) in + let exp = mk_exp (E_cast (typ, mk_exp (E_lit (mk_lit L_undef)))) in let exp = Type_check.check_exp env exp typ in { gstate with registers = Bindings.add id (eval_exp (initial_lstate, gstate) exp) gstate.registers } end diff --git a/src/isail.ml b/src/isail.ml index 02908321..7c4affa3 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -113,7 +113,8 @@ let sep = "-----------------------------------------------------" |> Util.blue | let vs_ids = ref (val_spec_ids !Interactive.ast) -let interactive_state = ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops) +let interactive_state = + ref (initial_state ~registers:false !Interactive.ast !Interactive.env !Value.primops) (* We can't set up the elf commands in elf_loader.ml because it's used by Sail OCaml emulators at runtime, so set them up here. *) @@ -314,6 +315,8 @@ let help = | ":option" -> sprintf ":option %s - Parse string as if it was an option passed on the command line. e.g. :option -help." (color yellow "") + | ":recheck" -> + sprintf ":recheck - Re type-check the Sail AST, and synchronize the interpreters internal state to that AST." | ":rewrite" -> sprintf ":rewrite %s - Apply a rewrite to the AST. %s shows all possible rewrites. See also %s" (color yellow " ") (color green ":list_rewrites") (color green ":rewrites") @@ -468,7 +471,7 @@ let handle_input' input = let more_commands = Util.string_of_list " " fst !Interactive.commands in let commands = [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :assume :clear :commands :help :output :option"; - "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :rewrite :rewrites :list_rewrites :compile " ^ more_commands; + "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :recheck :rewrite :rewrites :list_rewrites :compile " ^ more_commands; "Evaluation mode commands - :(r)un :(s)tep :(n)ormal"; ""; ":(c)ommand can be called as either :c or :command." ] @@ -510,9 +513,15 @@ let handle_input' input = | ":l" | ":load" -> let files = Util.split_on_char ' ' arg in let (_, ast, env) = Process_file.load_files options !Interactive.env files in + let ast, env = + if !Interactive.opt_auto_interpreter_rewrites then + Process_file.rewrite_ast_target "interpreter" env ast + else + ast, env + in Interactive.ast := append_ast !Interactive.ast ast; - interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; Interactive.env := env; + interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops; vs_ids := val_spec_ids !Interactive.ast | ":u" | ":unload" -> Interactive.ast := Ast.Defs []; @@ -819,6 +828,13 @@ let () = | _ -> None ); + if !Interactive.opt_auto_interpreter_rewrites then ( + let new_ast, new_env = Process_file.rewrite_ast_target "interpreter" !Interactive.env !Interactive.ast in + Interactive.ast := new_ast; + Interactive.env := new_env; + interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops + ); + (* Read the script file if it is set with the -is option, and excute them *) begin match !opt_interactive_script with | None -> () diff --git a/src/sail.ml b/src/sail.ml index ea642470..64e4f8c6 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -77,14 +77,24 @@ let options = Arg.align ([ Arg.String (fun f -> opt_file_out := Some f), " select output filename prefix"); ( "-i", - Arg.Tuple [Arg.Set Interactive.opt_interactive], + Arg.Tuple [Arg.Set Interactive.opt_interactive; + Arg.Set Interactive.opt_auto_interpreter_rewrites; + Arg.Set Initial_check.opt_undefined_gen], " start interactive interpreter"); ( "-is", - Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.String (fun s -> opt_interactive_script := Some s)], + Arg.Tuple [Arg.Set Interactive.opt_interactive; + Arg.Set Interactive.opt_auto_interpreter_rewrites; + Arg.Set Initial_check.opt_undefined_gen; + Arg.String (fun s -> opt_interactive_script := Some s)], " start interactive interpreter and execute commands in script"); ( "-iout", Arg.String (fun file -> Value.output_redirect (open_out file)), " print interpreter output to file"); + ( "-interact_custom", + Arg.Set Interactive.opt_interactive, + " drop to an interactive session after running Sail. Differs from \ + -i in that it does not set up the interpreter in the interactive \ + shell."); ( "-emacs", Arg.Set Interactive.opt_emacs_mode, " run sail interactively as an emacs mode child process"); -- cgit v1.2.3 From 54b6277d79c64d15b155fc161d927aa968afafa1 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 22 Apr 2020 14:46:33 +0100 Subject: Add an interactive command to evaluate until the end of a function Callable as either :f or :step_function Allow // to be used as a comment in the interactive toplevel --- src/isail.ml | 165 ++++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 107 insertions(+), 58 deletions(-) (limited to 'src') diff --git a/src/isail.ml b/src/isail.ml index 7c4affa3..dc7858c9 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -193,34 +193,75 @@ let rec run () = match !current_mode with | Normal | Emacs -> () | Evaluation frame -> - begin - match frame with - | Done (state, v) -> - interactive_state := state; - print_endline ("Result = " ^ Value.string_of_value v); - current_mode := Normal - | Fail (_, _, _, _, msg) -> - print_endline ("Error: " ^ msg); - current_mode := Normal - | Step (out, state, _, stack) -> - begin - try - current_mode := Evaluation (eval_frame frame) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run () - | Break frame -> - print_endline "Breakpoint"; - current_mode := Evaluation frame - | Effect_request (out, state, stack, eff) -> - begin - try - current_mode := Evaluation (!Interpreter.effect_interp state eff) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run () + begin match frame with + | Done (state, v) -> + interactive_state := state; + print_endline ("Result = " ^ Value.string_of_value v); + current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal + | Step (out, state, _, stack) -> + begin + try + current_mode := Evaluation (eval_frame frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run () + | Break frame -> + print_endline "Breakpoint"; + current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (!Interpreter.effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run () + end + +let rec run_function depth = + let run_function' stack = + match depth with + | None -> run_function (Some (List.length stack)) + | Some n -> + if List.compare_length_with stack n >= 0 then + run_function depth + else + () + in + match !current_mode with + | Normal | Emacs -> () + | Evaluation frame -> + begin match frame with + | Done (state, v) -> + interactive_state := state; + print_endline ("Result = " ^ Value.string_of_value v); + current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal + | Step (out, state, _, stack) -> + begin + try + current_mode := Evaluation (eval_frame frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_function' stack + | Break frame -> + print_endline "Breakpoint"; + current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (!Interpreter.effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_function' stack end let rec run_steps n = @@ -228,36 +269,35 @@ let rec run_steps n = | _ when n <= 0 -> () | Normal | Emacs -> () | Evaluation frame -> - begin - match frame with - | Done (state, v) -> - interactive_state := state; - print_endline ("Result = " ^ Value.string_of_value v); - current_mode := Normal - | Fail (_, _, _, _, msg) -> - print_endline ("Error: " ^ msg); - current_mode := Normal - | Step (out, state, _, stack) -> - begin - try - current_mode := Evaluation (eval_frame frame) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run_steps (n - 1) - | Break frame -> - print_endline "Breakpoint"; - current_mode := Evaluation frame - | Effect_request (out, state, stack, eff) -> - begin - try - current_mode := Evaluation (!Interpreter.effect_interp state eff) - with - | Failure str -> print_endline str; current_mode := Normal - end; - run_steps (n - 1) + begin match frame with + | Done (state, v) -> + interactive_state := state; + print_endline ("Result = " ^ Value.string_of_value v); + current_mode := Normal + | Fail (_, _, _, _, msg) -> + print_endline ("Error: " ^ msg); + current_mode := Normal + | Step (out, state, _, stack) -> + begin + try + current_mode := Evaluation (eval_frame frame) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_steps (n - 1) + | Break frame -> + print_endline "Breakpoint"; + current_mode := Evaluation frame + | Effect_request (out, state, stack, eff) -> + begin + try + current_mode := Evaluation (!Interpreter.effect_interp state eff) + with + | Failure str -> print_endline str; current_mode := Normal + end; + run_steps (n - 1) end - + let help = let open Printf in let open Util in @@ -298,6 +338,8 @@ let help = | ":s" | ":step" -> sprintf "(:s | :step) %s - Perform a number of evaluation steps." (color yellow "") + | ":f" | ":step_function" -> + sprintf "(:s | :step) - Perform evaluation steps until the currently evaulating function returns." | ":n" | ":normal" -> "(:n | :normal) - Exit evaluation mode back to normal mode." | ":clear" -> @@ -422,6 +464,9 @@ let handle_input' input = let cmd = Str.string_before input n in let arg = String.trim (Str.string_after input n) in Command (cmd, arg) + else if String.length input >= 2 && input.[0] = '/' && input.[1] = '/' then + (* Treat anything starting with // as a comment *) + Empty else if input <> "" then Expression input else @@ -693,7 +738,11 @@ let handle_input' input = | ":r" | ":run" -> run () | ":s" | ":step" -> - run_steps (int_of_string arg) + run_steps (int_of_string arg); + print_program () + | ":f" | ":step_function" -> + run_function None; + print_program () | _ -> unrecognised_command cmd end | Expression str -> -- cgit v1.2.3 From ba2e8265c99bc31c9d1eb8829c4b63d7e2ccf3f4 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 27 Apr 2020 17:20:46 +0100 Subject: Fix try in exception handler jib bug The have_exception flag wasn't being cleared until after the handler, resulting in false exception reporting. --- src/jib/jib_compile.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 34477967..e5dcd8b5 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -664,8 +664,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctyp = ctyp_of_typ ctx typ in let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in let try_return_id = ngensym () in - let handled_exception_label = label "handled_exception_" in - let fallthrough_label = label "fallthrough_exception_" in + let post_exception_handlers_label = label "post_exception_handlers_" in let compile_case (apat, guard, body) = let trivial_guard = match guard with | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) @@ -686,19 +685,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ [icomment "end guard"] else []) @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup - @ [igoto handled_exception_label] + @ [igoto post_exception_handlers_label] in [iblock case_instrs; ilabel try_label] in assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [idecl ctyp try_return_id; itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); - ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label] + ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) post_exception_handlers_label; + icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool))] @ List.concat (List.map compile_case cases) - @ [igoto fallthrough_label; - ilabel handled_exception_label; - icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool)); - ilabel fallthrough_label], + @ [(* fallthrough *) + icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool)); + ilabel post_exception_handlers_label], (fun clexp -> icopy l clexp (V_id (try_return_id, ctyp))), [] -- cgit v1.2.3 From 199e10df8e776e4b27f9cfd2357db6babf674ed1 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 28 Apr 2020 17:24:04 +0100 Subject: Functorise and refactor C code generator Currently uses the -c2 option Now generates a sail_state struct which is passed as a pointer to all generated functions. This contains all registers, letbindings, and the exception state. (Letbindings must be included as they can contain pointers to registers). This should make it possible to use sail models in a multi-threaded program by creating multiple sail_states, provided a suitable set of thread-safe memory builtins are provided. Currently the sail_state cannot be passed to the memory builtins. For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c. foo_emu.c wraps the generated library into an emulator that behaves the same as the one we previously generated. The sail_assert and sail_match_failure builtins are now in a separate file, as they must exist even when the RTS is not used. Name mangling can be controlled via the exports and exports_mangled fields of the configuration struct (currently not exposed outside of OCaml). exports allows specifying a name in C for any Sail identifier (before name mangling) and exports_mangled allows specifiying a name for a mangled Sail identifier - this is primarily useful for generic functions and data structures which have been specialised. --- src/jib/c_backend.ml | 181 ++++-- src/jib/c_backend.mli | 12 +- src/jib/c_codegen.ml | 1617 +++++++++++++++++++++++++++++++++++++++++++++++ src/jib/jib_compile.ml | 28 +- src/jib/jib_compile.mli | 11 +- src/jib/jib_ir.ml | 2 +- src/jib/jib_optimize.ml | 2 + src/jib/jib_smt.ml | 18 +- src/jib/jib_ssa.ml | 1 + src/jib/jib_util.ml | 8 +- src/rewrites.ml | 1 + src/sail.ml | 26 +- 12 files changed, 1836 insertions(+), 71 deletions(-) create mode 100644 src/jib/c_codegen.ml (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 2b2234b5..829f4d37 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -63,7 +63,6 @@ module Big_int = Nat_big_num let opt_static = ref false let opt_no_main = ref false -let opt_memo_cache = ref false let opt_no_lib = ref false let opt_no_rts = ref false let opt_prefix = ref "z" @@ -130,6 +129,41 @@ let rec is_stack_ctyp ctyp = match ctyp with let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true)) +let hex_char = + let open Sail2_values in + function + | '0' -> [B0; B0; B0; B0] + | '1' -> [B0; B0; B0; B1] + | '2' -> [B0; B0; B1; B0] + | '3' -> [B0; B0; B1; B1] + | '4' -> [B0; B1; B0; B0] + | '5' -> [B0; B1; B0; B1] + | '6' -> [B0; B1; B1; B0] + | '7' -> [B0; B1; B1; B1] + | '8' -> [B1; B0; B0; B0] + | '9' -> [B1; B0; B0; B1] + | 'A' | 'a' -> [B1; B0; B1; B0] + | 'B' | 'b' -> [B1; B0; B1; B1] + | 'C' | 'c' -> [B1; B1; B0; B0] + | 'D' | 'd' -> [B1; B1; B0; B1] + | 'E' | 'e' -> [B1; B1; B1; B0] + | 'F' | 'f' -> [B1; B1; B1; B1] + | _ -> failwith "Invalid hex character" + +let literal_to_fragment (L_aux (l_aux, _) as lit) = + match l_aux with + | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> + Some (V_lit (VL_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 + let content = Util.string_to_list str |> List.map hex_char |> List.concat in + Some (V_lit (VL_bits (padding @ content, true), CT_fbits (String.length str * 4, true))) + | L_unit -> Some (V_lit (VL_unit, CT_unit)) + | L_true -> Some (V_lit (VL_bool true, CT_bool)) + | L_false -> Some (V_lit (VL_bool false, CT_bool)) + | _ -> None + module C_config : Config = struct (** Convert a sail type into a C-type. This function can be quite @@ -232,41 +266,6 @@ module C_config : Config = struct (* 3. Optimization of primitives and literals *) (**************************************************************************) - let hex_char = - let open Sail2_values in - function - | '0' -> [B0; B0; B0; B0] - | '1' -> [B0; B0; B0; B1] - | '2' -> [B0; B0; B1; B0] - | '3' -> [B0; B0; B1; B1] - | '4' -> [B0; B1; B0; B0] - | '5' -> [B0; B1; B0; B1] - | '6' -> [B0; B1; B1; B0] - | '7' -> [B0; B1; B1; B1] - | '8' -> [B1; B0; B0; B0] - | '9' -> [B1; B0; B0; B1] - | 'A' | 'a' -> [B1; B0; B1; B0] - | 'B' | 'b' -> [B1; B0; B1; B1] - | 'C' | 'c' -> [B1; B1; B0; B0] - | 'D' | 'd' -> [B1; B1; B0; B1] - | 'E' | 'e' -> [B1; B1; B1; B0] - | 'F' | 'f' -> [B1; B1; B1; B1] - | _ -> failwith "Invalid hex character" - - let literal_to_fragment (L_aux (l_aux, _) as lit) = - match l_aux with - | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> - Some (V_lit (VL_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 - let content = Util.string_to_list str |> List.map hex_char |> List.concat in - Some (V_lit (VL_bits (padding @ content, true), CT_fbits (String.length str * 4, true))) - | L_unit -> Some (V_lit (VL_unit, CT_unit)) - | L_true -> Some (V_lit (VL_bool true, CT_bool)) - | L_false -> Some (V_lit (VL_bool false, CT_bool)) - | _ -> None - let c_literals ctx = let rec c_literal env l = function | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) -> @@ -565,6 +564,100 @@ module C_config : Config = struct let use_real = false end +(* When compiling to a C library, we want to do things slightly + differently. First, to ensure that functions have a predictable + type and calling convention, we don't use the SMT solver to + optimize types at all. Second we don't apply the analyse primitives + step in optimize_anf for similar reasons. *) +module Clib_config : Config = struct + let rec convert_typ ctx typ = + let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in + 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_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 + + | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool + | Typ_app (id, _) when + string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" || string_of_id id = "itself" -> + begin match destruct_range Env.empty typ with + | None -> assert false (* Checked if range type in guard *) + | Some (kids, constr, n, m) -> + let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env }in + match nexp_simp n, nexp_simp m with + | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) + when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> + CT_fint 64 + | _, _ -> + CT_lint + end + + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> + CT_list (convert_typ ctx typ) + + | Typ_app (id, [A_aux (A_nexp n, _); + A_aux (A_order ord, _)]) + when string_of_id id = "bitvector" -> + 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) + | _ -> CT_lbits direction + end + + | Typ_app (id, [A_aux (A_nexp n, _); + A_aux (A_order ord, _); + A_aux (A_typ typ, _)]) + when string_of_id id = "vector" -> + let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in + CT_vector (direction, convert_typ ctx typ) + + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" -> + CT_ref (convert_typ ctx typ) + + | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> UBindings.bindings) + | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants |> UBindings.bindings) + | Typ_id id when Bindings.mem id ctx.enums -> CT_enum (id, Bindings.find id ctx.enums |> IdSet.elements) + + | Typ_tup typs -> CT_tup (List.map (convert_typ ctx) typs) + + | Typ_exist _ -> + begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with + | Some (kids, nc, typ) -> + let env = add_existential l kids nc ctx.local_env in + convert_typ { ctx with local_env = env } typ + | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!") + end + + | Typ_var kid -> CT_poly + + | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ) + + let c_literals ctx = + let rec c_literal env l = function + | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) -> + begin + match literal_to_fragment lit with + | Some cval -> AV_cval (cval, typ) + | None -> v + end + | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals) + | v -> v + in + map_aval c_literal + + let optimize_anf ctx aexp = c_literals ctx aexp + + let unroll_loops () = None + let specialize_calls = false + let ignore_64 = false + let struct_value = false + let use_real = false +end + (** Functions that have heap-allocated return types are implemented by passing a pointer a location where the return value should be stored. The ANF -> Sail IR pass for expressions simply outputs an @@ -1329,6 +1422,7 @@ let rec sgen_clexp = function | CL_id (Throw_location _, _) -> "throw_location" | CL_id (Return _, _) -> assert false | CL_id (Name (id, _), _) -> "&" ^ sgen_id id + | CL_id (Global (id, _), _) -> "&" ^ sgen_id id | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ zencode_uid field ^ ")" | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")" | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))" @@ -1341,6 +1435,7 @@ let rec sgen_clexp_pure = function | CL_id (Throw_location _, _) -> "throw_location" | CL_id (Return _, _) -> assert false | CL_id (Name (id, _), _) -> sgen_id id + | CL_id (Global (id, _), _) -> sgen_id id | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ zencode_uid field | CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))" @@ -2222,7 +2317,7 @@ let jib_of_ast env ast = let module Jibc = Make(C_config) in let ctx = initial_ctx (add_special_functions env) in Jibc.compile_ast ctx ast - + let compile_ast env output_chan c_includes ast = try let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in @@ -2336,3 +2431,15 @@ let compile_ast env output_chan c_includes ast = with | Type_error (_, l, err) -> c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) + +let jib_of_ast_clib env ast = + let module Jibc = Make(Clib_config) in + let ctx = initial_ctx (add_special_functions env) in + Jibc.compile_ast ctx ast + +let compile_ast_clib env ast codegen = + let cdefs, ctx = jib_of_ast env ast in + let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in + Jib_interactive.ir := cdefs'; + let cdefs = insert_heap_returns Bindings.empty cdefs in + codegen ctx cdefs diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index e627ebd8..2334cc0e 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -88,15 +88,6 @@ val opt_prefix : string ref val opt_extra_params : string option ref val opt_extra_arguments : string option ref -(** (WIP) [opt_memo_cache] will store the compiled function - definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum - of the original function to be compiled. Enabled using the -memo - flag. Uses Marshal so it's quite picky about the exact version of - the Sail version. This cache can obviously become stale if the C - backend changes - it'll load an old version compiled without said - changes. *) -val opt_memo_cache : bool ref - (** Optimization flags *) val optimize_primops : bool ref @@ -108,3 +99,6 @@ val optimize_fixed_bits : bool ref val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit + +val jib_of_ast_clib : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx +val compile_ast_clib : Env.t -> tannot Ast.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml new file mode 100644 index 00000000..6aa0060c --- /dev/null +++ b/src/jib/c_codegen.ml @@ -0,0 +1,1617 @@ +(**************************************************************************) +(* 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. *) +(**************************************************************************) + +open Ast +open Ast_util +open Jib +open Jib_compile +open Jib_util +open Type_check +open PPrint +open Printf +open Value2 + +module StringMap = Map.Make(String) +module Big_int = Nat_big_num + +let opt_no_main = ref false +let opt_no_lib = ref false +let opt_no_rts = ref false + +let (gensym, _) = symbol_generator "c2" +let ngensym () = name (gensym ()) + +let zencode_id id = Util.zencode_string (string_of_id id) + +let zencode_uid (id, ctyps) = + match ctyps with + | [] -> Util.zencode_string (string_of_id id) + | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) + +let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty + +let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) +let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) + +(** This function is used to split types into those we allocate on the + stack, versus those which need to live on the heap, or otherwise + require some additional memory management *) +let rec is_stack_ctyp ctyp = match ctyp with + | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true + | CT_fint n -> n <= 64 + (* | CT_lint when !optimize_fixed_int -> true *) + | CT_lint -> false + (* | CT_lbits _ when !optimize_fixed_bits -> true *) + | CT_lbits _ -> false + | CT_real | CT_string | CT_list _ | CT_vector _ | CT_fvector _ -> 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 + | CT_ref ctyp -> true + | CT_poly -> true + | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64) + +let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true)) + +type codegen_options = { + exports : string Bindings.t; + exports_mangled : string StringMap.t; + } + +let add_export opts id = { opts with exports = Bindings.add id (string_of_id id) opts.exports } + +let add_custom_export opts id into = { opts with exports = Bindings.add id into opts.exports } + +let add_mangled_rename opts (from, into) = { opts with exports_mangled = StringMap.add from into opts.exports_mangled } + +let add_export_uid opts (id, ctyps) = + match ctyps with + | [] -> { opts with exports = Bindings.add id (string_of_id id) opts.exports } + | _ -> opts + +let ctype_def_initial_options opts = function + | CTD_enum (id, ids) -> + List.fold_left add_export (add_export opts id) ids + | CTD_struct (id, ctors) -> + List.fold_left add_export_uid (add_export opts id) (List.map fst ctors) + | _ -> opts + +let cdef_initial_options opts = function + | CDEF_type ctype_def -> ctype_def_initial_options opts ctype_def + | CDEF_reg_dec (id, _, _) -> add_export opts id + | CDEF_let (_, bindings, _) -> List.fold_left (fun opts (id, _) -> add_export opts id) opts bindings + | _ -> opts + +let initial_options = { + exports = Bindings.empty; + exports_mangled = StringMap.empty; + } + +let default_options cdefs = + let opts = List.fold_left cdef_initial_options initial_options cdefs in + let opts = add_export opts (mk_id "initialize_registers") in + let opts = add_custom_export opts (mk_id "main") "sail_main" in + List.fold_left add_mangled_rename opts (List.init 9 (fun n -> "ztup" ^ string_of_int n, "tuple_" ^ string_of_int n)) + +module type Config = sig + val opts : codegen_options +end + +module Make(C: Config) = struct + +let mangle str = + let mangled = Util.zencode_string str in + match StringMap.find_opt mangled C.opts.exports_mangled with + | Some export -> export + | None -> mangled + +let sgen_id id = + match Bindings.find_opt id C.opts.exports with + | Some export -> export + | None -> mangle (string_of_id id) + +let sgen_name = + function + | Name (id, _) -> + sgen_id id + | Global (id, _) -> + sprintf "(state->%s)" (sgen_id id) + | Have_exception _ -> + "(state->have_exception)" + | Return _ -> + assert false + | Current_exception _ -> + "(*(state->current_exception))" + | Throw_location _ -> + "(state->throw_location)" + +let sgen_uid (id, ctyps) = + match ctyps with + | [] -> sgen_id id + | _ -> + mangle (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) + +let codegen_id id = string (sgen_id id) +let codegen_uid id = string (sgen_uid id) + +let sgen_function_id id = sgen_id id +let sgen_function_uid uid = sgen_uid uid +let codegen_function_id id = string (sgen_function_id id) + +let rec sgen_ctyp = function + | CT_unit -> "unit" + | CT_bit -> "fbits" + | CT_bool -> "bool" + | CT_fbits _ -> "uint64_t" + | CT_sbits _ -> "sbits" + | CT_fint _ -> "int64_t" + | CT_constant _ -> "int64_t" + | 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 + | CT_enum (id, _) -> "enum " ^ sgen_id id + | CT_variant (id, _) -> "struct " ^ sgen_id id + | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) + | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v) + | CT_fvector (_, ord, typ) -> sgen_ctyp (CT_vector (ord, typ)) + | CT_string -> "sail_string" + | CT_real -> "real" + | CT_ref ctyp -> sgen_ctyp ctyp ^ "*" + | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *) + +let rec sgen_ctyp_name = function + | CT_unit -> "unit" + | CT_bit -> "fbits" + | CT_bool -> "bool" + | CT_fbits _ -> "fbits" + | CT_sbits _ -> "sbits" + | CT_fint _ -> "mach_int" + | CT_constant _ -> "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 + | CT_enum (id, _) -> sgen_id id + | CT_variant (id, _) -> sgen_id id + | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) + | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v) + | CT_fvector (_, ord, typ) -> sgen_ctyp_name (CT_vector (ord, typ)) + | CT_string -> "sail_string" + | CT_real -> "real" + | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp + | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *) + +let sgen_mask n = + if n = 0 then + "UINT64_C(0)" + else if n <= 64 then + let chars_F = String.make (n / 4) 'F' in + let first = match (n mod 4) with + | 0 -> "" + | 1 -> "1" + | 2 -> "3" + | 3 -> "7" + | _ -> assert false + in + "UINT64_C(0x" ^ first ^ chars_F ^ ")" + else + failwith "Tried to create a mask literal for a vector greater than 64 bits." + +let rec sgen_value = function + | VL_bits ([], _) -> "UINT64_C(0)" + | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" + | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")" + | VL_int i -> Big_int.to_string i ^ "l" + | VL_bool true -> "true" + | VL_bool false -> "false" + | VL_unit -> "UNIT" + | VL_bit Sail2_values.B0 -> "UINT64_C(0)" + | VL_bit Sail2_values.B1 -> "UINT64_C(1)" + | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value" + | VL_real str -> str + | VL_string str -> "\"" ^ str ^ "\"" + | VL_empty_list -> "NULL" + | VL_enum element -> mangle element + | VL_ref r -> "&(state->" ^ sgen_id (mk_id r) ^ ")" + | VL_undefined -> + Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal" + +let rec sgen_cval ctx = function + | V_id (id, ctyp) -> + sgen_name id + | V_lit (vl, ctyp) -> sgen_value vl + | V_call (op, cvals) -> sgen_call ctx op cvals + | V_field (f, field) -> + sprintf "%s.%s" (sgen_cval ctx f) (sgen_uid field) + | V_tuple_member (f, _, n) -> + sprintf "%s.%s" (sgen_cval ctx f) (mangle ("tup" ^ string_of_int n)) + | V_ctor_kind (f, ctor, unifiers, _) -> + sgen_cval ctx f ^ ".kind" + ^ " != Kind_" ^ zencode_uid (ctor, unifiers) + | V_struct (fields, _) -> + sprintf "{%s}" + (Util.string_of_list ", " (fun (field, cval) -> zencode_uid field ^ " = " ^ sgen_cval ctx cval) fields) + | V_ctor_unwrap (ctor, f, unifiers, _) -> + sprintf "%s.%s" + (sgen_cval ctx f) + (sgen_uid (ctor, unifiers)) + | V_poly (f, _) -> sgen_cval ctx f + +and sgen_call ctx op cvals = + match op, cvals with + | Bnot, [v] -> "!(" ^ sgen_cval ctx v ^ ")" + | List_hd, [v] -> + sprintf "(%s).hd" ("*" ^ sgen_cval ctx v) + | List_tl, [v] -> + sprintf "(%s).tl" ("*" ^ sgen_cval ctx v) + | Eq, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_sbits _ -> + sprintf "eq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> + sprintf "(%s == %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + end + | Neq, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_sbits _ -> + sprintf "neq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> + sprintf "(%s != %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + end + | Ilt, [v1; v2] -> + sprintf "(%s < %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Igt, [v1; v2] -> + sprintf "(%s > %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Ilteq, [v1; v2] -> + sprintf "(%s <= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Igteq, [v1; v2] -> + sprintf "(%s >= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Iadd, [v1; v2] -> + sprintf "(%s + %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Isub, [v1; v2] -> + sprintf "(%s - %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | Unsigned 64, [vec] -> + sprintf "((mach_int) %s)" (sgen_cval ctx vec) + | Signed 64, [vec] -> + begin match cval_ctyp vec with + | CT_fbits (n, _) -> + sprintf "fast_signed(%s, %d)" (sgen_cval ctx vec) n + | _ -> assert false + end + | Bvand, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + sprintf "(%s & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | CT_sbits _ -> + sprintf "and_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvnot, [v] -> + begin match cval_ctyp v with + | CT_fbits (n, _) -> + sprintf "(~(%s) & %s)" (sgen_cval ctx v) (sgen_cval ctx (v_mask_lower n)) + | CT_sbits _ -> + sprintf "not_sbits(%s)" (sgen_cval ctx v) + | _ -> assert false + end + | Bvor, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + sprintf "(%s | %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | CT_sbits _ -> + sprintf "or_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvxor, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + sprintf "(%s ^ %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | CT_sbits _ -> + sprintf "xor_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvadd, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits (n, _) -> + sprintf "((%s + %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n)) + | CT_sbits _ -> + sprintf "add_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvsub, [v1; v2] -> + begin match cval_ctyp v1 with + | CT_fbits (n, _) -> + sprintf "((%s - %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n)) + | CT_sbits _ -> + sprintf "sub_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | Bvaccess, [vec; n] -> + begin match cval_ctyp vec with + | CT_fbits _ -> + sprintf "(UINT64_C(1) & (%s >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n) + | CT_sbits _ -> + sprintf "(UINT64_C(1) & (%s.bits >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n) + | _ -> assert false + end + | Slice len, [vec; start] -> + begin match cval_ctyp vec with + | CT_fbits _ -> + sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start) + | CT_sbits _ -> + sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s.bits >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start) + | _ -> assert false + end + | Sslice 64, [vec; start; len] -> + begin match cval_ctyp vec with + | CT_fbits _ -> + sprintf "sslice(%s, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len) + | CT_sbits _ -> + sprintf "sslice(%s.bits, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len) + | _ -> assert false + end + | Set_slice, [vec; start; slice] -> + begin match cval_ctyp vec, cval_ctyp slice with + | CT_fbits (n, _), CT_fbits (m, _) -> + sprintf "((%s & ~(%s << %s)) | (%s << %s))" (sgen_cval ctx vec) (sgen_mask m) (sgen_cval ctx start) (sgen_cval ctx slice) (sgen_cval ctx start) + | _ -> assert false + end + | Zero_extend n, [v] -> + begin match cval_ctyp v with + | CT_fbits _ -> sgen_cval ctx v + | CT_sbits _ -> + sprintf "fast_zero_extend(%s, %d)" (sgen_cval ctx v) n + | _ -> assert false + end + | Sign_extend n, [v] -> + begin match cval_ctyp v with + | CT_fbits (m, _) -> + sprintf "fast_sign_extend(%s, %d, %d)" (sgen_cval ctx v) m n + | CT_sbits _ -> + sprintf "fast_sign_extend2(%s, %d)" (sgen_cval ctx v) n + | _ -> assert false + end + | Replicate n, [v] -> + begin match cval_ctyp v with + | CT_fbits (m, _) -> + sprintf "fast_replicate_bits(UINT64_C(%d), %s, %d)" m (sgen_cval ctx v) n + | _ -> assert false + end + | Concat, [v1; v2] -> + (* Optimized routines for all combinations of fixed and small bits + appends, where the result is guaranteed to be smaller than 64. *) + begin match cval_ctyp v1, cval_ctyp v2 with + | CT_fbits (0, _), CT_fbits (n2, _) -> + sgen_cval ctx v2 + | CT_fbits (n1, _), CT_fbits (n2, _) -> + sprintf "(%s << %d) | %s" (sgen_cval ctx v1) n2 (sgen_cval ctx v2) + | CT_sbits (64, ord1), CT_fbits (n2, _) -> + sprintf "append_sf(%s, %s, %d)" (sgen_cval ctx v1) (sgen_cval ctx v2) n2 + | CT_fbits (n1, ord1), CT_sbits (64, ord2) -> + sprintf "append_fs(%s, %d, %s)" (sgen_cval ctx v1) n1 (sgen_cval ctx v2) + | CT_sbits (64, ord1), CT_sbits (64, ord2) -> + sprintf "append_ss(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) + | _ -> assert false + end + | _, _ -> + failwith "Could not generate cval primop" + +let sgen_cval_param ctx cval = + match cval_ctyp cval with + | CT_lbits direction -> + sgen_cval ctx cval ^ ", " ^ string_of_bool direction + | CT_sbits (_, direction) -> + sgen_cval ctx cval ^ ", " ^ string_of_bool direction + | CT_fbits (len, direction) -> + sgen_cval ctx cval ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction + | _ -> + sgen_cval ctx cval + +let rec sgen_clexp ctx = function + | CL_id (Have_exception _, _) -> "(state->have_exception)" + | CL_id (Current_exception _, _) -> "(state->current_exception)" + | CL_id (Throw_location _, _) -> "(state->throw_location)" + | CL_id (Return _, _) -> assert false + | CL_id (Global (id, _), _) -> "&(state->" ^ sgen_id id ^ ")" + | CL_id (Name (id, _), _) -> "&" ^ sgen_id id + | CL_field (clexp, field) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ sgen_uid field ^ ")" + | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ mangle ("tup" ^ string_of_int n) ^ ")" + | CL_addr clexp -> "(*(" ^ sgen_clexp ctx clexp ^ "))" + | CL_void -> assert false + | CL_rmw _ -> assert false + +let rec sgen_clexp_pure ctx = function + | CL_id (Have_exception _, _) -> "(state->have_exception)" + | CL_id (Current_exception _, _) -> "(state->current_exception)" + | CL_id (Throw_location _, _) -> "(state->throw_location)" + | CL_id (Return _, _) -> assert false + | CL_id (Global (id, _), _) -> "state->" ^ sgen_id id + | CL_id (Name (id, _), _) -> sgen_id id + | CL_field (clexp, field) -> sgen_clexp_pure ctx clexp ^ "." ^ sgen_uid field + | CL_tuple (clexp, n) -> sgen_clexp_pure ctx clexp ^ "." ^ mangle ("tup" ^ string_of_int n) + | CL_addr clexp -> "(*(" ^ sgen_clexp_pure ctx clexp ^ "))" + | CL_void -> assert false + | CL_rmw _ -> assert false + +(** Generate instructions to copy from a cval to a clexp. This will + insert any needed type conversions from big integers to small + integers (or vice versa), or from arbitrary-length bitvectors to + and from uint64 bitvectors as needed. *) +let rec codegen_conversion l ctx clexp cval = + let ctyp_to = clexp_ctyp clexp in + let ctyp_from = cval_ctyp cval in + match ctyp_to, ctyp_from with + (* When both types are equal, we don't need any conversion. *) + | _, _ when ctyp_equal ctyp_to ctyp_from -> + if is_stack_ctyp ctyp_to then + ksprintf string " %s = %s;" (sgen_clexp_pure ctx clexp) (sgen_cval ctx cval) + else + ksprintf string " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp_to) (sgen_clexp ctx clexp) (sgen_cval ctx cval) + + | CT_ref ctyp_to, ctyp_from -> + codegen_conversion l ctx (CL_addr clexp) cval + + (* If we have to convert between tuple types, convert the fields individually. *) + | CT_tup ctyps_to, CT_tup ctyps_from when List.length ctyps_to = List.length ctyps_from -> + let len = List.length ctyps_to in + let conversions = + List.mapi (fun i ctyp -> codegen_conversion l ctx (CL_tuple (clexp, i)) (V_tuple_member (cval, len, i))) ctyps_from + in + string " /* conversions */" + ^^ hardline + ^^ separate hardline conversions + ^^ hardline + ^^ string " /* end conversions */" + + (* For anything not special cased, just try to call a appropriate CONVERT_OF function. *) + | _, _ when is_stack_ctyp (clexp_ctyp clexp) -> + ksprintf string " %s = CONVERT_OF(%s, %s)(%s);" + (sgen_clexp_pure ctx clexp) (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_cval_param ctx cval) + | _, _ -> + ksprintf string " CONVERT_OF(%s, %s)(%s, %s);" + (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_clexp ctx clexp) (sgen_cval_param ctx cval) + +let extra_params () = "sail_state *state, " + +let extra_arguments is_extern = + if is_extern then + "" + else + "state, " + +let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = + match instr with + | I_decl (ctyp, id) when is_stack_ctyp ctyp -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) + | I_decl (ctyp, id) -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) ^^ hardline + ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id) + + | I_copy (clexp, cval) -> codegen_conversion l ctx clexp cval + + | I_jump (cval, label) -> + ksprintf string " if (%s) goto %s;" (sgen_cval ctx cval) label + + | I_if (cval, [then_instr], [], ctyp) -> + ksprintf string " if (%s)" (sgen_cval ctx cval) ^^ hardline + ^^ twice space ^^ codegen_instr fid ctx then_instr + | I_if (cval, then_instrs, [], ctyp) -> + string " if" ^^ space ^^ parens (string (sgen_cval ctx cval)) ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace) + | I_if (cval, then_instrs, else_instrs, ctyp) -> + string " if" ^^ space ^^ parens (string (sgen_cval ctx cval)) ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace) + ^^ space ^^ string "else" ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) else_instrs) (twice space ^^ rbrace) + + | I_block instrs -> + string " {" + ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline + ^^ string " }" + + | I_try_block instrs -> + string " { /* try */" + ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline + ^^ string " }" + + | I_funcall (x, special_extern, f, args) -> + let c_args = Util.string_of_list ", " (sgen_cval ctx) args in + let ctyp = clexp_ctyp x in + let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || special_extern in + let fname = + if special_extern then + string_of_id (fst f) + else if Env.is_extern (fst f) ctx.tc_env "c" then + Env.get_extern (fst f) ctx.tc_env "c" + else + sgen_function_uid f + in + let fname = + match fname, ctyp with + | "internal_pick", _ -> sprintf "pick_%s" (sgen_ctyp_name ctyp) + | "cons", _ -> + begin match snd f with + | [ctyp] -> Util.zencode_string ("cons#" ^ string_of_ctyp ctyp) + | _ -> Reporting.unreachable l __POS__ "cons without specified type" + end + | "eq_anything", _ -> + begin match args with + | cval :: _ -> sprintf "eq_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> Reporting.unreachable l __POS__ "eq_anything function with bad arity." + end + | "length", _ -> + begin match args with + | cval :: _ -> sprintf "length_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> Reporting.unreachable l __POS__ "length function with bad arity." + end + | "vector_access", CT_bit -> "bitvector_access" + | "vector_access", _ -> + begin match args with + | cval :: _ -> sprintf "vector_access_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> Reporting.unreachable l __POS__ "vector access function with bad arity." + end + | "vector_update_subrange", _ -> sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp) + | "vector_subrange", _ -> sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp) + | "vector_update", CT_fbits _ -> "update_fbits" + | "vector_update", CT_lbits _ -> "update_lbits" + | "vector_update", _ -> sprintf "vector_update_%s" (sgen_ctyp_name ctyp) + | "string_of_bits", _ -> + begin match cval_ctyp (List.nth args 0) with + | CT_fbits _ -> "string_of_fbits" + | CT_lbits _ -> "string_of_lbits" + | _ -> assert false + end + | "decimal_string_of_bits", _ -> + begin match cval_ctyp (List.nth args 0) with + | CT_fbits _ -> "decimal_string_of_fbits" + | CT_lbits _ -> "decimal_string_of_lbits" + | _ -> assert false + end + | "internal_vector_update", _ -> sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) + | "internal_vector_init", _ -> sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) + | "undefined_bitvector", CT_fbits _ -> "UNDEFINED(fbits)" + | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)" + | "undefined_bit", _ -> "UNDEFINED(fbits)" + | "undefined_vector", _ -> sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) + | "undefined_list", _ -> sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp) + | fname, _ -> fname + in + if fname = "reg_deref" then + if is_stack_ctyp ctyp then + ksprintf string " %s = *(%s);" (sgen_clexp_pure ctx x) c_args + else + ksprintf string " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure ctx x) c_args + else + if is_stack_ctyp ctyp then + ksprintf string " %s = %s(%s%s);" (sgen_clexp_pure ctx x) fname (extra_arguments is_extern) c_args + else + ksprintf string " %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp ctx x) c_args + + | I_clear (ctyp, id) when is_stack_ctyp ctyp -> + empty + | I_clear (ctyp, id) -> + ksprintf string " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id) + + | I_init (ctyp, id, cval) -> + codegen_instr fid ctx (idecl ctyp id) ^^ hardline + ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval + + | I_reinit (ctyp, id, cval) -> + codegen_instr fid ctx (ireset ctyp id) ^^ hardline + ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval + + | I_reset (ctyp, id) when is_stack_ctyp ctyp -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) + | I_reset (ctyp, id) -> + ksprintf string " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id) + + | I_return cval -> + ksprintf string " return %s;" (sgen_cval ctx cval) + + | I_throw cval -> + Reporting.unreachable l __POS__ "I_throw reached code generator" + + | I_undefined ctyp -> + let rec codegen_exn_return ctyp = + match ctyp with + | CT_unit -> "UNIT", [] + | CT_bit -> "UINT64_C(0)", [] + | CT_fint _ -> "INT64_C(0xdeadc0de)", [] + (* | CT_lint when !optimize_fixed_int -> "((sail_int) 0xdeadc0de)", [] *) + | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] + | CT_sbits _ -> "undefined_sbits()", [] + (* | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits(false)", [] *) + | CT_bool -> "false", [] + | CT_enum (_, ctor :: _) -> sgen_id ctor, [] + | CT_tup ctyps when is_stack_ctyp ctyp -> + let gs = ngensym () in + let fold (inits, prev) (n, ctyp) = + let init, prev' = codegen_exn_return ctyp in + sprintf ".%s = %s" (mangle ("tup" ^ string_of_int n)) init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in + sgen_name gs, + [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | CT_struct (id, ctors) when is_stack_ctyp ctyp -> + let gs = ngensym () in + let fold (inits, prev) (uid, ctyp) = + let init, prev' = codegen_exn_return ctyp in + sprintf ".%s = %s" (sgen_uid uid) init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) ctors in + sgen_name gs, + [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | ctyp -> Reporting.unreachable l __POS__ ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp) + in + let ret, prev = codegen_exn_return ctyp in + separate_map hardline (fun str -> string (" " ^ str)) (List.rev prev) + ^^ hardline + ^^ ksprintf string " return %s;" ret + + | I_comment str -> + string (" /* " ^ str ^ " */") + + | I_label str -> + string (str ^ ": ;") + + | I_goto str -> + ksprintf string " goto %s;" str + + | I_raw _ when ctx.no_raw -> empty + | I_raw str -> + string (" " ^ str) + + | I_end _ -> assert false + + | I_match_failure -> + string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") + +(**************************************************************************) +(* Code generation for type definitions (enums, structs, and variants) *) +(**************************************************************************) + +let codegen_type_def_header = function + | CTD_enum (id, ids) -> + ksprintf string "// enum %s" (string_of_id id) ^^ hardline + ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi] + ^^ twice hardline + + | CTD_struct (id, ctors) -> + let codegen_ctor (id, ctyp) = + string (sgen_ctyp ctyp) ^^ space ^^ codegen_uid id + in + ksprintf string "// struct %s" (string_of_id id) ^^ hardline + ^^ string "struct" ^^ space ^^ codegen_id id ^^ space + ^^ surround 2 0 lbrace + (separate_map (semi ^^ hardline) codegen_ctor ctors ^^ semi) + rbrace + ^^ semi ^^ twice hardline + + | CTD_variant (id, tus) -> + let codegen_tu (ctor_id, ctyp) = + separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_uid ctor_id ^^ semi; rbrace] + in + ksprintf string "// union %s" (string_of_id id) ^^ hardline + ^^ string "enum" ^^ space + ^^ string ("kind_" ^ sgen_id id) ^^ space + ^^ separate space [ lbrace; + separate_map (comma ^^ space) (fun id -> string ("Kind_" ^ sgen_uid id)) (List.map fst tus); + rbrace ^^ semi ] + ^^ twice hardline + ^^ string "struct" ^^ space ^^ codegen_id id ^^ space + ^^ surround 2 0 lbrace + (separate space [string "enum"; string ("kind_" ^ sgen_id id); string "kind" ^^ semi] + ^^ hardline + ^^ string "union" ^^ space + ^^ surround 2 0 lbrace + (separate_map (semi ^^ hardline) codegen_tu tus ^^ semi) + rbrace + ^^ semi) + rbrace + ^^ semi + ^^ twice hardline + +let codegen_type_def_body ctx = function + | CTD_enum (id, ((first_id :: _) as ids)) -> + let codegen_eq = + let name = sgen_id id in + string (Printf.sprintf "bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name) + in + let codegen_undefined = + let name = sgen_id id in + string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) + in + codegen_eq + ^^ twice hardline + ^^ codegen_undefined + + | CTD_enum (id, []) -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot compile empty enum " ^ string_of_id id) + + | CTD_struct (id, ctors) -> + let struct_ctyp = CT_struct (id, ctors) in + (* Generate a set_T function for every struct T *) + let codegen_set (id, ctyp) = + if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op.%s;" (sgen_uid id) (sgen_uid id)) + else + string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid id) (sgen_uid id)) + in + let codegen_setter id ctors = + string (let n = sgen_id id in Printf.sprintf "static void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space + ^^ surround 2 0 lbrace + (separate_map hardline codegen_set (UBindings.bindings ctors)) + rbrace + in + (* Generate an init/clear_T function for every struct T *) + let codegen_field_init f (id, ctyp) = + if not (is_stack_ctyp ctyp) then + [string (Printf.sprintf "%s(%s)(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_uid id))] + else [] + in + let codegen_init f id ctors = + string (let n = sgen_id id in Printf.sprintf "static void %s(%s)(struct %s *op)" f n n) ^^ space + ^^ surround 2 0 lbrace + (separate hardline (UBindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat)) + rbrace + in + let codegen_eq = + let codegen_eq_test (id, ctyp) = + string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_uid id) (sgen_uid id)) + in + string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2)" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ space + ^^ surround 2 0 lbrace + (string "return" ^^ space + ^^ separate_map (string " && ") codegen_eq_test ctors + ^^ string ";") + rbrace + in + (* Generate the struct and add the generated functions *) + let codegen_ctor (id, ctyp) = + string (sgen_ctyp ctyp) ^^ space ^^ codegen_uid id + in + codegen_setter id (ctor_bindings ctors) + ^^ (if not (is_stack_ctyp struct_ctyp) then + twice hardline + ^^ codegen_init "CREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "RECREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "KILL" id (ctor_bindings ctors) + else empty) + ^^ twice hardline + ^^ codegen_eq + + | CTD_variant (id, tus) -> + let codegen_tu (ctor_id, ctyp) = + separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_uid ctor_id ^^ semi; rbrace] + in + (* Create an if, else if, ... block that does something for each constructor *) + let rec each_ctor v f = function + | [] -> string "{}" + | [(ctor_id, ctyp)] -> + string (Printf.sprintf "if (%skind == Kind_%s)" v (sgen_uid ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (f ctor_id ctyp) + ^^ hardline ^^ rbrace + | (ctor_id, ctyp) :: ctors -> + string (Printf.sprintf "if (%skind == Kind_%s) " v (sgen_uid ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (f ctor_id ctyp) + ^^ hardline ^^ rbrace ^^ string " else " ^^ each_ctor v f ctors + in + let codegen_init = + let n = sgen_id id in + let ctor_id, ctyp = List.hd tus in + string (Printf.sprintf "static void CREATE(%s)(struct %s *op)" n n) + ^^ hardline + ^^ surround 2 0 lbrace + (string (Printf.sprintf "op->kind = Kind_%s;" (sgen_uid ctor_id)) ^^ hardline + ^^ if not (is_stack_ctyp ctyp) then + string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) + else empty) + rbrace + in + let codegen_reinit = + let n = sgen_id id in + string (Printf.sprintf "static void RECREATE(%s)(struct %s *op) {}" n n) + in + let clear_field v ctor_id ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "/* do nothing */") + else + string (Printf.sprintf "KILL(%s)(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_uid ctor_id)) + in + let codegen_clear = + let n = sgen_id id in + string (Printf.sprintf "static void KILL(%s)(struct %s *op)" n n) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "op->" (clear_field "op") tus ^^ semi) + rbrace + in + let codegen_ctor (ctor_id, ctyp) = + let ctor_args = Printf.sprintf "%s op" (sgen_ctyp ctyp) in + string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_uid ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "rop->" (clear_field "rop") tus ^^ hardline + ^^ string ("rop->kind = Kind_" ^ sgen_uid ctor_id) ^^ semi ^^ hardline + ^^ if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op;" (sgen_uid ctor_id)) + else + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) ^^ hardline + ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id))) + rbrace + in + let codegen_setter = + let n = sgen_id id in + let set_field ctor_id ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op.%s;" (sgen_uid ctor_id) (sgen_uid ctor_id)) + else + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) + ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id) (sgen_uid ctor_id)) + in + string (Printf.sprintf "static void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "rop->" (clear_field "rop") tus + ^^ semi ^^ hardline + ^^ string "rop->kind = op.kind" + ^^ semi ^^ hardline + ^^ each_ctor "op." set_field tus) + rbrace + in + let codegen_eq = + let codegen_eq_test ctor_id ctyp = + string (Printf.sprintf "return EQUAL(%s)(op1.%s, op2.%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id) (sgen_uid ctor_id)) + in + let rec codegen_eq_tests = function + | [] -> string "return false;" + | (ctor_id, ctyp) :: ctors -> + string (Printf.sprintf "if (op1.kind == Kind_%s && op2.kind == Kind_%s) " (sgen_uid ctor_id) (sgen_uid ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (codegen_eq_test ctor_id ctyp) + ^^ hardline ^^ rbrace ^^ string " else " ^^ codegen_eq_tests ctors + in + let n = sgen_id id in + string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2) " n n n) + ^^ surround 2 0 lbrace (codegen_eq_tests tus) rbrace + in + codegen_init + ^^ twice hardline + ^^ codegen_reinit + ^^ twice hardline + ^^ codegen_clear + ^^ twice hardline + ^^ codegen_setter + ^^ twice hardline + ^^ codegen_eq + ^^ twice hardline + ^^ separate_map (twice hardline) codegen_ctor tus + +let codegen_type_def ctx ctype_def = + codegen_type_def_header ctype_def, codegen_type_def_body ctx ctype_def + +(**************************************************************************) +(* Code generation for generated types (lists, tuples, etc) *) +(**************************************************************************) + +(** GLOBAL: because C doesn't have real anonymous tuple types + (anonymous structs don't quite work the way we need) every tuple + type in the spec becomes some generated named struct in C. This is + done in such a way that every possible tuple type has a unique name + associated with it. This global variable keeps track of these + generated struct names, so we never generate two copies of the + struct that is used to represent them in C. + + The way this works is that codegen_def scans each definition's type + annotations for tuple types and generates the required structs + using codegen_type_def before the actual definition is generated by + codegen_def'. + + This variable should be reset to empty only when the entire AST has + been translated to C. **) +let generated = ref IdSet.empty + +let codegen_tup ctx ctyps = + let id = mk_id ("tuple_" ^ string_of_ctyp (CT_tup ctyps)) in + if IdSet.mem id !generated then + empty, empty + else + begin + let _, fields = List.fold_left (fun (n, fields) ctyp -> n + 1, UBindings.add (mk_id ("tup" ^ string_of_int n), []) ctyp fields) + (0, UBindings.empty) + ctyps + in + generated := IdSet.add id !generated; + codegen_type_def ctx (CTD_struct (id, UBindings.bindings fields)) + end + +let codegen_list_header id = + ksprintf string "// generated list type %s" (string_of_id id) ^^ hardline + ^^ ksprintf string "struct node_%s;" (sgen_id id) ^^ hardline + ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id) + ^^ twice hardline + +let codegen_node id ctyp = + ksprintf string "struct node_%s {\n %s hd;\n struct node_%s *tl;\n};\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id) + ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id) + +let codegen_list_init id = + ksprintf string "static void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id) + +let codegen_list_clear id ctyp = + ksprintf string "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id) + ^^ ksprintf string " if (*rop == NULL) return;" + ^^ (if is_stack_ctyp ctyp then empty + else ksprintf string " KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) + ^^ ksprintf string " KILL(%s)(&(*rop)->tl);\n" (sgen_id id) + ^^ string " sail_free(*rop);" + ^^ string "}" + +let codegen_list_recreate id = + ksprintf string "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id) + +let codegen_list_set id ctyp = + ksprintf string "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ string " if (op == NULL) { *rop = NULL; return; };\n" + ^^ ksprintf string " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id) + ^^ (if is_stack_ctyp ctyp then + string " (*rop)->hd = op->hd;\n" + else + ksprintf string " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp) + ^^ ksprintf string " COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp)) + ^^ ksprintf string " internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id) + ^^ string "}" + ^^ twice hardline + ^^ ksprintf string "static void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ ksprintf string " KILL(%s)(rop);\n" (sgen_id id) + ^^ ksprintf string " internal_set_%s(rop, op);\n" (sgen_id id) + ^^ string "}" + +let codegen_cons id ctyp = + let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in + ksprintf string "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id) + ^^ ksprintf string " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id) + ^^ (if is_stack_ctyp ctyp then + string " (*rop)->hd = x;\n" + else + ksprintf string " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp) + ^^ ksprintf string " COPY(%s)(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp)) + ^^ string " (*rop)->tl = xs;\n" + ^^ string "}" + +let codegen_pick id ctyp = + if is_stack_ctyp ctyp then + ksprintf string "static %s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id) + else + ksprintf string "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) + +let codegen_list_equal id ctyp = + ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ ksprintf string " if (op1 == NULL && op2 == NULL) { return true; };\n" + ^^ ksprintf string " if (op1 == NULL || op2 == NULL) { return false; };\n" + ^^ ksprintf string " return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id) + ^^ string "}" + +let codegen_list_undefined id ctyp = + ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp) + ^^ ksprintf string " *rop = NULL;\n" + ^^ string "}" + +let codegen_list ctx ctyp = + let id = mk_id (string_of_ctyp (CT_list ctyp)) in + if IdSet.mem id !generated then ( + (empty, empty) + ) else ( + generated := IdSet.add id !generated; + let header = codegen_list_header id in + let body = + codegen_node id ctyp ^^ twice hardline + ^^ codegen_list_init id ^^ twice hardline + ^^ codegen_list_clear id ctyp ^^ twice hardline + ^^ codegen_list_recreate id ^^ twice hardline + ^^ codegen_list_set id ctyp ^^ twice hardline + ^^ codegen_cons id ctyp ^^ twice hardline + ^^ codegen_pick id ctyp ^^ twice hardline + ^^ codegen_list_equal id ctyp ^^ twice hardline + ^^ codegen_list_undefined id ctyp + in + (header, body) + ) + +(* Generate functions for working with non-bit vectors of some specific type. *) +let codegen_vector_header ctx id (direction, ctyp) = + let vector_typedef = + string (Printf.sprintf "struct %s {\n size_t len;\n %s *data;\n};\n" (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id)) + in + vector_typedef ^^ twice hardline + +let codegen_vector_body ctx id (direction, ctyp) = + let vector_init = + string (Printf.sprintf "static void CREATE(%s)(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id)) + in + let vector_set = + string (Printf.sprintf "static void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id)) + ^^ string " rop->len = op.len;\n" + ^^ string (Printf.sprintf " rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string " for (int i = 0; i < op.len; i++) {\n" + ^^ string (if is_stack_ctyp ctyp then + " (rop->data)[i] = op.data[i];\n" + else + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + let vector_clear = + string (Printf.sprintf "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)) + ^^ (if is_stack_ctyp ctyp then empty + else + string " for (int i = 0; i < (rop->len); i++) {\n" + ^^ string (Printf.sprintf " KILL(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n") + ^^ string " if (rop->data != NULL) sail_free(rop->data);\n" + ^^ string "}" + in + let vector_update = + string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, sail_int n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string " int m = sail_int_get_ui(n);\n" + ^^ string " if (rop->data == op.data) {\n" + ^^ string (if is_stack_ctyp ctyp then + " rop->data[m] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string " } else {\n" + ^^ string (Printf.sprintf " COPY(%s)(rop, op);\n" (sgen_id id)) + ^^ string (if is_stack_ctyp ctyp then + " rop->data[m] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + let internal_vector_update = + string (Printf.sprintf "static void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (if is_stack_ctyp ctyp then + " rop->data[n] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string "}" + in + let vector_access = + if is_stack_ctyp ctyp then + string (Printf.sprintf "static %s vector_access_%s(%s op, sail_int n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id)) + ^^ string " int m = sail_int_get_ui(n);\n" + ^^ string " return op.data[m];\n" + ^^ string "}" + else + string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, sail_int n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) + ^^ string " int m = sail_int_get_ui(n);\n" + ^^ string (Printf.sprintf " COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp)) + ^^ string "}" + in + let internal_vector_init = + string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id)) + ^^ string " rop->len = len;\n" + ^^ string (Printf.sprintf " rop->data = sail_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_name ctyp)) + ^^ string " }\n" + else empty) + ^^ string "}" + in + let vector_undefined = + string (Printf.sprintf "static void undefined_vector_%s(%s *rop, sail_int len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf " rop->len = sail_int_get_ui(len);\n") + ^^ string (Printf.sprintf " rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string " for (int i = 0; i < (rop->len); i++) {\n" + ^^ string (if is_stack_ctyp ctyp then + " (rop->data)[i] = elem;\n" + else + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + vector_init ^^ twice hardline + ^^ vector_clear ^^ twice hardline + ^^ vector_undefined ^^ twice hardline + ^^ vector_access ^^ twice hardline + ^^ vector_set ^^ twice hardline + ^^ vector_update ^^ twice hardline + ^^ internal_vector_update ^^ twice hardline + ^^ internal_vector_init ^^ twice hardline + +let codegen_vector ctx (direction, ctyp) = + let id = mk_id (string_of_ctyp (CT_vector (direction, ctyp))) in + if IdSet.mem id !generated then ( + empty, empty + ) else ( + generated := IdSet.add id !generated; + codegen_vector_header ctx id (direction, ctyp), + codegen_vector_body ctx id (direction, ctyp) + ) + +(**************************************************************************) +(* Code generation for definitions *) +(**************************************************************************) + +(** To keep things neat we use GCC's local labels extension to limit + the scope of labels. We do this by iterating over all the blocks + and adding a __label__ declaration with all the labels local to + that block. + + See https://gcc.gnu.org/onlinedocs/gcc/Local-Labels.html **) +let add_local_labels' instrs = + let is_label (I_aux (instr, _)) = + match instr with + | I_label str -> [str] + | _ -> [] + in + let labels = List.concat (List.map is_label instrs) in + let local_label_decl = iraw ("__label__ " ^ String.concat ", " labels ^ ";\n") in + if labels = [] then + instrs + else + local_label_decl :: instrs + +let is_decl = function + | I_aux (I_decl _, _) -> true + | _ -> false + +let codegen_decl = function + | I_aux (I_decl (ctyp, id), _) -> + string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_name id)) + | _ -> assert false + +let codegen_alloc = function + | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty + | I_aux (I_decl (ctyp, id), _) -> + string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)) + | _ -> assert false + +let add_local_labels instrs = + match map_instrs add_local_labels' (iblock instrs) with + | I_aux (I_block instrs, _) -> instrs + | _ -> assert false + +let codegen_def_header ctx = function + | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> + if Env.is_extern id ctx.tc_env "c" then + empty + else if is_stack_ctyp ret_ctyp then + ksprintf string "%s %s(%s%s);" + (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps) + ^^ twice hardline + else + ksprintf string "void %s(%s%s *rop, %s);" + (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps) + ^^ twice hardline + + | CDEF_type ctype_def -> + codegen_type_def_header ctype_def + + | _ -> empty + +let codegen_def_body ctx = function + | CDEF_reg_dec _ -> empty + + | CDEF_spec _ -> empty + + | CDEF_fundef (id, ret_arg, args, instrs) as def -> + let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with + | Some vs -> vs + | None -> + Reporting.unreachable (id_loc id) __POS__ ("No valspec found for " ^ string_of_id id) + in + + (* Check that the function has the correct arity at this point. *) + if List.length arg_ctyps <> List.length args then + Reporting.unreachable (id_loc id) __POS__ + ("function arguments " + ^ Util.string_of_list ", " string_of_id args + ^ " matched against type " + ^ Util.string_of_list ", " string_of_ctyp arg_ctyps) + else (); + + let instrs = add_local_labels instrs in + let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in + let function_header = + match ret_arg with + | None -> + assert (is_stack_ctyp ret_ctyp); + string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline + | Some gs -> + assert (not (is_stack_ctyp ret_ctyp)); + string "void" ^^ space ^^ codegen_function_id id + ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) + ^^ hardline + in + function_header + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline + ^^ string "}" + ^^ twice hardline + + | CDEF_type ctype_def -> + codegen_type_def_body ctx ctype_def + + | CDEF_startup (id, instrs) -> + let startup_header = string (Printf.sprintf "void startup_%s(void)" (sgen_function_id id)) in + separate_map hardline codegen_decl instrs + ^^ twice hardline + ^^ startup_header ^^ hardline + ^^ string "{" + ^^ jump 0 2 (separate_map hardline codegen_alloc instrs) ^^ hardline + ^^ string "}" + + | CDEF_finish (id, instrs) -> + let finish_header = string (Printf.sprintf "void finish_%s(void)" (sgen_function_id id)) in + separate_map hardline codegen_decl (List.filter is_decl instrs) + ^^ twice hardline + ^^ finish_header ^^ hardline + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline + ^^ string "}" + + | CDEF_let (number, bindings, instrs) -> + let instrs = add_local_labels instrs in + let setup = + List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (global id)]) bindings) + in + let cleanup = + List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (global id)]) bindings) + in + hardline ^^ string (Printf.sprintf "void sail_create_letbind_%d(sail_state *state) " number) + ^^ string "{" + ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline + ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") { ctx with no_raw = true }) instrs) ^^ hardline + ^^ string "}" + ^^ hardline ^^ string (Printf.sprintf "void sail_kill_letbind_%d(sail_state *state) " number) + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) cleanup) ^^ hardline + ^^ string "}" + ^^ twice hardline + +(** As we generate C we need to generate specialized version of tuple, + list, and vector type. These must be generated in the correct + order. The ctyp_dependencies function generates a list of + c_gen_typs in the order they must be generated. Types may be + repeated in ctyp_dependencies so it's up to the code-generator not + to repeat definitions pointlessly (using the !generated variable) + *) +type c_gen_typ = + | CTG_tup of ctyp list + | CTG_list of ctyp + | CTG_vector of bool * ctyp + +let rec ctyp_dependencies = function + | CT_tup ctyps -> List.concat (List.map ctyp_dependencies ctyps) @ [CTG_tup ctyps] + | CT_list ctyp -> ctyp_dependencies ctyp @ [CTG_list ctyp] + | CT_vector (direction, ctyp) | CT_fvector (_, direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)] + | 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_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly | CT_constant _ -> [] + +let codegen_ctg ctx = function + | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp) + | CTG_tup ctyps -> codegen_tup ctx ctyps + | CTG_list ctyp -> codegen_list ctx ctyp + +(** When we generate code for a definition, we need to first generate + any auxillary type definitions that are required. *) +let codegen_def ctx def = + let ctyps = cdef_ctyps def |> CTSet.elements in + (* We should have erased any polymorphism introduced by variants at this point! *) + if List.exists is_polymorphic ctyps then + let polymorphic_ctyps = List.filter is_polymorphic ctyps in + Reporting.unreachable Parse_ast.Unknown __POS__ + (sprintf "Found polymorphic types:\n%s\nwhile generating definition." + (Util.string_of_list "\n" string_of_ctyp polymorphic_ctyps)) + else + let deps = List.concat (List.map ctyp_dependencies ctyps) in + let deps_header, deps_body = List.map (codegen_ctg ctx) deps |> List.split in + concat deps_header ^^ codegen_def_header ctx def, + concat deps_body ^^ codegen_def_body ctx def + +let codegen_state_struct_def ctx = function + | CDEF_reg_dec (id, ctyp, _) -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline + + | CDEF_let (_, [], _) -> empty + | CDEF_let (_, bindings, _) -> + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings + ^^ hardline + + | _ -> empty + +let codegen_state_struct ctx cdefs = + string "struct sail_state {" ^^ hardline + ^^ concat_map (codegen_state_struct_def ctx) cdefs + ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then ( + empty + ) else ( + string " // exception handling support" ^^ hardline + ^^ ksprintf string " struct %s *current_exception;" (sgen_id (mk_id "exception")) ^^ hardline + ^^ string " bool have_exception;" ^^ hardline + ^^ string " sail_string *throw_location;" ^^ hardline + )) + ^^ string "};" + +let is_cdef_startup = function + | CDEF_startup _ -> true + | _ -> false + +let sgen_startup = function + | CDEF_startup (id, _) -> + Printf.sprintf " startup_%s();" (sgen_id id) + | _ -> assert false + +let sgen_instr id ctx instr = + Pretty_print_sail.to_string (codegen_instr id ctx instr) + +let is_cdef_finish = function + | CDEF_startup _ -> true + | _ -> false + +let sgen_finish = function + | CDEF_startup (id, _) -> + Printf.sprintf " finish_%s();" (sgen_id id) + | _ -> assert false + +let rec get_recursive_functions (Defs defs) = + match defs with + | DEF_internal_mutrec fundefs :: defs -> + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + + | (DEF_fundef fdef as def) :: defs -> + let open Rewriter in + let ids = ref IdSet.empty in + let collect_funcalls e_aux annot = + match e_aux with + | E_app (id, args) -> (ids := IdSet.add id !ids; E_aux (e_aux, annot)) + | _ -> E_aux (e_aux, annot) + in + let map_exp = { + id_exp_alg with + e_aux = (fun (e_aux, annot) -> collect_funcalls e_aux annot) + } in + let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in + let _ = rewrite_def map_defs def in + if IdSet.mem (id_of_fundef fdef) !ids then + IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs)) + else + get_recursive_functions (Defs defs) + + | _ :: defs -> get_recursive_functions (Defs defs) + | [] -> IdSet.empty + +let codegen_output file_name docs = + let chan = open_out file_name in + output_string chan (Pretty_print_sail.to_string docs); + flush chan; + close_out chan + +let codegen ctx output_name cdefs = + let docs_header, docs_body = List.map (codegen_def ctx) cdefs |> List.split in + + let state = codegen_state_struct ctx cdefs in + + let stdlib_headers = + string "#include " ^^ hardline + ^^ string "#include " + in + let sail_headers = + string "#include \"sail.h\"" ^^ hardline + ^^ string "#include \"sail_failure.h\"" + in + + let register_init_clear (id, ctyp, instrs) = + if is_stack_ctyp ctyp then + List.map (sgen_instr (mk_id "reg") ctx) instrs, [] + else + [ Printf.sprintf " CREATE(%s)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ] + @ List.map (sgen_instr (mk_id "reg") ctx) instrs, + [ Printf.sprintf " KILL(%s)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ] + in + + let header = + stdlib_headers + ^^ hardline + ^^ sail_headers ^^ twice hardline + ^^ string "struct sail_state;" ^^ hardline + ^^ string "typedef struct sail_state sail_state;" + ^^ twice hardline + ^^ concat docs_header + ^^ state + ^^ twice hardline + ^^ string "void sail_initialize_state(sail_state *state);" + ^^ hardline + ^^ string "void sail_finalize_state(sail_state *state);" + ^^ hardline + in + + let regs = c_ast_registers cdefs in + + let letbind_initializers = + List.map (fun n -> Printf.sprintf " sail_create_letbind_%d(state);" n) (List.rev ctx.letbinds) + in + let letbind_finalizers = + List.map (fun n -> Printf.sprintf " sail_kill_letbind_%d(state);" n) ctx.letbinds + in + + let body = + ksprintf string "#include \"%s.h\"" output_name + ^^ twice hardline + ^^ concat docs_body + ^^ string "void sail_initialize_letbindings(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string letbind_initializers ^^ hardline + ^^ string "}" + ^^ twice hardline + ^^ string "void sail_finalize_letbindings(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string letbind_finalizers ^^ hardline + ^^ string "}" + ^^ twice hardline + ^^ string "void sail_initialize_state(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string (List.map (fun r -> fst (register_init_clear r)) regs |> List.concat) + ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then ( + empty + ) else ( + string " state->have_exception = false;" + ^^ ksprintf string " state->current_exception = sail_malloc(sizeof(struct %s));" + (sgen_id (mk_id "exception")) ^^ hardline + ^^ ksprintf string " CREATE(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline + ^^ string " state->throw_location = sail_malloc(sizeof(sail_string));" ^^ hardline + ^^ string " CREATE(sail_string)(state->throw_location);" + )) + ^^ hardline + ^^ string " sail_initialize_letbindings(state);" ^^ hardline + ^^ string "}" + ^^ twice hardline + ^^ string "void sail_finalize_state(sail_state *state) {" ^^ hardline + ^^ separate_map hardline string (List.map (fun r -> snd (register_init_clear r)) regs |> List.concat) + ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then ( + empty + ) else ( + ksprintf string " KILL(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline + ^^ string " sail_free(state->current_exception);" ^^ hardline + ^^ string " KILL(sail_string)(state->throw_location);" ^^ hardline + ^^ string " sail_free(state->throw_location);" + )) + ^^ hardline + ^^ string " sail_finalize_letbindings(state);" ^^ hardline + ^^ string "}" + ^^ hardline + in + + codegen_output (output_name ^ ".h") header; + codegen_output (output_name ^ ".c") body + +let emulator ctx output_name cdefs = + codegen ctx output_name cdefs; + + let preamble = separate hardline + ((if !opt_no_lib then [] else + [ string "#include \"sail.h\""; + string "#include \"sail_failure.h\"" ]) + @ (if !opt_no_rts then [] else + [ string "#include \"rts.h\""; + string "#include \"elf.h\"" ]) + @ [ ksprintf string "#include \"%s.h\"" output_name ] + @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) [] (*c_includes*))) + in + + let startup cdefs = + List.map sgen_startup (List.filter is_cdef_startup cdefs) + in + let finish cdefs = + List.map sgen_finish (List.filter is_cdef_finish cdefs) + in + + let regs = c_ast_registers cdefs in + + let model_init = separate hardline (List.map string + ( [ "void model_init(sail_state *state)"; + "{"; + " sail_initialize_state(state);"; + " setup_rts();" ] + @ startup cdefs + @ (if regs = [] then [] else [ Printf.sprintf " %s(state, UNIT);" (sgen_function_id (mk_id "initialize_registers")) ]) + @ [ "}" ] )) + in + + let model_fini = separate hardline (List.map string + ( [ "void model_fini(sail_state *state)"; + "{" ] + @ finish cdefs + @ [ " cleanup_rts();"; + " sail_finalize_state(state);"; + "}" ])) + in + + let model_default_main = separate hardline (List.map string + ([ "int model_main(int argc, char *argv[])"; + "{"; + " sail_state state;"; + " model_init(&state);"; + " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; + sprintf " %s(&state, UNIT);" (sgen_function_id (mk_id "main")) ] + @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else + [ " if (state.have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *state.throw_location);}" ]) + @ [ " model_fini(&state);" ] + @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else + [ " if (state.have_exception) {return(EXIT_FAILURE);}" ]) + @ [ " return EXIT_SUCCESS;"; + "}" ])) + in + + let model_main = separate hardline (if (!opt_no_main) then [] else List.map string + [ "int main(int argc, char *argv[])"; + "{"; + " return model_main(argc, argv);"; + "}" ] ) + in + + let hlhl = hardline ^^ hardline in + let emu = + preamble ^^ hlhl + ^^ (if not !opt_no_rts then + model_init ^^ hlhl + ^^ model_fini ^^ hlhl + ^^ model_default_main ^^ hlhl + else + empty) + ^^ model_main ^^ hardline + in + codegen_output (output_name ^ "_emu.c") emu + +end diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 34477967..1cd7d82a 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -190,6 +190,12 @@ let rec chunkify n xs = | xs, [] -> [xs] | xs, ys -> xs :: chunkify n ys +let name_or_global ctx id = + if Env.is_register id ctx.local_env || IdSet.mem id (Env.get_toplevel_lets ctx.local_env) then + global id + else + name id + let rec compile_aval l ctx = function | AV_cval (cval, typ) -> let ctyp = cval_ctyp cval in @@ -201,13 +207,11 @@ let rec compile_aval l ctx = function [], cval, [] | AV_id (id, typ) -> - begin - try - let _, ctyp = Bindings.find id ctx.locals in - [], V_id (name id, ctyp), [] - with - | Not_found -> - [], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), [] + begin match Bindings.find_opt id ctx.locals with + | Some (_, ctyp) -> + [], V_id (name id, ctyp), [] + | None -> + [], V_id (name_or_global ctx id, ctyp_of_typ ctx (lvar_typ typ)), [] end | AV_ref (id, typ) -> @@ -520,7 +524,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = | AP_global (pid, typ) -> let global_ctyp = ctyp_of_typ ctx typ in - [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx + [icopy l (CL_id (global pid, global_ctyp)) cval], [], ctx | AP_id (pid, _) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with @@ -778,7 +782,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup - @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), (field_id, []))) cval] + @ [icopy l (CL_field (CL_id (name_or_global ctx id, ctyp_of_typ ctx typ), (field_id, []))) cval] @ field_cleanup in List.concat (List.map compile_fields (Bindings.bindings fields)), @@ -792,7 +796,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | None -> ctyp_of_typ ctx assign_typ in let setup, call, cleanup = compile_aexp ctx aexp in - setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup + setup @ [call (CL_id (name_or_global ctx id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup | AE_write_ref (id, assign_typ, aexp) -> let assign_ctyp = @@ -801,7 +805,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | None -> ctyp_of_typ ctx assign_typ in let setup, call, cleanup = compile_aexp ctx aexp in - setup @ [call (CL_addr (CL_id (name id, assign_ctyp)))], (fun clexp -> icopy l clexp unit_cval), cleanup + setup @ [call (CL_addr (CL_id (name_or_global ctx id, assign_ctyp)))], (fun clexp -> icopy l clexp unit_cval), cleanup | AE_block (aexps, aexp, _) -> let block = compile_block ctx aexps in @@ -1302,7 +1306,7 @@ and compile_def' n total ctx = function | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in + let instrs = setup @ [call (CL_id (global id, ctyp_of_typ ctx typ))] @ cleanup in [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx | DEF_reg_dec (DEC_aux (_, (l, _))) -> diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index 9014d8f7..a642f29e 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -65,7 +65,16 @@ val optimize_aarch64_fast_struct : bool ref useful for debugging C but we want to turn it off for SMT generation where we can't use strings *) val opt_track_throw : bool ref - + +(** (WIP) [opt_memo_cache] will store the compiled function + definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum + of the original function to be compiled. Enabled using the -memo + flag. Uses Marshal so it's quite picky about the exact version of + the Sail version. This cache can obviously become stale if the Sail + changes - it'll load an old version compiled without said + changes. *) +val opt_memo_cache : bool ref + (** {2 Jib context} *) (** Dynamic context for compiling Sail to Jib. We need to pass a diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml index 4bf726aa..d30fe183 100644 --- a/src/jib/jib_ir.ml +++ b/src/jib/jib_ir.ml @@ -62,7 +62,7 @@ module StringMap = Map.Make(String) let string_of_name = let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in function - | Name (id, n) -> zencode_id id ^ ssa_num n + | Name (id, n) | Global (id, n) -> zencode_id id ^ ssa_num n | Have_exception n -> "have_exception" ^ ssa_num n | Return n -> diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml index e0f3bf0d..f156a040 100644 --- a/src/jib/jib_optimize.ml +++ b/src/jib/jib_optimize.ml @@ -76,6 +76,7 @@ let optimize_unit instrs = in let non_pointless_copy (I_aux (aux, annot)) = match aux with + | I_decl (CT_unit, _) -> false | I_copy (CL_void, _) -> false | _ -> true in @@ -245,6 +246,7 @@ let rec find_function fid = function let ssa_name i = function | Name (id, _) -> Name (id, i) + | Global (id, _) -> Global (id, i) | Have_exception _ -> Have_exception i | Current_exception _ -> Current_exception i | Throw_location _ -> Throw_location i diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 47f6ee49..b662ef41 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -343,7 +343,7 @@ let rec smt_cval ctx cval = | _ -> match cval with | V_lit (vl, ctyp) -> smt_value ctx vl ctyp - | V_id (Name (id, _) as ssa_id, _) -> + | V_id ((Name (id, _) | Global (id, _)) as ssa_id, _) -> begin match Type_check.Env.lookup_id id ctx.tc_env with | Enum _ -> Enum (zencode_id id) | _ when Bindings.mem id ctx.shared -> Shared (zencode_id id) @@ -1384,8 +1384,8 @@ let rec generate_ctype_defs ctx = function | [] -> [] let rec generate_reg_decs ctx inits = function - | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits)-> - Declare_const (zencode_name (Name (id, 0)), smt_ctyp ctx ctyp) + | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Global (id, 0)) inits)-> + Declare_const (zencode_name (Global (id, 0)), smt_ctyp ctx ctyp) :: generate_reg_decs ctx inits cdefs | _ :: cdefs -> generate_reg_decs ctx inits cdefs | [] -> [] @@ -1876,7 +1876,7 @@ let smt_instr ctx = | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) -> begin match id with - | Name (id, _) when IdSet.mem id ctx.preserved -> + | Name (id, _) | Global (id, _) when IdSet.mem id ctx.preserved -> [preserve_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] | _ -> @@ -1935,7 +1935,7 @@ let rec find_function lets id = function | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 -> lets, Some (heap_return, args, body) | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in find_function (lets @ vars @ setup) id cdefs; | _ :: cdefs -> find_function lets id cdefs @@ -2121,7 +2121,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_write_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - ifuncall (CL_id (name r, reg_ctyp)) function_id args; + ifuncall (CL_id (global r, reg_ctyp)) function_id args; igoto end_label; ilabel next_label] in @@ -2145,7 +2145,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_deref_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label; - icopy l clexp (V_id (name r, reg_ctyp)); + icopy l clexp (V_id (global r, reg_ctyp)); igoto end_label; ilabel next_label] in @@ -2167,7 +2167,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_write_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - icopy l (CL_id (name r, reg_ctyp)) cval; + icopy l (CL_id (global r, reg_ctyp)) cval; igoto end_label; ilabel next_label] in @@ -2301,7 +2301,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function let rec smt_cdefs props lets name_file ctx ast = function | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs; | cdef :: cdefs -> smt_cdef props lets name_file ctx ast cdef; diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index fe3238a4..f9777f9e 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -502,6 +502,7 @@ let rename_variables graph root children = let ssa_name i = function | Name (id, _) -> Name (id, i) + | Global (id, _) -> Global (id, i) | Have_exception _ -> Have_exception i | Current_exception _ -> Current_exception i | Throw_location _ -> Throw_location i diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 9b06c7be..88f09bcf 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -144,11 +144,16 @@ module Name = struct | Name (x, n), Name (y, m) -> let c1 = Id.compare x y in if c1 = 0 then compare n m else c1 + | Global (x, n), Global (y, m) -> + let c1 = Id.compare x y in + if c1 = 0 then compare n m else c1 | Have_exception n, Have_exception m -> compare n m | Current_exception n, Current_exception m -> compare n m | Return n, Return m -> compare n m | Name _, _ -> 1 | _, Name _ -> -1 + | Global _, _ -> 1 + | _, Global _ -> -1 | Have_exception _, _ -> 1 | _, Have_exception _ -> -1 | Current_exception _, _ -> 1 @@ -166,6 +171,7 @@ let throw_location = Throw_location (-1) let return = Return (-1) let name id = Name (id, -1) +let global id = Global (id, -1) let rec cval_rename from_id to_id = function | V_id (id, ctyp) when Name.compare id from_id = 0 -> V_id (to_id, ctyp) @@ -261,7 +267,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) = let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true) = let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in function - | Name (id, n) -> + | Name (id, n) | Global (id, n) -> (if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n | Have_exception n -> "have_exception" ^ ssa_num n diff --git a/src/rewrites.ml b/src/rewrites.ml index e622d620..89f67d87 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5059,6 +5059,7 @@ let rewrites_target tgt = | "lem" -> rewrites_lem | "ocaml" -> rewrites_ocaml | "c" -> rewrites_c + | "c2" -> rewrites_c | "ir" -> rewrites_c @ [("properties", [])] | "smt" -> rewrites_c @ [("properties", [])] | "sail" -> [] diff --git a/src/sail.ml b/src/sail.ml index 64e4f8c6..296bfdac 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -185,6 +185,9 @@ let options = Arg.align ([ ( "-c", Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); + ( "-c2", + Arg.Tuple [set_target "c2"; Arg.Set Initial_check.opt_undefined_gen], + " output a C translated version of the input"); ( "-c_include", Arg.String (fun i -> opt_includes_c := i::!opt_includes_c), " provide additional include for C output"); @@ -304,7 +307,7 @@ let options = Arg.align ([ Arg.Clear opt_memo_z3, " do not memoize calls to z3 (default)"); ( "-memo", - Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache], + Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set Jib_compile.opt_memo_cache], " memoize calls to z3, and intermediate compilation results"); ( "-have_feature", Arg.String (fun symbol -> opt_have_feature := Some symbol), @@ -474,6 +477,27 @@ let target name out_name ast type_envs = flush output_chan; if close then close_out output_chan else () + | Some "c2" -> + let module StringMap = Map.Make(String) in + let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in + let ast_c, type_envs = + if !opt_specialize_c then + Specialize.(specialize_passes 2 int_specialization type_envs ast_c) + else + ast_c, type_envs + in + let output_name = match !opt_file_out with Some f -> f | None -> "out" in + Reporting.opt_warnings := true; + let codegen ctx cdefs = + let module Codegen = + C_codegen.Make( + struct let opts = C_codegen.default_options cdefs end + ) + in + Codegen.emulator ctx output_name cdefs + in + C_backend.compile_ast_clib type_envs ast_c codegen; + | Some "ir" -> let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *) -- cgit v1.2.3 From 81516c8ad7c30adb3d52741ad6a7c68d4436ec35 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 12 May 2020 15:41:23 +0100 Subject: Support for user-defined state and headers in new codegen All the code-generator options can now be controlled via a json configuration file Extra fields can be added to the sail_state struct using a codegen.extra_state key in the configuration json for the code generator If primitives want to modify the state they can be specified via codegen.state_primops To import such state, codegen.extra_headers can be used to add user-defined headers to the generated .h file --- src/_tags | 4 +- src/jib/c_codegen.ml | 168 +++++++++++++++++++++++++++++++++++++-------------- src/reporting.ml | 4 +- src/reporting.mli | 3 + src/sail.ml | 19 +++++- 5 files changed, 148 insertions(+), 50 deletions(-) (limited to 'src') diff --git a/src/_tags b/src/_tags index ce4d0270..dc3d0c6e 100644 --- a/src/_tags +++ b/src/_tags @@ -2,10 +2,12 @@ true: -traverse, debug, use_menhir <**/parser.ml>: bin_annot, annot <**/*.ml> and not <**/parser.ml>: bin_annot, annot -: package(zarith), package(linksem), package(lem), package(omd), package(base64), package(pprint) +: package(zarith), package(linksem), package(lem), package(omd), package(base64), package(pprint), package(yojson) : package(zarith), package(linenoise), package(linksem), package(lem), package(omd), package(base64), package(yojson), package(pprint) : package(linenoise), package(yojson) +: package(yojson) +: package(yojson) : package(linksem) : package(omd) <**/*.m{l,li}>: package(lem), package(base64), package(pprint) diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index 6aa0060c..44d24367 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -59,12 +59,10 @@ open Printf open Value2 module StringMap = Map.Make(String) +module StringSet = Set.Make(String) module Big_int = Nat_big_num - -let opt_no_main = ref false -let opt_no_lib = ref false -let opt_no_rts = ref false - +module Json = Yojson.Basic + let (gensym, _) = symbol_generator "c2" let ngensym () = name (gensym ()) @@ -101,15 +99,35 @@ let rec is_stack_ctyp ctyp = match ctyp with let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true)) type codegen_options = { + (** Rewrites a Sail identifier into a user-specified name in the generated C *) exports : string Bindings.t; + (** Rewrites a generated symbol after name-mangling has ocurred *) exports_mangled : string StringMap.t; + (** Extra headers to include in the generated .h file *) + extra_headers : string list; + (** Extra lines that are included in the sail_state struct. Used + to add user-specified state to the structs, which can then be + passed to primops in state_primops *) + extra_state : string list; + (** Primitives in this set will be passed a pointer to the + sail_state struct *) + state_primops : StringSet.t; } +let initial_options = { + exports = Bindings.empty; + exports_mangled = StringMap.empty; + extra_headers = []; + extra_state = []; + state_primops = StringSet.empty; + } + let add_export opts id = { opts with exports = Bindings.add id (string_of_id id) opts.exports } let add_custom_export opts id into = { opts with exports = Bindings.add id into opts.exports } -let add_mangled_rename opts (from, into) = { opts with exports_mangled = StringMap.add from into opts.exports_mangled } +let add_mangled_rename opts (from, into) = + { opts with exports_mangled = StringMap.add from into opts.exports_mangled } let add_export_uid opts (id, ctyps) = match ctyps with @@ -128,18 +146,74 @@ let cdef_initial_options opts = function | CDEF_reg_dec (id, _, _) -> add_export opts id | CDEF_let (_, bindings, _) -> List.fold_left (fun opts (id, _) -> add_export opts id) opts bindings | _ -> opts - -let initial_options = { - exports = Bindings.empty; - exports_mangled = StringMap.empty; - } let default_options cdefs = let opts = List.fold_left cdef_initial_options initial_options cdefs in let opts = add_export opts (mk_id "initialize_registers") in let opts = add_custom_export opts (mk_id "main") "sail_main" in List.fold_left add_mangled_rename opts (List.init 9 (fun n -> "ztup" ^ string_of_int n, "tuple_" ^ string_of_int n)) - + +let options_from_json json cdefs = + let open Json.Util in + let bad_key k json = + raise (Reporting.err_general Parse_ast.Unknown + (sprintf "Invalid %s key in codegen json configuration: %s" k (Json.to_string json))) + in + let opts = match member "default_exports" json with + | `Bool true -> default_options cdefs + | `Bool false -> initial_options + | `Null -> + Reporting.simple_warn "No default_exports key in codegen json configuration"; + initial_options + | json -> bad_key "default_exports" json + in + let process_exports opts = function + | `List [`String from; `String into] -> add_custom_export opts (mk_id from) into + | `String str -> add_export opts (mk_id str) + | json -> bad_key "exports" json + in + let opts = match member "exports" json with + | `List exports -> List.fold_left process_exports opts exports + | `Null -> + Reporting.simple_warn "No exports key in codegen json configuration"; + opts + | json -> bad_key "exports" json + in + let process_exports_mangled opts = function + | `List [`String from; `String into] -> add_mangled_rename opts (from, into) + | json -> bad_key "exports_mangled" json + in + let opts = match member "exports_mangled" json with + | `List exports -> List.fold_left process_exports_mangled opts exports + | `Null -> + Reporting.simple_warn "No exports_mangled key in codegen json configuration"; + opts + | json -> bad_key "exports_mangled" json + in + let process_extra_header opts = function + | `String header -> { opts with extra_headers = header :: opts.extra_headers } + | json -> bad_key "extra_headers" json + in + let opts = match member "extra_headers" json with + | `List headers -> List.fold_left process_extra_header opts headers + | `Null -> + Reporting.simple_warn "No extra_headers key in codegen json configuration"; + opts + | json -> bad_key "extra_headers" json + in + let process_extra_state opts = function + | `String member -> { opts with extra_state = member :: opts.extra_state } + | json -> bad_key "extra_state" json + in + let opts = match member "extra_state" json with + | `List members -> List.fold_left process_extra_state opts members + | `Null -> + Reporting.simple_warn "No extra_state key in codegen json configuration"; + opts + | json -> bad_key "extra_state" json + in + opts + module type Config = sig val opts : codegen_options end @@ -195,7 +269,7 @@ let rec sgen_ctyp = function | CT_constant _ -> "int64_t" | CT_lint -> "sail_int" | CT_lbits _ -> "lbits" - | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup) + | CT_tup _ as tup -> "struct " ^ mangle ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> "struct " ^ sgen_id id | CT_enum (id, _) -> "enum " ^ sgen_id id | CT_variant (id, _) -> "struct " ^ sgen_id id @@ -217,7 +291,7 @@ let rec sgen_ctyp_name = function | CT_constant _ -> "mach_int" | CT_lint -> "sail_int" | CT_lbits _ -> "lbits" - | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup) + | CT_tup _ as tup -> mangle ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> sgen_id id | CT_enum (id, _) -> sgen_id id | CT_variant (id, _) -> sgen_id id @@ -565,14 +639,19 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | I_funcall (x, special_extern, f, args) -> let c_args = Util.string_of_list ", " (sgen_cval ctx) args in let ctyp = clexp_ctyp x in - let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || special_extern in - let fname = + let fname, is_extern = if special_extern then - string_of_id (fst f) + (string_of_id (fst f), true) else if Env.is_extern (fst f) ctx.tc_env "c" then - Env.get_extern (fst f) ctx.tc_env "c" + (Env.get_extern (fst f) ctx.tc_env "c", true) else - sgen_function_uid f + (sgen_function_uid f, false) + in + let sail_state_arg = + if is_extern && StringSet.mem fname C.opts.state_primops then + "sail_state *state, " + else + "" in let fname = match fname, ctyp with @@ -631,9 +710,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = ksprintf string " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure ctx x) c_args else if is_stack_ctyp ctyp then - ksprintf string " %s = %s(%s%s);" (sgen_clexp_pure ctx x) fname (extra_arguments is_extern) c_args + ksprintf string " %s = %s(%s%s%s);" (sgen_clexp_pure ctx x) fname sail_state_arg (extra_arguments is_extern) c_args else - ksprintf string " %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp ctx x) c_args + ksprintf string " %s(%s%s%s, %s);" fname sail_state_arg (extra_arguments is_extern) (sgen_clexp ctx x) c_args | I_clear (ctyp, id) when is_stack_ctyp ctyp -> empty @@ -1385,6 +1464,7 @@ let codegen_state_struct ctx cdefs = ^^ string " bool have_exception;" ^^ hardline ^^ string " sail_string *throw_location;" ^^ hardline )) + ^^ separate_map hardline (fun str -> string (" " ^ str)) C.opts.extra_state ^^ hardline ^^ string "};" let is_cdef_startup = function @@ -1465,9 +1545,9 @@ let codegen ctx output_name cdefs = in let header = - stdlib_headers - ^^ hardline - ^^ sail_headers ^^ twice hardline + stdlib_headers ^^ hardline + ^^ sail_headers ^^ hardline + ^^ concat_map (fun str -> string str ^^ hardline) C.opts.extra_headers ^^ hardline ^^ string "struct sail_state;" ^^ hardline ^^ string "typedef struct sail_state sail_state;" ^^ twice hardline @@ -1539,15 +1619,13 @@ let codegen ctx output_name cdefs = let emulator ctx output_name cdefs = codegen ctx output_name cdefs; - let preamble = separate hardline - ((if !opt_no_lib then [] else - [ string "#include \"sail.h\""; - string "#include \"sail_failure.h\"" ]) - @ (if !opt_no_rts then [] else - [ string "#include \"rts.h\""; - string "#include \"elf.h\"" ]) - @ [ ksprintf string "#include \"%s.h\"" output_name ] - @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) [] (*c_includes*))) + let headers = separate hardline + ([ string "#include \"sail.h\""; + string "#include \"sail_failure.h\""; + string "#include \"rts.h\""; + string "#include \"elf.h\""; + ksprintf string "#include \"%s.h\"" output_name ] + @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) [] (*c_includes*))) in let startup cdefs = @@ -1560,7 +1638,7 @@ let emulator ctx output_name cdefs = let regs = c_ast_registers cdefs in let model_init = separate hardline (List.map string - ( [ "void model_init(sail_state *state)"; + ( [ "void model_initialize(sail_state *state)"; "{"; " sail_initialize_state(state);"; " setup_rts();" ] @@ -1570,7 +1648,7 @@ let emulator ctx output_name cdefs = in let model_fini = separate hardline (List.map string - ( [ "void model_fini(sail_state *state)"; + ( [ "void model_finalize(sail_state *state)"; "{" ] @ finish cdefs @ [ " cleanup_rts();"; @@ -1582,34 +1660,30 @@ let emulator ctx output_name cdefs = ([ "int model_main(int argc, char *argv[])"; "{"; " sail_state state;"; - " model_init(&state);"; + " model_initialize(&state);"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; sprintf " %s(&state, UNIT);" (sgen_function_id (mk_id "main")) ] @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else [ " if (state.have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *state.throw_location);}" ]) - @ [ " model_fini(&state);" ] + @ [ " model_finalize(&state);" ] @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else [ " if (state.have_exception) {return(EXIT_FAILURE);}" ]) @ [ " return EXIT_SUCCESS;"; "}" ])) in - let model_main = separate hardline (if (!opt_no_main) then [] else List.map string + let model_main = separate hardline (List.map string [ "int main(int argc, char *argv[])"; "{"; " return model_main(argc, argv);"; - "}" ] ) + "}" ]) in - let hlhl = hardline ^^ hardline in let emu = - preamble ^^ hlhl - ^^ (if not !opt_no_rts then - model_init ^^ hlhl - ^^ model_fini ^^ hlhl - ^^ model_default_main ^^ hlhl - else - empty) + headers ^^ twice hardline + ^^ model_init ^^ twice hardline + ^^ model_fini ^^ twice hardline + ^^ model_default_main ^^ twice hardline ^^ model_main ^^ hardline in codegen_output (output_name ^ "_emu.c") emu diff --git a/src/reporting.ml b/src/reporting.ml index d5e3003c..0029b902 100644 --- a/src/reporting.ml +++ b/src/reporting.ml @@ -179,7 +179,7 @@ let ignored_files = ref StringSet.empty let suppress_warnings_for_file f = ignored_files := StringSet.add f !ignored_files - + let warn str1 l str2 = if !opt_warnings then match simp_loc l with @@ -191,3 +191,5 @@ let warn str1 l str2 = | Some _ -> () else () + +let simple_warn str = warn str Parse_ast.Unknown "" diff --git a/src/reporting.mli b/src/reporting.mli index e0744c66..54875398 100644 --- a/src/reporting.mli +++ b/src/reporting.mli @@ -116,6 +116,9 @@ val print_error : error -> unit location, the second after. *) val warn : string -> Parse_ast.l -> string -> unit +(** Print a simple one-line warning without a location. *) +val simple_warn: string -> unit + (** Will suppress all warnings for a given file. Used by $suppress_warnings directive in process_file.ml *) val suppress_warnings_for_file : string -> unit diff --git a/src/sail.ml b/src/sail.ml index 296bfdac..8e89bbed 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -51,9 +51,11 @@ open Process_file module Big_int = Nat_big_num +module Json = Yojson.Basic let lib = ref ([] : string list) let opt_interactive_script : string option ref = ref None +let opt_config : Json.t option ref = ref None let opt_print_version = ref false let opt_target = ref None let opt_tofrominterp_output_dir : string option ref = ref None @@ -72,6 +74,13 @@ let opt_have_feature = ref None let set_target name = Arg.Unit (fun _ -> opt_target := Some name) +let load_json_config file = + try Json.from_file file with + | Yojson.Json_error desc | Sys_error desc -> + prerr_endline "Error when loading configuration file:"; + prerr_endline desc; + exit 1 + let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), @@ -101,6 +110,9 @@ let options = Arg.align ([ ( "-no_warn", Arg.Clear Reporting.opt_warnings, " do not print warnings"); + ( "-config", + Arg.String (fun file -> opt_config := Some (load_json_config file)), + " JSON configuration file"); ( "-tofrominterp", set_target "tofrominterp", " output OCaml functions to translate between shallow embedding and interpreter"); @@ -489,9 +501,14 @@ let target name out_name ast type_envs = let output_name = match !opt_file_out with Some f -> f | None -> "out" in Reporting.opt_warnings := true; let codegen ctx cdefs = + let open Json.Util in + let codegen_opts = match !opt_config with + | Some config -> C_codegen.options_from_json (member "codegen" config) cdefs + | None -> C_codegen.default_options cdefs + in let module Codegen = C_codegen.Make( - struct let opts = C_codegen.default_options cdefs end + struct let opts = codegen_opts end ) in Codegen.emulator ctx output_name cdefs -- cgit v1.2.3 From b8f9e2a078035cc8e797b1c7c0609f6a0c031a2c Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 12 May 2020 21:07:00 +0100 Subject: Add support for instrumenting generated C with branch coverage metrics Will call: void sail_branch_reached(int branch_id, char *source_file, int l1, int c1, int l2, int c2); on each branch caused by a match or if statement in the source code For each branch that is taken, will call: void sail_branch_taken(int branch_id, char *source_file, int l1, int c1, int l2, int c2) Every branch gets a unique identifier, and the functions are called with the source file location and line/character information for the start and end of each match case or then/else branch. sail_branch_reached is given the location info for the whole match statement. --- src/jib/anf.ml | 2 ++ src/jib/anf.mli | 4 +++- src/jib/c_backend.ml | 12 +++++----- src/jib/jib_compile.ml | 60 +++++++++++++++++++++++++++++++++++++++++++------ src/jib/jib_compile.mli | 2 ++ src/jib/jib_smt.ml | 1 + src/reporting.ml | 5 +++++ 7 files changed, 73 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 6bc447c0..7757cd9a 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -106,6 +106,8 @@ and 'a aval = | AV_record of ('a aval) Bindings.t * 'a | AV_cval of cval * 'a +let aexp_loc (AE_aux (_, _, l)) = l + (* Renaming variables in ANF expressions *) let rec apat_bindings (AP_aux (apat_aux, _, _)) = diff --git a/src/jib/anf.mli b/src/jib/anf.mli index d01fe146..b96766da 100644 --- a/src/jib/anf.mli +++ b/src/jib/anf.mli @@ -133,8 +133,10 @@ and 'a aval = counter to ensure uniqueness. This function resets that counter. *) val reset_anf_counter : unit -> unit +val aexp_loc : 'a aexp -> Parse_ast.l + (** {2 Functions for transforming ANF expressions} *) - + val aval_typ : typ aval -> typ val aexp_typ : typ aexp -> typ diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 829f4d37..c38749f3 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -165,11 +165,11 @@ let literal_to_fragment (L_aux (l_aux, _) as lit) = | _ -> None module C_config : Config = struct - -(** Convert a sail type into a C-type. This function can be quite - 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_smt is true (default) **) + + (** Convert a sail type into a C-type. This function can be quite + 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_smt is true (default) **) let rec convert_typ ctx typ = let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in match typ_aux with @@ -562,6 +562,7 @@ module C_config : Config = struct let ignore_64 = false let struct_value = false let use_real = false + let branch_coverage = false end (* When compiling to a C library, we want to do things slightly @@ -656,6 +657,7 @@ module Clib_config : Config = struct let ignore_64 = false let struct_value = false let use_real = false + let branch_coverage = false end (** Functions that have heap-allocated return types are implemented by diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 1cd7d82a..cd86840b 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -179,6 +179,7 @@ module type Config = sig val ignore_64 : bool val struct_value : bool val use_real : bool + val branch_coverage : bool end module Make(C: Config) = struct @@ -195,6 +196,45 @@ let name_or_global ctx id = global id else name id + +let coverage_branch_count = ref 0 + +let coverage_loc_args l = + match Reporting.simp_loc l with + | None -> + Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation"; + None + | Some (p1, p2) -> + Some (Printf.sprintf "\"%s\", %d, %d, %d, %d" + p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)) + +let coverage_branch_reached l = + let branch_id = !coverage_branch_count in + incr coverage_branch_count; + branch_id, + if C.branch_coverage then + begin match coverage_loc_args l with + | None -> + Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation"; + [] + | Some args -> + [iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)] + end + else + [] + +let append_into_block instrs instr = + match instrs with + | [] -> instr + | _ -> iblock (instrs @ [instr]) + +let coverage_branch_taken branch_id (AE_aux (_, _, l)) = + if not C.branch_coverage then + [] + else + match coverage_loc_args l with + | None -> [] + | Some args -> [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)] let rec compile_aval l ctx = function | AV_cval (cval, typ) -> @@ -628,6 +668,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_case (aval, cases, typ) -> let ctyp = ctyp_of_typ ctx typ in let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in + let branch_id, on_reached = coverage_branch_reached l in let case_return_id = ngensym () in let finish_match_label = label "finish_match_" in let compile_case (apat, guard, body) = @@ -647,7 +688,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit] else []) - @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup + @ body_setup + @ coverage_branch_taken branch_id body + @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] in if is_dead_aexp body then @@ -655,7 +698,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = else [iblock case_instrs; ilabel case_label] in - aval_setup @ [idecl ctyp case_return_id] + aval_setup @ on_reached @ [idecl ctyp case_return_id] @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], @@ -713,16 +756,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = compile_aexp ctx then_aexp else let if_ctyp = ctyp_of_typ ctx if_typ in + let branch_id, on_reached = coverage_branch_reached l in let compile_branch aexp = let setup, call, cleanup = compile_aexp ctx aexp in - fun clexp -> setup @ [call clexp] @ cleanup + fun clexp -> coverage_branch_taken branch_id aexp @ setup @ [call clexp] @ cleanup in let setup, cval, cleanup = compile_aval l ctx aval in setup, - (fun clexp -> iif l cval - (compile_branch then_aexp clexp) - (compile_branch else_aexp clexp) - if_ctyp), + (fun clexp -> + append_into_block on_reached + (iif l 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. *) diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index a642f29e..98ab44de 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -117,6 +117,8 @@ module type Config = sig val struct_value : bool (** Allow real literals *) val use_real : bool + (** Insert branch coverage operations *) + val branch_coverage : bool end module Make(C: Config) : sig diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index b662ef41..734f3fe4 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1563,6 +1563,7 @@ let unroll_static_foreach ctx = function let unroll_loops () = Some !opt_unroll_limit let struct_value = true let use_real = true + let branch_coverage = false end diff --git a/src/reporting.ml b/src/reporting.ml index 0029b902..603bc84f 100644 --- a/src/reporting.ml +++ b/src/reporting.ml @@ -127,6 +127,11 @@ let short_loc_to_string l = Printf.sprintf "%s %d:%d - %d:%d" p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol) +let loc_to_coverage l = + match simp_loc l with + | None -> None + | Some (p1, p2) -> Some (p1.pos_fname, p1.pos_cnum - p1.pos_bol, p2.pos_lnum, p2.pos_cnum - p2.pos_bol) + let print_err l m1 m2 = print_err_internal (Loc l) m1 m2 -- cgit v1.2.3 From 0c4c75d13aad176fc664e159d2b0c48c77b41d27 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 May 2020 09:24:09 +0100 Subject: Various bugfixes and improvements for updated codegen --- src/jib/c_codegen.ml | 121 +++++++++++++++++++++++++++++---------------------- 1 file changed, 70 insertions(+), 51 deletions(-) (limited to 'src') diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index 44d24367..80d4e847 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -57,15 +57,15 @@ open Type_check open PPrint open Printf open Value2 - + module StringMap = Map.Make(String) module StringSet = Set.Make(String) module Big_int = Nat_big_num module Json = Yojson.Basic - + let (gensym, _) = symbol_generator "c2" let ngensym () = name (gensym ()) - + let zencode_id id = Util.zencode_string (string_of_id id) let zencode_uid (id, ctyps) = @@ -74,7 +74,7 @@ let zencode_uid (id, ctyps) = | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps) let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty - + let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) @@ -97,7 +97,7 @@ let rec is_stack_ctyp ctyp = match ctyp with | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64) let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true)) - + type codegen_options = { (** Rewrites a Sail identifier into a user-specified name in the generated C *) exports : string Bindings.t; @@ -121,32 +121,31 @@ let initial_options = { extra_state = []; state_primops = StringSet.empty; } - + let add_export opts id = { opts with exports = Bindings.add id (string_of_id id) opts.exports } let add_custom_export opts id into = { opts with exports = Bindings.add id into opts.exports } - + let add_mangled_rename opts (from, into) = { opts with exports_mangled = StringMap.add from into opts.exports_mangled } - + let add_export_uid opts (id, ctyps) = match ctyps with | [] -> { opts with exports = Bindings.add id (string_of_id id) opts.exports } | _ -> opts - + let ctype_def_initial_options opts = function | CTD_enum (id, ids) -> List.fold_left add_export (add_export opts id) ids - | CTD_struct (id, ctors) -> - List.fold_left add_export_uid (add_export opts id) (List.map fst ctors) - | _ -> opts - + | CTD_struct (id, members) | CTD_variant (id, members) -> + List.fold_left add_export_uid (add_export opts id) (List.map fst members) + let cdef_initial_options opts = function | CDEF_type ctype_def -> ctype_def_initial_options opts ctype_def | CDEF_reg_dec (id, _, _) -> add_export opts id | CDEF_let (_, bindings, _) -> List.fold_left (fun opts (id, _) -> add_export opts id) opts bindings | _ -> opts - + let default_options cdefs = let opts = List.fold_left cdef_initial_options initial_options cdefs in let opts = add_export opts (mk_id "initialize_registers") in @@ -213,7 +212,7 @@ let options_from_json json cdefs = | json -> bad_key "extra_state" json in opts - + module type Config = sig val opts : codegen_options end @@ -225,7 +224,7 @@ let mangle str = match StringMap.find_opt mangled C.opts.exports_mangled with | Some export -> export | None -> mangled - + let sgen_id id = match Bindings.find_opt id C.opts.exports with | Some export -> export @@ -245,7 +244,7 @@ let sgen_name = "(*(state->current_exception))" | Throw_location _ -> "(state->throw_location)" - + let sgen_uid (id, ctyps) = match ctyps with | [] -> sgen_id id @@ -273,8 +272,8 @@ let rec sgen_ctyp = function | CT_struct (id, _) -> "struct " ^ sgen_id id | CT_enum (id, _) -> "enum " ^ sgen_id id | CT_variant (id, _) -> "struct " ^ sgen_id id - | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) - | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v) + | CT_list _ as l -> mangle (string_of_ctyp l) + | CT_vector _ as v -> mangle (string_of_ctyp v) | CT_fvector (_, ord, typ) -> sgen_ctyp (CT_vector (ord, typ)) | CT_string -> "sail_string" | CT_real -> "real" @@ -295,8 +294,8 @@ let rec sgen_ctyp_name = function | CT_struct (id, _) -> sgen_id id | CT_enum (id, _) -> sgen_id id | CT_variant (id, _) -> sgen_id id - | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) - | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v) + | CT_list _ as l -> mangle (string_of_ctyp l) + | CT_vector _ as v -> mangle (string_of_ctyp v) | CT_fvector (_, ord, typ) -> sgen_ctyp_name (CT_vector (ord, typ)) | CT_string -> "sail_string" | CT_real -> "real" @@ -349,10 +348,10 @@ let rec sgen_cval ctx = function sprintf "%s.%s" (sgen_cval ctx f) (mangle ("tup" ^ string_of_int n)) | V_ctor_kind (f, ctor, unifiers, _) -> sgen_cval ctx f ^ ".kind" - ^ " != Kind_" ^ zencode_uid (ctor, unifiers) + ^ " != Kind_" ^ sgen_uid (ctor, unifiers) | V_struct (fields, _) -> sprintf "{%s}" - (Util.string_of_list ", " (fun (field, cval) -> zencode_uid field ^ " = " ^ sgen_cval ctx cval) fields) + (Util.string_of_list ", " (fun (field, cval) -> sgen_uid field ^ " = " ^ sgen_cval ctx cval) fields) | V_ctor_unwrap (ctor, f, unifiers, _) -> sprintf "%s.%s" (sgen_cval ctx f) @@ -600,7 +599,7 @@ let extra_arguments is_extern = "" else "state, " - + let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = match instr with | I_decl (ctyp, id) when is_stack_ctyp ctyp -> @@ -776,7 +775,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = separate_map hardline (fun str -> string (" " ^ str)) (List.rev prev) ^^ hardline ^^ ksprintf string " return %s;" ret - + | I_comment str -> string (" /* " ^ str ^ " */") @@ -798,7 +797,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = (**************************************************************************) (* Code generation for type definitions (enums, structs, and variants) *) (**************************************************************************) - + let codegen_type_def_header = function | CTD_enum (id, ids) -> ksprintf string "// enum %s" (string_of_id id) ^^ hardline @@ -1016,11 +1015,11 @@ let codegen_type_def_body ctx = function let codegen_type_def ctx ctype_def = codegen_type_def_header ctype_def, codegen_type_def_body ctx ctype_def - + (**************************************************************************) (* Code generation for generated types (lists, tuples, etc) *) (**************************************************************************) - + (** GLOBAL: because C doesn't have real anonymous tuple types (anonymous structs don't quite work the way we need) every tuple type in the spec becomes some generated named struct in C. This is @@ -1051,13 +1050,13 @@ let codegen_tup ctx ctyps = generated := IdSet.add id !generated; codegen_type_def ctx (CTD_struct (id, UBindings.bindings fields)) end - + let codegen_list_header id = ksprintf string "// generated list type %s" (string_of_id id) ^^ hardline ^^ ksprintf string "struct node_%s;" (sgen_id id) ^^ hardline ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id) ^^ twice hardline - + let codegen_node id ctyp = ksprintf string "struct node_%s {\n %s hd;\n struct node_%s *tl;\n};\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id) ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id) @@ -1123,7 +1122,7 @@ let codegen_list_undefined id ctyp = ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp) ^^ ksprintf string " *rop = NULL;\n" ^^ string "}" - + let codegen_list ctx ctyp = let id = mk_id (string_of_ctyp (CT_list ctyp)) in if IdSet.mem id !generated then ( @@ -1152,7 +1151,7 @@ let codegen_vector_header ctx id (direction, ctyp) = ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id)) in vector_typedef ^^ twice hardline - + let codegen_vector_body ctx id (direction, ctyp) = let vector_init = string (Printf.sprintf "static void CREATE(%s)(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id)) @@ -1248,7 +1247,7 @@ let codegen_vector_body ctx id (direction, ctyp) = ^^ vector_update ^^ twice hardline ^^ internal_vector_update ^^ twice hardline ^^ internal_vector_init ^^ twice hardline - + let codegen_vector ctx (direction, ctyp) = let id = mk_id (string_of_ctyp (CT_vector (direction, ctyp))) in if IdSet.mem id !generated then ( @@ -1258,7 +1257,7 @@ let codegen_vector ctx (direction, ctyp) = codegen_vector_header ctx id (direction, ctyp), codegen_vector_body ctx id (direction, ctyp) ) - + (**************************************************************************) (* Code generation for definitions *) (**************************************************************************) @@ -1285,7 +1284,7 @@ let add_local_labels' instrs = let is_decl = function | I_aux (I_decl _, _) -> true | _ -> false - + let codegen_decl = function | I_aux (I_decl (ctyp, id), _) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_name id)) @@ -1296,12 +1295,12 @@ let codegen_alloc = function | I_aux (I_decl (ctyp, id), _) -> string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)) | _ -> assert false - + let add_local_labels instrs = match map_instrs add_local_labels' (iblock instrs) with | I_aux (I_block instrs, _) -> instrs | _ -> assert false - + let codegen_def_header ctx = function | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> if Env.is_extern id ctx.tc_env "c" then @@ -1317,14 +1316,14 @@ let codegen_def_header ctx = function | CDEF_type ctype_def -> codegen_type_def_header ctype_def - + | _ -> empty let codegen_def_body ctx = function | CDEF_reg_dec _ -> empty | CDEF_spec _ -> empty - + | CDEF_fundef (id, ret_arg, args, instrs) as def -> let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with | Some vs -> vs @@ -1399,7 +1398,7 @@ let codegen_def_body ctx = function ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) cleanup) ^^ hardline ^^ string "}" ^^ twice hardline - + (** As we generate C we need to generate specialized version of tuple, list, and vector type. These must be generated in the correct order. The ctyp_dependencies function generates a list of @@ -1426,9 +1425,18 @@ let codegen_ctg ctx = function | CTG_tup ctyps -> codegen_tup ctx ctyps | CTG_list ctyp -> codegen_list ctx ctyp +let codegen_progress n total = function + | CDEF_reg_dec (id, _, _) -> + Util.progress "Codegen " ("R " ^ string_of_id id) n total + | CDEF_fundef (id, _, _, _) -> + Util.progress "Codegen " (string_of_id id) n total + | _ -> + Util.progress "Codegen " "" n total + (** When we generate code for a definition, we need to first generate any auxillary type definitions that are required. *) -let codegen_def ctx def = +let codegen_def n total ctx def = + codegen_progress n total def; let ctyps = cdef_ctyps def |> CTSet.elements in (* We should have erased any polymorphism introduced by variants at this point! *) if List.exists is_polymorphic ctyps then @@ -1448,7 +1456,7 @@ let codegen_state_struct_def ctx = function | CDEF_let (_, [], _) -> empty | CDEF_let (_, bindings, _) -> - separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline | _ -> empty @@ -1464,7 +1472,7 @@ let codegen_state_struct ctx cdefs = ^^ string " bool have_exception;" ^^ hardline ^^ string " sail_string *throw_location;" ^^ hardline )) - ^^ separate_map hardline (fun str -> string (" " ^ str)) C.opts.extra_state ^^ hardline + ^^ concat_map (fun str -> string (" " ^ str) ^^ hardline) C.opts.extra_state ^^ string "};" let is_cdef_startup = function @@ -1514,15 +1522,26 @@ let rec get_recursive_functions (Defs defs) = | _ :: defs -> get_recursive_functions (Defs defs) | [] -> IdSet.empty - + let codegen_output file_name docs = let chan = open_out file_name in output_string chan (Pretty_print_sail.to_string docs); flush chan; close_out chan +let add_extra_header str = + if String.length str > 0 then ( + if str.[0] == '<' && str.[String.length str - 1] == '>' then + string ("#include " ^ str) ^^ hardline + else + string ("#include \"" ^ str ^ "\"") ^^ hardline + ) else ( + empty + ) + let codegen ctx output_name cdefs = - let docs_header, docs_body = List.map (codegen_def ctx) cdefs |> List.split in + let total = List.length cdefs in + let docs_header, docs_body = List.mapi (fun n def -> codegen_def (n + 1) total ctx def) cdefs |> List.split in let state = codegen_state_struct ctx cdefs in @@ -1547,7 +1566,7 @@ let codegen ctx output_name cdefs = let header = stdlib_headers ^^ hardline ^^ sail_headers ^^ hardline - ^^ concat_map (fun str -> string str ^^ hardline) C.opts.extra_headers ^^ hardline + ^^ concat_map add_extra_header C.opts.extra_headers ^^ hardline ^^ string "struct sail_state;" ^^ hardline ^^ string "typedef struct sail_state sail_state;" ^^ twice hardline @@ -1568,9 +1587,9 @@ let codegen ctx output_name cdefs = let letbind_finalizers = List.map (fun n -> Printf.sprintf " sail_kill_letbind_%d(state);" n) ctx.letbinds in - + let body = - ksprintf string "#include \"%s.h\"" output_name + ksprintf string "#include \"%s.h\"" (Filename.basename output_name) ^^ twice hardline ^^ concat docs_body ^^ string "void sail_initialize_letbindings(sail_state *state) {" ^^ hardline @@ -1624,10 +1643,10 @@ let emulator ctx output_name cdefs = string "#include \"sail_failure.h\""; string "#include \"rts.h\""; string "#include \"elf.h\""; - ksprintf string "#include \"%s.h\"" output_name ] + ksprintf string "#include \"%s.h\"" (Filename.basename output_name) ] @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) [] (*c_includes*))) in - + let startup cdefs = List.map sgen_startup (List.filter is_cdef_startup cdefs) in @@ -1636,7 +1655,7 @@ let emulator ctx output_name cdefs = in let regs = c_ast_registers cdefs in - + let model_init = separate hardline (List.map string ( [ "void model_initialize(sail_state *state)"; "{"; -- cgit v1.2.3 From f05e81a641b4fb6f2d5e69ef4c13e0ada3dc3bfb Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 May 2020 10:08:43 +0100 Subject: Attempt to fix CI error --- src/sail.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/sail.ml b/src/sail.ml index 8e89bbed..1f1b2489 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -55,7 +55,9 @@ module Json = Yojson.Basic let lib = ref ([] : string list) let opt_interactive_script : string option ref = ref None -let opt_config : Json.t option ref = ref None +(* Note: May cause a depcrecated warning for json type, but this cannot be + fixed without breaking Ubuntu 18.04 CI *) +let opt_config : Json.json option ref = ref None let opt_print_version = ref false let opt_target = ref None let opt_tofrominterp_output_dir : string option ref = ref None -- cgit v1.2.3 From 3f217002bd732d4c408af6bd34fafbb8bdd4404e Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 May 2020 10:25:18 +0100 Subject: Re-activate some tests --- src/sail.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/sail.ml b/src/sail.ml index 1f1b2489..9dbd1f6c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -55,7 +55,7 @@ module Json = Yojson.Basic let lib = ref ([] : string list) let opt_interactive_script : string option ref = ref None -(* Note: May cause a depcrecated warning for json type, but this cannot be +(* Note: May cause a deprecated warning for json type, but this cannot be fixed without breaking Ubuntu 18.04 CI *) let opt_config : Json.json option ref = ref None let opt_print_version = ref false -- cgit v1.2.3 From 806e97ffbc0193a3539d5c0dc8902465d71fe0bd Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 May 2020 10:54:16 +0100 Subject: Output INT64_MIN in code generator for min 64-bit integer literal Fixes the warning generated because in C -X where X is the minimum integer is parsed as a positive integer which is then negated. This causes a (I believe spurious) warning that the integer literal is too large for the type. Also using INT64_C so we get either long or long long depending on platform --- src/jib/c_backend.ml | 6 +++++- src/jib/c_codegen.ml | 6 +++++- 2 files changed, 10 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index c38749f3..5947b500 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1212,7 +1212,11 @@ let rec sgen_value = function | VL_bits ([], _) -> "UINT64_C(0)" | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")" - | VL_int i -> Big_int.to_string i ^ "l" + | VL_int i -> + if Big_int.equal i (min_int 64) then + "INT64_MIN" + else + "INT64_C(" ^ Big_int.to_string i ^ ")" | VL_bool true -> "true" | VL_bool false -> "false" | VL_unit -> "UNIT" diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index 80d4e847..05abfe70 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -322,7 +322,11 @@ let rec sgen_value = function | VL_bits ([], _) -> "UINT64_C(0)" | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")" - | VL_int i -> Big_int.to_string i ^ "l" + | VL_int i -> + if Big_int.equal i (min_int 64) then + "INT64_MIN" + else + "INT64_C(" ^ Big_int.to_string i ^ ")" | VL_bool true -> "true" | VL_bool false -> "false" | VL_unit -> "UNIT" -- cgit v1.2.3 From ffaa84fe0a79a013da2169bcca76a23d4213d526 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 15 May 2020 10:54:59 +0100 Subject: Add coverage tracking tool See sailcov/README.md for a short description Fix many location info bugs discovered by eyeballing output --- src/ast_util.ml | 2 +- src/ast_util.mli | 2 +- src/jib/anf.ml | 13 +++-- src/jib/c_backend.ml | 149 ++++++++++-------------------------------------- src/jib/c_backend.mli | 3 +- src/jib/c_codegen.ml | 14 ++--- src/jib/jib_compile.ml | 44 +++++++++----- src/jib/jib_compile.mli | 11 ++-- src/jib/jib_smt.ml | 7 ++- src/lexer.mll | 12 ++-- src/rewrites.ml | 18 +++--- src/sail.ml | 9 ++- src/type_check.ml | 16 +++--- 13 files changed, 117 insertions(+), 183 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index ac5da907..d0af5da3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -89,7 +89,7 @@ let untyp_pat = function | P_aux (P_typ (typ, pat), _) -> pat, Some typ | pat -> pat, None -let mk_pexp pexp_aux = Pat_aux (pexp_aux, no_annot) +let mk_pexp ?loc:(l=Parse_ast.Unknown) pexp_aux = Pat_aux (pexp_aux, (l, ())) let mk_mpat mpat_aux = MP_aux (mpat_aux, no_annot) let mk_mpexp mpexp_aux = MPat_aux (mpexp_aux, no_annot) diff --git a/src/ast_util.mli b/src/ast_util.mli index 6be8ca34..1449a390 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -84,7 +84,7 @@ val mk_nexp : nexp_aux -> nexp val mk_exp : ?loc:l -> unit exp_aux -> unit exp val mk_pat : unit pat_aux -> unit pat val mk_mpat : unit mpat_aux -> unit mpat -val mk_pexp : unit pexp_aux -> unit pexp +val mk_pexp : ?loc:l -> unit pexp_aux -> unit pexp val mk_mpexp : unit mpexp_aux -> unit mpexp val mk_lexp : unit lexp_aux -> unit lexp val mk_lit : lit_aux -> lit diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 7757cd9a..c81f729c 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -525,13 +525,13 @@ let rec apat_globals (AP_aux (aux, _, _)) = let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in - let to_aval (AE_aux (aexp_aux, env, l) as aexp) = - let mk_aexp aexp = AE_aux (aexp, env, l) in + let to_aval (AE_aux (aexp_aux, env, _) as aexp) = + let mk_aexp (AE_aux (_, _, l)) aexp = AE_aux (aexp, env, l) in match aexp_aux with | AE_val v -> (v, fun x -> x) | AE_short_circuit (_, _, _) -> let id = gensym () in - (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp x (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp))) | AE_app (_, _, typ) | AE_let (_, _, _, _, _, typ) | AE_return (_, typ) @@ -544,10 +544,10 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | AE_record_update (_, _, typ) | AE_block (_, _, typ) -> let id = gensym () in - (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (Immutable, id, typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp x (AE_let (Immutable, id, typ, aexp, x, typ_of exp))) | AE_assign _ | AE_for _ | AE_loop _ | AE_write_ref _ -> let id = gensym () in - (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp x (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp))) in match e_aux with | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) @@ -703,7 +703,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_var (LEXP_aux (LEXP_id id, _), binding, body) | E_var (LEXP_aux (LEXP_cast (_, id), _), binding, body) - | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> + | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) + | E_let (LB_aux (LB_val (P_aux (P_typ (_, P_aux (P_id id, _)), _), binding), _), body) -> let env = env_of body in let lvar = Env.lookup_id id env in mk_aexp (AE_let (Mutable, id, lvar_typ lvar, anf binding, anf body, typ_of exp)) diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 5947b500..fa4fa802 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -68,7 +68,8 @@ let opt_no_rts = ref false let opt_prefix = ref "z" let opt_extra_params = ref None let opt_extra_arguments = ref None - +let opt_branch_coverage = ref false + let extra_params () = match !opt_extra_params with | Some str -> str ^ ", " @@ -164,7 +165,7 @@ let literal_to_fragment (L_aux (l_aux, _) as lit) = | L_false -> Some (V_lit (VL_bool false, CT_bool)) | _ -> None -module C_config : Config = struct +module C_config(Opts : sig val branch_coverage : bool end) : Config = struct (** Convert a sail type into a C-type. This function can be quite slow, because it uses ctx.local_env and SMT to analyse the Sail @@ -557,107 +558,13 @@ module C_config : Config = struct analyze_functions ctx analyze_primop (c_literals ctx aexp) - let unroll_loops () = None + let unroll_loops = None let specialize_calls = false let ignore_64 = false let struct_value = false let use_real = false - let branch_coverage = false -end - -(* When compiling to a C library, we want to do things slightly - differently. First, to ensure that functions have a predictable - type and calling convention, we don't use the SMT solver to - optimize types at all. Second we don't apply the analyse primitives - step in optimize_anf for similar reasons. *) -module Clib_config : Config = struct - let rec convert_typ ctx typ = - let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in - 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_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 - - | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool - | Typ_app (id, _) when - string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" || string_of_id id = "itself" -> - begin match destruct_range Env.empty typ with - | None -> assert false (* Checked if range type in guard *) - | Some (kids, constr, n, m) -> - let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env }in - match nexp_simp n, nexp_simp m with - | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) - when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> - CT_fint 64 - | _, _ -> - CT_lint - end - - | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> - CT_list (convert_typ ctx typ) - - | Typ_app (id, [A_aux (A_nexp n, _); - A_aux (A_order ord, _)]) - when string_of_id id = "bitvector" -> - 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) - | _ -> CT_lbits direction - end - - | Typ_app (id, [A_aux (A_nexp n, _); - A_aux (A_order ord, _); - A_aux (A_typ typ, _)]) - when string_of_id id = "vector" -> - let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in - CT_vector (direction, convert_typ ctx typ) - - | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" -> - CT_ref (convert_typ ctx typ) - - | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> UBindings.bindings) - | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants |> UBindings.bindings) - | Typ_id id when Bindings.mem id ctx.enums -> CT_enum (id, Bindings.find id ctx.enums |> IdSet.elements) - - | Typ_tup typs -> CT_tup (List.map (convert_typ ctx) typs) - - | Typ_exist _ -> - begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with - | Some (kids, nc, typ) -> - let env = add_existential l kids nc ctx.local_env in - convert_typ { ctx with local_env = env } typ - | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!") - end - - | Typ_var kid -> CT_poly - - | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ) - - let c_literals ctx = - let rec c_literal env l = function - | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) -> - begin - match literal_to_fragment lit with - | Some cval -> AV_cval (cval, typ) - | None -> v - end - | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals) - | v -> v - in - map_aval c_literal - - let optimize_anf ctx aexp = c_literals ctx aexp - - let unroll_loops () = None - let specialize_calls = false - let ignore_64 = false - let struct_value = false - let use_real = false - let branch_coverage = false + let branch_coverage = Opts.branch_coverage + let track_throw = true end (** Functions that have heap-allocated return types are implemented by @@ -2320,7 +2227,7 @@ let rec get_recursive_functions (Defs defs) = | [] -> IdSet.empty let jib_of_ast env ast = - let module Jibc = Make(C_config) in + let module Jibc = Make(C_config(struct let branch_coverage = !opt_branch_coverage end)) in let ctx = initial_ctx (add_special_functions env) in Jibc.compile_ast ctx ast @@ -2341,6 +2248,7 @@ let compile_ast env output_chan c_includes ast = @ (if !opt_no_rts then [] else [ string "#include \"rts.h\""; string "#include \"elf.h\"" ]) + @ (if !opt_branch_coverage then [string "#include \"sail_coverage.h\""] else []) @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes)) in @@ -2405,22 +2313,32 @@ let compile_ast env output_chan c_includes ast = @ [ "}" ] )) in - let model_default_main = separate hardline (List.map string - [ "int model_main(int argc, char *argv[])"; - "{"; - " model_init();"; - " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; - Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); - " model_fini();"; - " return EXIT_SUCCESS;"; - "}" ] ) + let model_default_main = + ([ "int model_main(int argc, char *argv[])"; + "{"; + " model_init();"; + " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; + Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); + " model_fini();" ] + @ (if !opt_branch_coverage then + [ " if (sail_coverage_exit() != 0) {"; + " fprintf(stderr, \"Could not write coverage information\\n\");"; + " exit(EXIT_FAILURE);"; + " }" ] + else + [] + ) + @ [ " return EXIT_SUCCESS;"; + "}" ]) + |> List.map string + |> separate hardline in let model_main = separate hardline (if (!opt_no_main) then [] else List.map string - [ "int main(int argc, char *argv[])"; - "{"; - " return model_main(argc, argv);"; - "}" ] ) + [ "int main(int argc, char *argv[])"; + "{"; + " return model_main(argc, argv);"; + "}" ] ) in let hlhl = hardline ^^ hardline in @@ -2438,11 +2356,6 @@ let compile_ast env output_chan c_includes ast = | Type_error (_, l, err) -> c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) -let jib_of_ast_clib env ast = - let module Jibc = Make(Clib_config) in - let ctx = initial_ctx (add_special_functions env) in - Jibc.compile_ast ctx ast - let compile_ast_clib env ast codegen = let cdefs, ctx = jib_of_ast env ast in let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index 2334cc0e..b10e53d3 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -88,6 +88,8 @@ val opt_prefix : string ref val opt_extra_params : string option ref val opt_extra_arguments : string option ref +val opt_branch_coverage : bool ref + (** Optimization flags *) val optimize_primops : bool ref @@ -100,5 +102,4 @@ val optimize_fixed_bits : bool ref val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit -val jib_of_ast_clib : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx val compile_ast_clib : Env.t -> tannot Ast.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index 05abfe70..d5015318 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -213,20 +213,20 @@ let options_from_json json cdefs = in opts -module type Config = sig +module type Options = sig val opts : codegen_options end -module Make(C: Config) = struct +module Make(O: Options) = struct let mangle str = let mangled = Util.zencode_string str in - match StringMap.find_opt mangled C.opts.exports_mangled with + match StringMap.find_opt mangled O.opts.exports_mangled with | Some export -> export | None -> mangled let sgen_id id = - match Bindings.find_opt id C.opts.exports with + match Bindings.find_opt id O.opts.exports with | Some export -> export | None -> mangle (string_of_id id) @@ -651,7 +651,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = (sgen_function_uid f, false) in let sail_state_arg = - if is_extern && StringSet.mem fname C.opts.state_primops then + if is_extern && StringSet.mem fname O.opts.state_primops then "sail_state *state, " else "" @@ -1476,7 +1476,7 @@ let codegen_state_struct ctx cdefs = ^^ string " bool have_exception;" ^^ hardline ^^ string " sail_string *throw_location;" ^^ hardline )) - ^^ concat_map (fun str -> string (" " ^ str) ^^ hardline) C.opts.extra_state + ^^ concat_map (fun str -> string (" " ^ str) ^^ hardline) O.opts.extra_state ^^ string "};" let is_cdef_startup = function @@ -1570,7 +1570,7 @@ let codegen ctx output_name cdefs = let header = stdlib_headers ^^ hardline ^^ sail_headers ^^ hardline - ^^ concat_map add_extra_header C.opts.extra_headers ^^ hardline + ^^ concat_map add_extra_header O.opts.extra_headers ^^ hardline ^^ string "struct sail_state;" ^^ hardline ^^ string "typedef struct sail_state sail_state;" ^^ twice hardline diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 11bfa2fc..84705ae2 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -58,7 +58,6 @@ open Value2 open Anf let opt_memo_cache = ref false -let opt_track_throw = ref true let optimize_aarch64_fast_struct = ref false @@ -174,12 +173,13 @@ let initial_ctx env = module type Config = sig val convert_typ : ctx -> typ -> ctyp val optimize_anf : ctx -> typ aexp -> typ aexp - val unroll_loops : unit -> int option + val unroll_loops : int option val specialize_calls : bool val ignore_64 : bool val struct_value : bool val use_real : bool val branch_coverage : bool + val track_throw : bool end module Make(C: Config) = struct @@ -201,12 +201,10 @@ let coverage_branch_count = ref 0 let coverage_loc_args l = match Reporting.simp_loc l with - | None -> - Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation"; - None + | None -> None | Some (p1, p2) -> Some (Printf.sprintf "\"%s\", %d, %d, %d, %d" - p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)) + (String.escaped p1.pos_fname) p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)) let coverage_branch_reached l = let branch_id = !coverage_branch_count in @@ -214,9 +212,7 @@ let coverage_branch_reached l = branch_id, if C.branch_coverage then begin match coverage_loc_args l with - | None -> - Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation"; - [] + | None -> [] | Some args -> [iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)] end @@ -234,8 +230,20 @@ let coverage_branch_taken branch_id (AE_aux (_, _, l)) = else match coverage_loc_args l with | None -> [] - | Some args -> [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)] - + | Some args -> + print_endline ("B " ^ args); + [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)] + +let coverage_function_entry id l = + if not C.branch_coverage then + [] + else + match coverage_loc_args l with + | None -> [] + | Some args -> + print_endline ("F " ^ args); + [iraw (Printf.sprintf "sail_function_entry(\"%s\", %s);" (string_of_id id) args)] + let rec compile_aval l ctx = function | AV_cval (cval, typ) -> let ctyp = cval_ctyp cval in @@ -668,6 +676,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_case (aval, cases, typ) -> let ctyp = ctyp_of_typ ctx typ in let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in + (* Get the number of cases, because we don't want to check branch + coverage for matches with only a single case. *) + let num_cases = List.length cases in let branch_id, on_reached = coverage_branch_reached l in let case_return_id = ngensym () in let finish_match_label = label "finish_match_" in @@ -689,7 +700,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit] else []) @ body_setup - @ coverage_branch_taken branch_id body + @ (if num_cases > 1 then coverage_branch_taken branch_id body else []) @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] in @@ -698,7 +709,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = else [iblock case_instrs; ilabel case_label] in - aval_setup @ on_reached @ [idecl ctyp case_return_id] + aval_setup + @ (if num_cases > 1 then on_reached else []) + @ [idecl ctyp case_return_id] @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], @@ -997,7 +1010,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (* We can either generate an actual loop body for C, or unroll the body for SMT *) let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure ()]) in - let body = match C.unroll_loops () with Some times -> unroll times 0 | None -> actual in + let body = match C.unroll_loops with Some times -> unroll times 0 | None -> actual in variable_init from_gs from_setup from_call from_cleanup @ variable_init to_gs to_setup to_call to_cleanup @@ -1106,7 +1119,7 @@ let fix_exception_block ?return:(return=None) ctx instrs = before @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval; icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool))] - @ (if !opt_track_throw then + @ (if C.track_throw then let loc_string = Reporting.short_loc_to_string l in [icopy l (CL_id (throw_location, CT_string)) (V_lit (VL_string loc_string, CT_string))] else []) @@ -1307,6 +1320,7 @@ let compile_funcl ctx id pat guard exp = let instrs = arg_setup @ destructure @ guard_instrs @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + let instrs = coverage_function_entry id (exp_loc exp) @ instrs in [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index 98ab44de..47ca6962 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -61,11 +61,6 @@ open Type_check ARM v8.5 spec. It is unsound in general. *) val optimize_aarch64_fast_struct : bool ref -(** If true (default) track the location of the last exception thrown, - useful for debugging C but we want to turn it off for SMT generation - where we can't use strings *) -val opt_track_throw : bool ref - (** (WIP) [opt_memo_cache] will store the compiled function definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the original function to be compiled. Enabled using the -memo @@ -105,7 +100,7 @@ module type Config = sig val optimize_anf : ctx -> typ aexp -> typ aexp (** Unroll all for loops a bounded number of times. Used for SMT generation. *) - val unroll_loops : unit -> int option + val unroll_loops : int option (** If false, function arguments must match the function type exactly. If true, they can be more specific. *) val specialize_calls : bool @@ -119,6 +114,10 @@ module type Config = sig val use_real : bool (** Insert branch coverage operations *) val branch_coverage : bool + (** If true track the location of the last exception thrown, useful + for debugging C but we want to turn it off for SMT generation + where we can't use strings *) + val track_throw : bool end module Make(C: Config) : sig diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 734f3fe4..a299d7b9 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1397,7 +1397,7 @@ let rec generate_reg_decs ctx inits = function let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) -module SMT_config : Jib_compile.Config = struct +module SMT_config(Opts : sig val unroll_limit : int end) : Jib_compile.Config = struct open Jib_compile (** Convert a sail type into a C-type. This function can be quite @@ -1560,10 +1560,11 @@ let unroll_static_foreach ctx = function let specialize_calls = true let ignore_64 = true - let unroll_loops () = Some !opt_unroll_limit + let unroll_loops = Some Opts.unroll_limit let struct_value = true let use_real = true let branch_coverage = false + let track_throw = false end @@ -2328,7 +2329,7 @@ let rec build_register_map rmap = function let compile env ast = let cdefs, jib_ctx = - let module Jibc = Jib_compile.Make(SMT_config) in + let module Jibc = Jib_compile.Make(SMT_config(struct let unroll_limit = !opt_unroll_limit end)) in let ctx = Jib_compile.(initial_ctx (add_special_functions env)) in let t = Profile.start () in let cdefs, ctx = Jibc.compile_ast ctx ast in diff --git a/src/lexer.mll b/src/lexer.mll index 8000879e..40f4b470 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -288,8 +288,10 @@ rule token = parse | "-" digit+ as i { (Num(Big_int.of_string i)) } | "0b" (binarydigit+ as i) { (Bin(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) } | "0x" (hexdigit+ as i) { (Hex(Util.string_of_list "" (fun s -> s) (Util.split_on_char '_' i))) } - | '"' { (String( - string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) } + | '"' { let startpos = Lexing.lexeme_start_p lexbuf in + let contents = string startpos (Buffer.create 10) lexbuf in + lexbuf.lex_start_p <- startpos; + String(contents) } | eof { Eof } | _ as c { raise (LexError( Printf.sprintf "Unexpected character: %c" c, @@ -331,10 +333,6 @@ and string pos b = parse | '\\' '\n' ws { Lexing.new_line lexbuf; string pos b lexbuf } | '\\' { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos, "illegal backslash escape in string"*) } - | '"' { let s = unescaped(Buffer.contents b) in - (*try Ulib.UTF8.validate s; s - with Ulib.UTF8.Malformed_code -> - raise (Reporting.Fatal_error (Reporting.Err_syntax (pos, - "String literal is not valid utf8"))) *) s } + | '"' { unescaped (Buffer.contents b) } | eof { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos, "String literal not terminated")))*) } diff --git a/src/rewrites.ml b/src/rewrites.ml index 89f67d87..48ea78ae 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -489,6 +489,13 @@ let remove_vector_concat_pat pat = let decls = List.fold_left (fun f g x -> f (g x)) (fun b -> b) decls in + (* Finally we patch up the top location for the expressions wrapped + by decls, otherwise this can cause the coverage instrumentation + to get super confused by the generated locations *) + let decls (E_aux (_, (l, _)) as exp) = + let E_aux (aux, (_, annot)) = decls exp in + E_aux (aux, (gen_loc l, annot)) in + (* at this point shouldn't have P_as patterns in P_vector_concat patterns any more, all P_as and P_id vectors should have their declarations in decls. Now flatten all vector_concat patterns *) @@ -691,7 +698,7 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2 | P_wild, _ -> Some [] - | P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) -> + | P_app (Id_aux (id1,_),args1), P_app (Id_aux (id2,_),args2) -> if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None | P_vector pats1, P_vector pats2 | P_vector_concat pats1, P_vector_concat pats2 @@ -1374,9 +1381,6 @@ let updates_vars exp = lit vectors in patterns or expressions *) let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as full_exp) = - let rewrap e = E_aux (e,annot) in - let rewrap_effects e eff = - E_aux (e, (l,Some (env_of_annot annot, typ_of_annot annot, eff))) in let rewrite_rec = rewriters.rewrite_exp rewriters in let rewrite_base = rewrite_exp rewriters in match exp with @@ -2562,7 +2566,7 @@ let fold_typed_guards env guards = | g :: gs -> List.fold_left (fun g g' -> annot_exp (E_app (mk_id "and_bool", [g; g'])) Parse_ast.Unknown env bool_typ) g gs -let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot annot)) as pexp) = +let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (l, _)) as pexp) = let guards = ref [] in match pexp_aux with @@ -2572,13 +2576,13 @@ let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot anno match !guards with | [] -> pexp | gs -> - let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in + let unchecked_pexp = mk_pexp ~loc:l (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp) end | Pat_when (pat, guard, exp) -> begin let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in - let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in + let unchecked_pexp = mk_pexp ~loc:l (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp) end diff --git a/src/sail.ml b/src/sail.ml index 9dbd1f6c..772d8564 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -173,10 +173,10 @@ let options = Arg.align ([ set_target "ir", " print intermediate representation"); ( "-smt", - Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw], + Arg.Tuple [set_target "smt"], " print SMT translated version of input"); ( "-smt_auto", - Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw; Arg.Set Jib_smt.opt_auto], + Arg.Tuple [set_target "smt"; Arg.Set Jib_smt.opt_auto], " generate SMT and automatically call the solver (implies -smt)"); ( "-smt_ignore_overflow", Arg.Set Jib_smt.opt_ignore_overflow, @@ -201,7 +201,7 @@ let options = Arg.align ([ " output a C translated version of the input"); ( "-c2", Arg.Tuple [set_target "c2"; Arg.Set Initial_check.opt_undefined_gen], - " output a C translated version of the input"); + " output a C translated version of the input (experimental code-generation)"); ( "-c_include", Arg.String (fun i -> opt_includes_c := i::!opt_includes_c), " provide additional include for C output"); @@ -232,6 +232,9 @@ let options = Arg.align ([ ( "-c_fold_unit", Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str), " remove comma separated list of functions from C output, replacing them with unit"); + ( "-c_coverage", + Arg.Set C_backend.opt_branch_coverage, + " instrument C code to track branch coverage"); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); diff --git a/src/type_check.ml b/src/type_check.ml index 82bc92d8..73cb8a57 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2994,7 +2994,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let checked_exp = crule check_exp env exp exc_typ in annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape]) | E_var (lexp, bind, exp), _ -> - let lexp, bind, env = match bind_assignment env lexp bind with + let lexp, bind, env = match bind_assignment l env lexp bind with | E_aux (E_assign (lexp, bind), _), env -> lexp, bind, env | _, _ -> assert false in @@ -3059,8 +3059,8 @@ and check_block l env exps ret_typ = match Nl_flow.analyze exps with | [] -> (match ret_typ with Some typ -> typ_equality l env typ unit_typ; [] | None -> []) | [exp] -> [final env exp] - | (E_aux (E_assign (lexp, bind), _) :: exps) -> - let texp, env = bind_assignment env lexp bind in + | (E_aux (E_assign (lexp, bind), (assign_l, _)) :: exps) -> + let texp, env = bind_assignment assign_l env lexp bind in texp :: check_block l env exps ret_typ | ((E_aux (E_assert (constr_exp, msg), _) as exp) :: exps) -> let msg = assert_msg msg in @@ -3548,9 +3548,9 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (A_aux (typ_arg_au | _, A_order _ -> typ_error env l "Cannot bind type pattern against order" | _, _ -> typ_error env l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat) -and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) = - let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, mk_tannot env (mk_typ (Typ_id (mk_id "unit"))) no_effect)) in - let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, mk_tannot env typ eff)) in +and bind_assignment assign_l env (LEXP_aux (lexp_aux, (lexp_l, ())) as lexp) (E_aux (_, (exp_l, ())) as exp) = + let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (assign_l, mk_tannot env (mk_typ (Typ_id (mk_id "unit"))) no_effect)) in + let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (lexp_l, mk_tannot env typ eff)) in let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in let has_typ v env = match Env.lookup_id v env with @@ -3559,7 +3559,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as in match lexp_aux with | LEXP_memory (f, xs) -> - check_exp env (E_aux (E_app (f, xs @ [exp]), (l, ()))) unit_typ, env + check_exp env (E_aux (E_app (f, xs @ [exp]), (lexp_l, ()))) unit_typ, env | LEXP_cast (typ_annot, v) -> let checked_exp = crule check_exp env exp typ_annot in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in @@ -3817,7 +3817,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let inferred_exps = List.map (irule infer_exp env) exps in annot_exp (E_tuple inferred_exps) (mk_typ (Typ_tup (List.map typ_of inferred_exps))) | E_assign (lexp, bind) -> - fst (bind_assignment env lexp bind) + fst (bind_assignment l env lexp bind) | E_record_update (exp, fexps) -> let inferred_exp = irule infer_exp env exp in let typ = typ_of inferred_exp in -- cgit v1.2.3 From e6354d8ceea7217e1544606c3c2b79bca4e582fe Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Thu, 14 May 2020 18:01:16 +0100 Subject: Add static to more C functions This allows me to compile sail-riscv64 and sail-riscv128 code in the same static library. --- src/jib/c_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index fa4fa802..e5486645 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1592,7 +1592,7 @@ let codegen_type_def ctx = function in let codegen_undefined = let name = sgen_id id in - string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) + string (Printf.sprintf "static enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) in string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi] -- cgit v1.2.3 From 363cf77a75cb8237fb13b028c0046b7817dbe734 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 13:43:07 +0100 Subject: Also allow adding static to model_{init,fini,main}() Without this I get the following linker error when trying to include both 64 and 128 bit sail-riscv code in the same binary: duplicate symbol '_model_init' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) duplicate symbol '_model_main' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) duplicate symbol '_model_fini' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) # Conflicts: # src/jib/c_backend.ml --- src/jib/c_backend.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index e5486645..e6610e93 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2291,7 +2291,7 @@ let compile_ast env output_chan c_includes ast = in let model_init = separate hardline (List.map string - ( [ "void model_init(void)"; + ( [ "static void model_init(void)"; "{"; " setup_rts();" ] @ fst exn_boilerplate @@ -2303,7 +2303,7 @@ let compile_ast env output_chan c_includes ast = in let model_fini = separate hardline (List.map string - ( [ "void model_fini(void)"; + ( [ "static void model_fini(void)"; "{" ] @ letbind_finalizers @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs) @@ -2313,8 +2313,8 @@ let compile_ast env output_chan c_includes ast = @ [ "}" ] )) in - let model_default_main = - ([ "int model_main(int argc, char *argv[])"; + let model_default_main = + ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (if !opt_static then "static " else ""); "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; -- cgit v1.2.3 From dc5a39649116c7fd76a024d069707f8b3aa7e201 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 09:43:12 +0100 Subject: Also make the letbinding C variables static I was getting run-time failures when code generate from cheri128 and cheri64 in the same process. This was caused because my compiler defaults to -fcommon so it merged multiple variables (with conflicting types!). When initializing the second set of letbindings, the first one was overwritten (first variable was lbits, the other was uint64_t). Compiling with -fno-common exposes this problem. --- src/jib/c_backend.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index e6610e93..080be248 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2127,7 +2127,8 @@ let codegen_def' ctx = function let cleanup = List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings) in - separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings + let static = if !opt_static then "static " else "" in + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" static (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number) ^^ string "{" ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline -- cgit v1.2.3 From 402fe1f632f7e6075e0810dcff2d8432b65352d2 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 13:51:32 +0100 Subject: Add static to registers if -static is passed This was the final missing step for me to link two almost identical C files generated from sail into the same library. --- src/jib/c_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 080be248..40d784ca 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2050,7 +2050,7 @@ let codegen_alloc = function let codegen_def' ctx = function | CDEF_reg_dec (id, ctyp, _) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline - ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) + ^^ string (Printf.sprintf "%s%s %s;" (if !opt_static then "static " else "") (sgen_ctyp ctyp) (sgen_id id)) | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> let static = if !opt_static then "static " else "" in -- cgit v1.2.3 From 4d50c7b8601907774da137f4f3609f644f5df20a Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 16:26:00 +0100 Subject: C backend: Add a static () helper This simplifies some of the code. --- src/jib/c_backend.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 40d784ca..4527aaa1 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -62,6 +62,7 @@ open Anf module Big_int = Nat_big_num let opt_static = ref false +let static () = if !opt_static then "static " else "" let opt_no_main = ref false let opt_no_lib = ref false let opt_no_rts = ref false @@ -2050,16 +2051,15 @@ let codegen_alloc = function let codegen_def' ctx = function | CDEF_reg_dec (id, ctyp, _) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline - ^^ string (Printf.sprintf "%s%s %s;" (if !opt_static then "static " else "") (sgen_ctyp ctyp) (sgen_id id)) + ^^ string (Printf.sprintf "%s%s %s;" (static ()) (sgen_ctyp ctyp) (sgen_id id)) | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> - let static = if !opt_static then "static " else "" in if Env.is_extern id ctx.tc_env "c" then empty else if is_stack_ctyp ret_ctyp then - string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%s%s %s(%s%s);" (static ()) (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) else - string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" (static ()) (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) | CDEF_fundef (id, ret_arg, args, instrs) as def -> let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with @@ -2100,8 +2100,7 @@ let codegen_def' ctx = function codegen_type_def ctx ctype_def | CDEF_startup (id, instrs) -> - let static = if !opt_static then "static " else "" in - let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_function_id id)) in + let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" (static ()) (sgen_function_id id)) in separate_map hardline codegen_decl instrs ^^ twice hardline ^^ startup_header ^^ hardline @@ -2110,8 +2109,7 @@ let codegen_def' ctx = function ^^ string "}" | CDEF_finish (id, instrs) -> - let static = if !opt_static then "static " else "" in - let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_function_id id)) in + let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" (static ()) (sgen_function_id id)) in separate_map hardline codegen_decl (List.filter is_decl instrs) ^^ twice hardline ^^ finish_header ^^ hardline @@ -2127,8 +2125,7 @@ let codegen_def' ctx = function let cleanup = List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings) in - let static = if !opt_static then "static " else "" in - separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" static (sgen_ctyp ctyp) (sgen_id id))) bindings + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" (static ()) (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number) ^^ string "{" ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline @@ -2315,7 +2312,7 @@ let compile_ast env output_chan c_includes ast = in let model_default_main = - ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (if !opt_static then "static " else ""); + ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (static ()); "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; -- cgit v1.2.3 From a2ddd7d0fb1f1c3b6ac0d7bd360ff9a6f9d728dc Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 16:26:37 +0100 Subject: C backend: Only add static to model_{init,fini} if -static is passed Otherwise the C emulator doesn't build. --- src/jib/c_backend.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 4527aaa1..b1d6cc40 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2289,7 +2289,7 @@ let compile_ast env output_chan c_includes ast = in let model_init = separate hardline (List.map string - ( [ "static void model_init(void)"; + ( [ Printf.sprintf "%svoid model_init(void)" (static ()); "{"; " setup_rts();" ] @ fst exn_boilerplate @@ -2301,7 +2301,7 @@ let compile_ast env output_chan c_includes ast = in let model_fini = separate hardline (List.map string - ( [ "static void model_fini(void)"; + ( [ Printf.sprintf "%svoid model_fini(void)" (static ()); "{" ] @ letbind_finalizers @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs) -- cgit v1.2.3