[CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface

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()

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 <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;
+};
+
+}
+}
+}

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 <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);
+}

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 <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;
+};
+
+}
+}
+}

libsolidity/formal/Z3Interface.h

@@ -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;
 };
 
 }