[SMTChecker] Fix ICE in array of structs type

Changelog.md

@@ -19,6 +19,7 @@ Build System:
 Bugfixes:
  * SMTChecker: Fix internal error when using ``abi.decode``.
  * SMTChecker: Fix internal error when using arrays or mappings of functions.
+ * SMTChecker: Fix internal error in array of structs type.
 
 
 

libsolidity/formal/SMTEncoder.cpp

@@ -869,8 +869,11 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 {
 	createExpr(_indexAccess);
 
+	if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
+		return;
+
 	shared_ptr<smt::SymbolicVariable> array;
-	if (auto const& id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
+	if (auto const* id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
 	{
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
@@ -885,7 +888,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 			return;
 		}
 	}
-	else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
+	else if (auto const* innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
 	{
 		solAssert(m_context.knownExpression(*innerAccess), "");
 		array = m_context.expression(*innerAccess);
@@ -899,9 +902,6 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		return;
 	}
 
-	if (_indexAccess.annotation().type->category() == Type::Category::TypeType)
-		return;
-
 	solAssert(array, "");
 	defineExpr(_indexAccess, smt::Expression::select(
 		array->currentValue(),

test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol

@@ -13,6 +13,5 @@ contract C {
 // Warning: (206-209): Assertion checker does not yet implement type abi
 // Warning: (225-226): Assertion checker does not yet implement type type(struct C.S storage pointer)
 // Warning: (235-241): Assertion checker does not yet implement type type(uint256[] memory)
-// Warning: (235-241): Assertion checker does not yet implement this expression.
 // Warning: (235-244): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
 // Warning: (206-246): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/no_effect_statements.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract test {
+ struct s { uint a; uint b;}
+    function f() pure public returns (byte) {
+		s;
+		s(1,2);
+		s[7];
+		uint;
+		uint[7];
+    }
+}
+// ----
+// Warning: (125-126): Statement has no effect.
+// Warning: (130-136): Statement has no effect.
+// Warning: (140-144): Statement has no effect.
+// Warning: (148-152): Statement has no effect.
+// Warning: (156-163): Statement has no effect.
+// Warning: (125-126): Assertion checker does not yet implement type type(struct test.s storage pointer)
+// Warning: (130-131): Assertion checker does not yet implement type type(struct test.s storage pointer)
+// Warning: (130-136): Assertion checker does not yet implement type struct test.s memory
+// Warning: (130-136): Assertion checker does not yet implement this expression.
+// Warning: (140-141): Assertion checker does not yet implement type type(struct test.s storage pointer)
+// Warning: (140-144): Assertion checker does not yet implement type type(struct test.s memory[7] memory)
+// Warning: (156-163): Assertion checker does not yet implement type type(uint256[7] memory)

test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol

@@ -7,5 +7,4 @@ function f() public pure { int[][]; }
 // ----
 // Warning: (73-80): Statement has no effect.
 // Warning: (73-78): Assertion checker does not yet implement type type(int256[] memory)
-// Warning: (73-78): Assertion checker does not yet implement this expression.
 // Warning: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory)

test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol

@@ -7,6 +7,5 @@ function f() public pure { int[][][]; }
 // ----
 // Warning: (73-82): Statement has no effect.
 // Warning: (73-78): Assertion checker does not yet implement type type(int256[] memory)
-// Warning: (73-78): Assertion checker does not yet implement this expression.
 // Warning: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory)
 // Warning: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)

test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol

@@ -7,6 +7,5 @@ function f() public pure { (int[][]); }
 // ----
 // Warning: (73-82): Statement has no effect.
 // Warning: (74-79): Assertion checker does not yet implement type type(int256[] memory)
-// Warning: (74-79): Assertion checker does not yet implement this expression.
 // Warning: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory)
 // Warning: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory)

test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol

@@ -7,7 +7,6 @@ function f() public pure { (int[][][]); }
 // ----
 // Warning: (73-84): Statement has no effect.
 // Warning: (74-79): Assertion checker does not yet implement type type(int256[] memory)
-// Warning: (74-79): Assertion checker does not yet implement this expression.
 // Warning: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory)
 // Warning: (74-83): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
 // Warning: (73-84): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)