aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asmblock.v25
-rw-r--r--mppa_k1c/Asmblockgen.v24
-rw-r--r--mppa_k1c/Asmblockgenproof.v36
-rw-r--r--mppa_k1c/Asmblockgenproof1.v196
-rw-r--r--mppa_k1c/Asmexpand.ml8
-rw-r--r--mppa_k1c/Conventions1.v15
-rw-r--r--mppa_k1c/Machregs.v33
7 files changed, 170 insertions, 167 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 40df63e5..1040d4c0 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -86,8 +86,9 @@ Module Pregmap := EMap(PregEq).
(** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
Notation "'SP'" := GPR12 (only parsing) : asm.
-Notation "'FP'" := GPR10 (only parsing) : asm.
-Notation "'RTMP'" := GPR31 (only parsing) : asm.
+Notation "'FP'" := GPR14 (only parsing) : asm.
+Notation "'GPRA'" := GPR16 (only parsing) : asm.
+Notation "'RTMP'" := GPR32 (only parsing) : asm.
Inductive btest: Type :=
| BTdnez (**r Double Not Equal to Zero *)
@@ -935,7 +936,7 @@ Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset :
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 (rs #FP <- (rs SP) #SP <- sp #GPR31 <- Vundef) m2
+ | Some m2 => Next (rs #FP <- (rs SP) #SP <- sp #RTMP <- Vundef) m2
end
| Pfreeframe sz pos =>
@@ -946,7 +947,7 @@ Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset :
| Vptr stk ofs =>
match Mem.free m stk 0 sz with
| None => Stuck
- | Some m' => Next (rs#SP <- v #GPR31 <- Vundef) m'
+ | Some m' => Next (rs#SP <- v #RTMP <- Vundef) m'
end
| _ => Stuck
end
@@ -1112,16 +1113,16 @@ Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcom
register is reserved as temporary, to be used by the generated RV32G
code. *)
- (* FIXME - R31 is not there *)
+ (* FIXME - R16 and R32 are excluded *)
Definition preg_of (r: mreg) : preg :=
match r with
| R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4
- | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R9 => GPR9
- | R10 => GPR10 (*| R11 => GPR11 | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *)
- | R15 => GPR15 | R16 => GPR16 | R17 => GPR17 | R18 => GPR18 | R19 => GPR19
+ | 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
+ | R30 => GPR30 | R31 => GPR31 (* | 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
@@ -1199,7 +1200,7 @@ Inductive step: state -> trace -> state -> Prop :=
rs' = nextblock bi
(set_res res vres
(undef_regs (map preg_of (destroyed_by_builtin ef))
- (rs#GPR31 <- Vundef))) ->
+ (rs#RTMP <- Vundef))) ->
step (State rs m) t (State rs' m')
| exec_step_external:
forall b ef args res rs m t rs' m',
@@ -1300,8 +1301,8 @@ Qed.
Definition data_preg (r: preg) : bool :=
match r with
| RA => false
- | IR GPR31 => false
- | IR GPR8 => false
+ | IR GPRA => false
+ | IR RTMP => false
| IR _ => true
| FR _ => true
| PC => false
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index d024a74f..8bcbc712 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -25,6 +25,8 @@ Require Import Op Locations Machblock Asmblock.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
+Notation "'MFP'" := R14 (only parsing).
+
(** The code generation functions take advantage of several
characteristics of the [Mach] code generated by earlier passes of the
compiler, mostly that argument and result registers are of the correct
@@ -447,10 +449,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 ::i k else
- Psraiw GPR31 rs (Int.repr 31) ::i
- Psrliw GPR31 GPR31 (Int.sub Int.iwordsize n) ::i
- Paddw GPR31 rs GPR31 ::i
- Psraiw rd GPR31 n ::i k)
+ Psraiw RTMP rs (Int.repr 31) ::i
+ Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i
+ Paddw RTMP rs RTMP ::i
+ Psraiw rd RTMP n ::i k)
(* [Omakelong], [Ohighlong] should not occur *)
| Olowlong, a1 :: nil =>
@@ -695,7 +697,7 @@ Definition transl_memory_access
do rs <- ireg_of a1;
OK (indexed_memory_access mk_instr rs ofs ::i k)
| Aglobal id ofs, nil =>
- OK (Ploadsymbol id ofs GPR31 ::i (mk_instr GPR31 (Ofsimm Ptrofs.zero) ::i k))
+ OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP (Ofsimm Ptrofs.zero) ::i k))
| Ainstack ofs, nil =>
OK (indexed_memory_access mk_instr SP ofs ::i k)
| _, _ =>
@@ -761,8 +763,8 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
(** Function epilogue *)
Definition make_epilogue (f: Machblock.function) (k: code) :=
- (loadind_ptr SP f.(fn_retaddr_ofs) GPR8)
- ::g Pset RA GPR8 ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k.
+ (loadind_ptr SP f.(fn_retaddr_ofs) GPRA)
+ ::g Pset RA GPRA ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k.
(** Translation of a Mach instruction. *)
@@ -830,8 +832,8 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co
Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
match i with
| MBsetstack src ofs ty => before
- | MBgetparam ofs ty dst => negb (mreg_eq dst R10)
- | MBop op args res => before && negb (mreg_eq res R10)
+ | MBgetparam ofs ty dst => negb (mreg_eq dst MFP)
+ | MBop op args res => before && negb (mreg_eq res MFP)
| _ => false
end.
@@ -919,8 +921,8 @@ Definition transl_function (f: Machblock.function) :=
do lb <- transl_blocks f f.(Machblock.fn_code) true;
OK (mkfunction f.(Machblock.fn_sig)
(Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
- Pget GPR8 RA ::b
- storeind_ptr GPR8 SP f.(fn_retaddr_ofs) ::b lb)).
+ Pget GPRA RA ::b
+ storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::b lb)).
Fixpoint size_blocks (l: bblocks): Z :=
match l with
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index f97a71b1..686e8349 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -758,9 +758,9 @@ Qed. *)
the unwanted behaviour. *)
-Remark preg_of_not_FP: forall r, negb (mreg_eq r R10) = true -> IR FP <> preg_of r.
+Remark preg_of_not_FP: forall r, negb (mreg_eq r R14) = true -> IR FP <> preg_of r.
Proof.
- intros. change (IR FP) with (preg_of R10). red; intros.
+ intros. change (IR FP) with (preg_of R14). red; intros.
exploit preg_of_injective; eauto. intros; subst r; discriminate.
Qed.
@@ -1455,7 +1455,7 @@ Proof.
(* left; eapply exec_straight_steps; eauto; intros. monadInv TR. *)
monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP.
destruct ep eqn:EPeq.
- (* GPR31 contains parent *)
+ (* RTMP contains parent *)
+ exploit loadind_correct. eexact EQ1.
instantiate (2 := rs1). rewrite DXP; eauto. congruence.
intros [rs2 [P [Q R]]].
@@ -2006,25 +2006,25 @@ Proof.
(* Execution of function prologue *)
monadInv EQ0. (* rewrite transl_code'_transl_code in EQ1. *)
set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::b
- Pget GPR8 RA ::b
- storeind_ptr GPR8 SP (fn_retaddr_ofs f) ::b x0) in *.
+ Pget GPRA RA ::b
+ storeind_ptr GPRA SP (fn_retaddr_ofs f) ::b x0) in *.
set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.
set (rs2 := nextblock (bblock_single_inst (Pallocframe (fn_stacksize f) (fn_link_ofs f)))
- (rs0#FP <- (parent_sp s) #SP <- sp #GPR31 <- Vundef)).
- exploit (Pget_correct tge GPR8 RA nil rs2 m2'); auto.
+ (rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef)).
+ exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto.
intros (rs' & U' & V').
exploit (exec_straight_through_singleinst); eauto.
intro W'. remember (nextblock _ rs') as rs''.
- exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPR8 nil rs'' m2').
+ exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs'' m2').
rewrite chunk_of_Tptr in P.
- assert (rs' GPR8 = rs0 RA). { apply V'. }
- assert (rs'' GPR8 = rs' GPR8). { subst. Simpl. }
- assert (rs' GPR12 = rs2 GPR12). { apply V'; discriminate. }
- assert (rs'' GPR12 = rs' GPR12). { subst. Simpl. }
+ assert (rs' GPRA = rs0 RA). { apply V'. }
+ assert (rs'' GPRA = rs' GPRA). { subst. Simpl. }
+ assert (rs' SP = rs2 SP). { apply V'; discriminate. }
+ assert (rs'' SP = rs' SP). { subst. Simpl. }
rewrite H4. rewrite H3. rewrite H6. rewrite H5.
- (* change (rs' GPR8) with (rs0 RA). *)
+ (* change (rs' GPRA) with (rs0 RA). *)
rewrite ATLR.
- change (rs2 GPR12) with sp. eexact P.
+ change (rs2 SP) with sp. eexact P.
congruence. congruence.
intros (rs3 & U & V).
exploit (exec_straight_through_singleinst); eauto.
@@ -2061,16 +2061,16 @@ Local Transparent destroyed_at_function_entry.
unfold sp; congruence.
intros.
- assert (r <> GPR31). { contradict H3; rewrite H3; unfold data_preg; auto. }
+ assert (r <> RTMP). { contradict H3; rewrite H3; unfold data_preg; auto. }
rewrite Heqrs3'. Simpl. rewrite V. rewrite Heqrs''. Simpl. inversion V'. rewrite H6. auto.
- assert (r <> GPR8). { contradict H3; rewrite H3; unfold data_preg; auto. }
- assert (forall r : preg, r <> PC -> r <> GPR8 -> rs' r = rs2 r). { apply V'. }
+ assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. }
+ assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
(* rewrite H8; auto. *)
contradict H3; rewrite H3; unfold data_preg; auto.
contradict H3; rewrite H3; unfold data_preg; auto.
contradict H3; rewrite H3; unfold data_preg; auto.
auto. intros. rewrite Heqrs3'. Simpl. rewrite V by auto with asmgen.
- assert (forall r : preg, r <> PC -> r <> GPR8 -> rs' r = rs2 r). { apply V'. }
+ assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
rewrite Heqrs''. Simpl.
rewrite H4 by auto with asmgen. reflexivity.
- (* external function *)
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index d0c205cd..2b653236 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -79,19 +79,19 @@ Qed.
(** Properties of registers *)
-Lemma ireg_of_not_GPR31:
- forall m r, ireg_of m = OK r -> IR r <> IR GPR31.
+Lemma ireg_of_not_RTMP:
+ forall m r, ireg_of m = OK r -> IR r <> IR RTMP.
Proof.
intros. erewrite <- ireg_of_eq; eauto with asmgen.
Qed.
-Lemma ireg_of_not_GPR31':
- forall m r, ireg_of m = OK r -> r <> GPR31.
+Lemma ireg_of_not_RTMP':
+ forall m r, ireg_of m = OK r -> r <> RTMP.
Proof.
- intros. apply ireg_of_not_GPR31 in H. congruence.
+ intros. apply ireg_of_not_RTMP in H. congruence.
Qed.
-Hint Resolve ireg_of_not_GPR31 ireg_of_not_GPR31': asmgen.
+Hint Resolve ireg_of_not_RTMP ireg_of_not_RTMP': asmgen.
(** Useful simplification tactic *)
@@ -158,7 +158,7 @@ Lemma loadimm64_correct:
exists rs',
exec_straight ge (loadimm64 rd n ::g k) rs m k rs' m
/\ rs'#rd = Vlong n
- /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
unfold loadimm64; intros. generalize (make_immed64_sound n); intros E.
destruct (make_immed64 n).
@@ -179,18 +179,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 <> GPR31 ->
+ r1 <> RTMP ->
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 <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> 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 GPR31 hi lo (op rd r1 GPR31 :: k) rs m)
+- destruct (load_hilo32_correct RTMP hi lo (op rd r1 RTMP :: k) rs m)
as (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
@@ -233,11 +233,11 @@ Lemma opimm64_correct:
(forall d s n rs,
exec_basic_instr ge (opi d s n) rs m = Next ((rs#d <- (sem rs#s (Vlong n)))) m) ->
forall rd r1 n k rs,
- r1 <> GPR31 ->
+ r1 <> RTMP ->
exists rs',
exec_straight ge (opimm64 op opi rd r1 n ::g k) rs m k rs' m
/\ rs'#rd = sem rs#r1 (Vlong n)
- /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. unfold opimm64. generalize (make_immed64_sound n); intros E.
destruct (make_immed64 n).
@@ -245,7 +245,7 @@ Proof.
apply exec_straight_one. rewrite H0. simpl; eauto. auto.
split. Simpl. intros; Simpl.
(*
-- destruct (load_hilo64_correct GPR31 hi lo (op rd r1 GPR31 :: k) rs m)
+- destruct (load_hilo64_correct RTMP hi lo (op rd r1 RTMP :: k) rs m)
as (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
@@ -262,11 +262,11 @@ Qed.
Lemma addptrofs_correct:
forall rd r1 n k rs m,
- r1 <> GPR31 ->
+ r1 <> RTMP ->
exists rs',
exec_straight ge (addptrofs rd r1 n ::g k) rs m k rs' m
/\ Val.lessdef (Val.offset_ptr rs#r1 n) rs'#rd
- /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
unfold addptrofs; intros.
destruct (Ptrofs.eq_dec n Ptrofs.zero).
@@ -285,12 +285,12 @@ Qed.
(*
Lemma addptrofs_correct_2:
forall rd r1 n k (rs: regset) m b ofs,
- r1 <> GPR31 -> rs#r1 = Vptr b of
+ r1 <> RTMP -> rs#r1 = Vptr b of
s ->
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 <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. exploit (addptrofs_correct rd r1 n); eauto. intros (rs' & A & B & C).
exists rs'; intuition eauto.
@@ -299,10 +299,10 @@ Qed.
(** Translation of conditional branches *)
-Remark branch_on_GPR31:
+Remark branch_on_RTMP:
forall normal lbl (rs: regset) m b,
- 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 =
+ rs#RTMP = Val.of_bool (eqb normal b) ->
+ exec_instr ge fn (if normal then Pbnew RTMP X0 lbl else Pbeqw RTMP X0 lbl) rs m =
eval_branch fn lbl rs m (Some b).
Proof.
intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity.
@@ -343,10 +343,10 @@ Qed.
Lemma transl_comp_correct:
forall cmp r1 r2 lbl k rs m tbb b,
exists rs',
- exec_straight ge (transl_comp cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::g k) rs' m
+ exec_straight ge (transl_comp cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
/\ ( Val.cmp_bool cmp rs#r1 rs#r2 = Some b ->
- exec_control ge fn (Some (PCtlFlow (Pcb BTwnez GPR31 lbl))) (nextblock tbb rs') m
+ exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
= eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
@@ -355,10 +355,10 @@ Proof.
- split.
+ intros; Simpl.
+ intros.
- remember (rs # GPR31 <- (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'.
- simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # GPR31 (Vint (Int.repr 0)) = Some b).
+ remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'.
+ simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
{
- assert ((nextblock tbb rs') # GPR31 = (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)).
+ assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)).
{ rewrite Heqrs'. auto. }
rewrite H0. rewrite <- H.
remember (Val.cmp_bool cmp rs#r1 rs#r2) as cmpbool.
@@ -372,10 +372,10 @@ Qed.
Lemma transl_compu_correct:
forall cmp r1 r2 lbl k rs m tbb b,
exists rs',
- exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::g k) rs' m
+ exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
/\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2 = Some b ->
- exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez GPR31 lbl)))) (nextblock tbb rs') m
+ exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
= eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
@@ -384,10 +384,10 @@ Proof.
- split.
+ intros; Simpl.
+ intros.
- remember (rs # GPR31 <- (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)) as rs'.
- simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # GPR31 (Vint (Int.repr 0)) = Some b).
+ remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)) as rs'.
+ simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
{
- assert ((nextblock tbb rs') # GPR31 = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)).
+ assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)).
{ rewrite Heqrs'. auto. }
rewrite H0. rewrite <- H.
remember (Val.cmpu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2) as cmpubool.
@@ -400,10 +400,10 @@ Qed.
Lemma transl_compl_correct:
forall cmp r1 r2 lbl k rs m tbb b,
exists rs',
- exec_straight ge (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::g k) rs' m
+ exec_straight ge (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
/\ ( Val.cmpl_bool cmp rs#r1 rs#r2 = Some b ->
- exec_control ge fn (Some (PCtlFlow (Pcb BTwnez GPR31 lbl))) (nextblock tbb rs') m
+ exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
= eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
@@ -412,10 +412,10 @@ Proof.
- split.
+ intros; Simpl.
+ intros.
- remember (rs # GPR31 <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'.
- simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # GPR31 (Vint (Int.repr 0)) = Some b).
+ remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'.
+ simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
{
- assert ((nextblock tbb rs') # GPR31 = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)).
+ assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)).
{ rewrite Heqrs'. auto. }
rewrite H0. rewrite <- H.
remember (Val.cmpl_bool cmp rs#r1 rs#r2) as cmpbool.
@@ -430,10 +430,10 @@ Qed.
Lemma transl_complu_correct:
forall cmp r1 r2 lbl k rs m tbb b,
exists rs',
- exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::g k) rs' m
+ exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
/\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2 = Some b ->
- exec_control ge fn (Some (PCtlFlow (Pcb BTwnez GPR31 lbl))) (nextblock tbb rs') m
+ exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
= eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
@@ -442,10 +442,10 @@ Proof.
- split.
+ intros; Simpl.
+ intros.
- remember (rs # GPR31 <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)) as rs'.
- simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # GPR31 (Vint (Int.repr 0)) = Some b).
+ remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)) as rs'.
+ simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
{
- assert ((nextblock tbb rs') # GPR31 = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)).
+ assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)).
{ rewrite Heqrs'. auto. }
rewrite H0. rewrite <- H.
remember (Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2) as cmpbool.
@@ -626,13 +626,13 @@ Proof.
destruct cond; simpl in TRANSL; ArgsInv.
(* Ccomp *)
- exploit (transl_comp_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
- exists rs', (Pcb BTwnez GPR31 lbl).
+ exists rs', (Pcb BTwnez RTMP lbl).
split.
+ constructor. eexact A.
+ split; auto. apply C; auto.
(* Ccompu *)
- exploit (transl_compu_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
- exists rs', (Pcb BTwnez GPR31 lbl).
+ exists rs', (Pcb BTwnez RTMP lbl).
split.
+ constructor. eexact A.
+ split; auto. apply C; auto.
@@ -652,12 +652,12 @@ Proof.
unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0.
destruct c0; simpl; auto;
unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
- + exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
- exploit (transl_comp_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
- exists rs'2, (Pcb BTwnez GPR31 lbl).
+ + exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C).
+ exploit (transl_comp_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C').
+ exists rs'2, (Pcb BTwnez RTMP lbl).
split.
* constructor. apply exec_straight_trans
- with (c2 := (transl_comp c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+ with (c2 := (transl_comp c0 Signed x RTMP lbl k)) (rs2 := rs') (m2 := m').
eexact A. eexact A'.
* split; auto.
{ apply C'; auto. rewrite B, C; eauto with asmgen. }
@@ -671,31 +671,31 @@ Proof.
split.
* apply A.
* split; auto. apply C. apply EVAL'.
- + assert (transl_opt_compuimm n c0 x lbl k = loadimm32 GPR31 n ::g transl_comp c0 Unsigned x GPR31 lbl k).
+ + assert (transl_opt_compuimm n c0 x lbl k = loadimm32 RTMP n ::g transl_comp c0 Unsigned x RTMP lbl k).
{ unfold transl_opt_compuimm.
destruct (Int.eq n Int.zero) eqn:EQN.
all: unfold select_comp in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto.
all: discriminate. }
rewrite H. clear H.
- exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
- exploit (transl_compu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
- exists rs'2, (Pcb BTwnez GPR31 lbl).
+ exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C).
+ exploit (transl_compu_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C').
+ exists rs'2, (Pcb BTwnez RTMP lbl).
split.
* constructor. apply exec_straight_trans
- with (c2 := (transl_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+ with (c2 := (transl_comp c0 Unsigned x RTMP lbl k)) (rs2 := rs') (m2 := m').
eexact A. eexact A'.
* split; auto.
{ apply C'; auto. rewrite B, C; eauto with asmgen. }
{ intros. rewrite B'; eauto with asmgen. }
(* Ccompl *)
- exploit (transl_compl_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
- exists rs', (Pcb BTwnez GPR31 lbl).
+ exists rs', (Pcb BTwnez RTMP lbl).
split.
+ constructor. eexact A.
+ split; auto. apply C; auto.
(* Ccomplu *)
- exploit (transl_complu_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
- exists rs', (Pcb BTwnez GPR31 lbl).
+ exists rs', (Pcb BTwnez RTMP lbl).
split.
+ constructor. eexact A.
+ split; auto. apply C; auto.
@@ -715,12 +715,12 @@ Proof.
unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0.
destruct c0; simpl; auto;
unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
- + exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
- exploit (transl_compl_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
- exists rs'2, (Pcb BTwnez GPR31 lbl).
+ + exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C).
+ exploit (transl_compl_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C').
+ exists rs'2, (Pcb BTwnez RTMP lbl).
split.
* constructor. apply exec_straight_trans
- with (c2 := (transl_compl c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+ with (c2 := (transl_compl c0 Signed x RTMP lbl k)) (rs2 := rs') (m2 := m').
eexact A. eexact A'.
* split; auto.
{ apply C'; auto. rewrite B, C; eauto with asmgen. }
@@ -735,18 +735,18 @@ Proof.
split.
* apply A.
* split; auto. apply C. apply EVAL'.
- + assert (transl_opt_compluimm n c0 x lbl k = loadimm64 GPR31 n ::g transl_compl c0 Unsigned x GPR31 lbl k).
+ + assert (transl_opt_compluimm n c0 x lbl k = loadimm64 RTMP n ::g transl_compl c0 Unsigned x RTMP lbl k).
{ unfold transl_opt_compluimm.
destruct (Int64.eq n Int64.zero) eqn:EQN.
all: unfold select_compl in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto.
all: discriminate. }
rewrite H. clear H.
- exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
- exploit (transl_complu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
- exists rs'2, (Pcb BTwnez GPR31 lbl).
+ exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C).
+ exploit (transl_complu_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C').
+ exists rs'2, (Pcb BTwnez RTMP lbl).
split.
* constructor. apply exec_straight_trans
- with (c2 := (transl_compl c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+ with (c2 := (transl_compl c0 Unsigned x RTMP lbl k)) (rs2 := rs') (m2 := m').
eexact A. eexact A'.
* split; auto.
{ apply C'; auto. rewrite B, C; eauto with asmgen. }
@@ -762,7 +762,7 @@ Lemma transl_cbranch_correct_true:
exists rs', exists insn,
exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
/\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = goto_label fn lbl (nextblock tbb rs') m'
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. eapply transl_cbranch_correct_1 with (b := true); eauto.
Qed.
@@ -776,7 +776,7 @@ Lemma transl_cbranch_correct_false:
exists rs', exists insn,
exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
/\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = Next (nextblock tbb rs') m'
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. exploit transl_cbranch_correct_1; eauto.
Qed.
@@ -878,11 +878,11 @@ Qed.
Lemma transl_condimm_int32s_correct:
forall cmp rd r1 n k rs m,
- r1 <> GPR31 ->
+ r1 <> RTMP ->
exists rs',
exec_straight ge (basics_to_code (transl_condimm_int32s cmp rd r1 n k)) rs m (basics_to_code k) rs' m
/\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
- /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto].
@@ -901,11 +901,11 @@ Qed.
Lemma transl_condimm_int32u_correct:
forall cmp rd r1 n k rs m,
- r1 <> GPR31 ->
+ r1 <> RTMP ->
exists rs',
exec_straight ge (basics_to_code (transl_condimm_int32u cmp rd r1 n k)) rs m (basics_to_code 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 <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto].
@@ -924,11 +924,11 @@ Qed.
Lemma transl_condimm_int64s_correct:
forall cmp rd r1 n k rs m,
- r1 <> GPR31 ->
+ r1 <> RTMP ->
exists rs',
exec_straight ge (basics_to_code (transl_condimm_int64s cmp rd r1 n k)) rs m (basics_to_code k) rs' m
/\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
- /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto].
@@ -947,11 +947,11 @@ Qed.
Lemma transl_condimm_int64u_correct:
forall cmp rd r1 n k rs m,
- r1 <> GPR31 ->
+ r1 <> RTMP ->
exists rs',
exec_straight ge (basics_to_code (transl_condimm_int64u cmp rd r1 n k)) rs m (basics_to_code 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 <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto].
@@ -974,7 +974,7 @@ Lemma transl_cond_op_correct:
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code 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 <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> 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. }
@@ -1141,7 +1141,7 @@ Opaque Int.eq.
intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.
+ TranslOpSimpl.
- (* Oaddrstack *)
- exploit addptrofs_correct. instantiate (1 := GPR12); auto with asmgen. intros (rs' & A & B & C).
+ exploit addptrofs_correct. instantiate (1 := SP); auto with asmgen. intros (rs' & A & B & C).
exists rs'; split; eauto. auto with asmgen.
- (* Ocast8signed *)
econstructor; split.
@@ -1267,12 +1267,12 @@ Qed.
Lemma indexed_memory_access_correct:
forall mk_instr base ofs k rs m,
- base <> GPR31 ->
+ base <> RTMP ->
exists base' ofs' rs',
exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m
(mk_instr base' ofs' ::g k) rs' m
/\ Val.offset_ptr rs'#base' (eval_offset ge ofs') = Val.offset_ptr rs#base ofs
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
unfold indexed_memory_access; intros.
(* destruct Archi.ptr64 eqn:SF. *)
@@ -1318,11 +1318,11 @@ Lemma indexed_load_access_correct:
exec_basic_instr ge (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 <> GPR31 -> rd <> PC ->
+ base <> RTMP -> rd <> PC ->
exists rs',
exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m
/\ rs'#rd = v
- /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> 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.
@@ -1339,10 +1339,10 @@ Lemma indexed_store_access_correct:
exec_basic_instr ge (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 <> GPR31 -> r1 <> GPR31 -> r1 <> PC ->
+ base <> RTMP -> r1 <> RTMP -> r1 <> PC ->
exists rs',
exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m'
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31' NOTPC.
exploit indexed_memory_access_correct. instantiate (1 := base). eauto.
@@ -1357,11 +1357,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 <> GPR31 ->
+ base <> RTMP ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros until v; intros TR LOAD NOT31.
assert (A: exists mk_instr,
@@ -1379,10 +1379,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 <> GPR31 ->
+ base <> RTMP ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros until m'; intros TR STORE NOT31.
assert (A: exists mk_instr,
@@ -1429,11 +1429,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 <> GPR31 ->
+ base <> RTMP ->
exists rs',
exec_straight ge (loadind_ptr base ofs dst ::g k) rs m k rs' m
/\ rs'#dst = v
- /\ forall r, r <> PC -> r <> GPR31 -> r <> dst -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> r <> dst -> rs'#r = rs#r.
Proof.
intros. eapply indexed_load_access_correct; eauto with asmgen.
intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H1. auto.
@@ -1442,10 +1442,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 <> GPR31 -> src <> GPR31 ->
+ base <> RTMP -> src <> RTMP ->
exists rs',
exec_straight ge (storeind_ptr src base ofs ::g k) rs m k rs' m'
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen.
intros. unfold Mptr. assert (Archi.ptr64 = true); auto.
@@ -1458,7 +1458,7 @@ Lemma transl_memory_access_correct:
exists base ofs rs',
exec_straight_opt (basics_to_code c) rs m (mk_instr base ofs ::g (basics_to_code k)) rs' m
/\ Val.offset_ptr rs'#base (eval_offset ge ofs) = v
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros until v; intros TR EV.
unfold transl_memory_access in TR; destruct addr; ArgsInv.
@@ -1496,7 +1496,7 @@ Lemma transl_load_access_correct:
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
/\ rs'#rd = v'
- /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
intros until v'; intros INSTR TR EV LOAD NOTPC.
exploit transl_memory_access_correct; eauto.
@@ -1514,10 +1514,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 <> GPR31 ->
+ r1 <> PC -> r1 <> RTMP ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros until m'; intros INSTR TR EV STORE NOTPC NOT31.
exploit transl_memory_access_correct; eauto.
@@ -1535,7 +1535,7 @@ Lemma transl_load_correct:
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros until v; intros TR EV LOAD.
assert (A: exists mk_instr,
@@ -1554,7 +1554,7 @@ Lemma transl_store_correct:
Mem.storev chunk m a rs#(preg_of src) = Some m' ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
- /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros until m'; intros TR EV STORE.
assert (A: exists mk_instr chunk',
@@ -1586,7 +1586,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 <> GPR31 -> r <> GPR8 -> rs'#r = rs#r).
+ /\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> RTMP -> r <> GPRA -> 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').
@@ -1597,7 +1597,7 @@ Proof.
unfold make_epilogue.
rewrite chunk_of_Tptr in *.
- exploit ((loadind_ptr_correct SP (fn_retaddr_ofs f) GPR8 (Pset RA GPR8 ::g Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k))
+ exploit ((loadind_ptr_correct SP (fn_retaddr_ofs f) GPRA (Pset RA GPRA ::g Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k))
rs tm).
- rewrite <- (sp_val _ _ rs AG). simpl. eexact LRA'.
- congruence.
@@ -1607,7 +1607,7 @@ Proof.
apply mkagree; auto.
rewrite C1; discriminate || auto.
intro. rewrite C1; auto; destruct r; simpl; try discriminate.
- + exploit (Pset_correct RA GPR8 (Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k) rs1 tm). auto.
+ + exploit (Pset_correct RA GPRA (Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k) rs1 tm). auto.
intros (rs2 & A2 & B2 & C2).
econstructor; econstructor; split.
* eapply exec_straight_trans.
@@ -1615,7 +1615,7 @@ Proof.
{ eapply exec_straight_trans.
{ eapply A2. }
{ apply exec_straight_one. simpl.
- rewrite (C2 GPR12) by auto with asmgen. rewrite <- (sp_val _ _ rs1 AG1). simpl; rewrite LP'.
+ rewrite (C2 SP) by auto with asmgen. rewrite <- (sp_val _ _ rs1 AG1). simpl; rewrite LP'.
rewrite FREE'; eauto. (* auto. *) } }
* split. (* apply agree_nextinstr. *)apply agree_set_other; auto with asmgen.
apply agree_change_sp with (Vptr stk soff).
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 3b3b2b65..45fe9b32 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -62,7 +62,7 @@ let expand_storeind_ptr src base ofs =
(* Fix-up code around calls to variadic functions. Floating-point arguments
residing in FP registers need to be moved to integer registers. *)
-let int_param_regs = let open Asmblock in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7 |]
+let int_param_regs = let open Asmblock in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11 |]
(* let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] *)
let float_param_regs = [| |]
@@ -441,20 +441,20 @@ let expand_instruction instr =
match instr with
| Pallocframe (sz, ofs) ->
let sg = get_current_function_sig() in
- emit (Pmv (Asmblock.GPR10, Asmblock.GPR12));
+ emit (Pmv (Asmblock.GPR14, Asmblock.GPR12));
if sg.sig_cc.cc_vararg then begin
let n = arguments_size sg in
let extra_sz = if n >= 8 then 0 else align 16 ((8 - n) * wordsize) in
let full_sz = Z.add sz (Z.of_uint extra_sz) in
expand_addptrofs Asmblock.GPR12 Asmblock.GPR12 (Ptrofs.repr (Z.neg full_sz));
- expand_storeind_ptr Asmblock.GPR10 Asmblock.GPR12 ofs;
+ expand_storeind_ptr Asmblock.GPR14 Asmblock.GPR12 ofs;
let va_ofs =
Z.add full_sz (Z.of_sint ((n - 8) * wordsize)) in
vararg_start_ofs := Some va_ofs;
save_arguments n va_ofs
end else begin
expand_addptrofs Asmblock.GPR12 Asmblock.GPR12 (Ptrofs.repr (Z.neg sz));
- expand_storeind_ptr Asmblock.GPR10 Asmblock.GPR12 ofs;
+ expand_storeind_ptr Asmblock.GPR14 Asmblock.GPR12 ofs;
vararg_start_ofs := None
end
| Pfreeframe (sz, ofs) ->
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v
index 99044be8..7460b2e4 100644
--- a/mppa_k1c/Conventions1.v
+++ b/mppa_k1c/Conventions1.v
@@ -34,14 +34,15 @@ 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 => true
+ (* | R15 | R16 | R17 *) | R18 | R19 | R20 | R21 | R22
+ | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 | R31 => true
| _ => false
end.
Definition int_caller_save_regs :=
- R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R9
- :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 :: R40 :: R41
+ R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9
+ :: R10 :: R11 :: R15 (* :: R16 *) :: R17
+ (* :: 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.
@@ -49,8 +50,8 @@ Definition int_caller_save_regs :=
Definition float_caller_save_regs := R62 :: nil. (* FIXME - for the dummy_float_reg *)
Definition int_callee_save_regs :=
- R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22
- :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: nil.
+ (* R15 :: R16 :: R17 :: *)R18 :: R19 :: R20 :: R21 :: R22
+ :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R31 :: nil.
Definition float_callee_save_regs := @nil mreg.
@@ -179,7 +180,7 @@ code can be introduced in the Asmexpand pass.
*)
Definition param_regs :=
- R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: nil.
+ R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: nil.
Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ)
(rec: Z -> Z -> list (rpair loc)) :=
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index bed3c040..41ea0979 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -38,13 +38,12 @@ 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 | R9
- | R10 (* R11 to R14 res *) | R15 | R16 | R17 | R18 | R19
+ | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9
+ | R10 | R11 | (* R12 | R13 | *) R14 | R15 (* | R16 *) | R17 | R18 | R19
| R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29
- | R30 | R32 | R33 | R34 | R35 | R36 | R37 | R38 | R39
+ | R30 | R31 (* | 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.
@@ -54,10 +53,10 @@ Proof. decide equality. Defined.
Global Opaque mreg_eq.
Definition all_mregs :=
- R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R9
- :: R10 :: R15 :: R16 :: R17 :: R18 :: R19
+ R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9
+ :: R10 :: R11 (* :: R12 :: R13 *) :: R14 :: R15 (* :: R16 *) :: R17 :: R18 :: R19
:: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29
- :: R30 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39
+ :: R30 :: R31 (* :: 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.
@@ -86,12 +85,12 @@ Module IndexedMreg <: INDEXED_TYPE.
Definition index (r: mreg): positive :=
match r with
| R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5
- | R5 => 6 | R6 => 7 | R7 => 8 | R9 => 10
- | R10 => 11
- | R15 => 16 | R16 => 17 | R17 => 18 | R18 => 19 | R19 => 20
+ | R5 => 6 | R6 => 7 | R7 => 8 | R8 => 9 | R9 => 10
+ | R10 => 11 | R11 => 12 (* | R12 => 13 | R13 => 14 *) | R14 => 15
+ | 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 | R32 => 33 | R33 => 34 | R34 => 35
+ | R30 => 31 | R31 => 32 (* | 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
@@ -115,12 +114,12 @@ Local Open Scope string_scope.
Definition register_names :=
("R0" , R0) :: ("R1" , R1) :: ("R2" , R2) :: ("R3" , R3) :: ("R4" , R4)
- :: ("R5" , R5) :: ("R6" , R6) :: ("R7" , R7) :: ("R9" , R9)
- :: ("R10", R10)
- :: ("R15", R15) :: ("R16", R16) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19)
+ :: ("R5" , R5) :: ("R6" , R6) :: ("R7" , R7) :: ("R8" , R8) :: ("R9" , R9)
+ :: ("R10", R10) :: ("R11", R11) (* :: ("R12", R12) :: ("R13", R13) *) :: ("R14", R14)
+ :: ("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) :: ("R32", R32) :: ("R33", R33) :: ("R34", R34)
+ :: ("R30", R30) :: ("R31", R31) (* :: ("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)
@@ -175,9 +174,9 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
Definition destroyed_by_setstack (ty: typ): list mreg := nil.
-Definition destroyed_at_function_entry: list mreg := R10 :: nil.
+Definition destroyed_at_function_entry: list mreg := R14 :: nil.
-Definition temp_for_parent_frame: mreg := R10. (* FIXME - and R8 ?? *)
+Definition temp_for_parent_frame: mreg := R14. (* FIXME - ?? *)
Definition destroyed_at_indirect_call: list mreg := nil.
(* R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. *)
generated by cgit (git 2.34.1) at 2024-07-04 01:48:57 +0000