From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/PPC.v | 843 ---------------------------------------------------------- 1 file changed, 843 deletions(-) delete mode 100644 backend/PPC.v (limited to 'backend/PPC.v') diff --git a/backend/PPC.v b/backend/PPC.v deleted file mode 100644 index e47cba01..00000000 --- a/backend/PPC.v +++ /dev/null @@ -1,843 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 PowerPC 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. - -(** * Abstract syntax *) - -(** Integer registers, floating-point registers. *) - -Inductive ireg: Set := - | GPR0: ireg | GPR1: ireg | GPR2: ireg | GPR3: ireg - | GPR4: ireg | GPR5: ireg | GPR6: ireg | GPR7: ireg - | GPR8: ireg | GPR9: ireg | GPR10: ireg | GPR11: ireg - | GPR12: ireg | GPR13: ireg | GPR14: ireg | GPR15: ireg - | GPR16: ireg | GPR17: ireg | GPR18: ireg | GPR19: ireg - | GPR20: ireg | GPR21: ireg | GPR22: ireg | GPR23: ireg - | GPR24: ireg | GPR25: ireg | GPR26: ireg | GPR27: ireg - | GPR28: ireg | GPR29: ireg | GPR30: ireg | GPR31: ireg. - -Inductive freg: Set := - | FPR0: freg | FPR1: freg | FPR2: freg | FPR3: freg - | FPR4: freg | FPR5: freg | FPR6: freg | FPR7: freg - | FPR8: freg | FPR9: freg | FPR10: freg | FPR11: freg - | FPR12: freg | FPR13: freg | FPR14: freg | FPR15: freg - | FPR16: freg | FPR17: freg | FPR18: freg | FPR19: freg - | FPR20: freg | FPR21: freg | FPR22: freg | FPR23: freg - | FPR24: freg | FPR25: freg | FPR26: freg | FPR27: freg - | FPR28: freg | FPR29: freg | FPR30: freg | FPR31: 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. - -(** Symbolic constants. Immediate operands to an arithmetic instruction - 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 - resolved later by the linker. -*) - -Inductive constant: Set := - | Cint: int -> constant - | Csymbol_low: ident -> int -> constant - | Csymbol_high: ident -> int -> constant. - -(** A note on constants: while immediate operands to PowerPC - instructions must be representable in 16 bits (with - sign extension or left shift by 16 positions for some instructions), - we do not attempt to capture these restrictions in the - abstract syntax nor in the semantics. The assembler will - emit an error if immediate operands exceed the representable - range. Of course, our PPC generator (file [PPCgen]) is - careful to respect this range. *) - -(** Bits in the condition register. We are only interested in the - first 4 bits. *) - -Inductive crbit: Set := - | CRbit_0: crbit - | CRbit_1: crbit - | CRbit_2: crbit - | CRbit_3: crbit. - -(** 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 instruction : Set := - | Padd: ireg -> ireg -> ireg -> instruction (**r integer addition *) - | Paddi: ireg -> ireg -> constant -> instruction (**r add immediate *) - | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) - | Paddze: ireg -> ireg -> instruction (**r add Carry bit *) - | Pallocblock: instruction (**r allocate new heap block *) - | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) - | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) - | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) - | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) - | Pandis_: ireg -> ireg -> constant -> instruction (**r and immediate high and set conditions *) - | Pb: label -> instruction (**r unconditional branch *) - | Pbctr: instruction (**r branch to contents of register CTR *) - | Pbctrl: instruction (**r branch to contents of CTR and link *) - | Pbf: crbit -> label -> instruction (**r branch if false *) - | Pbl: ident -> instruction (**r branch and link *) - | Pbs: ident -> instruction (**r branch to symbol *) - | Pblr: instruction (**r branch to contents of register LR *) - | Pbt: crbit -> label -> instruction (**r branch if true *) - | Pcmplw: ireg -> ireg -> instruction (**r unsigned integer comparison *) - | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) - | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) - | Pcmpwi: ireg -> constant -> instruction (**r same, with immediate argument *) - | Pcror: crbit -> crbit -> crbit -> instruction (**r or between condition bits *) - | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) - | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) - | Peqv: ireg -> ireg -> ireg -> instruction (**r bitwise not-xor *) - | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) - | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) - | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *) - | Pfabs: freg -> freg -> instruction (**r float absolute value *) - | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) - | Pfcmpu: freg -> freg -> instruction (**r float comparison *) - | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion *) - | Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion *) - | Pfdiv: freg -> freg -> freg -> instruction (**r float division *) - | Pfmadd: freg -> freg -> freg -> freg -> instruction (**r float multiply-add *) - | Pfmr: freg -> freg -> instruction (**r float move *) - | Pfmsub: freg -> freg -> freg -> freg -> instruction (**r float multiply-sub *) - | Pfmul: freg -> freg -> freg -> instruction (**r float multiply *) - | Pfneg: freg -> freg -> instruction (**r float negation *) - | Pfrsp: freg -> freg -> instruction (**r float round to single precision *) - | Pfsub: freg -> freg -> freg -> instruction (**r float subtraction *) - | Pictf: freg -> ireg -> instruction (**r int-to-float conversion *) - | Piuctf: freg -> ireg -> instruction (**r unsigned int-to-float conversion *) - | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) - | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) - | Plfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Plfs: freg -> constant -> ireg -> instruction (**r load 32-bit float *) - | Plfsx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Plha: ireg -> constant -> ireg -> instruction (**r load 16-bit signed int *) - | Plhax: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Plhz: ireg -> constant -> ireg -> instruction (**r load 16-bit unsigned int *) - | Plhzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Plfi: freg -> float -> instruction (**r load float constant *) - | Plwz: ireg -> constant -> ireg -> instruction (**r load 32-bit int *) - | Plwzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Pmfcrbit: ireg -> crbit -> instruction (**r move condition bit to reg *) - | Pmflr: ireg -> instruction (**r move LR to reg *) - | Pmr: ireg -> ireg -> instruction (**r integer move *) - | Pmtctr: ireg -> instruction (**r move ireg to CTR *) - | Pmtlr: ireg -> instruction (**r move ireg to LR *) - | Pmulli: ireg -> ireg -> constant -> instruction (**r integer multiply immediate *) - | Pmullw: ireg -> ireg -> ireg -> instruction (**r integer multiply *) - | Pnand: ireg -> ireg -> ireg -> instruction (**r bitwise not-and *) - | Pnor: ireg -> ireg -> ireg -> instruction (**r bitwise not-or *) - | Por: ireg -> ireg -> ireg -> instruction (**r bitwise or *) - | Porc: ireg -> ireg -> ireg -> instruction (**r bitwise or-complement *) - | Pori: ireg -> ireg -> constant -> instruction (**r or with immediate *) - | Poris: ireg -> ireg -> constant -> instruction (**r or with immediate high *) - | Prlwinm: ireg -> ireg -> int -> int -> instruction (**r rotate and mask *) - | Pslw: ireg -> ireg -> ireg -> instruction (**r shift left *) - | Psraw: ireg -> ireg -> ireg -> instruction (**r shift right signed *) - | Psrawi: ireg -> ireg -> int -> instruction (**r shift right signed immediate *) - | Psrw: ireg -> ireg -> ireg -> instruction (**r shift right unsigned *) - | Pstb: ireg -> constant -> ireg -> instruction (**r store 8-bit int *) - | Pstbx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Pstfd: freg -> constant -> ireg -> instruction (**r store 64-bit float *) - | Pstfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Pstfs: freg -> constant -> ireg -> instruction (**r store 32-bit float *) - | Pstfsx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Psth: ireg -> constant -> ireg -> instruction (**r store 16-bit int *) - | Psthx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Pstw: ireg -> constant -> ireg -> instruction (**r store 32-bit int *) - | Pstwx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Psubfc: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction *) - | Psubfic: ireg -> ireg -> constant -> instruction (**r integer subtraction from immediate *) - | Pxor: ireg -> ireg -> ireg -> instruction (**r bitwise xor *) - | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) - | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) - | Plabel: label -> instruction. (**r define a code label *) - -(** 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 a signed 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 ->> -- [Pfctiu]: convert a float to an unsigned integer. The PowerPC way - to do this is to compare the argument against the floating-point - constant [2^31], subtract [2^31] if bigger, then convert to a signed - integer as above, then add back [2^31] if needed. Expands to: -<< - addis r2, 0, ha16(lbl1) - lfd f13, lo16(lbl1)(r2) - fcmpu cr7, rsrc, f13 - cror 30, 29, 30 - beq cr7, lbl2 - fctiwz f13, rsrc - stfdu f13, -8(r1) - lwz rdst, 4(r1) - b lbl3 -lbl2: fsub f13, rsrc, f13 - fctiwz f13, f13 - stfdu f13, -8(r1) - lwz rdst, 4(r1) - addis rdst, rdst, 0x8000 -lbl3: addi r1, r1, 8 - .const_data -lbl1: .long 0x41e00000, 0x00000000 # 2^31 in double precision - .text ->> -- [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 ofs]: 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 offset [ofs] - in 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], assuming that [ofs = 0]: -<< - 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 ofs]: in the formal semantics, this pseudo-instruction - reads the word at offset [ofs] in the block pointed by [r1] (the - stack pointer), frees this block, and sets [r1] to the value of the - word at offset [ofs]. In the printed PowerPC assembly code, this - freeing is just a load of register [r1] relative to [r1] itself: -<< - lwz r1, ofs(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 *) - | PC: preg (**r program counter *) - | LR: preg (**r link register (return address) *) - | CTR: preg (**r count register, used for some branches *) - | CARRY: preg (**r carry bit of the status register *) - | CR0_0: preg (**r bit 0 of the condition register *) - | CR0_1: preg (**r bit 1 of the condition register *) - | CR0_2: preg (**r bit 2 of the condition register *) - | CR0_3: preg. (**r bit 3 of the condition register *) - -Coercion IR: ireg >-> preg. -Coercion FR: freg >-> preg. - -Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_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 boolean registers ([CARRY], [CR0_0], etc) 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. - -(** Some PowerPC instructions treat register GPR0 as the integer literal 0 - when that register is used in argument position. *) - -Definition gpr_or_zero (rs: regset) (r: ireg) := - if ireg_eq r GPR0 then Vzero else rs#r. - -Variable ge: genv. - -Definition symbol_offset (id: ident) (ofs: int) : val := - match Genv.find_symbol ge id with - | Some b => Vptr b ofs - | None => Vundef - end. - -(** The four functions below axiomatize how the linker processes - symbolic references [symbol + offset] and splits their - actual values into two 16-bit halves. *) - -Parameter low_half: val -> val. -Parameter high_half: val -> val. - -(** The fundamental property of these operations is that, when applied - to the address of a symbol, their results can be recombined by - addition, rebuilding the original address. *) - -Axiom low_high_half: - forall id ofs, - Val.add (low_half (symbol_offset id ofs)) (high_half (symbol_offset id ofs)) - = symbol_offset 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. - -(** 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 - are shifted left by 16 bits, but not symbol addresses: - we assume (as in the [low_high_half] axioms above) - that the results of [high_half] are already shifted - (their 16 low bits are equal to 0). *) - -Definition const_low (c: constant) := - match c with - | Cint n => Vint n - | Csymbol_low id ofs => low_half (symbol_offset id ofs) - | Csymbol_high id ofs => Vundef - end. - -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 (symbol_offset id ofs) - end. - -(** 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. - -(** Auxiliaries for memory accesses, in two forms: one operand - (plus constant offset) or two operands. *) - -Definition load1 (chunk: memory_chunk) (rd: preg) - (cst: constant) (r1: ireg) (rs: regset) (m: mem) := - match Mem.loadv chunk m (Val.add (gpr_or_zero rs r1) (const_low cst)) with - | None => Error - | Some v => OK (nextinstr (rs#rd <- v)) m - end. - -Definition load2 (chunk: memory_chunk) (rd: preg) (r1 r2: ireg) - (rs: regset) (m: mem) := - match Mem.loadv chunk m (Val.add rs#r1 rs#r2) with - | None => Error - | Some v => OK (nextinstr (rs#rd <- v)) m - end. - -Definition store1 (chunk: memory_chunk) (r: preg) - (cst: constant) (r1: ireg) (rs: regset) (m: mem) := - match Mem.storev chunk m (Val.add (gpr_or_zero rs r1) (const_low cst)) (rs#r) with - | None => Error - | Some m' => OK (nextinstr rs) m' - end. - -Definition store2 (chunk: memory_chunk) (r: preg) (r1 r2: ireg) - (rs: regset) (m: mem) := - match Mem.storev chunk m (Val.add rs#r1 rs#r2) (rs#r) with - | None => Error - | Some m' => OK (nextinstr rs) m' - end. - -(** Operations over condition bits. *) - -Definition reg_of_crbit (bit: crbit) := - match bit with - | CRbit_0 => CR0_0 - | CRbit_1 => CR0_1 - | CRbit_2 => CR0_2 - | CRbit_3 => CR0_3 - end. - -Definition compare_sint (rs: regset) (v1 v2: val) := - rs#CR0_0 <- (Val.cmp Clt v1 v2) - #CR0_1 <- (Val.cmp Cgt v1 v2) - #CR0_2 <- (Val.cmp Ceq v1 v2) - #CR0_3 <- Vundef. - -Definition compare_uint (rs: regset) (v1 v2: val) := - rs#CR0_0 <- (Val.cmpu Clt v1 v2) - #CR0_1 <- (Val.cmpu Cgt v1 v2) - #CR0_2 <- (Val.cmpu Ceq v1 v2) - #CR0_3 <- Vundef. - -Definition compare_float (rs: regset) (v1 v2: val) := - rs#CR0_0 <- (Val.cmpf Clt v1 v2) - #CR0_1 <- (Val.cmpf Cgt v1 v2) - #CR0_2 <- (Val.cmpf Ceq v1 v2) - #CR0_3 <- Vundef. - -Definition val_cond_reg (rs: regset) := - Val.or (Val.shl rs#CR0_0 (Vint (Int.repr 31))) - (Val.or (Val.shl rs#CR0_1 (Vint (Int.repr 30))) - (Val.or (Val.shl rs#CR0_2 (Vint (Int.repr 29))) - (Val.shl rs#CR0_3 (Vint (Int.repr 28))))). - -(** 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 exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := - match i with - | Padd rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m - | Paddi rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m - | Paddis rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m - | Paddze rd r1 => - OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY))) m - | Pallocblock => - match rs#GPR3 with - | Vint n => - let (m', b) := Mem.alloc m 0 (Int.signed n) in - OK (nextinstr (rs#GPR3 <- (Vptr b Int.zero) - #LR <- (Val.add rs#PC Vone))) m' - | _ => Error - end - | Pallocframe lo hi ofs => - 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 ofs)) rs#GPR1 with - | None => Error - | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)) m2 - end - | Pand_ rd r1 r2 => - let v := Val.and rs#r1 rs#r2 in - OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m - | Pandc rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.and rs#r1 (Val.notint rs#r2)))) m - | Pandi_ rd r1 cst => - let v := Val.and rs#r1 (const_low cst) in - OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m - | Pandis_ rd r1 cst => - let v := Val.and rs#r1 (const_high cst) in - OK (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m - | Pb lbl => - goto_label c lbl rs m - | Pbctr => - OK (rs#PC <- (rs#CTR)) m - | Pbctrl => - OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m - | Pbf bit lbl => - match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then goto_label c lbl rs m else OK (nextinstr rs) m - | _ => Error - end - | Pbl ident => - OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m - | Pbs ident => - OK (rs#PC <- (symbol_offset ident Int.zero)) m - | Pblr => - OK (rs#PC <- (rs#LR)) m - | Pbt bit lbl => - match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then OK (nextinstr rs) m else goto_label c lbl rs m - | _ => Error - end - | Pcmplw r1 r2 => - OK (nextinstr (compare_uint rs rs#r1 rs#r2)) m - | Pcmplwi r1 cst => - OK (nextinstr (compare_uint rs rs#r1 (const_low cst))) m - | Pcmpw r1 r2 => - OK (nextinstr (compare_sint rs rs#r1 rs#r2)) m - | Pcmpwi r1 cst => - OK (nextinstr (compare_sint rs rs#r1 (const_low cst))) m - | Pcror bd b1 b2 => - OK (nextinstr (rs#(reg_of_crbit bd) <- (Val.or rs#(reg_of_crbit b1) rs#(reg_of_crbit b2)))) m - | Pdivw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.divs rs#r1 rs#r2))) m - | Pdivwu rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.divu rs#r1 rs#r2))) m - | Peqv rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m - | Pextsb rd r1 => - OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m - | Pextsh rd r1 => - OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m - | Pfreeframe ofs => - match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with - | None => Error - | Some v => - match rs#GPR1 with - | Vptr stk ofs => OK (nextinstr (rs#GPR1 <- v)) (Mem.free m stk) - | _ => Error - end - end - | Pfabs rd r1 => - OK (nextinstr (rs#rd <- (Val.absf rs#r1))) m - | Pfadd rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m - | Pfcmpu r1 r2 => - OK (nextinstr (compare_float rs rs#r1 rs#r2)) m - | Pfcti rd r1 => - OK (nextinstr (rs#rd <- (Val.intoffloat rs#r1) #FPR13 <- Vundef)) m - | Pfctiu rd r1 => - OK (nextinstr (rs#rd <- (Val.intuoffloat rs#r1) #FPR13 <- Vundef)) m - | Pfdiv rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m - | Pfmadd rd r1 r2 r3 => - OK (nextinstr (rs#rd <- (Val.addf (Val.mulf rs#r1 rs#r2) rs#r3))) m - | Pfmr rd r1 => - OK (nextinstr (rs#rd <- (rs#r1))) m - | Pfmsub rd r1 r2 r3 => - OK (nextinstr (rs#rd <- (Val.subf (Val.mulf rs#r1 rs#r2) rs#r3))) m - | Pfmul rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m - | Pfneg rd r1 => - OK (nextinstr (rs#rd <- (Val.negf rs#r1))) m - | Pfrsp rd r1 => - OK (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m - | Pfsub rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m - | Pictf rd r1 => - OK (nextinstr (rs#rd <- (Val.floatofint rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m - | Piuctf rd r1 => - OK (nextinstr (rs#rd <- (Val.floatofintu rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m - | Plbz rd cst r1 => - load1 Mint8unsigned rd cst r1 rs m - | Plbzx rd r1 r2 => - load2 Mint8unsigned rd r1 r2 rs m - | Plfd rd cst r1 => - load1 Mfloat64 rd cst r1 rs m - | Plfdx rd r1 r2 => - load2 Mfloat64 rd r1 r2 rs m - | Plfs rd cst r1 => - load1 Mfloat32 rd cst r1 rs m - | Plfsx rd r1 r2 => - load2 Mfloat32 rd r1 r2 rs m - | Plha rd cst r1 => - load1 Mint16signed rd cst r1 rs m - | Plhax rd r1 r2 => - load2 Mint16signed rd r1 r2 rs m - | Plhz rd cst r1 => - load1 Mint16unsigned rd cst r1 rs m - | Plhzx rd r1 r2 => - load2 Mint16unsigned rd r1 r2 rs m - | Plfi rd f => - OK (nextinstr (rs#rd <- (Vfloat f) #GPR12 <- Vundef)) m - | Plwz rd cst r1 => - load1 Mint32 rd cst r1 rs m - | Plwzx rd r1 r2 => - load2 Mint32 rd r1 r2 rs m - | Pmfcrbit rd bit => - OK (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m - | Pmflr rd => - OK (nextinstr (rs#rd <- (rs#LR))) m - | Pmr rd r1 => - OK (nextinstr (rs#rd <- (rs#r1))) m - | Pmtctr r1 => - OK (nextinstr (rs#CTR <- (rs#r1))) m - | Pmtlr r1 => - OK (nextinstr (rs#LR <- (rs#r1))) m - | Pmulli rd r1 cst => - OK (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m - | Pmullw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m - | Pnand rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m - | Pnor rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.notint (Val.or rs#r1 rs#r2)))) m - | Por rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.or rs#r1 rs#r2))) m - | Porc rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.or rs#r1 (Val.notint rs#r2)))) m - | Pori rd r1 cst => - OK (nextinstr (rs#rd <- (Val.or rs#r1 (const_low cst)))) m - | Poris rd r1 cst => - OK (nextinstr (rs#rd <- (Val.or rs#r1 (const_high cst)))) m - | Prlwinm rd r1 amount mask => - OK (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m - | Pslw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m - | Psraw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2) #CARRY <- (Val.shr_carry rs#r1 rs#r2))) m - | Psrawi rd r1 n => - OK (nextinstr (rs#rd <- (Val.shr rs#r1 (Vint n)) #CARRY <- (Val.shr_carry rs#r1 (Vint n)))) m - | Psrw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m - | Pstb rd cst r1 => - store1 Mint8unsigned rd cst r1 rs m - | Pstbx rd r1 r2 => - store2 Mint8unsigned rd r1 r2 rs m - | Pstfd rd cst r1 => - store1 Mfloat64 rd cst r1 rs m - | Pstfdx rd r1 r2 => - store2 Mfloat64 rd r1 r2 rs m - | Pstfs rd cst r1 => - store1 Mfloat32 rd cst r1 rs m - | Pstfsx rd r1 r2 => - store2 Mfloat32 rd r1 r2 rs m - | Psth rd cst r1 => - store1 Mint16unsigned rd cst r1 rs m - | Psthx rd r1 r2 => - store2 Mint16unsigned rd r1 r2 rs m - | Pstw rd cst r1 => - store1 Mint32 rd cst r1 rs m - | Pstwx rd r1 r2 => - store2 Mint32 rd r1 r2 rs m - | Psubfc rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) #CARRY <- Vundef)) m - | Psubfic rd r1 cst => - OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) #CARRY <- Vundef)) m - | Pxor rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m - | Pxori rd r1 cst => - OK (nextinstr (rs#rd <- (Val.xor rs#r1 (const_low cst)))) m - | Pxoris rd r1 cst => - OK (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m - | Plabel lbl => - OK (nextinstr rs) m - end. - -(** Calling conventions for external functions. These are compatible with - the calling conventions in module [Conventions], except that - we use PPC registers instead of locations. *) - -Inductive extcall_args (rs: regset) (m: mem): - list typ -> list ireg -> list freg -> Z -> list val -> Prop := - | extcall_args_nil: forall irl frl ofs, - extcall_args rs m nil irl frl ofs nil - | extcall_args_int_reg: forall tyl ir1 irl frl ofs v1 vl, - v1 = rs (IR ir1) -> - extcall_args rs m tyl irl frl ofs vl -> - extcall_args rs m (Tint :: tyl) (ir1 :: irl) frl ofs (v1 :: vl) - | extcall_args_int_stack: forall tyl frl ofs v1 vl, - Mem.loadv Mint32 m (Val.add (rs (IR GPR1)) (Vint (Int.repr ofs))) = Some v1 -> - extcall_args rs m tyl nil frl (ofs + 4) vl -> - extcall_args rs m (Tint :: tyl) nil frl ofs (v1 :: vl) - | extcall_args_float_reg: forall tyl irl fr1 frl ofs v1 vl, - v1 = rs (FR fr1) -> - extcall_args rs m tyl (list_drop2 irl) frl ofs vl -> - extcall_args rs m (Tfloat :: tyl) irl (fr1 :: frl) ofs (v1 :: vl) - | extcall_args_float_stack: forall tyl irl ofs v1 vl, - Mem.loadv Mfloat64 m (Val.add (rs (IR GPR1)) (Vint (Int.repr ofs))) = Some v1 -> - extcall_args rs m tyl irl nil (ofs + 8) vl -> - extcall_args rs m (Tfloat :: tyl) irl nil ofs (v1 :: vl). - -Definition extcall_arguments - (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - extcall_args rs m - sg.(sig_args) - (GPR3 :: GPR4 :: GPR5 :: GPR6 :: GPR7 :: GPR8 :: GPR9 :: GPR10 :: nil) - (FPR1 :: FPR2 :: FPR3 :: FPR4 :: FPR5 :: FPR6 :: FPR7 :: FPR8 :: FPR9 :: FPR10 :: nil) - 56 args. - -Definition loc_external_result (s: signature) : preg := - match s.(sig_res) with - | None => GPR3 - | Some Tint => GPR3 - | Some Tfloat => FPR1 - end. - -(** 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 LR)) -> - 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) - # LR <- Vzero - # GPR1 <- (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#GPR3 = 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. - -- cgit