From ab5e3a8f6d9b92cef521b6855bf7ab649ebf751f Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 13 Jul 2017 21:08:24 +0200 Subject: Introduce native Z3 support. --- libsolidity/formal/Z3Interface.cpp | 179 +++++++++++++++++++++++++++++++++++++ libsolidity/formal/Z3Interface.h | 65 ++++++++++++++ 2 files changed, 244 insertions(+) create mode 100644 libsolidity/formal/Z3Interface.cpp create mode 100644 libsolidity/formal/Z3Interface.h (limited to 'libsolidity') diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp new file mode 100644 index 00000000..0d59a3c7 --- /dev/null +++ b/libsolidity/formal/Z3Interface.cpp @@ -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 . +*/ + +#include + +#include + +#include + +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> Z3Interface::check(vector 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 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 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(); +} diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h new file mode 100644 index 00000000..44d4bb2f --- /dev/null +++ b/libsolidity/formal/Z3Interface.h @@ -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 . +*/ + +#pragma once + +#include + +#include + +#include + +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> check(std::vector const& _expressionsToEvaluate) override; + +private: + z3::expr toZ3Expr(Expression const& _expr); + z3::sort z3Sort(smt::Sort _sort); + + std::string checkSatAndGetValuesCommand(std::vector const& _expressionsToEvaluate); + std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end); + + z3::context m_context; + z3::solver m_solver; + std::map m_constants; + std::map m_functions; +}; + +} +} +} -- cgit v1.2.3