diff options
| -rw-r--r-- | backend/Mach.v | 77 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 12 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 117 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 81 |
4 files changed, 241 insertions, 46 deletions
diff --git a/backend/Mach.v b/backend/Mach.v index 212088f3..839a25bd 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -189,13 +189,19 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := | i1 :: il => if is_label lbl i1 then Some il else find_label lbl il end. -Lemma find_label_incl: - forall lbl c c', find_label lbl c = Some c' -> incl c' c. +Lemma find_label_tail: + forall lbl c c', find_label lbl c = Some c' -> is_tail c' c. Proof. induction c; simpl; intros. discriminate. destruct (is_label lbl a). inv H. auto with coqlib. eauto with coqlib. Qed. +Lemma find_label_incl: + forall lbl c c', find_label lbl c = Some c' -> incl c' c. +Proof. + intros; red; intros. eapply is_tail_incl; eauto. eapply find_label_tail; eauto. +Qed. + Section RELSEM. Variable return_address_offset: function -> code -> ptrofs -> Prop. @@ -426,3 +432,70 @@ Inductive final_state: state -> int -> Prop := Definition semantics (rao: function -> code -> ptrofs -> Prop) (p: program) := Semantics (step rao) (initial_state p) final_state (Genv.globalenv p). + +(** * Leaf functions *) + +(** A leaf function is a function that contains no [Mcall] instruction. *) + +Definition is_leaf_function (f: function) : bool := + List.forallb + (fun i => match i with Mcall _ _ => false | _ => true end) + f.(fn_code). + +(** Semantic characterization of leaf functions: + functions in the call stack are never leaf functions. *) + +Section WF_STATES. + +Variable rao: function -> code -> ptrofs -> Prop. + +Variable ge: genv. + +Inductive wf_frame: stackframe -> Prop := + | wf_stackframe_intro: forall fb sp ra c f + (CODE: Genv.find_funct_ptr ge fb = Some (Internal f)) + (LEAF: is_leaf_function f = false) + (TAIL: is_tail c f.(fn_code)), + wf_frame (Stackframe fb sp ra c). + +Inductive wf_state: state -> Prop := + | wf_normal_state: forall s fb sp c rs m f + (STACK: Forall wf_frame s) + (CODE: Genv.find_funct_ptr ge fb = Some (Internal f)) + (TAIL: is_tail c f.(fn_code)), + wf_state (State s fb sp c rs m) + | wf_call_state: forall s fb rs m + (STACK: Forall wf_frame s), + wf_state (Callstate s fb rs m) + | wf_return_state: forall s rs m + (STACK: Forall wf_frame s), + wf_state (Returnstate s rs m). + +Lemma wf_step: + forall S1 t S2, step rao ge S1 t S2 -> wf_state S1 -> wf_state S2. +Proof. + induction 1; intros WF; inv WF; try (econstructor; now eauto with coqlib). +- (* call *) + assert (f0 = f) by congruence. subst f0. + constructor. + constructor; auto. econstructor; eauto with coqlib. + destruct (is_leaf_function f) eqn:E; auto. + unfold is_leaf_function in E; rewrite forallb_forall in E. + symmetry. apply (E (Mcall sig ros)). eapply is_tail_in; eauto. +- (* goto *) + assert (f0 = f) by congruence. subst f0. econstructor; eauto using find_label_tail. +- (* cond *) + assert (f0 = f) by congruence. subst f0. econstructor; eauto using find_label_tail. +- (* jumptable *) + assert (f0 = f) by congruence. subst f0. econstructor; eauto using find_label_tail. +- (* return *) + inv STACK. inv H1. econstructor; eauto. +Qed. + +End WF_STATES. + +Lemma wf_initial: + forall p S, initial_state p S -> wf_state (Genv.globalenv p) S. +Proof. + intros. inv H. fold ge. constructor. constructor. +Qed. diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index fc04b15d..774f58f9 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -672,10 +672,14 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) do r <- ireg_of arg; OK (Pbtbl r tbl :: k) | Mreturn => - OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 :: - Pmtlr GPR0 :: - Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pblr :: k) + if is_leaf_function f then + OK (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pblr :: k) + else + OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 :: + Pmtlr GPR0 :: + Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pblr :: k) end. (** Translation of a code sequence *) diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 6f0390b9..68c19db0 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -385,7 +385,8 @@ Inductive match_states: Mach.state -> Asm.state -> Prop := (MEXT: Mem.extends m m') (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) (AG: agree ms sp rs) - (DXP: ep = true -> rs#GPR11 = parent_sp s), + (DXP: ep = true -> rs#GPR11 = parent_sp s) + (LEAF: is_leaf_function f = true -> rs#LR = parent_ra s), match_states (Mach.State s fb sp c ms m) (Asm.State rs m') | match_states_call: @@ -412,20 +413,22 @@ Lemma exec_straight_steps: Mem.extends m2 m2' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> + (is_leaf_function f = true -> rs1#LR = parent_ra s) -> (forall k c (TR: transl_instr f i ep k = OK c), exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2 - /\ (it1_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) -> + /\ (it1_is_parent ep i = true -> rs2#GPR11 = parent_sp s) + /\ rs2#LR = rs1#LR) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c ms2 m2) st'. Proof. - intros. inversion H2. subst. monadInv H7. - exploit H3; eauto. intros [rs2 [A [B C]]]. + intros. inversion H2. subst. monadInv H8. + exploit H4; eauto. intros (rs2 & A & B & C & D). exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. - econstructor; eauto. eapply exec_straight_at; eauto. + econstructor; eauto. eapply exec_straight_at; eauto. rewrite D; auto. Qed. Lemma exec_straight_steps_goto: @@ -436,19 +439,21 @@ Lemma exec_straight_steps_goto: Mach.find_label lbl f.(Mach.fn_code) = Some c' -> transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> it1_is_parent ep i = false -> + (is_leaf_function f = true -> rs1#LR = parent_ra s) -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' /\ agree ms2 sp rs2 - /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> + /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' + /\ rs2#LR = rs1#LR) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c' ms2 m2) st'. Proof. - intros. inversion H3. subst. monadInv H9. - exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. - generalize (functions_transl _ _ _ H7 H8); intro FN. - generalize (transf_function_no_overflow _ _ H8); intro NOOV. + intros. inversion H3. subst. monadInv H10. + exploit H6; eauto. intros (jmp & k' & rs2 & A & B & C & D). + generalize (functions_transl _ _ _ H8 H9); intro FN. + generalize (transf_function_no_overflow _ _ H9); intro NOOV. exploit exec_straight_steps_2; eauto. intros [ofs' [PC2 CT2]]. exploit find_label_goto_label; eauto. @@ -463,6 +468,7 @@ Proof. econstructor; eauto. apply agree_exten with rs2; auto with asmgen. congruence. + intros. rewrite OTH by congruence. rewrite D. auto. Qed. (** We need to show that, in the simulation diagram, we cannot @@ -490,7 +496,7 @@ Qed. Theorem step_simulation: forall S1 t S2, Mach.step return_address_offset ge S1 t S2 -> - forall S1' (MS: match_states S1 S1'), + forall S1' (MS: match_states S1 S1') (WF: wf_state ge S1), (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. Proof. @@ -499,7 +505,9 @@ Proof. - (* Mlabel *) left; eapply exec_straight_steps; eauto; intros. monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. apply agree_nextinstr; auto. simpl; congruence. + split. apply agree_nextinstr; auto. + split. simpl; congruence. + auto with asmgen. - (* Mgetstack *) unfold load_stack in H. @@ -509,7 +517,8 @@ Proof. exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]]. exists rs'; split. eauto. split. eapply agree_set_mreg; eauto with asmgen. congruence. - simpl; congruence. + split. simpl; congruence. + apply R; auto with asmgen. - (* Msetstack *) unfold store_stack in H. @@ -520,7 +529,8 @@ Proof. exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]]. exists rs'; split. eauto. split. eapply agree_undef_regs; eauto with asmgen. - simpl; intros. rewrite Q; auto with asmgen. + split. simpl; intros. rewrite Q; auto with asmgen. + rewrite Q; auto with asmgen. - (* Mgetparam *) assert (f0 = f) by congruence; subst f0. @@ -539,8 +549,9 @@ Opaque loadind. intros [rs1 [P [Q R]]]. exists rs1; split. eauto. split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. - simpl; intros. rewrite R; auto with asmgen. + split. simpl; intros. rewrite R; auto with asmgen. apply preg_of_not_GPR11; auto. + apply R; auto with asmgen. (* GPR11 does not contain parent *) monadInv TR. exploit loadind_correct. eexact EQ0. eauto. congruence. intros [rs1 [P [Q R]]]. simpl in Q. @@ -551,8 +562,9 @@ Opaque loadind. instantiate (1 := rs1#GPR11 <- (rs2#GPR11)). intros. rewrite Pregmap.gso; auto with asmgen. congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' GPR11). congruence. auto with asmgen. - simpl; intros. rewrite U; auto with asmgen. + split. simpl; intros. rewrite U; auto with asmgen. apply preg_of_not_GPR11; auto. + rewrite U; auto with asmgen. - (* Mop *) assert (eval_operation tge sp op rs##args m = Some v). @@ -562,10 +574,11 @@ Opaque loadind. left; eapply exec_straight_steps; eauto; intros. simpl in TR. exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. exists rs2; split. eauto. split. auto. - destruct op; simpl; try discriminate. intros. + split. destruct op; simpl; try discriminate. intros. destruct (andb_prop _ _ H1); clear H1. rewrite R; auto. apply preg_of_not_GPR11; auto. change (destroyed_by_op Omove) with (@nil mreg). simpl; auto. + apply R; auto with asmgen. - (* Mload *) assert (eval_addressing tge sp addr rs##args = Some a). @@ -578,7 +591,8 @@ Opaque loadind. exists rs2; split. eauto. split. eapply agree_set_undef_mreg; eauto. congruence. intros; auto with asmgen. - simpl; congruence. + split. simpl; congruence. + apply R; auto with asmgen. - (* Mstore *) assert (eval_addressing tge sp addr rs##args = Some a). @@ -591,7 +605,8 @@ Opaque loadind. intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. split. eapply agree_undef_regs; eauto with asmgen. - simpl; congruence. + split. simpl; congruence. + apply Q; auto with asmgen. - (* Mcall *) assert (f0 = f) by congruence. subst f0. @@ -757,6 +772,8 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. apply agree_nextinstr. eapply agree_set_res; auto. eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. congruence. + intros. Simpl. rewrite set_res_other by auto. + rewrite undef_regs_other_2; auto with asmgen. - (* Mgoto *) assert (f0 = f) by congruence. subst f0. @@ -770,6 +787,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. econstructor; eauto. eapply agree_exten; eauto with asmgen. congruence. + rewrite INV by congruence; auto. - (* Mcond true *) assert (f0 = f) by congruence. subst f0. @@ -782,11 +800,13 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. (* Pbt, taken *) econstructor; econstructor; econstructor; split. eexact A. split. eapply agree_exten; eauto with asmgen. - simpl. rewrite B. reflexivity. + split. simpl. rewrite B. reflexivity. + auto with asmgen. (* Pbf, taken *) econstructor; econstructor; econstructor; split. eexact A. split. eapply agree_exten; eauto with asmgen. - simpl. rewrite B. reflexivity. + split. simpl. rewrite B. reflexivity. + auto with asmgen. - (* Mcond false *) exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. @@ -800,7 +820,8 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. apply exec_straight_one. simpl. rewrite B. reflexivity. auto. split. eapply agree_exten; eauto with asmgen. intros; Simpl. - simpl. congruence. + split. simpl. congruence. + Simpl. - (* Mjumptable *) assert (f0 = f) by congruence. subst f0. @@ -822,6 +843,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. Local Transparent destroyed_by_jumptable. simpl. intros. rewrite C; auto with asmgen. Simpl. congruence. + intros. rewrite C by auto with asmgen. Simpl. - (* Mreturn *) assert (f0 = f) by congruence. subst f0. @@ -834,7 +856,36 @@ Local Transparent destroyed_by_jumptable. exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. - monadInv H6. + monadInv H6. destruct (is_leaf_function f) eqn:ISLEAF; monadInv EQ0. ++ (* leaf function *) + set (rs2 := nextinstr (rs0#GPR1 <- (parent_sp s))). + set (rs3 := rs2#PC <- (parent_ra s)). + assert (exec_straight tge tf + (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0 + (Pblr :: x) rs2 m2'). + simpl. apply exec_straight_one. + simpl. rewrite A. + rewrite <- (sp_val _ _ _ AG). rewrite E. auto. + auto. + left; exists (State rs3 m2'); split. + (* execution *) + apply plus_right' with E0 (State rs2 m2') E0. + eapply exec_straight_exec; eauto. + econstructor. + change (rs2 PC) with (Val.offset_ptr (rs0 PC) Ptrofs.one). + rewrite <- H3. simpl. eauto. + eapply functions_transl; eauto. + eapply find_instr_tail. + eapply code_tail_next_int; eauto. + simpl. change (rs2 LR) with (rs0 LR). rewrite LEAF by auto. reflexivity. + traceEq. + (* match states *) + econstructor; eauto. + assert (AG2: agree rs (parent_sp s) rs2). + unfold rs2. apply agree_nextinstr. eapply agree_change_sp; eauto. + eapply parent_sp_def; eauto. + unfold rs3; auto with asmgen. ++ (* non-leaf function *) set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))). set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). @@ -949,7 +1000,9 @@ Local Transparent destroyed_by_jumptable. inv STACKS. simpl in *. right. split. omega. split. auto. rewrite <- ATPC in H5. - econstructor; eauto. congruence. + econstructor; eauto. + congruence. + inv WF. inv STACK. inv H1. congruence. Qed. Lemma transf_initial_states: @@ -984,11 +1037,17 @@ Qed. Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. - eapply forward_simulation_star with (measure := measure). - apply senv_preserved. - eexact transf_initial_states. - eexact transf_final_states. - exact step_simulation. + eapply forward_simulation_star with + (measure := measure) + (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1). +- apply senv_preserved. +- simpl; intros. exploit transf_initial_states; eauto. intros (s2 & A & B). + exists s2; intuition auto. apply wf_initial; auto. +- simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto. +- simpl; intros. destruct H0 as [MS WF]. + exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ]. ++ left; exists s2'; intuition auto. eapply wf_step; eauto. ++ right; intuition auto. eapply wf_step; eauto. Qed. End PRESERVATION. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index a7dcf41e..fe496825 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -110,6 +110,49 @@ Proof. intros. rewrite Val.add_assoc. rewrite low_high_half. apply add_zero_symbol_address. Qed. +(** * Useful properties of registers *) + +(** [important_preg] extends [data_preg] by tracking the LR register as well. + It is used to state that a code sequence modifies no data registers + and does not modify LR either. *) + +Definition important_preg (r: preg) : bool := + match r with + | IR GPR0 => false + | PC => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true + end. + +Lemma important_diff: + forall r r', + important_preg r = true -> important_preg r' = false -> r <> r'. +Proof. + congruence. +Qed. +Hint Resolve important_diff: asmgen. + +Lemma important_data_preg_1: + forall r, data_preg r = true -> important_preg r = true. +Proof. + destruct r; simpl; auto; discriminate. +Qed. + +Lemma important_data_preg_2: + forall r, important_preg r = false -> data_preg r = false. +Proof. + intros. destruct (data_preg r) eqn:E; auto. apply important_data_preg_1 in E. congruence. +Qed. + +Hint Resolve important_data_preg_1 important_data_preg_2: asmgen. + +Lemma nextinstr_inv2: + forall r rs, important_preg r = true -> (nextinstr rs)#r = rs#r. +Proof. + intros. apply nextinstr_inv. red; intro; subst; discriminate. +Qed. + (** Useful properties of the GPR0 registers. *) Lemma gpr_or_zero_not_zero: @@ -138,11 +181,27 @@ Proof. Qed. Hint Resolve ireg_of_not_GPR0': asmgen. +(** Useful properties of the LR register *) + +Lemma preg_of_not_LR: + forall r, LR <> preg_of r. +Proof. + intros. auto using sym_not_equal with asmgen. +Qed. + +Lemma preg_notin_LR: + forall rl, preg_notin LR rl. +Proof. + intros. rewrite preg_notin_charact. intros. apply preg_of_not_LR. +Qed. + +Hint Resolve preg_of_not_LR preg_notin_LR: asmgen. + (** Useful simplification tactic *) Ltac Simplif := ((rewrite nextinstr_inv by eauto with asmgen) - || (rewrite nextinstr_inv1 by eauto with asmgen) + || (rewrite nextinstr_inv2 by eauto with asmgen) || (rewrite Pregmap.gss) || (rewrite nextinstr_pc) || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen. @@ -291,7 +350,7 @@ Lemma andimm_base_correct: exec_straight ge fn (andimm_base r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ rs'#CR0_2 = Val.cmp Ceq v Vzero - /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', important_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm_base. case (Int.eq (high_u n) Int.zero). @@ -336,7 +395,7 @@ Lemma andimm_correct: exists rs', exec_straight ge fn (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.and rs#r2 (Vint n) - /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', important_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm. destruct (is_rlw_mask n). (* turned into rlw *) @@ -416,7 +475,7 @@ Lemma rolm_correct: exists rs', exec_straight ge fn (rolm r1 r2 amount mask k) rs m k rs' m /\ rs'#r1 = Val.rolm rs#r2 amount mask - /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', important_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold rolm. destruct (is_rlw_mask mask). (* rlwinm *) @@ -610,7 +669,7 @@ Lemma transl_cond_correct_1: (if snd (crbit_for_cond cond) then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m))) - /\ forall r, data_preg r = true -> rs'#r = rs#r. + /\ forall r, important_preg r = true -> rs'#r = rs#r. Proof. intros. Opaque Int.eq. @@ -708,7 +767,7 @@ Lemma transl_cond_correct_2: (if snd (crbit_for_cond cond) then Val.of_bool b else Val.notbool (Val.of_bool b)) - /\ forall r, data_preg r = true -> rs'#r = rs#r. + /\ forall r, important_preg r = true -> rs'#r = rs#r. Proof. intros. replace (Val.of_bool b) @@ -735,7 +794,7 @@ Proof. exploit transl_cond_correct_2. eauto. eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [rs' [A [B C]]]. - exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto. + exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto with asmgen. Qed. (** Translation of condition operators *) @@ -792,7 +851,7 @@ Lemma transl_cond_op_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) - /\ forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'. + /\ forall r', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'. Proof. intros until args. unfold transl_cond_op. destruct (classify_condition cond args); intros; monadInv H; simpl; @@ -857,7 +916,7 @@ Lemma transl_op_correct_aux: exists rs', exec_straight ge fn c rs m k rs' m /\ Val.lessdef v rs'#(preg_of res) - /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. + /\ forall r, important_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. assert (SAME: forall v1 v2, v1 = v2 -> Val.lessdef v2 v1). { intros; subst; auto. } Opaque Int.eq. @@ -1000,14 +1059,14 @@ Lemma transl_op_correct: exists rs', exec_straight ge fn c rs m' k rs' m' /\ agree (Regmap.set res v (Mach.undef_regs (destroyed_by_op op) ms)) sp rs' - /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. + /\ forall r, important_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. intros. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [v' [A B]]. rewrite (sp_val _ _ _ H0) in A. exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]]. exists rs'; split. eexact P. - split. apply agree_set_undef_mreg with rs; auto. eapply Val.lessdef_trans; eauto. + split. apply agree_set_undef_mreg with rs; auto with asmgen. eapply Val.lessdef_trans; eauto. auto. Qed. |