Correctness of instruction selection
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Values.
Require Import NormaliseSpec.
Require Import ExprEval.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Switch.
Require Import Cminor.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.
Require Import SelectDiv.
Require Import SelectLong.
Require Import Selection.
Require Import SelectOpproof.
Require Import SelectDivproof.
Require Import SelectLongproof.
Require Import SameEvalCmp.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Floats.
Require Import IntFacts.
Require Import MemRel.
Local Open Scope cminorsel_scope.
Local Open Scope error_monad_scope.
Correctness of the instruction selection functions for expressions
Section PRESERVATION.
Variable prog:
Cminor.program.
Variable tprog:
CminorSel.program.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Variable hf:
helper_functions.
Hypothesis HELPERS:
i64_helpers_correct tge hf.
Hypothesis TRANSFPROG:
transform_partial_program (
sel_fundef hf ge)
prog =
OK tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
Lemma function_ptr_translated:
forall (
b:
block) (
f:
Cminor.fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
sel_fundef hf ge f =
OK tf.
Proof.
Lemma functions_translated:
forall (
m:
mem) (
v v':
expr_sym) (
f:
Cminor.fundef),
Genv.find_funct m ge v =
Some f ->
Val.lessdef v v' ->
exists tf,
Genv.find_funct m tge v' =
Some tf /\
sel_fundef hf ge f =
OK tf.
Proof.
Lemma sig_function_translated:
forall f tf,
sel_fundef hf ge f =
OK tf ->
funsig tf =
Cminor.funsig f.
Proof.
intros. destruct f; monadInv H; auto. monadInv EQ. auto.
Qed.
Lemma stackspace_function_translated:
forall f tf,
sel_function hf ge f =
OK tf ->
fn_stackspace tf =
Cminor.fn_stackspace f.
Proof.
intros. monadInv H. auto.
Qed.
Lemma varinfo_preserved:
forall b,
Genv.find_var_info tge b =
Genv.find_var_info ge b.
Proof.
Lemma helper_implements_preserved:
forall id sg vargs vres,
helper_implements ge id sg vargs vres ->
helper_implements tge id sg vargs vres.
Proof.
Lemma builtin_implements_preserved:
forall id sg vargs vres,
builtin_implements ge id sg vargs vres ->
builtin_implements tge id sg vargs vres.
Proof.
Lemma helpers_correct_preserved:
forall h,
i64_helpers_correct ge h ->
i64_helpers_correct tge h.
Proof.
Section CMCONSTR.
Variable sp:
expr_sym.
Variable e:
env.
Variable m:
mem.
Lemma eval_condexpr_of_expr:
forall a le v i,
eval_expr tge sp e m le a v ->
Mem.mem_norm m v =
Vint i ->
eval_condexpr tge sp e m le (
condexpr_of_expr a) (
negb (
Int.eq i Int.zero)).
Proof.
Lemma eval_load:
forall le a v chunk v',
eval_expr tge sp e m le a v ->
Mem.loadv chunk m v =
Some v' ->
eval_expr tge sp e m le (
load chunk a)
v'.
Proof.
Lemma eval_store:
forall needed_stackspace chunk a1 a2 v1 v2 f k m',
eval_expr tge sp e m nil a1 v1 ->
eval_expr tge sp e m nil a2 v2 ->
Mem.storev chunk m v1 v2 =
Some m' ->
step tge needed_stackspace (
State f (
store chunk a1 a2)
k sp e m)
E0 (
State f Sskip k sp e m').
Proof.
Ltac UseHelper :=
red in HELPERS;
repeat (
eauto;
match goal with | [
H:
_ /\
_ |-
_ ] =>
destruct H end).
Lemma eval_intuoffloat:
forall le a1 v1
(
EVAL :
eval_expr tge sp e m le a1 v1),
exists v',
eval_expr tge sp e m le (
intuoffloat hf a1)
v' /\
Val.lessdef (
Val.intuoffloat v1)
v'.
Proof.
Lemma eval_floatofintu:
forall le a1 v1
(
EVAL :
eval_expr tge sp e m le a1 v1),
exists v',
eval_expr tge sp e m le (
floatofintu hf a1)
v' /\
Val.lessdef (
Val.floatofintu v1)
v'.
Proof.
Lemma eval_intuofsingle:
forall le a1 v1
(
EVAL :
eval_expr tge sp e m le a1 v1),
exists v',
eval_expr tge sp e m le (
intuofsingle hf a1)
v' /\
Val.lessdef (
Val.intuofsingle v1)
v'.
Proof.
Lemma eval_singleofintu:
forall le a1 v1
(
EVAL :
eval_expr tge sp e m le a1 v1),
exists v',
eval_expr tge sp e m le (
singleofintu hf a1)
v' /\
Val.lessdef (
Val.singleofintu v1)
v'.
Proof.
Correctness of instruction selection for operators
Lemma eval_sel_unop:
forall le op a1 v1 v,
eval_expr tge sp e m le a1 v1 ->
eval_unop op v1 =
Some v ->
exists v',
eval_expr tge sp e m le (
sel_unop hf op a1)
v' /\
Val.lessdef v v'.
Proof.
Lemma eval_sel_binop:
forall le op a1 a2 v1 v2 v,
eval_expr tge sp e m le a1 v1 ->
eval_expr tge sp e m le a2 v2 ->
eval_binop op v1 v2 m =
Some v ->
exists v',
eval_expr tge sp e m le (
sel_binop hf op a1 a2)
v' /\
Val.lessdef v v'.
Proof.
End CMCONSTR.
Recognition of calls to built-in functions
Lemma expr_is_addrof_ident_correct:
forall e id,
expr_is_addrof_ident e =
Some id ->
e =
Cminor.Econst (
Cminor.Oaddrsymbol id Int.zero).
Proof.
Lemma classify_call_correct:
forall sp e m a v fd,
Cminor.eval_expr ge sp e m a v ->
Genv.find_funct m ge v =
Some fd ->
match classify_call ge a with
|
Call_default =>
True
|
Call_imm id =>
exists b,
Genv.find_symbol ge id =
Some b /\
v =
Eval (
Vptr b Int.zero)
|
Call_builtin ef =>
fd =
External ef
end.
Proof.
Lemma classify_call_correct_free:
forall sp e m a v fd m'
m''
sz
(
EXPR:
Cminor.eval_expr ge sp e m a v)
(
FREE:
Mem.free m sp 0
sz =
Some m')
n (
REL:
MemReserve.release_boxes m'
n =
Some m'')
(
FF:
Genv.find_funct m''
ge v =
Some fd),
match classify_call ge a with
|
Call_default =>
True
|
Call_imm id =>
exists b,
Genv.find_symbol ge id =
Some b /\
v =
Eval (
Vptr b Int.zero)
|
Call_builtin ef =>
fd =
External ef
end.
Proof.
Translation of switch statements
Inductive Rint:
mem ->
Z ->
expr_sym ->
Prop :=
|
Rint_intro:
forall m n e,
Mem.mem_norm m e =
Vint n ->
Rint m (
Int.unsigned n)
e.
Inductive Rlong:
mem ->
Z ->
expr_sym ->
Prop :=
|
Rlong_intro:
forall m n e,
Mem.mem_norm m e =
Vlong n ->
Rlong m (
Int64.unsigned n)
e.
Section SEL_SWITCH.
Variable make_cmp_eq:
expr ->
Z ->
expr.
Variable make_cmp_ltu:
expr ->
Z ->
expr.
Variable make_sub:
expr ->
Z ->
expr.
Variable make_to_int:
expr ->
expr.
Variable modulus:
Z.
Variable R:
mem ->
Z ->
expr_sym ->
Prop.
Hypothesis eval_make_cmp_eq:
forall sp e m le a v i n,
eval_expr tge sp e m le a v ->
R m i v -> 0 <=
n <
modulus ->
exists vn,
eval_expr tge sp e m le (
make_cmp_eq a n)
vn /\
Mem.mem_norm m vn =
Values.Val.of_bool (
zeq i n).
Hypothesis eval_make_cmp_ltu:
forall sp e m le a v i n,
eval_expr tge sp e m le a v ->
R m i v -> 0 <=
n <
modulus ->
exists vn,
eval_expr tge sp e m le (
make_cmp_ltu a n)
vn /\
Mem.mem_norm m vn =
Values.Val.of_bool (
zlt i n).
Hypothesis eval_make_sub:
forall sp e m le a v i n,
eval_expr tge sp e m le a v ->
R m i v -> 0 <=
n <
modulus ->
exists v',
eval_expr tge sp e m le (
make_sub a n)
v' /\
R m ((
i -
n)
mod modulus)
v'.
Hypothesis eval_make_to_int:
forall sp e m le a v i,
eval_expr tge sp e m le a v ->
R m i v ->
exists v',
eval_expr tge sp e m le (
make_to_int a)
v' /\
Rint m (
i mod Int.modulus)
v'.
Lemma sel_switch_correct_rec:
forall sp e m varg i x,
R m i varg ->
forall t arg le,
wf_comptree modulus t ->
nth_error le arg =
Some varg ->
comptree_match modulus i t =
Some x ->
eval_exitexpr tge sp e m le (
sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t)
x.
Proof.
Lemma sel_switch_correct:
forall dfl cases arg sp e m varg i t le,
validate_switch modulus dfl cases t =
true ->
eval_expr tge sp e m le arg varg ->
R m i varg ->
0 <=
i <
modulus ->
eval_exitexpr tge sp e m le
(
XElet arg (
sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t))
(
switch_target i dfl cases).
Proof.
End SEL_SWITCH.
Require Import Psatz.
Lemma sel_switch_int_correct:
forall dfl cases arg sp e m i vi t le,
validate_switch Int.modulus dfl cases t =
true ->
eval_expr tge sp e m le arg vi ->
Mem.mem_norm m vi =
Vint i ->
eval_exitexpr tge sp e m le (
XElet arg (
sel_switch_int O t)) (
switch_target (
Int.unsigned i)
dfl cases).
Proof.
Lemma sel_switch_long_correct:
forall dfl cases arg sp e m i vi t le,
validate_switch Int64.modulus dfl cases t =
true ->
eval_expr tge sp e m le arg vi ->
Mem.mem_norm m vi =
Vlong i ->
eval_exitexpr tge sp e m le (
XElet arg (
sel_switch_long hf O t)) (
switch_target (
Int64.unsigned i)
dfl cases).
Proof.
Compatibility of evaluation functions with the "less defined than" relation.
Ltac TrivialExists :=
match goal with
| [ |-
exists v,
Some ?
x =
Some v /\
_ ] =>
exists x;
split;
auto
|
_ =>
idtac
end.
Lemma eval_unop_lessdef:
forall op v1 v1'
v,
eval_unop op v1 =
Some v ->
Val.lessdef v1 v1' ->
exists v',
eval_unop op v1' =
Some v' /\
Val.lessdef v v'.
Proof.
Lemma eval_binop_lessdef:
forall op v1 v1'
v2 v2'
v m m',
eval_binop op v1 v2 m =
Some v ->
Val.lessdef v1 v1' ->
Val.lessdef v2 v2' ->
exists v',
eval_binop op v1'
v2'
m' =
Some v' /\
Val.lessdef v v'.
Proof.
intros until m';
intros EV LD1 LD2.
destruct op;
destruct v1';
simpl in *;
inv EV;
TrivialExists;
repeat ((
apply Val.lessdef_unop;
auto)
||
(
apply Val.lessdef_binop;
auto)).
Qed.
Semantic preservation for instruction selection.
Relationship between the local environments.
Definition env_lessdef (
e1 e2:
env) :
Prop :=
forall id v1,
e1!
id =
Some v1 ->
exists v2,
e2!
id =
Some v2 /\
Val.lessdef v1 v2.
Lemma set_var_lessdef:
forall e1 e2 id v1 v2,
env_lessdef e1 e2 ->
Val.lessdef v1 v2 ->
env_lessdef (
PTree.set id v1 e1) (
PTree.set id v2 e2).
Proof.
intros;
red;
intros.
rewrite PTree.gsspec in *.
destruct (
peq id0 id);
eauto.
inv H1.
eauto.
Qed.
Lemma env_lessdef_refl:
forall e,
env_lessdef e e.
Proof.
red; intros.
eexists; split; eauto.
Qed.
Lemma set_params_lessdef:
forall il vl1 vl2,
Val.lessdef_list vl1 vl2 ->
env_lessdef (
set_params vl1 il) (
set_params vl2 il).
Proof.
Lemma set_locals_lessdef:
forall e1 e2,
env_lessdef e1 e2 ->
forall il,
env_lessdef (
set_locals il e1) (
set_locals il e2).
Proof.
Semantic preservation for expressions.
Lemma sel_expr_correct:
forall sp e m a v
(
EXPR:
Cminor.eval_expr ge sp e m a v),
forall e'
le m',
env_lessdef e e' ->
mem_lessdef m m' ->
exists v',
eval_expr tge (
Eval (
Vptr sp Int.zero))
e'
m'
le (
sel_expr hf a)
v' /\
Val.lessdef v v'.
Proof.
induction 1;
intros;
simpl.
-
exploit H0;
eauto.
intros [
v' [
A B]].
exists v';
split;
auto.
constructor;
auto.
-
destruct cst;
simpl in *;
inv H.
+ (
exists (
Eval (
Vint i));
split;
auto).
econstructor.
constructor.
auto.
+ (
exists (
Eval (
Vfloat f));
split;
auto).
econstructor.
constructor.
auto.
+ (
exists (
Eval (
Vsingle f));
split;
auto).
econstructor.
constructor.
auto.
+ (
exists (
Val.longofwords (
Eval (
Vint (
Int64.hiword i)))
(
Eval (
Vint (
Int64.loword i)))));
split.
eapply eval_Eop.
constructor.
EvalOp.
simpl;
eauto.
constructor.
EvalOp.
simpl;
eauto.
constructor.
auto.
red;
intros;
simpl;
intros;
seval;
auto.
rewrite Int64.ofwords_recompose.
auto.
+
revert H3;
destr.
inv H3.
rewrite <-
symbols_preserved in Heqo.
fold (
Genv.symbol_address tge i i0).
exploit (
eval_addrsymbol tge (
Eval (
Vptr sp Int.zero))
e'
m'
le i i0 b).
unfold Genv.symbol_address'.
rewrite Heqo.
eauto.
intros [
v [
A B]];
eexists;
split;
eauto.
red;
intros;
simpl.
destr.
rewrite B.
simpl;
auto.
+
exploit eval_addrstack.
intros [
v [
A B]].
eexists;
split;
eauto.
destr.
red;
intros.
rewrite <-
B.
simpl.
rewrite Int.add_zero.
auto.
-
exploit IHEXPR;
eauto.
intros [
v1' [
A B]].
exploit eval_unop_lessdef;
eauto.
intros [
v' [
C D]].
exploit eval_sel_unop;
eauto.
intros [
v'' [
E F]].
exists v'';
split;
eauto.
eapply Val.lessdef_trans;
eauto.
-
exploit IHEXPR1;
eauto.
intros [
v1' [
A B]].
exploit IHEXPR2;
eauto.
intros [
v2' [
C D]].
exploit eval_binop_lessdef;
eauto.
intros [
v' [
E F]].
exploit eval_sel_binop.
eexact A.
eexact C.
eauto.
intros [
v'' [
P Q]].
exists v'';
split;
eauto.
eapply Val.lessdef_trans;
eauto.
-
exploit IHEXPR;
eauto.
intros [
vaddr' [
A B]].
exploit loadv_mem_rel;
eauto.
apply wf_mr_ld.
intros [
v' [
C D]].
exists v';
split;
auto.
eapply eval_load;
eauto.
revert C.
unfold Mem.loadv.
generalize (
Mem.lessdef_eqm m'
_ _ B).
intro E;
repeat destr;
inv E.
auto.
Qed.
Lemma sel_exprlist_correct:
forall sp e m a v,
Cminor.eval_exprlist ge sp e m a v ->
forall e'
le m',
env_lessdef e e' ->
mem_lessdef m m' ->
exists v',
eval_exprlist tge (
Eval (
Vptr sp Int.zero))
e'
m'
le (
sel_exprlist hf a)
v' /\
Val.lessdef_list v v'.
Proof.
induction 1;
intros;
simpl.
- (
exists (@
nil expr_sym);
split;
auto).
constructor.
-
exploit sel_expr_correct;
eauto.
intros [
v1' [
A B]].
exploit IHeval_exprlist;
eauto.
intros [
vl' [
C D]].
exists (
v1' ::
vl');
split;
auto.
constructor;
eauto.
Qed.
Semantic preservation for functions and statements.
Inductive match_cont:
Cminor.cont ->
CminorSel.cont ->
Prop :=
|
match_cont_stop:
match_cont Cminor.Kstop Kstop
|
match_cont_seq:
forall s s'
k k',
sel_stmt hf ge s =
OK s' ->
match_cont k k' ->
match_cont (
Cminor.Kseq s k) (
Kseq s'
k')
|
match_cont_block:
forall k k',
match_cont k k' ->
match_cont (
Cminor.Kblock k) (
Kblock k')
|
match_cont_call:
forall id f sp e k f'
e'
k',
sel_function hf ge f =
OK f' ->
match_cont k k' ->
env_lessdef e e' ->
match_cont (
Cminor.Kcall id f sp e k) (
Kcall id f' (
Eval (
Vptr sp Int.zero))
e'
k').
Inductive match_states:
Cminor.state ->
CminorSel.state ->
Prop :=
|
match_state:
forall f f'
s k s'
k'
sp e m e'
m'
(
TF:
sel_function hf ge f =
OK f')
(
TS:
sel_stmt hf ge s =
OK s')
(
MC:
match_cont k k')
(
LD:
env_lessdef e e')
(
ME:
mem_lessdef m m'),
match_states
(
Cminor.State f s k sp e m)
(
State f'
s'
k' (
Eval (
Vptr sp Int.zero))
e'
m')
|
match_callstate:
forall f f'
args args'
k k'
m m'
(
TF:
sel_fundef hf ge f =
OK f')
(
MC:
match_cont k k')
(
LD:
Val.lessdef_list args args')
(
ME:
mem_lessdef m m'),
match_states
(
Cminor.Callstate f args k m)
(
Callstate f'
args'
k'
m')
|
match_returnstate:
forall v v'
k k'
m m'
(
MC:
match_cont k k')
(
LD:
Val.lessdef v v')
(
ME:
mem_lessdef m m'),
match_states
(
Cminor.Returnstate v k m)
(
Returnstate v'
k'
m')
|
match_builtin_1:
forall ef args args'
optid f sp e k m al f'
e'
k'
m'
(
TF:
sel_function hf ge f =
OK f')
(
MC:
match_cont k k')
(
LDA:
Val.lessdef_list args args')
(
LDE:
env_lessdef e e')
(
ME:
mem_lessdef m m')
(
EA:
eval_exprlist tge (
Eval (
Vptr sp Int.zero))
e'
m'
nil al args'),
match_states
(
Cminor.Callstate (
External ef)
args (
Cminor.Kcall optid f sp e k)
m)
(
State f' (
Sbuiltin optid ef al)
k' (
Eval (
Vptr sp Int.zero))
e'
m')
|
match_builtin_2:
forall v v'
optid f sp e k m f'
e'
m'
k'
(
TF:
sel_function hf ge f =
OK f')
(
MC:
match_cont k k')
(
LDV:
Val.lessdef v v')
(
LDE:
env_lessdef e e')
(
ME:
mem_lessdef m m'),
match_states
(
Cminor.Returnstate v (
Cminor.Kcall optid f sp e k)
m)
(
State f'
Sskip k' (
Eval (
Vptr sp Int.zero)) (
set_optvar optid v'
e')
m').
Remark call_cont_commut:
forall k k',
match_cont k k' ->
match_cont (
Cminor.call_cont k) (
call_cont k').
Proof.
induction 1; simpl; auto. constructor. constructor; auto.
Qed.
Remark find_label_commut:
forall lbl s k s'
k',
match_cont k k' ->
sel_stmt hf ge s =
OK s' ->
match Cminor.find_label lbl s k,
find_label lbl s'
k'
with
|
None,
None =>
True
|
Some(
s1,
k1),
Some(
s1',
k1') =>
sel_stmt hf ge s1 =
OK s1' /\
match_cont k1 k1'
|
_,
_ =>
False
end.
Proof.
Definition measure (
s:
Cminor.state) :
nat :=
match s with
|
Cminor.Callstate _ _ _ _ => 0%
nat
|
Cminor.State _ _ _ _ _ _ => 1%
nat
|
Cminor.Returnstate _ _ _ => 2%
nat
end.
Lemma ld_list_ok:
forall v v',
Val.lessdef_list v v' ->
list_forall2 Val.lessdef v v'.
Proof.
induction 1; simpl; intros; repeat constructor; eauto.
Qed.
Variable needed_stackspace :
ident ->
nat .
Lemma sel_step_correct:
forall S1 t S2,
Cminor.step ge needed_stackspace S1 t S2 ->
forall T1,
match_states S1 T1 ->
(
exists T2,
step tge needed_stackspace T1 t T2 /\
match_states S2 T2) \/
(
measure S2 <
measure S1 /\
t =
E0 /\
match_states S2 T1)%
nat.
Proof.
Lemma sel_initial_states:
forall sg S,
Cminor.initial_state prog sg S ->
exists R,
initial_state tprog sg R /\
match_states S R.
Proof.
Lemma sel_final_states:
forall S R r,
match_states S R ->
Cminor.final_state S r ->
final_state R r.
Proof.
End PRESERVATION.
Axiom get_helpers_correct:
forall ge hf,
get_helpers ge =
OK hf ->
i64_helpers_correct ge hf.
Theorem transf_program_correct:
forall prog tprog ns sg,
sel_program prog =
OK tprog ->
forward_simulation (
Cminor.semantics prog ns sg)
(
CminorSel.semantics tprog ns sg).
Proof.