Merge pull request #9891 from ethereum/smt-string-literals

[SMTChecker] Keep knowledge about string literals

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, even through assignment, and thus support the ``.length`` property properly.
  * SMTChecker: Support events and low-level logs.
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.

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(
@@ -1677,9 +1690,7 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression con
 	// This is a special case where the SMT sorts are different.
 	// For now we are unaware of other cases where this happens, but if they do appear
 	// we should extract this into an `implicitConversion` function.
-	if (_variable.type()->category() != Type::Category::Array || _value.annotation().type->category() != Type::Category::StringLiteral)
+	assignment(_variable, expr(_value, _variable.type()));
-		assignment(_variable, expr(_value, _variable.type()));
-	// TODO else { store each string literal byte into the array }
 }
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)

test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol

@@ -1,8 +1,13 @@
 pragma experimental SMTChecker;
+
 contract C {
-    bytes20 x;
+    function f(uint i) public pure {
-    function f(bytes16 b) public view {
+        bytes memory x = hex"00112233";
-        b[uint8(x[2])];
+        assert(x[0] == 0x00);
+        assert(x[1] == 0x11);
+        require(i > 3);
+        assert(x[i] == 0x00);
     }
 }
 // ----
+// Warning 6328: (215-235): Assertion violation happens here.

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])];
+    }
+}
+// ----

test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol

@@ -0,0 +1,14 @@
+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: (248-268): Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/bytes_length.sol

@@ -0,0 +1,13 @@
+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);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/types/string_length.sol

@@ -0,0 +1,18 @@
+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);
+	}
+}
+// ----