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 (Lib.mk_set (List.map snd (fst (f qs)))); 158 159val arm_steps_from_string = arm_steps_from arm_parse_from_string; 160val arm_steps_from_file = arm_steps_from arm_parse_from_file; 161val arm_steps_from_quote = arm_steps_from arm_parse_from_quote; 162 163fun bits32 (n,h,l) = 164let val s = StringCvt.padLeft #"0" 32 (Arbnum.toBinString n) 165 val ss = Substring.slice (Substring.full s, 31 - h, SOME (h + 1 - l)) 166in 167 Arbnum.fromBinString (Substring.string ss) 168end; 169 170fun decode_opcode opt opc = 171 case opt 172 of SOME (itstate, ee) => 173 let val n = wordsSyntax.mk_wordi (bits32 (opc,15,0),16) 174 val IT = wordsSyntax.mk_wordii (itstate,8) 175 in 176 if bits32 (opc,31,29) = Arbnum.fromBinString "111" andalso 177 bits32 (opc,28,27) <> Arbnum.zero 178 then 179 pairSyntax.mk_pair (Encoding_Thumb2_tm, 180 mk_thumb2_decode (``arm_coretypes$ARMv7_A``,IT, 181 wordsSyntax.mk_wordi (bits32 (opc,31,16),16),n)) 182 else if ee then 183 mk_thumbee_decode (``arm_coretypes$ARMv7_A``,IT,n) 184 else 185 pairSyntax.mk_pair (Encoding_Thumb_tm, 186 mk_thumb_decode (``arm_coretypes$ARMv7_A``,IT,n)) 187 end 188 | NONE => 189 pairSyntax.mk_pair (Encoding_ARM_tm, 190 mk_arm_decode (boolSyntax.F, wordsSyntax.mk_wordi (opc,32))); 191 192fun decode_from_string opt s = 193let val tm = decode_opcode opt (Arbnum.fromHexString s) in 194 Instruction 195 (case tm |> eval |> pairSyntax.strip_pair 196 of [enc,cond,tm] => (enc,cond,tm) 197 | _ => raise ERR "decode_from_string" "failed to evaluate decoding") 198end handle Option => 199 raise ERR "decode_from_string" "could not parse HEX string"; 200 201val arm_decode = decode_from_string NONE; 202fun thumb_decode i = decode_from_string (SOME (i,false)); 203fun thumbee_decode i = decode_from_string (SOME (i,true)); 204 205(* ------------------------------------------------------------------------- *) 206 207fun output_code ostrm line (c as Instruction _) = 208 let val i = arm_encoderLib.arm_encode c 209 val pad = StringCvt.padRight #" " 210 val comment = if !disassemble then 211 let val (m,a) = arm_disassemble c in 212 String.concat ["\t\t; ", pad 8 m, a] 213 end 214 else 215 "" 216 in 217 TextIO.output (ostrm, String.concat [line, " ", pad 8 i, comment, "\n"]) 218 end 219 | output_code ostrm line c = 220 TextIO.output(ostrm, 221 String.concat [line, " ", arm_encoderLib.arm_encode c, "\n"]); 222 223fun output_arm_assemble_parse ostrm s = 224let open Arbnum 225 val start = fromHexString s 226 handle Option => 227 raise ERR "output_arm_assemble_parse" "expecting Hex string" 228 val lower = String.map Char.toLower 229 val pad = StringCvt.padLeft #" " 230 val pad0 = StringCvt.padLeft #"0" 231 val count = pad 8 o pad0 4 o lower o toHexString 232in 233 List.app (fn (n,i) => output_code ostrm (count (start + n)) i) 234end; 235 236fun arm_assemble_to_file_parse start filename c = 237let val ostrm = TextIO.openOut filename in 238 output_arm_assemble_parse ostrm start c before TextIO.closeOut ostrm 239end; 240 241fun print_arm_assemble_from_quote s = 242 output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_quote; 243 244fun print_arm_assemble_from_string s = 245 output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_string; 246 247fun print_arm_assemble_from_file s = 248 output_arm_assemble_parse TextIO.stdOut s o fst o arm_parse_from_file; 249 250fun arm_assemble_to_file_from_quote s f = 251 arm_assemble_to_file_parse s f o fst o arm_parse_from_quote; 252 253fun arm_assemble_to_file_from_string s f = 254 arm_assemble_to_file_parse s f o fst o arm_parse_from_string; 255 256fun arm_assemble_to_file_from_file s f = 257 arm_assemble_to_file_parse s f o fst o arm_parse_from_file; 258 259fun join s (a,b) = 260 if a = "WORD" orelse a = "SHORT" 261 then "UDF; (" ^ s ^ ")" 262 else case b of "" => a | _ => String.concat [a, " ", b]; 263 264fun arm_disassemble_decode s = join s (arm_disassemble (arm_decode s)) 265fun thumb_disassemble_decode i s = join s (arm_disassemble (thumb_decode i s)) 266 267fun thumbee_disassemble_decode i s = 268 join s (arm_disassemble (thumbee_decode i s)) 269 270end 271