cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #8311 from ethereum/smt_split_2

Browse Source 
[SMTChecker] Change CHC encoding from explicit CFG to function forests
This commit is contained in:
Leonardo 2020-03-03 13:16:14 +01:00 committed by GitHub
commit 32ca1a5e26
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
13 changed files with 426 additions and 116 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

385
libsolidity/formal/CHC.cpp
View File

@ -27,6 +27,8 @@
#include <libsolidity/ast/TypeProvider.h>
#include <libsolutil/Algorithms.h>
using namespace std;
using namespace solidity;
using namespace solidity::langutil;
@ -75,16 +77,39 @@ void CHC::analyze(SourceUnit const& _source)
m_context.setAssertionAccumulation(false);
m_variableUsage.setFunctionInlining(false);
resetSourceAnalysis();
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);
addRule(genesis(), "genesis");
_source.accept(*this);
set<SourceUnit const*, IdCompare> sources;
sources.insert(&_source);
for (auto const& source: _source.referencedSourceUnits(true))
sources.insert(source);
for (auto const* source: sources)
defineInterfacesAndSummaries(*source);
for (auto const* source: sources)
source->accept(*this);
for (auto const& [scope, target]: m_verificationTargets)
{
auto assertions = transactionAssertions(scope);
for (auto const* assertion: assertions)
{
createErrorBlock();
connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
auto [result, model] = query(error(), assertion->location());
// This should be fine but it's a bug in the old compiler
(void)model;
if (result == smt::CheckResult::UNSATISFIABLE)
m_safeAssertions.insert(assertion);
}
}
}
vector<string> CHC::unhandledQueries() const
@ -97,26 +122,15 @@ vector<string> CHC::unhandledQueries() const
bool CHC::visit(ContractDefinition const& _contract)
{
if (!shouldVisit(_contract))
return false;
reset();
resetContractAnalysis();
initContract(_contract);
m_stateVariables = _contract.stateVariablesIncludingInherited();
for (auto const& var: m_stateVariables)
// SMT solvers do not support function types as arguments.
if (var->type()->category() == Type::Category::Function)
m_stateSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
else
m_stateSorts.push_back(smt::smtSort(*var->type()));
m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
m_stateSorts = stateSorts(_contract);
clearIndices(&_contract);
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);
@ -125,10 +139,12 @@ bool CHC::visit(ContractDefinition const& _contract)
boolSort
);
string suffix = _contract.name() + "_" + to_string(_contract.id());
m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error_" + suffix);
m_constructorPredicate = createSymbolicBlock(constructorSort(), "implicit_constructor_" + to_string(_contract.id()));
m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix);
m_implicitConstructorPredicate = createSymbolicBlock(interfaceSort(), "implicit_constructor_" + suffix);
auto stateExprs = currentStateVariables();
setCurrentBlock(*m_interfacePredicate, &stateExprs);
setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
SMTEncoder::visit(_contract);
return false;
@ -136,33 +152,33 @@ bool CHC::visit(ContractDefinition const& _contract)
void CHC::endVisit(ContractDefinition const& _contract)
{
if (!shouldVisit(_contract))
return;
for (auto const& var: m_stateVariables)
{
solAssert(m_context.knownVariable(*var), "");
auto const& symbVar = m_context.variable(*var);
symbVar->resetIndex();
m_context.setZeroValue(*var);
symbVar->increaseIndex();
}
auto genesisPred = (*m_genesisPredicate)({});
auto implicitConstructor = (*m_constructorPredicate)(currentStateVariables());
connectBlocks(genesisPred, implicitConstructor);
auto implicitConstructor = (*m_implicitConstructorPredicate)(initialStateVariables());
connectBlocks(genesis(), implicitConstructor);
m_currentBlock = implicitConstructor;
m_context.addAssertion(m_error.currentValue() == 0);
if (auto constructor = _contract.constructor())
constructor->accept(*this);
else
inlineConstructorHierarchy(_contract);
connectBlocks(m_currentBlock, interface());
auto summary = predicate(*m_constructorSummaryPredicate, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables());
connectBlocks(m_currentBlock, summary);
for (unsigned i = 0; i < m_verificationTargets.size(); ++i)
{
auto const& target = m_verificationTargets.at(i);
auto errorAppl = error(i + 1);
if (query(errorAppl, target->location()))
m_safeAssertions.insert(target);
}
clearIndices(m_currentContract, nullptr);
auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
addVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
SMTEncoder::endVisit(_contract);
}
@ -182,7 +198,7 @@ bool CHC::visit(FunctionDefinition const& _function)
return false;
}
solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
solAssert(!m_currentFunction, "Function inlining should not happen in CHC.");
m_currentFunction = &_function;
initFunction(_function);
@ -193,7 +209,17 @@ bool CHC::visit(FunctionDefinition const& _function)
auto functionPred = predicate(*functionEntryBlock, currentFunctionVariables());
auto bodyPred = predicate(*bodyBlock);
connectBlocks(m_currentBlock, functionPred);
if (_function.isConstructor())
connectBlocks(m_currentBlock, functionPred);
else
connectBlocks(genesis(), functionPred);
m_context.addAssertion(m_error.currentValue() == 0);
for (auto const* var: m_stateVariables)
m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
for (auto const& var: _function.parameters())
m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
connectBlocks(functionPred, bodyPred);
setCurrentBlock(*bodyBlock);
@ -225,18 +251,30 @@ void CHC::endVisit(FunctionDefinition const& _function)
// This is done in endVisit(ContractDefinition).
if (_function.isConstructor())
{
auto constructorExit = createSymbolicBlock(interfaceSort(), "constructor_exit_" + to_string(_function.id()));
connectBlocks(m_currentBlock, predicate(*constructorExit, currentStateVariables()));
string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables()));
clearIndices(m_currentContract, m_currentFunction);
auto stateExprs = currentStateVariables();
auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
setCurrentBlock(*constructorExit, &stateExprs);
}
else
{
connectBlocks(m_currentBlock, interface());
clearIndices(m_currentContract, m_currentFunction);
auto stateExprs = currentStateVariables();
setCurrentBlock(*m_interfacePredicate, &stateExprs);
auto assertionError = m_error.currentValue();
auto sum = summary(_function);
connectBlocks(m_currentBlock, sum);
auto iface = interface();
auto stateExprs = initialStateVariables();
setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
if (_function.isPublic())
{
addVerificationTarget(&_function, m_currentBlock, sum, assertionError);
connectBlocks(m_currentBlock, iface, sum && (assertionError == 0));
}
}
m_currentFunction = nullptr;
}
@ -468,12 +506,23 @@ void CHC::visitAssert(FunctionCall const& _funCall)
solAssert(args.size() == 1, "");
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
createErrorBlock();
solAssert(m_currentContract, "");
solAssert(m_currentFunction, "");
if (m_currentFunction->isConstructor())
m_functionAssertions[m_currentContract].insert(&_funCall);
else
m_functionAssertions[m_currentFunction].insert(&_funCall);
smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue());
connectBlocks(m_currentBlock, error(), currentPathConditions() && assertNeg);
auto previousError = m_error.currentValue();
m_error.increaseIndex();
m_verificationTargets.push_back(&_funCall);
connectBlocks(
m_currentBlock,
m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
currentPathConditions() && !m_context.expression(*args.front())->currentValue() && (m_error.currentValue() == _funCall.id())
);
m_context.addAssertion(m_error.currentValue() == previousError);
}
void CHC::unknownFunctionCall(FunctionCall const&)
@ -488,15 +537,23 @@ void CHC::unknownFunctionCall(FunctionCall const&)
m_unknownFunctionCallSeen = true;
}
void CHC::reset()
void CHC::resetSourceAnalysis()
{
m_verificationTargets.clear();
m_safeAssertions.clear();
m_functionAssertions.clear();
m_callGraph.clear();
m_summaries.clear();
}
void CHC::resetContractAnalysis()
{
m_stateSorts.clear();
m_stateVariables.clear();
m_verificationTargets.clear();
m_safeAssertions.clear();
m_unknownFunctionCallSeen = false;
m_breakDest = nullptr;
m_continueDest = nullptr;
m_error.resetIndex();
}
void CHC::eraseKnowledge()
@ -521,17 +578,6 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
}
}
bool CHC::shouldVisit(ContractDefinition const& _contract) const
{
if (
_contract.isLibrary() ||
_contract.isInterface()
)
return false;
return true;
}
bool CHC::shouldVisit(FunctionDefinition const& _function) const
{
if (
@ -547,7 +593,8 @@ void CHC::setCurrentBlock(
vector<smt::Expression> const* _arguments
)
{
m_context.popSolver();
if (m_context.solverStackHeigh() > 0)
m_context.popSolver();
solAssert(m_currentContract, "");
clearIndices(m_currentContract, m_currentFunction);
m_context.pushSolver();
@ -557,10 +604,42 @@ void CHC::setCurrentBlock(
m_currentBlock = predicate(_block);
}
set<Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
{
set<Expression const*, IdCompare> assertions;
solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
assertions.insert(m_functionAssertions[function].begin(), m_functionAssertions[function].end());
for (auto const* called: m_callGraph[function])
_addChild(called);
});
return assertions;
}
vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
{
vector<VariableDeclaration const*> stateVars;
for (auto const& contract: _contract.annotation().linearizedBaseContracts)
for (auto var: contract->stateVariables())
stateVars.push_back(var);
return stateVars;
}
vector<smt::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
{
vector<smt::SortPointer> stateSorts;
for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract))
stateSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
return stateSorts;
}
smt::SortPointer CHC::constructorSort()
{
// TODO this will change once we support function calls.
return interfaceSort();
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
return make_shared<smt::FunctionSort>(
vector<smt::SortPointer>{intSort} + m_stateSorts,
boolSort
);
}
smt::SortPointer CHC::interfaceSort()
@ -572,20 +651,38 @@ smt::SortPointer CHC::interfaceSort()
);
}
smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
{
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
return make_shared<smt::FunctionSort>(
stateSorts(_contract),
boolSort
);
}
/// A function in the symbolic CFG requires:
/// - Index of failed assertion. 0 means no assertion failed.
/// - 2 sets of state variables:
/// - State variables at the beginning of the current function, immutable
/// - Current state variables
/// At the beginning of the function these must equal set 1
/// - 2 sets of input variables:
/// - Input variables at the beginning of the current function, immutable
/// - Current input variables
/// At the beginning of the function these must equal set 1
/// - 1 set of output variables
smt::SortPointer CHC::sort(FunctionDefinition const& _function)
{
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
vector<smt::SortPointer> varSorts;
for (auto const& var: _function.parameters() + _function.returnParameters())
{
// SMT solvers do not support function types as arguments.
if (var->type()->category() == Type::Category::Function)
varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
else
varSorts.push_back(smt::smtSort(*var->type()));
}
auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
vector<smt::SortPointer> inputSorts;
for (auto const& var: _function.parameters())
inputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
vector<smt::SortPointer> outputSorts;
for (auto const& var: _function.returnParameters())
outputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
return make_shared<smt::FunctionSort>(
m_stateSorts + varSorts,
vector<smt::SortPointer>{intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
boolSort
);
}
@ -601,19 +698,31 @@ smt::SortPointer CHC::sort(ASTNode const* _node)
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
vector<smt::SortPointer> varSorts;
for (auto const& var: m_currentFunction->localVariables())
{
// SMT solvers do not support function types as arguments.
if (var->type()->category() == Type::Category::Function)
varSorts.push_back(make_shared<smt::Sort>(smt::Kind::Int));
else
varSorts.push_back(smt::smtSort(*var->type()));
}
varSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
return make_shared<smt::FunctionSort>(
fSort->domain + varSorts,
boolSort
);
}
smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
auto sorts = stateSorts(_contract);
auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
vector<smt::SortPointer> inputSorts, outputSorts;
for (auto const& var: _function.parameters())
inputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
for (auto const& var: _function.returnParameters())
outputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
return make_shared<smt::FunctionSort>(
vector<smt::SortPointer>{intSort} + sorts + inputSorts + sorts + outputSorts,
boolSort
);
}
unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
{
auto block = make_unique<smt::SymbolicFunctionVariable>(
@ -625,12 +734,33 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPoin
return block;
}
void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
{
for (auto const& node: _source.nodes())
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
for (auto const* base: contract->annotation().linearizedBaseContracts)
{
string suffix = base->name() + "_" + to_string(base->id());
m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix);
for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
if (!m_context.knownVariable(*var))
createVariable(*var);
for (auto const* function: base->definedFunctions())
m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
}
}
smt::Expression CHC::interface()
{
vector<smt::Expression> paramExprs;
for (auto const& var: m_stateVariables)
paramExprs.push_back(m_context.variable(*var)->currentValue());
return (*m_interfacePredicate)(paramExprs);
return (*m_interfaces.at(m_currentContract))(paramExprs);
}
smt::Expression CHC::interface(ContractDefinition const& _contract)
{
return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract));
}
smt::Expression CHC::error()
@ -643,6 +773,27 @@ smt::Expression CHC::error(unsigned _idx)
return m_errorPredicate->functionValueAtIndex(_idx)({});
}
smt::Expression CHC::summary(ContractDefinition const&)
{
return (*m_constructorSummaryPredicate)(
vector<smt::Expression>{m_error.currentValue()} +
currentStateVariables()
);
}
smt::Expression CHC::summary(FunctionDefinition const& _function)
{
vector<smt::Expression> args{m_error.currentValue()};
auto contract = _function.annotation().contract;
args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables();
for (auto const& var: _function.parameters())
args.push_back(m_context.variable(*var)->valueAtIndex(0));
args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
for (auto const& var: _function.returnParameters())
args.push_back(m_context.variable(*var)->currentValue());
return (*m_summaries.at(m_currentContract).at(&_function))(args);
}
unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
{
return createSymbolicBlock(sort(_node),
@ -653,6 +804,15 @@ unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node,
predicateName(_node));
}
unique_ptr<smt::SymbolicFunctionVariable> CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
return createSymbolicBlock(summarySort(_function, _contract),
"summary_" +
uniquePrefix() +
"_" +
predicateName(&_function, &_contract));
}
void CHC::createErrorBlock()
{
solAssert(m_errorPredicate, "");
@ -669,6 +829,28 @@ void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to
addRule(edge, _from.name + "_to_" + _to.name);
}
vector<smt::Expression> CHC::initialStateVariables()
{
return stateVariablesAtIndex(0);
}
vector<smt::Expression> CHC::stateVariablesAtIndex(int _index)
{
solAssert(m_currentContract, "");
vector<smt::Expression> exprs;
for (auto const& var: m_stateVariables)
exprs.push_back(m_context.variable(*var)->valueAtIndex(_index));
return exprs;
}
vector<smt::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
{
vector<smt::Expression> exprs;
for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract))
exprs.push_back(m_context.variable(*var)->valueAtIndex(_index));
return exprs;
}
vector<smt::Expression> CHC::currentStateVariables()
{
solAssert(m_currentContract, "");
@ -680,11 +862,22 @@ vector<smt::Expression> CHC::currentStateVariables()
vector<smt::Expression> CHC::currentFunctionVariables()
{
vector<smt::Expression> 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> initInputExprs;
vector<smt::Expression> mutableInputExprs;
for (auto const& var: m_currentFunction->parameters())
{
initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
}
vector<smt::Expression> returnExprs;
for (auto const& var: m_currentFunction->returnParameters())
returnExprs.push_back(m_context.variable(*var)->currentValue());
return vector<smt::Expression>{m_error.currentValue()} +
initialStateVariables() +
initInputExprs +
currentStateVariables() +
mutableInputExprs +
returnExprs;
}
vector<smt::Expression> CHC::currentBlockVariables()
@ -696,7 +889,7 @@ vector<smt::Expression> CHC::currentBlockVariables()
return currentFunctionVariables() + paramExprs;
}
string CHC::predicateName(ASTNode const* _node)
string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract)
{
string prefix;
if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
@ -705,7 +898,12 @@ string CHC::predicateName(ASTNode const* _node)
if (!funDef->name().empty())
prefix += "_" + funDef->name() + "_";
}
return prefix + to_string(_node->id());
else if (m_currentFunction && !m_currentFunction->name().empty())
prefix += m_currentFunction->name();
auto contract = _contract ? _contract : m_currentContract;
solAssert(contract, "");
return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
}
smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
@ -726,7 +924,7 @@ void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
m_interface->addRule(_rule, _ruleName);
}
bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
{
smt::CheckResult result;
vector<string> values;
@ -736,7 +934,7 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _
case smt::CheckResult::SATISFIABLE:
break;
case smt::CheckResult::UNSATISFIABLE:
return true;
break;
case smt::CheckResult::UNKNOWN:
break;
case smt::CheckResult::CONFLICTING:
@ -746,7 +944,12 @@ bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _
m_outerErrorReporter.warning(_location, "Error trying to invoke SMT solver.");
break;
}
return false;
return {result, values};
}
void CHC::addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
{
m_verificationTargets.emplace(_scope, CHCVerificationTarget{{VerificationTarget::Type::Assert, _from, _constraints}, _errorId});
}
string CHC::uniquePrefix()

77
libsolidity/formal/CHC.h
View File

@ -79,22 +79,38 @@ private:
void unknownFunctionCall(FunctionCall const& _funCall);
//@}
struct IdCompare
{
bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
{
return lhs->id() < rhs->id();
}
};
/// Helpers.
//@{
void reset();
void resetSourceAnalysis();
void resetContractAnalysis();
void eraseKnowledge();
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
bool shouldVisit(ContractDefinition const& _contract) const;
bool shouldVisit(FunctionDefinition const& _function) const;
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
//@}
/// Sort helpers.
//@{
static std::vector<smt::SortPointer> stateSorts(ContractDefinition const& _contract);
smt::SortPointer constructorSort();
smt::SortPointer interfaceSort();
static smt::SortPointer interfaceSort(ContractDefinition const& _const);
smt::SortPointer sort(FunctionDefinition const& _function);
smt::SortPointer sort(ASTNode const* _block);
/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
/// The _contract is also needed because the same function might be in many contracts due to inheritance,
/// where the sort changes because the set of state variables might change.
static smt::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract);
//@}
/// Predicate helpers.
@ -102,14 +118,24 @@ private:
/// @returns a new block of given _sort and _name.
std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
/// Creates summary predicates for all functions of all contracts
/// in a given _source.
void defineInterfacesAndSummaries(SourceUnit const& _source);
/// Genesis predicate.
smt::Expression genesis() { return (*m_genesisPredicate)({}); }
/// Interface predicate over current variables.
smt::Expression interface();
smt::Expression interface(ContractDefinition const& _contract);
/// Error predicate over current variables.
smt::Expression error();
smt::Expression error(unsigned _idx);
/// Creates a block for the given _node.
std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
/// Creates a call block for the given function _function from contract _contract.
/// The contract is needed here because of inheritance.
std::unique_ptr<smt::SymbolicFunctionVariable> createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// Creates a new error block to be used by an assertion.
/// Also registers the predicate.
@ -117,6 +143,11 @@ private:
void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
/// @returns the symbolic values of the state variables at the beginning
/// of the current transaction.
std::vector<smt::Expression> initialStateVariables();
std::vector<smt::Expression> stateVariablesAtIndex(int _index);
std::vector<smt::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
/// @returns the current symbolic values of the current state variables.
std::vector<smt::Expression> currentStateVariables();
@ -128,19 +159,26 @@ private:
std::vector<smt::Expression> currentBlockVariables();
/// @returns the predicate name for a given node.
std::string predicateName(ASTNode const* _node);
std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
/// @returns a predicate application over the current scoped variables.
smt::Expression predicate(smt::SymbolicFunctionVariable const& _block);
/// @returns a predicate application over @param _arguments.
smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const& _arguments);
/// @returns a predicate that defines a constructor summary.
smt::Expression summary(ContractDefinition const& _contract);
/// @returns a predicate that defines a function summary.
smt::Expression summary(FunctionDefinition const& _function);
//@}
/// Solver related.
//@{
/// Adds Horn rule to the solver.
void addRule(smt::Expression const& _rule, std::string const& _ruleName);
/// @returns true if query is unsatisfiable (safe).
bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
/// @returns <true, empty> if query is unsatisfiable (safe).
/// @returns <false, model> otherwise.
std::pair<smt::CheckResult, std::vector<std::string>> query(smt::Expression const& _query, langutil::SourceLocation const& _location);
void addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
//@}
/// Misc.
@ -157,15 +195,29 @@ private:
/// Implicit constructor predicate.
/// Explicit constructors are handled as functions.
std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorPredicate;
std::unique_ptr<smt::SymbolicFunctionVariable> m_implicitConstructorPredicate;
/// Constructor summary predicate, exists after the constructor
/// (implicit or explicit) and before the interface.
std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorSummaryPredicate;
/// Artificial Interface predicate.
/// Single entry block for all functions.
std::unique_ptr<smt::SymbolicFunctionVariable> m_interfacePredicate;
std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_interfaces;
/// Artificial Error predicate.
/// Single error block for all assertions.
std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;
/// Function predicates.
std::map<ContractDefinition const*, std::map<FunctionDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>>> m_summaries;
smt::SymbolicIntVariable m_error{
TypeProvider::uint256(),
TypeProvider::uint256(),
"error",
m_context
};
//@}
/// Variables.
@ -180,7 +232,12 @@ private:
/// Verification targets.
//@{
std::vector<Expression const*> m_verificationTargets;
struct CHCVerificationTarget: VerificationTarget
{
smt::Expression errorId;
};
std::map<ASTNode const*, CHCVerificationTarget, IdCompare> m_verificationTargets;
/// Assertions proven safe.
std::set<Expression const*> m_safeAssertions;
@ -190,6 +247,10 @@ private:
//@{
FunctionDefinition const* m_currentFunction = nullptr;
std::map<ASTNode const*, std::set<ASTNode const*, IdCompare>, IdCompare> m_callGraph;
std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
/// The current block.
smt::Expression m_currentBlock = smt::Expression(true);

1
libsolidity/formal/EncodingContext.h
View File

@ -140,6 +140,7 @@ public:
void pushSolver();
void popSolver();
void addAssertion(Expression const& _e);
unsigned solverStackHeigh() { return m_assertions.size(); } const
SolverInterface* solver()
{
solAssert(m_solver, "");

4
libsolidity/formal/ModelChecker.cpp
View File

@ -29,9 +29,9 @@ ModelChecker::ModelChecker(
ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
):
m_context(),
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
m_context()
m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers)
{
}

6
libsolidity/formal/ModelChecker.h
View File

@ -62,14 +62,14 @@ public:
static smt::SMTSolverChoice availableSolvers();
private:
/// Stores the context of the encoding.
smt::EncodingContext m_context;
/// Bounded Model Checker engine.
BMC m_bmc;
/// Constrained Horn Clauses engine.
CHC m_chc;
/// Stores the context of the encoding.
smt::EncodingContext m_context;
};
}

6
libsolidity/formal/Z3Interface.h
View File

@ -58,11 +58,11 @@ private:
z3::sort z3Sort(smt::Sort const& _sort);
z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
std::map<std::string, z3::expr> m_constants;
std::map<std::string, z3::func_decl> m_functions;
z3::context m_context;
z3::solver m_solver;
std::map<std::string, z3::expr> m_constants;
std::map<std::string, z3::func_decl> m_functions;
};
}

26
test/libsolidity/smtCheckerTests/functions/library_constant.sol Normal file
View File

@ -0,0 +1,26 @@
pragma experimental SMTChecker;
library l1 {
uint private constant TON = 1000;
function f1() public pure {
assert(TON == 1000);
assert(TON == 2000);
}
function f2(uint x, uint y) internal pure returns (uint) {
return x + y;
}
}
contract C {
function f(uint x) public pure {
uint z = l1.f2(x, 1);
assert(z == x + 1);
}
}
// ----
// Warning: (136-155): Assertion violation happens here
// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (300-302): Assertion checker does not yet implement type type(library l1)
// Warning: (229-234): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (327-332): Overflow (resulting value larger than 2**256 - 1) happens here

9
test/libsolidity/smtCheckerTests/functions/library_constant_2.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
library l1 {
uint private constant TON = 1000;
function f1() public pure {
assert(TON == 1000);
}
}

5
test/libsolidity/smtCheckerTests/invariants/loop_nested.sol
View File

@ -17,3 +17,8 @@ contract Simple {
}
// ====
// SMTSolvers: z3
// ----
// Warning: (172-187): Error trying to invoke SMT solver.
// Warning: (195-209): Error trying to invoke SMT solver.
// Warning: (172-187): Assertion violation happens here
// Warning: (195-209): Assertion violation happens here

5
test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
View File

@ -14,3 +14,8 @@ contract Simple {
}
// ====
// SMTSolvers: z3
// ----
// Warning: (164-179): Error trying to invoke SMT solver.
// Warning: (187-201): Error trying to invoke SMT solver.
// Warning: (164-179): Assertion violation happens here
// Warning: (187-201): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
View File

@ -12,12 +12,12 @@ contract LoopFor2 {
b[i] = i + 1;
c[i] = b[i];
}
// This is safe but too hard to solve currently.
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (312-331): Assertion violation happens here
// Warning: (316-336): Assertion violation happens here
// Warning: (363-382): Assertion violation happens here

8
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
View File

@ -12,13 +12,13 @@ contract LoopFor2 {
b[i] = i + 1;
c[i] = b[i];
}
// This is safe but too hard to prove currently.
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (290-309): Assertion violation happens here
// Warning: (313-332): Assertion violation happens here
// Warning: (317-337): Assertion violation happens here
// Warning: (341-360): Assertion violation happens here
// Warning: (364-383): Assertion violation happens here

4
test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol
View File

@ -13,5 +13,5 @@ contract C
assert(a[1][1] == 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (184-204): Assertion violation happens here