diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-03 08:43:54 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-03 08:43:54 +0000 |
commit | 0486654fac91947fec93d18a0738dd7aa10bcf96 (patch) | |
tree | 4f6b954a2dcc74df25c05bc4c15f0f317aa2d780 /arm | |
parent | e47dcb416c68da4e559d70e633276f7227659740 (diff) | |
download | compcert-kvx-0486654fac91947fec93d18a0738dd7aa10bcf96.tar.gz compcert-kvx-0486654fac91947fec93d18a0738dd7aa10bcf96.zip |
PowerPC/EABI port: preliminary support for #pragma section and
#pragma use_section.
Some clean-ups in Cil2Csyntax.
Separate mach-dep parts of extraction/extraction.v into
<arch>/extractionMachdep.v
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asm.v | 93 | ||||
-rw-r--r-- | arm/SelectOp.v | 3 | ||||
-rw-r--r-- | arm/extractionMachdep.v | 18 | ||||
-rw-r--r-- | arm/linux/CPragmas.ml | 20 |
4 files changed, 59 insertions, 75 deletions
@@ -152,82 +152,38 @@ Inductive instruction : Type := (** The pseudo-instructions are the following: -- [Plabel]: define a code label at the current program point -- [Plfi]: load a floating-point constant in a float register. - Expands to a float load [lfd] from an address in the constant data section - initialized with the floating-point constant: +- [Plabel]: define a code label at the current program point. +- [Ploadsymbol]: load the address of a symbol in an integer register. + Expands to a load from an address in the constant data section + initialized with the symbol value: << - addis r2, 0, ha16(lbl) - lfd rdst, lo16(lbl)(r2) + ldr rdst, lbl .const_data -lbl: .double floatcst +lbl: .word symbol .text >> Initialized data in the constant data section are not modeled here, which is why we use a pseudo-instruction for this purpose. -- [Pfcti]: convert a float to an integer. This requires a transfer - via memory of a 32-bit integer from a float register to an int register, - which our memory model cannot express. Expands to: -<< - fctiwz f13, rsrc - stfdu f13, -8(r1) - lwz rdst, 4(r1) - addi r1, r1, 8 ->> -- [Pictf]: convert a signed integer to a float. This requires complicated - bit-level manipulations of IEEE floats through mixed float and integer - arithmetic over a memory word, which our memory model and axiomatization - of floats cannot express. Expands to: -<< - addis r2, 0, 0x4330 - stwu r2, -8(r1) - addis r2, rsrc, 0x8000 - stw r2, 4(r1) - addis r2, 0, ha16(lbl) - lfd f13, lo16(lbl)(r2) - lfd rdst, 0(r1) - addi r1, r1, 8 - fsub rdst, rdst, f13 - .const_data -lbl: .long 0x43300000, 0x80000000 - .text ->> - (Don't worry if you do not understand this instruction sequence: intimate - knowledge of IEEE float arithmetic is necessary.) -- [Piuctf]: convert an unsigned integer to a float. The expansion is close - to that [Pictf], and equally obscure. -<< - addis r2, 0, 0x4330 - stwu r2, -8(r1) - stw rsrc, 4(r1) - addis r2, 0, ha16(lbl) - lfd f13, lo16(lbl)(r2) - lfd rdst, 0(r1) - addi r1, r1, 8 - fsub rdst, rdst, f13 - .const_data -lbl: .long 0x43300000, 0x00000000 - .text ->> -- [Pallocframe lo hi]: in the formal semantics, this pseudo-instruction +- [Pallocframe lo hi pos]: in the formal semantics, this pseudo-instruction allocates a memory block with bounds [lo] and [hi], stores the value - of register [r1] (the stack pointer, by convention) at the bottom - of this block, and sets [r1] to a pointer to the bottom of this - block. In the printed PowerPC assembly code, this allocation - is just a store-decrement of register [r1]: + of the stack pointer at offset [pos] in this block, and sets the + stack pointer to the address of the bottom of this block. + In the printed ASM assembly code, this allocation is: << - stwu r1, (lo - hi)(r1) + mov r12, sp + sub sp, sp, #(hi - lo) + str r12, [sp, #pos] >> This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline. -- [Pfreeframe]: in the formal semantics, this pseudo-instruction - reads the bottom word of the block pointed by [r1] (the stack pointer), - frees this block, and sets [r1] to the value of the bottom word. - In the printed PowerPC assembly code, this freeing - is just a load of register [r1] relative to [r1] itself: +- [Pfreeframe pos]: in the formal semantics, this pseudo-instruction + reads the word at [pos] of the block pointed by the stack pointer, + frees this block, and sets the stack pointer to the value read. + In the printed ASM assembly code, this freeing + is just a load of register [sp] relative to [sp] itself: << - lwz r1, 0(r1) + ldr sp, [sp, #pos] >> Again, our memory model cannot comprehend that this operation frees (logically) the current stack frame. @@ -239,8 +195,7 @@ Definition program := AST.program fundef unit. (** * Operational semantics *) -(** The PowerPC has a great many registers, some general-purpose, some very - specific. We model only the following registers: *) +(** We model the following registers of the ARM architecture. *) Inductive preg: Type := | IR: ireg -> preg (**r integer registers *) @@ -591,7 +546,7 @@ Definition preg_of (r: mreg) := (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that - we use PPC registers instead of locations. *) + we use ARM registers instead of locations. *) Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := | extcall_arg_reg: forall r, @@ -665,9 +620,3 @@ Inductive final_state: state -> int -> Prop := Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. - - -(** For compatibility with PowerPC *) - -Parameter low_half: val -> val. -Parameter high_half: val -> val. diff --git a/arm/SelectOp.v b/arm/SelectOp.v index 49676f83..4b5fde7f 100644 --- a/arm/SelectOp.v +++ b/arm/SelectOp.v @@ -1193,7 +1193,4 @@ Definition addressing (chunk: memory_chunk) (e: expr) := (Aindexed Int.zero, e:::Enil) end. -(** For compatibility with PowerPC, but unused. *) - -Parameter use_fused_mul : unit -> bool. diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v new file mode 100644 index 00000000..f6e17bab --- /dev/null +++ b/arm/extractionMachdep.v @@ -0,0 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Additional extraction directives specific to the ARM port *) + +(* Suppression of stupidly big equality functions *) +Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". +Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y". +Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". diff --git a/arm/linux/CPragmas.ml b/arm/linux/CPragmas.ml new file mode 100644 index 00000000..1602f9f1 --- /dev/null +++ b/arm/linux/CPragmas.ml @@ -0,0 +1,20 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Platform-dependent handling of pragmas *) + +(* No pragmas supported on ARM/Linux *) + +let initialize () = () |