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 #7490 from ethereum/smt_constructor

Browse Source 
[SMTChecker] Add support to constructors
This commit is contained in:
chriseth 2019-11-28 14:51:17 +01:00 committed by GitHub
commit 912a0e2e4d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
46 changed files with 1051 additions and 172 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -6,6 +6,7 @@ Language Features:
Compiler Features:
* SMTChecker: Add support to constructors including constructor inheritance.
* Yul: When compiling via Yul, string literals from the Solidity code are kept as string literals if every character is safely printable.
* Yul Optimizer: Perform loop-invariant code motion.

26
libsolidity/formal/BMC.cpp
View File

@ -110,11 +110,6 @@ bool BMC::visit(ContractDefinition const& _contract)
{
initContract(_contract);
/// Check targets created by state variable initialization.
smt::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
m_verificationTargets.clear();
SMTEncoder::visit(_contract);
return false;
@ -122,6 +117,17 @@ bool BMC::visit(ContractDefinition const& _contract)
void BMC::endVisit(ContractDefinition const& _contract)
{
if (auto constructor = _contract.constructor())
constructor->accept(*this);
else
{
inlineConstructorHierarchy(_contract);
/// Check targets created by state variable initialization.
smt::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
m_verificationTargets.clear();
}
SMTEncoder::endVisit(_contract);
}
@ -132,10 +138,14 @@ bool BMC::visit(FunctionDefinition const& _function)
solAssert(m_currentContract, "");
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end())
initializeStateVariables(*contract);
createStateVariables(*contract);
if (m_callStack.empty())
{
reset();
initFunction(_function);
resetStateVariables();
}
/// Already visits the children.
SMTEncoder::visit(_function);
@ -447,10 +457,6 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
// is that there we don't have `_funCall`.
pushCallStack({funDef, &_funCall});
// If an internal function is called to initialize
// a state variable.
if (m_callStack.empty())
initFunction(*funDef);
funDef->accept(*this);
}

184
libsolidity/formal/CHC.cpp
View File

@ -65,6 +65,15 @@ void CHC::analyze(SourceUnit const& _source)
m_context.setAssertionAccumulation(false);
m_variableUsage.setFunctionInlining(false);
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
auto genesisSort = make_shared<smt::FunctionSort>(
vector<smt::SortPointer>(),
boolSort
);
m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
auto genesis = (*m_genesisPredicate)({});
addRule(genesis, genesis.name);
_source.accept(*this);
}
@ -94,10 +103,10 @@ bool CHC::visit(ContractDefinition const& _contract)
else
m_stateSorts.push_back(smt::smtSort(*var->type()));
clearIndices();
clearIndices(&_contract);
string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id());
m_interfacePredicate = createSymbolicBlock(interfaceSort(), interfaceName);
string suffix = _contract.name() + "_" + to_string(_contract.id());
m_interfacePredicate = createSymbolicBlock(interfaceSort(), "interface_" + suffix);
// TODO create static instances for Bool/Int sorts in SolverInterface.
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
@ -105,27 +114,11 @@ bool CHC::visit(ContractDefinition const& _contract)
vector<smt::SortPointer>(),
boolSort
);
m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error");
// If the contract has a constructor it is handled as a function.
// Otherwise we zero-initialize all state vars.
if (!_contract.constructor())
{
string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id());
m_constructorPredicate = createSymbolicBlock(constructorSort(), constructorName);
smt::Expression constructorPred = (*m_constructorPredicate)({});
addRule(constructorPred, constructorName);
for (auto const& var: m_stateVariables)
{
auto const& symbVar = m_context.variable(*var);
symbVar->increaseIndex();
m_interface->declareVariable(symbVar->currentName(), symbVar->sort());
m_context.setZeroValue(*symbVar);
}
connectBlocks(constructorPred, interface());
}
m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix);
m_constructorPredicate = createSymbolicBlock(constructorSort(), "implicit_constructor_" + to_string(_contract.id()));
auto stateExprs = currentStateVariables();
setCurrentBlock(*m_interfacePredicate, &stateExprs);
SMTEncoder::visit(_contract);
return false;
@ -136,6 +129,23 @@ void CHC::endVisit(ContractDefinition const& _contract)
if (!shouldVisit(_contract))
return;
for (auto const& var: m_stateVariables)
{
solAssert(m_context.knownVariable(*var), "");
m_context.setZeroValue(*var);
}
auto genesisPred = (*m_genesisPredicate)({});
auto implicitConstructor = (*m_constructorPredicate)(currentStateVariables());
connectBlocks(genesisPred, implicitConstructor);
m_currentBlock = implicitConstructor;
if (auto constructor = _contract.constructor())
constructor->accept(*this);
else
inlineConstructorHierarchy(_contract);
connectBlocks(m_currentBlock, interface());
for (unsigned i = 0; i < m_verificationTargets.size(); ++i)
{
auto const& target = m_verificationTargets.at(i);
@ -152,6 +162,16 @@ bool CHC::visit(FunctionDefinition const& _function)
if (!shouldVisit(_function))
return false;
// This is the case for base constructor inlining.
if (m_currentFunction)
{
solAssert(m_currentFunction->isConstructor(), "");
solAssert(_function.isConstructor(), "");
solAssert(_function.scope() != m_currentContract, "");
SMTEncoder::visit(_function);
return false;
}
solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
m_currentFunction = &_function;
@ -163,20 +183,11 @@ bool CHC::visit(FunctionDefinition const& _function)
auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
auto bodyPred = predicate(*bodyBlock);
// Store the constraints related to variable initialization.
smt::Expression const& initAssertions = m_context.assertions();
m_context.pushSolver();
connectBlocks(interface(), functionPred);
connectBlocks(m_currentBlock, functionPred);
connectBlocks(functionPred, bodyPred);
m_context.popSolver();
setCurrentBlock(*bodyBlock);
// We need to re-add the constraints that were created for initialization of variables.
m_context.addAssertion(initAssertions);
SMTEncoder::visit(*m_currentFunction);
return false;
@ -187,10 +198,37 @@ void CHC::endVisit(FunctionDefinition const& _function)
if (!shouldVisit(_function))
return;
connectBlocks(m_currentBlock, interface());
// This is the case for base constructor inlining.
if (m_currentFunction != &_function)
{
solAssert(m_currentFunction && m_currentFunction->isConstructor(), "");
solAssert(_function.isConstructor(), "");
solAssert(_function.scope() != m_currentContract, "");
}
else
{
// We create an extra exit block for constructors that simply
// connects to the interface in case an explicit constructor
// exists in the hierarchy.
// It is not connected directly here, as normal functions are,
// because of the case where there are only implicit constructors.
// This is done in endVisit(ContractDefinition).
if (_function.isConstructor())
{
auto constructorExit = createBlock(&_function, "exit_");
connectBlocks(m_currentBlock, predicate(*constructorExit));
setCurrentBlock(*constructorExit);
}
else
{
connectBlocks(m_currentBlock, interface());
clearIndices(m_currentContract, m_currentFunction);
auto stateExprs = currentStateVariables();
setCurrentBlock(*m_interfacePredicate, &stateExprs);
}
m_currentFunction = nullptr;
}
solAssert(&_function == m_currentFunction, "");
m_currentFunction = nullptr;
SMTEncoder::endVisit(_function);
}
@ -445,7 +483,6 @@ void CHC::reset()
m_verificationTargets.clear();
m_safeAssertions.clear();
m_unknownFunctionCallSeen = false;
m_blockCounter = 0;
m_breakDest = nullptr;
m_continueDest = nullptr;
}
@ -470,28 +507,31 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
{
if (
_function.isPublic() &&
_function.isImplemented() &&
!_function.isConstructor()
_function.isImplemented()
)
return true;
return false;
}
void CHC::setCurrentBlock(smt::SymbolicFunctionVariable const& _block)
void CHC::setCurrentBlock(
smt::SymbolicFunctionVariable const& _block,
vector<smt::Expression> const* _arguments
)
{
m_context.popSolver();
clearIndices();
solAssert(m_currentContract, "");
clearIndices(m_currentContract, m_currentFunction);
m_context.pushSolver();
m_currentBlock = predicate(_block);
if (_arguments)
m_currentBlock = predicate(_block, *_arguments);
else
m_currentBlock = predicate(_block);
}
smt::SortPointer CHC::constructorSort()
{
solAssert(m_currentContract, "");
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
if (!m_currentContract->constructor())
return make_shared<smt::FunctionSort>(vector<smt::SortPointer>{}, boolSort);
return sort(*m_currentContract->constructor());
// TODO this will change once we support function calls.
return interfaceSort();
}
smt::SortPointer CHC::interfaceSort()
@ -556,19 +596,6 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPoin
return block;
}
smt::Expression CHC::constructor()
{
solAssert(m_currentContract, "");
if (!m_currentContract->constructor())
return (*m_constructorPredicate)({});
vector<smt::Expression> paramExprs;
for (auto const& var: m_currentContract->constructor()->parameters())
paramExprs.push_back(m_context.variable(*var)->currentValue());
return (*m_constructorPredicate)(paramExprs);
}
smt::Expression CHC::interface()
{
vector<smt::Expression> paramExprs;
@ -613,37 +640,31 @@ void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to
addRule(edge, _from.name + "_to_" + _to.name);
}
vector<smt::Expression> CHC::currentStateVariables()
{
solAssert(m_currentContract, "");
vector<smt::Expression> exprs;
for (auto const& var: m_stateVariables)
exprs.push_back(m_context.variable(*var)->currentValue());
return exprs;
}
vector<smt::Expression> CHC::currentFunctionVariables()
{
solAssert(m_currentFunction, "");
vector<smt::Expression> paramExprs;
for (auto const& var: m_stateVariables)
paramExprs.push_back(m_context.variable(*var)->currentValue());
for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
paramExprs.push_back(m_context.variable(*var)->currentValue());
return paramExprs;
if (m_currentFunction)
for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
paramExprs.push_back(m_context.variable(*var)->currentValue());
return currentStateVariables() + paramExprs;
}
vector<smt::Expression> CHC::currentBlockVariables()
{
solAssert(m_currentFunction, "");
vector<smt::Expression> paramExprs;
for (auto const& var: m_currentFunction->localVariables())
paramExprs.push_back(m_context.variable(*var)->currentValue());
return currentFunctionVariables() + paramExprs;
}
void CHC::clearIndices()
{
for (auto const& var: m_stateVariables)
m_context.variable(*var)->resetIndex();
if (m_currentFunction)
{
for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
m_context.variable(*var)->resetIndex();
for (auto const& var: m_currentFunction->localVariables())
m_context.variable(*var)->resetIndex();
}
paramExprs.push_back(m_context.variable(*var)->currentValue());
return currentFunctionVariables() + paramExprs;
}
string CHC::predicateName(ASTNode const* _node)
@ -674,7 +695,6 @@ smt::Expression CHC::predicate(
return _block(_arguments);
}
void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
{
m_interface->addRule(_rule, _ruleName);

20
libsolidity/formal/CHC.h
View File

@ -83,7 +83,7 @@ private:
void eraseKnowledge();
bool shouldVisit(ContractDefinition const& _contract) const;
bool shouldVisit(FunctionDefinition const& _function) const;
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block);
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
//@}
/// Sort helpers.
@ -99,8 +99,6 @@ private:
/// @returns a new block of given _sort and _name.
std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
/// Constructor predicate over current variables.
smt::Expression constructor();
/// Interface predicate over current variables.
smt::Expression interface();
/// Error predicate over current variables.
@ -116,17 +114,16 @@ private:
void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
/// @returns the current symbolic values of the current state variables.
std::vector<smt::Expression> currentStateVariables();
/// @returns the current symbolic values of the current function's
/// input and output parameters.
std::vector<smt::Expression> currentFunctionVariables();
/// @returns the samve as currentFunctionVariables plus
/// @returns the same as currentFunctionVariables plus
/// local variables.
std::vector<smt::Expression> currentBlockVariables();
/// Sets the SSA indices of the variables in scope to 0.
/// Used when starting a new block.
void clearIndices();
/// @returns the predicate name for a given node.
std::string predicateName(ASTNode const* _node);
/// @returns a predicate application over the current scoped variables.
@ -152,8 +149,11 @@ private:
/// Predicates.
//@{
/// Constructor predicate.
/// Default constructor sets state vars to 0.
/// Genesis predicate.
std::unique_ptr<smt::SymbolicFunctionVariable> m_genesisPredicate;
/// Implicit constructor predicate.
/// Explicit constructors are handled as functions.
std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorPredicate;
/// Artificial Interface predicate.

235
libsolidity/formal/SMTEncoder.cpp
View File

@ -22,6 +22,7 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <boost/range/adaptors.hpp>
#include <boost/range/adaptor/reversed.hpp>
using namespace std;
using namespace dev;
@ -39,11 +40,28 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
solAssert(m_currentContract, "");
for (auto const& node: _contract.subNodes())
if (!dynamic_pointer_cast<FunctionDefinition>(node))
if (
!dynamic_pointer_cast<FunctionDefinition>(node) &&
!dynamic_pointer_cast<VariableDeclaration>(node)
)
node->accept(*this);
vector<FunctionDefinition const*> resolvedFunctions = _contract.definedFunctions();
for (auto const& base: _contract.annotation().linearizedBaseContracts)
{
// Look for all the constructor invocations bottom up.
if (auto const& constructor = base->constructor())
for (auto const& invocation: constructor->modifiers())
{
auto refDecl = invocation->name()->annotation().referencedDeclaration;
if (auto const& baseContract = dynamic_cast<ContractDefinition const*>(refDecl))
{
solAssert(!m_baseConstructorCalls.count(baseContract), "");
m_baseConstructorCalls[baseContract] = invocation.get();
}
}
// Check for function overrides.
for (auto const& baseFunction: base->definedFunctions())
{
if (baseFunction->isConstructor())
@ -62,9 +80,18 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
if (!overridden)
resolvedFunctions.push_back(baseFunction);
}
}
// Functions are visited first since they might be used
// for state variable initialization which is part of
// the constructor.
// Constructors are visited as part of the constructor
// hierarchy inlining.
for (auto const& function: resolvedFunctions)
function->accept(*this);
if (!function->isConstructor())
function->accept(*this);
// Constructors need to be handled by the engines separately.
return false;
}
@ -73,13 +100,16 @@ void SMTEncoder::endVisit(ContractDefinition const& _contract)
{
m_context.resetAllVariables();
m_baseConstructorCalls.clear();
solAssert(m_currentContract == &_contract, "");
m_currentContract = nullptr;
}
void SMTEncoder::endVisit(VariableDeclaration const& _varDecl)
{
if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
// State variables are handled by the constructor.
if (_varDecl.isLocalVariable() &&_varDecl.value())
assignment(_varDecl, *_varDecl.value());
}
@ -90,25 +120,22 @@ bool SMTEncoder::visit(ModifierDefinition const&)
bool SMTEncoder::visit(FunctionDefinition const& _function)
{
// Not visited by a function call
if (m_callStack.empty())
initFunction(_function);
m_modifierDepthStack.push_back(-1);
if (_function.isConstructor())
{
m_errorReporter.warning(
_function.location(),
"Assertion checker does not yet support constructors."
);
}
else
{
_function.parameterList().accept(*this);
if (_function.returnParameterList())
_function.returnParameterList()->accept(*this);
visitFunctionOrModifier();
}
inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
// Base constructors' parameters should be set by explicit calls,
// but the most derived one needs to be initialized.
if (_function.scope() == m_currentContract)
initializeLocalVariables(_function);
_function.parameterList().accept(*this);
if (_function.returnParameterList())
_function.returnParameterList()->accept(*this);
visitFunctionOrModifier();
return false;
}
@ -130,27 +157,87 @@ void SMTEncoder::visitFunctionOrModifier()
solAssert(m_modifierDepthStack.back() < int(function.modifiers().size()), "");
ASTPointer<ModifierInvocation> const& modifierInvocation = function.modifiers()[m_modifierDepthStack.back()];
solAssert(modifierInvocation, "");
modifierInvocation->accept(*this);
auto const& modifierDef = dynamic_cast<ModifierDefinition const&>(
*modifierInvocation->name()->annotation().referencedDeclaration
);
vector<smt::Expression> modifierArgsExpr;
if (auto const* arguments = modifierInvocation->arguments())
{
auto const& modifierParams = modifierDef.parameters();
solAssert(modifierParams.size() == arguments->size(), "");
for (unsigned i = 0; i < arguments->size(); ++i)
modifierArgsExpr.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
}
initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
pushCallStack({&modifierDef, modifierInvocation.get()});
modifierDef.body().accept(*this);
popCallStack();
auto refDecl = modifierInvocation->name()->annotation().referencedDeclaration;
if (dynamic_cast<ContractDefinition const*>(refDecl))
visitFunctionOrModifier();
else if (auto modifierDef = dynamic_cast<ModifierDefinition const*>(refDecl))
inlineModifierInvocation(modifierInvocation.get(), modifierDef);
else
solAssert(false, "");
}
--m_modifierDepthStack.back();
}
void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition)
{
solAssert(_invocation, "");
_invocation->accept(*this);
vector<smt::Expression> args;
if (auto const* arguments = _invocation->arguments())
{
auto const& modifierParams = _definition->parameters();
solAssert(modifierParams.size() == arguments->size(), "");
for (unsigned i = 0; i < arguments->size(); ++i)
args.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
}
initializeFunctionCallParameters(*_definition, args);
pushCallStack({_definition, _invocation});
if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
{
modifier->body().accept(*this);
popCallStack();
}
else if (auto function = dynamic_cast<FunctionDefinition const*>(_definition))
{
if (function->isImplemented())
function->accept(*this);
// Functions are popped from the callstack in endVisit(FunctionDefinition)
}
}
void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
{
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
auto it = find(begin(hierarchy), end(hierarchy), &_contract);
solAssert(it != end(hierarchy), "");
auto nextBase = it + 1;
// Initialize the base contracts here as long as their constructors are implicit,
// stop when the first explicit constructor is found.
while (nextBase != end(hierarchy))
{
if (auto baseConstructor = (*nextBase)->constructor())
{
createLocalVariables(*baseConstructor);
// If any subcontract explicitly called baseConstructor, use those arguments.
if (m_baseConstructorCalls.count(*nextBase))
inlineModifierInvocation(m_baseConstructorCalls.at(*nextBase), baseConstructor);
else if (baseConstructor->isImplemented())
{
// The first constructor found is handled like a function
// and its pushed into the callstack there.
// This if avoids duplication in the callstack.
if (!m_callStack.empty())
pushCallStack({baseConstructor, nullptr});
baseConstructor->accept(*this);
// popped by endVisit(FunctionDefinition)
}
break;
}
else
{
initializeStateVariables(**nextBase);
++nextBase;
}
}
initializeStateVariables(_contract);
}
bool SMTEncoder::visit(PlaceholderStatement const&)
{
solAssert(!m_callStack.empty(), "");
@ -551,20 +638,25 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
solAssert(m_currentContract == nullptr, "");
m_currentContract = &_contract;
initializeStateVariables(_contract);
m_context.reset();
m_context.pushSolver();
createStateVariables(_contract);
clearIndices(m_currentContract, nullptr);
}
void SMTEncoder::initFunction(FunctionDefinition const& _function)
{
solAssert(m_callStack.empty(), "");
solAssert(m_currentContract, "");
m_context.reset();
m_context.pushSolver();
m_pathConditions.clear();
pushCallStack({&_function, nullptr});
m_uninterpretedTerms.clear();
resetStateVariables();
initializeLocalVariables(_function);
createStateVariables(*m_currentContract);
createLocalVariables(_function);
m_arrayAssignmentHappened = false;
clearIndices(m_currentContract, &_function);
}
void SMTEncoder::visitAssert(FunctionCall const& _funCall)
@ -1239,26 +1331,61 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
}
}
void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
{
for (auto var: _contract.stateVariablesIncludingInherited())
createVariable(*var);
}
void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
{
for (auto var: _contract.stateVariables())
{
solAssert(m_context.knownVariable(*var), "");
m_context.setZeroValue(*var);
}
for (auto var: _contract.stateVariables())
if (var->value())
{
var->value()->accept(*this);
assignment(*var, *var->value());
}
}
void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
{
for (auto const& variable: _function.localVariables())
if (createVariable(*variable))
m_context.setZeroValue(*variable);
createVariable(*variable);
for (auto const& param: _function.parameters())
if (createVariable(*param))
m_context.setUnknownValue(*param);
createVariable(*param);
if (_function.returnParameterList())
for (auto const& retParam: _function.returnParameters())
if (createVariable(*retParam))
m_context.setZeroValue(*retParam);
createVariable(*retParam);
}
void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
{
for (auto const& variable: _function.localVariables())
{
solAssert(m_context.knownVariable(*variable), "");
m_context.setZeroValue(*variable);
}
for (auto const& param: _function.parameters())
{
solAssert(m_context.knownVariable(*param), "");
m_context.setUnknownValue(*param);
}
if (_function.returnParameterList())
for (auto const& retParam: _function.returnParameters())
{
solAssert(m_context.knownVariable(*retParam), "");
m_context.setZeroValue(*retParam);
}
}
void SMTEncoder::resetStateVariables()
@ -1438,6 +1565,20 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
m_context.variable(*var.first)->index() = var.second;
}
void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
{
solAssert(_contract, "");
for (auto var: _contract->stateVariablesIncludingInherited())
m_context.variable(*var)->resetIndex();
if (_function)
{
for (auto const& var: _function->parameters() + _function->returnParameters())
m_context.variable(*var)->resetIndex();
for (auto const& var: _function->localVariables())
m_context.variable(*var)->resetIndex();
}
}
Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
{
Expression const* base = &_indexAccess.baseExpression();

13
libsolidity/formal/SMTEncoder.h
View File

@ -122,6 +122,12 @@ protected:
/// visit depth.
void visitFunctionOrModifier();
/// Inlines a modifier or base constructor call.
void inlineModifierInvocation(ModifierInvocation const* _invocation, CallableDeclaration const* _definition);
/// Inlines the constructor hierarchy into a single constructor.
void inlineConstructorHierarchy(ContractDefinition const& _contract);
/// Defines a new global variable or function.
void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
@ -161,7 +167,9 @@ protected:
using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
void createStateVariables(ContractDefinition const& _contract);
void initializeStateVariables(ContractDefinition const& _contract);
void createLocalVariables(FunctionDefinition const& _function);
void initializeLocalVariables(FunctionDefinition const& _function);
void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
void resetStateVariables();
@ -209,6 +217,9 @@ protected:
VariableIndices copyVariableIndices();
/// Resets the variable indices.
void resetVariableIndices(VariableIndices const& _indices);
/// Used when starting a new block.
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr);
/// @returns variables that are touched in _node's subtree.
std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
@ -253,6 +264,8 @@ protected:
/// Needs to be a stack because of function calls.
std::vector<int> m_modifierDepthStack;
std::map<ContractDefinition const*, ModifierInvocation const*> m_baseConstructorCalls;
ContractDefinition const* m_currentContract = nullptr;
/// Stores the context of the encoding.

3
test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
View File

@ -53,6 +53,5 @@ contract MyConc{
// ----
// Warning: (773-792): This declaration shadows an existing declaration.
// Warning: (1009-1086): Function state mutability can be restricted to view
// Warning: (874-879): Underflow (resulting value less than 0) happens here.
// Warning: (874-879): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning: (985-1002): Underflow (resulting value less than 0) happens here.
// Warning: (985-1002): Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol
View File

@ -137,4 +137,3 @@ contract PropagateThroughReturnValue {
// Warning: (748-755): Assertion checker does not yet support this expression.
// Warning: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer
// Warning: (748-770): Assertion checker does not yet implement such assignments.
// Warning: (849-905): Assertion checker does not yet support constructors.

2
test/libsolidity/smtCheckerTests/functions/constructor_base_basic.sol
View File

@ -13,5 +13,3 @@ contract B is A {
}
}
// ----
// Warning: (56-90): Assertion checker does not yet support constructors.
// Warning: (113-151): Assertion checker does not yet support constructors.

18
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy.sol
View File

@ -1,6 +1,16 @@
pragma experimental SMTChecker;
contract C { constructor(uint) public {} }
contract A is C { constructor() C(2) public {} }
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract A is C {
constructor() C(2) public {
assert(a == 2);
assert(a == 3);
}
}
// ----
// Warning: (45-72): Assertion checker does not yet support constructors.
// Warning: (93-121): Assertion checker does not yet support constructors.
// Warning: (166-180): Assertion violation happens here

13
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_2.sol
View File

@ -1,10 +1,7 @@
pragma experimental SMTChecker;
contract C { constructor(uint) public {} }
contract A is C { constructor() C(2) public {} }
contract B is C { constructor() C(3) public {} }
contract J is C { constructor() C(3) public {} }
contract C { uint a; constructor(uint x) public { a = x; } }
contract A is C { constructor() C(2) public { assert(a == 2); } }
contract B is C { constructor() C(3) public { assert(a == 3); } }
contract J is C { constructor() C(3) public { assert(a == 4); } }
// ----
// Warning: (45-72): Assertion checker does not yet support constructors.
// Warning: (93-121): Assertion checker does not yet support constructors.
// Warning: (142-170): Assertion checker does not yet support constructors.
// Warning: (191-219): Assertion checker does not yet support constructors.
// Warning: (271-285): Assertion violation happens here

22
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_3.sol Normal file
View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract B is C {
constructor(uint x) public {
a = x;
}
}
contract A is B {
constructor(uint x) B(x) C(x + 2) public {
assert(a == x);
assert(a == x + 1);
}
}
// ----
// Warning: (244-262): Assertion violation happens here

23
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol Normal file
View File

@ -0,0 +1,23 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract B is C {
constructor(uint x) public {
a = x;
}
}
contract A is B {
constructor(uint x) C(x + 2) B(x + 1) public {
assert(a == x + 1);
}
}
// ----
// Warning: (212-217): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (242-247): Overflow (resulting value larger than 2**256 - 1) happens here

29
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond.sol Normal file
View File

@ -0,0 +1,29 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract B1 is C {
constructor(uint x) public {
a = x;
}
}
contract B2 is C {
constructor(uint x) C(x + 2) public {
a = x;
}
}
contract A is B2, B1 {
constructor(uint x) B2(x) B1(x) public {
assert(a == x);
assert(a == x + 1);
}
}
// ----
// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (321-339): Assertion violation happens here

29
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol Normal file
View File

@ -0,0 +1,29 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract B1 is C {
constructor(uint x) public {
a = x;
}
}
contract B2 is C {
constructor(uint x) C(x + 2) public {
a = x;
}
}
contract A is B2, B1 {
constructor(uint x) B1(x) B2(x) public {
assert(a == x);
assert(a == x + 1);
}
}
// ----
// Warning: (205-210): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (321-339): Assertion violation happens here

34
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol Normal file
View File

@ -0,0 +1,34 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract B1 is C {
uint b1;
constructor(uint x) public {
b1 = x + a;
}
}
contract B2 is C {
uint b2;
constructor(uint x) C(x + 2) public {
b2 = x + a;
}
}
contract A is B2, B1 {
constructor(uint x) B2(x) B1(x) public {
assert(b1 == b2);
assert(b1 != b2);
}
}
// ----
// Warning: (165-170): Underflow (resulting value less than 0) happens here
// Warning: (165-170): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (230-235): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (253-258): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (353-369): Assertion violation happens here

23
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle.sol Normal file
View File

@ -0,0 +1,23 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor() public {
a = 2;
}
}
contract B is C {
}
contract B2 is C {
}
contract A is B, B2 {
constructor(uint x) public {
assert(a == 2);
assert(a == 3);
}
}
// ----
// Warning: (171-177): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (208-222): Assertion violation happens here

19
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_empty_middle_empty_base.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor() public {
a = 2;
}
}
contract B is C {
}
contract B2 is C {
constructor() public {
assert(a == 2);
}
}
contract A is B, B2 {
}

22
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_chain.sol Normal file
View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract F {
uint a;
constructor() public {
a = 2;
}
}
contract E is F {}
contract D is E {}
contract C is D {}
contract B is C {}
contract A is B {
constructor(uint x) public {
assert(a == 2);
assert(a == 3);
}
}
// ----
// Warning: (201-207): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (238-252): Assertion violation happens here

20
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor() public {
a = 2;
}
}
contract B is C {
}
contract A is B {
constructor(uint x) B() public {
assert(a == 2);
assert(a == 3);
}
}
// ----
// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (186-200): Assertion violation happens here

19
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_empty_middle_no_invocation.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor() public {
a = 2;
}
}
contract B is C {
}
contract A is B {
constructor(uint x) public {
assert(a == 3);
}
}
// ----
// Warning: (145-151): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (164-178): Assertion violation happens here

30
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain.sol Normal file
View File

@ -0,0 +1,30 @@
pragma experimental SMTChecker;
contract F {
uint a;
constructor() public {
a = 2;
}
}
contract E is F {}
contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
contract B is C {
constructor() public {
a = 4;
}
}
contract A is B {
constructor(uint x) public {
assert(a == 4);
assert(a == 5);
}
}
// ----
// Warning: (275-281): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (312-326): Assertion violation happens here

24
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_empty_base.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract F {
uint a;
constructor() public {
a = 2;
}
}
contract E is F {}
contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
contract B is C {
constructor() public {
assert(a == 3);
a = 4;
}
}
contract A is B {
}

29
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params.sol Normal file
View File

@ -0,0 +1,29 @@
pragma experimental SMTChecker;
contract F {
uint a;
constructor(uint x) public {
a = x;
}
}
contract E is F {}
contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
contract B is C {
constructor(uint x) F(x + 1) public {
}
}
contract A is B {
constructor(uint x) B(x) public {
assert(a == 3);
assert(a == 4);
}
}
// ----
// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (329-343): Assertion violation happens here

27
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_with_params_2.sol Normal file
View File

@ -0,0 +1,27 @@
pragma experimental SMTChecker;
contract F {
uint a;
constructor(uint x) public {
a = x;
}
}
contract E is F {}
contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
contract B is C {
constructor() F(1) public {
assert(a == 3);
assert(a == 2);
}
}
contract A is B {
}
// ----
// Warning: (260-274): Assertion violation happens here
// Warning: (260-274): Assertion violation happens here

17
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_modifier.sol Normal file
View File

@ -0,0 +1,17 @@
pragma experimental SMTChecker;
contract C {
uint a;
modifier n { _; a = 7; }
constructor(uint x) n public {
a = x;
}
}
contract A is C {
modifier m { a = 5; _; }
constructor() C(2) public {
assert(a == 4);
}
}
// ----
// Warning: (202-216): Assertion violation happens here

16
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_same_var.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract A is C {
constructor() C(2) public {
assert(a == 0);
assert(C.a == 0);
}
}
// ----
// Warning: (148-162): Assertion violation happens here

16
test/libsolidity/smtCheckerTests/functions/constructor_simple.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C {
uint x;
constructor() public {
assert(x == 0);
x = 10;
}
function f(uint y) public view {
assert(y == x);
}
}
// ----
// Warning: (148-162): Assertion violation happens here

16
test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C {
uint x = 5;
constructor() public {
assert(x == 5);
x = 10;
}
function f(uint y) public view {
assert(y == x);
}
}
// ----
// Warning: (152-166): Assertion violation happens here

18
test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol Normal file
View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract B {
uint x = 5;
}
contract C is B {
constructor() public {
assert(x == 5);
x = 10;
}
function f(uint y) public view {
assert(y == x);
}
}
// ----
// Warning: (172-186): Assertion violation happens here

17
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol Normal file
View File

@ -0,0 +1,17 @@
pragma experimental SMTChecker;
contract C {
uint x = 5;
constructor(uint a, uint b) public {
assert(x == 5);
x = a + b;
}
function f(uint y) public view {
assert(y == x);
}
}
// ----
// Warning: (169-183): Assertion violation happens here
// Warning: (122-127): Overflow (resulting value larger than 2**256 - 1) happens here

29
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_mixed_chain_with_params.sol Normal file
View File

@ -0,0 +1,29 @@
pragma experimental SMTChecker;
contract F {
uint a;
constructor(uint x) public {
a = x;
}
}
contract E is F {}
contract D is E {
constructor() public {
a = 3;
}
}
contract C is D {}
contract B is C {
constructor(uint x) F(x + 1) public {
}
}
contract A is B {
constructor(uint x) B(x) public {
assert(a == 3);
assert(a == 4);
}
}
// ----
// Warning: (234-239): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (329-343): Assertion violation happens here

11
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
uint x = 2;
constructor () public {
assert(x == 2);
assert(x == 3);
}
}
// ----
// Warning: (104-118): Assertion violation happens here

14
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_base.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
uint x = 2;
}
contract D is C {
constructor() public {
assert(x == 2);
assert(x == 3);
}
}
// ----
// Warning: (124-138): Assertion violation happens here

22
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain.sol Normal file
View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract A {
uint x = 1;
}
contract B is A {
constructor() public { x = 2; }
}
contract C is B {
constructor() public { x = 3; }
}
contract D is C {
constructor() public {
assert(x == 3);
assert(x == 2);
}
}
// ----
// Warning: (232-246): Assertion violation happens here

21
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_alternate.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract A {
uint x = 1;
}
contract B is A {
constructor() public { x = 2; }
}
contract C is B {
}
contract D is C {
constructor() public {
assert(x == 2);
assert(x == 3);
}
}
// ----
// Warning: (199-213): Assertion violation happens here

27
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol Normal file
View File

@ -0,0 +1,27 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract B is C {
uint b;
constructor(uint x) public {
b = a + x;
}
}
contract A is B {
constructor(uint x) B(x) C(x + 2) public {
assert(a == x + 2);
assert(b == x + x + 2);
assert(a == x + 5);
}
}
// ----
// Warning: (162-167): Underflow (resulting value less than 0) happens here
// Warning: (162-167): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (287-305): Assertion violation happens here

26
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol Normal file
View File

@ -0,0 +1,26 @@
pragma experimental SMTChecker;
contract C {
uint a;
constructor(uint x) public {
a = x;
}
}
contract B is C {
uint b;
constructor(uint x) public {
b = x + 10;
}
}
contract A is B {
constructor(uint x) B(x) C(x + 2) public {
assert(a == x + 2);
assert(b == x + 10);
assert(b == x + 5);
}
}
// ----
// Warning: (162-168): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (285-303): Assertion violation happens here

20
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract A {
uint x = 2;
}
contract B is A {
}
contract C is A {
}
contract D is B, C {
constructor() public {
assert(x == 2);
assert(x == 3);
}
}
// ----
// Warning: (169-183): Assertion violation happens here

22
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol Normal file
View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract A {
uint x = 1;
}
contract B is A {
constructor() public { x = 2; }
}
contract C is A {
constructor() public { x = 3; }
}
contract D is B, C {
constructor() public {
assert(x == 3);
assert(x == 4);
}
}
// ----
// Warning: (235-249): Assertion violation happens here

17
test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_function_call.sol Normal file
View File

@ -0,0 +1,17 @@
pragma experimental SMTChecker;
contract C {
uint x = f(2);
constructor () public {
assert(x == 2);
}
function f(uint y) internal view returns (uint) {
assert(y > 0);
assert(x == 0);
return y;
}
}
// ----
// Warning: (162-175): Assertion violation happens here
// Warning: (179-193): Assertion violation happens here

2
test/libsolidity/smtCheckerTests/inheritance/functions_1.sol
View File

@ -15,7 +15,7 @@ contract A {
// 2 warnings, B.f and A.g
contract B is A {
function f() public view {
assert(x == 0);
assert(x == 1);
}
}
// ----

2
test/libsolidity/smtCheckerTests/inheritance/functions_2.sol
View File

@ -17,7 +17,7 @@ contract B is A {
uint y;
function f() public view {
assert(x == 0);
assert(x == 1);
}
}
// ----

8
test/libsolidity/smtCheckerTests/inheritance/functions_3.sol
View File

@ -17,10 +17,10 @@ contract B is A {
uint y;
function f() public view {
assert(x == 0);
assert(x == 1);
}
function h() public view {
assert(x == 2);
assert(x == 1);
}
}
@ -29,10 +29,10 @@ contract C is B {
uint z;
function f() public view {
assert(x == 0);
assert(x == 1);
}
function i() public view {
assert(x == 0);
assert(x == 1);
}
}
// ----

16
test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract A {
uint x;
constructor (uint y) public { assert(x == 0); x = y; }
}
contract B is A {
constructor () A(2) public { assert(x == 2); }
}
contract C is B {
function f() public view {
assert(x == 2);
}
}

20
test/libsolidity/smtCheckerTests/inheritance/implicit_only_constructor_hierarchy.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract A {
uint x;
function h() public view {
assert(x == 0);
}
}
contract B is A {
function g() public view {
assert(x == 0);
}
}
contract C is B {
function f() public view {
assert(x == 0);
}
}