diff options
| -rw-r--r-- | src/jib/anf.ml | 5 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 14 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 3 | ||||
| -rw-r--r-- | src/jib/jib_ir.ml | 305 | ||||
| -rw-r--r-- | src/jib/jib_optimize.ml | 22 | ||||
| -rw-r--r-- | src/jib/jib_optimize.mli | 4 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 9 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 10 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 185 | ||||
| -rw-r--r-- | src/sail.ml | 11 |
11 files changed, 371 insertions, 199 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml index dbbb10e0..216c402e 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -378,6 +378,9 @@ let pp_order = function | Ord_aux (Ord_dec, _) -> string "dec" | _ -> assert false (* Order types have been specialised, so no polymorphism in C backend. *) +let pp_id id = + string (string_of_id id) + let rec pp_aexp (AE_aux (aexp, _, _)) = match aexp with | AE_val v -> pp_aval v @@ -465,7 +468,7 @@ and pp_aval = function | AV_tuple avals -> parens (separate_map (comma ^^ space) pp_aval avals) | AV_ref (id, lvar) -> string "ref" ^^ space ^^ pp_lvar lvar (pp_id id) | AV_cval (cval, typ) -> - pp_annot typ (string (string_of_cval cval |> Util.cyan |> Util.clear)) + pp_annot typ (string (Jib_ir.string_of_cval cval |> Util.cyan |> Util.clear)) | AV_vector (avals, typ) -> pp_annot typ (string "[" ^^ separate_map (comma ^^ space) pp_aval avals ^^ string "]") | AV_list (avals, typ) -> diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 3814b864..aceb32de 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2106,7 +2106,6 @@ let codegen_def ctx def = (* 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 - prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); c_error (Printf.sprintf "Found polymorphic types:\n%s\nwhile generating definition." (Util.string_of_list "\n" string_of_ctyp polymorphic_ctyps)) else @@ -2177,6 +2176,7 @@ let compile_ast env output_chan c_includes ast = let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in let cdefs, ctx = jib_of_ast env ast in + Interactive.ir := cdefs; let cdefs = insert_heap_returns Bindings.empty cdefs in let cdefs = optimize recursive_functions cdefs in diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 5e49af7f..23208e4a 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -57,7 +57,6 @@ open Value2 open Anf -let opt_debug_function = ref "" let opt_debug_flow_graphs = ref false let opt_memo_cache = ref false @@ -569,7 +568,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = raise (Reporting.err_general l (Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s" (string_of_id ctor) (string_of_typ variant_typ) - (string_of_cval cval) + (Jib_ir.string_of_cval cval) (string_of_ctyp ctyp))) end @@ -1242,17 +1241,6 @@ let compile_funcl ctx id pat guard exp = let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in - if Id.compare (mk_id !opt_debug_function) id = 0 then - let header = - Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id) - (Util.string_of_list ", " string_of_id (List.map fst compiled_args)) - (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps) - Util.(string_of_ctyp ret_ctyp |> yellow |> clear) - in - prerr_endline (Util.header header (List.length arg_ctyps + 2)); - prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs)) - else (); - if !opt_debug_flow_graphs then begin let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index 70a0b322..1a39e9b6 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -60,9 +60,6 @@ open Type_check (dot) format. *) val opt_debug_flow_graphs : bool ref -(** Print the IR representation of a specific function. *) -val opt_debug_function : string ref - (** This forces all integer struct fields to be represented as int64_t. Specifically intended for the various TLB structs in the ARM v8.5 spec. *) diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml new file mode 100644 index 00000000..1449b070 --- /dev/null +++ b/src/jib/jib_ir.ml @@ -0,0 +1,305 @@ +(**************************************************************************) +(* 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_util +open Value2 +open Printf + +let zencode_id id = Util.zencode_string (string_of_id id) + +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 + | Have_exception n -> + "have_exception" ^ ssa_num n + | Return n -> + "return" ^ ssa_num n + | Current_exception n -> + "current_exception" ^ ssa_num n + +let string_of_value = function + | VL_bits ([], _) -> "empty" + | VL_bits (bs, true) -> Sail2_values.show_bitlist bs + | VL_bits (bs, false) -> Sail2_values.show_bitlist (List.rev bs) + | VL_int i -> Big_int.to_string i + | VL_bool true -> "true" + | VL_bool false -> "false" + | VL_null -> "NULL" + | VL_unit -> "()" + | VL_bit Sail2_values.B0 -> "bitzero" + | VL_bit Sail2_values.B1 -> "bitone" + | VL_bit Sail2_values.BU -> "bitundef" + | VL_real str -> str + | VL_string str -> "\"" ^ str ^ "\"" + +let rec string_of_cval = function + | V_id (id, ctyp) -> string_of_name id + | V_ref (id, _) -> "&" ^ string_of_name id + | V_lit (vl, ctyp) -> string_of_value vl + | V_call (op, cvals) -> + Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals) + | V_field (f, field) -> + Printf.sprintf "%s.%s" (string_of_cval f) field + | V_tuple_member (f, _, n) -> + Printf.sprintf "%s.ztup%d" (string_of_cval f) n + | V_ctor_kind (f, ctor, [], _) -> + string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor) + | V_ctor_kind (f, ctor, unifiers, _) -> + string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers) + | V_ctor_unwrap (ctor, f, [], _) -> + Printf.sprintf "%s as %s" (string_of_cval f) (string_of_id ctor) + | V_ctor_unwrap (ctor, f, unifiers, _) -> + Printf.sprintf "%s as %s" + (string_of_cval f) + (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)) + | V_struct (fields, _) -> + Printf.sprintf "{%s}" + (Util.string_of_list ", " (fun (field, cval) -> zencode_id field ^ " = " ^ string_of_cval cval) fields) + | V_poly (f, _) -> string_of_cval f + +let rec string_of_clexp = function + | CL_id (id, ctyp) -> string_of_name id + | CL_field (clexp, field) -> string_of_clexp clexp ^ "." ^ field + | CL_addr clexp -> string_of_clexp clexp ^ "*" + | CL_tuple (clexp, n) -> string_of_clexp clexp ^ "." ^ string_of_int n + | CL_void -> "void" + | CL_rmw _ -> assert false + +let add_instr n buf indent str = + Buffer.add_string buf (String.make indent ' '); + Buffer.add_string buf str; + Buffer.add_string buf ";\n" + +module Ir_formatter = struct + module type Config = sig + type label + val make_label_map : instr list -> label StringMap.t + val output_label_instr : Buffer.t -> label StringMap.t -> string -> unit + val string_of_label : label -> string + val modify_instrs : instr list -> instr list + val keyword : string -> string + val typ : ctyp -> string + val value : cval -> string + end + + module Make (C : Config) = struct + let rec output_instr n buf indent label_map (I_aux (instr, (_, l))) = + match instr with + | I_decl (ctyp, id) | I_reset (ctyp, id) -> + add_instr n buf indent (string_of_name id ^ " : " ^ C.typ ctyp) + | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> + add_instr n buf indent (string_of_name id ^ " : " ^ C.typ ctyp ^ " = " ^ C.value cval) + | I_clear (ctyp, id) -> + add_instr n buf indent ("!" ^ string_of_name id) + | I_label label -> + C.output_label_instr buf label_map label + | I_jump (cval, label) -> + add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " " ^ C.string_of_label (StringMap.find label label_map)) + | I_goto label -> + add_instr n buf indent (C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map)) + | I_match_failure -> + add_instr n buf indent (C.keyword "failure") + | I_undefined _ -> + add_instr n buf indent (C.keyword "arbitrary") + | I_end _ -> + add_instr n buf indent (C.keyword "end") + | I_copy (clexp, cval) -> + add_instr n buf indent (string_of_clexp clexp ^ " = " ^ C.value cval) + | I_funcall (clexp, false, id, args) -> + add_instr n buf indent (string_of_clexp clexp ^ " = " ^ zencode_id id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")") + | I_funcall (clexp, true, id, args) -> + add_instr n buf indent (string_of_clexp clexp ^ " = $" ^ zencode_id id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")") + | I_return cval -> + add_instr n buf indent (C.keyword "return" ^ " " ^ C.value cval) + | I_comment str -> + Buffer.add_string buf (String.make indent ' ' ^ "/*" ^ str ^ "*/\n") + | I_raw str -> + Buffer.add_string buf str + | I_throw cval -> + add_instr n buf indent (C.keyword "throw" ^ " " ^ C.value cval) + | I_if _ | I_block _ | I_try_block _ -> + Reporting.unreachable Parse_ast.Unknown __POS__ "Can only format flat IR" + + and output_instrs n buf indent label_map = function + | (I_aux (I_label _, _) as instr) :: instrs -> + output_instr n buf indent label_map instr; + output_instrs n buf indent label_map instrs + | instr :: instrs -> + output_instr n buf indent label_map instr; + output_instrs (n + 1) buf indent label_map instrs + | [] -> () + + let id_ctyp (id, ctyp) = + sprintf "%s: %s" (zencode_id id) (C.typ ctyp) + + let output_def buf = function + | CDEF_reg_dec (id, ctyp, _) -> + Buffer.add_string buf (sprintf "%s %s : %s" (C.keyword "register") (zencode_id id) (C.typ ctyp)) + | CDEF_spec (id, ctyps, ctyp) -> + Buffer.add_string buf (sprintf "%s %s : (%s) -> %s" (C.keyword "val") (zencode_id id) (Util.string_of_list ", " C.typ ctyps) (C.typ ctyp)); + | CDEF_fundef (id, ret, args, instrs) -> + let instrs = C.modify_instrs instrs in + let label_map = C.make_label_map instrs in + let ret = match ret with + | None -> "" + | Some id -> " " ^ zencode_id id + in + Buffer.add_string buf (sprintf "%s %s%s(%s) {\n" (C.keyword "fn") (zencode_id id) ret (Util.string_of_list ", " zencode_id args)); + output_instrs 0 buf 2 label_map instrs; + Buffer.add_string buf "}" + | CDEF_type (CTD_enum (id, ids)) -> + Buffer.add_string buf (sprintf "%s %s {\n %s\n}" (C.keyword "enum") (zencode_id id) (Util.string_of_list ",\n " zencode_id ids)) + | CDEF_type (CTD_struct (id, ids)) -> + Buffer.add_string buf (sprintf "%s %s {\n %s\n}" (C.keyword "struct") (zencode_id id) (Util.string_of_list ",\n " id_ctyp ids)) + | CDEF_type (CTD_variant (id, ids)) -> + Buffer.add_string buf (sprintf "%s %s {\n %s\n}" (C.keyword "union") (zencode_id id) (Util.string_of_list ",\n " id_ctyp ids)) + | CDEF_let (_, bindings, instrs) -> + let instrs = C.modify_instrs instrs in + let label_map = C.make_label_map instrs in + Buffer.add_string buf (sprintf "%s (%s) {\n" (C.keyword "let") (Util.string_of_list ", " id_ctyp bindings)); + output_instrs 0 buf 2 label_map instrs; + Buffer.add_string buf "}" + | CDEF_startup _ | CDEF_finish _ -> + Reporting.unreachable Parse_ast.Unknown __POS__ "Unexpected startup / finish" + + let rec output_defs buf = function + | def :: defs -> + output_def buf def; + Buffer.add_string buf "\n\n"; + output_defs buf defs + | [] -> + Buffer.add_char buf '\n' + + end +end + +let colored_ir = ref false + +let with_colors f = + let is_colored = !colored_ir in + colored_ir := true; + f (); + colored_ir := is_colored + +module Flat_ir_config : Ir_formatter.Config = struct + type label = int + + let make_label_map instrs = + let rec make_label_map' n = function + | I_aux (I_label label, _) :: instrs -> + StringMap.add label n (make_label_map' n instrs) + | _ :: instrs -> + make_label_map' (n + 1) instrs + | [] -> StringMap.empty + in + make_label_map' 0 instrs + + let modify_instrs instrs = + let open Jib_optimize in + instrs + |> flatten_instrs + |> remove_clear + |> remove_dead_code + + let string_of_label = string_of_int + + let output_label_instr buf _ label = () + + let color f = + if !colored_ir then + f + else + (fun str -> str) + + let keyword str = + str |> color Util.red |> color Util.clear + + let typ str = + string_of_ctyp str |> color Util.yellow |> color Util.clear + + let value str = + string_of_cval str |> color Util.cyan |> color Util.clear + +end + +module Flat_ir_formatter = Ir_formatter.Make(Flat_ir_config) + +let () = + let open Interactive in + + (fun arg -> + let is_def id = function + | CDEF_fundef (id', _, _, _) -> Id.compare id id' = 0 + | CDEF_spec (id', _, _) -> Id.compare id (prepend_id "val " id') = 0 + | CDEF_reg_dec (id', _, _) -> Id.compare id (prepend_id "register " id') = 0 + | _ -> false + in + let id = mk_id arg in + match List.find_opt (is_def id) !ir with + | None -> print_endline ("Could not find definition " ^ string_of_id id) + | Some cdef -> + let buf = Buffer.create 256 in + with_colors (fun () -> Flat_ir_formatter.output_def buf cdef); + print_endline (Buffer.contents buf) + ) |> Interactive.(register_command ~name:"ir" ~help:(sprintf ":ir %s - Print the ir representation of a toplevel definition" (arg "(val|register)? identifier"))); + + (fun file -> + let buf = Buffer.create 256 in + let out_chan = open_out file in + Flat_ir_formatter.output_defs buf !ir; + output_string out_chan (Buffer.contents buf); + close_out out_chan + ) |> Interactive.(register_command ~name:"dump_ir" ~help:(sprintf ":dump_ir %s - Dump the ir to a file" (arg "file"))) diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml index 0ec92b97..e7cb70da 100644 --- a/src/jib/jib_optimize.ml +++ b/src/jib/jib_optimize.ml @@ -360,6 +360,28 @@ let remove_unused_labels instrs = in go [] instrs + +let remove_dead_after_goto instrs = + let rec go acc = function + | (I_aux (I_goto _, _) as instr) :: instrs -> go_dead (instr :: acc) instrs + | instr :: instrs -> go (instr :: acc) instrs + | [] -> acc + and go_dead acc = function + | (I_aux (I_label _, _) as instr) :: instrs -> go (instr :: acc) instrs + | instr :: instrs -> go acc instrs + | [] -> acc + in + List.rev (go [] instrs) + +let rec remove_dead_code instrs = + let instrs' = + instrs |> remove_unused_labels |> remove_pointless_goto |> remove_dead_after_goto + in + if List.length instrs' < List.length instrs then + remove_dead_code instrs' + else + instrs' + let rec remove_clear = function | I_aux (I_clear _, _) :: instrs -> remove_clear instrs | instr :: instrs -> instr :: remove_clear instrs diff --git a/src/jib/jib_optimize.mli b/src/jib/jib_optimize.mli index d992793c..a69b45b7 100644 --- a/src/jib/jib_optimize.mli +++ b/src/jib/jib_optimize.mli @@ -71,3 +71,7 @@ val remove_clear : instr list -> instr list val remove_pointless_goto : instr list -> instr list val remove_unused_labels : instr list -> instr list + +val remove_dead_after_goto : instr list -> instr list + +val remove_dead_code : instr list -> instr list diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 9fb77055..7a827ece 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -324,7 +324,7 @@ let rec smt_cval ctx cval = end | _ -> assert false end - | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval) + | cval -> failwith ("Unrecognised cval " ^ Jib_ir.string_of_cval cval) let add_event ctx ev smt = let stack = event_stack ctx ev in @@ -1497,8 +1497,7 @@ let rec rmw_write = function | CL_id _ -> assert false | CL_tuple (clexp, _) -> rmw_write clexp | CL_field (clexp, _) -> rmw_write clexp - | clexp -> - failwith (Pretty_print_sail.to_string (pp_clexp clexp)) + | clexp -> assert false let rmw_read = function | CL_rmw (read, _, _) -> zencode_name read @@ -1674,8 +1673,8 @@ let smt_instr ctx = | I_aux ((I_jump _ | I_goto _ | I_end _ | I_match_failure | I_undefined _), (_, l)) -> Reporting.unreachable l __POS__ "SMT: Instruction should only appear as block terminator" - | instr -> - failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr)) + | I_aux (_, (_, l)) -> + Reporting.unreachable l __POS__ "Cannot translate instruction" let smt_cfnode all_cdefs ctx ssa_elems = let open Jib_ssa in diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index 0f0f582e..840dea97 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -722,7 +722,7 @@ let string_of_ssainstr = function | Phi (id, ctyp, args) -> string_of_name id ^ " : " ^ string_of_ctyp ctyp ^ " = φ(" ^ Util.string_of_list ", " string_of_name args ^ ")" | Pi cvals -> - "π(" ^ Util.string_of_list ", " (fun v -> String.escaped (string_of_cval v)) cvals ^ ")" + "π(" ^ Util.string_of_list ", " (fun v -> String.escaped (Jib_ir.string_of_cval v)) cvals ^ ")" let string_of_phis = function | [] -> "" @@ -730,7 +730,13 @@ let string_of_phis = function let string_of_node = function | (phis, CF_label label) -> string_of_phis phis ^ label - | (phis, CF_block (instrs, terminator)) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs + | (phis, CF_block (instrs, terminator)) -> + let string_of_instr instr = + let buf = Buffer.create 128 in + Jib_ir.Flat_ir_formatter.output_instr 0 buf 0 Jib_ir.StringMap.empty instr; + Buffer.contents buf + in + string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (string_of_instr instr)) instrs | (phis, CF_start inits) -> string_of_phis phis ^ "START" | (phis, CF_guard cval) -> string_of_phis phis ^ string_of_int cval diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 48f686f1..4227a436 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -308,56 +308,27 @@ let string_of_op = function | Set_slice -> "@set_slice" | Concat -> "@concat" -let rec string_of_cval = function - | V_id (id, ctyp) -> string_of_name ~zencode:false id - | V_ref (id, _) -> "&" ^ string_of_name ~zencode:false id - | V_lit (vl, ctyp) -> string_of_value vl - | V_call (op, cvals) -> - Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals) - | V_field (f, field) -> - Printf.sprintf "%s.%s" (string_of_cval f) field - | V_tuple_member (f, _, n) -> - Printf.sprintf "%s.ztup%d" (string_of_cval f) n - | V_ctor_kind (f, ctor, [], _) -> - string_of_cval f ^ ".kind" - ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor) - | V_ctor_kind (f, ctor, unifiers, _) -> - string_of_cval f ^ ".kind" - ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers) - | V_ctor_unwrap (ctor, f, [], _) -> - Printf.sprintf "%s.%s" (string_of_cval f) (string_of_id ctor) - | V_struct (fields, _) -> - Printf.sprintf "{%s}" - (Util.string_of_list ", " (fun (field, cval) -> string_of_id field ^ " = " ^ string_of_cval cval) fields) - | V_ctor_unwrap (ctor, f, unifiers, _) -> - Printf.sprintf "%s.%s" - (string_of_cval f) - (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)) - | V_poly (f, _) -> string_of_cval f - (* String representation of ctyps here is only for debugging and intermediate language pretty-printer. *) -and string_of_ctyp = function - | CT_lint -> "int" - | CT_lbits true -> "lbits(dec)" - | CT_lbits false -> "lbits(inc)" - | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)" - | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)" - | CT_sbits (n, true) -> "sbits(" ^ string_of_int n ^ ", dec)" - | CT_sbits (n, false) -> "sbits(" ^ string_of_int n ^ ", inc)" - | CT_fint n -> "int(" ^ string_of_int n ^ ")" - | CT_constant n -> "constant(" ^ Big_int.to_string n ^ ")" - | CT_bit -> "bit" - | CT_unit -> "unit" - | CT_bool -> "bool" - | CT_real -> "real" +let rec string_of_ctyp = function + | CT_lint -> "%i" + | CT_fint n -> "%i" ^ string_of_int n + | CT_lbits _ -> "%lb" + | CT_sbits (n, _) -> "%sb" ^ string_of_int n + | CT_fbits (n, _) -> "%fb" ^ string_of_int n + | CT_constant n -> Big_int.to_string n + | CT_bit -> "%bit" + | CT_unit -> "%unit" + | CT_bool -> "%bool" + | CT_real -> "%real" + | CT_string -> "%string" | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")" - | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id - | CT_string -> "string" - | CT_vector (true, ctyp) -> "vector(dec, " ^ string_of_ctyp ctyp ^ ")" - | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")" - | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")" - | CT_ref ctyp -> "ref(" ^ string_of_ctyp ctyp ^ ")" + | CT_struct (id, _) -> "%struct " ^ Util.zencode_string (string_of_id id) + | CT_enum (id, _) -> "%enum " ^ Util.zencode_string (string_of_id id) + | CT_variant (id, _) -> "%union " ^ Util.zencode_string (string_of_id id) + | CT_vector (_, ctyp) -> "%vec(" ^ string_of_ctyp ctyp ^ ")" + | CT_list ctyp -> "%list(" ^ string_of_ctyp ctyp ^ ")" + | CT_ref ctyp -> "&(" ^ string_of_ctyp ctyp ^ ")" | CT_poly -> "*" (** This function is like string_of_ctyp, but recursively prints all @@ -560,126 +531,6 @@ let rec is_polymorphic = function | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp | CT_poly -> true -let pp_id id = - string (string_of_id id) - -let pp_name id = - string (string_of_name ~zencode:false id) - -let pp_ctyp ctyp = - string (string_of_ctyp ctyp |> Util.yellow |> Util.clear) - -let pp_keyword str = - string ((str |> Util.red |> Util.clear) ^ " ") - -let pp_cval cval = - string (string_of_cval cval) - -let rec pp_clexp = function - | CL_id (id, ctyp) -> pp_name id ^^ string " : " ^^ pp_ctyp ctyp - | CL_rmw (read, write, ctyp) -> - string "rmw" ^^ parens (pp_name read ^^ comma ^^ space ^^ pp_name write) ^^ string " : " ^^ pp_ctyp ctyp - | CL_field (clexp, field) -> parens (pp_clexp clexp) ^^ string "." ^^ string field - | CL_tuple (clexp, n) -> parens (pp_clexp clexp) ^^ string "." ^^ string (string_of_int n) - | CL_addr clexp -> string "*" ^^ pp_clexp clexp - | CL_void -> string "void" - -let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = - match instr with - | I_decl (ctyp, id) -> - pp_keyword "var" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp - | I_if (cval, then_instrs, else_instrs, ctyp) -> - let pp_if_block = function - | [] -> string "{}" - | instrs -> surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - in - parens (pp_ctyp ctyp) ^^ space - ^^ pp_keyword "if" ^^ pp_cval cval - ^^ if short then - empty - else - pp_keyword " then" ^^ pp_if_block then_instrs - ^^ pp_keyword " else" ^^ pp_if_block else_instrs - | I_jump (cval, label) -> - pp_keyword "jump" ^^ pp_cval cval ^^ space ^^ string (label |> Util.blue |> Util.clear) - | I_block instrs -> - surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - | I_try_block instrs -> - pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - | I_reset (ctyp, id) -> - pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp - | I_init (ctyp, id, cval) -> - pp_keyword "create" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval - | I_reinit (ctyp, id, cval) -> - pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval - | I_funcall (x, _, f, args) -> - separate space [ pp_clexp x; string "="; - string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args) ] - | I_copy (clexp, cval) -> - separate space [pp_clexp clexp; string "="; pp_cval cval] - | I_clear (ctyp, id) -> - pp_keyword "kill" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp - | I_return cval -> - pp_keyword "return" ^^ pp_cval cval - | I_throw cval -> - pp_keyword "throw" ^^ pp_cval cval - | I_comment str -> - string ("// " ^ str |> Util.magenta |> Util.clear) - | I_label str -> - string (str |> Util.blue |> Util.clear) ^^ string ":" - | I_goto str -> - pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear) - | I_match_failure -> - pp_keyword "match_failure" - | I_end _ -> - pp_keyword "end" - | I_undefined ctyp -> - pp_keyword "undefined" ^^ pp_ctyp ctyp - | I_raw str -> - pp_keyword "C" ^^ string (str |> Util.cyan |> Util.clear) - -let pp_ctype_def = function - | CTD_enum (id, ids) -> - pp_keyword "enum" ^^ pp_id id ^^ string " = " - ^^ separate_map (string " | ") pp_id ids - | CTD_struct (id, fields) -> - pp_keyword "struct" ^^ pp_id id ^^ string " = " - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) fields) rbrace - | CTD_variant (id, ctors) -> - pp_keyword "union" ^^ pp_id id ^^ string " = " - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) ctors) rbrace - -let pp_cdef = function - | CDEF_spec (id, ctyps, ctyp) -> - pp_keyword "val" ^^ pp_id id ^^ string " : " ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp - ^^ hardline - | CDEF_fundef (id, ret, args, instrs) -> - let ret = match ret with - | None -> empty - | Some id -> space ^^ pp_id id - in - pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_reg_dec (id, ctyp, instrs) -> - pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline - | CDEF_let (n, bindings, instrs) -> - let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in - pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space - ^^ hardline - | CDEF_startup (id, instrs)-> - pp_keyword "startup" ^^ pp_id id ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_finish (id, instrs)-> - pp_keyword "finish" ^^ pp_id id ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - let rec cval_deps = function | V_id (id, _) | V_ref (id, _) -> NameSet.singleton id | V_lit _ -> NameSet.empty diff --git a/src/sail.ml b/src/sail.ml index 81683b4d..da711e8d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -370,9 +370,6 @@ let options = Arg.align ([ ( "-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers"); - ( "-dfunction", - Arg.String (fun f -> Jib_compile.opt_debug_function := f), - " (debug) print debugging output for a single function"); ( "-dprofile", Arg.Set Profile.opt_profile, " (debug) provide basic profiling information for rewriting passes within Sail"); @@ -502,14 +499,14 @@ let target name out_name ast type_envs = (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *) let close, output_chan = match !opt_file_out with - | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".ir.sail")) + | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".ir")) | None -> false, stdout in Reporting.opt_warnings := true; let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in - (* let cdefs = List.map Jib_optimize.flatten_cdef cdefs in *) - let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in - output_string output_chan (str ^ "\n"); + let buf = Buffer.create 256 in + Jib_ir.Flat_ir_formatter.output_defs buf cdefs; + output_string output_chan (Buffer.contents buf); flush output_chan; if close then close_out output_chan else () |