diff options
| -rw-r--r-- | lib/sail.c | 11 | ||||
| -rw-r--r-- | lib/sail.h | 4 | ||||
| -rw-r--r-- | src/c_backend.ml | 22 |
3 files changed, 33 insertions, 4 deletions
@@ -134,6 +134,12 @@ void concat_str(sail_string *stro, const sail_string str1, const sail_string str /* ***** Sail integers ***** */ +inline +bool EQUAL(mach_int)(const mach_int op1, const mach_int op2) +{ + return op1 == op2; +} + #ifndef USE_INT128 inline @@ -341,6 +347,11 @@ void pow2(sail_int *rop, const sail_int exp) { /* ***** Sail bitvectors ***** */ +bool EQUAL(mach_bits)(const mach_bits op1, const mach_bits op2) +{ + return op1 == op2; +} + void CREATE(sail_bits)(sail_bits *rop) { rop->bits = malloc(sizeof(mpz_t)); @@ -82,6 +82,8 @@ void concat_str(sail_string *stro, const sail_string str1, const sail_string str typedef int64_t mach_int; +bool EQUAL(mach_int)(const mach_int, const mach_int); + /* * Integers can be either stack-allocated as 128-bit integers if * __int128 is available, or use GMP arbitrary precision @@ -165,6 +167,8 @@ typedef uint64_t mach_bits; bool eq_bit(const mach_bits a, const mach_bits b); +bool EQUAL(mach_bits)(const mach_bits, const mach_bits); + typedef struct { mp_bitcnt_t len; mpz_t *bits; diff --git a/src/c_backend.ml b/src/c_backend.ml index 6097e996..09501ce9 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -2121,10 +2121,7 @@ let codegen_type_def ctx = function in let codegen_eq = let codegen_eq_test (id, ctyp) = - if is_stack_ctyp ctyp then - string (Printf.sprintf "op1.%s == op2.%s" (sgen_id id) (sgen_id id)) - else - string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id)) + string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id)) in string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2)" (sgen_id id) (sgen_id id) (sgen_id id)) ^^ space @@ -2245,6 +2242,21 @@ let codegen_type_def ctx = function ^^ each_ctor "op." set_field tus) rbrace in + let codegen_eq = + let codegen_eq_test ctor_id ctyp = + string (Printf.sprintf "return EQUAL(%s)(op1.%s, op2.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id)) + in + let rec codegen_eq_tests = function + | [] -> string "return false;" + | (ctor_id, ctyp) :: ctors -> + string (Printf.sprintf "if (op1.kind == Kind_%s && op2.kind == Kind_%s) " (sgen_id ctor_id) (sgen_id ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (codegen_eq_test ctor_id ctyp) + ^^ hardline ^^ rbrace ^^ string " else " ^^ codegen_eq_tests ctors + in + let n = sgen_id id in + string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2) " n n n) + ^^ surround 2 0 lbrace (codegen_eq_tests tus) rbrace + in string (Printf.sprintf "// union %s" (string_of_id id)) ^^ hardline ^^ string "enum" ^^ space ^^ string ("kind_" ^ sgen_id id) ^^ space @@ -2272,6 +2284,8 @@ let codegen_type_def ctx = function ^^ twice hardline ^^ codegen_setter ^^ twice hardline + ^^ codegen_eq + ^^ twice hardline ^^ separate_map (twice hardline) codegen_ctor tus (* If this is the exception type, then we setup up some global variables to deal with exceptions. *) ^^ if string_of_id id = "exception" then |