Merge pull request #11032 from blishko/smt_string_to_bytes

[SMTChecker] Fix analysis of push to a string casted to bytes

Author: Leonardo

Changelog.md

@@ -7,7 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
-
+ * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
 
 AST Changes:
 

libsolidity/formal/SMTEncoder.cpp

@@ -1635,7 +1635,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 
 void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array)
 {
-	Expression const* expr = innermostTuple(_expr);
+	Expression const* expr = cleanExpression(_expr);
 
 	if (auto const* id = dynamic_cast<Identifier const*>(expr))
 	{
@@ -1654,8 +1654,10 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 		indexOrMemberAssignment(_expr, _array);
 	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
 	{
-		FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
-		if (funType.kind() == FunctionType::Kind::ArrayPush)
+		if (
+			auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
+			funType && funType->kind() == FunctionType::Kind::ArrayPush
+		)
 		{
 			auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
 			solAssert(memberAccess, "");
@@ -2608,6 +2610,33 @@ Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
 	return expr;
 }
 
+Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
+{
+	auto const* expr = &_expr;
+	if (auto const* tuple = dynamic_cast<TupleExpression const*>(expr))
+		return cleanExpression(*innermostTuple(*tuple));
+	if (auto const* functionCall = dynamic_cast<FunctionCall const*>(expr))
+		if (*functionCall->annotation().kind == FunctionCallKind::TypeConversion)
+		{
+			auto typeType = dynamic_cast<TypeType const*>(functionCall->expression().annotation().type);
+			solAssert(typeType, "");
+			if (auto const* arrayType = dynamic_cast<ArrayType const*>(typeType->actualType()))
+				if (arrayType->isByteArray())
+				{
+					// this is a cast to `bytes`
+					solAssert(functionCall->arguments().size() == 1, "");
+					Expression const& arg = *functionCall->arguments()[0];
+					if (
+						auto const* argArrayType = dynamic_cast<ArrayType const*>(arg.annotation().type);
+						argArrayType && argArrayType->isByteArray()
+					)
+						return cleanExpression(arg);
+				}
+		}
+	solAssert(expr, "");
+	return expr;
+}
+
 set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
 {
 	vector<CallableDeclaration const*> callStack;

libsolidity/formal/SMTEncoder.h

@@ -68,6 +68,12 @@ class SMTEncoder: public ASTConstVisitor
 	/// otherwise _expr.
 	static Expression const* innermostTuple(Expression const& _expr);
 
+	/// @returns the expression after stripping redundant syntactic sugar.
+	/// Currently supports stripping:
+	/// 1. 1-tuple; i.e. ((x)) -> x
+	/// 2. Explicit cast from string to bytes; i.e. bytes(s) -> s; for s of type string
+	static Expression const* cleanExpression(Expression const& _expr);
+
 	/// @returns the FunctionDefinition of a FunctionCall
 	/// if possible or nullptr.
 	/// @param _scopeContract is the contract that contains the function currently being

test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	string x;
+
+	function s() public {
+		x = "abc";
+		bytes(x).push("a");
+		assert(bytes(x).length == 4); // should hold
+		assert(bytes(x).length == 3); // should fail
+	}
+}
+// ----
+// Warning 6328: (165-193): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()

test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_2.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	string x;
+
+	function s() public {
+		x = "abc";
+		((bytes(((x))))).push("a");
+		assert(bytes(x).length == 4); // should hold
+		assert(bytes(x).length == 3); // should fail
+	}
+}
+// ----
+// Warning 6328: (173-201): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()