Basic support to free functions

libsolidity/formal/BMC.cpp

@@ -149,11 +149,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 +167,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 +180,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

@@ -82,10 +82,11 @@ void CHC::analyze(SourceUnit const& _source)
 	{
 		resetSourceAnalysis();
 
-		set<SourceUnit const*, EncodingContext::IdCompare> sources;
+		set<SourceUnit const*, ASTNode::CompareByID> sources;
 		sources.insert(&_source);
 		for (auto const& source: _source.referencedSourceUnits(true))
 			sources.insert(source);
+		collectFreeFunctions(sources);
 		for (auto const* source: sources)
 			defineInterfacesAndSummaries(*source);
 		for (auto const* source: sources)
@@ -219,6 +220,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 +263,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 +686,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 +1048,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 +1313,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 +1330,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 +1354,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);

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

@@ -59,16 +59,7 @@ bool SMTEncoder::analyze(SourceUnit const& _source)
 	bool analysis = true;
 	for (auto source: sources)
 		for (auto node: source->nodes())
-			if (auto function = dynamic_pointer_cast<FunctionDefinition>(node))
+			if (auto var = dynamic_pointer_cast<VariableDeclaration>(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,
@@ -116,7 +107,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 +143,8 @@ bool SMTEncoder::visit(ModifierDefinition const&)
 
 bool SMTEncoder::visit(FunctionDefinition const& _function)
 {
+	solAssert(m_currentContract, "");
+
 	m_modifierDepthStack.push_back(-1);
 
 	initializeLocalVariables(_function);
@@ -288,6 +281,8 @@ bool SMTEncoder::visit(PlaceholderStatement const&)
 
 void SMTEncoder::endVisit(FunctionDefinition const&)
 {
+	solAssert(m_currentContract, "");
+
 	popCallStack();
 	solAssert(m_modifierDepthStack.back() == -1, "");
 	m_modifierDepthStack.pop_back();
@@ -2963,6 +2958,26 @@ 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);
+			}
+}
+
 smt::SymbolicState& SMTEncoder::state()
 {
 	return m_context.state();

libsolidity/formal/SMTEncoder.h

@@ -369,6 +369,11 @@ 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; }
+
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
 
@@ -437,6 +442,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/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

@@ -4,6 +4,4 @@ function f()pure {
 // ====
 // SMTEngine: all
 // ----
-// Warning 2072: (20-28): Unused local variable.
+// Warning 2072: (52-60): 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

@@ -5,6 +5,4 @@ function f() pure {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6133: (35-51): Statement has no effect.
+// Warning 6133: (67-83): 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

@@ -12,7 +12,5 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 // ====
 // SMTEngine: all
 // ----
-// Warning 8195: (0-20): 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.
-// Warning 6660: (214-328): 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 8195: (0-20): Model checker analysis was not possible because file level constants are not supported.
-// Warning 6660: (214-328): Model checker analysis was not possible because file level functions are not supported.