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 #10355 from blishko/smtchecker-refactoring

Browse Source 
[SMTChecker] Small refactoring of assignments to provide a common low-level point for model checking engines to hook into.
This commit is contained in:
Leonardo 2020-11-20 14:31:32 -01:00 committed by GitHub
commit 61069ec77d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 15 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
libsolidity/formal/SMTEncoder.cpp
View File

@ -1078,10 +1078,10 @@ void SMTEncoder::endVisit(Return const& _return)
solAssert(types.size() == returnParams.size(), ""); solAssert(types.size() == returnParams.size(), "");
for (unsigned i = 0; i < returnParams.size(); ++i) for (unsigned i = 0; i < returnParams.size(); ++i)
m_context.addAssertion(symbTuple->component(i, types.at(i), returnParams.at(i)->type()) == m_context.newValue(*returnParams.at(i))); assignment(*returnParams.at(i), symbTuple->component(i, types.at(i), returnParams.at(i)->type()));
} }
else if (returnParams.size() == 1) else if (returnParams.size() == 1)
m_context.addAssertion(expr(*_return.expression(), returnParams.front()->type()) == m_context.newValue(*returnParams.front())); assignment(*returnParams.front(), expr(*_return.expression(), returnParams.front()->type()));
} }
} }
@ -1297,8 +1297,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
if (var->hasReferenceOrMappingType()) if (var->hasReferenceOrMappingType())
resetReferences(*var); resetReferences(*var);
m_context.addAssertion(m_context.newValue(*var) == _rightHandSide); assignment(*var, _rightHandSide);
m_context.expression(_expr)->increaseIndex();
defineExpr(_expr, currentValue(*var)); defineExpr(_expr, currentValue(*var));
return; return;
} }
@ -1323,7 +1322,6 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)), smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
{smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()} {smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
); );
m_context.expression(*indexAccess)->increaseIndex();
defineExpr(*indexAccess, smtutil::Expression::select( defineExpr(*indexAccess, smtutil::Expression::select(
symbArray->elements(), symbArray->elements(),
indexExpr indexExpr
@ -1364,8 +1362,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
if (varDecl->hasReferenceOrMappingType()) if (varDecl->hasReferenceOrMappingType())
resetReferences(*varDecl); resetReferences(*varDecl);
m_context.addAssertion(m_context.newValue(*varDecl) == toStore); assignment(*varDecl, toStore);
m_context.expression(*id)->increaseIndex();
defineExpr(*id, currentValue(*varDecl)); defineExpr(*id, currentValue(*varDecl));
break; break;
} }
@ -1378,8 +1375,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
) )
resetReferences(type); resetReferences(type);
m_context.expression(*lastExpr)->increaseIndex(); assignment(*m_context.expression(*lastExpr), toStore);
m_context.addAssertion(expr(*lastExpr) == toStore);
break; break;
} }
} }
@ -1958,7 +1954,12 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expre
TypePointer type = _variable.type(); TypePointer type = _variable.type();
if (type->category() == Type::Category::Mapping) if (type->category() == Type::Category::Mapping)
arrayAssignment(); arrayAssignment();
m_context.addAssertion(m_context.newValue(_variable) == _value); assignment(*m_context.variable(_variable), _value);
}
void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value)
{
m_context.addAssertion(_symVar.increaseIndex() == _value);
} }
SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition) SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition)

4
libsolidity/formal/SMTEncoder.h
View File

@ -194,6 +194,10 @@ protected:
IntegerType const& _type IntegerType const& _type
); );
/// Handles the actual assertion of the new value to the encoding context.
/// Other assignment methods should use this one in the end.
void assignment(smt::SymbolicVariable& _symVar, smtutil::Expression const& _value);
void assignment(VariableDeclaration const& _variable, Expression const& _value); void assignment(VariableDeclaration const& _variable, Expression const& _value);
/// Handles assignments to variables of different types. /// Handles assignments to variables of different types.
void assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value); void assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value);