diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 9 | ||||
| -rw-r--r-- | src/jib/jib_ir.ml | 8 | ||||
| -rw-r--r-- | src/jib/jib_smt_fuzz.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 13 |
4 files changed, 13 insertions, 19 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 98ee5bc1..c1f2d24c 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1022,7 +1022,7 @@ let optimize recursive_functions cdefs = let sgen_id id = Util.zencode_string (string_of_id id) let sgen_uid uid = zencode_uid uid -let sgen_name id = string_of_name id +let sgen_name id = string_of_name ~deref_current_exception:true ~zencode:true id let codegen_id id = string (sgen_id id) let codegen_uid id = string (sgen_uid id) @@ -1110,8 +1110,8 @@ let sgen_value = function | VL_string str -> "\"" ^ str ^ "\"" let rec sgen_cval = function - | V_id (id, ctyp) -> string_of_name id - | V_ref (id, _) -> "&" ^ string_of_name id + | V_id (id, ctyp) -> sgen_name id + | V_ref (id, _) -> "&" ^ sgen_name id | V_lit (vl, ctyp) -> sgen_value vl | V_call (op, cvals) -> sgen_call op cvals | V_field (f, field) -> @@ -2182,7 +2182,8 @@ 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 - Jib_interactive.ir := cdefs; + let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in + Jib_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_ir.ml b/src/jib/jib_ir.ml index c5f2b20a..2fdc4b88 100644 --- a/src/jib/jib_ir.ml +++ b/src/jib/jib_ir.ml @@ -244,7 +244,7 @@ let () = let open Interactive in let open Jib_interactive in - (fun arg -> + ArgString ("(val|register)? identifier", fun arg -> Action (fun () -> let is_def id = function | CDEF_fundef (id', _, _, _) -> Id.compare id id' = 0 | CDEF_spec (id', _, _) -> Id.compare id (prepend_id "val " id') = 0 @@ -258,12 +258,12 @@ let () = 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"))); + )) |> Interactive.register_command ~name:"ir" ~help:"Print the ir representation of a toplevel definition"; - (fun file -> + ArgString ("file", fun file -> Action (fun () -> 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"))) + )) |> Interactive.register_command ~name:"dump_ir" ~help:"Dump the ir to a file" diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml index 846d0178..02e70e29 100644 --- a/src/jib/jib_smt_fuzz.ml +++ b/src/jib/jib_smt_fuzz.ml @@ -158,7 +158,7 @@ let fuzz_cdef ctx all_cdefs = function if Env.is_extern id ctx.tc_env "smt" then ( let extern = Env.get_extern id ctx.tc_env "smt" in let typq, (Typ_aux (aux, _) as typ) = Env.get_val_spec id ctx.tc_env in - let istate = initial_state ctx.ast ctx.tc_env Value.primops in + let istate = initial_state ctx.ast ctx.tc_env !Value.primops in let header = smt_header ctx all_cdefs in prerr_endline (Util.("Fuzz: " |> cyan |> clear) ^ string_of_id id ^ " = \"" ^ extern ^ "\" : " ^ string_of_typ typ); diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 13438208..bec4ce75 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -257,8 +257,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) = (* 1. Instruction pretty printer *) (**************************************************************************) - -let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) = +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) -> @@ -377,16 +376,10 @@ let rec string_of_cval = function Printf.sprintf "%s.%s" (string_of_cval f) (string_of_uid 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) + string_of_cval f ^ " is " ^ string_of_uid (ctor, unifiers) | 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)) + string_of_cval f ^ " as " ^ string_of_uid (ctor, unifiers) | V_struct (fields, _) -> Printf.sprintf "{%s}" (Util.string_of_list ", " (fun (field, cval) -> string_of_uid field ^ " = " ^ string_of_cval cval) fields) |