nx_checked_arith.nx source
↩ module page · 140 lines · 5908 B
1// nx_checked_arith.nx -- LN1 CHECKED INTEGER ARITHMETIC fixture organ (lang.plan rung LN1, watch
2// symbol chk_add_overflow on /compare/lang row "Integer overflow checked (CWE-190 class)").
3//
4// WHAT THIS IS. The runnable witness for the compiler's --chkarith declared mode: every i64
5// `+ - *` is followed by an overflow check that traps exit 72 (NX_TRAP_OVERFLOW) instead of
6// wrapping (nx_parse.nx, the LN1 block). Each phase is selected by argv so a single trap ends
7// exactly one phase and the gate (nx_chkarith_gate) can assert every outcome independently:
8//
9// nx_checked_arith ok in-range add/sub/mul incl. the a==0 and a==-1 multiply paths
10// -> exit 0 under BOTH modes (the positive control: a deny mode that
11// refuses everything fails here)
12// nx_checked_arith add MAX + 1. Default build: WRAPS to MIN and keeps running (exit 0 only
13// if the wrapped value is observed -- anti-vacuity: the add executed).
14// --chkarith build: traps exit 72.
15// nx_checked_arith sub MIN - 1 -> wraps to MAX (default) / traps 72 (--chkarith).
16// nx_checked_arith mul 2^32 * 2^32 -> wraps to 0 (default) / traps 72 (--chkarith).
17// nx_checked_arith mulmin MIN * -1 -> wraps to MIN (default) / traps 72 (--chkarith) -- and
18// MUST NOT die of SIGFPE: the check's own division is branched around
19// for a == -1. Exit 72 is the only accepted outcome under the mode.
20//
21// The wrap-by-intent intrinsics (__wrap_add/__wrap_sub/__wrap_mul) are witnessed by the sibling
22// nx_checked_arith_wrap.nx so that THIS file compiles on a pre-LN1 compiler too -- which is what
23// makes the gate's bite ATTRIBUTABLE: against the old compiler only the mode teeth go RED.
24//
25// Operands are produced by FUNCTION CALLS, never literals or let-bound constants, so the runtime
26// legs exercise the RUNTIME check and not the compile-time refusal (that leg has its own sibling
27// witness, nx_checked_arith_const.nx).
28//
29// license_tier: ORIGINAL No hw writes (Rule 26).
30import "nx_syscalls.nx"
31
32// 2^62 built by shift (63 and 62 are inside the constant shift-count range the parser enforces).
33func ca_pow62() -> i64 {
34 var m: i64 = 1
35 m = m << 62
36 return m
37}
38// i64 MAX = (2^62 - 1) + 2^62 -- no overflow in either step, so it builds under --chkarith too.
39func ca_max() -> i64 {
40 let p: i64 = ca_pow62()
41 return p - 1 + p
42}
43// i64 MIN = 1 << 63 (the sign bit alone).
44func ca_min() -> i64 {
45 var m: i64 = 1
46 m = m << 63
47 return m
48}
49func ca_pow32() -> i64 {
50 var m: i64 = 1
51 m = m << 32
52 return m
53}
54func ca_pow31() -> i64 {
55 var m: i64 = 1
56 m = m << 31
57 return m
58}
59func ca_zero() -> i64 { return 0 }
60func ca_one() -> i64 { return 1 }
61func ca_neg1() -> i64 { return 0 - 1 }
62
63// THE WATCH SYMBOL and the ADD leg in one: MAX + 1. Under the default this returns the wrapped
64// value (MIN, negative); under --chkarith the add traps before the return executes.
65func chk_add_overflow() -> i64 {
66 let a: i64 = ca_max()
67 let b: i64 = ca_one()
68 return a + b
69}
70func ca_sub_overflow() -> i64 {
71 let a: i64 = ca_min()
72 let b: i64 = ca_one()
73 return a - b
74}
75func ca_mul_overflow() -> i64 {
76 let a: i64 = ca_pow32()
77 let b: i64 = ca_pow32()
78 return a * b
79}
80func ca_mulmin_overflow() -> i64 {
81 let a: i64 = ca_min()
82 let b: i64 = ca_neg1()
83 return b * a // a == -1 on the LEFT: the division-unsafe path the check must branch around
84}
85
86// Positive control: in-range arithmetic through every branch of the checker. Must exit 0 under
87// BOTH modes or the checker is refusing valid programs.
88func ca_inrange_control() -> i64 {
89 let mx: i64 = ca_max()
90 let mn: i64 = ca_min()
91 let one: i64 = ca_one()
92 let z: i64 = ca_zero()
93 let m1: i64 = ca_neg1()
94 let p31: i64 = ca_pow31()
95 var bad: i64 = 0
96 if (mx - one) + one != mx { bad = bad + 1 } // add up to the edge
97 if (mn + one) - one != mn { bad = bad + 1 } // sub down to the edge
98 if (p31 - one) * (p31 - one) <= z { bad = bad + 1 }// (2^31-1)^2 < 2^62 : fits, positive
99 if mx * m1 != (mn + one) { bad = bad + 1 } // MAX * -1 = MIN+1 : fits (a == MAX path)
100 if m1 * mx != (mn + one) { bad = bad + 1 } // a == -1, b != MIN : the neg1 branch, no trap
101 if z * mn != z { bad = bad + 1 } // a == 0 : the zero branch, no trap
102 if mn * one != mn { bad = bad + 1 } // r / a == b exactly at the edge
103 if bad != 0 { return 1 }
104 return 0
105}
106
107func main(argc: i64, argv: *i64) -> i64 {
108 var ph: i64 = 111 // 'o' -- default phase is the safe control
109 var ph2: i64 = 0
110 if argc >= 2 {
111 let a: *u8 = argv[1] as *u8
112 ph = a[0] as i64
113 ph2 = a[1] as i64
114 }
115 if ph == 97 { // 'a' add
116 let ra: i64 = chk_add_overflow()
117 if ra < 0 { return 0 } // wrapped to MIN: the add executed and wrapped
118 return 1
119 }
120 if ph == 115 { // 's' sub
121 let rs: i64 = ca_sub_overflow()
122 if rs > 0 { return 0 } // wrapped to MAX
123 return 1
124 }
125 if ph == 109 { // 'm' mul / 'mulmin'
126 if ph2 == 117 { // "mu..." -> check third byte: mul vs mulmin
127 let a: *u8 = argv[1] as *u8
128 if a[3] == 109 { // 'mulm'in
129 let rn: i64 = ca_mulmin_overflow()
130 if rn == ca_min() { return 0 } // wrapped back to MIN
131 return 1
132 }
133 let rm: i64 = ca_mul_overflow()
134 if rm == 0 { return 0 } // 2^64 wrapped to 0
135 return 1
136 }
137 return 1
138 }
139 return ca_inrange_control() // 'o' / anything else
140}