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.

2 files changed, 189 insertions, 34 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 4ec19fa9..fc4a59f6 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -643,6 +643,12 @@ Definition option_eq (A: Type) (eqA: forall (x y: A), {x=y} + {x<>y}):
 Proof. decide equality. Defined.
 Global Opaque option_eq.
 
+(** Lifting a relation to an option type. *)
+
+Inductive option_rel (A B: Type) (R: A -> B -> Prop) : option A -> option B -> Prop :=
+  | option_rel_none: option_rel R None None
+  | option_rel_some: forall x y, R x y -> option_rel R (Some x) (Some y).
+
 (** Mapping a function over an option type. *)
 
 Definition option_map (A B: Type) (f: A -> B) (x: option A) : option B :=
@@ -1184,6 +1190,24 @@ Proof.
   induction 1; simpl; congruence.
 Qed.
 
+Lemma list_forall2_in_left:
+  forall x1 l1 l2,
+  list_forall2 l1 l2 -> In x1 l1 -> exists x2, In x2 l2 /\ P x1 x2.
+Proof.
+  induction 1; simpl; intros. contradiction. destruct H1.
+  subst; exists b1; auto.
+  exploit IHlist_forall2; eauto. intros (x2 & U & V); exists x2; auto.
+Qed.
+  
+Lemma list_forall2_in_right:
+  forall x2 l1 l2,
+  list_forall2 l1 l2 -> In x2 l2 -> exists x1, In x1 l1 /\ P x1 x2.
+Proof.
+  induction 1; simpl; intros. contradiction. destruct H1.
+  subst; exists a1; auto.
+  exploit IHlist_forall2; eauto. intros (x1 & U & V); exists x1; auto.
+Qed.
+  
 End FORALL2.
 
 Lemma list_forall2_imply:
@@ -1376,3 +1400,35 @@ Qed.
 
 End LEX_ORDER.
 
+(** * Nonempty lists *)
+
+Inductive nlist (A: Type) : Type :=
+  | nbase: A -> nlist A
+  | ncons: A -> nlist A -> nlist A.
+
+Definition nfirst {A: Type} (l: nlist A) :=
+  match l with nbase a => a | ncons a l' => a end.
+
+Fixpoint nlast {A: Type} (l: nlist A) :=
+  match l with nbase a => a | ncons a l' => nlast l' end.
+
+Fixpoint nIn {A: Type} (x: A) (l: nlist A) : Prop :=
+  match l with
+  | nbase a => a = x
+  | ncons a l => a = x \/ nIn x l
+  end.
+
+Inductive nlist_forall2 {A B: Type} (R: A -> B -> Prop) : nlist A -> nlist B -> Prop :=
+  | nbase_forall2: forall a b, R a b -> nlist_forall2 R (nbase a) (nbase b)
+  | ncons_forall2: forall a l b m, R a b -> nlist_forall2 R l m -> nlist_forall2 R (ncons a l) (ncons b m).
+
+Lemma nlist_forall2_imply:
+  forall (A B: Type) (P1: A -> B -> Prop) (l1: nlist A) (l2: nlist B),
+  nlist_forall2 P1 l1 l2 ->
+  forall (P2: A -> B -> Prop),
+  (forall v1 v2, nIn v1 l1 -> nIn v2 l2 -> P1 v1 v2 -> P2 v1 v2) ->
+  nlist_forall2 P2 l1 l2.
+Proof.
+  induction 1; simpl; intros; constructor; auto.
+Qed.
+
diff --git a/lib/Maps.v b/lib/Maps.v
index 39fec9fd..b7825331 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -789,46 +789,42 @@ Module PTree <: TREE.
     intros. apply (H (xO i0)).
   Qed.
 
-  Theorem elements_canonical_order:
+  Theorem elements_canonical_order':
     forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
-    (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
-    (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
+    (forall i, option_rel R (get i m) (get i n)) ->
     list_forall2
       (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
       (elements m) (elements n).
   Proof.
-    intros until R.
-    assert (forall m n j,
+    intros until n. unfold elements. generalize 1%positive. revert m n.
+    induction m; intros.
+  - simpl. rewrite xelements_empty. constructor.
+    intros. specialize (H i). rewrite gempty in H. inv H; auto.
+  - destruct n as [ | n1 o' n2 ].
+  + rewrite (xelements_empty (Node m1 o m2)). simpl; constructor.
+    intros. specialize (H i). rewrite gempty in H. inv H; auto.
+  + rewrite ! xelements_node. repeat apply list_forall2_app.
+    apply IHm1. intros. apply (H (xO i)).
+    generalize (H xH); simpl; intros OR; inv OR.
+    constructor.
+    constructor. auto. constructor.
+    apply IHm2. intros. apply (H (xI i)).
+  Qed.
+
+  Theorem elements_canonical_order:
+    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
     (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
     (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
     list_forall2
       (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
-      (xelements m j nil) (xelements n j nil)).
-  {
-    induction m; intros.
-  - rewrite xelements_leaf. rewrite xelements_empty. constructor.
-    intros. destruct (get i n) eqn:E; auto. exploit H0; eauto.
-    intros [x [P Q]]. rewrite gleaf in P; congruence.
-  - destruct n as [ | n1 o' n2 ].
-    + rewrite xelements_leaf, xelements_empty. constructor.
-      intros. destruct (get i (Node m1 o m2)) eqn:E; auto. exploit H; eauto.
-      intros [x [P Q]]. rewrite gleaf in P; congruence.
-    + rewrite ! xelements_node. apply list_forall2_app.
-      apply IHm1.
-      intros. apply (H (xO i) x); auto.
-      intros. apply (H0 (xO i) y); auto.
-      apply list_forall2_app.
-      destruct o, o'.
-      destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P.
-      constructor. auto. constructor.
-      destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P.
-      destruct (H0 xH b) as [x [P Q]]. auto. simpl in P. inv P.
-      constructor.
-      apply IHm2.
-      intros. apply (H (xI i) x); auto.
-      intros. apply (H0 (xI i) y); auto.
-    }
-    intros. apply H with (j := xH); auto.
+      (elements m) (elements n).
+  Proof.
+    intros. apply elements_canonical_order'. 
+    intros. destruct (get i m) as [x|] eqn:GM. 
+    exploit H; eauto. intros (y & P & Q). rewrite P; constructor; auto.
+    destruct (get i n) as [y|] eqn:GN.
+    exploit H0; eauto. intros (x & P & Q). congruence.
+    constructor.
   Qed.
 
   Theorem elements_extensional:
@@ -837,9 +833,8 @@ Module PTree <: TREE.
     elements m = elements n.
   Proof.
     intros.
-    exploit (elements_canonical_order (fun (x y: A) => x = y) m n).
-    intros. rewrite H in H0. exists x; auto.
-    intros. rewrite <- H in H0. exists y; auto.
+    exploit (@elements_canonical_order' _ _ (fun (x y: A) => x = y) m n).
+    intros. rewrite H. destruct (get i n); constructor; auto.
     induction 1. auto. destruct a1 as [a2 a3]; destruct b1 as [b2 b3]; simpl in *.
     destruct H0. congruence.
   Qed.
@@ -1542,6 +1537,110 @@ Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
 
 End EXTENSIONAL_EQUALITY.
 
+(** Creating a tree from a list of (key, value) pairs. *)
+
+Section OF_LIST.
+
+Variable A: Type.
+
+Let f := fun (m: T.t A) (k_v: T.elt * A) => T.set (fst k_v) (snd k_v) m.
+
+Definition of_list (l: list (T.elt * A)) : T.t A :=
+  List.fold_left f l (T.empty _).
+
+Lemma in_of_list:
+  forall l k v, T.get k (of_list l) = Some v -> In (k, v) l.
+Proof.
+  assert (REC: forall k v l m,
+           T.get k (fold_left f l m) = Some v -> In (k, v) l \/ T.get k m = Some v).
+  { induction l as [ | [k1 v1] l]; simpl; intros.
+  - tauto.
+  - apply IHl in H. unfold f in H. simpl in H. rewrite T.gsspec in H.
+    destruct H; auto. 
+    destruct (T.elt_eq k k1). inv H. auto. auto. 
+  }
+  intros. apply REC in H. rewrite T.gempty in H. intuition congruence.
+Qed.
+
+Lemma of_list_dom:
+  forall l k, In k (map fst l) -> exists v, T.get k (of_list l) = Some v.
+Proof.
+  assert (REC: forall k l m,
+            In k (map fst l) \/ (exists v, T.get k m = Some v) ->
+            exists v, T.get k (fold_left f l m) = Some v).
+  { induction l as [ | [k1 v1] l]; simpl; intros.
+  - tauto.
+  - apply IHl. unfold f; rewrite T.gsspec. simpl. destruct (T.elt_eq k k1). 
+    right; econstructor; eauto.
+    intuition congruence.
+  }
+  intros. apply REC. auto.
+Qed.
+
+Remark of_list_unchanged:
+  forall k l m, ~In k (map fst l) -> T.get k (List.fold_left f l m) = T.get k m.
+Proof.
+  induction l as [ | [k1 v1] l]; simpl; intros.
+- auto.
+- rewrite IHl by tauto. unfold f; apply T.gso; intuition auto.
+Qed.
+
+Lemma of_list_unique:
+  forall k v l1 l2,
+  ~In k (map fst l2) -> T.get k (of_list (l1 ++ (k, v) :: l2)) = Some v.
+Proof.
+  intros. unfold of_list. rewrite fold_left_app. simpl. 
+  rewrite of_list_unchanged by auto. unfold f; apply T.gss.
+Qed.
+
+Lemma of_list_norepet:
+  forall l k v, list_norepet (map fst l) -> In (k, v) l -> T.get k (of_list l) = Some v.
+Proof.
+  assert (REC: forall k v l m,
+            list_norepet (map fst l) ->
+            In (k, v) l ->
+            T.get k (fold_left f l m) = Some v).
+  { induction l as [ | [k1 v1] l]; simpl; intros.
+    contradiction.
+    inv H. destruct H0.
+    inv H. rewrite of_list_unchanged by auto. apply T.gss. 
+    apply IHl; auto. 
+  }
+  intros; apply REC; auto.
+Qed.
+
+Lemma of_list_elements:
+  forall m k, T.get k (of_list (T.elements m)) = T.get k m.
+Proof.
+  intros. destruct (T.get k m) as [v|] eqn:M.
+- apply of_list_norepet. apply T.elements_keys_norepet. apply T.elements_correct; auto.
+- destruct (T.get k (of_list (T.elements m))) as [v|] eqn:M'; auto.
+  apply in_of_list in M'. apply T.elements_complete in M'. congruence.
+Qed.
+
+End OF_LIST.
+
+Lemma of_list_related:
+  forall (A B: Type) (R: A -> B -> Prop) k l1 l2,
+  list_forall2 (fun ka kb => fst ka = fst kb /\ R (snd ka) (snd kb)) l1 l2 ->
+  option_rel R (T.get k (of_list l1)) (T.get k (of_list l2)).
+Proof.
+  intros until k. unfold of_list.
+  set (R' := fun ka kb => fst ka = fst kb /\ R (snd ka) (snd kb)).
+  set (fa := fun (m : T.t A) (k_v : T.elt * A) => T.set (fst k_v) (snd k_v) m).
+  set (fb := fun (m : T.t B) (k_v : T.elt * B) => T.set (fst k_v) (snd k_v) m).
+  assert (REC: forall l1 l2, list_forall2 R' l1 l2 ->
+               forall m1 m2, option_rel R (T.get k m1) (T.get k m2) ->
+               option_rel R (T.get k (fold_left fa l1 m1)) (T.get k (fold_left fb l2 m2))).
+  { induction 1; intros; simpl.
+  - auto.
+  - apply IHlist_forall2. unfold fa, fb. rewrite ! T.gsspec.
+    destruct H as [E F]. rewrite E. destruct (T.elt_eq k (fst b1)).
+    constructor; auto.
+    auto. }
+  intros. apply REC; auto. rewrite ! T.gempty. constructor.
+Qed.
+
 End Tree_Properties.
 
 Module PTree_Properties := Tree_Properties(PTree).