1structure armLib :> armLib = 2struct 3 4(* interactive use: 5 app load ["arm_disassemblerLib", "arm_stepLib"]; 6*) 7 8open HolKernel boolLib bossLib; 9open armSyntax arm_astSyntax; 10open arm_parserLib arm_encoderLib arm_disassemblerLib arm_stepLib; 11 12(* ------------------------------------------------------------------------- *) 13 14val _ = numLib.prefer_num(); 15val _ = wordsLib.prefer_word(); 16 17val ERR = Feedback.mk_HOL_ERR "armLib"; 18 19val trace_progress = ref 1; 20val label_step_theorems = ref true; 21val disassemble = ref true; 22 23val _ = Feedback.register_trace ("arm steps", trace_progress, 3); 24val _ = Feedback.register_btrace ("label arm steps", label_step_theorems); 25val _ = Feedback.register_btrace ("add disassembler comments", disassemble); 26 27(* ------------------------------------------------------------------------- *) 28 29val eval = boolSyntax.rhs o Thm.concl o bossLib.EVAL; 30 31local 32 fun mk_word4 i = wordsSyntax.mk_wordii (i,4) 33 34 val is_AL = Term.term_eq (mk_word4 14) 35 val is_PC = Term.term_eq (mk_word4 15) 36 37 infix ** 38 39 fun opt1 ** opt2 = if opt2 = "" then opt1 else opt1 ^ "," ^ opt2 40 41 val dest_itstate = eval o wordsSyntax.mk_word_concat o dest_If_Then 42 43 val ITAdvance = eval o armSyntax.mk_ITAdvance 44 45 val w2s = 46 Arbnum.toString o numSyntax.dest_numeral o fst o wordsSyntax.dest_n2w 47 48 fun condition_to_word4 tm = 49 mk_word4 50 (case fst (Term.dest_var tm) 51 of "eq" => 0 52 | "ne" => 1 53 | "cs" => 2 54 | "hs" => 2 55 | "cc" => 3 56 | "lo" => 3 57 | "mi" => 4 58 | "pl" => 5 59 | "vs" => 6 60 | "vc" => 7 61 | "hi" => 8 62 | "ls" => 9 63 | "ge" => 10 64 | "lt" => 11 65 | "gt" => 12 66 | "le" => 13 67 | "al" => 14 68 | s => raise ERR "condition_to_word4" (s ^ " is not a condition")); 69 70 fun fix_condition tm = if is_var tm then condition_to_word4 tm else tm 71 72 fun encoding tm = 73 case fst (Term.dest_const tm) 74 of "Encoding_ARM" => "; ARM" 75 | "Encoding_Thumb" => "; 16-bit Thumb" 76 | "Encoding_Thumb2" => "; 32-bit Thumb" 77 | "Encoding_ThumbEE" => "; 16-bit ThumbEE" 78 | _ => raise ERR "encoding" "unexpected encoding" 79 80 val spaces = String.concat o Lib.separate " " 81 82 fun print_progress x c opt opc = 83 case x 84 of NONE => arm_step opt opc 85 | SOME ((m,a),e) => 86 let val label = spaces (List.filter (fn s => s <> "") [m,a,e,c]) 87 val _ = if !trace_progress mod 2 = 1 then 88 print (spaces ["step:", label, "...\n"]) 89 else 90 () 91 val thm = if (!trace_progress div 2) mod 2 = 1 then 92 Lib.real_time (arm_step opt) opc 93 else 94 arm_step opt opc 95 in 96 if !label_step_theorems then 97 markerLib.MK_LABEL(label,thm) 98 else 99 thm 100 end 101in 102 fun arm_steps_from_parse s l = 103 let fun arm_step_from_code (itstate,instr as Instruction (enc,cond,tm)) = 104 let val opc = arm_encoderLib.arm_encode instr 105 val pp = print_progress 106 (if !trace_progress mod 2 = 1 orelse 107 !label_step_theorems 108 then 109 SOME (arm_disassemble instr,encoding enc) 110 else 111 NONE) 112 in 113 SOME 114 (if enc ~~ Encoding_ARM_tm then 115 if is_AL cond orelse is_PC cond then 116 (itstate, pp "" ("arm,pass" ** s) opc, NONE) 117 else 118 (itstate, 119 pp "(pass condition)" ("arm,pass" ** s) opc, 120 SOME (pp "(fail condition)" ("arm,fail" ** s) opc)) 121 else 122 let val itstate' = if is_If_Then tm then 123 dest_itstate tm 124 else 125 ITAdvance itstate 126 val its = "it:" ^ w2s itstate 127 val cond' = fix_condition cond 128 val x = if enc ~~ Encoding_ThumbEE_tm then 129 "thumbee" 130 else 131 "thumb" 132 in 133 if is_AL cond' orelse is_PC cond' then 134 (itstate', pp "" (x ** "pass" ** its ** s) opc, 135 NONE) 136 else 137 (itstate', 138 pp "(pass condition)" ("thumb,pass" ** its ** s) opc, 139 SOME (pp "(fail condition)" 140 (x ** "fail" ** its ** s) opc)) 141 end) 142 end 143 | arm_step_from_code _ = NONE 144 fun recurse [] _ a = List.rev a 145 | recurse (h::t) itstate a = 146 case arm_step_from_code (itstate,h) 147 of SOME (itstate',pass,fail) => 148 recurse t itstate' ((pass,fail)::a) 149 | NONE => 150 recurse t itstate a 151 in 152 recurse l (wordsSyntax.mk_wordii(0,8)) [] 153 end 154end; 155 156fun arm_steps_from f opt qs = 157 arm_steps_from_parse opt 158 (Lib.op_mk_set arm_code_eq (List.map snd (fst (f qs)))); 159 160val arm_steps_from_string = arm_steps_from arm_parse_from_string; 161val arm_steps_from_file = arm_steps_from arm_parse_from_file; 162val arm_steps_from_quote = arm_steps_from arm_parse_from_quote; 163 164fun bits32 (n,h,l) = 165let val s = StringCvt.padLeft #"0" 32 (Arbnum.toBinString n) 166 val ss = Substring.slice (Substring.full s, 31 - h, SOME (h + 1 - l)) 167in 168 Arbnum.fromBinString (Substring.string ss) 169end; 170 171fun decode_opcode opt opc = 172 case opt 173 of SOME (itstate, ee) => 174 let val n = wordsSyntax.mk_wordi (bits32 (opc,15,0),16) 175 val IT = wordsSyntax.mk_wordii (itstate,8) 176 in 177 if bits32 (opc,31,29) = Arbnum.fromBinString "111" andalso 178 bits32 (opc,28,27) <> Arbnum.zero 179 then 180 pairSyntax.mk_pair (Encoding_Thumb2_tm, 181 mk_thumb2_decode (``arm_coretypes$ARMv7_A``,IT, 182 wordsSyntax.mk_wordi (bits32 (opc,31,16),16),n)) 183 else if ee then 184 mk_thumbee_decode (``arm_coretypes$ARMv7_A``,IT,n) 185 else 186 pairSyntax.mk_pair (Encoding_Thumb_tm, 187 mk_thumb_decode (``arm_coretypes$ARMv7_A``,IT,n)) 188 end 189 | NONE => 190 pairSyntax.mk_pair (Encoding_ARM_tm, 191 mk_arm_decode (boolSyntax.F, wordsSyntax.mk_wordi (opc,32))); 192 193fun decode_from_string opt s = 194let val tm = decode_opcode opt (Arbnum.fromHexString s) in 195 Instruction 196 (case tm |> eval |> pairSyntax.strip_pair 197 of [enc,cond,tm] => (enc,cond,tm) 198 | _ => raise ERR "decode_from_string" "failed to evaluate decoding") 199end handle Option => 200 raise ERR "decode_from_string" "could not parse HEX string"; 201 202val arm_decode = decode_from_string NONE; 203fun thumb_decode i = decode_from_string (SOME (i,false)); 204fun thumbee_decode i = decode_from_string (SOME (i,true)); 205 206(* ------------------------------------------------------------------------- *) 207 208fun output_code ostrm line (c as Instruction _) = 209 let val i = arm_encoderLib.arm_encode c 210 val pad = StringCvt.padRight #" " 211 val comment = if !disassemble then 212 let val (m,a) = arm_disassemble c in 213 String.concat ["\t\t; ", pad 8 m, a] 214 end 215 else 216 "" 217 in 218 TextIO.output (ostrm, String.concat [line, " ", pad 8 i, comment, "\n"]) 219 end 220 | output_code ostrm line c = 221 TextIO.output(ostrm, 222 String.concat [line, " ", arm_encoderLib.arm_encode c, "\n"]); 223 224fun output_arm_assemble_parse ostrm s = 225let open Arbnum 226 val start = fromHexString s 227 handle Option => 228 raise ERR "output_arm_assemble_parse" "expecting Hex string" 229 val lower = String.map Char.toLower 230 val pad = StringCvt.padLeft #" " 231 val pad0 = StringCvt.padLeft #"0" 232 val count = pad 8 o pad0 4 o lower o toHexString 233in 234 List.app (fn (n,i) => output_code ostrm (count (start + n)) i) 235end; 236 237fun arm_assemble_to_file_parse start filename c = 238let val ostrm = TextIO.openOut filename in 239 output_arm_assemble_parse ostrm start c before TextIO.closeOut ostrm 240end; 241 242fun print_arm_assemble_from_quote s = 243 output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_quote; 244 245fun print_arm_assemble_from_string s = 246 output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_string; 247 248fun print_arm_assemble_from_file s = 249 output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_file; 250 251fun arm_assemble_to_file_from_quote s f = 252 arm_assemble_to_file_parse s f o fst o arm_parse_from_quote; 253 254fun arm_assemble_to_file_from_string s f = 255 arm_assemble_to_file_parse s f o fst o arm_parse_from_string; 256 257fun arm_assemble_to_file_from_file s f = 258 arm_assemble_to_file_parse s f o fst o arm_parse_from_file; 259 260fun join s (a,b) = 261 if a = "WORD" orelse a = "SHORT" 262 then "UDF; (" ^ s ^ ")" 263 else case b of "" => a | _ => String.concat [a, " ", b]; 264 265fun arm_disassemble_decode s = join s (arm_disassemble (arm_decode s)) 266fun thumb_disassemble_decode i s = join s (arm_disassemble (thumb_decode i s)) 267 268fun thumbee_disassemble_decode i s = 269 join s (arm_disassemble (thumbee_decode i s)) 270 271end 272