smt encode call

Changelog.md

@@ -7,6 +7,7 @@ Compiler Features:
  * Peephole Optimizer: Remove operations without side effects before simple terminations.
  * Assembly-Json: Export: Include source list in `sourceList` field.
  * Commandline Interface: option ``--pretty-json`` works also with the following options: ``--abi``, ``--asm-json``, ``--ast-compact-json``, ``--devdoc``, ``--storage-layout``, ``--userdoc``.
+ * SMTChecker: Support ``abi.encodeCall`` taking into account the called selector.
 
 
 Bugfixes:

libsolidity/formal/SMTEncoder.cpp

@@ -586,6 +586,16 @@ bool SMTEncoder::visit(FunctionCall const& _funCall)
 			arg->accept(*this);
 		return false;
 	}
+	else if (funType.kind() == FunctionType::Kind::ABIEncodeCall)
+	{
+		auto fun = _funCall.arguments().front();
+		createExpr(*fun);
+		auto const* functionType = dynamic_cast<FunctionType const*>(fun->annotation().type);
+		if (functionType->hasDeclaration())
+			defineExpr(*fun, functionType->externalIdentifier());
+		return true;
+	}
+
 	// We do not really need to visit the expression in a wrap/unwrap no-op call,
 	// so we just ignore the function call expression to avoid "unsupported" warnings.
 	else if (
@@ -1323,6 +1333,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 
 	auto const& exprType = memberExpr->annotation().type;
 	solAssert(exprType, "");
+
 	if (exprType->category() == Type::Category::Magic)
 	{
 		if (auto const* identifier = dynamic_cast<Identifier const*>(memberExpr))

test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple.sol

@@ -1,26 +0,0 @@
-contract C {
-	function callMeMaybe(uint a, uint b, uint[] memory c) external {}
-
-	function abiEncodeSimple(uint x, uint y, uint z, uint[] memory a, uint[] memory b) public view {
-		require(x == y);
-		bytes memory b1 = abi.encodeCall(this.callMeMaybe, (x, z, a));
-		bytes memory b2 = abi.encodeCall(this.callMeMaybe, (y, z, a));
-		assert(b1.length == b2.length);
-
-		bytes memory b3 = abi.encodeCall(this.callMeMaybe, (y, z, b));
-		assert(b1.length == b3.length); // should fail
-	}
-}
-// ====
-// SMTEngine: all
-// SMTIgnoreCex: yes
-// ----
-// Warning 6031: (233-249): Internal error: Expression undefined for SMT solver.
-// Warning 6031: (298-314): Internal error: Expression undefined for SMT solver.
-// Warning 6031: (398-414): Internal error: Expression undefined for SMT solver.
-// Warning 1218: (330-360): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (430-460): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (330-360): CHC: Assertion violation might happen here.
-// Warning 6328: (430-460): CHC: Assertion violation might happen here.
-// Warning 4661: (330-360): BMC: Assertion violation happens here.
-// Warning 4661: (430-460): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_1.sol

@@ -0,0 +1,22 @@
+contract C {
+	function callMeMaybe(uint a, uint b) external {}
+
+	function abiEncodeSimple(uint x, uint y, uint z) public view {
+		require(x == y);
+		function (uint, uint) external f = this.callMeMaybe;
+		bytes memory b1 = abi.encodeCall(f, (x, z));
+		bytes memory b2 = abi.encodeCall(f, (y, z));
+		assert(b1.length == b2.length); // should hold
+		assert(b1[0] == b2[0]); // should hold
+
+		bytes memory b3 = abi.encodeCall(this.callMeMaybe, (3, z));
+		assert(b1.length == b3.length); // should hold, but we don't encode the length computation precisely
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6368: (354-359): CHC: Out of bounds access happens here.
+// Warning 6368: (363-368): CHC: Out of bounds access happens here.
+// Warning 6328: (451-481): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_2.sol

@@ -0,0 +1,21 @@
+contract C {
+	function callMeMaybe(uint a, uint b) external {}
+
+	function abiEncodeSimple(uint x, uint y, uint z) public view {
+		require(x == y);
+		bytes memory b1 = abi.encodeCall(this.callMeMaybe, (x, z));
+		bytes memory b2 = abi.encodeCall(this.callMeMaybe, (y, z));
+		assert(b1.length == b2.length); // should hold
+		assert(b1[0] == b2[0]); // should hold
+
+		bytes memory b3 = abi.encodeCall(this.callMeMaybe, (3, z));
+		assert(b1.length == b3.length); // should hold but we don't compute the length precisely
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6368: (329-334): CHC: Out of bounds access happens here.
+// Warning 6368: (338-343): CHC: Out of bounds access happens here.
+// Warning 6328: (426-456): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_3.sol

@@ -0,0 +1,21 @@
+contract C {
+	function callMeMaybe(uint a, uint b) external {}
+
+	function abiEncodeSimple(uint x, uint y, uint z) public pure {
+		require(x == y);
+		bytes memory b1 = abi.encodeCall(C.callMeMaybe, (x, z));
+		bytes memory b2 = abi.encodeCall(C.callMeMaybe, (y, z));
+		assert(b1.length == b2.length); // should hold
+		assert(b1[0] == b2[0]); // should hold
+
+		bytes memory b3 = abi.encodeCall(C.callMeMaybe, (3, z));
+		assert(b1.length == b3.length); // should hold but we don't compute the length precisely
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6368: (323-328): CHC: Out of bounds access happens here.
+// Warning 6368: (332-337): CHC: Out of bounds access happens here.
+// Warning 6328: (417-447): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_4.sol

@@ -0,0 +1,25 @@
+abstract contract D {
+	function no(uint a, uint b) external virtual;
+}
+
+contract C {
+	function callMeMaybe(uint a, uint b) external {}
+
+	function abiEncodeSimple(uint x, uint y, uint z) public pure {
+		require(x == y);
+		bytes memory b1 = abi.encodeCall(D.no, (x, z));
+		bytes memory b2 = abi.encodeCall(D.no, (y, z));
+		assert(b1.length == b2.length); // should hold
+		assert(b1[0] == b2[0]); // should hold
+
+		bytes memory b3 = abi.encodeCall(D.no, (3, z));
+		assert(b1.length == b3.length); // should hold but we don't compute the length precisely
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6368: (377-382): CHC: Out of bounds access happens here.
+// Warning 6368: (386-391): CHC: Out of bounds access happens here.
+// Warning 6328: (462-492): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/abi/abi_encode_call_simple_5.sol

@@ -0,0 +1,25 @@
+abstract contract D {
+	function no(uint a, uint b) external virtual;
+}
+
+contract C {
+	function callMeMaybe(uint a, uint b) external {}
+
+	function abiEncodeSimple(D d, uint x, uint y, uint z) public pure {
+		require(x == y);
+		bytes memory b1 = abi.encodeCall(d.no, (x, z));
+		bytes memory b2 = abi.encodeCall(d.no, (y, z));
+		assert(b1.length == b2.length); // should hold
+		assert(b1[0] == b2[0]); // should hold
+
+		bytes memory b3 = abi.encodeCall(d.no, (3, z));
+		assert(b1.length == b3.length); // should hold but we don't compute the length precisely
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6368: (382-387): CHC: Out of bounds access happens here.
+// Warning 6368: (391-396): CHC: Out of bounds access happens here.
+// Warning 6328: (467-497): CHC: Assertion violation happens here.