From 43b2ccd22458bf56a2a39091e0f9936ba8f47c9c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 25 Jun 2021 15:46:28 +0100 Subject: [PATCH] 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. --- .../smt2_solver/basic-bv1/basic-bv1.smt2 | 25 +++--- src/solvers/smt2/smt2_parser.cpp | 82 +++++++++++++++---- src/solvers/smt2/smt2_parser.h | 2 + 3 files changed, 82 insertions(+), 27 deletions(-) diff --git a/regression/smt2_solver/basic-bv1/basic-bv1.smt2 b/regression/smt2_solver/basic-bv1/basic-bv1.smt2 index f8337be0406..e5fe2668bb0 100644 --- a/regression/smt2_solver/basic-bv1/basic-bv1.smt2 +++ b/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))) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index cee001d1388..d58eb66753d 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/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()); }; diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 490f7af48f0..8cce34c5334 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/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);