Report out of bounds index access

libsolidity/formal/CHC.cpp

@@ -788,6 +788,32 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
 	verificationTargetEncountered(&_arrayPop, VerificationTargetType::PopEmptyArray, symbArray->length() <= 0);
 }
 
+void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess)
+{
+	if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
+		return;
+
+	auto baseType = _indexAccess.baseExpression().annotation().type;
+
+	optional<smtutil::Expression> length;
+	if (smt::isArray(*baseType))
+		length = dynamic_cast<smt::SymbolicArrayVariable const&>(
+			*m_context.expression(_indexAccess.baseExpression())
+		).length();
+	else if (auto const* type = dynamic_cast<FixedBytesType const*>(baseType))
+		length = smtutil::Expression(static_cast<size_t>(type->numBytes()));
+
+	optional<smtutil::Expression> target;
+	if (
+		auto index = _indexAccess.indexExpression();
+		index && length
+	)
+		target = expr(*index) < 0 || expr(*index) >= *length;
+
+	if (target)
+		verificationTargetEncountered(&_indexAccess, VerificationTargetType::OutOfBounds, *target);
+}
+
 pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	Token _op,
 	smtutil::Expression const& _left,
@@ -1415,6 +1441,12 @@ void CHC::checkVerificationTargets()
 			errorType = "Empty array \"pop\"";
 			errorReporterId = 2529_error;
 		}
+		else if (target.type == VerificationTargetType::OutOfBounds)
+		{
+			solAssert(dynamic_cast<IndexAccess const*>(target.errorNode), "");
+			errorType = "Out of bounds access";
+			errorReporterId = 6368_error;
+		}
 		else if (
 			target.type == VerificationTargetType::Underflow ||
 			target.type == VerificationTargetType::Overflow

libsolidity/formal/CHC.h

@@ -97,6 +97,7 @@ private:
 	void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
 	void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
+	void makeOutOfBoundsVerificationTarget(IndexAccess const& _access) override;
 	/// Creates underflow/overflow verification targets.
 	std::pair<smtutil::Expression, smtutil::Expression> arithmeticOperation(
 		Token _op,

libsolidity/formal/ModelCheckerSettings.cpp

@@ -36,7 +36,8 @@ std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const&
 		{"divByZero", TargetType::DivByZero},
 		{"balance", TargetType::Balance},
 		{"assert", TargetType::Assert},
-		{"popEmptyArray", TargetType::PopEmptyArray}
+		{"popEmptyArray", TargetType::PopEmptyArray},
+		{"outOfBounds", TargetType::OutOfBounds}
 	};
 
 	set<TargetType> chosenTargets;

libsolidity/formal/ModelCheckerSettings.h

@@ -54,7 +54,7 @@ struct ModelCheckerEngine
 	}
 };
 
-enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray };
+enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray, OutOfBounds };
 
 struct ModelCheckerTargets
 {

libsolidity/formal/SMTEncoder.cpp

@@ -1382,6 +1382,9 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
 		return;
+
+	makeOutOfBoundsVerificationTarget(_indexAccess);
+
 	if (auto const* type = dynamic_cast<FixedBytesType const*>(_indexAccess.baseExpression().annotation().type))
 	{
 		smtutil::Expression base = expr(_indexAccess.baseExpression());
@@ -1430,6 +1433,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
 	solAssert(arrayVar, "");
+
 	Type const* baseType = _indexAccess.baseExpression().annotation().type;
 	defineExpr(_indexAccess, smtutil::Expression::select(
 		arrayVar->elements(),

libsolidity/formal/SMTEncoder.h

@@ -224,6 +224,8 @@ protected:
 	/// Allows BMC and CHC to create verification targets for popping
 	/// an empty array.
 	virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
+	/// Allows BMC and CHC to create verification targets for out of bounds access.
+	virtual void makeOutOfBoundsVerificationTarget(IndexAccess const&) {}
 
 	void addArrayLiteralAssertions(
 		smt::SymbolicArrayVariable& _symArray,