diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-20 18:00:43 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-20 18:00:43 +0100 |
| commit | 1fdca8371317e656cb08eaec3adb4596d6447e9b (patch) | |
| tree | 8a5d390a4d38f4d840f516fb917eb824311a93a0 /driver/Complements.v | |
| parent | 1396a4051caef0957ede026f3b8fab5a9b10b6bc (diff) | |
| parent | 478ae4c3aeb1a31b0eec9ab7eb8fe20ec2671614 (diff) | |
| download | compcert-1fdca8371317e656cb08eaec3adb4596d6447e9b.tar.gz compcert-1fdca8371317e656cb08eaec3adb4596d6447e9b.zip | |
Merge pull request #93 from AbsInt/separate-compilation
This pull request implements "approach A" to separate compilation in CompCert from the paper
Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190
In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.
This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
Diffstat (limited to 'driver/Complements.v')
| -rw-r--r-- | driver/Complements.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/driver/Complements.v b/driver/Complements.v index 8651f2ff..f7598758 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -80,17 +80,19 @@ Theorem transf_cstrategy_program_preservation: Proof. assert (WBT: forall p, well_behaved_traces (Cstrategy.semantics p)). intros. eapply ssr_well_behaved. apply Cstrategy.semantics_strongly_receptive. - intros. intuition. + intros. + assert (MATCH: match_prog p tp) by (apply transf_c_program_match; auto). + intuition auto. eapply forward_simulation_behavior_improves; eauto. - apply (fst (transf_cstrategy_program_correct _ _ H)). + apply (proj1 (cstrategy_semantic_preservation _ _ MATCH)). exploit backward_simulation_behavior_improves. - apply (snd (transf_cstrategy_program_correct _ _ H)). + apply (proj2 (cstrategy_semantic_preservation _ _ MATCH)). eauto. intros [beh1 [A B]]. exists beh1; split; auto. rewrite atomic_behaviors; auto. eapply forward_simulation_same_safe_behavior; eauto. - apply (fst (transf_cstrategy_program_correct _ _ H)). + apply (proj1 (cstrategy_semantic_preservation _ _ MATCH)). exploit backward_simulation_same_safe_behavior. - apply (snd (transf_cstrategy_program_correct _ _ H)). + apply (proj2 (cstrategy_semantic_preservation _ _ MATCH)). intros. rewrite <- atomic_behaviors in H2; eauto. eauto. intros. rewrite atomic_behaviors; auto. Qed. |