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, 30 insertions, 26 deletions

diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index 35d53215..f15015e8 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -14,6 +14,7 @@
 
 Require Import String.
 Require Import Coqlib.
+Require Import Maps.
 Require Import AST.
 Require Import Errors.
 Require Import Integers.
@@ -36,7 +37,7 @@ Open Local Scope string_scope.
 
 Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
   forall F V (ge: Genv.t F V) m,
-  external_call (EF_external name sg) ge vargs m E0 vres m.
+  external_call (EF_runtime name sg) ge vargs m E0 vres m.
 
 Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
   forall F V (ge: Genv.t F V) m,
@@ -61,32 +62,32 @@ Axiom i64_helpers_correct :
  /\ (forall x y, external_implements "__i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
  /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)).
 
-Definition helper_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
-  exists b, Genv.find_symbol ge id = Some b
-         /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)).
-
-Definition helper_functions_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (hf: helper_functions) : Prop :=
-     helper_declared ge hf.(i64_dtos) "__i64_dtos" sig_f_l
-  /\ helper_declared ge hf.(i64_dtou) "__i64_dtou" sig_f_l
-  /\ helper_declared ge hf.(i64_stod) "__i64_stod" sig_l_f
-  /\ helper_declared ge hf.(i64_utod) "__i64_utod" sig_l_f
-  /\ helper_declared ge hf.(i64_stof) "__i64_stof" sig_l_s
-  /\ helper_declared ge hf.(i64_utof) "__i64_utof" sig_l_s
-  /\ helper_declared ge hf.(i64_sdiv) "__i64_sdiv" sig_ll_l
-  /\ helper_declared ge hf.(i64_udiv) "__i64_udiv" sig_ll_l
-  /\ helper_declared ge hf.(i64_smod) "__i64_smod" sig_ll_l
-  /\ helper_declared ge hf.(i64_umod) "__i64_umod" sig_ll_l
-  /\ helper_declared ge hf.(i64_shl) "__i64_shl" sig_li_l
-  /\ helper_declared ge hf.(i64_shr) "__i64_shr" sig_li_l
-  /\ helper_declared ge hf.(i64_sar) "__i64_sar" sig_li_l.
+Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
+  (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))).
+
+Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop :=
+     helper_declared p hf.(i64_dtos) "__i64_dtos" sig_f_l
+  /\ helper_declared p hf.(i64_dtou) "__i64_dtou" sig_f_l
+  /\ helper_declared p hf.(i64_stod) "__i64_stod" sig_l_f
+  /\ helper_declared p hf.(i64_utod) "__i64_utod" sig_l_f
+  /\ helper_declared p hf.(i64_stof) "__i64_stof" sig_l_s
+  /\ helper_declared p hf.(i64_utof) "__i64_utof" sig_l_s
+  /\ helper_declared p hf.(i64_sdiv) "__i64_sdiv" sig_ll_l
+  /\ helper_declared p hf.(i64_udiv) "__i64_udiv" sig_ll_l
+  /\ helper_declared p hf.(i64_smod) "__i64_smod" sig_ll_l
+  /\ helper_declared p hf.(i64_umod) "__i64_umod" sig_ll_l
+  /\ helper_declared p hf.(i64_shl) "__i64_shl" sig_li_l
+  /\ helper_declared p hf.(i64_shr) "__i64_shr" sig_li_l
+  /\ helper_declared p hf.(i64_sar) "__i64_sar" sig_li_l.
 
 (** * Correctness of the instruction selection functions for 64-bit operators *)
 
 Section CMCONSTR.
 
-Variable ge: genv.
+Variable prog: program.
 Variable hf: helper_functions.
-Hypothesis HELPERS: helper_functions_declared ge hf.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
@@ -97,17 +98,20 @@ Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.
 Lemma eval_helper:
   forall le id name sg args vargs vres,
   eval_exprlist ge sp e m le args vargs ->
-  helper_declared ge id name sg  ->
+  helper_declared prog id name sg  ->
   external_implements name sg vargs vres ->
   eval_expr ge sp e m le (Eexternal id sg args) vres.
 Proof.
-  intros. destruct H0 as (b & P & Q). econstructor; eauto.
+  intros.
+  red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q).
+  rewrite <- Genv.find_funct_ptr_iff in Q. 
+  econstructor; eauto.
 Qed.
 
 Corollary eval_helper_1:
   forall le id name sg arg1 varg1 vres,
   eval_expr ge sp e m le arg1 varg1 ->
-  helper_declared ge id name sg  ->
+  helper_declared prog id name sg  ->
   external_implements name sg (varg1::nil) vres ->
   eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres.
 Proof.
@@ -118,7 +122,7 @@ Corollary eval_helper_2:
   forall le id name sg arg1 arg2 varg1 varg2 vres,
   eval_expr ge sp e m le arg1 varg1 ->
   eval_expr ge sp e m le arg2 varg2 ->
-  helper_declared ge id name sg  ->
+  helper_declared prog id name sg  ->
   external_implements name sg (varg1::varg2::nil) vres ->
   eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres.
 Proof.
@@ -845,7 +849,7 @@ Qed.
 Lemma eval_binop_long:
   forall id name sem le a b x y z,
   (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) ->
-  helper_declared ge id name sig_ll_l ->
+  helper_declared prog id name sig_ll_l ->
   external_implements name sig_ll_l (x::y::nil) z ->
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->