1open HolKernel Parse boolLib bossLib; 2open mips_decompLib 3 4val () = new_theory "mips_decomp_demo"; 5 6fun mips_decompile_code s = 7 mips_decompLib.mips_decompile s o utilsLib.strings_to_quote o 8 List.map mips.encodeInstruction o helperLib.quote_to_strings 9 10val (test1_cert, test1_def) = mips_decompile_code "test1" 11 `ori $r1, $r0, 10 12 bne $r1, $r0, 0x3FFFC 13 daddiu $r1, $r1, 0xFFFF` 14 15val (test2_cert, test2_def) = mips_decompile_code "test2" 16 `ori $r1, $r0, 10 17 beq $r1, $r0, 4 18 nop` 19 20val (test3_cert, test3_def) = mips_decompile_code "test3" 21 `abs.d $f2, $f2 22 sqrt.d $f1, $f2 23 neg.d $f2, $f1 24 mov.d $f1, $f2 25 add.d $f3, $f1, $f2 26 sub.d $f1, $f2, $f3 27 mul.d $f1, $f1, $f1 28 div.d $f2, $f2, $f1 29 madd.d $f2, $f1, $f2, $f3 30 round.l.d $f4, $f2 31 trunc.l.d $f5, $f2 32 ceil.l.d $f6, $f2 33 floor.l.d $f6, $f2 34 c.eq.d $f1, $f2` 35 36(* These decompile under the assumption that arithmetic exceptions do not 37 occur *) 38 39val (test4_cert, test4_def) = mips_decompile_code "test4" 40 `dadd $r1, $r2, $r3 41 dmult $r1, $r3` 42 43val () = computeLib.add_funs [test1_def, test2_def, test3_def, test4_def, 44 mipsTheory.IntToDWordMIPS_def] 45 46val run1 = Theory.save_thm("run1", 47 EVAL ``test1 0w`` 48 ) 49 50val run2 = Theory.save_thm("run2", 51 EVAL ``test2 0w`` 52 ) 53 54val run3 = Theory.save_thm("run3", 55 EVAL ``test3 (0w, int_to_fp64 roundTiesToEven (-4), 0w)`` 56 ) 57 58val run4 = Theory.save_thm("run4", 59 EVAL ``test4 (0w, 2w, 4w)`` 60 ) 61 62val () = export_theory() 63