diff options
-rw-r--r-- | arm/Asmgenproof.v | 16 | ||||
-rw-r--r-- | arm/Op.v | 72 |
2 files changed, 38 insertions, 50 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 713e012c..c687722c 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -50,6 +50,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma functions_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> @@ -748,7 +756,7 @@ Opaque loadind. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. @@ -770,7 +778,7 @@ Opaque loadind. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. @@ -927,7 +935,7 @@ Opaque loadind. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply agree_set_other; auto with asmgen. eapply agree_set_mregs; eauto. @@ -972,7 +980,7 @@ Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. @@ -720,36 +720,15 @@ Proof. intros. destruct c; simpl; auto; congruence. Qed. -(** Checking whether two addressings, applied to the same arguments, produce - separated memory addresses. Used in [CSE]. *) - -Definition addressing_separated (chunk1: memory_chunk) (addr1: addressing) - (chunk2: memory_chunk) (addr2: addressing) : bool := - match addr1, addr2 with - | Aindexed ofs1, Aindexed ofs2 => - Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) - | Ainstack ofs1, Ainstack ofs2 => - Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) - | _, _ => false +(** Global variables mentioned in an operation or addressing mode *) + +Definition globals_operation (op: operation) : list ident := + match op with + | Oaddrsymbol s ofs => s :: nil + | _ => nil end. -Lemma addressing_separated_sound: - forall (F V: Type) (ge: Genv.t F V) sp chunk1 addr1 chunk2 addr2 vl b1 n1 b2 n2, - addressing_separated chunk1 addr1 chunk2 addr2 = true -> - eval_addressing ge sp addr1 vl = Some(Vptr b1 n1) -> - eval_addressing ge sp addr2 vl = Some(Vptr b2 n2) -> - b1 <> b2 \/ Int.unsigned n1 + size_chunk chunk1 <= Int.unsigned n2 \/ Int.unsigned n2 + size_chunk chunk2 <= Int.unsigned n1. -Proof. - unfold addressing_separated; intros. - generalize (size_chunk_pos chunk1) (size_chunk_pos chunk2); intros SZ1 SZ2. - destruct addr1; destruct addr2; try discriminate; simpl in *; FuncInv. -(* Aindexed *) - destruct v; simpl in *; inv H1; inv H2. - right. apply Int.no_overlap_sound; auto. -(* Ainstack *) - destruct sp; simpl in *; inv H1; inv H2. - right. apply Int.no_overlap_sound; auto. -Qed. +Definition globals_addressing (addr: addressing) : list ident := nil. (** * Invariance and compatibility properties. *) @@ -791,14 +770,11 @@ End GENV_TRANSF. Section EVAL_COMPAT. -Variable F V: Type. -Variable genv: Genv.t F V. +Variable F1 F2 V1 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. Variable f: meminj. -Hypothesis symbol_address_inj: - forall id ofs, - val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). - Variable m1: mem. Variable m2: mem. @@ -885,12 +861,16 @@ Ltac TrivialExists := Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_operation op) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_operation genv sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + eval_operation ge1 sp1 op vl1 m1 = Some v1 -> + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + apply GL; simpl; auto. apply Values.val_add_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. @@ -976,15 +956,15 @@ Qed. Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_addressing addr) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_addressing genv sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + eval_addressing ge1 sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. Proof. - assert (UNUSED: forall id ofs, - val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs)). - exact symbol_address_inj. - intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. apply eval_shift_inj; auto. @@ -1069,11 +1049,11 @@ Proof. eval_operation genv sp op vl2 m2 = Some v2 /\ val_inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). - intros. rewrite <- val_inject_lessdef; auto. apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. apply valid_different_pointers_extends; auto. + intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. eauto. auto. destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. @@ -1144,7 +1124,7 @@ Proof. intros. rewrite eval_shift_stack_addressing. simpl. eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. - exact symbol_address_inject. + intros; apply symbol_address_inject. Qed. Lemma eval_operation_inject: @@ -1159,11 +1139,11 @@ Proof. intros. rewrite eval_shift_stack_operation. simpl. eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. - exact symbol_address_inject. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. + intros; apply symbol_address_inject. Qed. End EVAL_INJECT. |