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

Merge pull request #6611 from ethereum/smt_refactor_assignment

Browse Source 
[SMTChecker] Refactor assignment handling
This commit is contained in:
chriseth 2019-04-30 15:26:51 +02:00 committed by GitHub
commit d940f6f7ef
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 104 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

145
libsolidity/formal/SMTChecker.cpp
View File

@ -341,15 +341,15 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
void SMTChecker::endVisit(Assignment const& _assignment)
{
static map<Token, Token> const compoundToArithmetic{
{Token::AssignAdd, Token::Add},
{Token::AssignSub, Token::Sub},
{Token::AssignMul, Token::Mul},
{Token::AssignDiv, Token::Div},
{Token::AssignMod, Token::Mod}
static set<Token> const compoundOps{
Token::AssignAdd,
Token::AssignSub,
Token::AssignMul,
Token::AssignDiv,
Token::AssignMod
};
Token op = _assignment.assignmentOperator();
if (op != Token::Assign && !compoundToArithmetic.count(op))
if (op != Token::Assign && !compoundOps.count(op))
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement this assignment operator."
@ -359,49 +359,20 @@ void SMTChecker::endVisit(Assignment const& _assignment)
_assignment.location(),
"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
);
else if (
dynamic_cast<Identifier const*>(&_assignment.leftHandSide()) ||
dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide())
)
{
boost::optional<smt::Expression> leftHandSide;
VariableDeclaration const* decl = nullptr;
auto identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide());
if (identifier)
{
decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration);
solAssert(decl, "");
solAssert(knownVariable(*decl), "");
leftHandSide = currentValue(*decl);
}
else
leftHandSide = expr(_assignment.leftHandSide());
solAssert(leftHandSide, "");
smt::Expression rightHandSide =
compoundToArithmetic.count(op) ?
arithmeticOperation(
compoundToArithmetic.at(op),
*leftHandSide,
expr(_assignment.rightHandSide()),
{
auto rightHandSide = compoundOps.count(op) ?
compoundAssignment(_assignment) :
expr(_assignment.rightHandSide());
defineExpr(_assignment, rightHandSide);
assignment(
_assignment.leftHandSide(),
expr(_assignment),
_assignment.annotation().type,
_assignment.location()
) :
expr(_assignment.rightHandSide())
;
defineExpr(_assignment, rightHandSide);
if (identifier)
assignment(*decl, _assignment, _assignment.location());
else
arrayIndexAssignment(_assignment.leftHandSide(), expr(_assignment));
}
else
m_errorReporter.warning(
_assignment.location(),
"Assertion checker does not yet implement such assignments."
);
}
}
void SMTChecker::endVisit(TupleExpression const& _tuple)
{
@ -495,9 +466,8 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
solAssert(_op.subExpression().annotation().lValueRequested, "");
if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{
auto decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration);
auto decl = identifierToVariable(*identifier);
solAssert(decl, "");
solAssert(knownVariable(*decl), "");
auto innerValue = currentValue(*decl);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
@ -754,7 +724,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
visitFunctionIdentifier(_identifier);
else if (isSupportedType(_identifier.annotation().type->category()))
{
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
if (auto decl = identifierToVariable(_identifier))
defineExpr(_identifier, currentValue(*decl));
else if (_identifier.name() == "now")
defineGlobalVariable(_identifier.name(), _identifier);
@ -923,9 +893,9 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
shared_ptr<SymbolicVariable> array;
if (auto const& id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
{
auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
solAssert(knownVariable(varDecl), "");
array = m_variables[&varDecl];
auto varDecl = identifierToVariable(*id);
solAssert(varDecl, "");
array = m_variables[varDecl];
}
else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
{
@ -964,15 +934,15 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
auto const& indexAccess = dynamic_cast<IndexAccess const&>(_expr);
if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
{
auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
solAssert(knownVariable(varDecl), "");
auto varDecl = identifierToVariable(*id);
solAssert(varDecl, "");
if (varDecl.hasReferenceOrMappingType())
if (varDecl->hasReferenceOrMappingType())
resetVariables([&](VariableDeclaration const& _var) {
if (_var == varDecl)
if (_var == *varDecl)
return false;
TypePointer prefix = _var.type();
TypePointer originalType = typeWithoutPointer(varDecl.type());
TypePointer originalType = typeWithoutPointer(varDecl->type());
while (
prefix->category() == Type::Category::Mapping ||
prefix->category() == Type::Category::Array
@ -997,15 +967,15 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
});
smt::Expression store = smt::Expression::store(
m_variables[&varDecl]->currentValue(),
m_variables[varDecl]->currentValue(),
expr(*indexAccess.indexExpression()),
_rightHandSide
);
m_interface->addAssertion(newValue(varDecl) == store);
m_interface->addAssertion(newValue(*varDecl) == store);
// Update the SMT select value after the assignment,
// necessary for sound models.
defineExpr(indexAccess, smt::Expression::select(
m_variables[&varDecl]->currentValue(),
m_variables[varDecl]->currentValue(),
expr(*indexAccess.indexExpression())
));
}
@ -1237,6 +1207,50 @@ smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _rig
return _left / _right;
}
void SMTChecker::assignment(
Expression const& _left,
smt::Expression const& _right,
TypePointer const& _type,
langutil::SourceLocation const& _location
)
{
if (!isSupportedType(_type->category()))
m_errorReporter.warning(
_location,
"Assertion checker does not yet implement type " + _type->toString()
);
else if (auto varDecl = identifierToVariable(_left))
assignment(*varDecl, _right, _location);
else if (dynamic_cast<IndexAccess const*>(&_left))
arrayIndexAssignment(_left, _right);
else
m_errorReporter.warning(
_location,
"Assertion checker does not yet implement such assignments."
);
}
smt::Expression SMTChecker::compoundAssignment(Assignment const& _assignment)
{
static map<Token, Token> const compoundToArithmetic{
{Token::AssignAdd, Token::Add},
{Token::AssignSub, Token::Sub},
{Token::AssignMul, Token::Mul},
{Token::AssignDiv, Token::Div},
{Token::AssignMod, Token::Mod}
};
Token op = _assignment.assignmentOperator();
solAssert(compoundToArithmetic.count(op), "");
auto decl = identifierToVariable(_assignment.leftHandSide());
return arithmeticOperation(
compoundToArithmetic.at(op),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
expr(_assignment.rightHandSide()),
_assignment.annotation().type,
_assignment.location()
);
}
void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location)
{
assignment(_variable, expr(_value), _location);
@ -1811,3 +1825,16 @@ set<VariableDeclaration const*> SMTChecker::touchedVariables(ASTNode const& _nod
solAssert(!m_functionPath.empty(), "");
return m_variableUsage.touchedVariables(_node, m_functionPath);
}
VariableDeclaration const* SMTChecker::identifierToVariable(Expression const& _expr)
{
if (auto identifier = dynamic_cast<Identifier const*>(&_expr))
{
if (auto decl = dynamic_cast<VariableDeclaration const*>(identifier->annotation().referencedDeclaration))
{
solAssert(knownVariable(*decl), "");
return decl;
}
}
return nullptr;
}

14
libsolidity/formal/SMTChecker.h
View File

@ -135,7 +135,18 @@ private:
smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
void assignment(VariableDeclaration const& _variable, Expression const& _value, langutil::SourceLocation const& _location);
/// Handles assignments to variables of different types.
void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, langutil::SourceLocation const& _location);
/// Handles assignments between generic expressions.
/// Will also be used for assignments of tuple components.
void assignment(
Expression const& _left,
smt::Expression const& _right,
TypePointer const& _type,
langutil::SourceLocation const& _location
);
/// Computes the right hand side of a compound assignment.
smt::Expression compoundAssignment(Assignment const& _assignment);
/// Maps a variable to an SSA index.
using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
@ -274,6 +285,9 @@ private:
/// @returns variables that are touched in _node's subtree.
std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
VariableDeclaration const* identifierToVariable(Expression const& _expr);
std::shared_ptr<smt::SolverInterface> m_interface;
VariableUsage m_variableUsage;
bool m_loopExecutionHappened = false;

4
test/libsolidity/smtCheckerTestsJSON/multi.json
View File

@ -3,8 +3,8 @@
{
"smtlib2responses":
{
"0x47a038dd9021ecb218726ea6bf1f75c215a50b1981bae4341e89c9f2b7ac5db7": "sat\n((|EVALEXPR_0| 1))",
"0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))",
"0x47a038dd9021ecb218726ea6bf1f75c215a50b1981bae4341e89c9f2b7ac5db7": "sat\n((|EVALEXPR_0| 1))\n",
"0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))\n",
"0xf49b9d0eb7b6d2f2ac9e1604288e52ee1a08cda57058e26d7843ed109ca6d7c9": "unsat\n"
}
}