[Admitted checker] Some more proof, version with buggy addirw0

1 files changed, 126 insertions, 5 deletions

diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 7b20db6c..311f2828 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -5,7 +5,7 @@ Require Import RTLpathSE_theory.
 Require Import RTLpathSE_simu_specs.
 Require Import Asmgen Asmgenproof1.
 
-(* Useful functions for conditions/branches expansion *)
+(** Useful functions for conditions/branches expansion *)
 
 Definition is_inv_cmp_int (cmp: comparison) : bool :=
   match cmp with | Cle | Cgt => true | _ => false end.
@@ -16,7 +16,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.
 
-(* Functions to manage lists of "fake" values *)
+(** Functions to manage lists of "fake" values *)
 
 Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
   let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
@@ -26,7 +26,9 @@ Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
 Definition make_lhsv_single (hvs: hsval) : list_hsval :=
   fScons hvs fSnil.
 
-(* Expansion functions *)
+(** Expansion functions *)
+
+(* Immediate loads *)
 
 Definition load_hilo32 (hi lo: int) :=
   if Int.eq lo Int.zero then
@@ -91,6 +93,9 @@ Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEslt
 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.
+
+(* Comparisons intructions *)
+
 Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
   match cmp with
   | Ceq => fSop (OEseqw optR0) lhsv
@@ -241,7 +246,7 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
   let hl := make_lhsv_single hvs in
   if normal' then hvs else fSop (OExoriw Int.one) hl.
 
-(* Target op simplifications using "fake" values *)
+(** Target op simplifications using "fake" values *)
 
 Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
   match op, lr with
@@ -312,7 +317,9 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
   | _, _ => None
   end.
 
-(* Auxiliary lemmas on comparisons *)
+(** 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)) =
@@ -327,6 +334,8 @@ Proof.
   auto.
 Qed.
 
+(* 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)).
@@ -351,6 +360,8 @@ Proof.
   repeat destruct (_ && _); simpl; auto.
 Qed.
 
+(* 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)).
@@ -369,6 +380,46 @@ Proof.
   destruct (Int64.lt _ _); auto.
 Qed.
 
+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.
+  intros. destruct c; inv H; try discriminate;
+  destruct v1, v2; simpl; auto;
+  destruct (Int64.eq i i0) eqn:EQ0.
+  1,3:
+    apply Int64.same_if_eq in EQ0; subst;
+    rewrite Int64.xor_idem;
+    rewrite Int64.eq_true; trivial.
+  1,2:
+    destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence;
+    rewrite Int64.xor_is_zero in EQ1; congruence.
+Qed.
+
+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.
+  intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto.
+  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
+  destruct (zlt (Int64.signed n) (Int64.signed i)).
+  rewrite zlt_false by omega. auto.
+  rewrite zlt_true by omega. auto.
+  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
+  specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)).
+  rewrite EQMAX; simpl; intros.
+  assert (Int64.signed n <> Int64.max_signed).
+  { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
+  generalize (Int64.signed_range n); omega.
+Qed.
+
+(* 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)).
@@ -413,6 +464,8 @@ Proof.
   repeat destruct (_ && _); simpl; auto.
 Qed.
 
+(* 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)).
@@ -424,6 +477,8 @@ Proof.
   destruct (Float.cmp _ _ _); simpl; auto.
 Qed.
 
+(* 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)).
@@ -435,6 +490,8 @@ Proof.
   destruct (Float32.cmp _ _ _); simpl; auto.
 Qed.
 
+(* 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).
@@ -645,6 +702,70 @@ Proof.
   - apply xor_neg_ltge_cmplu.
 Qed.
 
+Lemma simplify_ccomplimm_correct ge sp hst st c r n rs0 m m0 v: forall
+  (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
+           seval_smem ge sp (si_smem st) rs0 m0 = Some m ->
+           Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
+  (SREG: forall r: positive,
+          hsi_sreg_eval ge sp hst r rs0 m0 =
+          seval_sval ge sp (si_sreg st r) rs0 m0)
+  (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v)
+  (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m),
+  seval_sval ge sp
+    (hsval_proj (expanse_condimm_int64s c (fsi_sreg_get hst r) n)) rs0 m0 =
+  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;
+  unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64;
+  try erewrite !fsi_sreg_get_correct; eauto;
+  try rewrite OKv1;
+  unfold Val.cmpl, zero64.
+  (* Simplify make immediate and decompose subcases *)
+  2,4,6,10,12:
+    try (specialize make_immed64_sound with n;
+    destruct (make_immed64 n) eqn:EQMKI_A0).
+  20:
+    try (specialize make_immed32_sound with (Int.one);
+    destruct (make_immed32 Int.one) eqn:EQMKI_A1).
+  20,21:
+    try (specialize make_immed64_sound with (Int64.add n Int64.one);
+    destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2).
+  all:
+    try destruct (Int.eq lo Int.zero) eqn:EQLO32;
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO64;
+    try destruct (Int64.eq lo0 Int64.zero) eqn:EQLO064;
+    try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX;
+    try erewrite fSop_correct; eauto; simpl;
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try rewrite OKv1;
+    try rewrite OK2.
+  (* Ceq, Cne, Clt = itself *)
+  all: intros; try apply Int64.same_if_eq in EQIMM; subst;
+       try (rewrite optbool_mktotal; trivial; fail).
+  (* Others simple subcases *)
+  all:
+    unfold Val.cmpl;
+    try apply Int64.same_if_eq in EQLO64; subst;
+    try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
+    try (rewrite <- xor_neg_ltle_cmpl; unfold Val.cmpl;
+    trivial; fail);
+    try erewrite xorl_zero_eq_cmpl; eauto;
+    try apply xor_neg_ltle_cmpl; 
+    try apply xor_neg_ltge_cmpl;
+    trivial;
+    try rewrite optbool_mktotal; trivial.
+
+  all:
+    try apply Int64.same_if_eq in EQLO064; subst;
+    try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi0 (Int64.repr 12))) Int64.zero) in H;
+    try rewrite (Int64.add_commut (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) Int64.zero) in H;
+    try rewrite Int64.add_zero_l in H; try rewrite <- H;
+    try apply cmpl_ltle_add_one; auto.
+all: admit.
+Admitted.
+
 Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall
   (SMEM : forall (m : mem) (b : Values.block) (ofs : Z),
            seval_smem ge sp (si_smem st) rs0 m0 = Some m ->