[SMTChecker] Fix ICE in string literal to fixed bytes implicit conversion

Changelog.md

@@ -17,6 +17,7 @@ Bugfixes:
  * Code Generator: Fixed a faulty assert that would wrongly trigger for array sizes exceeding unsigned integer.
  * SMTChecker: Fix internal error when accessing indices of fixed bytes.
  * SMTChecker: Fix internal error when using function pointers as arguments.
+ * SMTChecker: Fix internal error when implicitly converting string literals to fixed bytes.
  * Type Checker: Disallow constructor of the same class to be used as modifier.
  * Type Checker: Treat magic variables as unknown identifiers in inline assembly.
 

libsolidity/formal/BMC.cpp

@@ -428,15 +428,20 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
 		solAssert(funType, "");
 
+		auto const& functionParams = funDef->parameters();
+		auto const& arguments = _funCall.arguments();
+		unsigned firstParam = 0;
 		if (funType->bound())
 		{
 			auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
 			solAssert(boundFunction, "");
-			funArgs.push_back(expr(boundFunction->expression()));
+			funArgs.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
+			firstParam = 1;
 		}
 
-		for (auto arg: _funCall.arguments())
-			funArgs.push_back(expr(*arg));
+		solAssert((arguments.size() + firstParam) == functionParams.size(), "");
+		for (unsigned i = 0; i < arguments.size(); ++i)
+			funArgs.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
 		initializeFunctionCallParameters(*funDef, funArgs);
 
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)

libsolidity/formal/SMTEncoder.cpp

@@ -135,9 +135,13 @@ void SMTEncoder::visitFunctionOrModifier()
 			*modifierInvocation->name()->annotation().referencedDeclaration
 		);
 		vector<smt::Expression> modifierArgsExpr;
-		if (modifierInvocation->arguments())
-			for (auto arg: *modifierInvocation->arguments())
-				modifierArgsExpr.push_back(expr(*arg));
+		if (auto const* arguments = modifierInvocation->arguments())
+		{
+			auto const& modifierParams = modifierDef.parameters();
+			solAssert(modifierParams.size() == arguments->size(), "");
+			for (unsigned i = 0; i < arguments->size(); ++i)
+				modifierArgsExpr.push_back(expr(*arguments->at(i), modifierParams.at(i)->type()));
+		}
 		initializeFunctionCallParameters(modifierDef, modifierArgsExpr);
 		pushCallStack({&modifierDef, modifierInvocation.get()});
 		modifierDef.body().accept(*this);
@@ -698,7 +702,7 @@ void SMTEncoder::endVisit(Return const& _return)
 			}
 		}
 		else if (returnParams.size() == 1)
-			m_context.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
+			m_context.addAssertion(expr(*_return.expression(), returnParams.front()->type()) == m_context.newValue(*returnParams.front()));
 	}
 }
 

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_function_call.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract B {
+    function f() pure public {
+		g("0123456");
+	}
+    function g(bytes7 a) pure public {
+		assert(a == "0123456");
+		assert(a == "1234567");
+	}
+}
+// ----
+// Warning: (162-184): Assertion violation happens here
+// Warning: (136-158): Assertion violation happens here
+// Warning: (162-184): Assertion violation happens here

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_modifier.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract B {
+    function f() mod2("0123456") pure public { }
+    modifier mod2(bytes7 a) {
+		assert(a == "0123456");
+		assert(a == "1234567");
+		_;
+	}
+}
+// ----
+// Warning: (152-174): Assertion violation happens here

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+    function g() public pure returns (bytes32 val) { return "abc"; }
+    function f1() public pure returns (bytes32 val) { return g(); }
+
+	function a() public pure {
+		assert(f1() == "abc");
+		assert(f1() == "cde");
+	}
+}
+// ----
+// Warning: (238-259): Assertion violation happens here

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+    function h() public pure returns (bytes32 val, bytes3 val2) { return ("abc", "def"); }
+    function g() public pure returns (bytes32 val) { return "abc"; }
+    function f1() public pure returns (bytes32 val) { return g(); }
+    function f2() public pure returns (bytes32 val, bytes3 val2) { return h(); }
+
+	function a() public pure {
+		(bytes32 v1, bytes3 v2) = f2();
+		assert(v1 == "abc");
+		assert(v2 == "cde");
+	}
+}
+// ----
+// Warning: (442-461): Assertion violation happens here