Revert "Removed unused parameter from is_small/rel_data."

This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.

5 files changed, 25 insertions, 23 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 81f81040..a9b60fbd 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -477,15 +477,15 @@ Axiom low_high_half:
   register pointing to the base of the small data area containing
   symbol [symb].  We leave this transformation up to the linker. *)
 
-Parameter symbol_is_small_data: ident -> bool.
+Parameter symbol_is_small_data: ident -> int -> bool.
 Parameter small_data_area_offset: genv -> ident -> int -> val.
 
 Axiom small_data_area_addressing:
   forall id ofs,
-  symbol_is_small_data id = true ->
+  symbol_is_small_data id ofs = true ->
   small_data_area_offset ge id ofs = Genv.symbol_address ge id ofs.
 
-Parameter symbol_is_rel_data: ident -> bool.
+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.
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 917d4466..a6795030 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -211,9 +211,9 @@ let expand_builtin_vload chunk args res =
         expand_builtin_vload_common chunk GPR11 (Cint _0) res
       end
   | [BA_addrglobal(id, ofs)] ->
-      if symbol_is_small_data id then
+      if symbol_is_small_data id ofs then
         expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res
-      else if symbol_is_rel_data id then begin
+      else if symbol_is_rel_data id ofs then begin
         emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs)));
         expand_builtin_vload_common chunk GPR11 (Csymbol_rel_low(id, ofs)) res
       end else begin
@@ -268,9 +268,9 @@ let expand_builtin_vstore chunk args =
         expand_builtin_vstore_common chunk tmp (Cint _0) src
       end
   | [BA_addrglobal(id, ofs); src] ->
-      if symbol_is_small_data id then
+      if symbol_is_small_data id ofs then
         expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src
-      else if symbol_is_rel_data id then begin
+      else if symbol_is_rel_data id ofs then begin
         let tmp = temp_for_vstore src in
         emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs)));
         expand_builtin_vstore_common chunk tmp (Csymbol_rel_low(id, ofs)) src
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index f961ad73..4ad5e2f9 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -331,9 +331,9 @@ Definition transl_op
       do r <- freg_of res; OK (Plfis r f :: k)
   | Oaddrsymbol s ofs, nil =>
       do r <- ireg_of res;
-      OK (if symbol_is_small_data s then
+      OK (if symbol_is_small_data s ofs then
            Paddi r GPR0 (Csymbol_sda s ofs) :: k
-         else if symbol_is_rel_data s then
+         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
@@ -352,10 +352,10 @@ Definition transl_op
        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 then
+       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 then
+           else if symbol_is_rel_data s ofs then
              Pmr GPR0 r1 ::
              Paddis r GPR0 (Csymbol_rel_high s ofs) ::
              Paddi r r (Csymbol_rel_low s ofs) ::
@@ -536,9 +536,9 @@ Definition transl_memory_access
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (mk2 r1 r2 :: k)
   | Aglobal symb ofs, nil =>
-      OK (if symbol_is_small_data symb then
+      OK (if symbol_is_small_data symb ofs then
            mk1 (Csymbol_sda symb ofs) GPR0 :: k
-         else if symbol_is_rel_data symb then
+         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
@@ -547,10 +547,10 @@ Definition transl_memory_access
            mk1 (Csymbol_low symb ofs) temp :: k)
   | Abased symb ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (if symbol_is_small_data symb then
+      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 then
+          else if symbol_is_rel_data symb ofs then
             Pmr GPR0 r1 ::
             Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
             Paddi temp temp (Csymbol_rel_low symb ofs) ::
@@ -736,3 +736,4 @@ Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
 
 Definition transf_program (p: Mach.program) : res Asm.program :=
   transform_partial_program transf_fundef p.
+
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 47b69d6a..4e59b297 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -254,8 +254,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). TailNoLabel. destruct (symbol_is_rel_data i); TailNoLabel.
-  destruct (symbol_is_small_data i). TailNoLabel. destruct (symbol_is_rel_data i); 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.
@@ -271,8 +271,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). TailNoLabel. destruct (symbol_is_rel_data i); TailNoLabel.
-  destruct (symbol_is_small_data i). TailNoLabel. destruct (symbol_is_rel_data i); 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 70698736..aa2645f3 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -844,7 +844,7 @@ Opaque Int.eq.
   exists rs'. auto with asmgen.
   (* Oaddrsymbol *)
   set (v' := Genv.symbol_address ge i i0).
-  destruct (symbol_is_small_data i) eqn:SD; [ | destruct (symbol_is_rel_data i) ].
+  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.
@@ -867,7 +867,7 @@ 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) eqn:SD; [ | destruct (symbol_is_rel_data i) ].
+  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.
@@ -1020,7 +1020,7 @@ Transparent Val.add.
   (* Aindexed2 *)
   apply MK2; auto.
   (* Aglobal *)
-  destruct (symbol_is_small_data i) eqn:SISD; [ | destruct (symbol_is_rel_data i) ]; 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.
@@ -1048,7 +1048,7 @@ Transparent Val.add.
   exists rs'; split. apply exec_straight_step with rs1 m; auto.
   eexact EX'. auto.
   (* Abased *)
-  destruct (symbol_is_small_data i) eqn:SISD; [ | destruct (symbol_is_rel_data i) ].
+  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).
@@ -1232,3 +1232,4 @@ Local Transparent destroyed_by_store.
 Qed.
 
 End CONSTRUCTORS.
+