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, 8 insertions, 16 deletions

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 048ab816..f9ccd5db 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -10,21 +10,12 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import Coqlib.
-Require Import Zwf.
-Require Import Maps.
-Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Lattice.
-Require Import Kildall.
-Require Import Registers.
-Require Import RTL.
+Require Import Zwf Coqlib Maps Integers Floats Lattice.
+Require Import Compopts AST.
+Require Import Values Memory Globalenvs Events.
+Require Import Registers RTL.
+
+(** The abstract domains for value analysis *)
 
 Inductive block_class : Type :=
   | BCinvalid
@@ -3814,7 +3805,8 @@ Lemma inj_of_bc_preserves_globals:
 Proof.
   intros. destruct H as [A B].
   split. intros. apply inj_of_bc_valid. rewrite A in H. congruence.
-  split. intros. apply inj_of_bc_valid. apply B. eapply Genv.genv_vars_range; eauto.
+  split. intros. apply inj_of_bc_valid. apply B.
+    rewrite Genv.find_var_info_iff in H. eapply Genv.genv_defs_range; eauto.
   intros. exploit inj_of_bc_inv; eauto. intros (P & Q & R). auto.
 Qed.