Merge pull request #9069 from ethereum/smt_try

[SMTChecker] Fix internal error on try/catch

Changelog.md

@@ -29,6 +29,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables.
  * SMTChecker: Fix internal error when short circuiting Boolean expressions with function calls in state variable initialization.
  * SMTChecker: Fix internal error when assigning to index access inside branches.
+ * SMTChecker: Fix internal error on try/catch clauses with parameters.
 
 ### 0.6.8 (2020-05-14)
 

libsolidity/formal/SMTEncoder.cpp

@@ -274,6 +274,20 @@ 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;
+}
+
 bool SMTEncoder::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);

libsolidity/formal/SMTEncoder.h

@@ -91,6 +91,7 @@ protected:
 	bool visit(InlineAssembly const& _node) override;
 	void endVisit(Break const&) override {}
 	void endVisit(Continue const&) override {}
+	bool visit(TryCatchClause const& _node) override;
 
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.

test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+	function g() public returns (uint) {
+		try this.g() returns (uint x) { x; }
+		catch Error(string memory s) { s; }
+	}
+}
+// ====
+// EVMVersion: >=byzantium
+// ----
+// Warning: (98-121): Assertion checker does not support try/catch clauses.
+// Warning: (124-159): Assertion checker does not support try/catch clauses.

test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public {
+		try this.f() {}
+		catch (bytes memory x) {
+			x;
+		}
+	}
+}
+// ====
+// EVMVersion: >=byzantium
+// ----
+// Warning: (83-85): Assertion checker does not support try/catch clauses.
+// Warning: (88-122): Assertion checker does not support try/catch clauses.