Correctness of instruction selection for 64-bit integer operations
Require Import String Coqlib Maps Integers Floats Errors.
Require Archi.
Require Import AST Values ExtValues Memory Globalenvs Events.
Require Import Cminor Op CminorSel.
Require Import OpHelpers OpHelpersproof.
Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
Require Import SelectLong.
Require Import DecBoolOps.
Require Import Lia.
Local Open Scope cminorsel_scope.
Local Open Scope string_scope.
Correctness of the instruction selection functions for 64-bit operators
Section CMCONSTR.
Variable prog:
program.
Variable hf:
helper_functions.
Hypothesis HELPERS:
helper_functions_declared prog hf.
Let ge :=
Genv.globalenv prog.
Variable sp:
val.
Variable e:
env.
Variable m:
mem.
Definition unary_constructor_sound (
cstr:
expr ->
expr) (
sem:
val ->
val) :
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:
val ->
val ->
val) :
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.
Definition partial_unary_constructor_sound (
cstr:
expr ->
expr) (
sem:
val ->
option val) :
Prop :=
forall le a x y,
eval_expr ge sp e m le a x ->
sem x =
Some y ->
exists v,
eval_expr ge sp e m le (
cstr a)
v /\
Val.lessdef y v.
Definition partial_binary_constructor_sound (
cstr:
expr ->
expr ->
expr) (
sem:
val ->
val ->
option val) :
Prop :=
forall le a x b y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
sem x y =
Some z ->
exists v,
eval_expr ge sp e m le (
cstr a b)
v /\
Val.lessdef z v.
Theorem eval_longconst:
forall le n,
eval_expr ge sp e m le (
longconst n) (
Vlong n).
Proof.
Lemma is_longconst_sound:
forall v a n le,
is_longconst a =
Some n ->
eval_expr ge sp e m le a v ->
v =
Vlong n.
Proof with
Theorem eval_intoflong:
unary_constructor_sound intoflong Val.loword.
Proof.
Theorem eval_longofintu:
unary_constructor_sound longofintu Val.longofintu.
Proof.
Theorem eval_longofint:
unary_constructor_sound longofint Val.longofint.
Proof.
Theorem eval_negl:
unary_constructor_sound negl Val.negl.
Proof.
Theorem eval_addlimm_shllimm:
forall sh k2,
unary_constructor_sound (
addlimm_shllimm sh k2) (
fun x =>
ExtValues.addxl sh x (
Vlong k2)).
Proof.
Theorem eval_addlimm:
forall n,
unary_constructor_sound (
addlimm n) (
fun v =>
Val.addl v (
Vlong n)).
Proof.
Lemma eval_addxl:
forall n,
binary_constructor_sound (
addl_shllimm n) (
ExtValues.addxl n).
Proof.
Theorem eval_addl:
binary_constructor_sound addl Val.addl.
Proof.
Theorem eval_subl:
binary_constructor_sound subl Val.subl.
Proof.
Theorem eval_shllimm:
forall n,
unary_constructor_sound (
fun e =>
shllimm e n) (
fun v =>
Val.shll v (
Vint n)).
Proof.
Theorem eval_shrluimm:
forall n,
unary_constructor_sound (
fun e =>
shrluimm e n) (
fun v =>
Val.shrlu v (
Vint n)).
Proof.
Theorem eval_shrlimm:
forall n,
unary_constructor_sound (
fun e =>
shrlimm e n) (
fun v =>
Val.shrl v (
Vint n)).
Proof.
Theorem eval_shll:
binary_constructor_sound shll Val.shll.
Proof.
Theorem eval_shrlu:
binary_constructor_sound shrlu Val.shrlu.
Proof.
Theorem eval_shrl:
binary_constructor_sound shrl Val.shrl.
Proof.
Theorem eval_mullimm_base:
forall n,
unary_constructor_sound (
mullimm_base n) (
fun v =>
Val.mull v (
Vlong n)).
Proof.
intros;
unfold mullimm_base.
red;
intros.
assert (
DEFAULT:
exists v,
eval_expr ge sp e m le (
Eop Omull (
a :::
longconst n :::
Enil))
v
/\
Val.lessdef (
Val.mull x (
Vlong n))
v).
{
econstructor;
split.
EvalOp.
constructor.
eauto.
constructor.
apply eval_longconst.
constructor.
simpl;
eauto.
auto. }
generalize (
Int64.one_bits'_decomp n);
intros D.
destruct (
Int64.one_bits' n)
as [ |
i [ |
j [ | ? ? ]]]
eqn:
B.
-
TrivialExists.
-
replace (
Val.mull x (
Vlong n))
with (
Val.shll x (
Vint i)).
apply eval_shllimm;
auto.
simpl in D.
rewrite D,
Int64.add_zero.
destruct x;
simpl;
auto.
rewrite (
Int64.one_bits'_range n)
by (
rewrite B;
auto with coqlib).
rewrite Int64.shl'_mul;
auto.
-
set (
le' :=
x ::
le).
assert (
A0:
eval_expr ge sp e m le' (
Eletvar O)
x)
by (
constructor;
reflexivity).
exploit (
eval_shllimm i).
eexact A0.
intros (
v1 &
A1 &
B1).
exploit (
eval_shllimm j).
eexact A0.
intros (
v2 &
A2 &
B2).
exploit (
eval_addl).
eexact A1.
eexact A2.
intros (
v3 &
A3 &
B3).
exists v3;
split.
econstructor;
eauto.
rewrite D.
simpl.
rewrite Int64.add_zero.
destruct x;
auto.
simpl in *.
rewrite (
Int64.one_bits'_range n)
in B1 by (
rewrite B;
auto with coqlib).
rewrite (
Int64.one_bits'_range n)
in B2 by (
rewrite B;
auto with coqlib).
inv B1;
inv B2.
simpl in B3;
inv B3.
rewrite Int64.mul_add_distr_r.
rewrite <- !
Int64.shl'_mul.
auto.
-
TrivialExists.
Qed.
Theorem eval_mullimm:
forall n,
unary_constructor_sound (
mullimm n) (
fun v =>
Val.mull v (
Vlong n)).
Proof.
Theorem eval_mull:
binary_constructor_sound mull Val.mull.
Proof.
Theorem eval_mullhu:
forall n,
unary_constructor_sound (
fun a =>
mullhu a n) (
fun v =>
Val.mullhu v (
Vlong n)).
Proof.
Theorem eval_mullhs:
forall n,
unary_constructor_sound (
fun a =>
mullhs a n) (
fun v =>
Val.mullhs v (
Vlong n)).
Proof.
Theorem eval_andlimm:
forall n,
unary_constructor_sound (
andlimm n) (
fun v =>
Val.andl v (
Vlong n)).
Proof.
Lemma int64_eq_commut:
forall x y :
int64,
(
Int64.eq x y) = (
Int64.eq y x).
Proof.
Theorem eval_andl:
binary_constructor_sound andl Val.andl.
Proof.
Theorem eval_orlimm:
forall n,
unary_constructor_sound (
orlimm n) (
fun v =>
Val.orl v (
Vlong n)).
Proof.
Theorem eval_orl:
binary_constructor_sound orl Val.orl.
Proof.
Theorem eval_xorlimm:
forall n,
unary_constructor_sound (
xorlimm n) (
fun v =>
Val.xorl v (
Vlong n)).
Proof.
Theorem eval_xorl:
binary_constructor_sound xorl Val.xorl.
Proof.
Theorem eval_notl:
unary_constructor_sound notl Val.notl.
Proof.
assert (
forall v,
Val.lessdef (
Val.notl (
Val.notl v))
v).
destruct v;
simpl;
auto.
rewrite Int64.not_involutive;
auto.
unfold notl;
red;
intros until x;
case (
notl_match a);
intros;
InvEval.
-
TrivialExists;
simpl;
congruence.
-
TrivialExists;
simpl;
congruence.
-
TrivialExists;
simpl;
congruence.
-
TrivialExists;
simpl;
congruence.
-
TrivialExists;
simpl;
congruence.
-
TrivialExists;
simpl;
congruence.
-
subst x.
exists (
Val.andl v1 v0);
split;
trivial.
econstructor.
constructor.
eassumption.
constructor.
eassumption.
constructor.
simpl.
reflexivity.
-
subst x.
exists (
Val.andl v1 (
Vlong n));
split;
trivial.
econstructor.
constructor.
eassumption.
constructor.
simpl.
reflexivity.
-
subst x.
exists (
Val.orl v1 v0);
split;
trivial.
econstructor.
constructor.
eassumption.
constructor.
eassumption.
constructor.
simpl.
reflexivity.
-
subst x.
exists (
Val.orl v1 (
Vlong n));
split;
trivial.
econstructor.
constructor.
eassumption.
constructor.
simpl.
reflexivity.
-
subst x.
exists (
Val.xorl v1 v0);
split;
trivial.
econstructor.
constructor.
eassumption.
constructor.
eassumption.
constructor.
simpl.
reflexivity.
-
subst x.
exists (
Val.xorl v1 (
Vlong n));
split;
trivial.
econstructor.
constructor.
eassumption.
constructor.
simpl.
reflexivity.
-
subst x.
TrivialExists.
simpl.
destruct v0;
destruct v1;
simpl;
trivial.
f_equal.
f_equal.
rewrite Int64.not_and_or_not.
rewrite Int64.not_involutive.
apply Int64.or_commut.
-
subst x.
TrivialExists.
simpl.
destruct v1;
simpl;
trivial.
f_equal.
f_equal.
rewrite Int64.not_and_or_not.
rewrite Int64.not_involutive.
reflexivity.
-
subst x.
TrivialExists.
simpl.
destruct v0;
destruct v1;
simpl;
trivial.
f_equal.
f_equal.
rewrite Int64.not_or_and_not.
rewrite Int64.not_involutive.
apply Int64.and_commut.
-
subst x.
TrivialExists.
simpl.
destruct v1;
simpl;
trivial.
f_equal.
f_equal.
rewrite Int64.not_or_and_not.
rewrite Int64.not_involutive.
reflexivity.
-
subst x.
exists v1;
split;
trivial.
-
TrivialExists.
-
TrivialExists.
Qed.
Theorem eval_divls_base:
forall le a b x y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.divls x y =
Some z ->
exists v,
eval_expr ge sp e m le (
divls_base a b)
v /\
Val.lessdef z v.
Proof.
Theorem eval_modls_base:
forall le a b x y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.modls x y =
Some z ->
exists v,
eval_expr ge sp e m le (
modls_base a b)
v /\
Val.lessdef z v.
Proof.
Theorem eval_divlu_base:
forall le a b x y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.divlu x y =
Some z ->
exists v,
eval_expr ge sp e m le (
divlu_base a b)
v /\
Val.lessdef z v.
Proof.
Theorem eval_modlu_base:
forall le a b x y z,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.modlu x y =
Some z ->
exists v,
eval_expr ge sp e m le (
modlu_base a b)
v /\
Val.lessdef z v.
Proof.
Theorem eval_shrxlimm:
forall le a n x z,
eval_expr ge sp e m le a x ->
Val.shrxl x (
Vint n) =
Some z ->
exists v,
eval_expr ge sp e m le (
shrxlimm a n)
v /\
Val.lessdef z v.
Proof.
Theorem eval_cmplu:
forall c le a x b y v,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.cmplu (
Mem.valid_pointer m)
c x y =
Some v ->
eval_expr ge sp e m le (
cmplu c a b)
v.
Proof.
Theorem eval_cmpl:
forall c le a x b y v,
eval_expr ge sp e m le a x ->
eval_expr ge sp e m le b y ->
Val.cmpl c x y =
Some v ->
eval_expr ge sp e m le (
cmpl c a b)
v.
Proof.
Theorem eval_longoffloat:
partial_unary_constructor_sound longoffloat Val.longoffloat.
Proof.
unfold longoffloat;
red;
intros.
TrivialExists.
simpl.
rewrite H0.
reflexivity.
Qed.
Theorem eval_longuoffloat:
partial_unary_constructor_sound longuoffloat Val.longuoffloat.
Proof.
unfold longuoffloat;
red;
intros.
TrivialExists.
simpl.
rewrite H0.
reflexivity.
Qed.
Theorem eval_floatoflong:
partial_unary_constructor_sound floatoflong Val.floatoflong.
Proof.
unfold floatoflong;
red;
intros.
TrivialExists.
simpl.
rewrite H0.
reflexivity.
Qed.
Theorem eval_floatoflongu:
partial_unary_constructor_sound floatoflongu Val.floatoflongu.
Proof.
unfold floatoflongu;
red;
intros.
TrivialExists.
simpl.
rewrite H0.
reflexivity.
Qed.
Theorem eval_longofsingle:
partial_unary_constructor_sound longofsingle Val.longofsingle.
Proof.
Theorem eval_longuofsingle:
partial_unary_constructor_sound longuofsingle Val.longuofsingle.
Proof.
Theorem eval_singleoflong:
partial_unary_constructor_sound singleoflong Val.singleoflong.
Proof.
Theorem eval_singleoflongu:
partial_unary_constructor_sound singleoflongu Val.singleoflongu.
Proof.
End CMCONSTR.