Merge pull request #13749 from ethereum/smt_fix_library

Fix SMTChecker bug when a public library function is called internally

Changelog.md

@@ -23,6 +23,7 @@ Bugfixes:
  * Solidity Upgrade Tool ``solidity-upgrade``: Fix the tool returning success code on uncaught exceptions.
  * SMTChecker: Fix display error for negative integers that are one more than powers of two.
  * SMTChecker: Improved readability for large integers that are powers of two or almost powers of two in error messages.
+ * SMTChecker: Fix internal error when a public library function is called internally.
 
 
 ### 0.8.17 (2022-09-08)

libsolidity/formal/CHC.cpp

@@ -1172,7 +1172,14 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 				m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
 
-				if (!function->isConstructor() && function->isPublic() && resolved.count(function))
+				if (
+					!function->isConstructor() &&
+					function->isPublic() &&
+					// Public library functions should have interfaces only for the libraries
+					// they're declared in.
+					(!function->libraryFunction() || (function->scope() == contract)) &&
+					resolved.count(function)
+				)
 				{
 					m_externalSummaries[contract].emplace(function, createSummaryBlock(*function, *contract));
 

libsolidity/formal/SMTEncoder.cpp

@@ -3162,11 +3162,10 @@ void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByI
 				auto contract = dynamic_cast<ContractDefinition const*>(node.get());
 				contract && contract->isLibrary()
 			)
-			{
 				for (auto function: contract->definedFunctions())
-					if (!function->isPublic())
+					// We need to add public library functions too because they can be called
-						m_freeFunctions.insert(function);
+					// internally by internal library functions that are considered free functions.
-			}
+					m_freeFunctions.insert(function);
 }
 
 void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)

test/libsolidity/SMTCheckerTest.cpp

@@ -29,6 +29,10 @@ using namespace solidity::frontend::test;
 
 SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, EVMVersion{})
 {
+	auto contract = m_reader.stringSetting("SMTContract", "");
+	if (!contract.empty())
+		m_modelCheckerSettings.contracts.contracts[""] = {contract};
+
 	auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes");
 	if (showUnproved == "no")
 		m_modelCheckerSettings.showUnproved = false;

test/libsolidity/smtCheckerTests/functions/library_public_called_as_internal_1.sol

@@ -0,0 +1,26 @@
+library L {
+    function f1(uint x) public pure {
+        assert(x > 0); // should fail
+    }
+    function f(uint x) internal pure { f1(x); }
+}
+
+contract C {
+    function g(uint x) external pure {
+        // This should trigger the assertion failure
+        // since it calls `f` internally, which calls
+        // `f1` internally.
+        return L.f(x);
+    }
+
+    function h(uint x) external pure {
+        // This should not trigger the assertion failure
+        // since it delegatecalls and that's not supported.
+        return L.f1(x);
+    }
+}
+// ====
+// SMTContract: C
+// ----
+// Warning 4588: (533-540): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (58-71): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    L.f(0) -- internal call\n        L.f1(0) -- internal call

test/libsolidity/smtCheckerTests/functions/library_public_called_as_internal_2.sol

@@ -0,0 +1,24 @@
+library L {
+    function f1(uint x) public pure {
+        assert(x > 0); // should fail
+    }
+    function f() internal pure {
+        f1(0); // should cause the assertion in `f1` to fail
+    }
+    function g() internal pure {
+        f1(1); // should not cause the assertion in `f1` to fail
+    }
+}
+
+contract C {
+    function f() external pure {
+        return L.f(); // should cause the assertion to fail
+    }
+    function g() external pure {
+        return L.g(); // should not cause the assertion to fail
+    }
+}
+// ====
+// SMTContract: C
+// ----
+// Warning 6328: (58-71): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n    L.f() -- internal call\n        L.f1(0) -- internal call