Merge pull request #7062 from ethereum/smt_chc_checker

[SMTChecker] Add skeleton for CHC

libsolidity/CMakeLists.txt

@@ -77,6 +77,8 @@ set(sources
 	codegen/ir/IRLValue.h
 	formal/BMC.cpp
 	formal/BMC.h
+	formal/CHC.cpp
+	formal/CHC.h
 	formal/CHCSolverInterface.h
 	formal/EncodingContext.cpp
 	formal/EncodingContext.h

libsolidity/formal/BMC.cpp

@@ -43,12 +43,13 @@ BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256
 #endif
 }
 
-void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
+void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner, set<Expression const*> _safeAssertions)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
 	m_scanner = _scanner;
 
+	m_safeAssertions += move(_safeAssertions);
 	m_context.setSolver(m_interface);
 	m_context.clear();
 	m_variableUsage.setFunctionInlining(true);
@@ -673,13 +674,14 @@ void BMC::checkBalance(VerificationTarget& _target)
 void BMC::checkAssert(VerificationTarget& _target)
 {
 	solAssert(_target.type == VerificationTarget::Type::Assert, "");
-	checkCondition(
-		_target.constraints && !_target.value,
-		_target.callStack,
-		_target.modelExpressions,
-		_target.expression->location(),
-		"Assertion violation"
-	);
+	if (!m_safeAssertions.count(_target.expression))
+		checkCondition(
+			_target.constraints && !_target.value,
+			_target.callStack,
+			_target.modelExpressions,
+			_target.expression->location(),
+			"Assertion violation"
+		);
 }
 
 void BMC::addVerificationTarget(

libsolidity/formal/BMC.h

@@ -36,6 +36,7 @@
 #include <liblangutil/ErrorReporter.h>
 #include <liblangutil/Scanner.h>
 
+#include <set>
 #include <string>
 #include <vector>
 
@@ -55,7 +56,7 @@ class BMC: public SMTEncoder
 public:
 	BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
 
-	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
+	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner, std::set<Expression const*> _safeAssertions);
 
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to
@@ -175,6 +176,9 @@ private:
 
 	std::vector<VerificationTarget> m_verificationTargets;
 
+	/// Assertions that are known to be safe.
+	std::set<Expression const*> m_safeAssertions;
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 };
 

libsolidity/formal/CHC.cpp

@@ -0,0 +1,178 @@
+/*
+	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/CHC.h>
+
+#ifdef HAVE_Z3
+#include <libsolidity/formal/Z3CHCInterface.h>
+#endif
+
+#include <libsolidity/formal/SymbolicTypes.h>
+
+#include <libsolidity/ast/TypeProvider.h>
+
+using namespace std;
+using namespace dev;
+using namespace langutil;
+using namespace dev::solidity;
+
+CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter):
+	SMTEncoder(_context),
+#ifdef HAVE_Z3
+	m_interface(make_shared<smt::Z3CHCInterface>()),
+#endif
+	m_outerErrorReporter(_errorReporter)
+{
+}
+
+void CHC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
+{
+	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
+
+	m_scanner = _scanner;
+
+#ifdef HAVE_Z3
+	auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
+	solAssert(z3Interface, "");
+	m_context.setSolver(z3Interface->z3Interface());
+	m_context.clear();
+	m_variableUsage.setFunctionInlining(false);
+
+	_source.accept(*this);
+#endif
+}
+
+bool CHC::visit(ContractDefinition const& _contract)
+{
+	if (!shouldVisit(_contract))
+		return false;
+
+	reset();
+
+	if (!SMTEncoder::visit(_contract))
+		return false;
+
+	return true;
+}
+
+void CHC::endVisit(ContractDefinition const& _contract)
+{
+	if (!shouldVisit(_contract))
+		return;
+
+	SMTEncoder::endVisit(_contract);
+}
+
+bool CHC::visit(FunctionDefinition const& _function)
+{
+	if (!shouldVisit(_function))
+		return false;
+
+	solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented");
+	m_currentFunction = &_function;
+
+	SMTEncoder::visit(*m_currentFunction);
+
+	return false;
+}
+
+void CHC::endVisit(FunctionDefinition const& _function)
+{
+	if (!shouldVisit(_function))
+		return;
+
+	solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented");
+	m_currentFunction = nullptr;
+
+	SMTEncoder::endVisit(_function);
+}
+
+bool CHC::visit(IfStatement const& _if)
+{
+	solAssert(m_currentFunction, "");
+
+	SMTEncoder::visit(_if);
+
+	return false;
+}
+
+void CHC::endVisit(FunctionCall const& _funCall)
+{
+	solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
+
+	if (_funCall.annotation().kind == FunctionCallKind::FunctionCall)
+	{
+		FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+		if (funType.kind() == FunctionType::Kind::Assert)
+			visitAssert(_funCall);
+	}
+
+	SMTEncoder::endVisit(_funCall);
+}
+
+void CHC::visitAssert(FunctionCall const&)
+{
+}
+
+void CHC::reset()
+{
+	m_verificationTargets.clear();
+	m_safeAssertions.clear();
+}
+
+bool CHC::shouldVisit(ContractDefinition const& _contract) const
+{
+	if (
+		_contract.isLibrary() ||
+		_contract.isInterface()
+	)
+		return false;
+	return true;
+}
+
+bool CHC::shouldVisit(FunctionDefinition const& _function) const
+{
+	if (
+		_function.isPublic() &&
+		_function.isImplemented()
+	)
+		return true;
+	return false;
+}
+
+bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
+{
+	smt::CheckResult result;
+	vector<string> values;
+	tie(result, values) = m_interface->query(_query);
+	switch (result)
+	{
+	case smt::CheckResult::SATISFIABLE:
+		break;
+	case smt::CheckResult::UNSATISFIABLE:
+		return true;
+	case smt::CheckResult::UNKNOWN:
+		break;
+	case smt::CheckResult::CONFLICTING:
+		m_outerErrorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
+		break;
+	case smt::CheckResult::ERROR:
+		m_outerErrorReporter.warning(_location, "Error trying to invoke SMT solver.");
+		break;
+	}
+	return false;
+}

libsolidity/formal/CHC.h

@@ -0,0 +1,100 @@
+/*
+	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/>.
+*/
+
+/**
+ * Model checker based on Constrained Horn Clauses.
+ *
+ * A Solidity contract's CFG is encoded into a system of Horn clauses where
+ * each block has a predicate and edges are rules.
+ *
+ * The entry block is the constructor which has no in-edges.
+ * The constructor has one out-edge to an artificial block named _Interface_
+ * which has in/out-edges from/to all public functions.
+ *
+ * Loop invariants for Interface -> Interface' are state invariants.
+ */
+
+#pragma once
+
+#include <libsolidity/formal/SMTEncoder.h>
+
+#include <libsolidity/formal/CHCSolverInterface.h>
+
+#include <set>
+
+namespace dev
+{
+namespace solidity
+{
+
+class CHC: public SMTEncoder
+{
+public:
+	CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter);
+
+	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
+
+	std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }
+
+private:
+	/// Visitor functions.
+	//@{
+	bool visit(ContractDefinition const& _node) override;
+	void endVisit(ContractDefinition const& _node) override;
+	bool visit(FunctionDefinition const& _node) override;
+	void endVisit(FunctionDefinition const& _node) override;
+	bool visit(IfStatement const& _node) override;
+	void endVisit(FunctionCall const& _node) override;
+
+	void visitAssert(FunctionCall const& _funCall);
+	//@}
+
+	/// Helpers.
+	//@{
+	void reset();
+	bool shouldVisit(ContractDefinition const& _contract) const;
+	bool shouldVisit(FunctionDefinition const& _function) const;
+	//@}
+
+	/// Solver related.
+	//@{
+	/// @returns true if query is unsatisfiable (safe).
+	bool query(smt::Expression const& _query, langutil::SourceLocation const& _location);
+	//@}
+
+	/// Verification targets.
+	//@{
+	std::vector<Expression const*> m_verificationTargets;
+
+	/// Assertions proven safe.
+	std::set<Expression const*> m_safeAssertions;
+	//@}
+
+	/// Control-flow.
+	//@{
+	FunctionDefinition const* m_currentFunction = nullptr;
+	//@}
+
+	/// CHC solver.
+	std::shared_ptr<smt::CHCSolverInterface> m_interface;
+
+	/// ErrorReporter that comes from CompilerStack.
+	langutil::ErrorReporter& m_outerErrorReporter;
+};
+
+}
+}

libsolidity/formal/ModelChecker.cpp

@@ -24,6 +24,7 @@ using namespace dev::solidity;
 
 ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
 	m_bmc(m_context, _errorReporter, _smtlib2Responses),
+	m_chc(m_context, _errorReporter),
 	m_context()
 {
 }
@@ -33,7 +34,8 @@ void ModelChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const&
 	if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_bmc.analyze(_source, _scanner);
+	m_chc.analyze(_source, _scanner);
+	m_bmc.analyze(_source, _scanner, m_chc.safeAssertions());
 }
 
 vector<string> ModelChecker::unhandledQueries()

libsolidity/formal/ModelChecker.h

@@ -23,6 +23,7 @@
 #pragma once
 
 #include <libsolidity/formal/BMC.h>
+#include <libsolidity/formal/CHC.h>
 #include <libsolidity/formal/EncodingContext.h>
 
 #include <libsolidity/interface/ReadFile.h>
@@ -56,6 +57,9 @@ private:
 	/// Bounded Model Checker engine.
 	BMC m_bmc;
 
+	/// Constrained Horn Clauses engine.
+	CHC m_chc;
+
 	/// Stores the context of the encoding.
 	smt::EncodingContext m_context;
 };

test/libsolidity/smtCheckerTestsJSON/multi.json

@@ -3,9 +3,9 @@
 	{
 		"smtlib2responses":
 		{
-			"0x6e5cf865938b82f1627009d26ecb4c59e9b8c05cc1024ccf548b9b94c1c73e56": "unsat\n",
-			"0x890d45bd5b96d51c4d11683bcf3b7547cea993b3e15961c216a0a782d5d3ccb2": "sat\n((|EVALEXPR_0| 0))\n",
-			"0xa649be28767cedec4a7b7f5591e3fb237447405a823dbd861869eb35d91bebce": "sat\n((|EVALEXPR_0| 1))\n"
+			"0x0e5da3eca3d435940329103801b225604b2117438acea19504f980c5c1aaa571": "sat\n((|EVALEXPR_0| 0))\n",
+			"0xb83649564ec7bcc0c986c9c9c9d3fc28d90ad276ed2a6605fd48d10d30bef5e6": "sat\n((|EVALEXPR_0| 1))\n",
+			"0xeb8a2252226643551271abef0bc6c5c68b3a12fa509ad78a687c2cf76ddb4148": "unsat\n"
 		}
 	}
 }

test/libsolidity/smtCheckerTestsJSON/simple.json

@@ -3,7 +3,7 @@
 	{
 		"smtlib2responses":
 		{
-			"0xcae00c08b91a968103a89431c473645366101a2b037d72aa10fbe3099ccd6931": "sat\n((|EVALEXPR_0| 0))\n"
+			"0x9804531ddd39e0d6df2dcb24d8dfd9e7b8c7ed3ece5d33f1680063d3e02f18f0": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}
 }