mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Introduce native Z3 support.
This commit is contained in:
chriseth
parent
4cea3d4aa4
commit
ab5e3a8f6d
179
libsolidity/formal/Z3Interface.cpp
Normal file
179
libsolidity/formal/Z3Interface.cpp
Normal file
@ -0,0 +1,179 @@
|
||||
/*
|
||||
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/Z3Interface.h>
|
||||
|
||||
#include <libsolidity/interface/Exceptions.h>
|
||||
|
||||
#include <libdevcore/CommonIO.h>
|
||||
|
||||
using namespace std;
|
||||
using namespace dev;
|
||||
using namespace dev::solidity::smt;
|
||||
|
||||
Z3Interface::Z3Interface():
|
||||
m_solver(m_context)
|
||||
{
|
||||
}
|
||||
|
||||
void Z3Interface::reset()
|
||||
{
|
||||
m_constants.clear();
|
||||
m_functions.clear();
|
||||
m_solver.reset();
|
||||
}
|
||||
|
||||
void Z3Interface::push()
|
||||
{
|
||||
m_solver.push();
|
||||
}
|
||||
|
||||
void Z3Interface::pop()
|
||||
{
|
||||
m_solver.pop();
|
||||
}
|
||||
|
||||
Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain)
|
||||
{
|
||||
m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
|
||||
return SolverInterface::newFunction(move(_name), _domain, _codomain);
|
||||
}
|
||||
|
||||
Expression Z3Interface::newInteger(string _name)
|
||||
{
|
||||
m_constants.insert({_name, m_context.int_const(_name.c_str())});
|
||||
return SolverInterface::newInteger(move(_name));
|
||||
}
|
||||
|
||||
Expression Z3Interface::newBool(string _name)
|
||||
{
|
||||
m_constants.insert({_name, m_context.bool_const(_name.c_str())});
|
||||
return SolverInterface::newBool(std::move(_name));
|
||||
}
|
||||
|
||||
void Z3Interface::addAssertion(Expression const& _expr)
|
||||
{
|
||||
m_solver.add(toZ3Expr(_expr));
|
||||
}
|
||||
|
||||
pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
|
||||
{
|
||||
CheckResult result;
|
||||
switch (m_solver.check())
|
||||
{
|
||||
case z3::check_result::sat:
|
||||
result = CheckResult::SAT;
|
||||
break;
|
||||
case z3::check_result::unsat:
|
||||
result = CheckResult::UNSAT;
|
||||
break;
|
||||
case z3::check_result::unknown:
|
||||
result = CheckResult::UNKNOWN;
|
||||
break;
|
||||
default:
|
||||
solAssert(false, "");
|
||||
}
|
||||
|
||||
vector<string> values;
|
||||
if (result != CheckResult::UNSAT)
|
||||
{
|
||||
z3::model m = m_solver.get_model();
|
||||
for (Expression const& e: _expressionsToEvaluate)
|
||||
values.push_back(toString(m.eval(toZ3Expr(e))));
|
||||
}
|
||||
return make_pair(result, values);
|
||||
}
|
||||
|
||||
z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
|
||||
{
|
||||
if (_expr.arguments.empty() && m_constants.count(_expr.name))
|
||||
return m_constants.at(_expr.name);
|
||||
z3::expr_vector arguments(m_context);
|
||||
for (auto const& arg: _expr.arguments)
|
||||
arguments.push_back(toZ3Expr(arg));
|
||||
|
||||
static map<string, unsigned> arity{
|
||||
{"not", 1},
|
||||
{"and", 2},
|
||||
{"or", 2},
|
||||
{"=", 2},
|
||||
{"<", 2},
|
||||
{"<=", 2},
|
||||
{">", 2},
|
||||
{">=", 2},
|
||||
{"+", 2},
|
||||
{"-", 2},
|
||||
{"*", 2},
|
||||
{">=", 2}
|
||||
};
|
||||
string const& n = _expr.name;
|
||||
if (m_functions.count(n))
|
||||
return m_functions.at(n)(arguments);
|
||||
else if (m_constants.count(n))
|
||||
{
|
||||
solAssert(arguments.empty(), "");
|
||||
return m_constants.at(n);
|
||||
}
|
||||
else if (arguments.empty())
|
||||
{
|
||||
// We assume it is an integer...
|
||||
return m_context.int_val(n.c_str());
|
||||
}
|
||||
|
||||
assert(arity.count(n) && arity.at(n) == arguments.size());
|
||||
if (n == "not")
|
||||
return !arguments[0];
|
||||
else if (n == "and")
|
||||
return arguments[0] && arguments[1];
|
||||
else if (n == "or")
|
||||
return arguments[0] || arguments[1];
|
||||
else if (n == "=")
|
||||
return arguments[0] == arguments[1];
|
||||
else if (n == "<")
|
||||
return arguments[0] < arguments[1];
|
||||
else if (n == "<=")
|
||||
return arguments[0] <= arguments[1];
|
||||
else if (n == ">")
|
||||
return arguments[0] > arguments[1];
|
||||
else if (n == ">=")
|
||||
return arguments[0] >= arguments[1];
|
||||
else if (n == "+")
|
||||
return arguments[0] + arguments[1];
|
||||
else if (n == "-")
|
||||
return arguments[0] - arguments[1];
|
||||
else if (n == "*")
|
||||
return arguments[0] * arguments[1];
|
||||
// Cannot reach here.
|
||||
solAssert(false, "");
|
||||
return arguments[0];
|
||||
}
|
||||
|
||||
z3::sort Z3Interface::z3Sort(Sort _sort)
|
||||
{
|
||||
switch (_sort)
|
||||
{
|
||||
case Sort::Bool:
|
||||
return m_context.bool_sort();
|
||||
case Sort::Int:
|
||||
return m_context.int_sort();
|
||||
default:
|
||||
break;
|
||||
}
|
||||
solAssert(false, "");
|
||||
// Cannot be reached.
|
||||
return m_context.int_sort();
|
||||
}
|
||||
65
libsolidity/formal/Z3Interface.h
Normal file
65
libsolidity/formal/Z3Interface.h
Normal file
@ -0,0 +1,65 @@
|
||||
/*
|
||||
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/>.
|
||||
*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <libsolidity/formal/SolverInterface.h>
|
||||
|
||||
#include <boost/noncopyable.hpp>
|
||||
|
||||
#include <z3++.h>
|
||||
|
||||
namespace dev
|
||||
{
|
||||
namespace solidity
|
||||
{
|
||||
namespace smt
|
||||
{
|
||||
|
||||
class Z3Interface: public SolverInterface, public boost::noncopyable
|
||||
{
|
||||
public:
|
||||
Z3Interface();
|
||||
|
||||
void reset() override;
|
||||
|
||||
void push() override;
|
||||
void pop() override;
|
||||
|
||||
Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
|
||||
Expression newInteger(std::string _name) override;
|
||||
Expression newBool(std::string _name) override;
|
||||
|
||||
void addAssertion(Expression const& _expr) override;
|
||||
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
|
||||
|
||||
private:
|
||||
z3::expr toZ3Expr(Expression const& _expr);
|
||||
z3::sort z3Sort(smt::Sort _sort);
|
||||
|
||||
std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
|
||||
std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
|
||||
|
||||
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;
|
||||
};
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
Loading…
Reference in New Issue
Block a user