Fix conversion from bytes to fixed bytes

Changelog.md

@@ -18,6 +18,7 @@ Bugfixes:
  * AST: Do not output value of Yul literal if it is not a valid UTF-8 string.
  * SMTChecker: Fix internal error on struct constructor with fixed bytes member initialized with string literal.
  * SMTChecker: Fix internal error on external calls from the constructor.
+ * SMTChecker: Fix internal error on conversion from ``bytes`` to ``fixed bytes``.
  * Source Locations: Properly set source location of scoped blocks.
  * Standard JSON: Properly allow the ``inliner`` setting under ``settings.optimizer.details``.
  * Type Checker: Fix internal compiler error related to having mapping types in constructor parameter for abstract contracts.

libsolidity/formal/SMTEncoder.cpp

@@ -1022,6 +1022,17 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 		return;
 	}
 
+	ArrayType const* arrayType = dynamic_cast<ArrayType const*>(argType);
+	if (auto sliceType = dynamic_cast<ArraySliceType const*>(argType))
+		arrayType = &sliceType->arrayType();
+
+	if (arrayType && arrayType->isByteArray() && smt::isFixedBytes(*funCallType))
+	{
+		auto array = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*argument));
+		bytesToFixedBytesAssertions(*array, _funCall);
+		return;
+	}
+
 	// TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed.
 
 	unsigned argSize = argType->storageBytes();
@@ -1206,6 +1217,25 @@ void SMTEncoder::addArrayLiteralAssertions(
 		m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]);
 }
 
+void SMTEncoder::bytesToFixedBytesAssertions(
+	smt::SymbolicArrayVariable& _symArray,
+	Expression const& _fixedBytes
+)
+{
+	auto const& fixed = dynamic_cast<FixedBytesType const&>(*_fixedBytes.annotation().type);
+	auto intType = TypeProvider::uint256();
+	string suffix = to_string(_fixedBytes.id()) + "_" + to_string(m_context.newUniqueId());
+	smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context);
+	m_context.addAssertion(k.currentValue() == 0);
+	size_t n = fixed.numBytes();
+	for (size_t i = 0; i < n; i++)
+	{
+		auto kPrev = k.currentValue();
+		m_context.addAssertion((smtutil::Expression::select(_symArray.elements(), i) * (u256(1) << ((n - i - 1) * 8))) + kPrev == k.increaseIndex());
+	}
+	m_context.addAssertion(expr(_fixedBytes) == k.currentValue());
+}
+
 void SMTEncoder::endVisit(Return const& _return)
 {
 	if (_return.expression() && m_context.knownExpression(*_return.expression()))

libsolidity/formal/SMTEncoder.h

@@ -245,6 +245,11 @@ protected:
 		std::vector<smtutil::Expression> const& _elementValues
 	);
 
+	void bytesToFixedBytesAssertions(
+		smt::SymbolicArrayVariable& _symArray,
+		Expression const& _fixedBytes
+	);
+
 	/// @returns a pair of expressions representing _left / _right and _left mod _right, respectively.
 	/// Uses slack variables and additional constraints to express the results using only operations
 	/// more friendly to the SMT solver (multiplication, addition, subtraction and comparison).

test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol

@@ -0,0 +1,22 @@
+contract C {
+	function f() external pure {
+		bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809";
+		bytes8 c = bytes8(b);
+		assert(c == 0x0001020304050607); // should hold
+		assert(c == 0x0001020304050608); // should fail
+		bytes16 d = bytes16(b);
+		assert(d == 0x00010203040506070809000102030405);
+		assert(d == 0x00010203040506070809000102030406); // should fail
+		bytes24 e = bytes24(b);
+		assert(e == 0x000102030405060708090001020304050607080900010203); // should hold
+		assert(e == 0x000102030405060708090001020304050607080900010204); // should fail
+		bytes32 g = bytes32(b);
+		assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold
+		assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
+	}
+}
+// ----
+// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 0\ne = 0\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 0\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 96533667595335344310996525432040024692804347064549891\ng = 0\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 283686952306183\nd = 5233100606242806050944357496980485\ne = 96533667595335344310996525432040024692804347064549891\ng = 1780731860627700044956966451854862080991451332659079878538166652776284161\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/typecast/slice_to_fixed_bytes_1.sol

@@ -0,0 +1,6 @@
+contract C {
+	function fromSlice(bytes calldata c) external pure returns (bytes32) {
+		return bytes32(c[0:33]);
+	}
+}
+// ----