From d96cd3e8d74b303ff89716294d173754c70cd6b7 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 11 Jun 2018 16:01:43 +0100 Subject: More efficient bitfield implementation --- aarch64/Makefile | 2 +- lib/sail.h | 31 ++++++++++++++++++------- mips/main.sail | 5 +++- src/bitfield.ml | 71 +++++++++++++++++++++++++++++++------------------------- src/c_backend.ml | 8 +++++-- 5 files changed, 73 insertions(+), 44 deletions(-) diff --git a/aarch64/Makefile b/aarch64/Makefile index 58281dc7..07bc67ae 100644 --- a/aarch64/Makefile +++ b/aarch64/Makefile @@ -8,7 +8,7 @@ aarch64.c: no_vector.sail $(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c aarch64_c: aarch64.c - gcc -O2 $^ -o aarch64_c -lgmp -L $(SAIL_DIR)/lib + gcc -O2 $^ -o aarch64_c -lgmp -I $(SAIL_DIR)/lib aarch64: no_vector.sail $(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3 diff --git a/lib/sail.h b/lib/sail.h index 99b57d8a..319db18d 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -740,6 +740,17 @@ void set_slice_int(mpz_t *rop, } } +// This is a bit of a hack to let us optimize away the Align__1 +// function in aarch64. +void arm_align(bv_t *rop, const bv_t x_bv, const mpz_t y_mpz) { + uint64_t x = mpz_get_ui(*x_bv.bits); + uint64_t y = mpz_get_ui(y_mpz); + uint64_t z = y * (x / y); + mp_bitcnt_t n = x_bv.len; + mpz_set_ui(*rop->bits, safe_rshift(UINT64_MAX, 64l - (n - 1)) & z); + rop->len = n; +} + void vector_update_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, @@ -765,16 +776,20 @@ void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, const mpz uint64_t n = mpz_get_ui(n_mpz); uint64_t m = mpz_get_ui(m_mpz); - mpz_set_ui(*rop->bits, 0ul); rop->len = n - (m - 1ul); + mpz_fdiv_q_2exp(*rop->bits, *op.bits, m); + normalise_bv_t(rop); - for (uint64_t i = 0; i < rop->len; i++) { - if (mpz_tstbit(*op.bits, i + m)) { - mpz_setbit(*rop->bits, i); - } else { - mpz_clrbit(*rop->bits, i); - } - } + /* mpz_set_ui(*rop->bits, 0ul); */ + /* rop->len = n - (m - 1ul); */ + + /* for (uint64_t i = 0; i < rop->len; i++) { */ + /* if (mpz_tstbit(*op.bits, i + m)) { */ + /* mpz_setbit(*rop->bits, i); */ + /* } else { */ + /* mpz_clrbit(*rop->bits, i); */ + /* } */ + /* } */ } int bitvector_access(const bv_t op, const mpz_t n_mpz) { diff --git a/mips/main.sail b/mips/main.sail index 8b1e01d7..6f7d377e 100644 --- a/mips/main.sail +++ b/mips/main.sail @@ -16,7 +16,7 @@ function fetch_and_execute () = { /* the following skips are required on mips to fake the tag effects otherwise type checker complains */ skip_rmemt(); skip_wmvt(); - prerr_bits("PC: ", PC); + /* prerr_bits("PC: ", PC); */ loop_again = true; try { let pc_pa = TranslatePC(PC); @@ -62,9 +62,12 @@ function dump_mips_state () : unit -> unit = { } } +val "load_raw" : (bits(64), string) -> unit + val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt} function main () = { + load_raw(0x0000000000100000, "/home/aa2019/mips_freebsd/kernel"); init_registers(to_bits(64, elf_entry())); startTime = get_time_ns(); while (fetch_and_execute()) do (); diff --git a/src/bitfield.ml b/src/bitfield.ml index 391a653d..161908cd 100644 --- a/src/bitfield.ml +++ b/src/bitfield.ml @@ -64,62 +64,68 @@ let rec combine = function Defs (defs @ defs') let newtype name size order = - let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in - ast_of_def_string order nt - -(* These functions define the getter and setter for all the bits in the field. *) -let full_getter name size order = - let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in - let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in - combine [ast_of_def_string order fg_val; ast_of_def_string order fg_function] - -let full_setter name size order = - let fs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" name name (bitvec size order) in - let fs_function = String.concat "\n" - [ Printf.sprintf "function _set_%s (r_ref, v) = {" name; - " r = _reg_deref(r_ref);"; - Printf.sprintf " r = Mk_%s(v);" name; - " (*r_ref) = r"; - "}" - ] + let chunks_64 = + Util.list_init (size / 64) (fun i -> Printf.sprintf "%s_chunk_%i : vector(64, %s, bit)" name i (string_of_order order)) in - combine [ast_of_def_string order fs_val; ast_of_def_string order fs_function] - -let full_overload name order = - ast_of_def_string order (Printf.sprintf "overload _mod_bits = {_get_%s, _set_%s}" name name) + let chunks = + if size mod 64 = 0 then chunks_64 else + let chunk_rem = + Printf.sprintf "%s_chunk_%i : vector(%i, %s, bit)" name (List.length chunks_64) (size mod 64) (string_of_order order) + in + chunk_rem :: List.rev chunks_64 + in + let nt = Printf.sprintf "struct %s = {\n %s }" name (Util.string_of_list ",\n " (fun x -> x) chunks) in + ast_of_def_string order nt -let full_accessor name size order = - combine [full_getter name size order; full_setter name size order; full_overload name order] +let rec translate_indices hi lo = + if hi / 64 = lo / 64 then + [(hi / 64, hi mod 64, lo mod 64)] + else + (hi / 64, hi mod 64, 0) :: translate_indices (hi - (hi mod 64 + 1)) lo (* For every index range, create a getter and setter *) let index_range_getter name field order start stop = + let indices = translate_indices start stop in let size = if start > stop then start - (stop - 1) else stop - (start - 1) in let irg_val = Printf.sprintf "val _get_%s_%s : %s -> %s" name field name (bitvec size order) in - let irg_function = Printf.sprintf "function _get_%s_%s Mk_%s(v) = v[%i .. %i]" name field name start stop in + let body (chunk, start, stop) = + Printf.sprintf "v.%s_chunk_%i[%i .. %i]" name chunk start stop + in + let irg_function = Printf.sprintf "function _get_%s_%s v = %s" name field (Util.string_of_list " @ " body indices) in combine [ast_of_def_string order irg_val; ast_of_def_string order irg_function] let index_range_setter name field order start stop = + let indices = translate_indices start stop in let size = if start > stop then start - (stop - 1) else stop - (start - 1) in let irs_val = Printf.sprintf "val _set_%s_%s : (register(%s), %s) -> unit effect {wreg}" name field name (bitvec size order) in (* Read-modify-write using an internal _reg_deref function without rreg effect *) + let body (chunk, hi, lo) = + Printf.sprintf "r.%s_chunk_%i = [ r.%s_chunk_%i with %i .. %i = v[%i .. %i]]" + name chunk name chunk hi lo ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop) + in let irs_function = String.concat "\n" [ Printf.sprintf "function _set_%s_%s (r_ref, v) = {" name field; - Printf.sprintf " r = _get_%s(_reg_deref(r_ref));" name; - Printf.sprintf " r[%i .. %i] = v;" start stop; - Printf.sprintf " (*r_ref) = Mk_%s(r)" name; + " r = _reg_deref(r_ref);"; + Printf.sprintf " %s;" (Util.string_of_list ";\n " body indices); + " (*r_ref) = r"; "}" ] in combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function] let index_range_update name field order start stop = + let indices = translate_indices start stop in let size = if start > stop then start - (stop - 1) else stop - (start - 1) in let iru_val = Printf.sprintf "val _update_%s_%s : (%s, %s) -> %s" name field name (bitvec size order) name in (* Read-modify-write using an internal _reg_deref function without rreg effect *) + let body (chunk, hi, lo) = + Printf.sprintf "let v = { v with %s_chunk_%i = [ v.%s_chunk_%i with %i .. %i = x[%i .. %i]] }" + name chunk name chunk hi lo ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop) + in let iru_function = String.concat "\n" - [ Printf.sprintf "function _update_%s_%s (Mk_%s(v), x) = {" name field name; - Printf.sprintf " Mk_%s([v with %i .. %i = x]);" name start stop; - "}" + [ Printf.sprintf "function _update_%s_%s (v, x) =" name field; + Printf.sprintf " %s in" (Util.string_of_list " in\n " body indices); + " v" ] in let iru_overload = Printf.sprintf "overload update_%s = {_update_%s_%s}" field name field in @@ -142,4 +148,5 @@ let field_accessor name order (id, ir) = index_range_accessor name (string_of_id let macro id size order ranges = let name = string_of_id id in - combine ([newtype name size order; full_accessor name size order] @ List.map (field_accessor name order) ranges) + let ranges = (mk_id "bits", BF_aux (BF_range (Big_int.of_int (size - 1), Big_int.of_int 0), Parse_ast.Unknown)) :: ranges in + combine ([newtype name size order] @ List.map (field_accessor name order) ranges) diff --git a/src/c_backend.ml b/src/c_backend.ml index 06e92f3a..e088b5e5 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -990,6 +990,9 @@ let analyze_primop' ctx env l id args typ = | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "&", v2), typ)) + | "not_bits", [AV_C_fragment (v, _)] -> + AE_val (AV_C_fragment (F_unary ("~", v), typ)) + | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> let len = F_op (f, "-", F_op (t, "-", v_one)) in AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ)) @@ -1700,7 +1703,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = be different. *) let pointer_assign ctyp1 ctyp2 = match ctyp1 with - | CT_ref ctyp1 -> ctyp_equal ctyp1 ctyp2 + | CT_ref ctyp1 when ctyp_equal ctyp1 ctyp2 -> true + | CT_ref ctyp1 -> c_error ~loc:l "Incompatible type in pointer assignment" | _ -> false in let assign_ctyp = ctyp_of_typ ctx assign_typ in @@ -2546,7 +2550,7 @@ let sgen_clexp = function let sgen_clexp_pure = function | CL_id id -> sgen_id id | CL_field (id, field) -> sgen_id id ^ "." ^ Util.zencode_string field - | CL_addr id -> sgen_id id + | CL_addr id -> "*" ^ sgen_id id | CL_addr_field (id, field) -> sgen_id id ^ "->" ^ Util.zencode_string field | CL_have_exception -> "have_exception" | CL_current_exception -> "current_exception" -- cgit v1.2.3 From 4b6732fdddebc07f072e012a52f7d9541e4d657c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 13 Jun 2018 21:26:35 +0100 Subject: Tracing instrumentation for C backend --- lib/sail.h | 161 +++++++++++++++++++++++++++++++++++++++---- riscv/platform_impl.ml | 2 +- src/bitfield.ml | 18 ++++- src/c_backend.ml | 58 +++++++++++++++- src/sail.ml | 3 + src/sail_lib.ml | 4 ++ src/value.ml | 3 + test/c/read_write_ram.expect | 1 + test/c/read_write_ram.sail | 29 ++++++++ 9 files changed, 264 insertions(+), 15 deletions(-) create mode 100644 test/c/read_write_ram.expect create mode 100644 test/c/read_write_ram.sail diff --git a/lib/sail.h b/lib/sail.h index 319db18d..a2f2f456 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -163,6 +163,11 @@ void concat_str(sail_string *stro, const sail_string str1, const sail_string str void undefined_string(sail_string *str, const unit u) { } +unit print(const sail_string str) { + printf("%s", str); + return UNIT; +} + unit print_endline(const sail_string str) { printf("%s\n", str); return UNIT; @@ -173,6 +178,11 @@ unit print_string(const sail_string str1, const sail_string str2) { return UNIT; } +unit prerr(const sail_string str) { + fprintf(stderr, "%s", str); + return UNIT; +} + unit prerr_endline(const sail_string str) { fprintf(stderr, "%s\n", str); return UNIT; @@ -185,6 +195,13 @@ unit print_int(const sail_string str, const mpz_t op) { return UNIT; } +unit prerr_int(const sail_string str, const mpz_t op) { + fputs(str, stderr); + mpz_out_str(stderr, 10, op); + fputs("\n", stderr); + return UNIT; +} + unit print_int64(const sail_string str, const int64_t op) { printf("%s%" PRId64 "\n", str, op); return UNIT; @@ -192,7 +209,8 @@ unit print_int64(const sail_string str, const int64_t op) { unit sail_putchar(const mpz_t op) { char c = (char) mpz_get_ui(op); - putchar(c); + printf("%c", c); + fflush(stdout); return UNIT; } @@ -936,8 +954,6 @@ void init_real_of_sail_string(real *rop, const sail_string op) { #endif -#endif - /* ***** Sail memory builtins ***** */ /* We organise memory available to the sail model into a linked list @@ -954,7 +970,7 @@ struct block { struct block *sail_memory = NULL; /* Must be one less than a power of two. */ -uint64_t MASK = 0xFFFFul; +uint64_t MASK = 0xFFFFFFul; // All sail vectors are at least 64-bits, but only the bottom 8 bits // are used in the second argument. @@ -979,10 +995,11 @@ void write_mem(uint64_t address, uint64_t byte) /* If we couldn't find a block matching the mask, allocate a new one, write the byte, and put it at the front of the block list. */ + fprintf(stderr, "[Sail] Allocating new block 0x%" PRIx64 "\n", mask); struct block *new_block = malloc(sizeof(struct block)); new_block->block_id = mask; new_block->mem = calloc(MASK + 1, sizeof(uint8_t)); - new_block->mem[offset] = byte; + new_block->mem[offset] = (uint8_t) byte; new_block->next = sail_memory; sail_memory = new_block; } @@ -1002,7 +1019,7 @@ uint64_t read_mem(uint64_t address) } } - return 0; + return 0x58; } void kill_mem() @@ -1040,7 +1057,7 @@ unit write_ram(const mpz_t addr_size, // Either 32 or 64 byte = mpz_get_ui(buf) & 0xFF; write_mem(addr + i, byte); - // Then shift buf 8 bits right, and increment addr. + // Then shift buf 8 bits right. mpz_fdiv_q_2exp(buf, buf, 8); } @@ -1072,6 +1089,7 @@ void read_ram(bv_t *data, } unit load_raw(uint64_t addr, const sail_string file) { + fprintf(stderr, "[Sail] Loading %s from 0x%" PRIx64 " to ", file, addr); FILE *fp = fopen(file, "r"); uint64_t byte; @@ -1080,6 +1098,8 @@ unit load_raw(uint64_t addr, const sail_string file) { addr++; } + fprintf(stderr, "0x%" PRIx64 "\n", addr - 1); + return UNIT; } @@ -1117,16 +1137,131 @@ void load_image(char *file) { fclose(fp); } -void load_instr(uint64_t addr, uint32_t instr) { - write_mem(addr , instr & 0xFF); - write_mem(addr + 1, instr >> 8 & 0xFF); - write_mem(addr + 2, instr >> 16 & 0xFF); - write_mem(addr + 3, instr >> 24 & 0xFF); +// ***** Setup and cleanup functions for library code ***** + +static int64_t g_trace_depth; +static bool g_trace_enabled; + +/* + * Bind these functions in Sail to enable and disable tracing: + * + * val "enable_tracing" : unit -> unit + * val "disable_tracing" : unit -> unit + * + * Compile with sail -c -c_trace. + */ +unit enable_tracing(const unit u) +{ + g_trace_depth = 0; + g_trace_enabled = true; + return UNIT; +} + +unit disable_tracing(const unit u) +{ + g_trace_depth = 0; + g_trace_enabled = false; + return UNIT; +} + +void trace_bv_t(const bv_t op) +{ + if (g_trace_enabled) { + if (op.len % 4 == 0) { + fputs("0x", stderr); + mpz_t buf; + mpz_init_set(buf, *op.bits); + + char *hex = malloc((op.len / 4) * sizeof(char)); + + for (int i = 0; i < op.len / 4; ++i) { + char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30); + hex[i] = (c < 0x3A) ? c : c + 0x7; + mpz_fdiv_q_2exp(buf, buf, 4); + } + + for (int i = op.len / 4; i > 0; --i) { + fputc(hex[i - 1], stderr); + } + + free(hex); + mpz_clear(buf); + } else { + fputs("0b", stderr); + for (int i = op.len; i > 0; --i) { + fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stderr); + } + } + } +} + +void trace_uint64_t(const uint64_t x) { + if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x); +} + +void trace_sail_string(const sail_string str) { + if (g_trace_enabled) fprintf(stderr, "\"%s\"", str); +} + +void trace_unit(const unit u) { + if (g_trace_enabled) fputs("()", stderr); +} + +void trace_mpz_t(const mpz_t op) { + if (g_trace_enabled) mpz_out_str(stderr, 10, op); +} + +void trace_bool(const bool b) { + if (g_trace_enabled) { + if (b) { + fprintf(stderr, "true"); + } else { + fprintf(stderr, "false"); + } + } +} + +void trace_unknown(void) { + if (g_trace_enabled) fputs("?", stderr); +} + +void trace_argsep(void) { + if (g_trace_enabled) fputs(", ", stderr); +} + +void trace_argend(void) { + if (g_trace_enabled) fputs(")\n", stderr); +} + +void trace_retend(void) { + if (g_trace_enabled) fputs("\n", stderr); +} + +void trace_start(char *name) +{ + if (g_trace_enabled) { + fprintf(stderr, "[TRACE] "); + for (int64_t i = 0; i < g_trace_depth; ++i) { + fprintf(stderr, "%s", "| "); + } + fprintf(stderr, "%s(", name); + } +} + +void trace_end(void) +{ + if (g_trace_enabled) { + fprintf(stderr, "[TRACE] "); + for (int64_t i = 0; i < g_trace_depth; ++i) { + fprintf(stderr, "%s", "| "); + } + } } // ***** Setup and cleanup functions for library code ***** void setup_library(void) { + disable_tracing(UNIT); mpf_set_default_prec(FLOAT_PRECISION); mpz_init(sail_lib_tmp1); mpz_init(sail_lib_tmp2); @@ -1137,3 +1272,5 @@ void cleanup_library(void) { mpz_clear(sail_lib_tmp2); kill_mem(); } + +#endif diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml index 9b063404..0902877a 100644 --- a/riscv/platform_impl.ml +++ b/riscv/platform_impl.ml @@ -152,7 +152,7 @@ let rec term_read () = let buf = Bytes.make 1 '\000' in let nbytes = Unix.read Unix.stdin buf 0 1 in (* todo: handle nbytes == 0 *) - buf.[0] + Bytes.get buf 0 (* let save_string_to_file s fname = diff --git a/src/bitfield.ml b/src/bitfield.ml index 161908cd..afdd5baf 100644 --- a/src/bitfield.ml +++ b/src/bitfield.ml @@ -83,6 +83,22 @@ let rec translate_indices hi lo = else (hi / 64, hi mod 64, 0) :: translate_indices (hi - (hi mod 64 + 1)) lo +let constructor name order start stop = + let indices = translate_indices start stop in + let size = if start > stop then start - (stop - 1) else stop - (start - 1) in + let constructor_val = Printf.sprintf "val Mk_%s : %s -> %s" name (bitvec size order) name in + let body (chunk, hi, lo) = + Printf.sprintf "%s_chunk_%i = v[%i .. %i]" + name chunk ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop) + in + let constructor_function = String.concat "\n" + [ Printf.sprintf "function Mk_%s v = struct {" name; + Printf.sprintf " %s" (Util.string_of_list ",\n " body indices); + "}" + ] + in + combine [ast_of_def_string order constructor_val; ast_of_def_string order constructor_function] + (* For every index range, create a getter and setter *) let index_range_getter name field order start stop = let indices = translate_indices start stop in @@ -149,4 +165,4 @@ let field_accessor name order (id, ir) = index_range_accessor name (string_of_id let macro id size order ranges = let name = string_of_id id in let ranges = (mk_id "bits", BF_aux (BF_range (Big_int.of_int (size - 1), Big_int.of_int 0), Parse_ast.Unknown)) :: ranges in - combine ([newtype name size order] @ List.map (field_accessor name order) ranges) + combine ([newtype name size order; constructor name order (size - 1) 0] @ List.map (field_accessor name order) ranges) diff --git a/src/c_backend.ml b/src/c_backend.ml index e088b5e5..96cd9ed7 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -59,6 +59,7 @@ module Big_int = Nat_big_num let c_verbosity = ref 1 let opt_ddump_flow_graphs = ref false +let opt_trace = ref false (* Optimization flags *) let optimize_primops = ref false @@ -990,8 +991,10 @@ let analyze_primop' ctx env l id args typ = | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "&", v2), typ)) + (* | "not_bits", [AV_C_fragment (v, _)] -> AE_val (AV_C_fragment (F_unary ("~", v), typ)) + *) | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> let len = F_op (f, "-", F_op (t, "-", v_one)) in @@ -3231,6 +3234,59 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false +let instrument_tracing ctx = + let module StringSet = Set.Make(String) in + let traceable = StringSet.of_list ["uint64_t"; "sail_string"; "bv_t"; "mpz_t"; "unit"; "bool"] in + let rec instrument = function + | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs -> + let trace_start = + iraw (Printf.sprintf "trace_start(\"%s\");" (String.escaped (string_of_id id))) + in + let trace_arg cval = + let ctyp_name = sgen_ctyp_name (cval_ctyp cval) in + if StringSet.mem ctyp_name traceable then + iraw (Printf.sprintf "trace_%s(%s);" ctyp_name (sgen_cval cval)) + else + iraw "trace_unknown();" + in + let rec trace_args = function + | [] -> [] + | [cval] -> [trace_arg cval] + | cval :: cvals -> + trace_arg cval :: iraw "trace_argsep();" :: trace_args cvals + in + let trace_end = iraw "trace_end();" in + let trace_ret = + let ctyp_name = sgen_ctyp_name ctyp in + if StringSet.mem ctyp_name traceable then + iraw (Printf.sprintf "trace_%s(%s);" (sgen_ctyp_name ctyp) (sgen_clexp_pure clexp)) + else + iraw "trace_unknown();" + in + [trace_start; + iraw "g_trace_depth++;"] + @ trace_args args + @ [iraw "trace_argend();"; + instr; + iraw "g_trace_depth--;"; + trace_end; + trace_ret; + iraw "trace_retend();"] + @ instrument instrs + + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (instrument block), aux) :: instrument instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (instrument block), aux) :: instrument instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (cval, instrument then_instrs, instrument else_instrs, ctyp), aux) :: instrument instrs + + | instr :: instrs -> instr :: instrument instrs + | [] -> [] + in + function + | CDEF_fundef (function_id, heap_return, args, body) -> + CDEF_fundef (function_id, heap_return, args, instrument body) + | cdef -> cdef + let bytecode_ast ctx rewrites (Defs defs) = let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in let exit_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_exit") "unit -> unit effect {escape}" in @@ -3258,7 +3314,7 @@ let compile_ast ctx (Defs defs) = 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 cdefs = List.concat (List.rev chunks) in - let cdefs = optimize ctx cdefs in + let cdefs = List.map (instrument_tracing ctx) (optimize ctx cdefs) in let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline diff --git a/src/sail.ml b/src/sail.ml index 36b4efd8..86c00254 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -119,6 +119,9 @@ let options = Arg.align ([ ( "-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " Apply constant folding optimizations"); + ( "-c_trace", + Arg.Set C_backend.opt_trace, + " Instrument C ouput with tracing"); ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 89056347..31b975df 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -575,6 +575,10 @@ let real_of_string str = (* Not a very good sqrt implementation *) let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *) +let print str = Pervasives.print_string str + +let prerr str = Pervasives.prerr_string str + let print_int (str, x) = print_endline (str ^ Big_int.to_string x) diff --git a/src/value.ml b/src/value.ml index 8ee219b7..41b52720 100644 --- a/src/value.ml +++ b/src/value.ml @@ -491,6 +491,9 @@ let primops = StringMap.empty [ ("and_bool", and_bool); ("or_bool", or_bool); + ("print", value_print); + ("prerr", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit)); + ("dec_str", fun _ -> V_string "X"); ("print_endline", value_print); ("prerr_endline", fun vs -> (prerr_endline (string_of_value (List.hd vs)); V_unit)); ("putchar", value_putchar); diff --git a/test/c/read_write_ram.expect b/test/c/read_write_ram.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/read_write_ram.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/read_write_ram.sail b/test/c/read_write_ram.sail new file mode 100644 index 00000000..751d15b5 --- /dev/null +++ b/test/c/read_write_ram.sail @@ -0,0 +1,29 @@ +default Order dec + +$include +$include +$include +$include +$include + +val write_ram = "write_ram" : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmem} + +val read_ram = "read_ram" : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val main : unit -> unit effect {escape, wmem, rmem} + +function main() = { + write_ram(64, 4, 64^0x0, 64^0x8000_0000, 0x01020304); + let data = read_ram(64, 4, 64^0x0, 64^0x8000_0000); + assert(data == 0x01020304); + let data = read_ram(64, 3, 64^0x0, 64^0x8000_0001); + assert(data == 0x010203); + let data = read_ram(64, 3, 64^0x0, 64^0x8000_0000); + assert(data == 0x020304); + write_ram(64, 4, 64^0x0, 64^0x7fff_ffff, 0xA1B2C3D4); + let data = read_ram(64, 3, 64^0x0, 64^0x8000_0000); + assert(data == 0xA1B2C3); + print_endline("ok"); +} \ No newline at end of file -- cgit v1.2.3 From 5dc3ee5029f6e828b7e77a176a67894e8fa00696 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 Jun 2018 04:49:47 +0100 Subject: Refactor C backend, and split RTS into multiple files --- language/bytecode.ott | 6 +- lib/rts.c | 275 ++++++++++ lib/rts.h | 86 +++ lib/sail.c | 558 ++++++++++++++++++++ lib/sail.h | 1380 ++++++------------------------------------------- lib/vector_dec.sail | 7 +- src/bytecode_util.ml | 10 +- src/c_backend.ml | 219 ++++---- test/c/run_tests.sh | 2 +- 9 files changed, 1213 insertions(+), 1330 deletions(-) create mode 100644 lib/rts.c create mode 100644 lib/rts.h create mode 100644 lib/sail.c diff --git a/language/bytecode.ott b/language/bytecode.ott index 704bda83..bcd7b5b0 100644 --- a/language/bytecode.ott +++ b/language/bytecode.ott @@ -65,11 +65,11 @@ fragment :: 'F_' ::= ctyp :: 'CT_' ::= {{ com C type }} - | mpz_t :: :: mpz + | mpz_t :: :: int % Arbitrary precision GMP integer, mpz_t in C. }} - | bv_t ( bool ) :: :: bv + | bv_t ( bool ) :: :: bits % Variable length bitvector - flag represents direction, true - dec or false - inc }} - | 'uint64_t' ( nat , bool ) :: :: uint64 + | 'uint64_t' ( nat , bool ) :: :: bits64 % Fixed length bitvector that fits within a 64-bit word. - int % represents length, and flag is the same as CT_bv. }} | 'int64_t' :: :: int64 diff --git a/lib/rts.c b/lib/rts.c new file mode 100644 index 00000000..b098ae0e --- /dev/null +++ b/lib/rts.c @@ -0,0 +1,275 @@ +#include + +#include"sail.h" +#include"rts.h" + +void sail_match_failure(sail_string msg) +{ + fprintf(stderr, "Pattern match failure in %s\n", msg); + exit(EXIT_FAILURE); +} + +unit sail_assert(bool b, sail_string msg) +{ + if (b) return UNIT; + fprintf(stderr, "Assertion failed: %s\n", msg); + exit(EXIT_FAILURE); +} + +/* ***** Sail memory builtins ***** */ + +/* + * We organise memory available to the sail model into a linked list + * of dynamically allocated MASK + 1 size blocks. + */ +struct block { + uint64_t block_id; + uint8_t *mem; + struct block *next; +}; + +struct block *sail_memory = NULL; + +/* + * Must be one less than a power of two. + */ +uint64_t MASK = 0xFFFFFFul; + +/* + * All sail vectors are at least 64-bits, but only the bottom 8 bits + * are used in the second argument. + */ +void write_mem(uint64_t address, uint64_t byte) +{ + //printf("ADDR: %lu, BYTE: %lu\n", address, byte); + + uint64_t mask = address & ~MASK; + uint64_t offset = address & MASK; + + struct block *current = sail_memory; + + while (current != NULL) { + if (current->block_id == mask) { + current->mem[offset] = (uint8_t) byte; + return; + } else { + current = current->next; + } + } + + /* + * If we couldn't find a block matching the mask, allocate a new + * one, write the byte, and put it at the front of the block list. + */ + fprintf(stderr, "[Sail] Allocating new block 0x%" PRIx64 "\n", mask); + struct block *new_block = malloc(sizeof(struct block)); + new_block->block_id = mask; + new_block->mem = calloc(MASK + 1, sizeof(uint8_t)); + new_block->mem[offset] = (uint8_t) byte; + new_block->next = sail_memory; + sail_memory = new_block; +} + +uint64_t read_mem(uint64_t address) +{ + uint64_t mask = address & ~MASK; + uint64_t offset = address & MASK; + + struct block *current = sail_memory; + + while (current != NULL) { + if (current->block_id == mask) { + return (uint64_t) current->mem[offset]; + } else { + current = current->next; + } + } + + return 0x00; +} + +void kill_mem() +{ + while (sail_memory != NULL) { + struct block *next = sail_memory->next; + + free(sail_memory->mem); + free(sail_memory); + + sail_memory = next; + } +} + +// ***** Memory builtins ***** + +unit write_ram(const mpz_t addr_size, // Either 32 or 64 + const mpz_t data_size_mpz, // Number of bytes + const sail_bits hex_ram, // Currently unused + const sail_bits addr_bv, + const sail_bits data) +{ + uint64_t addr = mpz_get_ui(*addr_bv.bits); + uint64_t data_size = mpz_get_ui(data_size_mpz); + + mpz_t buf; + mpz_init_set(buf, *data.bits); + + uint64_t byte; + for(uint64_t i = 0; i < data_size; ++i) { + // Take the 8 low bits of buf and write to addr. + byte = mpz_get_ui(buf) & 0xFF; + write_mem(addr + i, byte); + + // Then shift buf 8 bits right. + mpz_fdiv_q_2exp(buf, buf, 8); + } + + mpz_clear(buf); + return UNIT; +} + +void read_ram(sail_bits *data, + const mpz_t addr_size, + const mpz_t data_size_mpz, + const sail_bits hex_ram, + const sail_bits addr_bv) +{ + uint64_t addr = mpz_get_ui(*addr_bv.bits); + uint64_t data_size = mpz_get_ui(data_size_mpz); + + mpz_set_ui(*data->bits, 0); + data->len = data_size * 8; + + mpz_t byte; + mpz_init(byte); + for(uint64_t i = data_size; i > 0; --i) { + mpz_set_ui(byte, read_mem(addr + (i - 1))); + mpz_mul_2exp(*data->bits, *data->bits, 8); + mpz_add(*data->bits, *data->bits, byte); + } + + mpz_clear(byte); +} + +void load_image(char *file) { + FILE *fp = fopen(file, "r"); + + if (!fp) { + fprintf(stderr, "Image file %s could not be loaded\n", file); + exit(EXIT_FAILURE); + } + + char *addr = NULL; + char *data = NULL; + size_t len = 0; + + while (true) { + ssize_t addr_len = getline(&addr, &len, fp); + if (addr_len == -1) break; + ssize_t data_len = getline(&data, &len, fp); + if (data_len == -1) break; + + if (!strcmp(addr, "elf_entry\n")) { + if (sscanf(data, "%" PRIu64 "\n", &g_elf_entry) != 1) { + fprintf(stderr, "Failed to parse elf_entry\n"); + exit(EXIT_FAILURE); + }; + printf("Elf entry point: %" PRIx64 "\n", g_elf_entry); + } else { + write_mem((uint64_t) atoll(addr), (uint64_t) atoll(data)); + } + } + + free(addr); + free(data); + fclose(fp); +} + +// ***** Tracing support ***** + +unit enable_tracing(const unit u) +{ + g_trace_depth = 0; + g_trace_enabled = true; + return UNIT; +} + +unit disable_tracing(const unit u) +{ + g_trace_depth = 0; + g_trace_enabled = false; + return UNIT; +} + +void trace_uint64_t(const uint64_t x) { + if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x); +} + +void trace_unit(const unit u) { + if (g_trace_enabled) fputs("()", stderr); +} + +void trace_mpz_t(const mpz_t op) { + if (g_trace_enabled) mpz_out_str(stderr, 10, op); +} + +void trace_bool(const bool b) { + if (g_trace_enabled) { + if (b) { + fprintf(stderr, "true"); + } else { + fprintf(stderr, "false"); + } + } +} + +void trace_unknown(void) { + if (g_trace_enabled) fputs("?", stderr); +} + +void trace_argsep(void) { + if (g_trace_enabled) fputs(", ", stderr); +} + +void trace_argend(void) { + if (g_trace_enabled) fputs(")\n", stderr); +} + +void trace_retend(void) { + if (g_trace_enabled) fputs("\n", stderr); +} + +void trace_start(char *name) +{ + if (g_trace_enabled) { + fprintf(stderr, "[TRACE] "); + for (int64_t i = 0; i < g_trace_depth; ++i) { + fprintf(stderr, "%s", "| "); + } + fprintf(stderr, "%s(", name); + } +} + +void trace_end(void) +{ + if (g_trace_enabled) { + fprintf(stderr, "[TRACE] "); + for (int64_t i = 0; i < g_trace_depth; ++i) { + fprintf(stderr, "%s", "| "); + } + } +} + +/* ***** Setup and cleanup functions for RTS ***** */ + +void setup_rts(void) +{ + disable_tracing(UNIT); + setup_library(); +} + +void cleanup_rts(void) +{ + cleanup_library(); + kill_mem(); +} diff --git a/lib/rts.h b/lib/rts.h new file mode 100644 index 00000000..de32ef8d --- /dev/null +++ b/lib/rts.h @@ -0,0 +1,86 @@ +#pragma once + +#include +#include +#include + +#include"sail.h" + +/* + * This function should be called whenever a pattern match failure + * occurs. Pattern match failures are always fatal. + */ +void sail_match_failure(sail_string msg); + +/* + * sail_assert implements the assert construct in Sail. If any + * assertion fails we immediately exit the model. + */ +unit sail_assert(bool b, sail_string msg); + +/* ***** Memory builtins ***** */ + +// These memory builtins are intended to match the semantics for the +// __ReadRAM and __WriteRAM functions in ASL. + +unit write_ram(const mpz_t addr_size, // Either 32 or 64 + const mpz_t data_size_mpz, // Number of bytes + const sail_bits hex_ram, // Currently unused + const sail_bits addr_bv, + const sail_bits data); + +void read_ram(sail_bits *data, + const mpz_t addr_size, + const mpz_t data_size_mpz, + const sail_bits hex_ram, + const sail_bits addr_bv); + +void load_image(char *); + +/* ***** Tracing ***** */ + +static int64_t g_trace_depth; +static bool g_trace_enabled; + +/* + * Bind these functions in Sail to enable and disable tracing: + * + * val "enable_tracing" : unit -> unit + * val "disable_tracing" : unit -> unit + * + * Compile with sail -c -c_trace. + */ +unit enable_tracing(const unit); +unit disable_tracing(const unit); + +/* + * Tracing is implemented by void trace_TYPE functions, each of which + * takes the Sail value to print as the first argument, and prints it + * directly to stderr with no linebreaks. + * + * For types that don't have printing function we have trace_unknown, + * which simply prints '?'. trace_argsep, trace_argend, and + * trace_retend are used for formatting function arguments. They won't + * overlap with user defined types because the type names used for + * TYPE are zencoded. trace_start(NAME) and trace_end() are called + * before printing the function arguments and return value + * respectively. +*/ +void trace_sail_int(const sail_int); +void trace_bool(const bool); + +void trace_unknown(void); +void trace_argsep(void); +void trace_argend(void); +void trace_retend(void); +void trace_start(char *); +void trace_end(void); + +static uint64_t g_elf_entry; + +/* + * setup_rts and cleanup_rts are responsible for calling setup_library + * and cleanup_library in sail.h. + */ +void setup_rts(void); +void cleanup_rts(void); diff --git a/lib/sail.c b/lib/sail.c new file mode 100644 index 00000000..5fd7a04e --- /dev/null +++ b/lib/sail.c @@ -0,0 +1,558 @@ +#include +#include +#include +#include +#include + +#include"sail.h" + +/* + * Temporary mpzs for use in functions below. To avoid conflicts, only + * use in functions that do not call other functions in this file. + */ +static sail_int sail_lib_tmp1, sail_lib_tmp2; + +#define FLOAT_PRECISION 255 + +void setup_library(void) +{ + mpz_init(sail_lib_tmp1); + mpz_init(sail_lib_tmp2); + mpf_set_default_prec(FLOAT_PRECISION); +} + +void cleanup_library(void) +{ + mpz_clear(sail_lib_tmp1); + mpz_clear(sail_lib_tmp2); +} + +/* ***** Sail bit type ***** */ + +bool eq_bit(const mach_bits a, const mach_bits b) +{ + return a == b; +} + +/* ***** Sail booleans ***** */ + +bool not(const bool b) { + return !b; +} + +bool eq_bool(const bool a, const bool b) { + return a == b; +} + +bool UNDEFINED(bool)(const unit u) { + return false; +} + +/* ***** Sail strings ***** */ + +void CREATE(sail_string)(sail_string *str) { + char *istr = (char *) 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)); + istr[0] = '\0'; + *str = istr; +} + +void COPY(sail_string)(sail_string *str1, const sail_string str2) { + size_t len = strlen(str2); + *str1 = realloc(*str1, len + 1); + *str1 = strcpy(*str1, str2); +} + +void KILL(sail_string)(sail_string *str) { + free(*str); +} + +void dec_str(sail_string *str, const mpz_t n) { + free(*str); + gmp_asprintf(str, "%Zd", n); +} + +void hex_str(sail_string *str, const mpz_t n) { + free(*str); + gmp_asprintf(str, "0x%Zx", n); +} + +bool eq_string(const sail_string str1, const sail_string str2) { + return strcmp(str1, str2) == 0; +} + +/* ***** Sail integers ***** */ + +#ifndef USE_INT128 + +inline +void COPY(sail_int)(sail_int *rop, const sail_int op) +{ + mpz_set(*rop, op); +} + +inline +void CREATE(sail_int)(sail_int *rop) +{ + mpz_init(*rop); +} + +inline +void RECREATE(sail_int)(sail_int *rop) +{ + mpz_set_ui(*rop, 0); +} + +inline +void KILL(sail_int)(sail_int *rop) +{ + mpz_clear(*rop); +} + +inline +void CREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op) +{ + mpz_init_set_si(*rop, op); +} + +inline +void RECREATE_OF(sail_int, mach_int)(sail_int *rop, mach_int op) +{ + mpz_set_si(*rop, op); +} + +inline +void CREATE_OF(sail_int, sail_string)(sail_int *rop, sail_string str) +{ + mpz_init_set_str(*rop, str, 10); +} + +inline +void RECREATE_OF(sail_int, sail_string)(mpz_t *rop, sail_string str) +{ + mpz_set_str(*rop, str, 10); +} + +inline +mach_int CONVERT_OF(mach_int, sail_int)(const sail_int op) +{ + return mpz_get_si(op); +} + +inline +void CONVERT_OF(sail_int, mach_int)(sail_int *rop, const mach_int op) +{ + mpz_set_si(*rop, op); +} + +inline +bool eq_int(const sail_int op1, const sail_int op2) +{ + return !abs(mpz_cmp(op1, op2)); +} + +inline +bool lt(const sail_int op1, const sail_int op2) +{ + return mpz_cmp(op1, op2) < 0; +} + +inline +bool gt(const mpz_t op1, const mpz_t op2) +{ + return mpz_cmp(op1, op2) > 0; +} + +inline +bool lteq(const mpz_t op1, const mpz_t op2) +{ + return mpz_cmp(op1, op2) <= 0; +} + +inline +bool gteq(const mpz_t op1, const mpz_t op2) +{ + return mpz_cmp(op1, op2) >= 0; +} + +inline +void shl_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_mul_2exp(*rop, op1, mpz_get_ui(op2)); +} + +inline +void shr_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2)); +} + +inline +void undefined_int(sail_int *rop, const int n) +{ + mpz_set_ui(*rop, (uint64_t) n); +} + +inline +void undefined_range(sail_int *rop, const sail_int l, const sail_int u) +{ + mpz_set(*rop, l); +} + +inline +void add_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_add(*rop, op1, op2); +} + +inline +void sub_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_sub(*rop, op1, op2); +} + +inline +void mult_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_mul(*rop, op1, op2); +} + +inline +void tdiv_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_tdiv_q(*rop, op1, op2); +} + +inline +void tmod_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_tdiv_r(*rop, op1, op2); +} + +inline +void fdiv_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_fdiv_q(*rop, op1, op2); +} + +inline +void fmod_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_fdiv_r(*rop, op1, op2); +} + +void max_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + if (lt(op1, op2)) { + mpz_set(*rop, op2); + } else { + mpz_set(*rop, op1); + } +} + +void min_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + if (gt(op1, op2)) { + mpz_set(*rop, op2); + } else { + mpz_set(*rop, op1); + } +} + +inline +void neg_int(sail_int *rop, const sail_int op) +{ + mpz_neg(*rop, op); +} + +inline +void abs_int(sail_int *rop, const sail_int op) +{ + mpz_abs(*rop, op); +} + +void pow2(sail_int *rop, const sail_int exp) { + /* Assume exponent is never more than 2^64... */ + uint64_t exp_ui = mpz_get_ui(exp); + mpz_t base; + mpz_init_set_ui(base, 2ul); + mpz_pow_ui(*rop, base, exp_ui); + mpz_clear(base); +} + +#endif + +/* ***** Sail bitvectors ***** */ + +void CREATE(sail_bits)(sail_bits *rop) +{ + rop->bits = malloc(sizeof(mpz_t)); + rop->len = 0; + mpz_init(*rop->bits); +} + +void RECREATE(sail_bits)(sail_bits *rop) +{ + rop->len = 0; + mpz_set_ui(*rop->bits, 0); +} + +void COPY(sail_bits)(sail_bits *rop, const sail_bits op) +{ + rop->len = op.len; + mpz_set(*rop->bits, *op.bits); +} + +void KILL(sail_bits)(sail_bits *rop) +{ + mpz_clear(*rop->bits); + free(rop->bits); +} + +void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction) +{ + rop->bits = malloc(sizeof(mpz_t)); + rop->len = len; + mpz_init_set_ui(*rop->bits, op); +} + +void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction) +{ + rop->len = len; + mpz_set_ui(*rop->bits, op); +} + +mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits op) +{ + return mpz_get_ui(*op.bits); +} + +void UNDEFINED(sail_bits)(sail_bits *rop, const sail_int len, const mach_bits bit) +{ + zeros(rop, len); +} + +mach_bits UNDEFINED(mach_bits)(const unit u) { return 0; } + +mach_bits safe_rshift(const mach_bits x, const mach_bits n) +{ + if (n >= 64) { + return 0ul; + } else { + return x >> n; + } +} + +void normalize_sail_bits(sail_bits *rop) { + /* TODO optimisation: keep a set of masks of various sizes handy */ + mpz_set_ui(sail_lib_tmp1, 1); + mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len); + mpz_sub_ui(sail_lib_tmp1, sail_lib_tmp1, 1); + mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1); +} + +void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk) +{ + rop->len = rop->len + 64ul; + mpz_mul_2exp(*rop->bits, *op.bits, 64ul); + mpz_add_ui(*rop->bits, *rop->bits, chunk); +} + +void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mpz_add(*rop->bits, *op1.bits, *op2.bits); + normalize_sail_bits(rop); +} + +void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mpz_sub(*rop->bits, *op1.bits, *op2.bits); + normalize_sail_bits(rop); +} + +void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2) +{ + rop->len = op1.len; + mpz_add(*rop->bits, *op1.bits, op2); + normalize_sail_bits(rop); +} + +void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2) +{ + rop->len = op1.len; + mpz_sub(*rop->bits, *op1.bits, op2); + normalize_sail_bits(rop); +} + +void zeros(sail_bits *rop, const sail_int op) +{ + rop->len = mpz_get_ui(op); + mpz_set_ui(*rop->bits, 0); +} + +void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len) +{ + rop->len = mpz_get_ui(len); + mpz_set(*rop->bits, *op.bits); +} + +void length_sail_bits(sail_int *rop, const sail_bits op) +{ + mpz_set_ui(*rop, op.len); +} + +bool eq_bits(const sail_bits op1, const sail_bits op2) +{ + for (mp_bitcnt_t i = 0; i < op1.len; i++) { + if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return false; + } + return true; +} + +void vector_subrange_sail_bits(sail_bits *rop, + const sail_bits op, + const sail_int n_mpz, + const sail_int m_mpz) +{ + uint64_t n = mpz_get_ui(n_mpz); + uint64_t m = mpz_get_ui(m_mpz); + + rop->len = n - (m - 1ul); + mpz_fdiv_q_2exp(*rop->bits, *op.bits, m); + normalize_sail_bits(rop); +} + +void truncate(sail_bits *rop, const sail_bits op, const sail_int len) +{ + rop->len = mpz_get_ui(len); + mpz_set(*rop->bits, *op.bits); + normalize_sail_bits(rop); +} + +mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz) +{ + uint64_t n = mpz_get_ui(n_mpz); + return (mach_bits) mpz_tstbit(*op.bits, n); +} + +void sail_unsigned(sail_int *rop, const sail_bits op) +{ + /* Normal form of bv_t is always positive so just return the bits. */ + mpz_set(*rop, *op.bits); +} + +void sail_signed(sail_int *rop, const sail_bits op) +{ + if (op.len == 0) { + mpz_set_ui(*rop, 0); + } else { + mp_bitcnt_t sign_bit = op.len - 1; + mpz_set(*rop, *op.bits); + if (mpz_tstbit(*op.bits, sign_bit) != 0) { + /* If sign bit is unset then we are done, + otherwise clear sign_bit and subtract 2**sign_bit */ + mpz_set_ui(sail_lib_tmp1, 1); + mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, sign_bit); /* 2**sign_bit */ + mpz_combit(*rop, sign_bit); /* clear sign_bit */ + mpz_sub(*rop, *rop, sail_lib_tmp1); + } + } +} + +/* ***** Printing functions ***** */ + +void fprint_bits(const sail_string pre, + const sail_bits op, + const sail_string post, + FILE *stream) +{ + fputs(pre, stream); + + if (op.len % 4 == 0) { + fputs("0x", stream); + mpz_t buf; + mpz_init_set(buf, *op.bits); + + char *hex = malloc((op.len / 4) * sizeof(char)); + + for (int i = 0; i < op.len / 4; ++i) { + char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30); + hex[i] = (c < 0x3A) ? c : c + 0x7; + mpz_fdiv_q_2exp(buf, buf, 4); + } + + for (int i = op.len / 4; i > 0; --i) { + fputc(hex[i - 1], stream); + } + + free(hex); + mpz_clear(buf); + } else { + fputs("0b", stream); + for (int i = op.len; i > 0; --i) { + fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stream); + } + } + + fputs(post, stream); +} + +unit print_bits(const sail_string str, const sail_bits op) +{ + fprint_bits(str, op, "\n", stdout); + return UNIT; +} + +unit prerr_bits(const sail_string str, const sail_bits op) +{ + fprint_bits(str, op, "\n", stderr); + return UNIT; +} + +unit print(const sail_string str) +{ + printf("%s", str); + return UNIT; +} + +unit print_endline(const sail_string str) +{ + printf("%s\n", str); + return UNIT; +} + +unit prerr(const sail_string str) +{ + fprintf(stderr, "%s", str); + return UNIT; +} + +unit prerr_endline(const sail_string str) +{ + fprintf(stderr, "%s\n", str); + return UNIT; +} + +unit print_int(const sail_string str, const sail_int op) +{ + fputs(str, stdout); + mpz_out_str(stdout, 10, op); + putchar('\n'); + return UNIT; +} + +unit prerr_int(const sail_string str, const sail_int op) +{ + fputs(str, stderr); + mpz_out_str(stderr, 10, op); + fputs("\n", stderr); + return UNIT; +} diff --git a/lib/sail.h b/lib/sail.h index a2f2f456..1cd5d928 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -1,1276 +1,236 @@ -#ifndef SAIL_LIB -#define SAIL_LIB +#pragma once -#include #include #include +#include #include -#include + +#ifndef USE_INT128 #include -#include +#endif + +/* + * Called by the RTS to initialise and clear any library state. + */ +void setup_library(void); +void cleanup_library(void); + +/* + * 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 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 u) { - return UNIT; -} +unit UNDEFINED(unit)(const unit); +bool eq_unit(const unit, const unit); + +/* ***** Sail booleans ***** */ -bool eq_unit(const unit u1, const unit u2) { - return true; -} +/* + * and_bool and or_bool are special-cased by the compiler to ensure + * short-circuiting evaluation. + */ +bool not(const bool); +bool eq_bool(const bool, const bool); +bool UNDEFINED(bool)(const unit); -typedef struct { - mp_bitcnt_t len; - mpz_t *bits; -} bv_t; +/* ***** Sail strings ***** */ +/* + * Sail strings are just C strings. + */ typedef char *sail_string; -/* Temporary mpzs for use in functions below. To avoid conflicts, only - * use in functions that do not call other functions in this file. */ -static mpz_t sail_lib_tmp1, sail_lib_tmp2; - -/* Wrapper around >> operator to avoid UB when shift amount is greater - than or equal to 64. */ -uint64_t safe_rshift(const uint64_t x, const uint64_t n) { - if (n >= 64) { - return 0ul; - } else { - return x >> n; - } -} - -/* This function should be called whenever a pattern match failure - occurs. Pattern match failures are always fatal. */ -void sail_match_failure(sail_string msg) { - fprintf(stderr, "Pattern match failure in %s\n", msg); - exit(EXIT_FAILURE); -} - -/* sail_assert implements the assert construct in Sail. If any - assertion fails we immediately exit the model. */ -unit sail_assert(bool b, sail_string msg) { - if (b) return UNIT; - fprintf(stderr, "Assertion failed: %s\n", msg); - exit(EXIT_FAILURE); -} - -/* If the sail model calls the exit() function we print a message and - exit successfully. */ -unit sail_exit(const unit u) { - fprintf(stderr, "Sail model exit\n"); - exit(EXIT_SUCCESS); -} - -uint64_t g_elf_entry; - -void elf_entry(mpz_t *rop, const unit u) { - mpz_set_ui(*rop, g_elf_entry); -} - -void elf_tohost(mpz_t *rop, const unit u) { - mpz_set_ui(*rop, 0x0ul); -} - -/* ASL->Sail model has an EnterLowPowerState() function that calls a - sleep request builtin. If it gets called we print a message and - exit the model. */ -unit sleep_request(const unit u) { - fprintf(stderr, "Sail model going to sleep\n"); - exit(EXIT_SUCCESS); -} - -// Sail bits are mapped to uint64_t where bitzero = 0ul and bitone = 1ul -bool eq_bit(const uint64_t a, const uint64_t b) { - return a == b; -} - -uint64_t undefined_bit(unit u) { return 0; } - -unit skip(const unit u) { - return UNIT; -} - -// ***** Sail booleans ***** - -bool not(const bool b) { - return !b; -} - -bool and_bool(const bool a, const bool b) { - return a && b; -} - -bool or_bool(const bool a, const bool b) { - return a || b; -} - -bool eq_bool(const bool a, const bool b) { - return a == b; -} - -bool undefined_bool(const unit u) { - return false; -} - -// ***** Sail strings ***** -void init_sail_string(sail_string *str) { - char *istr = (char *) malloc(1 * sizeof(char)); - istr[0] = '\0'; - *str = istr; -} - -void reinit_sail_string(sail_string *str) { - free(*str); - char *istr = (char *) malloc(1 * sizeof(char)); - istr[0] = '\0'; - *str = istr; -} - -void set_sail_string(sail_string *str1, const sail_string str2) { - size_t len = strlen(str2); - *str1 = realloc(*str1, len + 1); - *str1 = strcpy(*str1, str2); -} - -void dec_str(sail_string *str, const mpz_t n) { - free(*str); - gmp_asprintf(str, "%Zd", n); -} - -void hex_str(sail_string *str, const mpz_t n) { - free(*str); - gmp_asprintf(str, "0x%Zx", n); -} - -void clear_sail_string(sail_string *str) { - free(*str); -} - -bool eq_string(const sail_string str1, const sail_string str2) { - return strcmp(str1, str2) == 0; -} - -void concat_str(sail_string *stro, const sail_string str1, const sail_string str2) { - *stro = realloc(*stro, strlen(str1) + strlen(str2) + 1); - (*stro)[0] = '\0'; - strcat(*stro, str1); - strcat(*stro, str2); -} - -void undefined_string(sail_string *str, const unit u) { -} - -unit print(const sail_string str) { - printf("%s", str); - return UNIT; -} - -unit print_endline(const sail_string str) { - printf("%s\n", str); - return UNIT; -} - -unit print_string(const sail_string str1, const sail_string str2) { - printf("%s%s\n", str1, str2); - return UNIT; -} - -unit prerr(const sail_string str) { - fprintf(stderr, "%s", str); - return UNIT; -} - -unit prerr_endline(const sail_string str) { - fprintf(stderr, "%s\n", str); - return UNIT; -} - -unit print_int(const sail_string str, const mpz_t op) { - fputs(str, stdout); - mpz_out_str(stdout, 10, op); - putchar('\n'); - return UNIT; -} - -unit prerr_int(const sail_string str, const mpz_t op) { - fputs(str, stderr); - mpz_out_str(stderr, 10, op); - fputs("\n", stderr); - return UNIT; -} - -unit print_int64(const sail_string str, const int64_t op) { - printf("%s%" PRId64 "\n", str, op); - return UNIT; -} - -unit sail_putchar(const mpz_t op) { - char c = (char) mpz_get_ui(op); - printf("%c", c); - fflush(stdout); - return UNIT; -} - -// ***** Arbitrary precision integers ***** - -// We wrap around the GMP functions so they follow a consistent naming -// scheme that is shared with the other builtin sail types. - -void set_mpz_t(mpz_t *rop, const mpz_t op) { - mpz_set(*rop, op); -} - -void init_mpz_t(mpz_t *op) { - mpz_init(*op); -} - -void reinit_mpz_t(mpz_t *op) { - mpz_set_ui(*op, 0); -} - -void clear_mpz_t(mpz_t *op) { - mpz_clear(*op); -} - -void init_mpz_t_of_int64_t(mpz_t *rop, int64_t op) { - mpz_init_set_si(*rop, op); -} - -void reinit_mpz_t_of_int64_t(mpz_t *rop, int64_t op) { - mpz_set_si(*rop, op); -} - -void init_mpz_t_of_sail_string(mpz_t *rop, sail_string str) { - mpz_init_set_str(*rop, str, 10); -} - -void reinit_mpz_t_of_sail_string(mpz_t *rop, sail_string str) { - mpz_set_str(*rop, str, 10); -} - -int64_t convert_int64_t_of_mpz_t(const mpz_t op) { - return mpz_get_si(op); -} - -void convert_mpz_t_of_int64_t(mpz_t *rop, const int64_t op) { - mpz_set_si(*rop, op); -} - -// ***** Sail builtins for integers ***** - -bool eq_int(const mpz_t op1, const mpz_t op2) { - return !abs(mpz_cmp(op1, op2)); -} - -bool lt(const mpz_t op1, const mpz_t op2) { - return mpz_cmp(op1, op2) < 0; -} - -bool gt(const mpz_t op1, const mpz_t op2) { - return mpz_cmp(op1, op2) > 0; -} - -bool lteq(const mpz_t op1, const mpz_t op2) { - return mpz_cmp(op1, op2) <= 0; -} - -bool gteq(const mpz_t op1, const mpz_t op2) { - return mpz_cmp(op1, op2) >= 0; -} - -void shl_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { - mpz_mul_2exp(*rop, op1, mpz_get_ui(op2)); -} - -void shr_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { - mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2)); -} - -void undefined_int(mpz_t *rop, const unit u) { - mpz_set_ui(*rop, 0ul); -} - -void undefined_range(mpz_t *rop, const mpz_t l, const mpz_t u) { - mpz_set(*rop, l); -} - -void add_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) -{ - mpz_add(*rop, op1, op2); -} - -void sub_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) -{ - mpz_sub(*rop, op1, op2); -} - -void mult_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) -{ - mpz_mul(*rop, op1, op2); -} - -void div_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) -{ - mpz_tdiv_q(*rop, op1, op2); -} - -void mod_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) -{ - mpz_tdiv_r(*rop, op1, op2); -} - -void max_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { - if (lt(op1, op2)) { - mpz_set(*rop, op2); - } else { - mpz_set(*rop, op1); - } -} - -void min_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { - if (gt(op1, op2)) { - mpz_set(*rop, op2); - } else { - mpz_set(*rop, op1); - } -} - -void neg_int(mpz_t *rop, const mpz_t op) { - mpz_neg(*rop, op); -} - -void abs_int(mpz_t *rop, const mpz_t op) { - mpz_abs(*rop, op); -} - -void pow2(mpz_t *rop, mpz_t exp) { - uint64_t exp_ui = mpz_get_ui(exp); - mpz_t base; - mpz_init_set_ui(base, 2ul); - mpz_pow_ui(*rop, base, exp_ui); - mpz_clear(base); -} - -void get_time_ns(mpz_t *rop, const unit u) { - struct timespec t; - clock_gettime(CLOCK_REALTIME, &t); - mpz_set_si(*rop, t.tv_sec); - mpz_mul_ui(*rop, *rop, 1000000000); - mpz_add_ui(*rop, *rop, t.tv_nsec); -} - -// ***** Sail bitvectors ***** - -void string_of_int(sail_string *str, mpz_t i) { - gmp_asprintf(str, "%Zd", i); -} - -void string_of_bits(sail_string *str, const bv_t op) { - if ((op.len % 4) == 0) { - gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits); - } else { - gmp_asprintf(str, "0b%*0Zb", op.len, *op.bits); - } -} - -unit fprint_bits(const sail_string str, const bv_t op, FILE *stream) -{ - fputs(str, stream); - - if (op.len % 4 == 0) { - fputs("0x", stream); - mpz_t buf; - mpz_init_set(buf, *op.bits); - - char *hex = malloc((op.len / 4) * sizeof(char)); - - for (int i = 0; i < op.len / 4; ++i) { - char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30); - hex[i] = (c < 0x3A) ? c : c + 0x7; - mpz_fdiv_q_2exp(buf, buf, 4); - } - - for (int i = op.len / 4; i > 0; --i) { - fputc(hex[i - 1], stream); - } - - free(hex); - mpz_clear(buf); - } else { - fputs("0b", stream); - for (int i = op.len; i > 0; --i) { - fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stream); - } - } - - fputs("\n", stream); - return UNIT; -} - -unit print_bits(const sail_string str, const bv_t op) -{ - return fprint_bits(str, op, stdout); -} - -unit prerr_bits(const sail_string str, const bv_t op) -{ - return fprint_bits(str, op, stderr); -} - -void length_bv_t(mpz_t *rop, const bv_t op) { - mpz_set_ui(*rop, op.len); -} - -void init_bv_t(bv_t *rop) { - rop->bits = malloc(sizeof(mpz_t)); - rop->len = 0; - mpz_init(*rop->bits); -} - -void reinit_bv_t(bv_t *rop) { - rop->len = 0; - mpz_set_ui(*rop->bits, 0); -} - -void normalise_bv_t(bv_t *rop) { - /* TODO optimisation: keep a set of masks of various sizes handy */ - mpz_set_ui(sail_lib_tmp1, 1); - mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len); - mpz_sub_ui(sail_lib_tmp1, sail_lib_tmp1, 1); - mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1); -} - -void init_bv_t_of_uint64_t(bv_t *rop, const uint64_t op, const uint64_t len, const bool direction) { - rop->bits = malloc(sizeof(mpz_t)); - rop->len = len; - mpz_init_set_ui(*rop->bits, op); -} - -void reinit_bv_t_of_uint64_t(bv_t *rop, const uint64_t op, const uint64_t len, const bool direction) { - rop->len = len; - mpz_set_ui(*rop->bits, op); -} - -void set_bv_t(bv_t *rop, const bv_t op) { - rop->len = op.len; - mpz_set(*rop->bits, *op.bits); -} - -void append_64(bv_t *rop, const bv_t op, const uint64_t chunk) { - rop->len = rop->len + 64ul; - mpz_mul_2exp(*rop->bits, *op.bits, 64ul); - mpz_add_ui(*rop->bits, *rop->bits, chunk); -} - -void append(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len + op2.len; - mpz_mul_2exp(*rop->bits, *op1.bits, op2.len); - mpz_ior(*rop->bits, *rop->bits, *op2.bits); -} - -void replicate_bits(bv_t *rop, const bv_t op1, const mpz_t op2) { - uint64_t op2_ui = mpz_get_ui(op2); - rop->len = op1.len * op2_ui; - mpz_set(*rop->bits, *op1.bits); - for (int i = 1; i < op2_ui; i++) { - mpz_mul_2exp(*rop->bits, *rop->bits, op1.len); - mpz_ior(*rop->bits, *rop->bits, *op1.bits); - } -} +SAIL_BUILTIN_TYPE(sail_string); -uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64_t times) { - uint64_t r = v; - for (int i = 1; i < times; ++i) { - r |= (r << shift); - } - return r; -} +void dec_str(sail_string *str, const mpz_t n); +void hex_str(sail_string *str, const mpz_t n); -void slice(bv_t *rop, const bv_t op, const mpz_t start_mpz, const mpz_t len_mpz) -{ - uint64_t start = mpz_get_ui(start_mpz); - uint64_t len = mpz_get_ui(len_mpz); +bool eq_string(const sail_string, const sail_string); - mpz_set_ui(*rop->bits, 0ul); - rop->len = len; +/* ***** Sail integers ***** */ - for (uint64_t i = 0; i < len; i++) { - if (mpz_tstbit(*op.bits, i + start)) mpz_setbit(*rop->bits, i); - } -} +typedef int64_t mach_int; -uint64_t convert_uint64_t_of_bv_t(const bv_t op) { - return mpz_get_ui(*op.bits); -} - -void zeros(bv_t *rop, const mpz_t op) { - rop->len = mpz_get_ui(op); - mpz_set_ui(*rop->bits, 0ul); -} - -void zero_extend(bv_t *rop, const bv_t op, const mpz_t len) { - rop->len = mpz_get_ui(len); - mpz_set(*rop->bits, *op.bits); -} - -void sign_extend(bv_t *rop, const bv_t op, const mpz_t len) { - rop->len = mpz_get_ui(len); - if(mpz_tstbit(*op.bits, op.len - 1)) { - mpz_set(*rop->bits, *op.bits); - for(mp_bitcnt_t i = rop->len - 1; i >= op.len; i--) { - mpz_setbit(*rop->bits, i); - } - } else { - mpz_set(*rop->bits, *op.bits); - } -} - -void clear_bv_t(bv_t *rop) { - mpz_clear(*rop->bits); - free(rop->bits); -} - -void undefined_bv_t(bv_t *rop, mpz_t len, int bit) { - zeros(rop, len); -} - -void mask(bv_t *rop) { - if (mpz_sizeinbase(*rop->bits, 2) > rop->len) { - mpz_t m; - mpz_init(m); - mpz_ui_pow_ui(m, 2ul, rop->len); - mpz_sub_ui(m, m, 1ul); - mpz_and(*rop->bits, *rop->bits, m); - mpz_clear(m); - } -} - -void truncate(bv_t *rop, const bv_t op, const mpz_t len) { - rop->len = mpz_get_ui(len); - mpz_set(*rop->bits, *op.bits); - mask(rop); -} - -void and_bits(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mpz_and(*rop->bits, *op1.bits, *op2.bits); -} - -void or_bits(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mpz_ior(*rop->bits, *op1.bits, *op2.bits); -} - -void not_bits(bv_t *rop, const bv_t op) { - rop->len = op.len; - mpz_set(*rop->bits, *op.bits); - for (mp_bitcnt_t i = 0; i < op.len; i++) { - mpz_combit(*rop->bits, i); - } -} - -void xor_bits(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mpz_xor(*rop->bits, *op1.bits, *op2.bits); -} - -bool eq_bits(const bv_t op1, const bv_t op2) -{ - for (mp_bitcnt_t i = 0; i < op1.len; i++) { - if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return false; - } - return true; -} - -void sail_uint(mpz_t *rop, const bv_t op) { - /* Normal form of bv_t is always positive so just return the bits. */ - mpz_set(*rop, *op.bits); -} - -void sint(mpz_t *rop, const bv_t op) -{ - if (op.len == 0) { - mpz_set_ui(*rop, 0); - } else { - mp_bitcnt_t sign_bit = op.len - 1; - mpz_set(*rop, *op.bits); - if (mpz_tstbit(*op.bits, sign_bit) != 0) { - /* If sign bit is unset then we are done, - otherwise clear sign_bit and subtract 2**sign_bit */ - mpz_set_ui(sail_lib_tmp1, 1); - mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, sign_bit); /* 2**sign_bit */ - mpz_combit(*rop, sign_bit); /* clear sign_bit */ - mpz_sub(*rop, *rop, sail_lib_tmp1); - } - } -} - -void add_bits(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mpz_add(*rop->bits, *op1.bits, *op2.bits); - normalise_bv_t(rop); -} - -void sub_bits(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mpz_sub(*rop->bits, *op1.bits, *op2.bits); - normalise_bv_t(rop); -} - -void add_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) { - rop->len = op1.len; - mpz_add(*rop->bits, *op1.bits, op2); - normalise_bv_t(rop); -} - -void sub_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) { - rop->len = op1.len; - mpz_sub(*rop->bits, *op1.bits, op2); -} - -void mults_vec(bv_t *rop, const bv_t op1, const bv_t op2) { - mpz_t op1_int, op2_int; - mpz_init(op1_int); - mpz_init(op2_int); - sint(&op1_int, op1); - sint(&op2_int, op2); - rop->len = op1.len * 2; - mpz_mul(*rop->bits, op1_int, op2_int); - normalise_bv_t(rop); - mpz_clear(op1_int); - mpz_clear(op2_int); -} - -void mult_vec(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len * 2; - mpz_mul(*rop->bits, *op1.bits, *op2.bits); - normalise_bv_t(rop); /* necessary? */ -} - -void shift_bits_left(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits)); - normalise_bv_t(rop); -} - -void shift_bits_right(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits)); -} - -/* FIXME */ -void shift_bits_right_arith(bv_t *rop, const bv_t op1, const bv_t op2) { - rop->len = op1.len; - mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits); - mp_bitcnt_t sign_bit = op1.len - 1; - mpz_fdiv_q_2exp(*rop->bits, *op1.bits, shift_amt); - if(mpz_tstbit(*op1.bits, sign_bit) != 0) { - /* */ - for(; shift_amt > 0; shift_amt--) { - mpz_setbit(*rop->bits, sign_bit - shift_amt + 1); - } - } -} - -void reverse_endianness(bv_t *rop, const bv_t op) { - rop->len = op.len; - if (rop->len == 64ul) { - uint64_t x = mpz_get_ui(*op.bits); - x = (x & 0xFFFFFFFF00000000) >> 32 | (x & 0x00000000FFFFFFFF) << 32; - x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16; - x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8; - mpz_set_ui(*rop->bits, x); - } else if (rop->len == 32ul) { - uint64_t x = mpz_get_ui(*op.bits); - x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16; - x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8; - mpz_set_ui(*rop->bits, x); - } else if (rop->len == 16ul) { - uint64_t x = mpz_get_ui(*op.bits); - x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8; - mpz_set_ui(*rop->bits, x); - } else if (rop->len == 8ul) { - mpz_set(*rop->bits, *op.bits); - } else { - /* For other numbers of bytes we reverse the bytes. - * XXX could use mpz_import/export for this. */ - mpz_set_ui(sail_lib_tmp1, 0xff); // byte mask - mpz_set_ui(*rop->bits, 0); // reset accumulator for result - for(mp_bitcnt_t byte = 0; byte < op.len; byte+=8) { - mpz_tdiv_q_2exp(sail_lib_tmp2, *op.bits, byte); // shift byte to bottom - mpz_and(sail_lib_tmp2, sail_lib_tmp2, sail_lib_tmp1); // and with mask - mpz_mul_2exp(*rop->bits, *rop->bits, 8); // shift result left 8 - mpz_ior(*rop->bits, *rop->bits, sail_lib_tmp2); // or byte into result - } - } -} - -// Takes a slice of the (two's complement) binary representation of -// integer n, starting at bit start, and of length len. With the -// argument in the following order: -// -// get_slice_int(len, n, start) -// -// For example: -// -// get_slice_int(8, 1680, 4) = -// -// 11 0 -// V V -// get_slice_int(8, 0b0110_1001_0000, 4) = 0b0110_1001 -// <-------^ -// (8 bit) 4 -// -void get_slice_int(bv_t *rop, const mpz_t len_mpz, const mpz_t n, const mpz_t start_mpz) -{ - uint64_t start = mpz_get_ui(start_mpz); - uint64_t len = mpz_get_ui(len_mpz); - - mpz_set_ui(*rop->bits, 0ul); - rop->len = len; - - for (uint64_t i = 0; i < len; i++) { - if (mpz_tstbit(n, i + start)) mpz_setbit(*rop->bits, i); - } -} - -// Set slice uses the same indexing scheme as get_slice_int, but it -// puts a bitvector slice into an integer rather than returning it. -void set_slice_int(mpz_t *rop, - const mpz_t len_mpz, - const mpz_t n, - const mpz_t start_mpz, - const bv_t slice) -{ - uint64_t start = mpz_get_ui(start_mpz); - - mpz_set(*rop, n); - - for (uint64_t i = 0; i < slice.len; i++) { - if (mpz_tstbit(*slice.bits, i)) { - mpz_setbit(*rop, i + start); - } else { - mpz_clrbit(*rop, i + start); - } - } -} - -// This is a bit of a hack to let us optimize away the Align__1 -// function in aarch64. -void arm_align(bv_t *rop, const bv_t x_bv, const mpz_t y_mpz) { - uint64_t x = mpz_get_ui(*x_bv.bits); - uint64_t y = mpz_get_ui(y_mpz); - uint64_t z = y * (x / y); - mp_bitcnt_t n = x_bv.len; - mpz_set_ui(*rop->bits, safe_rshift(UINT64_MAX, 64l - (n - 1)) & z); - rop->len = n; -} - -void vector_update_subrange_bv_t(bv_t *rop, - const bv_t op, - const mpz_t n_mpz, - const mpz_t m_mpz, - const bv_t slice) -{ - uint64_t n = mpz_get_ui(n_mpz); - uint64_t m = mpz_get_ui(m_mpz); - - mpz_set(*rop->bits, *op.bits); - - for (uint64_t i = 0; i < n - (m - 1ul); i++) { - if (mpz_tstbit(*slice.bits, i)) { - mpz_setbit(*rop->bits, i + m); - } else { - mpz_clrbit(*rop->bits, i + m); - } - } -} - -void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, const mpz_t m_mpz) -{ - uint64_t n = mpz_get_ui(n_mpz); - uint64_t m = mpz_get_ui(m_mpz); - - rop->len = n - (m - 1ul); - mpz_fdiv_q_2exp(*rop->bits, *op.bits, m); - normalise_bv_t(rop); - - /* mpz_set_ui(*rop->bits, 0ul); */ - /* rop->len = n - (m - 1ul); */ - - /* for (uint64_t i = 0; i < rop->len; i++) { */ - /* if (mpz_tstbit(*op.bits, i + m)) { */ - /* mpz_setbit(*rop->bits, i); */ - /* } else { */ - /* mpz_clrbit(*rop->bits, i); */ - /* } */ - /* } */ -} - -int bitvector_access(const bv_t op, const mpz_t n_mpz) { - uint64_t n = mpz_get_ui(n_mpz); - return mpz_tstbit(*op.bits, n); -} - -// Like slice but slices from a hexadecimal string. -void hex_slice (bv_t *rop, const sail_string hex, const mpz_t len_mpz, const mpz_t start_mpz) { - mpz_t op; - mpz_init_set_str(op, hex, 0); - get_slice_int(rop, len_mpz, op, start_mpz); - mpz_clear(op); -} - -void set_slice (bv_t *rop, - const mpz_t len_mpz, - const mpz_t slen_mpz, - const bv_t op, - const mpz_t start_mpz, - const bv_t slice) -{ - uint64_t start = mpz_get_ui(start_mpz); - - mpz_set(*rop->bits, *op.bits); - rop->len = op.len; - - for (uint64_t i = 0; i < slice.len; i++) { - if (mpz_tstbit(*slice.bits, i)) { - mpz_setbit(*rop->bits, i + start); - } else { - mpz_clrbit(*rop->bits, i + start); - } - } -} - -// ***** Real number implementation ***** - -#define REAL_FLOAT - -#ifdef REAL_FLOAT - -typedef mpf_t real; - -#define FLOAT_PRECISION 255 - -void init_real(real *rop) { - mpf_init(*rop); -} - -void reinit_real(real *rop) { - mpf_set_ui(*rop, 0); -} - -void clear_real(real *rop) { - mpf_clear(*rop); -} - -void set_real(real *rop, const real op) { - mpf_set(*rop, op); -} - -void undefined_real(real *rop, unit u) { - mpf_set_ui(*rop, 0ul); -} - -void neg_real(real *rop, const real op) { - mpf_neg(*rop, op); -} - -void mult_real(real *rop, const real op1, const real op2) { - mpf_mul(*rop, op1, op2); -} - -void sub_real(real *rop, const real op1, const real op2) { - mpf_sub(*rop, op1, op2); -} - -void add_real(real *rop, const real op1, const real op2) { - mpf_add(*rop, op1, op2); -} - -void div_real(real *rop, const real op1, const real op2) { - mpf_div(*rop, op1, op2); -} - -void sqrt_real(real *rop, const real op) { - mpf_sqrt(*rop, op); -} - -void abs_real(real *rop, const real op) { - mpf_abs(*rop, op); -} - -void round_up(mpz_t *rop, const real op) { - mpf_t x; - mpf_init(x); - mpf_ceil(x, op); - mpz_set_ui(*rop, mpf_get_ui(x)); - mpf_clear(x); -} - -void round_down(mpz_t *rop, const real op) { - mpf_t x; - mpf_init(x); - mpf_floor(x, op); - mpz_set_ui(*rop, mpf_get_ui(x)); - mpf_clear(x); -} - -void to_real(real *rop, const mpz_t op) { - mpf_set_z(*rop, op); -} +/* + * Integers can be either stack-allocated as 128-bit integers if + * __int128 is available, or use GMP arbitrary precision + * integers. This affects the function signatures, so use a macro to + * paper over the differences. + */ +#ifndef USE_INT128 -bool eq_real(const real op1, const real op2) { - return mpf_cmp(op1, op2) == 0; -} +typedef mpz_t sail_int; -bool lt_real(const real op1, const real op2) { - return mpf_cmp(op1, op2) < 0; -} +#define SAIL_INT_FUNCTION(fname, rtype, ...) void fname(rtype*, __VA_ARGS__) -bool gt_real(const real op1, const real op2) { - return mpf_cmp(op1, op2) > 0; -} +SAIL_BUILTIN_TYPE(sail_int); -bool lteq_real(const real op1, const real op2) { - return mpf_cmp(op1, op2) <= 0; -} +void CREATE_OF(sail_int, mach_int)(sail_int *, const mach_int); +void RECREATE_OF(sail_int, mach_int)(sail_int *, const mach_int); -bool gteq_real(const real op1, const real op2) { - return mpf_cmp(op1, op2) >= 0; -} +void CREATE_OF(sail_int, sail_string)(sail_int *, const sail_string); +void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string); -void real_power(real *rop, const real base, const mpz_t exp) { - uint64_t exp_ui = mpz_get_ui(exp); - mpf_pow_ui(*rop, base, exp_ui); -} +mach_int CONVERT_OF(mach_int, sail_int)(const sail_int); +void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int); + +#else -void init_real_of_sail_string(real *rop, const sail_string op) { - // FIXME - mpf_init(*rop); -} +typedef __int128 sail_int; +#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__) #endif -/* ***** Sail memory builtins ***** */ - -/* We organise memory available to the sail model into a linked list - of dynamically allocated MASK + 1 size blocks. The most recently - written block is moved to the front of the list, so contiguous - accesses should be as fast as possible. */ - -struct block { - uint64_t block_id; - uint8_t *mem; - struct block *next; -}; - -struct block *sail_memory = NULL; - -/* Must be one less than a power of two. */ -uint64_t MASK = 0xFFFFFFul; - -// All sail vectors are at least 64-bits, but only the bottom 8 bits -// are used in the second argument. -void write_mem(uint64_t address, uint64_t byte) -{ - //printf("ADDR: %lu, BYTE: %lu\n", address, byte); - - uint64_t mask = address & ~MASK; - uint64_t offset = address & MASK; - - struct block *current = sail_memory; - - while (current != NULL) { - if (current->block_id == mask) { - current->mem[offset] = (uint8_t) byte; - return; - } else { - current = current->next; - } - } - - /* If we couldn't find a block matching the mask, allocate a new - one, write the byte, and put it at the front of the block - list. */ - fprintf(stderr, "[Sail] Allocating new block 0x%" PRIx64 "\n", mask); - struct block *new_block = malloc(sizeof(struct block)); - new_block->block_id = mask; - new_block->mem = calloc(MASK + 1, sizeof(uint8_t)); - new_block->mem[offset] = (uint8_t) byte; - new_block->next = sail_memory; - sail_memory = new_block; -} - -uint64_t read_mem(uint64_t address) -{ - uint64_t mask = address & ~MASK; - uint64_t offset = address & MASK; - - struct block *current = sail_memory; - - while (current != NULL) { - if (current->block_id == mask) { - return (uint64_t) current->mem[offset]; - } else { - current = current->next; - } - } - - return 0x58; -} - -void kill_mem() -{ - while (sail_memory != NULL) { - struct block *next = sail_memory->next; - - free(sail_memory->mem); - free(sail_memory); - - sail_memory = next; - } -} - -// ***** ARM Memory builtins ***** - -// These memory builtins are intended to match the semantics for the -// __ReadRAM and __WriteRAM functions in ASL. - -unit write_ram(const mpz_t addr_size, // Either 32 or 64 - const mpz_t data_size_mpz, // Number of bytes - const bv_t hex_ram, // Currently unused - const bv_t addr_bv, - const bv_t data) -{ - uint64_t addr = mpz_get_ui(*addr_bv.bits); - uint64_t data_size = mpz_get_ui(data_size_mpz); - - mpz_t buf; - mpz_init_set(buf, *data.bits); - - uint64_t byte; - for(uint64_t i = 0; i < data_size; ++i) { - // Take the 8 low bits of buf and write to addr. - byte = mpz_get_ui(buf) & 0xFF; - write_mem(addr + i, byte); - - // Then shift buf 8 bits right. - mpz_fdiv_q_2exp(buf, buf, 8); - } +/* + * Comparison operators for integers + */ +bool eq_int(const sail_int, const sail_int); - mpz_clear(buf); - return UNIT; -} +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); -void read_ram(bv_t *data, - const mpz_t addr_size, - const mpz_t data_size_mpz, - const bv_t hex_ram, - const bv_t addr_bv) -{ - uint64_t addr = mpz_get_ui(*addr_bv.bits); - uint64_t data_size = mpz_get_ui(data_size_mpz); +/* + * Left and right shift for integers + */ +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); - mpz_set_ui(*data->bits, 0); - data->len = data_size * 8; +/* + * 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); - mpz_t byte; - mpz_init(byte); - for(uint64_t i = data_size; i > 0; --i) { - mpz_set_ui(byte, read_mem(addr + (i - 1))); - mpz_mul_2exp(*data->bits, *data->bits, 8); - mpz_add(*data->bits, *data->bits, byte); - } +/* + * 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(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); - mpz_clear(byte); -} +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); -unit load_raw(uint64_t addr, const sail_string file) { - fprintf(stderr, "[Sail] Loading %s from 0x%" PRIx64 " to ", file, addr); - FILE *fp = fopen(file, "r"); +SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int); +SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int); - uint64_t byte; - while ((byte = (uint64_t)fgetc(fp)) != EOF) { - write_mem(addr, byte); - addr++; - } +SAIL_INT_FUNCTION(pow2, sail_int, const sail_int); - fprintf(stderr, "0x%" PRIx64 "\n", addr - 1); +/* ***** Sail bitvectors ***** */ - return UNIT; -} +typedef uint64_t mach_bits; -void load_image(char *file) { - FILE *fp = fopen(file, "r"); +bool eq_bit(const mach_bits a, const mach_bits b); - if (!fp) { - fprintf(stderr, "Image file %s could not be loaded\n", file); - exit(EXIT_FAILURE); - } +typedef struct { + mp_bitcnt_t len; + mpz_t *bits; +} sail_bits; - char *addr = NULL; - char *data = NULL; - size_t len = 0; +SAIL_BUILTIN_TYPE(sail_bits); - while (true) { - ssize_t addr_len = getline(&addr, &len, fp); - if (addr_len == -1) break; - ssize_t data_len = getline(&data, &len, fp); - if (data_len == -1) break; +void CREATE_OF(sail_bits, mach_bits)(sail_bits *, + const mach_bits op, + const mach_bits len, + const bool direction); - if (!strcmp(addr, "elf_entry\n")) { - if (sscanf(data, "%" PRIu64 "\n", &g_elf_entry) != 1) { - fprintf(stderr, "Failed to parse elf_entry\n"); - exit(EXIT_FAILURE); - }; - printf("Elf entry point: %" PRIx64 "\n", g_elf_entry); - } else { - write_mem((uint64_t) atoll(addr), (uint64_t) atoll(data)); - } - } +void RECREATE_OF(sail_bits, mach_bits)(sail_bits *, + const mach_bits op, + const mach_bits len, + const bool direction); - free(addr); - free(data); - fclose(fp); -} +mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits); -// ***** Setup and cleanup functions for library code ***** +void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit); +mach_bits UNDEFINED(mach_bits)(const unit); -static int64_t g_trace_depth; -static bool g_trace_enabled; +/* + * Wrapper around >> operator to avoid UB when shift amount is greater + * than or equal to 64. + */ +mach_bits safe_rshift(const mach_bits, const mach_bits); /* - * Bind these functions in Sail to enable and disable tracing: - * - * val "enable_tracing" : unit -> unit - * val "disable_tracing" : unit -> unit - * - * Compile with sail -c -c_trace. + * Used internally to construct large bitvector literals. */ -unit enable_tracing(const unit u) -{ - g_trace_depth = 0; - g_trace_enabled = true; - return UNIT; -} - -unit disable_tracing(const unit u) -{ - g_trace_depth = 0; - g_trace_enabled = false; - return UNIT; -} +void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk); -void trace_bv_t(const bv_t op) -{ - if (g_trace_enabled) { - if (op.len % 4 == 0) { - fputs("0x", stderr); - mpz_t buf; - mpz_init_set(buf, *op.bits); +void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); - char *hex = malloc((op.len / 4) * sizeof(char)); +void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2); +void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2); - for (int i = 0; i < op.len / 4; ++i) { - char c = (char) ((0xF & mpz_get_ui(buf)) + 0x30); - hex[i] = (c < 0x3A) ? c : c + 0x7; - mpz_fdiv_q_2exp(buf, buf, 4); - } +void zeros(sail_bits *rop, const sail_int op); +void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len); - for (int i = op.len / 4; i > 0; --i) { - fputc(hex[i - 1], stderr); - } +void length_sail_bits(sail_int *rop, const sail_bits op); - free(hex); - mpz_clear(buf); - } else { - fputs("0b", stderr); - for (int i = op.len; i > 0; --i) { - fputc(mpz_tstbit(*op.bits, i - 1) + 0x30, stderr); - } - } - } -} +bool eq_bits(const sail_bits op1, const sail_bits op2); -void trace_uint64_t(const uint64_t x) { - if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x); -} +void vector_subrange_sail_bits(sail_bits *rop, + const sail_bits op, + const sail_int n_mpz, + const sail_int m_mpz); -void trace_sail_string(const sail_string str) { - if (g_trace_enabled) fprintf(stderr, "\"%s\"", str); -} +void truncate(sail_bits *rop, const sail_bits op, const sail_int len); -void trace_unit(const unit u) { - if (g_trace_enabled) fputs("()", stderr); -} +mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz); -void trace_mpz_t(const mpz_t op) { - if (g_trace_enabled) mpz_out_str(stderr, 10, op); -} +void sail_unsigned(sail_int *rop, const sail_bits op); +void sail_signed(sail_int *rop, const sail_bits op); -void trace_bool(const bool b) { - if (g_trace_enabled) { - if (b) { - fprintf(stderr, "true"); - } else { - fprintf(stderr, "false"); - } - } -} +/* ***** Sail reals ***** */ -void trace_unknown(void) { - if (g_trace_enabled) fputs("?", stderr); -} +/* ***** Printing ***** */ -void trace_argsep(void) { - if (g_trace_enabled) fputs(", ", stderr); -} - -void trace_argend(void) { - if (g_trace_enabled) fputs(")\n", stderr); -} - -void trace_retend(void) { - if (g_trace_enabled) fputs("\n", stderr); -} - -void trace_start(char *name) -{ - if (g_trace_enabled) { - fprintf(stderr, "[TRACE] "); - for (int64_t i = 0; i < g_trace_depth; ++i) { - fprintf(stderr, "%s", "| "); - } - fprintf(stderr, "%s(", name); - } -} - -void trace_end(void) -{ - if (g_trace_enabled) { - fprintf(stderr, "[TRACE] "); - for (int64_t i = 0; i < g_trace_depth; ++i) { - fprintf(stderr, "%s", "| "); - } - } -} +/* + * Utility function not callable from Sail! + */ +void fprint_bits(const sail_string pre, + const sail_bits op, + const sail_string post, + FILE *stream); -// ***** Setup and cleanup functions for library code ***** +unit print_bits(const sail_string str, const sail_bits op); +unit prerr_bits(const sail_string str, const sail_bits op); -void setup_library(void) { - disable_tracing(UNIT); - mpf_set_default_prec(FLOAT_PRECISION); - mpz_init(sail_lib_tmp1); - mpz_init(sail_lib_tmp2); -} +unit print(const sail_string str); +unit print_endline(const sail_string str); -void cleanup_library(void) { - mpz_clear(sail_lib_tmp1); - mpz_clear(sail_lib_tmp2); - kill_mem(); -} +unit prerr(const sail_string str); +unit prerr_endline(const sail_string str); -#endif +unit print_int(const sail_string str, const sail_int op); +unit prerr_int(const sail_string str, const sail_int op); diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index ad59f50e..cff5d4d3 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -121,10 +121,13 @@ val unsigned = { ocaml: "uint", lem: "uint", interpreter: "uint", - c: "sail_uint", + c: "sail_unsigned", coq: "unsigned" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) -val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) +val signed = { + c: "sail_signed", + _: "sint" +} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) $endif diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index 96513d7f..05709de9 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -161,11 +161,11 @@ and string_of_fragment' ?zencode:(zencode=true) f = (* String representation of ctyps here is only for debugging and intermediate language pretty-printer. *) let rec string_of_ctyp = function - | CT_mpz -> "mpz_t" - | CT_bv true -> "bv_t(dec)" - | CT_bv false -> "bv_t(inc)" - | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)" - | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)" + | CT_int -> "mpz_t" + | CT_bits true -> "bv_t(dec)" + | CT_bits false -> "bv_t(inc)" + | CT_bits64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)" + | CT_bits64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)" | CT_int64 -> "int64_t" | CT_bit -> "bit" | CT_unit -> "unit" diff --git a/src/c_backend.ml b/src/c_backend.ml index 96cd9ed7..7923a49c 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -751,9 +751,9 @@ let initial_ctx env = let rec ctyp_equal ctyp1 ctyp2 = match ctyp1, ctyp2 with - | CT_mpz, CT_mpz -> true - | CT_bv d1, CT_bv d2 -> d1 = d2 - | CT_uint64 (m1, d1), CT_uint64 (m2, d2) -> m1 = m2 && d1 = d2 + | CT_int, CT_int -> true + | CT_bits d1, CT_bits d2 -> d1 = d2 + | CT_bits64 (m1, d1), CT_bits64 (m2, d2) -> m1 = m2 && d1 = d2 | CT_bit, CT_bit -> true | CT_int64, CT_int64 -> true | CT_unit, CT_unit -> true @@ -776,8 +776,8 @@ let rec ctyp_of_typ ctx typ = match typ_aux with | Typ_id id when string_of_id id = "bit" -> CT_bit | Typ_id id when string_of_id id = "bool" -> CT_bool - | Typ_id id when string_of_id id = "int" -> CT_mpz - | Typ_id id when string_of_id id = "nat" -> CT_mpz + | Typ_id id when string_of_id id = "int" -> CT_int + | Typ_id id when string_of_id id = "nat" -> CT_int | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" -> begin match destruct_range Env.empty typ with @@ -792,8 +792,8 @@ let rec ctyp_of_typ ctx typ = if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then (prerr_endline "yes"; CT_int64) else - (prerr_endline "no"; CT_mpz) - | _ -> CT_mpz + (prerr_endline "no"; CT_int) + | _ -> CT_int end | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "list" -> @@ -806,8 +806,8 @@ let rec ctyp_of_typ ctx typ = begin let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in match nexp_simp n with - | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_uint64 (Big_int.to_int n, direction) - | _ -> CT_bv direction + | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_bits64 (Big_int.to_int n, direction) + | _ -> CT_bits direction end | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_order ord, _); @@ -846,8 +846,8 @@ let rec ctyp_of_typ ctx typ = | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ) let rec is_stack_ctyp ctyp = match ctyp with - | CT_uint64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true - | CT_bv _ | CT_mpz | CT_real | CT_string | CT_list _ | CT_vector _ -> false + | CT_bits64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true + | CT_bits _ | CT_int | 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 @@ -1184,17 +1184,17 @@ let rec compile_aval ctx = function | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> let gs = gensym () in - [idecl CT_mpz gs; - iinit CT_mpz gs (F_lit (V_int n), CT_int64)], - (F_id gs, CT_mpz), - [iclear CT_mpz gs] + [idecl CT_int gs; + iinit CT_int gs (F_lit (V_int n), CT_int64)], + (F_id gs, CT_int), + [iclear CT_int gs] | AV_lit (L_aux (L_num n, _), typ) -> let gs = gensym () in - [idecl CT_mpz gs; - iinit CT_mpz gs (F_lit (V_string (Big_int.to_string n)), CT_string)], - (F_id gs, CT_mpz), - [iclear CT_mpz gs] + [idecl CT_int gs; + iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)], + (F_id gs, CT_int), + [iclear CT_int gs] | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail_values.B0), CT_bit), [] | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail_values.B1), CT_bit), [] @@ -1254,9 +1254,9 @@ let rec compile_aval ctx = function let len = List.length avals in match destruct_vector ctx.tc_env typ with | Some (_, Ord_aux (Ord_inc, _), _) -> - [], (bitstring, CT_uint64 (len, false)), [] + [], (bitstring, CT_bits64 (len, false)), [] | Some (_, Ord_aux (Ord_dec, _), _) -> - [], (bitstring, CT_uint64 (len, true)), [] + [], (bitstring, CT_bits64 (len, true)), [] | Some _ -> c_error "Encountered order polymorphic bitvector literal" | None -> @@ -1271,14 +1271,14 @@ let rec compile_aval ctx = function let first_chunk = bitstring (Util.take (len mod 64) avals) in let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in let gs = gensym () in - [idecl (CT_bv true) gs; - iinit (CT_bv true) gs (first_chunk, CT_uint64 (len mod 64, true))] + [idecl (CT_bits true) gs; + iinit (CT_bits true) gs (first_chunk, CT_bits64 (len mod 64, true))] @ List.map (fun chunk -> ifuncall (CL_id gs) (mk_id "append_64") - [(F_id gs, CT_bv true); (chunk, CT_uint64 (64, true))] - (CT_bv true)) chunks, - (F_id gs, CT_bv true), - [iclear (CT_bv true) gs] + [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))] + (CT_bits true)) chunks, + (F_id gs, CT_bits true), + [iclear (CT_bits true) gs] (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *) | AV_vector (avals, Typ_aux (Typ_app (id, [_; Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id bit_id, _)), _)]), _)) @@ -1290,7 +1290,7 @@ let rec compile_aval ctx = function | Ord_aux (Ord_var _, _) -> c_error "Polymorphic vector direction found" in let gs = gensym () in - let ctyp = CT_uint64 (len, direction) in + let ctyp = CT_bits64 (len, direction) in let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail_values.B0) @ [Sail_values.B1] @ Util.list_init i (fun _ -> Sail_values.B0)) in let aval_mask i aval = let setup, cval, cleanup = compile_aval ctx aval in @@ -2304,7 +2304,7 @@ let rec instrs_rename from_id to_id = | [] -> [] let hoist_ctyp = function - | CT_mpz | CT_bv _ | CT_struct _ -> true + | CT_int | CT_bits _ | CT_struct _ -> true | _ -> false let hoist_counter = ref 0 @@ -2497,12 +2497,12 @@ let upper_codegen_id id = string (upper_sgen_id id) let rec sgen_ctyp = function | CT_unit -> "unit" - | CT_bit -> "uint64_t" + | CT_bit -> "mach_bits" | CT_bool -> "bool" - | CT_uint64 _ -> "uint64_t" - | CT_int64 -> "int64_t" - | CT_mpz -> "mpz_t" - | CT_bv _ -> "bv_t" + | CT_bits64 _ -> "mach_bits" + | CT_int64 -> "mach_int" + | CT_int -> "sail_int" + | CT_bits _ -> "sail_bits" | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> "struct " ^ sgen_id id | CT_enum (id, _) -> "enum " ^ sgen_id id @@ -2515,12 +2515,12 @@ let rec sgen_ctyp = function let rec sgen_ctyp_name = function | CT_unit -> "unit" - | CT_bit -> "uint64_t" + | CT_bit -> "mach_bits" | CT_bool -> "bool" - | CT_uint64 _ -> "uint64_t" - | CT_int64 -> "int64_t" - | CT_mpz -> "mpz_t" - | CT_bv _ -> "bv_t" + | CT_bits64 _ -> "mach_bits" + | CT_int64 -> "mach_int" + | CT_int -> "sail_int" + | CT_bits _ -> "sail_bits" | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> sgen_id id | CT_enum (id, _) -> sgen_id id @@ -2533,9 +2533,9 @@ let rec sgen_ctyp_name = function let sgen_cval_param (frag, ctyp) = match ctyp with - | CT_bv direction -> + | CT_bits direction -> string_of_fragment frag ^ ", " ^ string_of_bool direction - | CT_uint64 (len, direction) -> + | CT_bits64 (len, direction) -> string_of_fragment frag ^ ", " ^ string_of_int len ^ "ul , " ^ string_of_bool direction | _ -> string_of_fragment frag @@ -2567,7 +2567,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = if is_stack_ctyp ctyp then string (Printf.sprintf " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) else - string (Printf.sprintf " set_%s(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval)) + string (Printf.sprintf " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval)) | I_jump (cval, label) -> string (Printf.sprintf " if (%s) goto %s;" (sgen_cval cval) label) | I_if (cval, [then_instr], [], ctyp) -> @@ -2620,43 +2620,44 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = end | "vector_update_subrange", _ -> Printf.sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp) | "vector_subrange", _ -> Printf.sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp) - | "vector_update", CT_uint64 _ -> "update_uint64_t" - | "vector_update", CT_bv _ -> "update_bv" + | "vector_update", CT_bits64 _ -> "update_uint64_t" + | "vector_update", CT_bits _ -> "update_bv" | "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) - | "undefined_vector", CT_uint64 _ -> "undefined_uint64_t" - | "undefined_vector", CT_bv _ -> "undefined_bv_t" - | "undefined_vector", _ -> Printf.sprintf "undefined_vector_%s" (sgen_ctyp_name ctyp) + | "undefined_vector", CT_bits64 _ -> "UNDEFINED(mach_bits)" + | "undefined_vector", CT_bits _ -> "UNDEFINED(sail_bits)" + | "undefined_bit", _ -> "UNDEFINED(mach_bits)" + | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) | fname, _ -> fname in if fname = "reg_deref" then if is_stack_ctyp ctyp then string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args) else - string (Printf.sprintf " set_%s(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) + string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) else if is_stack_ctyp ctyp then string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) else string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) | I_clear (ctyp, id) -> - string (Printf.sprintf " clear_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) | I_init (ctyp, id, cval) -> - string (Printf.sprintf " init_%s_of_%s(&%s, %s);" + string (Printf.sprintf " CREATE_OF(%s, %s)(&%s, %s);" (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_id id) (sgen_cval_param cval)) | I_alloc (ctyp, id) -> - string (Printf.sprintf " init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) | I_reinit (ctyp, id, cval) -> - string (Printf.sprintf " reinit_%s_of_%s(&%s, %s);" + string (Printf.sprintf " RECREATE_OF(%s, %s)(&%s, %s);" (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_id id) (sgen_cval_param cval)) | I_reset (ctyp, id) -> - string (Printf.sprintf " reinit_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) (* FIXME: This just covers the cases we see in our specs, need a special conversion code-generator for full generality *) | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 -> @@ -2666,7 +2667,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = else if ctyp_equal ctyp1 ctyp2 then c_error "heap tuple type conversion" else if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s.ztup%i = convert_%s_of_%s(%s.ztup%i);" + string (Printf.sprintf " %s.ztup%i = CONVERT_OF(%s, %s)(%s.ztup%i);" (sgen_clexp_pure x) i (sgen_ctyp_name ctyp1) @@ -2674,7 +2675,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = (sgen_id y) i) else - string (Printf.sprintf " convert_%s_of_%s(%s.ztup%i, %s.ztup%i);" + string (Printf.sprintf " CONVERT_OF(%s, %s)(%s.ztup%i, %s.ztup%i);" (sgen_ctyp_name ctyp1) (sgen_ctyp_name ctyp2) (sgen_clexp x) @@ -2685,13 +2686,13 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = separate hardline (List.mapi convert (List.map2 (fun x y -> (x, y)) ctyps1 ctyps2)) | I_convert (x, ctyp1, y, ctyp2) -> if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s = convert_%s_of_%s(%s);" + string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);" (sgen_clexp_pure x) (sgen_ctyp_name ctyp1) (sgen_ctyp_name ctyp2) (sgen_id y)) else - string (Printf.sprintf " convert_%s_of_%s(%s, %s);" + string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s);" (sgen_ctyp_name ctyp1) (sgen_ctyp_name ctyp2) (sgen_clexp x) @@ -2699,7 +2700,7 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = | I_return cval -> string (Printf.sprintf " return %s;" (sgen_cval cval)) | I_throw cval -> - string (Printf.sprintf " THROW(%s)" (sgen_cval cval)) + c_error "I_throw reached code generator" | I_comment str -> string (" /* " ^ str ^ " */") | I_label str -> @@ -2728,10 +2729,10 @@ let codegen_type_def ctx = function if is_stack_ctyp ctyp then string (Printf.sprintf "rop->%s = op.%s;" (sgen_id id) (sgen_id id)) else - string (Printf.sprintf "set_%s(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id)) + string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id)) in let codegen_setter id ctors = - string (let n = sgen_id id in Printf.sprintf "void set_%s(struct %s *rop, const struct %s op)" n n n) ^^ space + string (let n = sgen_id id in Printf.sprintf "void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space ^^ surround 2 0 lbrace (separate_map hardline codegen_set (Bindings.bindings ctors)) rbrace @@ -2739,11 +2740,11 @@ let codegen_type_def ctx = function (* Generate an init/clear_T function for every struct T *) let codegen_field_init f (id, ctyp) = if not (is_stack_ctyp ctyp) then - [string (Printf.sprintf "%s_%s(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_id id))] + [string (Printf.sprintf "%s(%s)(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_id id))] else [] in let codegen_init f id ctors = - string (let n = sgen_id id in Printf.sprintf "void %s_%s(struct %s *op)" f n n) ^^ space + string (let n = sgen_id id in Printf.sprintf "void %s(%s)(struct %s *op)" f n n) ^^ space ^^ surround 2 0 lbrace (separate hardline (Bindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat)) rbrace @@ -2763,11 +2764,11 @@ let codegen_type_def ctx = function ^^ semi ^^ twice hardline ^^ codegen_setter id (ctor_bindings ctors) ^^ twice hardline - ^^ codegen_init "init" id (ctor_bindings ctors) + ^^ codegen_init "CREATE" id (ctor_bindings ctors) ^^ twice hardline - ^^ codegen_init "reinit" id (ctor_bindings ctors) + ^^ codegen_init "RECREATE" id (ctor_bindings ctors) ^^ twice hardline - ^^ codegen_init "clear" id (ctor_bindings ctors) + ^^ codegen_init "KILL" id (ctor_bindings ctors) ^^ twice hardline ^^ codegen_eq @@ -2790,28 +2791,28 @@ let codegen_type_def ctx = function let codegen_init = let n = sgen_id id in let ctor_id, ctyp = List.hd tus in - string (Printf.sprintf "void init_%s(struct %s *op)" n n) + string (Printf.sprintf "void CREATE(%s)(struct %s *op)" n n) ^^ hardline ^^ surround 2 0 lbrace (string (Printf.sprintf "op->kind = Kind_%s;" (sgen_id ctor_id)) ^^ hardline ^^ if not (is_stack_ctyp ctyp) then - string (Printf.sprintf "init_%s(&op->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) + string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) else empty) rbrace in let codegen_reinit = let n = sgen_id id in - string (Printf.sprintf "void reinit_%s(struct %s *op) {}" n n) + string (Printf.sprintf "void RECREATE(%s)(struct %s *op) {}" n n) in let clear_field v ctor_id ctyp = if is_stack_ctyp ctyp then string (Printf.sprintf "/* do nothing */") else - string (Printf.sprintf "clear_%s(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_id ctor_id)) + string (Printf.sprintf "KILL(%s)(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_id ctor_id)) in let codegen_clear = let n = sgen_id id in - string (Printf.sprintf "void clear_%s(struct %s *op)" n n) ^^ hardline + string (Printf.sprintf "void KILL(%s)(struct %s *op)" n n) ^^ hardline ^^ surround 2 0 lbrace (each_ctor "op->" (clear_field "op") tus ^^ semi) rbrace @@ -2828,7 +2829,7 @@ let codegen_type_def ctx = function | CT_tup ctyps -> String.concat ", " (List.mapi (fun i ctyp -> Printf.sprintf "%s op%d" (sgen_ctyp ctyp) i) ctyps), string (Printf.sprintf "%s op;" (sgen_ctyp ctyp)) ^^ hardline - ^^ string (Printf.sprintf "init_%s(&op);" (sgen_ctyp_name ctyp)) ^^ hardline + ^^ string (Printf.sprintf "CREATE(%s)(&op);" (sgen_ctyp_name ctyp)) ^^ hardline ^^ separate hardline (List.mapi tuple_set ctyps) ^^ hardline | ctyp -> Printf.sprintf "%s op" (sgen_ctyp ctyp), empty in @@ -2840,8 +2841,8 @@ let codegen_type_def ctx = function ^^ if is_stack_ctyp ctyp then string (Printf.sprintf "rop->%s = op;" (sgen_id ctor_id)) else - string (Printf.sprintf "init_%s(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline - ^^ string (Printf.sprintf "set_%s(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))) + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline + ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_id ctor_id))) rbrace in let codegen_setter = @@ -2850,10 +2851,10 @@ let codegen_type_def ctx = function if is_stack_ctyp ctyp then string (Printf.sprintf "rop->%s = op.%s;" (sgen_id ctor_id) (sgen_id ctor_id)) else - string (Printf.sprintf "init_%s(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) - ^^ string (Printf.sprintf " set_%s(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id)) + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) + ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id)) in - string (Printf.sprintf "void set_%s(struct %s *rop, struct %s op)" n n n) ^^ hardline + string (Printf.sprintf "void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline ^^ surround 2 0 lbrace (each_ctor "rop->" (clear_field "rop") tus ^^ semi ^^ hardline @@ -2935,14 +2936,14 @@ let codegen_node id ctyp = ^^ string (Printf.sprintf "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id)) let codegen_list_init id = - string (Printf.sprintf "void init_%s(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id)) + string (Printf.sprintf "void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id)) let codegen_list_clear id ctyp = - string (Printf.sprintf "void clear_%s(%s *rop) {\n" (sgen_id id) (sgen_id id)) + string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)) ^^ string (Printf.sprintf " if (*rop == NULL) return;") ^^ (if is_stack_ctyp ctyp then empty - else string (Printf.sprintf " clear_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))) - ^^ string (Printf.sprintf " clear_%s(&(*rop)->tl);\n" (sgen_id id)) + 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 "}" @@ -2953,13 +2954,13 @@ let codegen_list_set id ctyp = ^^ (if is_stack_ctyp ctyp then string " (*rop)->hd = op->hd;\n" else - string (Printf.sprintf " init_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) - ^^ string (Printf.sprintf " set_%s(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp))) + string (Printf.sprintf " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) + ^^ string (Printf.sprintf " COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp))) ^^ string (Printf.sprintf " internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id)) ^^ string "}" ^^ twice hardline - ^^ string (Printf.sprintf "void set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) - ^^ string (Printf.sprintf " clear_%s(rop);\n" (sgen_id id)) + ^^ string (Printf.sprintf "void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id)) ^^ string (Printf.sprintf " internal_set_%s(rop, op);\n" (sgen_id id)) ^^ string "}" @@ -2970,8 +2971,8 @@ let codegen_cons id ctyp = ^^ (if is_stack_ctyp ctyp then string " (*rop)->hd = x;\n" else - string (Printf.sprintf " init_%s(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) - ^^ string (Printf.sprintf " set_%s(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp))) + string (Printf.sprintf " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) + ^^ string (Printf.sprintf " COPY(%s)(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp))) ^^ string " (*rop)->tl = xs;\n" ^^ string "}" @@ -2979,7 +2980,7 @@ let codegen_pick id ctyp = if is_stack_ctyp ctyp then string (Printf.sprintf "%s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id)) else - string (Printf.sprintf "void pick_%s(%s *x, const %s xs) { set_%s(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp)) + string (Printf.sprintf "void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp)) let codegen_list ctx ctyp = let id = mk_id (string_of_ctyp (CT_list ctyp)) in @@ -3007,27 +3008,27 @@ let codegen_vector ctx (direction, ctyp) = ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id)) in let vector_init = - string (Printf.sprintf "void init_%s(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id)) + string (Printf.sprintf "void CREATE(%s)(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id)) in let vector_set = - string (Printf.sprintf "void set_%s(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) - ^^ string (Printf.sprintf " clear_%s(rop);\n" (sgen_id id)) + string (Printf.sprintf "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 " for (int i = 0; i < op.len; i++) {\n" ^^ string (if is_stack_ctyp ctyp then " (rop->data)[i] = op.data[i];\n" else - Printf.sprintf " init_%s((rop->data) + i);\n set_%s((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) ^^ string " }\n" ^^ string "}" in let vector_clear = - string (Printf.sprintf "void clear_%s(%s *rop) {\n" (sgen_id id) (sgen_id id)) + string (Printf.sprintf "void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)) ^^ (if is_stack_ctyp ctyp then empty else string " for (int i = 0; i < (rop->len); i++) {\n" - ^^ string (Printf.sprintf " clear_%s((rop->data) + i);\n" (sgen_ctyp_name ctyp)) + ^^ 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 "}" @@ -3039,13 +3040,13 @@ let codegen_vector ctx (direction, ctyp) = ^^ string (if is_stack_ctyp ctyp then " rop->data[m] = elem;\n" else - Printf.sprintf " set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) ^^ string " } else {\n" - ^^ string (Printf.sprintf " set_%s(rop, op);\n" (sgen_id id)) + ^^ string (Printf.sprintf " COPY(%s)(rop, op);\n" (sgen_id id)) ^^ string (if is_stack_ctyp ctyp then " rop->data[m] = elem;\n" else - Printf.sprintf " set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) ^^ string " }\n" ^^ string "}" in @@ -3054,7 +3055,7 @@ let codegen_vector ctx (direction, ctyp) = ^^ string (if is_stack_ctyp ctyp then " rop->data[n] = elem;\n" else - Printf.sprintf " set_%s((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp)) + Printf.sprintf " COPY(%s)((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp)) ^^ string "}" in let vector_access = @@ -3066,7 +3067,7 @@ let codegen_vector ctx (direction, ctyp) = else string (Printf.sprintf "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 " set_%s(rop, op.data[m]);\n" (sgen_ctyp_name ctyp)) + ^^ string (Printf.sprintf " COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp)) ^^ string "}" in let internal_vector_init = @@ -3083,7 +3084,7 @@ let codegen_vector ctx (direction, ctyp) = ^^ string (if is_stack_ctyp ctyp then " (rop->data)[i] = elem;\n" else - Printf.sprintf " init_%s((rop->data) + i);\n set_%s((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) ^^ string " }\n" ^^ string "}" in @@ -3152,11 +3153,9 @@ let codegen_def' ctx = function ^^ hardline in function_header - (* ^^ string (Printf.sprintf "{ fprintf(stderr, \"%s \"); " (string_of_id id)) *) ^^ string "{" ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline ^^ string "}" - (* ^^ string "}" *) | CDEF_type ctype_def -> codegen_type_def ctx ctype_def @@ -3290,6 +3289,7 @@ let instrument_tracing ctx = let bytecode_ast ctx rewrites (Defs defs) = let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in let exit_vs = Initial_check.extern_of_string dec_ord (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 cdefs = List.concat (List.rev chunks) in @@ -3314,18 +3314,19 @@ let compile_ast ctx (Defs defs) = 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 cdefs = List.concat (List.rev chunks) in - let cdefs = List.map (instrument_tracing ctx) (optimize ctx cdefs) in + let cdefs = optimize ctx cdefs in let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline - [ string "#include \"sail.h\"" ] + [ string "#include \"sail.h\""; + string "#include \"rts.h\""] in let exn_boilerplate = if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else ([ " current_exception = malloc(sizeof(struct zexception));"; - " init_zexception(current_exception);" ], - [ " clear_zexception(current_exception);"; + " CREATE(zexception)(current_exception);" ], + [ " KILL(zexception)(current_exception);"; " free(current_exception);"; " if (have_exception) fprintf(stderr, \"Exiting due to uncaught exception\\n\");" ]) in @@ -3349,15 +3350,15 @@ let compile_ast ctx (Defs defs) = if is_stack_ctyp ctyp then [], [] else - [ Printf.sprintf " init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ], - [ Printf.sprintf " clear_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ] + [ Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ], + [ Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ] in let postamble = separate hardline (List.map string ( [ "int main(int argc, char *argv[])"; "{"; " if (argc > 1) { load_image(argv[1]); }"; - " setup_library();" ] + " setup_rts();" ] @ fst exn_boilerplate @ startup cdefs @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs) @@ -3368,7 +3369,7 @@ let compile_ast ctx (Defs defs) = @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs) @ finish cdefs @ snd exn_boilerplate - @ [ " cleanup_library();"; + @ [ " cleanup_rts();"; " return EXIT_SUCCESS;"; "}" ] )) in diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh index 0990938d..b1ead724 100755 --- a/test/c/run_tests.sh +++ b/test/c/run_tests.sh @@ -54,7 +54,7 @@ function run_c_tests { if $SAILDIR/sail -no_warn -c $SAIL_OPTS $file 1> ${file%.sail}.c 2> /dev/null; then green "compiling $(basename $file) ($SAIL_OPTS)" "ok"; - if gcc $CC_OPTS ${file%.sail}.c -lgmp -I $SAILDIR/lib; + if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -I $SAILDIR/lib; then green "compiling $(basename ${file%.sail}.c) ($CC_OPTS)" "ok"; $DIR/a.out 1> ${file%.sail}.result 2> /dev/null; -- cgit v1.2.3 From e2da03c11fa37f82d24f3a11c93aca7537a97f6a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 15 Jun 2018 15:11:13 +0100 Subject: Fixes for C RTS for aarch64 no it's split into multiple files Fix a bug involving indentifers on the left hand side of assignment statements not being shadowed correctly within foreach loops. Make the different between different types of integer division explicit in at least the C compilation for now. fdiv_int is division rounding towards -infinity (floor). while tdiv_int is truncating towards zero. Same for fmod_int and tmod_int. --- lib/arith.sail | 4 +- lib/rts.c | 54 ++++++- lib/rts.h | 32 +++- lib/sail.c | 341 +++++++++++++++++++++++++++++++++++++++- lib/sail.h | 83 +++++++++- lib/smt.sail | 4 +- src/c_backend.ml | 26 ++- src/sail.ml | 6 +- test/c/assign_rename_bug.expect | 28 ++++ test/c/assign_rename_bug.sail | 35 +++++ 10 files changed, 584 insertions(+), 29 deletions(-) create mode 100644 test/c/assign_rename_bug.expect create mode 100644 test/c/assign_rename_bug.sail diff --git a/lib/arith.sail b/lib/arith.sail index f713805a..e5d2d6ea 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -54,7 +54,7 @@ val div_int = { smt: "div", ocaml: "quotient", lem: "integerDiv", - c: "div_int", + c: "tdiv_int", coq: "Z.quot" } : (int, int) -> int @@ -64,7 +64,7 @@ val mod_int = { smt: "mod", ocaml: "modulus", lem: "integerMod", - c: "mod_int", + c: "tmod_int", coq: "Z.rem" } : (int, int) -> int diff --git a/lib/rts.c b/lib/rts.c index b098ae0e..61f772cf 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -16,6 +16,18 @@ unit sail_assert(bool b, sail_string msg) exit(EXIT_FAILURE); } +unit sail_exit(unit u) +{ + exit(EXIT_SUCCESS); + return UNIT; +} + +unit sleep_request(const unit u) +{ + fprintf(stderr, "Sail model going to sleep\n"); + exit(EXIT_SUCCESS); +} + /* ***** Sail memory builtins ***** */ /* @@ -151,6 +163,19 @@ void read_ram(sail_bits *data, mpz_clear(byte); } +unit load_raw(mach_bits addr, const sail_string file) +{ + FILE *fp = fopen(file, "r"); + + uint64_t byte; + while ((byte = (uint64_t)fgetc(fp)) != EOF) { + write_mem(addr, byte); + addr++; + } + + return UNIT; +} + void load_image(char *file) { FILE *fp = fopen(file, "r"); @@ -201,7 +226,12 @@ unit disable_tracing(const unit u) return UNIT; } -void trace_uint64_t(const uint64_t x) { +bool is_tracing(const unit u) +{ + return g_trace_enabled; +} + +void trace_mach_bits(const mach_bits x) { if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x); } @@ -209,10 +239,18 @@ void trace_unit(const unit u) { if (g_trace_enabled) fputs("()", stderr); } -void trace_mpz_t(const mpz_t op) { +void trace_sail_string(const sail_string str) { + if (g_trace_enabled) fputs(str, stderr); +} + +void trace_sail_int(const sail_int op) { if (g_trace_enabled) mpz_out_str(stderr, 10, op); } +void trace_sail_bits(const sail_bits op) { + if (g_trace_enabled) fprint_bits("", op, "", stderr); +} + void trace_bool(const bool b) { if (g_trace_enabled) { if (b) { @@ -247,6 +285,7 @@ void trace_start(char *name) fprintf(stderr, "%s", "| "); } fprintf(stderr, "%s(", name); + g_trace_depth++; } } @@ -257,9 +296,20 @@ void trace_end(void) for (int64_t i = 0; i < g_trace_depth; ++i) { fprintf(stderr, "%s", "| "); } + g_trace_depth--; } } +/* ***** ELF functions ***** */ + +void elf_entry(mpz_t *rop, const unit u) { + mpz_set_ui(*rop, g_elf_entry); +} + +void elf_tohost(mpz_t *rop, const unit u) { + mpz_set_ui(*rop, 0x0ul); +} + /* ***** Setup and cleanup functions for RTS ***** */ void setup_rts(void) diff --git a/lib/rts.h b/lib/rts.h index de32ef8d..f86962c4 100644 --- a/lib/rts.h +++ b/lib/rts.h @@ -12,12 +12,21 @@ */ void sail_match_failure(sail_string msg); -/* +/* * sail_assert implements the assert construct in Sail. If any * assertion fails we immediately exit the model. */ unit sail_assert(bool b, sail_string msg); +unit sail_exit(unit); + +/* + * ASL->Sail model has an EnterLowPowerState() function that calls a + * sleep request builtin. If it gets called we print a message and + * exit the model. + */ +unit sleep_request(const unit u); + /* ***** Memory builtins ***** */ // These memory builtins are intended to match the semantics for the @@ -35,6 +44,8 @@ void read_ram(sail_bits *data, const sail_bits hex_ram, const sail_bits addr_bv); +unit load_raw(mach_bits addr, const sail_string file); + void load_image(char *); /* ***** Tracing ***** */ @@ -43,16 +54,20 @@ static int64_t g_trace_depth; static bool g_trace_enabled; /* - * Bind these functions in Sail to enable and disable tracing: + * Bind these functions in Sail to enable and disable tracing (see + * lib/trace.sail): * * val "enable_tracing" : unit -> unit * val "disable_tracing" : unit -> unit + * val "is_tracing" : unit -> bool * * Compile with sail -c -c_trace. */ unit enable_tracing(const unit); unit disable_tracing(const unit); +bool is_tracing(const unit); + /* * Tracing is implemented by void trace_TYPE functions, each of which * takes the Sail value to print as the first argument, and prints it @@ -68,7 +83,11 @@ unit disable_tracing(const unit); */ void trace_sail_int(const sail_int); void trace_bool(const bool); - +void trace_unit(const unit); +void trace_sail_string(const sail_string); +void trace_mach_bits(const mach_bits); +void trace_sail_bits(const sail_bits); + void trace_unknown(void); void trace_argsep(void); void trace_argend(void); @@ -76,8 +95,15 @@ void trace_retend(void); void trace_start(char *); void trace_end(void); +/* + * Functions to get info from ELF files. + */ + static uint64_t g_elf_entry; +void elf_entry(sail_int *rop, const unit u); +void elf_tohost(sail_int *rop, const unit u); + /* * setup_rts and cleanup_rts are responsible for calling setup_library * and cleanup_library in sail.h. diff --git a/lib/sail.c b/lib/sail.c index 5fd7a04e..13f1a0e8 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -27,6 +27,16 @@ void cleanup_library(void) mpz_clear(sail_lib_tmp2); } +bool eq_unit(const unit a, const unit b) +{ + return true; +} + +unit UNDEFINED(unit)(const unit u) +{ + return UNIT; +} + /* ***** Sail bit type ***** */ bool eq_bit(const mach_bits a, const mach_bits b) @@ -50,43 +60,60 @@ bool UNDEFINED(bool)(const unit u) { /* ***** Sail strings ***** */ -void CREATE(sail_string)(sail_string *str) { +void CREATE(sail_string)(sail_string *str) +{ char *istr = (char *) malloc(1 * sizeof(char)); istr[0] = '\0'; *str = istr; } -void RECREATE(sail_string)(sail_string *str) { +void RECREATE(sail_string)(sail_string *str) +{ free(*str); char *istr = (char *) malloc(1 * sizeof(char)); istr[0] = '\0'; *str = istr; } -void COPY(sail_string)(sail_string *str1, const sail_string str2) { +void COPY(sail_string)(sail_string *str1, const sail_string str2) +{ size_t len = strlen(str2); *str1 = realloc(*str1, len + 1); *str1 = strcpy(*str1, str2); } -void KILL(sail_string)(sail_string *str) { +void KILL(sail_string)(sail_string *str) +{ free(*str); } -void dec_str(sail_string *str, const mpz_t n) { +void dec_str(sail_string *str, const mpz_t n) +{ free(*str); gmp_asprintf(str, "%Zd", n); } -void hex_str(sail_string *str, const mpz_t n) { +void hex_str(sail_string *str, const mpz_t n) +{ free(*str); gmp_asprintf(str, "0x%Zx", n); } -bool eq_string(const sail_string str1, const sail_string str2) { +bool eq_string(const sail_string str1, const sail_string str2) +{ return strcmp(str1, str2) == 0; } +void undefined_string(sail_string *str, const unit u) {} + +void concat_str(sail_string *stro, const sail_string str1, const sail_string str2) +{ + *stro = realloc(*stro, strlen(str1) + strlen(str2) + 1); + (*stro)[0] = '\0'; + strcat(*stro, str1); + strcat(*stro, str2); +} + /* ***** Sail integers ***** */ #ifndef USE_INT128 @@ -392,6 +419,33 @@ void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2) normalize_sail_bits(rop); } +void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mpz_and(*rop->bits, *op1.bits, *op2.bits); +} + +void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mpz_ior(*rop->bits, *op1.bits, *op2.bits); +} + +void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mpz_xor(*rop->bits, *op1.bits, *op2.bits); +} + +void not_bits(sail_bits *rop, const sail_bits op) +{ + rop->len = op.len; + mpz_set(*rop->bits, *op.bits); + for (mp_bitcnt_t i = 0; i < op.len; i++) { + mpz_combit(*rop->bits, i); + } +} + void zeros(sail_bits *rop, const sail_int op) { rop->len = mpz_get_ui(op); @@ -467,8 +521,274 @@ void sail_signed(sail_int *rop, const sail_bits op) } } +void append(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len + op2.len; + mpz_mul_2exp(*rop->bits, *op1.bits, op2.len); + mpz_ior(*rop->bits, *rop->bits, *op2.bits); +} + +void replicate_bits(sail_bits *rop, const sail_bits op1, const mpz_t op2) +{ + uint64_t op2_ui = mpz_get_ui(op2); + rop->len = op1.len * op2_ui; + mpz_set(*rop->bits, *op1.bits); + for (int i = 1; i < op2_ui; i++) { + mpz_mul_2exp(*rop->bits, *rop->bits, op1.len); + mpz_ior(*rop->bits, *rop->bits, *op1.bits); + } +} + +uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64_t times) +{ + uint64_t r = v; + for (int i = 1; i < times; ++i) { + r |= (r << shift); + } + return r; +} + +// Takes a slice of the (two's complement) binary representation of +// integer n, starting at bit start, and of length len. With the +// argument in the following order: +// +// get_slice_int(len, n, start) +// +// For example: +// +// get_slice_int(8, 1680, 4) = +// +// 11 0 +// V V +// get_slice_int(8, 0b0110_1001_0000, 4) = 0b0110_1001 +// <-------^ +// (8 bit) 4 +// +void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz) +{ + uint64_t start = mpz_get_ui(start_mpz); + uint64_t len = mpz_get_ui(len_mpz); + + mpz_set_ui(*rop->bits, 0ul); + rop->len = len; + + for (uint64_t i = 0; i < len; i++) { + if (mpz_tstbit(n, i + start)) mpz_setbit(*rop->bits, i); + } +} + +// Set slice uses the same indexing scheme as get_slice_int, but it +// puts a bitvector slice into an integer rather than returning it. +void set_slice_int(sail_int *rop, + const sail_int len_mpz, + const sail_int n, + const sail_int start_mpz, + const sail_bits slice) +{ + uint64_t start = mpz_get_ui(start_mpz); + + mpz_set(*rop, n); + + for (uint64_t i = 0; i < slice.len; i++) { + if (mpz_tstbit(*slice.bits, i)) { + mpz_setbit(*rop, i + start); + } else { + mpz_clrbit(*rop, i + start); + } + } +} + +void vector_update_subrange_sail_bits(sail_bits *rop, + const sail_bits op, + const sail_int n_mpz, + const sail_int m_mpz, + const sail_bits slice) +{ + uint64_t n = mpz_get_ui(n_mpz); + uint64_t m = mpz_get_ui(m_mpz); + + mpz_set(*rop->bits, *op.bits); + + for (uint64_t i = 0; i < n - (m - 1ul); i++) { + if (mpz_tstbit(*slice.bits, i)) { + mpz_setbit(*rop->bits, i + m); + } else { + mpz_clrbit(*rop->bits, i + m); + } + } +} + +void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz) +{ + uint64_t start = mpz_get_ui(start_mpz); + uint64_t len = mpz_get_ui(len_mpz); + + mpz_set_ui(*rop->bits, 0ul); + rop->len = len; + + for (uint64_t i = 0; i < len; i++) { + if (mpz_tstbit(*op.bits, i + start)) mpz_setbit(*rop->bits, i); + } +} + +void set_slice(sail_bits *rop, + const sail_int len_mpz, + const sail_int slen_mpz, + const sail_bits op, + const sail_int start_mpz, + const sail_bits slice) +{ + uint64_t start = mpz_get_ui(start_mpz); + + mpz_set(*rop->bits, *op.bits); + rop->len = op.len; + + for (uint64_t i = 0; i < slice.len; i++) { + if (mpz_tstbit(*slice.bits, i)) { + mpz_setbit(*rop->bits, i + start); + } else { + mpz_clrbit(*rop->bits, i + start); + } + } +} + +/* ***** Sail Reals ***** */ + +void CREATE(real)(real *rop) +{ + mpf_init(*rop); +} + +void RECREATE(real)(real *rop) +{ + mpf_set_ui(*rop, 0); +} + +void KILL(real)(real *rop) +{ + mpf_clear(*rop); +} + +void COPY(real)(real *rop, const real op) +{ + mpf_set(*rop, op); +} + +void UNDEFINED(real)(real *rop, unit u) +{ + mpf_set_ui(*rop, 0ul); +} + +void neg_real(real *rop, const real op) +{ + mpf_neg(*rop, op); +} + +void mult_real(real *rop, const real op1, const real op2) { + mpf_mul(*rop, op1, op2); +} + +void sub_real(real *rop, const real op1, const real op2) +{ + mpf_sub(*rop, op1, op2); +} + +void add_real(real *rop, const real op1, const real op2) +{ + mpf_add(*rop, op1, op2); +} + +void div_real(real *rop, const real op1, const real op2) +{ + mpf_div(*rop, op1, op2); +} + +void sqrt_real(real *rop, const real op) +{ + mpf_sqrt(*rop, op); +} + +void abs_real(real *rop, const real op) +{ + mpf_abs(*rop, op); +} + +void round_up(sail_int *rop, const real op) +{ + mpf_t x; + mpf_init(x); + mpf_ceil(x, op); + mpz_set_ui(*rop, mpf_get_ui(x)); + mpf_clear(x); +} + +void round_down(sail_int *rop, const real op) +{ + mpf_t x; + mpf_init(x); + mpf_floor(x, op); + mpz_set_ui(*rop, mpf_get_ui(x)); + mpf_clear(x); +} + +void to_real(real *rop, const sail_int op) +{ + mpf_set_z(*rop, op); +} + +bool eq_real(const real op1, const real op2) +{ + return mpf_cmp(op1, op2) == 0; +} + +bool lt_real(const real op1, const real op2) +{ + return mpf_cmp(op1, op2) < 0; +} + +bool gt_real(const real op1, const real op2) +{ + return mpf_cmp(op1, op2) > 0; +} + +bool lteq_real(const real op1, const real op2) +{ + return mpf_cmp(op1, op2) <= 0; +} + +bool gteq_real(const real op1, const real op2) +{ + return mpf_cmp(op1, op2) >= 0; +} + +void real_power(real *rop, const real base, const sail_int exp) +{ + uint64_t exp_ui = mpz_get_ui(exp); + mpf_pow_ui(*rop, base, exp_ui); +} + +void CREATE_OF(real, sail_string)(real *rop, const sail_string op) +{ + mpf_init(*rop); + gmp_sscanf(op, "%Ff", *rop); +} + /* ***** Printing functions ***** */ +void string_of_int(sail_string *str, const sail_int i) +{ + gmp_asprintf(str, "%Zd", i); +} + +void string_of_bits(sail_string *str, const sail_bits op) +{ + if ((op.len % 4) == 0) { + gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits); + } else { + gmp_asprintf(str, "0b%*0Zb", op.len, *op.bits); + } +} + void fprint_bits(const sail_string pre, const sail_bits op, const sail_string post, @@ -556,3 +876,10 @@ unit prerr_int(const sail_string str, const sail_int op) fputs("\n", stderr); return UNIT; } + +unit sail_putchar(const sail_int op) +{ + char c = (char) mpz_get_ui(op); + putchar(c); + return UNIT; +} diff --git a/lib/sail.h b/lib/sail.h index 1cd5d928..23ff7f52 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -43,7 +43,7 @@ typedef int unit; unit UNDEFINED(unit)(const unit); bool eq_unit(const unit, const unit); - + /* ***** Sail booleans ***** */ /* @@ -66,8 +66,12 @@ SAIL_BUILTIN_TYPE(sail_string); void dec_str(sail_string *str, const mpz_t n); void hex_str(sail_string *str, const mpz_t n); +void undefined_string(sail_string *str, const unit u); + bool eq_string(const sail_string, const sail_string); +void concat_str(sail_string *stro, const sail_string str1, const sail_string str2); + /* ***** Sail integers ***** */ typedef int64_t mach_int; @@ -94,7 +98,7 @@ void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string); mach_int CONVERT_OF(mach_int, sail_int)(const sail_int); void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int); - + #else typedef __int128 sail_int; @@ -134,6 +138,7 @@ SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int); */ 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(mult_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); @@ -175,7 +180,7 @@ mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits); void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit); mach_bits UNDEFINED(mach_bits)(const unit); -/* +/* * Wrapper around >> operator to avoid UB when shift amount is greater * than or equal to 64. */ @@ -192,6 +197,11 @@ void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2); void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2); +void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void not_bits(sail_bits *rop, const sail_bits op); + void zeros(sail_bits *rop, const sail_int op); void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len); @@ -211,11 +221,74 @@ mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz); void sail_unsigned(sail_int *rop, const sail_bits op); void sail_signed(sail_int *rop, const sail_bits op); +void append(sail_bits *rop, const sail_bits op1, const sail_bits op2); + +void replicate_bits(sail_bits *rop, const sail_bits op1, const sail_int op2); +mach_bits fast_replicate_bits(const mach_bits shift, const mach_bits v, const mach_int times); + +void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz); + +void set_slice_int(sail_int *rop, + const sail_int len_mpz, + const sail_int n, + const sail_int start_mpz, + const sail_bits slice); + +void vector_update_subrange_sail_bits(sail_bits *rop, + const sail_bits op, + const sail_int n_mpz, + const sail_int m_mpz, + const sail_bits slice); + +void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz); + +void set_slice(sail_bits *rop, + const sail_int len_mpz, + const sail_int slen_mpz, + const sail_bits op, + const sail_int start_mpz, + const sail_bits slice); + /* ***** Sail reals ***** */ +typedef mpf_t real; + +SAIL_BUILTIN_TYPE(real); + +void CREATE_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); + +void round_up(sail_int *rop, const real op); +void round_down(sail_int *rop, const real op); + +void to_real(real *rop, const sail_int op); + +bool eq_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); + /* ***** Printing ***** */ -/* +void string_of_int(sail_string *str, const sail_int i); +void string_of_bits(sail_string *str, const sail_bits op); + +/* * Utility function not callable from Sail! */ void fprint_bits(const sail_string pre, @@ -234,3 +307,5 @@ 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); diff --git a/lib/smt.sail b/lib/smt.sail index ae672947..c9312819 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -7,7 +7,7 @@ val div = { smt: "div", ocaml: "quotient", lem: "integerDiv", - c: "div_int" + c: "tdiv_int" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)} overload operator / = {div} @@ -16,7 +16,7 @@ val mod = { smt: "mod", ocaml: "modulus", lem: "integerMod", - c: "mod_int" + c: "tmod_int" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)} overload operator % = {mod} diff --git a/src/c_backend.ml b/src/c_backend.ml index 7923a49c..1a2981e2 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -212,8 +212,8 @@ let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = | AE_val aval -> AE_val (aval_rename from_id to_id aval) | AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ) | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ) - | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp) - | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp) + | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp_rename from_id to_id aexp) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp_rename from_id to_id aexp) | AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2) | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2) | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ) @@ -1383,6 +1383,19 @@ let compile_funcall l ctx id args typ = setup := iinit ctyp gs cval :: !setup; cleanup := iclear ctyp gs :: !cleanup; (F_id gs, ctyp) + else if not (is_stack_ctyp have_ctyp) && is_stack_ctyp ctyp then + (* This is inefficient. FIXME: Remove id restriction on iconvert + instruction. Fortunatly only happens when flow typing makes a + length-polymorphic bitvector monomorphic. *) + let gs1 = gensym () in + let gs2 = gensym () in + setup := idecl have_ctyp gs1 :: !setup; + setup := ialloc have_ctyp gs1 :: !setup; + setup := icopy (CL_id gs1) cval :: !setup; + setup := idecl ctyp gs2 :: !setup; + setup := iconvert (CL_id gs2) ctyp gs1 have_ctyp :: !setup; + cleanup := iclear have_ctyp gs1 :: !cleanup; + (F_id gs2, ctyp) else c_error ~loc:l (Printf.sprintf "Failure when setting up function %s arguments: %s and %s." (string_of_id id) (string_of_ctyp have_ctyp) (string_of_ctyp ctyp)) @@ -3235,7 +3248,7 @@ let sgen_finish = function let instrument_tracing ctx = let module StringSet = Set.Make(String) in - let traceable = StringSet.of_list ["uint64_t"; "sail_string"; "bv_t"; "mpz_t"; "unit"; "bool"] in + let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in let rec instrument = function | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs -> let trace_start = @@ -3262,12 +3275,10 @@ let instrument_tracing ctx = else iraw "trace_unknown();" in - [trace_start; - iraw "g_trace_depth++;"] + [trace_start] @ trace_args args @ [iraw "trace_argend();"; instr; - iraw "g_trace_depth--;"; trace_end; trace_ret; iraw "trace_retend();"] @@ -3314,7 +3325,10 @@ let compile_ast ctx (Defs defs) = 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 cdefs = List.concat (List.rev chunks) in + let cdefs = optimize ctx cdefs in + let cdefs = if !opt_trace then List.map (instrument_tracing ctx) cdefs else cdefs in + let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline diff --git a/src/sail.ml b/src/sail.ml index 86c00254..af433799 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -119,9 +119,9 @@ let options = Arg.align ([ ( "-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " Apply constant folding optimizations"); - ( "-c_trace", - Arg.Set C_backend.opt_trace, - " Instrument C ouput with tracing"); + ( "-trace", + Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml], + " Instrument ouput with tracing"); ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); diff --git a/test/c/assign_rename_bug.expect b/test/c/assign_rename_bug.expect new file mode 100644 index 00000000..ef2503c0 --- /dev/null +++ b/test/c/assign_rename_bug.expect @@ -0,0 +1,28 @@ +0xFFF0000000001 +0xFFF0000000001 +0xFFEFFFFFFFFFF +0xFFEFFFFFFFFFF +0xFFF0000000002 +0xFFF0000000002 +0xFFEFFFFFFFFFE +0xFFEFFFFFFFFFE +0xFFF0000000003 +0xFFF0000000003 +0xFFEFFFFFFFFFD +0xFFEFFFFFFFFFD +0xFFF0000000004 +0xFFF0000000004 +0xFFEFFFFFFFFFC +0xFFEFFFFFFFFFC +0xFFF0000000005 +0xFFF0000000005 +0xFFEFFFFFFFFFB +0xFFEFFFFFFFFFB +0xFFF0000000006 +0xFFF0000000006 +0xFFEFFFFFFFFFA +0xFFEFFFFFFFFFA +0xFFF0000000007 +0xFFF0000000007 +0xFFEFFFFFFFFF9 +0xFFEFFFFFFFFF9 diff --git a/test/c/assign_rename_bug.sail b/test/c/assign_rename_bug.sail new file mode 100644 index 00000000..8b74df2a --- /dev/null +++ b/test/c/assign_rename_bug.sail @@ -0,0 +1,35 @@ +default Order dec + +$include +$include +$include + +$include + +val sub_vec_int = { + ocaml: "sub_vec_int", + lem: "sub_vec_int", + c: "sub_bits_int" +} : forall 'n. (bits('n), int) -> bits('n) + +overload operator - = {sub_vec_int} + +val print_bits52: (string, bits(52)) -> unit + +function print_bits52(str, x) = print_bits(str, x) + +val main : unit -> unit effect {undef} + +function main() = { + let addr : bits(52) = 0xF_FF00_0000_0000; + i : int = undefined; + size : int = 7; + ret : unit = (); + foreach (i from 1 to size by 1 in inc) { + ret = print_bits("", addr + i); + ret = print_bits52("", addr + i); + ret = print_bits("", addr - i); + ret = print_bits52("", addr - i); + }; + return ret +} -- cgit v1.2.3 From 0dd140219040664000573cbcf8c8a4d26629feeb Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 19 Jun 2018 16:11:57 +0100 Subject: Improvements to Sail C for booting Linux --- lib/rts.c | 5 +++-- lib/sail.c | 7 +++++++ lib/sail.h | 1 + src/c_backend.ml | 43 ++++++++++++++++++++++++++++++++++++------- 4 files changed, 47 insertions(+), 9 deletions(-) diff --git a/lib/rts.c b/lib/rts.c index 61f772cf..fa8830e4 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -25,7 +25,7 @@ unit sail_exit(unit u) unit sleep_request(const unit u) { fprintf(stderr, "Sail model going to sleep\n"); - exit(EXIT_SUCCESS); + return UNIT; } /* ***** Sail memory builtins ***** */ @@ -176,7 +176,8 @@ unit load_raw(mach_bits addr, const sail_string file) return UNIT; } -void load_image(char *file) { +void load_image(char *file) +{ FILE *fp = fopen(file, "r"); if (!fp) { diff --git a/lib/sail.c b/lib/sail.c index 13f1a0e8..35860419 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -360,6 +360,13 @@ mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits op) return mpz_get_ui(*op.bits); } +void CONVERT_OF(sail_bits, mach_bits)(sail_bits *rop, const mach_bits op, const uint64_t len) +{ + rop->len = len; + // use safe_rshift to correctly handle the case when we have a 0-length vector. + mpz_set_ui(*rop->bits, op & safe_rshift(UINT64_MAX, 64 - len)); +} + void UNDEFINED(sail_bits)(sail_bits *rop, const sail_int len, const mach_bits bit) { zeros(rop, len); diff --git a/lib/sail.h b/lib/sail.h index 23ff7f52..27b088fe 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -176,6 +176,7 @@ void RECREATE_OF(sail_bits, mach_bits)(sail_bits *, const bool direction); mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits); +void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t); void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit); mach_bits UNDEFINED(mach_bits)(const unit); diff --git a/src/c_backend.ml b/src/c_backend.ml index 1a2981e2..ae411654 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -465,12 +465,12 @@ let gensym () = incr gensym_counter; id -let rec split_block = function +let rec split_block l = function | [exp] -> [], exp | exp :: exps -> - let exps, last = split_block exps in + let exps, last = split_block l exps in exp :: exps, last - | [] -> c_error "empty block" + | [] -> c_error ~loc:l "empty block" let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in @@ -525,7 +525,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) | E_block exps -> - let exps, last = split_block exps in + let exps, last = split_block l exps in let aexps = List.map anf exps in let alast = anf last in mk_aexp (AE_block (aexps, alast, typ_of exp)) @@ -1740,6 +1740,18 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup + else if is_stack_ctyp assign_ctyp && not (is_stack_ctyp ctyp) then + let gs = gensym () in + setup @ [ icomment comment; + idecl ctyp gs; + ialloc ctyp gs; + call (CL_id gs); + iconvert (CL_id id) assign_ctyp gs ctyp; + iclear ctyp gs + ], + CT_unit, + (fun clexp -> icopy clexp unit_fragment), + cleanup else failwith comment @@ -2159,7 +2171,7 @@ 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)); let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in - prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)); + if string_of_id id = "fetch_and_execute" then prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)) else (); let setup, ctyp, call, cleanup = compile_aexp ctx aexp in c_debug (lazy "Compiled aexp"); let fundef_label = label "fundef_fail_" in @@ -2633,8 +2645,8 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = end | "vector_update_subrange", _ -> Printf.sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp) | "vector_subrange", _ -> Printf.sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp) - | "vector_update", CT_bits64 _ -> "update_uint64_t" - | "vector_update", CT_bits _ -> "update_bv" + | "vector_update", CT_bits64 _ -> "update_mach_bits" + | "vector_update", CT_bits _ -> "update_sail_bits" | "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) @@ -2697,6 +2709,23 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = i) in separate hardline (List.mapi convert (List.map2 (fun x y -> (x, y)) ctyps1 ctyps2)) + (* If we're converting from a bits type with a known compile time + length, pass it as an extra parameter to the conversion. *) + | I_convert (x, ctyp1, y, (CT_bits64 (n, _) as ctyp2)) -> + if is_stack_ctyp ctyp1 then + string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s, %d);" + (sgen_clexp_pure x) + (sgen_ctyp_name ctyp1) + (sgen_ctyp_name ctyp2) + (sgen_id y) + n) + else + string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s, %d);" + (sgen_ctyp_name ctyp1) + (sgen_ctyp_name ctyp2) + (sgen_clexp x) + (sgen_id y) + n) | I_convert (x, ctyp1, y, ctyp2) -> if is_stack_ctyp ctyp1 then string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);" -- cgit v1.2.3 From 4a09a35164be81467feea154ef7651ef96eaad88 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 19 Jun 2018 18:40:50 +0100 Subject: Add elf parsing from Alastair --- lib/elf.c | 390 ++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/elf.h | 5 + lib/rts.c | 7 +- lib/rts.h | 4 + lib/sail.c | 2 +- lib/sail.h | 2 +- lib/vector_dec.sail | 2 +- src/c_backend.ml | 5 +- 8 files changed, 410 insertions(+), 7 deletions(-) create mode 100644 lib/elf.c create mode 100644 lib/elf.h diff --git a/lib/elf.c b/lib/elf.c new file mode 100644 index 00000000..e0e75c91 --- /dev/null +++ b/lib/elf.c @@ -0,0 +1,390 @@ +//////////////////////////////////////////////////////////////// +// ELF Loader +//////////////////////////////////////////////////////////////// + +// Header files for simulator +#include "elf.h" +#include "rts.h" +#include "sail.h" + +// Use the zlib library to uncompress ELF.gz files +#include + +// Define ELF constants/types. These come from the +// Tool Interface Standard Executable and Linking Format Specification 1.2 + +typedef uint32_t Elf32_Addr; +typedef uint16_t Elf32_Half; +typedef uint32_t Elf32_Off; +typedef uint32_t Elf32_Word; + +typedef uint64_t Elf64_Addr; +typedef uint16_t Elf64_Half; +typedef uint64_t Elf64_Off; +typedef uint32_t Elf64_Word; +typedef uint64_t Elf64_Xword; + +/* Type for section indices, which are 16-bit quantities. */ +typedef uint16_t Elf32_Section; +typedef uint16_t Elf64_Section; + +/* Type for version symbol information. */ +typedef Elf32_Half Elf32_Versym; +typedef Elf64_Half Elf64_Versym; + +// Big-Endian support functions which reverse values + +uint16_t rev16(uint16_t x) { + uint16_t a = (x >> 0) & 0xff; + uint16_t b = (x >> 8) & 0xff; + return (a << 8) | (b << 0); +} + +uint32_t rev32(uint32_t x) { + uint32_t a = (x >> 0) & 0xff; + uint32_t b = (x >> 8) & 0xff; + uint32_t c = (x >> 16) & 0xff; + uint32_t d = (x >> 24) & 0xff; + return (a << 24) | (b << 16) | (c << 8) | (d << 0); +} + +uint64_t rev64(uint64_t x) { + uint64_t a = (x >> 0) & 0xff; + uint64_t b = (x >> 8) & 0xff; + uint64_t c = (x >> 16) & 0xff; + uint64_t d = (x >> 24) & 0xff; + uint64_t e = (x >> 32) & 0xff; + uint64_t f = (x >> 40) & 0xff; + uint64_t g = (x >> 48) & 0xff; + uint64_t h = (x >> 56) & 0xff; + return (a << 56) | (b << 48) | (c << 40) | (d << 32) | (e << 24) | (f << 16) | (g << 8) | (h << 0); +} + +// Endian support macros which reverse values on big-endian machines +// (We assume that the host machine is little-endian) + +#define rdAddr32(le, x) ((le) ? (x) : rev32(x)) +#define rdHalf32(le, x) ((le) ? (x) : rev16(x)) +#define rdOff32(le, x) ((le) ? (x) : rev32(x)) +#define rdWord32(le, x) ((le) ? (x) : rev32(x)) + +#define rdAddr64(le, x) ((le) ? (x) : rev64(x)) +#define rdHalf64(le, x) ((le) ? (x) : rev16(x)) +#define rdOff64(le, x) ((le) ? (x) : rev64(x)) +#define rdWord64(le, x) ((le) ? (x) : rev32(x)) +#define rdXword64(le, x) ((le) ? (x) : rev64(x)) + + +#define EI_NIDENT 16 /* Size of e_ident */ + +#define EI_MAG0 0 /* Offsets in e_ident */ +#define EI_MAG1 1 +#define EI_MAG2 2 +#define EI_MAG3 3 +#define EI_CLASS 4 +#define EI_DATA 5 + +#define ELFMAG0 0x7f /* Magic string */ +#define ELFMAG1 'E' +#define ELFMAG2 'L' +#define ELFMAG3 'F' + +#define ELFCLASS32 1 /* 32-bit ELF */ +#define ELFCLASS64 2 /* 64-bit ELF */ + +#define ELFDATA2LSB 1 /* Little-endian ELF */ + +#define ET_EXEC 2 /* Executable file */ + +#define EM_ARM 0x0028 /* 32-bit ARM */ +#define EM_AARCH64 0x00B7 /* 64-bit ARM */ + +#define PT_LOAD 1 /* Loadable segment */ + +#define SHT_SYMTAB 2 /* Symbol table type */ + +/* How to extract and insert information held in the st_info field. */ + +#define ELF32_ST_BIND(val) (((unsigned char) (val)) >> 4) +#define ELF32_ST_TYPE(val) ((val) & 0xf) +#define ELF32_ST_INFO(bind, type) (((bind) << 4) + ((type) & 0xf)) + +/* Both Elf32_Sym and Elf64_Sym use the same one-byte st_info field. */ +#define ELF64_ST_BIND(val) ELF32_ST_BIND (val) +#define ELF64_ST_TYPE(val) ELF32_ST_TYPE (val) +#define ELF64_ST_INFO(bind, type) ELF32_ST_INFO ((bind), (type)) + + +/* Legal values for ST_TYPE subfield of st_info (symbol type). */ + +#define STT_NOTYPE 0 /* Symbol type is unspecified */ +#define STT_OBJECT 1 /* Symbol is a data object */ +#define STT_FUNC 2 /* Symbol is a code object */ +#define STT_SECTION 3 /* Symbol associated with a section */ +#define STT_FILE 4 /* Symbol's name is file name */ +#define STT_COMMON 5 /* Symbol is a common data object */ +#define STT_TLS 6 /* Symbol is thread-local data object*/ +#define STT_NUM 7 /* Number of defined types. */ +#define STT_LOOS 10 /* Start of OS-specific */ +#define STT_GNU_IFUNC 10 /* Symbol is indirect code object */ +#define STT_HIOS 12 /* End of OS-specific */ +#define STT_LOPROC 13 /* Start of processor-specific */ +#define STT_HIPROC 15 /* End of processor-specific */ + + +typedef struct +{ + uint8_t e_ident[EI_NIDENT]; /* ELF file identifier */ + Elf32_Half e_type; /* Object file type */ + Elf32_Half e_machine; /* Processor architecture */ + Elf32_Word e_version; /* Object file version */ + Elf32_Addr e_entry; /* Entry point (loader jumps to this virtual address if != 0) */ + Elf32_Off e_phoff; /* Program header table offset */ + Elf32_Off e_shoff; /* Section header table offset */ + Elf32_Word e_flags; /* Processor-specific flags */ + Elf32_Half e_ehsize; /* ELF header size */ + Elf32_Half e_phentsize; /* Size of a single program header */ + Elf32_Half e_phnum; /* Number of program headers in table */ + Elf32_Half e_shensize; /* Size of a single section header */ + Elf32_Half e_shnum; /* Number of section headers in table */ + Elf32_Half e_shtrndx; /* Index of string table in section header table */ +} Elf32_Ehdr; + +typedef struct +{ + Elf32_Word p_type; /* Segment type */ + Elf32_Off p_offset; /* Segment offset in file */ + Elf32_Addr p_vaddr; /* Segment load virtual address */ + Elf32_Addr p_paddr; /* Segment load physical address */ + Elf32_Word p_filesz; /* Segment size in file */ + Elf32_Word p_memsz; /* Segment size in memory. Must be >= p_filesz. If > p_filesz, zero pad */ + Elf32_Word p_flags; /* Segment flags */ + Elf32_Word p_align; /* Segment alignment */ +} Elf32_Phdr; + +typedef struct +{ + uint8_t e_ident[EI_NIDENT]; /* ELF file identifier */ + Elf64_Half e_type; /* Object file type */ + Elf64_Half e_machine; /* Processor architecture */ + Elf64_Word e_version; /* Object file version */ + Elf64_Addr e_entry; /* Entry point (loader jumps to this virtual address if != 0) */ + Elf64_Off e_phoff; /* Program header table offset */ + Elf64_Off e_shoff; /* Section header table offset */ + Elf64_Word e_flags; /* Processor-specific flags */ + Elf64_Half e_ehsize; /* ELF header size */ + Elf64_Half e_phentsize; /* Size of a single program header */ + Elf64_Half e_phnum; /* Number of program headers in table */ + Elf64_Half e_shensize; /* Size of a single section header */ + Elf64_Half e_shnum; /* Number of section headers in table */ + Elf64_Half e_shtrndx; /* Index of string table in section header table */ +} Elf64_Ehdr; + +typedef struct +{ + Elf64_Word p_type; /* Segment type */ + Elf64_Word p_flags; /* Segment flags */ + Elf64_Off p_offset; /* Segment offset in file */ + Elf64_Addr p_vaddr; /* Segment load virtual address */ + Elf64_Addr p_paddr; /* Segment load physical address */ + Elf64_Xword p_filesz; /* Segment size in file */ + Elf64_Xword p_memsz; /* Segment size in memory. Must be >= p_filesz. + If > p_filesz, zero pad memory */ + Elf64_Xword p_align; /* Segment alignment */ +} Elf64_Phdr; + +typedef struct +{ + Elf32_Word sh_name; /* Section name (string tbl index) */ + Elf32_Word sh_type; /* Section type */ + Elf32_Word sh_flags; /* Section flags */ + Elf32_Addr sh_addr; /* Section virtual addr at execution */ + Elf32_Off sh_offset; /* Section file offset */ + Elf32_Word sh_size; /* Section size in bytes */ + Elf32_Word sh_link; /* Link to another section */ + Elf32_Word sh_info; /* Additional section information */ + Elf32_Word sh_addralign; /* Section alignment */ + Elf32_Word sh_entsize; /* Entry size if section holds table */ +} Elf32_Shdr; + +typedef struct +{ + Elf64_Word sh_name; /* Section name (string tbl index) */ + Elf64_Word sh_type; /* Section type */ + Elf64_Xword sh_flags; /* Section flags */ + Elf64_Addr sh_addr; /* Section virtual addr at execution */ + Elf64_Off sh_offset; /* Section file offset */ + Elf64_Xword sh_size; /* Section size in bytes */ + Elf64_Word sh_link; /* Link to another section */ + Elf64_Word sh_info; /* Additional section information */ + Elf64_Xword sh_addralign; /* Section alignment */ + Elf64_Xword sh_entsize; /* Entry size if section holds table */ +} Elf64_Shdr; + +/* Symbol table entry. */ + +typedef struct +{ + Elf32_Word st_name; /* Symbol name (string tbl index) */ + Elf32_Addr st_value; /* Symbol value */ + Elf32_Word st_size; /* Symbol size */ + uint8_t st_info; /* Symbol type and binding */ + uint8_t st_other; /* Symbol visibility */ + Elf32_Section st_shndx; /* Section index */ +} Elf32_Sym; + +typedef struct +{ + Elf64_Word st_name; /* Symbol name (string tbl index) */ + uint8_t st_info; /* Symbol type and binding */ + uint8_t st_other; /* Symbol visibility */ + Elf64_Section st_shndx; /* Section index */ + Elf64_Addr st_value; /* Symbol value */ + Elf64_Xword st_size; /* Symbol size */ +} Elf64_Sym; + +void loadBlock32(const char* buffer, Elf32_Off off, Elf32_Addr addr, Elf32_Word filesz, Elf32_Word memsz) { + //// std::cout << "Loading block from " << off << " to " << addr << "+:" << filesz << std::endl; + for(Elf32_Off i = 0; i < filesz; ++i) { + //// std::cout << "Writing " << (int)buffer[off+i] << " to " << addr+i << std::endl; + write_mem(addr+i, 0xff & buffer[off+i]); + } + // Zero fill if p_memsz > p_filesz + for(Elf32_Off i = filesz; i < memsz; ++i) { + write_mem(addr+i, 0); + } +} + +void loadProgHdr32(bool le, const char* buffer, Elf32_Off off, const int total_file_size) { + //// std::cout << "Loading program header at " << off << std::endl; + if (off > total_file_size - sizeof(Elf32_Phdr)) { + // // std::cout << "Invalid ELF file, section header overruns end of file" << std::endl; + exit(EXIT_FAILURE); + } + Elf32_Phdr *phdr = (Elf32_Phdr*) &buffer[off]; + // Only PT_LOAD segments should be loaded; + if (rdWord32(le, phdr->p_type) == PT_LOAD) { + Elf32_Off off = rdOff32(le, phdr->p_offset); + Elf32_Word filesz = rdWord32(le, phdr->p_filesz); + if (filesz > total_file_size - off) { + // // std::cout << "Invalid ELF file, section overruns end of file" << std::endl; + exit(EXIT_FAILURE); + } + loadBlock32(buffer, off, rdAddr32(le, phdr->p_paddr), filesz, rdWord32(le, phdr->p_memsz)); + } +} + +void loadBlock64(const char* buffer, Elf64_Off off, Elf64_Addr addr, Elf64_Word filesz, Elf64_Word memsz) { + //// std::cout << "Loading block from " << off << " to " << addr << "+:" << filesz << std::endl; + for(Elf64_Off i = 0; i < filesz; ++i) { + //// std::cout << "Writing " << (int)buffer[off+i] << " to " << addr+i << std::endl; + write_mem(addr+i, 0xff & buffer[off+i]); + } + // Zero fill if p_memsz > p_filesz + for(Elf64_Off i = filesz; i < memsz; ++i) { + write_mem(addr+i, 0); + } +} + +void loadProgHdr64(bool le, const char* buffer, Elf64_Off off, const int total_file_size) { + //// std::cout << "Loading program header at " << off << std::endl; + if (off > total_file_size - sizeof(Elf64_Phdr)) { + //// std::cout << "Invalid ELF file, section header overruns end of file" << std::endl; + exit(EXIT_FAILURE); + } + Elf64_Phdr *phdr = (Elf64_Phdr*) &buffer[off]; + // Only PT_LOAD segments should be loaded; + if (rdWord64(le, phdr->p_type) == PT_LOAD) { + Elf64_Off off = rdOff64(le, phdr->p_offset); + Elf64_Word filesz = rdXword64(le, phdr->p_filesz); + if (filesz > total_file_size - off) { + // // std::cout << "Invalid ELF file, section overruns end of file" << std::endl; + exit(EXIT_FAILURE); + } + loadBlock64(buffer, off, rdAddr64(le, phdr->p_paddr), filesz, rdXword64(le, phdr->p_memsz)); + } +} + +void loadELFHdr(const char* buffer, const int total_file_size) { + if (total_file_size < sizeof(Elf32_Ehdr)) { + // std::cout << "File too small, not big enough even for 32-bit ELF header" << std::endl; + exit(EXIT_FAILURE); + } + Elf32_Ehdr *hdr = (Elf32_Ehdr*) &buffer[0]; // both Elf32 and Elf64 have same magic + if (hdr->e_ident[EI_MAG0] != ELFMAG0 || + hdr->e_ident[EI_MAG1] != ELFMAG1 || + hdr->e_ident[EI_MAG2] != ELFMAG2 || + hdr->e_ident[EI_MAG3] != ELFMAG3) { + // std::cout << "Invalid ELF magic bytes. Not an ELF file?" << std::endl; + exit(EXIT_FAILURE); + } + + if (hdr->e_ident[EI_CLASS] == ELFCLASS32) { + bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB; + Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0]; + if (rdHalf32(le, ehdr->e_type) != ET_EXEC || + rdHalf32(le, ehdr->e_machine) != EM_ARM) { + // std::cout << "Invalid ELF type or machine for class (32-bit)" << std::endl; + exit(EXIT_FAILURE); + } + + for(int i = 0; i < rdHalf32(le, ehdr->e_phnum); ++i) { + loadProgHdr32(le, buffer, rdOff32(le, ehdr->e_phoff) + i * rdHalf32(le, ehdr->e_phentsize), total_file_size); + } + + return; + } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) { + if (total_file_size < sizeof(Elf64_Ehdr)) { + // std::cout << "File too small, specifies 64-bit ELF but not big enough for 64-bit ELF header" << std::endl; + exit(EXIT_FAILURE); + } + bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB; + Elf64_Ehdr *ehdr = (Elf64_Ehdr*) &buffer[0]; + if (rdHalf64(le, ehdr->e_type) != ET_EXEC || + rdHalf64(le, ehdr->e_machine) != EM_AARCH64) { + // std::cout << "Invalid ELF type or machine for class (64-bit)" << std::endl; + exit(EXIT_FAILURE); + } + + for(int i = 0; i < rdHalf64(le, ehdr->e_phnum); ++i) { + loadProgHdr64(le, buffer, rdOff64(le, ehdr->e_phoff) + i * rdHalf64(le, ehdr->e_phentsize), total_file_size); + } + + return; + } else { + // std::cout << "Unrecognized ELF file format" << std::endl; + exit(EXIT_FAILURE); + } +} + +void loadELF(char *filename) { + // Read input file into memory + char* buffer = NULL; + int size = 0; + int chunk = (1<<24); // increments output buffer this much + int read = 0; + gzFile in = gzopen(filename, "rb"); + if (in == NULL) { goto fail; } + while (!gzeof(in)) { + size = read + chunk; + buffer = (char*)realloc(buffer, size); + if (buffer == NULL) { goto fail; } + + int s = gzread(in, buffer+read, size - read); + if (s < 0) { goto fail; } + read += s; + } + + loadELFHdr(buffer, read); + free(buffer); + return; + +fail: + // std::cout << "Unable to read file " << filename << std::endl; + exit(EXIT_FAILURE); +} + +//////////////////////////////////////////////////////////////// +// ELF Loader +//////////////////////////////////////////////////////////////// + diff --git a/lib/elf.h b/lib/elf.h new file mode 100644 index 00000000..16dff677 --- /dev/null +++ b/lib/elf.h @@ -0,0 +1,5 @@ +#pragma once + +#include + +void loadELF(char *filename); diff --git a/lib/rts.c b/lib/rts.c index fa8830e4..bab788af 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -2,6 +2,7 @@ #include"sail.h" #include"rts.h" +#include"elf.h" void sail_match_failure(sail_string msg) { @@ -303,11 +304,13 @@ void trace_end(void) /* ***** ELF functions ***** */ -void elf_entry(mpz_t *rop, const unit u) { +void elf_entry(mpz_t *rop, const unit u) +{ mpz_set_ui(*rop, g_elf_entry); } -void elf_tohost(mpz_t *rop, const unit u) { +void elf_tohost(mpz_t *rop, const unit u) +{ mpz_set_ui(*rop, 0x0ul); } diff --git a/lib/rts.h b/lib/rts.h index f86962c4..7f26df4e 100644 --- a/lib/rts.h +++ b/lib/rts.h @@ -29,6 +29,9 @@ unit sleep_request(const unit u); /* ***** Memory builtins ***** */ +void write_mem(uint64_t, uint64_t); +uint64_t read_mem(uint64_t); + // These memory builtins are intended to match the semantics for the // __ReadRAM and __WriteRAM functions in ASL. @@ -51,6 +54,7 @@ void load_image(char *); /* ***** Tracing ***** */ static int64_t g_trace_depth; +static int64_t g_trace_max_depth; static bool g_trace_enabled; /* diff --git a/lib/sail.c b/lib/sail.c index 35860419..d377b099 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -491,7 +491,7 @@ void vector_subrange_sail_bits(sail_bits *rop, normalize_sail_bits(rop); } -void truncate(sail_bits *rop, const sail_bits op, const sail_int len) +void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len) { rop->len = mpz_get_ui(len); mpz_set(*rop->bits, *op.bits); diff --git a/lib/sail.h b/lib/sail.h index 27b088fe..2a143605 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -215,7 +215,7 @@ void vector_subrange_sail_bits(sail_bits *rop, const sail_int n_mpz, const sail_int m_mpz); -void truncate(sail_bits *rop, const sail_bits op, const sail_int len); +void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len); mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz); diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index cff5d4d3..c95379fe 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -41,7 +41,7 @@ val truncate = { ocaml: "vector_truncate", lem: "vector_truncate", coq: "vector_truncate", - c: "truncate" + c: "sail_truncate" } : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit) val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit) diff --git a/src/c_backend.ml b/src/c_backend.ml index ae411654..1858ec76 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -3362,7 +3362,8 @@ let compile_ast ctx (Defs defs) = let preamble = separate hardline [ string "#include \"sail.h\""; - string "#include \"rts.h\""] + string "#include \"rts.h\""; + string "#include \"elf.h\"" ] in let exn_boilerplate = @@ -3400,7 +3401,7 @@ let compile_ast ctx (Defs defs) = let postamble = separate hardline (List.map string ( [ "int main(int argc, char *argv[])"; "{"; - " if (argc > 1) { load_image(argv[1]); }"; + " if (argc > 1) { loadELF(argv[1]); }"; " setup_rts();" ] @ fst exn_boilerplate @ startup cdefs -- cgit v1.2.3 From 5489108f054fb51aa190e1fda847d8ab59ee915b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 20 Jun 2018 17:12:04 +0100 Subject: Simplify the ANF->IR translation Previously the ANF->IR translation cared too much about how things were allocated in C, so it had to constantly check whether things needed to be allocated on the stack or heap, and generate different cequences of IR instructions depending on either. This change removes the ialloc IR instruction, and changes iinit and idecl so that the code generator now generates different C for the same IR instructions based on the variable types involved. The next change in this vein would be to merge icopy and iconvert at the IR level so that conversions between uint64_t and large-bitvectors are inserted by the code generator. This would be good because it would make the ANF->IR translation more robust to changes in the types of variables caused by flow-typing, and optimization passes could convert large bitvectors to uint64_t as local changes. --- language/bytecode.ott | 3 - lib/rts.c | 2 +- src/bytecode_util.ml | 11 +-- src/c_backend.ml | 225 ++++++++++++++++++++++---------------------------- test/c/run_tests.sh | 2 +- 5 files changed, 101 insertions(+), 142 deletions(-) diff --git a/language/bytecode.ott b/language/bytecode.ott index bcd7b5b0..895ac34b 100644 --- a/language/bytecode.ott +++ b/language/bytecode.ott @@ -122,7 +122,6 @@ iannot :: 'IA_' ::= instr :: 'I_' ::= {{ aux _ iannot }} | ctyp id :: :: decl - | alloc ctyp id :: :: alloc | ctyp id = cval :: :: init | if ( cval ) { instr0 ; ... ; instrn } else { instr0 ; ... ; instrm } : ctyp :: :: if @@ -150,8 +149,6 @@ cdef :: 'CDEF_' ::= | ctype_def :: :: type | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = { instr0 ; ... ; instrm - } { - instr0 ; ... ; instri } :: :: let % The first list of instructions creates up the global letbinding, the % second kills it. diff --git a/lib/rts.c b/lib/rts.c index bab788af..563d11e2 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -70,7 +70,7 @@ void write_mem(uint64_t address, uint64_t byte) } } - /* + /* * If we couldn't find a block matching the mask, allocate a new * one, write the byte, and put it at the front of the block list. */ diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index 05709de9..1a206764 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -67,9 +67,6 @@ let instr_number () = let idecl ?loc:(l=Parse_ast.Unknown) ctyp id = I_aux (I_decl (ctyp, id), (instr_number (), l)) -let ialloc ?loc:(l=Parse_ast.Unknown) ctyp id = - I_aux (I_alloc (ctyp, id), (instr_number (), l)) - let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval = I_aux (I_init (ctyp, id, cval), (instr_number (), l)) @@ -221,8 +218,6 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace | I_try_block instrs -> pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - | I_alloc (ctyp, id) -> - pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp | I_reset (ctyp, id) -> pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp | I_init (ctyp, id, cval) -> @@ -282,11 +277,10 @@ let pp_cdef = function pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ hardline | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline - | CDEF_let (n, bindings, instrs, cleanup) -> + | CDEF_let (n, bindings, instrs) -> let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr cleanup) rbrace ^^ space ^^ hardline | CDEF_startup (id, instrs)-> pp_keyword "startup" ^^ pp_id id ^^ space @@ -357,7 +351,7 @@ let rec clexp_deps = function instruction **) let instr_deps = function | I_decl (ctyp, id) -> NS.empty, NS.singleton (G_id id) - | I_alloc (ctyp, id) | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id) + | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id) | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id) | I_if (cval, _, _, _) -> cval_deps cval, NS.empty | I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label) @@ -438,7 +432,6 @@ let make_dot id graph = | G_id _ -> "yellow" | G_instr (_, I_aux (I_decl _, _)) -> "olivedrab1" | G_instr (_, I_aux (I_init _, _)) -> "springgreen" - | G_instr (_, I_aux (I_alloc _, _)) -> "palegreen" | G_instr (_, I_aux (I_clear _, _)) -> "peachpuff" | G_instr (_, I_aux (I_goto _, _)) -> "orange1" | G_instr (_, I_aux (I_label _, _)) -> "white" diff --git a/src/c_backend.ml b/src/c_backend.ml index 1858ec76..0a9bede0 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -736,7 +736,8 @@ type ctx = tc_env : Env.t; local_env : Env.t; letbinds : int list; - recursive_functions : IdSet.t + recursive_functions : IdSet.t; + no_raw : bool; } let initial_ctx env = @@ -746,7 +747,8 @@ let initial_ctx env = tc_env = env; local_env = env; letbinds = []; - recursive_functions = IdSet.empty + recursive_functions = IdSet.empty; + no_raw = false; } let rec ctyp_equal ctyp1 ctyp2 = @@ -1085,7 +1087,7 @@ let cval_ctyp = function (_, ctyp) -> ctyp let rec map_instrs f (I_aux (instr, aux)) = let instr = match instr with - | I_decl _ | I_alloc _ | I_init _ | I_reset _ | I_reinit _ -> instr + | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> instr | I_if (cval, instrs1, instrs2, ctyp) -> I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp) | I_funcall _ | I_convert _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr @@ -1099,7 +1101,7 @@ let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ct let rec instr_ctyps (I_aux (instr, aux)) = match instr with - | I_decl (ctyp, _) | I_alloc (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) -> [ctyp] + | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) -> [ctyp] | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> [ctyp; cval_ctyp cval] | I_if (cval, instrs1, instrs2, ctyp) -> ctyp :: cval_ctyp cval :: List.concat (List.map instr_ctyps instrs1 @ List.map instr_ctyps instrs2) @@ -1131,10 +1133,9 @@ let cdef_ctyps ctx = function | CDEF_startup (id, instrs) | CDEF_finish (id, instrs) -> List.concat (List.map instr_ctyps instrs) | CDEF_type tdef -> ctype_def_ctyps tdef - | CDEF_let (_, bindings, instrs, cleanup) -> + | CDEF_let (_, bindings, instrs) -> List.map snd bindings @ List.concat (List.map instr_ctyps instrs) - @ List.concat (List.map instr_ctyps cleanup) let is_ct_enum = function | CT_enum _ -> true @@ -1184,15 +1185,13 @@ let rec compile_aval ctx = function | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> let gs = gensym () in - [idecl CT_int gs; - iinit CT_int gs (F_lit (V_int n), CT_int64)], + [iinit CT_int gs (F_lit (V_int n), CT_int64)], (F_id gs, CT_int), [iclear CT_int gs] | AV_lit (L_aux (L_num n, _), typ) -> let gs = gensym () in - [idecl CT_int gs; - iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)], + [iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)], (F_id gs, CT_int), [iclear CT_int gs] @@ -1204,8 +1203,7 @@ let rec compile_aval ctx = function | AV_lit (L_aux (L_real str, _), _) -> let gs = gensym () in - [idecl CT_real gs; - iinit CT_real gs (F_lit (V_string str), CT_string)], + [iinit CT_real gs (F_lit (V_string str), CT_string)], (F_id gs, CT_real), [iclear CT_real gs] @@ -1219,19 +1217,16 @@ let rec compile_aval ctx = function let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in let gs = gensym () in - let tup_setup, tup_cleanup = - if is_stack_ctyp tup_ctyp then [], [] else [ialloc tup_ctyp gs], [iclear tup_ctyp gs] - in setup - @ [idecl tup_ctyp gs] @ tup_setup + @ [idecl tup_ctyp gs] @ List.mapi (fun n cval -> icopy (CL_field (gs, "tup" ^ string_of_int n)) cval) cvals, (F_id gs, CT_tup (List.map cval_ctyp cvals)), - tup_cleanup @ cleanup + [iclear tup_ctyp gs] + @ cleanup | AV_record (fields, typ) -> let ctyp = ctyp_of_typ ctx typ in let gs = gensym () in - let setup, cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup @@ -1239,10 +1234,9 @@ let rec compile_aval ctx = function @ field_cleanup in [idecl ctyp gs] - @ setup @ List.concat (List.map compile_fields (Bindings.bindings fields)), (F_id gs, ctyp), - cleanup + [iclear ctyp gs] | AV_vector ([], _) -> c_error "Encountered empty vector literal" @@ -1271,8 +1265,7 @@ let rec compile_aval ctx = function let first_chunk = bitstring (Util.take (len mod 64) avals) in let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in let gs = gensym () in - [idecl (CT_bits true) gs; - iinit (CT_bits true) gs (first_chunk, CT_bits64 (len mod 64, true))] + [iinit (CT_bits true) gs (first_chunk, CT_bits64 (len mod 64, true))] @ List.map (fun chunk -> ifuncall (CL_id gs) (mk_id "append_64") [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))] @@ -1327,7 +1320,6 @@ let rec compile_aval ctx = function @ cleanup in [idecl vector_ctyp gs; - ialloc vector_ctyp gs; iextern (CL_id gs) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)] vector_ctyp] @ List.concat (List.mapi aval_set avals), (F_id gs, vector_ctyp), @@ -1346,8 +1338,7 @@ let rec compile_aval ctx = function let setup, cval, cleanup = compile_aval ctx aval in setup @ [ifuncall (CL_id gs) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)] (CT_list ctyp)] @ cleanup in - [idecl (CT_list ctyp) gs; - ialloc (CT_list ctyp) gs] + [idecl (CT_list ctyp) gs] @ List.concat (List.map mk_cons (List.rev avals)), (F_id gs, CT_list ctyp), [iclear (CT_list ctyp) gs] @@ -1379,7 +1370,6 @@ let compile_funcall l ctx id args typ = cval else if is_stack_ctyp have_ctyp && not (is_stack_ctyp ctyp) then let gs = gensym () in - setup := idecl ctyp gs :: !setup; setup := iinit ctyp gs cval :: !setup; cleanup := iclear ctyp gs :: !cleanup; (F_id gs, ctyp) @@ -1390,7 +1380,6 @@ let compile_funcall l ctx id args typ = let gs1 = gensym () in let gs2 = gensym () in setup := idecl have_ctyp gs1 :: !setup; - setup := ialloc have_ctyp gs1 :: !setup; setup := icopy (CL_id gs1) cval :: !setup; setup := idecl ctyp gs2 :: !setup; setup := iconvert (CL_id gs2) ctyp gs1 have_ctyp :: !setup; @@ -1410,7 +1399,7 @@ let compile_funcall l ctx id args typ = fun ret -> ifuncall ret id sargs ret_ctyp else if not (is_stack_ctyp ret_ctyp) && is_stack_ctyp final_ctyp then let gs = gensym () in - setup := ialloc ret_ctyp gs :: idecl ret_ctyp gs :: !setup; + setup := idecl ret_ctyp gs :: !setup; setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; cleanup := iclear ret_ctyp gs :: !cleanup; fun ret -> iconvert ret final_ctyp gs ret_ctyp @@ -1449,13 +1438,11 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = | AP_id (pid, typ), _ -> let ctyp = cval_ctyp cval in let id_ctyp = ctyp_of_typ ctx typ in - let init, cleanup = if is_stack_ctyp id_ctyp then [], [] else [ialloc id_ctyp pid], [iclear id_ctyp pid] in if ctyp_equal id_ctyp ctyp then - [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup + [idecl ctyp pid; icopy (CL_id pid) cval], [iclear id_ctyp pid] else let gs = gensym () in - let gs_init, gs_cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in - [idecl id_ctyp pid; idecl ctyp gs] @ init @ gs_init @ [icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp] @ gs_cleanup, cleanup + [idecl id_ctyp pid; idecl ctyp gs; icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp; iclear ctyp gs], [iclear id_ctyp pid] | AP_tup apats, (frag, ctyp) -> begin let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in @@ -1508,10 +1495,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_let (id, _, binding, body, typ) -> let setup, ctyp, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = - if is_stack_ctyp ctyp then - [idecl ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], [] - else - [idecl ctyp id; ialloc ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], [iclear ctyp id] + [idecl ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], [iclear ctyp id] in let setup, ctyp, call, cleanup = compile_aexp ctx body in let body_ctyp = ctyp_of_typ ctx typ in @@ -1521,7 +1505,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = begin prerr_endline ("Mismatch: " ^ string_of_ctyp body_ctyp ^ " and " ^ string_of_ctyp ctyp); let gs = gensym () in - letb_setup @ setup @ [idecl ctyp gs; ialloc ctyp gs; call (CL_id gs)], + letb_setup @ setup @ [idecl ctyp gs; call (CL_id gs)], body_ctyp, (fun clexp -> iconvert clexp body_ctyp gs ctyp), [iclear ctyp gs] @ cleanup @ letb_cleanup @@ -1566,7 +1550,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = [iblock case_instrs; ilabel case_label] in [icomment "begin match"] - @ aval_setup @ [idecl ctyp case_return_id] @ (if is_stack_ctyp ctyp then [] else [ialloc ctyp case_return_id]) + @ aval_setup @ [idecl ctyp case_return_id] @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], @@ -1624,20 +1608,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let setup, ctyp, call, cleanup = compile_aexp ctx aexp in if ctyp_equal if_ctyp ctyp then fun clexp -> setup @ [call clexp] @ cleanup - else if is_stack_ctyp ctyp then - fun clexp -> - let gs = gensym() in - setup - @ [idecl ctyp gs; - call (CL_id gs); - iconvert clexp if_ctyp gs ctyp] - @ cleanup else fun clexp -> let gs = gensym () in setup @ [idecl ctyp gs; - ialloc ctyp gs; call (CL_id gs); iconvert clexp if_ctyp gs ctyp; iclear ctyp gs] @@ -1656,7 +1631,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_record_update (aval, fields, typ) -> let ctyp = ctyp_of_typ ctx typ in let gs = gensym () in - let gs_setup, gs_cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup @@ -1665,14 +1639,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = in let setup, cval, cleanup = compile_aval ctx aval in [idecl ctyp gs] - @ gs_setup @ setup @ [icopy (CL_id gs) cval] @ cleanup @ List.concat (List.map compile_fields (Bindings.bindings fields)), ctyp, (fun clexp -> icopy clexp (F_id gs, ctyp)), - gs_cleanup + [iclear ctyp gs] | AE_short_circuit (SC_and, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval ctx aval in @@ -1730,21 +1703,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = setup @ [call (CL_id id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup else if pointer_assign assign_ctyp ctyp then setup @ [call (CL_addr id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup - else if not (is_stack_ctyp assign_ctyp) && is_stack_ctyp ctyp then - let gs = gensym () in - setup @ [ icomment comment; - idecl ctyp gs; - call (CL_id gs); - iconvert (CL_id id) assign_ctyp gs ctyp - ], - CT_unit, - (fun clexp -> icopy clexp unit_fragment), - cleanup - else if is_stack_ctyp assign_ctyp && not (is_stack_ctyp ctyp) then + else let gs = gensym () in setup @ [ icomment comment; idecl ctyp gs; - ialloc ctyp gs; call (CL_id gs); iconvert (CL_id id) assign_ctyp gs ctyp; iclear ctyp gs @@ -1752,8 +1714,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup - else - failwith comment | AE_block (aexps, aexp, _) -> let block = compile_block ctx aexps in @@ -1824,7 +1784,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = [idecl (cval_ctyp cval) gs1; icopy (CL_id gs1) cval; idecl fn_return_ctyp gs2; - ialloc fn_return_ctyp gs2; iconvert (CL_id gs2) fn_return_ctyp gs1 (cval_ctyp cval); ireturn (F_id gs2, fn_return_ctyp)] else @@ -1881,7 +1840,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = else let gs' = gensym () in iblock (setup - @ [idecl ctyp gs'; ialloc ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs'] + @ [idecl ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs'] @ cleanup)] in @@ -1965,7 +1924,7 @@ let generate_cleanup instrs = let generate_cleanup' (I_aux (instr, _)) = match instr with | I_init (ctyp, id, cval) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)] - | I_alloc (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)] + | I_decl (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)] | instr -> [] in let is_clear ids = function @@ -2105,7 +2064,7 @@ let fix_exception_block ctx instrs = let rec map_try_block f (I_aux (instr, aux)) = let instr = match instr with - | I_decl _ | I_alloc _ | I_reset _ | I_init _ | I_reinit _ -> instr + | I_decl _ | I_reset _ | I_init _ | I_reinit _ -> instr | I_if (cval, instrs1, instrs2, ctyp) -> I_if (cval, List.map (map_try_block f) instrs1, List.map (map_try_block f) instrs2, ctyp) | I_funcall _ | I_convert _ | I_copy _ | I_clear _ | I_throw _ | I_return _ -> instr @@ -2218,20 +2177,13 @@ let rec compile_def ctx = function let end_label = label "let_end_" in let destructure, destructure_cleanup = compile_match ctx apat (F_id gs, ctyp) end_label in let gs_setup, gs_cleanup = - if is_stack_ctyp ctyp then [idecl ctyp gs], [] else - [idecl ctyp gs; ialloc ctyp gs], [iclear ctyp gs] + [idecl ctyp gs], [iclear ctyp gs] in let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in - let global_setup = - List.concat (List.map (fun (id, ctyp) -> if is_stack_ctyp ctyp then [] else [ialloc ctyp id]) bindings) - in - let global_cleanup = - List.concat (List.map (fun (id, ctyp) -> if is_stack_ctyp ctyp then [] else [iclear ctyp id]) bindings) - in let n = !letdef_count in incr letdef_count; let instrs = - global_setup @ [icomment "gs_setup"] @ gs_setup @ [icomment "setup"] @ setup + [icomment "gs_setup"] @ gs_setup @ [icomment "setup"] @ setup @ [icomment "call"] @ [call (CL_id gs)] @ [icomment "cleanup"] @@ -2241,7 +2193,7 @@ let rec compile_def ctx = function @ destructure_cleanup @ gs_cleanup @ [ilabel end_label] in - [CDEF_let (n, bindings, instrs, global_cleanup)], + [CDEF_let (n, bindings, instrs)], { ctx with letbinds = n :: ctx.letbinds } (* Only DEF_default that matters is default Order, but all order @@ -2308,7 +2260,6 @@ let rec instrs_rename from_id to_id = function | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs - | I_aux (I_alloc (ctyp, id), aux) :: instrs -> I_aux (I_alloc (ctyp, rename id), aux) :: irename instrs | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs @@ -2347,43 +2298,29 @@ let hoist_allocations ctx = function let decls = ref [] in let cleanups = ref [] in let rec hoist = function - | (I_aux (I_decl (ctyp, decl_id), _) as decl) :: instrs when hoist_ctyp ctyp -> + | I_aux (I_decl (ctyp, decl_id), annot) :: instrs when hoist_ctyp ctyp -> + let hid = hoist_id () in + decls := idecl ctyp hid :: !decls; + cleanups := iclear ctyp hid :: !cleanups; + let instrs = instrs_rename decl_id hid instrs in + I_aux (I_reset (ctyp, hid), annot) :: hoist instrs + + | I_aux (I_init (ctyp, decl_id, cval), annot) :: instrs when hoist_ctyp ctyp -> let hid = hoist_id () in - let hoist_stop (I_aux (instr, _)) = - match instr with - | I_if _ | I_block _ | I_try_block _ | I_alloc _ | I_init _ | I_clear _ -> true - | _ -> false - in - let rec replace_inits instrs = - match instr_split_at hoist_stop instrs with - | before, I_aux (I_alloc (ctyp, id), aux) :: after when Id.compare id hid = 0 -> - before @ I_aux (I_reset (ctyp, id), aux) :: replace_inits after - | before, I_aux (I_init (ctyp, id, cval), aux) :: after when Id.compare id hid = 0 -> - before @ I_aux (I_reinit (ctyp, id, cval), aux) :: replace_inits after - | before, I_aux (I_clear (ctyp, id), aux) :: after when Id.compare id hid = 0 -> - before @ replace_inits after - - | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: after -> - before @ I_aux (I_if (cval, replace_inits then_instrs, replace_inits else_instrs, ctyp), aux) :: replace_inits after - | before, I_aux (I_block instrs, aux) :: after -> - before @ I_aux (I_block (replace_inits instrs), aux) :: replace_inits after - | before, I_aux (I_try_block instrs, aux) :: after -> - before @ I_aux (I_try_block (replace_inits instrs), aux) :: replace_inits after - - | before, instr :: after -> before @ instr :: replace_inits after - | before, [] -> before - in - decls := ialloc ctyp hid :: idecl ctyp hid :: !decls; + decls := idecl ctyp hid :: !decls; cleanups := iclear ctyp hid :: !cleanups; - let instrs = replace_inits (instrs_rename decl_id hid instrs) in + let instrs = instrs_rename decl_id hid instrs in + I_aux (I_reinit (ctyp, hid, cval), annot) :: hoist instrs + + | I_aux (I_clear (ctyp, _), _) :: instrs when hoist_ctyp ctyp -> hoist instrs - | I_aux (I_block block, aux) :: instrs -> - I_aux (I_block (hoist block), aux) :: hoist instrs - | I_aux (I_try_block block, aux) :: instrs -> - I_aux (I_try_block (hoist block), aux) :: hoist instrs - | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> - I_aux (I_if (cval, hoist then_instrs, hoist else_instrs, ctyp), aux) :: hoist instrs + | I_aux (I_block block, annot) :: instrs -> + I_aux (I_block (hoist block), annot) :: hoist instrs + | I_aux (I_try_block block, annot) :: instrs -> + I_aux (I_try_block (hoist block), annot) :: hoist instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), annot) :: instrs -> + I_aux (I_if (cval, hoist then_instrs, hoist else_instrs, ctyp), annot) :: hoist instrs | instr :: instrs -> instr :: hoist instrs | [] -> [] @@ -2434,9 +2371,9 @@ let flatten_instrs ctx = flat_counter := 0; [CDEF_fundef (function_id, heap_return, args, flatten body)] - | CDEF_let (n, bindings, instrs, cleanup) -> + | CDEF_let (n, bindings, instrs) -> flat_counter := 0; - [CDEF_let (n, bindings, flatten instrs, flatten cleanup)] + [CDEF_let (n, bindings, flatten instrs)] | cdef -> [cdef] @@ -2585,8 +2522,12 @@ let sgen_clexp_pure = function let rec codegen_instr fid ctx (I_aux (instr, _)) = match instr with - | I_decl (ctyp, id) -> + | I_decl (ctyp, id) when is_stack_ctyp ctyp -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) + | I_decl (ctyp, id) -> + string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) ^^ hardline + ^^ string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + | I_copy (clexp, cval) -> let ctyp = cval_ctyp cval in if is_stack_ctyp ctyp then @@ -2665,24 +2606,36 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) else string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) + + | I_clear (ctyp, id) when is_stack_ctyp ctyp -> + empty | I_clear (ctyp, id) -> string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + + | I_init (ctyp, id, cval) when is_stack_ctyp ctyp -> + string (Printf.sprintf " %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval)) | I_init (ctyp, id, cval) -> - string (Printf.sprintf " CREATE_OF(%s, %s)(&%s, %s);" - (sgen_ctyp_name ctyp) - (sgen_ctyp_name (cval_ctyp cval)) - (sgen_id id) - (sgen_cval_param cval)) - | I_alloc (ctyp, id) -> - string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) ^^ hardline + ^^ string (Printf.sprintf " CREATE_OF(%s, %s)(&%s, %s);" + (sgen_ctyp_name ctyp) + (sgen_ctyp_name (cval_ctyp cval)) + (sgen_id id) + (sgen_cval_param cval)) + + | I_reinit (ctyp, id, cval) when is_stack_ctyp ctyp -> + string (Printf.sprintf " %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval)) | I_reinit (ctyp, id, cval) -> string (Printf.sprintf " RECREATE_OF(%s, %s)(&%s, %s);" (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_id id) (sgen_cval_param cval)) + + | I_reset (ctyp, id) when is_stack_ctyp ctyp -> + string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) | I_reset (ctyp, id) -> string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + (* FIXME: This just covers the cases we see in our specs, need a special conversion code-generator for full generality *) | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 -> @@ -2749,8 +2702,11 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string (str ^ ": ;") | I_goto str -> string (Printf.sprintf " goto %s;" str) + + | I_raw _ when ctx.no_raw -> empty | I_raw str -> string (" " ^ str) + | I_match_failure -> string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") @@ -3152,6 +3108,12 @@ let codegen_decl = function string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) | _ -> assert false +let codegen_alloc = function + | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty + | I_aux (I_decl (ctyp, id), _) -> + string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + | _ -> assert false + let codegen_def' ctx = function | CDEF_reg_dec (id, ctyp) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline @@ -3204,11 +3166,11 @@ let codegen_def' ctx = function | CDEF_startup (id, instrs) -> let startup_header = string (Printf.sprintf "void startup_%s(void)" (sgen_id id)) in - separate_map hardline codegen_decl (List.filter is_decl instrs) + separate_map hardline codegen_decl instrs ^^ twice hardline ^^ startup_header ^^ hardline ^^ string "{" - ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) (List.filter (fun i -> not (is_decl i)) instrs)) ^^ hardline + ^^ jump 0 2 (separate_map hardline codegen_alloc instrs) ^^ hardline ^^ string "}" | CDEF_finish (id, instrs) -> @@ -3217,15 +3179,22 @@ let codegen_def' ctx = function ^^ twice hardline ^^ finish_header ^^ hardline ^^ string "{" - ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) (List.filter (fun i -> not (is_decl i)) instrs)) ^^ hardline + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline ^^ string "}" - | CDEF_let (number, bindings, instrs, cleanup) -> + | CDEF_let (number, bindings, instrs) -> let instrs = add_local_labels instrs in + let setup = + List.concat (List.map (fun (id, ctyp) -> [idecl ctyp id]) bindings) + in + let cleanup = + List.concat (List.map (fun (id, ctyp) -> [iclear ctyp id]) bindings) + in separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline ^^ string (Printf.sprintf "void create_letbind_%d(void) " number) ^^ string "{" - ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) instrs) ^^ hardline + ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline + ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") { ctx with no_raw = true }) instrs) ^^ hardline ^^ string "}" ^^ hardline ^^ string (Printf.sprintf "void kill_letbind_%d(void) " number) ^^ string "{" @@ -3329,7 +3298,7 @@ let instrument_tracing ctx = let bytecode_ast ctx rewrites (Defs defs) = let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in let exit_vs = Initial_check.extern_of_string dec_ord (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 cdefs = List.concat (List.rev chunks) in diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh index b1ead724..37787605 100755 --- a/test/c/run_tests.sh +++ b/test/c/run_tests.sh @@ -54,7 +54,7 @@ function run_c_tests { if $SAILDIR/sail -no_warn -c $SAIL_OPTS $file 1> ${file%.sail}.c 2> /dev/null; then green "compiling $(basename $file) ($SAIL_OPTS)" "ok"; - if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -I $SAILDIR/lib; + if gcc $CC_OPTS ${file%.sail}.c $SAILDIR/lib/*.c -lgmp -lz -I $SAILDIR/lib; then green "compiling $(basename ${file%.sail}.c) ($CC_OPTS)" "ok"; $DIR/a.out 1> ${file%.sail}.result 2> /dev/null; -- cgit v1.2.3 From 3658789d204eb100e901a2adb67b6bf8a30157bf Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 21 Jun 2018 16:06:21 +0100 Subject: Fix MIPS wrt changes to C runtime This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz. --- lib/elf.c | 2 +- lib/elf.h | 2 +- lib/sail.c | 111 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/sail.h | 20 ++++++++++ mips/Makefile | 2 +- mips/prelude.sail | 6 +-- src/c_backend.ml | 12 ++++-- 7 files changed, 145 insertions(+), 10 deletions(-) diff --git a/lib/elf.c b/lib/elf.c index e0e75c91..566ca96a 100644 --- a/lib/elf.c +++ b/lib/elf.c @@ -357,7 +357,7 @@ void loadELFHdr(const char* buffer, const int total_file_size) { } } -void loadELF(char *filename) { +void load_elf(char *filename) { // Read input file into memory char* buffer = NULL; int size = 0; diff --git a/lib/elf.h b/lib/elf.h index 16dff677..e5f90365 100644 --- a/lib/elf.h +++ b/lib/elf.h @@ -2,4 +2,4 @@ #include -void loadELF(char *filename); +void load_elf(char *filename); diff --git a/lib/sail.c b/lib/sail.c index d377b099..66321590 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -37,6 +37,11 @@ unit UNDEFINED(unit)(const unit u) return UNIT; } +unit skip(const unit u) +{ + return UNIT; +} + /* ***** Sail bit type ***** */ bool eq_bit(const mach_bits a, const mach_bits b) @@ -453,6 +458,28 @@ void not_bits(sail_bits *rop, const sail_bits op) } } +void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + mpz_t op1_int, op2_int; + mpz_init(op1_int); + mpz_init(op2_int); + sail_signed(&op1_int, op1); + sail_signed(&op2_int, op2); + rop->len = op1.len * 2; + mpz_mul(*rop->bits, op1_int, op2_int); + normalize_sail_bits(rop); + mpz_clear(op1_int); + mpz_clear(op2_int); +} + +void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len * 2; + mpz_mul(*rop->bits, *op1.bits, *op2.bits); + normalize_sail_bits(rop); /* necessary? */ +} + + void zeros(sail_bits *rop, const sail_int op) { rop->len = mpz_get_ui(op); @@ -465,6 +492,19 @@ void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len) mpz_set(*rop->bits, *op.bits); } +void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len) +{ + rop->len = mpz_get_ui(len); + if(mpz_tstbit(*op.bits, op.len - 1)) { + mpz_set(*rop->bits, *op.bits); + for(mp_bitcnt_t i = rop->len - 1; i >= op.len; i--) { + mpz_setbit(*rop->bits, i); + } + } else { + mpz_set(*rop->bits, *op.bits); + } +} + void length_sail_bits(sail_int *rop, const sail_bits op) { mpz_set_ui(*rop, op.len); @@ -659,6 +699,68 @@ void set_slice(sail_bits *rop, } } +void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits)); + normalize_sail_bits(rop); +} + +void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits)); +} + +/* FIXME */ +void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2) +{ + rop->len = op1.len; + mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits); + mp_bitcnt_t sign_bit = op1.len - 1; + mpz_fdiv_q_2exp(*rop->bits, *op1.bits, shift_amt); + if(mpz_tstbit(*op1.bits, sign_bit) != 0) { + /* */ + for(; shift_amt > 0; shift_amt--) { + mpz_setbit(*rop->bits, sign_bit - shift_amt + 1); + } + } +} + +void reverse_endianness(sail_bits *rop, const sail_bits op) +{ + rop->len = op.len; + if (rop->len == 64ul) { + uint64_t x = mpz_get_ui(*op.bits); + x = (x & 0xFFFFFFFF00000000) >> 32 | (x & 0x00000000FFFFFFFF) << 32; + x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16; + x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8; + mpz_set_ui(*rop->bits, x); + } else if (rop->len == 32ul) { + uint64_t x = mpz_get_ui(*op.bits); + x = (x & 0xFFFF0000FFFF0000) >> 16 | (x & 0x0000FFFF0000FFFF) << 16; + x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8; + mpz_set_ui(*rop->bits, x); + } else if (rop->len == 16ul) { + uint64_t x = mpz_get_ui(*op.bits); + x = (x & 0xFF00FF00FF00FF00) >> 8 | (x & 0x00FF00FF00FF00FF) << 8; + mpz_set_ui(*rop->bits, x); + } else if (rop->len == 8ul) { + mpz_set(*rop->bits, *op.bits); + } else { + /* For other numbers of bytes we reverse the bytes. + * XXX could use mpz_import/export for this. */ + mpz_set_ui(sail_lib_tmp1, 0xff); // byte mask + mpz_set_ui(*rop->bits, 0); // reset accumulator for result + for(mp_bitcnt_t byte = 0; byte < op.len; byte+=8) { + mpz_tdiv_q_2exp(sail_lib_tmp2, *op.bits, byte); // shift byte to bottom + mpz_and(sail_lib_tmp2, sail_lib_tmp2, sail_lib_tmp1); // and with mask + mpz_mul_2exp(*rop->bits, *rop->bits, 8); // shift result left 8 + mpz_ior(*rop->bits, *rop->bits, sail_lib_tmp2); // or byte into result + } + } +} + /* ***** Sail Reals ***** */ void CREATE(real)(real *rop) @@ -890,3 +992,12 @@ unit sail_putchar(const sail_int op) putchar(c); return UNIT; } + +void get_time_ns(sail_int *rop, const unit u) +{ + struct timespec t; + clock_gettime(CLOCK_REALTIME, &t); + mpz_set_si(*rop, t.tv_sec); + mpz_mul_ui(*rop, *rop, 1000000000); + mpz_add_ui(*rop, *rop, t.tv_nsec); +} diff --git a/lib/sail.h b/lib/sail.h index 2a143605..e3e21c92 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -9,6 +9,8 @@ #include #endif +#include + /* * Called by the RTS to initialise and clear any library state. */ @@ -44,6 +46,8 @@ typedef int unit; unit UNDEFINED(unit)(const unit); bool eq_unit(const unit, const unit); +unit skip(const unit); + /* ***** Sail booleans ***** */ /* @@ -203,8 +207,13 @@ void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2); void not_bits(sail_bits *rop, const sail_bits op); +void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2); + void zeros(sail_bits *rop, const sail_int op); + void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len); +void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len); void length_sail_bits(sail_int *rop, const sail_bits op); @@ -250,6 +259,13 @@ void set_slice(sail_bits *rop, const sail_int start_mpz, const sail_bits slice); + +void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2); + +void reverse_endianness(sail_bits*, sail_bits); + /* ***** Sail reals ***** */ typedef mpf_t real; @@ -310,3 +326,7 @@ 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 ***** */ + +void get_time_ns(sail_int*, const unit); diff --git a/mips/Makefile b/mips/Makefile index 6abf1848..007d56c7 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -19,7 +19,7 @@ mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail $(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@ mips_c: mips.c ../lib/sail.h Makefile - gcc -O2 -g -I ../lib $< -l gmp -o $@ + gcc -O2 -g -I ../lib $< ../lib/*.c -lgmp -lz -o $@ mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ diff --git a/mips/prelude.sail b/mips/prelude.sail index b2c2931b..bb80ec86 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -103,10 +103,10 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int overload operator / = {quotient_nat, quotient} -val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", _ : "div_int"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", _ : "mod_int"} : (int, int) -> int +val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", _ : "tdiv_int"} : (int, int) -> int +val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", _ : "tmod_int"} : (int, int) -> int -val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "mod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) +val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) overload operator % = {modulus} diff --git a/src/c_backend.ml b/src/c_backend.ml index 0a9bede0..f14fdace 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -963,6 +963,8 @@ let c_fragment = function | AV_C_fragment (frag, _) -> frag | _ -> assert false +let v_mask_lower i = F_lit (V_bits (Util.list_init i (fun _ -> Sail_values.B1))) + let analyze_primop' ctx env l id args typ = let ctx = { ctx with local_env = env } in let no_change = AE_app (id, args, typ) in @@ -993,10 +995,12 @@ let analyze_primop' ctx env l id args typ = | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "&", v2), typ)) - (* | "not_bits", [AV_C_fragment (v, _)] -> - AE_val (AV_C_fragment (F_unary ("~", v), typ)) - *) + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_op (F_unary ("~", v), "&", v_mask_lower (Big_int.to_int n)), typ)) + end | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> let len = F_op (f, "-", F_op (t, "-", v_one)) in @@ -3370,7 +3374,7 @@ let compile_ast ctx (Defs defs) = let postamble = separate hardline (List.map string ( [ "int main(int argc, char *argv[])"; "{"; - " if (argc > 1) { loadELF(argv[1]); }"; + " if (argc > 1) { load_image(argv[1]); }"; " setup_rts();" ] @ fst exn_boilerplate @ startup cdefs -- cgit v1.2.3