Add bitvector overflow predicate operators (#417)

Author: filipeom

src/smtml/bitwuzla_mappings.default.ml

@@ -296,6 +296,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let lshr t1 t2 = mk_term2 Kind.Bv_shr t1 t2
 
+    let smod t1 t2 = mk_term2 Kind.Bv_smod t1 t2
+
     let rem t1 t2 = mk_term2 Kind.Bv_srem t1 t2
 
     let rem_u t1 t2 = mk_term2 Kind.Bv_urem t1 t2
@@ -304,6 +306,19 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let rotate_right t1 t2 = mk_term2 Kind.Bv_ror t1 t2
 
+    let nego t = mk_term1 Kind.Bv_nego t
+
+    let addo ~signed t1 t2 =
+      mk_term2 (if signed then Kind.Bv_saddo else Kind.Bv_uaddo) t1 t2
+
+    let subo ~signed t1 t2 =
+      mk_term2 (if signed then Kind.Bv_ssubo else Kind.Bv_usubo) t1 t2
+
+    let mulo ~signed t1 t2 =
+      mk_term2 (if signed then Kind.Bv_smulo else Kind.Bv_umulo) t1 t2
+
+    let divo t1 t2 = mk_term2 Kind.Bv_sdivo t1 t2
+
     let lt t1 t2 = mk_term2 Kind.Bv_slt t1 t2
 
     let lt_u t1 t2 = mk_term2 Kind.Bv_ult t1 t2

src/smtml/cvc5_mappings.default.ml

@@ -280,6 +280,8 @@ module Fresh_cvc5 () = struct
 
     let lshr t1 t2 = Term.mk_term tm Kind.Bitvector_lshr [| t1; t2 |]
 
+    let smod _ = Fmt.failwith "Cvc5_mappings: smod not implemented"
+
     let rem t1 t2 = Term.mk_term tm Kind.Bitvector_srem [| t1; t2 |]
 
     let rem_u t1 t2 = Term.mk_term tm Kind.Bitvector_urem [| t1; t2 |]
@@ -290,6 +292,16 @@ module Fresh_cvc5 () = struct
     let rotate_right t1 t2 =
       Term.mk_term tm Kind.Bitvector_rotate_right [| t1; t2 |]
 
+    let nego _ = Fmt.failwith "Cvc5_mappings: nego not implemented"
+
+    let addo ~signed:_ = Fmt.failwith "Cvc5_mappings: addo not implemented"
+
+    let subo ~signed:_ = Fmt.failwith "Cvc5_mappings: subo not implemented"
+
+    let mulo ~signed:_ = Fmt.failwith "Cvc5_mappings: mulo not implemented"
+
+    let divo _ = Fmt.failwith "Cvc5_mappings: divo not support not implemented"
+
     let lt t1 t2 = Term.mk_term tm Kind.Bitvector_slt [| t1; t2 |]
 
     let lt_u t1 t2 = Term.mk_term tm Kind.Bitvector_ult [| t1; t2 |]

src/smtml/dolmenexpr_to_expr.ml

@@ -335,17 +335,27 @@ module DolmenIntf = struct
 
     let rotate_right t1 t2 = DTerm.Bitv.rotate_right (int_of_term t2) t1
 
-    let lt t1 t2 = DTerm.Bitv.slt t1 t2
+    let nego _ = Fmt.failwith "Dolmenexpr: nego not implemented"
 
-    let lt_u t1 t2 = DTerm.Bitv.ult t1 t2
+    let addo ~signed:_ = Fmt.failwith "Dolmenexpr: addo not implemented"
+
+    let subo ~signed:_ = Fmt.failwith "Dolmenexpr: subo not implemented"
+
+    let mulo ~signed:_ = Fmt.failwith "Dolmenexpr: mulo not implemented"
+
+    let divo _ = Fmt.failwith "Dolmenexpr: divo not implemented"
+
+    let lt = DTerm.Bitv.slt
+
+    let lt_u = DTerm.Bitv.ult
 
     let le = DTerm.Bitv.sle
 
     let le_u = DTerm.Bitv.ule
 
-    let gt t1 t2 = DTerm.Bitv.sgt t1 t2
+    let gt = DTerm.Bitv.sgt
 
-    let gt_u t1 t2 = DTerm.Bitv.ugt t1 t2
+    let gt_u = DTerm.Bitv.ugt
 
     let ge = DTerm.Bitv.sge
 

src/smtml/dolmenexpr_to_expr.mli

@@ -277,6 +277,8 @@ module DolmenIntf : sig
 
     val lshr : term -> term -> term
 
+    val smod : term -> term -> term
+
     val rem : term -> term -> term
 
     val rem_u : term -> term -> term
@@ -285,6 +287,16 @@ module DolmenIntf : sig
 
     val rotate_right : term -> term -> term
 
+    val nego : term -> term
+
+    val addo : signed:bool -> term -> term -> term
+
+    val subo : signed:bool -> term -> term -> term
+
+    val mulo : signed:bool -> term -> term -> term
+
+    val divo : term -> term -> term
+
     val lt : term -> term -> term
 
     val lt_u : term -> term -> term

src/smtml/mappings.nop.ml

@@ -253,6 +253,8 @@ module Nop = struct
 
       let lshr _ = assert false
 
+      let smod _ = assert false
+
       let rem _ = assert false
 
       let rem_u _ = assert false
@@ -261,6 +263,16 @@ module Nop = struct
 
       let rotate_right _ = assert false
 
+      let nego _ = assert false
+
+      let addo ~signed:_ = assert false
+
+      let subo ~signed:_ = assert false
+
+      let mulo ~signed:_ = assert false
+
+      let divo _ = assert false
+
       let lt _ = assert false
 
       let lt_u _ = assert false

src/smtml/mappings_intf.ml

@@ -446,6 +446,10 @@ module type M = sig
     (** [lshr t1 t2] constructs the logical right shift of [t1] by [t2]. *)
     val lshr : term -> term -> term
 
+    (** [smod t1 t2] two's complement signed remainder (sign follows divisor).
+    *)
+    val smod : term -> term -> term
+
     (** [rem t1 t2] constructs the remainder of the bitvector terms [t1] and
         [t2]. *)
     val rem : term -> term -> term
@@ -460,6 +464,38 @@ module type M = sig
     (** [rotate_right t1 t2] constructs the right rotation of [t1] by [t2]. *)
     val rotate_right : term -> term -> term
 
+    (** [nego t] constructs a predicate that checks that whether the bit-wise
+        negation of [t] does not overflow. *)
+    val nego : term -> term
+
+    (** [addo ~signed t1 t2] constructs a predicate that checks whether the
+        bitwise addition of [t1] and [t2] does not overflow.
+
+        The [signed] argument is a boolean:
+        - [true] -> for signed addition
+        - [false] -> for unsigned addition *)
+    val addo : signed:bool -> term -> term -> term
+
+    (** [subo ~signed t1 t2] constructs a predicate that checks whether the
+        bitwise subtraction of [t1] and [t2] does not overflow.
+
+        The [signed] argument is a boolean:
+        - [true] -> for signed subtraction
+        - [false] -> for unsigned subtraction *)
+    val subo : signed:bool -> term -> term -> term
+
+    (** [mulo ~signed t1 t2] constructs a predicate that checks whether the
+        bitwise multiplication of [t1] and [t2] does not overflow.
+
+        The [signed] argument is a boolean:
+        - [true] -> for signed multiplication
+        - [false] -> for unsigned multiplication *)
+    val mulo : signed:bool -> term -> term -> term
+
+    (** [divo t1 t2] constructs a predicate that checks whether the bitwise
+        division of [t1] and [t2] does not overflow. *)
+    val divo : term -> term -> term
+
     (** [lt t1 t2] constructs the less-than relation between bitvector terms
         [t1] and [t2]. *)
     val lt : term -> term -> term

src/smtml/z3_mappings.default.ml

@@ -322,6 +322,8 @@ module M = struct
 
       let lshr e1 e2 = Z3.BitVector.mk_lshr ctx e1 e2
 
+      let smod e1 e2 = Z3.BitVector.mk_smod ctx e1 e2
+
       let rem e1 e2 = Z3.BitVector.mk_srem ctx e1 e2
 
       let rem_u e1 e2 = Z3.BitVector.mk_urem ctx e1 e2
@@ -330,6 +332,16 @@ module M = struct
 
       let rotate_right e1 e2 = Z3.BitVector.mk_ext_rotate_right ctx e1 e2
 
+      let nego e = Z3.BitVector.mk_neg_no_overflow ctx e
+
+      let addo ~signed e1 e2 = Z3.BitVector.mk_add_no_overflow ctx e1 e2 signed
+
+      let subo ~signed:_ e1 e2 = Z3.BitVector.mk_sub_no_overflow ctx e1 e2
+
+      let mulo ~signed e1 e2 = Z3.BitVector.mk_mul_no_overflow ctx e1 e2 signed
+
+      let divo e1 e2 = Z3.BitVector.mk_sdiv_no_overflow ctx e1 e2
+
       let lt e1 e2 = Z3.BitVector.mk_slt ctx e1 e2
 
       let lt_u e1 e2 = Z3.BitVector.mk_ult ctx e1 e2