From fb44646eb7308c1dd6a44b85415528982083200b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 22 Jun 2016 16:39:53 +0200 Subject: Stricter control of permissions in memory injections and extensions As suggested by Lennart Beringer, this commits strengthens memory injections and extensions so as to guarantee that the permissions of existing memory locations are not increased by the injection/extension. The only increase of permissions permitted is empty locations in the source memory state of the injection/extension being mapped to nonempty locations. --- backend/Unusedglobproof.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'backend/Unusedglobproof.v') diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index bb40a2d3..44cf1e8a 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1178,6 +1178,17 @@ Proof. destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. split. omega. generalize (Int.unsigned_range_2 ofs). omega. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q2 in H0. destruct H0. subst. replace ofs with 0 by omega. + left; apply Mem.perm_cur; auto. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q2 in H0. destruct H0. subst. + left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + apply P1. omega. Qed. End INIT_MEM. -- cgit