powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.

powerpc/Asmgen*: simplify the code generated for far-data relative
  accesses, so that the only occurrences of Csymbol_rel_{low,high}
  are in the pattern
    Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...)
checklink/Check.ml: check the pattern above.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7 files changed, 139 insertions, 124 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 7eb3ea3..cc53f4e 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -415,13 +415,12 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw ->
       end
   | Csymbol_sda (ident, i) ->
       (* sda should be handled separately in places it occurs *)
-      fatal "Unhandled Csymbol_sda, please report."
+      ERR("Incorrect reference to near-data symbol "
+                ^ Hashtbl.find ffw.sf.ident_to_name ident)
   | 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)
+      (* should be handled separately in places it occurs *)
+      ERR("Incorrect reference to far-data symbol " 
+                ^ Hashtbl.find ffw.sf.ident_to_name ident)
 
 let match_z_int32 (cz: Z.t) (ei: int32) =
   let cz = z_int32 cz in
@@ -738,6 +737,23 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Paddis(rd, r1, Csymbol_rel_high(id, ofs)) ->
+          begin match cs with
+          | Paddi(rd', r1', Csymbol_rel_low(id', ofs')) :: cs
+            when id' = id && ofs' = ofs ->
+              begin match ecode with
+              | ADDIS(rD, rA, simm) :: ADDI(rD', rA', simm') :: es ->
+                  OK(fw)
+                  >>= match_iregs rd  rD
+                  >>= match_iregs r1' rA'
+                  >>= match_iregs rd' rD'
+                  >>= check_sda id ofs rA
+                        Int32.(add (shift_left (of_int simm) 16) (exts simm'))
+                  >>= compare_code cs es (Int32.add 8l pc)
+              | _ -> error
+              end
+          | _ -> error
+          end
       | Paddis(rd, r1, cst) ->
           begin match ecode with
           | ADDIS(rD, rA, simm) :: es ->
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index ab52ca5..fc8c2d9 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -429,8 +429,8 @@ Variable ge: genv.
   symbolic references [symbol + offset] and splits their
   actual values into two 16-bit halves. *)
 
-Parameter low_half: val -> val.
-Parameter high_half: val -> val.
+Parameter low_half: genv -> ident -> int -> val.
+Parameter high_half: genv -> ident -> int -> val.
 
 (** The fundamental property of these operations is that, when applied
   to the address of a symbol, their results can be recombined by
@@ -438,18 +438,8 @@ Parameter high_half: val -> val.
 
 Axiom low_high_half:
   forall id ofs,
-  Val.add (low_half (Genv.symbol_address ge id ofs)) (high_half (Genv.symbol_address ge id ofs))
-  = Genv.symbol_address ge id ofs.
-
-(** The other axioms we take is that the results of
-  the [low_half] and [high_half] functions are of type [Tint],
-  i.e. either integers, pointers or undefined values. *)
-
-Axiom low_half_type: 
-  forall v, Val.has_type (low_half v) Tint.
-Axiom high_half_type: 
-  forall v, Val.has_type (high_half v) Tint.
- 
+  Val.add (high_half ge id ofs) (low_half ge id ofs) = Genv.symbol_address ge id ofs.
+
 (** We also axiomatize the small data area.  For simplicity, we
   claim that small data symbols can be accessed by absolute 16-bit
   offsets, that is, relative to [GPR0].  In reality, the linker
@@ -479,10 +469,10 @@ Parameter symbol_is_rel_data: ident -> int -> bool.
 Definition const_low (c: constant) :=
   match c with
   | Cint n => Vint n
-  | Csymbol_low id ofs => low_half (Genv.symbol_address ge id ofs)
+  | Csymbol_low id ofs => low_half ge 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 (Genv.symbol_address ge id ofs)
+  | Csymbol_rel_low id ofs => low_half ge id ofs
   | Csymbol_rel_high id ofs => Vundef
   end.
 
@@ -490,10 +480,10 @@ Definition const_high (c: constant) :=
   match c with
   | Cint n => Vint (Int.shl n (Int.repr 16))
   | Csymbol_low id ofs => Vundef
-  | Csymbol_high id ofs => high_half (Genv.symbol_address ge id ofs)
+  | Csymbol_high id ofs => high_half ge id ofs
   | Csymbol_sda id ofs => Vundef
   | Csymbol_rel_low id ofs => Vundef
-  | Csymbol_rel_high id ofs => high_half (Genv.symbol_address ge id ofs)
+  | Csymbol_rel_high id ofs => high_half ge id ofs
   end.
 
 (** The semantics is purely small-step and defined as a function
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 07cc50b..bec4daa 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -212,6 +212,11 @@ let expand_builtin_vload_sda chunk id ofs args res =
       assert false
   end
 
+let expand_builtin_vload_rel chunk id ofs args res =
+  emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs)));
+  emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs)));
+  expand_builtin_vload chunk [IR GPR11] res
+
 let expand_builtin_vstore_common chunk base offset src =
   match chunk, src with
   | (Mint8signed | Mint8unsigned), IR src ->
@@ -264,11 +269,20 @@ let expand_builtin_vstore_sda chunk id ofs args =
       expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src
   | [IR src1; IR src2] when chunk = Mint64 ->
       emit (Pstw(src1, Csymbol_sda(id, ofs), GPR0));
+      let ofs = Int.add ofs _4 in
       emit (Pstw(src2, Csymbol_sda(id, ofs), GPR0))
   | _ ->
       assert false
   end
 
+let expand_builtin_vstore_rel chunk id ofs args =
+  let tmp =
+    if not (List.mem (IR GPR12) args) then GPR12 else
+    if not (List.mem (IR GPR11) args) then GPR11 else GPR10 in
+  emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs)));
+  emit (Paddi(tmp, tmp, Csymbol_rel_low(id, ofs)));
+  expand_builtin_vstore chunk (IR tmp :: args)
+
 (* Handling of varargs *)
 
 let current_function_stacksize = ref 0l
@@ -492,13 +506,19 @@ let expand_instruction instr =
       | EF_vstore chunk ->
           expand_builtin_vstore chunk args
       | EF_vload_global(chunk, id, ofs) ->
-          if symbol_is_small_data id ofs
-          then expand_builtin_vload_sda chunk id ofs args res
-          else expand_builtin_vload_global chunk id ofs args res
+          if symbol_is_small_data id ofs then
+             expand_builtin_vload_sda chunk id ofs args res
+          else if symbol_is_rel_data id ofs then
+             expand_builtin_vload_rel chunk id ofs args res
+          else
+             expand_builtin_vload_global chunk id ofs args res
       | EF_vstore_global(chunk, id, ofs) ->
-          if symbol_is_small_data id ofs
-          then expand_builtin_vstore_sda chunk id ofs args
-          else expand_builtin_vstore_global chunk id ofs args
+          if symbol_is_small_data id ofs then
+            expand_builtin_vstore_sda chunk id ofs args
+          else if symbol_is_rel_data id ofs then
+            expand_builtin_vstore_rel chunk id ofs args
+          else
+            expand_builtin_vstore_global chunk id ofs args
       | EF_memcpy(sz, al) ->
           expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
       | EF_annot_val(txt, targ) ->
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 5c4ffde..2bd69d9 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -314,11 +314,6 @@ 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
@@ -338,10 +333,12 @@ Definition transl_op
       do r <- ireg_of res;
       OK (if symbol_is_small_data s ofs then
            Paddi r GPR0 (Csymbol_sda s ofs) :: k
+         else if symbol_is_rel_data s ofs then
+           Paddis r GPR0 (Csymbol_rel_high s ofs) ::
+           Paddi r r (Csymbol_rel_low s ofs) :: k
          else
-           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)
+           Paddis r GPR0 (Csymbol_high s ofs) ::
+           Paddi r r (Csymbol_low s ofs) :: k)
   | Oaddrstack n, nil =>
       do r <- ireg_of res; OK (addimm r GPR1 n k)
   | Ocast8signed, a1 :: nil =>
@@ -359,9 +356,10 @@ Definition transl_op
              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
+             Pmr GPR0 r1 ::
+             Paddis r GPR0 (Csymbol_rel_high s ofs) ::
+             Paddi r r (Csymbol_rel_low s ofs) ::
+             Padd r r GPR0 :: k
            else
              Paddis r r1 (Csymbol_high s ofs) ::
              Paddi r r (Csymbol_low s ofs) :: k)
@@ -531,19 +529,23 @@ Definition transl_memory_access
   | Aglobal symb ofs, nil =>
       OK (if symbol_is_small_data symb ofs then
            mk1 (Csymbol_sda symb ofs) GPR0 :: k
+         else if symbol_is_rel_data symb ofs then
+           Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
+           Paddi temp temp (Csymbol_rel_low symb ofs) ::
+           mk1 (Cint Int.zero) temp :: k
          else
-           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)
+           Paddis temp GPR0 (Csymbol_high symb ofs) ::
+           mk1 (Csymbol_low symb ofs) temp :: k)
   | Abased symb ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
       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
+            Pmr GPR0 r1 ::
+            Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
+            Paddi temp temp (Csymbol_rel_low symb ofs) ::
+            mk2 temp GPR0 :: k
           else
             Paddis temp r1 (Csymbol_high symb ofs) ::
             mk1 (Csymbol_low symb ofs) temp :: k)
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 2b52fe0..9adf44d 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -246,9 +246,8 @@ Proof.
 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 (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_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.
@@ -264,9 +263,8 @@ Remark transl_memory_access_label:
 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 (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_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 e1ab9a1..cb94c55 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -31,17 +31,6 @@ Require Import Asmgenproof0.
 
 (** * Properties of low half/high half decomposition *)
 
-Lemma high_half_zero:
-  forall v, Val.add (high_half v) Vzero = high_half v.
-Proof.
-  intros. generalize (high_half_type v).
-  rewrite Val.add_commut. 
-  case (high_half v); simpl; intros; try contradiction.
-  auto. 
-  rewrite Int.add_commut; rewrite Int.add_zero; auto. 
-  rewrite Int.add_zero; auto. 
-Qed.
-
 Lemma low_high_u:
   forall n, Int.or (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n.
 Proof.
@@ -111,20 +100,12 @@ Proof.
   simpl. rewrite Int.add_zero; auto.
 Qed.
 
-Lemma csymbol_high_low:
+Lemma low_high_half_zero:
   forall (ge: genv) id ofs,
-  Val.add (high_half (Genv.symbol_address ge id ofs)) (low_half (Genv.symbol_address ge id ofs))
-  = Genv.symbol_address ge id ofs.
+  Val.add (Val.add Vzero (high_half ge id ofs)) (low_half ge id ofs) =
+  Genv.symbol_address ge id ofs.
 Proof.
-  intros. rewrite Val.add_commut. apply low_high_half.
-Qed.
-
-Lemma csymbol_high_low_2:
-  forall (ge: genv) id ofs rel,
-  Val.add (const_high ge (csymbol_high id ofs rel))
-          (const_low ge (csymbol_low id ofs rel)) = Genv.symbol_address ge id ofs.
-Proof.
-  intros. destruct rel; apply csymbol_high_low. 
+  intros. rewrite Val.add_assoc. rewrite low_high_half. apply add_zero_symbol_address.
 Qed.
 
 (** Useful properties of the GPR0 registers. *)
@@ -863,16 +844,21 @@ Opaque Int.eq.
   exists rs'. auto with asmgen. 
   (* Oaddrsymbol *)
   set (v' := Genv.symbol_address ge i i0).
-  destruct (symbol_is_small_data i i0) eqn:SD.
+  destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ].
   (* small data *)
 Opaque Val.add.
   econstructor; split. apply exec_straight_one; simpl; reflexivity.
   split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address.
   intros; Simpl.
-  (* not small data *)
+  (* relative data *)
+  econstructor; split. eapply exec_straight_two; simpl; reflexivity.
+  split. Simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. Simpl.
+  apply low_high_half_zero. 
+  intros; Simpl.
+  (* absolute data *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
   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_address. 
+  apply low_high_half_zero.
   intros; Simpl. 
   (* Oaddrstack *)
   destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen.
@@ -881,24 +867,24 @@ Opaque Val.add.
   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.
+  destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ].
   (* 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_address.
   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_address.
-  intros; Simpl.
+  econstructor; split. eapply exec_straight_trans. 
+  eapply exec_straight_two; simpl; reflexivity.
+  eapply exec_straight_two; simpl; reflexivity.
+  split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen).
+  Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl.
+  rewrite low_high_half_zero. auto.
+  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.
+  rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). rewrite low_high_half. auto.
   intros; Simpl.
   (* Osubimm *)
   case (Int.eq (high_s i) Int.zero).
@@ -1022,27 +1008,35 @@ Transparent Val.add.
   (* Aindexed2 *)
   apply MK2; auto.
   (* Aglobal *)
-  destruct (symbol_is_small_data i i0) eqn:SISD; inv TR.
+  destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
   (* Aglobal from small data *)
   apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. 
   apply add_zero_symbol_address.
   auto.
-  (* Aglobal general case *)
-  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. apply csymbol_high_low_2.
-    intros; unfold rs1; Simpl.
+  (* Aglobal from relative data *)
+  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+  set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
+  exploit (MK1 (Cint Int.zero) temp rs2).
+    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. 
+    unfold rs2. Simpl. rewrite Val.add_commut. apply add_zero_symbol_address.
+    intros; unfold rs2, 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, csymbol_high. 
-  destruct rel; rewrite high_half_zero; reflexivity.
-  reflexivity.
-  assumption. assumption.
+  exists rs'; split. apply exec_straight_step with rs1 m; auto. 
+  apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. 
+  rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
+  unfold rs1; Simpl. apply low_high_half_zero.
+  eexact EX'. auto.
+  (* Aglobal from absolute data *)
+  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+  exploit (MK1 (Csymbol_low i i0) temp rs1).
+    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. 
+    unfold rs1. Simpl. apply low_high_half_zero. 
+    intros; unfold rs1; Simpl. 
+  intros [rs' [EX' AG']].
+  exists rs'; split. apply exec_straight_step with rs1 m; auto. 
+  eexact EX'. auto.
   (* Abased *)
-  destruct (symbol_is_small_data i i0) eqn:SISD.
+  destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ].
   (* Abased from small data *)
   set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
   exploit (MK2 x GPR0 rs1 k).
@@ -1055,30 +1049,25 @@ Transparent Val.add.
   apply add_zero_symbol_address.
   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.
+  (* Abased from relative data *)
+  set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
+  set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
+  set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
+  exploit (MK2 temp GPR0 rs3).
+    f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. 
+    intros. unfold rs3, rs2, 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.
+  exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). 
+  apply exec_straight_three with rs1 m rs2 m; auto. 
+  simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. 
+  unfold rs2; Simpl. apply low_high_half_zero. 
+  eexact EX'. auto. 
   (* Abased absolute *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (const_high ge (Csymbol_high i i0))))).
+  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge 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. simpl. rewrite csymbol_high_low. apply Val.add_commut. 
+    rewrite Val.add_assoc. rewrite low_high_half. apply Val.add_commut. 
     intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index 352d3b5..b448e3d 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -13,8 +13,8 @@
 (* Additional extraction directives specific to the PowerPC port *)
 
 (* Asm *)
-Extract Constant Asm.low_half => "fun _ -> assert false".
-Extract Constant Asm.high_half => "fun _ -> assert false".
+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".