commit edbea61f7462e1584d862564470647372b578594
parent f725b1162f0038013abb884ca73dd3b10a7ddb89
Author: Ryan Sepassi <rsepassi@gmail.com>
Date: Sun, 26 Apr 2026 21:52:48 -0700
cc tests: lock in unsigned narrowing zero-extends (§A.5)
Pre-existing mask-on-unsigned-narrow path is already correct;
cc-cg/19-zext-narrow + cc-parse/19-zext-narrow are regression guards
that pin the contrast with §A.4: same -3 source, same cast chain
shape, divergent result via target signedness (i32 → -3, u32 → 253).
Diffstat:
5 files changed, 34 insertions(+), 4 deletions(-)
diff --git a/docs/CC-PUNCHLIST.md b/docs/CC-PUNCHLIST.md
@@ -74,10 +74,12 @@ upstream of nearly everything else. Land this first.
the canonical sign-extended 64-bit form. The widening cast back
(relabel-only) preserves it.
-- [ ] **Unsigned narrowing zero-extends**
- - cg: `cc-cg/NN-zext-narrow.scm` — `(unsigned)(unsigned char)-3` → 253.
- - parse: `cc-parse/NN-zext-narrow.c`
- - Needs: `cg-cast` zero-fill on unsigned target.
+- [x] **Unsigned narrowing zero-extends**
+ - cg: `cc-cg/19-zext-narrow.scm` — `(unsigned)(unsigned char)-3 == 253`.
+ - parse: `cc-parse/19-zext-narrow.c`
+ - Done: pre-existing mask-on-unsigned-narrow path was already
+ correct; fixture locks the contrast with §A.4 in (same source,
+ same chain shape, divergent result via target signedness).
- [ ] **Integer promotion preserves sign across operations**
- cg: `cc-cg/NN-promote-sign.scm` — operate on a `signed char` slot
diff --git a/tests/cc-cg/19-zext-narrow.expected-exit b/tests/cc-cg/19-zext-narrow.expected-exit
@@ -0,0 +1 @@
+1
diff --git a/tests/cc-cg/19-zext-narrow.scm b/tests/cc-cg/19-zext-narrow.scm
@@ -0,0 +1,20 @@
+;; tests/cc-cg/19-zext-narrow.scm — unsigned narrowing zero-extends
+;; (§A.5 of docs/CC-PUNCHLIST.md).
+;;
+;; Models: ((unsigned)(unsigned char)-3) == 253.
+;; The narrowing cast to u8 must mask off the high bits (not sign-
+;; extend), so the value 0xFFFFFFFD becomes 0xFD = 253. The
+;; widening cast back to u32 is relabel-only and preserves it.
+;; Locks in the contrast with §A.4: same source value, but the
+;; unsigned target arrives at 253 not -3.
+
+(let ((cg (cg-init)))
+ (cg-fn-begin cg "main" '() %t-i32)
+ (cg-push-imm cg %t-i32 -3)
+ (cg-cast cg %t-u8)
+ (cg-cast cg %t-u32)
+ (cg-push-imm cg %t-u32 253)
+ (cg-binop cg 'eq)
+ (cg-return cg)
+ (cg-fn-end cg)
+ (write-bv-fd 1 (cg-finish cg)))
diff --git a/tests/cc-parse/19-zext-narrow.c b/tests/cc-parse/19-zext-narrow.c
@@ -0,0 +1,6 @@
+// tests/cc-parse/19-zext-narrow.c — unsigned narrowing zero-extends.
+// §A.5 of docs/CC-PUNCHLIST.md.
+
+int main() {
+ return ((unsigned)(unsigned char)-3) == 253;
+}
diff --git a/tests/cc-parse/19-zext-narrow.expected-exit b/tests/cc-parse/19-zext-narrow.expected-exit
@@ -0,0 +1 @@
+1