mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
101 lines
2.7 KiB
C++
101 lines
2.7 KiB
C++
/*
|
|
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/>.
|
|
*/
|
|
|
|
/**
|
|
* Model checker based on Constrained Horn Clauses.
|
|
*
|
|
* A Solidity contract's CFG is encoded into a system of Horn clauses where
|
|
* each block has a predicate and edges are rules.
|
|
*
|
|
* The entry block is the constructor which has no in-edges.
|
|
* The constructor has one out-edge to an artificial block named _Interface_
|
|
* which has in/out-edges from/to all public functions.
|
|
*
|
|
* Loop invariants for Interface -> Interface' are state invariants.
|
|
*/
|
|
|
|
#pragma once
|
|
|
|
#include <libsolidity/formal/SMTEncoder.h>
|
|
|
|
#include <libsolidity/formal/CHCSolverInterface.h>
|
|
|
|
#include <set>
|
|
|
|
namespace dev
|
|
{
|
|
namespace solidity
|
|
{
|
|
|
|
class CHC: public SMTEncoder
|
|
{
|
|
public:
|
|
CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter);
|
|
|
|
void analyze(SourceUnit const& _sources);
|
|
|
|
std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }
|
|
|
|
private:
|
|
/// Visitor functions.
|
|
//@{
|
|
bool visit(ContractDefinition const& _node) override;
|
|
void endVisit(ContractDefinition const& _node) override;
|
|
bool visit(FunctionDefinition const& _node) override;
|
|
void endVisit(FunctionDefinition const& _node) override;
|
|
bool visit(IfStatement const& _node) override;
|
|
void endVisit(FunctionCall const& _node) override;
|
|
|
|
void visitAssert(FunctionCall const& _funCall);
|
|
//@}
|
|
|
|
/// Helpers.
|
|
//@{
|
|
void reset();
|
|
bool shouldVisit(ContractDefinition const& _contract) const;
|
|
bool shouldVisit(FunctionDefinition const& _function) const;
|
|
//@}
|
|
|
|
/// Solver related.
|
|
//@{
|
|
/// @returns true if query is unsatisfiable (safe).
|
|
bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
|
|
//@}
|
|
|
|
/// Verification targets.
|
|
//@{
|
|
std::vector<Expression const*> m_verificationTargets;
|
|
|
|
/// Assertions proven safe.
|
|
std::set<Expression const*> m_safeAssertions;
|
|
//@}
|
|
|
|
/// Control-flow.
|
|
//@{
|
|
FunctionDefinition const* m_currentFunction = nullptr;
|
|
//@}
|
|
|
|
/// CHC solver.
|
|
std::shared_ptr<smt::CHCSolverInterface> m_interface;
|
|
|
|
/// ErrorReporter that comes from CompilerStack.
|
|
langutil::ErrorReporter& m_outerErrorReporter;
|
|
};
|
|
|
|
}
|
|
}
|