diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 225 | ||||
| -rw-r--r-- | src/sail.ml | 5 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
3 files changed, 220 insertions, 12 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index 3d53b18a..f547d751 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -60,6 +60,9 @@ let opt_ddump_flow_graphs = ref false (* Optimization flags *) let optimize_primops = ref false +let optimize_hoist_allocations = ref false +let optimize_struct_undefined = ref false +let optimize_enum_undefined = ref false let c_debug str = if !c_verbosity > 0 then prerr_endline str else () @@ -82,6 +85,8 @@ let rec string_of_fragment ?zencode:(zencode=true) = function | F_id id when zencode -> Util.zencode_string (string_of_id id) | F_id id -> string_of_id id | F_lit str -> str + | F_call (str, frags) -> + Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags) | F_field (f, field) -> Printf.sprintf "%s.%s" (string_of_fragment' ~zencode:zencode f) field | F_op (f1, op, f2) -> @@ -172,6 +177,7 @@ let rec frag_rename from_id to_id = function | F_lit str -> F_lit str | F_have_exception -> F_have_exception | F_current_exception -> F_current_exception + | F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags) | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2) | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f) | F_field (f, field) -> F_field (frag_rename from_id to_id f, field) @@ -900,7 +906,7 @@ let analyze_primop' ctx id args typ = let no_change = AE_app (id, args, typ) in let args = List.map (c_aval ctx) args in let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in - prerr_endline ("Analysing: " ^ extern ^ Pretty_print_sail.to_string (separate_map (string ", ") pp_aval args)); + (* prerr_endline ("Analysing: " ^ string_of_typ typ ^ " " ^ extern ^ Pretty_print_sail.to_string (separate_map (string ", ") pp_aval args)); *) match extern, args with | "eq_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> @@ -916,11 +922,39 @@ let analyze_primop' ctx id args typ = | "eq_bit", [AV_C_fragment (a, _); AV_C_fragment (b, _)] -> AE_val (AV_C_fragment (F_op (a, "==", b), typ)) + | "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] -> + AE_val (AV_C_fragment (F_op (F_op (F_op (F_lit "1L", "<<", len), "-", F_lit "1L"), "&", F_op (vec, ">>", start)), typ)) + | "undefined_bit", _ -> AE_val (AV_C_fragment (F_lit "0ul", typ)) - | "undefined_bv_t", _ -> - AE_val (AV_C_fragment (F_lit "0ul", typ)) + | "undefined_vector", [AV_C_fragment (len, _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_lit "0ul", typ)) + | _ -> no_change + end + + | "sail_uint", [AV_C_fragment (frag, vtyp)] -> + begin match destruct_vector ctx.tc_env vtyp with + | Some (Nexp_aux (Nexp_constant n, _), _, _) + when Big_int.less_equal n (Big_int.of_int 63) && is_stack_typ ctx typ -> + prerr_endline "Optimizing uint"; (* TODO: Not sure this ever fires *) + AE_val (AV_C_fragment (frag, typ)) + | _ -> no_change + end + + | "replicate_bits", [AV_C_fragment (vec, vtyp); AV_C_fragment (times, _)] -> + begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with + | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _) + when Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_replicate_bits", [F_lit (Big_int.to_string m); vec; times]), typ)) + | _ -> no_change + end + + | "undefined_bool", _ -> + AE_val (AV_C_fragment (F_lit "false", typ)) | _, _ -> no_change @@ -1011,7 +1045,7 @@ let cval_ctyp = function (_, ctyp) -> ctyp let rec map_instrs f (I_aux (instr, aux)) = let instr = match instr with - | I_decl _ | I_alloc _ | I_init _ -> instr + | I_decl _ | I_alloc _ | I_init _ | I_reset _ | I_reinit _ -> instr | I_if (cval, instrs1, instrs2, ctyp) -> I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp) | I_funcall _ | I_convert _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr @@ -1021,10 +1055,12 @@ let rec map_instrs f (I_aux (instr, aux)) = in I_aux (instr, aux) +let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp) + let rec instr_ctyps (I_aux (instr, aux)) = match instr with - | I_decl (ctyp, _) | I_alloc (ctyp, _) | I_clear (ctyp, _) -> [ctyp] - | I_init (ctyp, _, cval) -> [ctyp; cval_ctyp cval] + | I_decl (ctyp, _) | I_alloc (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) -> [ctyp] + | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> [ctyp; cval_ctyp cval] | I_if (cval, instrs1, instrs2, ctyp) -> ctyp :: cval_ctyp cval :: List.concat (List.map instr_ctyps instrs1 @ List.map instr_ctyps instrs2) | I_funcall (_, _, cvals, ctyp) -> @@ -1062,6 +1098,7 @@ let cdef_ctyps ctx = function let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in ret_ctyp :: arg_ctyps @ List.concat (List.map instr_ctyps instrs) + | CDEF_startup (id, instrs) -> List.concat (List.map instr_ctyps instrs) | CDEF_type tdef -> ctype_def_ctyps tdef | CDEF_let (_, bindings, instrs, cleanup) -> List.map snd bindings @@ -1191,6 +1228,10 @@ let is_ct_vector = function | CT_vector _ -> true | _ -> false +let is_ct_struct = function + | CT_struct _ -> true + | _ -> false + let rec chunkify n xs = match Util.take n xs, Util.drop n xs with | xs, [] -> [xs] @@ -1749,7 +1790,6 @@ and compile_block ctx = function (* FIXME: this function is a bit of a hack *) let rec pat_ids (Typ_aux (arg_typ_aux, _) as arg_typ) (P_aux (p_aux, (l, _)) as pat) = - prerr_endline (string_of_typ arg_typ); match p_aux, arg_typ_aux with | P_id id, _ -> [id] | P_tup pats, Typ_tup arg_typs when List.length pats = List.length arg_typs -> @@ -1953,7 +1993,7 @@ let compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in - if string_of_id id = "test" then prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)) else (); + if string_of_id id = "AddWithCarry" then prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)) else (); let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let gs = gensym () in let pat = match pat with @@ -1965,7 +2005,6 @@ let compile_def ctx = function | Typ_fn (arg_typ, ret_typ, _) -> arg_typ, ret_typ | _ -> assert false in - prerr_endline (string_of_id id ^ " : " ^ string_of_ctyp ctyp); if is_stack_ctyp ctyp then let instrs = [idecl ctyp gs] @ setup @ [call (CL_id gs)] @ cleanup @ [ireturn (F_id gs, ctyp)] in let instrs = fix_exception ctx instrs in @@ -2101,6 +2140,7 @@ let rec fragment_deps = function | F_id id -> NS.singleton (G_id id) | F_lit _ -> NS.empty | F_field (frag, _) | F_unary (_, frag) -> fragment_deps frag + | F_call (_, frags) -> List.fold_left NS.union NS.empty (List.map fragment_deps frags) | F_op (frag1, _, frag2) -> NS.union (fragment_deps frag1) (fragment_deps frag2) | F_current_exception -> NS.empty | F_have_exception -> NS.empty @@ -2232,7 +2272,118 @@ let make_dot id graph = close_out out_chan (**************************************************************************) -(* 6. Code generation *) +(* 6. Optimizations *) +(**************************************************************************) + +let clexp_rename from_id to_id = + let rename id = if Id.compare id from_id = 0 then to_id else id in + function + | CL_id id -> CL_id (rename id) + | CL_field (id, field) -> CL_field (rename id, field) + | CL_addr id -> CL_addr (rename id) + | CL_current_exception -> CL_current_exception + | CL_have_exception -> CL_have_exception + +let rec instrs_rename from_id to_id = + let rename id = if Id.compare id from_id = 0 then to_id else id in + let crename = cval_rename from_id to_id in + let irename instrs = instrs_rename from_id to_id instrs in + let lrename = clexp_rename from_id to_id in + function + | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs + | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs + | I_aux (I_alloc (ctyp, id), aux) :: instrs -> I_aux (I_alloc (ctyp, rename id), aux) :: irename instrs + | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs + | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs + | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs + | I_aux (I_funcall (clexp, id, cvals, ctyp), aux) :: instrs -> + I_aux (I_funcall (lrename clexp, rename id, List.map crename cvals, ctyp), aux) :: irename instrs + | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs + | I_aux (I_convert (clexp, ctyp1, id, ctyp2), aux) :: instrs -> + I_aux (I_convert (lrename clexp, ctyp1, rename id, ctyp2), aux) :: irename instrs + | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs + | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs + | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs + | (I_aux ((I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure), _) as instr) :: instrs -> instr :: irename instrs + | [] -> [] + +let hoist_ctyp = function + | CT_mpz | CT_bv _ | CT_struct _ -> true + | _ -> false + +let hoist_counter = ref 0 + +let hoist_id () = + let id = mk_id ("gh#" ^ string_of_int !gensym_counter) in + incr gensym_counter; + id + +let hoist_allocations ctx = function + | CDEF_fundef (function_id, heap_return, args, body) -> + let decls = ref [] in + let rec hoist = function + | (I_aux (I_decl (ctyp, decl_id), _) as decl) :: instrs when hoist_ctyp ctyp -> + let hid = hoist_id () in + let hoist_stop (I_aux (instr, _)) = + match instr with + | I_if _ | I_block _ | I_try_block _ | I_alloc _ | I_init _ | I_clear _ -> true + | _ -> false + in + let rec replace_inits instrs = + match instr_split_at hoist_stop instrs with + | before, I_aux (I_alloc (ctyp, id), aux) :: after when Id.compare id hid = 0 -> + before @ I_aux (I_reset (ctyp, id), aux) :: replace_inits after + | before, I_aux (I_init (ctyp, id, cval), aux) :: after when Id.compare id hid = 0 -> + before @ I_aux (I_reinit (ctyp, id, cval), aux) :: replace_inits after + | before, I_aux (I_clear (ctyp, id), aux) :: after when Id.compare id hid = 0 -> + before @ replace_inits after + + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: after -> + before @ I_aux (I_if (cval, replace_inits then_instrs, replace_inits else_instrs, ctyp), aux) :: replace_inits after + | before, I_aux (I_block instrs, aux) :: after -> + before @ I_aux (I_block (replace_inits instrs), aux) :: replace_inits after + | before, I_aux (I_try_block instrs, aux) :: after -> + before @ I_aux (I_try_block (replace_inits instrs), aux) :: replace_inits after + + | before, instr :: after -> before @ instr :: replace_inits after + | before, [] -> before + in + decls := ialloc ctyp hid :: idecl ctyp hid :: !decls; + let instrs = replace_inits (instrs_rename decl_id hid instrs) in + hoist instrs + + | I_aux (I_block block, aux) :: instrs -> + I_aux (I_block (hoist block), aux) :: hoist instrs + | I_aux (I_try_block block, aux) :: instrs -> + I_aux (I_try_block (hoist block), aux) :: hoist instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (cval, hoist then_instrs, hoist else_instrs, ctyp), aux) :: hoist instrs + + | instr :: instrs -> instr :: hoist instrs + | [] -> [] + in + let body = hoist body in + if !decls = [] then + [CDEF_fundef (function_id, heap_return, args, body)] + else + [CDEF_startup (function_id, List.rev !decls); CDEF_fundef (function_id, heap_return, args, body)] + + | cdef -> [cdef] + +let concatMap f xs = List.concat (List.map f xs) + +let optimize ctx cdefs = + let nothing cdefs = cdefs in + cdefs + |> if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing + +(**************************************************************************) +(* 7. Code generation *) (**************************************************************************) let sgen_id id = Util.zencode_string (string_of_id id) @@ -2377,6 +2528,14 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = (sgen_cval_param cval)) | I_alloc (ctyp, id) -> string (Printf.sprintf " init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + | I_reinit (ctyp, id, cval) -> + string (Printf.sprintf " reinit_%s_of_%s(&%s, %s);" + (sgen_ctyp_name ctyp) + (sgen_ctyp_name (cval_ctyp cval)) + (sgen_id id) + (sgen_cval_param cval)) + | I_reset (ctyp, id) -> + string (Printf.sprintf " reinit_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) (* FIXME: This just covers the cases we see in our specs, need a special conversion code-generator for full generality *) | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 -> @@ -2476,6 +2635,8 @@ let codegen_type_def ctx = function ^^ twice hardline ^^ codegen_init "init" id (ctor_bindings ctors) ^^ twice hardline + ^^ codegen_init "reinit" id (ctor_bindings ctors) + ^^ twice hardline ^^ codegen_init "clear" id (ctor_bindings ctors) ^^ twice hardline ^^ codegen_eq @@ -2786,6 +2947,15 @@ let codegen_vector ctx (direction, ctyp) = ^^ vector_update ^^ twice hardline end +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_id id)) + | _ -> assert false + let codegen_def' ctx = function | CDEF_reg_dec (id, ctyp) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline @@ -2821,6 +2991,18 @@ let codegen_def' ctx = function ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) ^^ hardline in + let instrs = + if !optimize_struct_undefined && is_ct_struct ret_ctyp && Str.string_match (Str.regexp_string "undefined_") (string_of_id id) 0 then + [] + else + instrs + in + let instrs = + if !optimize_enum_undefined && is_ct_enum ret_ctyp && Str.string_match (Str.regexp_string "undefined_") (string_of_id id) 0 then + [] + else + instrs + in function_header ^^ string "{" ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline @@ -2829,6 +3011,15 @@ let codegen_def' ctx = function | CDEF_type ctype_def -> codegen_type_def ctx ctype_def + | CDEF_startup (id, instrs) -> + let startup_header = string (Printf.sprintf "void startup_%s(void)" (sgen_id id)) in + separate_map hardline codegen_decl (List.filter is_decl instrs) + ^^ twice hardline + ^^ startup_header ^^ hardline + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) (List.filter (fun i -> not (is_decl i)) instrs)) ^^ hardline + ^^ string "}" + | CDEF_let (number, bindings, instrs, cleanup) -> let instrs = add_local_labels instrs in separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings @@ -2866,6 +3057,15 @@ let codegen_def ctx def = ^^ concat vectors ^^ codegen_def' ctx def +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 compile_ast ctx (Defs defs) = try let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in @@ -2873,6 +3073,7 @@ let compile_ast ctx (Defs defs) = let ctx = { ctx with tc_env = snd (check ctx.tc_env (Defs [assert_vs; exit_vs])) } in let chunks, ctx = List.fold_left (fun (chunks, ctx) def -> let defs, ctx = compile_def ctx def in defs :: chunks, ctx) ([], ctx) defs in let cdefs = List.concat (List.rev chunks) in + let cdefs = optimize ctx cdefs in let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline @@ -2894,6 +3095,9 @@ let compile_ast ctx (Defs defs) = let letbind_finalizers = List.map (fun n -> Printf.sprintf " kill_letbind_%d();" n) ctx.letbinds in + let startup cdefs = + List.map sgen_startup (List.filter is_cdef_startup cdefs) + in let regs = c_ast_registers cdefs in @@ -2910,6 +3114,7 @@ let compile_ast ctx (Defs defs) = "{"; " setup_library();" ] @ fst exn_boilerplate + @ startup cdefs @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs) @ (if regs = [] then [] else [ " zinitializze_registers(UNIT);" ]) @ letbind_initializers diff --git a/src/sail.ml b/src/sail.ml index b43f7830..0d6069a0 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -91,7 +91,10 @@ let options = Arg.align ([ Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); ( "-O", - Arg.Tuple [Arg.Set C_backend.optimize_primops], + Arg.Tuple [Arg.Set C_backend.optimize_primops; + Arg.Set C_backend.optimize_hoist_allocations; + Arg.Set C_backend.optimize_enum_undefined; + Arg.Set C_backend.optimize_struct_undefined], " turn on optimizations for C compilation"); ( "-lem_ast", Arg.Set opt_print_lem_ast, diff --git a/src/type_check.ml b/src/type_check.ml index acc79933..44310b55 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -988,7 +988,7 @@ let destruct_vector env typ = | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_order o, _); Typ_arg_aux (Typ_arg_typ vtyp, _)] - ), _) when string_of_id id = "vector" -> Some (n1, o, vtyp) + ), _) when string_of_id id = "vector" -> Some (nexp_simp n1, o, vtyp) | typ -> None in destruct_vector' (Env.expand_synonyms env typ) |