ARM/v7/selftest.sml

118 val r15 = reg 15
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,
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
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)
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)``)])];
203      (r15, ``^r15 + 4w``),
216      (r15, ``^r15 + 4w``)]),
220      (r15, ``^r15 + 4w``)]),
223      (r15, ``^r15 + 4w``)]),
229      (r15, ``^r15 + 4w``)]),
233      (r15, ``^r15 + 4w``)]),
236      (r15, ``^r15 + 4w``)]),
239      (r15, ``^r15 + 4w``)]),
245      (r15, ``^r15 + 4w``)]),
248      (r15, ``^r15 + 4w``)]),
251      (r15, ``^r15 + 4w``)]),
253     [(r15, ``^r15 + 0xFFFFFFF4w``)]),
256      (r15, ``^r15 + 4w``)]),
259      (r15, ``^r15 + 4w``)]),
261     [(r15, ``^r15 + 420w``)]),
266     (r15, ``^r15 + 4w``)]),
269      (r15, ``^r15 + 4w``)]),
272      (r15, ``^r15 + 4w``)]),
275      (r15, ``^r15 + 4w``)]),
277     [(r0, ``^r15 + 24w``),
278      (r15, ``^r15 + 4w``)]),
280     [(r0, ``^r15 + 0xFFFFFFCCw``),
281      (r15, ``^r15 + 4w``)]),
283     [(r5, ``^r15 + 4104w``),
284      (r15, ``^r15 + 4w``)]),
287      (r15, ``^r15 + 4w``)]),
313      (r15, ``^r15 + 4w``)]),
315     [(r15, ``^r15 + 4w``),
334      (r15, ``^r15 + 4w``),
342      (r15, ``^r15 + 4w``)]),
344     [(r15, ``^mem (r8 + 3w) @@ mem (r8 + 2w) @@ mem (r8 + 1w) @@ mem r8``)]),
346     [(r15, ``^mem (r8 + 3w) @@ mem (r8 + 2w) @@ mem (r8 + 1w) @@ mem r8``),
348    ("LDMIA sp!, {r0-r2, r15}",
350      (r15,
364      ``^mem (r15 + 319w) @@ mem (r15 + 318w) @@
365         mem (r15 + 317w) @@ mem (r15 + 316w)``),
366     (r15, ``^r15 + 4w``)]),
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)``),
390      (r15, ``^r15 + 4w``)]),
394      (r15, ``^r15 + 4w``)]),
401      (r15, ``^r15 + 4w``)]),
404      (r15, ``^r15 + 4w``)]),
408      (r15, ``^r15 + 4w``)]),
417      (r15, ``^r15 + 4w``)]),
422      (r15, ``^r15 + 4w``)])
442      (r15, ``^r15 + 4w``)]),
450      (r15, ``^r15 + 4w``)])
471      (r15, ``align