diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/c_backend.ml | 22 | ||||
| -rw-r--r-- | src/jib/c_backend.mli | 1 | ||||
| -rw-r--r-- | src/sail.ml | 3 |
3 files changed, 17 insertions, 9 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index cb02d17d..d21d219c 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -86,6 +86,7 @@ let optimize_primops = ref false let optimize_hoist_allocations = ref false let optimize_struct_updates = ref false let optimize_alias = ref false +let optimize_int128 = ref false let c_debug str = if !c_verbosity > 0 then prerr_endline (Lazy.force str) else () @@ -192,7 +193,9 @@ let rec ctyp_of_typ ctx typ = let rec is_stack_ctyp ctyp = match ctyp with | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true | CT_fint n -> n <= 64 - | CT_lbits _ | CT_lint | CT_real | CT_string | CT_list _ | CT_vector _ -> false + | CT_lint when !optimize_int128 -> true + | CT_lint -> false + | CT_lbits _ | CT_real | CT_string | CT_list _ | CT_vector _ -> false | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *) | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps @@ -1493,6 +1496,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | CT_unit -> "UNIT", [] | CT_bit -> "UINT64_C(0)", [] | CT_fint _ -> "INT64_C(0xdeadc0de)", [] + | CT_lint when !optimize_int128 -> "((sail_int) 0xdeadc0de)", [] | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] | CT_sbits _ -> "undefined_sbits()", [] | CT_bool -> "false", [] @@ -1898,8 +1902,8 @@ let codegen_vector ctx (direction, ctyp) = ^^ string "}" in let vector_update = - string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, mpz_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) - ^^ string " int m = mpz_get_ui(n);\n" + string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, sail_int n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string " int m = sail_int_get_ui(n);\n" ^^ string " if (rop->data == op.data) {\n" ^^ string (if is_stack_ctyp ctyp then " rop->data[m] = elem;\n" @@ -1924,13 +1928,13 @@ let codegen_vector ctx (direction, ctyp) = in let vector_access = if is_stack_ctyp ctyp then - string (Printf.sprintf "static %s vector_access_%s(%s op, mpz_t n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id)) - ^^ string " int m = mpz_get_ui(n);\n" + string (Printf.sprintf "static %s vector_access_%s(%s op, sail_int n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id)) + ^^ string " int m = sail_int_get_ui(n);\n" ^^ string " return op.data[m];\n" ^^ string "}" else - string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, mpz_t n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) - ^^ string " int m = mpz_get_ui(n);\n" + string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, sail_int n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) + ^^ string " int m = sail_int_get_ui(n);\n" ^^ string (Printf.sprintf " COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp)) ^^ string "}" in @@ -1946,8 +1950,8 @@ let codegen_vector ctx (direction, ctyp) = ^^ string "}" in let vector_undefined = - string (Printf.sprintf "static void undefined_vector_%s(%s *rop, mpz_t len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) - ^^ string (Printf.sprintf " rop->len = mpz_get_ui(len);\n") + string (Printf.sprintf "static void undefined_vector_%s(%s *rop, sail_int len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf " rop->len = sail_int_get_ui(len);\n") ^^ string (Printf.sprintf " rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) ^^ string " for (int i = 0; i < (rop->len); i++) {\n" ^^ string (if is_stack_ctyp ctyp then diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index 3e8c426b..4628691d 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -100,6 +100,7 @@ val optimize_primops : bool ref val optimize_hoist_allocations : bool ref val optimize_struct_updates : bool ref val optimize_alias : bool ref +val optimize_int128 : bool ref (** Convert a typ to a IR ctyp *) val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp diff --git a/src/sail.ml b/src/sail.ml index 3c277fab..c2b2ed65 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -196,6 +196,9 @@ let options = Arg.align ([ ( "-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " apply constant folding optimizations"); + ( "-Oint128", + Arg.Set C_backend.optimize_int128, + " use 128-bit integers rather than GMP arbitrary precision integers"); ( "-Oaarch64_fast", Arg.Set Jib_compile.optimize_aarch64_fast_struct, " apply ARMv8.5 specific optimizations (potentially unsound in general)"); |