1(* interactive use: 2val HOLDIR = "/local/scratch/acjf3/hol98/"; 3val _ = loadPath := !loadPath @ ".." :: map (fn x => HOLDIR ^ x) 4 ["tools/mlyacc/mlyacclib", "tools/mlton/pre", 5 "src/portableML", "src/theoryML"]; 6val _ = app load ["assemblerML", "armML"]; 7val _ = app load ["OS", "Bool", "Time", "Timer", "CommandLine", "ListPair"]; 8*) 9 10(* ------------------------------------------------------------------------- *) 11 12exception Parse; 13 14fun toWord s i = wordsML.n2w_itself(i, fcpML.ITSELF(numML.fromInt s)); 15 16fun toWord4 i = toWord 4 (numML.fromInt i): wordsML.word4 17val toWord30 = toWord 30: numML.num -> wordsML.word30; 18val toWord32 = toWord 32: numML.num -> wordsML.word32 19 20val num2Arbnum = Arbnum.fromHexString o numML.toHexString; 21 22fun string2num s = 23 case String.explode s of 24 (#"0"::(#"x"::ls)) => numML.fromHexString (String.extract(s,2,NONE)) 25 | (#"0"::(#"b"::ls)) => numML.fromBinString (String.extract(s,2,NONE)) 26 | (#"0"::ls) => numML.fromOctString (String.extract(s,1,NONE)) 27 | ls => numML.fromString s; 28 29fun toHexString_w2n n = "0x" ^ numML.toHexString (wordsML.w2n n); 30 31fun for base top f = 32 let fun For i = if i>top then [] else f i::For(i+1) in For base end; 33 34fun for_se base top f = 35 let fun For i = if i>top then () else (f i; For(i+1)) in For base end; 36 37(* ------------------------------------------------------------------------- *) 38 39fun string2mode s = 40 case s of 41 "usr" => armML.usr 42 | "fiq" => armML.fiq 43 | "irq" => armML.irq 44 | "svc" => armML.svc 45 | "abt" => armML.abt 46 | "und" => armML.und 47 | _ => raise Parse; 48 49fun mode2string m = 50 case m of 51 armML.usr => "usr" 52 | armML.fiq => "fiq" 53 | armML.irq => "irq" 54 | armML.svc => "svc" 55 | armML.abt => "abt" 56 | armML.und => "und" 57 | _ => ""; 58 59fun register2string r = 60 case r of 61 armML.r0 => "r0" | armML.r1 => "r1" | armML.r2 => "r2" 62 | armML.r3 => "r3" | armML.r4 => "r4" | armML.r5 => "r5" 63 | armML.r6 => "r6" | armML.r7 => "r7" | armML.r8 => "r8" 64 | armML.r9 => "r9" | armML.r10 => "r10" | armML.r11 => "r11" 65 | armML.r12 => "r12" | armML.r13 => "sp" | armML.r14 => "lr" 66 | armML.r15 => "pc" 67 | armML.r8_fiq => "r8_fiq" | armML.r9_fiq => "r9_fiq" 68 | armML.r10_fiq => "r10_fiq" | armML.r11_fiq => "r11_fiq" 69 | armML.r12_fiq => "r12_fiq" | armML.r13_fiq => "r13_fiq" 70 | armML.r14_fiq => "r14_fiq" 71 | armML.r13_irq => "r13_irq" | armML.r14_irq => "r14_fiq" 72 | armML.r13_svc => "r13_svc" | armML.r14_svc => "r14_svc" 73 | armML.r13_abt => "r13_abt" | armML.r14_abt => "r14_abt" 74 | armML.r13_und => "r13_und" | armML.r14_und => "r14_und"; 75 76local 77 fun namedReg s = toWord4 78 (case s of 79 "sl" => 10 80 | "fp" => 11 81 | "ip" => 12 82 | "sp" => 13 83 | "lr" => 14 84 | "pc" => 15 85 | _ => raise Parse); 86 87 fun toReg(x, y) = 88 case Int.fromString (String.implode x) of 89 SOME i => if i < 16 then (toWord4 i, y) else raise Parse 90 | NONE => raise Parse 91 92 fun toNamedReg(x, y) = (namedReg(String.implode (map Char.toLower x)),y) 93 94 fun getReg l = 95 case l of 96 [r, n1] => (if Char.toUpper r = #"R" then toReg([n1],[]) 97 else toNamedReg([r,n1],[])) 98 | r :: (n1 :: (n2 :: ls)) => 99 if Char.toUpper r = #"R" then 100 if n1 = #"1" then 101 if Char.isDigit n2 then toReg([n1,n2],ls) 102 else (toWord4 1, n2::ls) 103 else 104 toReg([n1],n2::ls) 105 else toNamedReg([r,n1], n2::ls) 106 | _ => raise Parse 107 108 fun getRegister l = 109 let val (i,rest) = getReg l in 110 case rest of 111 [] => (i,armML.usr) 112 | (#"_" :: ls) => 113 if length ls = 3 then 114 (i,string2mode (String.implode (map Char.toLower ls))) 115 else 116 raise Parse 117 | _ => raise Parse 118 end 119in 120 val register = getRegister o String.explode; 121end; 122 123(* ------------------------------------------------------------------------- *) 124 125datatype env = 126 ENV of {N:bool, Z:bool, C:bool, V:bool, M:armML.mode, 127 Wreg:bool, Wmem:bool, Wmode:bool, Wflags:bool, 128 Wireg:bool, cycles:int, E:bool, mem:string, reg:armML.registers, 129 psr:armML.psrs}; 130 131fun update_switch fld (ENV e) = 132 let val {N,Z,C,V,E,M,mem,reg,cycles,Wreg,Wmem,Wmode,Wflags,Wireg,psr} = e 133 in 134 ENV 135 {N = if fld = "N" then true else N, 136 Z = if fld = "Z" then true else Z, 137 C = if fld = "Z" then true else C, 138 V = if fld = "V" then true else V, 139 E = if fld = "E" then true else E, 140 Wreg = if fld = "Wreg" orelse fld = "Wall" then true else Wreg, 141 Wmem = if fld = "Wmem" orelse fld = "Wall" then true else Wmem, 142 Wmode = if fld = "Wmode" orelse fld = "Wall" then true else Wmode, 143 Wflags = if fld = "Wflags" orelse fld = "Wall" then true else Wflags, 144 Wireg = if fld = "Wireg" orelse fld = "Wall" then true else Wireg, 145 M = M, mem = mem, reg = reg, cycles = cycles, psr = psr} 146 end; 147 148fun update_cycles i (ENV e) = 149 let val {N,Z,C,V,E,M,mem,reg,cycles,Wreg,Wmem,Wmode,Wflags,Wireg,psr} = e in 150 ENV {N = N, Z = Z, C = C, V = V, E = E, M = M, mem = mem, reg = reg, 151 cycles = i, Wreg = Wreg, Wmem = Wmem, Wmode = Wmode, Wflags = Wflags, 152 Wireg = Wireg, psr = psr} 153 end; 154 155fun update_mode m (ENV e) = 156 let val {N,Z,C,V,E,M,mem,reg,cycles,Wreg,Wmem,Wmode,Wflags,Wireg,psr} = e in 157 ENV {N = N, Z = Z, C = C, V = V, E = E, M = m, mem = mem, reg = reg, 158 cycles = cycles, Wreg = Wreg, Wmem = Wmem, Wmode = Wmode, 159 Wflags = Wflags, Wireg = Wireg, psr = psr} 160 end; 161 162fun update_mem m (ENV e) = 163 let val {N,Z,C,V,E,M,mem,reg,cycles,Wreg,Wmem,Wmode,Wflags,Wireg,psr} = e in 164 ENV {N = N, Z = Z, C = C, V = V, E = E, M = M, mem = m, reg = reg, 165 cycles = cycles, Wreg = Wreg, Wmem = Wmem, Wmode = Wmode, 166 Wflags = Wflags, Wireg = Wireg, psr = psr} 167 end; 168 169fun update_reg r (ENV e) = 170 let val {N,Z,C,V,E,M,mem,reg,cycles,Wreg,Wmem,Wmode,Wflags,Wireg,psr} = e in 171 ENV {N = N, Z = Z, C = C, V = V, E = E, M = M, mem = mem, reg = r, 172 cycles = cycles, Wreg = Wreg, Wmem = Wmem, Wmode = Wmode, 173 Wflags = Wflags, Wireg = Wireg, psr = psr} 174 end; 175 176fun update_psr (p, n) (ENV e) = 177 let val {N,Z,C,V,E,M,mem,reg,cycles,Wreg,Wmem,Wmode,Wflags,Wireg,psr} = e in 178 ENV {N = N, Z = Z, C = C, V = V, E = E, M = M, mem = mem, reg = reg, 179 cycles = cycles, Wreg = Wreg, Wmem = Wmem, Wmode = Wmode, 180 Wflags = Wflags, Wireg = Wireg, psr = combinML.UPDATE p n psr} 181 end; 182 183fun proj_ENV (ENV e) = e; 184val toLowerString = String.map Char.toLower; 185val toSpaces = String.map (fn _ => #" "); 186 187val usage_message = let val x = "Usage: " ^ CommandLine.name() in 188 "An ARM emulator (generated from a HOL model of the ARM7's ISA).\n" ^ 189 x ^ " [-cycles n] [-rN_m n] [-SPSR_m n] [-N] [-Z] [-C] [-V] [-M m] [-E]\n" ^ 190 toSpaces x ^ " [-Wreg] [-Wmem] [-Wmode] [-Wflags] [-Wireg] [-Wall] file\n" ^ 191 "Options:\n\ 192 \-cycles n - upper limit on the run length (will be " ^ 193 Int.toString (valOf Int.maxInt) ^ " by default)\n\ 194 \-rN_m n - set a Register e.g. -r8_fiq 0x20 -pc 0b101100\n\ 195 \-SPSR_m n - set a Saved Program Status Register e.g. -SPSR_svc 0x20\n\ 196 \-N - set the Negative flag (will be clear by default)\n\ 197 \-Z - set the Zero flag\n\ 198 \-C - set the Carry flag\n\ 199 \-V - set the oVerflow flag\n\ 200 \-M {usr,fiq,irq,svc,abt,und}\n\ 201 \ - set the mode (will be \"usr\" by default)\n\ 202 \-E - load the default \"rudimentary\" exception handler\n\ 203 \-Wreg - watch register updates\n\ 204 \-Wmem - watch memory updates\n\ 205 \-Wmode - watch mode changes\n\ 206 \-Wflags - watch changes to the status flags\n\ 207 \-Wireg - watch the instruction register\n\ 208 \-Wall - watch everything\n" 209end; 210 211fun setOptions l env = 212 let fun set_switch x rest = setOptions rest (update_switch x env) 213 fun set_psr x s rest = 214 setOptions rest (update_psr(x,toWord32 (string2num s)) env) 215 handle _ => setOptions (s::rest) env 216 in 217 case l of 218 [] => env 219 | ["--help"] => (print usage_message; OS.Process.exit OS.Process.success) 220 | ("-N"::ls) => set_switch "N" ls 221 | ("-Z"::ls) => set_switch "Z" ls 222 | ("-C"::ls) => set_switch "C" ls 223 | ("-V"::ls) => set_switch "V" ls 224 | ("-E"::ls) => set_switch "E" ls 225 | ("-Wreg"::ls) => set_switch "Wreg" ls 226 | ("-Wmem"::ls) => set_switch "Wmem" ls 227 | ("-Wmode"::ls) => set_switch "Wmode" ls 228 | ("-Wflags"::ls) => set_switch "Wflags" ls 229 | ("-Wireg"::ls) => set_switch "Wireg" ls 230 | ("-Wall"::ls) => set_switch "Wall" ls 231 | ("-M"::(s::ls)) => 232 (setOptions ls (update_mode (string2mode (toLowerString s)) env) 233 handle Parse => setOptions (s::ls) env) 234 | ("-cycles"::(s::ls)) => 235 (case Int.fromString s of 236 SOME i => setOptions ls (update_cycles i env) 237 | NONE => setOptions (s::ls) env) 238 | ("-SPSR_fiq"::(s::ls)) => set_psr armML.SPSR_fiq s ls 239 | ("-SPSR_irq"::(s::ls)) => set_psr armML.SPSR_irq s ls 240 | ("-SPSR_svc"::(s::ls)) => set_psr armML.SPSR_svc s ls 241 | ("-SPSR_abt"::(s::ls)) => set_psr armML.SPSR_abt s ls 242 | ("-SPSR_und"::(s::ls)) => set_psr armML.SPSR_und s ls 243 | (r::(s::ls)) => 244 (let val _ = String.sub(r,0) = #"-" orelse raise Parse 245 val reg = #reg (proj_ENV env) 246 val (n,m) = register (String.extract(r,1,NONE)) 247 val d = toWord32 (string2num s) 248 in 249 setOptions ls (update_reg (armML.REG_WRITE reg m n d) env) 250 end handle _ => setOptions (s::ls) env) 251 | [s] => update_mem s env 252 end; 253 254(* ------------------------------------------------------------------------- *) 255 256local 257 fun add1 a = Data.add32 a Arbnum.one; 258 fun div4 a = Arbnum.div(a,Arbnum.fromInt 4); 259 fun mul4 a = Arbnum.*(a,Arbnum.fromInt 4); 260 val start = Arbnum.zero; 261 val fromArbnum30 = toWord30 o numML.fromHexString o Arbnum.toHexString; 262 val fromArbnum32 = toWord32 o numML.fromHexString o Arbnum.toHexString; 263 264 fun mk_links [] dict n = dict 265 | mk_links (h::r) dict n = 266 case h of 267 Data.Code c => mk_links r dict (add1 n) 268 | Data.BranchS b => mk_links r dict (add1 n) 269 | Data.BranchN b => mk_links r dict (add1 n) 270 | Data.Label s => 271 mk_links r 272 (Redblackmap.insert(dict, s, "0x" ^ Arbnum.toHexString (mul4 n))) n 273 | Data.Mark m => mk_links r dict (div4 m); 274 275 fun mk_link_table code = 276 let val dict = Redblackmap.mkDict String.compare in 277 mk_links code dict start 278 end; 279 280 fun br_to_word32 (cond,link,label) dict n = 281 let val s = assemblerML.assembler_to_string 282 NONE (Data.BranchS(cond,link,"")) NONE 283 val address = Redblackmap.find(dict, label) 284 in 285 (fromArbnum32 o assemblerML.encode_arm) 286 ("0x" ^ Arbnum.toHexString (mul4 n) ^ ": " ^ s ^ address) 287 end; 288 289 fun is_label (Data.Label s) = true | is_label _ = false; 290 291 fun lcons h [] = [[h]] 292 | lcons h (x::l) = (h::x)::l; 293 294 fun do_link m l [] dict n = ListPair.zip(m, l) 295 | do_link m l (h::r) dict n = 296 case h of 297 Data.Code c => 298 do_link m (lcons (fromArbnum32 (assemblerML.arm_to_num 299 (assemblerML.validate_instruction c))) l) r dict (add1 n) 300 | Data.BranchS b => 301 do_link m (lcons (br_to_word32 b dict n) l) r dict (add1 n) 302 | Data.BranchN b => 303 let val t = fromArbnum32 (assemblerML.arm_to_num 304 (assemblerML.branch_to_arm b (mul4 n))) 305 in 306 do_link m (lcons t l) r dict (add1 n) 307 end 308 | Data.Label s => do_link m l r dict n 309 | Data.Mark mk => let val k = div4 mk in 310 if k = n then 311 do_link m l r dict n 312 else if null (hd l) then 313 do_link (k::(tl m)) l r dict k 314 else 315 do_link (k::m) ([]::l) r dict k 316 end; 317 318 fun do_links code = 319 let val l = do_link [start] [[]] code (mk_link_table code) start in 320 rev (map (fn (a,b) => (a,rev b)) l) 321 end; 322 323 fun assemble_assembler m a = let 324 val l = do_links a 325 val b = map (fn (m,c) => (fromArbnum30 m, c)) l 326 in 327 foldr (fn ((a,c),t) => updateML.mem_write_block t a c) m b 328 end 329in 330 fun assemble m file = assemble_assembler m (assemblerML.parse_arm file); 331 fun list_assemble m l = 332 let val c = String.concat (map (fn s => s ^ "\n") l) 333 in 334 assemble_assembler m (assemblerML.string_to_code c) 335 end; 336 fun assemble1 m t = list_assemble m [t]; 337end; 338 339(* ------------------------------------------------------------------------- *) 340 341local 342 fun regName(i, m) = "r" ^ (Int.toString i) ^ 343 (if m = armML.usr orelse i < 8 orelse i = 15 orelse 344 i <= 12 andalso not (m = armML.fiq) then "" else "_" ^ mode2string m); 345 346 fun regString reg (i, m) = regName(i, m) ^ " = " ^ 347 toHexString_w2n (armML.REG_READ reg m (toWord4 i)); 348 349 fun print_reg ostrm reg i = 350 if i < 8 then 351 TextIO.output(ostrm,regString reg (i, armML.usr) ^ "\n") 352 else if i <= 12 then 353 (TextIO.output(ostrm,regString reg (i, armML.usr) ^ "; "); 354 TextIO.output(ostrm,regString reg (i, armML.fiq) ^ "\n")) 355 else if i < 15 then 356 (app (fn m => TextIO.output(ostrm,regString reg (i, m) ^ "; ")) 357 [armML.usr, armML.fiq, armML.irq, armML.svc, armML.abt]; 358 TextIO.output(ostrm,regString reg (i, armML.und) ^ "\n")) 359 else 360 TextIO.output(ostrm, 361 "r15 = " ^ toHexString_w2n (armML.FETCH_PC reg) ^ "\n"); 362 363 fun print_psr ostrm s p = 364 let 365 val ((n,(z,(c,v))),(i,(f,m))) = armML.DECODE_PSR p 366 val m = armML.DECODE_MODE m 367 in 368 TextIO.output(ostrm, 369 s ^ " = {N = " ^ Bool.toString n ^ ", " ^ 370 "Z = " ^ Bool.toString z ^ ", " ^ 371 "C = " ^ Bool.toString c ^ ", " ^ 372 "V = " ^ Bool.toString v ^ ",\n" ^ 373 toSpaces (s ^ " = {") ^ 374 "I = " ^ Bool.toString i ^ ", " ^ 375 "F = " ^ Bool.toString f ^ ", " ^ 376 "mode = " ^ mode2string m ^ "}\n") 377 end; 378 379 fun print_line ostrm (l,c) = 380 let val n = numML.* (wordsML.w2n l) (numML.fromInt 4) 381 val m = wordsML.w2n c 382 in 383 TextIO.output(ostrm, 384 "0x" ^ numML.toHexString n ^ ": 0x" ^ numML.toHexString m ^ "; "); 385 TextIO.output(ostrm, 386 assemblerML.decode_arm (SOME (num2Arbnum n)) (num2Arbnum m) ^ "\n") 387 end 388in 389 fun print_state fname state count = 390 let val ostrm = TextIO.openOut fname 391 val reg = armML.arm_sys_state_registers state 392 val psr = armML.arm_sys_state_psrs state 393 val mem = armML.arm_sys_state_memory state 394 val items = updateML.mem_items mem 395 in 396 TextIO.output(ostrm,"Instuctions Run:" ^ Int.toString count ^ "\n"); 397 TextIO.output(ostrm,"\nRegisters\n---------\n"); 398 for_se 0 15 (print_reg ostrm reg); 399 400 TextIO.output(ostrm,"\nProgram Status\n--------------\n"); 401 print_psr ostrm "CPSR" (armML.CPSR_READ psr); 402 print_psr ostrm "SPSR_fiq" (armML.SPSR_READ psr armML.fiq); 403 print_psr ostrm "SPSR_irq" (armML.SPSR_READ psr armML.irq); 404 print_psr ostrm "SPSR_svc" (armML.SPSR_READ psr armML.svc); 405 print_psr ostrm "SPSR_abt" (armML.SPSR_READ psr armML.abt); 406 print_psr ostrm "SPSR_und" (armML.SPSR_READ psr armML.und); 407 408 if items = [] then () else 409 (TextIO.output(ostrm,"\nMemory\n------\n"); 410 map (print_line ostrm) items;()); 411 412 TextIO.closeOut ostrm 413 end 414end; 415 416(* ------------------------------------------------------------------------- *) 417 418val int2register = armML.num2register o numML.fromInt; 419 420fun gen_tabulate f g n = 421 let fun do_tab i l = 422 if i = 0 then l 423 else let val x = i - 1 in 424 do_tab x (if f x then (g x)::l else l) 425 end 426 in 427 do_tab n [] 428 end; 429 430fun reg_updates reg1 reg2 = 431 gen_tabulate 432 (fn i => let val r = int2register i in not (reg1 r = reg2 r) end) 433 int2register 31; 434 435fun printer (Wreg, Wmem, Wmode, Wflags, Wireg) cycle s ns = 436 if Wireg orelse Wreg orelse Wmem orelse Wflags orelse Wmode then 437 let val reg1 = armML.arm_sys_state_registers s 438 val reg2 = armML.arm_sys_state_registers ns 439 val mem1 = armML.arm_sys_state_memory s 440 val mem2 = armML.arm_sys_state_memory ns 441 val cpsr1 = armML.CPSR_READ (armML.arm_sys_state_psrs s) 442 val cpsr2 = armML.CPSR_READ (armML.arm_sys_state_psrs ns) 443 val (nzcv1, (i1, (f1, m1))) = armML.DECODE_PSR cpsr1 444 val (nzcv2, (i2, (f2, m2))) = armML.DECODE_PSR cpsr2 445 446 fun print_ireg ireg = print ("> " ^ 447 assemblerML.decode_arm NONE (num2Arbnum (wordsML.w2n ireg)) ^ 448 "\n") 449 450 fun print_reg i = print 451 ("; " ^ register2string i ^ " := " ^ toHexString_w2n (reg2(i))) 452 453 fun print_mem a = print 454 ("; mem[" ^ toHexString_w2n a ^ "] := " ^ 455 toHexString_w2n (updateML.mem_read(mem2,a))) 456 457 fun print_bool b = print (if b then "1" else "0") 458 fun print_nzcv (n,(z,(c, v))) = (print "; NZCV := "; 459 print_bool n; print_bool z; print_bool c; print_bool v) 460 461 fun print_mode m = print 462 ("; mode := " ^ mode2string (armML.DECODE_MODE m)) 463 in 464 ((if Wireg then 465 if armML.arm_sys_state_undefined s then 466 print "> undefined exception\n" 467 else 468 print_ireg 469 (updateML.mem_read(mem1,updateML.addr30 (armML.FETCH_PC reg1))) 470 else 471 ()); 472 print ("- t = " ^ Int.toString cycle); 473 (if Wreg then app print_reg (reg_updates reg1 reg2) else ()); 474 (if Wmem then app print_mem (rev (!updateML.mem_updates)) else ()); 475 (if not Wflags orelse nzcv1 = nzcv2 then () else print_nzcv nzcv2); 476 (if not Wmode orelse m1 = m2 then () else print_mode m2); 477 print "\n") 478 end 479 else 480 (); 481 482(* ------------------------------------------------------------------------- *) 483(* Taken from Joe Hurd's $HOLDIR/tools/mlton/src/mlibPortable.sml *) 484 485fun time f x = 486 let 487 fun p t = 488 let 489 val s = Time.fmt 3 t 490 in 491 case size (List.last (String.fields (fn x => x = #".") s)) of 3 => s 492 | 2 => s ^ "0" 493 | 1 => s ^ "00" 494 | _ => raise Fail "time" 495 end 496 val c = Timer.startCPUTimer () 497 val r = Timer.startRealTimer () 498 fun pt () = 499 let 500 val {usr, sys, gc} = Timer.checkCPUTimer c 501 val real = Timer.checkRealTimer r 502 in 503 print 504 ("User: " ^ p usr ^ " System: " ^ p sys ^ 505 " GC: " ^ p gc ^ " Real: " ^ p real ^ "\n") 506 end 507 val y = f x handle e => (pt (); raise e) 508 val () = pt () 509 in 510 y 511 end; 512 513(* ------------------------------------------------------------------------- *) 514 515val env = 516 let val initial_psr = armML.SET_NZCV (false,(false,(false,false))) 517 (armML.SET_IFMODE false false armML.usr (toWord32 (numML.fromInt 0))) 518 in 519 ENV {N = false, Z = false, C = false, V = false, E = false, M = armML.usr, 520 mem = "", reg = armML.empty_registers, psr = fn x => initial_psr, 521 cycles = valOf Int.maxInt, Wreg = false, Wmem = false, Wmode = false, 522 Wflags = false, Wireg = false} 523 end; 524 525val e = proj_ENV (setOptions (CommandLine.arguments()) env); 526val watches = (#Wreg e, #Wmem e, #Wmode e, #Wflags e, #Wireg e); 527 528val count = ref 0; 529 530fun STATE_ARM_MEM n s = 531 if n = 0 then s 532 else 533 let val _ = count := !count + 1 534 val _ = updateML.mem_updates := [] 535 val ns = armML.NEXT_ARM_MEM s 536 val _ = printer watches (!count) s ns 537 in 538 if armML.arm_sys_state_undefined s then 539 ns 540 else 541 STATE_ARM_MEM (n - 1) ns 542 end; 543 544(* ------------------------------------------------------------------------- *) 545 546val init_mem = if #E e then 547 list_assemble updateML.empty_memory 548 ["0x0: movs pc, #32", 549 "label: b label", 550 "movs pc, r14", 551 "subs pc, r14, #4", 552 "subs pc, r14, #8", 553 "movs pc, r14", 554 "subs pc, r14, #4", 555 "subs pc, r14, #4"] 556 else updateML.empty_memory; 557 558val init_mem = 559 let val m = #mem e in 560 if not (m = "") then 561 assemble init_mem m handle _ => 562 raise Fail ("Could not load file: " ^ m) 563 else 564 init_mem 565 end; 566 567val cpsr = armML.SET_NZCV (#N e,(#Z e,(#C e,#V e))) 568 (armML.SET_IFMODE false false (#M e) (toWord32 (numML.fromInt 0))); 569 570val psr = armML.CPSR_WRITE (#psr e) cpsr; 571 572val init_state = armML.arm_sys_state (#reg e, psr, init_mem, false, ()); 573 574val final_state = time (STATE_ARM_MEM (#cycles e)) init_state; 575 576val _ = print_state "run.in" init_state 0; 577val _ = print_state "run.out" final_state (!count); 578 579(* ------------------------------------------------------------------------- *) 580 581