Correctness of instruction selection
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Values.
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.
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:
helper_functions_declared ge 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 public_preserved:
forall (
s:
ident),
Genv.public_symbol tge s =
Genv.public_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 (
v v':
val) (
f:
Cminor.fundef),
Genv.find_funct ge v =
Some f ->
Val.lessdef v v' ->
exists tf,
Genv.find_funct 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_declared_preserved:
forall id name sg,
helper_declared ge id name sg ->
helper_declared tge id name sg.
Proof.
Let HELPERS':
helper_functions_declared tge hf.
Proof.
Section CMCONSTR.
Variable sp:
val.
Variable e:
env.
Variable m:
mem.
Lemma eval_condexpr_of_expr:
forall a le v b,
eval_expr tge sp e m le a v ->
Val.bool_of_val v b ->
eval_condexpr tge sp e m le (
condexpr_of_expr a)
b.
Proof.
intros until a.
functional induction (
condexpr_of_expr a);
intros.
compare *)
inv H.
econstructor;
eauto.
simpl in H6.
inv H6.
apply Val.bool_of_val_of_optbool.
auto.
condition *)
inv H.
econstructor;
eauto.
destruct va;
eauto.
let *)
inv H.
econstructor;
eauto.
default *)
econstructor.
constructor.
eauto.
constructor.
simpl.
inv H0.
auto.
Qed.
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 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 (
State f (
store chunk a1 a2)
k sp e m)
E0 (
State f Sskip k sp e m').
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 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 =
Vptr b Int.zero
|
Call_builtin ef =>
fd =
External ef
end.
Proof.
Translation of switch statements
Inductive Rint:
Z ->
val ->
Prop :=
|
Rint_intro:
forall n,
Rint (
Int.unsigned n) (
Vint n).
Inductive Rlong:
Z ->
val ->
Prop :=
|
Rlong_intro:
forall n,
Rlong (
Int64.unsigned n) (
Vlong n).
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:
Z ->
val ->
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 i v -> 0 <=
n <
modulus ->
eval_expr tge sp e m le (
make_cmp_eq a n) (
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 i v -> 0 <=
n <
modulus ->
eval_expr tge sp e m le (
make_cmp_ltu a n) (
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 i v -> 0 <=
n <
modulus ->
exists v',
eval_expr tge sp e m le (
make_sub a n)
v' /\
R ((
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 i v ->
exists v',
eval_expr tge sp e m le (
make_to_int a)
v' /\
Rint (
i mod Int.modulus)
v'.
Lemma sel_switch_correct_rec:
forall sp e m varg i x,
R 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 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.
Lemma sel_switch_int_correct:
forall dfl cases arg sp e m i t le,
validate_switch Int.modulus dfl cases t =
true ->
eval_expr tge sp e m le arg (
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 t le,
validate_switch Int64.modulus dfl cases t =
true ->
eval_expr tge sp e m le arg (
Vlong i) ->
eval_exitexpr tge sp e m le (
XElet arg (
sel_switch_long 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.
intros until v; intros EV LD. inv LD.
exists v; auto.
destruct op; simpl in *; inv EV; TrivialExists.
Qed.
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' ->
Mem.extends m m' ->
exists v',
eval_binop op v1'
v2'
m' =
Some v' /\
Val.lessdef v v'.
Proof.
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).
exists v2;
split;
congruence.
auto.
Qed.
Lemma set_optvar_lessdef:
forall e1 e2 optid v1 v2,
env_lessdef e1 e2 ->
Val.lessdef v1 v2 ->
env_lessdef (
set_optvar optid v1 e1) (
set_optvar optid v2 e2).
Proof.
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,
Cminor.eval_expr ge sp e m a v ->
forall e'
le m',
env_lessdef e e' ->
Mem.extends m m' ->
exists v',
eval_expr tge sp e'
m'
le (
sel_expr hf a)
v' /\
Val.lessdef v v'.
Proof.
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.extends m m' ->
exists v',
eval_exprlist tge sp e'
m'
le (
sel_exprlist hf a)
v' /\
Val.lessdef_list v v'.
Proof.
induction 1;
intros;
simpl.
exists (@
nil val);
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.
Lemma sel_builtin_arg_correct:
forall sp e e'
m m'
a v c,
env_lessdef e e' ->
Mem.extends m m' ->
Cminor.eval_expr ge sp e m a v ->
exists v',
CminorSel.eval_builtin_arg tge sp e'
m' (
sel_builtin_arg hf a c)
v'
/\
Val.lessdef v v'.
Proof.
Lemma sel_builtin_args_correct:
forall sp e e'
m m',
env_lessdef e e' ->
Mem.extends m m' ->
forall al vl,
Cminor.eval_exprlist ge sp e m al vl ->
forall cl,
exists vl',
list_forall2 (
CminorSel.eval_builtin_arg tge sp e'
m')
(
sel_builtin_args hf al cl)
vl'
/\
Val.lessdef_list vl vl'.
Proof.
induction 3;
intros;
simpl.
-
exists (@
nil val);
split;
constructor.
-
exploit sel_builtin_arg_correct;
eauto.
intros (
v1' &
A &
B).
edestruct IHeval_exprlist as (
vl' &
C &
D).
exists (
v1' ::
vl');
split;
auto.
constructor;
eauto.
Qed.
Lemma sel_builtin_res_correct:
forall oid v e v'
e',
env_lessdef e e' ->
Val.lessdef v v' ->
env_lessdef (
set_optvar oid v e) (
set_builtin_res (
sel_builtin_res oid)
v'
e').
Proof.
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'
sp 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.extends m m'),
match_states
(
Cminor.State f s k sp e m)
(
State f'
s'
k'
sp 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.extends 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.extends 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.extends m m')
(
EA:
list_forall2 (
CminorSel.eval_builtin_arg tge sp e'
m')
al args'),
match_states
(
Cminor.Callstate (
External ef)
args (
Cminor.Kcall optid f sp e k)
m)
(
State f' (
Sbuiltin (
sel_builtin_res optid)
ef al)
k'
sp 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.extends m m'),
match_states
(
Cminor.Returnstate v (
Cminor.Kcall optid f sp e k)
m)
(
State f'
Sskip k'
sp (
set_builtin_res (
sel_builtin_res 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 sel_step_correct:
forall S1 t S2,
Cminor.step ge S1 t S2 ->
forall T1,
match_states S1 T1 ->
(
exists T2,
step tge T1 t T2 /\
match_states S2 T2)
\/ (
measure S2 <
measure S1 /\
t =
E0 /\
match_states S2 T1)%
nat.
Proof.
Lemma sel_initial_states:
forall S,
Cminor.initial_state prog S ->
exists R,
initial_state tprog 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.
intros. inv H0. inv H. inv MC. inv LD. constructor.
Qed.
End PRESERVATION.
Processing of helper functions
Lemma record_globdefs_sound:
forall p id fd,
(
record_globdefs p)!
id =
Some (
Gfun fd) ->
exists b,
Genv.find_symbol (
Genv.globalenv p)
id =
Some b
/\
Genv.find_funct_ptr (
Genv.globalenv p)
b =
Some fd.
Proof.
Lemma lookup_helper_correct_1:
forall globs name sg id,
lookup_helper globs name sg =
OK id ->
globs!
id =
Some (
Gfun (
External (
EF_external name sg))).
Proof.
Lemma lookup_helper_correct:
forall p name sg id,
lookup_helper (
record_globdefs p)
name sg =
OK id ->
helper_declared (
Genv.globalenv p)
id name sg.
Proof.
Theorem get_helpers_correct:
forall p hf,
get_helpers p =
OK hf ->
helper_functions_declared (
Genv.globalenv p)
hf.
Proof.
All together
Theorem transf_program_correct:
forall prog tprog,
sel_program prog =
OK tprog ->
forward_simulation (
Cminor.semantics prog) (
CminorSel.semantics tprog).
Proof.