Remove unreachable/redundant error messages

libsolidity/formal/SMTEncoder.cpp

@@ -403,8 +403,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 			assignment(
 				_assignment.leftHandSide(),
 				expr(_assignment, type),
-				type,
+				type
-				_assignment.location()
 			);
 		}
 	}
@@ -527,11 +526,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 			)
 				indexOrMemberAssignment(_op.subExpression(), symbVar->currentValue());
 			else
-				m_errorReporter.warning(
+				solAssert(false, "");
-					2683_error,
-					_op.location(),
-					"Assertion checker does not yet implement \"delete\" for this expression."
-				);
 		}
 		break;
 	}
@@ -1061,11 +1056,15 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 		}
 		else
 		{
-			m_errorReporter.warning(
+			auto type = lastExpr->annotation().type;
-				9056_error,
+			if (
-				_expr.location(),
+				dynamic_cast<ReferenceType const*>(type) ||
-				"Assertion checker does not yet implement this expression."
+				dynamic_cast<MappingType const*>(type)
-			);
+			)
+				resetReferences(type);
+
+			m_context.expression(*lastExpr)->increaseIndex();
+			m_context.addAssertion(expr(*lastExpr) == toStore);
 			break;
 		}
 	}
@@ -1167,12 +1166,6 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 			arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
 		}
 	}
-	else if (dynamic_cast<MemberAccess const*>(expr))
-		m_errorReporter.warning(
-			9599_error,
-			_expr.location(),
-			"Assertion checker does not yet implement this expression."
-		);
 	else
 		solAssert(false, "");
 }
@@ -1461,8 +1454,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
 void SMTEncoder::assignment(
 	Expression const& _left,
 	smtutil::Expression const& _right,
-	TypePointer const& _type,
+	TypePointer const& _type
-	langutil::SourceLocation const& _location
 )
 {
 	solAssert(
@@ -1477,12 +1469,6 @@ void SMTEncoder::assignment(
 		// Give it a new index anyway to keep the SSA scheme sound.
 		if (auto varDecl = identifierToVariable(*left))
 			m_context.newValue(*varDecl);
-
-		m_errorReporter.warning(
-			6191_error,
-			_location,
-			"Assertion checker does not yet implement type " + _type->toString()
-		);
 	}
 	else if (auto varDecl = identifierToVariable(*left))
 		assignment(*varDecl, _right);
@@ -1492,11 +1478,7 @@ void SMTEncoder::assignment(
 	)
 		indexOrMemberAssignment(*left, _right);
 	else
-		m_errorReporter.warning(
+		solAssert(false, "");
-			8182_error,
-			_location,
-			"Assertion checker does not yet implement such assignments."
-		);
 }
 
 void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
@@ -1525,7 +1507,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
 			else
 			{
 				auto type = lExpr.annotation().type;
-				assignment(lExpr, expr(rExpr, type), type, lExpr.location());
+				assignment(lExpr, expr(rExpr, type), type);
 			}
 		}
 	}
@@ -1542,7 +1524,7 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
 
 		for (unsigned i = 0; i < lComponents.size(); ++i)
 			if (auto component = lComponents.at(i); component && rComponents.at(i))
-				assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type, component->location());
+				assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type);
 	}
 }
 
@@ -1706,32 +1688,43 @@ void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
 		if (_var.isStateVariable() && _varDecl.isStateVariable())
 			return false;
 
-		TypePointer prefix = _var.type();
+		return sameTypeOrSubtype(_var.type(), _varDecl.type());
-		TypePointer originalType = typeWithoutPointer(_varDecl.type());
-		while (
-			prefix->category() == Type::Category::Mapping ||
-			prefix->category() == Type::Category::Array
-		)
-		{
-			if (*originalType == *typeWithoutPointer(prefix))
-				return true;
-			if (prefix->category() == Type::Category::Mapping)
-			{
-				auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
-				solAssert(mapPrefix, "");
-				prefix = mapPrefix->valueType();
-			}
-			else
-			{
-				auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
-				solAssert(arrayPrefix, "");
-				prefix = arrayPrefix->baseType();
-			}
-		}
-		return false;
 	});
 }
 
+void SMTEncoder::resetReferences(TypePointer _type)
+{
+	m_context.resetVariables([&](VariableDeclaration const& _var) {
+		return sameTypeOrSubtype(_var.type(), _type);
+	});
+}
+
+bool SMTEncoder::sameTypeOrSubtype(TypePointer _a, TypePointer _b)
+{
+	TypePointer prefix = _a;
+	while (
+		prefix->category() == Type::Category::Mapping ||
+		prefix->category() == Type::Category::Array
+	)
+	{
+		if (*typeWithoutPointer(_b) == *typeWithoutPointer(prefix))
+			return true;
+		if (prefix->category() == Type::Category::Mapping)
+		{
+			auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
+			solAssert(mapPrefix, "");
+			prefix = mapPrefix->valueType();
+		}
+		else
+		{
+			auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
+			solAssert(arrayPrefix, "");
+			prefix = arrayPrefix->baseType();
+		}
+	}
+	return false;
+}
+
 TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
 {
 	if (auto refType = dynamic_cast<ReferenceType const*>(_type))

libsolidity/formal/SMTEncoder.h

@@ -168,8 +168,7 @@ protected:
 	void assignment(
 		Expression const& _left,
 		smtutil::Expression const& _right,
-		TypePointer const& _type,
+		TypePointer const& _type
-		langutil::SourceLocation const& _location
 	);
 	/// Handle assignments between tuples.
 	void tupleAssignment(Expression const& _left, Expression const& _right);
@@ -196,8 +195,12 @@ protected:
 	/// Resets all references/pointers that have the same type or have
 	/// a subexpression of the same type as _varDecl.
 	void resetReferences(VariableDeclaration const& _varDecl);
+	/// Resets all references/pointers that have type _type.
+	void resetReferences(TypePointer _type);
 	/// @returns the type without storage pointer information if it has it.
 	TypePointer typeWithoutPointer(TypePointer const& _type);
+	/// @returns whether _a or a subtype of _a is the same as _b.
+	bool sameTypeOrSubtype(TypePointer _a, TypePointer _b);
 
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables