diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-17 14:36:18 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-17 14:36:18 +0000 |
| commit | c29871c2d5c7860c6c6c53e8d5c8a9fe434742d2 (patch) | |
| tree | 9e002b414d3fb3a899deb43f9f6e14d02507121a /powerpc/Asm.v | |
| parent | 26bb5772c75efe1e4617fb9c4f2b8522989fac6d (diff) | |
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
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 10 |
1 files changed, 9 insertions, 1 deletions
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 |