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