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 --- lib/sail.h | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) (limited to 'lib') 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) { -- 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 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 149 insertions(+), 12 deletions(-) (limited to 'lib') 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 -- 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 --- lib/rts.c | 275 ++++++++++ lib/rts.h | 86 ++++ lib/sail.c | 558 +++++++++++++++++++++ lib/sail.h | 1380 +++++++-------------------------------------------- lib/vector_dec.sail | 7 +- 5 files changed, 1094 insertions(+), 1212 deletions(-) create mode 100644 lib/rts.c create mode 100644 lib/rts.h create mode 100644 lib/sail.c (limited to 'lib') 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 -- 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 +- 6 files changed, 498 insertions(+), 20 deletions(-) (limited to 'lib') 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} -- 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 + 3 files changed, 11 insertions(+), 2 deletions(-) (limited to 'lib') 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); -- 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 +- 7 files changed, 407 insertions(+), 5 deletions(-) create mode 100644 lib/elf.c create mode 100644 lib/elf.h (limited to 'lib') 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) -- 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. --- lib/rts.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') 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. */ -- 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 +++++++++++ 4 files changed, 133 insertions(+), 2 deletions(-) (limited to 'lib') 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); -- cgit v1.2.3