From ef5477a47b49c405744319fbdef0a689b1bf03d4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Dec 2020 10:30:51 +0100 Subject: Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat PowerPC operations. The pseudoinstructions were used to implement these operations, as follows: Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64 Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64 Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32 These pseudoinstructions were expanded (in Asmexpand.ml) in terms of Pfcfid : signed int64 -> float64 Pfctidz : float64 -> signed int64 and int32/int64 conversions. This commit performs this expansion during instruction selection (SelectOp.vp): floatofint(n) becomes floatoflong(longofint(n)) floatofintu(n) becomes floatoflong(longuofint(n)) intuoffloat(n) becomes cast32unsigned(longoffloat(n)) Then there is no need for the 3 removed operations and the 3 removed pseudoinstructions. More importantly, the correctness of these expansions is now proved as part of instruction selection, using the corresponding results from Floats.v. --- powerpc/Asm.v | 9 --------- powerpc/AsmToJSON.ml | 3 --- powerpc/Asmexpand.ml | 26 -------------------------- powerpc/Asmgen.v | 9 --------- powerpc/Asmgenproof1.v | 12 ------------ powerpc/Machregs.v | 2 +- powerpc/NeedOp.v | 2 +- powerpc/Op.v | 18 +----------------- powerpc/SelectOp.vp | 8 +++++--- powerpc/SelectOpproof.v | 24 +++++++++++++++--------- powerpc/TargetPrinter.ml | 6 ------ powerpc/ValueAOp.v | 3 --- 12 files changed, 23 insertions(+), 99 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 4fb38ff8..6ec20d62 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -200,12 +200,9 @@ Inductive instruction : Type := | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfadds: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) - | Pfcfi: freg -> ireg -> instruction (**r signed-int-to-float conversion (pseudo, PPC64) *) | Pfcfl: freg -> ireg -> instruction (**r signed-long-to-float conversion (pseudo, PPC64) *) - | Pfcfiu: freg -> ireg -> instruction (**r unsigned-int-to-float conversion (pseudo, PPC64) *) | Pfcfid: freg -> freg -> instruction (**r signed-long-to-float conversion (PPC64) *) | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo) *) - | Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *) | Pfctid: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo, PPC64) *) | Pfctidz: freg -> freg -> instruction (**r float-to-signed-long conversion, round towards 0 (PPC64) *) | Pfctiw: freg -> freg -> instruction (**r float-to-signed-int conversion, round by default *) @@ -825,16 +822,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m | Pfcmpu r1 r2 => Next (nextinstr (compare_float rs rs#r1 rs#r2)) m - | Pfcfi rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m | Pfcfl rd r1 => Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m - | Pfcfiu rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m | Pfcti rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m - | Pfctiu rd r1 => - Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m | Pfctid rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m | Pfdiv rd r1 r2 => diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index f4d4285a..09cfc28d 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -198,12 +198,9 @@ let pp_instructions pp ic = | Pfadd (fr1,fr2,fr3) -> instruction pp "Pfadd" [Freg fr1; Freg fr2; Freg fr3] | Pfadds (fr1,fr2,fr3) -> instruction pp "Pfadds" [Freg fr1; Freg fr2; Freg fr3] | Pfcmpu (fr1,fr2) -> instruction pp "Pfcmpu" [Freg fr1; Freg fr2] - | Pfcfi (ir,fr) | Pfcfl (ir,fr) -> assert false (* Should not occur *) | Pfcfid (fr1,fr2) -> instruction pp "Pfcfid" [Freg fr1; Freg fr2] - | Pfcfiu _ (* Should not occur *) | Pfcti _ (* Should not occur *) - | Pfctiu _ (* Should not occur *) | Pfctid _ -> assert false (* Should not occur *) | Pfctidz (fr1,fr2) -> instruction pp "Pfctidz" [Freg fr1; Freg fr2] | Pfctiw (fr1,fr2) -> instruction pp "Pfctiw" [Freg fr1; Freg fr2] diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index d8cbd94e..cb6a659f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -875,15 +875,6 @@ let expand_instruction instr = emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz))) else emit (Plwz(GPR1, Cint ofs, GPR1)) - | Pfcfi(r1, r2) -> - assert (Archi.ppc64); - emit (Pextsw(GPR0, r2)); - emit (Pstdu(GPR0, Cint _m8, GPR1)); - emit (Pcfi_adjust _8); - emit (Plfd(r1, Cint _0, GPR1)); - emit (Pfcfid(r1, r1)); - emit (Paddi(GPR1, GPR1, Cint _8)); - emit (Pcfi_adjust _m8) | Pfcfl(r1, r2) -> assert (Archi.ppc64); emit (Pstdu(r2, Cint _m8, GPR1)); @@ -892,15 +883,6 @@ let expand_instruction instr = emit (Pfcfid(r1, r1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) - | Pfcfiu(r1, r2) -> - assert (Archi.ppc64); - emit (Prldicl(GPR0, r2, _0, _32)); - emit (Pstdu(GPR0, Cint _m8, GPR1)); - emit (Pcfi_adjust _8); - emit (Plfd(r1, Cint _0, GPR1)); - emit (Pfcfid(r1, r1)); - emit (Paddi(GPR1, GPR1, Cint _8)); - emit (Pcfi_adjust _m8) | Pfcti(r1, r2) -> emit (Pfctiwz(FPR13, r2)); emit (Pstfdu(FPR13, Cint _m8, GPR1)); @@ -908,14 +890,6 @@ let expand_instruction instr = emit (Plwz(r1, Cint _4, GPR1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) - | Pfctiu(r1, r2) -> - assert (Archi.ppc64); - emit (Pfctidz(FPR13, r2)); - emit (Pstfdu(FPR13, Cint _m8, GPR1)); - emit (Pcfi_adjust _8); - emit (Plwz(r1, Cint _4, GPR1)); - emit (Paddi(GPR1, GPR1, Cint _8)); - emit (Pcfi_adjust _m8) | Pfctid(r1, r2) -> assert (Archi.ppc64); emit (Pfctidz(FPR13, r2)); diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index a686414a..1dca4ba4 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -611,15 +611,6 @@ Definition transl_op | Ointoffloat, a1 :: nil => do r1 <- freg_of a1; do r <- ireg_of res; OK (Pfcti r r1 :: k) - | Ointuoffloat, a1 :: nil => - do r1 <- freg_of a1; do r <- ireg_of res; - OK (Pfctiu r r1 :: k) - | Ofloatofint, a1 :: nil => - do r1 <- ireg_of a1; do r <- freg_of res; - OK (Pfcfi r r1 :: k) - | Ofloatofintu, a1 :: nil => - do r1 <- ireg_of a1; do r <- freg_of res; - OK (Pfcfiu r r1 :: k) | Ofloatofwords, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res; OK (Pfmake r r1 r2 :: k) diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 20cf9c1d..0442f7e8 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1498,18 +1498,6 @@ Opaque Val.add. rewrite H1; auto. (* Ointoffloat *) - replace v with (Val.maketotal (Val.intoffloat (rs x))). - TranslOpSimpl. - rewrite H1; auto. - (* Ointuoffloat *) -- replace v with (Val.maketotal (Val.intuoffloat (rs x))). - TranslOpSimpl. - rewrite H1; auto. - (* Ofloatofint *) -- replace v with (Val.maketotal (Val.floatofint (rs x))). - TranslOpSimpl. - rewrite H1; auto. - (* Ofloatofintu *) -- replace v with (Val.maketotal (Val.floatofintu (rs x))). TranslOpSimpl. rewrite H1; auto. (* Ocmp *) diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 07622a0e..9967bbae 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -166,7 +166,7 @@ Definition destroyed_by_op (op: operation): list mreg := | Ofloatconst _ => R12 :: nil | Osingleconst _ => R12 :: nil | Olongconst _ => R12 :: nil - | Ointoffloat | Ointuoffloat => F13 :: nil + | Ointoffloat => F13 :: nil | Olongoffloat => F13 :: nil | Oaddlimm _ => R12 :: nil | Oandlimm _ => R12 :: nil diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 5ea09bd8..74ee6b85 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -61,7 +61,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Osingleoffloat | Ofloatofsingle => op1 (default nv) - | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) + | Ointoffloat => op1 (default nv) | Ofloatofwords | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocmp c => needs_of_condition c diff --git a/powerpc/Op.v b/powerpc/Op.v index 0f082c1f..a96a0439 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -105,7 +105,7 @@ Inductive operation : Type := | Osubl: operation (**r [rd = r1 - r2] *) | Onegl: operation (**r [rd = - r1] *) | Omull: operation (**r [rd = r1 * r2] *) - | Omullhs: operation (**r [rd = high part of r1 * r2, signed] *) + | Omullhs: operation (**r [rd = high part of r1 * r2, signed] *) | Omullhu: operation (**r [rd = high part of r1 * r2, unsigned] *) | Odivl: operation (**r [rd = r1 / r2] (signed) *) | Odivlu: operation (**r [rd = r1 / r2] (unsigned) *) @@ -141,9 +141,6 @@ Inductive operation : Type := | Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) - | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] (PPC64 only) *) - | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] (PPC64 only) *) - | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] (PPC64 only *) | Ofloatofwords: operation (**r [rd = float_of_words(r1,r2)] *) (*c Manipulating 64-bit integers: *) | Omakelong: operation (**r [rd = r1 << 32 | r2] *) @@ -299,9 +296,6 @@ Definition eval_operation | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 - | Ointuoffloat, v1::nil => Val.intuoffloat v1 - | Ofloatofint, v1::nil => Val.floatofint v1 - | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2) | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) | Olowlong, v1::nil => Some(Val.loword v1) @@ -449,9 +443,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) - | Ointuoffloat => (Tfloat :: nil, Tint) - | Ofloatofint => (Tint :: nil, Tfloat) - | Ofloatofintu => (Tint :: nil, Tfloat) | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) @@ -570,9 +561,6 @@ Proof with (try exact I; try reflexivity). destruct v0... destruct v0... destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2... - destruct v0; simpl in H0; inv H0... - destruct v0; simpl in H0; inv H0... destruct v0; destruct v1... destruct v0; destruct v1... destruct v0... @@ -999,10 +987,6 @@ Proof. inv H4; simpl; auto. inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. - exists (Vint i); auto. - inv H4; simpl in H1; inv H1; simpl. TrivialExists. - inv H4; simpl in H1; inv H1; simpl. TrivialExists. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index ba6612e8..cd9a65df 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -468,7 +468,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := if Archi.ppc64 then - Eop Ointuoffloat (e ::: Enil) + Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil) else Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) @@ -482,7 +482,8 @@ Nondetfunction floatofintu (e: expr) := Eop (Ofloatconst (Float.of_intu n)) Enil | _ => if Archi.ppc64 then - Eop Ofloatofintu (e ::: Enil) else + Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil) + else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) end. @@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) := Eop (Ofloatconst (Float.of_int n)) Enil | _ => if Archi.ppc64 then - Eop Ofloatofint (e ::: Enil) else + Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: Enil) + else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: addimm Float.ox8000_0000 e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil) diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index c3eda068..7b34ea89 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -851,8 +851,13 @@ Proof. destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. destruct Archi.ppc64. - econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto. - set (im := Int.repr Int.half_modulus). +- apply Float.to_intu_to_long in Heqo. + econstructor. constructor. econstructor. econstructor; eauto. constructor. + simpl; rewrite Heqo; simpl; eauto. constructor. + simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto. + assert (Int.modulus < Int64.max_unsigned) by (compute; auto). + generalize (Int.unsigned_range n). omega. +- set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). constructor. auto. @@ -889,11 +894,12 @@ Theorem eval_floatofint: Proof. intros until y. unfold floatofint. destruct (floatofint_match a); intros. InvEval. TrivialExists. - destruct Archi.ppc64. - TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_int i)); split; auto. - set (t1 := addimm Float.ox8000_0000 a). + destruct Archi.ppc64. +- rewrite Float.of_int_of_long. + EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto. +- set (t1 := addimm Float.ox8000_0000 a). set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil). exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1. @@ -913,12 +919,12 @@ Theorem eval_floatofintu: Proof. intros until y. unfold floatofintu. destruct (floatofintu_match a); intros. InvEval. TrivialExists. - destruct Archi.ppc64. - TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_intu i)); split; auto. - unfold floatofintu. - set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)). + destruct Archi.ppc64. +- rewrite Float.of_intu_of_long. + EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto. +- set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil). exploit (eval_subf le t2). unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 0f608d25..43d2447d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -553,22 +553,16 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfcmpu(r1, r2) -> fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 - | Pfcfi(r1, r2) -> - assert false | Pfcfl(r1, r2) -> assert false | Pfcfid(r1, r2) -> fprintf oc " fcfid %a, %a\n" freg r1 freg r2 - | Pfcfiu(r1, r2) -> - assert false | Pfcti(r1, r2) -> assert false | Pfctid(r1, r2) -> assert false | Pfctidz(r1, r2) -> fprintf oc " fctidz %a, %a\n" freg r1 freg r2 - | Pfctiu(r1, r2) -> - assert false | Pfctiw(r1, r2) -> fprintf oc " fctiw %a, %a\n" freg r1 freg r2 | Pfctiwz(r1, r2) -> diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index a270d857..c81f1a6c 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -133,9 +133,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 - | Ointuoffloat, v1::nil => intuoffloat v1 - | Ofloatofint, v1::nil => floatofint v1 - | Ofloatofintu, v1::nil => floatofintu v1 | Ofloatofwords, v1::v2::nil => floatofwords v1 v2 | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 -- cgit From 5e3898945c063801d4a93f44182d160ccfe4badc Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Dec 2020 16:47:19 +0100 Subject: PowerPC modeling of registers destroyed by pseudo-instructions Inlined built-in functions destroy GPR0 --- powerpc/Asm.v | 2 +- powerpc/Asmgenproof.v | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 6ec20d62..d9901960 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -1195,7 +1195,7 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge vargs m t vres m' -> rs' = nextinstr (set_res res vres - (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> + (undef_regs (IR GPR0 :: map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index d653633c..a1ae5855 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -781,16 +781,18 @@ Opaque loadind. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. + rewrite set_res_other. simpl. rewrite undef_regs_other_2. + rewrite Pregmap.gso by auto with asmgen. rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. + eapply agree_undef_regs; eauto. + intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen. congruence. intros. Simpl. rewrite set_res_other by auto. - rewrite undef_regs_other_2; auto with asmgen. + simpl. rewrite undef_regs_other_2; auto with asmgen. - (* Mgoto *) assert (f0 = f) by congruence. subst f0. -- cgit