diff options
Diffstat (limited to 'backend/Machabstr2concr.v')
| -rw-r--r-- | backend/Machabstr2concr.v | 669 |
1 files changed, 434 insertions, 235 deletions
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 89529fd..7714f3d 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -74,19 +74,27 @@ Hypothesis wt_f: wt_function f. semantics. [ms] is the current memory state in the concrete semantics. The stack pointer is [Vptr sp base] in both semantics. *) -Inductive frame_match (fr: frame) - (sp: block) (base: int) - (mm ms: mem) : Prop := - frame_match_intro: - valid_block ms sp -> - low_bound mm sp = 0 -> - low_bound ms sp = -f.(fn_framesize) -> - high_bound ms sp >= 0 -> - base = Int.repr (-f.(fn_framesize)) -> - (forall ty ofs, - -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) -> - load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) -> - frame_match fr sp base mm ms. +Record frame_match (fr: frame) + (sp: block) (base: int) + (mm ms: mem) : Prop := + mk_frame_match { + fm_valid_1: + Mem.valid_block mm sp; + fm_valid_2: + Mem.valid_block ms sp; + fm_base: + base = Int.repr(- f.(fn_framesize)); + fm_stackdata_pos: + Mem.low_bound mm sp = 0; + fm_write_perm: + Mem.range_perm ms sp (-f.(fn_framesize)) 0 Freeable; + fm_contents_match: + forall ty ofs, + -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) -> + exists v, + Mem.load (chunk_of_type ty) ms sp ofs = Some v + /\ Val.lessdef (fr ty ofs) v + }. (** The following two innocuous-looking lemmas are the key results showing that [sp]-relative memory accesses in the concrete @@ -94,8 +102,8 @@ Inductive frame_match (fr: frame) semantics. First, a value [v] that has type [ty] is preserved when stored in memory with chunk [chunk_of_type ty], then read back with the same chunk. The typing hypothesis is crucial here: - for instance, a float value reads back as [Vundef] when stored - and load with chunk [Mint32]. *) + for instance, a float value is not preserved when stored + and loaded with chunk [Mint32]. *) Lemma load_result_ty: forall v ty, @@ -127,14 +135,15 @@ Lemma frame_match_load_stack: frame_match fr sp base mm ms -> 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> (4 | Int.signed ofs) -> - load_stack ms (Vptr sp base) ty ofs = - Some (fr ty (Int.signed ofs - f.(fn_framesize))). + exists v, + load_stack ms (Vptr sp base) ty ofs = Some v + /\ Val.lessdef (fr ty (Int.signed ofs - f.(fn_framesize))) v. Proof. intros. inv H. inv wt_f. - unfold load_stack, Val.add, loadv. + unfold load_stack, Val.add, Mem.loadv. replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs)) with (Int.signed ofs - fn_framesize f). - apply H7. omega. omega. + apply fm_contents_match0. omega. omega. apply Zdivide_minus_l; auto. assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). apply Int.signed_repr. @@ -149,9 +158,9 @@ Lemma frame_match_get_slot: forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> get_slot f fr ty (Int.signed ofs) v -> - load_stack ms (Vptr sp base) ty ofs = Some v. + exists v', load_stack ms (Vptr sp base) ty ofs = Some v' /\ Val.lessdef v v'. Proof. - intros. inversion H. inv H0. inv H7. eapply frame_match_load_stack; eauto. + intros. inv H0. inv H1. eapply frame_match_load_stack; eauto. Qed. (** Assigning a value to a frame slot (in the abstract semantics) @@ -160,19 +169,20 @@ Qed. and activation records is preserved. *) Lemma frame_match_store_stack: - forall fr sp base mm ms ty ofs v, + forall fr sp base mm ms ty ofs v v', frame_match fr sp base mm ms -> - 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + 0 <= Int.signed ofs -> Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> (4 | Int.signed ofs) -> Val.has_type v ty -> + Val.lessdef v v' -> Mem.extends mm ms -> exists ms', - store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ + store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\ frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\ Mem.extends mm ms'. Proof. intros. inv H. inv wt_f. - unfold store_stack, Val.add, storev. + unfold store_stack, Val.add, Mem.storev. assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) = Int.signed ofs - fn_framesize f). assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). @@ -183,58 +193,84 @@ Proof. apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. compute; congruence. rewrite H. - assert (exists ms', store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v = Some ms'). - apply valid_access_store. - constructor. auto. omega. - rewrite size_type_chunk. omega. + assert ({ ms' | Mem.store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v' = Some ms'}). + apply Mem.valid_access_store. constructor. + apply Mem.range_perm_implies with Freeable; auto with mem. + red; intros; apply fm_write_perm0. + rewrite <- size_type_chunk in H1. + generalize (size_chunk_pos (chunk_of_type ty)). + omega. replace (align_chunk (chunk_of_type ty)) with 4. apply Zdivide_minus_l; auto. destruct ty; auto. - destruct H8 as [ms' STORE]. - generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB. - generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB. + destruct X as [ms' STORE]. exists ms'. split. exact STORE. (* frame match *) - split. constructor; try congruence. - eauto with mem. intros. unfold update. - destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0. + split. constructor. + (* valid *) + eauto with mem. + eauto with mem. + (* base *) + auto. + (* stackdata_pos *) + auto. + (* write_perm *) + red; intros; eauto with mem. + (* contents *) + intros. + exploit fm_contents_match0; eauto. intros [v0 [LOAD0 VLD0]]. + assert (exists v1, Mem.load (chunk_of_type ty0) ms' sp ofs0 = Some v1). + apply Mem.valid_access_load; eauto with mem. + destruct H9 as [v1 LOAD1]. + exists v1; split; auto. + unfold update. + destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0. destruct (typ_eq ty ty0). subst ty0. (* same *) - transitivity (Some (Val.load_result (chunk_of_type ty) v)). - eapply load_store_same; eauto. - decEq. apply load_result_ty; auto. + inv H4. + assert (Some v1 = Some (Val.load_result (chunk_of_type ty) v')). + rewrite <- LOAD1. eapply Mem.load_store_same; eauto. + replace (type_of_chunk (chunk_of_type ty)) with ty. auto. + destruct ty; auto. + inv H4. rewrite load_result_ty; auto. + auto. (* mismatch *) - eapply load_store_mismatch'; eauto with mem. - destruct ty; destruct ty0; simpl; congruence. + auto. destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)). (* disjoint *) - rewrite <- H9; auto. eapply load_store_other; eauto. - right; left. rewrite size_type_chunk; auto. + assert (Some v1 = Some v0). + rewrite <- LOAD0; rewrite <- LOAD1. + eapply Mem.load_store_other; eauto. + right; left. rewrite size_type_chunk; auto. + inv H9. auto. destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)). - rewrite <- H9; auto. eapply load_store_other; eauto. - right; right. rewrite size_type_chunk; auto. + assert (Some v1 = Some v0). + rewrite <- LOAD0; rewrite <- LOAD1. + eapply Mem.load_store_other; eauto. + right; right. rewrite size_type_chunk; auto. + inv H9. auto. (* overlap *) - eapply load_store_overlap'; eauto with mem. - rewrite size_type_chunk; auto. - rewrite size_type_chunk; auto. + auto. (* extends *) - eapply store_outside_extends; eauto. - left. rewrite size_type_chunk. omega. + eapply Mem.store_outside_extends; eauto. + left. rewrite fm_stackdata_pos0. + rewrite size_type_chunk. omega. Qed. Lemma frame_match_set_slot: - forall fr sp base mm ms ty ofs v fr', + forall fr sp base mm ms ty ofs v fr' v', frame_match fr sp base mm ms -> set_slot f fr ty (Int.signed ofs) v fr' -> Val.has_type v ty -> + Val.lessdef v v' -> Mem.extends mm ms -> exists ms', - store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ + store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\ frame_match fr' sp base mm ms' /\ Mem.extends mm ms'. Proof. - intros. inv H0. inv H3. eapply frame_match_store_stack; eauto. + intros. inv H0. inv H4. eapply frame_match_store_stack; eauto. Qed. (** Agreement is preserved by stores within blocks other than the @@ -243,45 +279,40 @@ Qed. Lemma frame_match_store_other: forall fr sp base mm ms chunk b ofs v ms', frame_match fr sp base mm ms -> - store chunk ms b ofs v = Some ms' -> + Mem.store chunk ms b ofs v = Some ms' -> sp <> b -> frame_match fr sp base mm ms'. Proof. - intros. inv H. - generalize (low_bound_store _ _ _ _ _ _ H0 sp). intro LB. - generalize (high_bound_store _ _ _ _ _ _ H0 sp). intro HB. - apply frame_match_intro; auto. - eauto with mem. - congruence. - congruence. - intros. rewrite <- H7; auto. - eapply load_store_other; eauto. + intros. inv H. constructor; auto. + eauto with mem. + red; intros; eauto with mem. + intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]]. + exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto. Qed. (** Agreement is preserved by parallel stores in the Machabstr and the Machconcr semantics. *) Lemma frame_match_store: - forall fr sp base mm ms chunk b ofs v mm' ms', + forall fr sp base mm ms chunk b ofs v mm' v' ms', frame_match fr sp base mm ms -> - store chunk mm b ofs v = Some mm' -> - store chunk ms b ofs v = Some ms' -> + Mem.store chunk mm b ofs v = Some mm' -> + Mem.store chunk ms b ofs v' = Some ms' -> frame_match fr sp base mm' ms'. Proof. - intros. inv H. - generalize (low_bound_store _ _ _ _ _ _ H0 sp). intro LBm. - generalize (low_bound_store _ _ _ _ _ _ H1 sp). intro LBs. - generalize (high_bound_store _ _ _ _ _ _ H0 sp). intro HBm. - generalize (high_bound_store _ _ _ _ _ _ H1 sp). intro HBs. - apply frame_match_intro; auto. + intros. inv H. constructor; auto. eauto with mem. - congruence. congruence. congruence. - intros. rewrite <- H7; auto. eapply load_store_other; eauto. - destruct (zeq sp b). subst b. right. + eauto with mem. + rewrite (Mem.bounds_store _ _ _ _ _ _ H0). auto. + red; intros; eauto with mem. + intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]]. + exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto. + destruct (zeq sp b); auto. subst b. right. rewrite size_type_chunk. - assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H9. left. omega. - auto. + assert (Mem.valid_access mm chunk sp ofs Nonempty) by eauto with mem. + exploit Mem.store_valid_access_3. eexact H0. intro. + exploit Mem.valid_access_in_bounds. eauto. rewrite fm_stackdata_pos0. + omega. Qed. (** Memory allocation of the Cminor stack data block (in the abstract @@ -291,68 +322,111 @@ Qed. remain true. *) Lemma frame_match_new: - forall mm ms mm' ms' sp sp', - mm.(nextblock) = ms.(nextblock) -> - alloc mm 0 f.(fn_stacksize) = (mm', sp) -> - alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') -> - sp = sp' /\ + forall mm ms mm' ms' sp, + Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) -> + Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp) -> frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'. Proof. intros. - assert (sp = sp'). - exploit alloc_result. eexact H0. exploit alloc_result. eexact H1. - congruence. - subst sp'. split. auto. - generalize (low_bound_alloc_same _ _ _ _ _ H0). intro LBm. - generalize (low_bound_alloc_same _ _ _ _ _ H1). intro LBs. - generalize (high_bound_alloc_same _ _ _ _ _ H0). intro HBm. - generalize (high_bound_alloc_same _ _ _ _ _ H1). intro HBs. inv wt_f. constructor; simpl; eauto with mem. - rewrite HBs. auto. - intros. - eapply load_alloc_same'; eauto. + rewrite (Mem.bounds_alloc_same _ _ _ _ _ H). auto. + red; intros. eapply Mem.perm_alloc_2; eauto. omega. + intros. exists Vundef; split. + eapply Mem.load_alloc_same'; eauto. rewrite size_type_chunk. omega. - replace (align_chunk (chunk_of_type ty)) with 4; auto. destruct ty; auto. + replace (align_chunk (chunk_of_type ty)) with 4; auto. + destruct ty; auto. + unfold empty_frame. auto. Qed. Lemma frame_match_alloc: - forall mm ms fr sp base lom him los his mm' ms' bm bs, - mm.(nextblock) = ms.(nextblock) -> + forall mm ms fr sp base lom him los his mm' ms' b, frame_match fr sp base mm ms -> - alloc mm lom him = (mm', bm) -> - alloc ms los his = (ms', bs) -> + Mem.alloc mm lom him = (mm', b) -> + Mem.alloc ms los his = (ms', b) -> frame_match fr sp base mm' ms'. Proof. - intros. inversion H0. - assert (valid_block mm sp). red. rewrite H. auto. - exploit low_bound_alloc_other. eexact H1. eexact H9. intro LBm. - exploit high_bound_alloc_other. eexact H1. eexact H9. intro HBm. - exploit low_bound_alloc_other. eexact H2. eexact H3. intro LBs. - exploit high_bound_alloc_other. eexact H2. eexact H3. intro HBs. - apply frame_match_intro. - eapply valid_block_alloc; eauto. - congruence. congruence. congruence. auto. auto. - intros. eapply load_alloc_other; eauto. + intros. inversion H. + assert (sp <> b). + apply Mem.valid_not_valid_diff with ms; eauto with mem. + constructor; auto. + eauto with mem. + eauto with mem. + rewrite (Mem.bounds_alloc_other _ _ _ _ _ H0); auto. + red; intros; eauto with mem. + intros. exploit fm_contents_match0; eauto. intros [v [LOAD LD]]. + exists v; split; auto. eapply Mem.load_alloc_other; eauto. Qed. (** [frame_match] relations are preserved by freeing a block other than the one pointed to by [sp]. *) Lemma frame_match_free: - forall fr sp base mm ms b, + forall fr sp base mm ms b lom him los his mm' ms', frame_match fr sp base mm ms -> sp <> b -> - frame_match fr sp base (free mm b) (free ms b). + Mem.free mm b lom him = Some mm' -> + Mem.free ms b los his = Some ms' -> + frame_match fr sp base mm' ms'. +Proof. + intros. inversion H. constructor; auto. + eauto with mem. + eauto with mem. + rewrite (Mem.bounds_free _ _ _ _ _ H1). auto. + red; intros; eauto with mem. + intros. rewrite (Mem.load_free _ _ _ _ _ H2); auto. +Qed. + +Lemma frame_match_delete: + forall fr sp base mm ms mm', + frame_match fr sp base mm ms -> + Mem.free mm sp 0 f.(fn_stacksize) = Some mm' -> + Mem.extends mm ms -> + exists ms', + Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms' + /\ Mem.extends mm' ms'. Proof. intros. inversion H. - generalize (low_bound_free mm _ _ H0); intro LBm. - generalize (low_bound_free ms _ _ H0); intro LBs. - generalize (high_bound_free mm _ _ H0); intro HBm. - generalize (high_bound_free ms _ _ H0); intro HBs. - apply frame_match_intro; auto. - congruence. congruence. congruence. - intros. rewrite <- H6; auto. apply load_free. auto. + assert (Mem.range_perm mm sp 0 (fn_stacksize f) Freeable). + eapply Mem.free_range_perm; eauto. + assert ({ ms' | Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms' }). + apply Mem.range_perm_free. + red; intros. destruct (zlt ofs 0). + apply fm_write_perm0. omega. + eapply Mem.perm_extends; eauto. apply H2. omega. + destruct X as [ms' FREE]. exists ms'; split; auto. + eapply Mem.free_right_extends; eauto. + eapply Mem.free_left_extends; eauto. + intros; red; intros. + exploit Mem.perm_in_bounds; eauto. + rewrite (Mem.bounds_free _ _ _ _ _ H0). rewrite fm_stackdata_pos0; intro. + exploit Mem.perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. + auto. +Qed. + +(** [frame_match] is preserved by external calls. *) + +Lemma frame_match_external_call: + forall fr sp base mm ms mm' ms' ef vargs vres t vargs' vres', + frame_match fr sp base mm ms -> + Mem.extends mm ms -> + external_call ef vargs mm t vres mm' -> + Mem.extends mm' ms' -> + external_call ef vargs' ms t vres' ms' -> + mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> + frame_match fr sp base mm' ms'. +Proof. + intros. destruct H4 as [A B]. inversion H. constructor. + eapply external_call_valid_block; eauto. + eapply external_call_valid_block; eauto. + auto. + rewrite (external_call_bounds _ _ _ _ _ _ _ H1); auto. + red; intros. apply A; auto. red. omega. + intros. exploit fm_contents_match0; eauto. intros [v [C D]]. + exists v; split; auto. + apply B; auto. + rewrite size_type_chunk; intros; red. omega. Qed. End FRAME_MATCH. @@ -430,61 +504,130 @@ Proof. simpl. omega. Qed. +Definition is_pointer_or_int (v: val) : Prop := + match v with + | Vint _ => True + | Vptr _ _ => True + | _ => False + end. + +Remark is_pointer_has_type: + forall v, is_pointer_or_int v -> Val.has_type v Tint. +Proof. + intros; destruct v; elim H; exact I. +Qed. + +Lemma frame_match_load_stack_pointer: + forall fr sp base mm ms ty ofs, + frame_match f fr sp base mm ms -> + 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + (4 | Int.signed ofs) -> + is_pointer_or_int (fr ty (Int.signed ofs - f.(fn_framesize))) -> + load_stack ms (Vptr sp base) ty ofs = Some (fr ty (Int.signed ofs - f.(fn_framesize))). +Proof. + intros. exploit frame_match_load_stack; eauto. + intros [v [LOAD LD]]. + inv LD. auto. rewrite <- H4 in H2. elim H2. +Qed. + Lemma frame_match_load_link: forall fr sp base mm ms, frame_match f (extend_frame fr) sp base mm ms -> - load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs). + is_pointer_or_int (parent_sp cs) -> + load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some(parent_sp cs). Proof. intros. inversion wt_f. - replace (parent_sp cs) with - (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). - eapply frame_match_load_stack; eauto. - - unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. + assert (parent_sp cs = + extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). + unfold extend_frame. rewrite update_other. rewrite update_same. auto. + simpl. omega. + rewrite H1; eapply frame_match_load_stack_pointer; eauto. + rewrite <- H1; auto. Qed. Lemma frame_match_load_retaddr: forall fr sp base mm ms, frame_match f (extend_frame fr) sp base mm ms -> - load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs). + is_pointer_or_int (parent_ra cs) -> + load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some(parent_ra cs). Proof. intros. inversion wt_f. - replace (parent_ra cs) with - (extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))). - eapply frame_match_load_stack; eauto. - unfold extend_frame. apply update_same. + assert (parent_ra cs = + extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))). + unfold extend_frame. rewrite update_same. auto. + rewrite H1; eapply frame_match_load_stack_pointer; eauto. + rewrite <- H1; auto. Qed. Lemma frame_match_function_entry: - forall mm ms mm' ms1 sp sp', - extends mm ms -> - alloc mm 0 f.(fn_stacksize) = (mm', sp) -> - alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') -> - Val.has_type (parent_sp cs) Tint -> - Val.has_type (parent_ra cs) Tint -> + forall mm ms mm' sp, + Mem.extends mm ms -> + Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) -> + is_pointer_or_int (parent_sp cs) -> + is_pointer_or_int (parent_ra cs) -> let base := Int.repr (-f.(fn_framesize)) in - exists ms2, exists ms3, - sp = sp' /\ + exists ms1, exists ms2, exists ms3, + Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp) /\ store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\ store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\ frame_match f (extend_frame empty_frame) sp base mm' ms3 /\ - extends mm' ms3. + Mem.extends mm' ms3. Proof. intros. inversion wt_f. - exploit alloc_extends; eauto. omega. omega. intros [A EXT0]. - exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto. - fold base. intros [C FM0]. - destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM0 wt_function_link wt_function_link_aligned H2 EXT0) - as [ms2 [STORE1 [FM1 EXT1]]]. - destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM1 wt_function_retaddr wt_function_retaddr_aligned H3 EXT1) - as [ms3 [STORE2 [FM3 EXT3]]]. - exists ms2; exists ms3; auto. + exploit Mem.alloc_extends; eauto. + instantiate (1 := -f.(fn_framesize)). omega. + instantiate (1 := f.(fn_stacksize)). omega. + intros [ms1 [A EXT0]]. + exploit frame_match_new; eauto. fold base. intros FM0. + exploit frame_match_store_stack. eauto. eexact FM0. + instantiate (1 := fn_link_ofs f); omega. + instantiate (1 := Tint). simpl; omega. + auto. apply is_pointer_has_type. eexact H1. constructor. auto. + intros [ms2 [STORE1 [FM1 EXT1]]]. + exploit frame_match_store_stack. eauto. eexact FM1. + instantiate (1 := fn_retaddr_ofs f); omega. + instantiate (1 := Tint). simpl; omega. + auto. apply is_pointer_has_type. eexact H2. constructor. auto. + intros [ms3 [STORE2 [FM2 EXT2]]]. + exists ms1; exists ms2; exists ms3; auto. Qed. End EXTEND_FRAME. +(** ** The ``less defined than'' relation between register states. *) + +Definition regset_lessdef (rs1 rs2: regset) : Prop := + forall r, Val.lessdef (rs1 r) (rs2 r). + +Lemma regset_lessdef_list: + forall rs1 rs2, regset_lessdef rs1 rs2 -> + forall rl, Val.lessdef_list (rs1##rl) (rs2##rl). +Proof. + induction rl; simpl. + constructor. + constructor; auto. +Qed. + +Lemma regset_lessdef_set: + forall rs1 rs2 r v1 v2, + regset_lessdef rs1 rs2 -> Val.lessdef v1 v2 -> + regset_lessdef (rs1#r <- v1) (rs2#r <- v2). +Proof. + intros; red; intros. unfold Regmap.set. + destruct (RegEq.eq r0 r); auto. +Qed. + +Lemma regset_lessdef_find_function_ptr: + forall ge ros rs1 rs2 fb, + find_function_ptr ge ros rs1 = Some fb -> + regset_lessdef rs1 rs2 -> + find_function_ptr ge ros rs2 = Some fb. +Proof. + unfold find_function_ptr; intros; destruct ros; simpl in *. + generalize (H0 m); intro LD; inv LD. auto. rewrite <- H2 in H. congruence. + auto. +Qed. + (** ** Invariant for stacks *) Section SIMULATION. @@ -518,12 +661,26 @@ Inductive match_stacks: wt_function f -> frame_match f (extend_frame f ts fr) sp base mm ms -> stack_below ts sp -> - Val.has_type ra Tint -> + is_pointer_or_int ra -> match_stacks s ts mm ms -> match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s) (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts) mm ms. +Lemma match_stacks_parent_sp_pointer: + forall s ts mm ms, + match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_sp ts). +Proof. + induction 1; simpl; auto. +Qed. + +Lemma match_stacks_parent_ra_pointer: + forall s ts mm ms, + match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_ra ts). +Proof. + induction 1; simpl; auto. +Qed. + (** If [match_stacks] holds, a lookup in the parent frame in the Machabstr semantics corresponds to two memory loads in the Machconcr semantics, one to load the pointer to the parent's @@ -533,7 +690,9 @@ Lemma match_stacks_get_parent: forall s ts mm ms ty ofs v, match_stacks s ts mm ms -> get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v -> - load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v. + exists v', + load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v' + /\ Val.lessdef v v'. Proof. intros. inv H; simpl in H0. inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega. @@ -542,7 +701,7 @@ Proof. Qed. (** Preservation of the [match_stacks] invariant - by various kinds of memory stores. *) + by various kinds of memory operations. *) Remark stack_below_trans: forall ts b b', @@ -556,7 +715,7 @@ Lemma match_stacks_store_other: forall s ts ms mm, match_stacks s ts mm ms -> forall chunk b ofs v ms', - store chunk ms b ofs v = Some ms' -> + Mem.store chunk ms b ofs v = Some ms' -> stack_below ts b -> match_stacks s ts mm ms'. Proof. @@ -593,9 +752,9 @@ Qed. Lemma match_stacks_store: forall s ts ms mm, match_stacks s ts mm ms -> - forall chunk b ofs v mm' ms', - store chunk mm b ofs v = Some mm' -> - store chunk ms b ofs v = Some ms' -> + forall chunk b ofs v mm' v' ms', + Mem.store chunk mm b ofs v = Some mm' -> + Mem.store chunk ms b ofs v' = Some ms' -> match_stacks s ts mm' ms'. Proof. induction 1; intros. @@ -607,28 +766,28 @@ Qed. Lemma match_stacks_alloc: forall s ts ms mm, match_stacks s ts mm ms -> - forall lom him mm' bm los his ms' bs, - mm.(nextblock) = ms.(nextblock) -> - alloc mm lom him = (mm', bm) -> - alloc ms los his = (ms', bs) -> + forall lom him mm' b los his ms', + Mem.alloc mm lom him = (mm', b) -> + Mem.alloc ms los his = (ms', b) -> match_stacks s ts mm' ms'. Proof. induction 1; intros. constructor. - econstructor; eauto. - eapply frame_match_alloc; eauto. + econstructor; eauto. eapply frame_match_alloc; eauto. Qed. Lemma match_stacks_free: forall s ts ms mm, match_stacks s ts mm ms -> - forall b, + forall b lom him los his mm' ms', + Mem.free mm b lom him = Some mm' -> + Mem.free ms b los his = Some ms' -> stack_below ts b -> - match_stacks s ts (Mem.free mm b) (Mem.free ms b). + match_stacks s ts mm' ms'. Proof. induction 1; intros. constructor. - red in H5; simpl in H5. + red in H7; simpl in H7. econstructor; eauto. eapply frame_match_free; eauto. unfold block; omega. eapply IHmatch_stacks; eauto. @@ -636,21 +795,36 @@ Proof. Qed. Lemma match_stacks_function_entry: - forall s ts mm ms lom him mm' los his ms' stk, + forall s ts ms mm, match_stacks s ts mm ms -> - alloc mm lom him = (mm', stk) -> - alloc ms los his = (ms', stk) -> + forall lom him mm' stk los his ms', + Mem.alloc mm lom him = (mm', stk) -> + Mem.alloc ms los his = (ms', stk) -> match_stacks s ts mm' ms' /\ stack_below ts stk. Proof. intros. - assert (stk = nextblock mm). eapply Mem.alloc_result; eauto. - assert (stk = nextblock ms). eapply Mem.alloc_result; eauto. - split. - eapply match_stacks_alloc; eauto. congruence. - red. - inv H; simpl. - unfold nullptr. apply Zgt_lt. apply nextblock_pos. - inv H6. red in H. rewrite H3. auto. + assert (stk = Mem.nextblock mm) by eauto with mem. + split. eapply match_stacks_alloc; eauto. + red. inv H; simpl. + unfold Mem.nullptr. apply Zgt_lt. apply Mem.nextblock_pos. + inv H5. auto. +Qed. + +Lemma match_stacks_external_call: + forall s ts mm ms, + match_stacks s ts mm ms -> + forall ef vargs t vres mm' ms' vargs' vres', + Mem.extends mm ms -> + external_call ef vargs mm t vres mm' -> + Mem.extends mm' ms' -> + external_call ef vargs' ms t vres' ms' -> + mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> + match_stacks s ts mm' ms'. +Proof. + induction 1; intros. + constructor. + econstructor; eauto. + eapply frame_match_external_call; eauto. Qed. (** ** Invariant between states. *) @@ -666,27 +840,30 @@ Qed. Inductive match_states: Machabstr.state -> Machconcr.state -> Prop := | match_states_intro: - forall s f sp base c rs fr mm ts fb ms + forall s f sp base c rs fr mm ts trs fb ms (STACKS: match_stacks s ts mm ms) (FM: frame_match f (extend_frame f ts fr) sp base mm ms) (BELOW: stack_below ts sp) + (RLD: regset_lessdef rs trs) (MEXT: Mem.extends mm ms) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)), match_states (Machabstr.State s f (Vptr sp base) c rs fr mm) - (Machconcr.State ts fb (Vptr sp base) c rs ms) + (Machconcr.State ts fb (Vptr sp base) c trs ms) | match_states_call: - forall s f rs mm ts fb ms + forall s f rs mm ts trs fb ms (STACKS: match_stacks s ts mm ms) (MEXT: Mem.extends mm ms) + (RLD: regset_lessdef rs trs) (FIND: Genv.find_funct_ptr ge fb = Some f), match_states (Machabstr.Callstate s f rs mm) - (Machconcr.Callstate ts fb rs ms) + (Machconcr.Callstate ts fb trs ms) | match_states_return: - forall s rs mm ts ms + forall s rs mm ts trs ms (STACKS: match_stacks s ts mm ms) - (MEXT: Mem.extends mm ms), + (MEXT: Mem.extends mm ms) + (RLD: regset_lessdef rs trs), match_states (Machabstr.Returnstate s rs mm) - (Machconcr.Returnstate ts rs ms). + (Machconcr.Returnstate ts trs ms). (** * The proof of simulation *) @@ -725,20 +902,26 @@ Qed. (** Preservation of arguments to external functions. *) Lemma transl_extcall_arguments: - forall rs s sg args ts m ms, + forall rs s sg args ts trs m ms, Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args -> + regset_lessdef rs trs -> match_stacks s ts m ms -> - extcall_arguments rs ms (parent_sp ts) sg args. + exists targs, + extcall_arguments trs ms (parent_sp ts) sg targs + /\ Val.lessdef_list args targs. Proof. unfold Machabstr.extcall_arguments, extcall_arguments; intros. - assert (forall locs vals, - Machabstr.extcall_args (parent_function s) rs (parent_frame s) locs vals -> - extcall_args rs ms (parent_sp ts) locs vals). - induction locs; intros; inv H1. - constructor. + generalize (Conventions.loc_arguments sg) args H. + induction l; intros; inv H2. + exists (@nil val); split; constructor. + exploit IHl; eauto. intros [targs [A B]]. + inv H7. exists (trs r :: targs); split. + constructor; auto. constructor. + constructor; auto. + exploit match_stacks_get_parent; eauto. intros [targ [C D]]. + exists (targ :: targs); split. + constructor; auto. constructor; auto. constructor; auto. - inv H6. constructor. constructor. eapply match_stacks_get_parent; eauto. - auto. Qed. Hypothesis wt_prog: wt_program p. @@ -757,11 +940,11 @@ Proof. (* Mgetstack *) assert (WTF: wt_function f) by (inv WTS; auto). - exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. + exploit frame_match_get_slot; eauto. eapply get_slot_extends; eauto. + intros [v' [A B]]. + exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split. constructor; auto. - eapply frame_match_get_slot; eauto. - eapply get_slot_extends; eauto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. eapply regset_lessdef_set; eauto. (* Msetstack *) assert (WTF: wt_function f) by (inv WTS; auto). @@ -769,41 +952,51 @@ Proof. inv WTS. generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI. inv WTI. apply WTRS. - exploit frame_match_set_slot; eauto. + exploit frame_match_set_slot. eauto. eauto. eapply set_slot_extends; eauto. + auto. apply RLD. auto. intros [ms' [STORE [FM' EXT']]]. - exists (State ts fb (Vptr sp0 base) c rs ms'); split. + exists (State ts fb (Vptr sp0 base) c trs ms'); split. apply exec_Msetstack; auto. econstructor; eauto. eapply match_stacks_store_slot; eauto. (* Mgetparam *) assert (WTF: wt_function f) by (inv WTS; auto). - exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. + exploit match_stacks_get_parent; eauto. intros [v' [A B]]. + exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split. eapply exec_Mgetparam; eauto. eapply frame_match_load_link; eauto. - eapply match_stacks_get_parent; eauto. - econstructor; eauto with coqlib. + eapply match_stacks_parent_sp_pointer; eauto. + econstructor; eauto with coqlib. apply regset_lessdef_set; eauto. (* Mop *) - exists (State ts fb (Vptr sp0 base) c (rs#res <- v) ms); split. + exploit eval_operation_lessdef. 2: eauto. + eapply regset_lessdef_list; eauto. + intros [v' [A B]]. + exists (State ts fb (Vptr sp0 base) c (trs#res <- v') ms); split. apply exec_Mop; auto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. apply regset_lessdef_set; eauto. (* Mload *) - exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. + exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto. + intros [a' [A B]]. + exploit Mem.loadv_extends. eauto. eauto. eexact B. + intros [v' [C D]]. + exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split. eapply exec_Mload; eauto. - destruct a; simpl in H0; try discriminate. - simpl. eapply Mem.load_extends; eauto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. apply regset_lessdef_set; eauto. (* Mstore *) - destruct a; simpl in H0; try discriminate. - exploit Mem.store_within_extends; eauto. intros [ms' [STORE MEXT']]. - exists (State ts fb (Vptr sp0 base) c rs ms'); split. + exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto. + intros [a' [A B]]. + exploit Mem.storev_extends. eauto. eauto. eexact B. apply RLD. + intros [ms' [C D]]. + exists (State ts fb (Vptr sp0 base) c trs ms'); split. eapply exec_Mstore; eauto. + destruct a; simpl in H0; try congruence. inv B. simpl in C. econstructor; eauto with coqlib. - eapply match_stacks_store; eauto. + eapply match_stacks_store. eauto. eexact H0. eexact C. eapply frame_match_store; eauto. (* Mcall *) @@ -814,7 +1007,7 @@ Proof. inv WTS. eapply is_tail_cons_left; eauto. destruct H0 as [ra' RETADDR]. econstructor; split. - eapply exec_Mcall; eauto. + eapply exec_Mcall; eauto. eapply regset_lessdef_find_function_ptr; eauto. econstructor; eauto. econstructor; eauto. inv WTS; auto. exact I. @@ -822,12 +1015,13 @@ Proof. assert (WTF: wt_function f) by (inv WTS; auto). exploit find_function_find_function_ptr; eauto. intros [fb' [FIND' FINDFUNCT]]. + exploit frame_match_delete; eauto. intros [ms' [A B]]. econstructor; split. eapply exec_Mtailcall; eauto. - eapply frame_match_load_link; eauto. - eapply frame_match_load_retaddr; eauto. - econstructor; eauto. eapply match_stacks_free; auto. - apply free_extends; auto. + eapply regset_lessdef_find_function_ptr; eauto. + eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto. + eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto. + econstructor; eauto. eapply match_stacks_free; eauto. (* Mgoto *) econstructor; split. @@ -837,49 +1031,50 @@ Proof. (* Mcond *) econstructor; split. eapply exec_Mcond_true; eauto. + eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto. econstructor; eauto. econstructor; split. eapply exec_Mcond_false; eauto. + eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto. econstructor; eauto. (* Mjumptable *) econstructor; split. - eapply exec_Mjumptable; eauto. + eapply exec_Mjumptable; eauto. + generalize (RLD arg); intro LD. rewrite H in LD. inv LD. auto. econstructor; eauto. (* Mreturn *) assert (WTF: wt_function f) by (inv WTS; auto). + exploit frame_match_delete; eauto. intros [ms' [A B]]. econstructor; split. eapply exec_Mreturn; eauto. - eapply frame_match_load_link; eauto. - eapply frame_match_load_retaddr; eauto. + eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto. + eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto. econstructor; eauto. eapply match_stacks_free; eauto. - apply free_extends; auto. (* internal function *) assert (WTF: wt_function f). inv WTS. inv H5. auto. - caseEq (alloc ms (- f.(fn_framesize)) f.(fn_stacksize)). - intros ms' stk' ALLOC. - assert (Val.has_type (parent_sp ts) Tint). - inv STACKS; simpl; auto. - assert (Val.has_type (parent_ra ts) Tint). - inv STACKS; simpl; auto. - destruct (frame_match_function_entry _ WTF _ _ _ _ _ _ _ - MEXT H ALLOC H0 H1) - as [ms2 [ms3 [EQ [STORE1 [STORE2 [FM MEXT']]]]]]. - subst stk'. + exploit frame_match_function_entry. eauto. eauto. eauto. + instantiate (1 := ts). eapply match_stacks_parent_sp_pointer; eauto. + eapply match_stacks_parent_ra_pointer; eauto. + intros [ms1 [ms2 [ms3 [ALLOC [STORE1 [STORE2 [FM MEXT']]]]]]]. econstructor; split. eapply exec_function_internal; eauto. exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW]. econstructor; eauto. eapply match_stacks_store_slot with (ms := ms2); eauto. - eapply match_stacks_store_slot with (ms := ms'); eauto. + eapply match_stacks_store_slot with (ms := ms1); eauto. (* external function *) + exploit transl_extcall_arguments; eauto. intros [targs [A B]]. + exploit external_call_mem_extends; eauto. + intros [tres [ms' [C [D [E F]]]]]. econstructor; split. - eapply exec_function_external; eauto. - eapply transl_extcall_arguments; eauto. + eapply exec_function_external. eauto. eexact C. eexact A. reflexivity. econstructor; eauto. + eapply match_stacks_external_call; eauto. + apply regset_lessdef_set; auto. (* return *) inv STACKS. @@ -894,8 +1089,10 @@ Lemma equiv_initial_states: Proof. intros. inversion H. econstructor; split. - econstructor. eauto. - split. econstructor. constructor. apply Mem.extends_refl. auto. + econstructor. eauto. eauto. + split. econstructor. constructor. apply Mem.extends_refl. + unfold Regmap.init; red; intros. constructor. + auto. econstructor. simpl; intros; contradiction. eapply Genv.find_funct_ptr_prop; eauto. red; intros; exact I. @@ -906,7 +1103,9 @@ Lemma equiv_final_states: match_states st1 st2 /\ wt_state st1 -> Machabstr.final_state st1 r -> Machconcr.final_state st2 r. Proof. intros. inv H0. destruct H. inv H. inv STACKS. - constructor; auto. + constructor. + generalize (RLD (Conventions.loc_result (mksignature nil (Some Tint)))). + rewrite H1. intro LD. inv LD. auto. Qed. Theorem exec_program_equiv: |