Merge pull request #13000 from ethereum/smt_fix_recursive

[SMTChecker] Fix check that solver is available

Changelog.md

@@ -13,9 +13,10 @@ Compiler Features:
 
 Bugfixes:
  * Type Checker: Properly check restrictions of ``using ... global`` in conjunction with libraries.
-* Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`.
+ * Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`.
-* TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``.
+ * SMTChecker: Fix bug when z3 is selected but not available at runtime.
-* View Pure Checker: Mark ``returndatasize`` and ``returndatacopy`` as view to disallow them in inline assembly blocks in pure functions.
+ * TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``.
+ * View Pure Checker: Mark ``returndatasize`` and ``returndatacopy`` as view to disallow them in inline assembly blocks in pure functions.
 
 
 

libsolidity/formal/BMC.cpp

@@ -63,15 +63,14 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 {
 	if (m_interface->solvers() == 0)
 	{
-		if (!m_noSolverWarning)
-		{
-			m_noSolverWarning = true;
 		m_errorReporter.warning(
 			7710_error,
 			SourceLocation(),
 			"BMC analysis was not possible since no SMT solver was found and enabled."
+#ifdef HAVE_Z3_DLOPEN
+			" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
+#endif
 		);
-		}
 		return;
 	}
 
@@ -108,10 +107,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		m_interface->solvers() == 1 &&
 		m_settings.solvers.smtlib2
 	)
-	{
-		if (!m_noSolverWarning)
-		{
-			m_noSolverWarning = true;
 		m_errorReporter.warning(
 			8084_error,
 			SourceLocation(),
@@ -121,8 +116,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 			" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
 #endif
 		);
-		}
-	}
 }
 
 bool BMC::shouldInlineFunctionCall(

libsolidity/formal/CHC.cpp

@@ -60,21 +60,15 @@ using namespace solidity::frontend::smt;
 CHC::CHC(
 	EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
-	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
+	map<util::h256, string> const& _smtlib2Responses,
-	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
+	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider)
+	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
+	m_smtlib2Responses(_smtlib2Responses),
+	m_smtCallback(_smtCallback)
 {
-	bool usesZ3 = m_settings.solvers.z3;
-#ifdef HAVE_Z3
-	usesZ3 = usesZ3 && Z3Interface::available();
-#else
-	usesZ3 = false;
-#endif
-	if (!usesZ3 && m_settings.solvers.smtlib2)
-		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -82,17 +76,26 @@ void CHC::analyze(SourceUnit const& _source)
 	if (!shouldAnalyze(_source))
 		return;
 
-	if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2)
+	bool usesZ3 = m_settings.solvers.z3;
+#ifdef HAVE_Z3_DLOPEN
+	if (m_settings.solvers.z3 && !Z3Interface::available())
 	{
-		if (!m_noSolverWarning)
+		usesZ3 = false;
+		m_errorReporter.warning(
+			8158_error,
+			SourceLocation(),
+			"z3 was selected as a Horn solver for CHC analysis but libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
+		);
+	}
+#endif
+
+	if (!usesZ3 && !m_settings.solvers.smtlib2)
 	{
-			m_noSolverWarning = true;
 		m_errorReporter.warning(
 			7649_error,
 			SourceLocation(),
-				"CHC analysis was not possible since no Horn solver was enabled."
+			"CHC analysis was not possible since no Horn solver was found and enabled."
 		);
-		}
 		return;
 	}
 
@@ -115,20 +118,13 @@ void CHC::analyze(SourceUnit const& _source)
 	// actually given and the queries were solved.
 	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
 		ranSolver = smtLibInterface->unhandledQueries().empty();
-	if (!ranSolver && !m_noSolverWarning)
+	if (!ranSolver)
-	{
-		m_noSolverWarning = true;
 		m_errorReporter.warning(
 			3996_error,
 			SourceLocation(),
-#ifdef HAVE_Z3_DLOPEN
-			"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
-#else
 			"CHC analysis was not possible. No Horn solver was available."
 			" None of the installed solvers was enabled."
-#endif
 		);
-	}
 }
 
 vector<string> CHC::unhandledQueries() const
@@ -1012,6 +1008,11 @@ void CHC::resetSourceAnalysis()
 #endif
 	if (!usesZ3)
 	{
+		solAssert(m_settings.solvers.smtlib2);
+
+		if (!m_interface)
+			m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.timeout);
+
 		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
 		solAssert(smtlib2Interface, "");
 		smtlib2Interface->reset();

libsolidity/formal/CHC.h

@@ -421,6 +421,9 @@ private:
 
 	/// CHC solver.
 	std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
+
+	std::map<util::h256, std::string> const& m_smtlib2Responses;
+	ReadCallback::Callback const& m_smtCallback;
 };
 
 }

libsolidity/formal/SMTEncoder.h

@@ -426,8 +426,6 @@ protected:
 
 	smt::VariableUsage m_variableUsage;
 	bool m_arrayAssignmentHappened = false;
-	// True if the "No SMT solver available" warning was already created.
-	bool m_noSolverWarning = false;
 
 	/// Stores the instances of an Uninterpreted Function applied to arguments.
 	/// These may be direct application of UFs or Array index access.

scripts/error_codes.py

@@ -232,7 +232,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "3893", "3996", "4010", "4802",
         "5272", "5622", "7128", "7400",
         "7589", "7593", "7649", "7710",
-        "8065", "8084", "8140",
+        "8065", "8084", "8140", "8158",
         "8312", "8592", "9134", "9609",
     }
 

test/cmdlineTests/standard_model_checker_solvers_none/output.json

@@ -1,5 +1,5 @@
-{"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was enabled.
+{"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was found and enabled.
 
-","message":"CHC analysis was not possible since no Horn solver was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled.
+","message":"CHC analysis was not possible since no Horn solver was found and enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled.
 
 ","message":"BMC analysis was not possible since no SMT solver was found and enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}

test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol

@@ -21,4 +21,6 @@ contract C is B {
 // Warning 7812: (b.sol:62-75): BMC: Assertion violation might happen here.
 // Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
 // Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here.
+// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
 // Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here.
+// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.