nx_isa_cortexm_gate.nx source
↩ module page · 834 lines · 37529 B
1// nx_isa_cortexm_gate.nx -- THE ARMv7-M / Cortex-M CONFORMANCE RULER.
2//
3// WHY IT EXISTS: nx_emu_cortexm.nx has claimed "we emulate Cortex-M" since it was
4// written and had NEVER been run by anything. nx_isa_conform_gate measures five of
5// the estate's ten sovereign emulators and names cortexm in its own UNMEASURED list.
6// This organ closes that row for cortexm alone, in its own file, so two seats working
7// two architectures cannot clobber one shared source.
8//
9// THE LAW: expectations come FROM THE ARMv7-M ARCHITECTURE REFERENCE MANUAL --
10// encodings out of the Thumb instruction tables, results out of the operation
11// pseudocode -- never from reading the emulator and writing down what it happens to
12// do. Reading the decoder is allowed for exactly one purpose: learning which classes
13// are IMPLEMENTED versus MISSING, so a gap is named rather than mistaken for a wrong
14// answer. Calibrating the ruler to the subject is the one failure that makes every
15// green here worthless.
16//
17// WHAT READING THE DECODER FOUND, AND WHAT WAS DONE ABOUT IT (2026-09-03):
18// the emulator implemented NO conditional branch, NO unconditional branch, NO CMP in
19// either form, and carried ONE flag (C) with no N, Z or V. A machine that cannot
20// take a branch cannot run a loop, so more than half of these KATs were unrunnable by
21// construction. The gap was CLOSED in nx_emu_cortexm.nx rather than reported --
22// full NZCV off one shared ARM adder, the condition-code table, B-cond, B, CBZ/CBNZ,
23// the immediate add/sub forms, the whole data-processing register block, the shifter,
24// byte/halfword access, SP- and PC-relative addressing. Every KAT below that exercises
25// one of those was RED before that work and is GREEN after it; that transition is the
26// only evidence that this gate can fire at all.
27//
28// FIVE OUTCOMES, NEVER ONE:
29// PASS ran and matched the manual-derived expectation
30// WRONG-ANSWER ran to completion and computed the wrong value
31// UNSUPPORTED hit an instruction class the emulator does not implement
32// RAN-OFF-END the interpreter loop ended without reaching an exit
33// FAULT bad PC, out-of-range fetch, or the step budget
34// Collapsing these into "FAIL" is what makes a gap unactionable: an unimplemented
35// instruction class and a miscomputed result need OPPOSITE fixes.
36//
37// THE EXIT-STATUS MASK IS A REAL HAZARD AND IS DESIGNED AROUND. Cortex-M here halts
38// on BKPT with result = r0 & 0xff, so every legitimate answer is 0..255 and the three
39// negative sentinels can never collide with one -- but two KATs whose right and wrong
40// answers differ only above bit 7 would be indistinguishable. Each expectation below
41// was checked against the value a plausibly WRONG implementation would produce, and
42// where the mask collapsed them the program was changed until it did not (the
43// load/store KAT is the worked example: the obvious version cannot separate a scaled
44// from an unscaled imm5, so it stores twice and lets the second store clobber the
45// first only under the unscaled reading).
46//
47// WHY A RATCHET AND NOT A BAR: this emulator is still incomplete on purpose -- IT
48// blocks, SVC, LDM/STM and most 32-bit Thumb-2 encodings are undecoded and say so.
49// A gate demanding completeness would be permanently RED, and a permanently RED
50// detector is one everyone learns to ignore. So the VERDICT is "cortexm did not
51// regress against its banked score" and the absolute coverage is PUBLISHED AS A
52// NUMBER beside it. The number is the worklist; the verdict is the fence.
53//
54// DISPATCH: emu_cortexm_run_mem(mem, size, entry, sp0) -- the only surface all ten
55// emulators share. _run exists here but not on four of the ten, so building on it
56// would test a subset while looking general.
57//
58// license_tier: ORIGINAL
59
60import "nx_gate_verdict.nx"
61import "nx_syscalls.nx"
62import "nx_emu_cortexm.nx"
63
64// ---- guest layout THIS ORGAN owns (never read from the emulator) ----
65const CX_GUEST_BYTES: i64 = 1048576 // 1 MiB guest image
66const CX_ENTRY: i64 = 0 // KAT code is loaded at guest vaddr 0
67const CX_SP: i64 = 983040 // 960 KiB: above the code, inside the image
68const CX_DATA: i64 = 4096 // scratch word address, past any KAT's code
69const CX_MODE_FILE: i64 = 420 // 0644; 420 and 0x1a4 are the SAME constant and
70 // a sweep that greps one misses the other.
71
72// ---- non-completion codes, read out of nx_emu_cortexm.nx's own constant table ----
73const CX_UNSUPPORTED: i64 = -1
74const CX_RANOFF: i64 = -2
75const CX_FAULT: i64 = -3
76
77// ---- outcome classes ----
78const CX_O_PASS: i64 = 0
79const CX_O_WRONG: i64 = 1
80const CX_O_UNSUP: i64 = 2
81const CX_O_FAULT: i64 = 3
82const CX_O_RANOFF: i64 = 4
83
84// The non-PASS worklist buffer. A count without a worklist is not actionable, and a
85// worklist printed only in the BODY is lost the moment a caller tails the output.
86const CX_NB_BYTES: i64 = 2048
87const CX_NB_OFF: i64 = 0
88const CX_NB_PTR: i64 = 1
89const CX_NB_ROW_MAX: i64 = 256
90const CX_BOX_BYTES: i64 = 32
91
92const CX_NL: i64 = 10
93const CX_SPACE: i64 = 32
94const CX_DIG_LO: i64 = 48
95const CX_DIG_HI: i64 = 57
96const CX_UNSEEDED: i64 = -1
97const CX_RBUF: i64 = 256
98const CX_B10: i64 = 10
99
100// ---- Thumb field shifts and masks (ARMv7-M ARM, chapter A7) ----
101const CX_S3: i64 = 3
102const CX_S5: i64 = 5
103const CX_S6: i64 = 6
104const CX_S8: i64 = 8
105const CX_S9: i64 = 9
106const CX_S10: i64 = 10
107const CX_S11: i64 = 11
108const CX_S12: i64 = 12
109const CX_M3: i64 = 7
110const CX_M4: i64 = 15
111const CX_M5: i64 = 31
112const CX_M8: i64 = 255
113const CX_M11: i64 = 0x7FF
114const CX_BYTE: i64 = 255
115const CX_HWB: i64 = 2 // a Thumb halfword is two bytes
116const CX_PCBIAS: i64 = 4 // Thumb: the branch base is the instruction + 4
117
118// ---- 16-bit Thumb opcode bases ----
119const CX_T_LSLI: i64 = 0x0000
120const CX_T_LSRI: i64 = 0x0800
121const CX_T_ASRI: i64 = 0x1000
122const CX_T_ADDR: i64 = 0x1800
123const CX_T_SUBR: i64 = 0x1A00
124const CX_T_MOVI8: i64 = 0x2000
125const CX_T_ADDI8: i64 = 0x3000
126const CX_T_SUBI8: i64 = 0x3800
127const CX_T_AND: i64 = 0x4000
128const CX_T_CMPR: i64 = 0x4280
129const CX_T_ORR: i64 = 0x4300
130const CX_T_MUL: i64 = 0x4340
131const CX_T_STRI5: i64 = 0x6000
132const CX_T_LDRI5: i64 = 0x6800
133const CX_T_CBZ: i64 = 0xB100
134const CX_T_PUSH: i64 = 0xB400
135const CX_T_POP: i64 = 0xBC00
136const CX_T_BKPT: i64 = 0xBE00
137const CX_T_BCOND: i64 = 0xD000
138const CX_T_B: i64 = 0xE000
139// UDF is PERMANENTLY UNDEFINED by the manual (A7.7.194). That is what makes it a
140// STABLE negative control: no future revision of the emulator can legitimately start
141// executing it, so this control cannot rot into a false RED.
142const CX_T_UDF: i64 = 0xDE00
143// ---- 32-bit Thumb-2 bases ----
144const CX_T_MOVW: i64 = 0xF240
145const CX_T_MLA: i64 = 0xFB00
146
147// ---- condition codes used below (Table A7-1) ----
148const CX_C_NE: i64 = 1
149const CX_C_LT: i64 = 11
150
151// ---- KAT operands and manual-derived expectations ----
152// Every want is 0..255 so the BKPT exit mask cannot truncate it, and every want was
153// chosen so that the value a WRONG implementation produces differs after masking.
154const CX_A40: i64 = 40
155const CX_A2: i64 = 2
156const CX_A90: i64 = 90
157const CX_A48: i64 = 48
158const CX_A200: i64 = 200
159const CX_A7: i64 = 7
160const CX_A240: i64 = 240
161const CX_A15: i64 = 15
162const CX_A60: i64 = 60
163const CX_A6: i64 = 6
164const CX_A5: i64 = 5
165const CX_A8: i64 = 8
166const CX_A9: i64 = 9
167const CX_A33: i64 = 33
168const CX_A55: i64 = 55
169const CX_A42: i64 = 42
170const CX_SH24: i64 = 24
171const CX_SH31: i64 = 31
172const CX_LOOP_N: i64 = 10
173const CX_MOVW_TEST: i64 = 43981 // 0xABCD: imm4=A, i=1, imm3=3, imm8=CD -- all
174 // four MOVW fields non-zero, so an encoder that
175 // drops any one of them gives a different answer.
176
177const CX_W_ARITH: i64 = 42 // 40 + 2
178const CX_W_SUB: i64 = 42 // 90 - 48; a reversed operand order gives 214
179const CX_W_IMM8: i64 = 233 // 200 + 40 - 7
180const CX_W_LOGIC: i64 = 60 // (240 | 15) & 60 = 255 & 60; all-AND gives 0, all-OR gives 255
181const CX_W_LSR: i64 = 1 // 0xFF000000 >> 31 logical
182const CX_W_ASR: i64 = 255 // 0xFF000000 >> 31 arithmetic = 0xFFFFFFFF, masked
183const CX_W_MUL: i64 = 42 // 6 * 7
184const CX_W_LOOP: i64 = 45 // sum 0..9
185const CX_W_SIGNED: i64 = 33 // BLT taken: 0xFF000000 < 1 as SIGNED
186const CX_W_UNSIGN: i64 = 7 // the value only an UNSIGNED compare would leave
187const CX_W_CBZ: i64 = 55
188const CX_W_CBZMISS: i64 = 9
189const CX_W_MOVW: i64 = 171 // 0xABCD >> 8 = 0xAB
190const CX_W_MLA: i64 = 42 // 5 * 8 + 2
191const CX_W_LDST: i64 = 200
192const CX_W_PUSHPOP: i64 = 42
193
194// A bare newline inside a string literal is ambiguous to this lexer, so the byte is
195// CONSTRUCTED.
196func cx_nl() -> i64 {
197 let b: *u8 = sys_mmap(CX_BOX_BYTES)
198 b[0] = CX_NL as u8
199 sys_write(1, b, 1)
200 return 0
201}
202
203// ===== word emitters ============================================
204// ARMv7-M is little-endian and Thumb-2 is a MIXED 16/32-bit encoding, so the emitter
205// unit is the HALFWORD, not the word.
206
207func cx_put_le16(code: *u8, off: i64, w: i64) -> i64 {
208 code[off] = (w) & CX_BYTE
209 code[off + 1] = (w >> CX_S8) & CX_BYTE
210 return off + CX_HWB
211}
212
213// A 32-bit Thumb-2 instruction is TWO little-endian halfwords with hw1 FIRST -- it is
214// NOT a little-endian 32-bit word. Emitting it as one word swaps the halves, the
215// emulator decodes garbage, and the FIXTURE's bug then reads as the emulator being
216// incomplete. That is the silent-fixture defect, so the shape is named here once.
217func cx_put_t32(code: *u8, off: i64, hw1: i64, hw2: i64) -> i64 {
218 var o: i64 = cx_put_le16(code, off, hw1)
219 o = cx_put_le16(code, o, hw2)
220 return o
221}
222
223func cx_guest() -> *u8 { return sys_mmap(CX_GUEST_BYTES) }
224
225// ===== Thumb encoders, straight from the manual's instruction tables ==========
226
227func cx_movs(rd: i64, imm8: i64) -> i64 { return CX_T_MOVI8 | (rd << CX_S8) | (imm8 & CX_M8) }
228func cx_addr(rd: i64, rn: i64, rm: i64) -> i64 { return CX_T_ADDR | (rm << CX_S6) | (rn << CX_S3) | rd }
229func cx_subr(rd: i64, rn: i64, rm: i64) -> i64 { return CX_T_SUBR | (rm << CX_S6) | (rn << CX_S3) | rd }
230func cx_addi8(rdn: i64, imm8: i64) -> i64 { return CX_T_ADDI8 | (rdn << CX_S8) | (imm8 & CX_M8) }
231func cx_subi8(rdn: i64, imm8: i64) -> i64 { return CX_T_SUBI8 | (rdn << CX_S8) | (imm8 & CX_M8) }
232// The 0x4000..0x43FF data-processing register block: <base> Rm Rdn.
233func cx_dpr(base: i64, rdn: i64, rm: i64) -> i64 { return base | (rm << CX_S3) | rdn }
234// Shift-by-immediate: <base> imm5 Rm Rd.
235func cx_shi(base: i64, rd: i64, rm: i64, imm5: i64) -> i64 { return base | (imm5 << CX_S6) | (rm << CX_S3) | rd }
236// Load/store immediate: <base> imm5 Rn Rt. imm5 is SCALED by the access size.
237func cx_lsi5(base: i64, rt: i64, rn: i64, imm5: i64) -> i64 { return base | (imm5 << CX_S6) | (rn << CX_S3) | rt }
238func cx_push(list8: i64) -> i64 { return CX_T_PUSH | (list8 & CX_M8) }
239func cx_pop(list8: i64) -> i64 { return CX_T_POP | (list8 & CX_M8) }
240func cx_bcond(cond: i64, hwoff: i64) -> i64 { return CX_T_BCOND | (cond << CX_S8) | (hwoff & CX_M8) }
241func cx_b(hwoff: i64) -> i64 { return CX_T_B | (hwoff & CX_M11) }
242// CBZ: 1011 0 0 i 1 imm5 Rn, with imm32 = ZeroExtend(i:imm5:'0') -- forward only.
243func cx_cbz(rn: i64, hwoff: i64) -> i64 { return CX_T_CBZ | (((hwoff >> CX_S5) & 1) << CX_S9) | ((hwoff & CX_M5) << CX_S3) | rn }
244// MOVW T3: 11110 i 100100 imm4 / 0 imm3 Rd imm8.
245func cx_movw_hw1(imm16: i64) -> i64 { return CX_T_MOVW | (((imm16 >> CX_S11) & 1) << CX_S10) | ((imm16 >> CX_S12) & CX_M4) }
246func cx_movw_hw2(rd: i64, imm16: i64) -> i64 { return (((imm16 >> CX_S8) & CX_M3) << CX_S12) | (rd << CX_S8) | (imm16 & CX_M8) }
247// MLA: 111110110000 Rn / Ra Rd 0000 Rm.
248func cx_mla_hw1(rn: i64) -> i64 { return CX_T_MLA | rn }
249func cx_mla_hw2(rd: i64, ra: i64, rm: i64) -> i64 { return (ra << CX_S12) | (rd << CX_S8) | rm }
250
251// The branch displacement is DERIVED from the two byte offsets rather than hand-counted.
252// A hand-counted displacement written beside an instruction is a second copy of the
253// program's layout, and the two drift silently the moment a line is inserted.
254func cx_hwoff(here: i64, target: i64) -> i64 {
255 let d: i64 = target - (here + CX_PCBIAS)
256 if d < 0 { return 0 - ((0 - d) / CX_HWB) }
257 return d / CX_HWB
258}
259
260// ===== outcome classification ===================================
261
262func cx_classify(got: i64, want: i64) -> i64 {
263 if got == CX_UNSUPPORTED { return CX_O_UNSUP }
264 if got == CX_RANOFF { return CX_O_RANOFF }
265 if got == CX_FAULT { return CX_O_FAULT }
266 if got == want { return CX_O_PASS }
267 return CX_O_WRONG
268}
269
270func cx_outcome_name(o: i64) -> *u8 {
271 if o == CX_O_PASS { return "PASS" as *u8 }
272 if o == CX_O_WRONG { return "WRONG-ANSWER" as *u8 }
273 if o == CX_O_UNSUP { return "UNSUPPORTED-instruction-class" as *u8 }
274 if o == CX_O_RANOFF { return "RAN-OFF-END-no-exit" as *u8 }
275 return "FAULT-bad-pc-or-step-budget" as *u8
276}
277
278// Print the VALUES, not just the verdict: every vacuous tooth ever caught in this
279// estate was caught by a diagnostic dump and never by a verdict vector.
280func cx_report(kat: *u8, got: i64, want: i64, bx: *i64) -> i64 {
281 let o: i64 = cx_classify(got, want)
282 gv_puts(" KAT cortexm." as *u8)
283 gv_puts(kat)
284 gv_puts(" got=" as *u8)
285 gv_num(got)
286 gv_puts(" want=" as *u8)
287 gv_num(want)
288 gv_puts(" " as *u8)
289 gv_puts(cx_outcome_name(o))
290 cx_nl()
291 if o != CX_O_PASS {
292 let nb: *u8 = bx[CX_NB_PTR] as *u8
293 var p: i64 = bx[CX_NB_OFF]
294 if p < (CX_NB_BYTES - CX_NB_ROW_MAX) {
295 p = gv_cat(nb, p, "cortexm." as *u8)
296 p = gv_cat(nb, p, kat)
297 p = gv_cat(nb, p, "=" as *u8)
298 p = gv_cat(nb, p, cx_outcome_name(o))
299 p = gv_cat(nb, p, "(got=" as *u8)
300 p = gv_catn(nb, p, got)
301 p = gv_cat(nb, p, " want=" as *u8)
302 p = gv_catn(nb, p, want)
303 p = gv_cat(nb, p, ") " as *u8)
304 nb[p] = 0 as u8
305 bx[CX_NB_OFF] = p
306 }
307 }
308 return o
309}
310
311// ===== the KATs =================================================
312// Each program ends at BKPT, which is this bare-metal machine's exit: it halts with
313// result = r0 & 0xff. A KAT that did not end in one would run to the step budget.
314
315// A7.7.76 MOV (immediate) T1 + A7.7.4 ADD (register) T1.
316func cx_imm_arith() -> i64 {
317 let m: *u8 = cx_guest()
318 var o: i64 = 0
319 o = cx_put_le16(m, o, cx_movs(0, CX_A40)) // movs r0,#40
320 o = cx_put_le16(m, o, cx_movs(1, CX_A2)) // movs r1,#2
321 o = cx_put_le16(m, o, cx_addr(0, 0, 1)) // adds r0,r0,r1 -> 42
322 o = cx_put_le16(m, o, CX_T_BKPT)
323 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
324}
325
326// A7.7.171 SUB (register) T1. Rd = Rn - Rm, and the operand order is the whole test:
327// a decoder that computes Rm - Rn returns 48-90 = -42, which the exit mask renders as
328// 214 -- a DIFFERENT answer, which is what makes this KAT worth running.
329func cx_sub() -> i64 {
330 let m: *u8 = cx_guest()
331 var o: i64 = 0
332 o = cx_put_le16(m, o, cx_movs(0, CX_A90))
333 o = cx_put_le16(m, o, cx_movs(1, CX_A48))
334 o = cx_put_le16(m, o, cx_subr(0, 0, 1)) // subs r0,r0,r1 -> 42
335 o = cx_put_le16(m, o, CX_T_BKPT)
336 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
337}
338
339// A7.7.3 ADD (immediate) T2 and A7.7.170 SUB (immediate) T2: the Rdn field is bits
340// 10..8, NOT bits 2..0 as in the three-register forms. An emulator that reuses the
341// low-register field writes the wrong register and the answer changes.
342func cx_imm8_add_sub() -> i64 {
343 let m: *u8 = cx_guest()
344 var o: i64 = 0
345 o = cx_put_le16(m, o, cx_movs(0, CX_A200))
346 o = cx_put_le16(m, o, cx_addi8(0, CX_A40)) // adds r0,#40 -> 240
347 o = cx_put_le16(m, o, cx_subi8(0, CX_A7)) // subs r0,#7 -> 233
348 o = cx_put_le16(m, o, CX_T_BKPT)
349 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
350}
351
352// A7.7.91 ORR (register) then A7.7.9 AND (register). Doing BOTH is the point: a
353// machine that implements only AND returns 0 and one that implements only ORR returns
354// 255, so neither can pass by accident.
355func cx_logic() -> i64 {
356 let m: *u8 = cx_guest()
357 var o: i64 = 0
358 o = cx_put_le16(m, o, cx_movs(0, CX_A240))
359 o = cx_put_le16(m, o, cx_movs(1, CX_A15))
360 o = cx_put_le16(m, o, cx_dpr(CX_T_ORR, 0, 1)) // orrs r0,r1 -> 255
361 o = cx_put_le16(m, o, cx_movs(2, CX_A60))
362 o = cx_put_le16(m, o, cx_dpr(CX_T_AND, 0, 2)) // ands r0,r2 -> 60
363 o = cx_put_le16(m, o, CX_T_BKPT)
364 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
365}
366
367// LSR vs ASR on a value with bit 31 set is the discrimination that matters, and the
368// obvious version of this test CANNOT make it: shifting right by a small amount leaves
369// the same low byte under both, and the exit mask keeps only the low byte. Shifting
370// by 31 separates them completely: logical -> 1, arithmetic -> 0xFFFFFFFF -> 255.
371func cx_shift_logical() -> i64 {
372 let m: *u8 = cx_guest()
373 var o: i64 = 0
374 o = cx_put_le16(m, o, cx_movs(0, CX_M8))
375 o = cx_put_le16(m, o, cx_shi(CX_T_LSLI, 0, 0, CX_SH24)) // lsls r0,r0,#24 -> 0xFF000000
376 o = cx_put_le16(m, o, cx_shi(CX_T_LSRI, 0, 0, CX_SH31)) // lsrs r0,r0,#31 -> 1
377 o = cx_put_le16(m, o, CX_T_BKPT)
378 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
379}
380
381func cx_shift_arith() -> i64 {
382 let m: *u8 = cx_guest()
383 var o: i64 = 0
384 o = cx_put_le16(m, o, cx_movs(0, CX_M8))
385 o = cx_put_le16(m, o, cx_shi(CX_T_LSLI, 0, 0, CX_SH24)) // lsls r0,r0,#24
386 o = cx_put_le16(m, o, cx_shi(CX_T_ASRI, 0, 0, CX_SH31)) // asrs r0,r0,#31 -> -1 -> 255
387 o = cx_put_le16(m, o, CX_T_BKPT)
388 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
389}
390
391// A7.7.84 MUL T1: Rdm = Rn * Rdm. Both source fields matter, so 6*7 is asymmetric in
392// neither value -- but the register roles are, and a decoder that reads the fields the
393// other way round multiplies r0 by itself (36) rather than by r1.
394func cx_mul() -> i64 {
395 let m: *u8 = cx_guest()
396 var o: i64 = 0
397 o = cx_put_le16(m, o, cx_movs(0, CX_A6))
398 o = cx_put_le16(m, o, cx_movs(1, CX_A7))
399 o = cx_put_le16(m, o, cx_dpr(CX_T_MUL, 0, 1)) // muls r0,r1,r0 -> 42
400 o = cx_put_le16(m, o, CX_T_BKPT)
401 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
402}
403
404// THE FIRST PROGRAM THAT IS NOT A STRAIGHT LINE. A7.7.12 B T1 (conditional) plus
405// A7.7.27 CMP (register). Before the branch work this returned UNSUPPORTED, which is
406// exactly what the five-way taxonomy exists to say.
407func cx_branch_loop() -> i64 {
408 let m: *u8 = cx_guest()
409 var o: i64 = 0
410 o = cx_put_le16(m, o, cx_movs(0, 0)) // movs r0,#0 sum
411 o = cx_put_le16(m, o, cx_movs(1, 0)) // movs r1,#0 i
412 o = cx_put_le16(m, o, cx_movs(2, CX_LOOP_N)) // movs r2,#10 n
413 let lp_top: i64 = o
414 o = cx_put_le16(m, o, cx_addr(0, 0, 1)) // adds r0,r0,r1
415 o = cx_put_le16(m, o, cx_addi8(1, 1)) // adds r1,#1
416 o = cx_put_le16(m, o, cx_dpr(CX_T_CMPR, 1, 2)) // cmp r1,r2
417 let br: i64 = o
418 o = cx_put_le16(m, o, cx_bcond(CX_C_NE, cx_hwoff(br, lp_top)))
419 o = cx_put_le16(m, o, CX_T_BKPT) // -> sum 0..9 = 45
420 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
421}
422
423// SIGNED vs UNSIGNED conditions, which a one-flag machine cannot even express.
424// 0xFF000000 compared with 1: as SIGNED it is less (N=1, V=0 -> LT taken, 33); as
425// UNSIGNED it is greater (C=1 -> LO not taken, 7). An emulator that implements LT as
426// an unsigned compare therefore returns a DIFFERENT number rather than the same one.
427func cx_signed_cond() -> i64 {
428 let m: *u8 = cx_guest()
429 var o: i64 = 0
430 o = cx_put_le16(m, o, cx_movs(0, 1)) // movs r0,#1
431 o = cx_put_le16(m, o, cx_movs(1, CX_M8)) // movs r1,#255
432 o = cx_put_le16(m, o, cx_shi(CX_T_LSLI, 1, 1, CX_SH24)) // lsls r1,r1,#24
433 o = cx_put_le16(m, o, cx_dpr(CX_T_CMPR, 1, 0)) // cmp r1,r0
434 let br: i64 = o
435 o = o + CX_HWB // blt <patched below>
436 o = cx_put_le16(m, o, cx_movs(0, CX_W_UNSIGN)) // movs r0,#7
437 let jb: i64 = o
438 o = o + CX_HWB // b <patched below>
439 let sgn: i64 = o
440 o = cx_put_le16(m, o, cx_movs(0, CX_W_SIGNED)) // movs r0,#33
441 let done: i64 = o
442 o = cx_put_le16(m, o, CX_T_BKPT)
443 cx_put_le16(m, br, cx_bcond(CX_C_LT, cx_hwoff(br, sgn)))
444 cx_put_le16(m, jb, cx_b(cx_hwoff(jb, done)))
445 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
446}
447
448// A7.7.21 CBZ: compares against zero WITHOUT reading or writing the flags, so it is a
449// genuinely different mechanism from B-cond and not a duplicate of the KAT above.
450func cx_cbz_taken() -> i64 {
451 let m: *u8 = cx_guest()
452 var o: i64 = 0
453 o = cx_put_le16(m, o, cx_movs(0, 0)) // movs r0,#0
454 let cb: i64 = o
455 o = o + CX_HWB // cbz r0,<hit>
456 o = cx_put_le16(m, o, cx_movs(0, CX_W_CBZMISS)) // movs r0,#9
457 let jb: i64 = o
458 o = o + CX_HWB // b <done>
459 let hit: i64 = o
460 o = cx_put_le16(m, o, cx_movs(0, CX_W_CBZ)) // movs r0,#55
461 let done: i64 = o
462 o = cx_put_le16(m, o, CX_T_BKPT)
463 cx_put_le16(m, cb, cx_cbz(0, cx_hwoff(cb, hit)))
464 cx_put_le16(m, jb, cx_b(cx_hwoff(jb, done)))
465 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
466}
467
468// THE MIXED-WIDTH TEST. MOVW is a 32-bit Thumb-2 encoding and LSRS is 16-bit, so this
469// only works if the fetch width is decided per instruction. 0xABCD puts a non-zero
470// value in all four MOVW immediate fields (imm4, i, imm3, imm8): dropping i gives 163,
471// dropping imm3 gives 168, taking only the low byte gives 0 -- three distinct wrong
472// answers, none of which is 171.
473func cx_thumb2_movw() -> i64 {
474 let m: *u8 = cx_guest()
475 var o: i64 = 0
476 o = cx_put_t32(m, o, cx_movw_hw1(CX_MOVW_TEST), cx_movw_hw2(0, CX_MOVW_TEST))
477 o = cx_put_le16(m, o, cx_shi(CX_T_LSRI, 0, 0, CX_S8)) // lsrs r0,r0,#8 -> 0xAB
478 o = cx_put_le16(m, o, CX_T_BKPT)
479 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
480}
481
482// A7.7.74 MLA: Rd = Rn*Rm + Ra, with Ra in hw2 bits 15..12 and Rd in bits 11..8.
483// A decoder that swaps them writes the product into r2 and leaves r0 at 5.
484func cx_thumb2_mla() -> i64 {
485 let m: *u8 = cx_guest()
486 var o: i64 = 0
487 o = cx_put_le16(m, o, cx_movs(0, CX_A5))
488 o = cx_put_le16(m, o, cx_movs(1, CX_A8))
489 o = cx_put_le16(m, o, cx_movs(2, CX_A2))
490 o = cx_put_t32(m, o, cx_mla_hw1(0), cx_mla_hw2(0, 2, 1)) // mla r0,r0,r1,r2 -> 42
491 o = cx_put_le16(m, o, CX_T_BKPT)
492 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
493}
494
495// A7.7.119 LDR (immediate) T1 / A7.7.158 STR (immediate) T1. The imm5 field is SCALED
496// BY FOUR, and the obvious round-trip test cannot see whether the emulator scales it:
497// storing and loading at the same unscaled offset returns the same byte either way,
498// and the exit mask keeps only that byte. So this stores TWICE. Under the correct
499// scaled reading the two words are four bytes apart and the readback is 200; under an
500// unscaled reading they overlap and the second store zeroes the low three bytes of the
501// first, so the readback is 0.
502func cx_load_store() -> i64 {
503 let m: *u8 = cx_guest()
504 var o: i64 = 0
505 o = cx_put_t32(m, o, cx_movw_hw1(CX_DATA), cx_movw_hw2(1, CX_DATA)) // movw r1,#4096
506 o = cx_put_le16(m, o, cx_movs(0, CX_W_LDST)) // movs r0,#200
507 o = cx_put_le16(m, o, cx_lsi5(CX_T_STRI5, 0, 1, 1)) // str r0,[r1,#4]
508 o = cx_put_le16(m, o, cx_movs(0, 0)) // movs r0,#0
509 o = cx_put_le16(m, o, cx_lsi5(CX_T_STRI5, 0, 1, 0)) // str r0,[r1,#0]
510 o = cx_put_le16(m, o, cx_lsi5(CX_T_LDRI5, 0, 1, 1)) // ldr r0,[r1,#4]
511 o = cx_put_le16(m, o, CX_T_BKPT)
512 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
513}
514
515// A7.7.99 PUSH / A7.7.98 POP. The MOVS between them is load-bearing: without it a POP
516// that did nothing at all would still leave 42 in r0 and the KAT would pass vacuously.
517func cx_push_pop() -> i64 {
518 let m: *u8 = cx_guest()
519 var o: i64 = 0
520 o = cx_put_le16(m, o, cx_movs(0, CX_A42))
521 o = cx_put_le16(m, o, cx_push(1)) // push {r0}
522 o = cx_put_le16(m, o, cx_movs(0, 0)) // movs r0,#0
523 o = cx_put_le16(m, o, cx_pop(1)) // pop {r0} -> 42
524 o = cx_put_le16(m, o, CX_T_BKPT)
525 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
526}
527
528// NEGATIVE CONTROL, EMULATOR LEVEL. UDF is permanently undefined, so a machine that
529// returns anything other than UNSUPPORTED here is either inventing behaviour or its
530// refusal path never runs. A gate whose every subject is well-formed has not been
531// shown to fire.
532func cx_udf_refused() -> i64 {
533 let m: *u8 = cx_guest()
534 var o: i64 = 0
535 o = cx_put_le16(m, o, cx_movs(0, CX_A42))
536 o = cx_put_le16(m, o, CX_T_UDF)
537 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_ENTRY, CX_SP)
538}
539
540// NEGATIVE CONTROL, FETCH LEVEL. An entry PC one byte short of the end of the image
541// cannot hold a halfword, so the fetch is out of range. This proves the FAULT path
542// exists and is distinguishable from every real answer.
543func cx_fault_entry() -> i64 {
544 let m: *u8 = cx_guest()
545 return emu_cortexm_run_mem(m, CX_GUEST_BYTES, CX_GUEST_BYTES - 1, CX_SP)
546}
547
548// ===== ratchet ==================================================
549// One line: "cortexm <passed>". UNSEEDED is a NAMED third state, so adopting this
550// fence cannot fail closed on first sight. Polarity matters and inverts from an
551// offender-count ratchet: this metric is GOOD-when-higher, so it TIGHTENS on a rise
552// and must NEVER rewrite its baseline on a fall -- rewriting on a fall is how a
553// ratchet launders itself green.
554
555const CX_RATCHET: *u8 = "knowledge/status/isa_cortexm.ratchet"
556const CX_KEY: *u8 = "cortexm"
557
558func cx_match_at(buf: *u8, n: i64, p: i64, s: *u8) -> i64 {
559 var j: i64 = 0
560 var ok: i64 = 1
561 while s[j] != (0 as u8) {
562 if (p + j) >= n { ok = 0 }
563 if ok == 1 {
564 if buf[p + j] != s[j] { ok = 0 }
565 }
566 j = j + 1
567 }
568 if ok == 0 { return -1 }
569 return j
570}
571
572func cx_digits_at(buf: *u8, n: i64, p0: i64) -> i64 {
573 var v: i64 = 0
574 var any: i64 = 0
575 var p: i64 = p0
576 var go: i64 = 1
577 while go == 1 {
578 if p >= n { go = 0 }
579 if go == 1 {
580 let c: i64 = buf[p] & CX_BYTE
581 if c < CX_DIG_LO { go = 0 }
582 if go == 1 {
583 if c > CX_DIG_HI { go = 0 }
584 }
585 if go == 1 {
586 v = v * CX_B10 + (c - CX_DIG_LO)
587 any = 1
588 p = p + 1
589 }
590 }
591 }
592 if any == 0 { return -1 }
593 return v
594}
595
596func cx_ratchet_read() -> i64 {
597 let lenbox: *i64 = sys_mmap(CX_BOX_BYTES) as *i64
598 let buf: *u8 = sys_read_file(CX_RATCHET, lenbox)
599 if (buf as i64) == 0 { return CX_UNSEEDED }
600 let n: i64 = lenbox[0]
601 var i: i64 = 0
602 var found: i64 = CX_UNSEEDED
603 while i < n {
604 if found < 0 {
605 let mm: i64 = cx_match_at(buf, n, i, CX_KEY)
606 if mm > 0 {
607 if (i + mm) < n {
608 if buf[i + mm] == (CX_SPACE as u8) {
609 found = cx_digits_at(buf, n, i + mm + 1)
610 }
611 }
612 }
613 }
614 var adv: i64 = 1
615 while adv == 1 {
616 if i >= n { adv = 0 }
617 if adv == 1 {
618 if buf[i] == (CX_NL as u8) { adv = 0 }
619 i = i + 1
620 }
621 }
622 }
623 return found
624}
625
626// Callers must have already decided that the score did not regress; this function
627// does not re-check, and the tooth that guards it is asserted in main.
628func cx_ratchet_write(n: i64) -> i64 {
629 let d: *u8 = sys_mmap(CX_RBUF)
630 var o: i64 = 0
631 o = gv_cat(d, o, "cortexm " as *u8)
632 o = gv_catn(d, o, n)
633 d[o] = CX_NL as u8
634 o = o + 1
635 let fd: i64 = sys_openat_wr(CX_RATCHET, CX_MODE_FILE)
636 if fd < 0 { return -1 }
637 sys_write(fd, d, o)
638 sys_fsync(fd)
639 sys_close(fd)
640 return o
641}
642
643// ===== main =====================================================
644
645func main(argc: i64, argv: *i64) -> i64 {
646 gv_head("nx_isa_cortexm_gate -- ARMv7-M / Cortex-M Thumb-2 conformance, KATs encoded from the ARM ARM" as *u8)
647 let ctr: *i64 = gv_ctr()
648
649 let bx: *i64 = sys_mmap(CX_BOX_BYTES) as *i64
650 let nbuf: *u8 = sys_mmap(CX_NB_BYTES)
651 nbuf[0] = 0 as u8
652 bx[CX_NB_OFF] = 0
653 bx[CX_NB_PTR] = nbuf as i64
654
655 gv_puts("dispatch=emu_cortexm_run_mem exit=BKPT halts with r0 masked to 8 bits, so a real answer is 0..255" as *u8)
656 cx_nl()
657 gv_puts("outcomes are FIVE-WAY: PASS / WRONG-ANSWER / UNSUPPORTED-instruction-class / RAN-OFF-END / FAULT" as *u8)
658 cx_nl()
659 gv_puts("[cortexm] ARMv7-M Thumb-2 -- little-endian, MIXED 16/32-bit halfword instruction stream" as *u8)
660 cx_nl()
661
662 var cm_pass: i64 = 0
663 var cm_tot: i64 = 0
664 var o: i64 = 0
665
666 o = cx_report("imm-arith" as *u8, cx_imm_arith(), CX_W_ARITH, bx)
667 cm_tot = cm_tot + 1
668 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
669 gv_check("isa-cortexm-imm-arith" as *u8, o == CX_O_PASS, ctr)
670
671 o = cx_report("sub-reg-operand-order" as *u8, cx_sub(), CX_W_SUB, bx)
672 cm_tot = cm_tot + 1
673 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
674 gv_check("isa-cortexm-sub-reg-operand-order" as *u8, o == CX_O_PASS, ctr)
675
676 o = cx_report("imm8-add-sub-rdn-field" as *u8, cx_imm8_add_sub(), CX_W_IMM8, bx)
677 cm_tot = cm_tot + 1
678 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
679 gv_check("isa-cortexm-imm8-add-sub-rdn-field" as *u8, o == CX_O_PASS, ctr)
680
681 o = cx_report("logic-and-vs-or" as *u8, cx_logic(), CX_W_LOGIC, bx)
682 cm_tot = cm_tot + 1
683 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
684 gv_check("isa-cortexm-logic-and-vs-or" as *u8, o == CX_O_PASS, ctr)
685
686 o = cx_report("shift-logical" as *u8, cx_shift_logical(), CX_W_LSR, bx)
687 cm_tot = cm_tot + 1
688 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
689 gv_check("isa-cortexm-shift-logical" as *u8, o == CX_O_PASS, ctr)
690
691 o = cx_report("shift-arith" as *u8, cx_shift_arith(), CX_W_ASR, bx)
692 cm_tot = cm_tot + 1
693 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
694 gv_check("isa-cortexm-shift-arith" as *u8, o == CX_O_PASS, ctr)
695
696 o = cx_report("mul" as *u8, cx_mul(), CX_W_MUL, bx)
697 cm_tot = cm_tot + 1
698 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
699 gv_check("isa-cortexm-mul" as *u8, o == CX_O_PASS, ctr)
700
701 o = cx_report("branch-loop" as *u8, cx_branch_loop(), CX_W_LOOP, bx)
702 cm_tot = cm_tot + 1
703 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
704 gv_check("isa-cortexm-branch-loop" as *u8, o == CX_O_PASS, ctr)
705
706 o = cx_report("signed-vs-unsigned-condition" as *u8, cx_signed_cond(), CX_W_SIGNED, bx)
707 cm_tot = cm_tot + 1
708 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
709 gv_check("isa-cortexm-signed-vs-unsigned-condition" as *u8, o == CX_O_PASS, ctr)
710
711 o = cx_report("cbz-taken" as *u8, cx_cbz_taken(), CX_W_CBZ, bx)
712 cm_tot = cm_tot + 1
713 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
714 gv_check("isa-cortexm-cbz-taken" as *u8, o == CX_O_PASS, ctr)
715
716 let mw: i64 = cx_report("thumb2-movw-mixed-width" as *u8, cx_thumb2_movw(), CX_W_MOVW, bx)
717 cm_tot = cm_tot + 1
718 if mw == CX_O_PASS { cm_pass = cm_pass + 1 }
719 gv_check("isa-cortexm-thumb2-movw-mixed-width" as *u8, mw == CX_O_PASS, ctr)
720
721 o = cx_report("thumb2-mla" as *u8, cx_thumb2_mla(), CX_W_MLA, bx)
722 cm_tot = cm_tot + 1
723 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
724 gv_check("isa-cortexm-thumb2-mla" as *u8, o == CX_O_PASS, ctr)
725
726 o = cx_report("load-store-imm5-is-scaled" as *u8, cx_load_store(), CX_W_LDST, bx)
727 cm_tot = cm_tot + 1
728 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
729 gv_check("isa-cortexm-load-store-imm5-is-scaled" as *u8, o == CX_O_PASS, ctr)
730
731 o = cx_report("push-pop" as *u8, cx_push_pop(), CX_W_PUSHPOP, bx)
732 cm_tot = cm_tot + 1
733 if o == CX_O_PASS { cm_pass = cm_pass + 1 }
734 gv_check("isa-cortexm-push-pop" as *u8, o == CX_O_PASS, ctr)
735
736 // ---- the fixture must have REACHED the emulator ---------------
737 // Asserting an outcome without asserting the fixture ran is how four vacuous
738 // fixtures shipped in this estate in a single day.
739 cx_nl()
740 gv_check("fixture-reached-cortexm-emulator-at-all" as *u8, cm_pass > 0, ctr)
741 // And specifically the 32-bit half of the mixed-width stream: a machine that only
742 // ever fetched halfwords would still pass every 16-bit KAT above.
743 gv_check("fixture-reached-thumb2-32bit-decode" as *u8, mw == CX_O_PASS, ctr)
744
745 // ---- negative controls ---------------------------------------
746 // A comparison that cannot fail proves nothing. If cx_classify were stubbed to
747 // return PASS, every green above would be fake and only these teeth would notice.
748 let ncw: i64 = cx_classify(cx_imm_arith(), CX_W_ARITH - 1)
749 gv_puts(" neg-control imm-arith against a deliberately wrong want -> " as *u8)
750 gv_puts(cx_outcome_name(ncw))
751 cx_nl()
752 gv_check("neg-control-wrong-expectation-must-not-pass" as *u8, ncw == CX_O_WRONG, ctr)
753
754 // The three sentinels must never read as a PASS even when the caller's `want`
755 // happens to equal them -- that equality is exactly the trap.
756 gv_check("neg-control-unsupported-never-reads-as-pass" as *u8, cx_classify(CX_UNSUPPORTED, CX_UNSUPPORTED) == CX_O_UNSUP, ctr)
757 gv_check("neg-control-ranoff-never-reads-as-pass" as *u8, cx_classify(CX_RANOFF, CX_RANOFF) == CX_O_RANOFF, ctr)
758 gv_check("neg-control-fault-never-reads-as-pass" as *u8, cx_classify(CX_FAULT, CX_FAULT) == CX_O_FAULT, ctr)
759
760 // Emulator-level controls: these run real guest code and assert the emulator's own
761 // refusal and fault paths fire, not merely that the classifier's table is right.
762 let udf: i64 = cx_udf_refused()
763 gv_puts(" neg-control emulator on UDF (permanently undefined, A7.7.194) returned " as *u8)
764 gv_num(udf)
765 cx_nl()
766 gv_check("neg-control-emulator-refuses-undefined-instruction" as *u8, udf == CX_UNSUPPORTED, ctr)
767
768 let flt: i64 = cx_fault_entry()
769 gv_puts(" neg-control emulator on an out-of-range entry PC returned " as *u8)
770 gv_num(flt)
771 cx_nl()
772 gv_check("neg-control-emulator-faults-on-out-of-range-fetch" as *u8, flt == CX_FAULT, ctr)
773
774 // ---- coverage, published as a NUMBER not a verdict ------------
775 cx_nl()
776 gv_puts("coverage cortexm=" as *u8)
777 gv_num(cm_pass)
778 gv_puts("/" as *u8)
779 gv_num(cm_tot)
780 gv_puts(" classes measured: imm-arith sub logic shift-lsr shift-asr mul cond-branch signed-cond cbz thumb2-movw thumb2-mla load-store push-pop" as *u8)
781 cx_nl()
782 gv_puts("STILL UNDECODED and correctly reporting UNSUPPORTED: IT blocks, SVC, UDF, LDM/STM, REV/REVSH, and every 32-bit Thumb-2 encoding outside MOVW SUBW UMULL MLA LDR.W STR.W" as *u8)
783 cx_nl()
784
785 // ---- ratchet -------------------------------------------------
786 let base: i64 = cx_ratchet_read()
787 gv_puts("ratchet cortexm base=" as *u8)
788 gv_num(base)
789 gv_puts(" now=" as *u8)
790 gv_num(cm_pass)
791 gv_puts(" (base=-1 is UNSEEDED, a named state: first sight seeds, so adoption cannot fail closed)" as *u8)
792 cx_nl()
793
794 var no_regress: i64 = 1
795 if base >= 0 {
796 if cm_pass < base { no_regress = 0 }
797 }
798
799 // Seed when unseeded; tighten only on a rise; NEVER rewrite on a fall.
800 var wrote: i64 = 0
801 if no_regress == 1 {
802 if base < 0 { wrote = cx_ratchet_write(cm_pass) }
803 if wrote == 0 {
804 if cm_pass > base { wrote = cx_ratchet_write(cm_pass) }
805 }
806 }
807 gv_puts("ratchet_bytes_written=" as *u8)
808 gv_num(wrote)
809 gv_puts(" (0 = held: neither seeded nor tightened this run)" as *u8)
810 cx_nl()
811
812 // This dialect has no disjunction operator, so the laundering condition is
813 // computed rather than expressed.
814 var laundered: i64 = 0
815 if no_regress == 0 {
816 if wrote > 0 { laundered = 1 }
817 }
818
819 gv_check("ratchet-cortexm-did-not-regress" as *u8, no_regress == 1, ctr)
820 gv_check("ratchet-never-rewritten-on-a-regression" as *u8, laundered == 0, ctr)
821
822 // THE WORKLIST, LAST, where a tailing caller can still see it.
823 gv_puts("NONPASS: " as *u8)
824 if bx[CX_NB_OFF] == 0 {
825 gv_puts("none -- every measured KAT matched its manual-derived expectation" as *u8)
826 }
827 if bx[CX_NB_OFF] > 0 {
828 gv_puts(bx[CX_NB_PTR] as *u8)
829 }
830 cx_nl()
831
832 return gv_verdict("nx_isa_cortexm_gate" as *u8, ctr,
833 "ARMv7-M Thumb-2 conformance measured against KATs encoded from the ARM ARM with five-way outcomes, two emulator-level negative controls, coverage published as a number, fenced by a good-when-higher ratchet that seeds on first sight and never rewrites on a fall" as *u8)
834}