Abstract specification of CFG generation
In this module, we define inductive predicates that specify the
translations from Cminor to CFG performed by the functions in module
CFGgen. We then show that these functions satisfy these relational
specifications. The relational specifications will then be used
instead of the actual functions to show semantic equivalence between
the source Cminor code and the the generated CFG code
(see module CFGgenproof).
Require Import Coqlib.
Require Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Globalenvs.
Require Import Switch.
Require Import Cminor.
Require Import CFG.
Require Import CFGgen.
Reasoning about monadic computations
The tactics below simplify hypotheses of the form f ... = OK x s i
where f is a monadic computation. For instance, the hypothesis
(do x <- a; b) s = OK y s' i will generate the additional witnesses
x, s1, i1, i' and the additional hypotheses
a s = OK x s1 i1 and b x s1 = OK y s' i', reflecting the fact that
both monadic computations a and b succeeded.
Remark bind_inversion:
forall (
A B:
Type) (
f:
mon A) (
g:
A ->
mon B)
(
y:
B) (
s1 s3:
state) (
i:
state_incr s1 s3),
bind f g s1 =
OK y s3 i ->
exists x,
exists s2,
exists i1,
exists i2,
f s1 =
OK x s2 i1 /\
g x s2 =
OK y s3 i2.
Proof.
intros until i. unfold bind. destruct (f s1); intros.
discriminate.
exists a; exists s'; exists s.
destruct (g a s'); inv H.
exists s0; auto.
Qed.
Remark bind2_inversion:
forall (
A B C:
Type) (
f:
mon (
A*
B)) (
g:
A ->
B ->
mon C)
(
z:
C) (
s1 s3:
state) (
i:
state_incr s1 s3),
bind2 f g s1 =
OK z s3 i ->
exists x,
exists y,
exists s2,
exists i1,
exists i2,
f s1 =
OK (
x,
y)
s2 i1 /\
g x y s2 =
OK z s3 i2.
Proof.
unfold bind2;
intros.
exploit bind_inversion;
eauto.
intros [[
x y] [
s2 [
i1 [
i2 [
P Q]]]]].
simpl in Q.
exists x;
exists y;
exists s2;
exists i1;
exists i2;
auto.
Qed.
Ltac monadInv1 H :=
match type of H with
| (
OK _ _ _ =
OK _ _ _) =>
inversion H;
clear H;
try subst
| (
Error _ _ =
OK _ _ _) =>
discriminate
| (
ret _ _ =
OK _ _ _) =>
inversion H;
clear H;
try subst
| (
error _ _ =
OK _ _ _) =>
discriminate
| (
bind ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
let x :=
fresh "
x"
in (
let s :=
fresh "
s"
in (
let i1 :=
fresh "
INCR"
in (
let i2 :=
fresh "
INCR"
in (
let EQ1 :=
fresh "
EQ"
in (
let EQ2 :=
fresh "
EQ"
in (
destruct (
bind_inversion _ _ F G X S S'
I H)
as [
x [
s [
i1 [
i2 [
EQ1 EQ2]]]]];
clear H;
try (
monadInv1 EQ2)))))))
| (
bind2 ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
let x1 :=
fresh "
x"
in (
let x2 :=
fresh "
x"
in (
let s :=
fresh "
s"
in (
let i1 :=
fresh "
INCR"
in (
let i2 :=
fresh "
INCR"
in (
let EQ1 :=
fresh "
EQ"
in (
let EQ2 :=
fresh "
EQ"
in (
destruct (
bind2_inversion _ _ _ F G X S S'
I H)
as [
x1 [
x2 [
s [
i1 [
i2 [
EQ1 EQ2]]]]]];
clear H;
try (
monadInv1 EQ2))))))))
end.
Ltac monadInv H :=
match type of H with
| (
ret _ _ =
OK _ _ _) =>
monadInv1 H
| (
error _ _ =
OK _ _ _) =>
monadInv1 H
| (
bind ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
monadInv1 H
| (
bind2 ?
F ?
G ?
S =
OK ?
X ?
S' ?
I) =>
monadInv1 H
| (?
F _ _ _ _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ =
OK _ _ _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
end.
Monotonicity properties of the state
Hint Resolve state_incr_refl:
rtlg.
Lemma instr_at_incr:
forall s1 s2 n i,
state_incr s1 s2 ->
s1.(
st_code)!
n =
Some i ->
s2.(
st_code)!
n =
Some i.
Proof.
intros. inv H.
destruct (H2 n); congruence.
Qed.
Hint Resolve instr_at_incr:
rtlg.
The following tactic saturates the hypotheses with
state_incr properties that follow by transitivity from
the known hypotheses.
Ltac saturateTrans :=
match goal with
|
H1:
state_incr ?
x ?
y,
H2:
state_incr ?
y ?
z |-
_ =>
match goal with
|
H:
state_incr x z |-
_ =>
fail 1
|
_ =>
let i :=
fresh "
INCR"
in
(
generalize (
state_incr_trans x y z H1 H2);
intro i;
saturateTrans)
end
|
_ =>
idtac
end.
Properties of basic operations over the state
Properties of add_instr.
Lemma add_instr_at:
forall s1 s2 incr i n,
add_instr i s1 =
OK n s2 incr ->
s2.(
st_code)!
n =
Some i.
Proof.
intros.
monadInv H.
simpl.
apply PTree.gss.
Qed.
Hint Resolve add_instr_at:
rtlg.
Properties of update_instr.
Lemma update_instr_at:
forall n i s1 s2 incr u,
update_instr n i s1 =
OK u s2 incr ->
s2.(
st_code)!
n =
Some i.
Proof.
Hint Resolve update_instr_at:
rtlg.
Relational specification of the translation
We now define inductive predicates that characterize the fact that
the control-flow graph produced by compilation of a Cminor function
contains sub-graphs that correspond to the translation of each
Cminor statement in the original code.
Definition tr_cases (
nexits:
list node) (
cases:
table nat) (
ncases:
table node) :
Prop :=
Forall2 (
fun act nact =>
fst act =
fst nact /\
nth_error nexits (
snd act) =
Some (
snd nact)
)
cases ncases.
tr_stmt c stmt ns ncont nexits ngoto holds if the graph c,
starting at node ns, contains instructions that perform the Cminor
statement stmt. These instructions branch to node ncont if
the statement terminates normally, to the n-th node in nexits
if the statement terminates prematurely on a exit n statement,
and to the corresponding node in ngoto if the statement jumps to a
label.
Inductive tr_stmt (
c:
code):
stmt ->
node ->
node ->
list node ->
labelmap ->
Prop :=
|
tr_Sskip:
forall ns nexits ngoto,
tr_stmt c Sskip ns ns nexits ngoto
|
tr_Sassign:
forall v b ns nd nexits ngoto,
c!
ns =
Some (
Iassign v b nd) ->
tr_stmt c (
Sassign v b)
ns nd nexits ngoto
|
tr_Sstore:
forall chunk a b ns nd nexits ngoto,
c!
ns =
Some (
Istore chunk a b nd) ->
tr_stmt c (
Sstore chunk a b)
ns nd nexits ngoto
|
tr_Scall:
forall optid sig b cl ns nd nexits ngoto,
c!
ns =
Some (
Icall optid sig b cl nd) ->
tr_stmt c (
Scall optid sig b cl)
ns nd nexits ngoto
|
tr_Stailcall:
forall sig b cl ns nd nexits ngoto,
c!
ns =
Some (
Itailcall sig b cl) ->
tr_stmt c (
Stailcall sig b cl)
ns nd nexits ngoto
|
tr_Sbuiltin:
forall optid ef al ns nd nexits ngoto,
c!
ns =
Some (
Ibuiltin optid ef al nd) ->
tr_stmt c (
Sbuiltin optid ef al)
ns nd nexits ngoto
|
tr_Sseq:
forall s1 s2 ns nd nexits ngoto n,
tr_stmt c s2 n nd nexits ngoto ->
tr_stmt c s1 ns n nexits ngoto ->
tr_stmt c (
Sseq s1 s2)
ns nd nexits ngoto
|
tr_Sifthenelse:
forall a strue sfalse ns nd nexits ngoto ntrue nfalse,
tr_stmt c strue ntrue nd nexits ngoto ->
tr_stmt c sfalse nfalse nd nexits ngoto ->
c!
ns =
Some (
Iifthenelse a ntrue nfalse) ->
tr_stmt c (
Sifthenelse a strue sfalse)
ns nd nexits ngoto
|
tr_Sloop:
forall sbody ns nd nexits ngoto nloop nend,
tr_stmt c sbody nloop nend nexits ngoto ->
c!
ns =
Some(
Iskip nloop) ->
c!
nend =
Some(
Iskip nloop) ->
tr_stmt c (
Sloop sbody)
ns nd nexits ngoto
|
tr_Sblock:
forall sbody ns nd nexits ngoto,
tr_stmt c sbody ns nd (
nd ::
nexits)
ngoto ->
tr_stmt c (
Sblock sbody)
ns nd nexits ngoto
|
tr_Sexit:
forall n ns nd nexits ngoto,
nth_error nexits n =
Some ns ->
tr_stmt c (
Sexit n)
ns nd nexits ngoto
|
tr_Sswitch:
forall a cases default ns nd nexits ngoto ncases ndefault,
tr_cases nexits cases ncases ->
nth_error nexits default =
Some ndefault ->
c!
ns =
Some (
Iswitch a ncases ndefault) ->
tr_stmt c (
Sswitch a cases default)
ns nd nexits ngoto
|
tr_Sreturn:
forall optexpr ns nd nexits ngoto,
c!
ns =
Some (
Ireturn optexpr) ->
tr_stmt c (
Sreturn optexpr)
ns nd nexits ngoto
|
tr_Slabel:
forall lbl s ns nd nexits ngoto n,
ngoto!
lbl =
Some n ->
c!
n =
Some (
Iskip ns) ->
tr_stmt c s ns nd nexits ngoto ->
tr_stmt c (
Slabel lbl s)
ns nd nexits ngoto
|
tr_Sgoto:
forall lbl ns nd nexits ngoto,
ngoto!
lbl =
Some ns ->
tr_stmt c (
Sgoto lbl)
ns nd nexits ngoto.
tr_function f tf specifies the CFG function tf that
CFGgen.transl_function returns.
Inductive tr_function:
Cminor.function ->
CFG.function ->
Prop :=
|
tr_function_intro:
forall f code nentry nret ngoto,
tr_stmt code f.(
Cminor.fn_body)
nentry nret nil ngoto ->
code!
nret =
Some(
Ireturn None) ->
(
forall lbl n,
ngoto!
lbl =
Some n ->
forall k,
exists stmt,
exists k',
find_label lbl f.(
Cminor.fn_body)
k =
Some (
stmt,
k')) ->
tr_function f (
CFG.mkfunction
f.(
Cminor.fn_sig)
f.(
Cminor.fn_params)
f.(
Cminor.fn_vars)
f.(
Cminor.fn_stackspace)
code
nentry).
Correctness proof of the translation functions
We now show that the translation functions in module CFGgen
satisfy the specifications given above as inductive predicates.
Lemma tr_stmt_incr:
forall s1 s2,
state_incr s1 s2 ->
forall s ns nd nexits ngoto,
tr_stmt s1.(
st_code)
s ns nd nexits ngoto ->
tr_stmt s2.(
st_code)
s ns nd nexits ngoto.
Proof.
intros s1 s2 EXT.
pose (
AT :=
fun pc i =>
instr_at_incr s1 s2 pc i EXT).
induction 1;
econstructor;
eauto.
Qed.
Lemma transl_exit_charact:
forall nexits n s ne s'
incr,
transl_exit nexits n s =
OK ne s'
incr ->
nth_error nexits n =
Some ne /\
s' =
s.
Proof.
intros until incr.
unfold transl_exit.
destruct (
nth_error nexits n);
intro;
monadInv H.
auto.
Qed.
Lemma transl_cases_charact:
forall nexits cases ncases s s'
incr,
transl_cases nexits cases s =
OK ncases s'
incr ->
tr_cases nexits cases ncases /\
s =
s'.
Proof.
induction cases;
intros.
monadInv H.
split.
constructor.
auto.
destruct a.
monadInv H.
exploit transl_exit_charact;
eauto.
intros [
A B].
subst.
exploit IHcases;
eauto.
intros [
C D].
subst.
split.
constructor;
auto.
auto.
Qed.
Lemma transl_stmt_charact:
forall stmt nd nexits ngoto s ns s'
INCR
(
TR:
transl_stmt stmt nd nexits ngoto s =
OK ns s'
INCR),
tr_stmt s'.(
st_code)
stmt ns nd nexits ngoto.
Proof.
induction stmt;
intros;
simpl in TR.
monadInv TR;
constructor.
constructor;
eauto with rtlg.
constructor;
eauto with rtlg.
constructor;
eauto with rtlg.
constructor;
eauto with rtlg.
econstructor;
eauto 4
with rtlg.
monadInv TR;
econstructor.
apply tr_stmt_incr with s0;
auto.
eapply IHstmt2;
eauto with rtlg.
eapply IHstmt1;
eauto with rtlg.
monadInv TR;
saturateTrans;
econstructor;
eauto 4
with rtlg.
apply tr_stmt_incr with s0;
auto.
eapply IHstmt1;
eauto with rtlg.
apply tr_stmt_incr with s1;
auto.
eapply IHstmt2;
eauto with rtlg.
monadInv TR;
saturateTrans;
econstructor.
apply tr_stmt_incr with s1;
auto.
eapply IHstmt;
eauto with rtlg.
eauto with rtlg.
eauto with rtlg.
econstructor.
eapply IHstmt;
eauto with rtlg.
exploit transl_exit_charact;
eauto.
intros [
A B].
econstructor.
eauto.
monadInv TR;
saturateTrans.
exploit transl_cases_charact;
eauto.
intros [
A B].
subst.
econstructor;
eauto with rtlg.
exploit transl_exit_charact;
eauto.
tauto.
econstructor;
eauto with rtlg.
monadInv TR;
saturateTrans.
revert EQ0.
case_eq (
ngoto!
l);
intros;
monadInv EQ0.
revert EQ1.
unfold handle_error.
case_eq (
update_instr n (
Iskip ns)
s0);
intros;
inv EQ1.
econstructor.
eauto.
eauto with rtlg.
eapply tr_stmt_incr with s0;
eauto with rtlg.
revert TR.
case_eq (
ngoto!
l);
intros;
monadInv TR.
econstructor.
auto.
Qed.
Lemma reserve_labels_spec:
forall stmt (
s:
state)
lblmap lbl n,
(
fst (
reserve_labels stmt (
lblmap,
s))) !
lbl =
Some n ->
lblmap !
lbl =
Some n \/
forall k,
exists stmt',
exists k',
find_label lbl stmt k =
Some (
stmt',
k').
Proof.
induction stmt;
try (
left;
now eauto).
simpl.
intros.
destruct (
reserve_labels stmt2 (
lblmap,
s))
as []
_eqn.
edestruct IHstmt1.
eauto.
fold (
fst (
l,
s0))
in H0.
rewrite <-
Heqp in H0.
edestruct IHstmt2;
eauto.
right.
intro.
destruct (
find_label lbl stmt1 (
Kseq stmt2 k)).
destruct p.
eexists.
eexists.
eauto.
eauto.
right.
intro.
specialize (
H0 (
Kseq stmt2 k)).
edestruct H0 as [
stmt' [
k'
A]].
rewrite A.
eexists.
eexists.
eauto.
simpl.
intros.
destruct (
reserve_labels stmt2 (
lblmap,
s))
as []
_eqn.
edestruct IHstmt1.
eauto.
fold (
fst (
l,
s0))
in H0.
rewrite <-
Heqp in H0.
edestruct IHstmt2.
eauto.
eauto.
right.
intro.
destruct (
find_label lbl stmt1 k).
destruct p.
eexists.
eexists.
eauto.
eauto.
right.
intro.
specialize (
H0 k).
edestruct H0 as [
stmt' [
k'
A]].
rewrite A.
eexists.
eexists.
eauto.
simpl.
intros.
edestruct IHstmt;
eauto.
simpl.
intros.
edestruct IHstmt;
eauto.
simpl.
intros.
destruct (
ident_eq lbl l).
right.
eexists.
eexists.
eauto.
destruct (
reserve_labels stmt (
lblmap,
s))
as []
_eqn.
simpl in H.
rewrite PTree.gso in H.
fold (
fst (
l0,
s0))
in H.
rewrite <-
Heqp in H.
edestruct IHstmt;
eauto.
eauto.
Qed.
Lemma transl_function_charact:
forall f tf,
transl_function f =
Errors.OK tf ->
tr_function f tf.
Proof.