[SMTChecker] Fix ICE implicit conversion string literal -> byte

Changelog.md

@@ -5,6 +5,7 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
+ * SMTChecker: Fix internal error on conversion from string literal to byte.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

libsolidity/formal/SMTEncoder.cpp

@@ -878,10 +878,8 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 	if (argSize == castSize)
 	{
 		// If sizes are the same, it's possible that the signs are different.
-		if (smt::isNumber(*funCallType))
+		if (smt::isNumber(*funCallType) && smt::isNumber(*argType))
 		{
-			solAssert(smt::isNumber(*argType), "");
-
 			// castIsSigned && !argIsSigned => might overflow if arg > castType.max
 			// !castIsSigned && argIsSigned => might underflow if arg < castType.min
 			// !castIsSigned && !argIsSigned => ok
@@ -1211,9 +1209,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
 	solAssert(arrayVar, "");
+	TypePointer baseType = _indexAccess.baseExpression().annotation().type;
 	defineExpr(_indexAccess, smtutil::Expression::select(
 		arrayVar->elements(),
-		expr(*_indexAccess.indexExpression())
+		expr(*_indexAccess.indexExpression(), keyType(baseType))
 	));
 	setSymbolicUnknownValue(
 		expr(_indexAccess),
@@ -1245,17 +1244,19 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 			auto const& base = indexAccess->baseExpression();
 			if (dynamic_cast<Identifier const*>(&base))
 				base.accept(*this);
+
+			TypePointer baseType = base.annotation().type;
+			auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
 			solAssert(symbArray, "");
-			auto baseType = symbArray->type();
 			toStore = smtutil::Expression::tuple_constructor(
 				smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
-				{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+				{smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
 			);
 			m_context.expression(*indexAccess)->increaseIndex();
 			defineExpr(*indexAccess, smtutil::Expression::select(
 				symbArray->elements(),
-				expr(*indexAccess->indexExpression())
+				indexExpr
 			));
 			lastExpr = &indexAccess->baseExpression();
 		}
@@ -2239,6 +2240,19 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
 	return base;
 }
 
+TypePointer SMTEncoder::keyType(TypePointer _type)
+{
+	if (auto const* mappingType = dynamic_cast<MappingType const*>(_type))
+		return mappingType->keyType();
+	if (
+		dynamic_cast<ArrayType const*>(_type) ||
+		dynamic_cast<ArraySliceType const*>(_type)
+	)
+		return TypeProvider::uint256();
+	else
+		solAssert(false, "");
+}
+
 Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
 {
 	auto const* tuple = dynamic_cast<TupleExpression const*>(&_expr);

libsolidity/formal/SMTEncoder.h

@@ -55,6 +55,11 @@ public:
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 
+	/// @returns the key type in _type.
+	/// _type must allow IndexAccess, that is,
+	/// it must be either ArrayType or MappingType
+	static TypePointer keyType(TypePointer _type);
+
 	/// @returns the innermost element in a chain of 1-tuples if applicable,
 	/// otherwise _expr.
 	static Expression const* innermostTuple(Expression const& _expr);

test/libsolidity/smtCheckerTests/operators/slice_bytes.sol

@@ -0,0 +1,6 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(bytes calldata b) external pure {
+		((b[:])[5]);
+	}
+}

test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (byte => uint) map;
+	function f() public {
+		map[""] = 2;
+		uint x = map[""];
+		g("");
+		byte b = "";
+		assert(x == map[b]);
+		assert(x == map["x"]);
+	}
+	function g(byte b) internal pure {}
+}
+// ----
+// Warning 6328: (182-203): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_explicit.sol

@@ -0,0 +1,4 @@
+pragma experimental SMTChecker;
+contract SMT {
+	bytes32 constant internal NULL_BYTES32 = bytes32('');
+}