1structure arm_core_decompLib :> arm_core_decompLib =
2struct
3
4open HolKernel Parse boolLib bossLib Lib
5open core_decompilerLib
6open tripleLib arm_decompLib arm_core_decompTheory
7
8val ERR = Feedback.mk_HOL_ERR "arm_core_decompLib"
9
10(* ------------------------------------------------------------------------ *)
11
12val (spec, _, _, _) = arm_decompLib.l3_arm_tools
13
14val r15 = Term.mk_var ("r15", ``:word32``)
15
16val rule = tripleLib.spec_to_triple_rule (r15, ARM_ASSERT_def, L3_ARM_def)
17
18val l3_triple =
19   (* utilsLib.cache 10000 String.compare *)
20      (helperLib.instruction_apply rule o spec)
21
22val l3_triple_code =
23   List.map l3_triple o
24   (armAssemblerLib.arm_code: string quotation -> string list)
25
26val vars = Term.mk_var ("cond", Type.bool) ::
27           fst (boolSyntax.strip_forall (Thm.concl ARM_ASSERT_def))
28
29fun config_for_arm () =
30   core_decompilerLib.configure
31     { pc_tm = r15,
32       init_fn = fn () => arm_progLib.arm_config "vfpv3"
33                            "fpr-map, no-gpr-map, mapped",
34       pc_conv = RAND_CONV,
35       triple_fn = l3_triple,
36       component_vars = vars }
37
38val () = config_for_arm ()
39
40fun arm_core_decompile name qcode =
41   ( config_for_arm ()
42   ; core_decompilerLib.code_parser := NONE
43   ; core_decompilerLib.core_decompile name qcode
44   )
45
46fun arm_core_decompile_code name qcode =
47   ( config_for_arm ()
48   ; core_decompilerLib.code_parser := SOME armAssemblerLib.arm_code
49   ; core_decompilerLib.core_decompile name qcode
50   )
51
52(* ------------------------------------------------------------------------ *)
53
54end
55