From 5020a5a07da3fd690f5d171a48d0c73ef48f9430 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 1 Mar 2013 15:32:13 +0000 Subject: Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 263 +++++++++++++++++++++++++++++++--------------------------- 1 file changed, 139 insertions(+), 124 deletions(-) (limited to 'powerpc/Asm.v') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 5d815fda..27e801a7 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -84,6 +84,11 @@ End PregEq. Module Pregmap := EMap(PregEq). +(** Conventional names for stack pointer ([SP]) and return address ([RA]) *) + +Notation "'SP'" := GPR1 (only parsing). +Notation "'RA'" := LR (only parsing). + (** 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 @@ -291,7 +296,9 @@ lbl: .long table[0], table[1], ... *) Definition code := list instruction. -Definition fundef := AST.fundef code. +Definition function := code. +Definition fn_code (f: function) : code := f. +Definition fundef := AST.fundef function. Definition program := AST.program fundef unit. (** * Operational semantics *) @@ -309,6 +316,14 @@ Definition genv := Genv.t fundef unit. 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). +(** Undefining some registers *) + +Fixpoint undef_regs (l: list preg) (rs: regset) : regset := + match l with + | nil => rs + | r :: l' => undef_regs l' (rs#r <- Vundef) + end. + Section RELSEM. (** Looking up instructions in a code sequence by position. *) @@ -428,8 +443,8 @@ Definition const_high (c: constant) := or [Error] if the processor is stuck. *) Inductive outcome: Type := - | OK: regset -> mem -> outcome - | Error: outcome. + | Next: regset -> mem -> outcome + | Stuck: outcome. (** Manipulations over the [PC] register: continuing with the next instruction ([nextinstr]) or branching to a label ([goto_label]). *) @@ -439,11 +454,11 @@ Definition nextinstr (rs: regset) := Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := match label_pos lbl 0 c with - | None => Error + | None => Stuck | Some pos => match rs#PC with - | Vptr b ofs => OK (rs#PC <- (Vptr b (Int.repr pos))) m - | _ => Error + | Vptr b ofs => Next (rs#PC <- (Vptr b (Int.repr pos))) m + | _ => Stuck end end. @@ -453,29 +468,29 @@ Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := 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 + | None => Stuck + | Some v => Next (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 + | None => Stuck + | Some v => Next (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' + | None => Stuck + | Some m' => Next (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' + | None => Stuck + | Some m' => Next (nextinstr rs) m' end. (** Operations over condition bits. *) @@ -521,127 +536,124 @@ Definition compare_float (rs: regset) (v1 v2: val) := 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 + Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m | Padde rd r1 r2 => - OK (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY) + Next (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY) #CARRY <- (Val.add_carry rs#r1 rs#r2 rs#CARRY))) m | Paddi rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m + Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m | Paddic rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)) + Next (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)) #CARRY <- (Val.add_carry (gpr_or_zero rs r1) (const_low cst) Vzero))) m | Paddis rd r1 cst => - OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m + Next (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) + Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m | Pallocframe sz ofs => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Int.zero in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with - | None => Error - | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2 + | None => Stuck + | Some m2 => Next (nextinstr (rs#GPR1 <- sp #GPR0 <- 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 + Next (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 + Next (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 + Next (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 + Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m | Pb lbl => goto_label c lbl rs m | Pbctr => - OK (rs#PC <- (rs#CTR)) m + Next (rs#PC <- (rs#CTR)) m | Pbctrl => - OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m + Next (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 + | Vint n => if Int.eq n Int.zero then goto_label c lbl rs m else Next (nextinstr rs) m + | _ => Stuck end | Pbl ident => - OK (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m + Next (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 + Next (rs#PC <- (symbol_offset ident Int.zero)) m | Pblr => - OK (rs#PC <- (rs#LR)) m + Next (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 + | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label c lbl rs m + | _ => Stuck end | Pbtbl r tbl => - match gpr_or_zero rs r with + match rs r with | Vint n => - let pos := Int.unsigned n in - if zeq (Zmod pos 4) 0 then - match list_nth_z tbl (pos / 4) with - | None => Error - | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m - end - else Error - | _ => Error + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m + end + | _ => Stuck end | Pcmplw r1 r2 => - OK (nextinstr (compare_uint rs m rs#r1 rs#r2)) m + Next (nextinstr (compare_uint rs m rs#r1 rs#r2)) m | Pcmplwi r1 cst => - OK (nextinstr (compare_uint rs m rs#r1 (const_low cst))) m + Next (nextinstr (compare_uint rs m rs#r1 (const_low cst))) m | Pcmpw r1 r2 => - OK (nextinstr (compare_sint rs rs#r1 rs#r2)) m + Next (nextinstr (compare_sint rs rs#r1 rs#r2)) m | Pcmpwi r1 cst => - OK (nextinstr (compare_sint rs rs#r1 (const_low cst))) m + Next (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 + Next (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.maketotal (Val.divs rs#r1 rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m | Pdivwu rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m + Next (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m | Peqv rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m + Next (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 + Next (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m | Pextsh rd r1 => - OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m + Next (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m | Pfreeframe sz ofs => match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with - | None => Error + | None => Stuck | Some v => match rs#GPR1 with | Vptr stk ofs => match Mem.free m stk 0 sz with - | None => Error - | Some m' => OK (nextinstr (rs#GPR1 <- v)) m' + | None => Stuck + | Some m' => Next (nextinstr (rs#GPR1 <- v)) m' end - | _ => Error + | _ => Stuck end end | Pfabs rd r1 => - OK (nextinstr (rs#rd <- (Val.absf rs#r1))) m + Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m | Pfadd rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m | Pfcmpu r1 r2 => - OK (nextinstr (compare_float rs rs#r1 rs#r2)) m + Next (nextinstr (compare_float rs rs#r1 rs#r2)) m | Pfcti rd r1 => - OK (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m + Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m | Pfdiv rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m | Pfmake rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m | Pfmr rd r1 => - OK (nextinstr (rs#rd <- (rs#r1))) m + Next (nextinstr (rs#rd <- (rs#r1))) m | Pfmul rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m | Pfneg rd r1 => - OK (nextinstr (rs#rd <- (Val.negf rs#r1))) m + Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m | Pfrsp rd r1 => - OK (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m + Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m | Pfsub rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m + Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m | Plbz rd cst r1 => load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => @@ -663,50 +675,50 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Plhzx rd r1 r2 => load2 Mint16unsigned rd r1 r2 rs m | Plfi rd f => - OK (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) m + Next (nextinstr (rs #GPR12 <- Vundef #rd <- (Vfloat f))) 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 + Next (nextinstr (rs#rd <- (rs#(reg_of_crbit bit)))) m | Pmflr rd => - OK (nextinstr (rs#rd <- (rs#LR))) m + Next (nextinstr (rs#rd <- (rs#LR))) m | Pmr rd r1 => - OK (nextinstr (rs#rd <- (rs#r1))) m + Next (nextinstr (rs#rd <- (rs#r1))) m | Pmtctr r1 => - OK (nextinstr (rs#CTR <- (rs#r1))) m + Next (nextinstr (rs#CTR <- (rs#r1))) m | Pmtlr r1 => - OK (nextinstr (rs#LR <- (rs#r1))) m + Next (nextinstr (rs#LR <- (rs#r1))) m | Pmulli rd r1 cst => - OK (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m + Next (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 + Next (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 + Next (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 + Next (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 + Next (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 + Next (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 + Next (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 + Next (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 + Next (nextinstr (rs#rd <- (Val.rolm rs#r1 amount mask))) m | Prlwimi rd r1 amount mask => - OK (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask))) + Next (nextinstr (rs#rd <- (Val.or (Val.and rs#rd (Vint (Int.not mask))) (Val.rolm rs#r1 amount mask)))) m | Pslw rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m + Next (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 + Next (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 + Next (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 + Next (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 => @@ -717,13 +729,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome store2 Mfloat64al32 rd r1 r2 rs m | Pstfs rd cst r1 => match store1 Mfloat32 rd cst r1 rs m with - | OK rs' m' => OK (rs'#FPR13 <- Vundef) m' - | Error => Error + | Next rs' m' => Next (rs'#FPR13 <- Vundef) m' + | Stuck => Stuck end | Pstfsx rd r1 r2 => match store2 Mfloat32 rd r1 r2 rs m with - | OK rs' m' => OK (rs'#FPR13 <- Vundef) m' - | Error => Error + | Next rs' m' => Next (rs'#FPR13 <- Vundef) m' + | Stuck => Stuck end | Psth rd cst r1 => store1 Mint16unsigned rd cst r1 rs m @@ -734,41 +746,34 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | 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) + Next (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) Vone))) m | Psubfe rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY) + Next (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY) #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) rs#CARRY))) m | Psubfic rd r1 cst => - OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) + Next (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) #CARRY <- (Val.add_carry (const_low cst) (Val.notint rs#r1) Vone))) m | Pxor rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m + Next (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 + Next (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 + Next (nextinstr (rs#rd <- (Val.xor rs#r1 (const_high cst)))) m | Plabel lbl => - OK (nextinstr rs) m + Next (nextinstr rs) m | Pbuiltin ef args res => - Error (**r treated specially below *) + Stuck (**r treated specially below *) | Pannot ef args => - Error (**r treated specially below *) + Stuck (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers - to the PPC view. PPC 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 [Asmgenproof] will show that this never happens. - - Note that no LTL register maps to [GPR0]. + to the PPC view. Note that no LTL register maps to [GPR0]. This register is reserved as a temporary to be used by the generated PPC code. *) -Definition ireg_of (r: mreg) : ireg := +Definition preg_of (r: mreg) : preg := match r with | R3 => GPR3 | R4 => GPR4 | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9 | R10 => GPR10 @@ -778,11 +783,6 @@ Definition ireg_of (r: mreg) : ireg := | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 | R30 => GPR30 | R31 => GPR31 | IT1 => GPR11 | IT2 => GPR12 - | _ => GPR12 (* should not happen *) - end. - -Definition freg_of (r: mreg) : freg := - match r with | F1 => FPR1 | F2 => FPR2 | F3 => FPR3 | F4 => FPR4 | F5 => FPR5 | F6 => FPR6 | F7 => FPR7 | F8 => FPR8 | F9 => FPR9 | F10 => FPR10 | F11 => FPR11 @@ -792,13 +792,6 @@ Definition freg_of (r: mreg) : freg := | F24 => FPR24 | F25 => FPR25 | F26 => FPR26 | F27 => FPR27 | F28 => FPR28 | F29 => FPR29 | F30 => FPR30 | F31 => FPR31 | FT1 => FPR0 | FT2 => FPR12 | FT3 => FPR13 - | _ => FPR0 (* 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. @@ -849,7 +842,7 @@ Inductive step: state -> trace -> state -> Prop := 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' -> + exec_instr c i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: forall b ofs c ef args res rs m t v m', @@ -968,3 +961,25 @@ Ltac Equalities := (* final states *) inv H; inv H0. congruence. Qed. + +(** Classification functions for processor registers (used in Asmgenproof). *) + +Definition data_preg (r: preg) : bool := + match r with + | IR GPR0 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true + end. + +Definition nontemp_preg (r: preg) : bool := + match r with + | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false + | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true + end. + -- cgit