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, 6 insertions, 41 deletions

diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index b94465a1..453a4c9a 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -12,18 +12,9 @@
 
 (** Relational specification of expression simplification. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Memory.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Clight.
-Require Import SimplExpr.
+Require Import Coqlib Maps Errors Integers Floats.
+Require Import AST Linking Memory.
+Require Import Ctypes Cop Csyntax Clight SimplExpr.
 
 Section SPEC.
 
@@ -1077,8 +1068,7 @@ Opaque transl_expression transl_expr_stmt.
   monadInv TR; constructor; eauto.
 Qed.
 
-(** Relational presentation for the transformation of functions, fundefs, and va
-riables. *)
+(** Relational presentation for the transformation of functions, fundefs, and variables. *)
 
 Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
   | tr_function_intro: forall f tf,
@@ -1092,9 +1082,9 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
 Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
   | tr_internal: forall f tf,
       tr_function f tf ->
-      tr_fundef (Csyntax.Internal f) (Clight.Internal tf)
+      tr_fundef (Internal f) (Internal tf)
   | tr_external: forall ef targs tres cconv,
-      tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv).
+      tr_fundef (External ef targs tres cconv) (External ef targs tres cconv).
 
 Lemma transl_function_spec:
   forall f tf,
@@ -1117,30 +1107,5 @@ Proof.
 + constructor.
 Qed.
 
-Lemma transl_globdefs_spec:
-  forall l l',
-  transf_globdefs transl_fundef (fun v : type => OK v) l = OK l' ->
-  list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'.
-Proof.
-  induction l; simpl; intros.
-- inv H. constructor.
-- destruct a as [id gd]. destruct gd.
-  + destruct (transl_fundef f) as [tf | ?] eqn:E1; Errors.monadInv H.
-    constructor; eauto. constructor. eapply transl_fundef_spec; eauto.
-  + Errors.monadInv H. 
-    constructor; eauto. destruct v; constructor; auto.
-Qed.
-
-Theorem transl_program_spec:
-  forall p tp,
-  transl_program p = OK tp ->
-  match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp.
-Proof.
-  unfold transl_program, transform_partial_program; intros. Errors.monadInv H. Errors.monadInv EQ; simpl.
-  split; auto. exists x0; split.
-  eapply transl_globdefs_spec; eauto.
-  rewrite <- app_nil_end; auto.
-Qed.
-
 End SPEC.