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