some more proof for fake hsval checker expansions

1 files changed, 1 insertions, 324 deletions

diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index f42a3492..7e41b5b0 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -7,7 +7,6 @@ Require Import RTL RTLpath.
 Require Import Errors.
 Require Import RTLpathSE_theory RTLpathLivegenproof.
 Require Import Axioms RTLpathSE_simu_specs.
-Require Import Asmgen Asmgenproof1.
 Require Import RTLpathSE_simplify.
 
 Local Open Scope error_monad_scope.
@@ -659,214 +658,14 @@ Qed.
    end.*)
 
 (*
-Definition load_hilo32 (hi lo: int) :=
-  DO hnil <~ hSnil();;
-  if Int.eq lo Int.zero then
-    hSop (OEluiw hi) hnil
-  else
-    DO hvs <~ hSop (OEluiw hi) hnil;;
-    DO hl <~ make_lhsv_single hvs;;
-    hSop (Oaddimm lo) hl.
-
-Definition load_hilo64 (hi lo: int64) :=
-  DO hnil <~ hSnil();;
-  if Int64.eq lo Int64.zero then
-    hSop (OEluil hi) hnil
-  else
-    DO hvs <~ hSop (OEluil hi) hnil;;
-    DO hl <~ make_lhsv_single hvs;;
-    hSop (Oaddlimm lo) hl.
-
-Definition loadimm32 (n: int) :=
-  match make_immed32 n with
-  | Imm32_single imm =>
-      DO hnil <~ hSnil();;
-      hSop (OEaddiwr0 imm) hnil
-  | Imm32_pair hi lo => load_hilo32 hi lo
-  end.
-
-Definition loadimm64 (n: int64) :=
-  DO hnil <~ hSnil();;
-  match make_immed64 n with
-  | Imm64_single imm =>
-      hSop (OEaddilr0 imm) hnil
-  | Imm64_pair hi lo => load_hilo64 hi lo
-  | 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 =>
-      DO hl <~ make_lhsv_single hv1;;
-      hSop (opimm imm) hl
-  | Imm64_pair hi lo =>
-      DO hvs <~ load_hilo64 hi lo;;
-      DO hl <~ make_lhsv_cmp false hv1 hvs;;
-      hSop op hl
-  | Imm64_large imm =>
-      DO hnil <~ hSnil();;
-      DO hvs <~ hSop (OEloadli imm) hnil;;
-      DO hl <~ make_lhsv_cmp false hv1 hvs;;
-      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_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
-  match cmp with
-  | Ceq => hSop (OEsequw optR0) lhsv
-  | Cne => hSop (OEsneuw optR0) lhsv
-  | Clt | Cgt => hSop (OEsltuw optR0) lhsv
-  | Cle | Cge =>
-      DO hvs <~ (hSop (OEsltuw optR0) lhsv);;
-      DO hl <~ make_lhsv_single hvs;;
-      hSop (OExoriw Int.one) hl
-  end.
-
-Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
-  match cmp with
-  | Ceq => hSop (OEseql optR0) lhsv
-  | Cne => hSop (OEsnel optR0) lhsv
-  | Clt | Cgt => hSop (OEsltl optR0) lhsv
-  | Cle | Cge =>
-      DO hvs <~ (hSop (OEsltl optR0) lhsv);;
-      DO hl <~ make_lhsv_single hvs;;
-      hSop (OExoriw Int.one) hl
-  end.
 
-Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
-  match cmp with
-  | Ceq => hSop (OEsequl optR0) lhsv
-  | Cne => hSop (OEsneul optR0) lhsv
-  | Clt | Cgt => hSop (OEsltul optR0) lhsv
-  | Cle | Cge =>
-      DO hvs <~ (hSop (OEsltul optR0) lhsv);;
-      DO hl <~ make_lhsv_single hvs;;
-      hSop (OExoriw Int.one) hl
-  end.
 
-Definition cond_float (cmp: comparison) (lhsv: list_hsval) :=
-  match cmp with
-  | Ceq | Cne => hSop OEfeqd lhsv
-  | Clt | Cgt => hSop OEfltd lhsv
-  | Cle | Cge => hSop OEfled lhsv
-  end.
 
-Definition cond_single (cmp: comparison) (lhsv: list_hsval) :=
-  match cmp with
-  | Ceq | Cne => hSop OEfeqs lhsv
-  | Clt | Cgt => hSop OEflts lhsv
-  | Cle | Cge => hSop OEfles lhsv
-  end.
 
-Definition is_normal_cmp cmp :=
-  match cmp with | Cne => false | _ => true end.
 
-Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
-  let normal := is_normal_cmp cmp in
-  let normal' := if cnot then negb normal else normal in
-  DO hvs <~ fn_cond cmp lhsv;;
-  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
-    let optR0 := make_optR0 true is_inv in
-    DO hl <~ make_lhsv_cmp is_inv hv1 hv1;;
-    cond_int64s cmp hl optR0
-  else
-    match cmp with
-    | Ceq | Cne =>
-        let optR0 := make_optR0 true is_inv in
-        DO hvs <~ xorimm64 hv1 n;;
-        DO hl <~ make_lhsv_cmp false hvs hvs;;
-        cond_int64s cmp hl optR0
-    | Clt => sltimm64 hv1 n
-    | Cle =>
-        if Int64.eq n (Int64.repr Int64.max_signed) then
-          loadimm32 Int.one
-        else sltimm64 hv1 (Int64.add n Int64.one)
-    | _ =>
-        let optR0 := make_optR0 false is_inv in
-        DO hvs <~ loadimm64 n;;
-        DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
-        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 *)
@@ -911,27 +710,6 @@ Proof.
   intro H0; clear H0; simplify_SOME z; congruence. 
 Qed.
 
-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.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  unfold Val.cmp; simpl;
-  try rewrite Int.eq_sym;
-  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.
-
-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.
 
 Lemma xor_ceq_zero: forall v n cmp,
   cmp = Ceq \/ cmp = Cne ->
@@ -966,29 +744,6 @@ Proof.
   unfold Val.cmp; simpl; auto.
    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)) =
-  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
-Proof.
-  intros. eapply f_equal.
-  destruct v1, v2; simpl; try congruence.
-  unfold Val.cmpu; simpl;
-  try rewrite Int.eq_sym;
-  try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl;
-  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
-  auto.
-  1,2:
-    unfold Val.cmpu, Val.cmpu_bool;
-    destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _);
-    try destruct (eq_block _ _); auto.
-  unfold Val.cmpu, Val.cmpu_bool; 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.
 
 (* 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)) =
@@ -1143,16 +898,7 @@ 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)) =
@@ -1443,62 +1189,6 @@ Proof.
 Admitted.
 (*Qed.*)
 
-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;
-  unfold loadimm32, sltuimm32, opimm32, load_hilo32.
-  1,3,5,7,9,11: 
-    wlp_simplify;
-    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence;
-    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.
-  4: rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu.
-  5: intros; replace (Clt) with (swap_comparison Cgt) by auto;
-     rewrite Val.swap_cmpu_bool; trivial.
-  6: intros; replace (Clt) with (negate_comparison Cge) by auto;
-     rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb.
-  1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial.
-  all:
-    specialize make_immed32_sound with n;
-    destruct (make_immed32 n) eqn:EQMKI;
-    try destruct (Int.eq lo Int.zero) eqn:EQLO.
-  all:
-    wlp_simplify;
-    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-  all:
-    try erewrite H11; eauto;
-    try erewrite H10; eauto; 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.
-  all: try apply Int.same_if_eq in H1; subst.
-  all: try apply Int.same_if_eq in EQLO; subst.
-  all: try rewrite Int.add_commut, Int.add_zero_l; trivial.
-  all: try rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu; trivial.
-  all: 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;;
@@ -1576,20 +1266,7 @@ Proof.
     - 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;;