diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 80b3fef02..c9f9d6fbd 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -755,11 +755,12 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall) auto y = expr(*args.at(1)); auto k = expr(*args.at(2)); m_context.addAssertion(k != 0); + auto const& intType = dynamic_cast(*_funCall.annotation().type); if (kind == FunctionType::Kind::AddMod) - defineExpr(_funCall, (x + y) % k); + defineExpr(_funCall, divModWithSlacks(x + y, k, intType).second); else - defineExpr(_funCall, (x * y) % k); + defineExpr(_funCall, divModWithSlacks(x * y, k, intType).second); } void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall) @@ -1490,8 +1491,8 @@ pair SMTEncoder::arithmeticOperation( case Token::Add: return _left + _right; case Token::Sub: return _left - _right; case Token::Mul: return _left * _right; - case Token::Div: return division(_left, _right, *intType); - case Token::Mod: return _left % _right; + case Token::Div: return divModWithSlacks(_left, _right, *intType).first; + case Token::Mod: return divModWithSlacks(_left, _right, *intType).second; default: solAssert(false, ""); } }(); @@ -1693,13 +1694,30 @@ void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op) defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned)); } -smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type) +pair SMTEncoder::divModWithSlacks( + smtutil::Expression _left, + smtutil::Expression _right, + IntegerType const& _type +) { - // Signed division in SMTLIB2 rounds differently for negative division. + IntegerType const* intType = &_type; + string suffix = "div_mod_" + to_string(m_context.newUniqueId()); + smt::SymbolicIntVariable d(intType, intType, "d_" + suffix, m_context); + smt::SymbolicIntVariable r(intType, intType, "r_" + suffix, m_context); + + // x / y = d and x % y = r iff d * y + r = x and + // either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned) + // or x < 0 and -abs(y) < r <= 0 + m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left); if (_type.isSigned()) - return signedDivisionEVM(_left, _right); - else - return _left / _right; + m_context.addAssertion( + (_left >= 0 && 0 <= r.currentValue() && r.currentValue() < smtutil::abs(_right)) || + (_left < 0 && (0 - smtutil::abs(_right)) < r.currentValue() && r.currentValue() <= 0) + ); + else // unsigned version + m_context.addAssertion(0 <= r.currentValue() && r.currentValue() < _right); + + return {d.currentValue(), r.currentValue()}; } void SMTEncoder::assignment( diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index c39042fbb..2936368a3 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -36,6 +36,7 @@ #include #include #include +#include namespace solidity::langutil { @@ -174,9 +175,14 @@ protected: std::vector const& _elementValues ); - /// Division expression in the given type. Requires special treatment because - /// of rounding for signed division. - smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type); + /// @returns a pair of expressions representing _left / _right and _left mod _right, respectively. + /// Uses slack variables and additional constraints to express the results using only operations + /// more friendly to the SMT solver (multiplication, addition, subtraction and comparison). + std::pair divModWithSlacks( + smtutil::Expression _left, + smtutil::Expression _right, + IntegerType const& _type + ); void assignment(VariableDeclaration const& _variable, Expression const& _value); /// Handles assignments to variables of different types. diff --git a/scripts/error_codes.py b/scripts/error_codes.py index 2f7c0619a..100c0c0be 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -220,7 +220,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): return False old_source_only_ids = { - "1123", "1133", "1220", "1584", "1823", "1950", + "1123", "1133", "1218", "1220", "1584", "1823", "1950", "1988", "2418", "2461", "2512", "2592", "2657", "2800", "2842", "2856", "3263", "3356", "3441", "3682", "3876", "3893", "4010", "4281", "4802", "4805", "4828", diff --git a/test/libsolidity/smtCheckerTests/math/addmod_1.sol b/test/libsolidity/smtCheckerTests/math/addmod_1.sol index 67a6afc2f..a4ebed099 100644 --- a/test/libsolidity/smtCheckerTests/math/addmod_1.sol +++ b/test/libsolidity/smtCheckerTests/math/addmod_1.sol @@ -12,10 +12,5 @@ contract C { } } // ---- -// Warning 1218: (83-108): CHC: Error trying to invoke SMT solver. -// Warning 1218: (141-166): CHC: Error trying to invoke SMT solver. -// Warning 1218: (76-114): CHC: Error trying to invoke SMT solver. -// Warning 1218: (170-184): CHC: Error trying to invoke SMT solver. -// Warning 1218: (263-278): CHC: Error trying to invoke SMT solver. // Warning 3046: (141-166): BMC: Division by zero happens here. // Warning 3046: (263-278): BMC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/math/addmod_mulmod.sol b/test/libsolidity/smtCheckerTests/math/addmod_mulmod.sol index 61016ddf0..233f5e293 100644 --- a/test/libsolidity/smtCheckerTests/math/addmod_mulmod.sol +++ b/test/libsolidity/smtCheckerTests/math/addmod_mulmod.sol @@ -9,8 +9,5 @@ contract C { } } // ---- -// Warning 1218: (118-143): CHC: Error trying to invoke SMT solver. -// Warning 1218: (183-208): CHC: Error trying to invoke SMT solver. -// Warning 1218: (219-233): CHC: Error trying to invoke SMT solver. // Warning 6838: (93-143): BMC: Condition is always false. // Warning 6838: (158-208): BMC: Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol index 7c8b7ac10..84c6e4698 100644 --- a/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol +++ b/test/libsolidity/smtCheckerTests/math/addmod_mulmod_zero.sol @@ -22,15 +22,5 @@ contract C { } // ---- // Warning 6321: (253-260): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 1218: (94-109): CHC: Error trying to invoke SMT solver. -// Warning 1218: (113-126): CHC: Error trying to invoke SMT solver. -// Warning 1218: (180-195): CHC: Error trying to invoke SMT solver. -// Warning 1218: (199-212): CHC: Error trying to invoke SMT solver. -// Warning 1218: (275-290): CHC: Error trying to invoke SMT solver. -// Warning 1218: (303-318): CHC: Error trying to invoke SMT solver. -// Warning 1218: (349-364): CHC: Error trying to invoke SMT solver. -// Warning 1218: (377-392): CHC: Error trying to invoke SMT solver. -// Warning 1218: (322-336): CHC: Error trying to invoke SMT solver. -// Warning 1218: (396-410): CHC: Error trying to invoke SMT solver. // Warning 3046: (94-109): BMC: Division by zero happens here. // Warning 3046: (180-195): BMC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/math/addmulmod.sol b/test/libsolidity/smtCheckerTests/math/addmulmod.sol index e19b4d5e5..6ff977831 100644 --- a/test/libsolidity/smtCheckerTests/math/addmulmod.sol +++ b/test/libsolidity/smtCheckerTests/math/addmulmod.sol @@ -17,8 +17,3 @@ contract C { } } // ---- -// Warning 1218: (158-174): CHC: Error trying to invoke SMT solver. -// Warning 1218: (178-192): CHC: Error trying to invoke SMT solver. -// Warning 1218: (309-325): CHC: Error trying to invoke SMT solver. -// Warning 1218: (329-343): CHC: Error trying to invoke SMT solver. -// Warning 7812: (329-343): BMC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol index e5d9d9360..d75e6d267 100644 --- a/test/libsolidity/smtCheckerTests/math/mulmod_1.sol +++ b/test/libsolidity/smtCheckerTests/math/mulmod_1.sol @@ -12,10 +12,5 @@ contract C { } } // ---- -// Warning 1218: (83-108): CHC: Error trying to invoke SMT solver. -// Warning 1218: (141-166): CHC: Error trying to invoke SMT solver. -// Warning 1218: (76-114): CHC: Error trying to invoke SMT solver. -// Warning 1218: (170-184): CHC: Error trying to invoke SMT solver. -// Warning 1218: (263-278): CHC: Error trying to invoke SMT solver. // Warning 3046: (141-166): BMC: Division by zero happens here. // Warning 3046: (263-278): BMC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol index d5b3b7176..cdb2db7e1 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol @@ -9,6 +9,4 @@ contract C { } } // ---- -// Warning 1218: (129-143): CHC: Error trying to invoke SMT solver. -// Warning 1218: (147-161): CHC: Error trying to invoke SMT solver. -// Warning 4661: (147-161): BMC: Assertion violation happens here. +// Warning 6328: (147-161): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol index 87e0ba152..8bb0f2edb 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol @@ -10,6 +10,4 @@ contract C { } } // ---- -// Warning 1218: (163-184): CHC: Error trying to invoke SMT solver. -// Warning 1218: (188-209): CHC: Error trying to invoke SMT solver. -// Warning 4661: (188-209): BMC: Assertion violation happens here. +// Warning 6328: (188-209): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol index cffb2b5a1..2b25ee54e 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol @@ -10,6 +10,4 @@ contract C { } } // ---- -// Warning 1218: (171-190): CHC: Error trying to invoke SMT solver. -// Warning 1218: (194-213): CHC: Error trying to invoke SMT solver. -// Warning 4661: (194-213): BMC: Assertion violation happens here. +// Warning 6328: (194-213): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/division_3.sol b/test/libsolidity/smtCheckerTests/operators/division_3.sol index 522212855..e9d9ed5ae 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_3.sol @@ -6,5 +6,4 @@ contract C { } } // ---- -// Warning 1218: (127-132): CHC: Error trying to invoke SMT solver. -// Warning 2661: (127-132): BMC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. +// Warning 4984: (127-132): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/division_4.sol b/test/libsolidity/smtCheckerTests/operators/division_4.sol index b9add545b..90143db21 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_4.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_4.sol @@ -7,4 +7,3 @@ contract C { } } // ---- -// Warning 1218: (147-152): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/division_5.sol b/test/libsolidity/smtCheckerTests/operators/division_5.sol index 70c67d96c..32f69de7e 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_5.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_5.sol @@ -10,4 +10,3 @@ contract C { } } // ---- -// Warning 1218: (151-156): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/division_6.sol b/test/libsolidity/smtCheckerTests/operators/division_6.sol index 198f9e800..4dfd728c1 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_6.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_6.sol @@ -12,4 +12,3 @@ contract C { } } // ---- -// Warning 1218: (265-270): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol index 331da0d47..ddffc10fd 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol @@ -7,4 +7,3 @@ contract C { } } // ---- -// Warning 1218: (107-125): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol index 21acea379..985e7fdeb 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol @@ -7,5 +7,3 @@ contract C { } } // ---- -// Warning 1218: (112-117): CHC: Error trying to invoke SMT solver. -// Warning 1218: (105-123): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol index 354325e7c..58dc80262 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol @@ -7,5 +7,3 @@ contract C { } } // ---- -// Warning 1218: (113-118): CHC: Error trying to invoke SMT solver. -// Warning 1218: (106-125): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol index 5024e6805..44f34fb2a 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol @@ -7,5 +7,3 @@ contract C { } } // ---- -// Warning 1218: (113-118): CHC: Error trying to invoke SMT solver. -// Warning 1218: (106-125): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol index e59d26295..87f048482 100644 --- a/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol +++ b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol @@ -7,5 +7,3 @@ contract C { } } // ---- -// Warning 1218: (114-119): CHC: Error trying to invoke SMT solver. -// Warning 1218: (107-125): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/mod.sol b/test/libsolidity/smtCheckerTests/operators/mod.sol index 0c5940052..f147d7c0a 100644 --- a/test/libsolidity/smtCheckerTests/operators/mod.sol +++ b/test/libsolidity/smtCheckerTests/operators/mod.sol @@ -9,4 +9,3 @@ contract C { } } // ---- -// Warning 1218: (166-182): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/mod_even.sol b/test/libsolidity/smtCheckerTests/operators/mod_even.sol index 1b88e3fc5..b91b06fa8 100644 --- a/test/libsolidity/smtCheckerTests/operators/mod_even.sol +++ b/test/libsolidity/smtCheckerTests/operators/mod_even.sol @@ -9,5 +9,3 @@ contract C } } // ---- -// Warning 1218: (113-118): CHC: Error trying to invoke SMT solver. -// Warning 1218: (122-142): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/mod_n.sol b/test/libsolidity/smtCheckerTests/operators/mod_n.sol index 81f5b6a66..9db8855db 100644 --- a/test/libsolidity/smtCheckerTests/operators/mod_n.sol +++ b/test/libsolidity/smtCheckerTests/operators/mod_n.sol @@ -9,4 +9,3 @@ contract C } } // ---- -// Warning 1218: (126-139): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol b/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol index b219917d6..eb13ab3a8 100644 --- a/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol +++ b/test/libsolidity/smtCheckerTests/operators/mod_n_uint16.sol @@ -9,4 +9,3 @@ contract C } } // ---- -// Warning 1218: (130-149): CHC: Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/mod_signed.sol b/test/libsolidity/smtCheckerTests/operators/mod_signed.sol new file mode 100644 index 000000000..552e304dd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/mod_signed.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(int x, int y) public pure { + require(y != 0); + require(x == 42); + int z1 = x % y; + int z2 = -x % y; + assert(z1 == -z2); + assert((x >= 0 && z1 >=0) || (x <= 0 && z1 <= 0)); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol index a7fd99e15..a3ef63779 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol @@ -6,6 +6,5 @@ contract C { } } // ---- -// Warning 1218: (110-115): CHC: Error trying to invoke SMT solver. +// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. // Warning 3046: (110-115): BMC: Division by zero happens here. -// Warning 2661: (110-115): BMC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.