Merge pull request #6722 from ethereum/smt_fix_variable_usage

[SMTChecker] Fix VariableUsage for IndexAccess

libsolidity/formal/SMTChecker.cpp

@@ -1020,6 +1020,7 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
 	}
 	else
 	{
+		createExpr(_indexAccess);
 		m_errorReporter.warning(
 			_indexAccess.location(),
 			"Assertion checker does not yet implement this expression."
@@ -1096,10 +1097,19 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 		));
 	}
 	else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
+	{
+		auto identifier = dynamic_cast<Identifier const*>(leftmostBase(indexAccess));
+		if (identifier)
+		{
+			auto varDecl = identifierToVariable(*identifier);
+			newValue(*varDecl);
+		}
+
 		m_errorReporter.warning(
 			indexAccess.location(),
 			"Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays."
 		);
+	}
 	else
 		m_errorReporter.warning(
 			_expr.location(),
@@ -1982,6 +1992,14 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa
 	return nullptr;
 }
 
+Expression const* SMTChecker::leftmostBase(IndexAccess const& _indexAccess)
+{
+	Expression const* base = &_indexAccess.baseExpression();
+	while (auto access = dynamic_cast<IndexAccess const*>(base))
+		base = &access->baseExpression();
+	return base;
+}
+
 set<VariableDeclaration const*> SMTChecker::touchedVariables(ASTNode const& _node)
 {
 	solAssert(!m_callStack.empty(), "");

libsolidity/formal/SMTChecker.h

@@ -55,9 +55,11 @@ public:
 	/// the constructor.
 	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
 
-	/// @return the FunctionDefinition of a called function if possible and should inline,
+	/// @returns the FunctionDefinition of a called function if possible and should inline,
 	/// otherwise nullptr.
 	static FunctionDefinition const* inlinedFunctionCallToDefinition(FunctionCall const& _funCall);
+	/// @returns the leftmost identifier in a multi-d IndexAccess.
+	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
 
 private:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,

libsolidity/formal/VariableUsage.cpp

@@ -25,17 +25,32 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
+set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<CallableDeclaration const*> const& _outerCallstack)
+{
+	m_touchedVariables.clear();
+	m_callStack.clear();
+	m_callStack += _outerCallstack;
+	m_lastCall = m_callStack.back();
+	_node.accept(*this);
+	return m_touchedVariables;
+}
+
 void VariableUsage::endVisit(Identifier const& _identifier)
 {
-	Declaration const* declaration = _identifier.annotation().referencedDeclaration;
+	if (_identifier.annotation().lValueRequested)
-	solAssert(declaration, "");
+		checkIdentifier(_identifier);
-	if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
+}
-		if (_identifier.annotation().lValueRequested)
+
-		{
+void VariableUsage::endVisit(IndexAccess const& _indexAccess)
-			solAssert(m_lastCall, "");
+{
-			if (!varDecl->isLocalVariable() || varDecl->functionOrModifierDefinition() == m_lastCall)
+	if (_indexAccess.annotation().lValueRequested)
-				m_touchedVariables.insert(varDecl);
+	{
-		}
+		/// identifier.annotation().lValueRequested == false, that's why we
+		/// need to check that before.
+		auto identifier = dynamic_cast<Identifier const*>(SMTChecker::leftmostBase(_indexAccess));
+		if (identifier)
+			checkIdentifier(*identifier);
+	}
 }
 
 void VariableUsage::endVisit(FunctionCall const& _funCall)
@@ -75,12 +90,14 @@ void VariableUsage::endVisit(PlaceholderStatement const&)
 		funDef->body().accept(*this);
 }
 
-set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<CallableDeclaration const*> const& _outerCallstack)
+void VariableUsage::checkIdentifier(Identifier const& _identifier)
 {
-	m_touchedVariables.clear();
+	Declaration const* declaration = _identifier.annotation().referencedDeclaration;
-	m_callStack.clear();
+	solAssert(declaration, "");
-	m_callStack += _outerCallstack;
+	if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
-	m_lastCall = m_callStack.back();
+	{
-	_node.accept(*this);
+		solAssert(m_lastCall, "");
-	return m_touchedVariables;
+		if (!varDecl->isLocalVariable() || varDecl->functionOrModifierDefinition() == m_lastCall)
+			m_touchedVariables.insert(varDecl);
+	}
 }

libsolidity/formal/VariableUsage.h

@@ -38,12 +38,16 @@ public:
 
 private:
 	void endVisit(Identifier const& _node) override;
+	void endVisit(IndexAccess const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	void endVisit(ModifierInvocation const& _node) override;
 	void endVisit(PlaceholderStatement const& _node) override;
 
+	/// Checks whether an identifier should be added to touchedVariables.
+	void checkIdentifier(Identifier const& _identifier);
+
 	std::set<VariableDeclaration const*> m_touchedVariables;
 	std::vector<CallableDeclaration const*> m_callStack;
 	CallableDeclaration const* m_lastCall = nullptr;

test/libsolidity/smtCheckerTests/types/array_branch_1d.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool b, uint[] memory c) public {
+		c[0] = 0;
+		if (b)
+			c[0] = 1;
+		assert(c[0] > 0);
+	}
+}
+// ----
+// Warning: (47-148): Function state mutability can be restricted to pure
+// Warning: (128-144): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_branch_2d.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][] c;
+	function f(bool b) public {
+		c[0][0] = 0;
+		if (b)
+			c[0][0] = 1;
+		assert(c[0][0] > 0);
+	}
+}
+// ----
+// Warning: (90-97): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (115-122): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (130-149): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_branch_3d.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][][] c;
+	function f(bool b) public {
+		c[0][0][0] = 0;
+		if (b)
+			c[0][0][0] = 1;
+		assert(c[0][0][0] > 0);
+	}
+}
+// ----
+// Warning: (92-102): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (120-130): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (138-160): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_branches_1d.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool b, uint[] memory c) public {
+		c[0] = 0;
+		if (b)
+			c[0] = 1;
+		else
+			c[0] = 2;
+		assert(c[0] > 0);
+	}
+}
+// ----
+// Warning: (47-168): Function state mutability can be restricted to pure

test/libsolidity/smtCheckerTests/types/array_branches_2d.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][] c;
+	function f(bool b) public {
+		c[0][0] = 0;
+		if (b)
+			c[0][0] = 1;
+		else
+			c[0][0] = 2;
+		assert(c[0][0] > 0);
+	}
+}
+// ----
+// Warning: (90-97): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (115-122): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (138-145): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (153-172): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_branches_3d.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][][] c;
+	function f(bool b) public {
+		c[0][0][0] = 0;
+		if (b)
+			c[0][0][0] = 1;
+		else
+			c[0][0][0] = 2;
+		assert(c[0][0][0] > 0);
+	}
+}
+// ----
+// Warning: (92-102): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (120-130): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (146-156): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (164-186): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	struct S { uint[][] a; }
+	function f(bool b) public pure {
+		S[] memory c;
+		c[0].a[0][0] = 0;
+		if (b)
+			c[0].a[0][0] = 1;
+		else
+			c[0].a[0][0] = 2;
+		assert(c[0].a[0][0] > 0);
+	}
+}
+// ----
+// Warning: (124-130): Assertion checker does not yet support this expression.
+// Warning: (124-128): Assertion checker does not yet implement this type.
+// Warning: (124-133): Assertion checker does not yet implement this expression.
+// Warning: (124-136): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (154-160): Assertion checker does not yet support this expression.
+// Warning: (154-158): Assertion checker does not yet implement this type.
+// Warning: (154-163): Assertion checker does not yet implement this expression.
+// Warning: (154-166): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (182-188): Assertion checker does not yet support this expression.
+// Warning: (182-186): Assertion checker does not yet implement this type.
+// Warning: (182-191): Assertion checker does not yet implement this expression.
+// Warning: (182-194): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (209-215): Assertion checker does not yet support this expression.
+// Warning: (209-213): Assertion checker does not yet implement this type.
+// Warning: (209-218): Assertion checker does not yet implement this expression.
+// Warning: (202-226): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	struct S { uint[] a; }
+	function f(bool b) public {
+		S memory c;
+		c.a[0] = 0;
+		if (b)
+			c.a[0] = 1;
+		else
+			c.a[0] = 2;
+		assert(c.a[0] > 0);
+	}
+}
+// ----
+// Warning: (71-197): Function state mutability can be restricted to pure
+// Warning: (101-111): Assertion checker does not yet support the type of this variable.
+// Warning: (115-118): Assertion checker does not yet support this expression.
+// Warning: (115-121): Assertion checker does not yet implement this expression.
+// Warning: (115-121): Assertion checker does not yet implement this expression.
+// Warning: (139-142): Assertion checker does not yet support this expression.
+// Warning: (139-145): Assertion checker does not yet implement this expression.
+// Warning: (139-145): Assertion checker does not yet implement this expression.
+// Warning: (161-164): Assertion checker does not yet support this expression.
+// Warning: (161-167): Assertion checker does not yet implement this expression.
+// Warning: (161-167): Assertion checker does not yet implement this expression.
+// Warning: (182-185): Assertion checker does not yet support this expression.
+// Warning: (182-188): Assertion checker does not yet implement this expression.
+// Warning: (175-193): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	struct S { uint[][] a; }
+	function f(bool b) public {
+		S memory c;
+		c.a[0][0] = 0;
+		if (b)
+			c.a[0][0] = 1;
+		else
+			c.a[0][0] = 2;
+		assert(c.a[0][0] > 0);
+	}
+}
+// ----
+// Warning: (73-211): Function state mutability can be restricted to pure
+// Warning: (103-113): Assertion checker does not yet support the type of this variable.
+// Warning: (117-120): Assertion checker does not yet support this expression.
+// Warning: (117-123): Assertion checker does not yet implement this expression.
+// Warning: (117-126): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (144-147): Assertion checker does not yet support this expression.
+// Warning: (144-150): Assertion checker does not yet implement this expression.
+// Warning: (144-153): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (169-172): Assertion checker does not yet support this expression.
+// Warning: (169-175): Assertion checker does not yet implement this expression.
+// Warning: (169-178): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (193-196): Assertion checker does not yet support this expression.
+// Warning: (193-199): Assertion checker does not yet implement this expression.
+// Warning: (186-207): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	struct S { uint[][][] a; }
+	function f(bool b) public pure {
+		S memory c;
+		c.a[0][0][0] = 0;
+		if (b)
+			c.a[0][0][0] = 1;
+		else
+			c.a[0][0][0] = 2;
+		assert(c.a[0][0][0] > 0);
+	}
+}
+// ----
+// Warning: (110-120): Assertion checker does not yet support the type of this variable.
+// Warning: (124-127): Assertion checker does not yet support this expression.
+// Warning: (124-130): Assertion checker does not yet implement this expression.
+// Warning: (124-136): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (154-157): Assertion checker does not yet support this expression.
+// Warning: (154-160): Assertion checker does not yet implement this expression.
+// Warning: (154-166): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (182-185): Assertion checker does not yet support this expression.
+// Warning: (182-188): Assertion checker does not yet implement this expression.
+// Warning: (182-194): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays.
+// Warning: (209-212): Assertion checker does not yet support this expression.
+// Warning: (209-215): Assertion checker does not yet implement this expression.
+// Warning: (202-226): Assertion violation happens here