diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 4 | ||||
| -rw-r--r-- | lib/rts.c | 54 | ||||
| -rw-r--r-- | lib/rts.h | 32 | ||||
| -rw-r--r-- | lib/sail.c | 341 | ||||
| -rw-r--r-- | lib/sail.h | 83 | ||||
| -rw-r--r-- | lib/smt.sail | 4 |
6 files changed, 498 insertions, 20 deletions
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 @@ -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) @@ -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. @@ -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; +} @@ -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} |