[SMTChecker] Fixing conversion from StringLiteral to FixedBytes

Changelog.md

@@ -18,6 +18,7 @@ Bugfixes:
  * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals.
  * SMTChecker: Fix internal error when trying to generate counterexamples with old z3.
  * SMTChecker: Fix segmentation fault that could occur on certain SMT-enabled sources when no SMT solver was available.
+ * SMTChecker: Fix cast string literals to byte arrays.
  * Type Checker: ``super`` is not available in libraries.
  * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser.
  * Yul Optimizer: Removed NameSimplifier from optimization steps available to users.

libsolidity/formal/SMTEncoder.cpp

@@ -959,16 +959,21 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 	solAssert(_funCall.arguments().size() == 1, "");
 
 	auto argument = _funCall.arguments().front();
-	auto const& argType = argument->annotation().type;
+	auto const argType = argument->annotation().type;
+	auto const funCallType = _funCall.annotation().type;
 
-	unsigned argSize = argument->annotation().type->storageBytes();
-	unsigned castSize = _funCall.annotation().type->storageBytes();
+	auto symbArg = expr(*argument, funCallType);
 
-	auto const& funCallType = _funCall.annotation().type;
+	if (smt::isStringLiteral(*argType) && smt::isFixedBytes(*funCallType))
+	{
+		defineExpr(_funCall, symbArg);
+		return;
+	}
 
 	// TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed.
 
-	auto symbArg = expr(*argument, funCallType);
+	unsigned argSize = argType->storageBytes();
+	unsigned castSize = funCallType->storageBytes();
 	bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType);
 	bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType);
 	optional<smtutil::Expression> symbMin;
@@ -1112,7 +1117,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
 
 		addArrayLiteralAssertions(
 			*symbArray,
-			applyMap(_literal.value(), [&](auto const& c) { return smtutil::Expression{size_t(c)}; })
+			applyMap(_literal.value(), [](unsigned char c) { return smtutil::Expression{size_t(c)}; })
 		);
 	}
 	else

libsolidity/formal/SymbolicTypes.cpp

@@ -566,11 +566,13 @@ optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePoin
 		// but they can also be compared/assigned to fixed bytes, in which
 		// case they'd need to be encoded as numbers.
 		if (auto strType = dynamic_cast<StringLiteralType const*>(_from))
-			if (_to->category() == frontend::Type::Category::FixedBytes)
+			if (auto fixedBytesType = dynamic_cast<FixedBytesType const*>(_to))
 			{
 				if (strType->value().empty())
 					return smtutil::Expression(size_t(0));
-				return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
+				auto bytesVec = util::asBytes(strType->value());
+				bytesVec.resize(fixedBytesType->numBytes(), 0);
+				return smtutil::Expression(u256(toHex(bytesVec, util::HexPrefix::Add)));
 			}
 
 	return std::nullopt;

test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol

@@ -1,7 +1,11 @@
 pragma experimental SMTChecker;
 contract C {
-  function f() public pure returns (byte) {
-    return (byte("") & (""));
-  }
+	function f() public pure {
+		assert(byte("") & ("") == byte(0)); // should hold
+		assert(byte(0xAA) & byte(0x55) == byte(0)); // should hold
+		assert(byte(0xFF) & byte(0xAA) == byte(0xAA)); // should hold
+		assert(byte(0xFF) & byte(0xAA) == byte(0)); // should fail
+	}
 }
 // ----
+// Warning 6328: (253-295): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (175-198): CHC: Assertion violation happens here.
+// Warning 6328: (133-156): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/bitwise_or_fixed_bytes.sol

@@ -1,7 +1,11 @@
 pragma experimental SMTChecker;
 contract C {
-  function f() public pure returns (byte) {
-    return (byte(0x0F) | (byte(0xF0)));
-  }
+	function f() public pure returns (byte) {
+		byte b = (byte(0x0F) | (byte(0xF0)));
+		assert(b == byte(0xFF)); // should hold
+		assert(b == byte(0x00)); // should fail
+		return b;
+	}
 }
 // ----
+// Warning 6328: (172-195): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol

@@ -1,8 +1,11 @@
 pragma experimental SMTChecker;
 contract Simp {
-    function f3() public pure returns (byte) {
-        bytes memory y = "def";
-        return y[0] ^ "e";
-    }
+	function f3() public pure returns (byte) {
+		bytes memory y = "def";
+		assert(y[0] ^ "e" != byte(0)); // should hold
+		assert(y[1] ^ "e" != byte(0)); // should fail
+		return y[0];
+	}
 }
 // ----
+// Warning 6328: (168-197): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/typecast/string_literal_to_dynamic_bytes.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		bytes memory b = bytes(hex"ffff");
+		assert(b.length == 2); // should hold
+		assert(b[0] == byte(uint8(255))); // should hold
+		assert(b[1] == byte(uint8(100))); // should fail
+	}
+}
+// ----
+// Warning 6328: (204-236): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_upcast.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(bytes4(hex"0000ffff") == bytes4(hex"ffff")); // should fail
+		assert(bytes4(hex"ffff0000") == bytes4(hex"ffff")); // should hold
+	}
+}
+// ----
+// Warning 6328: (76-126): CHC: Assertion violation happens here.