diff options
| -rw-r--r-- | src/jib/jib_smt.ml | 9 | ||||
| -rw-r--r-- | test/smt/zeros_ones.unsat.sail | 13 |
2 files changed, 21 insertions, 1 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 4b868050..da0048d7 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -418,7 +418,7 @@ let unsigned_size ?checked:(checked=true) ctx n m smt = else if n > m then Fn ("concat", [bvzero (n - m); smt]) else - failwith "bad arguments to unsigned_size" + Extract (n - 1, 0, smt) let int_size ctx = function | CT_constant n -> required_width n @@ -715,6 +715,13 @@ let builtin_append ctx v1 v2 ret_ctyp = let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in Fn ("Bits", [bvadd (Fn ("len", [smt1])) (Fn ("len", [smt2])); bvor (bvshl x shift) (Fn ("contents", [smt2]))]) + | CT_lbits _, CT_lbits _, CT_fbits (n, _) -> + let smt1 = smt_cval ctx v1 in + let smt2 = smt_cval ctx v2 in + let x = Fn ("contents", [smt1]) in + let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in + unsigned_size ctx n (lbits_size ctx) (bvor (bvshl x shift) (Fn ("contents", [smt2]))) + | _ -> builtin_type_error ctx "append" [v1; v2] (Some ret_ctyp) let builtin_length ctx v ret_ctyp = diff --git a/test/smt/zeros_ones.unsat.sail b/test/smt/zeros_ones.unsat.sail new file mode 100644 index 00000000..0ebfba42 --- /dev/null +++ b/test/smt/zeros_ones.unsat.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +$property +function prop(x: range(0, 64)) -> bool = { + let bv: bits(64) = sail_zeros(64 - x) @ sail_ones(x); + if x == 32 then { + bv == 0x0000_0000_FFFF_FFFF + } else { + true + } +} |