arm8/model/arm8.sml

1258 fun DecodeShift sh = (Cast.natToShiftType o BitsN.toNat) sh;
1280 fun ExtendValue N (value,(ty,sh)) =
1293     val len = Nat.min(len,Nat.-(BitsN.size(BitsN.BV(0x0,N)),sh))
1296       (Bitstring.<<(Bitstring.bits(Nat.-(len,1),0) value,sh),unsigned)
1299 fun ExtendReg N (reg,(ty,sh)) = ExtendValue N (X N reg,(ty,sh));
5982      AddSubShiftedRegister''32(_,(opc,(s,(sh,(rm,(imm6,(rn,rd))))))) =>
5988                    BitsN.B(0xB,5),BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
5990    | AddSubShiftedRegister''64(_,(opc,(s,(sh,(rm,(imm6,(rn,rd))))))) =>
5994            BitsN.B(0xB,5),BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
6043      (sf,(opc,(invert,(s,(sh,(imm,(rm,(rn,rd)))))))) =>
6053                           BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
6059      (sf,(opc,(invert,(s,(sh,(imm,(rm,(rn,rd)))))))) =>
6069                           BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
6088    | Shift''32(_,(sh,(rm,(rn,rd)))) =>
6092            BitsN.fromNat(Cast.ShiftTypeToNat sh,2),rn,rd])
6093    | Shift''64(_,(sh,(rm,(rn,rd)))) =>
6097            BitsN.fromNat(Cast.ShiftTypeToNat sh,2),rn,rd])
7058 fun p_shift_amount (sh,s) =
7060      Option.SOME v => Option.SOME(sh,v)
7639            Option.SOME(sh,amount) =>
7650                                      (setflags,(sh,(xm,(imm6,(xn,xd)))))))))
7656                                    (setflags,(sh,(wm,(imm6,(wn,wd)))))))))
7658                          if sh = ShiftType_LSL
7685            (Option.SOME(true,(xd,(xn,xm))),Option.SOME(sh,amount)) =>
7689                       (opc,(invert,(setflags,(sh,(amount,(xm,(xn,xd))))))))))
7690          | (Option.SOME(false,(wd,(wn,wm))),Option.SOME(sh,amount)) =>
7694                     (opc,(invert,(setflags,(sh,(amount,(wm,(wn,wd))))))))))
7735             (Option.SOME(true,imm16),Option.SOME(sh,amount))) =>
8680 fun s_shift_amount (shift_type,sh) =
8681   if (sh = 0) andalso (shift_type = ShiftType_LSL)
8683   else String.concat[", ",s_shift_type shift_type," ",s_nat sh];
8895        val sh = Nat.*(BitsN.toNat hw,16)
8903                     (BitsN.<<(BitsN.fromNat(BitsN.toNat imm,64),sh))))
8914                                  (BitsN.fromNat(BitsN.toNat imm,64),sh)))
8918                                (BitsN.fromNat(BitsN.toNat imm,32),sh)))))
8924                 else ", lsl " ^ (s_nat sh)])
8929        val sh = Nat.*(BitsN.toNat hw,16)
8937                     (BitsN.<<(BitsN.fromNat(BitsN.toNat imm,64),sh))))
8948                                  (BitsN.fromNat(BitsN.toNat imm,64),sh)))
8952                                (BitsN.fromNat(BitsN.toNat imm,32),sh)))))
8958                 else ", lsl " ^ (s_nat sh)])