diff options
Diffstat (limited to 'cfrontend/SimplLocalsproof.v')
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 60 |
1 files changed, 38 insertions, 22 deletions
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 988988a1..e4b759c4 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -391,7 +391,7 @@ Lemma match_envs_assign_lifted: e!id = Some(b, ty) -> val_casted v ty -> Val.inject f v tv -> - assign_loc ge ty m b Ptrofs.zero v m' -> + assign_loc ge ty m b Ptrofs.zero Full v m' -> VSet.mem id cenv = true -> match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi. Proof. @@ -1004,13 +1004,13 @@ Proof. Qed. Lemma assign_loc_inject: - forall f ty m loc ofs v m' tm loc' ofs' v', - assign_loc ge ty m loc ofs v m' -> + forall f ty m loc ofs bf v m' tm loc' ofs' v', + assign_loc ge ty m loc ofs bf v m' -> Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> Val.inject f v v' -> Mem.inject f m tm -> exists tm', - assign_loc tge ty tm loc' ofs' v' tm' + assign_loc tge ty tm loc' ofs' bf v' tm' /\ Mem.inject f m' tm' /\ (forall b chunk v, f b = None -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v). @@ -1078,15 +1078,25 @@ Proof. split. auto. intros. rewrite <- H0. eapply Mem.load_storebytes_other; eauto. left. congruence. +- (* bitfield *) + inv H3. + exploit Mem.loadv_inject; eauto. intros (vc' & LD' & INJ). inv INJ. + exploit Mem.storev_mapped_inject; eauto. intros [tm' [A B]]. + inv H1. + exists tm'; split. eapply assign_loc_bitfield; eauto. econstructor; eauto. + split. auto. + intros. rewrite <- H3. eapply Mem.load_store_other; eauto. + left. inv H0. congruence. Qed. Lemma assign_loc_nextblock: - forall ge ty m b ofs v m', - assign_loc ge ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m. + forall ge ty m b ofs bf v m', + assign_loc ge ty m b ofs bf v m' -> Mem.nextblock m' = Mem.nextblock m. Proof. induction 1. simpl in H0. eapply Mem.nextblock_store; eauto. eapply Mem.nextblock_storebytes; eauto. + inv H. eapply Mem.nextblock_store; eauto. Qed. Theorem store_params_correct: @@ -1168,7 +1178,7 @@ Local Opaque Conventions1.parameter_needs_normalization. reflexivity. reflexivity. eexact U. traceEq. - rewrite (assign_loc_nextblock _ _ _ _ _ _ _ A) in Z. auto. + rewrite (assign_loc_nextblock _ _ _ _ _ _ _ _ A) in Z. auto. Qed. Lemma bind_parameters_nextblock: @@ -1400,19 +1410,22 @@ Proof. Qed. Lemma deref_loc_inject: - forall ty loc ofs v loc' ofs', - deref_loc ty m loc ofs v -> + forall ty loc ofs bf v loc' ofs', + deref_loc ty m loc ofs bf v -> Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> - exists tv, deref_loc ty tm loc' ofs' tv /\ Val.inject f v tv. + exists tv, deref_loc ty tm loc' ofs' bf tv /\ Val.inject f v tv. Proof. intros. inv H. - (* by value *) +- (* by value *) exploit Mem.loadv_inject; eauto. intros [tv [A B]]. exists tv; split; auto. eapply deref_loc_value; eauto. - (* by reference *) +- (* by reference *) exists (Vptr loc' ofs'); split; auto. eapply deref_loc_reference; eauto. - (* by copy *) +- (* by copy *) exists (Vptr loc' ofs'); split; auto. eapply deref_loc_copy; eauto. +- (* bitfield *) + inv H1. exploit Mem.loadv_inject; eauto. intros [tc [A B]]. inv B. + econstructor; split. eapply deref_loc_bitfield. econstructor; eauto. constructor. Qed. Lemma eval_simpl_expr: @@ -1422,11 +1435,11 @@ Lemma eval_simpl_expr: exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ Val.inject f v tv with eval_simpl_lvalue: - forall a b ofs, - eval_lvalue ge e le m a b ofs -> + forall a b ofs bf, + eval_lvalue ge e le m a b ofs bf -> compat_cenv (addr_taken_expr a) cenv -> match a with Evar id ty => VSet.mem id cenv = false | _ => True end -> - exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ Val.inject f (Vptr b ofs) (Vptr b' ofs'). + exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' bf /\ Val.inject f (Vptr b ofs) (Vptr b' ofs'). Proof. destruct 1; simpl; intros. @@ -1472,7 +1485,7 @@ Proof. subst a. simpl. rewrite OPT. exploit me_vars; eauto. instantiate (1 := id). intros MV. inv H; inv MV; try congruence. - rewrite ENV in H6; inv H6. + rewrite ENV in H7; inv H7. inv H0; try congruence. assert (chunk0 = chunk). simpl in H. congruence. subst chunk0. assert (v0 = v). unfold Mem.loadv in H2. rewrite Ptrofs.unsigned_zero in H2. congruence. subst v0. @@ -1516,7 +1529,8 @@ Proof. exploit eval_simpl_expr; eauto. intros [tv [A B]]. inversion B. subst. econstructor; econstructor; split. - eapply eval_Efield_union; eauto. rewrite typeof_simpl_expr; eauto. auto. + eapply eval_Efield_union; eauto. rewrite typeof_simpl_expr; eauto. + econstructor; eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. Qed. Lemma eval_simpl_exprlist: @@ -1607,18 +1621,20 @@ Qed. (** Invariance by assignment to location "above" *) Lemma match_cont_assign_loc: - forall f cenv k tk m bound tbound ty loc ofs v m', + forall f cenv k tk m bound tbound ty loc ofs bf v m', match_cont f cenv k tk m bound tbound -> - assign_loc ge ty m loc ofs v m' -> + assign_loc ge ty m loc ofs bf v m' -> Ple bound loc -> match_cont f cenv k tk m' bound tbound. Proof. intros. eapply match_cont_invariant; eauto. intros. rewrite <- H4. inv H0. - (* scalar *) +- (* scalar *) simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; extlia. - (* block copy *) +- (* block copy *) eapply Mem.load_storebytes_other; eauto. left. unfold block; extlia. +- (* bitfield *) + inv H5. eapply Mem.load_store_other; eauto. left. unfold block; extlia. Qed. (** Invariance by external calls *) |