diff options
| -rw-r--r-- | lib/rts.c | 7 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 5 | ||||
| -rw-r--r-- | test/smt/clear_overflow_regression.unsat.sail | 64 |
3 files changed, 71 insertions, 5 deletions
@@ -94,9 +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); - //} + /* if ((byte >= 97 && byte <= 122) || (byte >= 64 && byte <= 90) || (byte >= 48 && byte <= 57) || byte == 10 || byte == 32) { + fprintf(stderr, "%" PRIx64 "\n", address); + fprintf(stderr, "%c", (char) byte); + } */ struct block *current = sail_memory; diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 44f32f4b..d48ecd9a 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -56,7 +56,7 @@ open Jib_util open Smtlib module IntMap = Map.Make(struct type t = int let compare = compare end) - + let zencode_upper_id id = Util.zencode_upper_string (string_of_id id) let zencode_id id = Util.zencode_string (string_of_id id) let zencode_name id = string_of_name ~deref_current_exception:false ~zencode:true id @@ -1481,8 +1481,9 @@ let smt_cdef props lets name_file ctx all_cdefs = function smt_header ctx stack all_cdefs; + Stack.clear overflow_checks; let ctx = { ctx with pragma_l = pragma_l; arg_stack = Stack.create () } in - + (* When we create each argument declaration, give it a unique location from the $property pragma, so we can identify it later. *) let arg_decls = diff --git a/test/smt/clear_overflow_regression.unsat.sail b/test/smt/clear_overflow_regression.unsat.sail new file mode 100644 index 00000000..b10d7531 --- /dev/null +++ b/test/smt/clear_overflow_regression.unsat.sail @@ -0,0 +1,64 @@ +$include <arith.sail> +$include <vector_dec.sail> + +default Order dec + +infix 1 >> +infix 1 << +overload operator - = {sub_bits} +overload operator >> = {sail_shiftright} +overload operator << = {sail_shiftleft} + +infix 4 <+ +infix 4 >+ +infix 4 <=+ +infix 4 >=+ +val operator <+ : forall 'n. (bits('n), bits('n)) -> bool +val operator >+ : forall 'n. (bits('n), bits('n)) -> bool +val operator <=+ : forall 'n. (bits('n), bits('n)) -> bool +val operator >=+ : forall 'n. (bits('n), bits('n)) -> bool +function operator <+ (x, y) = unsigned(x) < unsigned(y) +function operator >+ (x, y) = unsigned(x) > unsigned(y) +function operator <=+ (x, y) = unsigned(x) <= unsigned(y) +function operator >=+ (x, y) = unsigned(x) >= unsigned(y) + +val full_bounds : (int, bits(32), bits(3)) -> bits(32) + +function full_bounds(E, a, r_tip) = { + let a_top : bits(32) = a >> (E + 9); + let a_tip : bits(3) = truncate(a >> (E + 6), 3); + let r_mid : bits(9) = sail_zero_extend(r_tip, 9) << 6; + let adjust : bits(32) = if (a_tip <+ r_tip) then 0xFFFFFFFF else 0x00000000; + let r_bot : bits(32) = sail_zero_extend(r_mid, 32) << E; + ((a_top + adjust) << (E + 9)) + r_bot +} + +val inside_rep_bounds : (int, bits(32), bits(3), bits(32)) -> bool + +function inside_rep_bounds(E, a, r_tip, i) = { + let a_mid : bits(9) = truncate(a >> E, 9); + let i_mid : bits(9) = truncate(i >> E, 9); + let r_mid : bits(9) = sail_zero_extend(r_tip, 9) << 6; + let s : bits(35) = sail_zero_extend(0b1, 35) << (E + 9); + let in_limits : bool = if (0 <= signed(i)) then i_mid <+ (r_mid - a_mid - 0b000000001) else (i_mid >=+ (r_mid - a_mid) & r_mid != a_mid); + E >= 23 | (abs_int(signed(i)) < unsigned(s) & in_limits) +} + +$property +function prop_safe(E : int, a : bits(32), r : bits(3), i : bits(32)) -> bool = { + if 0 <= E & E < 26 then { + let r_b = full_bounds(E, a, r); + let p = a + i; + if inside_rep_bounds(E, a, r, i) then (sail_zero_extend(p-r_b, 35) <+ (sail_zero_extend(0b1, 35) << (E + 9))) else true; + } else true; +} + +$property +function prop(E : int, a : bits(32), r : bits(3), i : bits(32)) -> bool = { + if 0 <= E then { + let r_b = full_bounds(E, a, r); + let p = a + i; + let diff = (p >> E) - (r_b >> E); + if (unsigned(diff) >= 1 & unsigned(diff) <= 510) then inside_rep_bounds(E, a, r, i) else true; + } else true; +} |