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