Skip to content

Commit

Permalink
Merge pull request #7490 from ethereum/smt_constructor
Browse files Browse the repository at this point in the history 
[SMTChecker] Add support to constructors
  • Loading branch information
@chriseth
chriseth committed Nov 28, 2019
2 parents 301215f + a352abe commit 912a0e2
Show file tree
Hide file tree
Showing 46 changed files with 1,048 additions and 169 deletions.
1 change: 1 addition & 0 deletions Changelog.md
View file
Expand Up @@ -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.

Expand Down
26 changes: 16 additions & 10 deletions libsolidity/formal/BMC.cpp
View file
Expand Up @@ -110,18 +110,24 @@ 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;
}

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);
}

Expand All @@ -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);
Expand Down Expand Up @@ -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);
}

Expand Down
182 changes: 101 additions & 81 deletions libsolidity/formal/CHC.cpp
View file
Expand Up @@ -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);
}

Expand Down Expand Up @@ -94,38 +103,22 @@ 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);
auto errorFunctionSort = make_shared<smt::FunctionSort>(
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;
Expand All @@ -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);
Expand All @@ -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;

Expand All @@ -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;
Expand All @@ -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);
}

Expand Down Expand Up @@ -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;
}
Expand All @@ -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()
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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::currentFunctionVariables()
vector<smt::Expression> CHC::currentStateVariables()
{
solAssert(m_currentFunction, "");
vector<smt::Expression> paramExprs;
solAssert(m_currentContract, "");
vector<smt::Expression> exprs;
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;
exprs.push_back(m_context.variable(*var)->currentValue());
return exprs;
}

vector<smt::Expression> CHC::currentBlockVariables()
vector<smt::Expression> CHC::currentFunctionVariables()
{
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;
if (m_currentFunction)
for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters())
paramExprs.push_back(m_context.variable(*var)->currentValue());
return currentStateVariables() + paramExprs;
}

void CHC::clearIndices()
vector<smt::Expression> CHC::currentBlockVariables()
{
for (auto const& var: m_stateVariables)
m_context.variable(*var)->resetIndex();
vector<smt::Expression> paramExprs;
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)
Expand Down Expand Up @@ -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);
Expand Down

0 comments on commit 912a0e2

Please sign in to comment.