Correctness of instruction selection for integer division
Require Import Coqlib.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import NormaliseSpec.
Require Import ExprEval.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Cminor.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.
Require Import SelectOpproof.
Require Import SelectLong.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import IntFacts.
Open Local Scope cminorsel_scope.
Axiomatization of the helper functions
Section HELPERS.
Context {
F V:
Type} (
ge:
Genv.t (
AST.fundef F)
V).
Definition helper_implements (
id:
ident) (
sg:
signature) (
vargs:
list expr_sym) (
vres:
expr_sym) :
Prop :=
exists b,
exists ef,
Genv.find_symbol ge id =
Some b
/\
Genv.find_funct_ptr ge b =
Some (
External ef)
/\
ef_sig ef =
sg
/\
forall m,
external_call ef ge vargs m E0 vres m.
Definition builtin_implements (
id:
ident) (
sg:
signature) (
vargs:
list expr_sym) (
vres:
expr_sym) :
Prop :=
forall m,
external_call (
EF_builtin id sg)
ge vargs m E0 vres m.
Definition i64_helpers_correct (
hf:
helper_functions) :
Prop :=
(
forall x z,
Val.longoffloat x =
z ->
helper_implements hf.(
i64_dtos)
sig_f_l (
x::
nil)
z)
/\(
forall x z,
Val.longuoffloat x =
z ->
helper_implements hf.(
i64_dtou)
sig_f_l (
x::
nil)
z)
/\(
forall x z,
Val.floatoflong x =
z ->
helper_implements hf.(
i64_stod)
sig_l_f (
x::
nil)
z)
/\(
forall x z,
Val.floatoflongu x =
z ->
helper_implements hf.(
i64_utod)
sig_l_f (
x::
nil)
z)
/\(
forall x z,
Val.singleoflong x =
z ->
helper_implements hf.(
i64_stof)
sig_l_s (
x::
nil)
z)
/\(
forall x z,
Val.singleoflongu x =
z ->
helper_implements hf.(
i64_utof)
sig_l_s (
x::
nil)
z)
/\(
forall x,
builtin_implements hf.(
i64_neg)
sig_l_l (
x::
nil) (
Val.negl x))
/\(
forall x y,
builtin_implements hf.(
i64_add)
sig_ll_l (
x::
y::
nil) (
Val.addl x y))
/\(
forall x y,
builtin_implements hf.(
i64_sub)
sig_ll_l (
x::
y::
nil) (
Val.subl x y))
/\(
forall x y,
builtin_implements hf.(
i64_mul)
sig_ii_l (
x::
y::
nil) (
Val.mull'
x y))
/\(
forall x y z,
Val.divls x y =
z ->
helper_implements hf.(
i64_sdiv)
sig_ll_l (
x::
y::
nil)
z)
/\(
forall x y z,
Val.divlu x y =
z ->
helper_implements hf.(
i64_udiv)
sig_ll_l (
x::
y::
nil)
z)
/\(
forall x y z,
Val.modls x y =
z ->
helper_implements hf.(
i64_smod)
sig_ll_l (
x::
y::
nil)
z)
/\(
forall x y z,
Val.modlu x y =
z ->
helper_implements hf.(
i64_umod)
sig_ll_l (
x::
y::
nil)
z)
/\(
forall x y,
helper_implements hf.(
i64_shl)
sig_li_l (
x::
y::
nil) (
Val.shll x y))
/\(
forall x y,
helper_implements hf.(
i64_shr)
sig_li_l (
x::
y::
nil) (
Val.shrlu x y))
/\(
forall x y,
helper_implements hf.(
i64_sar)
sig_li_l (
x::
y::
nil) (
Val.shrl x y))
/\(
forall x z,
Val.intuoffloat x =
z ->
helper_implements hf.(
helper_f2u)
sig_f_i (
x::
nil)
z)
/\(
forall x z,
Val.floatofintu x =
z ->
helper_implements hf.(
helper_u2f)
sig_i_f (
x::
nil)
z).
End HELPERS.
Correctness of the instruction selection functions for 64-bit operators
Section CMCONSTR.
Variable hf:
helper_functions.
Variable ge:
genv.
Hypothesis HELPERS:
i64_helpers_correct ge hf.
Variable sp:
expr_sym.
Variable e:
env.
Variable m:
mem.
Ltac UseHelper :=
red in HELPERS;
repeat (
eauto;
match goal with | [
H:
_ /\
_ |-
_ ] =>
destruct H end).
Lemma eval_helper:
forall le id sg args vargs vres,
eval_exprlist ge sp e m le args vargs ->
helper_implements ge id sg vargs vres ->
eval_expr ge sp e m le (
Eexternal id sg args)
vres.
Proof.
intros. destruct H0 as (b & ef & A & B & C & D). econstructor; eauto.
Qed.
Corollary eval_helper_1:
forall le id sg arg1 varg1 vres,
eval_expr ge sp e m le arg1 varg1 ->
helper_implements ge id sg (
varg1::
nil)
vres ->
eval_expr ge sp e m le (
Eexternal id sg (
arg1 :::
Enil))
vres.
Proof.
intros.
eapply eval_helper;
eauto.
constructor;
auto.
constructor.
Qed.
Corollary eval_helper_2:
forall le id sg arg1 arg2 varg1 varg2 vres,
eval_expr ge sp e m le arg1 varg1 ->
eval_expr ge sp e m le arg2 varg2 ->
helper_implements ge id sg (
varg1::
varg2::
nil)
vres ->
eval_expr ge sp e m le (
Eexternal id sg (
arg1 :::
arg2 :::
Enil))
vres.
Proof.
intros.
eapply eval_helper;
eauto.
constructor;
auto.
constructor;
auto.
constructor.
Qed.
Remark eval_builtin_1:
forall le id sg arg1 varg1 vres,
eval_expr ge sp e m le arg1 varg1 ->
builtin_implements ge id sg (
varg1::
nil)
vres ->
eval_expr ge sp e m le (
Ebuiltin (
EF_builtin id sg) (
arg1 :::
Enil))
vres.
Proof.
intros. econstructor. econstructor. eauto. constructor. apply H0.
Qed.
Remark eval_builtin_2:
forall le id sg arg1 arg2 varg1 varg2 vres,
eval_expr ge sp e m le arg1 varg1 ->
eval_expr ge sp e m le arg2 varg2 ->
builtin_implements ge id sg (
varg1::
varg2::
nil)
vres ->
eval_expr ge sp e m le (
Ebuiltin (
EF_builtin id sg) (
arg1 :::
arg2 :::
Enil))
vres.
Proof.
intros. econstructor. constructor; eauto. constructor; eauto. constructor. apply H1.
Qed.
Definition unary_constructor_sound (
cstr:
expr ->
expr) (
sem:
expr_sym ->
expr_sym) :
Prop :=
forall le a x,
eval_expr ge sp e m le a x ->
exists v,
eval_expr ge sp e m le (
cstr a)
v /\
Val.lessdef (
sem x)
v.
Definition binary_constructor_sound (
cstr:
expr ->
expr ->
expr) (
sem:
expr_sym ->
expr_sym ->
expr_sym) :
Prop :=
forall le a x b y,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
exists v,
eval_expr ge sp e m le (
cstr a b)
v /\
Val.lessdef (
sem x y)
v.
Ltac EvalOp :=
eauto;
match goal with
| [ |-
eval_exprlist _ _ _ _ _ Enil _ ] =>
constructor
| [ |-
eval_exprlist _ _ _ _ _ (
_:::
_)
_ ] =>
econstructor;
EvalOp
| [ |-
eval_expr _ _ _ _ _ (
Eletvar _)
_ ] =>
constructor;
simpl;
eauto
| [ |-
eval_expr _ _ _ _ _ (
Elet _ _)
_ ] =>
econstructor;
EvalOp
| [ |-
eval_expr _ _ _ _ _ (
lift _)
_ ] =>
apply eval_lift;
EvalOp
| [ |-
eval_expr _ _ _ _ _ _ _ ] =>
eapply eval_Eop; [
EvalOp |
simpl;
eauto]
|
_ =>
idtac
end.
Lemma same_eval_longofwords_recompose:
forall v,
wt_expr v Tlong ->
same_eval v (
Val.longofwords (
Val.hiword v) (
Val.loword v)).
Proof.
Lemma eval_splitlong:
forall le a f v sem
(
same_eval_sem:
forall v v',
Val.lessdef v v' ->
Val.lessdef (
sem v) (
sem v'))
(
sem_undef:
forall v, (~
wt_expr v Tlong) ->
forall alloc em,
eSexpr alloc em (
sem v) =
Vundef),
(
forall le a b x y
(
EXPRx:
eval_expr ge sp e m le a x)
(
EXPRy:
eval_expr ge sp e m le b y),
exists v,
eval_expr ge sp e m le (
f a b)
v /\
Val.lessdef (
sem (
Val.longofwords x y))
v) ->
eval_expr ge sp e m le a v ->
exists v',
eval_expr ge sp e m le (
splitlong a f)
v' /\
Val.lessdef (
sem v)
v'.
Proof.
Lemma eval_lowlong:
unary_constructor_sound lowlong Val.loword.
Proof.
Lemma eval_highlong:
unary_constructor_sound highlong Val.hiword.
Proof.
Lemma eval_splitlong_strict:
forall le a f va v,
eval_expr ge sp e m le a va ->
(
forall le a1 a2,
(
exists va1,
eval_expr ge sp e m le a1 va1
/\
Val.lessdef (
Val.hiword va)
va1) ->
(
exists va2,
eval_expr ge sp e m le a2 va2
/\
Val.lessdef (
Val.loword va)
va2) ->
exists v',
eval_expr ge sp e m le (
f a1 a2)
v' /\
Val.lessdef v v') ->
exists v',
eval_expr ge sp e m le (
splitlong a f)
v' /\
Val.lessdef v v'.
Proof.
Lemma eval_splitlong2:
forall le a b f va vb sem
(
same_eval_sem:
forall v v'
x x',
Val.lessdef v v' ->
Val.lessdef x x' ->
Val.lessdef (
sem v x) (
sem v'
x'))
(
sem_undef:
forall v x,
~
wt_expr v Tlong \/ ~
wt_expr x Tlong ->
forall alloc em,
eSexpr alloc em (
sem v x) =
Vundef)
(
EXEC:
forall le a1 a2 b1 b2 x1 x2 y1 y2
(
EXPRx1:
eval_expr ge sp e m le a1 x1)
(
EXPRx2:
eval_expr ge sp e m le a2 x2)
(
EXPRy1:
eval_expr ge sp e m le b1 y1)
(
EXPRy2:
eval_expr ge sp e m le b2 y2),
exists v,
eval_expr ge sp e m le (
f a1 a2 b1 b2)
v /\
Val.lessdef (
sem (
Val.longofwords x1 x2) (
Val.longofwords y1 y2))
v)
(
EXPR1:
eval_expr ge sp e m le a va)
(
EXPR2:
eval_expr ge sp e m le b vb),
exists v,
eval_expr ge sp e m le (
splitlong2 a b f)
v /\
Val.lessdef (
sem va vb)
v.
Proof.
Lemma eval_splitlong2_strict:
forall le a b f va vb v,
eval_expr ge sp e m le a va ->
eval_expr ge sp e m le b vb ->
(
forall le a1 a2 b1 b2,
(
exists va1,
eval_expr ge sp e m le a1 va1
/\
Val.lessdef (
Val.hiword va)
va1) ->
(
exists va2,
eval_expr ge sp e m le a2 va2
/\
Val.lessdef (
Val.loword va)
va2) ->
(
exists vb1,
eval_expr ge sp e m le b1 vb1
/\
Val.lessdef (
Val.hiword vb)
vb1) ->
(
exists vb2,
eval_expr ge sp e m le b2 vb2
/\
Val.lessdef (
Val.loword vb)
vb2) ->
exists v',
eval_expr ge sp e m le (
f a1 a2 b1 b2)
v' /\
Val.lessdef v v') ->
exists v',
eval_expr ge sp e m le (
splitlong2 a b f)
v' /\
Val.lessdef v v'.
Proof.
Lemma is_longconst_sound:
forall le a x n,
is_longconst a =
Some n ->
eval_expr ge sp e m le a x ->
same_eval x (
Eval (
Vlong n)).
Proof.
unfold is_longconst;
intros until n;
intros LC.
destruct (
is_longconst_match a);
intros.
inv LC.
InvEval.
simpl in H5.
inv H5.
constructor;
simpl;
auto.
discriminate.
Qed.
Lemma is_longconst_zero_sound:
forall le a x,
is_longconst_zero a =
true ->
eval_expr ge sp e m le a x ->
same_eval x (
Eval (
Vlong Int64.zero)).
Proof.
Lemma eval_longconst:
forall le n,
exists v,
eval_expr ge sp e m le (
longconst n)
v /\
same_eval v (
Eval (
Vlong n)).
Proof.
Theorem eval_intoflong:
unary_constructor_sound intoflong Val.loword.
Proof eval_lowlong.
Theorem eval_longofintu:
unary_constructor_sound longofintu Val.longofintu.
Proof.
Theorem eval_longofint:
unary_constructor_sound longofint Val.longofint.
Proof.
Ltac TrivialExists :=
eexists;
split; [
repeat (
econstructor;
simpl;
eauto)|
eauto;
try solve[
constructor;
simpl;
auto]].
Theorem eval_negl:
unary_constructor_sound (
negl hf)
Val.negl.
Proof.
Theorem eval_notl:
unary_constructor_sound notl Val.notl.
Proof.
Theorem eval_longoffloat:
unary_constructor_sound (
longoffloat hf)
Val.longoffloat.
Proof.
Theorem eval_longuoffloat:
unary_constructor_sound (
longuoffloat hf)
Val.longuoffloat.
Proof.
Theorem eval_floatoflong:
unary_constructor_sound (
floatoflong hf)
Val.floatoflong.
Proof.
Theorem eval_floatoflongu:
unary_constructor_sound (
floatoflongu hf)
Val.floatoflongu.
Proof.
Theorem eval_longofsingle:
unary_constructor_sound (
longofsingle hf)
Val.longofsingle.
Proof.
Theorem eval_longuofsingle:
unary_constructor_sound (
longuofsingle hf)
Val.longuofsingle.
Proof.
Theorem eval_singleoflong:
unary_constructor_sound (
singleoflong hf)
Val.singleoflong.
Proof.
Theorem eval_singleoflongu:
unary_constructor_sound (
singleoflongu hf)
Val.singleoflongu.
Proof.
Theorem eval_andl:
binary_constructor_sound andl Val.andl.
Proof.
Theorem eval_orl:
binary_constructor_sound orl Val.orl.
Proof.
Theorem eval_xorl:
binary_constructor_sound xorl Val.xorl.
Proof.
Lemma is_intconst_sound:
forall le a x n,
is_intconst a =
Some n ->
eval_expr ge sp e m le a x ->
x = (
Eval (
Vint n)).
Proof.
unfold is_intconst;
intros until n;
intros LC.
destruct a;
try discriminate.
destruct o;
try discriminate.
destruct e0;
try discriminate.
inv LC.
intros.
InvEval.
reflexivity.
Qed.
Remark eval_shift_imm:
forall (
P:
expr ->
Prop)
n a0 a1 a2 a3,
(
n =
Int.zero ->
P a0) ->
(0 <=
Int.unsigned n <
Int.zwordsize ->
Int.ltu n Int.iwordsize =
true ->
Int.ltu (
Int.sub Int.iwordsize n)
Int.iwordsize =
true ->
Int.ltu n Int64.iwordsize' =
true ->
P a1) ->
(
Int.zwordsize <=
Int.unsigned n <
Int64.zwordsize ->
Int.ltu (
Int.sub n Int.iwordsize)
Int.iwordsize =
true ->
P a2) ->
P a3 ->
P (
if Int.eq n Int.zero then a0
else if Int.ltu n Int.iwordsize then a1
else if Int.ltu n Int64.iwordsize'
then a2
else a3).
Proof.
Lemma eval_shllimm:
forall n,
unary_constructor_sound (
fun e =>
shllimm hf e n) (
fun v =>
Val.shll v (
Eval (
Vint n))).
Proof.
Theorem eval_shll:
binary_constructor_sound (
shll hf)
Val.shll.
Proof.
Ltac build_trans e :=
match e with
|
Eunop ?
u ?
t ?
f =>
let e' :=
build_trans f in
constr:(
Eunop u t e')
|
Ebinop ?
b ?
t ?
s ?
f1 ?
f2 =>
let f1' :=
build_trans f1 in
let f2' :=
build_trans f2 in
constr:(
Ebinop b t s f1'
f2')
|
_ =>
let a' :=
match goal with
|
H:
Val.lessdef ?
a e |-
_ =>
build_trans a
| |-
_ =>
e
end
in constr:(
a')
end.
Ltac ldt' :=
repeat match goal with
|-
Val.lessdef ?
c (
Ebinop ?
o ?
t ?
s ?
b ?
d) =>
let b' :=
build_trans b in
let d' :=
build_trans d in
apply Val.lessdef_trans with
(
v2:=
Ebinop o t s b'
d');
[|
repeat (
ldt;
apply Val.lessdef_binop;
auto)]
end.
Lemma eval_shrluimm:
forall n,
unary_constructor_sound (
fun e =>
shrluimm hf e n)
(
fun v =>
Val.shrlu v (
Eval (
Vint n))).
Proof.
Theorem eval_shrlu:
binary_constructor_sound (
shrlu hf)
Val.shrlu.
Proof.
Lemma eval_shrlimm:
forall n,
unary_constructor_sound
(
fun e =>
shrlimm hf e n)
(
fun v =>
Val.shrl v (
Eval (
Vint n))).
Proof.
Theorem eval_shrl:
binary_constructor_sound (
shrl hf)
Val.shrl.
Proof.
Theorem eval_addl:
binary_constructor_sound (
addl hf)
Val.addl.
Proof.
Theorem eval_subl:
binary_constructor_sound (
subl hf)
Val.subl.
Proof.
Lemma eval_mull_base:
binary_constructor_sound (
mull_base hf)
Val.mull.
Proof.
Lemma eval_mullimm:
forall n,
unary_constructor_sound
(
fun a =>
mullimm hf a n)
(
fun v =>
Val.mull v (
Eval (
Vlong n))).
Proof.
Theorem eval_mull:
binary_constructor_sound (
mull hf)
Val.mull.
Proof.
Lemma eval_binop_long:
forall id sem le a b x y z,
(
forall p q,
Val.lessdef x (
Eval (
Vlong p)) ->
Val.lessdef y (
Eval (
Vlong q)) ->
Val.lessdef z (
Eval (
Vlong (
sem p q)))) ->
helper_implements ge id sig_ll_l (
x::
y::
nil)
z ->
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
exists v,
eval_expr ge sp e m le (
binop_long id sem a b)
v /\
Val.lessdef z v.
Proof.
Theorem eval_divl:
binary_constructor_sound (
divl hf)
Val.divls.
Proof.
red;
intros.
unfold divl.
eapply eval_binop_long;
eauto.
red;
intros;
simpl;
seval;
try constructor.
destr;
try constructor.
specialize (
H1 alloc em).
rewrite Heqv in H1.
specialize (
H2 alloc em).
rewrite Heqv0 in H2.
simpl in *.
inv H1.
inv H2.
auto.
UseHelper.
Qed.
Theorem eval_modl:
binary_constructor_sound (
modl hf)
Val.modls.
Proof.
red;
intros.
eapply eval_binop_long;
eauto.
red;
intros;
simpl;
seval;
try constructor.
destr;
try constructor.
specialize (
H1 alloc em).
rewrite Heqv in H1.
specialize (
H2 alloc em).
rewrite Heqv0 in H2.
simpl in *.
inv H1.
inv H2.
auto.
UseHelper.
Qed.
Theorem eval_divlu:
binary_constructor_sound (
divlu hf)
Val.divlu.
Proof.
Theorem eval_modlu:
binary_constructor_sound (
modlu hf)
Val.modlu.
Proof.
Lemma eval_cmpl_eq_zero':
unary_constructor_sound (
cmpl_eq_zero) (
fun x =>
Val.cmpl Ceq x (
Eval (
Vlong Int64.zero))).
Proof.
Lemma eval_cmpl_ne_zero':
unary_constructor_sound cmpl_ne_zero (
fun x =>
Val.cmpl Cne x (
Eval (
Vlong Int64.zero))).
Proof.
Lemma eval_cmplu_gen':
forall ch cl,
binary_constructor_sound
(
cmplu_gen ch cl)
(
fun va vb =>
(
Val.add
(
Val.mul
(
Val.cmp Ceq (
Val.hiword va) (
Val.hiword vb))
(
Val.cmpu cl (
Val.loword va) (
Val.loword vb)))
(
Val.mul
(
Val.cmp Cne (
Val.hiword va) (
Val.hiword vb))
(
Val.cmpu ch (
Val.hiword va) (
Val.hiword vb))))).
Proof.
Theorem eval_cmplu:
forall c,
binary_constructor_sound (
cmplu c) (
Val.cmplu c).
Proof.
Lemma eval_cmpl_gen':
forall ch cl,
binary_constructor_sound
(
cmpl_gen ch cl)
(
fun va vb =>
(
Val.add
(
Val.mul
(
Val.cmp Ceq (
Val.hiword va) (
Val.hiword vb))
(
Val.cmpu cl (
Val.loword va) (
Val.loword vb)))
(
Val.mul
(
Val.cmp Cne (
Val.hiword va) (
Val.hiword vb))
(
Val.cmp ch (
Val.hiword va) (
Val.hiword vb))))).
Proof.
Theorem eval_cmpl:
forall c,
binary_constructor_sound (
cmpl c) (
Val.cmpl c).
Proof.
End CMCONSTR.