diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-17 14:36:18 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-17 14:36:18 +0000 |
| commit | c29871c2d5c7860c6c6c53e8d5c8a9fe434742d2 (patch) | |
| tree | 9e002b414d3fb3a899deb43f9f6e14d02507121a /powerpc/Asmgen.v | |
| parent | 26bb5772c75efe1e4617fb9c4f2b8522989fac6d (diff) | |
| download | compcert-kvx-c29871c2d5c7860c6c6c53e8d5c8a9fe434742d2.tar.gz compcert-kvx-c29871c2d5c7860c6c6c53e8d5c8a9fe434742d2.zip | |
powerpc/: new unary operation "addsymbol"
Support far-data addressing in sections.
(Currently ignored in checklink.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgen.v')
| -rw-r--r-- | powerpc/Asmgen.v | 39 |
1 files changed, 33 insertions, 6 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index cc9a51cb..b3f07224 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -322,6 +322,11 @@ Definition transl_cond_op (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) +Definition csymbol_high (s: ident) (ofs: int) (rel: bool) := + if rel then Csymbol_rel_high s ofs else Csymbol_high s ofs. +Definition csymbol_low (s: ident) (ofs: int) (rel: bool) := + if rel then Csymbol_rel_low s ofs else Csymbol_low s ofs. + Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with @@ -340,8 +345,9 @@ Definition transl_op OK (if symbol_is_small_data s ofs then Paddi r GPR0 (Csymbol_sda s ofs) :: k else - Paddis r GPR0 (Csymbol_high s ofs) :: - Paddi r r (Csymbol_low s ofs) :: k) + let rel := symbol_is_rel_data s ofs in + Paddis r GPR0 (csymbol_high s ofs rel) :: + Paddi r r (csymbol_low s ofs rel) :: k) | Oaddrstack n, nil => do r <- ireg_of res; OK (addimm r GPR1 n k) | Ocast8signed, a1 :: nil => @@ -353,6 +359,18 @@ Definition transl_op OK (Padd r r1 r2 :: k) | Oaddimm n, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; OK (addimm r r1 n k) + | Oaddsymbol s ofs, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (if symbol_is_small_data s ofs then + Paddi GPR0 GPR0 (Csymbol_sda s ofs) :: + Padd r r1 GPR0 :: k + else if symbol_is_rel_data s ofs then + Paddis GPR0 GPR0 (Csymbol_rel_high s ofs) :: + Padd r r1 GPR0 :: + Paddi r r (Csymbol_rel_low s ofs) :: k + else + Paddis r r1 (Csymbol_high s ofs) :: + Paddi r r (Csymbol_low s ofs) :: k) | Osub, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; OK (Psubfc r r2 r1 :: k) @@ -499,12 +517,21 @@ Definition transl_memory_access OK (if symbol_is_small_data symb ofs then mk1 (Csymbol_sda symb ofs) GPR0 :: k else - Paddis temp GPR0 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k) + let rel := symbol_is_rel_data symb ofs in + Paddis temp GPR0 (csymbol_high symb ofs rel) :: + mk1 (csymbol_low symb ofs rel) temp :: k) | Abased symb ofs, a1 :: nil => do r1 <- ireg_of a1; - OK (Paddis temp r1 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k) + OK (if symbol_is_small_data symb ofs then + Paddi GPR0 GPR0 (Csymbol_sda symb ofs) :: + mk2 r1 GPR0 :: k + else if symbol_is_rel_data symb ofs then + Paddis GPR0 GPR0 (Csymbol_rel_high symb ofs) :: + Padd temp r1 GPR0 :: + mk1 (Csymbol_rel_low symb ofs) temp :: k + else + Paddis temp r1 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k) | Ainstack ofs, nil => OK (if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) GPR1 :: k |