diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index fdd7f616f..a376bba9f 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -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() diff --git a/libsolidity/formal/CHCSolverInterface.h b/libsolidity/formal/CHCSolverInterface.h new file mode 100644 index 000000000..091aa3d7c --- /dev/null +++ b/libsolidity/formal/CHCSolverInterface.h @@ -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 . +*/ + +/** + * Interface for constrained Horn solvers. + */ + +#pragma once + +#include + +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> query( + Expression const& _expr + ) = 0; +}; + +} +} +} diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp new file mode 100644 index 000000000..7b8de2c91 --- /dev/null +++ b/libsolidity/formal/Z3CHCInterface.cpp @@ -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 . +*/ + +#include + +#include +#include + +using namespace std; +using namespace dev; +using namespace dev::solidity::smt; + +Z3CHCInterface::Z3CHCInterface(): + m_z3Interface(make_shared()), + 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> Z3CHCInterface::query(Expression const& _expr) +{ + CheckResult result; + vector 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); +} diff --git a/libsolidity/formal/Z3CHCInterface.h b/libsolidity/formal/Z3CHCInterface.h new file mode 100644 index 000000000..a107ad424 --- /dev/null +++ b/libsolidity/formal/Z3CHCInterface.h @@ -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 . +*/ + +/** + * Z3 specific Horn solver interface. + */ + +#pragma once + +#include +#include + +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> query(Expression const& _expr) override; + + std::shared_ptr z3Interface() { return m_z3Interface; } + +private: + // Used to handle variables. + std::shared_ptr m_z3Interface; + + z3::context* m_context; + // Horn solver. + z3::fixedpoint m_solver; + + // SMT query timeout in milliseconds. + static int const queryTimeout = 10000; +}; + +} +} +} diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h index ee4d1551d..171fdcaa5 100644 --- a/libsolidity/formal/Z3Interface.h +++ b/libsolidity/formal/Z3Interface.h @@ -43,17 +43,24 @@ public: void addAssertion(Expression const& _expr) override; std::pair> check(std::vector const& _expressionsToEvaluate) override; + z3::expr toZ3Expr(Expression const& _expr); + + std::map constants() const { return m_constants; } + std::map 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 const& _sorts); - z3::context m_context; - z3::solver m_solver; std::map m_constants; std::map m_functions; + + z3::context m_context; + z3::solver m_solver; }; }