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