nx_option_enforce_ok.nx source
↩ module page · 107 lines · 3861 B
1// nx_option_enforce_ok.nx -- LN2 POSITIVE CONTROL: every narrowing idiom the mode recognises, in one
2// program that must compile under `--optenforce` AND run to exit 0 under both modes. A deny mode
3// that refuses everything fails HERE, and a mode that missed one idiom would refuse real code.
4// I1 `if p == 0 { return }` early exit -> p non-null for the rest of the block
5// I2 `if p != 0 { ... }` -> non-null inside the then-block
6// I3 `if (p as i64) == 0 { return }` -> the cast-shaped early exit
7// I4 `while q != (0 as *OkNode) { ... }` -> non-null inside the body
8// I5 `if p == 0 { } else { ... }` -> non-null inside the else-block
9// I6 nx_assert_ptr(p as *u8, "...") -> non-null for the rest of the block
10// I7 `let s = &local` -> bound non-null, no guard needed
11// I8 a `var` pointer re-checked after reassignment
12// I9 the write legs: `p.f = v`, `*p = v` after a guard
13// license_tier: ORIGINAL No hw writes (Rule 26).
14import "nx_syscalls.nx"
15import "nx_assert.nx"
16
17struct OkNode {
18 val: i64,
19 next: *OkNode,
20}
21
22func ok_make(v: i64, nxt: *OkNode) -> *OkNode {
23 let n: *OkNode = sys_mmap(16) as *OkNode
24 n.val = v
25 n.next = nxt
26 return n
27}
28func ok_maybe(k: i64) -> *OkNode {
29 if k == 0 { return 0 as *OkNode }
30 return ok_make(k, 0 as *OkNode)
31}
32
33func i1_early_exit(k: i64) -> i64 {
34 let p: *OkNode = ok_maybe(k)
35 if p == 0 { return 0 - 1 }
36 return p.val // I1
37}
38func i2_then_block(k: i64) -> i64 {
39 let p: *OkNode = ok_maybe(k)
40 var r: i64 = 0 - 1
41 if p != 0 { r = p.val } // I2
42 return r
43}
44func i3_cast_exit(k: i64) -> i64 {
45 let p: *OkNode = ok_maybe(k)
46 if (p as i64) == 0 { return 0 - 1 }
47 return p.val // I3
48}
49func i4_while_walk(k: i64) -> i64 {
50 let head: *OkNode = ok_make(1, ok_make(2, ok_make(3, 0 as *OkNode)))
51 var q: *OkNode = head
52 var sum: i64 = 0
53 while q != (0 as *OkNode) { // I4
54 sum = sum + q.val
55 q = q.next
56 }
57 return sum + k - k
58}
59func i5_else_block(k: i64) -> i64 {
60 let p: *OkNode = ok_maybe(k)
61 var r: i64 = 0 - 1
62 if p == 0 { r = 0 - 1 } else { r = p.val } // I5
63 return r
64}
65func i6_assert(k: i64) -> i64 {
66 let p: *OkNode = ok_maybe(k)
67 nx_assert_ptr(p as *u8, "i6: k is never 0 here" as *u8)
68 return p.val // I6
69}
70func i7_addr_of() -> i64 {
71 var x: i64 = 5
72 let s: *i64 = &x
73 return *s // I7 (bound non-null)
74}
75func i8_var_recheck(k: i64) -> i64 {
76 var p: *OkNode = ok_maybe(k)
77 if p == 0 { return 0 - 1 }
78 let first: i64 = p.val
79 p = ok_maybe(k + 1) // reassigned: nullable again
80 if p == 0 { return 0 - 1 }
81 return first + p.val // I8 (re-checked)
82}
83func i9_writes(k: i64) -> i64 {
84 let p: *OkNode = ok_maybe(k)
85 if p == 0 { return 0 - 1 }
86 p.val = p.val + 10 // I9 field write
87 var x: i64 = 0
88 let px: *i64 = &x
89 *px = p.val // I9 star write through a non-null local
90 return x
91}
92
93func main(argc: i64, argv: *i64) -> i64 {
94 let k: i64 = argc + 6 // 7 with no args: never 0
95 var bad: i64 = 0
96 if i1_early_exit(k) != k { bad = bad + 1 }
97 if i2_then_block(k) != k { bad = bad + 1 }
98 if i3_cast_exit(k) != k { bad = bad + 1 }
99 if i4_while_walk(k) != 6 { bad = bad + 1 }
100 if i5_else_block(k) != k { bad = bad + 1 }
101 if i6_assert(k) != k { bad = bad + 1 }
102 if i7_addr_of() != 5 { bad = bad + 1 }
103 if i8_var_recheck(k) != k + k + 1 { bad = bad + 1 }
104 if i9_writes(k) != k + 10 { bad = bad + 1 }
105 if bad != 0 { return 1 }
106 return 0
107}