Separate compilation and syntactic linking
Require Import Coqlib Maps Errors AST.
This file follows "approach A" from the paper
"Lightweight Verification of Separate Compilation"
by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016.
Syntactic linking
A syntactic element
A supports syntactic linking if it is equipped with the following:
-
a partial binary operator link that produces the result of linking two elements,
or fails if they cannot be linked (e.g. two definitions that are incompatible);
-
a preorder linkorder with the meaning that linkorder a1 a2 holds
if a2 can be obtained by linking a1 with some other syntactic element.
(
A:
Type) := {
link:
A ->
A ->
option A;
linkorder:
A ->
A ->
Prop;
linkorder_refl:
forall x,
linkorder x x;
linkorder_trans:
forall x y z,
linkorder x y ->
linkorder y z ->
linkorder x z;
link_linkorder:
forall x y z,
link x y =
Some z ->
linkorder x z /\
linkorder y z
}.
Linking function definitions. External functions of the EF_external
kind can link with internal function definitions; the result of
linking is the internal definition. Two external functions can link
if they are identical.
Definition link_fundef {
F:
Type} (
fd1 fd2:
fundef F) :=
match fd1,
fd2 with
|
Internal _,
Internal _ =>
None
|
External ef1,
External ef2 =>
if external_function_eq ef1 ef2 then Some (
External ef1)
else None
|
Internal f,
External ef =>
match ef with EF_external id sg =>
Some (
Internal f) |
_ =>
None end
|
External ef,
Internal f =>
match ef with EF_external id sg =>
Some (
Internal f) |
_ =>
None end
end.
Inductive linkorder_fundef {
F:
Type}:
fundef F ->
fundef F ->
Prop :=
|
linkorder_fundef_refl:
forall fd,
linkorder_fundef fd fd
|
linkorder_fundef_ext_int:
forall f id sg,
linkorder_fundef (
External (
EF_external id sg)) (
Internal f).
Instance Linker_fundef (
F:
Type):
Linker (
fundef F) := {
link :=
link_fundef;
linkorder :=
linkorder_fundef
}.
Proof.
-
intros;
constructor.
-
intros.
inv H;
inv H0;
constructor.
-
intros x y z EQ.
destruct x,
y;
simpl in EQ.
+
discriminate.
+
destruct e;
inv EQ.
split;
constructor.
+
destruct e;
inv EQ.
split;
constructor.
+
destruct (
external_function_eq e e0);
inv EQ.
split;
constructor.
Defined.
.
Linking variable initializers. We adopt the following conventions:
-
an "extern" variable has an empty initialization list;
-
a "common" variable has an initialization list of the form Init_space sz;
-
all other initialization lists correspond to fully defined variables, neither "common" nor "extern".
:
list init_data ->
Type :=
|
Init_extern:
init_class nil
|
Init_common:
forall sz,
init_class (
Init_space sz ::
nil)
|
Init_definitive:
forall il,
init_class il.
Definition classify_init (
i:
list init_data) :
init_class i :=
match i with
|
nil =>
Init_extern
|
Init_space sz ::
nil =>
Init_common sz
|
i =>
Init_definitive i
end.
Definition link_varinit (
i1 i2:
list init_data) :=
match classify_init i1,
classify_init i2 with
|
Init_extern,
_ =>
Some i2
|
_,
Init_extern =>
Some i1
|
Init_common sz1,
_ =>
if zeq sz1 (
init_data_list_size i2)
then Some i2 else None
|
_,
Init_common sz2 =>
if zeq sz2 (
init_data_list_size i1)
then Some i1 else None
|
_,
_ =>
None
end.
Inductive linkorder_varinit:
list init_data ->
list init_data ->
Prop :=
|
linkorder_varinit_refl:
forall il,
linkorder_varinit il il
|
linkorder_varinit_extern:
forall il,
linkorder_varinit nil il
|
linkorder_varinit_common:
forall sz il,
il <>
nil ->
init_data_list_size il =
sz ->
linkorder_varinit (
Init_space sz ::
nil)
il.
Instance Linker_varinit :
Linker (
list init_data) := {
link :=
link_varinit;
linkorder :=
linkorder_varinit
}.
Proof.
-
intros.
constructor.
-
intros.
inv H;
inv H0;
constructor;
auto.
congruence.
simpl.
generalize (
init_data_list_size_pos z).
xomega.
-
unfold link_varinit;
intros until z.
destruct (
classify_init x)
eqn:
Cx, (
classify_init y)
eqn:
Cy;
intros E;
inv E;
try (
split;
constructor;
fail).
+
destruct (
zeq sz (
Z.max sz0 0 + 0));
inv H0.
split;
constructor.
congruence.
auto.
+
destruct (
zeq sz (
init_data_list_size il));
inv H0.
split;
constructor.
red;
intros;
subst z;
discriminate.
auto.
+
destruct (
zeq sz (
init_data_list_size il));
inv H0.
split;
constructor.
red;
intros;
subst z;
discriminate.
auto.
Defined.
.
Linking variable definitions.
Definition link_vardef {
V:
Type} {
LV:
Linker V} (
v1 v2:
globvar V) :=
match link v1.(
gvar_info)
v2.(
gvar_info)
with
|
None =>
None
|
Some info =>
match link v1.(
gvar_init)
v2.(
gvar_init)
with
|
None =>
None
|
Some init =>
if eqb v1.(
gvar_readonly)
v2.(
gvar_readonly)
&&
eqb v1.(
gvar_volatile)
v2.(
gvar_volatile)
then Some {|
gvar_info :=
info;
gvar_init :=
init;
gvar_readonly :=
v1.(
gvar_readonly);
gvar_volatile :=
v1.(
gvar_volatile) |}
else None
end
end.
Inductive linkorder_vardef {
V:
Type} {
LV:
Linker V}:
globvar V ->
globvar V ->
Prop :=
|
linkorder_vardef_intro:
forall info1 info2 i1 i2 ro vo,
linkorder info1 info2 ->
linkorder i1 i2 ->
linkorder_vardef (
mkglobvar info1 i1 ro vo) (
mkglobvar info2 i2 ro vo).
Instance Linker_vardef (
V:
Type) {
LV:
Linker V}:
Linker (
globvar V) := {
link :=
link_vardef;
linkorder :=
linkorder_vardef
}.
Proof.
-
intros.
destruct x;
constructor;
apply linkorder_refl.
-
intros.
inv H;
inv H0.
constructor;
eapply linkorder_trans;
eauto.
-
unfold link_vardef;
intros until z.
destruct x as [
f1 i1 r1 v1],
y as [
f2 i2 r2 v2];
simpl.
destruct (
link f1 f2)
as [
f|]
eqn:
LF;
try discriminate.
destruct (
link i1 i2)
as [
i|]
eqn:
LI;
try discriminate.
destruct (
eqb r1 r2)
eqn:
ER;
try discriminate.
destruct (
eqb v1 v2)
eqn:
EV;
intros EQ;
inv EQ.
apply eqb_prop in ER;
apply eqb_prop in EV;
subst r2 v2.
apply link_linkorder in LF.
apply link_linkorder in LI.
split;
constructor;
tauto.
Defined.
.
A trivial linker for the trivial var info unit.
Instance Linker_unit:
Linker unit := {
link :=
fun x y =>
Some tt;
linkorder :=
fun x y =>
True
}.
Proof.
- auto.
- auto.
- auto.
Defined.
Global Opaque Linker_unit.
Linking global definitions
Definition link_def {
F V:
Type} {
LF:
Linker F} {
LV:
Linker V} (
gd1 gd2:
globdef F V) :=
match gd1,
gd2 with
|
Gfun f1,
Gfun f2 =>
match link f1 f2 with Some f =>
Some (
Gfun f) |
None =>
None end
|
Gvar v1,
Gvar v2 =>
match link v1 v2 with Some v =>
Some (
Gvar v) |
None =>
None end
|
_,
_ =>
None
end.
Inductive linkorder_def {
F V:
Type} {
LF:
Linker F} {
LV:
Linker V}:
globdef F V ->
globdef F V ->
Prop :=
|
linkorder_def_fun:
forall fd1 fd2,
linkorder fd1 fd2 ->
linkorder_def (
Gfun fd1) (
Gfun fd2)
|
linkorder_def_var:
forall v1 v2,
linkorder v1 v2 ->
linkorder_def (
Gvar v1) (
Gvar v2).
Instance Linker_def (
F V:
Type) {
LF:
Linker F} {
LV:
Linker V}:
Linker (
globdef F V) := {
link :=
link_def;
linkorder :=
linkorder_def
}.
Proof.
-
intros.
destruct x;
constructor;
apply linkorder_refl.
-
intros.
inv H;
inv H0;
constructor;
eapply linkorder_trans;
eauto.
-
unfold link_def;
intros.
destruct x as [
f1|
v1],
y as [
f2|
v2];
try discriminate.
+
destruct (
link f1 f2)
as [
f|]
eqn:
L;
inv H.
apply link_linkorder in L.
split;
constructor;
tauto.
+
destruct (
link v1 v2)
as [
v|]
eqn:
L;
inv H.
apply link_linkorder in L.
split;
constructor;
tauto.
Defined.
.
Linking two compilation units. Compilation units are represented like
whole programs using the type program F V. If a name has
a global definition in one unit but not in the other, this definition
is left unchanged in the result of the link. If a name has
global definitions in both units, and is public (not static) in both,
the two definitions are linked as per Linker_def above.
If one or both definitions are static (not public), we should ideally
rename it so that it can be kept unchanged in the result of the link.
This would require a general notion of renaming of global identifiers
in programs that we do not have yet. Hence, as a first step, linking
is undefined if static definitions with the same name appear in both
compilation units.
Definition link_option {
V:
Type} {
LV:
Linker V}
v1 v2 :=
match v1 with
|
None =>
Some v2
|
Some v1' =>
match v2 with
|
None =>
Some v1
|
Some v2' =>
match link v1'
v2'
with
|
None =>
None
|
Some v' =>
Some (
Some v')
end
end
end.
Definition linkorder_option {
V:
Type} {
LV:
Linker V}
v1 v2 :=
match v1 with
|
None =>
True
|
Some v1' =>
match v2 with
|
None =>
False
|
Some v2' =>
linkorder v1'
v2'
end
end.
Local Program Instance Linker_option (
V:
Type) {
LV:
Linker V}:
Linker (
option V) := {
link :=
link_option;
linkorder :=
linkorder_option
}.
Next Obligation.
Next Obligation.
Next Obligation.
Section LINKER_PROG.
Context {
F V:
Type} {
LF:
Linker F} {
LV:
Linker V} (
p1 p2:
program F V).
Let dm1 :=
prog_option_defmap p1.
Let dm2 :=
prog_option_defmap p2.
Definition link_prog_check (
x:
ident) (
gd1:
option (
globdef F V)) :=
match dm2!
x with
|
None =>
true
|
Some gd2 =>
In_dec peq x p1.(
prog_public)
&&
In_dec peq x p2.(
prog_public)
&&
match link gd1 gd2 with Some _ =>
true |
None =>
false end
end.
Definition link_prog_merge (
o1 o2:
option (
option (
globdef F V))) :=
match o1,
o2 with
|
None,
_ =>
o2
|
_,
None =>
o1
|
Some gd1,
Some gd2 =>
link gd1 gd2
end.
Definition link_prog :=
if ident_eq p1.(
prog_main)
p2.(
prog_main)
&&
PTree_Properties.for_all dm1 link_prog_check then
Some {|
prog_main :=
p1.(
prog_main);
prog_public :=
p1.(
prog_public) ++
p2.(
prog_public);
prog_defs :=
PTree.elements (
PTree.combine link_prog_merge dm1 dm2) |}
else
None.
Lemma link_prog_inv:
forall p,
link_prog =
Some p ->
p1.(
prog_main) =
p2.(
prog_main)
/\ (
forall id gd1 gd2,
dm1!
id =
Some gd1 ->
dm2!
id =
Some gd2 ->
In id p1.(
prog_public) /\
In id p2.(
prog_public) /\
exists gd,
link gd1 gd2 =
Some gd)
/\
p = {|
prog_main :=
p1.(
prog_main);
prog_public :=
p1.(
prog_public) ++
p2.(
prog_public);
prog_defs :=
PTree.elements (
PTree.combine link_prog_merge dm1 dm2) |}.
Proof.
Lemma link_prog_inv_strong:
forall p,
link_prog =
Some p ->
p1.(
prog_main) =
p2.(
prog_main)
/\ (
forall id gd1 gd2,
(
prog_defmap p1)!
id =
Some gd1 -> (
prog_defmap p2)!
id =
Some gd2 ->
In id p1.(
prog_public) /\
In id p2.(
prog_public) /\
exists gd,
link gd1 gd2 =
Some gd)
/\
p = {|
prog_main :=
p1.(
prog_main);
prog_public :=
p1.(
prog_public) ++
p2.(
prog_public);
prog_defs :=
PTree.elements (
PTree.combine link_prog_merge dm1 dm2) |}.
Proof.
intros p H.
exploit link_prog_inv;
eauto.
intros (
MAIN &
DEFS &
P).
split;
auto.
split;
auto.
intros id gd1 gd2 H0 H1.
apply prog_defmap_option_defmap in H0.
apply prog_defmap_option_defmap in H1.
exploit DEFS;
eauto.
destruct 1
as (
I1 &
I2 &
gd &
Hgd).
split;
auto.
split;
auto.
simpl in Hgd.
destruct (
link gd1 gd2);
eauto.
discriminate.
Qed.
Lemma link_prog_succeeds:
p1.(
prog_main) =
p2.(
prog_main) ->
(
forall id gd1 gd2,
dm1!
id =
Some gd1 ->
dm2!
id =
Some gd2 ->
In id p1.(
prog_public) /\
In id p2.(
prog_public) /\
link gd1 gd2 <>
None) ->
link_prog =
Some {|
prog_main :=
p1.(
prog_main);
prog_public :=
p1.(
prog_public) ++
p2.(
prog_public);
prog_defs :=
PTree.elements (
PTree.combine link_prog_merge dm1 dm2) |}.
Proof.
Lemma prog_option_defmap_elements:
forall (
m:
PTree.t (
option (
globdef F V)))
pub mn x,
(
prog_option_defmap {|
prog_defs :=
PTree.elements m;
prog_public :=
pub;
prog_main :=
mn |})!
x =
m!
x.
Proof.
End LINKER_PROG.
Instance Linker_prog (
F V:
Type) {
LF:
Linker F} {
LV:
Linker V} :
Linker (
program F V) := {
link :=
link_prog;
linkorder :=
fun p1 p2 =>
p1.(
prog_main) =
p2.(
prog_main)
/\
incl p1.(
prog_public)
p2.(
prog_public)
/\
forall id gd1,
(
prog_option_defmap p1)!
id =
Some gd1 ->
exists gd2,
(
prog_option_defmap p2)!
id =
Some gd2
/\
linkorder gd1 gd2
/\ (~
In id p2.(
prog_public) ->
gd2 =
gd1)
}.
Proof.
Lemma prog_option_defmap_linkorder:
forall {
F V:
Type} {
LF:
Linker F} {
LV:
Linker V} (
p1 p2:
program F V)
id gd1,
linkorder p1 p2 ->
(
prog_option_defmap p1)!
id =
Some gd1 ->
exists gd2, (
prog_option_defmap p2)!
id =
Some gd2 /\
linkorder gd1 gd2.
Proof.
intros. destruct H as (A & B & C).
exploit C; eauto. intros (gd2 & P & Q & R). exists gd2; auto.
Qed.
Lemma prog_defmap_linkorder:
forall {
F V:
Type} {
LF:
Linker F} {
LV:
Linker V} (
p1 p2:
program F V)
id gd1,
linkorder p1 p2 ->
(
prog_defmap p1)!
id =
Some gd1 ->
exists gd2, (
prog_defmap p2)!
id =
Some gd2 /\
linkorder gd1 gd2.
Proof.
Global Opaque Linker_prog.
Matching between two programs
The following is a relational presentation of program transformations,
e.g. transf_partial_program from module AST.
To capture the possibility of separate compilation, we parameterize
the match_fundef relation between function definitions with
a context, e.g. the compilation unit from which the function definition comes.
This unit is characterized as any program that is in the linkorder
relation with the final, whole program.
Section MATCH_PROGRAM_GENERIC.
Context {
C F1 V1 F2 V2:
Type} {
LC:
Linker C} {
LF:
Linker F1} {
LV:
Linker V1}.
Variable match_fundef:
C ->
F1 ->
F2 ->
Prop.
Variable match_varinfo:
V1 ->
V2 ->
Prop.
Inductive match_globvar:
globvar V1 ->
globvar V2 ->
Prop :=
|
match_globvar_intro:
forall i1 i2 init ro vo,
match_varinfo i1 i2 ->
match_globvar (
mkglobvar i1 init ro vo) (
mkglobvar i2 init ro vo).
Inductive match_globdef (
ctx:
C):
globdef F1 V1 ->
globdef F2 V2 ->
Prop :=
|
match_globdef_fun:
forall ctx'
f1 f2,
linkorder ctx'
ctx ->
match_fundef ctx'
f1 f2 ->
match_globdef ctx (
Gfun f1) (
Gfun f2)
|
match_globdef_var:
forall v1 v2,
match_globvar v1 v2 ->
match_globdef ctx (
Gvar v1) (
Gvar v2).
Definition match_ident_option_globdef
(
ctx:
C) (
ig1:
ident *
option (
globdef F1 V1)) (
ig2:
ident *
option (
globdef F2 V2)) :
Prop :=
fst ig1 =
fst ig2 /\
option_rel (
match_globdef ctx) (
snd ig1) (
snd ig2).
Definition match_program_gen (
ctx:
C) (
p1:
program F1 V1) (
p2:
program F2 V2) :
Prop :=
list_forall2 (
match_ident_option_globdef ctx)
p1.(
prog_defs)
p2.(
prog_defs)
/\
p2.(
prog_main) =
p1.(
prog_main)
/\
p2.(
prog_public) =
p1.(
prog_public).
Theorem match_program_defmap:
forall ctx p1 p2,
match_program_gen ctx p1 p2 ->
forall id,
option_rel (
match_globdef ctx) (
prog_defmap p1)!
id (
prog_defmap p2)!
id.
Proof.
Theorem match_program_option_defmap:
forall ctx p1 p2,
match_program_gen ctx p1 p2 ->
forall id,
option_rel (
option_rel (
match_globdef ctx)) (
prog_option_defmap p1)!
id (
prog_option_defmap p2)!
id.
Proof.
Lemma match_program_gen_main:
forall ctx p1 p2,
match_program_gen ctx p1 p2 ->
p2.(
prog_main) =
p1.(
prog_main).
Proof.
intros. apply H.
Qed.
Lemma match_program_public:
forall ctx p1 p2,
match_program_gen ctx p1 p2 ->
p2.(
prog_public) =
p1.(
prog_public).
Proof.
intros. apply H.
Qed.
End MATCH_PROGRAM_GENERIC.
In many cases, the context for match_program_gen is the source program or
source compilation unit itself. We provide a specialized definition for this case.
Definition match_program {
F1 V1 F2 V2:
Type} {
LF:
Linker F1} {
LV:
Linker V1}
(
match_fundef:
program F1 V1 ->
F1 ->
F2 ->
Prop)
(
match_varinfo:
V1 ->
V2 ->
Prop)
(
p1:
program F1 V1) (
p2:
program F2 V2) :
Prop :=
match_program_gen match_fundef match_varinfo p1 p1 p2.
Lemma match_program_main:
forall {
F1 V1 F2 V2:
Type} {
LF:
Linker F1} {
LV:
Linker V1}
{
match_fundef:
program F1 V1 ->
F1 ->
F2 ->
Prop}
{
match_varinfo:
V1 ->
V2 ->
Prop}
{
p1:
program F1 V1} {
p2:
program F2 V2},
match_program match_fundef match_varinfo p1 p2 ->
p2.(
prog_main) =
p1.(
prog_main).
Proof.
intros. apply H.
Qed.
Relation between the program transformation functions from AST
and the match_program predicate.
Theorem match_transform_partial_program2:
forall {
C F1 V1 F2 V2:
Type} {
LC:
Linker C} {
LF:
Linker F1} {
LV:
Linker V1}
(
match_fundef:
C ->
F1 ->
F2 ->
Prop)
(
match_varinfo:
V1 ->
V2 ->
Prop)
(
transf_fun:
ident ->
F1 ->
res F2)
(
transf_var:
ident ->
V1 ->
res V2)
(
ctx:
C) (
p:
program F1 V1) (
tp:
program F2 V2),
transform_partial_program2 transf_fun transf_var p =
OK tp ->
(
forall i f tf,
transf_fun i f =
OK tf ->
match_fundef ctx f tf) ->
(
forall i v tv,
transf_var i v =
OK tv ->
match_varinfo v tv) ->
match_program_gen match_fundef match_varinfo ctx p tp.
Proof.
unfold transform_partial_program2;
intros.
monadInv H.
red;
simpl;
split;
auto.
revert x EQ.
generalize (
prog_defs p).
induction l as [ | [
i g]
l];
simpl;
intros.
-
monadInv EQ.
constructor.
-
destruct g as [[
f|
v]|].
+
destruct (
transf_fun i f)
as [
tf|?]
eqn:
TF;
monadInv EQ.
constructor;
auto.
split;
simpl;
auto.
econstructor.
econstructor.
apply linkorder_refl.
eauto.
+
destruct (
transf_globvar transf_var i v)
as [
tv|?]
eqn:
TV;
monadInv EQ.
constructor;
auto.
split;
simpl;
auto.
constructor.
constructor.
monadInv TV.
destruct v;
simpl;
constructor.
eauto.
+
monadInv EQ.
constructor;
auto.
split;
simpl;
auto.
constructor.
Qed.
Theorem match_transform_partial_program_contextual:
forall {
A B V:
Type} {
LA:
Linker A} {
LV:
Linker V}
(
match_fundef:
program A V ->
A ->
B ->
Prop)
(
transf_fun:
A ->
res B)
(
p:
program A V) (
tp:
program B V),
transform_partial_program transf_fun p =
OK tp ->
(
forall f tf,
transf_fun f =
OK tf ->
match_fundef p f tf) ->
match_program match_fundef eq p tp.
Proof.
Theorem match_transform_program_contextual:
forall {
A B V:
Type} {
LA:
Linker A} {
LV:
Linker V}
(
match_fundef:
program A V ->
A ->
B ->
Prop)
(
transf_fun:
A ->
B)
(
p:
program A V),
(
forall f,
match_fundef p f (
transf_fun f)) ->
match_program match_fundef eq p (
transform_program transf_fun p).
Proof.
The following two theorems are simpler versions for the case where the
function transformation does not depend on the compilation unit.
Theorem match_transform_partial_program:
forall {
A B V:
Type} {
LA:
Linker A} {
LV:
Linker V}
(
transf_fun:
A ->
res B)
(
p:
program A V) (
tp:
program B V),
transform_partial_program transf_fun p =
OK tp ->
match_program (
fun cu f tf =>
transf_fun f =
OK tf)
eq p tp.
Proof.
Theorem match_transform_program:
forall {
A B V:
Type} {
LA:
Linker A} {
LV:
Linker V}
(
transf:
A ->
B)
(
p:
program A V),
match_program (
fun cu f tf =>
tf =
transf f)
eq p (
transform_program transf p).
Proof.
Commutation between linking and program transformations
Section LINK_MATCH_PROGRAM.
Context {
C F1 V1 F2 V2:
Type} {
LC:
Linker C} {
LF1:
Linker F1} {
LF2:
Linker F2} {
LV1:
Linker V1} {
LV2:
Linker V2}.
Variable match_fundef:
C ->
F1 ->
F2 ->
Prop.
Variable match_varinfo:
V1 ->
V2 ->
Prop.
Local Transparent Linker_vardef Linker_def Linker_prog.
Hypothesis link_match_fundef:
forall ctx1 ctx2 f1 tf1 f2 tf2 f,
link f1 f2 =
Some f ->
match_fundef ctx1 f1 tf1 ->
match_fundef ctx2 f2 tf2 ->
exists tf,
link tf1 tf2 =
Some tf /\ (
match_fundef ctx1 f tf \/
match_fundef ctx2 f tf).
Hypothesis link_match_varinfo:
forall v1 tv1 v2 tv2 v,
link v1 v2 =
Some v ->
match_varinfo v1 tv1 ->
match_varinfo v2 tv2 ->
exists tv,
link tv1 tv2 =
Some tv /\
match_varinfo v tv.
Lemma link_match_globvar:
forall v1 tv1 v2 tv2 v,
link v1 v2 =
Some v ->
match_globvar match_varinfo v1 tv1 ->
match_globvar match_varinfo v2 tv2 ->
exists tv,
link tv1 tv2 =
Some tv /\
match_globvar match_varinfo v tv.
Proof.
simpl;
intros.
unfold link_vardef in *.
inv H0;
inv H1;
simpl in *.
destruct (
link i1 i0)
as [
info'|]
eqn:
LINFO;
try discriminate.
destruct (
link init init0)
as [
init'|]
eqn:
LINIT;
try discriminate.
destruct (
eqb ro ro0 &&
eqb vo vo0);
inv H.
exploit link_match_varinfo;
eauto.
intros (
tinfo &
P &
Q).
rewrite P.
econstructor;
split.
eauto.
constructor.
auto.
Qed.
Lemma link_match_globdef:
forall ctx1 ctx2 ctx g1 tg1 g2 tg2 g,
linkorder ctx1 ctx ->
linkorder ctx2 ctx ->
link g1 g2 =
Some g ->
match_globdef match_fundef match_varinfo ctx1 g1 tg1 ->
match_globdef match_fundef match_varinfo ctx2 g2 tg2 ->
exists tg,
link tg1 tg2 =
Some tg /\
match_globdef match_fundef match_varinfo ctx g tg.
Proof.
simpl link.
unfold link_def.
intros.
inv H2;
inv H3;
try discriminate.
-
destruct (
link f1 f0)
as [
f|]
eqn:
LF;
inv H1.
exploit link_match_fundef;
eauto.
intros (
tf &
P &
Q).
assert (
X:
exists ctx',
linkorder ctx'
ctx /\
match_fundef ctx'
f tf).
{
destruct Q as [
Q|
Q];
econstructor; (
split; [|
eassumption]).
apply linkorder_trans with ctx1;
auto.
apply linkorder_trans with ctx2;
auto. }
destruct X as (
cu &
X &
Y).
exists (
Gfun tf);
split.
rewrite P;
auto.
econstructor;
eauto.
-
destruct (
link v1 v0)
as [
v|]
eqn:
LVAR;
inv H1.
exploit link_match_globvar;
eauto.
intros (
tv &
P &
Q).
exists (
Gvar tv);
split.
rewrite P;
auto.
constructor;
auto.
Qed.
Lemma match_globdef_linkorder:
forall ctx ctx'
g tg,
match_globdef match_fundef match_varinfo ctx g tg ->
linkorder ctx ctx' ->
match_globdef match_fundef match_varinfo ctx'
g tg.
Proof.
intros.
inv H.
-
econstructor.
eapply linkorder_trans;
eauto.
auto.
-
constructor;
auto.
Qed.
Lemma option_rel_match_globdef_linkorder ctx ctx'
g1 g2:
option_rel (
match_globdef match_fundef match_varinfo ctx)
g1 g2 ->
linkorder ctx ctx' ->
option_rel (
match_globdef match_fundef match_varinfo ctx')
g1 g2.
Proof.
Lemma link_match_option_globdef:
forall ctx1 ctx2 ctx g1 tg1 g2 tg2 g,
linkorder ctx1 ctx ->
linkorder ctx2 ctx ->
link g1 g2 =
Some g ->
option_rel (
match_globdef match_fundef match_varinfo ctx1)
g1 tg1 ->
option_rel (
match_globdef match_fundef match_varinfo ctx2)
g2 tg2 ->
exists tg,
link tg1 tg2 =
Some tg /\
option_rel (
match_globdef match_fundef match_varinfo ctx)
g tg.
Proof.
inversion 4;
subst;
simpl in * .
+
inv H1.
esplit;
split;
eauto.
eapply option_rel_match_globdef_linkorder;
eauto.
+
inversion 1;
subst.
-
esplit.
split;
eauto.
inv H1.
constructor.
eapply match_globdef_linkorder;
eauto.
-
destruct (
link_def x x0)
eqn:
LINK ;
try discriminate.
inv H1.
exploit link_match_globdef; (
try eexact LINK); (
try eexact H3); (
try eexact H5);
eauto.
destruct 1
as (
tg &
LINK' &
MATCH).
assert (
link_def y y0 =
Some tg)
as LINK_DEF'
by assumption.
rewrite LINK_DEF' .
esplit.
split;
eauto.
constructor;
auto.
Qed.
Theorem link_match_program:
forall ctx1 ctx2 ctx p1 p2 tp1 tp2 p,
link p1 p2 =
Some p ->
match_program_gen match_fundef match_varinfo ctx1 p1 tp1 ->
match_program_gen match_fundef match_varinfo ctx2 p2 tp2 ->
linkorder ctx1 ctx ->
linkorder ctx2 ctx ->
exists tp,
link tp1 tp2 =
Some tp /\
match_program_gen match_fundef match_varinfo ctx p tp.
Proof.
End LINK_MATCH_PROGRAM.
We now wrap this commutation diagram into a class, and provide some common instances.
Class TransfLink {
A B:
Type} {
LA:
Linker A} {
LB:
Linker B} (
transf:
A ->
B ->
Prop) :=
transf_link:
forall (
p1 p2:
A) (
tp1 tp2:
B) (
p:
A),
link p1 p2 =
Some p ->
transf p1 tp1 ->
transf p2 tp2 ->
exists tp,
link tp1 tp2 =
Some tp /\
transf p tp.
Remark link_transf_partial_fundef:
forall (
A B:
Type) (
tr1 tr2:
A ->
res B) (
f1 f2:
fundef A) (
tf1 tf2:
fundef B) (
f:
fundef A),
link f1 f2 =
Some f ->
transf_partial_fundef tr1 f1 =
OK tf1 ->
transf_partial_fundef tr2 f2 =
OK tf2 ->
exists tf,
link tf1 tf2 =
Some tf
/\ (
transf_partial_fundef tr1 f =
OK tf \/
transf_partial_fundef tr2 f =
OK tf).
Proof.
Local Transparent Linker_fundef.
simpl;
intros.
destruct f1 as [
f1|
ef1],
f2 as [
f2|
ef2];
simpl in *;
monadInv H0;
monadInv H1.
-
discriminate.
-
destruct ef2;
inv H.
exists (
Internal x);
split;
auto.
left;
simpl;
rewrite EQ;
auto.
-
destruct ef1;
inv H.
exists (
Internal x);
split;
auto.
right;
simpl;
rewrite EQ;
auto.
-
destruct (
external_function_eq ef1 ef2);
inv H.
exists (
External ef2);
split;
auto.
simpl.
rewrite dec_eq_true;
auto.
Qed.
Instance TransfPartialContextualLink
{
A B C V:
Type} {
LV:
Linker V}
(
tr_fun:
C ->
A ->
res B)
(
ctx_for:
program (
fundef A)
V ->
C):
TransfLink (
fun (
p1:
program (
fundef A)
V) (
p2:
program (
fundef B)
V) =>
match_program
(
fun cu f tf =>
AST.transf_partial_fundef (
tr_fun (
ctx_for cu))
f =
OK tf)
eq p1 p2).
Proof.
Instance TransfPartialLink
{
A B V:
Type} {
LV:
Linker V}
(
tr_fun:
A ->
res B):
TransfLink (
fun (
p1:
program (
fundef A)
V) (
p2:
program (
fundef B)
V) =>
match_program
(
fun cu f tf =>
AST.transf_partial_fundef tr_fun f =
OK tf)
eq p1 p2).
Proof.
Instance TransfTotallContextualLink
{
A B C V:
Type} {
LV:
Linker V}
(
tr_fun:
C ->
A ->
B)
(
ctx_for:
program (
fundef A)
V ->
C):
TransfLink (
fun (
p1:
program (
fundef A)
V) (
p2:
program (
fundef B)
V) =>
match_program
(
fun cu f tf =>
tf =
AST.transf_fundef (
tr_fun (
ctx_for cu))
f)
eq p1 p2).
Proof.
red.
intros.
destruct (
link_linkorder _ _ _ H)
as [
LO1 LO2].
eapply link_match_program;
eauto.
-
intros.
subst.
destruct f1,
f2;
simpl in *.
+
discriminate.
+
destruct e;
inv H2.
econstructor;
eauto.
+
destruct e;
inv H2.
econstructor;
eauto.
+
destruct (
external_function_eq e e0);
inv H2.
econstructor;
eauto.
-
intros;
subst.
exists v;
auto.
Qed.
Instance TransfTotalLink
{
A B V:
Type} {
LV:
Linker V}
(
tr_fun:
A ->
B):
TransfLink (
fun (
p1:
program (
fundef A)
V) (
p2:
program (
fundef B)
V) =>
match_program
(
fun cu f tf =>
tf =
AST.transf_fundef tr_fun f)
eq p1 p2).
Proof.
red.
intros.
destruct (
link_linkorder _ _ _ H)
as [
LO1 LO2].
eapply link_match_program;
eauto.
-
intros.
subst.
destruct f1,
f2;
simpl in *.
+
discriminate.
+
destruct e;
inv H2.
econstructor;
eauto.
+
destruct e;
inv H2.
econstructor;
eauto.
+
destruct (
external_function_eq e e0);
inv H2.
econstructor;
eauto.
-
intros;
subst.
exists v;
auto.
Qed.
Linking a set of compilation units
Here, we take a more general view of linking as taking a nonempty list of compilation units
and producing a whole program.
Section LINK_LIST.
Context {
A:
Type} {
LA:
Linker A}.
Fixpoint link_list (
l:
nlist A) :
option A :=
match l with
|
nbase a =>
Some a
|
ncons a l =>
match link_list l with None =>
None |
Some b =>
link a b end
end.
End LINK_LIST.
List linking commutes with program transformations, provided the
transformation commutes with simple (binary) linking.
Section LINK_LIST_MATCH.
Context {
A B:
Type} {
LA:
Linker A} {
LB:
Linker B} (
prog_match:
A ->
B ->
Prop) {
TL:
TransfLink prog_match}.
Theorem link_list_match:
forall al bl,
nlist_forall2 prog_match al bl ->
forall a,
link_list al =
Some a ->
exists b,
link_list bl =
Some b /\
prog_match a b.
Proof.
induction 1;
simpl;
intros a'
L.
-
inv L.
exists b;
auto.
-
destruct (
link_list l)
as [
a1|]
eqn:
LL;
try discriminate.
exploit IHnlist_forall2;
eauto.
intros (
b' &
P &
Q).
red in TL.
exploit TL;
eauto.
intros (
b'' &
U &
V).
rewrite P;
exists b'';
auto.
Qed.
End LINK_LIST_MATCH.
Linking and composition of compilation passes
Set Implicit Arguments.
A generic language is a type of programs and a linker.
Structure Language :=
mklang {
lang_prog :>
Type;
lang_link:
Linker lang_prog }.
Canonical Structure Language_gen (
A:
Type) (
L:
Linker A) :
Language := @
mklang A L.
A compilation pass from language S (source) to language T (target)
is a matching relation between S programs and T programs,
plus two linkers, one for S and one for T,
and a property of commutation with linking.
Record Pass (
S T:
Language) :=
mkpass {
pass_match :>
lang_prog S ->
lang_prog T ->
Prop;
pass_match_link: @
TransfLink (
lang_prog S) (
lang_prog T) (
lang_link S) (
lang_link T)
pass_match
}.
Arguments mkpass {
S} {
T} (
pass_match) {
pass_match_link}.
Program Definition pass_identity (
l:
Language):
Pass l l :=
{|
pass_match :=
fun p1 p2 =>
p1 =
p2;
pass_match_link :=
_ |}.
Next Obligation.
red; intros. subst. exists p; auto.
Defined.
Program Definition pass_compose {
l1 l2 l3:
Language} (
pass:
Pass l1 l2) (
pass':
Pass l2 l3) :
Pass l1 l3 :=
{|
pass_match :=
fun p1 p3 =>
exists p2,
pass_match pass p1 p2 /\
pass_match pass'
p2 p3;
pass_match_link :=
_ |}.
Next Obligation.
red;
intros.
destruct H0 as (
p1' &
A1 &
B1).
destruct H1 as (
p2' &
A2 &
B2).
edestruct (
pass_match_link pass)
as (
p' &
A &
B);
eauto.
edestruct (
pass_match_link pass')
as (
tp &
C &
D);
eauto.
Defined.
A list of compilation passes that can be composed.
Inductive Passes:
Language ->
Language ->
Type :=
|
pass_nil:
forall l,
Passes l l
|
pass_cons:
forall l1 l2 l3,
Pass l1 l2 ->
Passes l2 l3 ->
Passes l1 l3.
Infix ":::" :=
pass_cons (
at level 60,
right associativity) :
linking_scope.
The pass corresponding to the composition of a list of passes.
Fixpoint compose_passes (
l l':
Language) (
passes:
Passes l l') :
Pass l l' :=
match passes in Passes l l'
return Pass l l'
with
|
pass_nil l =>
pass_identity l
|
pass_cons l1 l2 l3 pass1 passes =>
pass_compose pass1 (
compose_passes passes)
end.
Some more lemmas about nlist_forall2.
Lemma nlist_forall2_identity:
forall (
A:
Type) (
la lb:
nlist A),
nlist_forall2 (
fun a b =>
a =
b)
la lb ->
la =
lb.
Proof.
induction 1; congruence.
Qed.
Lemma nlist_forall2_compose_inv:
forall (
A B C:
Type) (
R1:
A ->
B ->
Prop) (
R2:
B ->
C ->
Prop)
(
la:
nlist A) (
lc:
nlist C),
nlist_forall2 (
fun a c =>
exists b,
R1 a b /\
R2 b c)
la lc ->
exists lb:
nlist B,
nlist_forall2 R1 la lb /\
nlist_forall2 R2 lb lc.
Proof.
induction 1.
-
rename b into c.
destruct H as (
b &
P &
Q).
exists (
nbase b);
split;
constructor;
auto.
-
rename b into c.
destruct H as (
b &
P &
Q).
destruct IHnlist_forall2 as (
lb &
U &
V).
exists (
ncons b lb);
split;
constructor;
auto.
Qed.
List linking with a composition of compilation passes.
Theorem link_list_compose_passes:
forall (
src tgt:
Language) (
passes:
Passes src tgt)
(
src_units:
nlist src) (
tgt_units:
nlist tgt),
nlist_forall2 (
pass_match (
compose_passes passes))
src_units tgt_units ->
forall src_prog,
@
link_list _ (
lang_link src)
src_units =
Some src_prog ->
exists tgt_prog,
@
link_list _ (
lang_link tgt)
tgt_units =
Some tgt_prog
/\
pass_match (
compose_passes passes)
src_prog tgt_prog.
Proof.