cerc-io/solidity
15
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

Refactor predicates

Browse Source
This commit is contained in:
Leonardo Alt 2020-08-13 14:00:33 +02:00
parent e582731aab
commit 016b9b83a8
6 changed files with 253 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/CMakeLists.txt
View File

@ -100,6 +100,8 @@ set(sources
formal/EncodingContext.h
formal/ModelChecker.cpp
formal/ModelChecker.h
formal/Predicate.cpp
formal/Predicate.h
formal/SMTEncoder.cpp
formal/SMTEncoder.h
formal/SSAVariable.cpp

116
libsolidity/formal/CHC.cpp
View File

@ -85,11 +85,7 @@ void CHC::analyze(SourceUnit const& _source)
resetSourceAnalysis();
auto genesisSort = make_shared<smtutil::FunctionSort>(
vector<smtutil::SortPointer>(),
smtutil::SortProvider::boolSort
);
m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
m_genesisPredicate = createSymbolicBlock(arity0FunctionSort(), "genesis");
addRule(genesis(), "genesis");
set<SourceUnit const*, IdCompare> sources;
@ -124,10 +120,8 @@ bool CHC::visit(ContractDefinition const& _contract)
clearIndices(&_contract);
string suffix = _contract.name() + "_" + to_string(_contract.id());
m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_" + suffix);
m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix);
m_symbolFunction[m_constructorSummaryPredicate->currentFunctionValue().name] = &_contract;
m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix);
m_constructorSummaryPredicate = createSymbolicBlock(constructorSort(), "summary_constructor_" + suffix, &_contract);
m_implicitConstructorPredicate = createSymbolicBlock(arity0FunctionSort(), "implicit_constructor_" + suffix, &_contract);
auto stateExprs = currentStateVariables();
setCurrentBlock(*m_interfaces.at(m_currentContract), &stateExprs);
@ -233,7 +227,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
if (_function.isConstructor())
{
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)));
clearIndices(m_currentContract, m_currentFunction);
@ -326,8 +320,8 @@ bool CHC::visit(WhileStatement const& _while)
auto outerBreakDest = m_breakDest;
auto outerContinueDest = m_continueDest;
m_breakDest = afterLoopBlock.get();
m_continueDest = loopHeaderBlock.get();
m_breakDest = afterLoopBlock;
m_continueDest = loopHeaderBlock;
if (_while.isDoWhile())
_while.body().accept(*this);
@ -377,8 +371,8 @@ bool CHC::visit(ForStatement const& _for)
auto outerBreakDest = m_breakDest;
auto outerContinueDest = m_continueDest;
m_breakDest = afterLoopBlock.get();
m_continueDest = postLoop ? postLoopBlock.get() : loopHeaderBlock.get();
m_breakDest = afterLoopBlock;
m_continueDest = postLoop ? postLoopBlock : loopHeaderBlock;
if (auto init = _for.initializationExpression())
init->accept(*this);
@ -571,7 +565,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
m_context.variable(*var)->increaseIndex();
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
m_symbolFunction[nondet.name] = &_funCall;
m_context.addAssertion(nondet);
m_context.addAssertion(m_error.currentValue() == 0);
@ -681,7 +674,9 @@ void CHC::resetSourceAnalysis()
m_errorIds.clear();
m_callGraph.clear();
m_summaries.clear();
m_symbolFunction.clear();
m_interfaces.clear();
m_nondetInterfaces.clear();
Predicate::reset();
}
void CHC::resetContractAnalysis()
@ -717,7 +712,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
}
void CHC::setCurrentBlock(
smt::SymbolicFunctionVariable const& _block,
Predicate const& _block,
vector<smtutil::Expression> const* _arguments
)
{
@ -806,7 +801,7 @@ smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contrac
);
}
smtutil::SortPointer CHC::arity0FunctionSort()
smtutil::SortPointer CHC::arity0FunctionSort() const
{
return make_shared<smtutil::FunctionSort>(
vector<smtutil::SortPointer>(),
@ -870,14 +865,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>(
_sort,
_name,
m_context
);
m_interface->registerRelation(block->currentFunctionValue());
auto const* block = Predicate::create(_sort, _name, m_context, _node);
m_interface->registerRelation(block->functor());
return block;
}
@ -887,20 +878,24 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
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);
m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix);
for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
if (!m_context.knownVariable(*var))
createVariable(*var);
/// 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");
if (!m_interfaces.count(base))
{
solAssert(!m_nondetInterfaces.count(base), "");
string suffix = base->name() + "_" + to_string(base->id());
m_interfaces.emplace(base, createSymbolicBlock(interfaceSort(*base), "interface_" + suffix, base));
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())
{
@ -923,8 +918,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto state1 = stateVariablesAtIndex(1, *base);
auto state2 = stateVariablesAtIndex(2, *base);
auto nondetPre = iface(state0 + state1);
auto nondetPost = iface(state0 + state2);
auto const* iface = m_nondetInterfaces.at(base);
auto state0 = stateVariablesAtIndex(0, *base);
auto nondetPre = (*iface)(state0 + state1);
auto nondetPost = (*iface)(state0 + state2);
vector<smtutil::Expression> args{m_error.currentValue()};
args += state1 +
@ -960,7 +957,7 @@ smtutil::Expression CHC::error()
smtutil::Expression CHC::error(unsigned _idx)
{
return m_errorPredicate->functionValueAtIndex(_idx)({});
return m_errorPredicate->functor(_idx)({});
}
smtutil::Expression CHC::summary(ContractDefinition const& _contract)
@ -994,37 +991,33 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function)
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),
"block_" +
uniquePrefix() +
"_" +
_prefix +
predicateName(_node));
auto block = createSymbolicBlock(
sort(_node),
"block_" + uniquePrefix() + "_" + _prefix + predicateName(_node),
_node
);
solAssert(m_currentFunction, "");
m_symbolFunction[block->currentFunctionValue().name] = m_currentFunction;
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),
"summary_" +
uniquePrefix() +
"_" +
predicateName(&_function, &_contract));
auto block = createSymbolicBlock(
summarySort(_function, _contract),
"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
&_function
);
m_symbolFunction[block->currentFunctionValue().name] = &_function;
return block;
}
void CHC::createErrorBlock()
{
solAssert(m_errorPredicate, "");
m_errorPredicate->increaseIndex();
m_interface->registerRelation(m_errorPredicate->currentFunctionValue());
m_errorPredicate = createSymbolicBlock(arity0FunctionSort(), "error_target_" + to_string(m_context.newUniqueId()));
m_interface->registerRelation(m_errorPredicate->functor());
}
void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints)
@ -1128,13 +1121,13 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
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());
}
smtutil::Expression CHC::predicate(
smt::SymbolicFunctionVariable const& _block,
Predicate const& _block,
vector<smtutil::Expression> const& _arguments
)
{
@ -1441,18 +1434,19 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
/// At this point property 2 from the function description is verified for this node.
auto const& summaryNode = _graph.nodes.at(summaryId);
solAssert(m_symbolFunction.count(summaryNode.first), "");
Predicate const* summaryPredicate = Predicate::predicate(summaryNode.first);
solAssert(summaryPredicate, "");
FunctionDefinition const* calledFun = nullptr;
ContractDefinition const* calledContract = nullptr;
if (auto const* contract = dynamic_cast<ContractDefinition const*>(m_symbolFunction.at(summaryNode.first)))
if (auto const* contract = dynamic_cast<ContractDefinition const*>(summaryPredicate->programNode()))
{
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)))
else if (auto const* fun = dynamic_cast<FunctionDefinition const*>(summaryPredicate->programNode()))
calledFun = fun;
else
solAssert(false, "");

33
libsolidity/formal/CHC.h
View File

@ -31,6 +31,7 @@
#pragma once
#include <libsolidity/formal/Predicate.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/interface/ReadFile.h>
@ -108,7 +109,7 @@ private:
void resetContractAnalysis();
void eraseKnowledge();
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);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
@ -122,7 +123,7 @@ private:
smtutil::SortPointer nondetInterfaceSort();
static smtutil::SortPointer interfaceSort(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(ASTNode const* _block);
/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
@ -134,7 +135,7 @@ private:
/// Predicate helpers.
//@{
/// @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
/// in a given _source.
@ -150,10 +151,10 @@ private:
smtutil::Expression error(unsigned _idx);
/// 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.
/// 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.
/// Also registers the predicate.
@ -184,9 +185,9 @@ private:
/// @returns the predicate name for a given node.
std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
/// @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.
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.
smtutil::Expression predicate(FunctionCall const& _funCall);
/// @returns a predicate that defines a constructor summary.
@ -251,32 +252,32 @@ private:
/// Predicates.
//@{
/// Genesis predicate.
std::unique_ptr<smt::SymbolicFunctionVariable> m_genesisPredicate;
Predicate const* m_genesisPredicate = nullptr;
/// Implicit constructor predicate.
/// 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
/// (implicit or explicit) and before the interface.
std::unique_ptr<smt::SymbolicFunctionVariable> m_constructorSummaryPredicate;
Predicate const* m_constructorSummaryPredicate = nullptr;
/// Artificial Interface predicate.
/// 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.
/// These are used when the analyzed contract makes external calls to unknown code,
/// which means that the analyzed contract can potentially be called
/// nondeterministically.
std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_nondetInterfaces;
std::map<ContractDefinition const*, Predicate const*> m_nondetInterfaces;
/// Artificial Error predicate.
/// Single error block for all assertions.
std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;
Predicate const* m_errorPredicate = nullptr;
/// 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{
TypeProvider::uint256(),
@ -337,9 +338,9 @@ private:
bool m_unknownFunctionCallSeen = false;
/// 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.
smt::SymbolicFunctionVariable const* m_continueDest = nullptr;
Predicate const* m_continueDest;
//@}
/// CHC solver.

92
libsolidity/formal/Predicate.cpp Normal file
View File

@ -0,0 +1,92 @@
/*
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/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;
}

86
libsolidity/formal/Predicate.h Normal file
View File

@ -0,0 +1,86 @@
/*
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 <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;
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;
};
}

2
test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol
View File

@ -26,4 +26,4 @@ contract C
}
}
// ----
// Warning 6328: (400-457): Assertion violation happens here.
// Warning 6328: (400-457): Assertion violation happens here