Require Import Integers Floats Op Registers Memory Values.
Require Import Coqlib OptionMonad Lia.
Require Import Asmgen Asmgenproof1.
Require Import BTL BTL_SEtheory BTL_SEsimuref BTL_SEsimplify ImpHCons.
Require Import IntPromotionCommon.
Require Import FunInd.
Import Notations.
Import SvalNotations.
Import PureComparisons.
Local Open Scope impure_scope.
Proofs for affine operations
Theory of affine values
Lemma mull_two_addl l:
Val.mull (
Vlong (
Int64.repr 2)) (
Vlong l) =
Val.addl (
Vlong l) (
Vlong l).
Proof.
Lemma addl_neutral_protected v1 v2:
Val.addl v1 v2 =
Val.addl v1 (
Val.addl v2 (
Vlong Int64.zero)).
Proof.
Lemma mull_shll_lone v n:
Int.ltu n Int64.iwordsize' =
true ->
Val.mull v (
Vlong (
Int64.shl' Int64.one n)) =
Val.shll v (
Vint n).
Proof.
unfold Val.mull,
Val.shll;
autodestruct.
intros _
LTU;
rewrite LTU;
clear LTU;
f_equal.
symmetry;
apply Int64.shl'_mul.
Qed.
Local Open Scope hashlist_full.
Local Open Scope option_monad_scope.
Import ListNotations.
Decomposing properties about affine symbolic values
Remark select_op_aff64_rv_correct op:
select_op_aff64_rv op =
true ->
op =
Oaddl.
Proof.
functional inversion 1. reflexivity.
Qed.
Remark is_aff64_rv_correct sv op lsv sv0:
is_aff64_rv sv =
Some (
op,
lsv,
sv0) ->
exists hid,
sv =
Sfoldr op lsv sv0 hid /\
select_op_aff64_rv op =
true.
Proof.
Remark find_subterm_aff64_rv_inl sv l:
find_subterm_aff64_rv sv =
Some (
inl l) ->
exists h1 h2,
sv =
Sop (
Olongconst l) [ \
h1 ]
h2.
Proof.
functional inversion 1. eauto.
Qed.
Remark find_term_const_aff64_rv_correct sv1 sv2:
forall l sv3,
find_term_const_aff64_rv sv1 sv2 =
Some (
l,
sv3) ->
exists h1 h2,
sv1 =
Sop (
Olongconst l) [ \
h1 ]
h2 /\
sv2 =
sv3 \/
sv2 =
Sop (
Olongconst l) [ \
h1 ]
h2 /\
sv1 =
sv3.
Proof.
Affine accumulation properties
Definition accv_aff64_rv v1 v2 :=
Val.addl v1 v2.
Remark accv_aff64_rv_eval:
forall ctx v1 v2 op,
select_op_aff64_rv op =
true ->
eval_operation (
cge ctx) (
csp ctx)
op [
v1;
v2] (
cm1 ctx) =
Some (
accv_aff64_rv v1 v2).
Proof.
Local Hint Resolve accv_aff64_rv_eval:
core.
Remark accv_aff64_rv_commut:
forall v1 v2,
accv_aff64_rv v1 v2 =
accv_aff64_rv v2 v1.
Proof.
Local Hint Resolve accv_aff64_rv_commut:
core.
Remark accv_aff64_rv_assoc:
forall v1 v2 v3,
accv_aff64_rv v1 (
accv_aff64_rv v2 v3) =
accv_aff64_rv (
accv_aff64_rv v1 v2)
v3.
Proof.
Local Hint Resolve accv_aff64_rv_assoc:
core.
Remark accv_mul_increment ctx sv1 sv2 sv3 sv4 i:
find_mul_aff64_rv sv1 =
Some (
i,
sv2) ->
sv1 =
sv3 /\
sv2 =
sv4 \/
sv1 =
sv4 /\
sv2 =
sv3 ->
eval_sval ctx (
build_mul_aff64_rv (
build_const_aff64_rv
(
Int64.add Int64.one i))
sv2) =
(
SOME v1 <-
eval_sval ctx sv3
IN SOME v2 <-
eval_sval ctx sv4 IN Some (
accv_aff64_rv v1 v2)).
Proof.
Affine scale properties
Definition scalev_aff64_rv l v :=
Val.mull l v.
Remark scalev_aff64_rv_distr:
forall ctx op vl v1 scv1 v2,
select_op_aff64_rv op =
true ->
scalev_aff64_rv vl v1 =
scv1 ->
eval_operation (
cge ctx) (
csp ctx)
op [
scv1;
scalev_aff64_rv vl v2]
(
cm1 ctx) =
(
SOME vr <-
eval_operation (
cge ctx) (
csp ctx)
op [
v1;
v2] (
cm1 ctx)
IN Some (
scalev_aff64_rv vl vr)).
Proof.
Local Hint Resolve scalev_aff64_rv_distr:
core.
Remark scale_aff64_rv_correct:
forall ctx l sv,
eval_sval ctx (
scale_aff64_rv l sv) =
(
SOME v <-
eval_sval ctx sv IN Some (
scalev_aff64_rv (
Vlong l)
v)).
Proof.
Local Hint Resolve scale_aff64_rv_correct:
core.
Compare, merge, and "acc0" (addition over the constant term of Sfoldr)
Lemma compare_aff64_rv_correct ctx sv1 sv2 sv3:
compare_aff64_rv sv1 sv2 =
Eq ->
merge_aff64_rv sv1 sv2 =
Some sv3 ->
eval_sval ctx (
sv3) =
(
SOME v1 <-
eval_sval ctx sv1
IN SOME v2 <-
eval_sval ctx sv2 IN Some (
accv_aff64_rv v1 v2)).
Proof.
Local Hint Resolve compare_aff64_rv_correct:
core.
Lemma acc0_aff64_rv_correct:
forall ctx sv1 sv2,
eval_sval ctx (
acc0_aff64_rv sv1 sv2) =
(
SOME v1 <-
eval_sval ctx sv1
IN SOME v2 <-
eval_sval ctx sv2 IN Some (
accv_aff64_rv v1 v2)).
Proof.
Local Hint Resolve acc0_aff64_rv_correct:
core.
Convertion of symbolic values to affine terms
Remark foldrof_aff64_rv_break sv op lsv sv0:
foldrof_aff64_rv sv = (
op,
lsv,
sv0) ->
is_aff64_rv sv =
Some (
op,
lsv,
sv0) \/
(
exists l,
find_subterm_aff64_rv sv =
Some (
inl l) /\
op =
op_aff64_rv /\
lsv =
fSnil /\
sv0 =
build_const_aff64_rv l) \/
let lsv' :=
build_flsv_single sv in
(
op,
lsv,
sv0) = (
op_aff64_rv,
lsv',
build_const_aff64_rv Int64.zero).
Proof.
unfold foldrof_aff64_rv;
repeat autodestruct;
intros;
subst;
inv H;
auto.
right;
left;
exists i;
auto.
Qed.
Lemma foldrof_aff64_rv_correct ctx sv1 sv2 v1 v2 op1 op2 lsv1 lsv2 sv0_1 sv0_2:
eval_sval ctx sv1 =
Some v1 ->
eval_sval ctx sv2 =
Some v2 ->
foldrof_aff64_rv sv1 = (
op1,
lsv1,
sv0_1) ->
foldrof_aff64_rv sv2 = (
op2,
lsv2,
sv0_2) ->
exists v1' v2',
eval_sval ctx (
fSfoldr op1 lsv1 sv0_1) =
Some v1' /\
eval_sval ctx (
fSfoldr op2 lsv2 sv0_2) =
Some v2' /\
accv_aff64_rv v1 v2 =
accv_aff64_rv v1' v2'.
Proof.
Addition over affine terms
Theorem add_foldr_aff64_rv_correct sv1 sv2:
forall fsv v1 v2 ctx,
add_foldr_aff64_rv sv1 sv2 =
Some fsv ->
eval_sval ctx sv1 =
Some v1 ->
eval_sval ctx sv2 =
Some v2 ->
eval_sval ctx fsv =
Some (
Val.addl v1 v2).
Proof.
Lemma sr_addl_correct (
ctx:
iblock_common_context)
args fsv lsv l hlsv:
forall
(
H:
match lsv with
|
nil =>
None
|
sv1 ::
nil =>
None
|
sv1 ::
sv2 ::
nil =>
add_foldr_aff64_rv sv1 sv2
|
sv1 ::
sv2 :: _ :: _ =>
None
end =
Some fsv)
(
LMAP:
lmap_sv (
fun sv :
sval =>
Some sv)
lsv =
Some l)
(
ELSVEQ:
eval_list_sval ctx l =
eval_list_sval ctx hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx)
Oaddl args (
cm1 ctx).
Proof.
repeat (
destruct lsv;
try congruence);
simpl.
intros AFF X1 ELSVEQ OK;
inv X1.
simpl in ELSVEQ;
revert ELSVEQ;
do 2
autodestruct;
intros.
rewrite <-
ELSVEQ in OK;
inv OK.
apply (
add_foldr_aff64_rv_correct s s0);
auto.
Qed.
Lemma sr_addlimm_correct (
ctx:
iblock_common_context)
args fsv lsv l hlsv n:
forall
(
H:
match lsv with
|
nil =>
None
|
sv ::
nil =>
add_foldr_aff64_rv (
build_const_aff64_rv n)
sv
|
sv :: _ :: _ =>
None
end =
Some fsv)
(
LMAP:
lmap_sv (
fun sv :
sval =>
Some sv)
lsv =
Some l)
(
ELSVEQ:
eval_list_sval ctx l =
eval_list_sval ctx hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx) (
Oaddlimm n)
args (
cm1 ctx).
Proof.
Multiplication over affine terms
Theorem find_term_const_rescale_correct sv1 sv2:
forall l sv3 v1 v2 ctx,
find_term_const_aff64_rv sv1 sv2 =
Some (
l,
sv3) ->
eval_sval ctx sv1 =
Some v1 ->
eval_sval ctx sv2 =
Some v2 ->
eval_sval ctx (
rescale select_op_aff64_rv (
scale_aff64_rv l)
sv3)
=
Some (
Val.mull v1 v2).
Proof.
Lemma sr_mull_correct (
ctx:
iblock_common_context)
args fsv lsv l hlsv:
forall
(
H:
match lsv with
|
nil =>
None
|
sv1 ::
nil =>
None
|
sv1 ::
sv2 ::
nil =>
match find_term_const_aff64_rv sv1 sv2 with
|
Some (
l2,
sv) =>
Some (
rescale select_op_aff64_rv (
scale_aff64_rv l2)
sv)
|
None =>
None
end
|
sv1 ::
sv2 :: _ :: _ =>
None
end =
Some fsv)
(
LMAP:
lmap_sv (
fun sv :
sval =>
Some sv)
lsv =
Some l)
(
ELSVEQ:
eval_list_sval ctx l =
eval_list_sval ctx hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx)
Omull args (
cm1 ctx).
Proof.
repeat (
destruct lsv;
try congruence);
simpl.
do 2
autodestruct;
intros p1 FIND X1 X2 ELSVEQ OK;
subst;
inv X1;
inv X2.
simpl in ELSVEQ;
revert ELSVEQ;
do 2
autodestruct;
intros.
rewrite <-
ELSVEQ in OK;
inv OK.
apply (
find_term_const_rescale_correct s s0);
auto.
Qed.
Lemma sr_shllimm_correct (
ctx:
iblock_common_context)
args fsv lsv l n hlsv:
forall
(
H:
match lsv with
|
nil =>
None
|
sv ::
nil =>
if negb (
Int.ltu n Int64.iwordsize')
then None
else
Some (
rescale select_op_aff64_rv
(
scale_aff64_rv (
Int64.shl' Int64.one n))
sv)
|
sv :: _ :: _ =>
None
end =
Some fsv)
(
LMAP:
lmap_sv (
fun sv :
sval =>
Some sv)
lsv =
Some l)
(
ELSVEQ:
eval_list_sval ctx l =
eval_list_sval ctx hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx) (
Oshllimm n)
args (
cm1 ctx).
Proof.
Lemma op_strength_reduction_correct ctx op lsv l hlsv fsv args:
forall
(
H:
op_strength_reduction op lsv =
Some fsv)
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
lsv =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx)
op args (
cm1 ctx).
Proof.
Global Opaque op_strength_reduction.
Local Hint Resolve op_strength_reduction_correct:
core.
Auxiliary lemmas on comparisons
Signed ints
Lemma xor_neg_ltle_cmp:
forall v1 v2,
Some (
Val.xor (
Val.cmp Clt v1 v2) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmp_bool Cle v2 v1)).
Proof.
Local Hint Resolve xor_neg_ltle_cmp:
core.
Unsigned ints
Lemma xor_neg_ltle_cmpu:
forall mptr v1 v2,
Some (
Val.xor (
Val.cmpu (
Mem.valid_pointer mptr)
Clt v1 v2) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmpu_bool (
Mem.valid_pointer mptr)
Cle v2 v1)).
Proof.
Local Hint Resolve xor_neg_ltle_cmpu:
core.
Remark ltu_12_wordsize:
Int.ltu (
Int.repr 12)
Int.iwordsize =
true.
Proof.
Local Hint Resolve ltu_12_wordsize:
core.
Signed longs
Lemma xor_neg_ltle_cmpl:
forall v1 v2,
Some (
Val.xor (
Val.maketotal (
Val.cmpl Clt v1 v2)) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmpl_bool Cle v2 v1)).
Proof.
intros.
eapply f_equal.
destruct v1,
v2;
simpl;
try congruence.
destruct (
Int64.lt _ _);
auto.
Qed.
Local Hint Resolve xor_neg_ltle_cmpl:
core.
Lemma xor_neg_ltge_cmpl:
forall v1 v2,
Some (
Val.xor (
Val.maketotal (
Val.cmpl Clt v1 v2)) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmpl_bool Cge v1 v2)).
Proof.
intros.
eapply f_equal.
destruct v1,
v2;
simpl;
try congruence.
destruct (
Int64.lt _ _);
auto.
Qed.
Local Hint Resolve xor_neg_ltge_cmpl:
core.
Lemma xorl_zero_eq_cmpl:
forall c v1 v2,
c =
Ceq \/
c =
Cne ->
Some
(
Val.maketotal
(
option_map Val.of_bool
(
Val.cmpl_bool c (
Val.xorl v1 v2) (
Vlong Int64.zero)))) =
Some (
Val.of_optbool (
Val.cmpl_bool c v1 v2)).
Proof.
Local Hint Resolve xorl_zero_eq_cmpl:
core.
Lemma cmp_ltle_add_one:
forall v n,
Int.eq n (
Int.repr Int.max_signed) =
false ->
Some (
Val.of_optbool (
Val.cmp_bool Clt v (
Vint (
Int.add n Int.one)))) =
Some (
Val.of_optbool (
Val.cmp_bool Cle v (
Vint n))).
Proof.
Local Hint Resolve cmp_ltle_add_one:
core.
Lemma cmpl_ltle_add_one:
forall v n,
Int64.eq n (
Int64.repr Int64.max_signed) =
false ->
Some (
Val.of_optbool (
Val.cmpl_bool Clt v (
Vlong (
Int64.add n Int64.one)))) =
Some (
Val.of_optbool (
Val.cmpl_bool Cle v (
Vlong n))).
Proof.
Local Hint Resolve cmpl_ltle_add_one:
core.
Remark lt_maxsgn_false_int:
forall i,
Int.lt (
Int.repr Int.max_signed)
i =
false.
Proof.
Local Hint Resolve lt_maxsgn_false_int:
core.
Remark lt_maxsgn_false_long:
forall i,
Int64.lt (
Int64.repr Int64.max_signed)
i =
false.
Proof.
Local Hint Resolve lt_maxsgn_false_long:
core.
Unsigned longs
Lemma xor_neg_ltle_cmplu:
forall mptr v1 v2,
Some (
Val.xor (
Val.maketotal (
Val.cmplu (
Mem.valid_pointer mptr)
Clt v1 v2)) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmplu_bool (
Mem.valid_pointer mptr)
Cle v2 v1)).
Proof.
intros.
eapply f_equal.
destruct v1,
v2;
simpl;
try congruence.
destruct (
Int64.ltu _ _);
auto.
1,2:
unfold Val.cmplu;
simpl;
auto;
destruct (
Archi.ptr64);
simpl;
try destruct (
eq_block _ _);
simpl;
try destruct (_ && _);
simpl;
try destruct (
Ptrofs.cmpu _ _);
try destruct cmp;
simpl;
auto.
unfold Val.cmplu;
simpl;
destruct Archi.ptr64;
try destruct (_ || _);
simpl;
auto;
destruct (
eq_block b b0);
destruct (
eq_block b0 b);
try congruence;
try destruct (_ || _);
simpl;
try destruct (
Ptrofs.ltu _ _);
simpl;
auto;
repeat destruct (_ && _);
simpl;
auto.
Qed.
Local Hint Resolve xor_neg_ltle_cmplu:
core.
Lemma xor_neg_ltge_cmplu:
forall mptr v1 v2,
Some (
Val.xor (
Val.maketotal (
Val.cmplu (
Mem.valid_pointer mptr)
Clt v1 v2)) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmplu_bool (
Mem.valid_pointer mptr)
Cge v1 v2)).
Proof.
intros.
eapply f_equal.
destruct v1,
v2;
simpl;
try congruence.
destruct (
Int64.ltu _ _);
auto.
1,2:
unfold Val.cmplu;
simpl;
auto;
destruct (
Archi.ptr64);
simpl;
try destruct (
eq_block _ _);
simpl;
try destruct (_ && _);
simpl;
try destruct (
Ptrofs.cmpu _ _);
try destruct cmp;
simpl;
auto.
unfold Val.cmplu;
simpl;
destruct Archi.ptr64;
try destruct (_ || _);
simpl;
auto;
destruct (
eq_block b b0);
destruct (
eq_block b0 b);
try congruence;
try destruct (_ || _);
simpl;
try destruct (
Ptrofs.ltu _ _);
simpl;
auto;
repeat destruct (_ && _);
simpl;
auto.
Qed.
Local Hint Resolve xor_neg_ltge_cmplu:
core.
Floats
Lemma xor_neg_eqne_cmpf:
forall v1 v2,
Some (
Val.xor (
Val.cmpf Ceq v1 v2) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmpf_bool Cne v1 v2)).
Proof.
Local Hint Resolve xor_neg_eqne_cmpf:
core.
Singles
Lemma xor_neg_eqne_cmpfs:
forall v1 v2,
Some (
Val.xor (
Val.cmpfs Ceq v1 v2) (
Vint Int.one)) =
Some (
Val.of_optbool (
Val.cmpfs_bool Cne v1 v2)).
Proof.
Local Hint Resolve xor_neg_eqne_cmpfs:
core.
More useful lemmas
Lemma xor_neg_optb:
forall v,
Some (
Val.xor (
Val.of_optbool (
option_map negb v))
(
Vint Int.one)) =
Some (
Val.of_optbool v).
Proof.
intros.
destruct v; simpl; trivial.
destruct b; simpl; auto.
Qed.
Local Hint Resolve xor_neg_optb:
core.
Lemma xor_neg_optb':
forall v,
Some (
Val.xor (
Val.of_optbool v) (
Vint Int.one)) =
Some (
Val.of_optbool (
option_map negb v)).
Proof.
intros.
destruct v; simpl; trivial.
destruct b; simpl; auto.
Qed.
Local Hint Resolve xor_neg_optb':
core.
Lemma optbool_mktotal:
forall v,
Val.maketotal (
option_map Val.of_bool v) =
Val.of_optbool v.
Proof.
intros.
destruct v; simpl; auto.
Qed.
Local Hint Resolve optbool_mktotal:
core.
Intermediates lemmas on each expanded instruction
Lemma simplify_ccomp_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx (
cond_int32s c (
make_lfsv_cmp (
is_inv_cmp_int c)
s s0)
None) =
Some (
Val.of_optbool (
Val.cmp_bool c v v0)).
Proof.
Lemma simplify_ccompu_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx
(
cond_int32u c (
make_lfsv_cmp (
is_inv_cmp_int c)
s s0)
None) =
Some (
Val.of_optbool (
Val.cmpu_bool (
Mem.valid_pointer (
cm1 ctx))
c v v0)).
Proof.
Lemma simplify_ccompimm_correct (
ctx:
iblock_common_context)
c s v n:
forall
(
OKv1 :
eval_sval ctx s =
Some v),
eval_sval ctx (
expanse_condimm_int32s c s n) =
Some (
Val.of_optbool (
Val.cmp_bool c v (
Vint n))).
Proof.
intros.
unfold expanse_condimm_int32s,
cond_int32s in *;
destruct c;
intros;
destruct (
Int.eq n Int.zero)
eqn:
EQIMM;
simpl;
try apply Int.same_if_eq in EQIMM;
subst;
unfold loadimm32,
sltimm32,
xorimm32,
opimm32,
load_hilo32;
try rewrite OKv1;
unfold Val.cmp,
zero32.
all:
try apply xor_neg_ltle_cmp;
try apply xor_neg_ltge_cmp;
trivial.
4:
try destruct (
Int.eq n (
Int.repr Int.max_signed))
eqn:
EQMAX;
subst;
try apply Int.same_if_eq in EQMAX;
subst;
simpl.
4:
intros;
try (
specialize make_immed32_sound with (
Int.one);
destruct (
make_immed32 Int.one)
eqn:
EQMKI_A1);
intros;
simpl.
6:
intros;
try (
specialize make_immed32_sound with (
Int.add n Int.one);
destruct (
make_immed32 (
Int.add n Int.one))
eqn:
EQMKI_A2);
intros;
simpl.
1,2,3,8,9:
intros;
try (
specialize make_immed32_sound with (
n);
destruct (
make_immed32 n)
eqn:
EQMKI);
intros;
simpl.
all:
try destruct (
Int.eq lo Int.zero)
eqn:
EQLO32;
try apply Int.same_if_eq in EQLO32;
subst;
try rewrite OKv1;
try rewrite (
Int.add_commut _
Int.zero),
Int.add_zero_l in H;
subst;
simpl;
unfold Val.cmp,
eval_may_undef,
zero32,
Val.add;
simpl;
destruct v;
auto.
all:
try rewrite ltu_12_wordsize;
try rewrite <-
H;
try (
apply cmp_ltle_add_one;
auto);
try rewrite Int.add_commut,
Int.add_zero_l in *;
try (
simpl;
trivial;
try rewrite Int.xor_is_zero;
try destruct (
Int.lt _ _)
eqn:
EQLT;
trivial;
try rewrite lt_maxsgn_false_int in EQLT;
simpl;
trivial;
try discriminate;
fail).
Qed.
Lemma simplify_ccompuimm_correct (
ctx:
iblock_common_context)
c s v n:
forall
(
OKv1 :
eval_sval ctx s =
Some v),
eval_sval ctx (
expanse_condimm_int32u c s n) =
Some (
Val.of_optbool (
Val.cmpu_bool (
Mem.valid_pointer (
cm1 ctx))
c v (
Vint n))).
Proof.
Lemma simplify_ccompl_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx
(
cond_int64s c (
make_lfsv_cmp (
is_inv_cmp_int c)
s s0)
None) =
Some (
Val.of_optbool (
Val.cmpl_bool c v v0)).
Proof.
Lemma simplify_ccomplu_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx
(
cond_int64u c (
make_lfsv_cmp (
is_inv_cmp_int c)
s s0)
None) =
Some (
Val.of_optbool (
Val.cmplu_bool (
Mem.valid_pointer (
cm1 ctx))
c v v0)).
Proof.
Lemma simplify_ccomplimm_correct (
ctx:
iblock_common_context)
c s v n:
forall
(
OKv1 :
eval_sval ctx s =
Some v),
eval_sval ctx (
expanse_condimm_int64s c s n) =
Some (
Val.of_optbool (
Val.cmpl_bool c v (
Vlong n))).
Proof.
intros.
unfold expanse_condimm_int64s,
cond_int64s in *;
destruct c;
intros;
destruct (
Int64.eq n Int64.zero)
eqn:
EQIMM;
simpl;
try apply Int64.same_if_eq in EQIMM;
subst;
unfold loadimm32,
loadimm64,
sltimm64,
xorimm64,
opimm64,
load_hilo32,
load_hilo64;
try rewrite OKv1;
unfold Val.cmpl,
zero64.
all:
try apply xor_neg_ltle_cmpl;
try apply xor_neg_ltge_cmpl;
try rewrite optbool_mktotal;
trivial.
4:
try destruct (
Int64.eq n (
Int64.repr Int64.max_signed))
eqn:
EQMAX;
subst;
try apply Int64.same_if_eq in EQMAX;
subst;
simpl.
4:
intros;
try (
specialize make_immed32_sound with (
Int.one);
destruct (
make_immed32 Int.one)
eqn:
EQMKI_A1);
intros;
simpl.
6:
intros;
try (
specialize make_immed64_sound with (
Int64.add n Int64.one);
destruct (
make_immed64 (
Int64.add n Int64.one))
eqn:
EQMKI_A2);
intros;
simpl.
1,2,3,9,10:
intros;
try (
specialize make_immed64_sound with (
n);
destruct (
make_immed64 n)
eqn:
EQMKI);
intros;
simpl.
all:
try destruct (
Int.eq lo Int.zero)
eqn:
EQLO32;
try apply Int.same_if_eq in EQLO32;
subst;
try destruct (
Int64.eq lo Int64.zero)
eqn:
EQLO64;
try apply Int64.same_if_eq in EQLO64;
subst;
simpl;
try rewrite OKv1;
try rewrite (
Int64.add_commut _
Int64.zero),
Int64.add_zero_l in H;
subst;
unfold Val.cmpl,
Val.addl;
try rewrite optbool_mktotal;
trivial;
destruct v;
auto.
all:
try rewrite <-
optbool_mktotal;
trivial;
try rewrite Int64.add_commut,
Int64.add_zero_l in *;
try fold (
Val.cmpl Clt (
Vlong i) (
Vlong imm));
try fold (
Val.cmpl Clt (
Vlong i) (
Vlong (
Int64.sign_ext 32 (
Int64.shl hi (
Int64.repr 12)))));
try fold (
Val.cmpl Clt (
Vlong i) (
Vlong (
Int64.add (
Int64.sign_ext 32 (
Int64.shl hi (
Int64.repr 12)))
lo))).
all:
try rewrite <-
cmpl_ltle_add_one;
auto;
try rewrite ltu_12_wordsize;
try rewrite Int.add_commut,
Int.add_zero_l in *;
simpl;
try rewrite lt_maxsgn_false_long;
try (
rewrite <-
H;
trivial;
fail);
simpl;
trivial.
Qed.
Lemma simplify_ccompluimm_correct (
ctx:
iblock_common_context)
c s v n:
forall
(
OKv1 :
eval_sval ctx s =
Some v),
eval_sval ctx (
expanse_condimm_int64u c s n) =
Some (
Val.of_optbool
(
Val.cmplu_bool (
Mem.valid_pointer (
cm1 ctx))
c v (
Vlong n))).
Proof.
Lemma simplify_ccompf_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
REG_EQ :
forall r :
positive,
eval_sval ctx s =
eval_sval ctx s)
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx
(
expanse_cond_fp false cond_float c
(
make_lfsv_cmp (
is_inv_cmp_float c)
s s0)) =
Some (
Val.of_optbool (
Val.cmpf_bool c v v0)).
Proof.
Lemma simplify_cnotcompf_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
REG_EQ :
forall r :
positive,
eval_sval ctx s =
eval_sval ctx s)
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx
(
expanse_cond_fp true cond_float c
(
make_lfsv_cmp (
is_inv_cmp_float c)
s s0)) =
Some (
Val.of_optbool (
option_map negb (
Val.cmpf_bool c v v0))).
Proof.
Lemma simplify_ccompfs_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
REG_EQ :
forall r :
positive,
eval_sval ctx s =
eval_sval ctx s)
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx
(
expanse_cond_fp false cond_single c
(
make_lfsv_cmp (
is_inv_cmp_float c)
s s0)) =
Some (
Val.of_optbool (
Val.cmpfs_bool c v v0)).
Proof.
Lemma simplify_cnotcompfs_correct (
ctx:
iblock_common_context)
c s s0 v v0:
forall
(
REG_EQ :
forall r :
positive,
eval_sval ctx s =
eval_sval ctx s)
(
OKv1 :
eval_sval ctx s =
Some v)
(
OKv2 :
eval_sval ctx s0 =
Some v0),
eval_sval ctx
(
expanse_cond_fp true cond_single c
(
make_lfsv_cmp (
is_inv_cmp_float c)
s s0)) =
Some (
Val.of_optbool (
option_map negb (
Val.cmpfs_bool c v v0))).
Proof.
Lemma simplify_intconst_correct (
ctx:
iblock_common_context)
args l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
nil =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
loadimm32 n) =
eval_operation (
cge ctx) (
csp ctx) (
Ointconst n)
args (
cm1 ctx).
Proof.
Lemma simplify_longconst_correct (
ctx:
iblock_common_context)
args l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
nil =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
loadimm64 n) =
eval_operation (
cge ctx) (
csp ctx) (
Olongconst n)
args (
cm1 ctx).
Proof.
Lemma simplify_floatconst_correct (
ctx:
iblock_common_context)
args l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
nil =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
fSop Ofloat_of_bits
(
make_lfsv_single (
loadimm64 (
Float.to_bits n)))) =
eval_operation (
cge ctx) (
csp ctx) (
Ofloatconst n)
args (
cm1 ctx).
Proof.
Lemma simplify_singleconst_correct (
ctx:
iblock_common_context)
args l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
nil =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
fSop Osingle_of_bits
(
make_lfsv_single (
loadimm32 (
Float32.to_bits n)))) =
eval_operation (
cge ctx) (
csp ctx) (
Osingleconst n)
args (
cm1 ctx).
Proof.
Lemma simplify_cast8signed_correct (
ctx:
iblock_common_context)
args sv1 l hlsv:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
fSop (
Oshrimm (
Int.repr 24))
(
make_lfsv_single
(
fSop (
Oshlimm (
Int.repr 24)) (
make_lfsv_single sv1)))) =
eval_operation (
cge ctx) (
csp ctx)
Ocast8signed args (
cm1 ctx).
Proof.
Lemma simplify_cast16signed_correct (
ctx:
iblock_common_context)
args sv1 l hlsv:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
fSop (
Oshrimm (
Int.repr 16))
(
make_lfsv_single
(
fSop (
Oshlimm (
Int.repr 16)) (
make_lfsv_single sv1)))) =
eval_operation (
cge ctx) (
csp ctx)
Ocast16signed args (
cm1 ctx).
Proof.
Lemma simplify_addimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
addimm32 sv1 n None) =
eval_operation (
cge ctx) (
csp ctx) (
Oaddimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_andimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
andimm32 sv1 n) =
eval_operation (
cge ctx) (
csp ctx) (
Oandimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_orimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
orimm32 sv1 n) =
eval_operation (
cge ctx) (
csp ctx) (
Oorimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_xorimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
xorimm32 sv1 n) =
eval_operation (
cge ctx) (
csp ctx) (
Oxorimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_shrximm_correct (
ctx:
iblock_common_context)
args fsv sv1 l hlsv n:
forall
(
H : (
if Int.eq n Int.zero
then
Some
(
fSop (
OEmayundef (
MUshrx n))
(
make_lfsv_cmp false sv1 sv1))
else
if Int.eq n Int.one
then
Some
(
fSop (
OEmayundef (
MUshrx n))
(
make_lfsv_cmp false
(
fSop (
Oshrimm Int.one)
(
make_lfsv_single
(
fSop Oadd
(
make_lfsv_cmp false sv1
(
fSop (
Oshruimm (
Int.repr 31))
(
make_lfsv_single sv1))))))
(
fSop (
Oshrimm Int.one)
(
make_lfsv_single
(
fSop Oadd
(
make_lfsv_cmp false sv1
(
fSop (
Oshruimm (
Int.repr 31))
(
make_lfsv_single sv1))))))))
else
Some
(
fSop (
OEmayundef (
MUshrx n))
(
make_lfsv_cmp false
(
fSop (
Oshrimm n)
(
make_lfsv_single
(
fSop Oadd
(
make_lfsv_cmp false sv1
(
fSop (
Oshruimm (
Int.sub Int.iwordsize n))
(
make_lfsv_single
(
fSop (
Oshrimm (
Int.repr 31))
(
make_lfsv_single sv1))))))))
(
fSop (
Oshrimm n)
(
make_lfsv_single
(
fSop Oadd
(
make_lfsv_cmp false sv1
(
fSop (
Oshruimm (
Int.sub Int.iwordsize n))
(
make_lfsv_single
(
fSop (
Oshrimm (
Int.repr 31))
(
make_lfsv_single sv1)))))))))))
=
Some fsv)
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx) (
Oshrximm n)
args (
cm1 ctx).
Proof.
Lemma simplify_cast32unsigned_correct (
ctx:
iblock_common_context)
args sv1 l hlsv:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
fSop (
Oshrluimm (
Int.repr 32))
(
make_lfsv_single
(
fSop (
Oshllimm (
Int.repr 32))
(
make_lfsv_single
(
fSop Ocast32signed (
make_lfsv_single sv1)))))) =
eval_operation (
cge ctx) (
csp ctx)
Ocast32unsigned args (
cm1 ctx).
Proof.
Lemma simplify_addlimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
addimm64 sv1 n None) =
eval_operation (
cge ctx) (
csp ctx) (
Oaddlimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_andlimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
andimm64 sv1 n) =
eval_operation (
cge ctx) (
csp ctx) (
Oandlimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_orlimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
orimm64 sv1 n) =
eval_operation (
cge ctx) (
csp ctx) (
Oorlimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_xorlimm_correct (
ctx:
iblock_common_context)
args sv1 l hlsv n:
forall
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx (
xorimm64 sv1 n) =
eval_operation (
cge ctx) (
csp ctx) (
Oxorlimm n)
args (
cm1 ctx).
Proof.
Lemma simplify_shrxlimm_correct (
ctx:
iblock_common_context)
args fsv sv1 l hlsv n:
forall
(
H : (
if Int.eq n Int.zero
then
Some
(
fSop (
OEmayundef (
MUshrxl n))
(
make_lfsv_cmp false sv1 sv1))
else
if Int.eq n Int.one
then
Some
(
fSop (
OEmayundef (
MUshrxl n))
(
make_lfsv_cmp false
(
fSop (
Oshrlimm Int.one)
(
make_lfsv_single
(
fSop Oaddl
(
make_lfsv_cmp false sv1
(
fSop (
Oshrluimm (
Int.repr 63))
(
make_lfsv_single sv1))))))
(
fSop (
Oshrlimm Int.one)
(
make_lfsv_single
(
fSop Oaddl
(
make_lfsv_cmp false sv1
(
fSop (
Oshrluimm (
Int.repr 63))
(
make_lfsv_single sv1))))))))
else
Some
(
fSop (
OEmayundef (
MUshrxl n))
(
make_lfsv_cmp false
(
fSop (
Oshrlimm n)
(
make_lfsv_single
(
fSop Oaddl
(
make_lfsv_cmp false sv1
(
fSop (
Oshrluimm (
Int.sub Int64.iwordsize' n))
(
make_lfsv_single
(
fSop (
Oshrlimm (
Int.repr 63))
(
make_lfsv_single sv1))))))))
(
fSop (
Oshrlimm n)
(
make_lfsv_single
(
fSop Oaddl
(
make_lfsv_cmp false sv1
(
fSop (
Oshrluimm (
Int.sub Int64.iwordsize' n))
(
make_lfsv_single
(
fSop (
Oshrlimm (
Int.repr 63))
(
make_lfsv_single sv1)))))))))))
=
Some fsv)
(
LMAP:
lmap_sv (
fun sv =>
Some sv) (
sv1 ::
nil) =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx) (
Oshrxlimm n)
args (
cm1 ctx).
Proof.
intros.
assert (
A:
Int.ltu Int.zero (
Int.repr 63) =
true)
by auto.
assert (
B:
Int.ltu (
Int.repr 63)
Int64.iwordsize' =
true)
by auto.
assert (
C:
Int.ltu Int.one Int64.iwordsize' =
true)
by auto.
destruct (
Int.eq n Int.zero)
eqn:
EQ0;
destruct (
Int.eq n Int.one)
eqn:
EQ1.
{
apply Int.same_if_eq in EQ0.
apply Int.same_if_eq in EQ1;
subst.
discriminate. }
all:
simpl in LMAP;
inv LMAP;
simpl in *;
inv H;
destruct (
eval_sval ctx sv1)
eqn:
OKv1;
try congruence;
inv OK;
destruct (
Val.shrxl v (
Vint n))
eqn:
TOTAL;
cbn;
unfold eval_may_undef;
rewrite OKv1;
rewrite <-
ELSVEQ in H0;
inv H0.
2,4,6:
unfold Val.shrxl in TOTAL;
destruct v;
simpl in TOTAL;
simpl;
auto;
try rewrite B;
simpl;
try rewrite C;
simpl;
try destruct (
Val.shrl _ _);
destruct (
Int.ltu n (
Int.repr 63));
simpl;
try congruence.
-
destruct v;
simpl in TOTAL;
simpl;
auto;
apply Int.same_if_eq in EQ0;
subst;
rewrite A,
Int64.shrx'_zero in *.
inv TOTAL;
simpl;
reflexivity.
-
apply Int.same_if_eq in EQ1;
subst;
unfold Val.shrl,
Val.shrlu,
Val.shrxl,
Val.addl;
simpl;
destruct v;
simpl in *;
try discriminate;
trivial.
rewrite B,
C.
rewrite Int64.shrx'1_shr';
auto.
-
exploit Val.shrxl_shrl_2;
eauto.
rewrite EQ0.
intros;
subst.
destruct v;
simpl in *;
simpl;
auto.
rewrite B in *.
destruct Int.ltu eqn:
EQN0 in TOTAL;
try discriminate.
simpl in *.
destruct Int.ltu eqn:
EQN1 in TOTAL;
try discriminate.
replace Int64.iwordsize' with (
Int.repr 64)
in *
by auto.
rewrite !
EQN1.
simpl in *.
destruct Int.ltu eqn:
EQN2 in TOTAL;
try discriminate.
rewrite !
EQN2.
rewrite EQN0.
rewrite TOTAL.
reflexivity.
Qed.
Rewriting promotions
Lemma promote_sval_correct ctx sgn sv:
eval_sval ctx (
promote_sval sgn sv) =
option_map (
promote_val sgn) (
eval_sval ctx sv).
Proof.
case sgn; simpl; autodestruct; reflexivity.
Qed.
Lemma promote_svalb_correct ctx sgn sv b:
eval_sval ctx (
promote_svalb sgn sv b) =
option_map (
fun v0 =>
promote_valb sgn (
b,
v0)) (
eval_sval ctx sv).
Proof.
Lemma ok_cast_sgn_correct sgn ceq sgn' v
(
CEQ :
ceq =
true ->
val_promotes_eq v)
(
OKC :
ok_cast_sgn sgn ceq sgn' =
true):
promote_val sgn' v =
promote_val sgn v.
Proof.
apply orb_prop in OKC as [
H|
H].
-
case sgn',
sgn;
rewrite ?(
CEQ H);
reflexivity.
-
apply bool_eq_ok in H as ->;
reflexivity.
Qed.
Lemma unpromote_args_length sgn args pargs cargs lsv:
unpromote_args sgn args pargs cargs =
Some lsv ->
lsv_length lsv =
length args.
Proof.
revert pargs cargs lsv; induction args; do 3 intro; simpl;
repeat (autodestruct; intro); injection 1 as <-; simpl; f_equal; eauto.
Qed.
Lemma unpromote_arg_correct ctx sv sgn ceq b sv0
(
CEQ :
ceq =
true ->
if_Some (
eval_sval ctx sv0)
val_promotes_eq):
unpromote_arg sgn ceq sv b =
Some sv0 ->
eval_sval ctx sv =
option_map (
fun v0 =>
promote_valb sgn (
b,
v0)) (
eval_sval ctx sv0).
Proof.
Lemma unpromote_args_correct ctx sgn lsv:
forall bs cargs lsv0 lsv1
(
UNP :
unpromote_args sgn lsv bs cargs =
Some lsv0)
(
LSV1 :
lmap_sv (
fun sv =>
Some sv)
lsv =
Some lsv1)
(
CEQ :
if_Some (
eval_list_sval ctx lsv0) (
list_val_promotes_eq cargs)),
eval_list_sval ctx lsv1 =
option_map (
fun vs0 =>
map (
promote_valb sgn) (
combine bs vs0)) (
eval_list_sval ctx lsv0).
Proof.
induction lsv as [|
sv lsv];
simpl;
intros [|
b0 bs] [|
c0 cs];
try discriminate 1;
do 2
intro.
-
do 2
injection 1
as <-.
reflexivity.
-
do 2
autodestruct;
injection 3
as <-.
autodestruct;
injection 2
as <-;
simpl.
autodestruct.
2:{
intros ERR _.
erewrite unpromote_arg_correct;
eauto;
rewrite ERR;
constructor. }
intros.
erewrite IHlsv;
eauto.
2:{
revert CEQ;
autodestruct;
simpl.
inversion 2;
assumption. }
destruct eval_list_sval. 2:
repeat autodestruct.
erewrite unpromote_arg_correct;
eauto.
2:{
intros ->;
rewrite EQ2;
simpl.
inversion CEQ;
assumption. }
simpl;
unfold option_map;
repeat autodestruct.
Qed.
Lemma unpromote_op_correct ctx op lsv iinfo l fsv pre args
(
H:
unpromote_op op lsv iinfo =
Some (
fsv,
pre))
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
lsv =
Some l)
(
EARGS:
eval_list_sval ctx l =
Some args)
(
PRE:
Forall (
eval_okclause ctx)
pre):
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx)
op args (
cm1 ctx).
Proof.
revert H;
unfold unpromote_op.
repeat (
autodestruct;
intro);
injection 1
as ?;
subst.
inversion_clear PRE as [|? ?
PROM _].
case PROM as (
args' &
EARGS' & (
PROM &
CARGS &
CRES)).
specialize (
PROM sgn);
rewrite EQ1 in PROM.
replace args with (
map (
promote_valb sgn) (
combine prom.(
op_prom_args)
args')). 2:{
exploit unpromote_args_correct;
eauto.
{
rewrite EARGS';
exact CARGS. }
rewrite EARGS,
EARGS'.
injection 1
as ->.
reflexivity.
}
rewrite PROM,
promote_svalb_correct.
simpl;
rewrite EARGS'.
unfold option_map;
repeat autodestruct;
intros;
f_equal.
eapply ok_cast_sgn_correct;
eauto.
intros REQ.
rewrite REQ in CRES.
apply CRES.
Qed.
Global Opaque unpromote_op.
Local Hint Resolve unpromote_op_correct:
core.
Lemma unpromote_condition_correct ctx cond args iinfo cond0 args0 pre
(
UNP :
unpromote_condition cond args iinfo =
Some ((
cond0,
args0),
pre))
(
PRE :
Forall (
eval_okclause ctx)
pre):
eval_scondition ctx cond0 args0 =
eval_scondition ctx cond (
lsv_of_list args).
Proof.
Global Opaque unpromote_condition.
Main proof for the expansions of operations
Lemma target_op_expanse_correct ctx op lsv l hlsv fsv args:
forall
(
H:
target_op_expanse op lsv =
Some fsv)
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
lsv =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args),
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx)
op args (
cm1 ctx).
Proof.
Global Opaque target_op_expanse.
Local Hint Resolve target_op_expanse_correct:
core.
Theorem rewrite_ops_correct RRULES ctx op lsv iinfo l hlsv fsv pre args
(
H:
rewrite_ops RRULES op lsv iinfo =
Some (
fsv,
pre))
(
LMAP:
lmap_sv (
fun sv =>
Some sv)
lsv =
Some l)
(
ELSVEQ:
list_sval_equiv ctx l hlsv)
(
OK:
eval_list_sval ctx hlsv =
Some args)
(
PRE:
Forall (
eval_okclause ctx)
pre):
eval_sval ctx fsv =
eval_operation (
cge ctx) (
csp ctx)
op args (
cm1 ctx).
Proof.
Main proof for the expansions of branches
Lemma loadimm32_correct ctx n:
eval_sval ctx (
loadimm32 n) =
Some (
Vint n).
Proof.
Lemma loadimm64_correct ctx n:
eval_sval ctx (
loadimm64 n) =
Some (
Vlong n).
Proof.
Lemma target_cbranch_expanse_correct ctx c1 l1 c2 l2:
forall
(
TARGET:
target_cbranch_expanse c1 l1 =
Some (
c2,
l2)),
eval_scondition ctx c2 l2 =
eval_scondition ctx c1 (
lsv_of_list l1).
Proof.
functional inversion 1;
unfold eval_scondition;
subst;
simpl.
all:
try match goal with
|
H :
Int.eq _ _ =
true |- _ =>
apply Int.same_if_eq in H as ->
|
H :
Int64.eq _ _ =
true |- _ =>
apply Int64.same_if_eq in H as ->
end.
1,2,7,8:
destruct c;
simpl;
do 2 (
destruct eval_sval;
try reflexivity);
try change Cle with (
swap_comparison Cge);
try change Clt with (
swap_comparison Cgt);
rewrite ?
Val.swap_cmp_bool, ?
Val.swap_cmpu_bool,
?
Val.swap_cmpl_bool, ?
Val.swap_cmplu_bool;
reflexivity.
1-8:
destruct c;
simpl;
try (
unfold fsv;
rewrite ?
loadimm32_correct, ?
loadimm64_correct;
simpl);
solve [
destruct eval_sval;
reflexivity].
1-4:
destruct c;
match goal with H :
expanse_cbranch_fp _ _ _ _ = (_, _) |- _ =>
inv H end;
simpl;
do 2 (
destruct eval_sval;
try reflexivity);
simpl;
unfold zero32,
zero64,
Val.cmpf,
Val.cmpfs;
destruct v,
v0;
simpl;
try reflexivity;
rewrite ?
Float.cmp_ne_eq, ?
Float32.cmp_ne_eq;
simpl;
rewrite <-1?
Float.cmp_swap, <-1?
Float32.cmp_swap;
simpl;
first [
destruct (
Float.cmp _ _) |
destruct (
Float32.cmp _ _)];
simpl;
rewrite ?
Int.eq_true, ?
Int.eq_false by apply Int.one_not_zero;
try reflexivity.
Qed.
Global Opaque target_cbranch_expanse.
Local Hint Resolve target_cbranch_expanse_correct:
core.
Theorem rewrite_cbranches_correct RRULES c1 l1 iinfo ctx c2 l2 pre:
forall
(
H :
rewrite_cbranches RRULES c1 l1 iinfo =
Some ((
c2,
l2),
pre))
(
PRE :
Forall (
eval_okclause ctx)
pre)
(
AARGS :
Forall (
fun sv =>
alive (
eval_sval ctx sv))
l1),
eval_scondition ctx c2 l2 =
eval_scondition ctx c1 (
lsv_of_list l1).
Proof.
Proofs of branch pruning rewrites
Lemma prunable_inequality_spec ctx cond sv v hid1 hid2 hid3
(
EVAL:
eval_sval ctx sv=
Some v)
(
PRUNE:
prunable_inequality cond sv =
true)
:
eval_scondition ctx cond
(
Scons sv (
Scons sv (
Snil hid1)
hid2)
hid3)=
Some false.
Proof.
Lemma branch_pruning_no_true ctx cond lsv
(
ALIVE:
alive (
eval_list_sval ctx lsv)):
WHEN branch_pruning cond lsv ~>
ob THEN
ob <>
Some true.
Proof.
wlp_simplify; try discriminate.
Qed.
Lemma branch_pruning_some_false ctx cond lsv
(
ALIVE:
alive (
eval_list_sval ctx lsv)):
WHEN branch_pruning cond lsv ~>
ob THEN
ob =
Some false ->
eval_scondition ctx cond lsv =
Some false.
Proof.
wlp_simplify;
try discriminate.
clear H3.
apply bool_eq_ok in H1;
subst.
exploit H0;
auto;
intro;
subst.
clear H0 Hexta.
destruct a;
simpl in H1;
subst.
apply lsv_len_two_correct in H as (
hid1 &
hid2 &
hid3 &
LEQ);
subst.
simpl in ALIVE.
destruct (
eval_sval ctx s0)
eqn:
EVAL;
try congruence.
simpl in H2.
eapply prunable_inequality_spec;
eauto.
Qed.
Global Opaque branch_pruning.