From 2245717b5800da80371952999bc0cff5f75aa490 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 1 Jan 2009 12:47:42 +0000 Subject: 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 --- arm/Asm.v | 687 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 687 insertions(+) create mode 100644 arm/Asm.v (limited to 'arm/Asm.v') 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. -- cgit