Merge pull request #11116 from blishko/issue-10985

[SMTChecker] Handle InaccessibleDynamicType

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * AST Output: Fix ``kind`` field of ``ModifierInvocation`` for base constructor calls.
+ * SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available.
 
 
 AST Changes:

libsolidity/formal/SMTEncoder.cpp

@@ -2443,14 +2443,13 @@ void SMTEncoder::createExpr(Expression const& _e)
 
 void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
 {
+	auto type = _e.annotation().type;
 	createExpr(_e);
 	solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
-	m_context.addAssertion(expr(_e) == _value);
+	if (!smt::isInaccessibleDynamic(*type))
+		m_context.addAssertion(expr(_e) == _value);
 
-	if (
+	if (m_checked && smt::isNumber(*type))
-		auto type = _e.annotation().type;
-		m_checked && smt::isNumber(*type)
-	)
 		m_context.addAssertion(smtutil::Expression::implies(
 			currentPathConditions(),
 			smt::symbolicUnknownConstraints(expr(_e), type)
@@ -2469,8 +2468,11 @@ void SMTEncoder::defineExpr(Expression const& _e, vector<optional<smtutil::Expre
 	symbTuple->increaseIndex();
 	auto const& symbComponents = symbTuple->components();
 	solAssert(symbComponents.size() == _values.size(), "");
+	auto tupleType = dynamic_cast<TupleType const*>(_e.annotation().type);
+	solAssert(tupleType, "");
+	solAssert(tupleType->components().size() == symbComponents.size(), "");
 	for (unsigned i = 0; i < symbComponents.size(); ++i)
-		if (_values[i])
+		if (_values[i] && !smt::isInaccessibleDynamic(*tupleType->components()[i]))
 			m_context.addAssertion(symbTuple->component(i) == *_values[i]);
 }
 

libsolidity/formal/SymbolicTypes.cpp

@@ -386,6 +386,11 @@ bool isNonRecursiveStruct(frontend::Type const& _type)
 	return structType && !structType->recursive();
 }
 
+bool isInaccessibleDynamic(frontend::Type const& _type)
+{
+	return _type.category() == frontend::Type::Category::InaccessibleDynamic;
+}
+
 smtutil::Expression minValue(frontend::IntegerType const& _type)
 {
 	return smtutil::Expression(_type.minValue());

libsolidity/formal/SymbolicTypes.h

@@ -59,6 +59,7 @@ bool isArray(frontend::Type const& _type);
 bool isTuple(frontend::Type const& _type);
 bool isStringLiteral(frontend::Type const& _type);
 bool isNonRecursiveStruct(frontend::Type const& _type);
+bool isInaccessibleDynamic(frontend::Type const& _type);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,

test/libsolidity/smtCheckerTests/functions/getters/inaccessible_dynamic_type_1.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+	struct S {
+		string a;
+		uint256 y;
+	}
+	S public s;
+	function g() public view returns (uint256) {
+		this.s();
+	}
+}
+// ====
+// EVMVersion: <=spuriousDragon
+// ----
+// Warning 6321: (133-140): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.

test/libsolidity/smtCheckerTests/functions/getters/inaccessible_dynamic_type_2.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public returns(bool[]memory) {
+		this.f();
+	}
+}
+// ====
+// EVMVersion: <=spuriousDragon
+// ----
+// Warning 6321: (74-86): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.

test/libsolidity/smtCheckerTests/functions/getters/inaccessible_dynamic_type_3.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	struct S {
+		string a;
+	}
+	S public s;
+	function g() public view returns (uint256) {
+		this.s();
+	}
+}
+// ====
+// EVMVersion: <=spuriousDragon
+// ----
+// Warning 6321: (120-127): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.

test/libsolidity/smtCheckerTests/functions/getters/inaccessible_dynamic_type_4.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+	string public s;
+	function g() public view returns (uint256) {
+		this.s();
+	}
+}
+// ====
+// EVMVersion: <=spuriousDragon
+// ----
+// Warning 6321: (98-105): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.