| import WordDialect |
| import WordIR |
| import Forth |
| import BCPL |
| import Wolfram |
|
|
| /-! |
| # Harness |
|
|
| Shared differential-testing harness for every backend. A backend supplies a `Runner`: it takes a |
| `Sample` (an IR program plus initial memory and register-file size), runs it on the real target, |
| and reports either the dumped final state or the exit code of a trap. The harness runs the same IR |
| program under the Lean semantics (`WordDialect.run`) and compares. |
|
|
| Trap exit codes are common to all backends: 1 stackUnderflow, 2 badAddress, 3 divideByZero, |
| 4 badPc, 5 returnUnderflow; 6 is a target stack overflow, which has no IR counterpart. On halt a backend writes, as raw little-endian 64-bit words, the data |
| stack depth, the data stack (top first), the IR memory and the virtual registers. |
| -/ |
|
|
| open WordDialect |
|
|
| structure Sample where |
| name : String |
| prog : Prog 64 |
| mem : List Nat |
| nregs : Nat := 4 |
| /-- Set when the sample could not be built (e.g. Forth source failed to parse); `check` |
| then reports an error instead of running anything. -/ |
| buildError : Option String := none |
|
|
| def mkMem (img : List Nat) : Memory 64 := Memory.ofImage img |
|
|
| inductive Result where |
| | halted (stack mem regs : List Nat) |
| | trap (code : Nat) |
| | timeout |
| deriving BEq, Repr |
|
|
| /-- Expected result under the Lean semantics. -/ |
| def trapCode : Trap → Nat |
| | .stackUnderflow => 1 |
| | .badAddress => 2 |
| | .divideByZero => 3 |
| | .badPc => 4 |
| | .returnUnderflow => 5 |
|
|
| def expected (s : Sample) : Result := |
| match run s.prog 200000 (State.init (mkMem s.mem)) with |
| | none => .timeout |
| | some (.trapped t) => .trap (trapCode t) |
| | some (.next _) => .timeout |
| | some (.halted st) => |
| .halted (st.dstack.map (·.toNat)) |
| ((List.range s.mem.length).map fun a => (st.mem.cell (BitVec.ofNat 64 a)).toNat) |
| ((List.range s.nregs).map fun r => (st.regs r).toNat) |
|
|
| def u64 (b : ByteArray) (off : Nat) : Nat := |
| (List.range 8).foldl (fun acc i => acc + (b.get! (off + i)).toNat * 2 ^ (8 * i)) 0 |
|
|
| partial def readAll (h : IO.FS.Handle) (acc : ByteArray) : IO ByteArray := do |
| let chunk ← h.read 65536 |
| if chunk.isEmpty then pure acc else readAll h (acc ++ chunk) |
|
|
| def parseDump (s : Sample) (b : ByteArray) : Option Result := |
| if b.size < 8 then none else |
| let depth := u64 b 0 |
| let m := s.mem.length |
| if b.size != 8 + 8 * depth + 8 * m + 8 * s.nregs then none else |
| some (.halted ((List.range depth).map fun i => u64 b (8 + 8 * i)) |
| ((List.range m).map fun i => u64 b (8 + 8 * depth + 8 * i)) |
| ((List.range s.nregs).map fun i => u64 b (8 + 8 * depth + 8 * m + 8 * i))) |
|
|
| /-- A backend: run a sample on the real target. -/ |
| abbrev Runner := Sample → IO (Except String Result) |
|
|
| def check (run : Runner) (s : Sample) : IO Bool := do |
| if let some e := s.buildError then |
| IO.println s!"ERROR {s.name}: {e}"; return false |
| let exp := expected s |
| match exp with |
| | .timeout => IO.println s!"SKIP {s.name} (IR did not terminate within fuel)"; return true |
| | _ => |
| match ← run s with |
| | .error e => IO.println s!"ERROR {s.name}: {e}"; return false |
| | .ok got => |
| if got == exp then |
| IO.println s!"PASS {s.name} {repr exp}"; return true |
| else |
| IO.println s!"FAIL {s.name}\n lean: {repr exp}\n target: {repr got}"; return false |
|
|
| /-! ## Programs from the frontends -/ |
|
|
| /-- Registers a compiled Forth program may use: the double-cell words keep their loop state |
| in virtual registers `0 … 7` (`Forth.Double`); other Forth code uses none. -/ |
| def forthRegs : Nat := 8 |
|
|
| def forthSample (name : String) (b : Forth.Block) (mem : List Nat := List.replicate 16 0) : Sample := |
| { name, prog := Forth.compileProgram b, mem, nregs := forthRegs } |
|
|
| /-- A sample written as Forth source text. A parse failure becomes a reported error. The memory |
| image is extended with zero cells if the program's `VARIABLE`s (cells `0 … vars - 1`) need more. -/ |
| def forthTextSample (name : String) (src : String) (mem : List Nat := List.replicate 16 0) : |
| Sample := |
| match Forth.parse src with |
| | .ok P => { name, prog := P.compile, mem := mem ++ List.replicate (P.vars - mem.length) 0, |
| nregs := forthRegs } |
| | .error e => { name, prog := [], mem, buildError := some s!"Forth parse error: {e}" } |
|
|
| open Forth in |
| def forthOps (ops : List Op) : Block := ops.foldr (fun o b => .op o b) .nil |
|
|
| def bcplAddr : BCPL.Var → Word 64 := fun x => BitVec.ofNat 64 x |
|
|
| def samplesFrontends : List Sample := |
| open Forth in |
| [ forthSample "forth_five_dup_plus" Forth.fiveDupPlus |
| , forthSample "forth_countdown" |
| (.op (.lit 10) (.untilL (forthOps [.lit 1, .sub, .dup, .lit 0, .eq]) .nil)) |
| , forthSample "forth_if_else" (.op (.lit 3) (.op (.lit 5) (.op .lt (.ite (.op (.lit 111) .nil) (.op (.lit 222) .nil) .nil)))) |
| , forthSample "forth_store_fetch" (forthOps [.lit 42, .lit 7, .store, .lit 7, .fetch]) |
| , forthSample "forth_sdiv_trunc" (forthOps [.lit (-7), .lit 2, .div]) |
| , forthSample "forth_sdiv_intmin" (forthOps [.lit (-9223372036854775808), .lit (-1), .div]) |
| , forthSample "forth_shifts" (forthOps [.lit 1, .lit 64, .lshift, .lit (-1), .lit 70, .rshift, |
| .lit 255, .lit 3, .rshift, .lit 1, .lit 63, .lshift]) |
| , forthSample "forth_compare_signed" (forthOps [.lit (-1), .lit 1, .lt, .lit (-1), .lit 1, .ult, |
| .lit 5, .lit 5, .eq, .lit 5, .lit 6, .ne]) |
| , forthSample "forth_stack_words" (forthOps [.lit 1, .lit 2, .lit 3, .rot, .over, .swap, .dup, |
| .drop]) |
| , forthSample "forth_trap_div0" (forthOps [.lit 1, .lit 0, .div]) |
| , forthSample "forth_trap_underflow" (forthOps [.add]) |
| , forthSample "forth_trap_badaddr" (forthOps [.lit 1000, .fetch]) |
| , forthTextSample "forth_text_sum_recursive" Forth.sumSrc |
| , forthTextSample "forth_text_fib_recursive" |
| ": FIB ( n -- fib[n] ) DUP 2 < IF ELSE DUP 1 - FIB SWAP 2 - FIB + THEN ;\n15 FIB" |
| , forthTextSample "forth_text_gcd_words" |
| ": MOD ( a b -- a mod b ) OVER OVER / * - ;\n\ |
| : GCD ( a b -- g ) BEGIN SWAP OVER MOD DUP 0 = UNTIL DROP ;\n\ |
| 1071 462 GCD 3 ! 3 @ \\ store the result at address 3, read it back" |
| , forthTextSample "forth_text_trap_in_word" ": INNER 1 0 / ; : OUTER 7 INNER 8 ; 5 OUTER" |
| , forthTextSample "forth_text_mod_zeq" |
| "-7 2 MOD 7 -2 MOD -7 -2 MOD 9223372036854775807 10 MOD\n\ |
| -9223372036854775808 -1 MOD 0 0= 5 0= -1 0=" |
| , forthTextSample "forth_text_trap_mod0" "5 1 0 MOD" |
| , forthTextSample "forth_text_variables" |
| "VARIABLE N VARIABLE ACC 100 CONSTANT LIMIT\n\ |
| : STEP ( -- ) ACC @ N @ + ACC ! N @ 1 + N ! ;\n\ |
| 0 N ! 0 ACC ! BEGIN STEP N @ LIMIT > UNTIL ACC @ N @" |
| , forthTextSample "forth_text_many_variables" |
| "VARIABLE A0 VARIABLE A1 VARIABLE A2 VARIABLE A3 VARIABLE A4 VARIABLE A5 VARIABLE A6\n\ |
| VARIABLE A7 VARIABLE A8 VARIABLE A9 VARIABLE A10 VARIABLE A11 VARIABLE A12 VARIABLE A13\n\ |
| VARIABLE A14 VARIABLE A15 VARIABLE A16 VARIABLE A17 VARIABLE A18 VARIABLE A19\n\ |
| 77 A19 ! -5 A0 ! A19 @ A0 @ + A19" |
| , forthTextSample "forth_text_exit_recursive" |
| ": GCD ( a b -- g ) DUP 0= IF DROP EXIT THEN SWAP OVER MOD RECURSE ;\n\ |
| : SUM ( n -- 0+...+n ) DUP 0= IF EXIT THEN DUP 1 - RECURSE + ;\n\ |
| 1071 462 GCD 20 SUM" |
| , forthTextSample "forth_text_exit_dead_code" ": F 1 EXIT 2 3 ; : G F F + EXIT F ; G" |
| , forthTextSample "forth_text_do_loop_sum" "0 10 0 DO I + LOOP 0 1 0 DO I 7 + + LOOP" |
| , forthTextSample "forth_text_nested_loops" "0 3 0 DO 4 0 DO I J * + LOOP LOOP" |
| , forthTextSample "forth_text_rstack_across_call" |
| ": BUMP ( R: x -- x+1 ) R> 1 + >R ; : PEEK R@ ; 5 >R BUMP BUMP PEEK R>" |
| , forthTextSample "forth_text_rstack_recursive" |
| ": SUMR ( n -- 0+...+n ) DUP 0= IF EXIT THEN DUP >R 1 - RECURSE R> + ;\n10 SUMR" |
| , forthTextSample "forth_text_trap_fromr_empty" "1 2 R>" |
| , forthTextSample "forth_text_trap_rfetch_empty" "1 >R R> R@" |
| , forthTextSample "forth_text_loop_calls_loop" |
| ": TRI ( n -- 0+...+n-1 ) 0 SWAP 0 DO I + LOOP ;\n0 6 1 DO I TRI + LOOP 4 TRI" |
| , forthTextSample "forth_text_loop_exit" |
| ": FIND3 10 0 DO I 3 = IF I EXIT THEN LOOP 99 ; FIND3 R> R>" |
| , forthTextSample "forth_text_loop_recursive" |
| ": F ( acc n -- acc' ) DUP IF DUP 0 DO SWAP I + SWAP LOOP 1 - RECURSE ELSE DROP THEN ;\n\ |
| 0 3 F" |
| , forthTextSample "forth_text_trap_do_underflow" "1 DO LOOP" |
| , forthTextSample "forth_text_trap_loop_rdrop" "3 0 DO R> DROP LOOP" |
| , forthTextSample "forth_text_trap_j_outside" "1 >R 2 >R J" |
| , forthTextSample "forth_text_plus_loop_up" "0 10 0 DO I + 2 +LOOP 0 10 0 DO I + 3 +LOOP" |
| , forthTextSample "forth_text_plus_loop_down" "0 0 10 DO I + -1 +LOOP 0 -5 5 DO I + -2 +LOOP" |
| , forthTextSample "forth_text_plus_loop_wrap" |
| "0 9223372036854775807 9223372036854775805 DO 1 + 1 +LOOP 0 0 -2 DO 1 + 1 +LOOP" |
| , forthTextSample "forth_text_qdo" "0 5 5 ?DO 1 + LOOP 0 3 0 ?DO 1 + LOOP 0 4 4 ?DO 1 + 2 +LOOP" |
| , forthTextSample "forth_text_leave" "100 0 DO I 5 > IF I LEAVE THEN LOOP 0 4 0 DO 1 + LEAVE LOOP" |
| , forthTextSample "forth_text_leave_nested" |
| "0 4 0 DO 2 0 DO BEGIN LEAVE 1 UNTIL LOOP 1 + LOOP 0 10 0 DO I 3 = IF LEAVE THEN 1 + 2 +LOOP" |
| , forthTextSample "forth_text_unloop_exit" |
| ": FIND7 20 0 DO I 7 = IF I UNLOOP EXIT THEN LOOP 99 ; FIND7 FIND7 +" |
| , forthTextSample "forth_text_trap_plus_loop_nostep" "3 0 DO +LOOP" |
| , forthTextSample "forth_text_trap_plus_loop_rdrop" "3 0 DO R> DROP 1 +LOOP" |
| , forthTextSample "forth_text_trap_leave_rdrop" "3 0 DO R> DROP LEAVE LOOP" |
| , forthTextSample "forth_text_trap_unloop_empty" "1 UNLOOP" |
| , forthTextSample "forth_text_while_gcd" ": GCD BEGIN DUP WHILE SWAP OVER MOD REPEAT DROP ; 1071 462 GCD" |
| , forthTextSample "forth_text_while_zero_times" "7 BEGIN 0 WHILE 1 + REPEAT 8" |
| , forthTextSample "forth_text_while_count" "0 BEGIN DUP 5 < WHILE 1 + REPEAT" |
| , forthTextSample "forth_text_while_exit" ": F 0 BEGIN 1 + DUP 3 = IF EXIT THEN -1 WHILE REPEAT 99 ; F" |
| , forthTextSample "forth_text_while_leave" "0 10 0 DO BEGIN -1 WHILE LEAVE REPEAT 1 + LOOP" |
| , forthTextSample "forth_text_trap_while_underflow" "BEGIN WHILE REPEAT" |
| , forthTextSample "forth_text_pairs" "1 2 3 4 2SWAP 5 6 2DUP 2DROP" |
| , forthTextSample "forth_text_divmod" "-7 2 /MOD 7 -2 /MOD 7 2 /MOD" |
| , forthTextSample "forth_text_negate_abs" "5 NEGATE -9 ABS 9 ABS -9223372036854775808 ABS" |
| , forthTextSample "forth_text_min_max" "3 -4 MIN 3 -4 MAX -1 1 MIN -1 1 MAX" |
| , forthTextSample "forth_text_qdup" "0 ?DUP 6 ?DUP" |
| , forthTextSample "forth_text_case" |
| ": C CASE 1 OF 100 ENDOF 2 OF 200 ENDOF DUP 1000 + SWAP ENDCASE ; 1 C 2 C 7 C" |
| , forthTextSample "forth_text_create_comma" "CREATE T 10 , 20 , 30 , T 1 + @ T 2 + @" |
| , forthTextSample "forth_text_allot" "CREATE B 3 ALLOT VARIABLE X 9 X ! X @ X" |
| , forthTextSample "forth_text_trap_divmod0" "1 0 /MOD" |
| , forthTextSample "forth_text_trap_twoswap" "1 2 3 2SWAP" |
| , forthTextSample "forth_text_um_star" "7 6 UM* -1 -1 UM* -1 2 UM*" |
| , forthTextSample "forth_text_um_divmod" "-2 3 7 UM/MOD 0 1 3 UM/MOD 5 0 2 UM/MOD" |
| , forthTextSample "forth_text_m_star" |
| "-3 7 M* -3 -7 M* -9223372036854775808 -9223372036854775808 M* 9223372036854775807 2 M*" |
| , forthTextSample "forth_text_sm_rem" |
| "7 0 2 SM/REM -7 -1 2 SM/REM 7 0 -2 SM/REM -7 -1 -2 SM/REM -9223372036854775808 -1 1 SM/REM" |
| , forthTextSample "forth_text_star_slash" |
| "6 7 4 */MOD -6 7 4 */ 4611686018427387904 4 8 */ -9223372036854775808 -1 -1 */" |
| , forthTextSample "forth_text_trap_um_divmod_overflow" "0 5 5 UM/MOD" |
| , forthTextSample "forth_text_trap_sm_rem_overflow" "-9223372036854775808 -1 -1 SM/REM" |
| , forthTextSample "forth_text_trap_star_slash0" "1 2 0 */" |
| , forthTextSample "forth_text_trap_star_slash_overflow" "4611686018427387904 4 2 */" |
| , forthTextSample "forth_text_trap_star_slash_underflow" "1 2 */MOD" |
| , forthTextSample "forth_text_fm_mod" |
| "7 0 2 FM/MOD -7 -1 2 FM/MOD 7 0 -2 FM/MOD -7 -1 -2 FM/MOD -8 -1 2 FM/MOD 1 -1 2 FM/MOD" |
| , forthTextSample "forth_text_trap_fm_mod_overflow" "-1 -2 2 FM/MOD" |
| , forthTextSample "forth_text_trap_fm_mod0" "5 0 0 FM/MOD" |
| , { name := "bcpl_sum_1_to_10", mem := List.replicate 4 0, |
| prog := BCPL.compileProgram bcplAddr |
| (.seq (.assign (.var 1) (.num 10)) (.seq (.assign (.var 0) (.num 0)) |
| (.while (.bin .ne (.var 1) (.num 0)) |
| (.seq (.assign (.var 0) (.bin .add (.var 0) (.var 1))) |
| (.assign (.var 1) (.bin .sub (.var 1) (.num 1))))))) } |
| , { name := "bcpl_indirect", mem := List.replicate 8 0, |
| prog := BCPL.compileProgram bcplAddr |
| (.seq (.assign (.var 0) (.addrOf 5)) |
| (.seq (.assign (.rv (.var 0)) (.num 77)) |
| (.assign (.var 1) (.bin .add (.rv (.var 0)) (.num 1))))) } |
| , { name := "wolfram_dot_2x2", nregs := 4, |
| mem := [1, 2, 3, 4, 5, 6, 7, 8, 0, 0, 0, 0], |
| prog := (Wolfram.dotFrag 2 2 2 0 4 8 : IR.Frag 64).emit 0 ++ [.halt] } |
| , { name := "wolfram_dot_3x2_2x4", nregs := 4, |
| mem := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], |
| prog := (Wolfram.dotFrag 3 2 4 0 6 14 : IR.Frag 64).emit 0 ++ [.halt] } |
| ] |
|
|
| /-! ## Hand-written IR covering control flow and calls -/ |
|
|
| def samplesRaw : List Sample := |
| [ { name := "raw_call_ret", mem := [], nregs := 1, |
| prog := [.word 5, .call 4, .call 4, .halt, .dup, .add, .ret] } |
| , { name := "raw_trap_ret_empty", mem := [], nregs := 1, prog := [.ret] } |
| , { name := "raw_trap_badpc", mem := [], nregs := 1, prog := [.word 1, .jmp 100] } |
| , { name := "raw_rotates", mem := [], nregs := 1, |
| prog := [.word 0x8000000000000001, .word 1, .rotl, .word 0x8000000000000001, .word 1, .rotr, |
| .word 3, .word 130, .rotl, .halt] } |
| , { name := "raw_select_regs", mem := [], nregs := 3, |
| prog := [.word 9, .pop 2, .word 11, .word 22, .word 0, .select, .push 2, .word 11, |
| .word 22, .word 1, .select, .halt] } |
| ] |
|
|
| /-! ## Randomised differential testing -/ |
|
|
| def edge : Array Nat := |
| #[0, 1, 2, 3, 7, 63, 64, 65, 127, 128, 255, 2 ^ 63 - 1, 2 ^ 63, 2 ^ 63 + 1, 2 ^ 64 - 1, |
| 2 ^ 64 - 2, 0xdeadbeef, 0x123456789abcdef0] |
|
|
| def randWord : IO Nat := do |
| let k ← IO.rand 0 3 |
| if k = 0 then |
| let hi ← IO.rand 0 (2 ^ 32 - 1) |
| let lo ← IO.rand 0 (2 ^ 32 - 1) |
| pure (hi * 2 ^ 32 + lo) |
| else |
| let i ← IO.rand 0 (edge.size - 1) |
| pure edge[i]! |
|
|
| def conds : Array Cond := #[.eq, .ne, .ult, .ule, .ugt, .uge, .slt, .sle, .sgt, .sge] |
|
|
| def genInstr (depth : Nat) : IO (List (Instr 64) × Int) := do |
| let r ← IO.rand 0 99 |
| if depth < 2 && r >= 6 then |
| let k ← IO.rand 0 2 |
| if k = 0 then do let w ← randWord; return ([.word (BitVec.ofNat 64 w)], 1) |
| else if k = 1 then do let q ← IO.rand 0 3; return ([.push q], 1) |
| else do let w ← randWord; return ([.word (BitVec.ofNat 64 w)], 1) |
| else |
| let k ← IO.rand 0 30 |
| match k with |
| | 0 => do let w ← randWord; return ([.word (BitVec.ofNat 64 w)], 1) |
| | 1 => return ([.add], -1) | 2 => return ([.sub], -1) | 3 => return ([.mul], -1) |
| | 4 => return ([.and], -1) | 5 => return ([.or], -1) | 6 => return ([.xor], -1) |
| | 7 => return ([.not], 0) |
| | 8 => return ([.shl], -1) | 9 => return ([.shr], -1) |
| | 10 => return ([.rotl], -1) | 11 => return ([.rotr], -1) |
| | 12 => return ([.div], -1) | 13 => return ([.sdiv], -1) |
| | 14 => do let c ← IO.rand 0 9; return ([.cmp (conds[c]?.getD .eq)], -1) |
| | 15 => return ([.select], -2) |
| | 16 => return ([.dup], 1) | 17 => return ([.drop], -1) | 18 => return ([.swap], 0) |
| | 19 => return ([.over], 1) | 20 => return ([.rot], 0) |
| | 21 => do let q ← IO.rand 0 3; return ([.push q], 1) |
| | 22 => do let q ← IO.rand 0 3; return ([.pop q], -1) |
| | 23 => do let v ← randWord; let a ← IO.rand 0 17 |
| return ([.word (BitVec.ofNat 64 v), .word (BitVec.ofNat 64 a), .store], 0) |
| | 24 => do let a ← IO.rand 0 17; return ([.word (BitVec.ofNat 64 a), .load], 1) |
| | 25 => do let v ← randWord; return ([.word (BitVec.ofNat 64 v), .word 0, .select], 0) |
| | 26 => return ([.tor], -1) | 27 => return ([.fromr], 1) | 28 => return ([.rfetch], 1) |
| | _ => do let w ← randWord; return ([.word (BitVec.ofNat 64 w)], 1) |
|
|
| def genProg (len : Nat) : IO (List (Instr 64)) := do |
| let mut code : List (Instr 64) := [] |
| let mut depth : Int := 0 |
| for _ in List.range len do |
| let (is, d) ← genInstr depth.toNat |
| code := code ++ is |
| depth := max 0 (depth + d) |
| -- a few forward jumps / conditional branches |
| let n := code.length |
| for _ in List.range 2 do |
| let k ← IO.rand 0 (n - 1) |
| let skip ← IO.rand 1 4 |
| let kind ← IO.rand 0 1 |
| if kind = 0 then |
| code := code.set k (.jmp (min n (k + 1 + skip))) |
| else |
| code := code.set k (.branch (min n (k + 1 + skip))) |
| return code ++ [.halt] |
|
|
| def fuzz (run : Runner) (count : Nat) : IO Bool := do |
| let mut ok := true |
| let mut skipped := 0 |
| let mut halts := 0 |
| let mut traps : Array Nat := #[0, 0, 0, 0, 0, 0] |
| let mut longest := 0 |
| for i in List.range count do |
| let len ← IO.rand 4 40 |
| let prog ← genProg len |
| let mem ← (List.range 16).mapM fun _ => randWord |
| let s : Sample := { name := s!"fuzz_{i}", prog, mem, nregs := 4 } |
| let exp := expected s |
| match exp with |
| | .halted st _ _ => halts := halts + 1; longest := max longest st.length |
| | .trap c => traps := traps.set! c (traps[c]! + 1) |
| | .timeout => pure () |
| if exp == .timeout then skipped := skipped + 1 else |
| match ← run s with |
| | .error e => IO.println s!"ERROR fuzz_{i}: {e}"; ok := false |
| | .ok got => |
| if got != exp then |
| IO.println s!"FAIL fuzz_{i}\n lean: {repr exp}\n target: {repr got}" |
| ok := false |
| IO.println s!"fuzz: {count} programs, {skipped} skipped; halted {halts}; traps by code (1 underflow, 2 badaddr, 3 div0, 4 badpc, 5 ret) {traps.toList.drop 1}; max final depth {longest}; {if ok then "all agree" else "MISMATCH"}" |
| return ok |
|
|
| def allSamples : List Sample := samplesFrontends ++ samplesRaw |
|
|
| /-- Run every sample and `count` random programs against a backend. -/ |
| def checkAll (run : Runner) (count : Nat) : IO Bool := do |
| IO.setRandSeed 20260610 |
| let mut ok := true |
| for s in allSamples do |
| if !(← check run s) then ok := false |
| if !(← fuzz run count) then ok := false |
| return ok |
|
|
