[SMTChecker] Fix literal string type mismatch

libsolidity/formal/SMTEncoder.cpp

@@ -187,7 +187,7 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 						declarations.at(i) &&
 						m_context.knownVariable(*declarations.at(i))
 					)
-						assignment(*declarations.at(i), components.at(i)->currentValue());
+						assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type()));
 			}
 		}
 	}
@@ -235,30 +235,43 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	}
 	else
 	{
+		auto const& type = _assignment.annotation().type;
 		vector<smt::Expression> rightArguments;
 		if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple)
 		{
-			auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.rightHandSide()));
-			solAssert(symbTuple, "");
-			for (auto const& component: symbTuple->components())
+			auto symbTupleLeft = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.leftHandSide()));
+			solAssert(symbTupleLeft, "");
+			auto symbTupleRight = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.rightHandSide()));
+			solAssert(symbTupleRight, "");
+
+			auto const& leftComponents = symbTupleLeft->components();
+			auto const& rightComponents = symbTupleRight->components();
+			solAssert(leftComponents.size() == rightComponents.size(), "");
+
+			for (unsigned i = 0; i < leftComponents.size(); ++i)
 			{
+				auto const& left = leftComponents.at(i);
+				auto const& right = rightComponents.at(i);
 				/// Right hand side tuple component cannot be empty.
-				solAssert(component, "");
-				rightArguments.push_back(component->currentValue());
+				solAssert(right, "");
+				if (left)
+					rightArguments.push_back(right->currentValue(left->originalType()));
+				else
+					rightArguments.push_back(right->currentValue());
 			}
 		}
 		else
 		{
 			auto rightHandSide = compoundOps.count(op) ?
 				compoundAssignment(_assignment) :
-				expr(_assignment.rightHandSide());
+				expr(_assignment.rightHandSide(), type);
 			defineExpr(_assignment, rightHandSide);
-			rightArguments.push_back(expr(_assignment));
+			rightArguments.push_back(expr(_assignment, type));
 		}
 		assignment(
 			_assignment.leftHandSide(),
 			rightArguments,
-			_assignment.annotation().type,
+			type,
 			_assignment.location()
 		);
 	}
@@ -620,16 +633,10 @@ void SMTEncoder::endVisit(Literal const& _literal)
 		defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
 	else if (smt::isBool(type.category()))
 		defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
+	else if (smt::isStringLiteral(type.category()))
+		createExpr(_literal);
 	else
 	{
-		if (type.category() == Type::Category::StringLiteral)
-		{
-			auto stringType = TypeProvider::stringMemory();
-			auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
-			solAssert(stringLit, "");
-			auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_context);
-			m_context.createExpression(_literal, result.second);
-		}
 		m_errorReporter.warning(
 			_literal.location(),
 			"Assertion checker does not yet support the type of this literal (" +
@@ -653,7 +660,7 @@ void SMTEncoder::endVisit(Return const& _return)
 			for (unsigned i = 0; i < returnParams.size(); ++i)
 			{
 				solAssert(components.at(i), "");
-				m_context.addAssertion(components.at(i)->currentValue() == m_context.newValue(*returnParams.at(i)));
+				m_context.addAssertion(components.at(i)->currentValue(returnParams.at(i)->type()) == m_context.newValue(*returnParams.at(i)));
 			}
 		}
 		else if (returnParams.size() == 1)
@@ -957,14 +964,15 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
 
 void SMTEncoder::compareOperation(BinaryOperation const& _op)
 {
-	solAssert(_op.annotation().commonType, "");
-	if (smt::isSupportedType(_op.annotation().commonType->category()))
+	auto const& commonType = _op.annotation().commonType;
+	solAssert(commonType, "");
+	if (smt::isSupportedType(commonType->category()))
 	{
-		smt::Expression left(expr(_op.leftExpression()));
-		smt::Expression right(expr(_op.rightExpression()));
+		smt::Expression left(expr(_op.leftExpression(), commonType));
+		smt::Expression right(expr(_op.rightExpression(), commonType));
 		Token op = _op.getOperator();
 		shared_ptr<smt::Expression> value;
-		if (smt::isNumber(_op.annotation().commonType->category()))
+		if (smt::isNumber(commonType->category()))
 		{
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
@@ -977,7 +985,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 		}
 		else // Bool
 		{
-			solUnimplementedAssert(smt::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
+			solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported");
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
 				/*op == Token::NotEqual*/ (left != right)
@@ -1104,7 +1112,7 @@ smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
 {
-	assignment(_variable, expr(_value));
+	assignment(_variable, expr(_value, _variable.type()));
 }
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value)
@@ -1258,14 +1266,15 @@ bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl)
 	return true;
 }
 
-smt::Expression SMTEncoder::expr(Expression const& _e)
+smt::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType)
 {
 	if (!m_context.knownExpression(_e))
 	{
 		m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
 		createExpr(_e);
 	}
-	return m_context.expression(_e)->currentValue();
+
+	return m_context.expression(_e)->currentValue(_targetType);
 }
 
 void SMTEncoder::createExpr(Expression const& _e)

libsolidity/formal/SMTEncoder.h

@@ -175,8 +175,10 @@ protected:
 	/// @returns an expression denoting the value of the variable declared in @a _decl
 	/// at the given index. Does not ensure that this index exists.
 	smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index);
-	/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
-	smt::Expression expr(Expression const& _e);
+	/// Returns the expression corresponding to the AST node.
+	/// If _targetType is not null apply conversion.
+	/// Throws if the expression does not exist.
+	smt::Expression expr(Expression const& _e, TypePointer _targetType = nullptr);
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
 	/// Creates the expression and sets its value.

libsolidity/formal/SymbolicTypes.cpp

@@ -64,6 +64,13 @@ SortPointer smtSort(solidity::Type const& _type)
 			solAssert(mapType, "");
 			return make_shared<ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
 		}
+		else if (isStringLiteral(_type.category()))
+		{
+			auto stringLitType = dynamic_cast<solidity::StringLiteralType const*>(&_type);
+			solAssert(stringLitType, "");
+			auto intSort = make_shared<Sort>(Kind::Int);
+			return make_shared<ArraySort>(intSort, intSort);
+		}
 		else
 		{
 			solAssert(isArray(_type.category()), "");
@@ -127,19 +134,19 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 	if (!isSupportedTypeDeclaration(_type))
 	{
 		abstract = true;
-		var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _context);
+		var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), type, _uniqueName, _context);
 	}
 	else if (isBool(_type.category()))
 		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
 	else if (isFunction(_type.category()))
 		var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
 	else if (isInteger(_type.category()))
-		var = make_shared<SymbolicIntVariable>(type, _uniqueName, _context);
+		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	else if (isFixedBytes(_type.category()))
 	{
 		auto fixedBytesType = dynamic_cast<solidity::FixedBytesType const*>(type);
 		solAssert(fixedBytesType, "");
-		var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _context);
+		var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
 	}
 	else if (isAddress(_type.category()) || isContract(_type.category()))
 		var = make_shared<SymbolicAddressVariable>(_uniqueName, _context);
@@ -150,16 +157,21 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		auto rational = dynamic_cast<solidity::RationalNumberType const*>(&_type);
 		solAssert(rational, "");
 		if (rational->isFractional())
-			var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _context);
+			var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), type, _uniqueName, _context);
 		else
-			var = make_shared<SymbolicIntVariable>(type, _uniqueName, _context);
+			var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	}
 	else if (isMapping(_type.category()))
 		var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _context);
 	else if (isArray(_type.category()))
-		var = make_shared<SymbolicArrayVariable>(type, _uniqueName, _context);
+		var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
 	else if (isTuple(_type.category()))
 		var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
+	else if (isStringLiteral(_type.category()))
+	{
+		auto stringType = TypeProvider::stringMemory();
+		var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
+	}
 	else
 		solAssert(false, "");
 	return make_pair(abstract, var);
@@ -232,7 +244,8 @@ bool isMapping(solidity::Type::Category _category)
 
 bool isArray(solidity::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Array;
+	return _category == solidity::Type::Category::Array ||
+		_category == solidity::Type::Category::StringLiteral;
 }
 
 bool isTuple(solidity::Type::Category _category)
@@ -240,6 +253,11 @@ bool isTuple(solidity::Type::Category _category)
 	return _category == solidity::Type::Category::Tuple;
 }
 
+bool isStringLiteral(solidity::Type::Category _category)
+{
+	return _category == solidity::Type::Category::StringLiteral;
+}
+
 Expression minValue(solidity::IntegerType const& _type)
 {
 	return Expression(_type.minValue());

libsolidity/formal/SymbolicTypes.h

@@ -54,6 +54,7 @@ bool isFunction(solidity::Type::Category _category);
 bool isMapping(solidity::Type::Category _category);
 bool isArray(solidity::Type::Category _category);
 bool isTuple(solidity::Type::Category _category);
+bool isStringLiteral(solidity::Type::Category _category);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,

libsolidity/formal/SymbolicVariables.cpp

@@ -27,10 +27,12 @@ using namespace dev::solidity::smt;
 
 SymbolicVariable::SymbolicVariable(
 	solidity::TypePointer _type,
+	solidity::TypePointer _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	m_type(move(_type)),
+	m_type(_type),
+	m_originalType(_originalType),
 	m_uniqueName(move(_uniqueName)),
 	m_context(_context),
 	m_ssa(make_unique<SSAVariable>())
@@ -53,7 +55,7 @@ SymbolicVariable::SymbolicVariable(
 	solAssert(m_sort, "");
 }
 
-Expression SymbolicVariable::currentValue() const
+Expression SymbolicVariable::currentValue(solidity::TypePointer const&) const
 {
 	return valueAtIndex(m_ssa->index());
 }
@@ -95,17 +97,18 @@ SymbolicBoolVariable::SymbolicBoolVariable(
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicVariable(move(_type), move(_uniqueName), _context)
+	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
 	solAssert(m_type->category() == solidity::Type::Category::Bool, "");
 }
 
 SymbolicIntVariable::SymbolicIntVariable(
 	solidity::TypePointer _type,
+	solidity::TypePointer _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicVariable(move(_type), move(_uniqueName), _context)
+	SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
 {
 	solAssert(isNumber(m_type->category()), "");
 }
@@ -114,16 +117,17 @@ SymbolicAddressVariable::SymbolicAddressVariable(
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _context)
+	SymbolicIntVariable(TypeProvider::uint(160), TypeProvider::uint(160), move(_uniqueName), _context)
 {
 }
 
 SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
+	solidity::TypePointer _originalType,
 	unsigned _numBytes,
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _context)
+	SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), _originalType, move(_uniqueName), _context)
 {
 }
 
@@ -132,7 +136,7 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicVariable(move(_type), move(_uniqueName), _context),
+	SymbolicVariable(_type, _type, move(_uniqueName), _context),
 	m_declaration(m_context.newVariable(currentName(), m_sort))
 {
 	solAssert(m_type->category() == solidity::Type::Category::Function, "");
@@ -171,27 +175,41 @@ SymbolicMappingVariable::SymbolicMappingVariable(
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicVariable(move(_type), move(_uniqueName), _context)
+	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
 	solAssert(isMapping(m_type->category()), "");
 }
 
 SymbolicArrayVariable::SymbolicArrayVariable(
 	solidity::TypePointer _type,
+	solidity::TypePointer _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicVariable(move(_type), move(_uniqueName), _context)
+	SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
 {
 	solAssert(isArray(m_type->category()), "");
 }
 
+Expression SymbolicArrayVariable::currentValue(solidity::TypePointer const& _targetType) const
+{
+	if (_targetType)
+		// StringLiterals are encoded as SMT arrays in the generic case,
+		// but they can also be compared/assigned to fixed bytes, in which
+		// case they'd need to be encoded as numbers.
+		if (auto strType = dynamic_cast<StringLiteralType const*>(m_originalType))
+			if (_targetType->category() == solidity::Type::Category::FixedBytes)
+				return smt::Expression(u256(toHex(asBytes(strType->value()), HexPrefix::Add)));
+
+	return SymbolicVariable::currentValue(_targetType);
+}
+
 SymbolicEnumVariable::SymbolicEnumVariable(
 	solidity::TypePointer _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicVariable(move(_type), move(_uniqueName), _context)
+	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
 	solAssert(isEnum(m_type->category()), "");
 }
@@ -201,7 +219,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 	string _uniqueName,
 	EncodingContext& _context
 ):
-	SymbolicVariable(move(_type), move(_uniqueName), _context)
+	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
 	solAssert(isTuple(m_type->category()), "");
 }

libsolidity/formal/SymbolicVariables.h

@@ -40,6 +40,7 @@ class SymbolicVariable
 public:
 	SymbolicVariable(
 		solidity::TypePointer _type,
+		solidity::TypePointer _originalType,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -51,7 +52,7 @@ public:
 
 	virtual ~SymbolicVariable() = default;
 
-	Expression currentValue() const;
+	virtual Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const;
 	std::string currentName() const;
 	virtual Expression valueAtIndex(int _index) const;
 	virtual std::string nameAtIndex(int _index) const;
@@ -67,6 +68,7 @@ public:
 
 	SortPointer const& sort() const { return m_sort; }
 	solidity::TypePointer const& type() const { return m_type; }
+	solidity::TypePointer const& originalType() const { return m_originalType; }
 
 protected:
 	std::string uniqueSymbol(unsigned _index) const;
@@ -75,6 +77,8 @@ protected:
 	SortPointer m_sort;
 	/// Solidity type, used for size and range in number types.
 	solidity::TypePointer m_type;
+	/// Solidity original type, used for type conversion if necessary.
+	solidity::TypePointer m_originalType;
 	std::string m_uniqueName;
 	EncodingContext& m_context;
 	std::unique_ptr<SSAVariable> m_ssa;
@@ -101,6 +105,7 @@ class SymbolicIntVariable: public SymbolicVariable
 public:
 	SymbolicIntVariable(
 		solidity::TypePointer _type,
+		solidity::TypePointer _originalType,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -125,6 +130,7 @@ class SymbolicFixedBytesVariable: public SymbolicIntVariable
 {
 public:
 	SymbolicFixedBytesVariable(
+		solidity::TypePointer _originalType,
 		unsigned _numBytes,
 		std::string _uniqueName,
 		EncodingContext& _context
@@ -180,9 +186,12 @@ class SymbolicArrayVariable: public SymbolicVariable
 public:
 	SymbolicArrayVariable(
 		solidity::TypePointer _type,
+		solidity::TypePointer _originalTtype,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
+
+	Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const override;
 };
 
 /**