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