Merge pull request #10206 from ethereum/smt_add_bmc_specific

Isoltest SMTChecker option and BMC specific tests

libsolidity/formal/BMC.cpp

@@ -492,7 +492,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 		m_errorReporter.warning(
 			5729_error,
 			_funCall.location(),
-			"Assertion checker does not yet implement this type of function call."
+			"BMC does not yet implement this type of function call."
 		);
 	else
 	{
@@ -910,9 +910,9 @@ void BMC::checkBooleanNotConstant(
 	m_interface->pop();
 
 	if (positiveResult == smtutil::CheckResult::ERROR || negatedResult == smtutil::CheckResult::ERROR)
-		m_errorReporter.warning(8592_error, _condition.location(), "Error trying to invoke SMT solver.");
+		m_errorReporter.warning(8592_error, _condition.location(), "BMC: Error trying to invoke SMT solver.");
 	else if (positiveResult == smtutil::CheckResult::CONFLICTING || negatedResult == smtutil::CheckResult::CONFLICTING)
-		m_errorReporter.warning(3356_error, _condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
+		m_errorReporter.warning(3356_error, _condition.location(), "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
 	else if (positiveResult == smtutil::CheckResult::SATISFIABLE && negatedResult == smtutil::CheckResult::SATISFIABLE)
 	{
 		// everything fine.
@@ -922,7 +922,7 @@ void BMC::checkBooleanNotConstant(
 		// can't do anything.
 	}
 	else if (positiveResult == smtutil::CheckResult::UNSATISFIABLE && negatedResult == smtutil::CheckResult::UNSATISFIABLE)
-		m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
+		m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
 	else
 	{
 		string description;
@@ -957,7 +957,7 @@ BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> const& _expres
 	}
 	catch (smtutil::SolverError const& _e)
 	{
-		string description("Error querying SMT solver");
+		string description("BMC: Error querying SMT solver");
 		if (_e.comment())
 			description += ": " + *_e.comment();
 		m_errorReporter.warning(8140_error, description);

scripts/error_codes.py

@@ -221,11 +221,11 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
 
     old_source_only_ids = {
         "1123", "1220", "1584", "1823", "1950",
-        "1988", "2512", "2657", "2800",
+        "1988", "2657", "2800",
-        "3046", "3263", "3356", "3682", "3876",
+        "3263", "3356", "3682", "3876",
         "3893", "3996", "4010", "4802",
         "5073", "5188", "5272",
-        "5622", "6084", "6272", "7128", "7186",
+        "5622", "6272", "7128", "7186",
         "7589", "7593", "7653", "7885", "8065", "8084", "8140",
         "8312", "8592", "9011",
         "9085", "9390", "9551",

test/libsolidity/SMTCheckerTest.cpp

@@ -19,8 +19,6 @@
 #include <test/libsolidity/SMTCheckerTest.h>
 #include <test/Common.h>
 
-#include <libsolidity/formal/ModelChecker.h>
-
 using namespace std;
 using namespace solidity;
 using namespace solidity::langutil;
@@ -47,7 +45,13 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 	if (!available.cvc4)
 		m_enabledSolvers.cvc4 = false;
 
-	if (m_enabledSolvers.none())
+	auto engine = ModelCheckerEngine::fromString(m_reader.stringSetting("SMTEngine", "all"));
+	if (engine)
+		m_modelCheckerSettings.engine = *engine;
+	else
+		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT engine choice."));
+
+	if (m_enabledSolvers.none() || m_modelCheckerSettings.engine.none())
 		m_shouldRun = false;
 }
 
@@ -55,6 +59,7 @@ TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePr
 {
 	setupCompiler();
 	compiler().setSMTSolverChoice(m_enabledSolvers);
+	compiler().setModelCheckerSettings(m_modelCheckerSettings);
 	parseAndAnalyze();
 	filterObtainedErrors();
 

test/libsolidity/SMTCheckerTest.h

@@ -22,6 +22,8 @@
 
 #include <libsmtutil/SolverInterface.h>
 
+#include <libsolidity/formal/ModelChecker.h>
+
 #include <string>
 
 namespace solidity::frontend::test
@@ -39,6 +41,12 @@ public:
 	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
 
 protected:
+	/// This contains engine and timeout.
+	/// The engine can be set via option SMTEngine in the test.
+	/// The possible options are `all`, `chc`, `bmc`, `none`,
+	/// where the default is `all`.
+	ModelCheckerSettings m_modelCheckerSettings;
+
 	/// This is set via option SMTSolvers in the test.
 	/// The possible options are `all`, `z3`, `cvc4`, `none`,
 	/// where if none is given the default used option is `all`.

test/libsolidity/smtCheckerTests/bmc_coverage/assert.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) public pure {
+		assert(x > 0);
+	}
+	function g(uint x) public pure {
+		require(x >= 0);
+	}
+	function h(uint x) public pure {
+		require(x == 2);
+		require(x != 2);
+	}
+	function i(uint x) public pure {
+		if (false) {
+			if (x != 2) {
+			}
+		}
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (81-94): BMC: Assertion violation happens here.
+// Warning 6838: (143-149): BMC: Condition is always true.
+// Warning 6838: (218-224): BMC: Condition is always false.
+// Warning 2512: (286-292): BMC: Condition unreachable.

test/libsolidity/smtCheckerTests/bmc_coverage/funds.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(address payable a) public {
+		a.transfer(200);
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 1236: (87-102): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/bmc_coverage/math.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+contract C {
+	uint z = 1;
+	uint w = z - 3;
+	function a(uint x, uint y) public pure returns (uint) {
+		return x + y;
+	}
+	function s(uint x, uint y) public pure returns (uint) {
+		return x - y;
+	}
+	function m(uint x, uint y) public pure returns (uint) {
+		return x * y;
+	}
+	function d(uint x, uint y) public pure returns (uint) {
+		return x / y;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 2661: (141-146): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4144: (217-222): BMC: Underflow (resulting value less than 0) happens here.
+// Warning 2661: (293-298): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 3046: (369-374): BMC: Division by zero happens here.
+// Warning 6084: (68-73): BMC: Underflow (resulting value less than 0) happens here.

test/libsolidity/smtCheckerTests/complex/slither/external_function.sol

@@ -85,4 +85,4 @@ contract InternalCall {
 // Warning 2018: (1280-1342): Function state mutability can be restricted to pure
 // Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
 // Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
-// Warning 5729: (1403-1408): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (1403-1408): BMC does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol

@@ -17,9 +17,9 @@ contract C {
 // Warning 7229: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons
 // Warning 6328: (207-227): CHC: Assertion violation happens here.
 // Warning 6328: (231-245): CHC: Assertion violation happens here.
-// Warning 5729: (214-218): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (214-218): BMC does not yet implement this type of function call.
-// Warning 5729: (222-226): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (222-226): BMC does not yet implement this type of function call.
 // Warning 7229: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons
-// Warning 5729: (214-218): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (214-218): BMC does not yet implement this type of function call.
-// Warning 5729: (222-226): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (222-226): BMC does not yet implement this type of function call.
 // Warning 7229: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons

test/libsolidity/smtCheckerTests/types/function_type_call.sol

@@ -9,5 +9,5 @@ contract C {
 	}
 }
 // ----
-// Warning 5729: (121-125): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (121-125): BMC does not yet implement this type of function call.
-// Warning 5729: (121-125): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (121-125): BMC does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/function_type_nested.sol

@@ -16,10 +16,10 @@ contract C {
 // Warning 8364: (212-214): Assertion checker does not yet implement type function (function (uint256))
 // Warning 6031: (255-257): Internal error: Expression undefined for SMT solver.
 // Warning 8364: (255-257): Assertion checker does not yet implement type function (function (uint256))
-// Warning 5729: (123-128): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (123-128): BMC does not yet implement this type of function call.
 // Warning 8115: (152-197): Assertion checker does not yet support the type of this variable.
 // Warning 8364: (212-214): Assertion checker does not yet implement type function (function (uint256))
-// Warning 5729: (212-219): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (212-219): BMC does not yet implement this type of function call.
 // Warning 6031: (255-257): Internal error: Expression undefined for SMT solver.
 // Warning 8364: (255-257): Assertion checker does not yet implement type function (function (uint256))
-// Warning 5729: (212-219): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (212-219): BMC does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol

@@ -20,11 +20,11 @@ contract C {
 // Warning 1695: (287-288): Assertion checker does not yet support this global variable.
 // Warning 6031: (327-329): Internal error: Expression undefined for SMT solver.
 // Warning 8364: (327-329): Assertion checker does not yet implement type function (function (uint256))
-// Warning 5729: (195-200): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (195-200): BMC does not yet implement this type of function call.
 // Warning 8115: (224-269): Assertion checker does not yet support the type of this variable.
 // Warning 8364: (284-286): Assertion checker does not yet implement type function (function (uint256))
 // Warning 1695: (287-288): Assertion checker does not yet support this global variable.
-// Warning 5729: (284-291): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (284-291): BMC does not yet implement this type of function call.
 // Warning 6031: (327-329): Internal error: Expression undefined for SMT solver.
 // Warning 8364: (327-329): Assertion checker does not yet implement type function (function (uint256))
-// Warning 5729: (284-291): Assertion checker does not yet implement this type of function call.
+// Warning 5729: (284-291): BMC does not yet implement this type of function call.