From 5056bf80156738b3ed146ae052f751fa703fecad Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 14 Oct 2019 19:55:08 +0100 Subject: Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and bitvectors in C Assumes a Sail C library that has functions with the right types to support this. Currently lib/int128 supports the -Ofixed_int option, which was previously -Oint128. Add a version of Sail C library that can be built with -nostdlib and -ffreestanding, assuming the above options. Currently just a header file without any implementation, but with the right types --- lib/nostd/sail.h | 341 ++++++++++++++++++++++++++++++++++++++++++++++++++ lib/sail.c | 36 +++--- lib/sail.h | 10 ++ src/isail.ml | 5 + src/jib/c_backend.ml | 44 ++++--- src/jib/c_backend.mli | 5 +- src/jib/jib_util.ml | 2 +- src/sail.ml | 9 +- src/slice.ml | 10 ++ 9 files changed, 421 insertions(+), 41 deletions(-) create mode 100644 lib/nostd/sail.h diff --git a/lib/nostd/sail.h b/lib/nostd/sail.h new file mode 100644 index 00000000..52318a61 --- /dev/null +++ b/lib/nostd/sail.h @@ -0,0 +1,341 @@ +#ifndef __SAIL_LIB +#define __SAIL_LIB + +#include +#include +#include + +void *sail_malloc(size_t); +void sail_free(void *); + +void sail_match_failure(char *message); + +/* + * The Sail compiler expects functions to follow a specific naming + * convention for allocation, deallocation, and (deep)-copying. These + * macros implement this naming convention. + */ +#define CREATE(type) create_ ## type +#define RECREATE(type) recreate_ ## type +#define CREATE_OF(type1, type2) create_ ## type1 ## _of_ ## type2 +#define RECREATE_OF(type1, type2) recreate_ ## type1 ## _of_ ## type2 +#define CONVERT_OF(type1, type2) convert_ ## type1 ## _of_ ## type2 +#define COPY(type) copy_ ## type +#define KILL(type) kill_ ## type +#define UNDEFINED(type) undefined_ ## type +#define EQUAL(type) eq_ ## type + +#define SAIL_BUILTIN_TYPE(type)\ + void create_ ## type(type *);\ + void recreate_ ## type(type *);\ + void copy_ ## type(type *, const type);\ + void kill_ ## type(type *); + +/* ***** Sail unit type ***** */ + +typedef int unit; + +#define UNIT 0 + +unit UNDEFINED(unit)(const unit); +bool EQUAL(unit)(const unit, const unit); + +unit skip(const unit); +unit sail_exit(const unit); + +/* ***** Sail booleans ***** */ + +/* + * and_bool and or_bool are special-cased by the compiler to ensure + * short-circuiting evaluation. + */ +bool not(const bool); +bool EQUAL(bool)(const bool, const bool); +bool UNDEFINED(bool)(const unit); + +/* ***** Sail strings ***** */ + +/* + * Sail strings are just C strings. + */ +typedef char *sail_string; + +SAIL_BUILTIN_TYPE(sail_string); + +void undefined_string(sail_string *str, const unit u); + +bool eq_string(const sail_string, const sail_string); +bool EQUAL(sail_string)(const sail_string, const sail_string); + +void concat_str(sail_string *stro, const sail_string str1, const sail_string str2); +bool string_startswith(sail_string s, sail_string prefix); + +unit sail_assert(bool, sail_string); + +/* ***** Sail integers ***** */ + +typedef int64_t mach_int; + +bool EQUAL(mach_int)(const mach_int, const mach_int); + +typedef __int128 sail_int; + +uint64_t sail_int_get_ui(const sail_int); + +void dec_str(sail_string *str, const sail_int n); +void hex_str(sail_string *str, const sail_int n); + +#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__) + +// SAIL_BUILTIN_TYPE(sail_int); + +sail_int CREATE_OF(sail_int, mach_int)(const mach_int); +mach_int CREATE_OF(mach_int, sail_int)(const sail_int); + +mach_int CONVERT_OF(mach_int, sail_int)(const sail_int); +sail_int CONVERT_OF(sail_int, mach_int)(const mach_int); +sail_int CONVERT_OF(sail_int, sail_string)(const sail_string); + +/* + * Comparison operators for integers + */ +bool eq_int(const sail_int, const sail_int); +bool EQUAL(sail_int)(const sail_int, const sail_int); + +bool lt(const sail_int, const sail_int); +bool gt(const sail_int, const sail_int); +bool lteq(const sail_int, const sail_int); +bool gteq(const sail_int, const sail_int); + +/* + * Left and right shift for integers + */ +mach_int shl_mach_int(const mach_int, const mach_int); +mach_int shr_mach_int(const mach_int, const mach_int); +SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int); + +/* + * undefined_int and undefined_range can't use the UNDEFINED(TYPE) + * macro, because they're slightly magical. They take extra parameters + * to ensure that no undefined int can violate any type-guaranteed + * constraints. + */ +SAIL_INT_FUNCTION(undefined_int, sail_int, const int); +SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int); + +/* + * Arithmetic operations in integers. We include functions for both + * truncating towards zero, and rounding towards -infinity (floor) as + * fdiv/fmod and tdiv/tmod respectively. + */ +SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(sub_nat, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(ediv_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(emod_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int); +//SAIL_INT_FUNCTION(fdiv_int, sail_int, const sail_int, const sail_int); +//SAIL_INT_FUNCTION(fmod_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(max_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(min_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int); +SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int); +SAIL_INT_FUNCTION(pow_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(pow2, sail_int, const sail_int); + +SAIL_INT_FUNCTION(make_the_value, sail_int, const sail_int); +SAIL_INT_FUNCTION(size_itself_int, sail_int, const sail_int); + +/* ***** Sail bitvectors ***** */ + +typedef uint64_t fbits; + +bool eq_bit(const fbits a, const fbits b); + +bool EQUAL(fbits)(const fbits, const fbits); + +typedef struct { + uint64_t len; + uint64_t bits; +} sbits; + +// For backwards compatability +typedef uint64_t mach_bits; +typedef sbits lbits; + +lbits append_64(const lbits, const uint64_t); + +lbits add_bits_int(const lbits, const sail_int); +lbits sub_bits_int(const lbits, const sail_int); + +lbits UNDEFINED(lbits)(bool); + +lbits vector_subrange_lbits(const lbits, const sail_int, const sail_int); + +lbits vector_update_subrange_lbits(const lbits, const sail_int, const sail_int, const lbits); + +lbits slice(const lbits, const sail_int, const sail_int); + +lbits set_slice(const sail_int, const sail_int, const lbits, const sail_int, const lbits); + +lbits get_slice_int(const sail_int, const sail_int, const sail_int); + +lbits zeros(const sail_int); +lbits zero_extend(const lbits, const sail_int); + +bool eq_bits(const lbits, const lbits); +bool neq_bits(const lbits, const lbits); +lbits not_bits(const lbits); +lbits xor_bits(const lbits, const lbits); +lbits or_bits(const lbits, const lbits); +lbits and_bits(const lbits, const lbits); +lbits add_bits(const lbits, const lbits); +lbits sub_bits(const lbits, const lbits); + +lbits append(const lbits, const lbits); + +lbits replicate_bits(const lbits, const sail_int); + +sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction); +fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction); +sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction); + +/* Bitvector conversions */ + +lbits CONVERT_OF(lbits, fbits)(const fbits, const uint64_t, const bool); +lbits CONVERT_OF(lbits, sbits)(const sbits, const bool); + +fbits CONVERT_OF(fbits, lbits)(const lbits, const bool); +fbits CONVERT_OF(fbits, sbits)(const sbits, const bool); + +sbits CONVERT_OF(sbits, fbits)(const fbits, const uint64_t, const bool); +sbits CONVERT_OF(sbits, lbits)(const lbits, const bool); + +fbits UNDEFINED(fbits)(const unit); + +sbits undefined_sbits(void); + +/* + * Wrapper around >> operator to avoid UB when shift amount is greater + * than or equal to 64. + */ +fbits safe_rshift(const fbits, const fbits); + +fbits fast_zero_extend(const sbits op, const uint64_t n); +fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m); +fbits fast_sign_extend2(const sbits op, const uint64_t m); + +sail_int length_lbits(const lbits op); + +bool eq_bits(const lbits op1, const lbits op2); +bool EQUAL(lbits)(const lbits op1, const lbits op2); +bool neq_bits(const lbits op1, const lbits op2); + +fbits bitvector_access(const lbits op, const sail_int n_mpz); + +sail_int sail_unsigned(const lbits op); +sail_int sail_signed(const lbits op); + +mach_int fast_signed(const fbits, const uint64_t); +mach_int fast_unsigned(const fbits); + +sbits append_sf(const sbits, const fbits, const uint64_t); +sbits append_fs(const fbits, const uint64_t, const sbits); +sbits append_ss(const sbits, const sbits); + +fbits fast_replicate_bits(const fbits shift, const fbits v, const mach_int times); + +sail_int set_slice_int(const sail_int, const sail_int, const sail_int, const lbits); + +fbits fast_update_subrange(const fbits op, + const mach_int n, + const mach_int m, + const fbits slice); + +sbits sslice(const fbits op, const mach_int start, const mach_int len); + +bool eq_sbits(const sbits op1, const sbits op2); +bool neq_sbits(const sbits op1, const sbits op2); +sbits not_sbits(const sbits op); +sbits xor_sbits(const sbits op1, const sbits op2); +sbits or_sbits(const sbits op1, const sbits op2); +sbits and_sbits(const sbits op1, const sbits op2); +sbits add_sbits(const sbits op1, const sbits op2); +sbits sub_sbits(const sbits op1, const sbits op2); + +/* ***** Sail reals ***** */ + +typedef double real; + +SAIL_BUILTIN_TYPE(real); + +void CREATE_OF(real, sail_string)(real *rop, const sail_string op); +void CONVERT_OF(real, sail_string)(real *rop, const sail_string op); + +void UNDEFINED(real)(real *rop, unit u); + +void neg_real(real *rop, const real op); + +void mult_real(real *rop, const real op1, const real op2); +void sub_real(real *rop, const real op1, const real op2); +void add_real(real *rop, const real op1, const real op2); +void div_real(real *rop, const real op1, const real op2); + +void sqrt_real(real *rop, const real op); +void abs_real(real *rop, const real op); + +SAIL_INT_FUNCTION(round_up, sail_int, const real); +SAIL_INT_FUNCTION(round_down, sail_int, const real); + +void to_real(real *rop, const sail_int op); + +bool EQUAL(real)(const real op1, const real op2); + +bool lt_real(const real op1, const real op2); +bool gt_real(const real op1, const real op2); +bool lteq_real(const real op1, const real op2); +bool gteq_real(const real op1, const real op2); + +void real_power(real *rop, const real base, const sail_int exp); + +unit print_real(const sail_string, const real); +unit prerr_real(const sail_string, const real); + +void random_real(real *rop, unit); + +/* ***** String utilities ***** */ + +SAIL_INT_FUNCTION(string_length, sail_int, sail_string); +void string_drop(sail_string *dst, sail_string s, sail_int len); +void string_take(sail_string *dst, sail_string s, sail_int len); + +/* ***** Printing ***** */ + +void string_of_int(sail_string *str, const sail_int i); +void string_of_lbits(sail_string *str, const lbits op); +void string_of_fbits(sail_string *str, const fbits op); +void decimal_string_of_lbits(sail_string *str, const lbits op); +void decimal_string_of_fbits(sail_string *str, const fbits op); + +unit print_bits(const sail_string str, const lbits op); +unit prerr_bits(const sail_string str, const lbits op); + +unit print(const sail_string str); +unit print_endline(const sail_string str); + +unit prerr(const sail_string str); +unit prerr_endline(const sail_string str); + +unit print_int(const sail_string str, const sail_int op); +unit prerr_int(const sail_string str, const sail_int op); + +unit sail_putchar(const sail_int op); + +/* ***** Misc ***** */ + +sail_int get_time_ns(const unit); + +#endif diff --git a/lib/sail.c b/lib/sail.c index c544c9aa..1753ab8e 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -78,15 +78,15 @@ bool UNDEFINED(bool)(const unit u) { void CREATE(sail_string)(sail_string *str) { - char *istr = (char *) malloc(1 * sizeof(char)); + char *istr = (char *) sail_malloc(1 * sizeof(char)); istr[0] = '\0'; *str = istr; } void RECREATE(sail_string)(sail_string *str) { - free(*str); - char *istr = (char *) malloc(1 * sizeof(char)); + sail_free(*str); + char *istr = (char *) sail_malloc(1 * sizeof(char)); istr[0] = '\0'; *str = istr; } @@ -100,18 +100,18 @@ void COPY(sail_string)(sail_string *str1, const sail_string str2) void KILL(sail_string)(sail_string *str) { - free(*str); + sail_free(*str); } void dec_str(sail_string *str, const mpz_t n) { - free(*str); + sail_free(*str); gmp_asprintf(str, "%Zd", n); } void hex_str(sail_string *str, const mpz_t n) { - free(*str); + sail_free(*str); gmp_asprintf(str, "0x%Zx", n); } @@ -463,7 +463,7 @@ bool EQUAL(fbits)(const fbits op1, const fbits op2) void CREATE(lbits)(lbits *rop) { - rop->bits = malloc(sizeof(mpz_t)); + rop->bits = sail_malloc(sizeof(mpz_t)); rop->len = 0; mpz_init(*rop->bits); } @@ -483,12 +483,12 @@ void COPY(lbits)(lbits *rop, const lbits op) void KILL(lbits)(lbits *rop) { mpz_clear(*rop->bits); - free(rop->bits); + sail_free(rop->bits); } void CREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len, const bool direction) { - rop->bits = malloc(sizeof(mpz_t)); + rop->bits = sail_malloc(sizeof(mpz_t)); rop->len = len; mpz_init_set_ui(*rop->bits, op); } @@ -522,7 +522,7 @@ void RECREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len void CREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction) { - rop->bits = malloc(sizeof(mpz_t)); + rop->bits = sail_malloc(sizeof(mpz_t)); rop->len = op.len; mpz_init_set_ui(*rop->bits, op.bits); } @@ -1477,14 +1477,14 @@ void random_real(real *rop, const unit u) void string_of_int(sail_string *str, const sail_int i) { - free(*str); + sail_free(*str); gmp_asprintf(str, "%Zd", i); } /* asprintf is a GNU extension, but it should exist on BSD */ void string_of_fbits(sail_string *str, const fbits op) { - free(*str); + sail_free(*str); int bytes = asprintf(str, "0x%" PRIx64, op); if (bytes == -1) { fprintf(stderr, "Could not print bits 0x%" PRIx64 "\n", op); @@ -1493,11 +1493,11 @@ void string_of_fbits(sail_string *str, const fbits op) void string_of_lbits(sail_string *str, const lbits op) { - free(*str); + sail_free(*str); if ((op.len % 4) == 0) { gmp_asprintf(str, "0x%*0ZX", op.len / 4, *op.bits); } else { - *str = (char *) malloc((op.len + 3) * sizeof(char)); + *str = (char *) sail_malloc((op.len + 3) * sizeof(char)); (*str)[0] = '0'; (*str)[1] = 'b'; for (int i = 1; i <= op.len; ++i) { @@ -1509,7 +1509,7 @@ void string_of_lbits(sail_string *str, const lbits op) void decimal_string_of_fbits(sail_string *str, const fbits op) { - free(*str); + sail_free(*str); int bytes = asprintf(str, "%" PRId64, op); if (bytes == -1) { fprintf(stderr, "Could not print bits %" PRId64 "\n", op); @@ -1518,7 +1518,7 @@ void decimal_string_of_fbits(sail_string *str, const fbits op) void decimal_string_of_lbits(sail_string *str, const lbits op) { - free(*str); + sail_free(*str); gmp_asprintf(str, "%Z", *op.bits); } @@ -1534,7 +1534,7 @@ void fprint_bits(const sail_string pre, mpz_t buf; mpz_init_set(buf, *op.bits); - char *hex = malloc((op.len / 4) * sizeof(char)); + char *hex = sail_malloc((op.len / 4) * sizeof(char)); for (int i = 0; i < op.len / 4; ++i) { char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30); @@ -1546,7 +1546,7 @@ void fprint_bits(const sail_string pre, fputc(hex[i - 1], stream); } - free(hex); + sail_free(hex); mpz_clear(buf); } else { fputs("0b", stream); diff --git a/lib/sail.h b/lib/sail.h index a79ea295..f5ff0eaa 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -8,6 +8,16 @@ #include +static inline void *sail_malloc(size_t size) +{ + return malloc(size); +} + +static inline void sail_free(void *ptr) +{ + free(ptr); +} + /* * Called by the RTS to initialise and clear any library state. */ diff --git a/src/isail.ml b/src/isail.ml index 88408dcd..bb42804a 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -608,6 +608,11 @@ let handle_input' input = Interactive.ast := ast; interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops; vs_ids := val_spec_ids !Interactive.ast + | ":recheck_types" -> + let ast, env = Type_check.check Type_check.initial_env !Interactive.ast in + Interactive.env := env; + Interactive.ast := ast; + vs_ids := val_spec_ids !Interactive.ast | ":compile" -> let out_name = match !opt_file_out with | None -> "out.sail" diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 52061444..27bab7e4 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -86,7 +86,8 @@ 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 optimize_fixed_int = ref false +let optimize_fixed_bits = ref false let c_debug str = if !c_verbosity > 0 then prerr_endline (Lazy.force str) else () @@ -192,9 +193,11 @@ 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_lint when !optimize_int128 -> true + | CT_lint when !optimize_fixed_int -> true | CT_lint -> false - | CT_lbits _ | CT_real | CT_string | CT_list _ | CT_vector _ -> false + | CT_lbits _ when !optimize_fixed_int -> true + | CT_lbits _ -> false + | 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 @@ -279,6 +282,12 @@ let rec value_of_aval_bit = function | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1 | _ -> assert false +(** Used to make sure the -Ofixed_int and -Ofixed_bits don't interfere + with assumptions made about optimizations in the common case. *) +let rec never_optimize = function + | CT_lbits _ | CT_lint -> true + | _ -> false + let rec c_aval ctx = function | AV_lit (lit, typ) as v -> begin @@ -294,7 +303,7 @@ let rec c_aval ctx = function match lvar with | Local (_, typ) -> let ctyp = ctyp_of_typ ctx typ in - if is_stack_ctyp ctyp then + if is_stack_ctyp ctyp && not (never_optimize ctyp) then begin try (* We need to check that id's type hasn't changed due to flow typing *) @@ -311,9 +320,9 @@ let rec c_aval ctx = function end else v - | Register (_, _, typ) when is_stack_typ ctx typ -> + | Register (_, _, typ) -> let ctyp = ctyp_of_typ ctx typ in - if is_stack_ctyp ctyp then + if is_stack_ctyp ctyp && not (never_optimize ctyp) then AV_cval (V_id (name id, ctyp), typ) else v @@ -1475,11 +1484,12 @@ 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_lint when !optimize_fixed_int -> "((sail_int) 0xdeadc0de)", [] | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] | CT_sbits _ -> "undefined_sbits()", [] + | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits()", [] | CT_bool -> "false", [] - | CT_enum (_, ctor :: _) -> sgen_id ctor, [] + | CT_enum (_, ctor :: _) -> sgen_id ctor, [] | CT_tup ctyps when is_stack_ctyp ctyp -> let gs = ngensym () in let fold (inits, prev) (n, ctyp) = @@ -1791,13 +1801,13 @@ let codegen_list_clear id ctyp = ^^ (if is_stack_ctyp ctyp then empty else string (Printf.sprintf " KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))) ^^ string (Printf.sprintf " KILL(%s)(&(*rop)->tl);\n" (sgen_id id)) - ^^ string " free(*rop);" + ^^ string " sail_free(*rop);" ^^ string "}" let codegen_list_set id ctyp = string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) ^^ string " if (op == NULL) { *rop = NULL; return; };\n" - ^^ string (Printf.sprintf " *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id)) + ^^ string (Printf.sprintf " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id)) ^^ (if is_stack_ctyp ctyp then string " (*rop)->hd = op->hd;\n" else @@ -1814,7 +1824,7 @@ let codegen_list_set id ctyp = let codegen_cons id ctyp = let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) - ^^ string (Printf.sprintf " *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id)) + ^^ string (Printf.sprintf " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id)) ^^ (if is_stack_ctyp ctyp then string " (*rop)->hd = x;\n" else @@ -1861,7 +1871,7 @@ let codegen_vector ctx (direction, ctyp) = string (Printf.sprintf "static void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id)) ^^ string " rop->len = op.len;\n" - ^^ string (Printf.sprintf " rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf " rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) ^^ string " for (int i = 0; i < op.len; i++) {\n" ^^ string (if is_stack_ctyp ctyp then " (rop->data)[i] = op.data[i];\n" @@ -1877,7 +1887,7 @@ let codegen_vector ctx (direction, ctyp) = string " for (int i = 0; i < (rop->len); i++) {\n" ^^ string (Printf.sprintf " KILL(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp)) ^^ string " }\n") - ^^ string " if (rop->data != NULL) free(rop->data);\n" + ^^ string " if (rop->data != NULL) sail_free(rop->data);\n" ^^ string "}" in let vector_update = @@ -1920,7 +1930,7 @@ let codegen_vector ctx (direction, ctyp) = let internal_vector_init = string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id)) ^^ string " rop->len = len;\n" - ^^ string (Printf.sprintf " rop->data = malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf " rop->data = sail_malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp)) ^^ (if not (is_stack_ctyp ctyp) then string " for (int i = 0; i < len; i++) {\n" ^^ string (Printf.sprintf " CREATE(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp)) @@ -1931,7 +1941,7 @@ let codegen_vector ctx (direction, ctyp) = let vector_undefined = 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 (Printf.sprintf " rop->data = sail_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 " (rop->data)[i] = elem;\n" @@ -2181,10 +2191,10 @@ let compile_ast env output_chan c_includes ast = let exn_boilerplate = if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else - ([ " current_exception = malloc(sizeof(struct zexception));"; + ([ " current_exception = sail_malloc(sizeof(struct zexception));"; " CREATE(zexception)(current_exception);" ], [ " KILL(zexception)(current_exception);"; - " free(current_exception);"; + " sail_free(current_exception);"; " if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception\\n\"); exit(EXIT_FAILURE);}" ]) in diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index 4628691d..90e86d70 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -89,7 +89,7 @@ val opt_extra_arguments : string option ref definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the original function to be compiled. Enabled using the -memo flag. Uses Marshal so it's quite picky about the exact version of -b the Sail version. This cache can obviously become stale if the C + the Sail version. This cache can obviously become stale if the C backend changes - it'll load an old version compiled without said changes. *) val opt_memo_cache : bool ref @@ -100,7 +100,8 @@ 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 +val optimize_fixed_int : bool ref +val optimize_fixed_bits : bool ref (** Convert a typ to a IR ctyp *) val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 3326d4ad..48f686f1 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -919,7 +919,7 @@ let rec infer_call op vs = | (Unsigned n | Signed n), _ -> CT_fint n | (Zero_extend n | Sign_extend n), [v] -> begin match cval_ctyp v with - | CT_fbits (_, ord) | CT_sbits (_, ord) | CT_lbits ord -> + | CT_fbits (_, ord) | CT_sbits (_, ord) -> CT_fbits (n, ord) | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Invalid type for zero/sign_extend argument" end diff --git a/src/sail.ml b/src/sail.ml index 21075818..fd13deea 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -209,9 +209,12 @@ 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"); + ( "-Ofixed_int", + Arg.Set C_backend.optimize_fixed_int, + " assume fixed size integers rather than GMP arbitrary precision integers"); + ( "-Ofixed_bits", + Arg.Set C_backend.optimize_fixed_bits, + " assume fixed size bitvectors rather than arbitrary precision bitvectors"); ( "-Oaarch64_fast", Arg.Set Jib_compile.optimize_aarch64_fast_struct, " apply ARMv8.5 specific optimizations (potentially unsound in general)"); diff --git a/src/slice.ml b/src/slice.ml index 427d5913..0011bb4d 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -173,6 +173,15 @@ let add_def_to_graph graph def = IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ) | LEXP_memory (id, _) -> graph := G.add_edge self (Function id) !graph + | LEXP_id id -> + begin match Env.lookup_id id env with + | Register _ -> graph := G.add_edge self (Register id) !graph + | Enum _ -> graph := G.add_edge self (Constructor id) !graph + | _ -> + if IdSet.mem id (Env.get_toplevel_lets env) then + graph := G.add_edge self (Letbind id) !graph + else () + end | _ -> () end; LEXP_aux (lexp_aux, annot) @@ -204,6 +213,7 @@ let add_def_to_graph graph def = E_aux (e_aux, annot) in let rw_exp self = { id_exp_alg with e_aux = (fun (e_aux, annot) -> scan_exp self e_aux annot); + lEXP_aux = (fun (l_aux, annot) -> scan_lexp self l_aux annot); pat_alg = rw_pat self } in let rewriters self = -- cgit v1.2.3