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

21 files changed, 302 insertions, 92 deletions

diff --git a/Makefile b/Makefile
index 66765d6..a4d2036 100644
--- a/Makefile
+++ b/Makefile
@@ -138,7 +138,7 @@ proof: $(FILES:.v=.vo)
 
 extraction: extraction/STAMP
 
-extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v
+extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v
 	rm -f extraction/*.ml extraction/*.mli
 	$(COQEXEC) extraction/extraction.v
 	touch extraction/STAMP
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 3890985..850682e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -36,7 +36,7 @@ type atom_info =
     a_alignment: int option;           (* alignment *)
     a_sections: Sections.section_name list; (* in which section to put it *)
       (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *)
-    a_small_data: bool;                (* data in a small data area? *)
+    a_access: Sections.access_mode;    (* access mode, e.g. small data area *)
     a_inline: bool;                    (* function declared inline? *)
     a_loc: location                    (* source location *)
 }
@@ -120,7 +120,7 @@ let name_for_string_literal env s =
       { a_storage = C.Storage_static;
         a_alignment = Some 1;
         a_sections = [Sections.for_stringlit()];
-        a_small_data = false;
+        a_access = Sections.Access_default;
         a_inline = false;
         a_loc = Cutil.no_loc };
     Hashtbl.add stringTable s id;
@@ -786,7 +786,7 @@ let convertFundef loc env fd =
     { a_storage = fd.fd_storage;
       a_alignment = None;
       a_sections = Sections.for_function env id' fd.fd_ret;
-      a_small_data = false;
+      a_access = Sections.Access_default;
       a_inline = fd.fd_inline;
       a_loc = loc };
   (id', Gfun(Internal {fn_return = ret; fn_params = params;
@@ -856,7 +856,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
         if sto = C.Storage_extern then [] else [Init_space sz]
     | Some i ->
         convertInitializer env ty i in
-  let (section, near_access) =
+  let (section, access) =
     Sections.for_variable env id' ty (optinit <> None) in
   if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then
     error (sprintf "Variable %s is too big (%s bytes)"
@@ -865,7 +865,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
     { a_storage = sto;
       a_alignment = Some (Z.to_int al);
       a_sections = [section];
-      a_small_data = near_access;
+      a_access = access;
       a_inline = false;
       a_loc = loc };
   let volatile = List.mem C.AVolatile attr in
@@ -1048,7 +1048,13 @@ let atom_sections a =
 
 let atom_is_small_data a ofs =
   try
-    (Hashtbl.find decl_atom a).a_small_data
+    (Hashtbl.find decl_atom a).a_access = Sections.Access_near
+  with Not_found ->
+    false
+
+let atom_is_rel_data a ofs =
+  try
+    (Hashtbl.find decl_atom a).a_access = Sections.Access_far
   with Not_found ->
     false
 
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index a31378e..3c0c9f1 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -20,19 +20,20 @@ open Camlcoq
 
 (* #pragma section *)
 
-let sda_supported =
-  match Configuration.arch, Configuration.system with
-  | "powerpc", "linux" -> true
-  | "powerpc", "diab"  -> true
-  | _, _ -> false
-
 let process_section_pragma classname istring ustring addrmode accmode =
   Sections.define_section classname
     ?iname: (if istring = "" then None else Some istring)
     ?uname: (if ustring = "" then None else Some ustring)
-    ?writable: (if accmode = "" then None else Some(String.contains accmode 'W'))
-    ?executable: (if accmode = "" then None else Some(String.contains accmode 'X'))
-    ?near: (if addrmode = "" then None else Some(sda_supported && addrmode = "near-data"))
+    ?writable:
+      (if accmode = "" then None else Some(String.contains accmode 'W'))
+    ?executable:
+      (if accmode = "" then None else Some(String.contains accmode 'X'))
+    ?access:
+      (match addrmode with
+       | "" -> None
+       | "near-data" -> Some Sections.Access_near
+       | "far-data" -> Some Sections.Access_far
+       | _ -> Some Sections.Access_default)
     ()
 
 (* #pragma use_section *)
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml
index 794d47a..5b3abe8 100644
--- a/checklink/Asm_printers.ml
+++ b/checklink/Asm_printers.ml
@@ -109,6 +109,8 @@ let string_of_constant = function
 | Csymbol_low   (i0, i1)    -> "Csymbol_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
 | Csymbol_high  (i0, i1)    -> "Csymbol_high(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
 | Csymbol_sda   (i0, i1)    -> "Csymbol_sda(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
+| Csymbol_rel_low  (i0, i1) -> "Csymbol_rel_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
+| Csymbol_rel_high (i0, i1) -> "Csymbol_rel_high(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
 
 let string_of_crbit = function
 | CRbit_0    -> "CRbit_0"
diff --git a/checklink/Check.ml b/checklink/Check.ml
index be1360d..59ee4ee 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -436,6 +436,12 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw ->
   | Csymbol_sda (ident, i) ->
       (* sda should be handled separately in places it occurs *)
       fatal "Unhandled Csymbol_sda, please report."
+  | Csymbol_rel_low (ident, i) | Csymbol_rel_high (ident, i) ->
+      (* not checked yet *)
+      OK((ff_ef ^%=
+           (add_log (WARNING("Cannot check access to far-data symbol " ^
+                              Hashtbl.find ffw.sf.ident_to_name ident))))
+         ffw)
 
 let match_z_int32 (cz: Z.t) (ei: int32) =
   let cz = z_int32 cz in
diff --git a/common/Sections.ml b/common/Sections.ml
index 90ddea7..d7ae819 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -28,12 +28,17 @@ type section_name =
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
 
+type access_mode =
+  | Access_default
+  | Access_near
+  | Access_far
+
 type section_info = {
   sec_name_init: section_name;
   sec_name_uninit: section_name;
   sec_writable: bool;
   sec_executable: bool;
-  sec_near_access: bool
+  sec_access: access_mode
 }
 
 let default_section_info = {
@@ -41,7 +46,7 @@ let default_section_info = {
   sec_name_uninit = Section_data false;
   sec_writable = true;
   sec_executable = false;
-  sec_near_access = false
+  sec_access = Access_default
 }
 
 (* Built-in sections *)
@@ -51,42 +56,42 @@ let builtin_sections = [
      {sec_name_init = Section_text; 
       sec_name_uninit = Section_text;
       sec_writable = false; sec_executable = true;
-      sec_near_access = false};
+      sec_access = Access_default};
   "DATA",
      {sec_name_init = Section_data true;
       sec_name_uninit = Section_data false;
       sec_writable = true; sec_executable = false;
-      sec_near_access = false};
+      sec_access = Access_default};
   "SDATA",
      {sec_name_init = Section_small_data true;
       sec_name_uninit = Section_small_data false;
       sec_writable = true; sec_executable = false;
-      sec_near_access = true};
+      sec_access = Access_near};
   "CONST",
      {sec_name_init = Section_const;
       sec_name_uninit = Section_const;
       sec_writable = false; sec_executable = false;
-      sec_near_access = false};
+      sec_access = Access_default};
   "SCONST",
      {sec_name_init = Section_small_const;
       sec_name_uninit = Section_small_const;
       sec_writable = false; sec_executable = false;
-      sec_near_access = true};
+      sec_access = Access_near};
   "STRING",
      {sec_name_init = Section_string;
       sec_name_uninit = Section_string;
       sec_writable = false; sec_executable = false;
-      sec_near_access = false};
+      sec_access = Access_default};
   "LITERAL",
      {sec_name_init = Section_literal;
       sec_name_uninit = Section_literal;
       sec_writable = false; sec_executable = false;
-      sec_near_access = false};
+      sec_access = Access_default};
   "JUMPTABLE",
      {sec_name_init = Section_jumptable;
       sec_name_uninit = Section_jumptable;
       sec_writable = false; sec_executable = false;
-      sec_near_access = false}
+      sec_access = Access_default}
 ]
 
 (* The current mapping from section names to section info *)
@@ -108,7 +113,7 @@ let initialize () =
 
 (* Define or update a given section. *)
 
-let define_section name ?iname ?uname ?writable ?executable ?near () =
+let define_section name ?iname ?uname ?writable ?executable ?access () =
   let si = 
     try Hashtbl.find current_section_table name
     with Not_found -> default_section_info in
@@ -116,8 +121,8 @@ let define_section name ?iname ?uname ?writable ?executable ?near () =
     match writable with Some b -> b | None -> si.sec_writable
   and executable =
     match executable with Some b -> b | None -> si.sec_executable
-  and near =
-    match near with Some b -> b | None -> si.sec_near_access in
+  and access =
+    match access with Some b -> b | None -> si.sec_access in
   let iname =
     match iname with Some s -> Section_user(s, writable, executable)
                    | None -> si.sec_name_init in
@@ -129,7 +134,7 @@ let define_section name ?iname ?uname ?writable ?executable ?near () =
       sec_name_uninit = uname;
       sec_writable = writable;
       sec_executable = executable;
-      sec_near_access = near } in
+      sec_access = access } in
   Hashtbl.replace current_section_table name new_si
 
 (* Explicitly associate a section to a global symbol *)
@@ -148,7 +153,7 @@ let gcc_section name readonly exec =
   let sn = Section_user(name, not readonly, exec) in
   { sec_name_init = sn; sec_name_uninit = sn;
     sec_writable = not readonly; sec_executable = exec;
-    sec_near_access = false }
+    sec_access = Access_default }
 
 (* Determine section for a variable definition *)
 
@@ -176,7 +181,7 @@ let for_variable env id ty init =
           Hashtbl.find current_section_table name
         with Not_found ->
           assert false in
-  ((if init then si.sec_name_init else si.sec_name_uninit), si.sec_near_access)
+  ((if init then si.sec_name_init else si.sec_name_uninit), si.sec_access)
 
 (* Determine sections for a function definition *)
 
diff --git a/common/Sections.mli b/common/Sections.mli
index 8b7c9dc..ff6c8c9 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -27,14 +27,19 @@ type section_name =
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
 
+type access_mode =
+  | Access_default
+  | Access_near
+  | Access_far
+
 val initialize: unit -> unit
 
 val define_section:
   string -> ?iname:string -> ?uname:string
-         -> ?writable:bool -> ?executable:bool -> ?near:bool -> unit -> unit
+         -> ?writable:bool -> ?executable:bool -> ?access:access_mode -> unit -> unit
 val use_section_for: AST.ident -> string -> bool
 
 val for_variable: Env.t -> AST.ident -> C.typ -> bool ->
-                                          section_name * bool
+                                          section_name * access_mode
 val for_function: Env.t -> AST.ident -> C.typ -> section_name list
 val for_stringlit: unit -> section_name
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index e6e9d76..1441929 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -101,7 +101,9 @@ Inductive constant: Type :=
   | Cint: int -> constant
   | Csymbol_low: ident -> int -> constant
   | Csymbol_high: ident -> int -> constant
-  | Csymbol_sda: ident -> int -> constant.
+  | Csymbol_sda: ident -> int -> constant
+  | Csymbol_rel_low: ident -> int -> constant
+  | Csymbol_rel_high: ident -> int -> constant.
 
 (** A note on constants: while immediate operands to PowerPC
   instructions must be representable in 16 bits (with
@@ -422,6 +424,8 @@ Axiom small_data_area_addressing:
   symbol_is_small_data id ofs = true ->
   small_data_area_offset ge id ofs = symbol_offset id ofs.
 
+Parameter symbol_is_rel_data: ident -> int -> bool.
+
 (** Armed with the [low_half] and [high_half] functions,
   we can define the evaluation of a symbolic constant.
   Note that for [const_high], integer constants
@@ -436,6 +440,8 @@ Definition const_low (c: constant) :=
   | Csymbol_low id ofs => low_half (symbol_offset id ofs)
   | Csymbol_high id ofs => Vundef
   | Csymbol_sda id ofs => small_data_area_offset ge id ofs
+  | Csymbol_rel_low id ofs => low_half (symbol_offset id ofs)
+  | Csymbol_rel_high id ofs => Vundef
   end.
 
 Definition const_high (c: constant) :=
@@ -444,6 +450,8 @@ Definition const_high (c: constant) :=
   | Csymbol_low id ofs => Vundef
   | Csymbol_high id ofs => high_half (symbol_offset id ofs)
   | Csymbol_sda id ofs => Vundef
+  | Csymbol_rel_low id ofs => Vundef
+  | Csymbol_rel_high id ofs => high_half (symbol_offset id ofs)
   end.
 
 (** The semantics is purely small-step and defined as a function
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index cc9a51c..b3f0722 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
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 869fab3..990d35d 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -243,6 +243,8 @@ Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
   destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
   destruct (symbol_is_small_data i i0); TailNoLabel.
+  destruct (symbol_is_small_data i i0); TailNoLabel.
+  destruct (symbol_is_rel_data i i0); TailNoLabel.
   destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
   destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
   eapply transl_cond_op_label; eauto.
@@ -259,6 +261,8 @@ Proof.
   unfold transl_memory_access; intros; destruct addr; TailNoLabel.
   destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
   destruct (symbol_is_small_data i i0); TailNoLabel.
+  destruct (symbol_is_small_data i i0); TailNoLabel.
+  destruct (symbol_is_rel_data i i0); TailNoLabel.
   destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
 Qed.
 
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index cd961c9..d9b6cf3 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -103,6 +103,42 @@ Proof.
   rewrite Int.sub_idem. apply Int.add_zero.
 Qed.
 
+Lemma add_zero_symbol_offset:
+  forall ge id ofs,
+  Val.add Vzero (symbol_offset ge id ofs) = symbol_offset ge id ofs.
+Proof.
+  unfold symbol_offset; intros. destruct (Genv.find_symbol ge id); auto. 
+  simpl. rewrite Int.add_zero; auto.
+Qed.
+
+Lemma csymbol_high_low:
+  forall ge id ofs,
+  Val.add (high_half (symbol_offset ge id ofs)) (low_half (symbol_offset ge id ofs))
+  = symbol_offset ge id ofs.
+Proof.
+  intros. rewrite Val.add_commut. apply low_high_half.
+Qed.
+
+Lemma csymbol_high_low_2:
+  forall ge id ofs rel,
+  Val.add (const_high ge (csymbol_high id ofs rel))
+          (const_low ge (csymbol_low id ofs rel)) = symbol_offset ge id ofs.
+Proof.
+  intros. destruct rel; apply csymbol_high_low. 
+Qed.
+
+(*
+Lemma csymbol_sda_eq:
+  forall ge id ofs,
+  symbol_is_small_data id ofs = true ->
+  Val.add Vzero (const_low ge (Csymbol_sda id ofs)) = symbol_offset ge id ofs.
+Proof.
+  intros. unfold const_low. rewrite small_data_area_addressing by auto. 
+  unfold symbol_offset. 
+  destruct (Genv.find_symbol ge id); simpl; auto. rewrite Int.add_zero; auto.
+Qed.
+*)
+
 (** Useful properties of the GPR0 registers. *)
 
 Lemma gpr_or_zero_not_zero:
@@ -827,17 +863,14 @@ Opaque Int.eq.
   set (v' := symbol_offset ge i i0).
   destruct (symbol_is_small_data i i0) eqn:SD.
   (* small data *)
+Opaque Val.add.
   econstructor; split. apply exec_straight_one; simpl; reflexivity.
-  split. Simpl. rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. 
-  destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. 
+  split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset.
   intros; Simpl.
   (* not small data *)
-Opaque Val.add.
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
-  split. Simpl. rewrite gpr_or_zero_zero.
-  rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl.  
-  rewrite (Val.add_commut Vzero). rewrite high_half_zero. 
-  rewrite Val.add_commut. rewrite low_high_half. auto.
+  split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl.
+  rewrite Val.add_assoc. rewrite csymbol_high_low_2. apply add_zero_symbol_offset. 
   intros; Simpl. 
   (* Oaddrstack *)
   destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen.
@@ -845,6 +878,26 @@ Opaque Val.add.
   (* Oaddimm *)
   destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen.
   exists rs'; auto with asmgen.
+  (* Oaddsymbol *)
+  destruct (symbol_is_small_data i i0) eqn:SD.
+  (* small data *)
+  econstructor; split. eapply exec_straight_two; simpl; reflexivity. 
+  split. Simpl. rewrite (Val.add_commut (rs x)). f_equal.
+  rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset.
+  intros; Simpl.
+  destruct (symbol_is_rel_data i i0).
+  (* relative data *)
+  econstructor; split. eapply exec_straight_three; simpl; reflexivity. 
+  split. Simpl. rewrite gpr_or_zero_zero. rewrite gpr_or_zero_not_zero by (eauto with asmgen).
+  Simpl. rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal. 
+  rewrite Val.add_assoc. rewrite csymbol_high_low. apply add_zero_symbol_offset.
+  intros; Simpl.
+  (* absolute data *)
+  econstructor; split. eapply exec_straight_two; simpl; reflexivity.
+  split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl. 
+  rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal.
+  apply csymbol_high_low.
+  intros; Simpl.
   (* Osubimm *)
   case (Int.eq (high_s i) Int.zero).
   TranslOpSimpl.
@@ -935,12 +988,12 @@ Lemma transl_memory_access_correct:
   temp <> GPR0 ->
   (forall cst (r1: ireg) (rs1: regset) k,
     Val.add (gpr_or_zero rs1 r1) (const_low ge cst) = a ->
-    (forall r, r <> PC -> r <> temp -> rs1 r = rs r) ->
+    (forall r, r <> PC -> r <> temp -> r <> GPR0 -> rs1 r = rs r) ->
     exists rs',
         exec_straight ge fn (mk1 cst r1 :: k) rs1 m k rs' m' /\ P rs') ->
   (forall (r1 r2: ireg) (rs1: regset) k,
     Val.add rs1#r1 rs1#r2 = a ->
-    (forall r, r <> PC -> r <> temp -> rs1 r = rs r) ->
+    (forall r, r <> PC -> r <> temp -> r <> GPR0 -> rs1 r = rs r) ->
     exists rs',
         exec_straight ge fn (mk2 r1 r2 :: k) rs1 m k rs' m' /\ P rs') ->
   exists rs',
@@ -969,34 +1022,61 @@ Transparent Val.add.
   (* Aglobal *)
   destruct (symbol_is_small_data i i0) eqn:SISD; inv TR.
   (* Aglobal from small data *)
-  apply MK1. simpl. rewrite small_data_area_addressing; auto.
-  unfold symbol_address, symbol_offset. 
-  destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto.
+  apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. 
+  apply add_zero_symbol_offset.
   auto.
   (* Aglobal general case *)
-  set (rs1 := nextinstr (rs#temp <- (const_high ge (Csymbol_high i i0)))).
-  exploit (MK1 (Csymbol_low i i0) temp rs1 k).
+  set (rel := symbol_is_rel_data i i0).
+  set (rs1 := nextinstr (rs#temp <- (const_high ge (csymbol_high i i0 rel)))).
+  exploit (MK1 (csymbol_low i i0 rel) temp rs1 k).
     simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
-    unfold rs1. Simpl. 
-    unfold const_high, const_low.
-    rewrite Val.add_commut. rewrite low_high_half. auto.
+    unfold rs1. Simpl. apply csymbol_high_low_2.
     intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
   unfold exec_instr. rewrite gpr_or_zero_zero. 
-  rewrite Val.add_commut. unfold const_high. 
-  rewrite high_half_zero.
-  reflexivity. reflexivity.
+  rewrite Val.add_commut. unfold const_high, csymbol_high. 
+  destruct rel; rewrite high_half_zero; reflexivity.
+  reflexivity.
   assumption. assumption.
   (* Abased *)
+  destruct (symbol_is_small_data i i0) eqn:SISD.
+  (* Abased from small data *)
+  set (rs1 := nextinstr (rs#GPR0 <- (symbol_offset ge i i0))).
+  exploit (MK2 x GPR0 rs1 k).
+    unfold rs1; Simpl. apply Val.add_commut.
+    intros. unfold rs1; Simpl.
+  intros [rs' [EX' AG']].
+  exists rs'; split. apply exec_straight_step with rs1 m. 
+  unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. 
+  unfold const_low. rewrite small_data_area_addressing; auto.
+  apply add_zero_symbol_offset.
+  reflexivity.
+  assumption. assumption.
+  destruct (symbol_is_rel_data i i0).
+  (* Abased relative *)
+  set (rs1 := nextinstr (rs#GPR0 <- (const_high ge (Csymbol_rel_high i i0)))).
+  set (rs2 := nextinstr (rs1#temp <- (Val.add (rs x) (const_high ge (Csymbol_rel_high i i0))))).
+  exploit (MK1 (Csymbol_rel_low i i0) temp rs2 k).
+    simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
+    unfold rs2. Simpl. rewrite Val.add_assoc. simpl. rewrite csymbol_high_low. 
+    apply Val.add_commut.
+    intros. unfold rs2; Simpl. unfold rs1; Simpl.
+  intros [rs' [EX' AG']].
+  exists rs'. split. apply exec_straight_step with rs1 m.
+  unfold exec_instr. rewrite gpr_or_zero_zero. 
+  rewrite (Val.add_commut Vzero). unfold const_high. rewrite high_half_zero. auto.
+  reflexivity.
+  apply exec_straight_step with rs2 m.
+  simpl. unfold rs2, rs1. Simpl.
+  reflexivity.
+  assumption. assumption.
+  (* Abased absolute *)
   set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (const_high ge (Csymbol_high i i0))))).
   exploit (MK1 (Csymbol_low i i0) temp rs1 k).
     simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
     unfold rs1. Simpl. 
-    rewrite Val.add_assoc. 
-    unfold const_high, const_low. 
-    symmetry. rewrite Val.add_commut. f_equal. f_equal. 
-    rewrite Val.add_commut. rewrite low_high_half. auto.
+    rewrite Val.add_assoc. simpl. rewrite csymbol_high_low. apply Val.add_commut. 
     intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
@@ -1028,7 +1108,7 @@ Lemma transl_load_correct:
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dst) = v
-  /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r.
+  /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r.
 Proof.
   intros.
   assert (BASE: forall mk1 mk2 k' chunk' v',
@@ -1043,7 +1123,7 @@ Proof.
   exists rs',
      exec_straight ge fn c rs m k' rs' m
   /\ rs'#(preg_of dst) = v'
-  /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r).
+  /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r).
   {
   intros. eapply transl_memory_access_correct; eauto. congruence.
   intros. econstructor; split. apply exec_straight_one. 
@@ -1095,7 +1175,7 @@ Lemma transl_store_correct:
   Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
   exists rs',
      exec_straight ge fn c rs m k rs' m'
-  /\ forall r, r <> PC -> preg_notin r (destroyed_by_store chunk addr) -> rs' r = rs r.
+  /\ forall r, r <> PC -> r <> GPR0 -> preg_notin r (destroyed_by_store chunk addr) -> rs' r = rs r.
 Proof.
 Local Transparent destroyed_by_store.
   intros.
@@ -1119,15 +1199,15 @@ Local Transparent destroyed_by_store.
     store2 chunk' (preg_of src) r1 r2 rs1 m) ->
   exists rs',
      exec_straight ge fn c rs m k rs' m'
-  /\ forall r, r <> PC -> r <> GPR11 /\ r <> GPR12 -> rs' r = rs r).
+  /\ forall r, r <> PC -> r <> GPR0 -> r <> GPR11 /\ r <> GPR12 -> rs' r = rs r).
   {
   intros. eapply transl_memory_access_correct; eauto.
   intros. econstructor; split. apply exec_straight_one. 
   rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. 
-  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H9; congruence. 
+  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. 
   intros. econstructor; split. apply exec_straight_one. 
   rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. 
-  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H9; congruence. 
+  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. 
   }
   destruct chunk; monadInv H.
 - (* Mint8signed *)
@@ -1150,10 +1230,10 @@ Local Transparent destroyed_by_store.
   intros. econstructor; split. apply exec_straight_one. 
   simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. 
 Local Transparent destroyed_by_store.
-  simpl; intros. destruct H4 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
+  simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
   intros. econstructor; split. apply exec_straight_one. 
   simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. 
-  simpl; intros. destruct H4 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
+  simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence.
 - (* Mfloat64 *)
   apply Mem.storev_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto.
 - (* Mfloat64al32 *)
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index b755b5e..9bee4db 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -89,6 +89,7 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Oaddimm n, I n1 :: nil => I (Int.add n1 n)
   | Oaddimm n, G s1 n1 :: nil => G s1 (Int.add n1 n)
   | Oaddimm n, S n1 :: nil => S (Int.add n1 n)
+  | Oaddsymbol s ofs, I n :: nil => G s (Int.add ofs n)
   | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2)
   | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
   | Osub, S n1 :: I n2 :: nil => S (Int.sub n1 n2)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index b7fad69..2aba9c2 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -138,6 +138,8 @@ Proof.
 
   rewrite Val.add_assoc; auto.
 
+  rewrite shift_symbol_address; auto. 
+  
   unfold symbol_address. destruct (Genv.find_symbol ge s1); auto. 
 
   rewrite Val.sub_add_opp. rewrite Val.add_assoc. simpl. rewrite Int.sub_add_opp. auto.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 085a098..dbc474e 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -61,6 +61,7 @@ Inductive operation : Type :=
   | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
   | Oadd: operation                     (**r [rd = r1 + r2] *)
   | Oaddimm: int -> operation           (**r [rd = r1 + n] *)
+  | Oaddsymbol: ident -> int -> operation (**r [rd = addr(id + ofs) + r1] *)
   | Osub: operation                     (**r [rd = r1 - r2] *)
   | Osubimm: int -> operation           (**r [rd = n - r1] *)
   | Omul: operation                     (**r [rd = r1 * r2] *)
@@ -183,6 +184,7 @@ Definition eval_operation
   | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1::v2::nil => Some (Val.add v1 v2)
   | Oaddimm n, v1::nil => Some (Val.add v1 (Vint n))
+  | Oaddsymbol s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1)
   | Osub, v1::v2::nil => Some (Val.sub v1 v2)
   | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1)
   | Omul, v1::v2::nil => Some (Val.mul v1 v2)
@@ -276,6 +278,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocast16signed => (Tint :: nil, Tint)
   | Oadd => (Tint :: Tint :: nil, Tint)
   | Oaddimm _ => (Tint :: nil, Tint)
+  | Oaddsymbol _ _ => (Tint :: nil, Tint)
   | Osub => (Tint :: Tint :: nil, Tint)
   | Osubimm _ => (Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
@@ -353,6 +356,7 @@ Proof with (try exact I).
   destruct v0...
   destruct v0; destruct v1...
   destruct v0...
+  unfold symbol_address. destruct (Genv.find_symbol genv i)... destruct v0...
   destruct v0; destruct v1... simpl. destruct (eq_block b b0)...
   destruct v0...
   destruct v0; destruct v1...
@@ -650,19 +654,24 @@ Variable ge2: Genv.t F2 V2.
 Hypothesis agree_on_symbols:
   forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
 
+Remark symbol_address_preserved:
+  forall s ofs, symbol_address ge2 s ofs = symbol_address ge1 s ofs.
+Proof.
+  unfold symbol_address; intros. rewrite agree_on_symbols; auto.
+Qed.
+ 
 Lemma eval_operation_preserved:
   forall sp op vl m,
   eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
 Proof.
-  intros. destruct op; simpl; auto. 
-  destruct vl; auto. decEq. unfold symbol_address. rewrite agree_on_symbols. auto.
+  intros. destruct op; simpl; auto; rewrite symbol_address_preserved; auto.
 Qed.
 
 Lemma eval_addressing_preserved:
   forall sp addr vl,
   eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl.
 Proof.
-  intros. destruct addr; simpl; auto; unfold symbol_address; rewrite agree_on_symbols; auto.
+  intros. destruct addr; simpl; auto; rewrite symbol_address_preserved; auto.
 Qed.
 
 End GENV_TRANSF.
@@ -760,6 +769,7 @@ Proof.
   inv H4; simpl; auto.
   apply Values.val_add_inject; auto.
   apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto.
   inv H4; inv H2; simpl; auto. econstructor; eauto. 
     rewrite Int.sub_add_l. auto.
     destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. 
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 08438df..e720b6f 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -100,6 +100,10 @@ let constant oc cst =
       | Diab ->
           fprintf oc "(%a)@sdarx" symbol_offset (s, camlint_of_coqint n)
       end
+  | Csymbol_rel_low(s, n) ->
+      fprintf oc "(%a)@sdax@l" symbol_offset (s, camlint_of_coqint n)
+  | Csymbol_rel_high(s, n) ->
+      fprintf oc "(%a)@sdarx@ha" symbol_offset (s, camlint_of_coqint n)
 
 let num_crbit = function
   | CRbit_0 -> 0
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index eda41d1..664280f 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -57,6 +57,8 @@ let print_operation reg pp = function
   | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1
   | Oadd, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2
   | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n)
+  | Oaddsymbol(id, ofs), [r1] ->
+      fprintf pp "\"%s\" + %ld + %a" (extern_atom id) (camlint_of_coqint ofs) reg r1
   | Osub, [r1;r2] -> fprintf pp "%a - %a" reg r1 reg r2
   | Osubimm n, [r1] -> fprintf pp "%ld - %a" (camlint_of_coqint n) reg r1
   | Omul, [r1;r2] -> fprintf pp "%a * %a" reg r1 reg r2
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index b0e7c4d..bdb94bd 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -79,25 +79,41 @@ Nondetfunction addimm (n: int) (e: expr) :=
   | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Int.add n m)) Enil
   | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Int.add n m)) Enil
   | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
+  | Eop (Oaddsymbol s m) (t ::: Enil) => Eop (Oaddsymbol s (Int.add n m)) (t ::: Enil)
   | _                            => Eop (Oaddimm n) (e ::: Enil)
   end.
 
+Nondetfunction addsymbol (s: ident) (ofs: int) (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Eop (Oaddrsymbol s (Int.add ofs n)) Enil
+  | Eop (Oaddimm n) (t ::: Enil) => Eop (Oaddsymbol s (Int.add ofs n)) (t ::: Enil)
+  | _ => Eop (Oaddsymbol s ofs) (e ::: Enil)
+  end.
+
 Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 =>
       addimm n1 t2
   | t1, Eop (Ointconst n2) Enil =>
       addimm n2 t1
+  | Eop (Oaddrsymbol s ofs) Enil, t2 =>
+      addsymbol s ofs t2
+  | t1, Eop (Oaddrsymbol s ofs) Enil =>
+      addsymbol s ofs t1
   | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
   | Eop (Oaddimm n1) (t1:::Enil), t2 =>
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
-  | Eop (Oaddrsymbol s n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
-      Eop Oadd (Eop (Oaddrsymbol s (Int.add n1 n2)) Enil ::: t2 ::: Enil)
   | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
       Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil)
+  | Eop (Oaddsymbol s ofs) (t1:::Enil), Eop (Oaddimm n) (t2:::Enil) =>
+      addsymbol s (Int.add ofs n) (Eop Oadd (t1:::t2:::Enil))
+  | Eop (Oaddsymbol s ofs) (t1:::Enil), t2 =>
+      addsymbol s ofs (Eop Oadd (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | t1, Eop (Oaddsymbol s ofs) (t2:::Enil) =>
+      addsymbol s ofs (Eop Oadd (t1:::t2:::Enil))
   | _, _ =>
       Eop Oadd (e1:::e2:::Enil)
   end.
@@ -435,7 +451,7 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   match e with
   | Eop (Oaddrsymbol s n) Enil => (Aglobal s n, Enil)
   | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
-  | Eop Oadd (Eop (Oaddrsymbol s n) Enil ::: e2 ::: Enil) => (Abased s n, e2:::Enil)
+  | Eop (Oaddsymbol s n) (e1:::Enil) => (Abased s n, e1:::Enil)
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil)
   | Eop Oadd (e1:::e2:::Enil) =>
      if can_use_Aindexed2 chunk
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index c0601eb..0cfa707 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -152,6 +152,13 @@ Proof.
   TrivialExists. 
 Qed.
 
+Remark symbol_address_shift:
+  forall s ofs n,
+  symbol_address ge s (Int.add ofs n) = Val.add (symbol_address ge s ofs) (Vint n).
+Proof.
+  unfold symbol_address; intros. destruct (Genv.find_symbol ge s); auto. 
+Qed.
+
 Theorem eval_addimm:
   forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
 Proof.
@@ -164,34 +171,50 @@ Proof.
   unfold symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
   rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
+  subst. rewrite Int.add_commut. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut.
 Qed. 
 
+Theorem eval_addsymbol:
+  forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (symbol_address ge s ofs)).
+Proof.
+  red; unfold addsymbol; intros until x.
+  case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl.
+  rewrite symbol_address_shift. auto. 
+  rewrite symbol_address_shift. subst x. rewrite Val.add_assoc. f_equal. f_equal. 
+  apply Val.add_commut.
+Qed.
+
 Theorem eval_add: binary_constructor_sound add Val.add.
 Proof.
   red; intros until y.
   unfold add; case (add_match a b); intros; InvEval.
-  rewrite Val.add_commut. apply eval_addimm; auto.
-  apply eval_addimm; auto.
-  subst. 
+- rewrite Val.add_commut. apply eval_addimm; auto.
+- apply eval_addimm; auto.
+- apply eval_addsymbol; auto.
+- rewrite Val.add_commut. apply eval_addsymbol; auto.
+- subst. 
   replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
      with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_permut.
-  subst. 
+- subst. 
   replace (Val.add (Val.add v1 (Vint n1)) y)
      with (Val.add (Val.add v1 y) (Vint n1)).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_commut.
-  subst. TrivialExists. 
-    econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. 
-    simpl. rewrite (Val.add_commut v1). rewrite <- Val.add_assoc. decEq; decEq. 
-    unfold symbol_address. destruct (Genv.find_symbol ge s); auto.
-  subst. TrivialExists.
-    econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. 
+- subst. TrivialExists. 
+    econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor.
     simpl. repeat rewrite Val.add_assoc. decEq; decEq.
     rewrite Val.add_commut. rewrite Val.add_permut. auto.
-  subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
-  TrivialExists. 
+- replace (Val.add x y) with
+    (Val.add (symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)).
+  apply eval_addsymbol; auto. EvalOp. 
+  subst. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. 
+  rewrite Val.add_permut. f_equal. apply Val.add_commut.
+- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. 
+- subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
+- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp. 
+- TrivialExists. 
 Qed.
 
 Theorem eval_sub: binary_constructor_sound sub Val.sub.
@@ -834,7 +857,7 @@ Proof.
   intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
   exists (@nil val). split. eauto with evalexpr. simpl. auto.
   exists (@nil val). split. eauto with evalexpr. simpl. auto.
-  exists (v0 :: nil). split. eauto with evalexpr. simpl. congruence.
+  exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence.
   exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence.
   destruct (can_use_Aindexed2 chunk). 
   exists (v1 :: v0 :: nil). split. eauto with evalexpr. simpl. congruence.
diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml
index c16cd2f..fabac33 100644
--- a/powerpc/Unusedglob1.ml
+++ b/powerpc/Unusedglob1.ml
@@ -21,6 +21,8 @@ let referenced_constant = function
   | Csymbol_low(s, ofs) -> [s]
   | Csymbol_high(s, ofs) -> [s]
   | Csymbol_sda(s, ofs) -> [s]
+  | Csymbol_rel_low(s, ofs) -> [s]
+  | Csymbol_rel_high(s, ofs) -> [s]
 
 let referenced_builtin ef =
   match ef with
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index bc0184e..352d3b5 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -17,6 +17,7 @@ Extract Constant Asm.low_half => "fun _ -> assert false".
 Extract Constant Asm.high_half => "fun _ -> assert false".
 Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data".
 Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
+Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data".
 
 (* Suppression of stupidly big equality functions *)
 Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
diff --git a/test/regression/pragmas.c b/test/regression/pragmas.c
index bc47dbb..f01820c 100644
--- a/test/regression/pragmas.c
+++ b/test/regression/pragmas.c
@@ -13,6 +13,7 @@ double g(void) { return a + b; }
 #pragma section MYDATA ".mydata_i" ".mydata_u" far-absolute RW
 #pragma section MYCONST ".myconst" ".myconst" far-absolute R
 #pragma section MYSDA ".mysda_i" ".mysda_u" near-data RW
+#pragma section MYRDA ".myrda_i" ".myrda_u" far-data RW
 
 #pragma use_section MYDATA x, y
 int x;
@@ -24,11 +25,15 @@ char z[4] = { 'a', 'b', 'c', 'd' };
 #pragma use_section MYSDA u
 int u;
 
+#pragma use_section MYRDA s
+int s = 42;
+
 #pragma use_section MYCODE f
 int f(int n)
 {
   x += n;
   u -= n;
+  s += n;
   return z[n];
 }