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

Merge pull request #10599 from blishko/smt-inc-dec-push-fix

Browse Source 
[SMTChecker] Fix internal error when increment/decrement is applied on a result of push().
This commit is contained in:
Leonardo 2020-12-14 23:52:54 +01:00 committed by GitHub
commit d83ce0bcdd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 42 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
libsolidity/formal/SMTEncoder.cpp
View File

@ -507,18 +507,21 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
{
solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
solAssert(subExpr->annotation().willBeWrittenTo, "");
auto computeNewValue = [&](auto currentValue) {
return arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
currentValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
};
if (auto identifier = dynamic_cast<Identifier const*>(subExpr))
{
auto decl = identifierToVariable(*identifier);
solAssert(decl, "");
auto innerValue = currentValue(*decl);
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
auto newValue = computeNewValue(innerValue);
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
assignment(*decl, newValue);
}
@ -528,16 +531,17 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
)
{
auto innerValue = expr(*subExpr);
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
auto newValue = computeNewValue(innerValue);
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
indexOrMemberAssignment(*subExpr, newValue);
}
else if (isEmptyPush(*subExpr))
{
auto innerValue = expr(*subExpr);
auto newValue = computeNewValue(innerValue);
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
arrayPushPopAssign(*subExpr, newValue);
}
else
solAssert(false, "");

13
test/libsolidity/smtCheckerTests/operators/unary_add_array_push_1.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
uint[] x;
function f() public {
require(x.length == 0);
++x.push();
assert(x.length == 1);
assert(x[0] == 1); // should hold
assert(x[0] == 42); // should fail
}
}
// ----
// Warning 6328: (182-200): CHC: Assertion violation happens here.\nCounterexample:\nx = [1]\n\n\n\nTransaction trace:\nconstructor()\nState: x = []\nf()

11
test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
struct S {
int[][] d;
}
S[] data;
function f() public {
++data[1].d[3].push();
}
}