[SMTChecker] Support try-catch in CHC engine

libsolidity/formal/CHC.cpp

@@ -541,6 +541,74 @@ void CHC::endVisit(Return const& _return)
 	m_currentBlock = predicate(*returnGhost);
 }
 
+bool CHC::visit(TryStatement const& _tryStatement)
+{
+	FunctionCall const* externalCall = dynamic_cast<FunctionCall const*>(&_tryStatement.externalCall());
+	solAssert(externalCall && externalCall->annotation().tryCall, "");
+	solAssert(m_currentFunction, "");
+
+	auto tryHeaderBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_header_");
+	auto tryAfterCallSuccessBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_after_call_success_");
+	auto tryAfterCallFailBlock = createBlock(&_tryStatement, PredicateType::FunctionBlock, "try_after_call_fail_");
+	auto afterTryBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock);
+
+	connectBlocks(m_currentBlock, predicate(*tryHeaderBlock));
+	setCurrentBlock(*tryHeaderBlock);
+	// fine-grained control over how the external call is visited
+	// cannot use "_tryStatement.externalCall().accept(*this);" since we need to insert the "connectBlocks"
+	// visit(*externalCall); currently there is nothing to do here, so it's commented out
+	externalCall->expression().accept(*this);
+	ASTNode::listAccept(externalCall->arguments(), *this);
+	connectBlocks(m_currentBlock, predicate(*tryAfterCallFailBlock));
+	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));
+	}
+
+	connectBlocks(m_currentBlock, predicate(*tryAfterCallSuccessBlock));
+
+	auto const& clauses = _tryStatement.clauses();
+	solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause");
+	auto clauseBlocks = applyMap(clauses, [this](ASTPointer<TryCatchClause> clause) {
+		return createBlock(clause.get(), PredicateType::FunctionBlock, "try_clause_" + std::to_string(clause->id()));
+	});
+
+	setCurrentBlock(*tryAfterCallSuccessBlock);
+	connectBlocks(m_currentBlock, predicate(*clauseBlocks[0]));
+
+	setCurrentBlock(*tryAfterCallFailBlock);
+	for (size_t i = 1; i < clauseBlocks.size(); ++i)
+		connectBlocks(m_currentBlock, predicate(*clauseBlocks[i]));
+
+	for (size_t i = 0; i < clauses.size(); ++i)
+	{
+		setCurrentBlock(*clauseBlocks[i]);
+		clauses[i]->accept(*this);
+		connectBlocks(m_currentBlock, predicate(*afterTryBlock));
+	}
+	setCurrentBlock(*afterTryBlock);
+
+	return false;
+}
+
 void CHC::pushInlineFrame(CallableDeclaration const& _callable)
 {
 	m_returnDests.push_back(createBlock(&_callable, PredicateType::FunctionBlock, "return_"));

libsolidity/formal/CHC.h

@@ -84,6 +84,7 @@ private:
 	void endVisit(Continue const& _node) override;
 	void endVisit(IndexRangeAccess const& _node) override;
 	void endVisit(Return const& _node) override;
+	bool visit(TryStatement const& _node) override;
 
 	void pushInlineFrame(CallableDeclaration const& _callable) override;
 	void popInlineFrame(CallableDeclaration const& _callable) override;

libsolidity/formal/SMTEncoder.cpp

@@ -312,20 +312,6 @@ bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
 	return false;
 }
 
-bool SMTEncoder::visit(TryCatchClause const& _clause)
-{
-	if (auto params = _clause.parameters())
-		for (auto const& var: params->parameters())
-			createVariable(*var);
-
-	m_errorReporter.warning(
-		7645_error,
-		_clause.location(),
-		"Assertion checker does not support try/catch clauses."
-	);
-	return false;
-}
-
 void SMTEncoder::pushInlineFrame(CallableDeclaration const&)
 {
 	pushPathCondition(currentPathConditions());
@@ -2688,7 +2674,29 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
 
 vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
 {
-	return _function.localVariables() + modifiersVariables(_function, _contract);
+	return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract);
+}
+
+vector<VariableDeclaration const*> SMTEncoder::tryCatchVariables(FunctionDefinition const& _function)
+{
+	struct TryCatchVarsVisitor : public ASTConstVisitor
+	{
+		bool visit(TryCatchClause const& _catchClause) override
+		{
+			if (_catchClause.parameters())
+			{
+				auto const& params = _catchClause.parameters()->parameters();
+				for (auto param: params)
+					vars.push_back(param.get());
+			}
+
+			return false;
+		}
+
+		vector<VariableDeclaration const*> vars;
+	} tryCatchVarsVisitor;
+	_function.accept(tryCatchVarsVisitor);
+	return tryCatchVarsVisitor.vars;
 }
 
 vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract)

libsolidity/formal/SMTEncoder.h

@@ -76,6 +76,7 @@ public:
 
 	static std::vector<VariableDeclaration const*> localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract);
 	static std::vector<VariableDeclaration const*> modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract);
+	static std::vector<VariableDeclaration const*> tryCatchVariables(FunctionDefinition const& _function);
 
 	/// @returns the ModifierDefinition of a ModifierInvocation if possible, or nullptr.
 	static ModifierDefinition const* resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract);
@@ -130,7 +131,7 @@ protected:
 	bool visit(InlineAssembly const& _node) override;
 	void endVisit(Break const&) override {}
 	void endVisit(Continue const&) override {}
-	bool visit(TryCatchClause const& _node) override;
+	bool visit(TryStatement const&) override { return false; }
 
 	virtual void pushInlineFrame(CallableDeclaration const&);
 	virtual void popInlineFrame(CallableDeclaration const&);