SMT-LIB2 parser now models bit-vector division and mod/rem by zero correctly

SMT-LIB2 defines the result of bvsdiv and bvudiv when dividing by zero to be
1...1.  The result of bvurem, bvsrem and bvsmod when dividing by zero is the
value of the first operand.

Author: kroening

regression/smt2_solver/basic-bv1/basic-bv1.smt2

@@ -8,19 +8,24 @@
 (define-fun b03 () Bool (= (bvneg #x07) #xf9)) ; unary minus
 (define-fun b04 () Bool (= (bvmul #x07 #x03) #x15)) ; multiplication
 (define-fun b05 () Bool (= (bvurem #x07 #x03) #x01)) ; unsigned remainder
-(define-fun b06 () Bool (= (bvsrem #x07 #x03) #x01)) ; signed remainder
-(define-fun b07 () Bool (= (bvsmod #x07 #x03) #x01)) ; signed modulo
-(define-fun b08 () Bool (= (bvshl #x07 #x03) #x38)) ; shift left
-(define-fun b09 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right
-(define-fun b10 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a
+(define-fun b06 () Bool (= (bvurem #x07 #x00) #x07)) ; unsigned remainder (div. by zero)
+(define-fun b07 () Bool (= (bvudiv #x01 #x00) #xff)) ; unsigned division (div. by zero)
+(define-fun b08 () Bool (= (bvsrem #x07 #x03) #x01)) ; signed remainder
+(define-fun b09 () Bool (= (bvsrem #x07 #x00) #x07)) ; signed remainder (div. by zero)
+(define-fun b10 () Bool (= (bvsmod #x07 #x03) #x01)) ; signed modulo
+(define-fun b11 () Bool (= (bvsmod #x07 #x00) #x07)) ; signed modulo (div. by zero)
+(define-fun b12 () Bool (= (bvsdiv #x01 #x00) #xff)) ; signed division (div. by zero)
+(define-fun b13 () Bool (= (bvshl #x07 #x03) #x38)) ; shift left
+(define-fun b14 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right
+(define-fun b15 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a
 
 ; Multi-ary variants, where applicable
-(define-fun b11 () Bool (= (bvadd #x07 #x03 #x01) #x0b)) ; addition
-(define-fun b12 () Bool (= (bvmul #x07 #x03 #x01) #x15)) ; multiplication
+(define-fun b16 () Bool (= (bvadd #x07 #x03 #x01) #x0b)) ; addition
+(define-fun b17 () Bool (= (bvmul #x07 #x03 #x01) #x15)) ; multiplication
 
 ; rotation
-(define-fun b13 () Bool (= ((_ rotate_left 2) #xf7) #xdf)) ; rotation left
-(define-fun b14 () Bool (= ((_ rotate_right 2) #x07) #xc1)) ; rotation right
+(define-fun b18 () Bool (= ((_ rotate_left 2) #xf7) #xdf)) ; rotation left
+(define-fun b19 () Bool (= ((_ rotate_right 2) #x07) #xc1)) ; rotation right
 
 ; Bitwise Operations
 
@@ -67,7 +72,7 @@
 ; all must be true
 
 (assert (not (and
-  b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 b11 b12 b13 b14
+  b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19
   d01
   power-test
   p1 p2 p3 p4 p5 p6 p7 p8)))

src/solvers/smt2/smt2_parser.cpp

@@ -872,6 +872,64 @@ exprt smt2_parsert::function_application()
   UNREACHABLE;
 }
 
+exprt smt2_parsert::bv_division(
+  const exprt::operandst &operands,
+  bool is_signed)
+{
+  if(operands.size() != 2)
+    throw error() << "bitvector division expects two operands";
+
+  // SMT-LIB2 defines the result of division by 0 to be 1....1
+  auto divisor = symbol_exprt("divisor", operands[1].type());
+  auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
+  auto all_ones = to_unsignedbv_type(operands[0].type()).largest_expr();
+
+  exprt division_result;
+
+  if(is_signed)
+  {
+    auto signed_operands = cast_bv_to_signed({operands[0], divisor});
+    division_result =
+      cast_bv_to_unsigned(div_exprt(signed_operands[0], signed_operands[1]));
+  }
+  else
+    division_result = div_exprt(operands[0], divisor);
+
+  return let_exprt(
+    {divisor},
+    {operands[1]},
+    if_exprt(divisor_is_zero, all_ones, division_result));
+}
+
+exprt smt2_parsert::bv_mod(const exprt::operandst &operands, bool is_signed)
+{
+  if(operands.size() != 2)
+    throw error() << "bitvector modulo expects two operands";
+
+  // SMT-LIB2 defines the result of "lhs modulo 0" to be "lhs"
+  auto dividend = symbol_exprt("dividend", operands[0].type());
+  auto divisor = symbol_exprt("divisor", operands[1].type());
+  auto divisor_is_zero = equal_exprt(divisor, from_integer(0, divisor.type()));
+
+  exprt mod_result;
+
+  // bvurem and bvsrem match our mod_exprt.
+  // bvsmod doesn't.
+  if(is_signed)
+  {
+    auto signed_operands = cast_bv_to_signed({dividend, divisor});
+    mod_result =
+      cast_bv_to_unsigned(mod_exprt(signed_operands[0], signed_operands[1]));
+  }
+  else
+    mod_result = mod_exprt(dividend, divisor);
+
+  return let_exprt(
+    {dividend, divisor},
+    {operands[0], operands[1]},
+    if_exprt(divisor_is_zero, dividend, mod_result));
+}
+
 exprt smt2_parsert::expression()
 {
   switch(next_token())
@@ -1045,27 +1103,17 @@ void smt2_parsert::setup_expressions()
       return binary(ID_minus, op);
   };
 
-  expressions["bvsdiv"] = [this] {
-    return cast_bv_to_unsigned(binary(ID_div, cast_bv_to_signed(operands())));
-  };
-
-  expressions["bvudiv"] = [this] { return binary(ID_div, operands()); };
+  expressions["bvsdiv"] = [this] { return bv_division(operands(), true); };
+  expressions["bvudiv"] = [this] { return bv_division(operands(), false); };
   expressions["/"] = [this] { return binary(ID_div, operands()); };
   expressions["div"] = [this] { return binary(ID_div, operands()); };
 
-  expressions["bvsrem"] = [this] {
-    // 2's complement signed remainder (sign follows dividend)
-    // This matches our ID_mod, and what C does since C99.
-    return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(operands())));
-  };
-
-  expressions["bvsmod"] = [this] {
-    // 2's complement signed remainder (sign follows divisor)
-    // We don't have that.
-    return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(operands())));
-  };
+  expressions["bvsrem"] = [this] { return bv_mod(operands(), true); };
+  expressions["bvurem"] = [this] { return bv_mod(operands(), false); };
 
-  expressions["bvurem"] = [this] { return binary(ID_mod, operands()); };
+  // 2's complement signed remainder (sign follows divisor)
+  // We don't have that.
+  expressions["bvsmod"] = [this] { return bv_mod(operands(), true); };
 
   expressions["%"] = [this] { return binary(ID_mod, operands()); };
 

src/solvers/smt2/smt2_parser.h

@@ -162,6 +162,8 @@ class smt2_parsert
   exprt binary_predicate(irep_idt, const exprt::operandst &);
   exprt binary(irep_idt, const exprt::operandst &);
   exprt unary(irep_idt, const exprt::operandst &);
+  exprt bv_division(const exprt::operandst &, bool is_signed);
+  exprt bv_mod(const exprt::operandst &, bool is_signed);
 
   exprt let_expression();
   exprt quantifier_expression(irep_idt);