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] Adding unary increment and decrement as under/overflow verification targets for the CHC engine

Browse Source
This commit is contained in:
Martin Blicha
2020-12-11 17:41:50 +01:00
parent ccd1f283aa
commit 8927015e5a
40 changed files with 150 additions and 59 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+1 -16
View File
@@ -356,27 +356,12 @@ void BMC::endVisit(UnaryOperation const& _op)
)
return;
switch (_op.getOperator())
{
case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix)
if (_op.getOperator() == Token::Sub && smt::isInteger(*_op.annotation().type))
addVerificationTarget(
VerificationTarget::Type::UnderOverflow,
expr(_op),
&_op
);
break;
case Token::Sub: // -
if (_op.annotation().type->category() == Type::Category::Integer)
addVerificationTarget(
VerificationTarget::Type::UnderOverflow,
expr(_op),
&_op
);
break;
default:
break;
}
}
void BMC::endVisit(FunctionCall const& _funCall)
libsolidity/formal/SMTEncoder.cpp
+14 -2
View File
@@ -512,7 +512,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
auto decl = identifierToVariable(*identifier);
solAssert(decl, "");
auto innerValue = currentValue(*decl);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
assignment(*decl, newValue);
}
@@ -522,7 +528,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
)
{
auto innerValue = expr(*subExpr);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
indexOrMemberAssignment(*subExpr, newValue);
}