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.

1 files changed, 58 insertions, 3 deletions

diff --git a/common/Memory.v b/common/Memory.v
index 93d0e432..0ea9e3b0 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -4143,6 +4143,8 @@ Section UNCHANGED_ON.
 Variable P: block -> Z -> Prop.
 
 Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
+  unchanged_on_nextblock:
+    Ple (nextblock m_before) (nextblock m_after);
   unchanged_on_perm:
     forall b ofs k p,
     P b ofs -> valid_block m_before b ->
@@ -4157,15 +4159,22 @@ Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
 Lemma unchanged_on_refl:
   forall m, unchanged_on m m.
 Proof.
-  intros; constructor; tauto.
+  intros; constructor. apply Ple_refl. tauto. tauto.
+Qed.
+
+Lemma valid_block_unchanged_on:
+  forall m m' b,
+  unchanged_on m m' -> valid_block m b -> valid_block m' b.
+Proof.
+  unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega.
 Qed.
 
 Lemma perm_unchanged_on:
   forall m m' b ofs k p,
-  unchanged_on m m' -> P b ofs -> valid_block m b ->
+  unchanged_on m m' -> P b ofs ->
   perm m b ofs k p -> perm m' b ofs k p.
 Proof.
-  intros. destruct H. apply unchanged_on_perm0; auto.
+  intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. 
 Qed.
 
 Lemma perm_unchanged_on_2:
@@ -4176,6 +4185,17 @@ Proof.
   intros. destruct H. apply unchanged_on_perm0; auto.
 Qed.
 
+Lemma unchanged_on_trans:
+  forall m1 m2 m3, unchanged_on m1 m2 -> unchanged_on m2 m3 -> unchanged_on m1 m3.
+Proof.
+  intros; constructor.
+- apply Ple_trans with (nextblock m2); apply unchanged_on_nextblock; auto.
+- intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto.
+  eapply valid_block_unchanged_on; eauto.
+- intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto.
+  eapply perm_unchanged_on; eauto. 
+Qed.
+
 Lemma loadbytes_unchanged_on_1:
   forall m m' b ofs n,
   unchanged_on m m' ->
@@ -4243,6 +4263,7 @@ Lemma store_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_store _ _ _ _ _ _ H). apply Ple_refl.
 - split; intros; eauto with mem.
 - erewrite store_mem_contents; eauto. rewrite PMap.gsspec.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
@@ -4259,6 +4280,7 @@ Lemma storebytes_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_storebytes _ _ _ _ _ H). apply Ple_refl.
 - split; intros. eapply perm_storebytes_1; eauto. eapply perm_storebytes_2; eauto.
 - erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
@@ -4273,6 +4295,7 @@ Lemma alloc_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_alloc _ _ _ _ _ H). apply Ple_succ.
 - split; intros.
   eapply perm_alloc_1; eauto.
   eapply perm_alloc_4; eauto.
@@ -4288,6 +4311,7 @@ Lemma free_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_free _ _ _ _ _ H). apply Ple_refl.
 - split; intros.
   eapply perm_free_1; eauto.
   destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto.
@@ -4297,8 +4321,39 @@ Proof.
   simpl. auto.
 Qed.
 
+Lemma drop_perm_unchanged_on:
+  forall m b lo hi p m',
+  drop_perm m b lo hi p = Some m' ->
+  (forall i, lo <= i < hi -> ~ P b i) ->
+  unchanged_on m m'.
+Proof.
+  intros; constructor; intros.
+- rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl.
+- split; intros. eapply perm_drop_3; eauto.
+  destruct (eq_block b0 b); auto.
+  subst b0. 
+  assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. }
+  right; omega.
+  eapply perm_drop_4; eauto. 
+- unfold drop_perm in H. 
+  destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto.
+Qed. 
+
 End UNCHANGED_ON.
 
+Lemma unchanged_on_implies:
+  forall (P Q: block -> Z -> Prop) m m',
+  unchanged_on P m m' ->
+  (forall b ofs, Q b ofs -> valid_block m b -> P b ofs) ->
+  unchanged_on Q m m'.
+Proof.
+  intros. destruct H. constructor; intros.
+- auto.
+- apply unchanged_on_perm0; auto. 
+- apply unchanged_on_contents0; auto. 
+  apply H0; auto. eapply perm_valid_block; eauto. 
+Qed.
+
 End Mem.
 
 Notation mem := Mem.mem.