From 71a8a9586078c0132aa326a8c7968d38fe25a78d Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 18 Aug 2014 12:34:43 +0000 Subject: 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 --- powerpc/Asm.v | 26 ++++++++------------------ 1 file changed, 8 insertions(+), 18 deletions(-) (limited to 'powerpc/Asm.v') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index ab52ca52..fc8c2d9b 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 -- cgit