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 #7480 from ethereum/smt_chcsmtlib2interface

Browse Source 
[SMTChecker] Add CHCSmtLib2Interface
This commit is contained in:
chriseth 2019-11-07 15:10:23 +01:00 committed by GitHub
commit ed7be7b9c7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
18 changed files with 316 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/CMakeLists.txt
View File

@ -79,6 +79,8 @@ set(sources
formal/BMC.h
formal/CHC.cpp
formal/CHC.h
formal/CHCSmtLib2Interface.cpp
formal/CHCSmtLib2Interface.h
formal/CHCSolverInterface.h
formal/EncodingContext.cpp
formal/EncodingContext.h

27
libsolidity/formal/CHC.cpp
View File

@ -17,6 +17,8 @@
#include <libsolidity/formal/CHC.h>
#include <libsolidity/formal/CHCSmtLib2Interface.h>
#ifdef HAVE_Z3
#include <libsolidity/formal/Z3CHCInterface.h>
#endif
@ -30,13 +32,20 @@ using namespace dev;
using namespace langutil;
using namespace dev::solidity;
CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter):
CHC::CHC(
smt::EncodingContext& _context,
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses
):
SMTEncoder(_context),
#ifdef HAVE_Z3
m_interface(make_shared<smt::Z3CHCInterface>()),
#else
m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses)),
#endif
m_outerErrorReporter(_errorReporter)
{
(void)_smtlib2Responses;
}
void CHC::analyze(SourceUnit const& _source)
@ -47,12 +56,24 @@ void CHC::analyze(SourceUnit const& _source)
auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
solAssert(z3Interface, "");
m_context.setSolver(z3Interface->z3Interface());
#else
auto smtlib2Interface = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface);
solAssert(smtlib2Interface, "");
m_context.setSolver(smtlib2Interface->smtlib2Interface());
#endif
m_context.clear();
m_context.setAssertionAccumulation(false);
m_variableUsage.setFunctionInlining(false);
_source.accept(*this);
#endif
}
vector<string> CHC::unhandledQueries() const
{
if (auto smtlib2 = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface))
return smtlib2->unhandledQueries();
return {};
}
bool CHC::visit(ContractDefinition const& _contract)
@ -99,7 +120,7 @@ bool CHC::visit(ContractDefinition const& _contract)
{
auto const& symbVar = m_context.variable(*var);
symbVar->increaseIndex();
m_interface->declareVariable(symbVar->currentName(), *symbVar->sort());
m_interface->declareVariable(symbVar->currentName(), symbVar->sort());
m_context.setZeroValue(*symbVar);
}

11
libsolidity/formal/CHC.h
View File

@ -44,12 +44,21 @@ namespace solidity
class CHC: public SMTEncoder
{
public:
CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter);
CHC(
smt::EncodingContext& _context,
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses
);
void analyze(SourceUnit const& _sources);
std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }
/// This is used if the Horn solver is not directly linked into this binary.
/// @returns a list of inputs to the Horn solver that were not part of the argument to
/// the constructor.
std::vector<std::string> unhandledQueries() const;
private:
/// Visitor functions.
//@{

160
libsolidity/formal/CHCSmtLib2Interface.cpp Normal file
View File

@ -0,0 +1,160 @@
/*
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/>.
*/
#include <libsolidity/formal/CHCSmtLib2Interface.h>
#include <libdevcore/Keccak256.h>
#include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp>
#include <boost/filesystem/operations.hpp>
#include <array>
#include <fstream>
#include <iostream>
#include <memory>
#include <stdexcept>
using namespace std;
using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
CHCSmtLib2Interface::CHCSmtLib2Interface(map<h256, string> const& _queryResponses):
m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses)),
m_queryResponses(_queryResponses)
{
reset();
}
void CHCSmtLib2Interface::reset()
{
m_accumulatedOutput.clear();
m_variables.clear();
}
void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr)
{
solAssert(_expr.sort, "");
solAssert(_expr.sort->kind == smt::Kind::Function, "");
if (!m_variables.count(_expr.name))
{
auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
string domain = m_smtlib2->toSmtLibSort(fSort->domain);
// Relations are predicates which have implicit codomain Bool.
m_variables.insert(_expr.name);
write(
"(declare-rel |" +
_expr.name +
"| " +
domain +
")"
);
}
}
void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string const& _name)
{
write(
"(rule (! " +
m_smtlib2->toSExpr(_expr) +
" :named " +
_name +
"))"
);
}
pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(smt::Expression const& _block)
{
string accumulated{};
swap(m_accumulatedOutput, accumulated);
for (auto const& var: m_smtlib2->variables())
declareVariable(var.first, var.second);
m_accumulatedOutput += accumulated;
string response = querySolver(
m_accumulatedOutput +
"\n(query " + _block.name + " :print-certificate true)"
);
CheckResult result;
// TODO proper parsing
if (boost::starts_with(response, "sat\n"))
result = CheckResult::SATISFIABLE;
else if (boost::starts_with(response, "unsat\n"))
result = CheckResult::UNSATISFIABLE;
else if (boost::starts_with(response, "unknown\n"))
result = CheckResult::UNKNOWN;
else
result = CheckResult::ERROR;
// TODO collect invariants or counterexamples.
return make_pair(result, vector<string>{});
}
void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, _sort);
else if (!m_variables.count(_name))
{
m_variables.insert(_name);
write("(declare-var |" + _name + "| " + m_smtlib2->toSmtLibSort(*_sort) + ')');
}
}
void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
solAssert(_sort->kind == smt::Kind::Function, "");
// TODO Use domain and codomain as key as well
if (!m_variables.count(_name))
{
auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
solAssert(fSort->codomain, "");
string domain = m_smtlib2->toSmtLibSort(fSort->domain);
string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain);
m_variables.insert(_name);
write(
"(declare-fun |" +
_name +
"| " +
domain +
" " +
codomain +
")"
);
}
}
void CHCSmtLib2Interface::write(string _data)
{
m_accumulatedOutput += move(_data) + "\n";
}
string CHCSmtLib2Interface::querySolver(string const& _input)
{
h256 inputHash = dev::keccak256(_input);
if (m_queryResponses.count(inputHash))
return m_queryResponses.at(inputHash);
else
{
m_unhandledQueries.push_back(_input);
return "unknown\n";
}
}

75
libsolidity/formal/CHCSmtLib2Interface.h Normal file
View File

@ -0,0 +1,75 @@
/*
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/>.
*/
/**
* Interface for solving Horn systems via smtlib2.
*/
#pragma once
#include <libsolidity/formal/CHCSolverInterface.h>
#include <libsolidity/formal/SMTLib2Interface.h>
namespace dev
{
namespace solidity
{
namespace smt
{
class CHCSmtLib2Interface: public CHCSolverInterface
{
public:
explicit CHCSmtLib2Interface(std::map<h256, std::string> const& _queryResponses);
void reset();
void registerRelation(Expression const& _expr) override;
void addRule(Expression const& _expr, std::string const& _name) override;
std::pair<CheckResult, std::vector<std::string>> query(Expression const& _expr) override;
void declareVariable(std::string const& _name, SortPointer const& _sort) override;
std::vector<std::string> unhandledQueries() const { return m_unhandledQueries; }
std::shared_ptr<SMTLib2Interface> smtlib2Interface() { return m_smtlib2; }
private:
void declareFunction(std::string const& _name, SortPointer const& _sort);
void write(std::string _data);
/// Communicates with the solver via the callback. Throws SMTSolverError on error.
std::string querySolver(std::string const& _input);
/// Used to access toSmtLibSort, SExpr, and handle variables.
/// Needs to be a shared_ptr since it's also passed to EncodingContext.
std::shared_ptr<SMTLib2Interface> m_smtlib2;
std::string m_accumulatedOutput;
std::set<std::string> m_variables;
std::map<h256, std::string> const& m_queryResponses;
std::vector<std::string> m_unhandledQueries;
};
}
}
}

2
libsolidity/formal/CHCSolverInterface.h
View File

@ -35,7 +35,7 @@ class CHCSolverInterface
public:
virtual ~CHCSolverInterface() = default;
virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0;
/// Takes a function declaration as a relation.
virtual void registerRelation(Expression const& _expr) = 0;

5
libsolidity/formal/CVC4Interface.cpp
View File

@ -48,9 +48,10 @@ void CVC4Interface::pop()
m_solver.pop();
}
void CVC4Interface::declareVariable(string const& _name, Sort const& _sort)
void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(_sort));
solAssert(_sort, "");
m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
}
void CVC4Interface::addAssertion(Expression const& _expr)

2
libsolidity/formal/CVC4Interface.h
View File

@ -50,7 +50,7 @@ public:
void push() override;
void pop() override;
void declareVariable(std::string const&, Sort const&) override;
void declareVariable(std::string const&, SortPointer const&) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;

4
libsolidity/formal/ModelChecker.cpp
View File

@ -24,7 +24,7 @@ using namespace dev::solidity;
ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
m_bmc(m_context, _errorReporter, _smtlib2Responses),
m_chc(m_context, _errorReporter),
m_chc(m_context, _errorReporter, _smtlib2Responses),
m_context()
{
}
@ -40,5 +40,5 @@ void ModelChecker::analyze(SourceUnit const& _source)
vector<string> ModelChecker::unhandledQueries()
{
return m_bmc.unhandledQueries();
return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
}

23
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -60,27 +60,29 @@ void SMTLib2Interface::pop()
m_accumulatedOutput.pop_back();
}
void SMTLib2Interface::declareVariable(string const& _name, Sort const& _sort)
void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
if (_sort.kind == Kind::Function)
solAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, _sort);
else if (!m_variables.count(_name))
{
m_variables.insert(_name);
write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')');
m_variables.emplace(_name, _sort);
write("(declare-fun |" + _name + "| () " + toSmtLibSort(*_sort) + ')');
}
}
void SMTLib2Interface::declareFunction(string const& _name, Sort const& _sort)
void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
{
solAssert(_sort.kind == smt::Kind::Function, "");
solAssert(_sort, "");
solAssert(_sort->kind == smt::Kind::Function, "");
// TODO Use domain and codomain as key as well
if (!m_variables.count(_name))
{
FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
string domain = toSmtLibSort(fSort.domain);
string codomain = toSmtLibSort(*fSort.codomain);
m_variables.insert(_name);
auto const& fSort = dynamic_pointer_cast<FunctionSort>(_sort);
string domain = toSmtLibSort(fSort->domain);
string codomain = toSmtLibSort(*fSort->codomain);
m_variables.emplace(_name, _sort);
write(
"(declare-fun |" +
_name +
@ -159,6 +161,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
solAssert(arraySort.domain && arraySort.range, "");
return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
}
default:

13
libsolidity/formal/SMTLib2Interface.h
View File

@ -48,20 +48,23 @@ public:
void push() override;
void pop() override;
void declareVariable(std::string const&, Sort const&) override;
void declareVariable(std::string const&, SortPointer const&) override;
void addAssertion(smt::Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
private:
void declareFunction(std::string const&, Sort const&);
// Used by CHCSmtLib2Interface
std::string toSExpr(smt::Expression const& _expr);
std::string toSmtLibSort(Sort const& _sort);
std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
std::map<std::string, SortPointer> variables() { return m_variables; }
private:
void declareFunction(std::string const& _name, SortPointer const& _sort);
void write(std::string _data);
std::string checkSatAndGetValuesCommand(std::vector<smt::Expression> const& _expressionsToEvaluate);
@ -71,7 +74,7 @@ private:
std::string querySolver(std::string const& _input);
std::vector<std::string> m_accumulatedOutput;
std::set<std::string> m_variables;
std::map<std::string, SortPointer> m_variables;
std::map<h256, std::string> const& m_queryResponses;
std::vector<std::string> m_unhandledQueries;

3
libsolidity/formal/SMTPortfolio.cpp
View File

@ -59,8 +59,9 @@ void SMTPortfolio::pop()
s->pop();
}
void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
for (auto const& s: m_solvers)
s->declareVariable(_name, _sort);
}

2
libsolidity/formal/SMTPortfolio.h
View File

@ -49,7 +49,7 @@ public:
void push() override;
void pop() override;
void declareVariable(std::string const&, Sort const&) override;
void declareVariable(std::string const&, SortPointer const&) override;
void addAssertion(smt::Expression const& _expr) override;

8
libsolidity/formal/SolverInterface.h
View File

@ -338,13 +338,13 @@ public:
virtual void push() = 0;
virtual void pop() = 0;
virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
Expression newVariable(std::string _name, SortPointer _sort)
virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0;
Expression newVariable(std::string _name, SortPointer const& _sort)
{
// Subclasses should do something here
solAssert(_sort, "");
declareVariable(_name, *_sort);
return Expression(std::move(_name), {}, std::move(_sort));
declareVariable(_name, _sort);
return Expression(std::move(_name), {}, _sort);
}
virtual void addAssertion(Expression const& _expr) = 0;

3
libsolidity/formal/Z3CHCInterface.cpp
View File

@ -47,8 +47,9 @@ Z3CHCInterface::Z3CHCInterface():
m_solver.set(p);
}
void Z3CHCInterface::declareVariable(string const& _name, Sort const& _sort)
void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
m_z3Interface->declareVariable(_name, _sort);
}

2
libsolidity/formal/Z3CHCInterface.h
View File

@ -37,7 +37,7 @@ public:
Z3CHCInterface();
/// Forwards variable declaration to Z3Interface.
void declareVariable(std::string const& _name, Sort const& _sort) override;
void declareVariable(std::string const& _name, SortPointer const& _sort) override;
void registerRelation(Expression const& _expr) override;

11
libsolidity/formal/Z3Interface.cpp
View File

@ -50,14 +50,15 @@ void Z3Interface::pop()
m_solver.pop();
}
void Z3Interface::declareVariable(string const& _name, Sort const& _sort)
void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
if (_sort.kind == Kind::Function)
declareFunction(_name, _sort);
solAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, *_sort);
else if (m_constants.count(_name))
m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(_sort));
m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(*_sort));
else
m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(_sort)));
m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(*_sort)));
}
void Z3Interface::declareFunction(string const& _name, Sort const& _sort)

2
libsolidity/formal/Z3Interface.h
View File

@ -38,7 +38,7 @@ public:
void push() override;
void pop() override;
void declareVariable(std::string const& _name, Sort const& _sort) override;
void declareVariable(std::string const& _name, SortPointer const& _sort) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;