Correctness of instruction selection
Require Import Coqlib.
Require Import Classical.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Floats.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Cminor.
Require Import CminorP.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.
Require Import Cminorops.
Require Import Selection.
Require Import SelectOpproof.
Require Import Memcomp Traces.
Require Import Simulations MCsimulation.
Require Import Libtactics.
Open Local Scope cminorsel_scope.
Correctness of the instruction selection functions for expressions
Section CMCONSTR.
Variable ge:
genv.
Variable sp:
option pointer.
Variable e:
env.
Conversion of condition expressions.
Hint Constructors eval_condexpr :
myhints.
Hint Constructors eval_exprlist :
myhints.
Lemma negate_condexpr_correct:
forall t a b,
eval_condexpr ge sp e t a b ->
eval_condexpr ge sp e t (
negate_condexpr a) (
negb b).
Proof.
Scheme expr_ind2 :=
Induction for expr Sort Prop
with exprlist_ind2 :=
Induction for exprlist Sort Prop.
Fixpoint forall_exprlist (
P:
expr ->
Prop) (
el:
exprlist) {
struct el}:
Prop :=
match el with
|
Enil =>
True
|
Econs e el' =>
P e /\
forall_exprlist P el'
end.
Lemma expr_induction_principle:
forall (
P:
expr ->
Prop),
(
forall i :
ident,
P (
Evar i)) ->
(
forall (
o :
operation) (
e :
exprlist),
forall_exprlist P e ->
P (
Eop o e)) ->
(
forall (
m :
memory_chunk) (
a :
Op.addressing) (
e :
exprlist),
forall_exprlist P e ->
P (
Eload m a e)) ->
(
forall (
c :
condexpr) (
e :
expr),
P e ->
forall e0 :
expr,
P e0 ->
P (
Econdition c e e0)) ->
(
forall e :
expr,
P e ->
forall e0 :
expr,
P e0 ->
P (
Ediscard e e0)) ->
forall e :
expr,
P e.
Proof.
Lemma eval_base_condition_of_expr:
forall t a v b,
eval_expr ge sp e t a v ->
Val.bool_of_val v b ->
eval_condexpr ge sp e t
(
CEcond (
Ccompimm Cne Int.zero) (
a :::
Enil))
b.
Proof.
Lemma is_compare_neq_zero_correct:
forall c v b,
is_compare_neq_zero c =
true ->
eval_condition c (
v ::
nil) =
Some b ->
Val.bool_of_val v b.
Proof.
Lemma is_compare_eq_zero_correct:
forall c v b,
is_compare_eq_zero c =
true ->
eval_condition c (
v ::
nil) =
Some b ->
Val.bool_of_val v (
negb b).
Proof.
Lemma eval_condition_of_expr:
forall a t v b,
eval_expr ge sp e t a v ->
Val.bool_of_val v b ->
eval_condexpr ge sp e t (
condexpr_of_expr a)
b.
Proof.
Lemma eval_load:
forall t tl a p c v
(
HT :
Val.has_type v (
type_of_chunk c))
(
TT :
t =
tl++((
TEmem(
MEread p c v)) ::
nil)),
eval_expr ge sp e tl a (
Vptr p) ->
eval_expr ge sp e t (
load c a)
v.
Proof.
intros.
generalize H.
unfold load.
unfold addressing.
destruct (
addressing_match a).
-
inversion 1;
inv EVAL;
eauto with evalexpr.
-
intros.
eapply eval_Eload with (
p:=
p);
eauto with evalexpr.
by destruct p;
simpl;
rewrite Int.add_zero.
by rewrite <-
app_nil_end.
Qed.
Lemma cast_and_conv:
forall c v,
(
cast_value_to_chunk c v) = (
cast_value_to_chunk c (
Val.conv v (
type_of_chunk c))).
Proof.
intros [] []; simpl; try done.
Qed.
Lemma eval_store:
forall c a1 a2 p1 v2 k t1 t2 t env
(
TT :
t =
t1++
t2++((
TEmem(
MEwrite p1 c (
cast_value_to_chunk c v2)) ::
nil))),
eval_expr ge sp env t1 a1 (
Vptr p1) ->
eval_expr ge sp env t2 a2 v2 ->
step ge (
SKstmt (
store c a1 a2)
sp env k)
t (
SKstmt Sskip sp env k).
Proof.
Correctness of instruction selection for operators
Hint Resolve eval_cast8unsigned eval_cast8signed
eval_cast16unsigned eval_cast16signed
eval_negint eval_notint eval_notbool
eval_negf eval_singleoffloat
eval_intoffloat eval_intuoffloat
eval_floatofint eval_floatofintu :
evhints.
Hint Constructors Val.bool_of_val :
evhints.
Hint Resolve eval_add eval_add_ptr_2 eval_add_ptr
eval_sub eval_sub_ptr_int eval_sub_ptr_ptr
eval_mul eval_divs eval_divu eval_mods eval_modu
eval_and eval_or eval_xor eval_shl eval_shr eval_shru
eval_addf eval_subf eval_mulf eval_divf
eval_comp_int eval_comp_int_ptr eval_comp_ptr_int
eval_comp_ptr_ptr3 eval_compu eval_compf :
evhints.
Lemma eval_sel_unop:
forall t op a1 v1 v,
eval_expr ge sp e t a1 v1 ->
eval_unop op v1 =
Some v ->
eval_expr ge sp e t (
sel_unop op a1)
v.
Proof.
Lemma eval_sel_binop:
forall t1 t2 op a1 a2 v1 v2 v,
eval_expr ge sp e t1 a1 v1 ->
eval_expr ge sp e t2 a2 v2 ->
eval_binop op v1 v2 =
Some v ->
eval_expr ge sp e (
t1++
t2) (
sel_binop op a1 a2)
v.
Proof.
destruct op;
simpl;
intros;
FuncInv;
clarify;
eauto with evhints;
try generalize (
Int.eq_spec i0 Int.zero);
repeat
(
match goal with
|
H:
context[
match ?
a with true =>
_ |
false =>
_ end] |-
_ =>
destruct a as []
_eqn: ?
|
H:
context[
if ?
a then _ else _] |-
_ =>
destruct a
end;
simpl in *;
clarify;
eauto with evhints).
Qed.
End CMCONSTR.
Semantic preservation for instruction selection.
Section PRESERVATION.
Variable prog:
Cminor.program.
Let tprog :=
sel_program prog.
Variables (
ge :
Cminor.cm_sem.(
SEM_GE)) (
tge :
CminorSel.genv).
Definition genv_rel :
Cminor.cm_sem.(
SEM_GE) ->
CminorSel.genv ->
Prop :=
(
fun x y =>
Genv.genv_match (
fun a b =>
sel_fundef a =
b)
y x).
Hypothesis TRANSF:
genv_rel ge tge.
Relationship between the global environments for the original
CminorSel program and the generated RTL program.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
by intros;
destruct TRANSF. Qed.
Lemma functions_translated:
forall (
v:
val) (
f:
Cminor.fundef),
Genv.find_funct ge v =
Some f ->
Genv.find_funct tge v =
Some (
sel_fundef f).
Proof.
Lemma sig_function_translated:
forall f,
funsig (
sel_fundef f) =
Cminor.funsig f.
Proof.
by destruct f. Qed.
Semantic preservation for expressions.
Hint Resolve eval_sel_unop eval_sel_binop eval_load eval_condition_of_expr :
evalexpr.
Lemma sel_expr_correct:
forall sp e t a v,
CminorP.cmp_eval_expr ge sp e t a v ->
eval_expr tge sp e t (
sel_expr a)
v.
Proof.
induction 1;
intros;
simpl;
clarify;
try destruct b1;
eauto with evalexpr.
destruct cst;
simpl;
simpl in EC; (
econstructor; [
constructor|
simpl;
auto]).
rewrite symbols_preserved.
auto.
Qed.
Hint Resolve sel_expr_correct:
evalexpr.
Lemma sel_exprlist_correct:
forall sp e t a v,
CminorP.cmp_eval_exprlist ge sp e t a v ->
eval_exprlist tge sp e t (
sel_exprlist a)
v.
Proof.
induction 1; intros; simpl; subst; eauto with evalexpr.
Qed.
Hint Resolve sel_exprlist_correct:
evalexpr.
Semantic preservation for terminating function calls and statements.
Fixpoint sel_cont (
k:
Cminor.cont) :
CminorSel.cont :=
match k with
|
Cminor.Kstop =>
Kstop
|
Cminor.Kseq s1 k1 =>
Kseq (
sel_stmt s1) (
sel_cont k1)
|
Cminor.Kblock k1 =>
Kblock (
sel_cont k1)
|
Cminor.Kcall id f sp e k1 =>
Kcall id (
sel_fundef f)
sp e (
sel_cont k1)
end.
Inductive match_states:
Cminor.state ->
CminorSel.state ->
Prop :=
|
match_state:
forall s k s'
k'
sp env,
s' =
sel_stmt s ->
k' =
sel_cont k ->
match_states
(
Cminor.SKstmt s sp env k)
(
SKstmt s'
sp env k')
|
match_callstate:
forall args k k',
k' =
sel_cont k ->
match_states
(
Cminor.SKcall args k)
(
SKcall args k')
|
match_externalstate:
forall efsig k k',
k' =
sel_cont k ->
match_states
(
Cminor.SKexternal efsig k)
(
SKexternal efsig k')
|
match_returnstate:
forall v k k',
k' =
sel_cont k ->
match_states
(
Cminor.SKreturn v k)
(
SKreturn v k').
Remark call_cont_commut:
forall k,
call_cont (
sel_cont k) =
sel_cont (
Cminor.call_cont k).
Proof.
induction k; simpl; auto.
Qed.
Remark find_label_commut:
forall lbl s k,
find_label lbl (
sel_stmt s) (
sel_cont k) =
option_map (
fun sk => (
sel_stmt (
fst sk),
sel_cont (
snd sk)))
(
Cminor.find_label lbl s k).
Proof.
Definition sel_option_fundef (
ofd:
option Cminor.fundef) :
option fundef :=
match ofd with
|
Some fd =>
Some (
sel_fundef fd)
|
None =>
None
end.
Lemma get_fundef_commut:
forall (
k:
Cminor.cont),
(
CminorSel.get_fundef (
sel_cont (
Cminor.call_cont k))
=
sel_option_fundef (
Cminor.get_fundef (
Cminor.call_cont k))).
Proof.
by induction k. Qed.
Hint Constructors match_states.
Lemma sel_aop_correct:
forall aop vargs p rmwi v'
(
AS :
sem_atomic_statement aop vargs =
Some (
p,
rmwi)),
atomic_statement_mem_event (
sel_aop aop)
vargs v'
(
MErmw p Mint32 v'
rmwi).
Proof.
intros.
destruct aop;
destruct vargs as [|[]
vargs];
try done.
do 3 (
destruct vargs;
try done);
simpl in AS.
destruct Val.eq_dec; [
done|].
destruct (
Val.has_type v0 Tint)
as []
_eqn :
HT1; [|
done].
destruct Val.eq_dec; [
done|].
destruct (
Val.has_type v Tint)
as []
_eqn :
HT2; [|
done].
inv AS.
eby econstructor.
destruct vargs; [|
done].
inv AS.
eby econstructor.
Qed.
Lemma sel_step_correct:
forall S1 t S2,
CminorP.cmp_step ge S1 t S2 ->
forall T1,
match_states S1 T1 ->
(
exists T2,
step tge T1 t T2 /\
match_states S2 T2).
Proof.
Gluing the CminorP cmp_step_correct and above sel_step_correct
simulations: forward simulation of compound cm_steps (from clean via
unclean to clean) to CminorSel step.
Definition match_states_clean (
st:
Cminor.state) (
st':
CminorSel.state) :
Prop :=
clean st /\
match_states st st'.
Lemma cmp_step_correct_foo:
forall st1 t st2 st1'
(
VIA:
cm_via_unclean ge st1 t st2)
(
MATCH_CLEAN:
match_states_clean st1 st1'),
(
exists st2',
step tge st1'
t st2' /\
match_states_clean st2 st2').
Proof.
Now we need to build a small-step simulation out of that, from our
original small-step Cminor semantics to a small-step CminorSel
semantics constructed from its trace-set semantics. We do so in
two steps: first lift cmp_step_correct to a simulation between
constructed small-step LTSs (cmp_small_step_correct), and then stick a
simulation from small-step Cminor to constructed small-step Cminor on
the front.
Lemma small_step_cs_intro :
forall s te s',
small_step_Recep CminorSel.state (
step tge)
s te s' ->
small_step_cs tge s te s'.
Proof.
done. Qed.
Hint Resolve small_step_cs_intro.
Lift match_states_clean to a relation between the constructed small-step LTSs
(Cminor.small_step_cm, constructed from Cminor.cm_via_unclean, and
small_step_cs, constructed from CminorSel.step
Inductive match_small_step :
small_step_state Cminor.state ->
small_step_state CminorSel.state ->
Prop :=
|
Match:
forall st st'
t
(
M:
match_states_clean st st'),
match_small_step (
SSState Cminor.state st t) (
SSState CminorSel.state st'
t)
|
MatchStuck:
forall st,
match_small_step (
SSStuck _)
st.
Hint Constructors small_step_Recep.
Hint Constructors match_small_step.
Check that that is a small-step simulation.
Lemma cmp_small_step_correct:
forall st1 st2 st1'
te
(
S:
small_step_cm ge st1 te st2)
(
M:
match_small_step st1 st1'),
(
exists st2',
small_step_cs tge st1'
te st2' /\
match_small_step st2 st2').
Proof.
intros [
st1 t1|] [
st2 t2|] [
st1'
t1'|];
intros;
inv M;
inv S;
try destruct TS as (
stB &
te' &
tb &
X);
exploit cmp_step_correct_foo;
try eassumption;
intros (
stB' & ? & ?);
eauto 10;
assert (
te <>
TEtau)
by (
destruct te;
destruct te0;
clarify);
destruct (
classic (
exists stB,
exists tb,
step tge st1' (
t1' ++
te ::
tb)
stB))
as [(? & [|] & ?)|];
eauto 8.
Qed.
Now that has to be glued onto the CminorP.v cm_small_step_correct.
Inductive match_all :
Cminor.state ->
small_step_state CminorSel.state ->
Prop :=
|
Match_all:
forall st st'
st''
(
M1:
match_cm ge st st')
(
M2:
match_small_step st'
st''),
match_all st st''
|
Match_all_stuck :
forall st st'
(
STUCK:
cm_ev_stuck ge st),
match_all st st'.
Hint Constructors match_all.
Lemma small_step_correct_all:
forall st1 te st2 st1''
(
S:
cm_step ge st1 te st2)
(
M:
match_all st1 st1''),
(
cm_ev_stuck ge st1) \/
(
exists st2'',
( (
te=
TEtau /\
st2''=
st1'' /\ (
measure st2 <
measure st1)%
nat) \/
(
small_step_cs tge st1''
te st2'')) /\
match_all st2 st2'').
Proof.
intros;
inv M;
eauto.
rename st'
into st1'.
exploit cm_small_step_correct;
try eassumption; [].
intros (? & [(? & ? & ?)|?] & [?|?]);
clarify;
eauto 10;
exploit cmp_small_step_correct;
try eassumption;
intros (? & ? & ?);
eauto 10.
Qed.
Let lts :=
mklts thread_labels (
cm_step ge).
Let tlts :=
mklts thread_labels (
small_step_cs tge).
Lemma cm_ev_stuckE :
forall s,
cm_ev_stuck ge s ->
ev_stuck_or_error lts s.
Proof.
induction 1;
vauto.
econstructor 4;
simpl;
eauto.
-
by inv H.
intros [|[]| | | | | |];
try done;
intros;
eauto using te_read_read.
Qed.
Hint Resolve cm_ev_stuckE.
Definition bsim_rel :=
bsr lts tlts match_all.
Definition bsim_order :=
bsc tlts.
Lemma my_backward_sim:
backward_sim lts tlts false bsim_rel bsim_order.
Proof.
Lemma init_sim_succ:
forall {
p vals tinit},
cms_init tge p vals =
Some tinit ->
exists sinit,
cm_init ge p vals =
Some sinit /\
match_all sinit tinit.
Proof.
intros p vals tinit INIT.
unfold cms_init,
cm_init in *.
pose proof TRANSF as (
MG &
MF).
specialize (
MF p).
repeat (
destruct Genv.find_funct_ptr);
clarify; [].
destruct f0; [|
done].
simpl in INIT.
destruct beq_nat; [|
done].
inv INIT.
eexists;
split;
try done;
vauto.
econstructor;
vauto;
econstructor;
vauto.
Qed.
Lemma init_sim_fail:
forall p vals,
cms_init tge p vals =
None ->
cm_init ge p vals =
None.
Proof.
intros p vals INIT.
unfold cms_init,
cm_init in *.
pose proof TRANSF as (
MG &
MF).
specialize (
MF p).
repeat (
destruct Genv.find_funct_ptr);
clarify.
destruct f0; [|
done];
simpl in INIT.
by destruct beq_nat.
Qed.
End PRESERVATION.
Definition full_genv_rel ge tge :=
genv_rel ge tge /\ (
forall (
b :
Z) (
ofs :
int),
match Genv.find_funct_ptr ge (
Ptr b ofs)
with
|
Some _ =>
b = 0%
Z
|
None =>
True
end).
Definition sel_match_prg p p' :=
sel_program p =
p'.
Theorem sel_sim Mm :
Sim.sim Mm Mm cm_sem cms_sem sel_match_prg.
Proof.