diff options
| -rw-r--r-- | src/jib/jib_smt.ml | 28 | ||||
| -rw-r--r-- | test/smt/sail_mask.unsat.sail | 10 | ||||
| -rw-r--r-- | test/smt/sail_mask_2.unsat.sail | 10 |
3 files changed, 41 insertions, 7 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index c1a7191c..be4badf0 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -384,7 +384,7 @@ let builtin_gteq = builtin_int_comparison "bvsge" Big_int.greater_equal (* ***** Arithmetic operations: lib/arith.sail ***** *) -(** [force_size n m exp] takes a smt expression assumed to be a +(** [force_size ctx n m exp] takes a smt expression assumed to be a integer (signed bitvector) of length m and forces it to be length n by either sign extending it or truncating it as required *) let force_size ?checked:(checked=true) ctx n m smt = @@ -404,6 +404,16 @@ let force_size ?checked:(checked=true) ctx n m smt = if checked then overflow_check ctx check else (); Extract (n - 1, 0, smt) +(** [unsigned_size ctx n m exp] is much like force_size, but it + assumes that the bitvector is unsigned *) +let unsigned_size ?checked:(checked=true) ctx n m smt = + if n = m then + smt + else if n > m then + Fn ("concat", [bvzero (n - m); smt]) + else + failwith "bad arguments to unsigned_size" + let int_size ctx = function | CT_constant n -> required_width n | CT_fint sz -> sz @@ -542,7 +552,7 @@ let builtin_ones ctx cval = function Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; bvones (lbits_size ctx)])]); | ret_ctyp -> builtin_type_error ctx "ones" [cval] (Some ret_ctyp) -(* [bvzeint esz cval] (BitVector Zero Extend INTeger), takes a cval +(* [bvzeint ctx esz cval] (BitVector Zero Extend INTeger), takes a cval which must be an integer type (either CT_fint, or CT_lint), and produces a bitvector which is either zero extended or truncated to exactly esz bits. *) @@ -801,11 +811,10 @@ let builtin_replicate_bits ctx v1 v2 ret_ctyp = let smt = smt_cval ctx v1 in Fn ("concat", List.init (Big_int.to_int c) (fun _ -> smt)) - (*| CT_fbits (n, _), ctyp2, CT_lbits _ -> - let len = Fn ("bvmul", [bvint ctx.lbits_index (Big_int.of_int n); - Extract (ctx.lbits_index - 1, 0, smt_cval ctx v2)]) - in - assert false*) + | CT_fbits (n, _), _, CT_fbits (m, _) -> + let smt = smt_cval ctx v1 in + let c = m / n in + Fn ("concat", List.init c (fun _ -> smt)) | _ -> builtin_type_error ctx "replicate_bits" [v1; v2] (Some ret_ctyp) @@ -819,6 +828,11 @@ let builtin_sail_truncate ctx v1 v2 ret_ctyp = assert (Big_int.to_int c = m && m < lbits_size ctx); Extract (Big_int.to_int c - 1, 0, Fn ("contents", [smt_cval ctx v1])) + | CT_fbits (n, _), _, CT_lbits _ -> + let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in + let smt2 = bvzeint ctx ctx.lbits_index v2 in + Fn ("Bits", [smt2; Fn ("bvand", [bvmask ctx smt2; smt1])]) + | _ -> builtin_type_error ctx "sail_truncate" [v1; v2] (Some ret_ctyp) let builtin_sail_truncateLSB ctx v1 v2 ret_ctyp = diff --git a/test/smt/sail_mask.unsat.sail b/test/smt/sail_mask.unsat.sail new file mode 100644 index 00000000..4afbab90 --- /dev/null +++ b/test/smt/sail_mask.unsat.sail @@ -0,0 +1,10 @@ +default Order dec + +$include <prelude.sail> + +$property +function prop forall 'n, 0 <= 'n <= 128. (n: int('n)) -> bool = { + let x = sail_mask(n, 0b0); + assert(x == sail_zeros(n)); + true +} diff --git a/test/smt/sail_mask_2.unsat.sail b/test/smt/sail_mask_2.unsat.sail new file mode 100644 index 00000000..8904bbe9 --- /dev/null +++ b/test/smt/sail_mask_2.unsat.sail @@ -0,0 +1,10 @@ +default Order dec + +$include <prelude.sail> + +$property +function prop forall 'n, 1 <= 'n <= 128. (n: int('n)) -> bool = { + let x = sail_mask(n, 0b1); + assert(x == sail_zero_extend(0b1, n)); + true +} |