Merge pull request #11222 from ethereum/smt_free_functions

[SMTChecker] Free functions and constants

Changelog.md

@@ -17,6 +17,7 @@ Compiler Features:
  * SMTChecker: Deprecate ``pragma experimental SMTChecker;`` and set default model checker engine to ``none``.
  * SMTChecker: Report local variables in CHC counterexamples.
  * SMTChecker: Report out of bounds index access for arrays and fixed bytes.
+ * SMTChecker: Support file level functions and constants.
  * Standard JSON: Model checker option ``settings.modelChecker.targets`` also accepts ``outOfBounds``.
  * Standard JSON: Model checker option ``settings.modelChecker.targets`` takes an array of string targets instead of string of comma separated targets.
  * Yul Optimizer: Added a new step FunctionSpecializer, that specializes a function with its literal arguments.

libsolidity/formal/BMC.cpp

@@ -61,8 +61,6 @@ BMC::BMC(
 
 void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
 {
-	/// This is currently used to abort analysis of SourceUnits
-	/// containing file level functions or constants.
 	if (SMTEncoder::analyze(_source))
 	{
 		m_solvedTargets = move(_solvedTargets);
@@ -70,6 +68,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		m_context.clear();
 		m_context.setAssertionAccumulation(true);
 		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
+		createFreeConstants(sourceDependencies(_source));
 
 		_source.accept(*this);
 	}
@@ -149,11 +148,13 @@ void BMC::endVisit(ContractDefinition const& _contract)
 
 bool BMC::visit(FunctionDefinition const& _function)
 {
+	// Free functions need to be visited in the context of a contract.
+	if (!m_currentContract)
+		return false;
+
 	auto contract = dynamic_cast<ContractDefinition const*>(_function.scope());
-	solAssert(contract, "");
-	solAssert(m_currentContract, "");
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
-	if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end())
+	if (contract && find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end())
 		createStateVariables(*contract);
 
 	if (m_callStack.empty())
@@ -165,7 +166,10 @@ bool BMC::visit(FunctionDefinition const& _function)
 	}
 
 	if (_function.isConstructor())
-		inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
+	{
+		solAssert(contract, "");
+		inlineConstructorHierarchy(*contract);
+	}
 
 	/// Already visits the children.
 	SMTEncoder::visit(_function);
@@ -175,6 +179,10 @@ bool BMC::visit(FunctionDefinition const& _function)
 
 void BMC::endVisit(FunctionDefinition const& _function)
 {
+	// Free functions need to be visited in the context of a contract.
+	if (!m_currentContract)
+		return;
+
 	if (isRootFunction())
 	{
 		checkVerificationTargets();

libsolidity/formal/CHC.cpp

@@ -76,16 +76,13 @@ CHC::CHC(
 
 void CHC::analyze(SourceUnit const& _source)
 {
-	/// 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;
+		auto sources = sourceDependencies(_source);
-		sources.insert(&_source);
+		collectFreeFunctions(sources);
-		for (auto const& source: _source.referencedSourceUnits(true))
+		createFreeConstants(sources);
-			sources.insert(source);
 		for (auto const* source: sources)
 			defineInterfacesAndSummaries(*source);
 		for (auto const* source: sources)
@@ -219,6 +216,10 @@ void CHC::endVisit(ContractDefinition const& _contract)
 
 bool CHC::visit(FunctionDefinition const& _function)
 {
+	// Free functions need to be visited in the context of a contract.
+	if (!m_currentContract)
+		return false;
+
 	if (!_function.isImplemented())
 	{
 		addRule(summary(_function), "summary_function_" + to_string(_function.id()));
@@ -258,6 +259,10 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 void CHC::endVisit(FunctionDefinition const& _function)
 {
+	// Free functions need to be visited in the context of a contract.
+	if (!m_currentContract)
+		return;
+
 	if (!_function.isImplemented())
 		return;
 
@@ -677,19 +682,13 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
 
-	auto scopeContract = currentScopeContract();
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
-	auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract);
 	if (function)
 	{
 		if (m_currentFunction && !m_currentFunction->isConstructor())
 			m_callGraph[m_currentFunction].insert(function);
 		else
 			m_callGraph[m_currentContract].insert(function);
-
-		// Libraries can have constants as their "state" variables,
-		// so we need to ensure they were constructed correctly.
-		if (function->annotation().contract->isLibrary())
-			m_context.addAssertion(interface(*scopeContract));
 	}
 
 	m_context.addAssertion(predicate(_funCall));
@@ -1045,7 +1044,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			addRule(smtutil::Expression::implies(errorFlag().currentValue() == 0, smt::nondetInterface(iface, *contract, m_context, 0, 0)), "base_nondet");
 
 			auto const& resolved = contractFunctions(*contract);
-			for (auto const* function: contractFunctionsWithoutVirtual(*contract))
+			for (auto const* function: contractFunctionsWithoutVirtual(*contract) + allFreeFunctions())
 			{
 				for (auto var: function->parameters())
 					createVariable(*var);
@@ -1310,8 +1309,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	solAssert(m_currentContract, "");
-	auto scopeContract = currentScopeContract();
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
-	auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract);
 	if (!function)
 		return smtutil::Expression(true);
 
@@ -1328,27 +1326,20 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
-	solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), "");
+	solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || contains(hierarchy, contract), "");
-
-	/// If the call is to a library, we use that library as the called contract.
-	/// If the call is to a contract not in the inheritance hierarchy, we also use that as the called contract.
-	/// Otherwise, the call is to some contract in the inheritance hierarchy of the current contract.
-	/// In this case we use current contract as the called one since the interfaces/predicates are different.
-	auto const* calledContract = contains(hierarchy, contract) ? m_currentContract : contract;
-	solAssert(calledContract, "");
 
 	bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
 
-	args += currentStateVariables(*calledContract);
+	args += currentStateVariables(*m_currentContract);
 	args += symbolicArguments(_funCall, m_currentContract);
-	if (!calledContract->isLibrary() && !usesStaticCall)
+	if (!m_currentContract->isLibrary() && !usesStaticCall)
 	{
 		state().newState();
 		for (auto const& var: m_stateVariables)
 			m_context.variable(*var)->increaseIndex();
 	}
 	args += vector<smtutil::Expression>{state().state()};
-	args += currentStateVariables(*calledContract);
+	args += currentStateVariables(*m_currentContract);
 
 	for (auto var: function->parameters() + function->returnParameters())
 	{
@@ -1359,14 +1350,14 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		args.push_back(currentValue(*var));
 	}
 
-	Predicate const& summary = *m_summaries.at(calledContract).at(function);
+	Predicate const& summary = *m_summaries.at(m_currentContract).at(function);
-	auto from = smt::function(summary, calledContract, m_context);
+	auto from = smt::function(summary, m_currentContract, m_context);
 	Predicate const& callPredicate = *createSummaryBlock(
 		*function,
-		*calledContract,
+		*m_currentContract,
 		kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
 	);
-	auto to = smt::function(callPredicate, calledContract, m_context);
+	auto to = smt::function(callPredicate, m_currentContract, m_context);
 	addRule(smtutil::Expression::implies(from, to), to.name);
 
 	return callPredicate(args);
@@ -1427,7 +1418,8 @@ void CHC::verificationTargetEncountered(
 	if (!m_settings.targets.has(_type))
 		return;
 
-	solAssert(m_currentContract || m_currentFunction, "");
+	if (!(m_currentContract || m_currentFunction))
+		return;
 
 	bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor();
 	auto errorId = newErrorId();

libsolidity/formal/Predicate.cpp

@@ -243,9 +243,16 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
 		fun->isFallback() ? "fallback" :
 		fun->isReceive() ? "receive" :
 		fun->name();
-	solAssert(fun->annotation().contract, "");
-	return fun->annotation().contract->name() + "." + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + value;
 
+	string prefix;
+	if (fun->isFree())
+		prefix = !fun->sourceUnitName().empty() ? (fun->sourceUnitName() + ":") : "";
+	else
+	{
+		solAssert(fun->annotation().contract, "");
+		prefix = fun->annotation().contract->name() + ".";
+	}
+	return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + value;
 }
 
 vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const

libsolidity/formal/SMTEncoder.cpp

@@ -51,36 +51,6 @@ 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;
-			}
-
-	if (!analysis)
-		return false;
-
 	state().prepareForSourceUnit(_source);
 
 	return true;
@@ -116,7 +86,7 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 	// the constructor.
 	// Constructors are visited as part of the constructor
 	// hierarchy inlining.
-	for (auto const* function: contractFunctionsWithoutVirtual(_contract))
+	for (auto const* function: contractFunctionsWithoutVirtual(_contract) + allFreeFunctions())
 		if (!function->isConstructor())
 			function->accept(*this);
 
@@ -152,6 +122,8 @@ bool SMTEncoder::visit(ModifierDefinition const&)
 
 bool SMTEncoder::visit(FunctionDefinition const& _function)
 {
+	solAssert(m_currentContract, "");
+
 	m_modifierDepthStack.push_back(-1);
 
 	initializeLocalVariables(_function);
@@ -288,6 +260,8 @@ bool SMTEncoder::visit(PlaceholderStatement const&)
 
 void SMTEncoder::endVisit(FunctionDefinition const&)
 {
+	solAssert(m_currentContract, "");
+
 	popCallStack();
 	solAssert(m_modifierDepthStack.back() == -1, "");
 	m_modifierDepthStack.pop_back();
@@ -442,14 +416,9 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 		auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional<smtutil::Expression> {
 			if (component)
 			{
-				if (auto varDecl = identifierToVariable(*component))
+				if (!m_context.knownExpression(*component))
-					return currentValue(*varDecl);
-				else
-				{
-					if (!m_context.knownExpression(*component))
 						createExpr(*component);
-					return expr(*component);
+				return expr(*component);
-				}
 			}
 			return {};
 		});
@@ -1400,6 +1369,9 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
 		array = m_context.variable(*varDecl);
+
+		if (varDecl && varDecl->isConstant())
+			m_context.addAssertion(currentValue(*varDecl) == expr(*id));
 	}
 	else
 	{
@@ -2604,6 +2576,7 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e
 				solAssert(m_context.knownVariable(*varDecl), "");
 				return varDecl;
 			}
+
 	return nullptr;
 }
 
@@ -2918,6 +2891,15 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
 	return ABIFunctions(_node).abiCalls;
 }
 
+set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies(SourceUnit const& _source)
+{
+	set<SourceUnit const*, ASTNode::CompareByID> sources;
+	sources.insert(&_source);
+	for (auto const& source: _source.referencedSourceUnits(true))
+		sources.insert(source);
+	return sources;
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
 {
 	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
@@ -2963,6 +2945,34 @@ vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _f
 	return args;
 }
 
+void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
+{
+	if (!m_freeFunctions.empty())
+		return;
+
+	for (auto source: _sources)
+		for (auto node: source->nodes())
+			if (auto function = dynamic_cast<FunctionDefinition const*>(node.get()))
+				m_freeFunctions.insert(function);
+			else if (
+				auto contract = dynamic_cast<ContractDefinition const*>(node.get());
+				contract && contract->isLibrary()
+			)
+			{
+				for (auto function: contract->definedFunctions())
+					if (!function->isPublic())
+						m_freeFunctions.insert(function);
+			}
+}
+
+void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
+{
+	for (auto source: _sources)
+		for (auto node: source->nodes())
+			if (auto var = dynamic_cast<VariableDeclaration const*>(node.get()))
+				createVariable(*var);
+}
+
 smt::SymbolicState& SMTEncoder::state()
 {
 	return m_context.state();

libsolidity/formal/SMTEncoder.h

@@ -112,6 +112,10 @@ public:
 
 	static std::set<FunctionCall const*> collectABICalls(ASTNode const* _node);
 
+	/// @returns all the sources that @param _source depends on,
+	/// including itself.
+	static std::set<SourceUnit const*, ASTNode::CompareByID> sourceDependencies(SourceUnit const& _source);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined
@@ -369,6 +373,13 @@ protected:
 	/// type conversion.
 	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
 
+	/// Traverses all source units available collecting free functions
+	/// and internal library functions in m_freeFunctions.
+	void collectFreeFunctions(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources);
+	std::set<FunctionDefinition const*, ASTNode::CompareByID> const& allFreeFunctions() const { return m_freeFunctions; }
+	/// Create symbolic variables for the free constants in all @param _sources.
+	void createFreeConstants(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources);
+
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
 
@@ -437,6 +448,10 @@ protected:
 
 	ContractDefinition const* m_currentContract = nullptr;
 
+	/// Stores the free functions and internal library functions.
+	/// Those need to be encoded repeatedely for every analyzed contract.
+	std::set<FunctionDefinition const*, ASTNode::CompareByID> m_freeFunctions;
+
 	/// Stores the context of the encoding.
 	smt::EncodingContext& m_context;
 

libsolutil/CommonData.h

@@ -99,19 +99,19 @@ inline std::vector<T> operator+(std::vector<T>&& _a, std::vector<T>&& _b)
 }
 
 /// Concatenate something to a sets of elements.
-template <class T, class U>
+template <class U, class... T>
-inline std::set<T> operator+(std::set<T> const& _a, U&& _b)
+inline std::set<T...> operator+(std::set<T...> const& _a, U&& _b)
 {
-	std::set<T> ret(_a);
+	std::set<T...> ret(_a);
 	ret += std::forward<U>(_b);
 	return ret;
 }
 
 /// Concatenate something to a sets of elements, move variant.
-template <class T, class U>
+template <class U, class... T>
-inline std::set<T> operator+(std::set<T>&& _a, U&& _b)
+inline std::set<T...> operator+(std::set<T...>&& _a, U&& _b)
 {
-	std::set<T> ret(std::move(_a));
+	std::set<T...> ret(std::move(_a));
 	ret += std::forward<U>(_b);
 	return ret;
 }

test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_1.sol

@@ -0,0 +1,26 @@
+interface I {
+    function i() external;
+}
+
+library L {
+    function f(I _i) internal {
+        _i.i();
+    }
+}
+
+contract C {
+    uint x;
+    bool inG;
+    function s() public {
+        require(inG);
+        x = 2;
+    }
+    function g(I _i) public {
+        inG = true;
+        L.f(_i);
+        assert(x == 0);
+        inG = false;
+    }
+}
+// ----
+// Warning 6328: (296-310): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n    L.f(0) -- internal call\n        _i.i() -- untrusted external call, synthesized as:\n            C.s() -- reentrant call

test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_2.sol

@@ -0,0 +1,29 @@
+interface I {
+    function i() external;
+}
+
+library L {
+    function f(I _i) internal {
+        _i.i();
+    }
+	function g(I _i) internal {
+		f(_i);
+	}
+}
+
+contract C {
+    uint x;
+    bool inG;
+    function s() public {
+        require(inG);
+        x = 2;
+    }
+    function g(I _i) public {
+        inG = true;
+        L.g(_i);
+        assert(x == 0);
+        inG = false;
+    }
+}
+// ----
+// Warning 6328: (337-351): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n    L.g(0) -- internal call\n        L.f(0) -- internal call\n            _i.i() -- untrusted external call, synthesized as:\n                C.s() -- reentrant call

test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_3.sol

@@ -0,0 +1,32 @@
+interface I {
+    function i() external;
+}
+
+library M {
+    function f(I _i) internal {
+        _i.i();
+    }
+}
+
+library L {
+	function g(I _i) internal {
+		M.f(_i);
+	}
+}
+
+contract C {
+    uint x;
+    bool inG;
+    function s() public {
+        require(inG);
+        x = 2;
+    }
+    function g(I _i) public {
+        inG = true;
+        L.g(_i);
+        assert(x == 0);
+        inG = false;
+    }
+}
+// ----
+// Warning 6328: (354-368): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n    L.g(0) -- internal call\n        M.f(0) -- internal call\n            _i.i() -- untrusted external call, synthesized as:\n                C.s() -- reentrant call

test/libsolidity/smtCheckerTests/file_level/constant_easy.sol

@@ -0,0 +1,12 @@
+uint constant x = 42;
+
+contract C {
+	function f() public pure {
+		uint z = x;
+		assert(z == 41);
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (80-95): CHC: Assertion violation happens here.\nCounterexample:\n\nz = 42\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/file_level/constant_string_at_file_level.sol

@@ -0,0 +1,41 @@
+bytes constant a = "\x03\x01\x02";
+bytes constant b = hex"030102";
+string constant c = "hello";
+uint256 constant x = 56;
+enum ActionChoices {GoLeft, GoRight, GoStraight, Sit}
+ActionChoices constant choices = ActionChoices.GoRight;
+bytes32 constant st = "abc\x00\xff__";
+
+contract C {
+	function f() internal pure returns (bytes memory) {
+		return a;
+	}
+
+	function g() internal pure returns (bytes memory) {
+		return b;
+	}
+
+	function h() internal pure returns (bytes memory) {
+		return bytes(c);
+	}
+
+	function i() internal pure returns (uint, ActionChoices, bytes32) {
+		return (x, choices, st);
+	}
+
+	function p() public pure {
+		assert(f().length == 3); // should hold
+		assert(g().length == 3); // should hold
+		assert(h().length == 5); // should hold
+		(uint w, ActionChoices z, bytes32 t) = i();
+		assert(x == 56); // should hold
+		assert(w == 56); // should hold
+		assert(z == ActionChoices.GoRight); // should hold
+		assert(t == "abc\x00\xff__"); // should hold
+		assert(w == 59); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (968-983): CHC: Assertion violation happens here.\nCounterexample:\n\nw = 56\nz = 1\nt = 44048180624707321370159228589897778088919435935156254407473833945046349512704\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n    C.g() -- internal call\n    C.h() -- internal call\n    C.i() -- internal call

test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol

@@ -0,0 +1,64 @@
+==== Source: s1.sol ====
+
+
+bytes constant a = b;
+bytes constant b = hex"030102";
+
+function fre() pure returns (bytes memory) {
+	return a;
+}
+
+==== Source: s2.sol ====
+
+import "s1.sol";
+
+uint256 constant c = uint8(a[0]) + 2;
+
+contract C {
+	function f() internal pure returns (bytes memory) {
+		return a;
+	}
+
+	function g() internal pure returns (bytes memory) {
+		return b;
+	}
+
+	function h() internal pure returns (uint) {
+		return c;
+	}
+
+	function i() internal pure returns (bytes memory) {
+		return fre();
+	}
+
+	function p() public pure {
+		bytes memory r1 = f();
+		assert(r1[0] == 0x03); // should hold
+		assert(r1[1] == 0x01); // should hold
+		assert(r1[2] == 0x02); // should hold
+		assert(r1[2] == 0x04); // should fail
+
+		bytes memory r2 = g();
+		assert(r2[0] == 0x03); // should hold
+		assert(r2[1] == 0x01); // should hold
+		assert(r2[2] == 0x02); // should hold
+		assert(r2[2] == 0x04); // should fail
+
+		bytes memory r3 = i();
+		assert(r3[0] == 0x03); // should hold
+		assert(r3[1] == 0x01); // should hold
+		assert(r3[2] == 0x02); // should hold
+		assert(r3[2] == 0x04); // should fail
+
+		uint z = h();
+		assert(z == 5); // should hold
+		assert(z == 7); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call
+// Warning 6328: (s2.sol:704-725): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = [3, 1, 2]\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n    C.g() -- internal call
+// Warning 6328: (s2.sol:890-911): CHC: Assertion violation happens here.
+// Warning 6328: (s2.sol:980-994): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/file_level/easy.sol

@@ -0,0 +1,17 @@
+function add(uint a, uint b) pure returns (uint) {
+	return a + b;
+}
+
+contract C {
+	function f(uint x) internal pure returns (uint) {
+		return add(x, 2);
+	}
+	function g() public pure {
+		assert(f(7) == 9); // should hold
+		assert(f(8) == 9); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (222-239): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f(7) -- internal call\n        add(7, 2) -- internal call\n    C.f(8) -- internal call\n        add(8, 2) -- internal call

test/libsolidity/smtCheckerTests/file_level/enum.sol

@@ -0,0 +1,23 @@
+enum E {
+	READ,
+	WRITE
+}
+
+function allocate(bool b) pure returns (E) {
+	if (b) return E.READ;
+	return E.WRITE;
+}
+
+contract C {
+	function f() public pure {
+		E e1 = allocate(true);
+		assert(e1 == E.READ); // should hold
+		E e2 = allocate(false);
+		assert(e2 == E.READ); // should fail
+		assert(allocate(false) == E.WRITE); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (247-267): CHC: Assertion violation happens here.\nCounterexample:\n\ne1 = 0\ne2 = 1\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(true) -- internal call\n    allocate(false) -- internal call

test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol

@@ -0,0 +1,26 @@
+==== Source: a.sol ====
+function f(uint) pure returns (uint) { return 7; }
+function f(bytes memory x) pure returns (uint) { return x.length; }
+==== Source: b.sol ====
+import "a.sol" as M;
+contract C {
+	function f() internal pure returns (uint, uint) {
+		return (M.f(2), M.f("abc"));
+	}
+	function p() public pure {
+		(uint a, uint b) = f();
+		assert(a == 7); // should hold
+		assert(a == 9); // should fail
+		assert(b == 3); // should hold
+		assert(b == 5); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol"
+// Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"
+// Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol:f(2) -- internal call\n        a.sol:f([97, 98, 99]) -- internal call
+// Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol:f(2) -- internal call\n        a.sol:f([97, 98, 99]) -- internal call
+// Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol"
+// Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"

test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol

@@ -7,5 +7,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported.
+// Warning 4984: (93-98): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639894\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639894)
-// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported.

test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol

@@ -11,9 +11,3 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 2018: (188-278): Function state mutability can be restricted to pure
-// Warning 8195: (0-23): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (79-133): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (135-172): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (0-23): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (79-133): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (135-172): Model checker analysis was not possible because file level constants are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_1.sol

@@ -11,5 +11,5 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 // ====
 // SMTEngine: all
 // ----
-// Warning 6660: (188-302): Model checker analysis was not possible because file level functions are not supported.
+// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    fun(_x, []) -- internal call
-// Warning 6660: (188-302): Model checker analysis was not possible because file level functions are not supported.
+// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call

test/libsolidity/smtCheckerTests/file_level/free_function_2.sol

@@ -6,6 +6,3 @@ contract C {
 function f() {}
 // ====
 // SMTEngine: all
-// ----
-// Warning 6660: (50-65): Model checker analysis was not possible because file level functions are not supported.
-// Warning 6660: (50-65): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_3.sol

@@ -1,6 +1,3 @@
 function f() view {}
 // ====
 // SMTEngine: all
-// ----
-// Warning 6660: (0-20): Model checker analysis was not possible because file level functions are not supported.
-// Warning 6660: (0-20): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_4.sol

@@ -5,5 +5,3 @@ function f()pure {
 // SMTEngine: all
 // ----
 // Warning 2072: (20-28): Unused local variable.
-// Warning 6660: (0-55): Model checker analysis was not possible because file level functions are not supported.
-// Warning 6660: (0-55): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_5.sol

@@ -6,5 +6,3 @@ function f() pure {
 // SMTEngine: all
 // ----
 // Warning 6133: (35-51): Statement has no effect.
-// Warning 6660: (14-54): Model checker analysis was not possible because file level functions are not supported.
-// Warning 6660: (14-54): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol

@@ -11,8 +11,8 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported.
+// Warning 4984: (190-202): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 6660: (214-328): Model checker analysis was not possible because file level functions are not supported.
+// Warning 4984: (190-206): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported.
+// Warning 6368: (315-320): CHC: Out of bounds access happens here.
-// Warning 6660: (214-328): Model checker analysis was not possible because file level functions are not supported.

test/libsolidity/smtCheckerTests/file_level/free_namesake_contract_function.sol

@@ -0,0 +1,14 @@
+function f() pure returns (uint) { return 1337; }
+
+contract C {
+	function g() public pure {
+		assert(f() == 42); // should hold
+		assert(f() == 1337); // should fail
+	}
+	function f() internal pure returns (uint) { return 42; }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 2519: (170-226): This declaration shadows an existing declaration.
+// Warning 6328: (130-149): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call\n    C.f() -- internal call

test/libsolidity/smtCheckerTests/file_level/free_runtimecode.sol

@@ -0,0 +1,20 @@
+contract C {
+	uint public x = 2;
+}
+
+function test() pure returns (bool) {
+	return type(C).runtimeCode.length > 20;
+}
+
+contract D {
+	function f() public pure {
+		assert(test()); // should hold but SMTChecker doesn't know that
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 7507: (82-101): Assertion checker does not yet support this expression.
+// Warning 7507: (82-101): Assertion checker does not yet support this expression.
+// Warning 6328: (161-175): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n    test() -- internal call
+// Warning 7507: (82-101): Assertion checker does not yet support this expression.

test/libsolidity/smtCheckerTests/file_level/import.sol

@@ -0,0 +1,28 @@
+==== Source: A ====
+struct S { uint x; }
+function set(S storage a, uint v) { a.x = v; }
+
+==== Source: B ====
+import "A";
+import "A" as A;
+contract C {
+	A.S data;
+	function f(uint v) internal returns (uint one, uint two) {
+		A.set(data, v);
+		one = data.x;
+		set(data, v + 1);
+		two = data.x;
+	}
+	function g() public {
+		(uint x, uint y) = f(7);
+		assert(x == 7); // should hold but the SMTChecker doesn't know that
+		assert(y == 8); // should hold but the SMTChecker doesn't know that
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8364: (B:115-116): Assertion checker does not yet implement type module "A"
+// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call
+// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call
+// Warning 8364: (B:115-116): Assertion checker does not yet implement type module "A"

test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol

@@ -0,0 +1,28 @@
+library L {
+	function pub() public pure returns (uint) {
+		return 7;
+	}
+	function inter() internal pure returns (uint) {
+		return 8;
+	}
+}
+
+function fu() pure returns (uint, uint) {
+	return (L.pub(), L.inter());
+}
+
+contract C {
+	function f() public pure {
+		(uint x, uint y) = fu();
+		assert(x == 7); // should hold but SMTChecker doesn't implement delegatecall
+		assert(y == 9); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
+// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n    fu() -- internal call\n        L.inter() -- internal call
+// Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n    fu() -- internal call\n        L.inter() -- internal call
+// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/file_level/new_operator.sol

@@ -0,0 +1,20 @@
+contract C {
+	uint public x = 2;
+}
+
+function test() returns (uint) {
+	return (new C()).x();
+}
+
+contract D {
+	function f() public {
+		assert(test() == 2); // should hold but the SMTChecker doesn't support `new`
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
+// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n    test() -- internal call
+// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/file_level/overloads.sol

@@ -0,0 +1,18 @@
+function f(uint) pure returns (uint) {
+	return 2;
+}
+function f(string memory) pure returns (uint) {
+	return 3;
+}
+
+contract C {
+	function g() public pure {
+		(uint x, uint y) = (f(2), f("abc"));
+		assert(x == 2); // should hold
+		assert(y == 4); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n    f(2) -- internal call\n    f([97, 98, 99]) -- internal call

test/libsolidity/smtCheckerTests/file_level/recursion.sol

@@ -0,0 +1,39 @@
+function exp(uint base, uint exponent) pure returns (uint power) {
+	if (exponent == 0)
+		return 1;
+	power = exp(base, exponent / 2);
+	power *= power;
+	if (exponent & 1 == 1)
+		power *= base;
+}
+
+contract C {
+	function g(uint base, uint exponent) internal pure returns (uint) {
+		return exp(base, exponent);
+	}
+	function f() public pure {
+		// All of these should hold but the SMTChecker can't prove them.
+		assert(g(0, 0) == 1);
+		assert(g(0, 1) == 0);
+		assert(g(1, 0) == 1);
+		assert(g(2, 3) == 8);
+		assert(g(3, 10) == 59049);
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4281: (118-130): CHC: Division by zero might happen here.
+// Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 6328: (430-450): CHC: Assertion violation happens here.
+// Warning 6328: (478-498): CHC: Assertion violation might happen here.
+// Warning 6328: (502-527): CHC: Assertion violation might happen here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 8065: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4661: (478-498): BMC: Assertion violation happens here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (502-527): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol

@@ -0,0 +1,37 @@
+==== Source: s1.sol ====
+
+
+uint constant a = 89;
+
+function fre() pure returns (uint) {
+	return a;
+}
+
+==== Source: s2.sol ====
+
+import {a as b, fre} from "s1.sol";
+import "s1.sol" as M;
+
+uint256 constant a = 13;
+
+contract C {
+	function f() internal pure returns (uint, uint, uint, uint) {
+		return (a, fre(), M.a, b);
+	}
+	function p() public pure {
+		(uint x, uint y, uint z, uint t) = f();
+		assert(x == 13); // should hold
+		assert(y == 89); // should hold
+		assert(z == 89); // should hold but the SMTChecker does not implement module access
+		assert(t == 89); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
+// Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
+// Warning 6328: (s2.sol:334-349): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 90\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        s1.sol:fre() -- internal call
+// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
+// Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
+// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.

test/libsolidity/smtCheckerTests/file_level/struct.sol

@@ -0,0 +1,27 @@
+struct S {
+	uint x;
+	uint[] a;
+}
+
+function allocate(uint _x, uint _f) pure returns (S memory) {
+	S memory s;
+	s.x = _x;
+	s.a = new uint[](1);
+	s.a[0] = _f;
+	return s;
+}
+
+contract C {
+	function f() public pure {
+		S memory s = allocate(2, 1);
+		assert(s.x == 2); // should hold
+		assert(s.a[0] == 1); // should hold
+		assert(s.x == 3); // should fail
+		assert(s.a[0] == 4); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (317-333): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(2, 1) -- internal call
+// Warning 6328: (352-371): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(2, 1) -- internal call