From 3c4e2863908cc158edf083aa570d3940430b98ca Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 9 Jun 2020 13:07:40 +0200 Subject: [PATCH] [SMTChecker] Replace wrap mod by slack vars --- libsolidity/formal/EncodingContext.cpp | 11 +++ libsolidity/formal/EncodingContext.h | 7 ++ libsolidity/formal/SMTEncoder.cpp | 69 +++++++++++++------ .../functions_recursive_indirect.sol | 1 - .../loops/for_1_false_positive.sol | 2 - ..._loop_array_assignment_storage_storage.sol | 2 - 6 files changed, 66 insertions(+), 26 deletions(-) diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 51dd37a3d..57686ace4 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -32,12 +32,23 @@ EncodingContext::EncodingContext(): void EncodingContext::reset() { resetAllVariables(); + resetSlackId(); m_expressions.clear(); m_globalContext.clear(); m_state.reset(); m_assertions.clear(); } +void EncodingContext::resetSlackId() +{ + m_nextSlackId = 0; +} + +unsigned EncodingContext::newSlackId() +{ + return m_nextSlackId++; +} + void EncodingContext::clear() { m_variables.clear(); diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index 79f9567a5..fcfd5e149 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -40,6 +40,10 @@ public: /// alive because of state variables and inlined function calls. /// To be used in the beginning of a root function visit. void reset(); + /// Resets the fresh id for slack variables. + void resetSlackId(); + /// Returns the current fresh slack id and increments it. + unsigned newSlackId(); /// Clears the entire context, erasing everything. /// To be used before a model checking engine starts. void clear(); @@ -168,6 +172,9 @@ private: /// Whether to conjoin assertions in the assertion stack. bool m_accumulateAssertions = true; //@} + + /// Fresh ids for slack variables to be created deterministically. + unsigned m_nextSlackId = 0; }; } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 82cd75578..6faaaf600 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1204,7 +1204,7 @@ pair SMTEncoder::arithmeticOperation( smtutil::Expression const& _left, smtutil::Expression const& _right, TypePointer const& _commonType, - Expression const& + Expression const& _operation ) { static set validOperators{ @@ -1227,39 +1227,66 @@ pair SMTEncoder::arithmeticOperation( else intType = TypeProvider::uint256(); - smtutil::Expression valueNoMod( - _op == Token::Add ? _left + _right : - _op == Token::Sub ? _left - _right : - _op == Token::Div ? division(_left, _right, *intType) : - _op == Token::Mul ? _left * _right : - /*_op == Token::Mod*/ _left % _right - ); + auto valueUnbounded = [&]() -> smtutil::Expression { + switch (_op) + { + 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; + default: solAssert(false, ""); + } + }(); if (_op == Token::Div || _op == Token::Mod) + { m_context.addAssertion(_right != 0); + // mod and unsigned division never underflow/overflow + if (_op == Token::Mod || !intType->isSigned()) + return {valueUnbounded, valueUnbounded}; + + // The only case where division overflows is + // - type is signed + // - LHS is type.min + // - RHS is -1 + // the result is then -(type.min), which wraps back to type.min + smtutil::Expression maxLeft = _left == smt::minValue(*intType); + smtutil::Expression minusOneRight = _right == -1; + smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded); + return {wrap, valueUnbounded}; + } + auto symbMin = smt::minValue(*intType); auto symbMax = smt::maxValue(*intType); smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1; + string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newSlackId()); + smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); + smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context); + + // To wrap around valueUnbounded in case of overflow or underflow, we replace it with a k, given: + // 1. k + m * intValueRange = valueUnbounded + // 2. k is in range of the desired integer type + auto wrap = k.currentValue(); + m_context.addAssertion(valueUnbounded == (k.currentValue() + intValueRange * m.currentValue())); + m_context.addAssertion(k.currentValue() >= symbMin); + m_context.addAssertion(k.currentValue() <= symbMax); + + // TODO this could be refined: + // for unsigned types it's enough to check only the upper bound. auto value = smtutil::Expression::ite( - valueNoMod > symbMax, - valueNoMod % intValueRange, + valueUnbounded > symbMax, + wrap, smtutil::Expression::ite( - valueNoMod < symbMin, - valueNoMod % intValueRange, - valueNoMod + valueUnbounded < symbMin, + wrap, + valueUnbounded ) ); - if (intType->isSigned()) - value = smtutil::Expression::ite( - value > symbMax, - value - intValueRange, - value - ); - - return {value, valueNoMod}; + return {value, valueUnbounded}; } void SMTEncoder::compareOperation(BinaryOperation const& _op) diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol index 5d3292992..7cb7b22b1 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol @@ -22,4 +22,3 @@ contract C } } // ---- -// Warning: (130-144): Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol index 11cd22d11..c37df70c4 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -14,6 +14,4 @@ contract C } } // ---- -// Warning: (296-309): Error trying to invoke SMT solver. // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (296-309): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol index 5c664f214..a90053024 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol @@ -19,7 +19,5 @@ contract LoopFor2 { } } // ---- -// Warning: (317-337): Error trying to invoke SMT solver. -// Warning: (317-337): Assertion violation happens here // Warning: (341-360): Assertion violation happens here // Warning: (364-383): Assertion violation happens here