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, 7 insertions, 39 deletions

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 086f4654..e6426fb8 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -146,9 +146,7 @@ Definition var_names (vars: list(ident * type)) : list ident :=
 (** Functions can either be defined ([Internal]) or declared as
   external functions ([External]). *)
 
-Inductive fundef : Type :=
-  | Internal: function -> fundef
-  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+Definition fundef := Ctypes.fundef function.
 
 (** The type of a function definition. *)
 
@@ -163,45 +161,16 @@ Definition type_of_fundef (f: fundef) : type :=
 
 (** ** Programs *)
 
-(** A program is composed of:
+(** As defined in module [Ctypes], a program, or compilation unit, is
+  composed of:
 - a list of definitions of functions and global variables;
 - the names of functions and global variables that are public (not static);
 - the name of the function that acts as entry point ("main" function).
-- a list of definitions for structure and union names;
-- the corresponding composite environment;
-*)
-
-Record program : Type := {
-  prog_defs: list (ident * globdef fundef type);
-  prog_public: list ident;
-  prog_main: ident;
-  prog_types: list composite_definition;
-  prog_comp_env: composite_env;
-  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
-}.
+- a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
 
-Definition program_of_program (p: program) : AST.program fundef type :=
-  {| AST.prog_defs := p.(prog_defs);
-     AST.prog_public := p.(prog_public);
-     AST.prog_main := p.(prog_main) |}.
-
-Coercion program_of_program: program >-> AST.program.
-
-Program Definition make_program (types: list composite_definition)
-                                (defs: list (ident * globdef fundef type))
-                                (public: list ident)
-                                (main: ident): res program :=
-  match build_composite_env types with
-  | OK env =>
-      OK {| prog_defs := defs;
-            prog_public := public;
-            prog_main := main;
-            prog_types := types;
-            prog_comp_env := env;
-            prog_comp_env_eq := _ |}
-  | Error msg =>
-      Error msg
-  end.
+Definition program := Ctypes.program function.
 
 (** * Operational semantics *)
 
@@ -774,4 +743,3 @@ Proof.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
-