"""Compare zero-vector CFG facts and store addressing with native ARM64 fixtures."""
import json
import struct
import subprocess
import sys
from pathlib import Path
ROOT=Path(__file__).resolve().parents[1];sys.path.insert(0,str(ROOT/'tools'))
from a64_program import ProgramCompiler
from a64_lift import UnsupportedInstruction
OUT=ROOT/'build/zero-vectors';OUT.mkdir(parents=True,exist_ok=True)
def body(words):return struct.pack('<'+'I'*len(words),*words)
def run(*args):subprocess.run(list(map(str,args)),cwd=ROOT,check=True)
def zero(register):return 0x6f00e400|register
def single(register,offset,mode=0):return 0x3c800000|((offset&511)<<12)|(mode<<10)|register
def pair(first,second,offset,mode=2):return 0xac000000|(mode<<23)|(((offset//16)&127)<<15)|(second<<10)|first
fixtures={
 'unscaled':[zero(31),single(31,-256),single(31,255),0xd65f03c0],
 'scaled':[zero(1),0x3d800000|(63<<10)|1,0xd65f03c0],
 'prepost':[zero(0),single(0,-32,3),single(0,64,1),0xd65f03c0],
 'pair':[zero(0),zero(31),pair(0,31,-1024),pair(31,0,1008),0xd65f03c0],
 'pairprepost':[zero(1),zero(31),pair(1,31,-32,3),pair(31,1,64,1),0xd65f03c0],
 'branch':[zero(0),0x14000001,0x91000408,single(0,0),0xd65f03c0],
 'merge':[0xb4000061,zero(0),0x14000002,zero(0),single(0,0),0xd65f03c0],
 'loop':[zero(0),single(0,0),0x91000421,0xf100103f,0x54ffffa3,0xd65f03c0]}
assembly=['.text','.p2align 2']
for name,words in fixtures.items():
    (OUT/f'{name}.wat').write_text(ProgramCompiler().compile({0x1000:body(words)},0x1000))
    run(ROOT/'build/wabt/wat2wasm',OUT/f'{name}.wat','-o',OUT/f'{name}.wasm')
    run(ROOT/'build/wabt/wasm2c',OUT/f'{name}.wasm','-o',OUT/f'{name}.c','--module-name='+name)
    assembly += [f'.globl _native_{name}',f'_native_{name}:',*[f'.long 0x{word:08x}' for word in words]]
(OUT/'oracle.S').write_text('\n'.join(assembly)+'\n')
invalid=[([zero(0),pair(0,1,0),0xd65f03c0],{}),
         ([zero(0),0x9400003f,single(0,0),0xd65f03c0],{0x1100:'clobber'}),
         ([zero(0),pair(0,0,0,0),0xd65f03c0],{}),
         ([zero(0),single(0,0,2),0xd65f03c0],{})]
for words,hosts in invalid:
    try:ProgramCompiler(hosts).compile({0x1000:body(words)},0x1000)
    except UnsupportedInstruction:pass
    else:raise AssertionError('Invalid vector facts/access accepted')
includes='\n'.join(f'#include "{name}.h"\nextern uint8_t *native_{name}(uint8_t *,uint64_t);' for name in fixtures)
checks=[]
for name in fixtures:
    checks.append(f'''
 {{ w2c_{name} module;wasm2c_{name}_instantiate(&module);
 uint8_t *memory=w2c_{name}_memory(&module)->data;
 for(unsigned i=0;i<512;++i) {{
  uint8_t expected[4096];memset(expected,i&255,sizeof(expected));
  memset(memory,0xa5,65536);memset(memory+16384,i&255,sizeof(expected));
  uint64_t registers[32]={{0}};registers[0]=16384+1024;registers[1]=i%2;
  memcpy(memory,registers,sizeof(registers));
  uint8_t *result=native_{name}(expected+1024,i%2);
  assert(w2c_{name}_run(&module,0,1000)==0);
  uint64_t returned;memcpy(&returned,memory,8);
  assert(returned==16384+(uint64_t)(result-expected));
  assert(memcmp(memory+16384,expected,sizeof(expected))==0);
  for(unsigned j=256;j<65536;++j) {{if(j>=16384 && j<20480)continue;assert(memory[j]==0xa5);}}
 }}
 wasm2c_{name}_free(&module); }}''')
(OUT/'verify.c').write_text(f'''
#include <assert.h>
#include <stdint.h>
#include <stdio.h>
#include <string.h>
{includes}
int main(void) {{wasm_rt_init();{''.join(checks)}wasm_rt_free();
puts("PASS: 4096 native zero-vector store comparisons, pairs, writeback, negative offsets, branches, merges, loops and 4 rejection cases");}}
''')
runtime=ROOT/'third_party/wabt/wasm2c'
run('xcrun','clang','-O2','-DWASM_RT_USE_MMAP=0','-DWASM_RT_MEMCHECK_BOUNDS_CHECK=1',
    '-I'+str(OUT),'-I'+str(runtime),*[OUT/f'{name}.c' for name in fixtures],OUT/'verify.c',OUT/'oracle.S',
    runtime/'wasm-rt-impl.c',runtime/'wasm-rt-mem-impl.c','-o',OUT/'verify')
run(OUT/'verify')
(OUT/'verification.json').write_text(json.dumps({'status':'pass','native_comparisons':4096,
    'fixtures':list(fixtures),'invalid_cases':4,'scope':'hand-authored zero-vector fixtures'},indent=2)+'\n')