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 #7031 from ethereum/smt_chcsolver_interface

Browse Source 
[CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface
This commit is contained in:
Leonardo 2019-07-17 17:29:53 +02:00 committed by GitHub
commit dd031edd59
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 229 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libsolidity/CMakeLists.txt
View File

@ -77,6 +77,7 @@ set(sources
codegen/ir/IRLValue.h
formal/BMC.cpp
formal/BMC.h
formal/CHCSolverInterface.h
formal/EncodingContext.cpp
formal/EncodingContext.h
formal/ModelChecker.cpp
@ -121,7 +122,7 @@ find_package(Z3 4.6.0)
if (${Z3_FOUND})
add_definitions(-DHAVE_Z3)
message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
set(z3_SRCS formal/Z3Interface.cpp formal/Z3Interface.h)
set(z3_SRCS formal/Z3Interface.cpp formal/Z3Interface.h formal/Z3CHCInterface.cpp formal/Z3CHCInterface.h)
else()
set(z3_SRCS)
endif()

56
libsolidity/formal/CHCSolverInterface.h Normal file
View File

@ -0,0 +1,56 @@
/*
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 constrained Horn solvers.
*/
#pragma once
#include <libsolidity/formal/SolverInterface.h>
namespace dev
{
namespace solidity
{
namespace smt
{
class CHCSolverInterface
{
public:
virtual ~CHCSolverInterface() = default;
virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
/// Takes a function declaration as a relation.
virtual void registerRelation(Expression const& _expr) = 0;
/// Takes an implication and adds as rule.
/// Needs to bound all vars as universally quantified.
virtual void addRule(Expression const& _expr, std::string const& _name) = 0;
/// Takes a function application and checks
/// for reachability.
virtual std::pair<CheckResult, std::vector<std::string>> query(
Expression const& _expr
) = 0;
};
}
}
}

97
libsolidity/formal/Z3CHCInterface.cpp Normal file
View File

@ -0,0 +1,97 @@
/*
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/Z3CHCInterface.h>
#include <liblangutil/Exceptions.h>
#include <libdevcore/CommonIO.h>
using namespace std;
using namespace dev;
using namespace dev::solidity::smt;
Z3CHCInterface::Z3CHCInterface():
m_z3Interface(make_shared<Z3Interface>()),
m_context(m_z3Interface->context()),
m_solver(*m_context)
{
// This needs to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true);
// This needs to be set in the context.
m_context->set("timeout", queryTimeout);
}
void Z3CHCInterface::declareVariable(string const& _name, Sort const& _sort)
{
m_z3Interface->declareVariable(_name, _sort);
}
void Z3CHCInterface::registerRelation(Expression const& _expr)
{
m_solver.register_relation(m_z3Interface->functions().at(_expr.name));
}
void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
{
z3::expr rule = m_z3Interface->toZ3Expr(_expr);
if (m_z3Interface->constants().empty())
m_solver.add_rule(rule, m_context->str_symbol(_name.c_str()));
else
{
z3::expr_vector variables(*m_context);
for (auto const& var: m_z3Interface->constants())
variables.push_back(var.second);
z3::expr boundRule = z3::forall(variables, rule);
m_solver.add_rule(boundRule, m_context->str_symbol(_name.c_str()));
}
}
pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
{
CheckResult result;
vector<string> values;
try
{
z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
switch (m_solver.query(z3Expr))
{
case z3::check_result::sat:
{
result = CheckResult::SATISFIABLE;
// TODO retrieve model.
break;
}
case z3::check_result::unsat:
{
result = CheckResult::UNSATISFIABLE;
// TODO retrieve invariants.
break;
}
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
break;
}
// TODO retrieve model / invariants
}
catch (z3::exception const& _e)
{
result = CheckResult::ERROR;
values.clear();
}
return make_pair(result, values);
}

64
libsolidity/formal/Z3CHCInterface.h Normal file
View File

@ -0,0 +1,64 @@
/*
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/>.
*/
/**
* Z3 specific Horn solver interface.
*/
#pragma once
#include <libsolidity/formal/CHCSolverInterface.h>
#include <libsolidity/formal/Z3Interface.h>
namespace dev
{
namespace solidity
{
namespace smt
{
class Z3CHCInterface: public CHCSolverInterface
{
public:
Z3CHCInterface();
/// Forwards variable declaration to Z3Interface.
void declareVariable(std::string const& _name, Sort const& _sort) override;
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;
std::shared_ptr<Z3Interface> z3Interface() { return m_z3Interface; }
private:
// Used to handle variables.
std::shared_ptr<Z3Interface> m_z3Interface;
z3::context* m_context;
// Horn solver.
z3::fixedpoint m_solver;
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
};
}
}
}

13
libsolidity/formal/Z3Interface.h
View File

@ -43,17 +43,24 @@ public:
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
z3::expr toZ3Expr(Expression const& _expr);
std::map<std::string, z3::expr> constants() const { return m_constants; }
std::map<std::string, z3::func_decl> functions() const { return m_functions; }
z3::context* context() { return &m_context; }
private:
void declareFunction(std::string const& _name, Sort const& _sort);
z3::expr toZ3Expr(Expression const& _expr);
z3::sort z3Sort(smt::Sort const& _sort);
z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
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;
z3::context m_context;
z3::solver m_solver;
};
}