diff options
Diffstat (limited to 'power/gen/trans_sail.gen')
| -rw-r--r-- | power/gen/trans_sail.gen | 1516 |
1 files changed, 0 insertions, 1516 deletions
diff --git a/power/gen/trans_sail.gen b/power/gen/trans_sail.gen deleted file mode 100644 index b6f406f2..00000000 --- a/power/gen/trans_sail.gen +++ /dev/null @@ -1,1516 +0,0 @@ - | `Pb(setaa0, setlk1, k2) -> - ("B", - [("LI", IInt.Bvector (Some 24), SB.bit_list_of_integer 24 (Nat_big_num.of_int (trans_li_setaa_setlk_k setaa0 setlk1 k2))); - ("AA", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_aa setaa0))); - ("LK", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_lk setlk1)))], - [(* always empty base effects*)] - ) - | `Pbc(setaa0, setlk1, k2, k3, k4) -> - ("Bc", - [("BO", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2)); - ("BI", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k3)); - ("BD", IInt.Bvector (Some 14), SB.bit_list_of_integer 14 (Nat_big_num.of_int (trans_bd_setaa_setlk_k_k_k setaa0 setlk1 k2 k3 k4))); - ("AA", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_aa setaa0))); - ("LK", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_lk setlk1)))], - [(* always empty base effects*)] - ) - | `Pbclr(setlk0, k1, k2, k3) -> - ("Bclr", - [("BO", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BI", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2)); - ("BH", IInt.Bvector (Some 2), SB.bit_list_of_integer 2 (Nat_big_num.of_int k3)); - ("LK", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_lk setlk0)))], - [(* always empty base effects*)] - ) - | `Pbcctr(setlk0, k1, k2, k3) -> - ("Bcctr", - [("BO", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BI", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2)); - ("BH", IInt.Bvector (Some 2), SB.bit_list_of_integer 2 (Nat_big_num.of_int k3)); - ("LK", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_lk setlk0)))], - [(* always empty base effects*)] - ) - | `Pcrand(k0, k1, k2) -> - ("Crand", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pcrnand(k0, k1, k2) -> - ("Crnand", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pcror(k0, k1, k2) -> - ("Cror", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pcrxor(k0, k1, k2) -> - ("Crxor", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pcrnor(k0, k1, k2) -> - ("Crnor", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pcreqv(k0, k1, k2) -> - ("Creqv", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pcrandc(k0, k1, k2) -> - ("Crandc", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pcrorc(k0, k1, k2) -> - ("Crorc", - [("BT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("BA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("BB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pmcrf(crindex0, k1) -> - ("Mcrf", - [("BF", IInt.Bvector (Some 3), SB.bit_list_of_integer 3 (Nat_big_num.of_int crindex0)); - ("BFA", IInt.Bvector (Some 3), SB.bit_list_of_integer 3 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Psc(k0) -> - ("Sc", - [("LEV", IInt.Bvector (Some 7), SB.bit_list_of_integer 7 (Nat_big_num.of_int k0))], - [(* always empty base effects*)] - ) - | `Pscv(k0) -> - ("Scv", - [("LEV", IInt.Bvector (Some 7), SB.bit_list_of_integer 7 (Nat_big_num.of_int k0))], - [(* always empty base effects*)] - ) - | `Plbz(reg0, k1, reg2) -> - ("Lbz", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plbzx(reg0, reg1, reg2) -> - ("Lbzx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plbzu(reg0, k1, reg2) -> - ("Lbzu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plbzux(reg0, reg1, reg2) -> - ("Lbzux", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plhz(reg0, k1, reg2) -> - ("Lhz", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plhzx(reg0, reg1, reg2) -> - ("Lhzx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plhzu(reg0, k1, reg2) -> - ("Lhzu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plhzux(reg0, reg1, reg2) -> - ("Lhzux", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plha(reg0, k1, reg2) -> - ("Lha", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plhax(reg0, reg1, reg2) -> - ("Lhax", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plhau(reg0, k1, reg2) -> - ("Lhau", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plhaux(reg0, reg1, reg2) -> - ("Lhaux", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plwz(reg0, k1, reg2) -> - ("Lwz", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plwzx(reg0, reg1, reg2) -> - ("Lwzx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plwzu(reg0, k1, reg2) -> - ("Lwzu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plwzux(reg0, reg1, reg2) -> - ("Lwzux", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plwa(reg0, ds1, reg2) -> - ("Lwa", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("DS", IInt.Bvector (Some 14), SB.bit_list_of_integer 14 (Nat_big_num.of_int ds1))], - [(* always empty base effects*)] - ) - | `Plwax(reg0, reg1, reg2) -> - ("Lwax", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plwaux(reg0, reg1, reg2) -> - ("Lwaux", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pld(reg0, ds1, reg2) -> - ("Ld", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("DS", IInt.Bvector (Some 14), SB.bit_list_of_integer 14 (Nat_big_num.of_int ds1))], - [(* always empty base effects*)] - ) - | `Pldx(reg0, reg1, reg2) -> - ("Ldx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pldu(reg0, ds1, reg2) -> - ("Ldu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("DS", IInt.Bvector (Some 14), SB.bit_list_of_integer 14 (Nat_big_num.of_int ds1))], - [(* always empty base effects*)] - ) - | `Pldux(reg0, reg1, reg2) -> - ("Ldux", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstb(reg0, k1, reg2) -> - ("Stb", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Pstbx(reg0, reg1, reg2) -> - ("Stbx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstbu(reg0, k1, reg2) -> - ("Stbu", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Pstbux(reg0, reg1, reg2) -> - ("Stbux", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Psth(reg0, k1, reg2) -> - ("Sth", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Psthx(reg0, reg1, reg2) -> - ("Sthx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Psthu(reg0, k1, reg2) -> - ("Sthu", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Psthux(reg0, reg1, reg2) -> - ("Sthux", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstw(reg0, k1, reg2) -> - ("Stw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Pstwx(reg0, reg1, reg2) -> - ("Stwx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstwu(reg0, k1, reg2) -> - ("Stwu", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Pstwux(reg0, reg1, reg2) -> - ("Stwux", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstd(reg0, ds1, reg2) -> - ("Std", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("DS", IInt.Bvector (Some 14), SB.bit_list_of_integer 14 (Nat_big_num.of_int ds1))], - [(* always empty base effects*)] - ) - | `Pstdx(reg0, reg1, reg2) -> - ("Stdx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstdu(reg0, ds1, reg2) -> - ("Stdu", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("DS", IInt.Bvector (Some 14), SB.bit_list_of_integer 14 (Nat_big_num.of_int ds1))], - [(* always empty base effects*)] - ) - | `Pstdux(reg0, reg1, reg2) -> - ("Stdux", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plq(k0, k1, reg2, k3) -> - ("Lq", - [("RTp", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("DQ", IInt.Bvector (Some 12), SB.bit_list_of_integer 12 (Nat_big_num.of_int k1)); - ("PT", IInt.Bvector (Some 4), SB.bit_list_of_integer 4 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Pstq(k0, ds1, reg2) -> - ("Stq", - [("RSp", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("DS", IInt.Bvector (Some 14), SB.bit_list_of_integer 14 (Nat_big_num.of_int ds1))], - [(* always empty base effects*)] - ) - | `Plhbrx(reg0, reg1, reg2) -> - ("Lhbrx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Psthbrx(reg0, reg1, reg2) -> - ("Sthbrx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plwbrx(reg0, reg1, reg2) -> - ("Lwbrx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstwbrx(reg0, reg1, reg2) -> - ("Stwbrx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pldbrx(reg0, reg1, reg2) -> - ("Ldbrx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstdbrx(reg0, reg1, reg2) -> - ("Stdbrx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Plmw(reg0, k1, reg2) -> - ("Lmw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Pstmw(reg0, k1, reg2) -> - ("Stmw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("D", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Plswi(k0, reg1, k2) -> - ("Lswi", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("NB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Plswx(reg0, reg1, reg2) -> - ("Lswx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstswi(k0, reg1, k2) -> - ("Stswi", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("NB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pstswx(k0, reg1, reg2) -> - ("Stswx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k0)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Paddi(reg0, reg1, k2) -> - ("Addi", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Paddis(reg0, reg1, k2) -> - ("Addis", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Padd(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Add", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Psubf(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Subf", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Paddic(reg0, reg1, k2) -> - ("Addic", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Paddicdot(reg0, reg1, k2) -> - ("AddicDot", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Psubfic(reg0, reg1, k2) -> - ("Subfic", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Paddc(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Addc", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Psubfc(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Subfc", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Padde(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Adde", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Psubfe(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Subfe", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Paddme(setsoov0, setcr01, reg2, reg3) -> - ("Addme", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Psubfme(setsoov0, setcr01, reg2, reg3) -> - ("Subfme", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Paddze(setsoov0, setcr01, reg2, reg3) -> - ("Addze", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Psubfze(setsoov0, setcr01, reg2, reg3) -> - ("Subfze", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pneg(setsoov0, setcr01, reg2, reg3) -> - ("Neg", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmulli(reg0, reg1, k2) -> - ("Mulli", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pmullw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Mullw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmulhw(setcr00, reg1, reg2, reg3) -> - ("Mulhw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmulhwu(setcr00, reg1, reg2, reg3) -> - ("Mulhwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pdivw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pdivwu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pdivwe(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divwe", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pdivweu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divweu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmulld(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Mulld", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmulhd(setcr00, reg1, reg2, reg3) -> - ("Mulhd", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmulhdu(setcr00, reg1, reg2, reg3) -> - ("Mulhdu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pdivd(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divd", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pdivdu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divdu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pdivde(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divde", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pdivdeu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Divdeu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pcmpi(crindex0, k1, reg2, k3) -> - ("Cmpi", - [("BF", IInt.Bvector (Some 3), SB.bit_list_of_integer 3 (Nat_big_num.of_int crindex0)); - ("L", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k1)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("SI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Pcmp(crindex0, k1, reg2, reg3) -> - ("Cmp", - [("BF", IInt.Bvector (Some 3), SB.bit_list_of_integer 3 (Nat_big_num.of_int crindex0)); - ("L", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k1)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3)))], - [(* always empty base effects*)] - ) - | `Pcmpli(crindex0, k1, reg2, k3) -> - ("Cmpli", - [("BF", IInt.Bvector (Some 3), SB.bit_list_of_integer 3 (Nat_big_num.of_int crindex0)); - ("L", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k1)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("UI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Pcmpl(crindex0, k1, reg2, reg3) -> - ("Cmpl", - [("BF", IInt.Bvector (Some 3), SB.bit_list_of_integer 3 (Nat_big_num.of_int crindex0)); - ("L", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k1)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3)))], - [(* always empty base effects*)] - ) - | `Pisel(reg0, reg1, reg2, k3) -> - ("Isel", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("BC", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Pandi(reg0, reg1, k2) -> - ("Andi", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("UI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pandis(reg0, reg1, k2) -> - ("Andis", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("UI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pori(reg0, reg1, k2) -> - ("Ori", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("UI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Poris(reg0, reg1, k2) -> - ("Oris", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("UI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pxori(reg0, reg1, k2) -> - ("Xori", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("UI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pxoris(reg0, reg1, k2) -> - ("Xoris", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("UI", IInt.Bvector (Some 16), SB.bit_list_of_integer 16 (Nat_big_num.of_int k2))], - [(* always empty base effects*)] - ) - | `Pand(setcr00, reg1, reg2, reg3) -> - ("And", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pxor(setcr00, reg1, reg2, reg3) -> - ("Xor", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pnand(setcr00, reg1, reg2, reg3) -> - ("Nand", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Por(setcr00, reg1, reg2, reg3) -> - ("Or", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pnor(setcr00, reg1, reg2, reg3) -> - ("Nor", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Peqv(setcr00, reg1, reg2, reg3) -> - ("Eqv", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pandc(setcr00, reg1, reg2, reg3) -> - ("Andc", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Porc(setcr00, reg1, reg2, reg3) -> - ("Orc", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pextsb(setcr00, reg1, reg2) -> - ("Extsb", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pextsh(setcr00, reg1, reg2) -> - ("Extsh", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pcntlzw(setcr00, reg1, reg2) -> - ("Cntlzw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pcmpb(reg0, k1, reg2) -> - ("Cmpb", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k1)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Ppopcntb(reg0, reg1) -> - ("Popcntb", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Ppopcntw(reg0, reg1) -> - ("Popcntw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Pprtyd(reg0, reg1) -> - ("Prtyd", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Pprtyw(reg0, reg1) -> - ("Prtyw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Pextsw(setcr00, reg1, reg2) -> - ("Extsw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pcntlzd(setcr00, reg1, reg2) -> - ("Cntlzd", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Ppopcntd(reg0, reg1) -> - ("Popcntd", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Pbpermd(reg0, reg1, reg2) -> - ("Bpermd", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Prlwinm(setcr00, reg1, reg2, k3, k4, k5) -> - ("Rlwinm", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SH", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k3)); - ("MB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k4)); - ("ME", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k5)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prlwnm(setcr00, reg1, reg2, reg3, k4, k5) -> - ("Rlwnm", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("MB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k4)); - ("ME", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k5)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prlwimi(setcr00, reg1, reg2, k3, k4, k5) -> - ("Rlwimi", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SH", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k3)); - ("MB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k4)); - ("ME", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k5)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prldicl(setcr00, reg1, reg2, k3, k4) -> - ("Rldicl", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("sh", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k3)); - ("mb", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k4)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prldicr(setcr00, reg1, reg2, k3, k4) -> - ("Rldicr", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("sh", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k3)); - ("me", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k4)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prldic(setcr00, reg1, reg2, k3, k4) -> - ("Rldic", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("sh", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k3)); - ("mb", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k4)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prldcl(setcr00, reg1, reg2, reg3, k4) -> - ("Rldcl", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("mb", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k4)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prldcr(setcr00, reg1, reg2, reg3, k4) -> - ("Rldcr", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("me", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k4)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Prldimi(setcr00, reg1, reg2, k3, k4) -> - ("Rldimi", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("sh", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k3)); - ("mb", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k4)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pslw(setcr00, reg1, reg2, reg3) -> - ("Slw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Psrw(setcr00, reg1, reg2, reg3) -> - ("Srw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Psrawi(setcr00, reg1, reg2, k3) -> - ("Srawi", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("SH", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k3)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Psraw(setcr00, reg1, reg2, reg3) -> - ("Sraw", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Psld(setcr00, reg1, reg2, reg3) -> - ("Sld", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Psrd(setcr00, reg1, reg2, reg3) -> - ("Srd", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Psradi(setcr00, reg1, reg2, k3) -> - ("Sradi", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("sh", IInt.Bvector (Some 6), SB.bit_list_of_integer 6 (Nat_big_num.of_int k3)); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Psrad(setcr00, reg1, reg2, reg3) -> - ("Srad", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pcdtbcd(reg0, reg1) -> - ("Cdtbcd", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Pcbcdtd(reg0, reg1) -> - ("Cbcdtd", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Paddg6s(reg0, reg1, reg2) -> - ("Addg6s", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pmtspr(k0, reg1) -> - ("Mtspr", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("spr", IInt.Bvector (Some 10), SB.bit_list_of_integer 10 (Nat_big_num.of_int k0))], - [(* always empty base effects*)] - ) - | `Pmfspr(reg0, k1) -> - ("Mfspr", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("spr", IInt.Bvector (Some 10), SB.bit_list_of_integer 10 (Nat_big_num.of_int k1))], - [(* always empty base effects*)] - ) - | `Pmtcrf(crmask0, reg1) -> - ("Mtcrf", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("FXM", IInt.Bvector (Some 8), SB.bit_list_of_integer 8 (Nat_big_num.of_int crmask0))], - [(* always empty base effects*)] - ) - | `Pmfcr(reg0) -> - ("Mfcr", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0)))], - [(* always empty base effects*)] - ) - | `Pmtocrf(crmask0, reg1) -> - ("Mtocrf", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("FXM", IInt.Bvector (Some 8), SB.bit_list_of_integer 8 (Nat_big_num.of_int crmask0))], - [(* always empty base effects*)] - ) - | `Pmfocrf(reg0, crmask1) -> - ("Mfocrf", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("FXM", IInt.Bvector (Some 8), SB.bit_list_of_integer 8 (Nat_big_num.of_int crmask1))], - [(* always empty base effects*)] - ) - | `Pmcrxr(crindex0) -> - ("Mcrxr", - [("BF", IInt.Bvector (Some 3), SB.bit_list_of_integer 3 (Nat_big_num.of_int crindex0))], - [(* always empty base effects*)] - ) - | `Pdlmzb(setcr00, reg1, reg2, reg3) -> - ("Dlmzb", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmacchw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Macchw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmacchws(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Macchws", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmacchwu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Macchwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmacchwsu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Macchwsu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmachhw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Machhw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmachhws(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Machhws", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmachhwu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Machhwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmachhwsu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Machhwsu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmaclhw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Maclhw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmaclhws(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Maclhws", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmaclhwu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Maclhwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmaclhwsu(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Maclhwsu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pmulchw(setcr00, reg1, reg2, reg3) -> - ("Mulchw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmulchwu(setcr00, reg1, reg2, reg3) -> - ("Mulchwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmulhhw(setcr00, reg1, reg2, reg3) -> - ("Mulhhw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmulhhwu(setcr00, reg1, reg2, reg3) -> - ("Mulhhwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmullhw(setcr00, reg1, reg2, reg3) -> - ("Mullhw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pmullhwu(setcr00, reg1, reg2, reg3) -> - ("Mullhwu", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr00)))], - [(* always empty base effects*)] - ) - | `Pnmacchw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Nmacchw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pnmacchws(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Nmacchws", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pnmachhw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Nmachhw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pnmachhws(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Nmachhws", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pnmaclhw(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Nmaclhw", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Pnmaclhws(setsoov0, setcr01, reg2, reg3, reg4) -> - ("Nmaclhws", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg3))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg4))); - ("OE", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_soov setsoov0))); - ("Rc", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int (trans_cr0 setcr01)))], - [(* always empty base effects*)] - ) - | `Picbi(reg0, reg1) -> - ("Icbi", - [("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1)))], - [(* always empty base effects*)] - ) - | `Picbt(k0, reg1, reg2) -> - ("Icbt", - [("CT", IInt.Bvector (Some 4), SB.bit_list_of_integer 4 (Nat_big_num.of_int k0)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pdcba(reg0, reg1) -> - ("Dcba", - [("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1)))], - [(* always empty base effects*)] - ) - | `Pdcbt(reg0, reg1, k2) -> - ("Dcbt", - [("TH", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1)))], - [(* always empty base effects*)] - ) - | `Pdcbtst(reg0, reg1, k2) -> - ("Dcbtst", - [("TH", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int k2)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1)))], - [(* always empty base effects*)] - ) - | `Pdcbz(reg0, reg1) -> - ("Dcbz", - [("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1)))], - [(* always empty base effects*)] - ) - | `Pdcbst(reg0, reg1) -> - ("Dcbst", - [("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1)))], - [(* always empty base effects*)] - ) - | `Pdcbf(reg0, reg1, k2) -> - ("Dcbf", - [("L", IInt.Bvector (Some 2), SB.bit_list_of_integer 2 (Nat_big_num.of_int k2)); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1)))], - [(* always empty base effects*)] - ) - | `Pisync -> - ("Isync", - [], - [(* always empty base effects*)] - ) - | `Plbarx(reg0, reg1, reg2, k3) -> - ("Lbarx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("EH", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Plharx(reg0, reg1, reg2, k3) -> - ("Lharx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("EH", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Plwarx(reg0, reg1, reg2, k3) -> - ("Lwarx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("EH", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Pstbcx(reg0, reg1, reg2) -> - ("Stbcx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Psthcx(reg0, reg1, reg2) -> - ("Sthcx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pstwcx(reg0, reg1, reg2) -> - ("Stwcx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Pldarx(reg0, reg1, reg2, k3) -> - ("Ldarx", - [("RT", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2))); - ("EH", IInt.Bit, SB.bit_list_of_integer 1 (Nat_big_num.of_int k3))], - [(* always empty base effects*)] - ) - | `Pstdcx(reg0, reg1, reg2) -> - ("Stdcx", - [("RS", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg0))); - ("RA", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg1))); - ("RB", IInt.Bvector (Some 5), SB.bit_list_of_integer 5 (Nat_big_num.of_int (int_of_reg reg2)))], - [(* always empty base effects*)] - ) - | `Psync(k0) -> - ("Sync", - [("L", IInt.Bvector (Some 2), SB.bit_list_of_integer 2 (Nat_big_num.of_int k0))], - [(* always empty base effects*)] - ) - | `Peieio -> - ("Eieio", - [], - [(* always empty base effects*)] - ) - | `Pwait(k0) -> - ("Wait", - [("WC", IInt.Bvector (Some 2), SB.bit_list_of_integer 2 (Nat_big_num.of_int k0))], - [(* always empty base effects*)] - ) |