diff options
Diffstat (limited to 'powerpc/ConstpropOpproof.v')
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index a28d908..584865a 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -49,7 +49,7 @@ Hypothesis MATCH: ematch bc rs ae. Lemma match_G: forall r id ofs, - AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (symbol_address ge id ofs). + AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (Genv.symbol_address ge id ofs). Proof. intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. Qed. @@ -82,7 +82,7 @@ Ltac SimplVM := rewrite E in *; clear H; SimplVM | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] => let E := fresh in - assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); + assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); clear H; SimplVM | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] => let E := fresh in @@ -436,13 +436,6 @@ Proof. exists v; auto. Qed. -Remark shift_symbol_address: - forall symb ofs n, - Op.symbol_address ge symb (Int.add ofs n) = Val.add (Op.symbol_address ge symb ofs) (Vint n). -Proof. - unfold Op.symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. -Qed. - Lemma addr_strength_reduction_correct: forall addr args vl res, vl = map (fun r => AE.get r ae) args -> @@ -453,8 +446,8 @@ Proof. intros until res. unfold addr_strength_reduction. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). -- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. -- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. +- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. - rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)). @@ -467,8 +460,8 @@ Proof. - fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. econstructor; split; eauto. - econstructor; split; eauto. -- rewrite shift_symbol_address. econstructor; split; eauto. -- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- rewrite Genv.shift_symbol_address. econstructor; split; eauto. +- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. - rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). econstructor; split; eauto. apply Val.add_lessdef; auto. |