diff options
| -rw-r--r-- | src/c_backend.ml | 18 | ||||
| -rw-r--r-- | src/constant_fold.ml | 34 | ||||
| -rw-r--r-- | src/sail.ml | 3 |
3 files changed, 51 insertions, 4 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index d14b5391..925c7fd9 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -499,7 +499,7 @@ let analyze_primop' ctx id args typ = AE_val (AV_C_fragment (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true))) | _ -> no_change end - + | "sign_extend", [AV_C_fragment (v1, _, CT_fbits (n, _)); _] -> begin match destruct_vector ctx.tc_env typ with | Some (Nexp_aux (Nexp_constant m, _), _, Typ_aux (Typ_id id, _)) @@ -515,9 +515,19 @@ let analyze_primop' ctx id args typ = AE_val (AV_C_fragment (F_call ("fast_sign_extend2", [v1; v_int (Big_int.to_int m)]) , typ, CT_fbits (Big_int.to_int m, true))) | _ -> no_change end - + + | "add_bits", [AV_C_fragment (v1, _, CT_fbits (n, ord)); AV_C_fragment (v2, _, CT_fbits _)] + when n <= 63 -> + AE_val (AV_C_fragment (F_op (F_op (v1, "+", v2), "&", v_mask_lower n), typ, CT_fbits (n, ord))) + + | "lteq", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, "<=", v2), typ, CT_bool)) | "gteq", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> AE_val (AV_C_fragment (F_op (v1, ">=", v2), typ, CT_bool)) + | "lt", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, "<", v2), typ, CT_bool)) + | "gt", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, ">", v2), typ, CT_bool)) | "xor_bits", [AV_C_fragment (v1, _, (CT_fbits _ as ctyp)); AV_C_fragment (v2, _, CT_fbits _)] -> AE_val (AV_C_fragment (F_op (v1, "^", v2), typ, ctyp)) @@ -608,7 +618,7 @@ let analyze_primop' ctx id args typ = AE_val (AV_C_fragment (F_call ("fast_signed", [frag; v_int (Big_int.to_int n)]), typ, ctyp_of_typ ctx typ)) | _ -> no_change end - + | "add_int", [AV_C_fragment (op1, _, _); AV_C_fragment (op2, _, _)] -> begin match destruct_range Env.empty typ with | None -> no_change @@ -638,7 +648,7 @@ let analyze_primop' ctx id args typ = AV_C_fragment (lo, _, CT_fint 64); AV_C_fragment (ys, _, CT_fbits (m, true))] -> AE_val (AV_C_fragment (F_call ("fast_update_subrange", [xs; hi; lo; ys]), typ, CT_fbits (n, true))) - + | "undefined_bool", _ -> AE_val (AV_C_fragment (F_lit (V_bool false), typ, CT_bool)) diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 6ad1f663..0ede2401 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -62,6 +62,9 @@ let optimize_constant_fold = ref false let rec fexp_of_ctor (field, value) = FE_aux (FE_Fexp (mk_id field, exp_of_value value), no_annot) +(* The interpreter will return a value for each folded expression, so + we must convert that back to expression to re-insert it in the AST + *) and exp_of_value = let open Value in function @@ -107,6 +110,32 @@ let safe_primops = "Elf_loader.elf_tohost" ] +(** We can specify a list of identifiers that we want to remove from + the final AST here. This is useful for removing tracing features in + optimized builds, e.g. for booting an OS as fast as possible. + + Basically we just do this by mapping + + f(x, y, z) -> () + + when f is in the list of identifiers to be mapped to unit. The + advantage of doing it like this is if x, y, and z are + computationally expensive then we remove them also. String + concatentation is very expensive at runtime so this is something we + really want when cutting out tracing features. Obviously it's + important that they don't have any meaningful side effects, and + that f does actually have type unit. +*) +let opt_fold_to_unit = ref [] + +let fold_to_unit id = + let remove = + !opt_fold_to_unit + |> List.map mk_id + |> List.fold_left (fun m id -> IdSet.add id m) IdSet.empty + in + IdSet.mem id remove + let rec is_constant (E_aux (e_aux, _)) = match e_aux with | E_lit _ -> true @@ -177,6 +206,11 @@ let rec rewrite_constant_function_calls' ast = let rw_funcall e_aux annot = match e_aux with + (* + | E_app (id, args) when fold_to_unit id -> + ok (); E_aux (E_lit (L_aux (L_unit, Parse_ast.Unknown)), annot) + *) + | E_app (id, args) when List.for_all is_constant args -> evaluate e_aux annot diff --git a/src/sail.ml b/src/sail.ml index eb81a0ee..aad7097f 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -155,6 +155,9 @@ let options = Arg.align ([ ( "-c_specialize", Arg.Set opt_specialize_c, " specialize integer arguments in C output"); + ( "-c_fold_unit", + Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str), + " remove comma separated list of functions from C output, replacing them with unit"); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); |