Isoltets SMTChecker option and BMC specific tests

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: (222-226): 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): 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: (222-226): 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): 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): 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): 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.