diff options
| -rw-r--r-- | backend/Asmgenproof0.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asm.v | 164 | ||||
| -rw-r--r-- | mppa_k1c/Asmgen.v | 173 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 148 | ||||
| -rw-r--r-- | mppa_k1c/Conventions1.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Machregs.v | 9 |
6 files changed, 248 insertions, 254 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f6f03868..b1b7453a 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -39,12 +39,14 @@ Proof. unfold ireg_of; intros. destruct (preg_of r); inv H; auto. Qed. +(* FIXME - Replaced FR by IR for MPPA *) Lemma freg_of_eq: - forall r r', freg_of r = OK r' -> preg_of r = FR r'. + forall r r', freg_of r = OK r' -> preg_of r = IR r'. Proof. unfold freg_of; intros. destruct (preg_of r); inv H; auto. Qed. + Lemma preg_of_injective: forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. Proof. diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 4cd3b1fd..21e088fd 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -33,53 +33,43 @@ Require Import Conventions. (** * Abstract syntax *) -(** Integer registers. X0 is treated specially because it always reads - as zero and is never used as a destination of an instruction. *) - -Inductive ireg: Type := - | X1: ireg | X2: ireg | X3: ireg | X4: ireg | X5: ireg - | X6: ireg | X7: ireg | X8: ireg | X9: ireg | X10: ireg - | X11: ireg | X12: ireg | X13: ireg | X14: ireg | X15: ireg - | X16: ireg | X17: ireg | X18: ireg | X19: ireg | X20: ireg - | X21: ireg | X22: ireg | X23: ireg | X24: ireg | X25: ireg - | X26: ireg | X27: ireg | X28: ireg | X29: ireg | X30: ireg - | X31: ireg. - -Inductive ireg0: Type := - | X0: ireg0 | X: ireg -> ireg0. - -Coercion X: ireg >-> ireg0. - -(** Floating-point registers *) - -Inductive freg: Type := - | F0: freg | F1: freg | F2: freg | F3: freg - | F4: freg | F5: freg | F6: freg | F7: freg - | F8: freg | F9: freg | F10: freg | F11: freg - | F12: freg | F13: freg | F14: freg | F15: freg - | F16: freg | F17: freg | F18: freg | F19: freg - | F20: freg | F21: freg | F22: freg | F23: freg - | F24: freg | F25: freg | F26: freg | F27: freg - | F28: freg | F29: freg | F30: freg | F31: freg. +(** General Purpose registers. *) + +Inductive gpreg: Type := + | GPR0: gpreg | GPR1: gpreg | GPR2: gpreg | GPR3: gpreg | GPR4: gpreg + | GPR5: gpreg | GPR6: gpreg | GPR7: gpreg | GPR8: gpreg | GPR9: gpreg + | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg + | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg + | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg + | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg + | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg + | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg + | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg + | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg + | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg + | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg + | GPR60: gpreg | GPR61: gpreg | GPR62: gpreg | GPR63: gpreg. + +Definition ireg := gpreg. + +Definition freg := gpreg. Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. -Lemma ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. Defined. - Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. Proof. decide equality. Defined. - + (** We model the following registers of the RISC-V architecture. *) Inductive preg: Type := - | IR: ireg -> preg (**r integer registers *) - | FR: freg -> preg (**r double-precision float registers *) - | PC: preg. (**r program counter *) + | IR: gpreg -> preg (**r integer registers *) + | FR: gpreg -> preg (**r float registers *) + | RA: preg (**r return address *) + | PC: preg. (**r program counter *) -Coercion IR: ireg >-> preg. -Coercion FR: freg >-> preg. +Coercion IR: gpreg >-> preg. +Coercion FR: gpreg >-> preg. Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. Proof. decide equality. apply ireg_eq. apply freg_eq. Defined. @@ -93,8 +83,10 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]). *) -Notation "'SP'" := X2 (only parsing) : asm. -Notation "'RA'" := X1 (only parsing) : asm. +Notation "'SP'" := GPR12 (only parsing) : asm. + +(* FIXME - placeholder definitions to make sure the Risc-V instruction definitions work *) +Definition ireg0 := ireg. (** Offsets for load and store instructions. An offset is either an immediate integer or the low part of a symbol. *) @@ -139,6 +131,7 @@ Definition label := positive. [Asmgen]) is careful to respect this range. *) Inductive instruction : Type := +(* | Pmv (rd: ireg) (rs: ireg) (**r integer move *) (** 32-bit integer register-immediate instructions *) @@ -175,7 +168,7 @@ Inductive instruction : Type := | Psraw (rd: ireg) (rs1 rs2: ireg0) (**r shift-right-arith *) (** 64-bit integer register-immediate instructions *) - | Paddil (rd: ireg) (rs: ireg0) (imm: int64) (**r add immediate *) +*) | Paddil (rd: ireg) (rs: ireg0) (imm: int64) (**r add immediate *) (* | Psltil (rd: ireg) (rs: ireg0) (imm: int64) (**r set-less-than immediate *) | Psltiul (rd: ireg) (rs: ireg0) (imm: int64) (**r set-less-than unsigned immediate *) | Pandil (rd: ireg) (rs: ireg0) (imm: int64) (**r and immediate *) @@ -186,7 +179,7 @@ Inductive instruction : Type := | Psrail (rd: ireg) (rs: ireg0) (imm: int) (**r shift-right-arith immediate *) | Pluil (rd: ireg) (imm: int64) (**r load upper-immediate *) (** 64-bit integer register-register instructions *) - | Paddl (rd: ireg) (rs1 rs2: ireg0) (**r integer addition *) +*) | Paddl (rd: ireg) (rs1 rs2: ireg0) (**r integer addition *) (* | Psubl (rd: ireg) (rs1 rs2: ireg0) (**r integer subtraction *) | Pmull (rd: ireg) (rs1 rs2: ireg0) (**r integer multiply low *) @@ -213,8 +206,8 @@ Inductive instruction : Type := (* Unconditional jumps. Links are always to X1/RA. *) | Pj_l (l: label) (**r jump to label *) | Pj_s (symb: ident) (sg: signature) (**r jump to symbol *) - | Pj_r (r: ireg) (sg: signature) (**r jump register *) - | Pjal_s (symb: ident) (sg: signature) (**r jump-and-link symbol *) +*)| Pj_r (r: ireg) (sg: signature) (**r jump register *) +(*| Pjal_s (symb: ident) (sg: signature) (**r jump-and-link symbol *) | Pjal_r (r: ireg) (sg: signature) (**r jump-and-link register *) (* Conditional branches, 32-bit comparisons *) @@ -332,20 +325,20 @@ Inductive instruction : Type := | Pfcvtds (rd: freg) (rs: freg) (**r float32 -> float *) | Pfcvtsd (rd: freg) (rs: freg) (**r float -> float32 *) - +*) (* Pseudo-instructions *) | Pallocframe (sz: Z) (pos: ptrofs) (**r allocate new stack frame *) | Pfreeframe (sz: Z) (pos: ptrofs) (**r deallocate stack frame and restore previous frame *) | Plabel (lbl: label) (**r define a code label *) - | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *) +(* | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *) | Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *) | Ploadli (rd: ireg) (i: int64) (**r load an immediate int64 *) | Ploadfi (rd: freg) (f: float) (**r load an immediate float *) | Ploadsi (rd: freg) (f: float32) (**r load an immediate single *) - | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) + | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) | Pbuiltin: external_function -> list (builtin_arg preg) - -> builtin_res preg -> instruction. (**r built-in function (pseudo) *) - + -> builtin_res preg -> instruction. (**r built-in function (pseudo) *) (* +*) (** The pseudo-instructions are the following: @@ -441,13 +434,11 @@ Definition genv := Genv.t fundef unit. Definition get0w (rs: regset) (r: ireg0) : val := match r with | X0 => Vint Int.zero - | X r => rs r end. Definition get0l (rs: regset) (r: ireg0) : val := match r with | X0 => Vlong Int64.zero - | X r => rs r end. Notation "a # b" := (a b) (at level 1, only parsing) : asm. @@ -612,7 +603,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := match i with - | Pmv d s => +(* | Pmv d s => Next (nextinstr (rs#d <- (rs#s))) m (** 32-bit integer register-immediate instructions *) @@ -678,9 +669,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.shr rs##s1 rs##s2))) m (** 64-bit integer register-immediate instructions *) - | Paddil d s i => +*)| Paddil d s i => Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m - | Psltil d s i => +(*| Psltil d s i => Next (nextinstr (rs#d <- (Val.maketotal (Val.cmpl Clt rs###s (Vlong i))))) m | Psltiul d s i => Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt rs###s (Vlong i))))) m @@ -700,9 +691,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Vlong (Int64.sign_ext 32 (Int64.shl i (Int64.repr 12)))))) m (** 64-bit integer register-register instructions *) - | Paddl d s1 s2 => +*)| Paddl d s1 s2 => Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m - | Psubl d s1 s2 => +(*| Psubl d s1 s2 => Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m | Pmull d s1 s2 => Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m @@ -749,9 +740,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out goto_label f l rs m | Pj_s s sg => Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m - | Pj_r r sg => +*)| Pj_r r sg => Next (rs#PC <- (rs#r)) m - | Pjal_s s sg => +(*| Pjal_s s sg => Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero) #RA <- (Val.offset_ptr rs#PC Ptrofs.one) ) m @@ -919,12 +910,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.singleoffloat rs#s))) m (** Pseudo-instructions *) - | Pallocframe sz pos => +*)| Pallocframe sz pos => let (m1, stk) := Mem.alloc m 0 sz in let sp := (Vptr stk Ptrofs.zero) in match Mem.storev Mptr m1 (Val.offset_ptr sp pos) rs#SP with | None => Stuck - | Some m2 => Next (nextinstr (rs #X30 <- (rs SP) #SP <- sp #X31 <- Vundef)) m2 + | Some m2 => Next (nextinstr (rs #GPR30 <- (rs SP) #SP <- sp #GPR31 <- Vundef)) m2 end | Pfreeframe sz pos => match Mem.loadv Mptr m (Val.offset_ptr rs#SP pos) with @@ -934,38 +925,38 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Vptr stk ofs => match Mem.free m stk 0 sz with | None => Stuck - | Some m' => Next (nextinstr (rs#SP <- v #X31 <- Vundef)) m' + | Some m' => Next (nextinstr (rs#SP <- v #GPR31 <- Vundef)) m' end | _ => Stuck end end | Plabel lbl => Next (nextinstr rs) m - | Ploadsymbol rd s ofs => +(*| Ploadsymbol rd s ofs => Next (nextinstr (rs#rd <- (Genv.symbol_address ge s ofs))) m | Ploadsymbol_high rd s ofs => Next (nextinstr (rs#rd <- (high_half ge s ofs))) m | Ploadli rd i => - Next (nextinstr (rs#X31 <- Vundef #rd <- (Vlong i))) m + Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vlong i))) m | Ploadfi rd f => - Next (nextinstr (rs#X31 <- Vundef #rd <- (Vfloat f))) m + Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vfloat f))) m | Ploadsi rd f => - Next (nextinstr (rs#X31 <- Vundef #rd <- (Vsingle f))) m + Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vsingle f))) m | Pbtbl r tbl => match rs r with | Vint n => match list_nth_z tbl (Int.unsigned n) with | None => Stuck - | Some lbl => goto_label f lbl (rs#X5 <- Vundef #X31 <- Vundef) m + | Some lbl => goto_label f lbl (rs#GPR5 <- Vundef #GPR31 <- Vundef) m end | _ => Stuck end - | Pbuiltin ef args res => +*)| Pbuiltin ef args res => Stuck (**r treated specially below *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) - | Pfence +(*| Pfence | Pfmvxs _ _ | Pfmvxd _ _ @@ -986,31 +977,29 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfnmaddd _ _ _ _ | Pfnmsubd _ _ _ _ => Stuck - end. +*)end. (** Translation of the LTL/Linear/Mach view of machine registers to the RISC-V view. Note that no LTL register maps to [X31]. This register is reserved as temporary, to be used by the generated RV32G code. *) + (* FIXME - R31 is not there *) Definition preg_of (r: mreg) : preg := match r with - | R5 => X5 | R6 => X6 | R7 => X7 - | R8 => X8 | R9 => X9 | R10 => X10 | R11 => X11 - | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15 - | R16 => X16 | R17 => X17 | R18 => X18 | R19 => X19 - | R20 => X20 | R21 => X21 | R22 => X22 | R23 => X23 - | R24 => X24 | R25 => X25 | R26 => X26 | R27 => X27 - | R28 => X28 | R29 => X29 | R30 => X30 - - | Machregs.F0 => F0 | Machregs.F1 => F1 | Machregs.F2 => F2 | Machregs.F3 => F3 - | Machregs.F4 => F4 | Machregs.F5 => F5 | Machregs.F6 => F6 | Machregs.F7 => F7 - | Machregs.F8 => F8 | Machregs.F9 => F9 | Machregs.F10 => F10 | Machregs.F11 => F11 - | Machregs.F12 => F12 | Machregs.F13 => F13 | Machregs.F14 => F14 | Machregs.F15 => F15 - | Machregs.F16 => F16 | Machregs.F17 => F17 | Machregs.F18 => F18 | Machregs.F19 => F19 - | Machregs.F20 => F20 | Machregs.F21 => F21 | Machregs.F22 => F22 | Machregs.F23 => F23 - | Machregs.F24 => F24 | Machregs.F25 => F25 | Machregs.F26 => F26 | Machregs.F27 => F27 - | Machregs.F28 => F28 | Machregs.F29 => F29 | Machregs.F30 => F30 | Machregs.F31 => F31 + | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4 + | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9 +(*| R10 => GPR10 | R11 => GPR11 | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *) + | R15 => GPR15 | R16 => GPR16 | R17 => GPR17 | R18 => GPR18 | R19 => GPR19 + | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 + | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 + | R30 => GPR30 | R32 => GPR32 | R33 => GPR33 | R34 => GPR34 + | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39 => GPR39 + | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44 => GPR44 + | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49 => GPR49 + | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54 => GPR54 + | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59 => GPR59 + | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63 end. (** Extract the values of the arguments of an external call. @@ -1065,7 +1054,7 @@ Inductive step: state -> trace -> state -> Prop := rs' = nextinstr (set_res res vres (undef_regs (map preg_of (destroyed_by_builtin ef)) - (rs#X31 <- Vundef))) -> + (rs#GPR31 <- Vundef))) -> step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', @@ -1094,7 +1083,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, rs PC = Vnullptr -> - rs X10 = Vint r -> + rs GPR9 = Vint r -> final_state (State rs m) r. Definition semantics (p: program) := @@ -1164,8 +1153,7 @@ Qed. Definition data_preg (r: preg) : bool := match r with - | IR RA => false - | IR X31 => false + | RA => false | IR _ => true | FR _ => true | PC => false diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index a704ed74..72822f70 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -37,8 +37,9 @@ Definition ireg_of (r: mreg) : res ireg := match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end. Definition freg_of (r: mreg) : res freg := - match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. +(* (** Decomposition of 32-bit integer constants. They are split into either small signed immediates that fit in 12-bits, or, if they do not fit, into a (20-bit hi, 12-bit lo) pair where lo is sign-extended. *) @@ -61,7 +62,7 @@ Definition make_immed32 (val: int) := *) (** Likewise, for 64-bit integer constants. *) - +*) Inductive immed64 : Type := | Imm64_single (imm: int64) | Imm64_pair (hi: int64) (lo: int64) @@ -74,7 +75,7 @@ Definition make_immed64 (val: int64) := if Int64.eq val (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo) then Imm64_pair hi lo else Imm64_large val. - +(* (** Smart constructors for arithmetic operations involving a 32-bit or 64-bit integer constant. Depending on whether the constant fits in 12 bits or not, one or several instructions @@ -87,7 +88,7 @@ Definition load_hilo32 (r: ireg) (hi lo: int) k := Definition loadimm32 (r: ireg) (n: int) (k: code) := match make_immed32 n with - | Imm32_single imm => Paddiw r X0 imm :: k + | Imm32_single imm => Paddiw r GPR0 imm :: k | Imm32_pair hi lo => load_hilo32 r hi lo k end. @@ -96,7 +97,7 @@ Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction) (rd rs: ireg) (n: int) (k: code) := match make_immed32 n with | Imm32_single imm => opimm rd rs imm :: k - | Imm32_pair hi lo => load_hilo32 X31 hi lo (op rd rs X31 :: k) + | Imm32_pair hi lo => load_hilo32 GPR31 hi lo (op rd rs GPR31 :: k) end. Definition addimm32 := opimm32 Paddw Paddiw. @@ -109,24 +110,26 @@ Definition sltuimm32 := opimm32 Psltuw Psltiuw. Definition load_hilo64 (r: ireg) (hi lo: int64) k := if Int64.eq lo Int64.zero then Pluil r hi :: k else Pluil r hi :: Paddil r r lo :: k. - + Definition loadimm64 (r: ireg) (n: int64) (k: code) := match make_immed64 n with - | Imm64_single imm => Paddil r X0 imm :: k + | Imm64_single imm => Paddil r GPR0 imm :: k | Imm64_pair hi lo => load_hilo64 r hi lo k | Imm64_large imm => Ploadli r imm :: k end. - +*) Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction) (opimm: ireg -> ireg0 -> int64 -> instruction) (rd rs: ireg) (n: int64) (k: code) := match make_immed64 n with | Imm64_single imm => opimm rd rs imm :: k - | Imm64_pair hi lo => load_hilo64 X31 hi lo (op rd rs X31 :: k) - | Imm64_large imm => Ploadli X31 imm :: op rd rs X31 :: k +(*| Imm64_pair hi lo => load_hilo64 GPR31 hi lo (op rd rs GPR31 :: k) + | Imm64_large imm => Ploadli GPR31 imm :: op rd rs GPR31 :: k +*)| _ => nil end. Definition addimm64 := opimm64 Paddl Paddil. +(* Definition andimm64 := opimm64 Pandl Pandil. Definition orimm64 := opimm64 Porl Poril. Definition xorimm64 := opimm64 Pxorl Pxoril. @@ -215,15 +218,15 @@ Definition transl_cbranch | Ccompimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int.eq n Int.zero then - transl_cbranch_int32s c r1 X0 lbl :: k + transl_cbranch_int32s c r1 GPR0 lbl :: k else - loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k)) + loadimm32 GPR31 n (transl_cbranch_int32s c r1 GPR31 lbl :: k)) | Ccompuimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int.eq n Int.zero then - transl_cbranch_int32u c r1 X0 lbl :: k + transl_cbranch_int32u c r1 GPR0 lbl :: k else - loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k)) + loadimm32 GPR31 n (transl_cbranch_int32u c r1 GPR31 lbl :: k)) | Ccompl c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cbranch_int64s c r1 r2 lbl :: k) @@ -233,31 +236,31 @@ Definition transl_cbranch | Ccomplimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int64.eq n Int64.zero then - transl_cbranch_int64s c r1 X0 lbl :: k + transl_cbranch_int64s c r1 GPR0 lbl :: k else - loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k)) + loadimm64 GPR31 n (transl_cbranch_int64s c r1 GPR31 lbl :: k)) | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if Int64.eq n Int64.zero then - transl_cbranch_int64u c r1 X0 lbl :: k + transl_cbranch_int64u c r1 GPR0 lbl :: k else - loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k)) + loadimm64 GPR31 n (transl_cbranch_int64u c r1 GPR31 lbl :: k)) | Ccompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_float c GPR31 r1 r2 in + OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k) | Cnotcompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_float c GPR31 r1 r2 in + OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k) | Ccompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_single c GPR31 r1 r2 in + OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k) | Cnotcompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) + let (insn, normal) := transl_cond_single c GPR31 r1 r2 in + OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k) | _, _ => Error(msg "Asmgen.transl_cond_branch") end. @@ -307,45 +310,46 @@ Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: co end. Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else + if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 GPR0 k else match cmp with - | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k) + | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd GPR0 k) | Clt => sltimm32 rd r1 n k | Cle => if Int.eq n (Int.repr Int.max_signed) then loadimm32 rd Int.one k else sltimm32 rd r1 (Int.add n Int.one) k - | _ => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k) + | _ => loadimm32 GPR31 n (transl_cond_int32s cmp rd r1 GPR31 k) end. Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else + if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 GPR0 k else match cmp with | Clt => sltuimm32 rd r1 n k - | _ => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k) + | _ => loadimm32 GPR31 n (transl_cond_int32u cmp rd r1 GPR31 k) end. Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else + if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 GPR0 k else match cmp with - | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k) + | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd GPR0 k) | Clt => sltimm64 rd r1 n k | Cle => if Int64.eq n (Int64.repr Int64.max_signed) then loadimm32 rd Int.one k else sltimm64 rd r1 (Int64.add n Int64.one) k - | _ => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k) + | _ => loadimm64 GPR31 n (transl_cond_int64s cmp rd r1 GPR31 k) end. Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else + if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 GPR0 k else match cmp with | Clt => sltuimm64 rd r1 n k - | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) + | _ => loadimm64 GPR31 n (transl_cond_int64u cmp rd r1 GPR31 k) end. +*) Definition transl_cond_op - (cond: condition) (rd: ireg) (args: list mreg) (k: code) := + (cond: condition) (rd: ireg) (args: list mreg) (k: code) : res (list instruction) := match cond, args with - | Ccomp c, a1 :: a2 :: nil => +(*| Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cond_int32s c rd r1 r2 k) | Ccompu c, a1 :: a2 :: nil => @@ -385,7 +389,7 @@ Definition transl_cond_op do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_single c rd r1 r2 in OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | _, _ => +*)| _, _ => Error(msg "Asmgen.transl_cond_op") end. @@ -395,10 +399,9 @@ Definition transl_cond_op Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with - | Omove, a1 :: nil => +(*| Omove, a1 :: nil => match preg_of res, preg_of a1 with | IR r, IR a => OK (Pmv r a :: k) - | FR r, FR a => OK (Pfmv r a :: k) | _ , _ => Error(msg "Asmgen.Omove") end | Ointconst n, nil => @@ -410,12 +413,12 @@ Definition transl_op | Ofloatconst f, nil => do rd <- freg_of res; OK (if Float.eq_dec f Float.zero - then Pfcvtdw rd X0 :: k + then Pfcvtdw rd GPR0 :: k else Ploadfi rd f :: k) | Osingleconst f, nil => do rd <- freg_of res; OK (if Float32.eq_dec f Float32.zero - then Pfcvtsw rd X0 :: k + then Pfcvtsw rd GPR0 :: k else Ploadsi rd f :: k) | Oaddrsymbol s ofs, nil => do rd <- ireg_of res; @@ -440,7 +443,7 @@ Definition transl_op OK (addimm32 rd rs n k) | Oneg, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (Psubw rd X0 rs :: k) + OK (Psubw rd GPR0 rs :: k) | Osub, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubw rd rs1 rs2 :: k) @@ -504,10 +507,10 @@ Definition transl_op | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psraiw X31 rs (Int.repr 31) :: - Psrliw X31 X31 (Int.sub Int.iwordsize n) :: - Paddw X31 rs X31 :: - Psraiw rd X31 n :: k) + Psraiw GPR31 rs (Int.repr 31) :: + Psrliw GPR31 GPR31 (Int.sub Int.iwordsize n) :: + Paddw GPR31 rs GPR31 :: + Psraiw rd GPR31 n :: k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => @@ -521,15 +524,15 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; assertion (ireg_eq rd rs); OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k) - | Oaddl, a1 :: a2 :: nil => +*)| Oaddl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Paddl rd rs1 rs2 :: k) | Oaddlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (addimm64 rd rs n k) - | Onegl, a1 :: nil => +(*| Onegl, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (Psubl rd X0 rs :: k) + OK (Psubl rd GPR0 rs :: k) | Osubl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubl rd rs1 rs2 :: k) @@ -593,10 +596,10 @@ Definition transl_op | Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psrail X31 rs (Int.repr 63) :: - Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: - Paddl X31 rs X31 :: - Psrail rd X31 n :: k) + Psrail GPR31 rs (Int.repr 63) :: + Psrlil GPR31 GPR31 (Int.sub Int64.iwordsize' n) :: + Paddl GPR31 rs GPR31 :: + Psrail rd GPR31 n :: k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; @@ -696,13 +699,13 @@ Definition transl_op | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k - +*) | _, _ => Error(msg "Asmgen.transl_op") end. (** Accessing data in the stack frame. *) - +(* Definition indexed_memory_access (mk_instr: ireg -> offset -> instruction) (base: ireg) (ofs: ptrofs) (k: code) := @@ -711,27 +714,26 @@ Definition indexed_memory_access | Imm64_single imm => mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) :: k | Imm64_pair hi lo => - Pluil X31 hi :: Paddl X31 base X31 :: mk_instr X31 (Ofsimm (Ptrofs.of_int64 lo)) :: k + Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k | Imm64_large imm => - Ploadli X31 imm :: Paddl X31 base X31 :: mk_instr X31 (Ofsimm Ptrofs.zero) :: k + Ploadli GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k end else match make_immed32 (Ptrofs.to_int ofs) with | Imm32_single imm => mk_instr base (Ofsimm (Ptrofs.of_int imm)) :: k | Imm32_pair hi lo => - Pluiw X31 hi :: Paddw X31 base X31 :: mk_instr X31 (Ofsimm (Ptrofs.of_int lo)) :: k + Pluiw GPR31 hi :: Paddw GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int lo)) :: k end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := match ty, preg_of dst with | Tint, IR rd => OK (indexed_memory_access (Plw rd) base ofs k) | Tlong, IR rd => OK (indexed_memory_access (Pld rd) base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pfls rd) base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pfld rd) base ofs k) + | Tsingle, IR rd => OK (indexed_memory_access (Pfls rd) base ofs k) + | Tfloat, IR rd => OK (indexed_memory_access (Pfld rd) base ofs k) | Tany32, IR rd => OK (indexed_memory_access (Plw_a rd) base ofs k) | Tany64, IR rd => OK (indexed_memory_access (Pld_a rd) base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pfld_a rd) base ofs k) | _, _ => Error (msg "Asmgen.loadind") end. @@ -739,11 +741,10 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : match ty, preg_of src with | Tint, IR rd => OK (indexed_memory_access (Psw rd) base ofs k) | Tlong, IR rd => OK (indexed_memory_access (Psd rd) base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pfss rd) base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pfsd rd) base ofs k) + | Tsingle, IR rd => OK (indexed_memory_access (Pfss rd) base ofs k) + | Tfloat, IR rd => OK (indexed_memory_access (Pfsd rd) base ofs k) | Tany32, IR rd => OK (indexed_memory_access (Psw_a rd) base ofs k) | Tany64, IR rd => OK (indexed_memory_access (Psd_a rd) base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pfsd_a rd) base ofs k) | _, _ => Error (msg "Asmgen.storeind") end. @@ -752,28 +753,28 @@ Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) := Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) (k: code) := indexed_memory_access (if Archi.ptr64 then Psd src else Psw src) base ofs k. - +*) (** Translation of memory accesses: loads, and stores. *) Definition transl_memory_access (mk_instr: ireg -> offset -> instruction) - (addr: addressing) (args: list mreg) (k: code) := + (addr: addressing) (args: list mreg) (k: code) : res (list instruction) := match addr, args with - | Aindexed ofs, a1 :: nil => +(*| Aindexed ofs, a1 :: nil => do rs <- ireg_of a1; OK (indexed_memory_access mk_instr rs ofs k) | Aglobal id ofs, nil => - OK (Ploadsymbol_high X31 id ofs :: mk_instr X31 (Ofslow id ofs) :: k) + OK (Ploadsymbol_high GPR31 id ofs :: mk_instr GPR31 (Ofslow id ofs) :: k) | Ainstack ofs, nil => OK (indexed_memory_access mk_instr SP ofs k) - | _, _ => +*)| _, _ => Error(msg "Asmgen.transl_memory_access") end. Definition transl_load (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (dst: mreg) (k: code) := + (args: list mreg) (dst: mreg) (k: code) : res (list instruction) := match chunk with - | Mint8signed => +(*| Mint8signed => do r <- ireg_of dst; transl_memory_access (Plb r) addr args k | Mint8unsigned => @@ -797,14 +798,14 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) | Mfloat64 => do r <- freg_of dst; transl_memory_access (Pfld r) addr args k - | _ => +*)| _ => Error (msg "Asmgen.transl_load") end. Definition transl_store (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (src: mreg) (k: code) := + (args: list mreg) (src: mreg) (k: code) : res (list instruction) := match chunk with - | Mint8signed | Mint8unsigned => +(*| Mint8signed | Mint8unsigned => do r <- ireg_of src; transl_memory_access (Psb r) addr args k | Mint16signed | Mint16unsigned => @@ -822,7 +823,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) | Mfloat64 => do r <- freg_of src; transl_memory_access (Pfsd r) addr args k - | _ => +*)| _ => Error (msg "Asmgen.transl_store") end. @@ -837,18 +838,18 @@ Definition make_epilogue (f: Mach.function) (k: code) := Definition transl_instr (f: Mach.function) (i: Mach.instruction) (ep: bool) (k: code) := match i with - | Mgetstack ofs ty dst => +(*| Mgetstack ofs ty dst => loadind SP ofs ty dst k | Msetstack src ofs ty => storeind src SP ofs ty k | Mgetparam ofs ty dst => (* load via the frame pointer if it is valid *) - do c <- loadind X30 ofs ty dst k; + do c <- loadind GPR30 ofs ty dst k; OK (if ep then c - else loadind_ptr SP f.(fn_link_ofs) X30 c) - | Mop op args res => + else loadind_ptr SP f.(fn_link_ofs) GPR30 c) +*)| Mop op args res => transl_op op args res k - | Mload chunk addr args dst => +(*| Mload chunk addr args dst => transl_load chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k @@ -861,19 +862,21 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (make_epilogue f (Pj_r r1 sig :: k)) | Mtailcall sig (inr symb) => OK (make_epilogue f (Pj_s symb sig :: k)) - | Mbuiltin ef args res => +*)| Mbuiltin ef args res => OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) | Mlabel lbl => OK (Plabel lbl :: k) - | Mgoto lbl => +(*| Mgoto lbl => OK (Pj_l lbl :: k) | Mcond cond args lbl => transl_cbranch cond args lbl k | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k) - | Mreturn => +*)| Mreturn => OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k)) + | _ => + Error (msg "Asmgen.transl_instr") end. (** Translation of a code sequence *) diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 8bbdbd4c..0a67466a 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -76,19 +76,19 @@ Qed. (** Properties of registers *) -Lemma ireg_of_not_X31: - forall m r, ireg_of m = OK r -> IR r <> IR X31. +Lemma ireg_of_not_GPR31: + forall m r, ireg_of m = OK r -> IR r <> IR GPR31. Proof. - intros. erewrite <- ireg_of_eq; eauto with asmgen. + intros. erewrite <- ireg_of_eq; eauto with asmgen. destruct m; unfold preg_of; discriminate. Qed. -Lemma ireg_of_not_X31': - forall m r, ireg_of m = OK r -> r <> X31. +Lemma ireg_of_not_GPR31': + forall m r, ireg_of m = OK r -> r <> GPR31. Proof. - intros. apply ireg_of_not_X31 in H. congruence. + intros. apply ireg_of_not_GPR31 in H. congruence. Qed. -Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen. +Hint Resolve ireg_of_not_GPR31 ireg_of_not_GPR31': asmgen. (** Useful simplification tactic *) @@ -154,18 +154,18 @@ Lemma opimm32_correct: (forall d s n rs, exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs##s (Vint n)))) m) -> forall rd r1 n k rs, - r1 <> X31 -> + r1 <> GPR31 -> exists rs', exec_straight ge fn (opimm32 op opi rd r1 n k) rs m k rs' m /\ rs'#rd = sem rs##r1 (Vint n) - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. unfold opimm32. generalize (make_immed32_sound n); intros E. destruct (make_immed32 n). - subst imm. econstructor; split. apply exec_straight_one. rewrite H0. simpl; eauto. auto. split. Simpl. intros; Simpl. -- destruct (load_hilo32_correct X31 hi lo (op rd r1 X31 :: k) rs m) +- destruct (load_hilo32_correct GPR31 hi lo (op rd r1 GPR31 :: k) rs m) as (rs' & A & B & C). econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. @@ -200,7 +200,7 @@ Lemma loadimm64_correct: exists rs', exec_straight ge fn (loadimm64 rd n k) rs m k rs' m /\ rs'#rd = Vlong n - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. unfold loadimm64; intros. generalize (make_immed64_sound n); intros E. destruct (make_immed64 n). @@ -225,18 +225,18 @@ Lemma opimm64_correct: (forall d s n rs, exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs###s (Vlong n)))) m) -> forall rd r1 n k rs, - r1 <> X31 -> + r1 <> GPR31 -> exists rs', exec_straight ge fn (opimm64 op opi rd r1 n k) rs m k rs' m /\ rs'#rd = sem rs##r1 (Vlong n) - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. unfold opimm64. generalize (make_immed64_sound n); intros E. destruct (make_immed64 n). - subst imm. econstructor; split. apply exec_straight_one. rewrite H0. simpl; eauto. auto. split. Simpl. intros; Simpl. -- destruct (load_hilo64_correct X31 hi lo (op rd r1 X31 :: k) rs m) +- destruct (load_hilo64_correct GPR31 hi lo (op rd r1 GPR31 :: k) rs m) as (rs' & A & B & C). econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. @@ -252,11 +252,11 @@ Qed. Lemma addptrofs_correct: forall rd r1 n k rs m, - r1 <> X31 -> + r1 <> GPR31 -> exists rs', exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m /\ Val.lessdef (Val.offset_ptr rs#r1 n) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. unfold addptrofs; intros. destruct (Ptrofs.eq_dec n Ptrofs.zero). @@ -279,11 +279,11 @@ Qed. Lemma addptrofs_correct_2: forall rd r1 n k (rs: regset) m b ofs, - r1 <> X31 -> rs#r1 = Vptr b ofs -> + r1 <> GPR31 -> rs#r1 = Vptr b ofs -> exists rs', exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m /\ rs'#rd = Vptr b (Ptrofs.add ofs n) - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. exploit (addptrofs_correct rd r1 n); eauto. intros (rs' & A & B & C). exists rs'; intuition eauto. @@ -377,10 +377,10 @@ Proof. rewrite <- Float32.cmp_swap. auto. Qed. -Remark branch_on_X31: +Remark branch_on_GPR31: forall normal lbl (rs: regset) m b, - rs#X31 = Val.of_bool (eqb normal b) -> - exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = + rs#GPR31 = Val.of_bool (eqb normal b) -> + exec_instr ge fn (if normal then Pbnew GPR31 X0 lbl else Pbeqw GPR31 X0 lbl) rs m = eval_branch fn lbl rs m (Some b). Proof. intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. @@ -425,7 +425,7 @@ Lemma transl_cbranch_correct_1: exists rs', exists insn, exec_straight_opt c rs m' (insn :: k) rs' m' /\ exec_instr ge fn insn rs' m' = eval_branch fn lbl rs' m' (Some b) - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until m'; intros TRANSL EVAL AG MEXT. set (vl' := map rs (map preg_of args)). @@ -440,16 +440,16 @@ Proof. - predSpec Int.eq Int.eq_spec n Int.zero. + subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl). intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32s c0 x X31 lbl). ++ exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C). + exists rs', (transl_cbranch_int32s c0 x GPR31 lbl). split. constructor; eexact A. split; auto. apply transl_cbranch_int32s_correct; auto. simpl; rewrite B, C; eauto with asmgen. - predSpec Int.eq Int.eq_spec n Int.zero. + subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl). intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32u c0 x X31 lbl). ++ exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C). + exists rs', (transl_cbranch_int32u c0 x GPR31 lbl). split. constructor; eexact A. split; auto. apply transl_cbranch_int32u_correct; auto. simpl; rewrite B, C; eauto with asmgen. @@ -460,20 +460,20 @@ Proof. - predSpec Int64.eq Int64.eq_spec n Int64.zero. + subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl). intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64s c0 x X31 lbl). ++ exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C). + exists rs', (transl_cbranch_int64s c0 x GPR31 lbl). split. constructor; eexact A. split; auto. apply transl_cbranch_int64s_correct; auto. simpl; rewrite B, C; eauto with asmgen. - predSpec Int64.eq Int64.eq_spec n Int64.zero. + subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl). intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64u c0 x X31 lbl). ++ exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C). + exists rs', (transl_cbranch_int64u c0 x GPR31 lbl). split. constructor; eexact A. split; auto. apply transl_cbranch_int64u_correct; auto. simpl; rewrite B, C; eauto with asmgen. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. +- destruct (transl_cond_float c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). assert (V: v = Val.of_bool (eqb normal b)). { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. } @@ -481,7 +481,7 @@ Proof. split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. intros; Simpl. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. +- destruct (transl_cond_float c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)). { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). @@ -491,7 +491,7 @@ Proof. split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. +- destruct (transl_cond_single c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). assert (V: v = Val.of_bool (eqb normal b)). { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. } @@ -499,7 +499,7 @@ Proof. split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. +- destruct (transl_cond_single c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2. assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)). { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). @@ -520,7 +520,7 @@ Lemma transl_cbranch_correct_true: exists rs', exists insn, exec_straight_opt c rs m' (insn :: k) rs' m' /\ exec_instr ge fn insn rs' m' = goto_label fn lbl rs' m' - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. eapply transl_cbranch_correct_1 with (b := true); eauto. Qed. @@ -533,7 +533,7 @@ Lemma transl_cbranch_correct_false: Mem.extends m m' -> exists rs', exec_straight ge fn c rs m' k rs' m' - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. exploit transl_cbranch_correct_1; eauto. simpl. intros (rs' & insn & A & B & C). @@ -654,11 +654,11 @@ Qed. Lemma transl_condimm_int32s_correct: forall cmp rd r1 n k rs m, - r1 <> X31 -> + r1 <> GPR31 -> exists rs', exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. unfold transl_condimm_int32s. predSpec Int.eq Int.eq_spec n Int.zero. @@ -666,9 +666,9 @@ Proof. exists rs'; eauto. - assert (DFL: exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m + exec_straight ge fn (loadimm32 GPR31 n (transl_cond_int32s cmp rd r1 GPR31 k)) rs m k rs' m /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r). { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). exists rs2; split. @@ -718,11 +718,11 @@ Qed. Lemma transl_condimm_int32u_correct: forall cmp rd r1 n k rs m, - r1 <> X31 -> + r1 <> GPR31 -> exists rs', exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. unfold transl_condimm_int32u. predSpec Int.eq Int.eq_spec n Int.zero. @@ -730,9 +730,9 @@ Proof. exists rs'; split. eexact A. split; auto. rewrite B; auto. - assert (DFL: exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m + exec_straight ge fn (loadimm32 GPR31 n (transl_cond_int32u cmp rd r1 GPR31 k)) rs m k rs' m /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r). { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2). exists rs2; split. @@ -752,11 +752,11 @@ Qed. Lemma transl_condimm_int64s_correct: forall cmp rd r1 n k rs m, - r1 <> X31 -> + r1 <> GPR31 -> exists rs', exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. unfold transl_condimm_int64s. predSpec Int64.eq Int64.eq_spec n Int64.zero. @@ -764,9 +764,9 @@ Proof. exists rs'; eauto. - assert (DFL: exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m + exec_straight ge fn (loadimm64 GPR31 n (transl_cond_int64s cmp rd r1 GPR31 k)) rs m k rs' m /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r). { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). exists rs2; split. @@ -816,11 +816,11 @@ Qed. Lemma transl_condimm_int64u_correct: forall cmp rd r1 n k rs m, - r1 <> X31 -> + r1 <> GPR31 -> exists rs', exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. unfold transl_condimm_int64u. predSpec Int64.eq Int64.eq_spec n Int64.zero. @@ -828,9 +828,9 @@ Proof. exists rs'; split. eexact A. split; auto. rewrite B; auto. - assert (DFL: exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m + exec_straight ge fn (loadimm64 GPR31 n (transl_cond_int64u cmp rd r1 GPR31 k)) rs m k rs' m /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r). { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2). exists rs2; split. @@ -854,7 +854,7 @@ Lemma transl_cond_op_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)). { destruct ob as [[]|]; reflexivity. } @@ -1106,12 +1106,12 @@ Qed. Lemma indexed_memory_access_correct: forall mk_instr base ofs k rs m, - base <> X31 -> + base <> GPR31 -> exists base' ofs' rs', exec_straight_opt (indexed_memory_access mk_instr base ofs k) rs m (mk_instr base' ofs' :: k) rs' m /\ Val.offset_ptr rs'#base' (eval_offset ge ofs') = Val.offset_ptr rs#base ofs - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. unfold indexed_memory_access; intros. destruct Archi.ptr64 eqn:SF. @@ -1152,11 +1152,11 @@ Lemma indexed_load_access_correct: exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) -> forall (base: ireg) ofs k (rs: regset) v, Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> - base <> X31 -> rd <> PC -> + base <> GPR31 -> rd <> PC -> exists rs', exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m /\ rs'#rd = v - /\ forall r, r <> PC -> r <> X31 -> r <> rd -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r. Proof. intros until m; intros EXEC; intros until v; intros LOAD NOT31 NOTPC. exploit indexed_memory_access_correct; eauto. @@ -1173,10 +1173,10 @@ Lemma indexed_store_access_correct: exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) -> forall (base: ireg) ofs k (rs: regset) m', Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' -> - base <> X31 -> r1 <> X31 -> r1 <> PC -> + base <> GPR31 -> r1 <> GPR31 -> r1 <> PC -> exists rs', exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m' - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31' NOTPC. exploit indexed_memory_access_correct; eauto. @@ -1191,11 +1191,11 @@ Lemma loadind_correct: forall (base: ireg) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> - base <> X31 -> + base <> GPR31 -> exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros until v; intros TR LOAD NOT31. assert (A: exists mk_instr, @@ -1212,10 +1212,10 @@ Lemma storeind_correct: forall (base: ireg) ofs ty src k c (rs: regset) m m', storeind src base ofs ty k = OK c -> Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' -> - base <> X31 -> + base <> GPR31 -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until m'; intros TR STORE NOT31. assert (A: exists mk_instr, @@ -1231,11 +1231,11 @@ Qed. Lemma loadind_ptr_correct: forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v, Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v -> - base <> X31 -> + base <> GPR31 -> exists rs', exec_straight ge fn (loadind_ptr base ofs dst k) rs m k rs' m /\ rs'#dst = v - /\ forall r, r <> PC -> r <> X31 -> r <> dst -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> r <> dst -> rs'#r = rs#r. Proof. intros. eapply indexed_load_access_correct; eauto with asmgen. intros. unfold Mptr. destruct Archi.ptr64; auto. @@ -1244,10 +1244,10 @@ Qed. Lemma storeind_ptr_correct: forall (base: ireg) ofs (src: ireg) k (rs: regset) m m', Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' -> - base <> X31 -> src <> X31 -> + base <> GPR31 -> src <> GPR31 -> exists rs', exec_straight ge fn (storeind_ptr src base ofs k) rs m k rs' m' - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen. intros. unfold Mptr. destruct Archi.ptr64; auto. @@ -1260,7 +1260,7 @@ Lemma transl_memory_access_correct: exists base ofs rs', exec_straight_opt c rs m (mk_instr base ofs :: k) rs' m /\ Val.offset_ptr rs'#base (eval_offset ge ofs) = v - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until v; intros TR EV. unfold transl_memory_access in TR; destruct addr; ArgsInv. @@ -1285,7 +1285,7 @@ Lemma transl_load_access_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#rd = v' - /\ forall r, r <> PC -> r <> X31 -> r <> rd -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r. Proof. intros until v'; intros INSTR TR EV LOAD NOTPC. exploit transl_memory_access_correct; eauto. @@ -1303,10 +1303,10 @@ Lemma transl_store_access_correct: transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.storev chunk m v rs#r1 = Some m' -> - r1 <> PC -> r1 <> X31 -> + r1 <> PC -> r1 <> GPR31 -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until m'; intros INSTR TR EV STORE NOTPC NOT31. exploit transl_memory_access_correct; eauto. @@ -1325,7 +1325,7 @@ Lemma transl_load_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros until v; intros TR EV LOAD. assert (A: exists mk_instr, @@ -1344,7 +1344,7 @@ Lemma transl_store_correct: Mem.storev chunk m a rs#(preg_of src) = Some m' -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, r <> PC -> r <> X31 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until m'; intros TR EV STORE. assert (A: exists mk_instr chunk', @@ -1378,7 +1378,7 @@ Lemma make_epilogue_correct: /\ Mem.extends m' tm' /\ rs'#RA = parent_ra cs /\ rs'#SP = parent_sp cs - /\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> X31 -> rs'#r = rs#r). + /\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> GPR31 -> rs'#r = rs#r). Proof. intros until tm; intros LP LRA FREE AG MEXT MCS. exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP'). diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index 400168ab..42905b30 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -35,7 +35,7 @@ Require Import AST Machregs Locations. Definition is_callee_save (r: mreg): bool := match r with | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 - | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 | R31 => true + | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 => true | _ => false end. @@ -50,7 +50,7 @@ Definition float_caller_save_regs := @nil mreg. Definition int_callee_save_regs := R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 - :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R31 :: nil. + :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: nil. Definition float_callee_save_regs := @nil mreg. diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index fe39471a..09a6a237 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -38,12 +38,13 @@ Require Import Op. assembly-code generator [Asmgen]. *) +(* FIXME - no R31 *) Inductive mreg: Type := (* Allocatable General Purpose regs. *) | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 (* R10 to R14 are reserved *) | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29 - | R30 | R31 | R32 | R33 | R34 | R35 | R36 | R37 | R38 | R39 + | R30 | R32 | R33 | R34 | R35 | R36 | R37 | R38 | R39 | R40 | R41 | R42 | R43 | R44 | R45 | R46 | R47 | R48 | R49 | R50 | R51 | R52 | R53 | R54 | R55 | R56 | R57 | R58 | R59 | R60 | R61 | R62 | R63. @@ -56,7 +57,7 @@ Definition all_mregs := R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 - :: R30 :: R31 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 + :: R30 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 :: R40 :: R41 :: R42 :: R43 :: R44 :: R45 :: R46 :: R47 :: R48 :: R49 :: R50 :: R51 :: R52 :: R53 :: R54 :: R55 :: R56 :: R57 :: R58 :: R59 :: R60 :: R61 :: R62 :: R63 :: nil. @@ -89,7 +90,7 @@ Module IndexedMreg <: INDEXED_TYPE. | R15 => 16 | R16 => 17 | R17 => 18 | R18 => 19 | R19 => 20 | R20 => 21 | R21 => 22 | R22 => 23 | R23 => 24 | R24 => 25 | R25 => 26 | R26 => 27 | R27 => 28 | R28 => 29 | R29 => 30 - | R30 => 31 | R31 => 32 | R32 => 33 | R33 => 34 | R34 => 35 + | R30 => 31 | R32 => 33 | R33 => 34 | R34 => 35 | R35 => 36 | R36 => 37 | R37 => 38 | R38 => 39 | R39 => 40 | R40 => 41 | R41 => 42 | R42 => 43 | R43 => 44 | R44 => 45 | R45 => 46 | R46 => 47 | R47 => 48 | R48 => 49 | R49 => 50 @@ -116,7 +117,7 @@ Definition register_names := :: ("R15", R15) :: ("R16", R16) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) :: ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) :: ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: ("R29", R29) - :: ("R30", R30) :: ("R31", R31) :: ("R32", R32) :: ("R33", R33) :: ("R34", R34) + :: ("R30", R30) :: ("R32", R32) :: ("R33", R33) :: ("R34", R34) :: ("R35", R35) :: ("R36", R36) :: ("R37", R37) :: ("R38", R38) :: ("R39", R39) :: ("R40", R40) :: ("R41", R41) :: ("R42", R42) :: ("R43", R43) :: ("R44", R44) :: ("R45", R45) :: ("R46", R46) :: ("R47", R47) :: ("R48", R48) :: ("R49", R49) |