mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #9648 from ethereum/smt_refactor_predicates
[SMTChecker] Refactor CHC predicates
This commit is contained in:
commit
0d83977d5a
@ -100,6 +100,8 @@ set(sources
|
|||||||
formal/EncodingContext.h
|
formal/EncodingContext.h
|
||||||
formal/ModelChecker.cpp
|
formal/ModelChecker.cpp
|
||||||
formal/ModelChecker.h
|
formal/ModelChecker.h
|
||||||
|
formal/Predicate.cpp
|
||||||
|
formal/Predicate.h
|
||||||
formal/SMTEncoder.cpp
|
formal/SMTEncoder.cpp
|
||||||
formal/SMTEncoder.h
|
formal/SMTEncoder.h
|
||||||
formal/SSAVariable.cpp
|
formal/SSAVariable.cpp
|
||||||
|
@ -29,7 +29,6 @@
|
|||||||
#include <libsmtutil/CHCSmtLib2Interface.h>
|
#include <libsmtutil/CHCSmtLib2Interface.h>
|
||||||
#include <libsolutil/Algorithms.h>
|
#include <libsolutil/Algorithms.h>
|
||||||
|
|
||||||
#include <boost/algorithm/string/join.hpp>
|
|
||||||
#include <boost/range/adaptor/reversed.hpp>
|
#include <boost/range/adaptor/reversed.hpp>
|
||||||
|
|
||||||
#include <queue>
|
#include <queue>
|
||||||
@ -85,11 +84,7 @@ void CHC::analyze(SourceUnit const& _source)
|
|||||||
|
|
||||||
resetSourceAnalysis();
|
resetSourceAnalysis();
|
||||||
|
|
||||||
auto genesisSort = make_shared<smtutil::FunctionSort>(
|
m_genesisPredicate = createSymbolicBlock(arity0FunctionSort(), "genesis");
|
||||||
vector<smtutil::SortPointer>(),
|
|
||||||
smtutil::SortProvider::boolSort
|
|
||||||
);
|
|
||||||
m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
|
|
||||||
addRule(genesis(), "genesis");
|
addRule(genesis(), "genesis");
|
||||||
|
|
||||||
set<SourceUnit const*, IdCompare> sources;
|
set<SourceUnit const*, IdCompare> sources;
|
||||||
@ -118,16 +113,14 @@ bool CHC::visit(ContractDefinition const& _contract)
|
|||||||
|
|
||||||
initContract(_contract);
|
initContract(_contract);
|
||||||
|
|
||||||
m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
|
m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
|
||||||
m_stateSorts = stateSorts(_contract);
|
m_stateSorts = stateSorts(_contract);
|
||||||
|
|
||||||
clearIndices(&_contract);
|
clearIndices(&_contract);
|
||||||
|
|
||||||
string suffix = _contract.name() + "_" + to_string(_contract.id());
|
string suffix = _contract.name() + "_" + to_string(_contract.id());
|
||||||
m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_" + suffix);
|
m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix, &_contract);
|
||||||
m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix);
|
m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix, &_contract);
|
||||||
m_symbolFunction[m_constructorSummaryPredicate->currentFunctionValue().name] = &_contract;
|
|
||||||
m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix);
|
|
||||||
auto stateExprs = currentStateVariables();
|
auto stateExprs = currentStateVariables();
|
||||||
setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
|
setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
|
||||||
|
|
||||||
@ -233,7 +226,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
|
|||||||
if (_function.isConstructor())
|
if (_function.isConstructor())
|
||||||
{
|
{
|
||||||
string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
|
string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
|
||||||
auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
|
auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix, m_currentContract);
|
||||||
connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
|
connectBlocks(m_currentBlock, predicate(*constructorExit, currentFunctionVariables(*m_currentContract)));
|
||||||
|
|
||||||
clearIndices(m_currentContract, m_currentFunction);
|
clearIndices(m_currentContract, m_currentFunction);
|
||||||
@ -326,8 +319,8 @@ bool CHC::visit(WhileStatement const& _while)
|
|||||||
|
|
||||||
auto outerBreakDest = m_breakDest;
|
auto outerBreakDest = m_breakDest;
|
||||||
auto outerContinueDest = m_continueDest;
|
auto outerContinueDest = m_continueDest;
|
||||||
m_breakDest = afterLoopBlock.get();
|
m_breakDest = afterLoopBlock;
|
||||||
m_continueDest = loopHeaderBlock.get();
|
m_continueDest = loopHeaderBlock;
|
||||||
|
|
||||||
if (_while.isDoWhile())
|
if (_while.isDoWhile())
|
||||||
_while.body().accept(*this);
|
_while.body().accept(*this);
|
||||||
@ -377,8 +370,8 @@ bool CHC::visit(ForStatement const& _for)
|
|||||||
|
|
||||||
auto outerBreakDest = m_breakDest;
|
auto outerBreakDest = m_breakDest;
|
||||||
auto outerContinueDest = m_continueDest;
|
auto outerContinueDest = m_continueDest;
|
||||||
m_breakDest = afterLoopBlock.get();
|
m_breakDest = afterLoopBlock;
|
||||||
m_continueDest = postLoop ? postLoopBlock.get() : loopHeaderBlock.get();
|
m_continueDest = postLoop ? postLoopBlock : loopHeaderBlock;
|
||||||
|
|
||||||
if (auto init = _for.initializationExpression())
|
if (auto init = _for.initializationExpression())
|
||||||
init->accept(*this);
|
init->accept(*this);
|
||||||
@ -571,7 +564,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
|
|||||||
m_context.variable(*var)->increaseIndex();
|
m_context.variable(*var)->increaseIndex();
|
||||||
|
|
||||||
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
|
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
|
||||||
m_symbolFunction[nondet.name] = &_funCall;
|
|
||||||
m_context.addAssertion(nondet);
|
m_context.addAssertion(nondet);
|
||||||
|
|
||||||
m_context.addAssertion(m_error.currentValue() == 0);
|
m_context.addAssertion(m_error.currentValue() == 0);
|
||||||
@ -681,7 +673,9 @@ void CHC::resetSourceAnalysis()
|
|||||||
m_errorIds.clear();
|
m_errorIds.clear();
|
||||||
m_callGraph.clear();
|
m_callGraph.clear();
|
||||||
m_summaries.clear();
|
m_summaries.clear();
|
||||||
m_symbolFunction.clear();
|
m_interfaces.clear();
|
||||||
|
m_nondetInterfaces.clear();
|
||||||
|
Predicate::reset();
|
||||||
}
|
}
|
||||||
|
|
||||||
void CHC::resetContractAnalysis()
|
void CHC::resetContractAnalysis()
|
||||||
@ -717,7 +711,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
|
|||||||
}
|
}
|
||||||
|
|
||||||
void CHC::setCurrentBlock(
|
void CHC::setCurrentBlock(
|
||||||
smt::SymbolicFunctionVariable const& _block,
|
Predicate const& _block,
|
||||||
vector<smtutil::Expression> const* _arguments
|
vector<smtutil::Expression> const* _arguments
|
||||||
)
|
)
|
||||||
{
|
{
|
||||||
@ -743,24 +737,10 @@ set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTN
|
|||||||
return assertions;
|
return assertions;
|
||||||
}
|
}
|
||||||
|
|
||||||
vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
|
|
||||||
{
|
|
||||||
return fold(
|
|
||||||
_contract.annotation().linearizedBaseContracts,
|
|
||||||
vector<VariableDeclaration const*>{},
|
|
||||||
[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
|
|
||||||
);
|
|
||||||
}
|
|
||||||
|
|
||||||
vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
|
|
||||||
{
|
|
||||||
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
|
|
||||||
}
|
|
||||||
|
|
||||||
vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
|
vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
|
||||||
{
|
{
|
||||||
return applyMap(
|
return applyMap(
|
||||||
stateVariablesIncludingInheritedAndPrivate(_contract),
|
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
|
||||||
[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
|
[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
@ -806,7 +786,7 @@ smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contrac
|
|||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
smtutil::SortPointer CHC::arity0FunctionSort()
|
smtutil::SortPointer CHC::arity0FunctionSort() const
|
||||||
{
|
{
|
||||||
return make_shared<smtutil::FunctionSort>(
|
return make_shared<smtutil::FunctionSort>(
|
||||||
vector<smtutil::SortPointer>(),
|
vector<smtutil::SortPointer>(),
|
||||||
@ -853,7 +833,7 @@ smtutil::SortPointer CHC::sort(ASTNode const* _node)
|
|||||||
|
|
||||||
smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
||||||
{
|
{
|
||||||
auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
|
auto stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
|
||||||
auto sorts = stateSorts(_contract);
|
auto sorts = stateSorts(_contract);
|
||||||
|
|
||||||
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
|
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
|
||||||
@ -870,14 +850,10 @@ smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, Contr
|
|||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smtutil::SortPointer _sort, string const& _name)
|
Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, ASTNode const* _node)
|
||||||
{
|
{
|
||||||
auto block = make_unique<smt::SymbolicFunctionVariable>(
|
auto const* block = Predicate::create(_sort, _name, m_context, _node);
|
||||||
_sort,
|
m_interface->registerRelation(block->functor());
|
||||||
_name,
|
|
||||||
m_context
|
|
||||||
);
|
|
||||||
m_interface->registerRelation(block->currentFunctionValue());
|
|
||||||
return block;
|
return block;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -887,20 +863,24 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
|
|||||||
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
|
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
|
||||||
for (auto const* base: contract->annotation().linearizedBaseContracts)
|
for (auto const* base: contract->annotation().linearizedBaseContracts)
|
||||||
{
|
{
|
||||||
string suffix = base->name() + "_" + to_string(base->id());
|
for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base))
|
||||||
m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix);
|
|
||||||
m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix);
|
|
||||||
|
|
||||||
for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
|
|
||||||
if (!m_context.knownVariable(*var))
|
if (!m_context.knownVariable(*var))
|
||||||
createVariable(*var);
|
createVariable(*var);
|
||||||
|
|
||||||
/// Base nondeterministic interface that allows
|
if (!m_interfaces.count(base))
|
||||||
/// 0 steps to be taken, used as base for the inductive
|
{
|
||||||
/// rule for each function.
|
solAssert(!m_nondetInterfaces.count(base), "");
|
||||||
auto const& iface = *m_nondetInterfaces.at(base);
|
string suffix = base->name() + "_" + to_string(base->id());
|
||||||
auto state0 = stateVariablesAtIndex(0, *base);
|
m_interfaces.emplace(base, createSymbolicBlock(interfaceSort(*base), "interface_" + suffix, base));
|
||||||
addRule(iface(state0 + state0), "base_nondet");
|
m_nondetInterfaces.emplace(base, createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix, base));
|
||||||
|
|
||||||
|
/// Base nondeterministic interface that allows
|
||||||
|
/// 0 steps to be taken, used as base for the inductive
|
||||||
|
/// rule for each function.
|
||||||
|
auto const* iface = m_nondetInterfaces.at(base);
|
||||||
|
auto state0 = stateVariablesAtIndex(0, *base);
|
||||||
|
addRule((*iface)(state0 + state0), "base_nondet");
|
||||||
|
}
|
||||||
|
|
||||||
for (auto const* function: base->definedFunctions())
|
for (auto const* function: base->definedFunctions())
|
||||||
{
|
{
|
||||||
@ -923,8 +903,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
|
|||||||
auto state1 = stateVariablesAtIndex(1, *base);
|
auto state1 = stateVariablesAtIndex(1, *base);
|
||||||
auto state2 = stateVariablesAtIndex(2, *base);
|
auto state2 = stateVariablesAtIndex(2, *base);
|
||||||
|
|
||||||
auto nondetPre = iface(state0 + state1);
|
auto const* iface = m_nondetInterfaces.at(base);
|
||||||
auto nondetPost = iface(state0 + state2);
|
auto state0 = stateVariablesAtIndex(0, *base);
|
||||||
|
auto nondetPre = (*iface)(state0 + state1);
|
||||||
|
auto nondetPost = (*iface)(state0 + state2);
|
||||||
|
|
||||||
vector<smtutil::Expression> args{m_error.currentValue()};
|
vector<smtutil::Expression> args{m_error.currentValue()};
|
||||||
args += state1 +
|
args += state1 +
|
||||||
@ -960,7 +942,7 @@ smtutil::Expression CHC::error()
|
|||||||
|
|
||||||
smtutil::Expression CHC::error(unsigned _idx)
|
smtutil::Expression CHC::error(unsigned _idx)
|
||||||
{
|
{
|
||||||
return m_errorPredicate->functionValueAtIndex(_idx)({});
|
return m_errorPredicate->functor(_idx)({});
|
||||||
}
|
}
|
||||||
|
|
||||||
smtutil::Expression CHC::summary(ContractDefinition const& _contract)
|
smtutil::Expression CHC::summary(ContractDefinition const& _contract)
|
||||||
@ -994,37 +976,33 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function)
|
|||||||
return summary(_function, *m_currentContract);
|
return summary(_function, *m_currentContract);
|
||||||
}
|
}
|
||||||
|
|
||||||
unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
|
Predicate const* CHC::createBlock(ASTNode const* _node, string const& _prefix)
|
||||||
{
|
{
|
||||||
auto block = createSymbolicBlock(sort(_node),
|
auto block = createSymbolicBlock(
|
||||||
"block_" +
|
sort(_node),
|
||||||
uniquePrefix() +
|
"block_" + uniquePrefix() + "_" + _prefix + predicateName(_node),
|
||||||
"_" +
|
_node
|
||||||
_prefix +
|
);
|
||||||
predicateName(_node));
|
|
||||||
|
|
||||||
solAssert(m_currentFunction, "");
|
solAssert(m_currentFunction, "");
|
||||||
m_symbolFunction[block->currentFunctionValue().name] = m_currentFunction;
|
|
||||||
return block;
|
return block;
|
||||||
}
|
}
|
||||||
|
|
||||||
unique_ptr<smt::SymbolicFunctionVariable> CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
||||||
{
|
{
|
||||||
auto block = createSymbolicBlock(summarySort(_function, _contract),
|
auto block = createSymbolicBlock(
|
||||||
"summary_" +
|
summarySort(_function, _contract),
|
||||||
uniquePrefix() +
|
"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
|
||||||
"_" +
|
&_function
|
||||||
predicateName(&_function, &_contract));
|
);
|
||||||
|
|
||||||
m_symbolFunction[block->currentFunctionValue().name] = &_function;
|
|
||||||
return block;
|
return block;
|
||||||
}
|
}
|
||||||
|
|
||||||
void CHC::createErrorBlock()
|
void CHC::createErrorBlock()
|
||||||
{
|
{
|
||||||
solAssert(m_errorPredicate, "");
|
m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()));
|
||||||
m_errorPredicate->increaseIndex();
|
m_interface->registerRelation(m_errorPredicate->functor());
|
||||||
m_interface->registerRelation(m_errorPredicate->currentFunctionValue());
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints)
|
void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints)
|
||||||
@ -1055,7 +1033,7 @@ vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
|
|||||||
vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
|
vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
|
||||||
{
|
{
|
||||||
return applyMap(
|
return applyMap(
|
||||||
stateVariablesIncludingInheritedAndPrivate(_contract),
|
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
|
||||||
[&](auto _var) { return valueAtIndex(*_var, _index); }
|
[&](auto _var) { return valueAtIndex(*_var, _index); }
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
@ -1068,7 +1046,7 @@ vector<smtutil::Expression> CHC::currentStateVariables()
|
|||||||
|
|
||||||
vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
|
vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
|
||||||
{
|
{
|
||||||
return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
|
return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
|
||||||
}
|
}
|
||||||
|
|
||||||
vector<smtutil::Expression> CHC::currentFunctionVariables()
|
vector<smtutil::Expression> CHC::currentFunctionVariables()
|
||||||
@ -1128,13 +1106,13 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
|
|||||||
return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
|
return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
|
||||||
}
|
}
|
||||||
|
|
||||||
smtutil::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
|
smtutil::Expression CHC::predicate(Predicate const& _block)
|
||||||
{
|
{
|
||||||
return _block(currentBlockVariables());
|
return _block(currentBlockVariables());
|
||||||
}
|
}
|
||||||
|
|
||||||
smtutil::Expression CHC::predicate(
|
smtutil::Expression CHC::predicate(
|
||||||
smt::SymbolicFunctionVariable const& _block,
|
Predicate const& _block,
|
||||||
vector<smtutil::Expression> const& _arguments
|
vector<smtutil::Expression> const& _arguments
|
||||||
)
|
)
|
||||||
{
|
{
|
||||||
@ -1425,42 +1403,31 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
|
|||||||
solAssert(edges.size() <= 2, "");
|
solAssert(edges.size() <= 2, "");
|
||||||
|
|
||||||
unsigned summaryId = edges.at(0);
|
unsigned summaryId = edges.at(0);
|
||||||
|
|
||||||
optional<unsigned> interfaceId;
|
optional<unsigned> interfaceId;
|
||||||
if (edges.size() == 2)
|
if (edges.size() == 2)
|
||||||
{
|
{
|
||||||
interfaceId = edges.at(1);
|
interfaceId = edges.at(1);
|
||||||
if (_graph.nodes.at(summaryId).first.rfind("summary", 0) != 0)
|
if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary())
|
||||||
swap(summaryId, *interfaceId);
|
swap(summaryId, *interfaceId);
|
||||||
solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, "");
|
auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
|
||||||
|
solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
|
||||||
}
|
}
|
||||||
/// The children are unordered, so we need to check which is the summary and
|
/// The children are unordered, so we need to check which is the summary and
|
||||||
/// which is the interface.
|
/// which is the interface.
|
||||||
|
|
||||||
solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, "");
|
Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first);
|
||||||
|
solAssert(summaryPredicate && summaryPredicate->isSummary(), "");
|
||||||
/// At this point property 2 from the function description is verified for this node.
|
/// At this point property 2 from the function description is verified for this node.
|
||||||
|
auto summaryArgs = _graph.nodes.at(summaryId).second;
|
||||||
|
|
||||||
auto const& summaryNode = _graph.nodes.at(summaryId);
|
FunctionDefinition const* calledFun = summaryPredicate->programFunction();
|
||||||
solAssert(m_symbolFunction.count(summaryNode.first), "");
|
ContractDefinition const* calledContract = summaryPredicate->programContract();
|
||||||
|
|
||||||
FunctionDefinition const* calledFun = nullptr;
|
|
||||||
ContractDefinition const* calledContract = nullptr;
|
|
||||||
if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_symbolFunction.at(summaryNode.first)))
|
|
||||||
{
|
|
||||||
if (auto const* constructor = contract->constructor())
|
|
||||||
calledFun = constructor;
|
|
||||||
else
|
|
||||||
calledContract = contract;
|
|
||||||
}
|
|
||||||
else if (auto const* fun = dynamic_cast<FunctionDefinition const*>(m_symbolFunction.at(summaryNode.first)))
|
|
||||||
calledFun = fun;
|
|
||||||
else
|
|
||||||
solAssert(false, "");
|
|
||||||
|
|
||||||
solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
|
solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
|
||||||
auto const& stateVars = calledFun ? stateVariablesIncludingInheritedAndPrivate(*calledFun) : stateVariablesIncludingInheritedAndPrivate(*calledContract);
|
auto stateVars = summaryPredicate->stateVariables();
|
||||||
/// calledContract != nullptr implies that the constructor of the analyzed contract is implicit and
|
solAssert(stateVars.has_value(), "");
|
||||||
/// therefore takes no parameters.
|
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
|
||||||
|
solAssert(stateValues.size() == stateVars->size(), "");
|
||||||
|
|
||||||
/// This summary node is the end of a tx.
|
/// This summary node is the end of a tx.
|
||||||
/// If it is the first summary node seen in this loop, it is the summary
|
/// If it is the first summary node seen in this loop, it is the summary
|
||||||
@ -1470,36 +1437,23 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
|
|||||||
{
|
{
|
||||||
lastTxSeen = true;
|
lastTxSeen = true;
|
||||||
/// Generate counterexample message local to the failed target.
|
/// Generate counterexample message local to the failed target.
|
||||||
localState = formatStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n";
|
localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
|
||||||
if (calledFun)
|
if (calledFun)
|
||||||
{
|
{
|
||||||
/// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
|
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
|
||||||
auto const& inParams = calledFun->parameters();
|
auto const& inParams = calledFun->parameters();
|
||||||
unsigned initLocals = stateVars.size() * 2 + 1 + inParams.size();
|
localState += formatVariableModel(inParams, inValues, "\n") + "\n";
|
||||||
/// In this loop we are interested in postInputVars.
|
auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
|
||||||
for (unsigned i = initLocals; i < initLocals + inParams.size(); ++i)
|
|
||||||
{
|
|
||||||
auto param = inParams.at(i - initLocals);
|
|
||||||
if (param->type()->isValueType())
|
|
||||||
localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
|
|
||||||
}
|
|
||||||
auto const& outParams = calledFun->returnParameters();
|
auto const& outParams = calledFun->returnParameters();
|
||||||
initLocals += inParams.size();
|
localState += formatVariableModel(outParams, outValues, "\n") + "\n";
|
||||||
/// In this loop we are interested in outputVars.
|
|
||||||
for (unsigned i = initLocals; i < initLocals + outParams.size(); ++i)
|
|
||||||
{
|
|
||||||
auto param = outParams.at(i - initLocals);
|
|
||||||
if (param->type()->isValueType())
|
|
||||||
localState += param->name() + " = " + summaryNode.second.at(i) + "\n";
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
/// We report the state after every tx in the trace except for the last, which is reported
|
/// We report the state after every tx in the trace except for the last, which is reported
|
||||||
/// first in the code above.
|
/// first in the code above.
|
||||||
path.emplace_back("State: " + formatStateCounterexample(stateVars, calledFun, summaryNode.second));
|
path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", "));
|
||||||
|
|
||||||
string txCex = calledContract ? "constructor()" : formatFunctionCallCounterexample(stateVars, *calledFun, summaryNode.second);
|
string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
|
||||||
path.emplace_back(txCex);
|
path.emplace_back(txCex);
|
||||||
|
|
||||||
/// Recurse on the next interface node which represents the previous transaction
|
/// Recurse on the next interface node which represents the previous transaction
|
||||||
@ -1513,66 +1467,6 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
|
|||||||
return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
|
return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
string CHC::formatStateCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const* _function, vector<string> const& _summaryValues)
|
|
||||||
{
|
|
||||||
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
|
|
||||||
/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
|
|
||||||
/// Here we are interested in postStateVars.
|
|
||||||
vector<string>::const_iterator stateFirst;
|
|
||||||
vector<string>::const_iterator stateLast;
|
|
||||||
if (_function)
|
|
||||||
{
|
|
||||||
stateFirst = _summaryValues.begin() + 1 + static_cast<int>(_stateVars.size()) + static_cast<int>(_function->parameters().size());
|
|
||||||
stateLast = stateFirst + static_cast<int>(_stateVars.size());
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
stateFirst = _summaryValues.begin() + 1;
|
|
||||||
stateLast = stateFirst + static_cast<int>(_stateVars.size());
|
|
||||||
}
|
|
||||||
|
|
||||||
solAssert(stateFirst >= _summaryValues.begin() && stateFirst <= _summaryValues.end(), "");
|
|
||||||
solAssert(stateLast >= _summaryValues.begin() && stateLast <= _summaryValues.end(), "");
|
|
||||||
vector<string> stateArgs(stateFirst, stateLast);
|
|
||||||
solAssert(stateArgs.size() == _stateVars.size(), "");
|
|
||||||
|
|
||||||
vector<string> stateCex;
|
|
||||||
for (unsigned i = 0; i < stateArgs.size(); ++i)
|
|
||||||
{
|
|
||||||
auto var = _stateVars.at(i);
|
|
||||||
if (var->type()->isValueType())
|
|
||||||
stateCex.emplace_back(var->name() + " = " + stateArgs.at(i));
|
|
||||||
}
|
|
||||||
|
|
||||||
return boost::algorithm::join(stateCex, ", ");
|
|
||||||
}
|
|
||||||
|
|
||||||
string CHC::formatFunctionCallCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const& _function, vector<string> const& _summaryValues)
|
|
||||||
{
|
|
||||||
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
|
|
||||||
/// Here we are interested in preInputVars.
|
|
||||||
vector<string>::const_iterator first = _summaryValues.begin() + static_cast<int>(_stateVars.size()) + 1;
|
|
||||||
vector<string>::const_iterator last = first + static_cast<int>(_function.parameters().size());
|
|
||||||
solAssert(first >= _summaryValues.begin() && first <= _summaryValues.end(), "");
|
|
||||||
solAssert(last >= _summaryValues.begin() && last <= _summaryValues.end(), "");
|
|
||||||
vector<string> functionArgsCex(first, last);
|
|
||||||
vector<string> functionArgs;
|
|
||||||
|
|
||||||
auto const& params = _function.parameters();
|
|
||||||
solAssert(params.size() == functionArgsCex.size(), "");
|
|
||||||
for (unsigned i = 0; i < params.size(); ++i)
|
|
||||||
if (params[i]->type()->isValueType())
|
|
||||||
functionArgs.emplace_back(functionArgsCex[i]);
|
|
||||||
else
|
|
||||||
functionArgs.emplace_back(params[i]->name());
|
|
||||||
|
|
||||||
string fName = _function.isConstructor() ? "constructor" :
|
|
||||||
_function.isFallback() ? "fallback" :
|
|
||||||
_function.isReceive() ? "receive" :
|
|
||||||
_function.name();
|
|
||||||
return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
|
|
||||||
}
|
|
||||||
|
|
||||||
string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
|
string CHC::cex2dot(smtutil::CHCSolverInterface::CexGraph const& _cex)
|
||||||
{
|
{
|
||||||
string dot = "digraph {\n";
|
string dot = "digraph {\n";
|
||||||
|
@ -31,12 +31,15 @@
|
|||||||
|
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
||||||
|
#include <libsolidity/formal/Predicate.h>
|
||||||
#include <libsolidity/formal/SMTEncoder.h>
|
#include <libsolidity/formal/SMTEncoder.h>
|
||||||
|
|
||||||
#include <libsolidity/interface/ReadFile.h>
|
#include <libsolidity/interface/ReadFile.h>
|
||||||
|
|
||||||
#include <libsmtutil/CHCSolverInterface.h>
|
#include <libsmtutil/CHCSolverInterface.h>
|
||||||
|
|
||||||
|
#include <boost/algorithm/string/join.hpp>
|
||||||
|
|
||||||
#include <map>
|
#include <map>
|
||||||
#include <optional>
|
#include <optional>
|
||||||
#include <set>
|
#include <set>
|
||||||
@ -108,10 +111,8 @@ private:
|
|||||||
void resetContractAnalysis();
|
void resetContractAnalysis();
|
||||||
void eraseKnowledge();
|
void eraseKnowledge();
|
||||||
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
|
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
|
||||||
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
|
void setCurrentBlock(Predicate const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
|
||||||
std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
|
std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
|
||||||
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
|
|
||||||
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
|
|
||||||
//@}
|
//@}
|
||||||
|
|
||||||
/// Sort helpers.
|
/// Sort helpers.
|
||||||
@ -122,7 +123,7 @@ private:
|
|||||||
smtutil::SortPointer nondetInterfaceSort();
|
smtutil::SortPointer nondetInterfaceSort();
|
||||||
static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
|
static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
|
||||||
static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const);
|
static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const);
|
||||||
smtutil::SortPointer arity0FunctionSort();
|
smtutil::SortPointer arity0FunctionSort() const;
|
||||||
smtutil::SortPointer sort(FunctionDefinition const& _function);
|
smtutil::SortPointer sort(FunctionDefinition const& _function);
|
||||||
smtutil::SortPointer sort(ASTNode const* _block);
|
smtutil::SortPointer sort(ASTNode const* _block);
|
||||||
/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
|
/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
|
||||||
@ -134,7 +135,7 @@ private:
|
|||||||
/// Predicate helpers.
|
/// Predicate helpers.
|
||||||
//@{
|
//@{
|
||||||
/// @returns a new block of given _sort and _name.
|
/// @returns a new block of given _sort and _name.
|
||||||
std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name);
|
Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, ASTNode const* _node = nullptr);
|
||||||
|
|
||||||
/// Creates summary predicates for all functions of all contracts
|
/// Creates summary predicates for all functions of all contracts
|
||||||
/// in a given _source.
|
/// in a given _source.
|
||||||
@ -150,10 +151,10 @@ private:
|
|||||||
smtutil::Expression error(unsigned _idx);
|
smtutil::Expression error(unsigned _idx);
|
||||||
|
|
||||||
/// Creates a block for the given _node.
|
/// Creates a block for the given _node.
|
||||||
std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
|
Predicate const* createBlock(ASTNode const* _node, std::string const& _prefix = "");
|
||||||
/// Creates a call block for the given function _function from contract _contract.
|
/// Creates a call block for the given function _function from contract _contract.
|
||||||
/// The contract is needed here because of inheritance.
|
/// The contract is needed here because of inheritance.
|
||||||
std::unique_ptr<smt::SymbolicFunctionVariable> createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
|
Predicate const* createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
|
||||||
|
|
||||||
/// Creates a new error block to be used by an assertion.
|
/// Creates a new error block to be used by an assertion.
|
||||||
/// Also registers the predicate.
|
/// Also registers the predicate.
|
||||||
@ -184,9 +185,9 @@ private:
|
|||||||
/// @returns the predicate name for a given node.
|
/// @returns the predicate name for a given node.
|
||||||
std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
|
std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
|
||||||
/// @returns a predicate application over the current scoped variables.
|
/// @returns a predicate application over the current scoped variables.
|
||||||
smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block);
|
smtutil::Expression predicate(Predicate const& _block);
|
||||||
/// @returns a predicate application over @param _arguments.
|
/// @returns a predicate application over @param _arguments.
|
||||||
smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const& _arguments);
|
smtutil::Expression predicate(Predicate const& _block, std::vector<smtutil::Expression> const& _arguments);
|
||||||
/// @returns the summary predicate for the called function.
|
/// @returns the summary predicate for the called function.
|
||||||
smtutil::Expression predicate(FunctionCall const& _funCall);
|
smtutil::Expression predicate(FunctionCall const& _funCall);
|
||||||
/// @returns a predicate that defines a constructor summary.
|
/// @returns a predicate that defines a constructor summary.
|
||||||
@ -222,15 +223,23 @@ private:
|
|||||||
);
|
);
|
||||||
|
|
||||||
std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root);
|
std::optional<std::string> generateCounterexample(smtutil::CHCSolverInterface::CexGraph const& _graph, std::string const& _root);
|
||||||
/// @returns values for the _stateVariables after a transaction calling
|
|
||||||
/// _function was executed.
|
/// @returns a set of pairs _var = _value separated by _separator.
|
||||||
/// _function = nullptr means the transaction was the deployment of a
|
template <typename T>
|
||||||
/// contract without an explicit constructor.
|
std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::string> const& _values, std::string const& _separator) const
|
||||||
std::string formatStateCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const* _function, std::vector<std::string> const& _summaryValues);
|
{
|
||||||
/// @returns a formatted text representing a call to _function
|
solAssert(_variables.size() == _values.size(), "");
|
||||||
/// with the concrete values for value type parameters and
|
|
||||||
/// the parameter name for reference types.
|
std::vector<std::string> assignments;
|
||||||
std::string formatFunctionCallCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const& _function, std::vector<std::string> const& _summaryValues);
|
for (unsigned i = 0; i < _values.size(); ++i)
|
||||||
|
{
|
||||||
|
auto var = _variables.at(i);
|
||||||
|
if (var && var->type()->isValueType())
|
||||||
|
assignments.emplace_back(var->name() + " = " + _values.at(i));
|
||||||
|
}
|
||||||
|
|
||||||
|
return boost::algorithm::join(assignments, _separator);
|
||||||
|
}
|
||||||
|
|
||||||
/// @returns a DAG in the dot format.
|
/// @returns a DAG in the dot format.
|
||||||
/// Used for debugging purposes.
|
/// Used for debugging purposes.
|
||||||
@ -251,32 +260,32 @@ private:
|
|||||||
/// Predicates.
|
/// Predicates.
|
||||||
//@{
|
//@{
|
||||||
/// Genesis predicate.
|
/// Genesis predicate.
|
||||||
std::unique_ptr<smt::SymbolicFunctionVariable> m_genesisPredicate;
|
Predicate const* m_genesisPredicate = nullptr;
|
||||||
|
|
||||||
/// Implicit constructor predicate.
|
/// Implicit constructor predicate.
|
||||||
/// Explicit constructors are handled as functions.
|
/// Explicit constructors are handled as functions.
|
||||||
std::unique_ptr<smt::SymbolicFunctionVariable> m_implicitConstructorPredicate;
|
Predicate const* m_implicitConstructorPredicate = nullptr;
|
||||||
|
|
||||||
/// Constructor summary predicate, exists after the constructor
|
/// Constructor summary predicate, exists after the constructor
|
||||||
/// (implicit or explicit) and before the interface.
|
/// (implicit or explicit) and before the interface.
|
||||||
std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorSummaryPredicate;
|
Predicate const* m_constructorSummaryPredicate = nullptr;
|
||||||
|
|
||||||
/// Artificial Interface predicate.
|
/// Artificial Interface predicate.
|
||||||
/// Single entry block for all functions.
|
/// Single entry block for all functions.
|
||||||
std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_interfaces;
|
std::map<ContractDefinition const*, Predicate const*> m_interfaces;
|
||||||
|
|
||||||
/// Nondeterministic interfaces.
|
/// Nondeterministic interfaces.
|
||||||
/// These are used when the analyzed contract makes external calls to unknown code,
|
/// These are used when the analyzed contract makes external calls to unknown code,
|
||||||
/// which means that the analyzed contract can potentially be called
|
/// which means that the analyzed contract can potentially be called
|
||||||
/// nondeterministically.
|
/// nondeterministically.
|
||||||
std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_nondetInterfaces;
|
std::map<ContractDefinition const*, Predicate const*> m_nondetInterfaces;
|
||||||
|
|
||||||
/// Artificial Error predicate.
|
/// Artificial Error predicate.
|
||||||
/// Single error block for all assertions.
|
/// Single error block for all assertions.
|
||||||
std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;
|
Predicate const* m_errorPredicate = nullptr;
|
||||||
|
|
||||||
/// Function predicates.
|
/// Function predicates.
|
||||||
std::map<ContractDefinition const*, std::map<FunctionDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>>> m_summaries;
|
std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries;
|
||||||
|
|
||||||
smt::SymbolicIntVariable m_error{
|
smt::SymbolicIntVariable m_error{
|
||||||
TypeProvider::uint256(),
|
TypeProvider::uint256(),
|
||||||
@ -337,9 +346,9 @@ private:
|
|||||||
bool m_unknownFunctionCallSeen = false;
|
bool m_unknownFunctionCallSeen = false;
|
||||||
|
|
||||||
/// Block where a loop break should go to.
|
/// Block where a loop break should go to.
|
||||||
smt::SymbolicFunctionVariable const* m_breakDest = nullptr;
|
Predicate const* m_breakDest;
|
||||||
/// Block where a loop continue should go to.
|
/// Block where a loop continue should go to.
|
||||||
smt::SymbolicFunctionVariable const* m_continueDest = nullptr;
|
Predicate const* m_continueDest;
|
||||||
//@}
|
//@}
|
||||||
|
|
||||||
/// CHC solver.
|
/// CHC solver.
|
||||||
|
260
libsolidity/formal/Predicate.cpp
Normal file
260
libsolidity/formal/Predicate.cpp
Normal file
@ -0,0 +1,260 @@
|
|||||||
|
/*
|
||||||
|
This file is part of solidity.
|
||||||
|
|
||||||
|
solidity is free software: you can redistribute it and/or modify
|
||||||
|
it under the terms of the GNU General Public License as published by
|
||||||
|
the Free Software Foundation, either version 3 of the License, or
|
||||||
|
(at your option) any later version.
|
||||||
|
|
||||||
|
solidity is distributed in the hope that it will be useful,
|
||||||
|
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||||
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||||
|
GNU General Public License for more details.
|
||||||
|
|
||||||
|
You should have received a copy of the GNU General Public License
|
||||||
|
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
*/
|
||||||
|
// SPDX-License-Identifier: GPL-3.0
|
||||||
|
|
||||||
|
#include <libsolidity/formal/Predicate.h>
|
||||||
|
|
||||||
|
#include <libsolidity/formal/SMTEncoder.h>
|
||||||
|
|
||||||
|
#include <libsolidity/ast/AST.h>
|
||||||
|
|
||||||
|
#include <boost/algorithm/string/join.hpp>
|
||||||
|
#include <utility>
|
||||||
|
|
||||||
|
using namespace std;
|
||||||
|
using namespace solidity;
|
||||||
|
using namespace solidity::smtutil;
|
||||||
|
using namespace solidity::frontend;
|
||||||
|
using namespace solidity::frontend::smt;
|
||||||
|
|
||||||
|
map<string, Predicate> Predicate::m_predicates;
|
||||||
|
|
||||||
|
Predicate const* Predicate::create(
|
||||||
|
SortPointer _sort,
|
||||||
|
string _name,
|
||||||
|
EncodingContext& _context,
|
||||||
|
ASTNode const* _node
|
||||||
|
)
|
||||||
|
{
|
||||||
|
smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context};
|
||||||
|
string functorName = predicate.currentName();
|
||||||
|
solAssert(!m_predicates.count(functorName), "");
|
||||||
|
return &m_predicates.emplace(
|
||||||
|
std::piecewise_construct,
|
||||||
|
std::forward_as_tuple(functorName),
|
||||||
|
std::forward_as_tuple(move(predicate), _node)
|
||||||
|
).first->second;
|
||||||
|
}
|
||||||
|
|
||||||
|
Predicate::Predicate(
|
||||||
|
smt::SymbolicFunctionVariable&& _predicate,
|
||||||
|
ASTNode const* _node
|
||||||
|
):
|
||||||
|
m_predicate(move(_predicate)),
|
||||||
|
m_node(_node)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
Predicate const* Predicate::predicate(string const& _name)
|
||||||
|
{
|
||||||
|
return &m_predicates.at(_name);
|
||||||
|
}
|
||||||
|
|
||||||
|
void Predicate::reset()
|
||||||
|
{
|
||||||
|
m_predicates.clear();
|
||||||
|
}
|
||||||
|
|
||||||
|
smtutil::Expression Predicate::operator()(vector<smtutil::Expression> const& _args) const
|
||||||
|
{
|
||||||
|
return m_predicate(_args);
|
||||||
|
}
|
||||||
|
|
||||||
|
smtutil::Expression Predicate::functor() const
|
||||||
|
{
|
||||||
|
return m_predicate.currentFunctionValue();
|
||||||
|
}
|
||||||
|
|
||||||
|
smtutil::Expression Predicate::functor(unsigned _idx) const
|
||||||
|
{
|
||||||
|
return m_predicate.functionValueAtIndex(_idx);
|
||||||
|
}
|
||||||
|
|
||||||
|
void Predicate::newFunctor()
|
||||||
|
{
|
||||||
|
m_predicate.increaseIndex();
|
||||||
|
}
|
||||||
|
|
||||||
|
ASTNode const* Predicate::programNode() const
|
||||||
|
{
|
||||||
|
return m_node;
|
||||||
|
}
|
||||||
|
|
||||||
|
ContractDefinition const* Predicate::programContract() const
|
||||||
|
{
|
||||||
|
if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
|
||||||
|
if (!contract->constructor())
|
||||||
|
return contract;
|
||||||
|
|
||||||
|
return nullptr;
|
||||||
|
}
|
||||||
|
|
||||||
|
FunctionDefinition const* Predicate::programFunction() const
|
||||||
|
{
|
||||||
|
if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_node))
|
||||||
|
{
|
||||||
|
if (contract->constructor())
|
||||||
|
return contract->constructor();
|
||||||
|
return nullptr;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (auto const* fun = dynamic_cast<FunctionDefinition const*>(m_node))
|
||||||
|
return fun;
|
||||||
|
|
||||||
|
return nullptr;
|
||||||
|
}
|
||||||
|
|
||||||
|
optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
|
||||||
|
{
|
||||||
|
if (auto const* fun = programFunction())
|
||||||
|
return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
|
||||||
|
if (auto const* contract = programContract())
|
||||||
|
return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract);
|
||||||
|
|
||||||
|
auto const* node = m_node;
|
||||||
|
while (auto const* scopable = dynamic_cast<Scopable const*>(node))
|
||||||
|
{
|
||||||
|
node = scopable->scope();
|
||||||
|
if (auto const* fun = dynamic_cast<FunctionDefinition const*>(node))
|
||||||
|
return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun);
|
||||||
|
}
|
||||||
|
|
||||||
|
return nullopt;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool Predicate::isSummary() const
|
||||||
|
{
|
||||||
|
return functor().name.rfind("summary", 0) == 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool Predicate::isInterface() const
|
||||||
|
{
|
||||||
|
return functor().name.rfind("interface", 0) == 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
string Predicate::formatSummaryCall(vector<string> const& _args) const
|
||||||
|
{
|
||||||
|
if (programContract())
|
||||||
|
return "constructor()";
|
||||||
|
|
||||||
|
solAssert(isSummary(), "");
|
||||||
|
|
||||||
|
auto stateVars = stateVariables();
|
||||||
|
solAssert(stateVars.has_value(), "");
|
||||||
|
auto const* fun = programFunction();
|
||||||
|
solAssert(fun, "");
|
||||||
|
|
||||||
|
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
|
||||||
|
/// Here we are interested in preInputVars.
|
||||||
|
vector<string>::const_iterator first = _args.begin() + static_cast<int>(stateVars->size()) + 1;
|
||||||
|
vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
|
||||||
|
solAssert(first >= _args.begin() && first <= _args.end(), "");
|
||||||
|
solAssert(last >= _args.begin() && last <= _args.end(), "");
|
||||||
|
vector<string> functionArgsCex(first, last);
|
||||||
|
vector<string> functionArgs;
|
||||||
|
|
||||||
|
auto const& params = fun->parameters();
|
||||||
|
solAssert(params.size() == functionArgsCex.size(), "");
|
||||||
|
for (unsigned i = 0; i < params.size(); ++i)
|
||||||
|
if (params[i]->type()->isValueType())
|
||||||
|
functionArgs.emplace_back(functionArgsCex[i]);
|
||||||
|
else
|
||||||
|
functionArgs.emplace_back(params[i]->name());
|
||||||
|
|
||||||
|
string fName = fun->isConstructor() ? "constructor" :
|
||||||
|
fun->isFallback() ? "fallback" :
|
||||||
|
fun->isReceive() ? "receive" :
|
||||||
|
fun->name();
|
||||||
|
return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
|
||||||
|
{
|
||||||
|
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
|
||||||
|
/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
|
||||||
|
/// Here we are interested in postStateVars.
|
||||||
|
|
||||||
|
auto stateVars = stateVariables();
|
||||||
|
solAssert(stateVars.has_value(), "");
|
||||||
|
|
||||||
|
vector<string>::const_iterator stateFirst;
|
||||||
|
vector<string>::const_iterator stateLast;
|
||||||
|
if (auto const* function = programFunction())
|
||||||
|
{
|
||||||
|
stateFirst = _args.begin() + 1 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size());
|
||||||
|
stateLast = stateFirst + static_cast<int>(stateVars->size());
|
||||||
|
}
|
||||||
|
else if (programContract())
|
||||||
|
{
|
||||||
|
stateFirst = _args.begin() + 1;
|
||||||
|
stateLast = stateFirst + static_cast<int>(stateVars->size());
|
||||||
|
}
|
||||||
|
else
|
||||||
|
solAssert(false, "");
|
||||||
|
|
||||||
|
solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), "");
|
||||||
|
solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), "");
|
||||||
|
|
||||||
|
vector<string> stateArgs(stateFirst, stateLast);
|
||||||
|
solAssert(stateArgs.size() == stateVars->size(), "");
|
||||||
|
return stateArgs;
|
||||||
|
}
|
||||||
|
|
||||||
|
vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
|
||||||
|
{
|
||||||
|
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
|
||||||
|
/// Here we are interested in postInputVars.
|
||||||
|
auto const* function = programFunction();
|
||||||
|
solAssert(function, "");
|
||||||
|
|
||||||
|
auto stateVars = stateVariables();
|
||||||
|
solAssert(stateVars.has_value(), "");
|
||||||
|
|
||||||
|
auto const& inParams = function->parameters();
|
||||||
|
|
||||||
|
vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size());
|
||||||
|
vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
|
||||||
|
|
||||||
|
solAssert(first >= _args.begin() && first <= _args.end(), "");
|
||||||
|
solAssert(last >= _args.begin() && last <= _args.end(), "");
|
||||||
|
|
||||||
|
vector<string> inValues(first, last);
|
||||||
|
solAssert(inValues.size() == inParams.size(), "");
|
||||||
|
return inValues;
|
||||||
|
}
|
||||||
|
|
||||||
|
vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
|
||||||
|
{
|
||||||
|
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
|
||||||
|
/// Here we are interested in outputVars.
|
||||||
|
auto const* function = programFunction();
|
||||||
|
solAssert(function, "");
|
||||||
|
|
||||||
|
auto stateVars = stateVariables();
|
||||||
|
solAssert(stateVars.has_value(), "");
|
||||||
|
|
||||||
|
auto const& inParams = function->parameters();
|
||||||
|
|
||||||
|
vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2;
|
||||||
|
|
||||||
|
solAssert(first >= _args.begin() && first <= _args.end(), "");
|
||||||
|
|
||||||
|
vector<string> outValues(first, _args.end());
|
||||||
|
solAssert(outValues.size() == function->returnParameters().size(), "");
|
||||||
|
return outValues;
|
||||||
|
}
|
120
libsolidity/formal/Predicate.h
Normal file
120
libsolidity/formal/Predicate.h
Normal file
@ -0,0 +1,120 @@
|
|||||||
|
/*
|
||||||
|
This file is part of solidity.
|
||||||
|
|
||||||
|
solidity is free software: you can redistribute it and/or modify
|
||||||
|
it under the terms of the GNU General Public License as published by
|
||||||
|
the Free Software Foundation, either version 3 of the License, or
|
||||||
|
(at your option) any later version.
|
||||||
|
|
||||||
|
solidity is distributed in the hope that it will be useful,
|
||||||
|
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||||
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||||
|
GNU General Public License for more details.
|
||||||
|
|
||||||
|
You should have received a copy of the GNU General Public License
|
||||||
|
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
*/
|
||||||
|
// SPDX-License-Identifier: GPL-3.0
|
||||||
|
|
||||||
|
#pragma once
|
||||||
|
|
||||||
|
#include <libsolidity/formal/SymbolicVariables.h>
|
||||||
|
#include <libsolidity/formal/SymbolicVariables.h>
|
||||||
|
|
||||||
|
#include <libsmtutil/Sorts.h>
|
||||||
|
|
||||||
|
#include <map>
|
||||||
|
#include <optional>
|
||||||
|
#include <vector>
|
||||||
|
|
||||||
|
namespace solidity::frontend
|
||||||
|
{
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Represents a predicate used by the CHC engine.
|
||||||
|
*/
|
||||||
|
class Predicate
|
||||||
|
{
|
||||||
|
public:
|
||||||
|
static Predicate const* create(
|
||||||
|
smtutil::SortPointer _sort,
|
||||||
|
std::string _name,
|
||||||
|
smt::EncodingContext& _context,
|
||||||
|
ASTNode const* _node = nullptr
|
||||||
|
);
|
||||||
|
|
||||||
|
Predicate(
|
||||||
|
smt::SymbolicFunctionVariable&& _predicate,
|
||||||
|
ASTNode const* _node = nullptr
|
||||||
|
);
|
||||||
|
|
||||||
|
/// Predicate should not be copiable.
|
||||||
|
Predicate(Predicate const&) = delete;
|
||||||
|
Predicate& operator=(Predicate const&) = delete;
|
||||||
|
|
||||||
|
/// @returns the Predicate associated with _name.
|
||||||
|
static Predicate const* predicate(std::string const& _name);
|
||||||
|
|
||||||
|
/// Resets all the allocated predicates.
|
||||||
|
static void reset();
|
||||||
|
|
||||||
|
/// @returns a function application of the predicate over _args.
|
||||||
|
smtutil::Expression operator()(std::vector<smtutil::Expression> const& _args) const;
|
||||||
|
|
||||||
|
/// @returns the function declaration of the predicate.
|
||||||
|
smtutil::Expression functor() const;
|
||||||
|
/// @returns the function declaration of the predicate with index _idx.
|
||||||
|
smtutil::Expression functor(unsigned _idx) const;
|
||||||
|
/// Increases the index of the function declaration of the predicate.
|
||||||
|
void newFunctor();
|
||||||
|
|
||||||
|
/// @returns the program node this predicate represents.
|
||||||
|
ASTNode const* programNode() const;
|
||||||
|
|
||||||
|
/// @returns the ContractDefinition that this predicate represents
|
||||||
|
/// or nullptr otherwise.
|
||||||
|
ContractDefinition const* programContract() const;
|
||||||
|
|
||||||
|
/// @returns the FunctionDefinition that this predicate represents
|
||||||
|
/// or nullptr otherwise.
|
||||||
|
FunctionDefinition const* programFunction() const;
|
||||||
|
|
||||||
|
/// @returns the program state variables in the scope of this predicate.
|
||||||
|
std::optional<std::vector<VariableDeclaration const*>> stateVariables() const;
|
||||||
|
|
||||||
|
/// @returns true if this predicate represents a summary.
|
||||||
|
bool isSummary() const;
|
||||||
|
|
||||||
|
/// @returns true if this predicate represents an interface.
|
||||||
|
bool isInterface() const;
|
||||||
|
|
||||||
|
/// @returns a formatted string representing a call to this predicate
|
||||||
|
/// with _args.
|
||||||
|
std::string formatSummaryCall(std::vector<std::string> const& _args) const;
|
||||||
|
|
||||||
|
/// @returns the values of the state variables from _args at the point
|
||||||
|
/// where this summary was reached.
|
||||||
|
std::vector<std::string> summaryStateValues(std::vector<std::string> const& _args) const;
|
||||||
|
|
||||||
|
/// @returns the values of the function input variables from _args at the point
|
||||||
|
/// where this summary was reached.
|
||||||
|
std::vector<std::string> summaryPostInputValues(std::vector<std::string> const& _args) const;
|
||||||
|
|
||||||
|
/// @returns the values of the function output variables from _args at the point
|
||||||
|
/// where this summary was reached.
|
||||||
|
std::vector<std::string> summaryPostOutputValues(std::vector<std::string> const& _args) const;
|
||||||
|
|
||||||
|
private:
|
||||||
|
/// The actual SMT expression.
|
||||||
|
smt::SymbolicFunctionVariable m_predicate;
|
||||||
|
|
||||||
|
/// The ASTNode that this predicate represents.
|
||||||
|
/// nullptr if this predicate is not associated with a specific program AST node.
|
||||||
|
ASTNode const* m_node = nullptr;
|
||||||
|
|
||||||
|
/// Maps the name of the predicate to the actual Predicate.
|
||||||
|
/// Used in counterexample generation.
|
||||||
|
static std::map<std::string, Predicate> m_predicates;
|
||||||
|
};
|
||||||
|
|
||||||
|
}
|
@ -1985,6 +1985,20 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
|
|||||||
return funDef;
|
return funDef;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
|
||||||
|
{
|
||||||
|
return fold(
|
||||||
|
_contract.annotation().linearizedBaseContracts,
|
||||||
|
vector<VariableDeclaration const*>{},
|
||||||
|
[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
|
||||||
|
{
|
||||||
|
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
|
||||||
|
}
|
||||||
|
|
||||||
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
|
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
|
||||||
{
|
{
|
||||||
FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
|
FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
|
||||||
|
@ -62,6 +62,9 @@ public:
|
|||||||
/// if possible or nullptr.
|
/// if possible or nullptr.
|
||||||
static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);
|
static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);
|
||||||
|
|
||||||
|
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
|
||||||
|
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
// TODO: Check that we do not have concurrent reads and writes to a variable,
|
// TODO: Check that we do not have concurrent reads and writes to a variable,
|
||||||
// because the order of expression evaluation is undefined
|
// because the order of expression evaluation is undefined
|
||||||
|
@ -21,5 +21,5 @@ contract C
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ----
|
// ----
|
||||||
// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here
|
// Warning 4984: (203-208): Overflow (resulting value larger than 2**256 - 1) happens here.
|
||||||
// Warning 6328: (136-149): Assertion violation happens here
|
// Warning 6328: (136-149): Assertion violation happens here
|
||||||
|
@ -26,4 +26,4 @@ contract C
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ----
|
// ----
|
||||||
// Warning 6328: (400-457): Assertion violation happens here.
|
// Warning 6328: (400-457): Assertion violation happens here
|
||||||
|
Loading…
Reference in New Issue
Block a user