cerc-io/solidity
16
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] Fix compound assignment to push

Browse Source
This commit is contained in:
Martin Blicha 2021-03-23 19:34:46 +01:00
parent 13d3b35141
commit 98446782e2
3 changed files with 22 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* AST Output: Fix ``kind`` field of ``ModifierInvocation`` for base constructor calls. * AST Output: Fix ``kind`` field of ``ModifierInvocation`` for base constructor calls.
* SMTChecker: Fix false positive and false negative on ``push`` as LHS of a compound assignment.
* SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available. * SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available.

33
libsolidity/formal/SMTEncoder.cpp
View File

@ -373,34 +373,12 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
bool SMTEncoder::visit(Assignment const& _assignment) bool SMTEncoder::visit(Assignment const& _assignment)
{ {
auto const& left = _assignment.leftHandSide(); // RHS must be visited before LHS; as opposed to what Assignment::accept does
auto const& right = _assignment.rightHandSide(); _assignment.rightHandSide().accept(*this);
_assignment.leftHandSide().accept(*this);
if (auto const* memberAccess = isEmptyPush(left))
{
right.accept(*this);
left.accept(*this);
auto const& memberExpr = memberAccess->expression();
auto& symbArray = dynamic_cast<smt::SymbolicArrayVariable&>(*m_context.expression(memberExpr));
smtutil::Expression oldElements = symbArray.elements();
smtutil::Expression length = symbArray.length();
symbArray.increaseIndex();
m_context.addAssertion(symbArray.elements() == smtutil::Expression::store(
oldElements,
length - 1,
expr(right)
));
m_context.addAssertion(symbArray.length() == length);
arrayPushPopAssign(memberExpr, symbArray.currentValue());
defineExpr(_assignment, expr(left));
return false; return false;
} }
return true;
}
void SMTEncoder::endVisit(Assignment const& _assignment) void SMTEncoder::endVisit(Assignment const& _assignment)
{ {
createExpr(_assignment); createExpr(_assignment);
@ -408,9 +386,6 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
Token op = _assignment.assignmentOperator(); Token op = _assignment.assignmentOperator();
solAssert(TokenTraits::isAssignmentOp(op), ""); solAssert(TokenTraits::isAssignmentOp(op), "");
if (isEmptyPush(_assignment.leftHandSide()))
return;
if (!smt::isSupportedType(*_assignment.annotation().type)) if (!smt::isSupportedType(*_assignment.annotation().type))
{ {
// Give it a new index anyway to keep the SSA scheme sound. // Give it a new index anyway to keep the SSA scheme sound.
@ -2022,6 +1997,8 @@ void SMTEncoder::assignment(
dynamic_cast<MemberAccess const*>(left) dynamic_cast<MemberAccess const*>(left)
) )
indexOrMemberAssignment(*left, _right); indexOrMemberAssignment(*left, _right);
else if (isEmptyPush(*left))
arrayPushPopAssign(*left, _right);
else else
solAssert(false, ""); solAssert(false, "");
} }

15
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
int[] u;
function t() public {
require(u.length == 0);
u.push() -= 1;
assert(u[0] < 0); // should hold
assert(u[0] >= 0); // should fail
}
}
// ----
// Warning 6328: (161-178): CHC: Assertion violation happens here.\nCounterexample:\nu = [(- 1)]\n\nTransaction trace:\nC.constructor()\nState: u = []\nC.t()