[SMTChecker] Added support for precise modeling of external calls to this.

Modeling external calls to this, since we can trust these calls.

fixed problem with transaction data not being restored after trusted external call

update to the tests

additional tests

changelog entry

added tests for external getters of this

Changelog.md

@@ -9,6 +9,7 @@ Compiler Features:
  * Command Line interface: Report proper error for each output file which could not be written. Previously an exception was thrown, and execution aborted, on the first error.
  * SMTChecker: Add division by zero checks in the CHC engine.
  * SMTChecker: Support ``selector`` for expressions with value known at compile-time.
+ * SMTChecker: More precise analysis of external calls using ``this``.
  * Command Line Interface: New option ``--model-checker-timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker.
  * Standard JSON: New option ``modelCheckerSettings.timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker.
  * Assembler: Perform linking in assembly mode when library addresses are provided.

libsolidity/formal/BMC.cpp

@@ -96,20 +96,7 @@ bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall)
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (funType.kind() == FunctionType::Kind::External)
-	{
-		auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
-		if (!memberAccess)
-			return false;
-
-		auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
-		if (!(
-			identifier &&
-			identifier->name() == "this" &&
-			identifier->annotation().referencedDeclaration &&
-			dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
-		))
-			return false;
-	}
+		return isTrustedExternalCall(&_funCall.expression());
 	else if (funType.kind() != FunctionType::Kind::Internal)
 		return false;
 

libsolidity/formal/CHC.cpp

@@ -562,8 +562,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 			m_context.addAssertion(interface(*contract));
 	}
 
-	auto previousError = errorFlag().currentValue();
-
 	m_context.addAssertion(predicate(_funCall));
 
 	connectBlocks(
@@ -572,8 +570,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 		(errorFlag().currentValue() > 0)
 	);
 	m_context.addAssertion(errorFlag().currentValue() == 0);
-	errorFlag().increaseIndex();
-	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
 
 void CHC::externalFunctionCall(FunctionCall const& _funCall)
@@ -583,6 +579,11 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	/// so we just add the nondet_interface predicate.
 
 	solAssert(m_currentContract, "");
+	if (isTrustedExternalCall(&_funCall.expression()))
+	{
+		externalFunctionCallToTrustedCode(_funCall);
+		return;
+	}
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	auto kind = funType.kind();
@@ -615,6 +616,42 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	m_context.addAssertion(errorFlag().currentValue() == 0);
 }
 
+void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
+{
+	solAssert(m_currentContract, "");
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
+
+	auto const* function = functionCallToDefinition(_funCall);
+	if (!function)
+		return;
+
+	// External call creates a new transaction.
+	auto originalTx = state().tx();
+	auto txOrigin = state().txMember("tx.origin");
+	state().newTx();
+	// set the transaction sender as this contract
+	m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
+	// set the origin to be the current transaction origin
+	m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
+
+	smtutil::Expression pred = predicate(_funCall);
+
+	auto txConstraints = m_context.state().txConstraints(*function);
+	m_context.addAssertion(pred && txConstraints);
+	// restore the original transaction data
+	state().newTx();
+	m_context.addAssertion(originalTx == state().tx());
+
+	connectBlocks(
+		m_currentBlock,
+		(m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract),
+		(errorFlag().currentValue() > 0)
+	);
+	m_context.addAssertion(errorFlag().currentValue() == 0);
+}
+
 void CHC::unknownFunctionCall(FunctionCall const&)
 {
 	/// Function calls are not handled at the moment,
@@ -1011,27 +1048,34 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 
 smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 {
-	/// Used only for internal calls.
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	auto const* function = functionCallToDefinition(_funCall);
 	if (!function)
 		return smtutil::Expression(true);
 
+	auto contractAddressValue = [this](FunctionCall const& _f) {
+		FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
+		if (funType.kind() == FunctionType::Kind::Internal)
+			return state().thisAddress();
+		if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(&_f.expression()))
+			return expr(callBase->expression());
+		solAssert(false, "Unreachable!");
+	};
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().crypto(), state().tx(), state().state()};
 
-	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	solAssert(funType.kind() == FunctionType::Kind::Internal, "");
-
-	/// Internal calls can be made to the contract itself or a library.
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
-	solAssert(contract->isLibrary() || find(hierarchy.begin(), hierarchy.end(), contract) != hierarchy.end(), "");
+	solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), "");
 
 	/// If the call is to a library, we use that library as the called contract.
-	/// If it is not, we use the current contract even if it is a call to a contract
-	/// up in the inheritance hierarchy, since the interfaces/predicates are different.
-	auto const* calledContract = contract->isLibrary() ? contract : m_currentContract;
+	/// 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;

libsolidity/formal/CHC.h

@@ -88,6 +88,7 @@ private:
 	void visitAddMulMod(FunctionCall const& _funCall) override;
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCall(FunctionCall const& _funCall);
+	void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
 	void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
 	/// Creates underflow/overflow verification targets.

libsolidity/formal/SMTEncoder.cpp

@@ -2391,6 +2391,19 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
 	return nullptr;
 }
 
+bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
+	auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
+	if (!memberAccess)
+		return false;
+
+	auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
+	return identifier &&
+		identifier->name() == "this" &&
+		identifier->annotation().referencedDeclaration &&
+		dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
+	;
+}
+
 string SMTEncoder::extraComment()
 {
 	string extra;

libsolidity/formal/SMTEncoder.h

@@ -295,6 +295,10 @@ protected:
 	/// otherwise nullptr.
 	MemberAccess const* isEmptyPush(Expression const& _expr) const;
 
+	/// @returns true if the given identifier is a contract which is known and trusted.
+	/// This means we don't have to abstract away effects of external function calls to this contract.
+	static bool isTrustedExternalCall(Expression const* _expr);
+
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.
 	void createReturnedExpressions(FunctionCall const& _funCall);

test/libsolidity/smtCheckerTests/functions/this_external_call.sol

@@ -9,9 +9,7 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		this.f(y);
-		// Fails as false positive because CHC does not support `this`.
 		assert(x < 1000);
 	}
 }
 // ----
-// Warning 6328: (227-243): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+    uint a;
+    function f(uint x) public {
+        this.g(x);
+        assert(a == x);
+        assert(a != 42);
+    }
+
+    function g(uint x) public {
+        a = x;
+    }
+}
+// ----
+// Warning 6328: (141-156): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol

@@ -10,9 +10,7 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		uint z = this.f(y);
-		// Fails as false positive because CHC does not support `this`.
 		assert(z < 1000);
 	}
 }
 // ----
-// Warning 6328: (263-279): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+    address lastCaller;
+
+    constructor() {
+        lastCaller = msg.sender;
+    }
+
+    modifier log {
+        lastCaller = msg.sender;
+        _;
+    }
+
+    function test() log public {
+        assert(lastCaller == msg.sender);
+        this.g();
+        assert(lastCaller == address(this));
+        assert(lastCaller == msg.sender);
+        assert(lastCaller == address(0));
+    }
+
+    function g() log public {
+    }
+}
+// ----
+// Warning 6328: (347-379): CHC: Assertion violation happens here.
+// Warning 6328: (389-421): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test() view public {
+		require(address(this) != tx.origin);
+		assert(!this.g());
+	}
+
+	function g() view public returns (bool) {
+		return msg.sender == tx.origin;
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint public x;
+
+	function f() public view {
+		uint y = this.x();
+		assert(y == x); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (114-128): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint) public map;
+
+	function f() public view {
+		uint y = this.map(2);
+		assert(y == map[2]); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (137-156): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => mapping (uint => uint)) public map;
+
+	function f() public view {
+		uint y = this.map(2, 3);
+		assert(y == map[2][3]); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (158-180): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/this_state.sol

@@ -6,7 +6,6 @@ contract C
     function g() public {
 		x = 0;
         this.h();
-		// Fails as false positive because CHC does not support `this`.
 		assert(x == 2);
     }
     function h() public {
@@ -14,4 +13,3 @@ contract C
     }
 }
 // ----
-// Warning 6328: (186-200): CHC: Assertion violation happens here.