cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] encoding division and modulo operations using slack variables

Browse Source
This commit is contained in:
Martin Blicha
2020-10-16 16:06:31 +02:00
parent 23314fc96c
commit 78c8fbc7ce
24 changed files with 41 additions and 70 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+27 -9
View File
@@ -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<IntegerType const&>(*_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<smtutil::Expression, smtutil::Expression> 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<smtutil::Expression, smtutil::Expression> 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(
libsolidity/formal/SMTEncoder.h
+9 -3
View File
@@ -36,6 +36,7 @@
#include <string>
#include <unordered_map>
#include <vector>
#include <utility>
namespace solidity::langutil
{
@@ -174,9 +175,14 @@ protected:
std::vector<smtutil::Expression> 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<smtutil::Expression, smtutil::Expression> 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.