Elimination of unreferenced static definitions
Require Import FSets Coqlib Maps Ordered Iteration Errors.
Require Import AST Linking.
Require Import Integers Values Memory Globalenvs Events Smallstep.
Require Import Op Registers RTL.
Require Import Unusedglob.
Require Import sflib.
Require SimMemInj.
Module ISF :=
FSetFacts.Facts(
IS).
Module ISP :=
FSetProperties.Properties(
IS).
Definition IS_to_idset (
used:
IS.t):
ident ->
bool :=
fun elt =>
IS.mem elt used.
Hint Unfold IS_to_idset.
Coercion IS_to_idset:
IS.t >->
Funclass.
Relational specification of the transformation
The transformed program is obtained from the original program
by keeping only the global definitions that belong to a given
set u of names.
Record match_prog_1 (
used:
ident ->
bool) (
p tp:
program) :
Prop := {
match_prog_main:
tp.(
prog_main) =
p.(
prog_main);
match_prog_public:
tp.(
prog_public) =
p.(
prog_public);
match_prog_def:
forall id,
(
prog_defmap tp)!
id =
if used id then (
prog_defmap p)!
id else None;
match_prog_unique:
list_norepet (
prog_defs_names tp)
}.
This set u (as "used") must be closed under references, and
contain the entry point and the public identifiers of the program.
Definition ref_function (
f:
function) (
id:
ident) :
Prop :=
exists pc i,
f.(
fn_code)!
pc =
Some i /\
In id (
ref_instruction i).
Definition ref_fundef (
fd:
fundef) (
id:
ident) :
Prop :=
match fd with Internal f =>
ref_function f id |
External ef =>
False end.
Definition ref_init (
il:
list init_data) (
id:
ident) :
Prop :=
exists ofs,
In (
Init_addrof id ofs)
il.
Definition ref_def (
gd:
globdef fundef unit) (
id:
ident) :
Prop :=
match gd with
|
Gfun fd =>
ref_fundef fd id
|
Gvar gv =>
ref_init gv.(
gvar_init)
id
end.
Record valid_used_set (
p:
program) (
used:
ident ->
bool) :
Prop := {
used_closed:
forall id gd id',
used id -> (
prog_defmap p)!
id =
Some gd ->
ref_def gd id' ->
used id';
used_main:
used p.(
prog_main);
used_public:
forall id,
In id p.(
prog_public) ->
used id;
used_defined:
forall id,
used id ->
In id (
prog_defs_names p) \/
id =
p.(
prog_main)
}.
Definition used_set (
tp:
program):
ident ->
bool :=
fun id =>
in_dec Pos.eq_dec id (
tp.(
prog_main) :: (
tp.(
prog_defs_names))).
Definition match_prog (
p tp:
program) :
Prop :=
exists used:
ident ->
bool,
valid_used_set p used /\
match_prog_1 used p tp
/\ <<
EXACT:
used =
used_set tp>>.
Definition match_prog_weak (
p tp:
program) :
Prop :=
exists used:
ident ->
bool,
valid_used_set p used /\
match_prog_1 used p tp.
Lemma match_prog_weakening:
match_prog <2=
match_prog_weak.
Proof.
i. inv PR. des. econs; eauto. Qed.
Properties of the static analysis
Monotonic evolution of the workset.
Inductive workset_incl (
w1 w2:
workset) :
Prop :=
workset_incl_intro:
forall (
SEEN:
IS.Subset w1.(
w_seen)
w2.(
w_seen))
(
TODO:
List.incl w1.(
w_todo)
w2.(
w_todo))
(
TRACK:
forall id,
IS.In id w2.(
w_seen) ->
IS.In id w1.(
w_seen) \/
List.In id w2.(
w_todo)),
workset_incl w1 w2.
Lemma seen_workset_incl:
forall w1 w2 id,
workset_incl w1 w2 ->
IS.In id w1 ->
IS.In id w2.
Proof.
intros. destruct H. auto.
Qed.
Lemma workset_incl_refl:
forall w,
workset_incl w w.
Proof.
intros; split. red; auto. red; auto. auto.
Qed.
Lemma workset_incl_trans:
forall w1 w2 w3,
workset_incl w1 w2 ->
workset_incl w2 w3 ->
workset_incl w1 w3.
Proof.
intros. destruct H, H0; split.
red; eauto.
red; eauto.
intros. edestruct TRACK0; eauto. edestruct TRACK; eauto.
Qed.
Lemma add_workset_incl:
forall id w,
workset_incl w (
add_workset id w).
Proof.
Lemma addlist_workset_incl:
forall l w,
workset_incl w (
addlist_workset l w).
Proof.
Lemma add_ref_function_incl:
forall f w,
workset_incl w (
add_ref_function f w).
Proof.
Lemma add_ref_globvar_incl:
forall gv w,
workset_incl w (
add_ref_globvar gv w).
Proof.
Lemma add_ref_definition_incl:
forall pm id w,
workset_incl w (
add_ref_definition pm id w).
Proof.
Lemma initial_workset_incl:
forall p,
workset_incl {|
w_seen :=
IS.empty;
w_todo :=
nil |} (
initial_workset p).
Proof.
Soundness properties for functions that add identifiers to the workset
Lemma seen_add_workset:
forall id (
w:
workset),
IS.In id (
add_workset id w).
Proof.
Lemma seen_addlist_workset:
forall id l (
w:
workset),
In id l ->
IS.In id (
addlist_workset l w).
Proof.
Lemma seen_add_ref_function:
forall id f w,
ref_function f id ->
IS.In id (
add_ref_function f w).
Proof.
Lemma seen_add_ref_definition:
forall pm id gd id'
w,
pm!
id =
Some gd ->
ref_def gd id' ->
IS.In id' (
add_ref_definition pm id w).
Proof.
Lemma seen_main_initial_workset:
forall p,
IS.In p.(
prog_main) (
initial_workset p).
Proof.
Lemma seen_public_initial_workset:
forall p id,
In id p.(
prog_public) ->
IS.In id (
initial_workset p).
Proof.
Correctness of the transformation with respect to the relational specification
Correctness of the dependency graph traversal.
Section ANALYSIS.
Variable p:
program.
Let pm :=
prog_defmap p.
Definition workset_invariant (
w:
workset) :
Prop :=
forall id gd id',
IS.In id w -> ~
List.In id (
w_todo w) ->
pm!
id =
Some gd ->
ref_def gd id' ->
IS.In id'
w.
Definition used_set_closed (
u:
IS.t) :
Prop :=
forall id gd id',
IS.In id u ->
pm!
id =
Some gd ->
ref_def gd id' ->
IS.In id'
u.
Lemma iter_step_invariant:
forall w,
workset_invariant w ->
match iter_step pm w with
|
inl u =>
used_set_closed u
|
inr w' =>
workset_invariant w'
end.
Proof.
Theorem used_globals_sound:
forall u,
used_globals p pm =
Some u ->
used_set_closed u.
Proof.
Theorem used_globals_incl:
forall u,
used_globals p pm =
Some u ->
IS.Subset (
initial_workset p)
u.
Proof.
Corollary used_globals_valid:
forall u,
used_globals p pm =
Some u ->
IS.for_all (
global_defined p pm)
u =
true ->
valid_used_set p u.
Proof.
End ANALYSIS.
Properties of the elimination of unused global definitions.
Section TRANSFORMATION.
Variable p:
program.
Variable used:
IS.t.
Let add_def (
m:
prog_map)
idg :=
PTree.set (
fst idg) (
snd idg)
m.
Remark filter_globdefs_accu:
forall defs accu1 accu2 u,
filter_globdefs u (
accu1 ++
accu2)
defs =
filter_globdefs u accu1 defs ++
accu2.
Proof.
induction defs;
simpl;
intros.
auto.
destruct a as [
id gd].
destruct (
IS.mem id u);
auto.
rewrite <-
IHdefs.
auto.
Qed.
Remark filter_globdefs_nil:
forall u accu defs,
filter_globdefs u accu defs =
filter_globdefs u nil defs ++
accu.
Proof.
Lemma filter_globdefs_map_1:
forall id l u m1,
IS.mem id u =
false ->
m1!
id =
None ->
(
fold_left add_def (
filter_globdefs u nil l)
m1)!
id =
None.
Proof.
Lemma filter_globdefs_map_2:
forall id l u m1 m2,
IS.mem id u =
true ->
m1!
id =
m2!
id ->
(
fold_left add_def (
filter_globdefs u nil l)
m1)!
id = (
fold_left add_def (
List.rev l)
m2)!
id.
Proof.
Lemma filter_globdefs_map:
forall id u defs,
(
PTree_Properties.of_list (
filter_globdefs u nil (
List.rev defs)))!
id =
if IS.mem id u then (
PTree_Properties.of_list defs)!
id else None.
Proof.
Lemma filter_globdefs_domain:
forall id l u,
In id (
map fst (
filter_globdefs u nil l)) ->
IS.In id u /\
In id (
map fst l).
Proof.
induction l as [ | [
id1 gd1]
l];
simpl;
intros.
-
tauto.
-
destruct (
IS.mem id1 u)
eqn:
MEM.
+
rewrite filter_globdefs_nil,
map_app,
in_app_iff in H.
destruct H.
apply IHl in H.
rewrite ISF.remove_iff in H.
tauto.
simpl in H.
destruct H;
try tauto.
subst id1.
split;
auto.
apply IS.mem_2;
auto.
+
apply IHl in H.
tauto.
Qed.
Lemma filter_globdefs_image:
forall id l u,
IS.In id u /\
In id (
map fst l) ->
In id (
map fst (
filter_globdefs u nil l)).
Proof.
Lemma filter_globdefs_unique_names:
forall l u,
list_norepet (
map fst (
filter_globdefs u nil l)).
Proof.
End TRANSFORMATION.
Theorem transf_program_match:
forall p tp,
transform_program p =
OK tp ->
match_prog p tp.
Proof.
Semantic preservation
Section SOUNDNESS.
Variable p:
program.
Variable tp:
program.
Variable kept:
ident ->
bool.
Hypothesis USED_VALID:
valid_used_set p kept.
Hypothesis TRANSF:
match_prog_1 kept p tp.
Let pm :=
prog_defmap p.
Section CORELEMMA.
Variable (
se tse:
Senv.t).
Variable ge tge:
genv.
Hypothesis SECOMPATSRC:
senv_genv_compat se ge.
Hypothesis SECOMPATTGT:
senv_genv_compat tse tge.
Lemma kept_closed:
forall id gd id',
kept id ->
pm!
id =
Some gd ->
ref_def gd id' ->
kept id'.
Proof.
Lemma kept_main:
kept p.(
prog_main).
Proof.
Lemma kept_public:
forall id,
In id p.(
prog_public) ->
kept id.
Proof.
Injections that preserve used globals.
Record meminj_preserves_globals (
f:
meminj) :
Prop := {
symbols_inject_1:
forall id b b'
delta,
f b =
Some(
b',
delta) ->
Genv.find_symbol ge id =
Some b ->
delta = 0 /\
Genv.find_symbol tge id =
Some b';
symbols_inject_2:
forall id b,
kept id ->
Genv.find_symbol ge id =
Some b ->
exists b',
Genv.find_symbol tge id =
Some b' /\
f b =
Some(
b', 0);
symbols_inject_3:
forall id b',
Genv.find_symbol tge id =
Some b' ->
exists b,
Genv.find_symbol ge id =
Some b /\
f b =
Some(
b', 0);
defs_inject:
forall b b'
delta gd,
f b =
Some(
b',
delta) ->
Genv.find_def ge b =
Some gd ->
Genv.find_def tge b' =
Some gd /\
delta = 0 /\
(
forall id,
ref_def gd id ->
kept id);
defs_rev_inject:
forall b b'
delta gd,
f b =
Some(
b',
delta) ->
Genv.find_def tge b' =
Some gd ->
Genv.find_def ge b =
Some gd /\
delta = 0;
public_eq:
Genv.genv_public ge =
prog_public p /\
Genv.genv_public tge =
prog_public tp;
}.
Lemma globals_symbols_inject:
forall j,
meminj_preserves_globals j ->
symbols_inject j ge tge.
Proof.
Lemma symbol_address_inject:
forall j id ofs,
meminj_preserves_globals j ->
kept id ->
Val.inject j (
Genv.symbol_address ge id ofs) (
Genv.symbol_address tge id ofs).
Proof.
Semantic preservation
Definition regset_inject (
f:
meminj) (
rs rs':
regset):
Prop :=
forall r,
Val.inject f rs#
r rs'#
r.
Lemma regs_inject:
forall f rs rs',
regset_inject f rs rs' ->
forall l,
Val.inject_list f rs##
l rs'##
l.
Proof.
induction l; simpl. constructor. constructor; auto.
Qed.
Lemma set_reg_inject:
forall f rs rs'
r v v',
regset_inject f rs rs' ->
Val.inject f v v' ->
regset_inject f (
rs#
r <-
v) (
rs'#
r <-
v').
Proof.
Lemma set_res_inject:
forall f rs rs'
res v v',
regset_inject f rs rs' ->
Val.inject f v v' ->
regset_inject f (
regmap_setres res v rs) (
regmap_setres res v'
rs').
Proof.
Lemma regset_inject_incr:
forall f f'
rs rs',
regset_inject f rs rs' ->
inject_incr f f' ->
regset_inject f'
rs rs'.
Proof.
Lemma regset_undef_inject:
forall f,
regset_inject f (
Regmap.init Vundef) (
Regmap.init Vundef).
Proof.
intros;
red;
intros.
rewrite Regmap.gi.
auto.
Qed.
Lemma init_regs_inject:
forall f args args',
Val.inject_list f args args' ->
forall params,
regset_inject f (
init_regs args params) (
init_regs args'
params).
Proof.
Inductive match_stacks (
j:
meminj):
list stackframe ->
list stackframe ->
block ->
block ->
Prop :=
|
match_stacks_nil:
forall bound tbound,
forall (
SYMBINJ:
symbols_inject j se tse),
meminj_preserves_globals j ->
Ple (
Genv.genv_next ge)
bound ->
Ple (
Genv.genv_next tge)
tbound ->
match_stacks j nil nil bound tbound
|
match_stacks_cons:
forall res f sp pc rs s tsp trs ts bound tbound
(
STACKS:
match_stacks j s ts sp tsp)
(
KEPT:
forall id,
ref_function f id ->
kept id)
(
SPINJ:
j sp =
Some(
tsp, 0))
(
REGINJ:
regset_inject j rs trs)
(
BELOW:
Plt sp bound)
(
TBELOW:
Plt tsp tbound),
match_stacks j (
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
s)
(
Stackframe res f (
Vptr tsp Ptrofs.zero)
pc trs ::
ts)
bound tbound.
Lemma match_stacks_symbols_inject:
forall j s ts bound tbound,
match_stacks j s ts bound tbound ->
symbols_inject j se tse.
Proof.
induction 1; auto. Qed.
Lemma match_stacks_preserves_globals:
forall j s ts bound tbound,
match_stacks j s ts bound tbound ->
meminj_preserves_globals j.
Proof.
induction 1; auto.
Qed.
Lemma match_stacks_incr:
forall j j',
inject_incr j j' ->
forall s ts bound tbound,
match_stacks j s ts bound tbound ->
(
forall b1 b2 delta,
j b1 =
None ->
j'
b1 =
Some(
b2,
delta) ->
Ple bound b1 /\
Ple tbound b2) ->
match_stacks j'
s ts bound tbound.
Proof.
Lemma match_stacks_bound:
forall j s ts bound tbound bound'
tbound',
match_stacks j s ts bound tbound ->
Ple bound bound' ->
Ple tbound tbound' ->
match_stacks j s ts bound'
tbound'.
Proof.
Inductive match_states:
state ->
state ->
SimMemInj.t' ->
Prop :=
|
match_states_regular:
forall s f sp pc rs m ts tsp trs tm j
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m tm j)
(
MWF:
SimMemInj.wf'
sm0)
(
STACKS:
match_stacks j s ts sp tsp)
(
KEPT:
forall id,
ref_function f id ->
kept id)
(
SPINJ:
j sp =
Some(
tsp, 0))
(
REGINJ:
regset_inject j rs trs)
(
MEMINJ:
Mem.inject j m tm),
match_states (
State s f (
Vptr sp Ptrofs.zero)
pc rs m)
(
State ts f (
Vptr tsp Ptrofs.zero)
pc trs tm)
sm0
|
match_states_call:
forall s fptr sg args m ts tfptr targs tm j
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m tm j)
(
MWF:
SimMemInj.wf'
sm0)
(
STACKS:
match_stacks j s ts (
Mem.nextblock m) (
Mem.nextblock tm))
(
FPTR:
Val.inject j fptr tfptr)
(
ARGINJ:
Val.inject_list j args targs)
(
MEMINJ:
Mem.inject j m tm),
match_states (
Callstate s fptr sg args m)
(
Callstate ts tfptr sg targs tm)
sm0
|
match_states_return:
forall s res m ts tres tm j
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m tm j)
(
MWF:
SimMemInj.wf'
sm0)
(
STACKS:
match_stacks j s ts (
Mem.nextblock m) (
Mem.nextblock tm))
(
RESINJ:
Val.inject j res tres)
(
MEMINJ:
Mem.inject j m tm),
match_states (
Returnstate s res m)
(
Returnstate ts tres tm)
sm0.
Lemma external_call_inject:
forall ef vargs m1 t vres m2 f m1'
vargs' (
SYMBINJ:
symbols_inject f se tse),
external_call ef se vargs m1 t vres m2 ->
Mem.inject f m1 m1' ->
Val.inject_list f vargs vargs' ->
exists f',
exists vres',
exists m2',
external_call ef tse vargs'
m1'
t vres'
m2'
/\
Val.inject f'
vres vres'
/\
Mem.inject f'
m2 m2'
/\
Mem.unchanged_on (
loc_unmapped f)
m1 m2
/\
Mem.unchanged_on (
loc_out_of_reach f m1)
m1'
m2'
/\
inject_incr f f'
/\
inject_separated f f'
m1 m1'.
Proof.
Lemma find_function_inject:
forall j ros rs fptr trs,
meminj_preserves_globals j ->
find_function_ptr ge ros rs =
fptr ->
match ros with inl r =>
regset_inject j rs trs |
inr id =>
kept id end ->
exists tfptr,
find_function_ptr tge ros trs =
tfptr /\
Val.inject j fptr tfptr.
Proof.
Lemma eval_builtin_arg_inject:
forall rs sp m j rs'
sp'
m'
a v,
eval_builtin_arg ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m a v ->
j sp =
Some(
sp', 0) ->
meminj_preserves_globals j ->
regset_inject j rs rs' ->
Mem.inject j m m' ->
(
forall id,
In id (
globals_of_builtin_arg a) ->
kept id) ->
exists v',
eval_builtin_arg tge (
fun r =>
rs'#
r) (
Vptr sp'
Ptrofs.zero)
m'
a v'
/\
Val.inject j v v'.
Proof.
Lemma eval_builtin_args_inject:
forall rs sp m j rs'
sp'
m'
al vl,
eval_builtin_args ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m al vl ->
j sp =
Some(
sp', 0) ->
meminj_preserves_globals j ->
regset_inject j rs rs' ->
Mem.inject j m m' ->
(
forall id,
In id (
globals_of_builtin_args al) ->
kept id) ->
exists vl',
eval_builtin_args tge (
fun r =>
rs'#
r) (
Vptr sp'
Ptrofs.zero)
m'
al vl'
/\
Val.inject_list j vl vl'.
Proof.
induction 1;
intros.
-
exists (@
nil val);
split;
constructor.
-
simpl in H5.
exploit eval_builtin_arg_inject;
eauto using in_or_app.
intros (
v1' &
A &
B).
destruct IHlist_forall2 as (
vl' &
C &
D);
eauto using in_or_app.
exists (
v1' ::
vl');
split;
constructor;
auto.
Qed.
Theorem step_simulation:
forall S1 t S2,
step se ge S1 t S2 ->
forall S1'
sm0 (
MS:
match_states S1 S1'
sm0),
exists S2',
step tse tge S1'
t S2' /\ (
exists sm1,
match_states S2 S2'
sm1 /\ <<
MLE:
SimMemInj.le'
sm0 sm1>>).
Proof.
End CORELEMMA.
Section WHOLE.
Let ge :=
Genv.globalenv p.
Let tge :=
Genv.globalenv tp.
Relating Genv.find_symbol operations in the original and transformed program
Lemma transform_find_symbol_1:
forall id b,
Genv.find_symbol ge id =
Some b ->
kept id ->
exists b',
Genv.find_symbol tge id =
Some b'.
Proof.
Lemma transform_find_symbol_2:
forall id b,
Genv.find_symbol tge id =
Some b ->
kept id /\
exists b',
Genv.find_symbol ge id =
Some b'.
Proof.
Definition init_meminj :
meminj :=
fun b =>
match Genv.invert_symbol ge b with
|
Some id =>
match Genv.find_symbol tge id with
|
Some b' =>
Some (
b', 0)
|
None =>
None
end
|
None =>
None
end.
Remark init_meminj_eq:
forall id b b',
Genv.find_symbol ge id =
Some b ->
Genv.find_symbol tge id =
Some b' ->
init_meminj b =
Some(
b', 0).
Proof.
Remark init_meminj_invert:
forall b b'
delta,
init_meminj b =
Some(
b',
delta) ->
delta = 0 /\
exists id,
Genv.find_symbol ge id =
Some b /\
Genv.find_symbol tge id =
Some b'.
Proof.
Lemma init_meminj_preserves_globals:
meminj_preserves_globals ge tge init_meminj.
Proof.
Relating initial memory states
Lemma init_meminj_invert_strong:
forall b b'
delta,
init_meminj b =
Some(
b',
delta) ->
delta = 0 /\
exists id gd,
Genv.find_symbol ge id =
Some b
/\
Genv.find_symbol tge id =
Some b'
/\
Genv.find_def ge b =
Some gd
/\
Genv.find_def tge b' =
Some gd
/\ (
forall i,
ref_def gd i ->
kept i).
Proof.
Section INIT_MEM.
Variables m tm:
mem.
Hypothesis IM:
Genv.init_mem p =
Some m.
Hypothesis TIM:
Genv.init_mem tp =
Some tm.
Lemma bytes_of_init_inject:
forall il,
(
forall id,
ref_init il id ->
kept id) ->
list_forall2 (
memval_inject init_meminj) (
Genv.bytes_of_init_data_list ge il) (
Genv.bytes_of_init_data_list tge il).
Proof.
Lemma Mem_getN_forall2:
forall (
P:
memval ->
memval ->
Prop)
c1 c2 i n p,
list_forall2 P (
Mem.getN n p c1) (
Mem.getN n p c2) ->
p <=
i ->
i <
p +
Z.of_nat n ->
P (
ZMap.get i c1) (
ZMap.get i c2).
Proof.
induction n;
simpl Mem.getN;
intros.
-
simpl in H1.
omegaContradiction.
-
inv H.
rewrite Nat2Z.inj_succ in H1.
destruct (
zeq i p0).
+
congruence.
+
apply IHn with (
p0 + 1);
auto.
omega.
omega.
Qed.
Lemma init_mem_inj_1:
Mem.mem_inj init_meminj m tm.
Proof.
Lemma init_mem_inj_2:
Mem.inject init_meminj m tm.
Proof.
End INIT_MEM.
Lemma init_mem_exists:
forall m,
Genv.init_mem p =
Some m ->
exists tm,
Genv.init_mem tp =
Some tm.
Proof.
Theorem init_mem_inject:
forall m,
Genv.init_mem p =
Some m ->
exists f tm,
Genv.init_mem tp =
Some tm /\
Mem.inject f m tm /\
meminj_preserves_globals ge tge f.
Proof.
Lemma transf_initial_states:
forall S1,
initial_state p S1 ->
exists S2,
initial_state tp S2 /\
exists sm,
match_states ge tge ge tge S1 S2 sm.
Proof.
Lemma transf_final_states:
forall S1 S2 r,
(
exists sm,
match_states ge tge ge tge S1 S2 sm) ->
final_state S1 r ->
final_state S2 r.
Proof.
intros. des. inv H0. inv H. inv STACKS. inv RESINJ. constructor.
Qed.
Lemma transf_program_correct_1:
forward_simulation (
semantics p) (
semantics tp).
Proof.
End WHOLE.
End SOUNDNESS.
Theorem transf_program_correct:
forall p tp,
match_prog_weak p tp ->
forward_simulation (
semantics p) (
semantics tp).
Proof.
Commutation with linking
Remark link_def_either:
forall (
gd1 gd2 gd:
globdef fundef unit),
link_def gd1 gd2 =
Some gd ->
gd =
gd1 \/
gd =
gd2.
Proof with
(
try discriminate).
intros until gd.
Local Transparent Linker_def Linker_fundef Linker_varinit Linker_vardef Linker_unit.
destruct gd1 as [
f1|
v1],
gd2 as [
f2|
v2]...
destruct f1 as [
f1|
ef1],
f2 as [
f2|
ef2];
simpl...
destruct ef2;
intuition congruence.
destruct ef1;
intuition congruence.
des_ifs;
intuition congruence.
simpl.
unfold link_vardef.
destruct v1 as [
info1 init1 ro1 vo1],
v2 as [
info2 init2 ro2 vo2];
simpl.
destruct (
link_varinit init1 init2)
as [
init|]
eqn:
LI...
destruct (
eqb ro1 ro2)
eqn:
RO...
destruct (
eqb vo1 vo2)
eqn:
VO...
simpl.
destruct info1,
info2.
assert (
EITHER:
init =
init1 \/
init =
init2).
{
revert LI.
unfold link_varinit.
destruct (
classify_init init1), (
classify_init init2);
intro EQ;
inv EQ;
auto.
destruct (
zeq sz (
Z.max sz0 0 + 0));
inv H0;
auto.
destruct (
zeq sz (
init_data_list_size il));
inv H0;
auto.
destruct (
zeq sz (
init_data_list_size il));
inv H0;
auto. }
apply eqb_prop in RO.
apply eqb_prop in VO.
intro EQ;
inv EQ.
destruct EITHER;
subst init;
auto.
Qed.
Remark used_not_defined:
forall p used id,
valid_used_set p used ->
(
prog_defmap p)!
id =
None ->
used id =
false \/
id =
prog_main p.
Proof.
Remark used_not_defined_2:
forall p used id,
valid_used_set p used ->
id <>
prog_main p ->
(
prog_defmap p)!
id =
None ->
~
used id.
Proof.
intros.
exploit used_not_defined;
eauto.
intros [
A|
A].
congruence.
congruence.
Qed.
Lemma link_valid_used_set:
forall p1 p2 p used1 used2,
link p1 p2 =
Some p ->
valid_used_set p1 used1 ->
valid_used_set p2 used2 ->
valid_used_set p (
fun id =>
used1 id ||
used2 id).
Proof.
Theorem link_match_program:
forall p1 p2 tp1 tp2 p,
link p1 p2 =
Some p ->
match_prog_weak p1 tp1 ->
match_prog_weak p2 tp2 ->
exists tp,
link tp1 tp2 =
Some tp /\
match_prog_weak p tp.
Proof.
intros.
destruct H0 as (
used1 &
A1 &
B1).
destruct H1 as (
used2 &
A2 &
B2).
destruct (
link_prog_inv _ _ _ H)
as (
U &
V &
W).
econstructor;
split.
-
apply link_prog_succeeds.
+
rewrite (
match_prog_main _ _ _ B1), (
match_prog_main _ _ _ B2).
auto.
+
intros.
rewrite (
match_prog_def _ _ _ B1)
in H0.
rewrite (
match_prog_def _ _ _ B2)
in H1.
destruct (
used1 id)
eqn:
U1;
try discriminate.
destruct (
used2 id)
eqn:
U2;
try discriminate.
edestruct V as (
X &
Y &
gd &
Z);
eauto.
split.
rewrite (
match_prog_public _ _ _ B1);
auto.
split.
rewrite (
match_prog_public _ _ _ B2);
auto.
congruence.
-
exists (
fun id =>
used1 id ||
used2 id);
split.
+
eapply link_valid_used_set;
eauto.
+
rewrite W.
constructor;
simpl;
intros.
*
eapply match_prog_main;
eauto.
*
rewrite (
match_prog_public _ _ _ B1), (
match_prog_public _ _ _ B2).
auto.
*
rewrite !
prog_defmap_elements, !
PTree.gcombine by auto.
rewrite (
match_prog_def _ _ _ B1 id), (
match_prog_def _ _ _ B2 id).
{
destruct (
prog_defmap p1)!
id as [
gd1|]
eqn:
GD1;
destruct (
prog_defmap p2)!
id as [
gd2|]
eqn:
GD2.
-
exploit V;
eauto.
intros (
PUB1 &
PUB2 &
_).
assert (
EQ1:
used1 id =
true)
by (
eapply used_public;
eauto).
assert (
EQ2:
used2 id =
true)
by (
eapply used_public;
eauto).
rewrite EQ1,
EQ2;
auto.
-
exploit used_not_defined;
try apply GD2;
eauto.
intros [
A|
A].
rewrite A,
orb_false_r.
destruct (
used1 id);
auto.
replace (
used1 id)
with true.
destruct (
used2 id);
auto.
symmetry.
rewrite A, <-
U.
eapply used_main;
eauto.
-
exploit used_not_defined.
eexact A1.
eauto.
intros [
A|
A].
rewrite A,
orb_false_l.
destruct (
used2 id);
auto.
replace (
used2 id)
with true.
destruct (
used1 id);
auto.
symmetry.
rewrite A,
U.
eapply used_main;
eauto.
-
destruct (
used1 id), (
used2 id);
auto.
}
*
intros.
apply PTree.elements_keys_norepet.
Qed.
Instance TransfSelectionLink :
TransfLink match_prog_weak :=
link_match_program.