From c8c17b693b47ddbfa4fe016bafbc82b7262c938b Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Sat, 12 Sep 2020 12:22:03 +0100
Subject: [PATCH] [SMTChecker] Support events and low-level logs

---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             |  8 ++++
 .../smtCheckerTests/special/event.sol         | 28 +++++++++++++
 .../smtCheckerTests/special/log.sol           | 39 +++++++++++++++++++
 4 files changed, 76 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/special/event.sol
 create mode 100644 test/libsolidity/smtCheckerTests/special/log.sol

diff --git a/Changelog.md b/Changelog.md
index b6643af58..904a7859a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * Export compiler-generated utility sources via standard-json or combined-json.
+ * SMTChecker: Support events and low-level logs.
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
  * SMTChecker: Support structs.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index f8a8893bd..cb7322d62 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -676,6 +676,14 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ArrayPop:
 		arrayPop(_funCall);
 		break;
+	case FunctionType::Kind::Log0:
+	case FunctionType::Kind::Log1:
+	case FunctionType::Kind::Log2:
+	case FunctionType::Kind::Log3:
+	case FunctionType::Kind::Log4:
+	case FunctionType::Kind::Event:
+		// These can be safely ignored.
+		break;
 	default:
 		m_errorReporter.warning(
 			4588_error,
diff --git a/test/libsolidity/smtCheckerTests/special/event.sol b/test/libsolidity/smtCheckerTests/special/event.sol
new file mode 100644
index 000000000..c3e45c30e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/event.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+	event Nudge();
+	event SomeArgs(uint, uint);
+	event Caller(address, uint);
+	function f() payable external {
+		emit Nudge();
+		emit SomeArgs(134, 567);
+		emit Caller(msg.sender, msg.value);
+	}
+	function g_data() pure internal returns (uint) {
+		assert(true);
+	}
+	function g() external {
+		emit SomeArgs(g_data(), g_data());
+	}
+	bool x = true;
+	function h_data() view internal returns (uint) {
+		assert(x);
+	}
+	function h() external {
+		x = false;
+		emit SomeArgs(h_data(), h_data());
+	}
+}
+// ----
+// Warning 6328: (440-449): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/special/log.sol b/test/libsolidity/smtCheckerTests/special/log.sol
new file mode 100644
index 000000000..a9d6fcc08
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/log.sol
@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() external {
+		bytes32 t1 = bytes32(uint256(0x1234));
+		log0(t1);
+		log1(t1, t1);
+		log2(t1, t1, t1);
+		log3(t1, t1, t1, t1);
+		log4(t1, t1, t1, t1, t1);
+	}
+	function g_data() pure internal returns (bytes32) {
+		assert(true);
+		return bytes32(uint256(0x5678));
+	}
+	function g() external {
+		// To test that the function call is actually visited.
+		log0(g_data());
+		log1(g_data(), g_data());
+		log2(g_data(), g_data(), g_data());
+		log3(g_data(), g_data(), g_data(), g_data());
+		log4(g_data(), g_data(), g_data(), g_data(), g_data());
+	}
+	bool x = true;
+	function h_data() view internal returns (bytes32) {
+		assert(x);
+	}
+	function h() external {
+		// To test that the function call is actually visited.
+		x = false;
+		log0(h_data());
+		log1(h_data(), h_data());
+		log2(h_data(), h_data(), h_data());
+		log3(h_data(), h_data(), h_data(), h_data());
+		log4(h_data(), h_data(), h_data(), h_data(), h_data());
+	}
+}
+// ----
+// Warning 6328: (668-677): Assertion violation happens here.