nx_cap_detect_ir_gate_t278.nx source

1// nx_cap_detect_ir_gate_t278.nx -- Analyzes IR code to detect memory access ranges and verifies safety properties against allocated memory. 2import "nx_syscalls.nx" 3import "nx_tokenizer.nx" 4import "nx_parse.nx" 5import "nx_cap_detect_ir_candidate_t278.nx" 6func jc_test_puts(s:*u8)->i64{var n:i64=0;while s[n]!=(0 as u8){n=n+1};return sys_write(1,s,n)} 7func main()->i64{ 8 let src:*u8="const CAP:i64=64\nfunc sys_mmap(n:i64)->*u8{return 0 as *u8}\nfunc bad()->i64{let p:*u8=sys_mmap(CAP);let q:*u8=p;q[64]=1 as u8;return 0}\nfunc safe()->i64{let p:*u8=sys_mmap(64);p[63]=1 as u8;return 0}\nfunc wide()->i64{let p:*u8=sys_mmap(CAP);let q:*i64=p as *i64;q[8]=1;return 0}\nfunc dynamic(n:i64)->i64{let p:*u8=sys_mmap(n);p[0]=1 as u8;return 0}\nfunc variable(i:i64)->i64{let p:*u8=sys_mmap(CAP);p[i]=1 as u8;return 0}\n" 9 var n:i64=0;while src[n]!=(0 as u8){n=n+1} 10 let toks:*Tok=lex_source(src,n+2);let m:*Module=parse_module(toks,0 as *Module) 11 if m==(0 as *Module){return 1} 12 // The allocation stub is trusted only for this parser fixture, not as a runtime allocator proof. 13 var allocator:*Function=0 as *Function 14 var ai:i64=0 15 while ai<m.n_functions{ 16 let af:*Function=((m.functions as i64)+ai*NX_MODULE_FN_STRIDE) as *Function 17 var ab:i64=0 18 while ab<af.n_blocks{ 19 var ac:*Instr=block_at(af,ab).head 20 while ac!=(0 as *Instr){ 21 if ac.op==OP_CALL{if jc_ir_name(ac.callee,"sys_mmap")==1{allocator=ac.callee}} 22 ac=ac.next 23 } 24 ab=ab+1 25 } 26 ai=ai+1 27 } 28 if allocator==(0 as *Function){return 5} 29 var fi:i64=0;var bad:i64=0;var good:i64=0;var unknown:i64=0;var untrusted:i64=0 30 let result:*JcIrAccess=sys_mmap(__size_of(JcIrAccess)) as *JcIrAccess 31 while fi<m.n_functions{ 32 let f:*Function=((m.functions as i64)+fi*NX_MODULE_FN_STRIDE) as *Function 33 let rows:*JcIrValue=jc_ir_values(f,allocator) 34 let denied:*JcIrValue=jc_ir_values(f,0 as *Function) 35 var bi:i64=0 36 while bi<f.n_blocks{ 37 let bb:*BasicBlock=block_at(f,bi);var ins:*Instr=bb.head 38 while ins!=(0 as *Instr){ 39 if ins.op==OP_STORE{ 40 let state:i64=jc_ir_store(f,rows,ins,result) 41 if jc_ir_store(f,denied,ins,result)==0{untrusted=untrusted+1} 42 if state==JC_IR_ACCESS_IN_RANGE{good=good+1} 43 if state==JC_IR_ACCESS_OUT_OF_RANGE{bad=bad+1} 44 if state==JC_IR_UNKNOWN{unknown=unknown+1} 45 sys_write(1,f.name_start as *u8,f.name_len) 46 if state==0{sys_write(1," unknown\n",9)} 47 if state==1{sys_write(1," in-range\n",10)} 48 if state==2{sys_write(1," out-of-range\n",14)} 49 } 50 ins=ins.next 51 } 52 bi=bi+1 53 } 54 if rows!=(0 as *JcIrValue){sys_munmap(rows as *u8,f.n_values*__size_of(JcIrValue))} 55 if denied!=(0 as *JcIrValue){sys_munmap(denied as *u8,f.n_values*__size_of(JcIrValue))} 56 fi=fi+1 57 } 58 if bad!=2{return 2};if good!=1{return 3};if unknown!=5{return 4};if untrusted!=8{return 6} 59 let arithmetic:*i64=sys_mmap(8) as *i64 60 if jc_ir_add(JC_IR_I64_MAX,1,arithmetic)!=0{return 7} 61 if jc_ir_add(JC_IR_I64_MIN,0-1,arithmetic)!=0{return 8} 62 if jc_ir_mul(JC_IR_I64_MAX,2,arithmetic)!=0{return 9} 63 sys_munmap(arithmetic as *u8,8) 64 jc_test_puts("IR-FIXTURE PASS explicit allocation identity; no reachability or runtime safety proof\n") 65 return 0 66}