Correctness of instruction selection for 64-bit integer operations
Require Import String Coqlib Maps Zbits Integers Floats Errors.
Require Archi.
Require Import AST Values Memory Globalenvs Events.
Require Import Cminor Op CminorSel.
Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
Require Import SelectLong.
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_notl:
unary_constructor_sound notl Val.notl.
Proof.
Theorem eval_andlimm:
forall n,
unary_constructor_sound (
andlimm n) (
fun v =>
Val.andl v (
Vlong n)).
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_rolml:
forall amount mask,
unary_constructor_sound (
fun v =>
rolml v amount mask) (
fun v =>
Val.rolml v amount mask).
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_negl:
unary_constructor_sound negl Val.negl.
Proof.
Theorem eval_addlimm:
forall n,
unary_constructor_sound (
addlimm n) (
fun v =>
Val.addl v (
Vlong n)).
Proof.
Theorem eval_addl:
binary_constructor_sound addl Val.addl.
Proof.
Theorem eval_subl:
binary_constructor_sound subl Val.subl.
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 :
val,
eval_expr ge sp e m le (
Eop Omull (
a :::
longconst n :::
Enil))
v
/\
Val.lessdef (
Val.mull x (
Vlong n))
v).
{
TrivialExists.
constructor.
eauto.
constructor.
apply eval_longconst.
constructor.
auto. }
generalize (
Int64.one_bits'
_decomp n);
intros D.
destruct (
Int64.one_bits'
n)
as [ |
i [ |
j [ | ? ? ]]]
eqn:
B;
auto.
-
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.
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_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_divls_base:
partial_binary_constructor_sound divls_base Val.divls.
Proof.
Lemma eval_modl_aux:
forall divop semdivop,
(
forall sp x y m,
eval_operation ge sp divop (
x ::
y ::
nil)
m =
semdivop x y) ->
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 ->
semdivop x y =
Some z ->
eval_expr ge sp e m le (
modl_aux divop a b) (
Val.subl x (
Val.mull z y)).
Proof.
Theorem eval_modls_base:
partial_binary_constructor_sound modls_base Val.modls.
Proof.
Theorem eval_divlu_base:
partial_binary_constructor_sound divlu_base Val.divlu.
Proof.
Theorem eval_modlu_base:
partial_binary_constructor_sound modlu_base Val.modlu.
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:
forall le a x y,
eval_expr ge sp e m le a x ->
Val.longoffloat x =
Some y ->
exists v,
eval_expr ge sp e m le (
longoffloat a)
v /\
Val.lessdef y v.
Proof.
Theorem eval_floatoflong:
forall le a x y,
eval_expr ge sp e m le a x ->
Val.floatoflong x =
Some y ->
exists v,
eval_expr ge sp e m le (
floatoflong a)
v /\
Val.lessdef y v.
Proof.
Theorem eval_longofsingle:
forall le a x y,
eval_expr ge sp e m le a x ->
Val.longofsingle x =
Some y ->
exists v,
eval_expr ge sp e m le (
longofsingle a)
v /\
Val.lessdef y v.
Proof.
End CMCONSTR.