diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 20 | ||||
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 22 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 42 | ||||
| -rw-r--r-- | lib/flow.sail | 2 | ||||
| -rw-r--r-- | lib/rts.c | 24 | ||||
| -rw-r--r-- | lib/rts.h | 24 | ||||
| -rw-r--r-- | lib/sail.c | 285 | ||||
| -rw-r--r-- | lib/sail.h | 192 | ||||
| -rw-r--r-- | lib/smt.sail | 6 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 16 | ||||
| -rw-r--r-- | lib/vector_inc.sail | 8 |
11 files changed, 437 insertions, 204 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 61a1ff76..db011f14 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -50,7 +50,25 @@ val "prerr_int" : (string, int) -> unit // ***** Integer shifts ***** -val shl_int = "shl_int" : (int, int) -> int +/*! +A common idiom in asl is to take two bits of an opcode and convert in into a variable like +``` +let elsize = shl_int(8, UInt(size)) +``` +THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` +*/ +val _shl8 = {c: "shl_mach_int", _: "shl_int"} : + forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64} + +/*! +Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` +*/ +val _shl32 = {c: "shl_mach_int", _: "shl_int"} : + forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64} + +val _shl_int = "shl_int" : (int, int) -> int + +overload shl_int = {_shl8, _shl32, _shl_int} val shr_int = "shr_int" : (int, int) -> int diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 497b4a46..e37e9d26 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -9,12 +9,6 @@ Require Import ZArith. Require Import Omega. Require Import Eqdep_dec. -Module Z_eq_dec. -Definition U := Z. -Definition eq_dec := Z.eq_dec. -End Z_eq_dec. -Module ZEqdep := DecidableEqDep (Z_eq_dec). - Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q. refine ( match p, q with @@ -444,6 +438,20 @@ Definition sgteq_vec := sgteq_bv. *) +Definition eq_vec_dec {n} : forall (x y : mword n), {x = y} + {x <> y}. +refine (match n with +| Z0 => _ +| Zpos m => _ +| Zneg m => _ +end). +* simpl. apply Word.weq. +* simpl. apply Word.weq. +* simpl. destruct x. +Defined. + +Instance Decidable_eq_mword {n} : forall (x y : mword n), Decidable (x = y) := + Decidable_eq_from_dec eq_vec_dec. + Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n := match n with | S (S (S (S (S (S (S (S m))))))) => @@ -471,3 +479,5 @@ Definition set_slice_int len n lo (v : mword len) : Z := let bs : mword (hi + 1) := mword_of_int n in (int_of_mword true (update_subrange_vec_dec bs hi lo v)) else n. + +Definition prerr_bits {a} (s : string) (bs : mword a) : unit := tt. diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 83fe1dc7..aebc3376 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -8,10 +8,18 @@ Require Import bbv.Word. Require Export List. Require Export Sumbool. Require Export DecidableClass. +Require Import Eqdep_dec. Import ListNotations. Open Scope Z. +Module Z_eq_dec. +Definition U := Z. +Definition eq_dec := Z.eq_dec. +End Z_eq_dec. +Module ZEqdep := DecidableEqDep (Z_eq_dec). + + (* Constraint solving basics. A HintDb which unfolding hints and lemmata can be added to, and a typeclass to wrap constraint arguments in to trigger automatic solving. *) @@ -93,6 +101,22 @@ split. tauto. Qed. +Definition generic_dec {T:Type} (x y:T) `{Decidable (x = y)} : {x = y} + {x <> y}. +refine ((if Decidable_witness as b return (b = true <-> x = y -> _) then fun H' => _ else fun H' => _) Decidable_spec). +* left. tauto. +* right. intuition. +Defined. + +(* Used by generated code that builds Decidable equality instances for records. *) +Ltac cmp_record_field x y := + let H := fresh "H" in + case (generic_dec x y); + intro H; [ | + refine (Build_Decidable _ false _); + split; [congruence | intros Z; destruct H; injection Z; auto] + ]. + + (* Project away range constraints in comparisons *) Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r. @@ -1736,6 +1760,20 @@ Qed. Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v. +Definition vec_eq_dec {T n} (D : forall x y : T, {x = y} + {x <> y}) (x y : vec T n) : + {x = y} + {x <> y}. +refine (if List.list_eq_dec D (projT1 x) (projT1 y) then left _ else right _). +* apply eq_sigT_hprop; auto using ZEqdep.UIP. +* contradict n0. rewrite n0. reflexivity. +Defined. + +Instance Decidable_eq_vec {T : Type} {n} `(DT : forall x y : T, Decidable (x = y)) : + forall x y : vec T n, Decidable (x = y) := { + Decidable_witness := proj1_sig (bool_of_sumbool (vec_eq_dec (fun x y => generic_dec x y) x y)) +}. +destruct (vec_eq_dec _ x y); simpl; split; congruence. +Defined. + Program Definition vec_of_list {A} n (l : list A) : option (vec A n) := if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None. Next Obligation. @@ -1756,3 +1794,7 @@ Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y {z : Z & ArithFact (z >= 0)} := let z := projT1 x - projT1 y in if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0. + +Definition min_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) : + {z : Z & ArithFact (z >= 0)} := + build_ex (Z.min (projT1 x) (projT1 y)). diff --git a/lib/flow.sail b/lib/flow.sail index 5ee9a74a..cdc6b2fd 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -11,7 +11,7 @@ therefore be included in just about every Sail specification. val eq_unit : (unit, unit) -> bool -val "eq_bit" : (bit, bit) -> bool +val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool function eq_unit(_, _) = true @@ -32,7 +32,7 @@ unit sail_exit(unit u) static uint64_t g_verbosity = 0; -mach_bits sail_get_verbosity(const unit u) +fbits sail_get_verbosity(const unit u) { return g_verbosity; } @@ -94,6 +94,10 @@ void write_mem(uint64_t address, uint64_t byte) uint64_t mask = address & ~MASK; uint64_t offset = address & MASK; + //if ((byte >= 97 && byte <= 122) || (byte >= 64 && byte <= 90) || (byte >= 48 && byte <= 57) || byte == 10 || byte == 32) { + // fprintf(stderr, "%c", (char) byte); + //} + struct block *current = sail_memory; while (current != NULL) { @@ -210,9 +214,9 @@ void kill_mem() bool 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) + const lbits hex_ram, // Currently unused + const lbits addr_bv, + const lbits data) { uint64_t addr = mpz_get_ui(*addr_bv.bits); uint64_t data_size = mpz_get_ui(data_size_mpz); @@ -234,11 +238,11 @@ bool write_ram(const mpz_t addr_size, // Either 32 or 64 return true; } -void read_ram(sail_bits *data, +void read_ram(lbits *data, const mpz_t addr_size, const mpz_t data_size_mpz, - const sail_bits hex_ram, - const sail_bits addr_bv) + const lbits hex_ram, + const lbits addr_bv) { uint64_t addr = mpz_get_ui(*addr_bv.bits); uint64_t data_size = mpz_get_ui(data_size_mpz); @@ -257,7 +261,7 @@ void read_ram(sail_bits *data, mpz_clear(byte); } -unit load_raw(mach_bits addr, const sail_string file) +unit load_raw(fbits addr, const sail_string file) { FILE *fp = fopen(file, "r"); @@ -335,7 +339,7 @@ bool is_tracing(const unit u) return g_trace_enabled; } -void trace_mach_bits(const mach_bits x) { +void trace_fbits(const fbits x) { if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x); } @@ -351,7 +355,7 @@ 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) { +void trace_lbits(const lbits op) { if (g_trace_enabled) fprint_bits("", op, "", stderr); } @@ -26,7 +26,7 @@ unit sail_exit(unit); * The intention is that you can use individual bits to turn on/off different * pieces of debugging output. */ -mach_bits sail_get_verbosity(const unit u); +fbits sail_get_verbosity(const unit u); /* * Put processor to sleep until an external device calls wakeup_request(). @@ -55,20 +55,20 @@ uint64_t read_mem(uint64_t); bool 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); + const lbits hex_ram, // Currently unused + const lbits addr_bv, + const lbits data); -void read_ram(sail_bits *data, +void read_ram(lbits *data, const mpz_t addr_size, const mpz_t data_size_mpz, - const sail_bits hex_ram, - const sail_bits addr_bv); + const lbits hex_ram, + const lbits addr_bv); -unit write_tag_bool(const mach_bits, const bool); -bool read_tag_bool(const mach_bits); +unit write_tag_bool(const fbits, const bool); +bool read_tag_bool(const fbits); -unit load_raw(mach_bits addr, const sail_string file); +unit load_raw(fbits addr, const sail_string file); void load_image(char *); @@ -106,8 +106,8 @@ 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_fbits(const fbits); +void trace_lbits(const lbits); void trace_unknown(void); void trace_argsep(void); @@ -7,6 +7,8 @@ #include<string.h> #include<time.h> +#include <x86intrin.h> + #include"sail.h" /* @@ -53,7 +55,7 @@ unit skip(const unit u) /* ***** Sail bit type ***** */ -bool eq_bit(const mach_bits a, const mach_bits b) +bool eq_bit(const fbits a, const fbits b) { return a == b; } @@ -291,6 +293,12 @@ void shl_int(sail_int *rop, const sail_int op1, const sail_int op2) } inline +mach_int shl_mach_int(const mach_int op1, const mach_int op2) +{ + return op1 << 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)); @@ -409,69 +417,144 @@ void pow2(sail_int *rop, const sail_int exp) /* ***** Sail bitvectors ***** */ -bool EQUAL(mach_bits)(const mach_bits op1, const mach_bits op2) +bool EQUAL(fbits)(const fbits op1, const fbits op2) { return op1 == op2; } -void CREATE(sail_bits)(sail_bits *rop) +void CREATE(lbits)(lbits *rop) { rop->bits = malloc(sizeof(mpz_t)); rop->len = 0; mpz_init(*rop->bits); } -void RECREATE(sail_bits)(sail_bits *rop) +void RECREATE(lbits)(lbits *rop) { rop->len = 0; mpz_set_ui(*rop->bits, 0); } -void COPY(sail_bits)(sail_bits *rop, const sail_bits op) +void COPY(lbits)(lbits *rop, const lbits op) { rop->len = op.len; mpz_set(*rop->bits, *op.bits); } -void KILL(sail_bits)(sail_bits *rop) +void KILL(lbits)(lbits *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) +void CREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len, const bool direction) { rop->bits = malloc(sizeof(mpz_t)); rop->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) +fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction) +{ + return mpz_get_ui(*op.bits); +} + +sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction) +{ + sbits rop; + rop.bits = mpz_get_ui(*op.bits); + rop.len = op.len; + return rop; +} + +sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction) +{ + sbits rop; + rop.bits = op; + rop.len = len; + return rop; +} + +void RECREATE_OF(lbits, fbits)(lbits *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, const bool direction) +void CREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction) +{ + rop->bits = malloc(sizeof(mpz_t)); + rop->len = op.len; + mpz_init_set_ui(*rop->bits, op.bits); +} + +void RECREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction) +{ + rop->len = op.len; + mpz_set_ui(*rop->bits, op.bits); +} + +// Bitvector conversions + +inline +fbits CONVERT_OF(fbits, lbits)(const lbits op, const bool direction) { return mpz_get_ui(*op.bits); } -void CONVERT_OF(sail_bits, mach_bits)(sail_bits *rop, const mach_bits op, const uint64_t len, const bool direction) +inline +fbits CONVERT_OF(fbits, sbits)(const sbits op, const bool direction) +{ + return op.bits; +} + +void CONVERT_OF(lbits, fbits)(lbits *rop, const fbits op, const uint64_t len, const bool direction) { 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) +void CONVERT_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction) +{ + rop->len = op.len; + mpz_set_ui(*rop->bits, op.bits & safe_rshift(UINT64_MAX, 64 - op.len)); +} + +inline +sbits CONVERT_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction) +{ + sbits rop; + rop.len = len; + rop.bits = op; + return rop; +} + +inline +sbits CONVERT_OF(sbits, lbits)(const lbits op, const bool direction) +{ + sbits rop; + rop.len = op.len; + rop.bits = mpz_get_ui(*op.bits); + return rop; +} + +void UNDEFINED(lbits)(lbits *rop, const sail_int len, const fbits bit) { zeros(rop, len); } -mach_bits UNDEFINED(mach_bits)(const unit u) { return 0; } +fbits UNDEFINED(fbits)(const unit u) { return 0; } + +sbits undefined_sbits(void) +{ + sbits rop; + rop.bits = UINT64_C(0); + rop.len = UINT64_C(0); + return rop; +} -mach_bits safe_rshift(const mach_bits x, const mach_bits n) +fbits safe_rshift(const fbits x, const fbits n) { if (n >= 64) { return 0ul; @@ -480,7 +563,7 @@ mach_bits safe_rshift(const mach_bits x, const mach_bits n) } } -void normalize_sail_bits(sail_bits *rop) { +void normalize_lbits(lbits *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); @@ -488,64 +571,64 @@ void normalize_sail_bits(sail_bits *rop) { mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1); } -void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk) +void append_64(lbits *rop, const lbits op, const fbits 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) +void add_bits(lbits *rop, const lbits op1, const lbits op2) { rop->len = op1.len; mpz_add(*rop->bits, *op1.bits, *op2.bits); - normalize_sail_bits(rop); + normalize_lbits(rop); } -void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) +void sub_bits(lbits *rop, const lbits op1, const lbits op2) { assert(op1.len == op2.len); rop->len = op1.len; mpz_sub(*rop->bits, *op1.bits, *op2.bits); - normalize_sail_bits(rop); + normalize_lbits(rop); } -void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2) +void add_bits_int(lbits *rop, const lbits op1, const mpz_t op2) { rop->len = op1.len; mpz_add(*rop->bits, *op1.bits, op2); - normalize_sail_bits(rop); + normalize_lbits(rop); } -void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2) +void sub_bits_int(lbits *rop, const lbits op1, const mpz_t op2) { rop->len = op1.len; mpz_sub(*rop->bits, *op1.bits, op2); - normalize_sail_bits(rop); + normalize_lbits(rop); } -void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) +void and_bits(lbits *rop, const lbits op1, const lbits op2) { assert(op1.len == op2.len); 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) +void or_bits(lbits *rop, const lbits op1, const lbits op2) { assert(op1.len == op2.len); 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) +void xor_bits(lbits *rop, const lbits op1, const lbits op2) { assert(op1.len == op2.len); rop->len = op1.len; mpz_xor(*rop->bits, *op1.bits, *op2.bits); } -void not_bits(sail_bits *rop, const sail_bits op) +void not_bits(lbits *rop, const lbits op) { rop->len = op.len; mpz_set(*rop->bits, *op.bits); @@ -554,7 +637,7 @@ 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 mults_vec(lbits *rop, const lbits op1, const lbits op2) { mpz_t op1_int, op2_int; mpz_init(op1_int); @@ -563,33 +646,33 @@ void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2) sail_signed(&op2_int, op2); rop->len = op1.len * 2; mpz_mul(*rop->bits, op1_int, op2_int); - normalize_sail_bits(rop); + normalize_lbits(rop); mpz_clear(op1_int); mpz_clear(op2_int); } -void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2) +void mult_vec(lbits *rop, const lbits op1, const lbits op2) { rop->len = op1.len * 2; mpz_mul(*rop->bits, *op1.bits, *op2.bits); - normalize_sail_bits(rop); /* necessary? */ + normalize_lbits(rop); /* necessary? */ } -void zeros(sail_bits *rop, const sail_int op) +void zeros(lbits *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) +void zero_extend(lbits *rop, const lbits op, const sail_int len) { assert(op.len <= mpz_get_ui(len)); rop->len = mpz_get_ui(len); mpz_set(*rop->bits, *op.bits); } -void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len) +void sign_extend(lbits *rop, const lbits op, const sail_int len) { assert(op.len <= mpz_get_ui(len)); rop->len = mpz_get_ui(len); @@ -603,12 +686,12 @@ 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) +void length_lbits(sail_int *rop, const lbits op) { mpz_set_ui(*rop, op.len); } -bool eq_bits(const sail_bits op1, const sail_bits op2) +bool eq_bits(const lbits op1, const lbits op2) { assert(op1.len == op2.len); for (mp_bitcnt_t i = 0; i < op1.len; i++) { @@ -617,12 +700,12 @@ bool eq_bits(const sail_bits op1, const sail_bits op2) return true; } -bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2) +bool EQUAL(lbits)(const lbits op1, const lbits op2) { return eq_bits(op1, op2); } -bool neq_bits(const sail_bits op1, const sail_bits op2) +bool neq_bits(const lbits op1, const lbits op2) { assert(op1.len == op2.len); for (mp_bitcnt_t i = 0; i < op1.len; i++) { @@ -631,8 +714,8 @@ bool neq_bits(const sail_bits op1, const sail_bits op2) return false; } -void vector_subrange_sail_bits(sail_bits *rop, - const sail_bits op, +void vector_subrange_lbits(lbits *rop, + const lbits op, const sail_int n_mpz, const sail_int m_mpz) { @@ -641,30 +724,30 @@ void vector_subrange_sail_bits(sail_bits *rop, rop->len = n - (m - 1ul); mpz_fdiv_q_2exp(*rop->bits, *op.bits, m); - normalize_sail_bits(rop); + normalize_lbits(rop); } -void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len) +void sail_truncate(lbits *rop, const lbits op, const sail_int len) { assert(op.len >= mpz_get_ui(len)); rop->len = mpz_get_ui(len); mpz_set(*rop->bits, *op.bits); - normalize_sail_bits(rop); + normalize_lbits(rop); } -mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz) +fbits bitvector_access(const lbits op, const sail_int n_mpz) { uint64_t n = mpz_get_ui(n_mpz); - return (mach_bits) mpz_tstbit(*op.bits, n); + return (fbits) mpz_tstbit(*op.bits, n); } -void sail_unsigned(sail_int *rop, const sail_bits op) +void sail_unsigned(sail_int *rop, const lbits 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) +void sail_signed(sail_int *rop, const lbits op) { if (op.len == 0) { mpz_set_ui(*rop, 0); @@ -682,14 +765,20 @@ void sail_signed(sail_int *rop, const sail_bits op) } } -void append(sail_bits *rop, const sail_bits op1, const sail_bits op2) +inline +mach_int fast_unsigned(const fbits op) +{ + return (mach_int) op; +} + +void append(lbits *rop, const lbits op1, const lbits 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) +void replicate_bits(lbits *rop, const lbits op1, const mpz_t op2) { uint64_t op2_ui = mpz_get_ui(op2); rop->len = op1.len * op2_ui; @@ -725,7 +814,7 @@ uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64 // <-------^ // (8 bit) 4 // -void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz) +void get_slice_int(lbits *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); @@ -744,7 +833,7 @@ 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) + const lbits slice) { uint64_t start = mpz_get_ui(start_mpz); @@ -759,11 +848,11 @@ void set_slice_int(sail_int *rop, } } -void vector_update_subrange_sail_bits(sail_bits *rop, - const sail_bits op, +void vector_update_subrange_lbits(lbits *rop, + const lbits op, const sail_int n_mpz, const sail_int m_mpz, - const sail_bits slice) + const lbits slice) { uint64_t n = mpz_get_ui(n_mpz); uint64_t m = mpz_get_ui(m_mpz); @@ -780,7 +869,7 @@ void vector_update_subrange_sail_bits(sail_bits *rop, } } -void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz) +void slice(lbits *rop, const lbits op, const sail_int start_mpz, const sail_int len_mpz) { assert(mpz_get_ui(start_mpz) + mpz_get_ui(len_mpz) <= op.len); uint64_t start = mpz_get_ui(start_mpz); @@ -794,12 +883,25 @@ void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const s } } -void set_slice(sail_bits *rop, +inline +sbits sslice(const fbits op, const mach_int start, const mach_int len) +{ + sbits rop; +#ifdef INTRINSICS + rop.bits = _bzhi_u64(op >> start, len); +#else + rop.bits = (op >> start) & safe_rshift(UINT64_MAX, 64 - len); +#endif + rop.len = len; + return rop; +} + +void set_slice(lbits *rop, const sail_int len_mpz, const sail_int slen_mpz, - const sail_bits op, + const lbits op, const sail_int start_mpz, - const sail_bits slice) + const lbits slice) { uint64_t start = mpz_get_ui(start_mpz); @@ -815,21 +917,21 @@ void set_slice(sail_bits *rop, } } -void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2) +void shift_bits_left(lbits *rop, const lbits op1, const lbits op2) { rop->len = op1.len; mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits)); - normalize_sail_bits(rop); + normalize_lbits(rop); } -void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2) +void shift_bits_right(lbits *rop, const lbits op1, const lbits 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) +void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2) { rop->len = op1.len; mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits); @@ -843,20 +945,20 @@ void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits } } -void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2) +void shiftl(lbits *rop, const lbits op1, const sail_int op2) { rop->len = op1.len; mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2)); - normalize_sail_bits(rop); + normalize_lbits(rop); } -void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2) +void shiftr(lbits *rop, const lbits op1, const sail_int op2) { rop->len = op1.len; mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2)); } -void reverse_endianness(sail_bits *rop, const sail_bits op) +void reverse_endianness(lbits *rop, const lbits op) { rop->len = op.len; if (rop->len == 64ul) { @@ -890,6 +992,26 @@ void reverse_endianness(sail_bits *rop, const sail_bits op) } } +inline +bool eq_sbits(const sbits op1, const sbits op2) +{ + return op1.bits == op2.bits; +} + +inline +bool neq_sbits(const sbits op1, const sbits op2) +{ + return op1.bits != op2.bits; +} + +sbits xor_sbits(const sbits op1, const sbits op2) +{ + sbits rop; + rop.bits = op1.bits ^ op2.bits; + rop.len = op1.len; + return rop; +} + /* ***** Sail Reals ***** */ void CREATE(real)(real *rop) @@ -1127,42 +1249,53 @@ void random_real(real *rop, const unit u) void string_of_int(sail_string *str, const sail_int i) { + free(*str); gmp_asprintf(str, "%Zd", i); } -/* asprinf is a GNU extension, but it should exist on BSD */ -void string_of_mach_bits(sail_string *str, const mach_bits op) +/* asprintf is a GNU extension, but it should exist on BSD */ +void string_of_fbits(sail_string *str, const fbits op) { + free(*str); int bytes = asprintf(str, "0x%" PRIx64, op); if (bytes == -1) { fprintf(stderr, "Could not print bits 0x%" PRIx64 "\n", op); } } -void string_of_sail_bits(sail_string *str, const sail_bits op) +void string_of_lbits(sail_string *str, const lbits op) { + free(*str); if ((op.len % 4) == 0) { - gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits); + gmp_asprintf(str, "0x%*0ZX", op.len / 4, *op.bits); } else { - gmp_asprintf(str, "0b%*0Zb", op.len, *op.bits); + *str = (char *) malloc((op.len + 3) * sizeof(char)); + (*str)[0] = '0'; + (*str)[1] = 'b'; + for (int i = 1; i <= op.len; ++i) { + (*str)[i + 1] = mpz_tstbit(*op.bits, op.len - i) + 0x30; + } + (*str)[op.len + 2] = '\0'; } } -void decimal_string_of_mach_bits(sail_string *str, const mach_bits op) +void decimal_string_of_fbits(sail_string *str, const fbits op) { + free(*str); int bytes = asprintf(str, "%" PRId64, op); if (bytes == -1) { fprintf(stderr, "Could not print bits %" PRId64 "\n", op); } } -void decimal_string_of_sail_bits(sail_string *str, const sail_bits op) +void decimal_string_of_lbits(sail_string *str, const lbits op) { + free(*str); gmp_asprintf(str, "%Z", *op.bits); } void fprint_bits(const sail_string pre, - const sail_bits op, + const lbits op, const sail_string post, FILE *stream) { @@ -1197,13 +1330,13 @@ void fprint_bits(const sail_string pre, fputs(post, stream); } -unit print_bits(const sail_string str, const sail_bits op) +unit print_bits(const sail_string str, const lbits op) { fprint_bits(str, op, "\n", stdout); return UNIT; } -unit prerr_bits(const sail_string str, const sail_bits op) +unit prerr_bits(const sail_string str, const lbits op) { fprint_bits(str, op, "\n", stderr); return UNIT; @@ -4,10 +4,7 @@ #include<stdlib.h> #include<stdio.h> #include<stdbool.h> - -#ifndef USE_INT128 #include<gmp.h> -#endif #include<time.h> @@ -85,14 +82,6 @@ typedef int64_t mach_int; bool EQUAL(mach_int)(const mach_int, const mach_int); -/* - * Integers can be either stack-allocated as 128-bit integers if - * __int128 is available, or use GMP arbitrary precision - * integers. This affects the function signatures, so use a macro to - * paper over the differences. - */ -#ifndef USE_INT128 - typedef mpz_t sail_int; #define SAIL_INT_FUNCTION(fname, rtype, ...) void fname(rtype*, __VA_ARGS__) @@ -110,13 +99,6 @@ 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; -#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__) - -#endif - /* * Comparison operators for integers */ @@ -131,6 +113,7 @@ bool gteq(const sail_int, const sail_int); /* * Left and right shift for integers */ +mach_int shl_mach_int(const mach_int, const mach_int); 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); @@ -169,120 +152,159 @@ SAIL_INT_FUNCTION(pow2, sail_int, const sail_int); /* ***** Sail bitvectors ***** */ -typedef uint64_t mach_bits; +typedef uint64_t fbits; -bool eq_bit(const mach_bits a, const mach_bits b); +bool eq_bit(const fbits a, const fbits b); -bool EQUAL(mach_bits)(const mach_bits, const mach_bits); +bool EQUAL(fbits)(const fbits, const fbits); + +typedef struct { + uint64_t len; + uint64_t bits; +} sbits; typedef struct { mp_bitcnt_t len; mpz_t *bits; -} sail_bits; +} lbits; + +// For backwards compatability +typedef uint64_t mach_bits; +typedef lbits sail_bits; + +SAIL_BUILTIN_TYPE(lbits); + +void CREATE_OF(lbits, fbits)(lbits *, + const fbits op, + const uint64_t len, + const bool direction); + +void RECREATE_OF(lbits, fbits)(lbits *, + const fbits op, + const uint64_t len, + const bool direction); + +void CREATE_OF(lbits, sbits)(lbits *, + const sbits op, + const bool direction); + +void RECREATE_OF(lbits, sbits)(lbits *, + const sbits op, + const bool direction); -SAIL_BUILTIN_TYPE(sail_bits); +sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction); +fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction); +sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction); -void CREATE_OF(sail_bits, mach_bits)(sail_bits *, - const mach_bits op, - const mach_bits len, - const bool direction); +/* Bitvector conversions */ -void RECREATE_OF(sail_bits, mach_bits)(sail_bits *, - const mach_bits op, - const mach_bits len, - const bool direction); +fbits CONVERT_OF(fbits, lbits)(const lbits, const bool); +fbits CONVERT_OF(fbits, sbits)(const sbits, const bool); -mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool); -void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool); +void CONVERT_OF(lbits, fbits)(lbits *, const fbits, const uint64_t, const bool); +void CONVERT_OF(lbits, sbits)(lbits *, const sbits, const bool); -void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit); -mach_bits UNDEFINED(mach_bits)(const unit); +sbits CONVERT_OF(sbits, fbits)(const fbits, const uint64_t, const bool); +sbits CONVERT_OF(sbits, lbits)(const lbits, const bool); + +void UNDEFINED(lbits)(lbits *, const sail_int len, const fbits bit); +fbits UNDEFINED(fbits)(const unit); + +sbits undefined_sbits(void); /* * Wrapper around >> operator to avoid UB when shift amount is greater * than or equal to 64. */ -mach_bits safe_rshift(const mach_bits, const mach_bits); +fbits safe_rshift(const fbits, const fbits); /* * Used internally to construct large bitvector literals. */ -void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk); +void append_64(lbits *rop, const lbits op, const fbits chunk); -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); +void add_bits(lbits *rop, const lbits op1, const lbits op2); +void sub_bits(lbits *rop, const lbits op1, const lbits 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 add_bits_int(lbits *rop, const lbits op1, const mpz_t op2); +void sub_bits_int(lbits *rop, const lbits 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 and_bits(lbits *rop, const lbits op1, const lbits op2); +void or_bits(lbits *rop, const lbits op1, const lbits op2); +void xor_bits(lbits *rop, const lbits op1, const lbits op2); +void not_bits(lbits *rop, const lbits 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 mults_vec(lbits *rop, const lbits op1, const lbits op2); +void mult_vec(lbits *rop, const lbits op1, const lbits op2); -void zeros(sail_bits *rop, const sail_int op); +void zeros(lbits *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 zero_extend(lbits *rop, const lbits op, const sail_int len); +void sign_extend(lbits *rop, const lbits op, const sail_int len); -void length_sail_bits(sail_int *rop, const sail_bits op); +void length_lbits(sail_int *rop, const lbits op); -bool eq_bits(const sail_bits op1, const sail_bits op2); -bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2); -bool neq_bits(const sail_bits op1, const sail_bits op2); +bool eq_bits(const lbits op1, const lbits op2); +bool EQUAL(lbits)(const lbits op1, const lbits op2); +bool neq_bits(const lbits op1, const lbits op2); -void vector_subrange_sail_bits(sail_bits *rop, - const sail_bits op, +void vector_subrange_lbits(lbits *rop, + const lbits op, const sail_int n_mpz, const sail_int m_mpz); -void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len); +void sail_truncate(lbits *rop, const lbits op, const sail_int len); + +fbits bitvector_access(const lbits op, const sail_int n_mpz); -mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz); +void sail_unsigned(sail_int *rop, const lbits op); +void sail_signed(sail_int *rop, const lbits op); -void sail_unsigned(sail_int *rop, const sail_bits op); -void sail_signed(sail_int *rop, const sail_bits op); +mach_int fast_unsigned(const fbits); -void append(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void append(lbits *rop, const lbits op1, const lbits 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 replicate_bits(lbits *rop, const lbits op1, const sail_int op2); +fbits fast_replicate_bits(const fbits shift, const fbits 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 get_slice_int(lbits *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); + const lbits slice); -void vector_update_subrange_sail_bits(sail_bits *rop, - const sail_bits op, +void vector_update_subrange_lbits(lbits *rop, + const lbits op, const sail_int n_mpz, const sail_int m_mpz, - const sail_bits slice); + const lbits slice); -void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz); +void slice(lbits *rop, const lbits op, const sail_int start_mpz, const sail_int len_mpz); -void set_slice(sail_bits *rop, +sbits sslice(const fbits op, const mach_int start, const mach_int len); + +void set_slice(lbits *rop, const sail_int len_mpz, const sail_int slen_mpz, - const sail_bits op, + const lbits op, const sail_int start_mpz, - const sail_bits slice); + const lbits slice); + +void shift_bits_left(lbits *rop, const lbits op1, const lbits op2); +void shift_bits_right(lbits *rop, const lbits op1, const lbits op2); +void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2); -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 shiftl(lbits *rop, const lbits op1, const sail_int op2); +void shiftr(lbits *rop, const lbits op1, const sail_int op2); -void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2); -void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2); +void reverse_endianness(lbits*, lbits); -void reverse_endianness(sail_bits*, sail_bits); +bool eq_sbits(const sbits op1, const sbits op2); +bool neq_sbits(const sbits op1, const sbits op2); +sbits xor_sbits(const sbits op1, const sbits op2); /* ***** Sail reals ***** */ @@ -332,21 +354,21 @@ void string_take(sail_string *dst, sail_string s, sail_int len); /* ***** Printing ***** */ void string_of_int(sail_string *str, const sail_int i); -void string_of_sail_bits(sail_string *str, const sail_bits op); -void string_of_mach_bits(sail_string *str, const mach_bits op); -void decimal_string_of_sail_bits(sail_string *str, const sail_bits op); -void decimal_string_of_mach_bits(sail_string *str, const mach_bits op); +void string_of_lbits(sail_string *str, const lbits op); +void string_of_fbits(sail_string *str, const fbits op); +void decimal_string_of_lbits(sail_string *str, const lbits op); +void decimal_string_of_fbits(sail_string *str, const fbits op); /* * Utility function not callable from Sail! */ void fprint_bits(const sail_string pre, - const sail_bits op, + const lbits op, const sail_string post, FILE *stream); -unit print_bits(const sail_string str, const sail_bits op); -unit prerr_bits(const sail_string str, const sail_bits op); +unit print_bits(const sail_string str, const lbits op); +unit prerr_bits(const sail_string str, const lbits op); unit print(const sail_string str); unit print_endline(const sail_string str); diff --git a/lib/smt.sail b/lib/smt.sail index efcbe48c..c57f7bd1 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -9,7 +9,7 @@ val div = { lem: "integerDiv", c: "tdiv_int", coq: "div_with_eq" -} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)} +} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)} overload operator / = {div} @@ -19,7 +19,7 @@ val mod = { lem: "integerMod", c: "tmod_int", coq: "mod_with_eq" -} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)} +} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)} overload operator % = {mod} @@ -29,7 +29,7 @@ val abs_atom = { lem: "abs_int", c: "abs_int", coq: "abs_with_eq" -} : forall 'n. atom('n) -> {'o, 'o = abs_atom('n). atom('o)} +} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)} $ifdef TEST diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 8abcd218..6953264f 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -5,8 +5,6 @@ $include <flow.sail> type bits ('n : Int) = vector('n, dec, bit) -val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool - val eq_bits = { ocaml: "eq_list", lem: "eq_vec", @@ -63,7 +61,7 @@ val bitvector_access = { lem: "access_vec_dec", coq: "access_vec_dec", c: "vector_access" -} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit +} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit val plain_vector_access = { ocaml: "access", @@ -79,14 +77,14 @@ val bitvector_update = { lem: "update_vec_dec", coq: "update_vec_dec", c: "vector_update" -} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n) +} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n) val plain_vector_update = { ocaml: "update", lem: "update_list_dec", coq: "vec_update_dec", c: "vector_update" -} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) +} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m), 'a) -> vector('n, dec, 'a) overload vector_update = {bitvector_update, plain_vector_update} @@ -119,7 +117,7 @@ val vector_update_subrange = { lem: "update_subrange_vec_dec", c: "vector_update_subrange", coq: "update_subrange_vec_dec" -} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) +} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) // Some ARM specific builtins @@ -135,6 +133,9 @@ val slice = "slice" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm & 0 <= 'n. val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) +/*! +converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$. + */ val unsigned = { ocaml: "uint", lem: "uint", @@ -144,6 +145,9 @@ val unsigned = { } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) /* We need a non-empty vector so that the range makes sense */ +/*! +converts a bit vector of length $n$ to an integer in the range $-2^{n-1}$ to $2^{n-1} - 1$ using twos-complement. + */ val signed = { c: "sail_signed", _: "sint" diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index b295c92c..581dded7 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -61,7 +61,7 @@ val bitvector_access = { lem: "access_vec_inc", coq: "access_vec_inc", c: "vector_access" -} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit +} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit val plain_vector_access = { ocaml: "access", @@ -77,14 +77,14 @@ val bitvector_update = { lem: "update_vec_inc", coq: "update_vec_inc", c: "vector_update" -} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n) +} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n) val plain_vector_update = { ocaml: "update", lem: "update_list_inc", coq: "update_list_inc", c: "vector_update" -} : forall 'n ('a : Type). (vector('n, inc, 'a), int, 'a) -> vector('n, inc, 'a) +} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, inc, 'a), atom('m), 'a) -> vector('n, inc, 'a) overload vector_update = {bitvector_update, plain_vector_update} @@ -113,7 +113,7 @@ val vector_update_subrange = { lem: "update_subrange_vec_inc", c: "vector_update_subrange", coq: "update_subrange_vec_inc" -} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) +} : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) // Some ARM specific builtins |