From 8587b8310a91702e2635a689e1622a87b7bf8985 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 2 Mar 2020 10:32:07 +0100 Subject: Weaker ec_readonly condition over external calls (#225) Currently we require the memory to be unchanged on readonly locations. This is too strong. For example, current permissions could decrease from readonly to none. This commit weakens the ec_readonly condition to the strict minimum needed to show the correctness of value analysis for const globals. --- backend/ValueAnalysis.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'backend/ValueAnalysis.v') diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 2b233900..b0ce019c 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1039,9 +1039,8 @@ Proof. red; simpl; intros. destruct (plt b (Mem.nextblock m)). exploit RO; eauto. intros (R & P & Q). split; auto. - split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto. - intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto. - auto. intros; red. apply Q. + split. apply bmatch_incr with bc; auto. apply bmatch_ext with m; auto. + intros. eapply external_call_readonly with (m2 := m'); eauto. intros; red; intros; elim (Q ofs). eapply external_call_max_perm with (m2 := m'); eauto. destruct (j' b); congruence. -- cgit