summaryrefslogtreecommitdiff
path: root/src/c_backend.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/c_backend.ml')
-rw-r--r--src/c_backend.ml86
1 files changed, 73 insertions, 13 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 65702764..a8063740 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -66,6 +66,7 @@ let opt_debug_function = ref ""
let opt_trace = ref false
let opt_static = ref false
let opt_no_main = ref false
+let opt_memo_cache = ref false
(* Optimization flags *)
let optimize_primops = ref false
@@ -150,7 +151,7 @@ let rec ctyp_of_typ ctx typ =
when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
CT_int64
| n, m when ctx.optimize_z3 ->
- if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then
+ if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then
CT_int64
else
CT_int
@@ -171,7 +172,7 @@ let rec ctyp_of_typ ctx typ =
let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
begin match nexp_simp n with
| Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
- | n when ctx.optimize_z3 && prove ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
+ | n when ctx.optimize_z3 && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction
| _ -> CT_lbits direction
end
@@ -541,7 +542,7 @@ let analyze_primop' ctx id args typ =
| Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 ->
AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
- | n, m when prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) ->
+ | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) ->
AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64))
| _ -> no_change
end
@@ -1390,18 +1391,20 @@ and compile_block ctx = function
it returns a ctypdef * ctx pair. **)
let compile_type_def ctx (TD_aux (type_def, _)) =
match type_def with
- | TD_enum (id, _, ids, _) ->
+ | TD_enum (id, ids, _) ->
CTD_enum (id, ids),
{ ctx with enums = Bindings.add id (IdSet.of_list ids) ctx.enums }
- | TD_record (id, _, _, ctors, _) ->
+ | TD_record (id, _, ctors, _) ->
let ctors = List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ ctx typ) ctors) Bindings.empty ctors in
CTD_struct (id, Bindings.bindings ctors),
{ ctx with records = Bindings.add id ctors ctx.records }
- | TD_variant (id, _, _, tus, _) ->
+ | TD_variant (id, typq, tus, _) ->
let compile_tu = function
- | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id
+ | Tu_aux (Tu_ty_id (typ, id), _) ->
+ let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in
+ ctyp_of_typ ctx typ, id
in
let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in
CTD_variant (id, Bindings.bindings ctus),
@@ -1623,8 +1626,42 @@ let fix_destructure fail_label = function
let letdef_count = ref 0
(** Compile a Sail toplevel definition into an IR definition **)
-let rec compile_def ctx = function
- | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) ->
+let rec compile_def n total ctx def =
+ match def with
+ | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), _))
+ when !opt_memo_cache ->
+ let digest =
+ def |> Pretty_print_sail.doc_def |> Pretty_print_sail.to_string |> Digest.string
+ in
+ let cachefile = Filename.concat "_sbuild" ("ccache" ^ Digest.to_hex digest) in
+ let cached =
+ if Sys.file_exists cachefile then
+ let in_chan = open_in cachefile in
+ try
+ let compiled = Marshal.from_channel in_chan in
+ close_in in_chan;
+ Some (compiled, ctx)
+ with
+ | _ -> close_in in_chan; None
+ else
+ None
+ in
+ begin match cached with
+ | Some (compiled, ctx) ->
+ Util.progress "Compiling " (string_of_id id) n total;
+ compiled, ctx
+ | None ->
+ let compiled, ctx = compile_def' n total ctx def in
+ let out_chan = open_out cachefile in
+ Marshal.to_channel out_chan compiled [Marshal.Closures];
+ close_out out_chan;
+ compiled, ctx
+ end
+
+ | _ -> compile_def' n total ctx def
+
+and compile_def' n total ctx = function
+ | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) ->
[CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx
| DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
let aexp = analyze_functions ctx analyze_primop (c_literals ctx (no_shadow IdSet.empty (anf exp))) in
@@ -1645,6 +1682,8 @@ let rec compile_def ctx = function
| DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
c_debug (lazy ("Compiling function " ^ string_of_id id));
+ Util.progress "Compiling " (string_of_id id) n total;
+
(* Find the function's type. *)
let quant, Typ_aux (fn_typ, _) =
try Env.get_val_spec id ctx.local_env
@@ -1761,9 +1800,12 @@ let rec compile_def ctx = function
(* Only the parser and sail pretty printer care about this. *)
| DEF_fixity _ -> [], ctx
+ (* We just ignore any pragmas we don't want to deal with. *)
+ | DEF_pragma _ -> [], ctx
+
| DEF_internal_mutrec fundefs ->
let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in
- List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs
+ List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs
| def ->
c_error ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def))
@@ -3321,7 +3363,10 @@ let bytecode_ast ctx rewrites (Defs defs) =
let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in
let ctx = { ctx with tc_env = snd (Type_error.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 total = List.length defs in
+ let _, chunks, ctx =
+ List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs
+ in
let cdefs = List.concat (List.rev chunks) in
rewrites cdefs
@@ -3362,8 +3407,23 @@ let compile_ast ctx c_includes (Defs defs) =
let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in
let ctx = { ctx with tc_env = snd (Type_error.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
+
+ if !opt_memo_cache then
+ (try
+ if Sys.is_directory "_sbuild" then
+ ()
+ else
+ raise (Reporting.err_general Parse_ast.Unknown "_sbuild exists, but is a file not a directory!")
+ with
+ | Sys_error _ -> Unix.mkdir "_sbuild" 0o775)
+ else ();
+
+ let total = List.length defs in
+ let _, chunks, ctx =
+ List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs
+ in
let cdefs = List.concat (List.rev chunks) in
+
let cdefs, ctx = specialize_variants ctx [] cdefs in
let cdefs = sort_ctype_defs cdefs in
let cdefs = optimize ctx cdefs in
@@ -3460,4 +3520,4 @@ let compile_ast ctx c_includes (Defs defs) =
^^ model_main)
|> print_endline
with
- Type_error (l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
+ Type_error (_, l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:15:47 +0000