Require Import CoqlibC.
Require Export GlobalenvsC.
Require Import Memory.
Require Export ASTC.
Require Import MapsC.
Require Import Values.
Require Import Linking.
Require Import Conventions1.
Require Import Integers.
Set Implicit Arguments.
Generalizable Variables F.
Definition skdef_of_gdef {
F V} (
get_sg:
F ->
signature)
(
gdef:
globdef (
AST.fundef F)
V):
globdef (
AST.fundef signature)
unit :=
match gdef with
|
Gfun (
Internal f) =>
Gfun (
Internal f.(
get_sg))
|
Gfun (
External ef) =>
Gfun (
External ef)
|
Gvar v =>
Gvar (
mkglobvar tt v.(
gvar_init)
v.(
gvar_readonly)
v.(
gvar_volatile))
end.
Lemma skdef_of_gdef_is_external_gd
F V get_sg
(
gdef:
globdef (
AST.fundef F)
V):
is_external_gd (
skdef_of_gdef get_sg gdef) =
is_external_gd gdef.
Proof.
u. des_ifs. ss. clarify. Qed.
Definition skdefs_of_gdefs {
F V} (
get_sg:
F ->
signature)
(
gdefs:
list (
ident *
globdef (
AST.fundef F)
V)):
list (
ident *
globdef (
AST.fundef signature)
unit) :=
map (
update_snd (
skdef_of_gdef get_sg))
gdefs.
Module Sk.
Definition t :=
AST.program (
AST.fundef signature)
unit.
Definition load_skenv:
t ->
Genv.t (
AST.fundef signature)
unit := @
Genv.globalenv (
AST.fundef signature)
unit.
Definition load_mem:
t ->
option mem := @
Genv.init_mem (
AST.fundef signature)
unit.
Definition of_program {
F V} (
get_sg:
F ->
signature) (
prog:
AST.program (
AST.fundef F)
V):
t :=
mkprogram (
skdefs_of_gdefs get_sg prog.(
prog_defs))
prog.(
prog_public)
prog.(
prog_main).
Definition wf_match_fundef CTX F1 F2 (
match_fundef:
CTX ->
fundef F1 ->
fundef F2 ->
Prop)
(
fn_sig1:
F1 ->
signature) (
fn_sig2:
F2 ->
signature):
Prop :=
forall
ctx f1 f2
(
MATCH:
match_fundef ctx f1 f2),
(<<
EXT:
exists ef,
f1 =
External ef /\
f2 =
External ef>>)
\/ (<<
INT:
exists fd1 fd2,
f1 =
Internal fd1 /\
f2 =
Internal fd2 /\ <<
SIG:
fn_sig1 fd1 =
fn_sig2 fd2>> >>).
Definition is_external_weak F (
f:
AST.fundef F):
bool :=
match f with
|
Internal _ =>
false
|
External _ =>
true
end.
Lemma match_program_eq
F1 V1 F2 V2 fn_sig1 fn_sig2
`{
Linker (
fundef F1)} `{
Linker V1}
match_fundef match_varinfo
(
p1:
AST.program (
fundef F1)
V1)
(
p2:
AST.program (
fundef F2)
V2)
(
MATCH:
match_program match_fundef match_varinfo p1 p2)
(
WF:
wf_match_fundef match_fundef fn_sig1 fn_sig2):
<<
EQ:
Sk.of_program fn_sig1 p1 =
Sk.of_program fn_sig2 p2>>.
Proof.
rr in MATCH.
des.
unfold of_program.
r.
f_equal;
ss.
revert MATCH.
generalize p1 at 1
as CTX.
i.
destruct p1,
p2;
ss.
clear -
MATCH WF.
ginduction prog_defs;
ii;
ss;
inv MATCH;
ss.
erewrite IHprog_defs;
eauto.
f_equal;
eauto.
inv H3.
destruct a,
b1;
ss.
clarify.
inv H2;
ss.
-
unfold update_snd.
exploit WF;
eauto.
i;
des;
clarify;
ss.
+
repeat f_equal.
exploit WF;
et.
-
inv H1.
ss.
Qed.
Let match_fundef F0 F1 (
get_sig:
F0 ->
F1) (
_:
unit):
AST.fundef F0 ->
AST.fundef F1 ->
Prop :=
fun f0 f1 =>
match f0,
f1 with
|
Internal func1,
Internal func2 =>
get_sig func1 =
func2
|
External ef0,
External ef1 =>
external_function_eq ef0 ef1
|
_,
_ =>
false
end.
Lemma of_program_prog_defmap
F V (
p:
AST.program (
AST.fundef F)
V)
get_sg:
<<
SIM:
forall id,
option_rel (@
Linking.match_globdef unit _ _ _ _ _
(@
match_fundef _ _ get_sg)
top2 tt)
(
p.(
prog_defmap) !
id) ((
of_program get_sg p).(
prog_defmap) !
id)>>.
Proof.
Lemma of_program_defs_names
F V get_sg (
p:
AST.program (
AST.fundef F)
V):
(
of_program get_sg p).(
prog_defs_names) =
p.(
prog_defs_names).
Proof.
destruct p;
ss.
Local Opaque in_dec.
u;
ss.
Local Transparent in_dec.
rewrite map_map.
ss.
Qed.
Lemma of_program_defs
F V get_sg (
p:
AST.program (
AST.fundef F)
V):
(
of_program get_sg p).(
defs) =
p.(
defs).
Proof.
Local Opaque prog_defmap.
Lemma of_program_internals
F V get_sg (
p:
AST.program (
AST.fundef F)
V):
(
of_program get_sg p).(
internals) =
p.(
internals).
Proof.
Local Transparent prog_defmap.
Lemma of_program_internals'
F V get_sg (
p:
AST.program (
AST.fundef F)
V):
(
of_program get_sg p).(
internals') =
p.(
internals').
Proof.
Lemma of_program_prog_defmap_eq
F V get_sg (
p tp :
AST.program (
AST.fundef F)
V)
id
(
EQ: (
prog_defmap p) !
id = (
prog_defmap tp) !
id):
<<
EQ: (
prog_defmap (
Sk.of_program get_sg p)) !
id = (
prog_defmap (
Sk.of_program get_sg tp)) !
id>>.
Proof.
Definition empty:
t := (
mkprogram [] [] 1%
positive).
Definition get_csig (
skdef: (
AST.fundef signature)):
option signature :=
match skdef with
|
Internal sg0 =>
if sg0.(
sig_cstyle)
then Some sg0 else None
|
External ef =>
if ef.(
ef_sig).(
sig_cstyle)
then Some ef.(
ef_sig)
else None
end
.
Definition get_sig (
skdef: (
AST.fundef signature)):
signature :=
match skdef with
|
Internal sg0 =>
sg0
|
External ef =>
ef.(
ef_sig)
end.
Inductive wf (
sk:
t):
Prop :=
|
wf_intro
(
NODUP:
NoDup sk.(
prog_defs_names))
(
WFPTR:
forall id_fr gv id_to _ofs
(
IN:
In (
id_fr, (
Gvar gv))
sk.(
prog_defs))
(
INDAT:
In (
Init_addrof id_to _ofs)
gv.(
gvar_init)),
<<
IN:
In id_to sk.(
prog_defs_names)>>)
(
PUBINCL:
incl sk.(
prog_public)
sk.(
prog_defs_names))
(
WFPARAM:
forall id skd
(
IN:
In (
id, (
Gfun skd))
sk.(
prog_defs)),
4 *
size_arguments (
get_sig skd) <=
Ptrofs.max_unsigned).
End Sk.
Hint Unfold skdef_of_gdef skdefs_of_gdefs Sk.load_skenv Sk.load_mem Sk.empty.
Module SkEnv.
Definition t :=
Genv.t (
AST.fundef signature)
unit.
Inductive wf (
skenv:
t):
Prop :=
|
wf_intro
(
SYMBDEF:
forall id blk
(
SYMB:
skenv.(
Genv.find_symbol)
id =
Some blk),
<<
DEF:
exists skd,
skenv.(
Genv.find_def)
blk =
Some skd>>)
(
DEFSYMB:
forall blk skd
(
DEF:
skenv.(
Genv.find_def)
blk =
Some skd),
<<
SYMB:
exists id,
skenv.(
Genv.find_symbol)
id =
Some blk>>)
(
WFPARAM:
forall blk skd
(
DEF:
skenv.(
Genv.find_def)
blk =
Some (
Gfun skd)),
<<
SIZE: 4 *
size_arguments (
Sk.get_sig skd) <=
Ptrofs.max_unsigned>>).
Inductive wf_mem (
skenv:
t) (
sk:
Sk.t) (
m0:
mem):
Prop :=
|
wf_mem_intro
(
WFPTR:
forall blk_fr _ofs_fr blk_to _ofs_to id_fr _q _n gv
(
SYMB:
skenv.(
Genv.find_symbol)
id_fr =
Some blk_fr)
(
IN:
In (
id_fr, (
Gvar gv))
sk.(
prog_defs))
(
NONVOL:
gv.(
gvar_volatile) =
false)
(
DEFINITIVE:
classify_init gv.(
gvar_init) =
Init_definitive gv.(
gvar_init))
(
LOAD:
Mem.loadbytes m0 blk_fr _ofs_fr 1 =
Some [
Fragment (
Vptr blk_to _ofs_to)
_q _n]),
exists id_to, (<<
SYMB:
skenv.(
Genv.invert_symbol)
blk_to =
Some id_to>>)
/\ (<<
IN:
In id_to sk.(
prog_defs_names)>>)).
Lemma load_skenv_wf
sk (
WF:
Sk.wf sk):
<<
WF:
SkEnv.wf sk.(
Sk.load_skenv)>>.
Proof.
unfold Sk.load_skenv.
u.
econs;
try r.
-
unfold Genv.globalenv,
Genv.find_symbol,
Genv.find_def.
eapply Genv.add_globals_preserves;
i;
ss.
+
destruct (
peq id0 id).
{
subst id0.
rewrite PTree.gss in SYMB.
inv SYMB.
exists g.
eapply PTree.gss. }
{
rewrite PTree.gso in SYMB;
eauto.
exploit H;
eauto.
i.
inv H1.
exists x.
rewrite PTree.gso;
eauto.
exploit Genv.genv_symb_range;
eauto.
i.
xomega. }
+
rewrite PTree.gempty in SYMB.
inv SYMB.
-
intros blk skd.
set (
P :=
fun ge =>
Genv.find_def ge blk =
Some skd ->
exists id,
Genv.find_symbol ge id =
Some blk).
assert(
REC:
forall l ge,
P ge ->
NoDup (
map fst l) ->
(
forall id,
In id (
map fst l) ->
Genv.find_symbol ge id =
None) ->
P (
Genv.add_globals ge l)).
{
induction l as [| [
id1 g1]
l];
auto.
i.
eapply IHl.
-
unfold P,
Genv.add_global,
Genv.find_def,
Genv.find_symbol in *.
ss.
i.
destruct (
peq (
Genv.genv_next ge)
blk).
+
subst blk.
exists id1.
eapply PTree.gss.
+
rewrite PTree.gso in H2;
eauto.
exploit H;
eauto.
i.
des.
exists id.
rewrite PTree.gso;
eauto.
ii.
subst.
exploit H1;
eauto.
i.
congruence.
-
inv H0.
eauto.
-
i.
unfold Genv.add_global,
Genv.find_symbol.
ss.
rewrite PTree.gso.
+
eapply H1.
right.
eauto.
+
ii.
subst.
inv H0;
eauto.
}
eapply REC.
{
unfold P,
Genv.find_def.
i.
ss.
rewrite PTree.gempty in H.
inv H. }
{
inv WF.
eauto. }
{
i.
unfold Genv.find_symbol.
ss.
eapply PTree.gempty. }
-
inv WF.
i.
eapply Genv.find_def_inversion in DEF.
des.
eapply WFPARAM in DEF.
eauto.
Qed.
Inductive includes (
skenv:
SkEnv.t) (
sk:
AST.program (
AST.fundef signature)
unit):
Prop :=
|
includes_intro
(
DEFS:
forall id gd0
(
DEF:
sk.(
prog_defmap) !
id =
Some gd0),
exists blk gd1, (<<
SYMB:
skenv.(
Genv.find_symbol)
id =
Some blk>>) /\
(<<
DEF:
skenv.(
Genv.find_def)
blk =
Some gd1>>) /\
(<<
MATCH:
linkorder gd0 gd1>>))
(
PUBS:
incl sk.(
prog_public)
skenv.(
Genv.genv_public)).
Inductive project_spec (
skenv:
t) (
prog:
Sk.t) (
skenv_proj:
t):
Prop :=
|
project_spec_intro
(
NEXT:
skenv.(
Genv.genv_next) =
skenv_proj.(
Genv.genv_next))
(
SYMBKEEP:
forall id
(
KEEP:
prog.(
defs)
id),
(<<
KEEP:
skenv_proj.(
Genv.find_symbol)
id =
skenv.(
Genv.find_symbol)
id>>))
(
SYMBDROP:
forall id
(
DROP: ~
prog.(
defs)
id),
<<
NONE:
skenv_proj.(
Genv.find_symbol)
id =
None>>)
(
DEFKEEP:
forall id blk gd_big
(
INV:
skenv.(
Genv.invert_symbol)
blk =
Some id)
(
KEEP:
prog.(
internals)
id)
(
BIG:
skenv.(
Genv.find_def)
blk =
Some gd_big),
exists gd_small, <<
DEFSMALL:
skenv_proj.(
Genv.find_def)
blk =
Some gd_small>>
/\ <<
INTERNAL: ~
is_external gd_small>>
/\ <<
LO:
linkorder gd_small gd_big>>
/\ <<
PROG:
prog.(
prog_defmap) !
id =
Some gd_small>>)
(
DEFKEPT:
forall id blk gd_small
(
INV:
skenv.(
Genv.invert_symbol)
blk =
Some id)
(
SMALL:
skenv_proj.(
Genv.find_def)
blk =
Some gd_small),
<<
KEEP:
prog.(
internals)
id>> /\ <<
INTERNAL: ~
is_external gd_small>>
/\ <<
PROG:
prog.(
prog_defmap) !
id =
Some gd_small>> /\
exists gd_big, <<
DEFBIG:
skenv.(
Genv.find_def)
blk =
Some gd_big>> /\ <<
LO:
linkorder gd_small gd_big>>)
(
DEFORPHAN:
forall
blk
(
INV:
skenv.(
Genv.invert_symbol)
blk =
None),
<<
SMALL:
skenv_proj.(
Genv.find_def)
blk =
None>>)
(
PUBLIC:
prog.(
prog_public) =
skenv_proj.(
Genv.genv_public)).
Definition project (
skenv:
t) (
prog:
Sk.t):
t :=
((
Genv_update_publics skenv prog.(
prog_public)).(
Genv_filter_symb) (
fun id =>
prog.(
defs)
id))
.(
Genv_map_defs) (
fun blk gd => (
do id <-
skenv.(
Genv.invert_symbol)
blk;
assertion(
prog.(
internals)
id);
do gd <-
prog.(
prog_defmap) !
id;
Some gd)).
Lemma match_globdef_is_external_gd
(
gd1 gd2:
globdef (
AST.fundef signature)
unit)
(
MATCH:
match_globdef (@
Sk.match_fundef _ _ id)
top2 tt gd1 gd2):
is_external_gd gd1 =
is_external_gd gd2.
Proof.
inv MATCH; ss. rr in H0. des_ifs. ss. des_sumbool. clarify.
Qed.
Lemma project_impl_spec
skenv (
prog:
Sk.t)
(
INCL:
SkEnv.includes skenv prog):
<<
PROJ:
project_spec skenv prog (
project skenv prog)>>.
Proof.
Inductive wf_proj (
skenv:
t):
Prop :=
|
wf_proj_intro
(
DEFSYMB:
forall blk skd
(
DEF:
skenv.(
Genv.find_def)
blk =
Some skd),
<<
SYMB:
exists id,
skenv.(
Genv.find_symbol)
id =
Some blk>> /\ <<
INTERNAL: ~
is_external skd>>).
Lemma project_spec_preserves_wf
skenv
(
WF:
wf skenv)
(
prog:
Sk.t)
skenv_proj
(
PROJ:
project_spec skenv prog skenv_proj):
<<
WF:
wf_proj skenv_proj>>.
Proof.
inv WF.
inv PROJ.
econs;
eauto.
ii.
destruct (
Genv.invert_symbol skenv blk)
eqn:
T;
cycle 1.
{
exploit DEFORPHAN;
eauto.
i;
des.
clarify. }
rename i into id.
exploit Genv.invert_find_symbol;
eauto.
intro TT.
exploit DEFKEPT;
eauto.
i;
des.
u in H.
des_ifs_safe.
esplits;
eauto.
{
erewrite SYMBKEEP;
eauto.
u.
des_sumbool.
eapply prog_defmap_image;
et. }
Qed.
Definition internals (
skenv:
t):
list block :=
List.map fst (
skenv.(
Genv.genv_defs).(
PTree.elements)).
Definition filter_symbols (
skenv:
t) (
symbols:
list ident):
t :=
skenv.(
Genv_filter_symb) (
fun id =>
List.in_dec ident_eq id symbols).
Definition revive `{
HasExternal F} {
V} (
skenv:
SkEnv.t) (
prog:
AST.program F V):
Genv.t F V :=
(
skenv.(
Genv_map_defs)
(
fun blk gd => (
do id <-
skenv.(
Genv.invert_symbol)
blk;
do gd <-
prog.(
prog_defmap) !
id;
Some gd))).
Inductive genv_precise `{
HasExternal F} {
V} (
ge:
Genv.t F V) (
p:
program F V):
Prop :=
|
genv_compat_intro
(
P2GE:
forall id g
(
PROG:
p.(
prog_defmap) !
id =
Some g),
(
exists b, <<
SYMB:
Genv.find_symbol ge id =
Some b>> /\
<<
DEF:
Genv.find_def ge b =
if negb (
is_external g)
then Some g else None>>))
(
GE2P:
forall b g
(
DEF:
Genv.find_def ge b =
Some g),
exists id, <<
SYMB:
Genv.find_symbol ge id =
Some b>> /\ <<
PROG:
p.(
prog_defmap) !
id =
Some g>>
/\ <<
INTERNAL: ~ (
is_external g)>>)
(
SYMB2P:
forall id blk
(
SYMB:
Genv.find_symbol ge id =
Some blk),
<<
IN:
p.(
defs)
id>>).
Lemma project_revive_precise
F V
skenv (
prog:
AST.program (
fundef F)
V)
skenv_link
get_sg
(
PROJ:
SkEnv.project_spec skenv_link prog.(
Sk.of_program get_sg)
skenv)
(
INCL:
SkEnv.includes skenv_link prog.(
Sk.of_program get_sg))
:
<<
PRECISE:
SkEnv.genv_precise (
SkEnv.revive skenv prog)
prog>>
.
Proof.
Lemma project_revive_no_external
F V (
prog:
AST.program (
AST.fundef F)
V)
skenv_link get_sg blk gd
(
DEF:
Genv.find_def (
SkEnv.revive (
SkEnv.project skenv_link (
Sk.of_program get_sg prog))
prog)
blk =
Some gd)
(
EXTERNAL:
is_external gd)
(
INCL:
SkEnv.includes skenv_link (
Sk.of_program get_sg prog))
(
WF:
SkEnv.wf skenv_link):
False.
Proof.
Definition privs (
skenv:
SkEnv.t):
ident ->
bool :=
fun id =>
match skenv.(
Genv.find_symbol)
id with
|
Some _ =>
negb (
proj_sumbool (
in_dec ident_eq id skenv.(
Genv.genv_public)))
|
None =>
false
end.
Definition empty:
t := @
Genv.empty_genv _ _ [].
Lemma senv_genv_compat
F V (
skenv_link:
t)
fn_sig (
prog:
program (
AST.fundef F)
V)
(
INCL:
includes skenv_link (
Sk.of_program fn_sig prog)):
senv_genv_compat skenv_link (
SkEnv.revive (
SkEnv.project skenv_link (
Sk.of_program fn_sig prog))
prog).
Proof.
Lemma revive_incl_skenv
F V (
skenv:
t)
fn_sig (
prog:
program (
AST.fundef F)
V)
fptr fd
(
INCL :
includes skenv (
Sk.of_program fn_sig prog))
(
WF :
wf skenv)
(
FINDF :
Genv.find_funct (
SkEnv.revive (
SkEnv.project skenv (
Sk.of_program fn_sig prog))
prog)
fptr =
Some (
Internal fd)):
exists blk,
Genv.find_def skenv blk =
Some (
Gfun (
Internal (
fn_sig fd))).
Proof.
End SkEnv.
Hint Unfold SkEnv.empty.