[SMTChecker] Clear state knowledge after external function calls

7 files changed, 93 insertions, 12 deletions

diff --git a/Changelog.md b/Changelog.md
index d3bb8e10..53097159 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -7,6 +7,7 @@ Language Features:
 Compiler Features:
  * Control Flow Graph: Warn about unreachable code.
  * SMTChecker: Support basic typecasts without truncation.
+ * SMTChecker: Support external function calls and erase all knowledge regarding storage variables and references.
 
 
 Bugfixes:
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 38715289..500b610f 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -418,6 +418,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::Internal:
 		inlineFunctionCall(_funCall);
 		break;
+	case FunctionType::Kind::External:
+		resetStateVariables();
+		resetStorageReferences();
+		break;
 	case FunctionType::Kind::KECCAK256:
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
@@ -1194,25 +1198,35 @@ void SMTChecker::removeLocalVariables()
 	}
 }
 
+void SMTChecker::resetVariable(VariableDeclaration const& _variable)
+{
+	newValue(_variable);
+	setUnknownValue(_variable);
+}
+
 void SMTChecker::resetStateVariables()
 {
-	for (auto const& variable: m_variables)
-	{
-		if (variable.first->isStateVariable())
-		{
-			newValue(*variable.first);
-			setUnknownValue(*variable.first);
-		}
-	}
+	resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); });
+}
+
+void SMTChecker::resetStorageReferences()
+{
+	resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
 }
 
 void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables)
 {
 	for (auto const* decl: _variables)
+		resetVariable(*decl);
+}
+
+void SMTChecker::resetVariables(function<bool(VariableDeclaration const&)> const& _filter)
+{
+	for_each(begin(m_variables), end(m_variables), [&](auto _variable)
 	{
-		newValue(*decl);
-		setUnknownValue(*decl);
-	}
+		if (_filter(*_variable.first))
+			this->resetVariable(*_variable.first);
+	});
 }
 
 void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index caa83764..a85933c8 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -147,8 +147,11 @@ private:
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector<smt::Expression> const& _callArgs);
+	void resetVariable(VariableDeclaration const& _variable);
 	void resetStateVariables();
+	void resetStorageReferences();
 	void resetVariables(std::vector<VariableDeclaration const*> _variables);
+	void resetVariables(std::function<bool(VariableDeclaration const&)> const& _filter);
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables
 	/// using the branch condition as guard.
diff --git a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol
index b4260224..0ceb3b46 100644
--- a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol
+++ b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol
@@ -9,5 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (99-107): Assertion checker does not yet implement this type of function call.
 // Warning: (141-144): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
new file mode 100644
index 00000000..16482e7a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract D
+{
+	function g(uint x) public;
+}
+
+contract C
+{
+	uint x;
+	function f(uint y, D d) public {
+		require(x == y);
+		assert(x == y);
+		d.g(y);
+		// Storage knowledge is cleared after an external call.
+		assert(x == y);
+	}
+}
+// ----
+// Warning: (119-122): Assertion checker does not yet support the type of this variable.
+// Warning: (240-254): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
new file mode 100644
index 00000000..1e704c9d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract D
+{
+	function g(uint x) public;
+}
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint y, D d) public {
+		require(map[0] == map[1]);
+		assert(map[0] == map[1]);
+		d.g(y);
+		// Storage knowledge is cleared after an external call.
+		assert(map[0] == map[1]);
+	}
+}
+// ----
+// Warning: (139-142): Assertion checker does not yet support the type of this variable.
+// Warning: (280-304): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol
new file mode 100644
index 00000000..dd36ec73
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract D
+{
+	function g(uint x) public;
+}
+
+contract C
+{
+	mapping (uint => uint) storageMap;
+	function f(uint y, D d) public {
+		mapping (uint => uint) storage map = storageMap;
+		require(map[0] == map[1]);
+		assert(map[0] == map[1]);
+		d.g(y);
+		// Storage knowledge is cleared after an external call.
+		assert(map[0] == map[1]);
+	}
+}
+// ----
+// Warning: (146-149): Assertion checker does not yet support the type of this variable.
+// Warning: (338-362): Assertion violation happens here