1structure x64_decompLib :> x64_decompLib =
2struct
3
4open HolKernel Parse boolLib bossLib
5open helperLib set_sepTheory addressTheory progTheory wordsTheory wordsLib
6open pred_setTheory combinTheory x64_progTheory listTheory decompilerLib
7
8structure Parse =
9struct
10   open Parse
11   val (Type, Term) = parse_from_grammars x64_progTheory.x64_prog_grammars
12end
13
14open Parse
15
16local
17   val x64_triple = Q.INST [`rip` |-> `p`] o x64_progLib.x64_spec
18   val match_pc_cond = fst o match_term ``x64_PC (if b then x else y)``
19   val lemma1 = prove(``b ==> (x64_PC (if b then x else y) = x64_PC x)``,
20                      SIMP_TAC std_ss []);
21   val lemma2 = prove(``~b ==> (x64_PC (if b then x else y) = x64_PC y)``,
22                      SIMP_TAC std_ss []);
23   val lemma3 = SPEC_MOVE_COND |> GSYM |> REWRITE_RULE [GSYM precond_def]
24   fun get_length th =
25      let
26         val (_,_,c,_) = th |> concl |> dest_spec
27      in
28         c |> rator |> rand |> rand |> listSyntax.dest_list |> fst |> length
29      end
30   val find_exit =
31      stateLib.get_pc_delta
32         (Lib.equal "x64_prog$x64_PC" o fst o boolSyntax.dest_strip_comb)
33   fun finalise th = (th, get_length th, find_exit th)
34in
35   fun x64_triples hex =
36      let
37         val th = x64_triple hex
38         val (th1, th2) =
39            let
40               val m = match_pc_cond (find_term (can match_pc_cond) (concl th))
41               fun fix l = finalise o REWRITE_RULE [lemma3] o
42                           DISCH_ALL o REWRITE_RULE [UNDISCH (INST m l)]
43            in
44               (fix lemma1 th, SOME (fix lemma2 th))
45            end
46            handle HOL_ERR _ => (finalise th, NONE)
47      in
48         (th1, th2)
49      end
50end
51
52fun tools hide =
53   (x64_triples, fn _ => fail(), hide, ``x64_PC``) : decompiler_tools
54
55val x64_tools = tools x64_ALL_EFLAGS_def
56val x64_tools_no_status = tools TRUTH
57
58val x64_decompile = decompilerLib.decompile x64_tools
59
60val x64_decompile_code =
61   decompilerLib.decompile_with x64AssemblerLib.x64_code_no_spaces x64_tools
62
63val x64_decompile_no_status = decompilerLib.decompile x64_tools_no_status
64
65val x64_decompile_no_status_code =
66   decompilerLib.decompile_with x64AssemblerLib.x64_code_no_spaces
67     x64_tools_no_status
68
69
70(* Testing:
71
72val (text_cert, test_def) = x64_decompile_code "test" `add rax, rbx`
73
74val x64_triples = Count.apply x64_triples
75
76  val hex = "55"; x64_triples hex;
77  val hex = "4889E5"; x64_triples hex;
78  val hex = "48897DE8"; x64_triples hex;
79  val hex = "8975E4"; x64_triples hex;
80  val hex = "C745F800000000"; x64_triples hex;
81  val hex = "EB3B"; x64_triples hex;
82  val hex = "8B45F8"; x64_triples hex;
83  val hex = "4863D0"; x64_triples hex;
84  val hex = "488B45E8"; x64_triples hex;
85  val hex = "4801D0"; x64_triples hex;
86  val hex = "0FB600"; x64_triples hex;
87  val hex = "0FBEC0"; x64_triples hex;
88  val hex = "8945FC"; x64_triples hex;
89  val hex = "837DFC60"; x64_triples hex;
90  val hex = "7E1B"; x64_triples hex;
91  val hex = "837DFC7A"; x64_triples hex;
92  val hex = "7F15"; x64_triples hex;
93  val hex = "8B45F8"; x64_triples hex;
94  val hex = "4863D0"; x64_triples hex;
95  val hex = "488B45E8"; x64_triples hex;
96  val hex = "4801C2"; x64_triples hex;
97  val hex = "8B45FC"; x64_triples hex;
98  val hex = "83E820"; x64_triples hex;
99  val hex = "8802"; x64_triples hex;
100  val hex = "8345F801"; x64_triples hex;
101  val hex = "8B45F8"; x64_triples hex;
102  val hex = "3B45E4"; x64_triples hex;
103  val hex = "7CBD"; x64_triples hex;
104  val hex = "5D"; x64_triples hex;
105
106*)
107
108end
109