diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/anf.ml | 15 | ||||
| -rw-r--r-- | src/jib/anf.mli | 4 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 170 | ||||
| -rw-r--r-- | src/jib/c_backend.mli | 13 | ||||
| -rw-r--r-- | src/jib/c_codegen.ml | 1714 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 125 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 22 | ||||
| -rw-r--r-- | src/jib/jib_ir.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_optimize.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 26 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 1 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 8 |
12 files changed, 1962 insertions, 140 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 6bc447c0..c81f729c 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, _, _)) = @@ -523,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) @@ -542,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)) @@ -701,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/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 2b2234b5..b1d6cc40 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -62,14 +62,15 @@ 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_memo_cache = ref false let opt_no_lib = ref false 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 ^ ", " @@ -130,12 +131,47 @@ 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)) -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) **) +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(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 + 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 @@ -232,41 +268,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) -> @@ -558,13 +559,15 @@ 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 = Opts.branch_coverage + let track_throw = true 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 @@ -1117,7 +1120,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" @@ -1329,6 +1336,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 +1349,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 ^ "))" @@ -1584,7 +1593,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] @@ -2042,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;" (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 @@ -2092,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 @@ -2102,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 @@ -2119,7 +2125,7 @@ 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 + 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 @@ -2219,10 +2225,10 @@ 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 - + let compile_ast env output_chan c_includes ast = try let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in @@ -2240,6 +2246,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 @@ -2282,7 +2289,7 @@ let compile_ast env output_chan c_includes ast = in let model_init = separate hardline (List.map string - ( [ "void model_init(void)"; + ( [ Printf.sprintf "%svoid model_init(void)" (static ()); "{"; " setup_rts();" ] @ fst exn_boilerplate @@ -2294,7 +2301,7 @@ let compile_ast env output_chan c_includes ast = in let model_fini = separate hardline (List.map string - ( [ "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) @@ -2304,22 +2311,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 = + ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (static ()); + "{"; + " 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 @@ -2336,3 +2353,10 @@ 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 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..b10e53d3 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -88,15 +88,8 @@ 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 - +val opt_branch_coverage : bool ref + (** Optimization flags *) val optimize_primops : bool ref @@ -108,3 +101,5 @@ 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 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..d5015318 --- /dev/null +++ b/src/jib/c_codegen.ml @@ -0,0 +1,1714 @@ +(**************************************************************************) +(* 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 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) = + 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 = { + (** 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_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, 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 + 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 Options = sig + val opts : codegen_options +end + +module Make(O: Options) = struct + +let mangle str = + let mangled = Util.zencode_string str in + match StringMap.find_opt mangled O.opts.exports_mangled with + | Some export -> export + | None -> mangled + +let sgen_id id = + match Bindings.find_opt id O.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 " ^ 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 + | 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" + | 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 -> mangle ("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 -> 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" + | 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 -> + 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" + | 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_" ^ sgen_uid (ctor, unifiers) + | V_struct (fields, _) -> + sprintf "{%s}" + (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) + (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 fname, is_extern = + if special_extern then + (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", true) + else + (sgen_function_uid f, false) + in + let sail_state_arg = + if is_extern && StringSet.mem fname O.opts.state_primops then + "sail_state *state, " + else + "" + 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%s);" (sgen_clexp_pure ctx x) fname sail_state_arg (extra_arguments is_extern) c_args + else + 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 + | 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 + +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 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 + 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 + )) + ^^ concat_map (fun str -> string (" " ^ str) ^^ hardline) O.opts.extra_state + ^^ 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 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 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 + + let stdlib_headers = + string "#include <stdint.h>" ^^ hardline + ^^ string "#include <stdbool.h>" + 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 ^^ 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 + ^^ 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\"" (Filename.basename 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 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\"" (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 + 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_initialize(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_finalize(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_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_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 (List.map string + [ "int main(int argc, char *argv[])"; + "{"; + " return model_main(argc, argv);"; + "}" ]) + in + + let emu = + 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 + +end diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 34477967..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,11 +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 @@ -190,6 +191,59 @@ 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 coverage_branch_count = ref 0 + +let coverage_loc_args l = + match Reporting.simp_loc l with + | None -> None + | Some (p1, p2) -> + Some (Printf.sprintf "\"%s\", %d, %d, %d, %d" + (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 + incr coverage_branch_count; + branch_id, + if C.branch_coverage then + begin match coverage_loc_args l with + | None -> [] + | 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 -> + 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 @@ -201,13 +255,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 +572,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 @@ -624,6 +676,10 @@ 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 let compile_case (apat, guard, body) = @@ -643,7 +699,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 + @ (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 if is_dead_aexp body then @@ -651,7 +709,9 @@ 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 + @ (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], @@ -664,8 +724,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 +745,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))), [] @@ -709,16 +768,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. *) @@ -778,7 +840,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 +854,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 +863,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 @@ -948,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 @@ -1057,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 []) @@ -1258,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 @@ -1302,7 +1365,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..47ca6962 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -61,11 +61,15 @@ 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 + 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 @@ -96,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 @@ -108,6 +112,12 @@ module type Config = sig val struct_value : bool (** Allow real literals *) 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_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 310a38a5..26509a69 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -345,7 +345,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) @@ -1405,8 +1405,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 | [] -> [] @@ -1418,7 +1418,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 @@ -1581,9 +1581,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 @@ -1897,7 +1899,7 @@ let smt_instr ctx = | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) -> begin match id, cval 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))] | _, V_lit (VL_undefined, _) -> @@ -1959,7 +1961,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 @@ -2145,7 +2147,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 @@ -2169,7 +2171,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 @@ -2191,7 +2193,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 @@ -2325,7 +2327,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; @@ -2351,7 +2353,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/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 |