Merge pull request #6665 from ethereum/smt_inline_external_this

[SMTChecker] Inline external function calls to `this`

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
  * SMTChecker: Support inherited state variables.
  * SMTChecker: Support tuples and function calls with multiple return values.
  * SMTChecker: Support ``delete``.
+ * SMTChecker: Inline external function calls to ``this``.
  * Assembler: Encode the compiler version in the deployed bytecode.
 
 

libsolidity/formal/SMTChecker.cpp

@@ -665,8 +665,6 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		visitGasLeft(_funCall);
 		break;
 	case FunctionType::Kind::Internal:
-		inlineFunctionCall(_funCall);
-		break;
 	case FunctionType::Kind::External:
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCall:
@@ -674,9 +672,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::BareDelegateCall:
 	case FunctionType::Kind::BareStaticCall:
 	case FunctionType::Kind::Creation:
-		m_externalFunctionCallHappened = true;
+		internalOrExternalFunctionCall(_funCall);
-		resetStateVariables();
-		resetStorageReferences();
 		break;
 	case FunctionType::Kind::KECCAK256:
 	case FunctionType::Kind::ECRecover:
@@ -804,6 +800,25 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 	}
 }
 
+void SMTChecker::internalOrExternalFunctionCall(FunctionCall const& _funCall)
+{
+	auto funDef = inlinedFunctionCallToDefinition(_funCall);
+	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	if (funDef)
+		inlineFunctionCall(_funCall);
+	else if (funType.kind() == FunctionType::Kind::Internal)
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not yet implement this type of function call."
+		);
+	else
+	{
+		m_externalFunctionCallHappened = true;
+		resetStateVariables();
+		resetStorageReferences();
+	}
+}
+
 void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
 {
 	vector<smt::Expression> smtArguments;
@@ -1930,7 +1945,21 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa
 		return nullptr;
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	if (funType.kind() != FunctionType::Kind::Internal)
+	if (funType.kind() == FunctionType::Kind::External)
+	{
+		auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
+		auto identifier = memberAccess ?
+			dynamic_cast<Identifier const*>(&memberAccess->expression()) :
+			nullptr;
+		if (!(
+			identifier &&
+			identifier->name() == "this" &&
+			identifier->annotation().referencedDeclaration &&
+			dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
+		))
+			return nullptr;
+	}
+	else if (funType.kind() != FunctionType::Kind::Internal)
 		return nullptr;
 
 	FunctionDefinition const* funDef = nullptr;

libsolidity/formal/SMTChecker.h

@@ -115,6 +115,9 @@ private:
 	void inlineFunctionCall(FunctionCall const& _funCall);
 	/// Creates an uninterpreted function call.
 	void abstractFunctionCall(FunctionCall const& _funCall);
+	/// Inlines if the function call is internal or external to `this`.
+	/// Erases knowledge about state variables if external.
+	void internalOrExternalFunctionCall(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);
 
 	/// Encodes a modifier or function body according to the modifier

test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol

@@ -9,4 +9,5 @@ contract C {
     }
 }
 // ----
+// Warning: (99-107): Assertion checker does not support recursive function calls.
 // Warning: (141-144): Assertion checker does not support recursive function calls.

test/libsolidity/smtCheckerTests/functions/this_external_call.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint x;
+	function f(uint y) public {
+		x = y;
+	}
+	function g(uint y) public {
+		require(y < 1000);
+		this.f(y);
+		assert(x < 1000);
+	}
+}

test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint x;
+	function f(uint y) public returns (uint) {
+		x = y;
+		return x;
+	}
+	function g(uint y) public {
+		require(y < 1000);
+		uint z = this.f(y);
+		assert(z < 1000);
+	}
+}

test/libsolidity/smtCheckerTests/functions/this_fake.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+    uint public x;
+    C c;
+    function f(C _c) public {
+        c = _c;
+    }
+    function g() public {
+        C this = c;
+		x = 0;
+        this.h();
+		// State knowledge is erased.
+		// Function call is not inlined.
+		assert(x == 0);
+    }
+    function h() public {
+        x = 2;
+    }
+}
+// ----
+// Warning: (160-166): This declaration shadows a builtin symbol.
+// Warning: (268-282): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/this_state.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+    uint public x;
+    function g() public {
+		x = 0;
+        this.h();
+		// Function call is inlined.
+		assert(x == 2);
+    }
+    function h() public {
+        x = 2;
+    }
+}