1open HolKernel Parse boolLib bossLib
2open armLib arm_random_testingLib;
3
4val ERR = mk_HOL_ERR "selftest"
5
6val _ = wordsLib.guess_lengths();
7
8val _ = set_trace "Unicode" 0;
9val _ = set_trace "arm steps" 3;
10val _ = set_trace "arm step" 2;
11val _ = set_trace "arm step check" 1;
12val _ = set_trace "notify type variable guesses" 0;
13val _ = set_trace "notify word length guesses" 0;
14
15fun die() = ()
16fun die() = OS.Process.exit OS.Process.failure
17
18fun test str f x = let
19  val rt = Timer.startRealTimer ()
20  val res = Lib.total f x
21  val elapsed = Timer.checkRealTimer rt
22in
23  TextIO.print ("\n" ^ str ^ " ... " ^ Time.toString elapsed ^ "s" ^
24                (case res of NONE => "FAILED!\n" | _ => "\n\n"));
25  case res of NONE => die() | _ => ()
26end
27
28local
29  val updates_compare = Lib.pair_compare (Term.compare, Term.compare)
30  val updates_empty = Redblackset.empty updates_compare
31  fun updates_to_set l = Redblackset.addList (updates_empty, l)
32  fun print_differences (s1,s2) = let
33        val delta = Redblackset.listItems o Redblackset.difference
34        val d1 = delta (s1, s2)
35        val d2 = delta (s2, s1)
36        val t2s = trace ("types",2) term_to_string
37        fun update (l,r) = "[" ^ t2s l ^ " <- " ^ t2s r ^ "]\n"
38      in
39        print "Expecting:\n";
40        List.app (print o update) d2;
41        print "\nGot:\n";
42        List.app (print o update) d1
43      end
44in
45  fun step opt instr =
46  let
47    val opc = case arm_assemble_from_string instr
48              of ([(_,n)],_) => n
49               | _ => raise ERR "validate_arm_step" ""
50  in
51    case arm_step_updates opt opc
52    of (_, Simple_step l) => l
53     | _ => raise ERR "validate_arm_step" ""
54  end
55
56  fun validate_arm_step opt (instr,upds) =
57  let
58    val _ = print ("Validating step theorem for: " ^ instr ^ " ...\n")
59    val cmp = (updates_to_set (step opt instr), updates_to_set upds)
60  in
61    Redblackset.equal cmp orelse
62      (print_differences cmp; raise ERR "validate_arm_step" "")
63  end
64end
65
66fun flag tm = mk_var (fst (dest_const tm), bool);
67fun spsr_flag tm = mk_var ("s" ^ fst (dest_const tm), bool);
68
69val psrN = flag ``psrN``
70val psrZ = flag ``psrZ``
71val psrC = flag ``psrC``
72val psrV = flag ``psrV``
73val psrQ = flag ``psrQ``
74val psrE = flag ``psrE``
75val psrA = flag ``psrA``
76val psrI = flag ``psrI``
77val psrF = flag ``psrF``
78val psrJ = flag ``psrJ``
79val psrT = flag ``psrT``
80
81val spsrN = spsr_flag ``psrN``
82val spsrZ = spsr_flag ``psrZ``
83val spsrC = spsr_flag ``psrC``
84val spsrV = spsr_flag ``psrV``
85val spsrQ = spsr_flag ``psrQ``
86val spsrE = spsr_flag ``psrE``
87val spsrA = spsr_flag ``psrA``
88val spsrI = spsr_flag ``psrI``
89val spsrF = spsr_flag ``psrF``
90val spsrJ = spsr_flag ``psrJ``
91val spsrT = spsr_flag ``psrT``
92
93val sctlrNMFI = flag ``sctlrNMFI``
94
95val GE = mk_var ("GE", ``:word4``);
96val spsrGE = mk_var ("spsrGE", ``:word4``);
97
98val mode = mk_var ("mode", ``:word5``);
99val spsrmode = mk_var ("spsrmode", ``:word5``);
100
101fun reg i = mk_var ("r" ^ Int.toString i, ``:word32``);
102
103val r0  = reg 0
104val r1  = reg 1
105val r2  = reg 2
106val r3  = reg 3
107val r4  = reg 4
108val r5  = reg 5
109val r6  = reg 6
110val r7  = reg 7
111val r8  = reg 8
112val r9  = reg 9
113val r10 = reg 10
114val r11 = reg 11
115val r12 = reg 12
116val r13 = reg 13
117val r14 = reg 14
118val r15 = reg 15
119
120val mem = mk_var ("mem", ``:word32 -> word8``);
121
122val _ = print "Starting tests ... \n\n";
123
124val tt = Timer.startRealTimer ()
125
126(* start tests *)
127
128val _ = test "print_arm_assemble_from_quote" (print_arm_assemble_from_quote "0")
129  `     ARCH    ARMv7
130        ARM
131        ALIGN   4
132
133        ASCII   "abcd"
134        BYTE    31,32
135        SHORT   0xfaDB
136        WORD    0b100010000,07030
137
138        SPACE   20
139
140        ALIGN   8
141
142        adc     r1,#99
143        adc     r1,r2
144        adcs    r1,r2,#0xFF0000
145        adc     pc,r3,r4,asr #29
146.label: adc     sp,r3,r4,lsl lr
147        adc     lr,r4,ror #0b1000
148        adc     r8,r9,r4,rrx
149
150        adr     sp,.label
151        adr     r1,+#0xab0008
152        adr     r2,-#20
153
154        asr     r3,#11
155        asr     r3,r9
156        asr     r3,r9,r4
157        rrx     r3
158        rrx     r3,r5
159        ror     r3,r5
160
161        beq     .label
162        bne     .label
163        bcs     .label
164        bcc     .label
165        bmi     .label
166        bpl     .label
167        bvs     .label
168        bvc     .label
169        bhi     .label
170        bls     .label
171        bge     .label
172        blt     .label
173        bgt     .label
174        ble     .label
175        `;
176
177(*
178val go = step "v6";
179*)
180val _ = test "validate_arm_step" (fn l => List.map (validate_arm_step "v6") l)
181  [("ldr pc,[pc,r2,lsl #2]",
182    [(psrT,
183       ``(^mem (r15 + 8w + r2 << 2 + 3w) @@ mem (r15 + 8w + r2 << 2 + 2w) @@
184           mem (r15 + 8w + r2 << 2 + 1w) @@ mem (r15 + 8w + r2 << 2)) ' 0``),
185     (r15,
186       ``if
187           (^mem (r15 + 8w + r2 << 2 + 3w) @@ mem (r15 + 8w + r2 << 2 + 2w) @@
188             mem (r15 + 8w + r2 << 2 + 1w) @@ mem (r15 + 8w + r2 << 2)) ' 0
189         then
190           align
191             (mem (r15 + 8w + r2 << 2 + 3w) @@ mem (r15 + 8w + r2 << 2 + 2w) @@
192              mem (r15 + 8w + r2 << 2 + 1w) @@ mem (r15 + 8w + r2 << 2),2)
193         else
194              mem (r15 + 8w + r2 << 2 + 3w) @@ mem (r15 + 8w + r2 << 2 + 2w) @@
195              mem (r15 + 8w + r2 << 2 + 1w) @@ mem (r15 + 8w + r2 << 2)``)])];
196
197(*
198val go = step "v4";
199*)
200val _ = test "validate_arm_step" (fn l => List.map (validate_arm_step "v4") l)
201  [("ldm r1!,{r1,r2}",
202    [(r1, ``ARB:word32``),
203     (r15, ``^r15 + 4w``),
204     (r2, ``^mem (r1 + 7w) @@ mem (r1 + 6w) @@
205             mem (r1 + 5w) @@ mem (r1 + 4w)``)]),
206   ("stm r1!,{r0,r1}",
207    [(``^mem (r1 + 7w)``, ``ARB:word8``),
208     (``^mem (r1 + 6w)``, ``ARB:word8``),
209     (``^mem (r1 + 5w)``, ``ARB:word8``),
210     (``^mem (r1 + 4w)``, ``ARB:word8``),
211     (``^mem (r1 + 3w)``, ``(31 >< 24) ^r0``),
212     (``^mem (r1 + 2w)``, ``(23 >< 16) ^r0``),
213     (``^mem (r1 + 1w)``, ``(15 >< 8) ^r0``),
214     (``^mem r1``, ``(7 >< 0) ^r0``),
215     (r1, ``^r1 + 8w``),
216     (r15, ``^r15 + 4w``)]),
217   ("TST r5, #3",
218    [(psrN, ``word_msb (^r5 && 3w)``),
219     (psrZ, ``(^r5) && 3w = 0w``),
220     (r15, ``^r15 + 4w``)]),
221   ("ADD r1, #10",
222    [(r1, ``^r1 + 10w``),
223     (r15, ``^r15 + 4w``)]),
224   ("CMP r1, #10",
225    [(psrN, ``word_msb (^r1 + 0xFFFFFFF6w)``),
226     (psrZ, ``^r1 + 0xFFFFFFF6w = 0w``),
227     (psrC, ``CARRY_OUT ^r1 0xFFFFFFF5w T``),
228     (psrV, ``OVERFLOW ^r1 0xFFFFFFF5w T``),
229     (r15, ``^r15 + 4w``)]),
230   ("TST r2, #6",
231    [(psrN, ``word_msb (^r2 && 6w)``),
232     (psrZ, ``^r2 && 6w = 0w``),
233     (r15, ``^r15 + 4w``)]),
234   ("SUBCS r1, r1, #10",
235    [(r1, ``^r1 + 0xFFFFFFF6w``),
236     (r15, ``^r15 + 4w``)]),
237   ("MOV r0, #0",
238    [(r0, ``0w : word32``),
239     (r15, ``^r15 + 4w``)]),
240   ("CMP r1, #0",
241    [(psrN, ``word_msb ^r1``),
242     (psrZ, ``^r1 = 0w``),
243     (psrC, ``CARRY_OUT ^r1 0xFFFFFFFFw T``),
244     (psrV, ``OVERFLOW ^r1 0xFFFFFFFFw T``),
245     (r15, ``^r15 + 4w``)]),
246   ("ADDNE r0, r0, #1",
247    [(r0, ``^r0 + 1w``),
248     (r15, ``^r15 + 4w``)]),
249   ("LDRNE r1, [r1]",
250    [(r1, ``^mem (r1 + 3w) @@ mem (r1 + 2w) @@ mem (r1 + 1w) @@ mem r1``),
251     (r15, ``^r15 + 4w``)]),
252   ("BNE -#12",
253    [(r15, ``^r15 + 0xFFFFFFF4w``)]),
254   ("MOVGT r2, #5",
255    [(r2, ``5w : word32``),
256     (r15, ``^r15 + 4w``)]),
257   ("LDRBNE r2, [r3]",
258    [(r2, ``w2w (^mem r3) : word32``),
259     (r15, ``^r15 + 4w``)]),
260   ("BNE +#420",
261    [(r15, ``^r15 + 420w``)]),
262   ("LDRLS r2, [r11, #-40]",
263    [(r2,
264     ``^mem (r11 + 0xFFFFFFDBw) @@ mem (r11 + 0xFFFFFFDAw) @@
265        mem (r11 + 0xFFFFFFD9w) @@ mem (r11 + 0xFFFFFFD8w)``),
266    (r15, ``^r15 + 4w``)]),
267   ("SUBLS r2, r2, #1",
268    [(r2, ``^r2 + 0xFFFFFFFFw``),
269     (r15, ``^r15 + 4w``)]),
270   ("SUBLS r11, r11, #4",
271    [(r11, ``^r11 + 0xFFFFFFFCw``),
272     (r15, ``^r15 + 4w``)]),
273   ("MOVGT r12, r0",
274    [(r12, ``^r0``),
275     (r15, ``^r15 + 4w``)]),
276   ("ADD r0, pc, #16",
277    [(r0, ``^r15 + 24w``),
278     (r15, ``^r15 + 4w``)]),
279   ("SUB r0, pc, #60",
280    [(r0, ``^r15 + 0xFFFFFFCCw``),
281     (r15, ``^r15 + 4w``)]),
282   ("ADD r5, pc, #4096",
283    [(r5, ``^r15 + 4104w``),
284     (r15, ``^r15 + 4w``)]),
285   ("STRB r2, [r3]",
286    [(``^mem r3``, ``w2w ^r2 : word8``),
287     (r15, ``^r15 + 4w``)]),
288   ("STMIA r4, {r5-r10}",
289    [(``^mem (r4 + 23w)``, ``(31 >< 24) ^r10``),
290     (``^mem (r4 + 22w)``, ``(23 >< 16) ^r10``),
291     (``^mem (r4 + 21w)``, ``(15 >< 8) ^r10``),
292     (``^mem (r4 + 20w)``, ``(7 >< 0) ^r10``),
293     (``^mem (r4 + 19w)``, ``(31 >< 24) ^r9``),
294     (``^mem (r4 + 18w)``, ``(23 >< 16) ^r9``),
295     (``^mem (r4 + 17w)``, ``(15 >< 8) ^r9``),
296     (``^mem (r4 + 16w)``, ``(7 >< 0) ^r9``),
297     (``^mem (r4 + 15w)``, ``(31 >< 24) ^r8``),
298     (``^mem (r4 + 14w)``, ``(23 >< 16) ^r8``),
299     (``^mem (r4 + 13w)``, ``(15 >< 8) ^r8``),
300     (``^mem (r4 + 12w)``, ``(7 >< 0) ^r8``),
301     (``^mem (r4 + 11w)``, ``(31 >< 24) ^r7``),
302     (``^mem (r4 + 10w)``, ``(23 >< 16) ^r7``),
303     (``^mem (r4 + 9w)``, ``(15 >< 8) ^r7``),
304     (``^mem (r4 + 8w)``, ``(7 >< 0) ^r7``),
305     (``^mem (r4 + 7w)``, ``(31 >< 24) ^r6``),
306     (``^mem (r4 + 6w)``, ``(23 >< 16) ^r6``),
307     (``^mem (r4 + 5w)``, ``(15 >< 8) ^r6``),
308     (``^mem (r4 + 4w)``, ``(7 >< 0) ^r6``),
309     (``^mem (r4 + 3w)``, ``(31 >< 24) ^r5``),
310     (``^mem (r4 + 2w)``, ``(23 >< 16) ^r5``),
311     (``^mem (r4 + 1w)``, ``(15 >< 8) ^r5``),
312     (``^mem r4``, ``(7 >< 0) ^r5``),
313     (r15, ``^r15 + 4w``)]),
314   ("LDMIA r4, {r5-r10}",
315    [(r15, ``^r15 + 4w``),
316     (r10,
317      ``^mem (r4 + 23w) @@ mem (r4 + 22w) @@
318         mem (r4 + 21w) @@ mem (r4 + 20w)``),
319     (r9,
320      ``^mem (r4 + 19w) @@ mem (r4 + 18w) @@
321         mem (r4 + 17w) @@ mem (r4 + 16w)``),
322     (r8,
323      ``^mem (r4 + 15w) @@ mem (r4 + 14w) @@
324         mem (r4 + 13w) @@ mem (r4 + 12w)``),
325     (r7,
326      ``^mem (r4 + 11w) @@ mem (r4 + 10w) @@
327         mem (r4 + 9w) @@ mem (r4 + 8w)``),
328     (r6,
329      ``^mem (r4 + 7w) @@ mem (r4 + 6w) @@ mem (r4 + 5w) @@ mem (r4 + 4w)``),
330     (r5,
331      ``^mem (r4 + 3w) @@ mem (r4 + 2w) @@ mem (r4 + 1w) @@ mem r4``)]),
332   ("STRB r2, [r1], #1",
333    [(``^mem ^r1``, ``w2w ^r2 : word8``),
334     (r15, ``^r15 + 4w``),
335     (r1, ``^r1 + 1w``)]),
336   ("STMIB r8!, {r14}",
337    [(``^mem (r8 + 7w)``, ``(31 >< 24) ^r14``),
338     (``^mem (r8 + 6w)``, ``(23 >< 16) ^r14``),
339     (``^mem (r8 + 5w)``, ``(15 >< 8) ^r14``),
340     (``^mem (r8 + 4w)``, ``(7 >< 0) ^r14``),
341     (r8, ``^r8 + 4w``),
342     (r15, ``^r15 + 4w``)]),
343   ("LDR pc, [r8]",
344    [(r15, ``^mem (r8 + 3w) @@ mem (r8 + 2w) @@ mem (r8 + 1w) @@ mem r8``)]),
345   ("LDRLS pc, [r8], #-4",
346    [(r15, ``^mem (r8 + 3w) @@ mem (r8 + 2w) @@ mem (r8 + 1w) @@ mem r8``),
347     (r8, ``^r8 + 0xFFFFFFFCw``)]),
348   ("LDMIA sp!, {r0-r2, r15}",
349    [(r13, ``^r13 + 16w``),
350     (r15,
351      ``^mem (r13 + 15w) @@ mem (r13 + 14w) @@
352         mem (r13 + 13w) @@ mem (r13 + 12w)``),
353     (r2,
354      ``^mem (r13 + 11w) @@ mem (r13 + 10w) @@
355         mem (r13 + 9w) @@ mem (r13 + 8w)``),
356     (r1,
357      ``^mem (r13 + 7w) @@ mem (r13 + 6w) @@
358         mem (r13 + 5w) @@ mem (r13 + 4w)``),
359     (r0,
360      ``^mem (r13 + 3w) @@ mem (r13 + 2w) @@
361         mem (r13 + 1w) @@ mem r13``)]),
362   ("LDR r0, [pc, #308]",
363    [(r0,
364     ``^mem (r15 + 319w) @@ mem (r15 + 318w) @@
365        mem (r15 + 317w) @@ mem (r15 + 316w)``),
366    (r15, ``^r15 + 4w``)]),
367   ("LDR r1, [pc, #-20]",
368    [(r1,
369     ``^mem (r15 + 0xFFFFFFF7w) @@ mem (r15 + 0xFFFFFFF6w) @@
370        mem (r15 + 0xFFFFFFF5w) @@ mem (r15 + 0xFFFFFFF4w)``),
371    (r15, ``^r15 + 4w``)]),
372   ("STMDB sp!, {r0-r2, r15}",
373    [(``^mem (r13 + 0xFFFFFFFFw)``, ``(31 >< 24) (^r15 + 8w)``),
374     (``^mem (r13 + 0xFFFFFFFEw)``, ``(23 >< 16) (^r15 + 8w)``),
375     (``^mem (r13 + 0xFFFFFFFDw)``, ``(15 >< 8) (^r15 + 8w)``),
376     (``^mem (r13 + 0xFFFFFFFCw)``, ``(7 >< 0) (^r15 + 8w)``),
377     (``^mem (r13 + 0xFFFFFFFBw)``, ``(31 >< 24) ^r2``),
378     (``^mem (r13 + 0xFFFFFFFAw)``, ``(23 >< 16) ^r2``),
379     (``^mem (r13 + 0xFFFFFFF9w)``, ``(15 >< 8) ^r2``),
380     (``^mem (r13 + 0xFFFFFFF8w)``, ``(7 >< 0) ^r2``),
381     (``^mem (r13 + 0xFFFFFFF7w)``, ``(31 >< 24) ^r1``),
382     (``^mem (r13 + 0xFFFFFFF6w)``, ``(23 >< 16) ^r1``),
383     (``^mem (r13 + 0xFFFFFFF5w)``, ``(15 >< 8) ^r1``),
384     (``^mem (r13 + 0xFFFFFFF4w)``, ``(7 >< 0) ^r1``),
385     (``^mem (r13 + 0xFFFFFFF3w)``, ``(31 >< 24) ^r0``),
386     (``^mem (r13 + 0xFFFFFFF2w)``, ``(23 >< 16) ^r0``),
387     (``^mem (r13 + 0xFFFFFFF1w)``, ``(15 >< 8) ^r0``),
388     (``^mem (r13 + 0xFFFFFFF0w)``, ``(7 >< 0) ^r0``),
389     (r13, ``^r13 + 0xFFFFFFF0w``),
390     (r15, ``^r15 + 4w``)]),
391   ("SWPB r2, r4, [r3]",
392    [(``^mem r3``, ``w2w ^r4 : word8``),
393     (r2, ``w2w (^mem r3) : word32``),
394     (r15, ``^r15 + 4w``)]),
395   ("SWP r2, r4, [r3]",
396    [(``^mem (r3 + 3w)``, ``(31 >< 24) ^r4``),
397     (``^mem (r3 + 2w)``, ``(23 >< 16) ^r4``),
398     (``^mem (r3 + 1w)``, ``(15 >< 8) ^r4``),
399     (``^mem r3``, ``(7 >< 0) ^r4``),
400     (r2, ``^mem (r3 + 3w) @@ mem (r3 + 2w) @@ mem (r3 + 1w) @@ mem r3``),
401     (r15, ``^r15 + 4w``)]),
402   ("LDRH r2, [r3]",
403    [(r2, ``w2w (^mem (r3 + 1w) @@ mem r3) : word32``),
404     (r15, ``^r15 + 4w``)]),
405   ("STRH r2, [r3]",
406    [(``^mem (r3 + 1w)``, ``(15 >< 8) ^r2``),
407     (``^mem r3``, ``(7 >< 0) ^r2``),
408     (r15, ``^r15 + 4w``)]),
409   ("MSR CPSR, r1",
410    [(psrN, ``^r1 ' 31``),
411     (psrZ, ``^r1 ' 30``),
412     (psrC, ``^r1 ' 29``),
413     (psrV, ``^r1 ' 28``),
414     (psrQ, ``^r1 ' 27``),
415     (GE, ``(19 >< 16) ^r1``),
416     (psrE, ``^r1 ' 9``),
417     (r15, ``^r15 + 4w``)]),
418   ("MSR CPSR, #219",
419    [(psrN, ``F``), (psrZ, ``F``),
420     (psrC, ``F``), (psrV, ``F``),
421     (psrQ, ``F``), (GE, ``0w : word4``),
422     (r15, ``^r15 + 4w``)])
423  ];
424
425(*
426val go = step "v4,sys";
427*)
428val _ = test "validate_arm_step"
429        (fn l => List.map (validate_arm_step "v4,sys") l)
430  [("MSR CPSR, r1",
431    [(psrN, ``^r1 ' 31``),
432     (psrZ, ``^r1 ' 30``),
433     (psrC, ``^r1 ' 29``),
434     (psrV, ``^r1 ' 28``),
435     (psrQ, ``^r1 ' 27``),
436     (GE, ``(19 >< 16) ^r1``),
437     (psrE, ``^r1 ' 9``),
438     (psrA, ``^r1 ' 8``),
439     (psrI, ``^r1 ' 7``),
440     (psrF, ``if ~^sctlrNMFI \/ ~r1 ' 6 then ^r1 ' 6 else ^psrF``),
441     (mode, ``(4 >< 0) ^r1``),
442     (r15, ``^r15 + 4w``)]),
443   ("MSR CPSR, #219",
444    [(psrN, ``F``), (psrZ, ``F``),
445     (psrC, ``F``), (psrV, ``F``),
446     (psrQ, ``F``), (GE, ``0w : word4``),
447     (psrA, ``F``), (psrI, ``T``),
448     (psrF, ``~^sctlrNMFI \/ ^psrF``),
449     (mode, ``27w : word5``),
450     (r15, ``^r15 + 4w``)])
451  ];
452
453(*
454val go = step "fiq";
455*)
456val _ = test "validate_arm_step" (fn l => List.map (validate_arm_step "fiq") l)
457  [("ldm sp!,{r0,r1,pc}^",
458    [(psrN, spsrN),
459     (psrZ, spsrZ),
460     (psrC, spsrC),
461     (psrV, spsrV),
462     (psrQ, spsrQ),
463     (psrJ, spsrJ),
464     (GE, spsrGE),
465     (psrE, spsrE),
466     (psrA, spsrA),
467     (psrI, spsrI),
468     (psrF, ``if ~^sctlrNMFI \/ ~^spsrF then spsrF else ^psrF``),
469     (psrT, spsrT),
470     (mode, spsrmode),
471     (r15, ``align
472               (^mem (^r13 + 11w) @@ mem (r13 + 10w) @@ mem (r13 + 9w) @@
473                 mem (r13 + 8w),if ~^spsrJ /\ ~^spsrT then 4 else 2)``),
474     (r13, ``^r13 + 12w``),
475     (r1, ``^mem (^r13 + 7w) @@ mem (r13 + 6w) @@
476             mem (r13 + 5w) @@ mem (r13 + 4w)``),
477     (r0, ``^mem (^r13 + 3w) @@ mem (r13 + 2w) @@
478             mem (r13 + 1w) @@ mem r13``)])
479  ];
480
481val _ = test "arm_steps_from_quote v7 conds" (arm_steps_from_quote "v7")`
482        movseq  r1,r2
483        movsne  r1,r2
484        movscs  r1,r2
485        movscc  r1,r2
486        movsmi  r1,r2
487        movspl  r1,r2
488        movsvs  r1,r2
489        movsvc  r1,r2
490        movshi  r1,r2
491        movsls  r1,r2
492        movsge  r1,r2
493        movslt  r1,r2
494        movsgt  r1,r2
495        movsle  r1,r2
496        `;
497
498val _ = test "arm_steps_from_quote v4" (arm_steps_from_quote "v4,fiq")`
499        adds    pc,pc,#4
500        subs    pc,pc,#4
501        ldr     pc,[r2,#-5]
502// not supported
503//      ldr     pc,[pc,r1]
504        ldr     pc,[r1,-r2]!
505        ldr     r2,[pc,-r3]
506        ldr     r2,[r3],#-5
507        ldr     pc,[r3],#-5
508        ldr     pc,[r1],r2
509        `;
510
511val _ = test "arm_steps_from_quote v5" (arm_steps_from_quote "v5,fiq")`
512        adds    pc,pc,#4
513        subs    pc,pc,#4
514        eor     pc,r1,#2
515        eor     pc,r1,pc
516        ldr     pc,[r2,#-5]
517        ldr     pc,[pc,r1]
518        ldr     pc,[r1,-r2]!
519        ldr     r2,[pc,-r3]
520        ldr     r2,[r3],#-5
521        ldr     pc,[r3],#-5
522        ldr     pc,[r1],r2
523        `;
524
525val _ = test "arm_steps_from_quote v6" (arm_steps_from_quote "v6,fiq")`
526        adds    pc,pc,#3
527        subs    pc,pc,#3
528        ldr     pc,[r2,#-5]
529        ldr     pc,[pc,r1]
530        ldr     pc,[r1,-r2]!
531        ldr     r2,[pc,-r3]
532        ldr     r2,[r3],#-5
533        ldr     pc,[r3],#-5
534        ldr     pc,[r1],r2
535        `;
536
537val _ = test "arm_steps_from_quote v7" (arm_steps_from_quote "v7,fiq")`
538        adc     r1,pc,r2
539        adcs    r1,r10,r3,lsl r10
540        add     pc,sp,#4
541        adds    pc,pc,#3
542        add     pc,r1,#3
543        add     r1,r2,r3,ror r4
544        and     r1,r2
545        asr     r1,#4
546        asr     r1,r2,r3
547        movs    pc,lr
548        b       +#16
549        bfc     r10,#10,#0b1100
550        bfi     r10,r9,#0xA,#5
551        bic     r1,r2
552        bkpt    #10
553        bl      -#24
554        blx     sp
555        bx      sp
556        clz     r1,r8
557        cmn     r10,r8
558        cmp     r10,r8
559        cpsie   aif,#0b10000
560        dbg     #4
561        dmb     sy
562        dsb     sy
563        eor     pc,r8
564        isb     sy
565        ldmia   r1!,{r3-r5}
566        ldmia   sp,{r3,pc}
567        ldmdb   r1,{r1-r3}^
568        ldmda   r1,{r1,r5,pc}^
569        ldr     r1,[r2,#+3]
570        ldr     pc,[r2,#-5]
571        ldr     pc,[pc,r1]
572        ldr     pc,[r1,-r2]!
573        ldr     r2,[pc,-r3]
574        ldr     r2,[r3],#-5
575        ldr     pc,[r3],#-5
576        ldr     pc,[r1],r2
577        ldrb    r1,[r2,#+3]
578        ldrb    r2,[pc,-r3]
579        ldrb    r2,[r3],#-5
580        ldrh    r1,[r2,#+3]
581        ldrh    r2,[pc,-r3]
582        ldrh    r2,[r3],#-5
583        ldrsb   r1,[r2,#+3]
584        ldrsb   r2,[pc,-r3]
585        ldrsb   r2,[r3],#-5
586        ldrsh   r1,[r2,#+3]
587        ldrsh   r2,[pc,-r3]
588        ldrsh   r2,[r3],#-5
589        mlas    r8,r9,r10,r11
590        mls     r8,r9,r10,r11
591        movt    r8,#0xABCD
592        movw    r8,#0xEF01
593        mrs     r1,cpsr
594        mrs     r1,spsr
595        msr     cpsr,#16
596        msr     cpsr,r1
597        msr     spsr,#16
598        msr     spsr,r1
599        muls    r1,r3,r4
600        mvn     r3,r4,rrx
601        nop
602        orr     r3,r4,lsl r6
603        pkhbt   r1,r2,r3,lsl #4
604        pld     [r2]
605        pli     [r2,-r2]
606        pop     {r5,r9}
607        push    {r5,r9}
608        qadd    r1,r2,r3
609        qadd16  r1,r2,r3
610        qadd8   r1,r2,r3
611        qasx    r1,r2,r3
612        qdadd   r1,r2,r3
613        qdsub   r1,r2,r3
614        qsax    r1,r2,r3
615        qsub    r1,r2,r3
616        qsub16  r1,r2,r3
617        qsub8   r1,r2,r3
618        rbit    r8,r9
619        rev     r8,r9
620        rev16   r8,r9
621        revsh   r8,r9
622        rfeia   r2!
623        rsb     r3,r6,r8
624        rsc     pc,r6,r8
625        sadd16  r1,r2,r3
626        sadd8   r1,r2,r3
627        sasx    r1,r2,r3
628        sbc     pc,r6,r8
629        sbfx    r1,r2,#3,#4
630        sel     r1,r2,r3
631        setend  be
632        sev
633        shadd16 r5,r9,r2
634        shadd8  r5,r9,r2
635        shasx   r5,r9,r2
636        shsax   r5,r9,r2
637        shsub16 r5,r9,r2
638        shsub8  r5,r9,r2
639        smlabb  r0,r1,r2,r3
640        smlabt  r0,r1,r2,r3
641        smlatb  r0,r1,r2,r3
642        smlatt  r0,r1,r2,r3
643        smlad   r0,r1,r2,r3
644        smladx  r0,r1,r2,r3
645        smlal   r0,r1,r2,r3
646        smlalbb r0,r1,r2,r3
647        smlalbt r0,r1,r2,r3
648        smlaltb r0,r1,r2,r3
649        smlaltt r0,r1,r2,r3
650        smlawb  r0,r1,r2,r3
651        smlawt  r0,r1,r2,r3
652        smull   r0,r1,r2,r3
653        smulbb  r0,r1,r2
654        smulbt  r0,r1,r2
655        smultb  r0,r1,r2
656        smultt  r0,r1,r2
657        smulwb  r0,r1,r2
658        smulwt  r0,r1,r2
659        smlsd   r0,r1,r2,r3
660        smlsld  r0,r1,r2,r3
661        smmla   r1,r2,r3,r4
662        smmls   r1,r2,r3,r4
663        smmul   r1,r2,r3
664        smuad   r1,r2,r3
665        smusd   r1,r2,r3
666        srs     sp!,#31
667        ssat    r1,#2,r3
668        ssat16  r1,#2,r3
669        ssax    r1,r2,r3
670        ssub16  r1,r2,r3
671        ssub8   r1,r2,r3
672        stm     r1!,{r2-r4}
673        strb    r1,[r2,#4]
674        strh    r1,[r2,#4]
675        str     r1,[r2,#4]
676        strd    r0,r1,[r2,#4]
677        subs    r1,r2,#3
678        svc     #8
679        swp     r1,r2,[r3]
680        swpb    r1,r2,[r3]
681        sxtab   r1,r2,r3
682        sxtab16 r1,r2,r3
683        sxtah   r1,r2,r3
684        sxtb    r1,r2
685        sxtb16  r1,r2
686        sxth    r1,r2
687        teq     r1,r2
688        tst     r1,r2
689        uadd16  r1,r2,r3
690        uadd8   r1,r2,r3
691        uasx    r1,r2,r3
692        ubfx    r1,r2,#3,#4
693        uhadd16 r1,r2,r3
694        uhadd8  r1,r2,r3
695        uhasx   r1,r2,r3
696        uhsax   r1,r2,r3
697        uhsub16 r1,r2,r3
698        uhsub8  r1,r2,r3
699        umaal   r0,r1,r2,r3
700        umlal   r0,r1,r2,r3
701        umull   r0,r1,r2,r3
702        uqadd16 r1,r2,r3
703        uqadd8  r1,r2,r3
704        uqasx   r1,r2,r3
705        uqsax   r1,r2,r3
706        uqsub16 r1,r2,r3
707        uqsub8  r1,r2,r3
708        usad8   r1,r2,r3
709        usada8  r1,r2,r3,r4
710        usat    r1,#2,r3
711        usat16  r1,#2,r3
712        usax    r1,r2,r3
713        usub16  r1,r2,r3
714        usub8   r1,r2,r3
715        uxtab   r1,r2,r3
716        uxtab16 r1,r2,r3
717        uxtah   r1,r2,r3
718        uxtb    r1,r2
719        uxtb16  r1,r2
720        uxth    r1,r2
721        wfe
722        wfi
723        yield
724        `;
725
726val _ = test "arm_steps_from_quote ThumbEE" (arm_steps_from_quote "v7-R,thumb")`
727        ARCH    ARMv7-R
728        THUMBX
729
730        chka    r1,r2
731        hbl     #4
732        hblp    #4,#5
733        hbp     #4,#5
734        ldr     r1,[r2,#8]
735        str     r1,[r2],#8
736        pop     {r3,r4}
737        push    {r3,r4}
738        leavex
739
740        THUMB
741        sdiv    r1,r2,r3
742        tbb     [r1,r2]
743        tbh     [r1,r2,LSL #1]
744        udiv    r1,r2,r3
745        enterx
746        `;
747
748val elapsed = Timer.checkRealTimer tt;
749
750val _ = print ("\nTotal time: " ^ Lib.time_to_string elapsed ^ "\n");
751
752val _ = OS.Process.exit OS.Process.success;
753