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] Supporting compound shift operators.

Browse Source
This commit is contained in:
Djordje Mijovic 2020-09-22 11:15:56 +02:00
parent 0193952106
commit 79f550dba9
1 changed files with 9 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
libsolidity/formal/SMTEncoder.cpp
View File

@ -352,34 +352,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
{ {
createExpr(_assignment); createExpr(_assignment);
static set<Token> const compoundOps{
Token::AssignAdd,
Token::AssignSub,
Token::AssignMul,
Token::AssignDiv,
Token::AssignMod,
Token::AssignBitAnd,
Token::AssignBitOr,
Token::AssignBitXor
};
Token op = _assignment.assignmentOperator(); Token op = _assignment.assignmentOperator();
if (op != Token::Assign && !compoundOps.count(op)) solAssert(TokenTraits::isAssignmentOp(op), "");
{
Expression const* identifier = &_assignment.leftHandSide();
if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(identifier))
identifier = leftmostBase(*indexAccess);
// Give it a new index anyway to keep the SSA scheme sound.
solAssert(identifier, "");
if (auto varDecl = identifierToVariable(*identifier))
m_context.newValue(*varDecl);
m_errorReporter.warning( if (!smt::isSupportedType(*_assignment.annotation().type))
9149_error,
_assignment.location(),
"Assertion checker does not yet implement this assignment operator."
);
}
else 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.
@ -397,9 +373,9 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
else else
{ {
auto const& type = _assignment.annotation().type; auto const& type = _assignment.annotation().type;
auto rightHandSide = compoundOps.count(op) ? auto rightHandSide = op == Token::Assign ?
compoundAssignment(_assignment) : expr(_assignment.rightHandSide(), type) :
expr(_assignment.rightHandSide(), type); compoundAssignment(_assignment);
defineExpr(_assignment, rightHandSide); defineExpr(_assignment, rightHandSide);
assignment( assignment(
_assignment.leftHandSide(), _assignment.leftHandSide(),
@ -1629,7 +1605,10 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
static map<Token, Token> const compoundToBitwise{ static map<Token, Token> const compoundToBitwise{
{Token::AssignBitAnd, Token::BitAnd}, {Token::AssignBitAnd, Token::BitAnd},
{Token::AssignBitOr, Token::BitOr}, {Token::AssignBitOr, Token::BitOr},
{Token::AssignBitXor, Token::BitXor} {Token::AssignBitXor, Token::BitXor},
{Token::AssignShl, Token::SHL},
{Token::AssignShr, Token::SHR},
{Token::AssignSar, Token::SAR}
}; };
Token op = _assignment.assignmentOperator(); Token op = _assignment.assignmentOperator();
solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), ""); solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");