1structure arm_decompLib :> arm_decompLib =
2struct
3
4open HolKernel Parse boolLib bossLib;
5open helperLib set_sepTheory addressTheory progTheory;
6open pred_setTheory combinTheory;
7open arm_decompTheory decompilerLib;
8
9val ERR = Feedback.mk_HOL_ERR "arm_decompLib"
10
11(* automation *)
12
13local
14   fun w_var i = Term.mk_var ("w" ^ Int.toString i, ``:word32``)
15   fun word32 w = wordsSyntax.mk_wordi (Arbnum.fromHexString w, 32)
16   val ok_rule = PURE_ONCE_REWRITE_RULE [GSYM arm_OK_def]
17   val sbst = [``vfp:VFPExtension`` |-> ``VFPv3``,
18               ``arch:Architecture`` |-> ``ARMv7_A``]
19   fun arm_OK_intro l = ok_rule o Thm.INST (l @ sbst)
20   fun format_thm th =
21      (th, 4,
22       stateLib.get_pc_delta
23          (Lib.equal "arm_prog$arm_PC" o fst o boolSyntax.dest_strip_comb) th)
24in
25   val set_opt = arm_progLib.arm_config "vfpv3"
26   fun l3_arm_triples hex =
27      case String.tokens (fn c => c = #" ") hex of
28         h :: r =>
29           let
30              val ws = List.tabulate (List.length r, w_var)
31              val l =
32                List.map (fn (v, hx) => v |-> word32 hx) (ListPair.zip (ws, r))
33           in
34              List.map (arm_OK_intro l)
35                 (stateLib.fix_precond (arm_progLib.arm_spec_hex h))
36           end
37       | _ => raise ERR "l3_arm_triples" "empty string"
38   fun l3_arm_spec hex =
39      case List.map format_thm (l3_arm_triples hex) of
40         [x] => (x, NONE)
41       | [x1, x2] => (x1, SOME x2)
42       | _ => raise ERR "l3_arm_spec" ""
43   fun l3_arm_spec_opt s hex = (set_opt s; l3_arm_spec hex)
44end
45
46val arm_pc = Term.prim_mk_const {Thy = "arm_prog", Name = "arm_PC"}
47
48fun arm_tools f hide = (f, fn _ => fail(), hide, arm_pc): decompiler_tools
49fun arm_tools_opt opt = arm_tools (l3_arm_spec_opt opt)
50
51val l3_arm_tools = arm_tools l3_arm_spec arm_progTheory.aS_HIDE
52val l3_arm_tools_no_status = arm_tools l3_arm_spec TRUTH
53
54val l3_arm_tools_array = arm_tools_opt "array" arm_progTheory.aS_HIDE
55val l3_arm_tools_array_no_status = arm_tools_opt "array" TRUTH
56val l3_arm_tools_mapped = arm_tools_opt "mapped" arm_progTheory.aS_HIDE
57val l3_arm_tools_mapped_no_status = arm_tools_opt "mapped" TRUTH
58val l3_arm_tools_mapped32 = arm_tools_opt "mapped32" arm_progTheory.aS_HIDE
59val l3_arm_tools_mapped32_no_status = arm_tools_opt "mapped32" TRUTH
60
61fun arm_decompile iscode tools opt name (qcode: string quotation) =
62   let
63      val q = if iscode then armAssemblerLib.arm_code
64              else helperLib.quote_to_strings
65      val decomp = decompilerLib.decompile_with q tools
66   in
67      set_opt opt
68    ; arm_progLib.set_newline ""
69    ; (decompilerLib.UNABBREV_CODE_RULE ## I) (decomp name qcode)
70   end
71
72val l3_arm_decompile = arm_decompile false l3_arm_tools "mapped"
73val arm_decompile_code = arm_decompile true l3_arm_tools "mapped"
74
75val l3_arm_decompile_no_status =
76   arm_decompile false l3_arm_tools_no_status "mapped"
77
78val arm_decompile_code_no_status =
79   arm_decompile true l3_arm_tools_no_status "mapped"
80
81val arm_decompile32 = arm_decompile false l3_arm_tools "mapped32"
82val arm_decompile32_code = arm_decompile true l3_arm_tools "mapped32"
83
84val arm_decompile32_no_status =
85   arm_decompile false l3_arm_tools_no_status "mapped32"
86
87val arm_decompile32_code_no_status =
88   arm_decompile true l3_arm_tools_no_status "mapped32"
89
90(* testing
91
92open arm_decompLib
93
94val q =
95   `movs r1, #0        ; accumulator
96    mov  r3, r0        ; first address
97    adds r3, #40       ; last address (10 loads)
98label:
99    ldr  r2, [r0, #4]  ; load data
100    adds r0, #4        ; increment address
101    add  r1, r2        ; add to accumulator
102    cmp  r0, r3        ; test if done
103    blt  label         ; loop if not done`
104
105val () = armAssemblerLib.print_arm_code q
106
107val (test_cert, test_def) = arm_decompile_code "test" q
108
109*)
110
111end
112