instruction-set-models/arm/prog_armLib.sml

531   val thms = [arm_step "v6" s]
532   val thms = (thms @ [arm_step "v6,fail" s]) handle HOL_ERR _ => thms
533   val thms = map (RW [minus_one,minus_one_mult]) thms
534   val th = hd thms
555   val result = map derive_spec thms
599   val thms = arm_spec (enc "TST r5, #3");
600   val thms = arm_spec (enc "ADD r1, #10");
601   val thms = arm_spec (enc "CMP r1, #10");
602   val thms = arm_spec (enc "TST r2, #6");
603   val thms = arm_spec (enc "SUBCS r1, r1, #10");
604   val thms = arm_spec (enc "MOV r0, #0");
605   val thms = arm_spec (enc "CMP r1, #0");
606   val thms = arm_spec (enc "ADDNE r0, r0, #1");
607   val thms = arm_spec (enc "LDRNE r1, [r1]");
608   val thms = arm_spec (enc "BNE -#12");
609   val thms = arm_spec (enc "MOVGT r2, #5");
610   val thms = arm_spec (enc "LDRBNE r2, [r3]");
611   val thms = arm_spec (enc "BNE +#420");
612   val thms = arm_spec (enc "LDRLS r2, [r11, #-40]");
613   val thms = arm_spec (enc "SUBLS r2, r2, #1");
614   val thms = arm_spec (enc "SUBLS r11, r11, #4");
615   val thms = arm_spec (enc "MOVGT r12, r0");
616   val thms = arm_spec (enc "ADD r0, pc, #16");
617   val thms = arm_spec (enc "SUB r0, pc, #60");
618   val thms = arm_spec (enc "SUBLS r2, r2, #1");
619   val thms = arm_spec (enc "SUBLS r11, r11, #4");
620   val thms = arm_spec (enc "LDRGT r0, [r11, #-44]");
621   val thms = arm_spec (enc "MOVGT r1, r3");
622   val thms = arm_spec (enc "MOVGT r12, r5");
623   val thms = arm_spec (enc "MOVGT r1, r6");
624   val thms = arm_spec (enc "MOVGT r0, r6");
625   val thms = arm_spec (enc "ADD r5, pc, #4096");
626   val thms = arm_spec (enc "ADD r6, pc, #4096");
627   val thms = arm_spec (enc "STRB r2, [r3]");
628   val thms = arm_spec (enc "STMIA r4, {r5-r10}");
629   val thms = arm_spec (enc "LDMIA r4, {r5-r10}");
630   val thms = arm_spec (enc "STRB r2, [r1], #1");
631   val thms = arm_spec (enc "STRB r3, [r1], #1");
632   val thms = arm_spec (enc "STMIB r8!, {r14}");
633   val thms = arm_spec (enc "STMIB r8!, {r0, r14}");
634   val thms = arm_spec (enc "LDR pc, [r8]");
635   val thms = arm_spec (enc "LDRLS pc, [r8], #-4");
636   val thms = arm_spec (enc "LDMIA sp!, {r0-r2, r15}");
637   val thms = arm_spec (enc "LDR r0, [pc, #308]");
638   val thms = arm_spec (enc "LDR r0, [pc, #4056]");
639   val thms = arm_spec (enc "LDR r8, [pc, #3988]");
640   val thms = arm_spec (enc "LDR r2, [pc, #3984]");
641   val thms = arm_spec (enc "LDR r12, [pc, #3880]");
642   val thms = arm_spec (enc "LDR r12, [pc, #3856]");
643   val thms = arm_spec (enc "LDR r1, [pc, #1020]");
644   val thms = arm_spec (enc "LDR r1, [pc, #-20]");
645   val thms = arm_spec (enc "STMDB sp!, {r0-r2, r15}");
646   val thms = arm_spec (enc "LDRB r2, [r3]");
647   val thms = arm_spec (enc "STRB r2, [r3]");
648   val thms = arm_spec (enc "SWPB r2, r4, [r3]");
649   val thms = arm_spec (enc "LDR r2, [r3,#12]");
650   val thms = arm_spec (enc "STR r2, [r3,#12]");
651   val thms = arm_spec (enc "SWP r2, r4, [r3]");
652   val thms = arm_spec (enc "LDMIB r4, {r5-r7}");
653   val thms = arm_spec (enc "STMIA r4, {r5-r6}");
654   val thms = arm_spec (enc "LDRH r2, [r3]");
655   val thms = arm_spec (enc "STRH r2, [r3]");
656   val thms = arm_spec (enc "MSR CPSR, r1");
657   val thms = arm_spec (enc "MSR CPSR, #219");
658   val thms = arm_spec (enc "MRS r1, CPSR");
659   val thms = arm_spec (enc "LDR r0, [r11, #-8]");
660   val thms = arm_spec (enc "LDR r0, [r11]");
661   val thms = arm_spec (enc "STR r0, [r11, #-8]");
662   val thms = arm_spec (enc "BX lr");
665   val thms = arm_spec_mem (enc "SWP r0, r1, [r11]");
666   val thms = arm_spec_mem (enc "LDR r0, [r11]");
667   val thms = arm_spec_mem (enc "LDRB r0, [r11]");
668   val thms = arm_spec_mem (enc "STRB r0, [r11]");
669   val thms = arm_spec_mem (enc "STR r0, [r11]");
670   val thms = arm_spec_mem (enc "STR r0, [r11,#8]");
671   val thms = arm_spec_mem (enc "LDR r0, [r11,#8]");
672   val thms = arm_spec_mem (enc "STR r0, [r11,#-8]");
673   val thms = arm_spec_mem (enc "LDR r0, [r11,#-8]");
674   val thms = arm_spec_mem (enc "LDMDB r0, {r2-r4}");
675   val thms = arm_spec_mem (enc "STMDB r0, {r2-r4}");
676   val thms = arm_spec_mem (enc "LDR r0, [sp,#8]");
677   val thms = arm_spec_mem (enc "PUSH {r0-r2}");
678   val thms = arm_spec_mem (enc "POP {r0-r2}");
679   val thms = arm_spec_mem (enc "POP {r0-r2,pc}");
680   val thms = arm_spec_mem (enc "POP {r4,pc}");
681   val thms = arm_spec_mem (enc "BLNE -#40");
682   val thms = arm_spec_mem (enc "LDRLS pc,[pc,r3,lsl #2]");
683   val thms = arm_spec_mem "15832014"
685   val thms = arm_spec_m (enc "POP {r4,pc}");
686   val thms = arm_spec_m (enc "STM r0, {r2-r3}");