1structure emit_eval :> emit_eval = 2struct 3 4(* intactive use: 5 app load 6 ["combinML", "pairML", "sumML", "numML", "listML", "setML", "optionML", 7 "rich_listML", "basicSizeML", "stringML", "bitML", "fcpML", "wordsML", 8 "intML", "sortingML", "patriciaML", "armML"] 9*) 10 11local 12 open combinML pairML sumML numML listML setML optionML rich_listML basicSizeML 13 stringML bitML fcpML wordsML intML sortingML patriciaML armML 14in end 15 16(* ------------------------------------------------------------------------ *) 17 18(* 19open Int 20val op o = General.o 21*) 22 23type arm_mem = armML.word8 patriciaML.ptree 24 25fun mem i = List.exists (fn x => x = i) 26 27fun load_program (s, t) = 28 let 29 val istrm = TextIO.openIn s 30 val a = TextIO.inputAll istrm before TextIO.closeIn istrm 31 fun pair [a, b] = (numML.fromHexString a, 32 wordsML.toWord8 (numML.fromHexString b)) 33 | pair _ = raise Match 34 in 35 a |> String.tokens (fn c => c = #"\n") 36 |> List.map (pair o String.tokens Char.isSpace) 37 |> patriciaML.ADD_LIST t 38 end 39 40val load_programs = List.foldl load_program patriciaML.Empty 41 42(* ------------------------------------------------------------------------ *) 43 44fun toWord i n = wordsML.fromNum (n, fcpML.ITSELF (numML.fromInt i)) 45val zero32 = wordsML.toWord32 numML.ZERO 46 47fun mk_arm_state arch regs psrs md mem = 48 armML.arm_state 49 (armML.proc numML.ZERO regs, 50 armML.proc numML.ZERO psrs, 51 combinML.K true, (* event_register *) 52 combinML.K false, (* interrupt_wait *) 53 fn a => case patriciaML.PEEK mem (wordsML.w2n a) 54 of SOME d => d 55 | NONE => md, 56 [], (* accesses *) 57 armML.ARMinfo (arch, setML.EMPTY, true), 58 armML.Coprocessors 59 (armML.coproc_state 60 (armML.CP14reg zero32, 61 armML.CP15reg 62 (armML.CP15sctlr (true, false, false, false, true, true, 63 false, false, false, false, false, false, 64 false, false, false, false, false, false, 65 true, false), 66 armML.CP15scr (false, false, false, false, false, false, false), 67 armML.CP15nsacr (false, false, false, toWord 14 numML.ZERO), 68 zero32, zero32)), 69 combinML.K (armML.constC false), 70 combinML.K (armML.constC ()), 71 combinML.K (armML.constC numML.ZERO), 72 combinML.K (combinML.K (armML.constC ())), 73 combinML.K (armML.constC []), 74 combinML.K (combinML.K (armML.constC ())), 75 combinML.K (armML.constC zero32), 76 combinML.K (combinML.K (armML.constC ())), 77 combinML.K (armML.constC (zero32, zero32))), 78 armML.ExclusiveMonitors 79 ((combinML.K setML.EMPTY, setML.EMPTY), 80 combinML.K (armML.constE ()), 81 combinML.K (armML.constE ()), 82 combinML.K (armML.constE false), 83 combinML.K (armML.constE false), 84 combinML.K (armML.constE ()), 85 combinML.K (armML.constE ()))) 86 87(* ------------------------------------------------------------------------ *) 88 89fun w2int w = w |> wordsML.w2n |> numML.toInt |> valOf 90 91fun architecture a = 92 case a 93 of "armv4" => armML.ARMv4 94 | "armv4t" => armML.ARMv4T 95 | "armv5t" => armML.ARMv5T 96 | "armv5te" => armML.ARMv5TE 97 | "armv6" => armML.ARMv6 98 | "armv6k" => armML.ARMv6K 99 | "armv6t2" => armML.ARMv6T2 100 | "armv7-a" => armML.ARMv7_A 101 | "armv7-r" => armML.ARMv7_R 102 | _ => raise Fail "architecture" 103 104fun string_of_rname r = 105 case r 106 of armML.RName_0usr => "r0" 107 | armML.RName_1usr => "r1" 108 | armML.RName_2usr => "r2" 109 | armML.RName_3usr => "r3" 110 | armML.RName_4usr => "r4" 111 | armML.RName_5usr => "r5" 112 | armML.RName_6usr => "r6" 113 | armML.RName_7usr => "r7" 114 | armML.RName_8usr => "r8" 115 | armML.RName_8fiq => "r8_fiq" 116 | armML.RName_9usr => "r9" 117 | armML.RName_9fiq => "r9_fiq" 118 | armML.RName_10usr => "r10" 119 | armML.RName_10fiq => "r10_fiq" 120 | armML.RName_11usr => "r11" 121 | armML.RName_11fiq => "r11_fiq" 122 | armML.RName_12usr => "r12" 123 | armML.RName_12fiq => "r12_fiq" 124 | armML.RName_SPusr => "sp" 125 | armML.RName_SPfiq => "sp_fiq" 126 | armML.RName_SPirq => "sp_irq" 127 | armML.RName_SPsvc => "sp_svc" 128 | armML.RName_SPabt => "sp_abt" 129 | armML.RName_SPund => "sp_und" 130 | armML.RName_SPmon => "sp_mon" 131 | armML.RName_LRusr => "lr" 132 | armML.RName_LRfiq => "lr_fiq" 133 | armML.RName_LRirq => "lr_irq" 134 | armML.RName_LRsvc => "lr_svc" 135 | armML.RName_LRabt => "lr_abt" 136 | armML.RName_LRund => "lr_und" 137 | armML.RName_LRmon => "lr_mon" 138 | armML.RName_PC => "pc" 139 140fun rname i = 141 case i 142 of 0 => armML.RName_0usr 143 | 1 => armML.RName_1usr 144 | 2 => armML.RName_2usr 145 | 3 => armML.RName_3usr 146 | 4 => armML.RName_4usr 147 | 5 => armML.RName_5usr 148 | 6 => armML.RName_6usr 149 | 7 => armML.RName_7usr 150 | 8 => armML.RName_8usr 151 | 9 => armML.RName_8fiq 152 | 10 => armML.RName_9usr 153 | 11 => armML.RName_9fiq 154 | 12 => armML.RName_10usr 155 | 13 => armML.RName_10fiq 156 | 14 => armML.RName_11usr 157 | 15 => armML.RName_11fiq 158 | 16 => armML.RName_12usr 159 | 17 => armML.RName_12fiq 160 | 18 => armML.RName_SPusr 161 | 19 => armML.RName_SPfiq 162 | 20 => armML.RName_SPirq 163 | 21 => armML.RName_SPsvc 164 | 22 => armML.RName_SPabt 165 | 23 => armML.RName_SPund 166 | 24 => armML.RName_SPmon 167 | 25 => armML.RName_LRusr 168 | 26 => armML.RName_LRfiq 169 | 27 => armML.RName_LRirq 170 | 28 => armML.RName_LRsvc 171 | 29 => armML.RName_LRabt 172 | 30 => armML.RName_LRund 173 | 31 => armML.RName_LRmon 174 | 32 => armML.RName_PC 175 | _ => raise Fail "rname" 176 177fun string_of_psrname p = 178 case p 179 of armML.CPSR => "cpsr" 180 | armML.SPSR_fiq => "spsr_fiq" 181 | armML.SPSR_irq => "spsr_irq" 182 | armML.SPSR_svc => "spsr_svc" 183 | armML.SPSR_mon => "spsr_mon" 184 | armML.SPSR_abt => "spsr_abt" 185 | armML.SPSR_und => "spsr_und" 186 187fun psrname i = 188 case i 189 of 0 => armML.CPSR 190 | 1 => armML.SPSR_fiq 191 | 2 => armML.SPSR_irq 192 | 3 => armML.SPSR_svc 193 | 4 => armML.SPSR_mon 194 | 5 => armML.SPSR_abt 195 | 6 => armML.SPSR_und 196 | _ => raise Fail "psrname" 197 198fun encoding armML.Encoding_Thumb = "16-bit Thumb:\t" 199 | encoding armML.Encoding_Thumb2 = "32-bit Thumb:\t" 200 | encoding armML.Encoding_ThumbEE = "ThumbEE:\t" 201 | encoding armML.Encoding_ARM = "ARM:\t\t" 202 203fun condition (cond:armML.word4) = 204 case w2int cond 205 of 0 => "eq" 206 | 1 => "ne" 207 | 2 => "cs" 208 | 3 => "cc" 209 | 4 => "mi" 210 | 5 => "pl" 211 | 6 => "vs" 212 | 7 => "vc" 213 | 8 => "hi" 214 | 9 => "ls" 215 | 10 => "ge" 216 | 11 => "lt" 217 | 12 => "gt" 218 | 13 => "le" 219 | 14 => "al" 220 | _ => raise Fail "condition" 221 222fun data_processing (enc, opc, n) = 223 case w2int opc 224 of 0 => "and" 225 | 1 => "eor" 226 | 2 => "sub" 227 | 3 => "rsb" 228 | 4 => "add" 229 | 5 => "adc" 230 | 6 => "sbc" 231 | 7 => "rsc" 232 | 8 => "tst" 233 | 9 => "teq" 234 | 10 => "cmp" 235 | 11 => "cmn" 236 | 12 => "orr" 237 | 13 => "mov" 238 | 14 => "bic" 239 | 15 => if enc = armML.Encoding_Thumb2 andalso (w2int n <> 15) then 240 "orn" 241 else 242 "mvn" 243 | _ => raise Fail "data_processing" 244 245fun instruction (enc, instr) = 246 case instr 247 of armML.Unpredictable => "unpredictable" 248 | armML.Undefined => "undefined" 249 | armML.Branch (armML.Branch_Target _) => "branch target" 250 | armML.Branch (armML.Branch_Exchange _) => "branch exchange" 251 | armML.Branch (armML.Compare_Branch _) => "compare branch" 252 | armML.Branch (armML.Check_Array _) => "check array" 253 | armML.Branch (armML.Table_Branch_Byte _) => "table branch byte" 254 | armML.Branch (armML.Branch_Link_Exchange_Immediate _) => 255 "branch link exchange (imm)" 256 | armML.Branch (armML.Branch_Link_Exchange_Register _) => 257 "branch link exchange (reg)" 258 | armML.Branch (armML.Handler_Branch_Link _) => 259 "handler branch (link)" 260 | armML.Branch (armML.Handler_Branch_Link_Parameter _) => 261 "handler branch with link and parameter" 262 | armML.Branch (armML.Handler_Branch_Parameter _) => 263 "handler branch with parameter" 264 | armML.DataProcessing (armML.Data_Processing (opc, _, n, _, _)) => 265 data_processing (enc, opc, n) 266 | armML.DataProcessing (armML.Add_Sub (add, _, _, _)) => 267 if add then "add (wide)" else "sub (wide)" 268 | armML.DataProcessing (armML.Move_Halfword _) => "move halfword" 269 | armML.DataProcessing (armML.Divide _) => "divide" 270 | armML.DataProcessing (armML.Multiply _) => "multiply" 271 | armML.DataProcessing (armML.Multiply_Subtract _) => "multiply subtract" 272 | armML.DataProcessing (armML.Multiply_Long _) => "multiply (long)" 273 | armML.DataProcessing (armML.Saturate _) => "saturate" 274 | armML.DataProcessing (armML.Saturate_16 _) => "saturate (16)" 275 | armML.DataProcessing (armML.Select_Bytes _) => "select bytes" 276 | armML.DataProcessing (armML.Extend_Byte _) => "extend byte" 277 | armML.DataProcessing (armML.Extend_Byte_16 _) => "extend byte (16)" 278 | armML.DataProcessing (armML.Extend_Halfword _) => "extend halfword" 279 | armML.DataProcessing (armML.Pack_Halfword _) => "pack halfword" 280 | armML.DataProcessing (armML.Reverse_Bits _) => "reverse bits" 281 | armML.DataProcessing (armML.Byte_Reverse_Word _) => "byte reverse word" 282 | armML.DataProcessing (armML.Byte_Reverse_Packed_Halfword _) => 283 "byte reverse packed halfword" 284 | armML.DataProcessing (armML.Byte_Reverse_Signed_Halfword _) => 285 "byte reverse signed halfword" 286 | armML.DataProcessing (armML.Signed_Halfword_Multiply _) => 287 "signed halfword multiply" 288 | armML.DataProcessing (armML.Signed_Multiply_Dual _) => 289 "signed multiply dual" 290 | armML.DataProcessing (armML.Signed_Multiply_Long_Dual _) => 291 "signed multiply dual (long)" 292 | armML.DataProcessing (armML.Signed_Most_Significant_Multiply _) => 293 "signed most significant multiply" 294 | armML.DataProcessing (armML.Signed_Most_Significant_Multiply_Subtract _) => 295 "signed most significant multiply subtract" 296 | armML.DataProcessing (armML.Multiply_Accumulate_Accumulate _) => 297 "multiply accumulate accumulate" 298 | armML.DataProcessing (armML.Saturating_Add_Subtract _) => 299 "saturating add subtract" 300 | armML.DataProcessing (armML.Bit_Field_Clear_Insert _) => 301 "bit field clear/insert" 302 | armML.DataProcessing (armML.Bit_Field_Extract _) => 303 "bit field extract" 304 | armML.DataProcessing (armML.Count_Leading_Zeroes _) => 305 "count leading zeroes" 306 | armML.DataProcessing (armML.Unsigned_Sum_Absolute_Differences _) => 307 "unsigned sum absolute differences" 308 | armML.DataProcessing (armML.Parallel_Add_Subtract _) => 309 "parallel add subtract" 310 | armML.StatusAccess (armML.Status_to_Register _) => 311 "program status to register (mrs)" 312 | armML.StatusAccess (armML.Register_to_Status _) => 313 "register to program status (msr)" 314 | armML.StatusAccess (armML.Immediate_to_Status _) => 315 "immediate to program status (msr)" 316 | armML.StatusAccess (armML.Change_Processor_State _) => 317 "change processor state" 318 | armML.StatusAccess (armML.Set_Endianness _) => 319 "set endianess" 320 | armML.LoadStore (armML.Load _) => "load" 321 | armML.LoadStore (armML.Store _) => "store" 322 | armML.LoadStore (armML.Load_Halfword _) => "load halfword" 323 | armML.LoadStore (armML.Store_Halfword _) => "store halfword" 324 | armML.LoadStore (armML.Load_Dual _) => "load dual" 325 | armML.LoadStore (armML.Store_Dual _) => "store dual" 326 | armML.LoadStore (armML.Load_Multiple _) => "load multiple" 327 | armML.LoadStore (armML.Store_Multiple _) => "store multiple" 328 | armML.LoadStore (armML.Load_Exclusive _) => "load exclusive" 329 | armML.LoadStore (armML.Store_Exclusive _) => "store exclusive" 330 | armML.LoadStore (armML.Load_Exclusive_Doubleword _) => 331 "load exclusive doubleword" 332 | armML.LoadStore (armML.Store_Exclusive_Doubleword _) => 333 "store exclusive doubleword" 334 | armML.LoadStore (armML.Load_Exclusive_Halfword _) => 335 "load exclusive halfword" 336 | armML.LoadStore (armML.Store_Exclusive_Halfword _) => 337 "store exclusive halfword" 338 | armML.LoadStore (armML.Load_Exclusive_Byte _) => 339 "load exclusive byte" 340 | armML.LoadStore (armML.Store_Exclusive_Byte _) => 341 "store exclusive byte" 342 | armML.LoadStore (armML.Store_Return_State _) => 343 "store return state" 344 | armML.LoadStore (armML.Return_From_Exception _) => 345 "return from exception" 346 | armML.Miscellaneous armML.Clear_Exclusive => "clear exclusive" 347 | armML.Miscellaneous (armML.Hint _) => "hint" 348 | armML.Miscellaneous (armML.Breakpoint _) => "breakpoint" 349 | armML.Miscellaneous (armML.Swap _) => "swap" 350 | armML.Miscellaneous (armML.Preload_Data _) => "preload data" 351 | armML.Miscellaneous (armML.Preload_Instruction _) => "preload instruction" 352 | armML.Miscellaneous (armML.Supervisor_Call _) => "supervisor call" 353 | armML.Miscellaneous (armML.Secure_Monitor_Call _) => "secure monitor call" 354 | armML.Miscellaneous (armML.If_Then _) => "if-then" 355 | armML.Miscellaneous (armML.Enterx_Leavex true) => "enterx" 356 | armML.Miscellaneous (armML.Enterx_Leavex false) => "leavex" 357 | armML.Miscellaneous (armML.Data_Memory_Barrier _) => "data memory barrier" 358 | armML.Miscellaneous (armML.Data_Synchronization_Barrier _) => 359 "data synchronization barrier" 360 | armML.Miscellaneous (armML.Instruction_Synchronization_Barrier _) => 361 "instruction synchronization barrier" 362 | armML.Coprocessor _ => "coprocessor" 363 364fun for_se base top f = 365 let 366 fun For i = if i > top then () else (f i; For (i+1)) 367 in 368 For base 369 end 370 371val word8 = wordsML.toWord8 o numML.fromHexString 372val word32 = wordsML.toWord32 o numML.fromHexString 373 374fun for_word32 base top f = 375 let 376 val t = word32 top 377 val b = word32 base 378 val one = wordsML.toWord32 numML.ONE 379 val add1 = wordsML.word_add one 380 fun For i = if wordsML.word_gt i t then () else (f i; For (add1 i)) 381 in 382 For b 383 end 384 385fun hex n s = StringCvt.padLeft #"0" n (wordsML.word_to_hex_string s) 386 387val traceOut = ref TextIO.stdOut 388 389fun out l = TextIO.output (!traceOut, String.concat (l @ ["\n"])) 390 391fun print_reg_updates ii (s1, s2) = 392 let 393 val reg1 = armML.arm_state_registers s1 394 val reg2 = armML.arm_state_registers s2 395 val psr1 = armML.arm_state_psrs s1 396 val psr2 = armML.arm_state_psrs s2 397 val id = armML.iiid_proc ii 398 val first = ref true 399 in 400 for_se 0 32 (fn i => 401 let 402 val r = rname i 403 val d = reg2 (id, r) 404 in 405 if reg1 (id, r) <> d then 406 out [if !first then 407 (first := false; "Registers:\t") 408 else 409 "\t\t", string_of_rname r, " <- ", hex 8 d] 410 else 411 () 412 end); 413 for_se 0 6 (fn i => 414 let 415 val r = psrname i 416 val d = psr2 (id, r) 417 in 418 if psr1 (id, r) <> d then 419 out [if !first then (first := false; "Registers:\t") else "\t\t", 420 string_of_psrname r, " <- ", hex 8 (armML.encode_psr d)] 421 else 422 () 423 end) 424 end 425 426fun print_mem_updates s = 427 let 428 val first = ref true 429 in 430 List.app (fn acc => 431 case acc 432 of armML.MEM_WRITE (a, d) => 433 out [if !first then (first := false; "Memory:") else "", 434 "\t\t[", hex 8 a, "] <- ", hex 2 d] 435 | _ => ()) (List.rev (armML.arm_state_accesses s)) 436 end 437 438fun print_instr (opc, (enc, (cond, instr))) = 439 out [encoding enc, opc, " ; ", condition cond, ", ", 440 instruction (enc, instr)] 441 442val instruction_printer = ref print_instr 443 444type run_trace = 445 { cycle : bool, pc : bool, ireg : bool, regs : bool, mem : bool, 446 rule : int * char } 447 448fun int_to_trace i = 449 { cycle = i > 0, 450 pc = i > 1, 451 ireg = i > 2, 452 regs = i > 3, 453 mem = i > 4, 454 rule = if i > 1 then (40, #"-") else (0, #" ") } 455 456fun print_trace ii (trace : run_trace) (cycle, pc, instr, s1, s2) = 457 (if #cycle trace then out ["Cycle:\t\t", Int.toString cycle] else (); 458 if #pc trace then out ["PC:\t\t", hex 8 pc] else (); 459 if #ireg trace then (!instruction_printer) instr else (); 460 if #regs trace then print_reg_updates ii (s1, s2) else (); 461 if #mem trace then print_mem_updates s2 else (); 462 let 463 val (l, c) = #rule trace 464 in 465 if l > 0 then out [StringCvt.padLeft c l ""] else () 466 end) 467 468fun print_arm_state s = 469 let 470 val reg = armML.arm_state_registers s 471 val psr = armML.arm_state_psrs s 472 val ii = armML.iiid numML.ZERO 473 val id = armML.iiid_proc ii 474 fun pad n s = StringCvt.padRight #" " n s ^ ": " 475 in 476 out ["General Purpose Registers\n", 477 "=========================\n"]; 478 for_se 0 32 (fn i => 479 let 480 val r = rname i 481 in 482 out [pad 9 (string_of_rname r), hex 8 (reg (id, r))] 483 end); 484 out ["\nProgram Status Registers\n", 485 "========================\n"]; 486 for_se 0 6 (fn i => 487 let 488 val r = psrname i 489 in 490 out [pad 9 (string_of_psrname r), 491 hex 8 (armML.encode_psr (psr (id, r)))] 492 end) 493 end 494 495(* 496fun examine_arm_mem mem = 497let 498 fun print_arm_mem b t = 499 for_word32 b t (fn a => out ["[", hex 8 a, "] : ", hex 2 (mem a)]) 500 501 fun print_range () : unit = 502 let val _ = print "Enter memory range [hex - hex]: " 503 val s = valOf (TextIO.inputLine TextIO.stdIn) 504 val (b, t) = case String.tokens 505 (fn c => Char.isSpace c orelse c = #"-") s 506 of [l, r] => let 507 val x = word32 l 508 val y = word32 r 509 in 510 if wordsML.word_lo x y then (l,r) else (r,l) 511 end 512 | _ => raise Fail "print_arm_mem" 513 in 514 print_arm_mem b t; print_range () 515 end 516in 517 print_range () 518end 519*) 520 521local 522 fun print_line (a, b : wordsML.word8) = 523 out ["[", hex 8 (wordsML.toWord32 a), "] : ", hex 2 b] 524 fun mem_compare ((a1, _), (a2, _)) = 525 if a1 = a2 then 526 General.EQUAL 527 else if numML.< a1 a2 then 528 General.LESS 529 else 530 General.GREATER 531 val print_mem = List.app print_line o Listsort.sort mem_compare 532in 533 val print_arm_mem = print_mem o patriciaML.toList 534 fun print_diff_arm_mem prog1 prog2 = 535 let 536 val new = Lib.set_diff (patriciaML.toList prog2) (patriciaML.toList prog1) 537 in 538 out ["\nModified Memory\n", 539 "===============\n"]; 540 print_mem new 541 end 542end 543 544fun print_arm_run prog (message, prog_state) = 545 (if message = "" then () else 546 out ["Final Message\n", "=============\n\n", message, "\n"]; 547 case prog_state 548 of SOME (prog', state) => 549 (print_arm_state state; print_diff_arm_mem prog prog') 550 | _ => out ["state upredictable"]) 551 552(* ------------------------------------------------------------------------ *) 553 554fun update_prog p [] = p 555 | update_prog p (armML.MEM_READ _ :: l) = update_prog p l 556 | update_prog p (armML.MEM_WRITE (a, d) :: l) = 557 update_prog (patriciaML.ADD p (wordsML.w2n a, d)) l 558 559fun ptree_arm_run run_trace (prog, state) t = 560 let 561 val ii = armML.iiid numML.ZERO 562 val arch = case armML.read_arch ii state 563 of armML.Error s => raise Fail "couldn't read Architecture" 564 | armML.ValueState (a, _) => a 565 fun ptree_arm_loop prog' cycle t = 566 armML.seqT (armML.waiting_for_interrupt ii) (fn wfi => 567 if wfi orelse t = 0 then 568 armML.constT ((prog', cycle), "finished") 569 else 570 armML.attempt (prog', cycle) 571 (armML.fetch_instruction ii 572 (armML.ptree_read_word prog') 573 (armML.ptree_read_halfword prog')) 574 (fn instr => 575 armML.seqT 576 (armML.writeT 577 (armML.arm_state_accesses_fupd (combinML.K []))) 578 (fn _ => 579 armML.seqT (armML.readT combinML.I) (fn s1 => 580 armML.seqT (armML.arm_instr ii (pairML.SND instr)) 581 (fn _ => armML.seqT (armML.readT combinML.I) 582 (fn s2 => 583 let 584 val pc = armML.arm_state_registers s1 585 (numML.ZERO, armML.RName_PC) 586 val _ = print_trace ii run_trace 587 (cycle, pc, instr, s1, s2) 588 in 589 ptree_arm_loop 590 (update_prog prog' 591 (armML.arm_state_accesses s2)) 592 (cycle + 1) 593 (if t < 0 then t else t - 1) 594 end)))))) 595 in 596 case ptree_arm_loop prog 0 t state 597 of armML.Error e => (e, NONE) 598 | armML.ValueState (((prog', c), v), s') => 599 ("at cycle " ^ Int.toString c ^ ": " ^ v, SOME (prog', s')) 600 end 601 602(* ------------------------------------------------------------------------ *) 603 604val lower_string = String.implode o map Char.toLower o String.explode 605 606fun pluck P = 607 let fun pl _ [] = raise Fail "pluck: predicate not satisfied" 608 | pl A (h::t) = if P h then (h, List.revAppend(A, t)) else pl (h::A) t 609 in 610 pl [] 611 end 612 613fun init_config prog s = 614 let 615 val l = 616 s |> String.tokens (fn c => mem c [#",", #";",#"\n"]) 617 |> map (fn a => 618 case String.tokens (fn c => c = #"=" orelse Char.isSpace c) a 619 of [l, r] => (lower_string l, lower_string r) 620 | _ => raise Fail "init_config") 621 val ((_, arch), l) = pluck (fn (n, _) => n = "arch") l 622 handle Fail _ => (("", "armv7-a"), l) 623 val ((_, default_reg), l) = pluck (fn (n, _) => n = "reg_") l 624 handle Fail _ => (("", "0"), l) 625 val ((_, default_psr), l) = pluck (fn (n, _) => n = "_psr") l 626 handle Fail _ => (("", "10"), l) 627 val ((_, default_mem), l) = pluck (fn (n, _) => n = "mem_") l 628 handle Fail _ => (("", "0"), l) 629 val dreg = word32 default_reg 630 val dpsr = armML.decode_psr (word32 default_psr) 631 in 632 mk_arm_state (architecture arch) 633 (fn r => case List.find (fn (n, _) => string_of_rname r = n) l 634 of SOME (_, v) => word32 v 635 | _ => dreg) 636 (fn r => case List.find (fn (n, _) => string_of_psrname r = n) l 637 of SOME (_, v) => armML.decode_psr (word32 v) 638 | _ => dpsr) 639 (word8 default_mem) prog 640 end 641 642(* ------------------------------------------------------------------------ *) 643 644(* 645fun time f x = 646 let 647 fun p t = 648 let 649 val s = Time.fmt 3 t 650 in 651 case size (List.last (String.fields (fn x => x = #".") s)) of 3 => s 652 | 2 => s ^ "0" 653 | 1 => s ^ "00" 654 | _ => raise Fail "time" 655 end 656 val c = Timer.startCPUTimer () 657 val r = Timer.startRealTimer () 658 fun pt () = 659 let 660 val {usr, sys, ...} = Timer.checkCPUTimer c 661 val real = Timer.checkRealTimer r 662 in 663 print 664 ("User: " ^ p usr ^ " System: " ^ p sys ^ " Real: " ^ p real ^ "\n") 665 end 666 val y = f x handle e => (pt (); raise e) 667 val () = pt () 668 in 669 y 670 end 671*) 672 673fun input_number P message = 674 let 675 val _ = print message 676 in 677 case TextIO.inputLine TextIO.stdIn 678 of NONE => input_number P message 679 | SOME s => case Int.fromString s 680 of SOME n => if P n then n else input_number P message 681 | NONE => input_number P message 682 end 683 684fun arm_run trace prog options count = 685 let 686 val state = init_config prog options 687 in 688 ptree_arm_run trace (prog, state) count 689 end 690 691fun main () = 692 let 693 val prog = load_programs (CommandLine.arguments()) 694 val _ = print "Enter architecture, initial register values and default\ 695 \ memory content.\n(Enter values as Hex.)\n\ 696 \For example: arch = ARMv7-A, pc = A00, r0 = AF, r_ = 10,\n\ 697 \ cpsr = 80000010, _psr = 10, mem_ = 0\n> " 698 val options = valOf (TextIO.inputLine TextIO.stdIn) 699 val trace = input_number (fn i => 0 <= i andalso i <= 5) 700 "Enter trace level [0 - 5]: " 701 val count = input_number (fn i => ~1 <= i) "Enter number of cycles: " 702 in 703 case time (arm_run (int_to_trace trace) prog options) count 704 of out as (_, SOME _) => print_arm_run prog out 705 | (e, NONE) => out [e] 706 end 707 708(* 709let 710 fun pp _ _ (_: 'a patriciaML.ptree) = PolyML.PrettyString "?" 711in 712 PolyML.addPrettyPrinter pp 713end; 714val prog = load_programs ["md5.o"]; 715val options = "pc = 8000, r0 = C0000, lr = A0000, sp = B0000, cpsr = 10"; 716val trace = 5; 717 718PolyML.shareCommonData main; 719PolyML.export("HOLarm", main); 720 721gcc -o run HOLarm.o -L$HOME/polyml/lib -lpolymain -lpolyml 722*) 723 724end 725 726(* ------------------------------------------------------------------------ *) 727