Correctness proof for the Debugvar pass.
Require Import Axioms Coqlib Maps Iteration Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Machregs Locations Conventions Op Linear.
Require Import Debugvar.
Relational characterization of the transformation
Definition match_prog (
p tp:
program) :=
match_program (
fun _ f tf =>
transf_fundef f =
OK tf)
eq p tp.
Lemma transf_program_match:
forall p tp,
transf_program p =
OK tp ->
match_prog p tp.
Proof.
Inductive match_code:
code ->
code ->
Prop :=
|
match_code_nil:
match_code nil nil
|
match_code_cons:
forall i before after c c',
match_code c c' ->
match_code (
i ::
c) (
i ::
add_delta_ranges before after c').
Remark diff_same:
forall s,
diff s s =
nil.
Proof.
Remark delta_state_same:
forall s,
delta_state s s = (
nil,
nil).
Proof.
destruct s;
simpl.
rewrite !
diff_same;
auto.
auto.
Qed.
Lemma transf_code_match:
forall lm c before,
match_code c (
transf_code lm before c).
Proof.
Inductive match_function:
function ->
function ->
Prop :=
|
match_function_intro:
forall f c,
match_code f.(
fn_code)
c ->
match_function f (
mkfunction f.(
fn_sig)
f.(
fn_stacksize)
c).
Lemma transf_function_match:
forall f tf,
transf_function f =
OK tf ->
match_function f tf.
Proof.
Remark find_label_add_delta_ranges:
forall lbl c before after,
find_label lbl (
add_delta_ranges before after c) =
find_label lbl c.
Proof.
intros.
unfold add_delta_ranges.
destruct (
delta_state before after)
as [
killed born].
induction killed as [ | [
v i]
l];
simpl;
auto.
induction born as [ | [
v i]
l];
simpl;
auto.
Qed.
Lemma find_label_match_rec:
forall lbl c'
c tc,
match_code c tc ->
find_label lbl c =
Some c' ->
exists before after tc',
find_label lbl tc =
Some (
add_delta_ranges before after tc') /\
match_code c'
tc'.
Proof.
induction 1;
simpl;
intros.
-
discriminate.
-
destruct (
is_label lbl i).
inv H0.
econstructor;
econstructor;
econstructor;
eauto.
rewrite find_label_add_delta_ranges.
auto.
Qed.
Lemma find_label_match:
forall f tf lbl c,
match_function f tf ->
find_label lbl f.(
fn_code) =
Some c ->
exists before after tc,
find_label lbl tf.(
fn_code) =
Some (
add_delta_ranges before after tc) /\
match_code c tc.
Proof.
Properties of availability sets
These properties are not used in the semantic preservation proof,
but establish some confidence in the availability analysis.
Definition avail_above (
v:
ident) (
s:
avail) :
Prop :=
forall v'
i',
In (
v',
i')
s ->
Plt v v'.
Inductive wf_avail:
avail ->
Prop :=
|
wf_avail_nil:
wf_avail nil
|
wf_avail_cons:
forall v i s,
avail_above v s ->
wf_avail s ->
wf_avail ((
v,
i) ::
s).
Lemma set_state_1:
forall v i s,
In (
v,
i) (
set_state v i s).
Proof.
induction s as [ | [
v'
i']
s];
simpl.
-
auto.
-
destruct (
Pos.compare v v');
simpl;
auto.
Qed.
Lemma set_state_2:
forall v i v'
i'
s,
v' <>
v ->
In (
v',
i')
s ->
In (
v',
i') (
set_state v i s).
Proof.
induction s as [ | [
v1 i1]
s];
simpl;
intros.
-
contradiction.
-
destruct (
Pos.compare_spec v v1);
simpl.
+
subst v1.
destruct H0.
congruence.
auto.
+
auto.
+
destruct H0;
auto.
Qed.
Lemma set_state_3:
forall v i v'
i'
s,
wf_avail s ->
In (
v',
i') (
set_state v i s) ->
(
v' =
v /\
i' =
i) \/ (
v' <>
v /\
In (
v',
i')
s).
Proof.
induction 1;
simpl;
intros.
-
intuition congruence.
-
destruct (
Pos.compare_spec v v0);
simpl in H1.
+
subst v0.
destruct H1.
inv H1;
auto.
right;
split.
apply sym_not_equal.
apply Plt_ne.
eapply H;
eauto.
auto.
+
destruct H1.
inv H1;
auto.
destruct H1.
inv H1.
right;
split;
auto.
apply sym_not_equal.
apply Plt_ne.
auto.
right;
split;
auto.
apply sym_not_equal.
apply Plt_ne.
apply Plt_trans with v0;
eauto.
+
destruct H1.
inv H1.
right;
split;
auto.
apply Plt_ne.
auto.
destruct IHwf_avail as [
A | [
A B]];
auto.
Qed.
Lemma wf_set_state:
forall v i s,
wf_avail s ->
wf_avail (
set_state v i s).
Proof.
induction 1;
simpl.
-
constructor.
red;
simpl;
tauto.
constructor.
-
destruct (
Pos.compare_spec v v0).
+
subst v0.
constructor;
auto.
+
constructor.
red;
simpl;
intros.
destruct H2.
inv H2.
auto.
apply Plt_trans with v0;
eauto.
constructor;
auto.
+
constructor.
red;
intros.
exploit set_state_3.
eexact H0.
eauto.
intros [[
A B] | [
A B]];
subst;
eauto.
auto.
Qed.
Lemma remove_state_1:
forall v i s,
wf_avail s -> ~
In (
v,
i) (
remove_state v s).
Proof.
Lemma remove_state_2:
forall v v'
i'
s,
v' <>
v ->
In (
v',
i')
s ->
In (
v',
i') (
remove_state v s).
Proof.
induction s as [ | [
v1 i1]
s];
simpl;
intros.
-
auto.
-
destruct (
Pos.compare_spec v v1);
simpl.
+
subst v1.
destruct H0.
congruence.
auto.
+
auto.
+
destruct H0;
auto.
Qed.
Lemma remove_state_3:
forall v v'
i'
s,
wf_avail s ->
In (
v',
i') (
remove_state v s) ->
v' <>
v /\
In (
v',
i')
s.
Proof.
Lemma wf_remove_state:
forall v s,
wf_avail s ->
wf_avail (
remove_state v s).
Proof.
induction 1;
simpl.
-
constructor.
-
destruct (
Pos.compare_spec v v0).
+
auto.
+
constructor;
auto.
+
constructor;
auto.
red;
intros.
exploit remove_state_3.
eexact H0.
eauto.
intros [
A B].
eauto.
Qed.
Lemma wf_filter:
forall pred s,
wf_avail s ->
wf_avail (
List.filter pred s).
Proof.
induction 1;
simpl.
-
constructor.
-
destruct (
pred (
v,
i))
eqn:
P;
auto.
constructor;
auto.
red;
intros.
apply filter_In in H1.
destruct H1.
eauto.
Qed.
Lemma join_1:
forall v i s1,
wf_avail s1 ->
forall s2,
wf_avail s2 ->
In (
v,
i)
s1 ->
In (
v,
i)
s2 ->
In (
v,
i) (
join s1 s2).
Proof.
induction 1;
simpl;
try tauto;
induction 1;
simpl;
intros I1 I2;
auto.
destruct I1,
I2.
-
inv H3;
inv H4.
rewrite Pos.compare_refl.
rewrite dec_eq_true;
auto with coqlib.
-
inv H3.
assert (
L:
Plt v1 v)
by eauto.
apply Pos.compare_gt_iff in L.
rewrite L.
auto.
-
inv H4.
assert (
L:
Plt v0 v)
by eauto.
apply Pos.compare_lt_iff in L.
rewrite L.
apply IHwf_avail.
constructor;
auto.
auto.
auto with coqlib.
-
destruct (
Pos.compare v0 v1).
+
destruct (
eq_debuginfo i0 i1);
auto with coqlib.
+
apply IHwf_avail;
auto with coqlib.
constructor;
auto.
+
eauto.
Qed.
Lemma join_2:
forall v i s1,
wf_avail s1 ->
forall s2,
wf_avail s2 ->
In (
v,
i) (
join s1 s2) ->
In (
v,
i)
s1 /\
In (
v,
i)
s2.
Proof.
induction 1;
simpl;
try tauto;
induction 1;
simpl;
intros I;
try tauto.
destruct (
Pos.compare_spec v0 v1).
-
subst v1.
destruct (
eq_debuginfo i0 i1).
+
subst i1.
destruct I.
auto.
exploit IHwf_avail;
eauto.
tauto.
+
exploit IHwf_avail;
eauto.
tauto.
-
exploit (
IHwf_avail ((
v1,
i1) ::
s0));
eauto.
constructor;
auto.
simpl.
tauto.
-
exploit IHwf_avail0;
eauto.
tauto.
Qed.
Lemma wf_join:
forall s1,
wf_avail s1 ->
forall s2,
wf_avail s2 ->
wf_avail (
join s1 s2).
Proof.
induction 1;
simpl;
induction 1;
simpl;
try constructor.
destruct (
Pos.compare_spec v v0).
-
subst v0.
destruct (
eq_debuginfo i i0);
auto.
constructor;
auto.
red;
intros.
apply join_2 in H3;
auto.
destruct H3.
eauto.
-
apply IHwf_avail.
constructor;
auto.
-
apply IHwf_avail0.
Qed.
Semantic preservation
Section PRESERVATION.
Context `{
external_calls_prf:
ExternalCalls}.
Variable fn_stack_requirements:
ident ->
Z.
Variable prog:
program.
Variable tprog:
program.
Hypothesis TRANSF:
match_prog prog tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_match TRANSF).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_match TRANSF).
Lemma genv_next_preserved:
Genv.genv_next tge =
Genv.genv_next ge.
Proof.
Lemma functions_translated:
forall (
v:
val) (
f:
fundef),
Genv.find_funct ge v =
Some f ->
exists tf,
Genv.find_funct tge v =
Some tf /\
transf_fundef f =
OK tf.
Proof (
Genv.find_funct_transf_partial TRANSF).
Lemma function_ptr_translated:
forall (
b:
block) (
f:
fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
transf_fundef f =
OK tf.
Proof (
Genv.find_funct_ptr_transf_partial TRANSF).
Lemma sig_preserved:
forall f tf,
transf_fundef f =
OK tf ->
funsig tf =
funsig f.
Proof.
Lemma find_function_translated:
forall ros ls f,
find_function ge ros ls =
Some f ->
exists tf,
find_function tge ros ls =
Some tf /\
transf_fundef f =
OK tf.
Proof.
Evaluation of the debug annotations introduced by the transformation.
Lemma can_eval_safe_arg:
forall (
rs:
locset)
sp m (
a:
builtin_arg loc),
safe_builtin_arg a ->
exists v,
eval_builtin_arg tge rs sp m a v.
Proof.
induction a;
simpl;
intros;
try contradiction;
try (
econstructor;
now eauto with barg).
destruct H as [
S1 S2].
destruct (
IHa1 S1)
as [
v1 E1].
destruct (
IHa2 S2)
as [
v2 E2].
exists (
Val.longofwords v1 v2);
auto with barg.
Qed.
Section WITHINITLS.
Variable init_ls:
locset.
Lemma eval_add_delta_ranges:
forall s f sp c rs m before after,
star (
step fn_stack_requirements init_ls)
tge (
State s f sp (
add_delta_ranges before after c)
rs m)
E0 (
State s f sp c rs m).
Proof.
intros.
unfold add_delta_ranges.
destruct (
delta_state before after)
as [
killed born].
induction killed as [ | [
v i]
l];
simpl.
-
induction born as [ | [
v i]
l];
simpl.
+
apply star_refl.
+
destruct i as [
a SAFE];
simpl.
exploit can_eval_safe_arg;
eauto.
intros [
v1 E1].
eapply star_step;
eauto.
econstructor.
constructor.
eexact E1.
constructor.
simpl;
constructor.
apply Mem.unrecord_push.
simpl;
auto.
auto.
traceEq.
-
eapply star_step;
eauto.
econstructor.
constructor.
simpl;
constructor.
apply Mem.unrecord_push.
simpl;
auto.
auto.
traceEq.
Qed.
Matching between program states.
Inductive match_stackframes:
Linear.stackframe ->
Linear.stackframe ->
Prop :=
|
match_stackframe_intro:
forall f sp rs c tf tc before after,
match_function f tf ->
match_code c tc ->
match_stackframes
(
Stackframe f sp rs c)
(
Stackframe tf sp rs (
add_delta_ranges before after tc)).
Inductive match_states:
Linear.state ->
Linear.state ->
Prop :=
|
match_states_instr:
forall s f sp c rs m tf ts tc
(
STACKS:
list_forall2 match_stackframes s ts)
(
TRF:
match_function f tf)
(
TRC:
match_code c tc),
match_states (
State s f sp c rs m)
(
State ts tf sp tc rs m)
|
match_states_call:
forall s f rs m tf ts sz,
list_forall2 match_stackframes s ts ->
transf_fundef f =
OK tf ->
match_states (
Callstate s f rs m sz)
(
Callstate ts tf rs m sz)
|
match_states_return:
forall s rs m ts,
list_forall2 match_stackframes s ts ->
match_states (
Returnstate s rs m)
(
Returnstate ts rs m).
Lemma parent_locset_match:
forall s ts,
list_forall2 match_stackframes s ts ->
parent_locset init_ls ts =
parent_locset init_ls s.
Proof.
induction 1; simpl. auto. inv H; auto.
Qed.
Lemma ros_is_function_translated:
forall ros rs i,
ros_is_function ge ros rs i ->
ros_is_function tge ros rs i.
Proof.
The simulation diagram.
Theorem transf_step_correct:
forall s1 t s2,
step fn_stack_requirements init_ls ge s1 t s2 ->
forall ts1 (
MS:
match_states s1 ts1),
exists ts2,
plus (
step fn_stack_requirements init_ls)
tge ts1 t ts2 /\
match_states s2 ts2.
Proof.
End WITHINITLS.
Lemma transf_initial_states:
forall st1,
initial_state fn_stack_requirements prog st1 ->
exists st2,
initial_state fn_stack_requirements tprog st2 /\
match_states st1 st2.
Proof.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 ->
final_state st1 r ->
final_state st2 r.
Proof.
intros. inv H0. inv H. inv H5. econstructor; eauto.
Qed.
Theorem transf_program_correct:
forward_simulation (
semantics fn_stack_requirements prog) (
semantics fn_stack_requirements tprog).
Proof.
End PRESERVATION.