From c29871c2d5c7860c6c6c53e8d5c8a9fe434742d2 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Nov 2013 14:36:18 +0000
Subject: 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
---
 powerpc/Asmgen.v | 39 +++++++++++++++++++++++++++++++++------
 1 file changed, 33 insertions(+), 6 deletions(-)

(limited to 'powerpc/Asmgen.v')

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
-- 
cgit