Merge pull request #11188 from blishko/issue-11181

[SMTChecker] Fix crash when analysing try-catch clauses with function call.

Changelog.md

@@ -20,6 +20,7 @@ Bugfixes:
  * SMTChecker: Fix false positive and false negative on ``push`` as LHS of a compound assignment.
  * SMTChecker: Fix false positive in contracts that cannot be deployed.
  * SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available.
+ * SMTChecker: Fix internal error on try-catch with function call in catch block.
 
 
 AST Changes:

libsolidity/formal/BMC.cpp

@@ -208,22 +208,18 @@ bool BMC::visit(IfStatement const& _node)
 	auto conditionExpr = expr(_node.condition());
 	// visit true branch
 	auto [indicesEndTrue, trueEndPathCondition] = visitBranch(&_node.trueStatement(), conditionExpr);
-	auto touchedVars = touchedVariables(_node.trueStatement());
 
 	// visit false branch
 	decltype(indicesEndTrue) indicesEndFalse;
 	auto falseEndPathCondition = currentPathConditions() && !conditionExpr;
 	if (_node.falseStatement())
-	{
 		std::tie(indicesEndFalse, falseEndPathCondition) = visitBranch(_node.falseStatement(), !conditionExpr);
-		touchedVars += touchedVariables(*_node.falseStatement());
-	}
 	else
 		indicesEndFalse = copyVariableIndices();
 
 	// merge the information from branches
 	setPathCondition(trueEndPathCondition || falseEndPathCondition);
-	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
+	mergeVariables(expr(_node.condition()), indicesEndTrue, indicesEndFalse);
 
 	return false;
 }
@@ -258,8 +254,7 @@ bool BMC::visit(Conditional const& _op)
 bool BMC::visit(WhileStatement const& _node)
 {
 	auto indicesBeforeLoop = copyVariableIndices();
-	auto touchedVars = touchedVariables(_node);
+	m_context.resetVariables(touchedVariables(_node));
-	m_context.resetVariables(touchedVars);
 	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
@@ -294,7 +289,7 @@ bool BMC::visit(WhileStatement const& _node)
 	if (!_node.isDoWhile())
 		_node.condition().accept(*this);
 
-	mergeVariables(touchedVars, expr(_node.condition()), indicesAfterLoop, copyVariableIndices());
+	mergeVariables(expr(_node.condition()), indicesAfterLoop, copyVariableIndices());
 
 	m_loopExecutionHappened = true;
 	return false;
@@ -344,7 +339,7 @@ bool BMC::visit(ForStatement const& _node)
 		_node.condition()->accept(*this);
 
 	auto forCondition = _node.condition() ? expr(*_node.condition()) : smtutil::Expression(true);
-	mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices());
+	mergeVariables(forCondition, indicesAfterLoop, copyVariableIndices());
 
 	m_loopExecutionHappened = true;
 	return false;
@@ -363,20 +358,16 @@ bool BMC::visit(TryStatement const& _tryStatement)
 	auto const& clauses = _tryStatement.clauses();
 	m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size());
 	solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause");
-	vector<set<VariableDeclaration const*>> touchedVars;
 	vector<pair<VariableIndices, smtutil::Expression>> clausesVisitResults;
 	for (size_t i = 0; i < clauses.size(); ++i)
-	{
 		clausesVisitResults.push_back(visitBranch(clauses[i].get()));
-		touchedVars.push_back(touchedVariables(*clauses[i]));
-	}
 
 	// merge the information from all clauses
 	smtutil::Expression pathCondition = clausesVisitResults.front().second;
 	auto currentIndices = clausesVisitResults[0].first;
 	for (size_t i = 1; i < clauses.size(); ++i)
 	{
-		mergeVariables(touchedVars[i - 1] + touchedVars[i], clauseId == i, clausesVisitResults[i].first, currentIndices);
+		mergeVariables(clauseId == i, clausesVisitResults[i].first, currentIndices);
 		currentIndices = copyVariableIndices();
 		pathCondition = pathCondition || clausesVisitResults[i].second;
 	}

libsolidity/formal/SMTEncoder.cpp

@@ -600,12 +600,10 @@ bool SMTEncoder::visit(Conditional const& _op)
 	_op.condition().accept(*this);
 
 	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition())).first;
-	auto touchedVars = touchedVariables(_op.trueExpression());
 
 	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition())).first;
-	touchedVars += touchedVariables(_op.falseExpression());
 
-	mergeVariables(touchedVars, expr(_op.condition()), indicesEndTrue, indicesEndFalse);
+	mergeVariables(expr(_op.condition()), indicesEndTrue, indicesEndFalse);
 
 	defineExpr(_op, smtutil::Expression::ite(
 		expr(_op.condition()),
@@ -1916,13 +1914,13 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
 	if (_op.getOperator() == Token::And)
 	{
 		auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
-		mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
+		mergeVariables(!expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 		defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
 	}
 	else
 	{
 		auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
-		mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
+		mergeVariables(expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 		defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
 	}
 }
@@ -2347,38 +2345,20 @@ Type const* SMTEncoder::typeWithoutPointer(Type const* _type)
 	return _type;
 }
 
-void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
+void SMTEncoder::mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
 {
-	auto cmp = [] (VariableDeclaration const* var1, VariableDeclaration const* var2) {
+	for (auto const& entry: _indicesEndTrue)
-		return var1->id() < var2->id();
-	};
-	set<VariableDeclaration const*, decltype(cmp)> sortedVars(begin(_variables), end(_variables), cmp);
-
-	/// Knowledge about references is erased if a reference is assigned,
-	/// so those also need their SSA's merged.
-	/// This does not cause scope harm since the symbolic variables
-	/// are kept alive.
-	for (auto const& var: _indicesEndTrue)
 	{
-		solAssert(_indicesEndFalse.count(var.first), "");
+		VariableDeclaration const* var = entry.first;
-		if (
+		auto trueIndex = entry.second;
-			_indicesEndFalse.at(var.first) != var.second &&
+		if (_indicesEndFalse.count(var) && _indicesEndFalse.at(var) != trueIndex)
-			!sortedVars.count(var.first)
+		{
-		)
+			m_context.addAssertion(m_context.newValue(*var) == smtutil::Expression::ite(
-			sortedVars.insert(var.first);
+				_condition,
-	}
+				valueAtIndex(*var, trueIndex),
-
+				valueAtIndex(*var, _indicesEndFalse.at(var)))
-	for (auto const* decl: sortedVars)
+			);
-	{
+		}
-		solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), "");
-		auto trueIndex = static_cast<unsigned>(_indicesEndTrue.at(decl));
-		auto falseIndex = static_cast<unsigned>(_indicesEndFalse.at(decl));
-		solAssert(trueIndex != falseIndex, "");
-		m_context.addAssertion(m_context.newValue(*decl) == smtutil::Expression::ite(
-			_condition,
-			valueAtIndex(*decl, trueIndex),
-			valueAtIndex(*decl, falseIndex))
-		);
 	}
 }
 
@@ -2555,7 +2535,7 @@ SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
 void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 {
 	for (auto const& var: _indices)
-		m_context.variable(*var.first)->setIndex(static_cast<unsigned>(var.second));
+		m_context.variable(*var.first)->setIndex(var.second);
 }
 
 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)

libsolidity/formal/SMTEncoder.h

@@ -266,7 +266,7 @@ protected:
 	void expressionToTupleAssignment(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs);
 
 	/// Maps a variable to an SSA index.
-	using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
+	using VariableIndices = std::unordered_map<VariableDeclaration const*, unsigned>;
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
@@ -295,10 +295,9 @@ protected:
 	/// @returns whether _a or a subtype of _a is the same as _b.
 	bool sameTypeOrSubtype(Type const* _a, Type const* _b);
 
-	/// Given two different branches and the touched variables,
+	/// Given the state of the symbolic variables at the end of two different branches,
-	/// merge the touched variables into after-branch ite variables
+	/// create a merged state using the given branch condition.
-	/// using the branch condition as guard.
+	void mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
-	void mergeVariables(std::set<VariableDeclaration const*> const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
 	/// Tries to create an uninitialized variable and returns true on success.
 	bool createVariable(VariableDeclaration const& _varDecl);
 

test/libsolidity/smtCheckerTests/try_catch/try_call_in_catch_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public returns (uint) {
+        try this.f() {
+        } catch Error(string memory) {
+			g();
+		}
+	}
+	function g() public pure returns (address) {
+	}
+}
+// ----
+// Warning 6321: (78-82): 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/try_catch/try_call_in_catch_2.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public returns (uint, uint) {
+        try this.f() {
+        } catch Error(string memory) {
+			g();
+		}
+	}
+	function g() public pure {
+		int test = 1;
+	}
+}
+// ----
+// Warning 6321: (78-82): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
+// Warning 6321: (84-88): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
+// Warning 2072: (199-207): Unused local variable.