arm/model/arm.sml

2456 fun PC () = R(BitsN.B(0xF,4));
2461 fun PCStoreValue () = PC ();
2856                then if (Align 32 (PC (),4)) = (BitsN.B(0x0,32))
2865                         (BitsN.@@(BitsN.bits(31,1) (PC ()),BitsN.B(0x1,1)))
3183         then BitsN.-(PC (),BitsN.B(0x2,32))
3184       else BitsN.-(PC (),BitsN.B(0x4,32))
3234           then BitsN.-(PC (),BitsN.B(0x2,32))
3235         else BitsN.-(PC (),BitsN.B(0x4,32))
3285           then PC ()
3286         else BitsN.-(PC (),BitsN.B(0x4,32))
3308           then PC ()
3309         else BitsN.-(PC (),BitsN.B(0x4,32))
3323       if #T((!CPSR) : PSR) then BitsN.+(PC (),BitsN.B(0x4,32)) else PC ()
3385       if #T((!CPSR) : PSR) then PC () else BitsN.-(PC (),BitsN.B(0x4,32))
3447       if #T((!CPSR) : PSR) then PC () else BitsN.-(PC (),BitsN.B(0x4,32))
3515       if #T((!CPSR) : PSR) then PC () else BitsN.-(PC (),BitsN.B(0x4,32))
3537       if #T((!CPSR) : PSR) then PC () else BitsN.-(PC (),BitsN.B(0x4,32))
3611       if #T((!CPSR) : PSR) then PC () else BitsN.-(PC (),BitsN.B(0x4,32))
3635         then BitsN.-(PC (),BitsN.B(0x4,32))
3636       else BitsN.-(PC (),BitsN.B(0x8,32))
3790 fun dfn'BranchTarget imm32 = BranchWritePC(BitsN.+(PC (),imm32));
3796       then write'LR(BitsN.-(PC (),BitsN.B(0x4,32)))
3797     else write'LR(BitsN.@@(BitsN.bits(31,1) (PC ()),BitsN.B(0x1,1)))
3801           then BitsN.+(Align 32 (PC (),4),imm32)
3802         else BitsN.+(PC (),imm32)
3814                val next_instr_addr = BitsN.-(PC (),BitsN.B(0x4,32))
3819              val next_instr_addr = BitsN.-(PC (),BitsN.B(0x2,32))
3830     then BranchWritePC(BitsN.+(PC (),imm32))
3843                 (PC (),
3852     then ( write'LR(BitsN.@@(BitsN.bits(31,1) (PC ()),BitsN.B(0x1,1)))
3861              val next_instr_addr = BitsN.-(PC (),BitsN.B(0x2,32))
3873       val next_instr_addr = BitsN.-(PC (),BitsN.B(0x2,32))
3922         then Align 32 (PC (),4)
3952         then Align 32 (PC (),4)
5013            val base = Align 32 (PC (),4)
5088            val base = Align 32 (PC (),4)
5164            val base = Align 32 (PC (),4)
5356                then BitsN.+(Align 32 (PC (),4),imm32)
5357              else BitsN.-(Align 32 (PC (),4),imm32)
6701     val base = if n = (BitsN.B(0xF,4)) then Align 32 (PC (),4) else R n
17270                                 (mc,"SUBS<c> PC, LR, #0")