From ad1798b000ebae16cca9a782859ca605114282f9 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 27 Jul 2020 12:11:10 +0200
Subject: [PATCH] [SMTChecker] Fix ICE on fixed bytes access

---
 Changelog.md                                  |  2 +-
 libsolidity/formal/SMTEncoder.cpp             | 19 +++++++++----------
 .../types/fixed_bytes_access_1.sol            |  9 +++++++++
 .../types/fixed_bytes_access_2.sol            | 11 +++++++++++
 .../types/fixed_bytes_access_3.sol            | 18 ++++++++++++++++++
 5 files changed, 48 insertions(+), 11 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol

diff --git a/Changelog.md b/Changelog.md
index 2422ad026..2e857a89f 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -7,7 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
-
+ * SMTChecker: Fix internal error on fixed bytes index access.
 
 
 ### 0.7.0 (2020-07-28)
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index b101a3147..50ede6d13 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -923,6 +923,15 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
 		return;
+	if (_indexAccess.baseExpression().annotation().type->category() == Type::Category::FixedBytes)
+	{
+		m_errorReporter.warning(
+			7989_error,
+			_indexAccess.location(),
+			"Assertion checker does not yet support index accessing fixed bytes."
+		);
+		return;
+	}
 
 	shared_ptr<smt::SymbolicVariable> array;
 	if (auto const* id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
@@ -930,16 +939,6 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
 		array = m_context.variable(*varDecl);
-
-		if (varDecl->type()->category() == Type::Category::FixedBytes)
-		{
-			m_errorReporter.warning(
-				7989_error,
-				_indexAccess.location(),
-				"Assertion checker does not yet support index accessing fixed bytes."
-			);
-			return;
-		}
 	}
 	else if (auto const* innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
 	{
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol
new file mode 100644
index 000000000..636dd7ff1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_1.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract c {
+	bytes10[6] data2;
+	function test() public view returns (bytes10 r2) {
+		r2 = data2[4][5];
+	}
+}
+// ----
+// Warning 7989: (123-134): Assertion checker does not yet support index accessing fixed bytes.
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
new file mode 100644
index 000000000..e81d093f8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(bytes calldata x, uint y) external pure {
+		x[8][0];
+		x[8][5%y];
+	}
+}
+// ----
+// 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
diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
new file mode 100644
index 000000000..5348ca1b4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+contract C {
+	bytes16[][] a;
+	function g() internal view returns (bytes16[] storage) {
+		return a[2];
+	}
+	function h() internal view returns (bytes16) {
+		return a[2][2];
+	}
+	function f() external view {
+		g()[3][4];
+		h()[5];
+	}
+}
+// ----
+// Warning 9118: (238-244): Assertion checker does not yet implement this expression.
+// 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.