Merge pull request #10540 from ethereum/smt_file_level

Do not run SMTChecker when file level functions/constants are present.

libsolidity/formal/BMC.cpp

@@ -58,6 +58,10 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
+	/// This is currently used to abort analysis of SourceUnits
+	/// containing file level functions or constants.
+	if (SMTEncoder::analyze(_source))
+	{
 		m_solvedTargets = move(_solvedTargets);
 		m_context.setSolver(m_interface.get());
 		m_context.clear();
@@ -65,6 +69,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 
 		_source.accept(*this);
+	}
 
 	solAssert(m_interface->solvers() > 0, "");
 	// If this check is true, Z3 and CVC4 are not available

libsolidity/formal/CHC.cpp

@@ -69,6 +69,10 @@ void CHC::analyze(SourceUnit const& _source)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
+	/// This is currently used to abort analysis of SourceUnits
+	/// containing file level functions or constants.
+	if (SMTEncoder::analyze(_source))
+	{
 		resetSourceAnalysis();
 
 		set<SourceUnit const*, EncodingContext::IdCompare> sources;
@@ -81,6 +85,7 @@ void CHC::analyze(SourceUnit const& _source)
 			source->accept(*this);
 
 		checkVerificationTargets();
+	}
 
 	bool ranSolver = true;
 #ifndef HAVE_Z3

libsolidity/formal/SMTEncoder.cpp

@@ -40,6 +40,38 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 {
 }
 
+bool SMTEncoder::analyze(SourceUnit const& _source)
+{
+	set<SourceUnit const*, smt::EncodingContext::IdCompare> sources;
+	sources.insert(&_source);
+	for (auto const& source: _source.referencedSourceUnits(true))
+		sources.insert(source);
+
+	bool analysis = true;
+	for (auto source: sources)
+		for (auto node: source->nodes())
+			if (auto function = dynamic_pointer_cast<FunctionDefinition>(node))
+			{
+				m_errorReporter.warning(
+					6660_error,
+					function->location(),
+					"Model checker analysis was not possible because file level functions are not supported."
+				);
+				analysis = false;
+			}
+			else if (auto var = dynamic_pointer_cast<VariableDeclaration>(node))
+			{
+				m_errorReporter.warning(
+					8195_error,
+					var->location(),
+					"Model checker analysis was not possible because file level constants are not supported."
+				);
+				analysis = false;
+			}
+
+	return analysis;
+}
+
 bool SMTEncoder::visit(ContractDefinition const& _contract)
 {
 	solAssert(m_currentContract, "");

libsolidity/formal/SMTEncoder.h

@@ -52,6 +52,9 @@ class SMTEncoder: public ASTConstVisitor
 public:
 	SMTEncoder(smt::EncodingContext& _context);
 
+	/// @returns true if engine should proceed with analysis.
+	bool analyze(SourceUnit const& _sources);
+
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 

test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+uint constant A = 42;
+contract C {
+	function f(uint x) public pure returns (uint) {
+		return x + A;
+	}
+}
+// ----
+// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported.
+// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported.

test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+uint256 constant x = 56;
+enum ActionChoices {GoLeft, GoRight, GoStraight, Sit}
+ActionChoices constant choices = ActionChoices.GoRight;
+bytes32 constant st = "abc\x00\xff__";
+contract C {
+	function i() public returns (uint, ActionChoices, bytes32) {
+		return (x, choices, st);
+	}
+}
+// ----
+// Warning 2018: (220-310): Function state mutability can be restricted to pure
+// Warning 8195: (32-55): Model checker analysis was not possible because file level constants are not supported.
+// Warning 8195: (111-165): Model checker analysis was not possible because file level constants are not supported.
+// Warning 8195: (167-204): Model checker analysis was not possible because file level constants are not supported.
+// Warning 8195: (32-55): Model checker analysis was not possible because file level constants are not supported.
+// Warning 8195: (111-165): Model checker analysis was not possible because file level constants are not supported.
+// Warning 8195: (167-204): Model checker analysis was not possible because file level constants are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_1.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	uint[] data;
+	function f(uint x, uint[] calldata input) public view returns (uint, uint) {
+		(uint a, uint[] calldata b) = fun(input, data);
+		return (a, b.length + x);
+	}
+}
+function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[] calldata) {
+	return (_y[0], _x);
+}
+// ----
+// Warning 6660: (220-334): Model checker analysis was not possible because file level functions are not supported.
+// Warning 6660: (220-334): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_2.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() external {
+		f();
+	}
+}
+function f() {}
+// ----
+// Warning 6660: (82-97): Model checker analysis was not possible because file level functions are not supported.
+// Warning 6660: (82-97): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_3.sol

@@ -0,0 +1,5 @@
+pragma experimental SMTChecker;
+function f() view {}
+// ----
+// Warning 6660: (32-52): Model checker analysis was not possible because file level functions are not supported.
+// Warning 6660: (32-52): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_4.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+function f()pure {
+	ufixed a = uint64(1) + ufixed(2);
+}
+// ----
+// Warning 2072: (52-60): Unused local variable.
+// Warning 6660: (32-87): Model checker analysis was not possible because file level functions are not supported.
+// Warning 6660: (32-87): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_5.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract K {}
+function f() pure {
+	(abi.encode, "");
+}
+// ----
+// Warning 6133: (67-83): Statement has no effect.
+// Warning 6660: (46-86): Model checker analysis was not possible because file level functions are not supported.
+// Warning 6660: (46-86): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+uint constant A = 42;
+contract C {
+	uint[] data;
+	function f(uint x, uint[] calldata input) public view returns (uint, uint) {
+		(uint a, uint[] calldata b) = fun(input, data);
+		return (a, b.length + x + A);
+	}
+}
+function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[] calldata) {
+	return (_y[0], _x);
+}
+// ----
+// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported.
+// Warning 6660: (246-360): Model checker analysis was not possible because file level functions are not supported.
+// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported.
+// Warning 6660: (246-360): Model checker analysis was not possible because file level functions are not supported.