SMT-LIB2 parser now models bit-vector division by zero correctly

SMT-LIB2 defines the result of bvsdiv and bvudiv to be 1...1.

Author: kroening

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

@@ -8,19 +8,21 @@
 (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 (= (bvudiv #x01 #x00) #xff)) ; unsigned division
+(define-fun b07 () Bool (= (bvsrem #x07 #x03) #x01)) ; signed remainder
+(define-fun b08 () Bool (= (bvsmod #x07 #x03) #x01)) ; signed modulo
+(define-fun b09 () Bool (= (bvsdiv #x01 #x00) #xff)) ; signed division
+(define-fun b10 () Bool (= (bvshl #x07 #x03) #x38)) ; shift left
+(define-fun b11 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right
+(define-fun b12 () 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 b13 () Bool (= (bvadd #x07 #x03 #x01) #x0b)) ; addition
+(define-fun b14 () 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 b15 () Bool (= ((_ rotate_left 2) #xf7) #xdf)) ; rotation left
+(define-fun b16 () Bool (= ((_ rotate_right 2) #x07) #xc1)) ; rotation right
 
 ; Bitwise Operations
 
@@ -67,7 +69,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
   d01
   power-test
   p1 p2 p3 p4 p5 p6 p7 p8)))

src/solvers/smt2/smt2_parser.cpp

@@ -872,6 +872,35 @@ 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::expression()
 {
   switch(next_token())
@@ -1045,11 +1074,8 @@ 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()); };
 

src/solvers/smt2/smt2_parser.h

@@ -162,6 +162,7 @@ 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 let_expression();
   exprt quantifier_expression(irep_idt);