[SMTChecker] Support fixed bytes index access

Changelog.md

@@ -12,6 +12,7 @@ Compiler Features:
  * SMTChecker: Support structs.
  * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
  * SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``.
+ * SMTChecker: Support fixed bytes index access.
  * Type Checker: Report position of first invalid UTF-8 sequence in ``unicode""`` literals.
  * Type Checker: More detailed error messages why implicit conversions fail.
  * Type Checker: Explain why oversized hex string literals can not be explicitly converted to a shorter ``bytesNN`` type.

libsolidity/formal/SMTEncoder.cpp

@@ -970,13 +970,36 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
 		return;
-	if (_indexAccess.baseExpression().annotation().type->category() == Type::Category::FixedBytes)
+	if (auto const* type = dynamic_cast<FixedBytesType const*>(_indexAccess.baseExpression().annotation().type))
 	{
-		m_errorReporter.warning(
-			7989_error,
-			_indexAccess.location(),
-			"Assertion checker does not yet support index accessing fixed bytes."
-		);
+		smtutil::Expression base = expr(_indexAccess.baseExpression());
+
+		if (type->numBytes() == 1)
+			defineExpr(_indexAccess, base);
+		else
+		{
+			auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_indexAccess.baseExpression().annotation().type);
+			solAssert(!isSigned, "");
+			solAssert(bvSize >= 16, "");
+			solAssert(bvSize % 8 == 0, "");
+
+			smtutil::Expression idx = expr(*_indexAccess.indexExpression());
+
+			auto bvBase = smtutil::Expression::int2bv(base, bvSize);
+			auto bvShl = smtutil::Expression::int2bv(idx * 8, bvSize);
+			auto bvShr = smtutil::Expression::int2bv(bvSize - 8, bvSize);
+			auto result = (bvBase << bvShl) >> bvShr;
+
+			auto anyValue = expr(_indexAccess);
+			m_context.expression(_indexAccess)->increaseIndex();
+			unsigned numBytes = bvSize / 8;
+			auto withBound = smtutil::Expression::ite(
+				idx < numBytes,
+				smtutil::Expression::bv2int(result, false),
+				anyValue
+			);
+			defineExpr(_indexAccess, withBound);
+		}
 		return;
 	}
 

test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol

@@ -6,5 +6,3 @@ contract C {
     }
 }
 // ----
-// Warning 7989: (116-120): Assertion checker does not yet support index accessing fixed bytes.
-// Warning 7989: (108-122): Assertion checker does not yet support index accessing fixed bytes.

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol

@@ -6,4 +6,3 @@ contract c {
 	}
 }
 // ----
-// Warning 7989: (123-134): Assertion checker does not yet support index accessing fixed bytes.

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol

@@ -6,6 +6,4 @@ contract C {
 	}
 }
 // ----
-// Warning 7989: (101-108): Assertion checker does not yet support index accessing fixed bytes.
-// Warning 7989: (112-121): Assertion checker does not yet support index accessing fixed bytes.
 // Warning 3046: (117-120): Division by zero happens here.

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol

@@ -13,5 +13,3 @@ contract C {
 	}
 }
 // ----
-// Warning 7989: (238-247): Assertion checker does not yet support index accessing fixed bytes.
-// Warning 7989: (251-257): Assertion checker does not yet support index accessing fixed bytes.

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_4.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		bytes32 x = 0x00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff;
+		byte z = 0x00;
+		byte o = 0xff;
+		assert(x[0] == z);
+		assert(x[31] == o);
+		assert(x[0] == x[22]);
+		assert(x[0] == x[23]);
+	}
+}
+// ----
+// Warning 6328: (260-281): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_5.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		bytes4 x = 0x01020304;
+		byte b = 0x02;
+		assert(x[0] == b); // fails
+		assert(x[1] == b);
+		assert(x[2] == b); // fails
+		assert(x[3] == b); // fails
+	}
+}
+// ----
+// Warning 6328: (118-135): Assertion violation happens here.
+// Warning 6328: (169-186): Assertion violation happens here.
+// Warning 6328: (199-216): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_6.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		bytes4 x = 0x01020304;
+		byte b = x[3];
+		assert(b == b[0]);
+		assert(b == b[0][0]);
+		assert(b == b[0][0][0][0][0][0][0][0][0][0][0]);
+	}
+}

test/libsolidity/smtCheckerTests/types/fixed_bytes_access_7.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint i) public pure {
+		bytes4 x = 0x01020304;
+		require(i > 3);
+		assert(x[i] == 0x00);
+		i = 5;
+		assert(x[i] == 0);
+		assert(x[i] != 0);
+	}
+}
+// ----
+// Warning 6328: (125-145): Assertion violation happens here.
+// Warning 6328: (158-175): Assertion violation happens here.
+// Warning 6328: (179-196): Assertion violation happens here.