diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-01 12:47:42 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-01 12:47:42 +0000 |
commit | 2245717b5800da80371952999bc0cff5f75aa490 (patch) | |
tree | 607052bd5604bdd13e33530bcfa0f6f9e4b25e70 /arm | |
parent | 58fca75f4ab089d21fc4f4a5bdac71d4b79f899f (diff) | |
download | compcert-2245717b5800da80371952999bc0cff5f75aa490.tar.gz compcert-2245717b5800da80371952999bc0cff5f75aa490.zip |
Continuation of ARM port.
Cleaned up Makefile and SVN properties.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asm.v | 687 | ||||
-rw-r--r-- | arm/Asmgen.v | 29 | ||||
-rw-r--r-- | arm/PrintAsm.ml | 507 | ||||
-rw-r--r-- | arm/PrintAsm.mli | 13 | ||||
-rw-r--r-- | arm/Selection.v | 3 |
5 files changed, 1209 insertions, 30 deletions
diff --git a/arm/Asm.v b/arm/Asm.v new file mode 100644 index 00000000..72534c0b --- /dev/null +++ b/arm/Asm.v @@ -0,0 +1,687 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Abstract syntax and semantics for ARM assembly language *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Locations. +Require Stacklayout. +Require Conventions. + +(** * Abstract syntax *) + +(** Integer registers, floating-point registers. *) + +Inductive ireg: Set := + | IR0: ireg | IR1: ireg | IR2: ireg | IR3: ireg + | IR4: ireg | IR5: ireg | IR6: ireg | IR7: ireg + | IR8: ireg | IR9: ireg | IR10: ireg | IR11: ireg + | IR12: ireg | IR13: ireg | IR14: ireg. + +Inductive freg: Set := + | FR0: freg | FR1: freg | FR2: freg | FR3: freg + | FR4: freg | FR5: freg | FR6: freg | FR7: freg. + +Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +(** Bits in the condition register. *) + +Inductive crbit: Set := + | CReq: crbit (**r equal *) + | CRne: crbit (**r not equal *) + | CRhs: crbit (**r unsigned higher or same *) + | CRlo: crbit (**r unsigned lower *) + | CRmi: crbit (**r negative *) + | CRpl: crbit (**r positive *) + | CRhi: crbit (**r unsigned higher *) + | CRls: crbit (**r unsigned lower or same *) + | CRge: crbit (**r signed greater or equal *) + | CRlt: crbit (**r signed less than *) + | CRgt: crbit (**r signed greater *) + | CRle: crbit. (**r signed less than or equal *) + +Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +(** The instruction set. Most instructions correspond exactly to + actual instructions of the PowerPC processor. See the PowerPC + reference manuals for more details. Some instructions, + described below, are pseudo-instructions: they expand to + canned instruction sequences during the printing of the assembly + code. *) + +Definition label := positive. + +Inductive shift_op : Set := + | SOimm: int -> shift_op + | SOreg: ireg -> shift_op + | SOlslimm: ireg -> int -> shift_op + | SOlslreg: ireg -> ireg -> shift_op + | SOlsrimm: ireg -> int -> shift_op + | SOlsrreg: ireg -> ireg -> shift_op + | SOasrimm: ireg -> int -> shift_op + | SOasrreg: ireg -> ireg -> shift_op + | SOrorimm: ireg -> int -> shift_op + | SOrorreg: ireg -> ireg -> shift_op. + +Inductive shift_addr : Set := + | SAimm: int -> shift_addr + | SAreg: ireg -> shift_addr + | SAlsl: ireg -> int -> shift_addr + | SAlsr: ireg -> int -> shift_addr + | SAasr: ireg -> int -> shift_addr + | SAror: ireg -> int -> shift_addr. + +Inductive instruction : Set := + (* Core instructions *) + | Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *) + | Pand: ireg -> ireg -> shift_op -> instruction (**r bitwise and *) + | Pb: label -> instruction (**r branch to label *) + | Pbc: crbit -> label -> instruction (**r conditional branch to label *) + | Pbsymb: ident -> instruction (**r branch to symbol *) + | Pbreg: ireg -> instruction (**r computed branch *) + | Pblsymb: ident -> instruction (**r branch and link to symbol *) + | Pblreg: ireg -> instruction (**r computed branch and link *) + | Pbic: ireg -> ireg -> shift_op -> instruction (**r bitwise bit-clear *) + | Pcmp: ireg -> shift_op -> instruction (**r integer comparison *) + | Peor: ireg -> ireg -> shift_op -> instruction (**r bitwise exclusive or *) + | Pldr: ireg -> ireg -> shift_addr -> instruction (**r int32 load *) + | Pldrb: ireg -> ireg -> shift_addr -> instruction (**r unsigned int8 load *) + | Pldrh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *) + | Pldrsb: ireg -> ireg -> shift_addr -> instruction (**r signed int8 load *) + | Pldrsh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *) + | Pmov: ireg -> shift_op -> instruction (**r integer move *) + | Pmovc: crbit -> ireg -> shift_op -> instruction (**r integer conditional move *) + | Pmul: ireg -> ireg -> ireg -> instruction (**r integer multiplication *) + | Pmvn: ireg -> shift_op -> instruction (**r integer complement *) + | Porr: ireg -> ireg -> shift_op -> instruction (**r bitwise or *) + | Prsb: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction *) + | Pstr: ireg -> ireg -> shift_addr -> instruction (**r int32 store *) + | Pstrb: ireg -> ireg -> shift_addr -> instruction (**r int8 store *) + | Pstrh: ireg -> ireg -> shift_addr -> instruction (**r int16 store *) + | Psdiv: ireg -> ireg -> ireg -> instruction (**r signed division *) + | Psub: ireg -> ireg -> shift_op -> instruction (**r integer subtraction *) + | Pudiv: ireg -> ireg -> ireg -> instruction (**r unsigned division *) + (* Floating-point coprocessor instructions *) + | Pabsd: freg -> freg -> instruction (**r float absolute value *) + | Padfd: freg -> freg -> freg -> instruction (**r float addition *) + | Pcmf: freg -> freg -> instruction (**r float comparison *) + | Pdvfd: freg -> freg -> freg -> instruction (**r float division *) + | Pfixz: ireg -> freg -> instruction (**r float to signed int *) + | Pfixzu: ireg -> freg -> instruction (**r float to unsigned int *) + | Pfltd: freg -> ireg -> instruction (**r signed int to float *) + | Pfltud: freg -> ireg -> instruction (**r unsigned int to float *) + | Pldfd: freg -> ireg -> int -> instruction (**r float64 load *) + | Pldfs: freg -> ireg -> int -> instruction (**r float32 load *) + | Plifd: freg -> float -> instruction (**r load float constant *) + | Pmnfd: freg -> freg -> instruction (**r float opposite *) + | Pmvfd: freg -> freg -> instruction (**r float move *) + | Pmvfs: freg -> freg -> instruction (**r float move single precision *) + | Pmufd: freg -> freg -> freg -> instruction (**r float multiplication *) + | Pstfd: freg -> ireg -> int -> instruction (**r float64 store *) + | Pstfs: freg -> ireg -> int -> instruction (**r float32 store *) + | Psufd: freg -> freg -> freg -> instruction (**r float subtraction *) + + (* Pseudo-instructions *) + | Pallocblock: instruction (**r dynamic allocation *) + | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) + | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *) + | Plabel: label -> instruction (**r define a code label *) + | Ploadsymbol: ireg -> ident -> int -> instruction. (**r load the address of a symbol *) + +(** 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: +<< + addis r2, 0, ha16(lbl) + lfd rdst, lo16(lbl)(r2) + .const_data +lbl: .double floatcst + .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 + 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]: +<< + stwu r1, (lo - hi)(r1) +>> + 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: +<< + lwz r1, 0(r1) +>> + Again, our memory model cannot comprehend that this operation + frees (logically) the current stack frame. +- [Pallocheap]: in the formal semantics, this pseudo-instruction + allocates a heap block of size the contents of [GPR3], and leaves + a pointer to this block in [GPR3]. In the generated assembly code, + it is turned into a call to the allocation function of the run-time + system. +*) + +Definition code := list instruction. +Definition fundef := AST.fundef code. +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: *) + +Inductive preg: Set := + | IR: ireg -> preg (**r integer registers *) + | FR: freg -> preg (**r float registers *) + | CR: crbit -> preg (**r bits in the condition register *) + | PC: preg. (**r program counter *) + +Coercion IR: ireg >-> preg. +Coercion FR: freg >-> preg. +Coercion CR: crbit >-> preg. + +Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. +Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined. + +Module PregEq. + Definition t := preg. + Definition eq := preg_eq. +End PregEq. + +Module Pregmap := EMap(PregEq). + +(** The semantics operates over a single mapping from registers + (type [preg]) to values. We maintain (but do not enforce) + the convention that integer registers are mapped to values of + type [Tint], float registers to values of type [Tfloat], + and condition bits to either [Vzero] or [Vone]. *) + +Definition regset := Pregmap.t val. +Definition genv := Genv.t fundef. + +Notation "a # b" := (a b) (at level 1, only parsing). +Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level). + +Section RELSEM. + +(** Looking up instructions in a code sequence by position. *) + +Fixpoint find_instr (pos: Z) (c: code) {struct c} : option instruction := + match c with + | nil => None + | i :: il => if zeq pos 0 then Some i else find_instr (pos - 1) il + end. + +(** Position corresponding to a label *) + +Definition is_label (lbl: label) (instr: instruction) : bool := + match instr with + | Plabel lbl' => if peq lbl lbl' then true else false + | _ => false + end. + +Lemma is_label_correct: + forall lbl instr, + if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl. +Proof. + intros. destruct instr; simpl; try discriminate. + case (peq lbl l); intro; congruence. +Qed. + +Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z := + match c with + | nil => None + | instr :: c' => + if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c' + end. + +Variable ge: genv. + +(** The semantics is purely small-step and defined as a function + from the current state (a register set + a memory state) + to either [OK rs' m'] where [rs'] and [m'] are the updated register + set and memory state after execution of the instruction at [rs#PC], + or [Error] if the processor is stuck. *) + +Inductive outcome: Set := + | OK: regset -> mem -> outcome + | Error: outcome. + +(** Manipulations over the [PC] register: continuing with the next + instruction ([nextinstr]) or branching to a label ([goto_label]). *) + +Definition nextinstr (rs: regset) := + rs#PC <- (Val.add rs#PC Vone). + +Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := + match label_pos lbl 0 c with + | None => Error + | Some pos => + match rs#PC with + | Vptr b ofs => OK (rs#PC <- (Vptr b (Int.repr pos))) m + | _ => Error + end + end. + +(** Evaluation of [shift_op] operands *) + +Definition eval_shift_op (so: shift_op) (rs: regset) := + match so with + | SOimm n => Vint n + | SOreg r => rs r + | SOlslimm r n => Val.shl (rs r) (Vint n) + | SOlslreg r r' => Val.shl (rs r) (rs r') + | SOlsrimm r n => Val.shru (rs r) (Vint n) + | SOlsrreg r r' => Val.shru (rs r) (rs r') + | SOasrimm r n => Val.shr (rs r) (Vint n) + | SOasrreg r r' => Val.shr (rs r) (rs r') + | SOrorimm r n => Val.ror (rs r) (Vint n) + | SOrorreg r r' => Val.ror (rs r) (rs r') + end. + +(** Evaluation of [shift_addr] operands *) + +Definition eval_shift_addr (sa: shift_addr) (rs: regset) := + match sa with + | SAimm n => Vint n + | SAreg r => rs r + | SAlsl r n => Val.shl (rs r) (Vint n) + | SAlsr r n => Val.shru (rs r) (Vint n) + | SAasr r n => Val.shr (rs r) (Vint n) + | SAror r n => Val.ror (rs r) (Vint n) + end. + + +(** Auxiliaries for memory accesses *) + +Definition exec_load (chunk: memory_chunk) (addr: val) (r: preg) + (rs: regset) (m: mem) := + match Mem.loadv chunk m addr with + | None => Error + | Some v => OK (nextinstr (rs#r <- v)) m + end. + +Definition exec_store (chunk: memory_chunk) (addr: val) (r: preg) + (rs: regset) (m: mem) := + match Mem.storev chunk m addr (rs r) with + | None => Error + | Some m' => OK (nextinstr rs) m' + end. + +(** Operations over condition bits. *) + +Definition compare_int (rs: regset) (v1 v2: val) := + rs#CReq <- (Val.cmp Ceq v1 v2) + #CRne <- (Val.cmp Cne v1 v2) + #CRhs <- (Val.cmpu Cge v1 v2) + #CRlo <- (Val.cmpu Clt v1 v2) + #CRmi <- Vundef + #CRpl <- Vundef + #CRhi <- (Val.cmpu Cgt v1 v2) + #CRls <- (Val.cmpu Cle v1 v2) + #CRge <- (Val.cmp Cge v1 v2) + #CRlt <- (Val.cmp Clt v1 v2) + #CRgt <- (Val.cmp Cgt v1 v2) + #CRle <- (Val.cmp Cle v1 v2). + +Definition compare_float (rs: regset) (v1 v2: val) := + rs#CReq <- (Val.cmpf Ceq v1 v2) + #CRne <- (Val.cmpf Cne v1 v2) + #CRhs <- Vundef + #CRlo <- Vundef + #CRmi <- (Val.cmpf Clt v1 v2) (* lt *) + #CRpl <- (Val.notbool (Val.cmpf Clt v1 v2)) (* not lt *) + #CRhi <- (Val.notbool (Val.cmpf Cle v1 v2)) (* not le *) + #CRls <- (Val.cmpf Cle v1 v2) (* le *) + #CRge <- (Val.cmpf Cge v1 v2) (* ge *) + #CRlt <- (Val.notbool (Val.cmpf Cge v1 v2)) (* not ge *) + #CRgt <- (Val.cmpf Cgt v1 v2) (* gt *) + #CRle <- (Val.notbool (Val.cmpf Cgt v1 v2)). (* not gt *) + +(** Execution of a single instruction [i] in initial state + [rs] and [m]. Return updated state. For instructions + that correspond to actual PowerPC instructions, the cases are + straightforward transliterations of the informal descriptions + given in the PowerPC reference manuals. For pseudo-instructions, + refer to the informal descriptions given above. Note that + we set to [Vundef] the registers used as temporaries by the + expansions of the pseudo-instructions, so that the PPC code + we generate cannot use those registers to hold values that + must survive the execution of the pseudo-instruction. +*) + +Definition symbol_offset (id: ident) (ofs: int) : val := + match Genv.find_symbol ge id with + | Some b => Vptr b ofs + | None => Vundef + end. + +Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := + match i with + | Padd r1 r2 so => + OK (nextinstr (rs#r1 <- (Val.add rs#r2 (eval_shift_op so rs)))) m + | Pand r1 r2 so => + OK (nextinstr (rs#r1 <- (Val.and rs#r2 (eval_shift_op so rs)))) m + | Pb lbl => + goto_label c lbl rs m + | Pbc bit lbl => + match rs#bit with + | Vint n => if Int.eq n Int.zero then OK (nextinstr rs) m else goto_label c lbl rs m + | _ => Error + end + | Pbsymb id => + OK (rs#PC <- (symbol_offset id Int.zero)) m + | Pbreg r => + OK (rs#PC <- (rs#r)) m + | Pblsymb id => + OK (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m + | Pblreg r => + OK (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m + | Pbic r1 r2 so => + OK (nextinstr (rs#r1 <- (Val.and rs#r2 (Val.notint (eval_shift_op so rs))))) m + | Pcmp r1 so => + OK (nextinstr (compare_int rs rs#r1 (eval_shift_op so rs))) m + | Peor r1 r2 so => + OK (nextinstr (rs#r1 <- (Val.xor rs#r2 (eval_shift_op so rs)))) m + | Pldr r1 r2 sa => + exec_load Mint32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pldrb r1 r2 sa => + exec_load Mint8unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pldrh r1 r2 sa => + exec_load Mint16unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pldrsb r1 r2 sa => + exec_load Mint8signed (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pldrsh r1 r2 sa => + exec_load Mint16signed (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pmov r1 so => + OK (nextinstr (rs#r1 <- (eval_shift_op so rs))) m + | Pmovc bit r1 so => + match rs#bit with + | Vint n => if Int.eq n Int.zero + then OK (nextinstr rs) m + else OK (nextinstr (rs#r1 <- (eval_shift_op so rs))) m + | _ => Error + end + | Pmul r1 r2 r3 => + OK (nextinstr (rs#r1 <- (Val.mul rs#r2 rs#r3))) m + | Pmvn r1 so => + OK (nextinstr (rs#r1 <- (Val.notint (eval_shift_op so rs)))) m + | Porr r1 r2 so => + OK (nextinstr (rs#r1 <- (Val.or rs#r2 (eval_shift_op so rs)))) m + | Prsb r1 r2 so => + OK (nextinstr (rs#r1 <- (Val.sub (eval_shift_op so rs) rs#r2))) m + | Pstr r1 r2 sa => + exec_store Mint32 (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pstrb r1 r2 sa => + exec_store Mint8unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Pstrh r1 r2 sa => + exec_store Mint16unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m + | Psdiv rd r1 r2 => + OK (nextinstr (rs#rd <- (Val.divs rs#r1 rs#r2))) m + | Psub r1 r2 so => + OK (nextinstr (rs#r1 <- (Val.sub rs#r2 (eval_shift_op so rs)))) m + | Pudiv rd r1 r2 => + OK (nextinstr (rs#rd <- (Val.divu rs#r1 rs#r2))) m + (* Floating-point coprocessor instructions *) + | Pabsd r1 r2 => + OK (nextinstr (rs#r1 <- (Val.absf rs#r2))) m + | Padfd r1 r2 r3 => + OK (nextinstr (rs#r1 <- (Val.addf rs#r2 rs#r3))) m + | Pcmf r1 r2 => + OK (nextinstr (compare_float rs rs#r1 rs#r2)) m + | Pdvfd r1 r2 r3 => + OK (nextinstr (rs#r1 <- (Val.divf rs#r2 rs#r3))) m + | Pfixz r1 r2 => + OK (nextinstr (rs#r1 <- (Val.intoffloat rs#r2))) m + | Pfixzu r1 r2 => + OK (nextinstr (rs#r1 <- (Val.intuoffloat rs#r2))) m + | Pfltd r1 r2 => + OK (nextinstr (rs#r1 <- (Val.floatofint rs#r2))) m + | Pfltud r1 r2 => + OK (nextinstr (rs#r1 <- (Val.floatofintu rs#r2))) m + | Pldfd r1 r2 n => + exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m + | Pldfs r1 r2 n => + exec_load Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m + | Plifd r1 f => + OK (nextinstr (rs#r1 <- (Vfloat f))) m + | Pmnfd r1 r2 => + OK (nextinstr (rs#r1 <- (Val.negf rs#r2))) m + | Pmvfd r1 r2 => + OK (nextinstr (rs#r1 <- (rs#r2))) m + | Pmvfs r1 r2 => + OK (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m + | Pmufd r1 r2 r3 => + OK (nextinstr (rs#r1 <- (Val.mulf rs#r2 rs#r3))) m + | Pstfd r1 r2 n => + exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m + | Pstfs r1 r2 n => + exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m + | Psufd r1 r2 r3 => + OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m + (* Pseudo-instructions *) + | Pallocblock => + match rs#IR0 with + | Vint n => + let (m', b) := Mem.alloc m 0 (Int.signed n) in + OK (nextinstr (rs#IR0 <- (Vptr b Int.zero) + #IR14 <- (Val.add rs#PC Vone))) m' + | _ => Error + end + | Pallocframe lo hi pos => + let (m1, stk) := Mem.alloc m lo hi in + let sp := (Vptr stk (Int.repr lo)) in + match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with + | None => Error + | Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2 + end + | Pfreeframe pos => + match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with + | None => Error + | Some v => + match rs#IR13 with + | Vptr stk ofs => OK (nextinstr (rs#IR13 <- v)) (Mem.free m stk) + | _ => Error + end + end + | Plabel lbl => + OK (nextinstr rs) m + | Ploadsymbol r1 lbl ofs => + OK (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m + end. + +(** Translation of the LTL/Linear/Mach view of machine registers + to the ARM view. ARM has two different types for registers + (integer and float) while LTL et al have only one. The + [ireg_of] and [freg_of] are therefore partial in principle. + To keep things simpler, we make them return nonsensical + results when applied to a LTL register of the wrong type. + The proof in [ARMgenproof] will show that this never happens. + + Note that no LTL register maps to [IR14]. + This register is reserved as temporary, to be used + by the generated ARM code. *) + +Definition ireg_of (r: mreg) : ireg := + match r with + | R0 => IR0 | R1 => IR1 | R2 => IR2 | R3 => IR3 + | R4 => IR4 | R5 => IR5 | R6 => IR6 | R7 => IR7 + | R8 => IR8 | R9 => IR9 | R11 => IR11 + | IT1 => IR10 | IT2 => IR12 + | _ => IR0 (* should not happen *) + end. + +Definition freg_of (r: mreg) : freg := + match r with + | F0 => FR0 | F1 => FR1 + | F4 => FR4 | F5 => FR5 | F6 => FR6 | F7 => FR7 + | FT1 => FR2 | FT2 => FR3 + | _ => FR0 (* should not happen *) + end. + +Definition preg_of (r: mreg) := + match mreg_type r with + | Tint => IR (ireg_of r) + | Tfloat => FR (freg_of r) + end. + +(** 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. *) + +Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := + | extcall_arg_reg: forall r, + extcall_arg rs m (R r) (rs (preg_of r)) + | extcall_arg_int_stack: forall ofs bofs v, + bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> + Mem.loadv Mint32 m (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v -> + extcall_arg rs m (S (Outgoing ofs Tint)) v + | extcall_arg_float_stack: forall ofs bofs v, + bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> + Mem.loadv Mfloat64 m (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v -> + extcall_arg rs m (S (Outgoing ofs Tfloat)) v. + +Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop := + | extcall_args_nil: + extcall_args rs m nil nil + | extcall_args_cons: forall l1 ll v1 vl, + extcall_arg rs m l1 v1 -> extcall_args rs m ll vl -> + extcall_args rs m (l1 :: ll) (v1 :: vl). + +Definition extcall_arguments + (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := + extcall_args rs m (Conventions.loc_arguments sg) args. + +Definition loc_external_result (sg: signature) : preg := + preg_of (Conventions.loc_result sg). + +(** Execution of the instruction at [rs#PC]. *) + +Inductive state: Set := + | State: regset -> mem -> state. + +Inductive step: state -> trace -> state -> Prop := + | exec_step_internal: + forall b ofs c i rs m rs' m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal c) -> + find_instr (Int.unsigned ofs) c = Some i -> + exec_instr c i rs m = OK rs' m' -> + step (State rs m) E0 (State rs' m') + | exec_step_external: + forall b ef args res rs m t rs', + rs PC = Vptr b Int.zero -> + Genv.find_funct_ptr ge b = Some (External ef) -> + event_match ef args t res -> + extcall_arguments rs m ef.(ef_sig) args -> + rs' = (rs#(loc_external_result ef.(ef_sig)) <- res + #PC <- (rs IR14)) -> + step (State rs m) t (State rs' m). + +End RELSEM. + +(** Execution of whole programs. *) + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + let rs0 := + (Pregmap.init Vundef) + # PC <- (symbol_offset ge p.(prog_main) Int.zero) + # IR14 <- Vzero + # IR13 <- (Vptr Mem.nullptr Int.zero) in + initial_state p (State rs0 m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r, + rs#PC = Vzero -> + rs#IR0 = Vint r -> + final_state (State rs m) r. + +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/Asmgen.v b/arm/Asmgen.v index a360bded..5e21e14e 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -26,35 +26,6 @@ Require Import Locations. Require Import Mach. Require Import Asm. -(** Translation of the LTL/Linear/Mach view of machine registers - to the ARM view. ARM has two different types for registers - (integer and float) while LTL et al have only one. The - [ireg_of] and [freg_of] are therefore partial in principle. - To keep things simpler, we make them return nonsensical - results when applied to a LTL register of the wrong type. - The proof in [ARMgenproof] will show that this never happens. - - Note that no LTL register maps to [IR14]. - This register is reserved as temporary, to be used - by the generated ARM code. *) - -Definition ireg_of (r: mreg) : ireg := - match r with - | R0 => IR0 | R1 => IR1 | R2 => IR2 | R3 => IR3 - | R4 => IR4 | R5 => IR5 | R6 => IR6 | R7 => IR7 - | R8 => IR8 | R9 => IR9 | R11 => IR11 - | IT1 => IR10 | IT2 => IR12 - | _ => IR0 (* should not happen *) - end. - -Definition freg_of (r: mreg) : freg := - match r with - | F0 => FR0 | F1 => FR1 - | F4 => FR4 | F5 => FR5 | F6 => FR6 | F7 => FR7 - | FT1 => FR2 | FT2 => FR3 - | _ => FR0 (* should not happen *) - end. - (** Recognition of integer immediate arguments. - For arithmetic operations, immediates are 8-bit quantities zero-extended and rotated right by 0, 2, 4, ... 30 bits. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml new file mode 100644 index 00000000..e5b21f9c --- /dev/null +++ b/arm/PrintAsm.ml @@ -0,0 +1,507 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Printing ARM assembly code in asm syntax *) + +open Printf +open Datatypes +open CList +open Camlcoq +open AST +open Asm + +(* On-the-fly label renaming *) + +let next_label = ref 100 + +let new_label() = + let lbl = !next_label in incr next_label; lbl + +let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t) + +let label_for_label lbl = + try + Hashtbl.find current_function_labels lbl + with Not_found -> + let lbl' = new_label() in + Hashtbl.add current_function_labels lbl lbl'; + lbl' + +(* Record identifiers of external functions *) + +module IdentSet = Set.Make(struct type t = ident let compare = compare end) + +let extfuns = (ref IdentSet.empty) + +let record_extfun (Coq_pair(name, defn)) = + match defn with + | Internal _ -> () + | External _ -> extfuns := IdentSet.add name !extfuns + +(* Basic printing functions *) + +let print_symb oc symb = + if IdentSet.mem symb !extfuns + then fprintf oc ".L%s$stub" (extern_atom symb) + else fprintf oc "%s" (extern_atom symb) + +let print_label oc lbl = + fprintf oc ".L%d" (label_for_label lbl) + +let coqint oc n = + fprintf oc "%ld" (camlint_of_coqint n) + +let print_symb_ofs oc (symb, ofs) = + print_symb oc symb; + let ofs = camlint_of_coqint ofs in + if ofs <> 0l then fprintf oc " + %ld" ofs + +let int_reg_name = function + | IR0 -> "r0" | IR1 -> "r1" | IR2 -> "r2" | IR3 -> "r3" + | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7" + | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11" + | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr" + +let float_reg_name = function + | FR0 -> "f0" | FR1 -> "f1" | FR2 -> "f2" | FR3 -> "f3" + | FR4 -> "f4" | FR5 -> "f5" | FR6 -> "f6" | FR7 -> "f7" + +let ireg oc r = output_string oc (int_reg_name r) +let freg oc r = output_string oc (float_reg_name r) + +let condition_name = function + | CReq -> "eq" + | CRne -> "ne" + | CRhs -> "hs" + | CRlo -> "lo" + | CRmi -> "mi" + | CRpl -> "pl" + | CRhi -> "hi" + | CRls -> "ls" + | CRge -> "ge" + | CRlt -> "lt" + | CRgt -> "gt" + | CRle -> "le" + +(* Record current code position and latest position at which to + emit float and symbol constants. *) + +let currpos = ref 0 +let size_constants = ref 0 +let max_pos_constants = ref max_int + +let distance_to_emit_constants () = + !max_pos_constants - (!currpos + !size_constants) + +(* Associate labels to floating-point constants and to symbols *) + +let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) + +let label_float f = + let bf = Int64.bits_of_float f in + try + Hashtbl.find float_labels bf + with Not_found -> + let lbl' = new_label() in + Hashtbl.add float_labels bf lbl'; + size_constants := !size_constants + 8; + max_pos_constants := min !max_pos_constants (!currpos + 1024); + lbl' + +let symbol_labels = (Hashtbl.create 39 : (ident * Integers.int, int) Hashtbl.t) + +let label_symbol id ofs = + try + Hashtbl.find symbol_labels (id, ofs) + with Not_found -> + let lbl' = new_label() in + Hashtbl.add symbol_labels (id, ofs) lbl'; + size_constants := !size_constants + 4; + max_pos_constants := min !max_pos_constants (!currpos + 4096); + lbl' + +let reset_constants () = + Hashtbl.clear float_labels; + Hashtbl.clear symbol_labels; + size_constants := 0; + max_pos_constants := max_int + +let emit_constants oc = + Hashtbl.iter + (fun bf lbl -> + (* Floats are mixed-endian on this flavor of ARM *) + let bfhi = Int64.shift_right_logical bf 32 + and bflo = Int64.logand bf 0xFFFF_FFFFL in + fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" + lbl bfhi bflo) + float_labels; + Hashtbl.iter + (fun (id, ofs) lbl -> + fprintf oc ".L%d: .word %a\n" + lbl print_symb_ofs (id, ofs)) + symbol_labels; + reset_constants () + +(* Simulate instructions by calling helper functions *) + +let print_list_ireg oc l = + match l with + | [] -> assert false + | r1 :: rs -> ireg oc r1; List.iter (fun r -> fprintf oc ", %a" ireg r) rs + +let rec remove l r = + match l with + | [] -> [] + | hd :: tl -> if hd = r then remove tl r else hd :: remove tl r + +let call_helper oc fn dst arg1 arg2 = + (* Preserve caller-save registers r0...r3 except dst *) + let tosave = remove [IR0; IR1; IR2; IR3] dst in + fprintf oc " stmfd sp!, {%a}\n" print_list_ireg tosave; + (* Copy arg1 to R0 and arg2 to R1 *) + let moves = + Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in + List.iter + (fun (Coq_pair(s, d)) -> + fprintf oc " mov %a, %a\n" ireg d ireg s) + moves; + (* Call the helper function *) + fprintf oc " bl %s\n" fn; + (* Move result to dst *) + begin match dst with + | IR0 -> () + | _ -> + fprintf oc " mov %a, r0\n" ireg dst + end; + (* Restore the other caller-save registers *) + fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave; + (* ... for a total of at most 7 instructions *) + 7 + +(* Printing of instructions *) + +let shift_op oc = function + | SOimm n -> fprintf oc "#%a" coqint n + | SOreg r -> ireg oc r + | SOlslimm(r, n) -> fprintf oc "%a, lsl #%a" ireg r coqint n + | SOlslreg(r, r') -> fprintf oc "%a, lsl %a" ireg r ireg r' + | SOlsrimm(r, n) -> fprintf oc "%a, lsr #%a" ireg r coqint n + | SOlsrreg(r, r') -> fprintf oc "%a, lsr %a" ireg r ireg r' + | SOasrimm(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n + | SOasrreg(r, r') -> fprintf oc "%a, asr %a" ireg r ireg r' + | SOrorimm(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n + | SOrorreg(r, r') -> fprintf oc "%a, ror %a" ireg r ireg r' + +let shift_addr oc = function + | SAimm n -> fprintf oc "#%a" coqint n + | SAreg r -> ireg oc r + | SAlsl(r, n) -> fprintf oc "%a, lsl #%a" ireg r coqint n + | SAlsr(r, n) -> fprintf oc "%a, lsr #%a" ireg r coqint n + | SAasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n + | SAror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n + +module Labelset = Set.Make(struct type t = label let compare = compare end) + +let print_instruction oc labels = function + (* Core instructions *) + | Padd(r1, r2, so) -> + fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Pand(r1, r2, so) -> + fprintf oc " and %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Pb lbl -> + fprintf oc " b %a\n" print_label lbl; 1 + | Pbc(bit, lbl) -> + fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 + | Pbsymb id -> + fprintf oc " b %a\n" print_symb id; 1 + | Pbreg r -> + fprintf oc " mov pc, %a\n" ireg r; 1 + | Pblsymb id -> + fprintf oc " bl %a\n" print_symb id; 1 + | Pblreg r -> + fprintf oc " mov lr, pc\n"; + fprintf oc " mov pc, %a\n" ireg r; 2 + | Pbic(r1, r2, so) -> + fprintf oc " bic %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Pcmp(r1, so) -> + fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 + | Peor(r1, r2, so) -> + fprintf oc " eor %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Pldr(r1, r2, sa) -> + fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pldrb(r1, r2, sa) -> + fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pldrh(r1, r2, sa) -> + fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pldrsb(r1, r2, sa) -> + fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pldrsh(r1, r2, sa) -> + fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pmov(r1, so) -> + fprintf oc " mov %a, %a\n" ireg r1 shift_op so; 1 + | Pmovc(bit, r1, so) -> + fprintf oc " mov%s %a, %a\n" (condition_name bit) ireg r1 shift_op so; 1 + | Pmul(r1, r2, r3) -> + fprintf oc " mul %a, %a, %a\n" ireg r1 ireg r2 ireg r3; 1 + | Pmvn(r1, so) -> + fprintf oc " mvn %a, %a\n" ireg r1 shift_op so; 1 + | Porr(r1, r2, so) -> + fprintf oc " orr %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Prsb(r1, r2, so) -> + fprintf oc " rsb %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Pstr(r1, r2, sa) -> + fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pstrb(r1, r2, sa) -> + fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pstrh(r1, r2, sa) -> + fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Psdiv(r1, r2, r3) -> + call_helper oc "__divsi3" r1 r2 r3 + | Psub(r1, r2, so) -> + fprintf oc " sub %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Pudiv(r1, r2, r3) -> + call_helper oc "__udivsi3" r1 r2 r3 + (* Floating-point coprocessor instructions *) + | Pabsd(r1, r2) -> + fprintf oc " absd %a, %a\n" freg r1 freg r2; 1 + | Padfd(r1, r2, r3) -> + fprintf oc " adfd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + | Pcmf(r1, r2) -> + fprintf oc " cmf %a, %a\n" freg r1 freg r2; 1 + | Pdvfd(r1, r2, r3) -> + fprintf oc " dvfd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + | Pfixz(r1, r2) -> + fprintf oc " fixz %a, %a\n" ireg r1 freg r2; 1 + | Pfixzu(r1, r2) -> + (* F3 = second float temporary is unused at this point, + but this should be reflected in the proof *) + let lbl = label_float 2147483648.0 in + let lbl2 = new_label() in + fprintf oc " ldfd f3, .L%d\n" lbl; + fprintf oc " cmfe %a, f3\n" freg r2; + fprintf oc " fixltz %a, %a\n" ireg r1 freg r2; + fprintf oc " blt .L%d\n" lbl2; + fprintf oc " sufd f3, %a, f3\n" freg r2; + fprintf oc " fixz %a, f3\n" ireg r1; + fprintf oc " eor %a, %a, #-2147483648\n" ireg r1 ireg r1; + fprintf oc ".L%d\n" lbl2; + 7 + | Pfltd(r1, r2) -> + fprintf oc " fltd %a, %a\n" freg r1 ireg r2; 1 + | Pfltud(r1, r2) -> + fprintf oc " fltd %a, %a\n" freg r1 ireg r2; + fprintf oc " cmp %a, #0\n" ireg r2; + (* F3 = second float temporary is unused at this point, + but this should be reflected in the proof *) + let lbl = label_float 4294967296.0 in + fprintf oc " ldfltd f3, .L%d\n" lbl; + fprintf oc " adfltd %a, %a, f3\n" freg r1 freg r1; 4 + | Pldfd(r1, r2, n) -> + fprintf oc " ldfd %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 + | Pldfs(r1, r2, n) -> + fprintf oc " ldfs %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; + fprintf oc " mvfd %a, %a\n" freg r1 freg r1; 2 + | Plifd(r1, f) -> + if Int64.bits_of_float f = 0L (* +0.0 *) then begin + fprintf oc " mvfd %a, #0.0\n" freg r1; 1 + end else begin + let lbl = label_float f in + fprintf oc " ldfd %a, .L%d @ %.12g\n" freg r1 lbl f; 1 + end + | Pmnfd(r1, r2) -> + fprintf oc " mnfd %a, %a\n" freg r1 freg r2; 1 + | Pmvfd(r1, r2) -> + fprintf oc " mvfd %a, %a\n" freg r1 freg r2; 1 + | Pmvfs(r1, r2) -> + fprintf oc " mvfs %a, %a\n" freg r1 freg r2; + fprintf oc " mvfd %a, %a\n" freg r2 freg r2; 2 + | Pmufd(r1, r2, r3) -> + fprintf oc " mufd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + | Pstfd(r1, r2, n) -> + fprintf oc " stfd %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 + | Pstfs(r1, r2, n) -> + (* F3 = second float temporary is unused at this point, + but this should be reflected in the proof *) + fprintf oc " mvfs f3, %a\n" freg r1; + fprintf oc " stfs f3, [%a, #%a]\n" ireg r2 coqint n; 2 + | Psufd(r1, r2, r3) -> + fprintf oc " sufd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + (* Pseudo-instructions *) + | Pallocblock -> + fprintf oc " bl compcert_alloc\n"; 1 + | Pallocframe(lo, hi, ofs) -> + let lo = camlint_of_coqint lo + and hi = camlint_of_coqint hi + and ofs = camlint_of_coqint ofs in + let sz = Int32.sub hi lo in + (* Keep stack 4-aligned *) + let sz4 = Int32.logand (Int32.add sz 3l) 0xFFFF_FFFCl in + (* FIXME: consider a store multiple? *) + (* R12 = first int temporary is unused at this point, + but this should be reflected in the proof *) + fprintf oc " mov r12, sp\n"; + fprintf oc " sub sp, sp, #%ld\n" sz4; + fprintf oc " str r12, [sp, #%ld]\n" ofs; 3 + | Pfreeframe ofs -> + fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 + | Plabel lbl -> + if Labelset.mem lbl labels then + fprintf oc "%a:\n" print_label lbl; 0 + | Ploadsymbol(r1, id, ofs) -> + let lbl = label_symbol id ofs in + fprintf oc " ldr %a, .L%d @ %a\n" + ireg r1 lbl print_symb_ofs (id, ofs); 1 + +let no_fallthrough = function + | Pb _ -> true + | Pbsymb _ -> true + | Pbreg _ -> true + | _ -> false + +let rec print_instructions oc labels instrs = + match instrs with + | [] -> () + | i :: il -> + let n = print_instruction oc labels i in + currpos := !currpos + n * 4; + let d = distance_to_emit_constants() in + if d < 256 && no_fallthrough i then + emit_constants oc + else if d < 16 then begin + let lbl = new_label() in + fprintf oc " b .L%d\n" lbl; + emit_constants oc; + fprintf oc ".L%d:\n" lbl + end; + print_instructions oc labels il + +let rec labels_of_code = function + | [] -> Labelset.empty + | (Pb lbl | Pbc(_, lbl)) :: c -> Labelset.add lbl (labels_of_code c) + | _ :: c -> labels_of_code c + +let print_function oc name code = + Hashtbl.clear current_function_labels; + reset_constants(); + currpos := 0; + fprintf oc " .text\n"; + fprintf oc " .align 2\n"; + fprintf oc " .global %a\n" print_symb name; + fprintf oc " .type %a, %%function\n" print_symb name; + fprintf oc "%a:\n" print_symb name; + print_instructions oc (labels_of_code code) code; + emit_constants oc + +(* Generation of stub code for external functions. + Compcert passes the first two float arguments in F0 and F1, + while gcc passes them in pairs of integer registers. *) + +let print_external_function oc name sg = + let name = extern_atom name in + let rec move_args ty_args int_regs float_regs = + match ty_args with + | [] -> () + | Tint :: tys -> + begin match int_regs with + | [] -> move_args tys [] float_regs + | ir :: irs -> move_args tys irs float_regs + end + | Tfloat :: tys -> + begin match float_regs, int_regs with + | fr :: frs, ir1 :: ir2 :: irs -> + (* transfer fr to the pair (ir1, ir2) *) + fprintf oc " stfd %a, [sp, #-8]!\n" freg fr; + fprintf oc " ldmfd sp!, {%a, %a}\n" ireg ir1 ireg ir2; + move_args tys irs frs + | fr :: frs, ir1 :: [] -> + (* transfer fr to ir1 and the bottom stack word *) + fprintf oc " stfd %a, [sp, #-4]!\n" freg fr; + fprintf oc " ldmfd sp!, {%a}\n" ireg ir1; + move_args tys [] frs + | _, _ -> + (* no more float regs, or no more int regs: + float arg is already on stack, where it should be *) + move_args tys int_regs float_regs + end + in + fprintf oc " .text\n"; + fprintf oc " .align 2\n"; + fprintf oc ".L%s$stub:\n" name; + move_args sg.sig_args [IR0;IR1;IR2;IR3] [FR0;FR1]; + (* Remove variadic prefix $iiff if any *) + let real_name = + try String.sub name 0 (String.index name '$') + with Not_found -> name in + fprintf oc " b %s\n" real_name + +let print_fundef oc (Coq_pair(name, defn)) = + match defn with + | Internal code -> print_function oc name code + | External ef -> print_external_function oc name ef.ef_sig + +(* Data *) + +let init_data_queue = ref [] + +let print_init oc = function + | Init_int8 n -> + fprintf oc " .byte %ld\n" (camlint_of_coqint n) + | Init_int16 n -> + fprintf oc " .short %ld\n" (camlint_of_coqint n) + | Init_int32 n -> + fprintf oc " .word %ld\n" (camlint_of_coqint n) + | Init_float32 n -> + fprintf oc " .word 0x%lx @ %.15g \n" (Int32.bits_of_float n) n + | Init_float64 n -> + (* Floats are mixed-endian on this flavor of ARM *) + let bf = Int64.bits_of_float n in + let bfhi = Int64.shift_right_logical bf 32 + and bflo = Int64.logand bf 0xFFFF_FFFFL in + fprintf oc " .word 0x%Lx, 0x%Lx @ %.15g\n" bfhi bflo n + | Init_space n -> + let n = camlint_of_z n in + if n > 0l then fprintf oc " .space %ld\n" n + | Init_pointer id -> + let lbl = new_label() in + fprintf oc " .word .L%d\n" lbl; + init_data_queue := (lbl, id) :: !init_data_queue + +let print_init_data oc id = + init_data_queue := []; + List.iter (print_init oc) id; + let rec print_remainder () = + match !init_data_queue with + | [] -> () + | (lbl, id) :: rem -> + init_data_queue := rem; + fprintf oc ".L%d:\n" lbl; + List.iter (print_init oc) id; + print_remainder() + in print_remainder() + +let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = + match init_data with + | [] -> () + | _ -> + fprintf oc " .data\n"; + fprintf oc " .align 2\n"; + fprintf oc " .global %a\n" print_symb name; + fprintf oc " .type %a, %%object\n" print_symb name; + fprintf oc "%a:\n" print_symb name; + print_init_data oc init_data + +let print_program oc p = + extfuns := IdentSet.empty; + List.iter record_extfun p.prog_funct; + List.iter (print_var oc) p.prog_vars; + List.iter (print_fundef oc) p.prog_funct + diff --git a/arm/PrintAsm.mli b/arm/PrintAsm.mli new file mode 100644 index 00000000..aefe3a0a --- /dev/null +++ b/arm/PrintAsm.mli @@ -0,0 +1,13 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +val print_program: out_channel -> Asm.program -> unit diff --git a/arm/Selection.v b/arm/Selection.v index d5eb6b8b..1b5411b1 100644 --- a/arm/Selection.v +++ b/arm/Selection.v @@ -1390,5 +1390,6 @@ Definition sel_fundef (f: Cminor.fundef) : fundef := Definition sel_program (p: Cminor.program) : program := transform_program sel_fundef p. +(** For compatibility with PowerPC *) - +Parameter use_fused_mul: unit -> bool. |