Commit 9c9d516b authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Proof of Ocmp expansions without immediate and some drafts in comment

parent 1e06ebb8
......@@ -377,7 +377,7 @@ Proof.
rewrite <- Float32.cmp_swap. auto.
Qed.
(* TODO UNUSUED ? Remark branch_on_X31:
(* TODO gourdinl UNUSUED ? Remark branch_on_X31:
forall normal lbl (rs: regset) m b,
rs#X31 = Val.of_bool (eqb normal b) ->
exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m =
......
......@@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
insn
:: (if normal' then
Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info)
else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO Maybe incorrect *)
else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO gourdinl Maybe incorrect *)
:: k
let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
......@@ -392,14 +392,14 @@ let expanse (sb : superblock) code pm =
debug "Iop/Ccompu\n";
exp := cond_int32u false c a1 a2 dest succ [];
was_exp := true
(*| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompimm\n";
exp := expanse_condimm_int32s c a1 imm dest succ [];
was_exp := true
| Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompuimm\n";
exp := expanse_condimm_int32u c a1 imm dest succ [];
was_exp := true*)
was_exp := true
| Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
debug "Iop/Ccompl\n";
exp := cond_int64s false c a1 a2 dest succ [];
......@@ -408,14 +408,14 @@ let expanse (sb : superblock) code pm =
debug "Iop/Ccomplu\n";
exp := cond_int64u false c a1 a2 dest succ [];
was_exp := true
(*| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccomplimm\n";
exp := expanse_condimm_int64s c a1 imm dest succ [];
was_exp := true
| Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
debug "Iop/Ccompluimm\n";
exp := expanse_condimm_int64u c a1 imm dest succ [];
was_exp := true*)
was_exp := true
| Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
debug "Iop/Ccompf\n";
exp := expanse_cond_fp false cond_float c f1 f2 dest succ [];
......
......@@ -597,7 +597,7 @@ Proof.
explore; try congruence.
Qed.
(* TODO MOVE EXPANSIONS BELOW ELSEWHERE *)
(* TODO gourdinl MOVE EXPANSIONS BELOW ELSEWHERE *)
Definition is_inv_cmp_int (cmp: comparison) : bool :=
match cmp with | Cle | Cgt => true | _ => false end.
......@@ -608,7 +608,7 @@ Definition is_inv_cmp_float (cmp: comparison) : bool :=
Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
if is_x0 then Some is_inv else None.
(* TODO IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval :=
(* TODO gourdinl IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval :=
match l with
| nil => hSnil()
| r::l =>
......@@ -663,6 +663,17 @@ Definition loadimm64 (n: int64) :=
| Imm64_large imm => hSop (OEloadli imm) hnil
end.
Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
match make_immed32 n with
| Imm32_single imm =>
DO hl <~ make_lhsv_single hv1;;
hSop (opimm imm) hl
| Imm32_pair hi lo =>
DO hvs <~ load_hilo32 hi lo;;
DO hl <~ make_lhsv_cmp false hv1 hvs;;
hSop op hl
end.
Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
match make_immed64 n with
| Imm64_single imm =>
......@@ -679,8 +690,12 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
hSop op hl
end.
Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
......@@ -750,6 +765,47 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
DO hl <~ make_lhsv_single hvs;;
if normal' then RET hvs else hSop (OExoriw Int.one) hl.
Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
let is_inv := is_inv_cmp_int cmp in
if Int.eq n Int.zero then
let optR0 := make_optR0 true is_inv in
DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
cond_int32s cmp hl optR0
else
match cmp with
| Ceq | Cne =>
let optR0 := make_optR0 true is_inv in
DO hvs <~ xorimm32 hv1 n;;
DO hl <~ make_lhsv_cmp false hvs hvs;;
cond_int32s cmp hl optR0
| Clt => sltimm32 hv1 n
| Cle =>
if Int.eq n (Int.repr Int.max_signed) then
loadimm32 Int.one
else sltimm32 hv1 (Int.add n Int.one)
| _ =>
let optR0 := make_optR0 false is_inv in
DO hvs <~ loadimm32 n;;
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int32s cmp hl optR0
end.
Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
let is_inv := is_inv_cmp_int cmp in
if Int.eq n Int.zero then
let optR0 := make_optR0 true is_inv in
DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
cond_int32u cmp hl optR0
else
match cmp with
| Clt => sltuimm32 hv1 n
| _ =>
let optR0 := make_optR0 false is_inv in
DO hvs <~ loadimm32 n;;
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int32u cmp hl optR0
end.
Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
let is_inv := is_inv_cmp_int cmp in
if Int64.eq n Int64.zero then
......@@ -775,6 +831,22 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
cond_int64s cmp hl optR0
end.
Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
let is_inv := is_inv_cmp_int cmp in
if Int64.eq n Int64.zero then
let optR0 := make_optR0 true is_inv in
DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
cond_int64u cmp hl optR0
else
match cmp with
| Clt => sltuimm64 hv1 n
| _ =>
let optR0 := make_optR0 false is_inv in
DO hvs <~ loadimm64 n;;
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int64u cmp hl optR0
end.
(** simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
match rsv with
......@@ -801,6 +873,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int32u c lhsv optR0
| (Ccompimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32s c hv1 imm
| (Ccompuimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32u c hv1 imm
| (Ccompl c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
......@@ -839,9 +917,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_single c lhsv
(*| (Ccomplimm c imm), a1 :: nil =>
| (Ccomplimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm
| (Ccompluimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm*)
expanse_condimm_int64u c hv1 imm
| _, _ =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
......@@ -889,7 +970,16 @@ Proof.
auto.
Qed.
Lemma xor_neg_ltge_cmp: forall v1 v2,
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.
(* TODO gourdinl Lemma xor_neg_ltge_cmp: forall v1 v2,
Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
Some (Val.of_optbool (Val.cmp_bool Cge v1 v2)).
Proof.
......@@ -900,15 +990,15 @@ Proof.
try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl;
try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
auto.
Qed.
Qed.*)
Lemma cmp_neg_ltgt_cmp: forall v1 v2,
(* TODO gourdinl useless? Lemma cmp_neg_ltgt_cmp: forall v1 v2,
Some (Val.cmp Clt v1 v2) = Some (Val.of_optbool (Val.cmp_bool Cgt v2 v1)).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence;
unfold Val.cmp; simpl; auto.
Qed.
Qed.*)
Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
......@@ -934,7 +1024,7 @@ Proof.
repeat destruct (_ && _); simpl; auto.
Qed.
Lemma xor_neg_ltge_cmpu: forall mptr v1 v2,
(* TODO gourdinl Lemma xor_neg_ltge_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) Cge v1 v2)).
Proof.
......@@ -956,9 +1046,9 @@ Proof.
try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
simpl; auto;
repeat destruct (_ && _); simpl; auto.
Qed.
Qed.*)
Lemma cmp_neg_ltgt_cmpu: forall mptr v1 v2,
(* TODO gourdinl Lemma cmp_neg_ltgt_cmpu: forall mptr v1 v2,
Some (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) =
Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cgt v2 v1)).
Proof.
......@@ -970,15 +1060,14 @@ Proof.
try congruence.
- repeat destruct (_ || _); simpl; auto.
- repeat destruct (_ && _); simpl; auto.
Qed.
Qed.*)
Lemma cmpl_optbool_mktotal: forall cmp v1 v2,
Some (Val.maketotal (Val.cmpl cmp v1 v2)) =
Some (Val.of_optbool (Val.cmpl_bool cmp v1 v2)).
Lemma optbool_mktotal: forall v,
Some (Val.maketotal (option_map Val.of_bool v)) =
Some (Val.of_optbool v).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence.
destruct (Int64.cmp _ _); auto.
destruct v; simpl; auto.
Qed.
Lemma cmplu_optbool_mktotal: forall mptr cmp v1 v2,
......@@ -1088,6 +1177,50 @@ Proof.
repeat destruct (_ && _); simpl; auto.
Qed.
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.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence;
unfold Val.cmpf; simpl.
rewrite Float.cmp_ne_eq.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
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.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence;
unfold Val.cmpfs; simpl.
rewrite Float32.cmp_ne_eq.
destruct (Float32.cmp _ _ _); simpl; auto.
Qed.
Lemma cmp_neg_ltgt_cmpf: forall v1 v2,
Some (Val.cmpf Clt v1 v2) = Some (Val.of_optbool (Val.cmpf_bool Cgt v2 v1)).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence;
unfold Val.cmpf; simpl; auto.
replace Cgt with (swap_comparison Clt) by auto.
rewrite Float.cmp_swap.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
Lemma cmp_neg_lege_cmpf: forall v1 v2,
Some (Val.cmpf Cle v1 v2) = Some (Val.of_optbool (Val.cmpf_bool Cge v2 v1)).
Proof.
intros. eapply f_equal.
destruct v1, v2; simpl; try congruence;
unfold Val.cmpf; simpl; auto.
replace Cle with (swap_comparison Cge) by auto.
rewrite Float.cmp_swap.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
Lemma simplify_ccomp_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
DO hv2 <~ hsi_sreg_get hst r0;;
......@@ -1117,10 +1250,13 @@ Proof.
try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
simplify_SOME z.
intros; apply xor_neg_ltle_cmp.
intros; apply cmp_neg_ltgt_cmp.
intros; apply xor_neg_ltge_cmp.
simplify_SOME z; unfold Val.cmp.
- intros; apply xor_neg_ltle_cmp.
- intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmp_bool; trivial.
- intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmp_bool.
rewrite xor_neg_optb; trivial.
Qed.
Lemma simplify_ccompu_correct: forall c r r0 (hst: hsistate_local),
......@@ -1152,12 +1288,119 @@ Proof.
try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
simplify_SOME z.
intros; apply xor_neg_ltle_cmpu.
intros; apply cmp_neg_ltgt_cmpu.
intros; apply xor_neg_ltge_cmpu.
simplify_SOME z; unfold Val.cmpu.
- intros; apply xor_neg_ltle_cmpu.
- intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmpu_bool; trivial.
- intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool.
rewrite xor_neg_optb; trivial.
Qed.
Lemma mkimm_single_equal: forall n imm,
make_immed32 n = Imm32_single imm ->
n = imm.
Proof.
intros. unfold make_immed32 in H.
destruct (Int.eq _ _); inv H; auto.
Qed.
(* TODO gourdinl Lemma mkimm_pair_lo_zero_equal: forall n hi lo,
make_immed32 n = Imm32_pair hi lo ->
Int.eq n Int.zero = false ->
Int.eq lo Int.zero = true ->
n = Int.shl hi (Int.repr 12).
Proof.
intros. unfold make_immed32 in H.
destruct (Int.eq _ _) in H; try discriminate.
inv H. apply Int.same_if_eq in H1. rewrite H1.
rewrite Int.sub_zero_l. unfold Int.shru, Int.shl.
*)
(* TODO gourdinl Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32u c hv1 n ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
hsok_local ge sp rs0 m0 hst ->
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m)).
Proof.
unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
- wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
apply Int.same_if_eq in EQIMM; subst. trivial.
- unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI;
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail);
try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
+ apply mkimm_single_equal in EQMKI; subst.
rewrite Int.add_commut, Int.add_zero_l. trivial.
+
2: { intros. destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
2: { unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI.
2: {
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail);
try erewrite H9; eauto; try erewrite H8; eauto;
try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
2: {
apply mkimm_single_equal in EQMKI; subst.
rewrite Int.add_commut, Int.add_zero_l. trivial.
2: {
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
2: {
all:
try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
simplify_SOME z; unfold Val.cmp, zero32.
all:
try apply Int.same_if_eq in H0; subst; trivial.
erewrite H0.
- intros; apply xor_neg_ltle_cmpu.
- intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmpu_bool; trivial.
- intros; replace (Clt) with (negate_comparison Cge) by auto;
rewrite Val.negate_cmpu_bool.
rewrite xor_neg_optb; trivial.
Qed.
*)
Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
DO hv2 <~ hsi_sreg_get hst r0;;
......@@ -1187,11 +1430,13 @@ Proof.
try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
simplify_SOME z.
1,2,3: intros; apply cmpl_optbool_mktotal.
intros; apply xor_neg_ltle_cmpl.
intros; apply cmp_neg_ltgt_cmpl.
intros; apply xor_neg_ltge_cmpl.
simplify_SOME z; unfold Val.cmpl.
1,2,3: intros; apply optbool_mktotal.
- intros; apply xor_neg_ltle_cmpl.
- intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmpl_bool; trivial.
apply optbool_mktotal.
- intros; apply xor_neg_ltge_cmpl.
Qed.
Lemma simplify_ccomplu_correct: forall c r r0 (hst: hsistate_local),
......@@ -1223,11 +1468,186 @@ Proof.
try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
simplify_SOME z.
1,2,3: intros; apply cmplu_optbool_mktotal.
intros; apply xor_neg_ltle_cmplu.
intros; apply cmp_neg_ltgt_cmplu.
intros; apply xor_neg_ltge_cmplu.
simplify_SOME z; unfold Val.cmplu.
1,2,3: intros; apply optbool_mktotal.
- intros; apply xor_neg_ltle_cmplu.
- intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite Val.swap_cmplu_bool; trivial.
apply optbool_mktotal.
- intros; apply xor_neg_ltge_cmplu.
Qed.
(* TODO gourdinl move to common/Values ? *)
Theorem swap_cmpf_bool:
forall c x y,
Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x.
Proof.
destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto.
Qed.
Theorem swap_cmpfs_bool:
forall c x y,
Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x.
Proof.
destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
Qed.
Lemma simplify_ccompf_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
DO hv2 <~ hsi_sreg_get hst r0;;
DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;;
expanse_cond_fp false cond_float c lhsv ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
hsok_local ge sp rs0 m0 hst ->
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompf c)) args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Ccompf c)) args m)).
Proof.
unfold expanse_cond_fp in *; destruct c;
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
all:
try (erewrite H9; eauto; erewrite H8; eauto);
try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto;
erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto;
simplify_SOME z; unfold Val.cmpf.
- intros; apply xor_neg_eqne_cmpf.
- intros; replace (Clt) with (swap_comparison Cgt) by auto;
rewrite swap_cmpf_bool; trivial.
- intros; replace (Cle) with (swap_comparison Cge) by auto;
rewrite swap_cmpf_bool; trivial.
Qed.
Lemma simplify_cnotcompf_correct: forall c r r0 (hst: hsistate_local),
WHEN DO hv1 <~ hsi_sreg_get hst r;;
DO hv2 <~ hsi_sreg_get hst r0;;
DO lhsv <~ make_lhsv_cmp (is_inv_cmp_float c) hv1 hv2;;
expanse_cond_fp true cond_float c lhsv ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
(m0 : mem) (st : sistate_local),
hsilocal_refines ge sp rs0 m0 hst st ->
hsok_local ge sp rs0 m0 hst ->
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Cnotcompf c)) args m) <> None ->
seval_sval ge sp (hsval_proj hv) rs0 m0 =
(SOME args <-
seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0
m0
IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
IN eval_operation ge sp (Ocmp (Cnotcompf c)) args m)).
Proof.
unfold expanse_cond_fp in *; destruct c;
wlp_simplify;
destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
all: try (simplify_SOME z; contradiction; fail).
all:
try (erewrite H9; eauto; erewrite H8; eauto);