diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-01 16:51:47 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-01 16:51:47 +0000 |
commit | 3ccc93675292bf9a44ac0d7111d3f44981e1f56d (patch) | |
tree | 2879f37d1625e035f21134bc2307fce427531ce4 /powerpc/Asm.v | |
parent | 033aa0555a209fa3e825b1eeb8a5fc00ff8163e3 (diff) | |
download | compcert-3ccc93675292bf9a44ac0d7111d3f44981e1f56d.tar.gz compcert-3ccc93675292bf9a44ac0d7111d3f44981e1f56d.zip |
Preliminary support for small data area in PowerPC port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asm.v')
-rw-r--r-- | powerpc/Asm.v | 26 |
1 files changed, 22 insertions, 4 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index ab70072b..bea5f5c0 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -57,16 +57,18 @@ Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. Proof. decide equality. Defined. (** Symbolic constants. Immediate operands to an arithmetic instruction - or an indexed memory access can be either integer literals + or an indexed memory access can be either integer literals, or the low or high 16 bits of a symbolic reference (the address - of a symbol plus a displacement). These symbolic references are + of a symbol plus a displacement), or a 16-bit offset from the + small data area register. These symbolic references are resolved later by the linker. *) Inductive constant: Type := | Cint: int -> constant | Csymbol_low: ident -> int -> constant - | Csymbol_high: ident -> int -> constant. + | Csymbol_high: ident -> int -> constant + | Csymbol_sda: ident -> int -> constant. (** A note on constants: while immediate operands to PowerPC instructions must be representable in 16 bits (with @@ -413,6 +415,19 @@ Axiom low_half_type: Axiom high_half_type: forall v, Val.has_type (high_half v) Tint. +(** The function below axiomatizes how the linker builds the + small data area. *) + +Parameter symbol_is_small_data: ident -> int -> bool. +Parameter small_data_area_base: genv -> val. +Parameter small_data_area_offset: genv -> ident -> int -> val. + +Axiom small_data_area_addressing: + forall id ofs, + symbol_is_small_data id ofs = true -> + Val.add (small_data_area_base ge) (small_data_area_offset ge id ofs) = + symbol_offset id ofs. + (** 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 @@ -426,6 +441,7 @@ Definition const_low (c: constant) := | Cint n => Vint n | 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 end. Definition const_high (c: constant) := @@ -433,6 +449,7 @@ Definition const_high (c: constant) := | Cint n => Vint (Int.shl n (Int.repr 16)) | Csymbol_low id ofs => Vundef | Csymbol_high id ofs => high_half (symbol_offset id ofs) + | Csymbol_sda id ofs => Vundef end. (** The semantics is purely small-step and defined as a function @@ -852,7 +869,8 @@ Inductive initial_state (p: program): state -> Prop := (Pregmap.init Vundef) # PC <- (symbol_offset ge p.(prog_main) Int.zero) # LR <- Vzero - # GPR1 <- (Vptr Mem.nullptr Int.zero) in + # GPR1 <- (Vptr Mem.nullptr Int.zero) + # GPR13 <- (small_data_area_base ge) in initial_state p (State rs0 m0). Inductive final_state: state -> int -> Prop := |