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 /cfrontend/Cexec.v | |
| parent | 1396a4051caef0957ede026f3b8fab5a9b10b6bc (diff) | |
| parent | 478ae4c3aeb1a31b0eec9ab7eb8fe20ec2671614 (diff) | |
| download | compcert-kvx-1fdca8371317e656cb08eaec3adb4596d6447e9b.tar.gz compcert-kvx-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 'cfrontend/Cexec.v')
| -rw-r--r-- | cfrontend/Cexec.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 00d77b00..bf88e033 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -536,6 +536,7 @@ Definition do_external (ef: external_function): match ef with | EF_external name sg => do_external_function name sg ge | EF_builtin name sg => do_external_function name sg ge + | EF_runtime name sg => do_external_function name sg ge | EF_vload chunk => do_ef_volatile_load chunk | EF_vstore chunk => do_ef_volatile_store chunk | EF_malloc => do_ef_malloc @@ -558,6 +559,8 @@ Proof with try congruence. eapply do_external_function_sound; eauto. (* EF_builtin *) eapply do_external_function_sound; eauto. +(* EF_runtime *) + eapply do_external_function_sound; eauto. (* EF_vload *) unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... mydestr. destruct p as [[w'' t''] v]; mydestr. @@ -604,6 +607,8 @@ Proof. eapply do_external_function_complete; eauto. (* EF_builtin *) eapply do_external_function_complete; eauto. +(* EF_runtime *) + eapply do_external_function_complete; eauto. (* EF_vload *) inv H; unfold do_ef_volatile_load. exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. |