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, 21 deletions

diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index fa99915d..e5b2ce3a 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -12,22 +12,10 @@
 
 (** Elimination of unneeded computations over RTL. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Memory.
-Require Import Registers.
-Require Import Op.
-Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
-Require Import ValueDomain.
-Require Import ValueAnalysis.
-Require Import NeedDomain.
-Require Import NeedOp.
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL.
+Require Import ValueDomain ValueAnalysis NeedDomain NeedOp.
 
 (** * Part 1: the static analysis *)
 
@@ -205,10 +193,8 @@ Definition transf_instr (approx: PMap.t VA.t) (an: PMap.t NA.t)
       instr
   end.
 
-Definition vanalyze := ValueAnalysis.analyze.
-
 Definition transf_function (rm: romem) (f: function) : res function :=
-  let approx := vanalyze rm f in
+  let approx := ValueAnalysis.analyze rm f in
   match analyze approx f with
   | Some an =>
       OK {| fn_sig := f.(fn_sig);
@@ -220,10 +206,9 @@ Definition transf_function (rm: romem) (f: function) : res function :=
       Error (msg "Neededness analysis failed")
   end.
 
-
 Definition transf_fundef (rm: romem) (fd: fundef) : res fundef :=
   AST.transf_partial_fundef (transf_function rm) fd.
 
 Definition transf_program (p: program) : res program :=
-  transform_partial_program (transf_fundef (romem_for_program p)) p.
+  transform_partial_program (transf_fundef (romem_for p)) p.