FStar.BV: expose bvshl, bvshr and bvmod with bit vector rhs

src/parser/FStar.Parser.Const.fst

@@ -216,9 +216,18 @@ let bv_sub_lid         = bvconst "bvsub"
 let bv_shift_left_lid  = bvconst "bvshl"
 let bv_shift_right_lid = bvconst "bvshr"
 let bv_udiv_lid        = bvconst "bvdiv"
-let bv_udiv_unsafe_lid = bvconst "bvdiv_unsafe"
 let bv_mod_lid         = bvconst "bvmod"
 let bv_mul_lid         = bvconst "bvmul"
+// shifts, division and multiplication take natural numbers as their second
+// arguments, which incurs some encoding overhead. The primed versions bvshl',
+// bvshr', bvdiv_unsafe, bvmod_unsafe and bvmul' take a bitvector as the second
+// argument instead, which more closely matches SMT-LIB.
+let bv_shift_left'_lid = bvconst "bvshl'"
+let bv_shift_right'_lid= bvconst "bvshr'"
+let bv_udiv_unsafe_lid = bvconst "bvdiv_unsafe"
+let bv_mod_unsafe_lid  = bvconst "bvmod_unsafe"
+let bv_mul'_lid        = bvconst "bvmul'"
+
 let bv_ult_lid         = bvconst "bvult"
 let bv_uext_lid        = bvconst "bv_uext"
 

src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst

@@ -330,11 +330,15 @@ let is_BitVector_primitive head args =
       || S.fv_eq_lid fv Const.bv_shift_left_lid
       || S.fv_eq_lid fv Const.bv_shift_right_lid
       || S.fv_eq_lid fv Const.bv_udiv_lid
-      || S.fv_eq_lid fv Const.bv_udiv_unsafe_lid
       || S.fv_eq_lid fv Const.bv_mod_lid
+      || S.fv_eq_lid fv Const.bv_mul_lid
+      || S.fv_eq_lid fv Const.bv_shift_left'_lid
+      || S.fv_eq_lid fv Const.bv_shift_right'_lid
+      || S.fv_eq_lid fv Const.bv_udiv_unsafe_lid
+      || S.fv_eq_lid fv Const.bv_mod_unsafe_lid
+      || S.fv_eq_lid fv Const.bv_mul'_lid
       || S.fv_eq_lid fv Const.bv_ult_lid
-      || S.fv_eq_lid fv Const.bv_uext_lid
-      || S.fv_eq_lid fv Const.bv_mul_lid) &&
+      || S.fv_eq_lid fv Const.bv_uext_lid) &&
       (isInteger sz_arg.n)
     | Tm_fvar fv, [(sz_arg, _); _] ->
         (S.fv_eq_lid fv Const.nat_to_bv_lid
@@ -534,6 +538,14 @@ and encode_arith_term env head args_e =
     let bv_udiv = mk_bv (Util.mkBvUdiv sz) binary_arith (Term.boxBitVec sz) in
     let bv_mod  = mk_bv (Util.mkBvMod sz) binary_arith (Term.boxBitVec sz) in
     let bv_mul  = mk_bv (Util.mkBvMul sz) binary_arith (Term.boxBitVec sz) in
+
+    // Binary bv_t -> bv_t -> bv_t variants
+    let bv_shl' = mk_bv (Util.mkBvShl' sz) binary (Term.boxBitVec sz) in
+    let bv_shr' = mk_bv (Util.mkBvShr' sz) binary (Term.boxBitVec sz) in
+    let bv_udiv_unsafe = mk_bv (Util.mkBvUdivUnsafe sz) binary (Term.boxBitVec sz) in
+    let bv_mod_unsafe  = mk_bv (Util.mkBvModUnsafe sz) binary (Term.boxBitVec sz) in
+    let bv_mul' = mk_bv (Util.mkBvMul' sz) binary (Term.boxBitVec sz) in
+
     let bv_ult  = mk_bv Util.mkBvUlt binary Term.boxBool in
     let bv_uext arg_tms =
            mk_bv (Util.mkBvUext (match ext_sz with | Some x -> x | None -> failwith "impossible")) unary
@@ -549,10 +561,13 @@ and encode_arith_term env head args_e =
          (Const.bv_shift_left_lid, bv_shl);
          (Const.bv_shift_right_lid, bv_shr);
          (Const.bv_udiv_lid, bv_udiv);
-         (* NOTE: unsafe 'udiv' also compiles to the same smtlib2 expr *)
-         (Const.bv_udiv_unsafe_lid, bv_udiv);
          (Const.bv_mod_lid, bv_mod);
          (Const.bv_mul_lid, bv_mul);
+         (Const.bv_shift_left'_lid, bv_shl');
+         (Const.bv_shift_right'_lid, bv_shr');
+         (Const.bv_udiv_unsafe_lid, bv_udiv_unsafe);
+         (Const.bv_mod_unsafe_lid, bv_mod_unsafe);
+         (Const.bv_mul'_lid, bv_mul');
          (Const.bv_ult_lid, bv_ult);
          (Const.bv_uext_lid, bv_uext);
          (Const.bv_to_nat_lid, to_int);

src/smtencoding/FStar.SMTEncoding.Term.fst

@@ -322,6 +322,11 @@ let mkBvShr sz (t1, t2) r = mkApp'(BvShr, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvUdiv sz (t1, t2) r = mkApp'(BvUdiv, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvMod sz (t1, t2) r = mkApp'(BvMod, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvMul sz (t1, t2) r = mkApp' (BvMul, [t1;(mkNatToBv sz t2 r)]) r
+let mkBvShl' sz (t1, t2) r = mkApp'(BvShl, [t1;t2]) r
+let mkBvShr' sz (t1, t2) r = mkApp'(BvShr, [t1;t2]) r
+let mkBvMul' sz (t1, t2) r = mkApp' (BvMul, [t1;t2]) r
+let mkBvUdivUnsafe sz (t1, t2) r = mkApp'(BvUdiv, [t1;t2]) r
+let mkBvModUnsafe sz (t1, t2) r = mkApp'(BvMod, [t1;t2]) r
 let mkBvUlt = mk_bin_op BvUlt
 let mkIff = mk_bin_op Iff
 let mkEq (t1, t2) r = match t1.tm, t2.tm with

src/smtencoding/FStar.SMTEncoding.Term.fsti

@@ -248,6 +248,11 @@ val mkBvShr   : (int -> (term * term) -> Range.range -> term)
 val mkBvUdiv  : (int -> (term * term) -> Range.range -> term)
 val mkBvMod   : (int -> (term * term) -> Range.range -> term)
 val mkBvMul   : (int -> (term * term) -> Range.range -> term)
+val mkBvShl'  : (int -> (term * term) -> Range.range -> term)
+val mkBvShr'  : (int -> (term * term) -> Range.range -> term)
+val mkBvUdivUnsafe : (int -> (term * term) -> Range.range -> term)
+val mkBvModUnsafe  : (int -> (term * term) -> Range.range -> term)
+val mkBvMul'  : (int -> (term * term) -> Range.range -> term)
 
 val mkITE: (term * term * term) -> Range.range -> term
 val mkCases : list term -> Range.range -> term

src/smtencoding/FStar.SMTEncoding.Util.fst

@@ -79,6 +79,11 @@ let mkBvShr sz = norng (mkBvShr sz)
 let mkBvUdiv sz = norng (mkBvUdiv sz)
 let mkBvMod sz = norng (mkBvMod sz)
 let mkBvMul sz = norng (mkBvMul sz)
+let mkBvShl' sz = norng (mkBvShl' sz)
+let mkBvShr' sz = norng (mkBvShr' sz)
+let mkBvUdivUnsafe sz = norng (mkBvUdivUnsafe sz)
+let mkBvModUnsafe  sz = norng (mkBvModUnsafe sz)
+let mkBvMul' sz = norng (mkBvMul' sz)
 let mkBvUlt = norng mkBvUlt
 let mkBvUext sz = norng (mkBvUext sz)
 let mkBvToNat = norng mkBvToNat

tests/bug-reports/BvBinaryOps.fst

@@ -0,0 +1,51 @@
+module BvBinaryOps
+
+module BV = FStar.BV
+module BitVector = FStar.BitVector
+
+module Tac = FStar.Tactics
+
+module UInt = FStar.UInt
+
+#set-options "--split_queries always"
+
+(** Tests for bvshl *)
+
+// small integer works ok with bvshl or bvshl'
+let lemma_test_bv8 (bv: BV.bv_t 8) (i: UInt.uint_t 3): unit =
+  let shl = BV.bvshl #8 (BV.int2bv #8 1) i in
+  assert ((BV.bvand #8 (BV.bvor #8 bv shl) shl <> BV.int2bv #8 0 == true))
+
+let lemma_test_bv8' (bv: BV.bv_t 8) (i: UInt.uint_t 3): unit =
+  let i' = BV.bv_uext #3 #5 (BV.int2bv #3 i) in
+  let shl = (BV.bvshl' #8 (BV.int2bv #8 1) i') in
+  assert ((BV.bvand #8 (BV.bvor #8 bv shl) shl <> BV.int2bv #8 0 == true))
+
+// The corresponding 64-bit version doesn't usually prove with bvshl.
+// The uint is converted directly to a 64-bit bv and Z3 doesn't seem to take
+// into account the range of the nat in this conversion.
+
+// let lemma_test_bv64 (bv: BV.bv_t 64) (i: UInt.uint_t 6): unit =
+//   let shl = BV.bvshl #64 (BV.int2bv #64 1) i in
+//   assert ((BV.bvand #64 (BV.bvor #64 bv shl) shl <> BV.int2bv #64 0 == true))
+
+// But if we convert the uint to a 6-bit bv first and then zero-extend it, it's
+// much clearer that the top 58 bits are zeros:
+
+let lemma_test_bv64' (bv: BV.bv_t 64) (i: UInt.uint_t 6): unit =
+  let i' = BV.bv_uext #6 #58 (BV.int2bv #6 i) in
+  let shl = BV.bvshl' #64 (BV.int2bv #64 1) i' in
+  assert ((BV.bvand #64 (BV.bvor #64 bv shl) shl <> BV.int2bv #64 0 == true))
+
+(** Tests for division and mod *)
+
+// This follows from lemma bvdiv_unsafe_sound, but it doesn't have an SMT pattern,
+// so if it succeeds then the encoding is probably correct.
+let lemma_test_bvdiv_unsafe (bv: BV.bv_t 64) (num: UInt.uint_t 8 { num <> 0 }): unit =
+  assert (BV.bvdiv_unsafe #64 bv (BV.int2bv #64 num) == BV.bvdiv #64 bv num)
+
+let lemma_test_bvmod_unsafe (bv: BV.bv_t 64) (num: UInt.uint_t 8 { num <> 0 }): unit =
+  assert (BV.bvmod_unsafe #64 bv (BV.int2bv #64 num) == BV.bvmod #64 bv num)
+
+let lemma_test_bvmul' (bv: BV.bv_t 64) (num: UInt.uint_t 64): unit =
+  assert (BV.bvmul' #64 bv (BV.int2bv #64 num) == BV.bvmul #64 bv num)