Merge pull request #11861 from ethereum/smt_value

[SMTChecker] Support `value` in CHC for external function calls

Author: ekpyron

Changelog.md

@@ -10,6 +10,7 @@ Compiler Features:
  * Immutable variables can be read at construction time once they are initialized.
  * SMTChecker: Support low level ``call`` as external calls to unknown code.
  * SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``.
+ * SMTChecker: Support the ``value`` option for external function calls.
  * Commandline Interface: Disallowed the ``--experimental-via-ir`` option to be used with Standard Json, Assembler and Linker modes.
 
 

libsolidity/formal/CHC.cpp

@@ -34,6 +34,7 @@
 
 #include <range/v3/algorithm/for_each.hpp>
 
+#include <range/v3/view/enumerate.hpp>
 #include <range/v3/view/reverse.hpp>
 
 #ifdef HAVE_Z3_DLOPEN
@@ -743,13 +744,15 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	/// so we just add the nondet_interface predicate.
 
 	solAssert(m_currentContract, "");
-	if (isTrustedExternalCall(&_funCall.expression()))
+	auto [callExpr, callOptions] = functionCallExpression(_funCall);
+
+	if (isTrustedExternalCall(callExpr))
 	{
 		externalFunctionCallToTrustedCode(_funCall);
 		return;
 	}
 
-	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
 	auto kind = funType.kind();
 	solAssert(
 		kind == FunctionType::Kind::External ||
@@ -773,6 +776,19 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	if (!m_currentFunction || m_currentFunction->isConstructor())
 		return;
 
+	if (callOptions)
+	{
+		optional<unsigned> valueIndex;
+		for (auto&& [i, name]: callOptions->names() | ranges::views::enumerate)
+			if (name && *name == "value")
+			{
+				valueIndex = i;
+				break;
+			}
+		solAssert(valueIndex, "");
+		state().addBalance(state().thisAddress(), 0 - expr(*callOptions->options().at(*valueIndex)));
+	}
+
 	auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
 
 	if (!usesStaticCall)
@@ -829,6 +845,8 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	state().newTx();
 	// set the transaction sender as this contract
 	m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
+	// set the transaction value as 0
+	m_context.addAssertion(state().txMember("msg.value") == 0);
 	// set the origin to be the current transaction origin
 	m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
 
@@ -1451,10 +1469,12 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		return smtutil::Expression(true);
 
 	auto contractAddressValue = [this](FunctionCall const& _f) {
-		FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
+		auto [callExpr, callOptions] = functionCallExpression(_f);
+
+		FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
 		if (funType.kind() == FunctionType::Kind::Internal)
 			return state().thisAddress();
-		if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(&_f.expression()))
+		if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
 			return expr(callBase->expression());
 		solAssert(false, "Unreachable!");
 	};

libsolidity/formal/SMTEncoder.cpp

@@ -2590,6 +2590,16 @@ Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
 	return expr;
 }
 
+pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall)
+{
+	Expression const* callExpr = &_funCall.expression();
+	auto const* callOptions = dynamic_cast<FunctionCallOptions const*>(callExpr);
+	if (callOptions)
+		callExpr = &callOptions->expression();
+
+	return {callExpr, callOptions};
+}
+
 Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
 {
 	auto const* expr = &_expr;
@@ -2713,7 +2723,8 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(
 	if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall)
 		return {};
 
-	Expression const* calledExpr = &_funCall.expression();
+	auto [calledExpr, callOptions] = functionCallExpression(_funCall);
+
 	if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(calledExpr))
 	{
 		solAssert(fun->components().size() == 1, "");

libsolidity/formal/SMTEncoder.h

@@ -71,6 +71,10 @@ class SMTEncoder: public ASTConstVisitor
 	/// otherwise _expr.
 	static Expression const* innermostTuple(Expression const& _expr);
 
+	/// @returns {_funCall.expression(), nullptr} if function call option values are not given, and
+	/// {_funCall.expression().expression(), _funCall.expression()} if they are.
+	static std::pair<Expression const*, FunctionCallOptions const*> functionCallExpression(FunctionCall const& _funCall);
+
 	/// @returns the expression after stripping redundant syntactic sugar.
 	/// Currently supports stripping:
 	/// 1. 1-tuple; i.e. ((x)) -> x

test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol

@@ -0,0 +1,14 @@
+contract C {
+	function g(address payable i) public {
+		require(address(this).balance == 100);
+		i.call{value: 10}("");
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 90); // should hold
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 100); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (96-117): Return value of low-level calls not used.

test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol

@@ -0,0 +1,15 @@
+contract C {
+	function g(address payable i) public {
+		require(address(this).balance == 100);
+		i.call{value: 0}("");
+		assert(address(this).balance == 100); // should hold
+		assert(address(this).balance == 20); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (96-116): Return value of low-level calls not used.
+// Warning 6328: (120-156): CHC: Assertion violation might happen here.
+// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.call{value: 0}("") -- untrusted external call
+// Warning 4661: (120-156): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/call_with_value_3.sol

@@ -0,0 +1,15 @@
+contract C {
+	function g(address payable i) public {
+		require(address(this).balance > 100);
+		i.call{value: 20}("");
+		assert(address(this).balance > 0); // should hold
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 9302: (95-116): Return value of low-level calls not used.
+// Warning 6328: (120-153): CHC: Assertion violation might happen here.
+// Warning 4661: (120-153): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol

@@ -0,0 +1,14 @@
+contract C {
+	function g() public {
+		require(address(this).balance == 100);
+		this.h{value: 10}();
+		assert(address(this).balance == 100); // should hold
+		assert(address(this).balance == 90); // should fail
+	}
+
+	function h() external payable {}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (157-192): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol

@@ -0,0 +1,15 @@
+contract C {
+	function g(uint i) public {
+		require(address(this).balance == 100);
+		this.h{value: i}();
+		assert(address(this).balance == 100); // should hold
+		assert(address(this).balance == 90); // should fail
+	}
+
+	function h() external payable {}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (162-197): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_1.sol

@@ -0,0 +1,18 @@
+interface I {
+	function f() external payable;
+}
+
+contract C {
+	function g(I i) public {
+		require(address(this).balance == 100);
+		i.f{value: 10}();
+		assert(address(this).balance == 90); // should hold
+		// Disabled due to Spacer nondeterminism
+		//assert(address(this).balance == 100); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (151-186): CHC: Assertion violation might happen here.
+// Warning 4661: (151-186): BMC: Assertion violation happens here.