diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 14:25:31 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 14:25:31 +0200 |
| commit | 7b0d7a74ccfaf5843c41e2844e02e94e9a76bfd8 (patch) | |
| tree | 3edc201591691eac531aa12a98a5aa08ecc0398b /backend/CSE3analysisproof.v | |
| parent | 67290187fff3f813412059c6bfed69015c95c890 (diff) | |
| download | compcert-kvx-7b0d7a74ccfaf5843c41e2844e02e94e9a76bfd8.tar.gz compcert-kvx-7b0d7a74ccfaf5843c41e2844e02e94e9a76bfd8.zip | |
CSE3 across calls
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 116353fa..c65a6d9e 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -917,6 +917,17 @@ Section SOUNDNESS. Hint Resolve kill_builtin_res_sound : cse3. + Lemma top_sound: + forall rs m, (sem_rel RELATION.top rs m). + Proof. + unfold RELATION.top, sem_rel. + intros. + rewrite PSet.gempty in H. + discriminate. + Qed. + + Hint Resolve top_sound : cse3. + Lemma external_call_sound: forall ge ef (rel : RELATION.t) (m m' : mem) (rs : regset) vargs t vres (REL : sem_rel rel rs m) @@ -926,11 +937,11 @@ Section SOUNDNESS. destruct ef; intros; simpl in *. all: eauto using kill_mem_sound. all: unfold builtin_or_external_sem in *. - 1, 2: destruct (Builtins.lookup_builtin_function name sg); - eauto using kill_mem_sound; - inv CALL; eauto using kill_mem_sound. - all: inv CALL. - all: eauto using kill_mem_sound. + 1, 2, 3, 5, 6: destruct (Compopts.optim_CSE3_across_calls tt). + all: eauto using kill_mem_sound, top_sound. + 1, 2, 3: destruct (Builtins.lookup_builtin_function name sg). + all: eauto using kill_mem_sound, top_sound. + all: inv CALL; eauto using kill_mem_sound. Qed. Hint Resolve external_call_sound : cse3. |