cerc-io/solidity
10
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

Force SMT variable creation order

Browse Source
This commit is contained in:
Leonardo Alt 2020-11-06 11:51:01 +00:00
parent 646be53f2f
commit 89dce24f24
1 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
libsolidity/formal/SMTEncoder.cpp
View File

@ -1804,23 +1804,25 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
{ {
IntegerType const* intType = &_type; IntegerType const* intType = &_type;
string suffix = "div_mod_" + to_string(m_context.newUniqueId()); string suffix = "div_mod_" + to_string(m_context.newUniqueId());
smt::SymbolicIntVariable d(intType, intType, "d_" + suffix, m_context); smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context);
smt::SymbolicIntVariable r(intType, intType, "r_" + suffix, m_context); smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context);
auto d = dSymb.currentValue();
auto r = rSymb.currentValue();
// x / y = d and x % y = r iff d * y + r = x and // 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) // either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned)
// or x < 0 and -abs(y) < r <= 0 // or x < 0 and -abs(y) < r <= 0
m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left); m_context.addAssertion(((d * _right) + r) == _left);
if (_type.isSigned()) if (_type.isSigned())
m_context.addAssertion( m_context.addAssertion(
(_left >= 0 && 0 <= r.currentValue() && (_right == 0 || r.currentValue() < smtutil::abs(_right))) || (_left >= 0 && 0 <= r && (_right == 0 || r < smtutil::abs(_right))) ||
(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r.currentValue()) && r.currentValue() <= 0)) (_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r) && r <= 0))
); );
else // unsigned version else // unsigned version
m_context.addAssertion(0 <= r.currentValue() && (_right == 0 || r.currentValue() < _right)); m_context.addAssertion(0 <= r && (_right == 0 || r < _right));
auto divResult = smtutil::Expression::ite(_right == 0, 0, d.currentValue()); auto divResult = smtutil::Expression::ite(_right == 0, 0, d);
auto modResult = smtutil::Expression::ite(_right == 0, 0, r.currentValue()); auto modResult = smtutil::Expression::ite(_right == 0, 0, r);
return {divResult, modResult}; return {divResult, modResult};
} }