Merge pull request #15204 from ethereum/smt-tests-update

SMTChecker: Bring back assertions in "external_calls" SMTChecker tests

Author: blishko

docs/contributing.rst

@@ -93,7 +93,8 @@ Prerequisites
 
 For running all compiler tests you may want to optionally install a few
 dependencies (`evmone <https://github.com/ethereum/evmone/releases>`_,
-`libz3 <https://github.com/Z3Prover/z3>`_).
+`libz3 <https://github.com/Z3Prover/z3>`_, `Eldarica <https://github.com/uuverifiers/eldarica/>`_,
+`cvc5 <https://github.com/cvc5/cvc5>`).
 
 On macOS systems, some of the testing scripts expect GNU coreutils to be installed.
 This can be easiest accomplished using Homebrew: ``brew install coreutils``.
@@ -133,11 +134,14 @@ extension ``.so`` on Linux, ``.dll`` on Windows systems and ``.dylib`` on macOS.
 
 For running SMT tests, the ``libz3`` library must be installed and locatable
 by ``cmake`` during compiler configure stage.
+A few SMT tests use ``Eldarica`` instead of ``Z3``.
+``Eldarica`` is a runtime dependency, its executable (``eld``) must be present in ``PATH`` for the tests to pass.
+However, if ``Eldarica`` is not found, these tests will be automatically skipped.
 
 If the ``libz3`` library is not installed on your system, you should disable the
 SMT tests by exporting ``SMT_FLAGS=--no-smt`` before running ``./scripts/tests.sh`` or
 running ``./scripts/soltest.sh --no-smt``.
-These tests are ``libsolidity/smtCheckerTests`` and ``libsolidity/smtCheckerTestsJSON``.
+These tests are ``libsolidity/smtCheckerTests``.
 
 .. note::
 

docs/installing-solidity.rst

@@ -527,19 +527,24 @@ If you are interested what CMake options are available run ``cmake .. -LH``.
 
 SMT Solvers
 -----------
-Solidity can be built against SMT solvers and will do so by default if
-they are found in the system. Each solver can be disabled by a ``cmake`` option.
+Solidity can be built against Z3 SMT solver and will do so by default if
+it is found in the system. Z3 can be disabled by a ``cmake`` option.
 
 *Note: In some cases, this can also be a potential workaround for build failures.*
 
 
-Inside the build folder you can disable them, since they are enabled by default:
+Inside the build folder you can disable Z3, since it is enabled by default:
 
 .. code-block:: bash
 
-    # disables only Z3 SMT Solver.
+    # disables Z3 SMT Solver.
     cmake .. -DUSE_Z3=OFF
 
+.. note::
+
+    Solidity can optionally use other solvers, namely ``cvc5`` and ``Eldarica``,
+    but their presence is checked only at runtime, they are not needed for the build to succeed.
+
 The Version String in Detail
 ============================
 

libsolidity/interface/SMTSolverCommand.cpp

@@ -63,7 +63,7 @@ void SMTSolverCommand::setCvc5(std::optional<unsigned int> timeoutInMilliseconds
 	}
 }
 
-ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query)
+ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query) const
 {
 	try
 	{

libsolidity/interface/SMTSolverCommand.h

@@ -29,9 +29,9 @@ class SMTSolverCommand
 {
 public:
 	/// Calls an SMT solver with the given query.
-	frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query);
+	frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query) const;
 
-	frontend::ReadCallback::Callback solver()
+	frontend::ReadCallback::Callback solver() const
 	{
 		return [this](std::string const& _kind, std::string const& _query) { return solve(_kind, _query); };
 	}

libsolidity/interface/UniversalCallback.h

@@ -46,7 +46,7 @@ class UniversalCallback
 		solAssert(false, "Unknown callback kind.");
 	}
 
-	frontend::ReadCallback::Callback callback()
+	frontend::ReadCallback::Callback callback() const
 	{
 		return *this;
 	}

test/libsolidity/SMTCheckerTest.cpp

@@ -25,8 +25,11 @@ using namespace solidity;
 using namespace solidity::langutil;
 using namespace solidity::frontend;
 using namespace solidity::frontend::test;
+using namespace solidity::test;
 
-SMTCheckerTest::SMTCheckerTest(std::string const& _filename): SyntaxTest(_filename, EVMVersion{})
+SMTCheckerTest::SMTCheckerTest(std::string const& _filename):
+	SyntaxTest(_filename, EVMVersion{}),
+	universalCallback(nullptr, smtCommand)
 {
 	auto contract = m_reader.stringSetting("SMTContract", "");
 	if (!contract.empty())
@@ -168,3 +171,7 @@ void SMTCheckerTest::printUpdatedExpectations(std::ostream &_stream, const std::
 	else
 		CommonSyntaxTest::printUpdatedExpectations(_stream, _linePrefix);
 }
+
+std::unique_ptr<CompilerStack> SMTCheckerTest::createStack() const {
+	return std::make_unique<CompilerStack>(universalCallback.callback());
+}

test/libsolidity/SMTCheckerTest.h

@@ -24,6 +24,9 @@
 
 #include <libsolidity/formal/ModelChecker.h>
 
+#include <libsolidity/interface/SMTSolverCommand.h>
+#include <libsolidity/interface/UniversalCallback.h>
+
 #include <string>
 
 namespace solidity::frontend::test
@@ -36,14 +39,16 @@ class SMTCheckerTest: public SyntaxTest
 	{
 		return std::make_unique<SMTCheckerTest>(_config.filename);
 	}
-	SMTCheckerTest(std::string const& _filename);
+	explicit SMTCheckerTest(std::string const& _filename);
 
 	void setupCompiler(CompilerStack& _compiler) override;
 	void filterObtainedErrors() override;
 
 	void printUpdatedExpectations(std::ostream& _stream, std::string const& _linePrefix) const override;
 
 protected:
+	std::unique_ptr<CompilerStack> createStack() const override;
+
 	/*
 	Options that can be set in the test:
 	SMTEngine: `all`, `chc`, `bmc`, `none`, where the default is `all`.
@@ -56,7 +61,7 @@ class SMTCheckerTest: public SyntaxTest
 		Set in m_modelCheckerSettings.
 	SMTShowUnproved: `yes`, `no`, where the default is `yes`.
 		Set in m_modelCheckerSettings.
-	SMTSolvers: `all`, `cvc5`, `z3`, `none`, where the default is `all`.
+	SMTSolvers: `all`, `cvc5`, `z3`, `eld`, `none`, where the default is `z3`.
 		Set in m_modelCheckerSettings.
 	BMCLoopIterations: number of loop iterations for BMC engine, the default is 1.
 		Set in m_modelCheckerSettings.
@@ -67,6 +72,9 @@ class SMTCheckerTest: public SyntaxTest
 	bool m_ignoreCex = false;
 
 	std::vector<SyntaxTestError> m_unfilteredErrorList;
+
+	SMTSolverCommand smtCommand;
+	UniversalCallback universalCallback;
 };
 
 }

test/libsolidity/smtCheckerTests/external_calls/call_with_value_3.sol

@@ -3,13 +3,14 @@ contract C {
 		require(address(this).balance > 100);
 		i.call{value: 20}("");
 		assert(address(this).balance > 0); // should hold
-		// Disabled due to Spacer nondeterminism
-		//assert(address(this).balance == 0); // should fail
+		assert(address(this).balance == 0); // should fail
 	}
 }
 // ====
-// SMTEngine: all
+// SMTEngine: chc
+// SMTIgnoreCex: yes
+// SMTSolvers: eld
 // ----
 // Warning 9302: (95-116): Return value of low-level calls not used.
-// Warning 6328: (120-153): CHC: Assertion violation might happen here.
-// Warning 4661: (120-153): BMC: Assertion violation happens here.
+// Warning 6328: (172-206): CHC: Assertion violation happens here.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_1.sol

@@ -7,12 +7,12 @@ contract C {
 		require(address(this).balance == 100);
 		i.f{value: 10}();
 		assert(address(this).balance == 90); // should hold
-		// Disabled due to Spacer nondeterminism
-		//assert(address(this).balance == 100); // should fail
+		assert(address(this).balance == 100); // should fail
 	}
 }
 // ====
-// SMTEngine: all
+// SMTEngine: chc
+// SMTSolvers: eld
 // ----
-// Warning 6328: (151-186): CHC: Assertion violation might happen here.
-// Warning 4661: (151-186): BMC: Assertion violation happens here.
+// Warning 6328: (205-241): CHC: Assertion violation happens here.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -19,8 +19,7 @@ contract C {
 		address prevOwner = owner;
 		uint z = s.f();
 		assert(z == y);
-		// Disabled because of Spacer nondeterminism.
-		//assert(prevOwner == owner);
+		assert(prevOwner == owner);
 	}
 
 	function g() public view returns (uint) {
@@ -31,5 +30,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 2072: (219-236): Unused local variable.
-// Warning 6328: (266-280): CHC: Assertion violation happens here.
+// Warning 6328: (266-280): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0x0, y = 0, s = 0\nprevOwner = 0x0\nz = 1\n\nTransaction trace:\nC.constructor(){ msg.sender: 0x0 }\nState: owner = 0x0, y = 0, s = 0\nC.f()\n    s.f() -- untrusted external call
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.