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

1 files changed, 8 insertions, 18 deletions

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