From 5090353a1a3be0f26792d5957f55d099ec8de2a8 Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Thu, 24 Sep 2020 12:16:38 +0100
Subject: [PATCH] [SMTChecker] Keep knowledge about string literals

---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             | 13 ++++++++++++
 .../operators/index_access_for_bytes.sol      | 11 +++++++---
 .../operators/index_access_for_bytesNN.sol    |  8 +++++++
 .../operators/index_access_for_string.sol     | 15 +++++++++++++
 .../smtCheckerTests/types/bytes_length.sol    | 14 +++++++++++++
 .../smtCheckerTests/types/string_length.sol   | 21 +++++++++++++++++++
 7 files changed, 80 insertions(+), 3 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/bytes_length.sol
 create mode 100644 test/libsolidity/smtCheckerTests/types/string_length.sol

diff --git a/Changelog.md b/Changelog.md
index 209d65b26..be808276a 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: Keep knowledge about string literals and thus support the ``.length`` property properly.
  * SMTChecker: Support events and low-level logs.
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 32f249b0e..fa6b74399 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -834,7 +834,20 @@ void SMTEncoder::endVisit(Literal const& _literal)
 	else if (smt::isBool(type))
 		defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
 	else if (smt::isStringLiteral(type))
+	{
 		createExpr(_literal);
+
+		// Add constraints for the length and values as it is known.
+		auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_literal));
+		solAssert(symbArray, "");
+
+		auto value = _literal.value();
+		m_context.addAssertion(symbArray->length() == value.length());
+		for (size_t i = 0; i < value.length(); i++)
+			m_context.addAssertion(
+				smtutil::Expression::select(symbArray->elements(), i) == size_t(value[i])
+			);
+	}
 	else
 	{
 		m_errorReporter.warning(
diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
index 65ea05950..ebd97db67 100644
--- a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
+++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
@@ -1,8 +1,13 @@
 pragma experimental SMTChecker;
+
 contract C {
-    bytes20 x;
-    function f(bytes16 b) public view {
-        b[uint8(x[2])];
+    function f(uint i) public pure {
+        bytes memory x = hex"00112233";
+        assert(x[0] == 0x00);
+        assert(x[1] == 0x11);
+        require(i > 3);
+        assert(x[i] == 0x00);
     }
 }
 // ----
+// Warning 6328: (161-181): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol
new file mode 100644
index 000000000..65ea05950
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+    bytes20 x;
+    function f(bytes16 b) public view {
+        b[uint8(x[2])];
+    }
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol
new file mode 100644
index 000000000..93a620f9d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint i) public pure {
+        string memory x = "\x12\x34";
+        bytes memory y = bytes(x);
+        assert(y[0] == 0x12);
+        assert(y[1] == 0x34);
+        require(i > 2);
+        assert(y[i] == 0x00);
+    }
+}
+// ----
+// Warning 6328: (164-184): Assertion violation happens here.
+// Warning 6328: (194-214): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/bytes_length.sol b/test/libsolidity/smtCheckerTests/types/bytes_length.sol
new file mode 100644
index 000000000..4959b170b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/bytes_length.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		bytes memory x = hex"0123";
+		assert(x.length == 2);
+	}
+	function g() public pure {
+		bytes memory x = bytes(hex"0123");
+		assert(x.length == 2);
+	}
+}
+// ----
+// Warning 6328: (106-127): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/string_length.sol b/test/libsolidity/smtCheckerTests/types/string_length.sol
new file mode 100644
index 000000000..5cc8910f0
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/string_length.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		string memory x = "Hello World";
+		assert(bytes(x).length == 11);
+	}
+	function g() public pure {
+		string memory x = unicode"Hello World";
+		assert(bytes(x).length == 11);
+	}
+	function h() public pure {
+		bytes memory x = unicode"Hello World";
+		string memory y = string(x);
+		assert(bytes(y).length == 11);
+	}
+}
+// ----
+// Warning 6328: (111-140): Assertion violation happens here.
+// Warning 6328: (217-246): Assertion violation happens here.
+// Warning 6328: (353-382): Assertion violation happens here.