diff options
Diffstat (limited to 'powerpc/Machregs.v')
-rw-r--r-- | powerpc/Machregs.v | 23 |
1 files changed, 18 insertions, 5 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index ce9c3542..6f2c6a03 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -86,7 +86,7 @@ Definition mreg_type (r: mreg): typ := match r with | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 - | R25 | R26 | R27 | R28 | R29 | R30 | R31 => Tany32 + | R25 | R26 | R27 | R28 | R29 | R30 | R31 => if Archi.ppc64 then Tany64 else Tany32 | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 @@ -159,11 +159,25 @@ Definition register_by_name (s: string) : option mreg := (** ** Destroyed registers, preferred registers *) +Definition destroyed_by_cond (cond: condition): list mreg := + match cond with + | Ccomplimm _ _ | Ccompluimm _ _ => R12 :: nil + | _ => nil + end. + Definition destroyed_by_op (op: operation): list mreg := match op with | Ofloatconst _ => R12 :: nil | Osingleconst _ => R12 :: nil + | Olongconst _ => R12 :: nil | Ointoffloat | Ointuoffloat => F13 :: nil + | Olongoffloat => F13 :: nil + | Oaddlimm _ => R12 :: nil + | Oandlimm _ => R12 :: nil + | Oorlimm _ => R12 :: nil + | Oxorlimm _ => R12 :: nil + | Orolml _ _ => R12 :: nil + | Ocmp c => destroyed_by_cond c | _ => nil end. @@ -173,9 +187,6 @@ Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := R11 :: R12 :: nil. -Definition destroyed_by_cond (cond: condition): list mreg := - nil. - Definition destroyed_by_jumptable: list mreg := R12 :: nil. @@ -239,11 +250,13 @@ Global Opaque (** Two-address operations. Return [true] if the first argument and the result must be in the same location *and* are unconstrained - by [mregs_for_operation]. There is only one: rotate-mask-insert. *) + by [mregs_for_operation]. *) Definition two_address_op (op: operation) : bool := match op with | Oroli _ _ => true + | Olowlong => true + | Ofloatofsingle => true | _ => false end. |