;; GENERATED BY `isaspec`. DO NOT EDIT!!!
(attr MInst.Store8 (tag isaspec_generated))
(spec
(MInst.Store8 rd mem flags)
(provide
(match
mem
((RegReg rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn rm))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
((RegScaled rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn rm))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
((RegScaledExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 31 0 rm))))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 31 0 rm))))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (sign_ext 64 rm)))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
)
)
((RegExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 31 0 rm))))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 31 0 rm))))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (sign_ext 64 rm)))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
)
)
((Unscaled rn simm9)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 8 0 simm9))))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
((UnsignedOffset rn uimm12)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 8)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 11 0 uimm12))))
(= (conv_to 8 (:value isa_store)) (extract 7 0 (as rd (bv 64))))
)
)
)
)
(require
(match
mem
((RegReg rn rm) true)
((RegScaled rn rm) true)
((RegScaledExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((RegExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((Unscaled rn simm9) true)
((UnsignedOffset rn uimm12) true)
)
)
(modifies isa_store)
)
(attr MInst.Store16 (tag isaspec_generated))
(spec
(MInst.Store16 rd mem flags)
(provide
(match
mem
((RegReg rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn rm))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
((RegScaled rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (concat (extract 62 0 rm) #b0)))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
((RegScaledExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (concat (extract 31 0 rm) #b0))))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 31 0 rm) #b0))))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 62 0 rm) #b0))))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
)
)
((RegExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 31 0 rm))))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 31 0 rm))))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (sign_ext 64 rm)))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
)
)
((Unscaled rn simm9)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 8 0 simm9))))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
((UnsignedOffset rn uimm12)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 16)
(= (:addr isa_store) (bvadd rn (concat (zero_ext 63 (extract 11 0 uimm12)) #b0)))
(= (conv_to 16 (:value isa_store)) (extract 15 0 (as rd (bv 64))))
)
)
)
)
(require
(match
mem
((RegReg rn rm) true)
((RegScaled rn rm) true)
((RegScaledExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((RegExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((Unscaled rn simm9) true)
((UnsignedOffset rn uimm12) true)
)
)
(modifies isa_store)
)
(attr MInst.Store32 (tag isaspec_generated))
(spec
(MInst.Store32 rd mem flags)
(provide
(match
mem
((RegReg rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn rm))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
((RegScaled rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (concat (extract 61 0 rm) #b00)))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
((RegScaledExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (concat (extract 31 0 rm) #b00))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 31 0 rm) #b00))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 61 0 rm) #b00))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
)
)
((RegExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 31 0 rm))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 31 0 rm))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 rm)))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
)
)
((Unscaled rn simm9)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 8 0 simm9))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
((UnsignedOffset rn uimm12)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (concat (zero_ext 62 (extract 11 0 uimm12)) #b00)))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (as rd (bv 64))))
)
)
)
)
(require
(match
mem
((RegReg rn rm) true)
((RegScaled rn rm) true)
((RegScaledExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((RegExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((Unscaled rn simm9) true)
((UnsignedOffset rn uimm12) true)
)
)
(modifies isa_store)
)
(attr MInst.Store64 (tag isaspec_generated))
(spec
(MInst.Store64 rd mem flags)
(provide
(match
mem
((RegReg rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn rm))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
((RegScaled rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (concat (extract 60 0 rm) #b000)))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
((RegScaledExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (concat (extract 31 0 rm) #b000))))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 31 0 rm) #b000))))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 60 0 rm) #b000))))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
)
)
((RegExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 31 0 rm))))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 31 0 rm))))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 rm)))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
)
)
((Unscaled rn simm9)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 8 0 simm9))))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
((UnsignedOffset rn uimm12)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (concat (zero_ext 61 (extract 11 0 uimm12)) #b000)))
(= (conv_to 64 (:value isa_store)) (as rd (bv 64)))
)
)
)
)
(require
(match
mem
((RegReg rn rm) true)
((RegScaled rn rm) true)
((RegScaledExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((RegExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((Unscaled rn simm9) true)
((UnsignedOffset rn uimm12) true)
)
)
(modifies isa_store)
)
(attr MInst.FpuStore32 (tag isaspec_generated))
(spec
(MInst.FpuStore32 rd mem flags)
(provide
(match
mem
((RegReg rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn rm))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
((RegScaled rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (concat (extract 61 0 rm) #b00)))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
((RegScaledExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (concat (extract 31 0 rm) #b00))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 31 0 rm) #b00))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 61 0 rm) #b00))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
)
)
((RegExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 31 0 rm))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 31 0 rm))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 rm)))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
)
)
((Unscaled rn simm9)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 8 0 simm9))))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
((UnsignedOffset rn uimm12)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 32)
(= (:addr isa_store) (bvadd rn (concat (zero_ext 62 (extract 11 0 uimm12)) #b00)))
(= (conv_to 32 (:value isa_store)) (extract 31 0 (conv_to 128 (as rd (bv 64)))))
)
)
)
)
(require
(match
mem
((RegReg rn rm) true)
((RegScaled rn rm) true)
((RegScaledExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((RegExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((Unscaled rn simm9) true)
((UnsignedOffset rn uimm12) true)
)
)
(modifies isa_store)
)
(attr MInst.FpuStore64 (tag isaspec_generated))
(spec
(MInst.FpuStore64 rd mem flags)
(provide
(match
mem
((RegReg rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn rm))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
((RegScaled rn rm)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (concat (extract 60 0 rm) #b000)))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
((RegScaledExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (concat (extract 31 0 rm) #b000))))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 31 0 rm) #b000))))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (concat (extract 60 0 rm) #b000))))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
)
)
((RegExtended rn rm extendop)
(match
extendop
((UXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (zero_ext 64 (extract 31 0 rm))))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTW)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 31 0 rm))))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
((SXTX)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 rm)))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
)
)
((Unscaled rn simm9)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (sign_ext 64 (extract 8 0 simm9))))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
((UnsignedOffset rn uimm12)
(and
(= (:active isa_store) true)
(= (:size_bits isa_store) 64)
(= (:addr isa_store) (bvadd rn (concat (zero_ext 61 (extract 11 0 uimm12)) #b000)))
(= (conv_to 64 (:value isa_store)) (extract 63 0 (conv_to 128 (as rd (bv 64)))))
)
)
)
)
(require
(match
mem
((RegReg rn rm) true)
((RegScaled rn rm) true)
((RegScaledExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((RegExtended rn rm extendop) (match extendop ((UXTW) true) ((SXTW) true) ((SXTX) true)))
((Unscaled rn simm9) true)
((UnsignedOffset rn uimm12) true)
)
)
(modifies isa_store)
)