ARM/v4/armScript.sml

67 val _ = Hol_datatype `mode = usr | fiq | irq | svc | abt | und | sys | safe`;
159   mode_num mode =
160     case mode of
171   SET_IFMODE irq' fiq' mode w:word32 =
174                         (i < 5) /\ (mode_num mode) ' i) w`;
196   mode2psr mode =
197     case mode of
206 val SPSR_READ_def = Define `SPSR_READ (psr:psrs) mode = psr (mode2psr mode)`;
213   SPSR_WRITE (psr:psrs) mode spsr =
214     if USER mode then psr else (mode2psr mode =+ spsr) psr`;
236     and mode' = exception2mode type
238     let reg' = REG_WRITE r.reg mode' 14w (FETCH_PC r.reg + 4w) in
240          psr := CPSR_WRITE (SPSR_WRITE r.psr mode' cpsr)
241                   (SET_IFMODE T fiq' mode' cpsr) |>`;
251   BRANCH r mode ireg =
257                   REG_WRITE pc_reg mode 14w (FETCH_PC r.reg + 4w)
310   SHIFT_IMMEDIATE reg mode C (opnd2:word12) =
312     let rm = REG_READ reg mode Rm
319   SHIFT_REGISTER reg mode C (opnd2:word12) =
323     and rm = REG_READ (INC_PC reg) mode Rm
324     and shift = (7 >< 0) (REG_READ reg mode Rs) in
328   ADDR_MODE1 reg mode C Im opnd2 =
332       SHIFT_REGISTER reg mode C opnd2
334       SHIFT_IMMEDIATE reg mode C opnd2`;
391   DATA_PROCESSING r C mode ireg =
393     let (C_s,op2) = ADDR_MODE1 r.reg mode C I opnd2
395     let rn = REG_READ (if ~I /\ (opnd2 ' 4) then pc_reg else r.reg) mode Rn in
398       <| reg := if tc then pc_reg else REG_WRITE pc_reg mode Rd res;
401                     (if (Rd = 15w) /\ ~tc then SPSR_READ r.psr mode
414   MRS r mode ireg =
416     let word = if R then SPSR_READ r.psr mode else CPSR_READ r.psr in
417       <| reg := REG_WRITE (INC_PC r.reg) mode Rd word; psr := r.psr |>`;
426   MSR r mode ireg =
428     if (USER mode /\ (R \/ (~bit19 /\ bit16))) \/ (~bit19 /\ ~bit16) then
431       let psrd = if R then SPSR_READ r.psr mode else CPSR_READ r.psr
432       and  src = if I then SND (IMMEDIATE F opnd) else REG_READ r.reg mode Rm in
436                     (i <= 7) /\ (if bit16 /\ ~USER mode then src ' i else b))
441                     SPSR_WRITE r.psr mode psrd'
471   MLA_MUL r mode ireg =
474     let rd = REG_READ r.reg mode Rd
475     and rn = REG_READ r.reg mode Rn
476     and rs = REG_READ r.reg mode Rs
477     and rm = REG_READ r.reg mode Rm in
484                     REG_WRITE (REG_WRITE pc_reg mode Rn resLo) mode Rd resHi
486                     REG_WRITE pc_reg mode Rd resLo;
499   ADDR_MODE2 reg mode C Im P U Rn offset =
500     let addr = REG_READ reg mode Rn in
502           (if Im then SND (SHIFT_IMMEDIATE reg mode C offset)
512   LDR_STR r C mode ireg input =
514     let (addr,wb_addr) = ADDR_MODE2 r.reg mode C I P U Rn offset in
521               let w = REG_READ pc_reg mode Rd in
525                           REG_WRITE pc_reg mode Rn wb_addr
533                     REG_WRITE wb_reg mode Rd
542   ADDR_MODE3 reg mode Im P U Rn offsetH offsetL =
543     let addr = REG_READ reg mode Rn in
546                  else REG_READ reg mode offsetL) in
555   LDRH_STRH r mode ireg input =
557     let (addr,wb_addr) = ADDR_MODE3 r.reg mode I P U Rn offsetH offsetL in
564               MemWrite addr (Half ((15 >< 0) (REG_READ pc_reg mode Rd)))]
567                           REG_WRITE pc_reg mode Rn wb_addr
581                      REG_WRITE wb_reg mode Rd
613   LDM_LIST reg mode rp_list data =
614     FOLDL (\reg' (rp,rd). REG_WRITE reg' mode rp rd) reg (ZIP (rp_list,data))`;
617   STM_LIST reg mode bl_list =
618     MAP (\(rp,addr). MemWrite addr (Word (REG_READ reg mode rp))) bl_list`;
625   LDM_STM r mode ireg input =
628     and rn = REG_READ r.reg mode Rn in
630     and mode' = if S /\ (L ==> ~pc_in_list) then usr else mode
633                    REG_WRITE pc_reg (if L then mode else mode') Rn rn'
642              STM_LIST (if HD rp_list = Rn then pc_reg else wb_reg) mode'
651                   let ldm_reg = LDM_LIST wb_reg mode' (FIRSTN t rp_list)
654                       REG_WRITE ldm_reg mode' Rn (REG_READ wb_reg mode' Rn)
657                           CPSR_WRITE r.psr (SPSR_READ r.psr mode)
669   SWP r mode ireg input =
671     let rn = REG_READ r.reg mode Rn
673     let rm = REG_READ pc_reg mode Rm in
683                   REG_WRITE pc_reg mode Rd
697   MRC r mode data ireg =
704         <| reg := REG_WRITE pc_reg mode Rd data; psr := r.psr |>`;
707   MCR_OUT reg mode ireg =
709       [CPWrite (REG_READ (INC_PC reg) mode Rd)]`;
721   ADDR_MODE5 reg mode P U Rn (offset:word8) =
722     let addr = REG_READ reg mode Rn in
727   LDC_STC r mode ireg input =
729     let (addr,wb_addr) = ADDR_MODE5 r.reg mode P U Rn offset in
733                        REG_WRITE pc_reg mode Rn wb_addr
811         else let mode = DECODE_MODE m
815             data_proc => DATA_PROCESSING r (CARRY nzcv) mode ireg
816           | mla_mul   => MLA_MUL r mode ireg
818           | br        => BRANCH r mode ireg
819           | msr       => MSR r mode ireg
820           | mrs       => MRS r mode ireg
821           | swp       => OUTR (SWP r mode ireg (SOME (IS_SOME dabt, data)))
822           | ldm_stm   => OUTR (LDM_STM r mode ireg (SOME (dabt, data)))
824                (LDR_STR r (CARRY nzcv) mode ireg (SOME (IS_SOME dabt, data)))
826                (LDRH_STRH r mode ireg (SOME (IS_SOME dabt, data)))
827           | ldc_stc   => coproc (\x. (OUTR (LDC_STC x mode ireg T)))
828           | mrc       => coproc (\x. MRC x mode (ELL 1 data) ireg)
895     let mode = DECODE_MODE m in
900                   ldr_str   => OUTL (LDR_STR r (CARRY nzcv) mode ireg NONE)
901                 | ldrh_strh => OUTL (LDRH_STRH r mode ireg NONE)
902                 | ldm_stm   => OUTL (LDM_STM r mode ireg NONE)
903                 | swp       => OUTL (SWP r mode ireg NONE)
904                 | ldc_stc   => OUTL (LDC_STC r mode ireg F)
905                 | mcr       => MCR_OUT r.reg mode ireg
908               user := USER mode
911            <| transfers := []; cpi := F; user := USER mode |>`;