ARM/arm6-verification/armScript.sml

57 val _ = Hol_datatype `mode = usr | fiq | irq | svc | abt | und | safe`;
74 val USER_def = Define `USER mode = (mode = usr) \/ (mode = safe)`;
117   mode_num mode =
118     case mode of
128   SET_IFMODE irq' fiq' mode w:word32 =
131                         (i < 5) /\ (mode_num mode) %% i) w`;
151   mode2psr mode =
152     case mode of
161 val SPSR_READ_def = Define `SPSR_READ (psr:psr) mode = psr (mode2psr mode)`;
168   SPSR_WRITE (psr:psr) mode spsr =
169     if USER mode then psr else (mode2psr mode =+ spsr) psr`;
191     and mode' = exception2mode type
193     let reg' = REG_WRITE reg mode' 14w (FETCH_PC reg + 4w) in
195          (CPSR_WRITE (SPSR_WRITE psr mode' cpsr)
196             (SET_IFMODE T fiq' mode' cpsr))`;
206   BRANCH (ARM reg psr) mode ireg =
212              REG_WRITE pc_reg mode 14w (FETCH_PC reg + 4w)
268   SHIFT_IMMEDIATE reg mode C (opnd2:word12) =
270     let rm = REG_READ reg mode Rm
277   SHIFT_REGISTER reg mode C (opnd2:word12) =
281     and rm = REG_READ (INC_PC reg) mode Rm
282     and shift = (7 >< 0) (REG_READ reg mode Rs) in
286   ADDR_MODE1 reg mode C Im opnd2 =
290       SHIFT_REGISTER reg mode C opnd2
292       SHIFT_IMMEDIATE reg mode C opnd2`;
345   DATA_PROCESSING (ARM reg psr) C mode ireg =
347     let (C_s,op2) = ADDR_MODE1 reg mode C I opnd2
349     let rn = REG_READ (if ~I /\ (opnd2 %% 4) then pc_reg else reg) mode Rn in
352       ARM (if tc then pc_reg else REG_WRITE pc_reg mode Rd res)
355              (if (Rd = 15w) /\ ~tc then SPSR_READ psr mode
368   MRS (ARM reg psr) mode ireg =
370     let word = if R then SPSR_READ psr mode else CPSR_READ psr in
371       ARM (REG_WRITE (INC_PC reg) mode Rd word) psr`;
380   MSR (ARM reg psr) mode ireg =
382     if (USER mode /\ (R \/ (~bit19 /\ bit16))) \/ (~bit19 /\ ~bit16) then
385       let psrd = if R then SPSR_READ psr mode else CPSR_READ psr
386       and  src = if I then SND (IMMEDIATE F opnd) else REG_READ reg mode Rm in
390                     (i <= 7) /\ (if bit16 /\ ~USER mode then src %% i else b))
394          (if R then SPSR_WRITE psr mode psrd' else CPSR_WRITE psr psrd')`;
433   MLA_MUL (ARM reg psr) C mode ireg =
436     let rn = REG_READ reg mode Rn
437     and rs = REG_READ reg mode Rs
438     and rm = REG_READ pc_reg mode Rm in
443         ARM (REG_WRITE pc_reg mode Rd res)
459   ADDR_MODE2 reg mode C Im P U Rn offset =
460     let addr  = REG_READ reg mode Rn in
462           (if Im then SND (SHIFT_IMMEDIATE reg mode C offset)
472   LDR_STR (ARM reg psr) C mode isdabort data ireg =
474     let (addr,wb_addr) = ADDR_MODE2 reg mode C I P U Rn offset in
477                    REG_WRITE pc_reg mode Rn wb_addr
485                   REG_WRITE wb_reg mode Rd (BW_READ B ((1 >< 0) addr) data))
491               MemWrite B addr (REG_READ pc_reg mode Rd)] |>`;
521   LDM_LIST reg mode rp_list data =
522     FOLDL (\reg' (rp,rd). REG_WRITE reg' mode rp rd) reg (ZIP (rp_list,data))`;
525   STM_LIST reg mode bl_list =
526     MAP (\(rp,addr). MemWrite F addr (REG_READ reg mode rp)) bl_list`;
533   LDM_STM (ARM reg psr) mode dabort_t data ireg =
536     and rn = REG_READ reg mode Rn in
538     and mode' = if S /\ (L ==> ~pc_in_list) then usr else mode
541                    REG_WRITE pc_reg (if L then mode else mode') Rn rn'
551                   let ldm_reg = LDM_LIST wb_reg mode' (FIRSTN t rp_list)
554                       REG_WRITE ldm_reg mode' Rn (REG_READ wb_reg mode' Rn)
557                     CPSR_WRITE psr (SPSR_READ psr mode)
564              STM_LIST (if HD rp_list = Rn then pc_reg else wb_reg) mode'
575   SWP (ARM reg psr) mode isdabort data ireg =
577     let rn = REG_READ reg mode Rn
579     let rm = REG_READ pc_reg mode Rm in
584                   REG_WRITE pc_reg mode Rd (BW_READ B ((1 ><  0) rn) data))
593   MRC (ARM reg psr) mode data ireg =
599         ARM (REG_WRITE pc_reg mode Rd data) psr`;
602   MCR_OUT (ARM reg psr) mode ireg =
604       [CPWrite (REG_READ (INC_PC reg) mode Rn)]`;
615   ADDR_MODE5 reg mode P U Rn (offset:word8) =
616     let addr = REG_READ reg mode Rn in
621   LDC_STC (ARM reg psr) mode ireg =
623     let (addr,wb_addr) = ADDR_MODE5 reg mode P U Rn offset in
626                    REG_WRITE pc_reg mode Rn wb_addr
708         else let mode = DECODE_MODE m in
710           DATA_PROCESSING (ARM reg psr) (CARRY nzcv) mode ireg
712           MLA_MUL (ARM reg psr) (CARRY nzcv) mode ireg
714           BRANCH (ARM reg psr) mode ireg
716           (LDR_STR (ARM reg psr) (CARRY nzcv) mode
719           (LDM_STM (ARM reg psr) mode dabort_t data ireg).state
721           (SWP (ARM reg psr) mode (IS_SOME dabort_t) (HD data) ireg).state
726             MSR (ARM reg psr) mode ireg
728             MRS (ARM reg psr) mode ireg
733           MRC (ARM reg psr) mode (ELL 1 data) ireg
735           (LDC_STC (ARM reg psr) mode ireg).state
806          let mode = DECODE_MODE m in
808            (LDR_STR (ARM reg psr) (CARRY nzcv) mode ARB ARB ireg).out
810            (LDM_STM (ARM reg psr) mode ARB ARB ireg).out
812            (SWP (ARM reg psr) mode ARB ARB ireg).out
814            (LDC_STC (ARM reg psr) mode ireg).out
816            MCR_OUT (ARM reg psr) mode ireg