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