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, 68 insertions, 73 deletions

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 07c7008d..2c144249 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -12,28 +12,21 @@
 
 (** Correctness proof for common subexpression elimination. *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import Kildall.
-Require Import ValueDomain.
-Require Import ValueAOp.
-Require Import ValueAnalysis.
-Require Import CSEdomain.
-Require Import CombineOp.
-Require Import CombineOpproof.
-Require Import CSE.
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Registers RTL.
+Require Import ValueDomain ValueAOp ValueAnalysis.
+Require Import CSEdomain CombineOp CombineOpproof CSE.
+
+Definition match_prog (prog tprog: RTL.program) :=
+  match_program (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog tprog.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. eapply match_transform_partial_program_contextual; eauto.
+Qed.
 
 (** * Soundness of operations over value numberings *)
 
@@ -809,37 +802,32 @@ Section PRESERVATION.
 
 Variable prog: program.
 Variable tprog : program.
-Hypothesis TRANSF: transf_program prog = OK tprog.
+Hypothesis TRANSF: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
-Let rm := romem_for_program prog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_transf_partial (transf_fundef rm) prog TRANSF).
+Proof (Genv.find_symbol_match TRANSF).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof (Genv.public_symbol_transf_partial (transf_fundef rm) prog TRANSF).
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof (Genv.find_var_info_transf_partial (transf_fundef rm) prog TRANSF).
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
 
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
-  exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef rm f = OK tf.
-Proof (Genv.find_funct_transf_partial (transf_fundef rm) prog TRANSF).
+  exists cu tf, Genv.find_funct tge v = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
+Proof (Genv.find_funct_match TRANSF).
 
 Lemma funct_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef rm f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial (transf_fundef rm) prog TRANSF).
+  exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
+Proof (Genv.find_funct_ptr_match TRANSF).
 
 Lemma sig_preserved:
-  forall f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f.
+  forall rm f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f.
 Proof.
   unfold transf_fundef; intros. destruct f; monadInv H; auto.
   unfold transf_function in EQ.
@@ -887,7 +875,9 @@ Lemma find_function_translated:
   forall ros rs fd rs',
   find_function ge ros rs = Some fd ->
   regs_lessdef rs rs' ->
-  exists tfd, find_function tge ros rs' = Some tfd /\ transf_fundef rm fd = OK tfd.
+  exists cu tfd, find_function tge ros rs' = Some tfd
+              /\ transf_fundef (romem_for cu) fd = OK tfd
+              /\ linkorder cu prog.
 Proof.
   unfold find_function; intros; destruct ros.
 - specialize (H0 r). inv H0.
@@ -914,12 +904,16 @@ Qed.
   the numbering at [pc] (returned by the static analysis) is satisfiable.
 *)
 
+Definition analyze (cu: program) (f: function) :=
+  CSE.analyze f (vanalyze (romem_for cu) f).
+
 Inductive match_stackframes: list stackframe -> list stackframe -> Prop :=
   | match_stackframes_nil:
       match_stackframes nil nil
   | match_stackframes_cons:
-      forall res sp pc rs f approx s rs' s'
-           (ANALYZE: analyze f (vanalyze rm f) = Some approx)
+      forall res sp pc rs f s rs' s' cu approx
+           (LINK: linkorder cu prog)
+           (ANALYZE: analyze cu f = Some approx)
            (SAT: forall v m, exists valu, numbering_holds valu ge sp (rs#res <- v) m approx!!pc)
            (RLD: regs_lessdef rs rs')
            (STACKS: match_stackframes s s'),
@@ -929,8 +923,9 @@ Inductive match_stackframes: list stackframe -> list stackframe -> Prop :=
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
-      forall s sp pc rs m s' rs' m' f approx
-             (ANALYZE: analyze f (vanalyze rm f) = Some approx)
+      forall s sp pc rs m s' rs' m' f cu approx
+             (LINK: linkorder cu prog)
+             (ANALYZE: analyze cu f = Some approx)
              (SAT: exists valu, numbering_holds valu ge sp rs m approx!!pc)
              (RLD: regs_lessdef rs rs')
              (MEXT: Mem.extends m m')
@@ -938,18 +933,19 @@ Inductive match_states: state -> state -> Prop :=
       match_states (State s f sp pc rs m)
                    (State s' (transf_function' f approx) sp pc rs' m')
   | match_states_call:
-      forall s f tf args m s' args' m',
-      match_stackframes s s' ->
-      transf_fundef rm f = OK tf ->
-      Val.lessdef_list args args' ->
-      Mem.extends m m' ->
+      forall s f tf args m s' args' m' cu
+             (LINK: linkorder cu prog)
+             (STACKS: match_stackframes s s')
+             (TFD: transf_fundef (romem_for cu) f = OK tf)
+             (ARGS: Val.lessdef_list args args')
+             (MEXT: Mem.extends m m'),
       match_states (Callstate s f args m)
                    (Callstate s' tf args' m')
   | match_states_return:
-      forall s s' v v' m m',
-      match_stackframes s s' ->
-      Val.lessdef v v' ->
-      Mem.extends m m' ->
+      forall s s' v v' m m'
+             (STACK: match_stackframes s s')
+             (RES: Val.lessdef v v')
+             (MEXT: Mem.extends m m'),
       match_states (Returnstate s v m)
                    (Returnstate s' v' m').
 
@@ -1076,28 +1072,28 @@ Proof.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
-  inv SOUND.
+  InvSoundState.
   eapply add_store_result_hold; eauto.
   eapply kill_loads_after_store_holds; eauto.
 
 - (* Icall *)
-  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']].
+  exploit find_function_translated; eauto. intros (cu' & tf & FIND' & TRANSF' & LINK').
   econstructor; split.
   eapply exec_Icall; eauto.
-  apply sig_preserved; auto.
-  econstructor; eauto.
+  eapply sig_preserved; eauto.
   econstructor; eauto.
+  eapply match_stackframes_cons with (cu := cu); eauto.
   intros. eapply analysis_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
   exists (fun _ => Vundef); apply empty_numbering_holds.
   apply regs_lessdef_regs; auto.
 
 - (* Itailcall *)
-  exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']].
+  exploit find_function_translated; eauto. intros (cu' & tf & FIND' & TRANSF' & LINK').
   exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]].
   econstructor; split.
   eapply exec_Itailcall; eauto.
-  apply sig_preserved; auto.
+  eapply sig_preserved; eauto.
   econstructor; eauto.
   apply regs_lessdef_regs; auto.
 
@@ -1109,8 +1105,7 @@ Proof.
   econstructor; split.
   eapply exec_Ibuiltin; eauto.
   eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
   eapply analysis_correct_1; eauto. simpl; auto.
 * unfold transfer; rewrite H.
@@ -1125,6 +1120,7 @@ Proof.
   destruct ef.
   + apply CASE1.
   + apply CASE3.
+  + apply CASE1.
   + apply CASE2; inv H1; auto.
   + apply CASE3.
   + apply CASE1.
@@ -1133,7 +1129,7 @@ Proof.
     simpl in H1. inv H1.
     exists valu.
     apply set_res_unknown_holds.
-    inv SOUND. unfold vanalyze, rm; rewrite AN.
+    InvSoundState. unfold vanalyze; rewrite AN.
     assert (pmatch bc bsrc osrc (aaddr_arg (VA.State ae am) a0))
     by (eapply aaddr_arg_sound_1; eauto).
     assert (pmatch bc bdst odst (aaddr_arg (VA.State ae am) a1))
@@ -1179,8 +1175,8 @@ Proof.
   destruct or; simpl; auto.
 
 - (* internal function *)
-  monadInv H6. unfold transf_function in EQ.
-  destruct (analyze f (vanalyze rm f)) as [approx|] eqn:?; inv EQ.
+  monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ.
+  destruct (analyze cu f) as [approx|] eqn:?; inv EQ.
   exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
   intros (m'' & A & B).
   econstructor; split.
@@ -1190,17 +1186,16 @@ Proof.
   apply init_regs_lessdef; auto.
 
 - (* external function *)
-  monadInv H6.
+  monadInv TFD.
   exploit external_call_mem_extends; eauto.
   intros (v' & m1' & P & Q & R & S).
   econstructor; split.
   eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 
 - (* return *)
-  inv H2.
+  inv STACK.
   econstructor; split.
   eapply exec_return; eauto.
   econstructor; eauto.
@@ -1212,22 +1207,22 @@ Lemma transf_initial_states:
   exists st2, initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H.
-  exploit funct_ptr_translated; eauto. intros [tf [A B]].
+  exploit funct_ptr_translated; eauto. intros (cu & tf & A & B & C).
   exists (Callstate nil tf nil m0); split.
   econstructor; eauto.
-  eapply Genv.init_mem_transf_partial; eauto.
+  eapply (Genv.init_mem_match TRANSF); eauto.
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
-  symmetry. eapply transform_partial_program_main; eauto.
-  rewrite <- H3. apply sig_preserved; auto.
-  constructor. constructor. auto. auto. apply Mem.extends_refl.
+  symmetry. eapply match_program_main; eauto.
+  rewrite <- H3. eapply sig_preserved; eauto.
+  econstructor. eauto. constructor. auto. auto. apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r,
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H5. inv H3. constructor.
+  intros. inv H0. inv H. inv RES. inv STACK. constructor.
 Qed.
 
 Theorem transf_program_correct:
@@ -1235,7 +1230,7 @@ Theorem transf_program_correct:
 Proof.
   eapply forward_simulation_step with
     (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2).
-- eexact public_preserved.
+- apply senv_preserved.
 - intros. exploit transf_initial_states; eauto. intros [s2 [A B]].
   exists s2. split. auto. split. apply sound_initial; auto. auto.
 - intros. destruct H. eapply transf_final_states; eauto.