From dd43ce15781be3040fe9fd51462cdde09414bae6 Mon Sep 17 00:00:00 2001
From: Martin Blicha <blichm@usi.ch>
Date: Sat, 9 Jan 2021 16:35:21 +0100
Subject: [PATCH] fixing try/catch encoding for BMC, refactoring

---
 libsolidity/formal/BMC.cpp        | 12 +++++++++---
 libsolidity/formal/CHC.cpp        | 21 ++-------------------
 libsolidity/formal/SMTEncoder.cpp | 20 ++++++++++++++++++++
 libsolidity/formal/SMTEncoder.h   |  2 ++
 4 files changed, 33 insertions(+), 22 deletions(-)

diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 156d514d5..0d1364bce 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -352,23 +352,29 @@ bool BMC::visit(TryStatement const& _tryStatement)
 
 	externalCall->accept(*this);
 	auto callExpr = expr(*externalCall);
-	smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort);
+	if (_tryStatement.successClause()->parameters())
+		tryCatchAssignment(
+			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall));
 
+	smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort);
 	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(), clauseId == 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 - 1), clausesVisitResults[i - 1].first, clausesVisitResults[i].first);
+		mergeVariables(touchedVars[i - 1] + touchedVars[i], clauseId == i, clausesVisitResults[i].first, currentIndices);
+		currentIndices = copyVariableIndices();
 		pathCondition = pathCondition || clausesVisitResults[i].second;
 	}
 	setPathCondition(pathCondition);
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 6257adb7f..0795189b8 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -563,25 +563,8 @@ bool CHC::visit(TryStatement const& _tryStatement)
 	endVisit(*externalCall);
 
 	if (_tryStatement.successClause()->parameters())
-	{
-		auto const& params = _tryStatement.successClause()->parameters()->parameters();
-		if (params.size() > 1)
-		{
-			auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*externalCall));
-			solAssert(symbTuple, "");
-			auto const& symbComponents = symbTuple->components();
-			solAssert(symbComponents.size() == params.size(), "");
-			for (unsigned i = 0; i < symbComponents.size(); ++i)
-			{
-				auto param = params.at(i);
-				solAssert(param, "");
-				solAssert(m_context.knownVariable(*param), "");
-				assignment(*param, symbTuple->component(i));
-			}
-		}
-		else if (params.size() == 1)
-			assignment(*params.front(), expr(*externalCall));
-	}
+		tryCatchAssignment(
+			_tryStatement.successClause()->parameters()->parameters(), *m_context.expression(*externalCall));
 
 	connectBlocks(m_currentBlock, predicate(*tryAfterCallSuccessBlock));
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index c9faf08b3..2e73a418f 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2107,6 +2107,26 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
 	return values.first;
 }
 
+void SMTEncoder::tryCatchAssignment(vector<shared_ptr<VariableDeclaration>> const& _variables, smt::SymbolicVariable const& _rhs)
+{
+	if (_variables.size() > 1)
+	{
+		auto const* symbTuple = dynamic_cast<smt::SymbolicTupleVariable const*>(&_rhs);
+		solAssert(symbTuple, "");
+		auto const& symbComponents = symbTuple->components();
+		solAssert(symbComponents.size() == _variables.size(), "");
+		for (unsigned i = 0; i < symbComponents.size(); ++i)
+		{
+			auto param = _variables.at(i);
+			solAssert(param, "");
+			solAssert(m_context.knownVariable(*param), "");
+			assignment(*param, symbTuple->component(i));
+		}
+	}
+	else if (_variables.size() == 1)
+		assignment(*_variables.front(), _rhs.currentValue());
+}
+
 void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
 {
 	// In general, at this point, the SMT sorts of _variable and _value are the same,
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index bc7b360c3..bc0a9482a 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -238,6 +238,8 @@ protected:
 	void tupleAssignment(Expression const& _left, Expression const& _right);
 	/// Computes the right hand side of a compound assignment.
 	smtutil::Expression compoundAssignment(Assignment const& _assignment);
+	/// Handles assignment of the result of external call in try statement to the parameters of success clause
+	void tryCatchAssignment(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, smt::SymbolicVariable const& rhs);
 
 	/// Maps a variable to an SSA index.
 	using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;