PArithComparison special lemmas and adaptations

1 files changed, 315 insertions, 17 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index ae4e12b2..df9586c1 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -62,6 +62,8 @@ Inductive value_wrap :=
 
 Definition value := value_wrap.
 
+Record CRflags := { _CN: val; _CZ:val; _CC: val; _CV: val }.
+
 Inductive control_op :=
   (*| Oj_l (l: label)*)
   | Ob (l: label)
@@ -84,6 +86,13 @@ Inductive arith_op :=
   | OArithRR0_XZR (n: arith_rr0) (vz: val)
   | OArithARRRR0 (n: arith_arrrr0)
   | OArithARRRR0_XZR (n: arith_arrrr0) (vz: val)
+  | OArithComparisonPP_CN (n: arith_comparison_pp)
+  | OArithComparisonPP_CZ (n: arith_comparison_pp)
+  | OArithComparisonPP_CC (n: arith_comparison_pp)
+  | OArithComparisonPP_CV (n: arith_comparison_pp)
+  | OArithComparisonR0R (n: arith_comparison_r0r)
+  | OArithComparisonR0R_XZR (n: arith_comparison_r0r) (vz: val)
+  | OArithComparisonP (n: arith_comparison_p)
 .
 
 Inductive op_wrap :=
@@ -92,6 +101,48 @@ Inductive op_wrap :=
   | Control (co: control_op)
 .
 
+Definition v_compare_long (v1 v2: val) : CRflags :=
+  {| _CN := (Val.negativel (Val.subl v1 v2));
+     _CZ := (Val_cmplu Ceq v1 v2);
+     _CC := (Val_cmplu Cge v1 v2);
+     _CV := (Val.subl_overflow v1 v2) |}.
+
+Definition v_compare_float (v1 v2: val) : CRflags :=
+  match v1, v2 with
+  | Vfloat f1, Vfloat f2 =>
+      {| _CN := (Val.of_bool (Float.cmp Clt f1 f2));
+         _CZ := (Val.of_bool (Float.cmp Ceq f1 f2));
+         _CC := (Val.of_bool (negb (Float.cmp Clt f1 f2)));
+         _CV := (Val.of_bool (negb (Float.ordered f1 f2))) |}
+  | _, _ =>
+      {| _CN := Vundef;
+         _CZ := Vundef;
+         _CC := Vundef;
+         _CV := Vundef |}
+  end.
+
+Definition v_compare_single (v1 v2: val) : CRflags :=
+  match v1, v2 with
+  | Vsingle f1, Vsingle f2 =>
+      {| _CN := (Val.of_bool (Float32.cmp Clt f1 f2));
+         _CZ := (Val.of_bool (Float32.cmp Ceq f1 f2));
+         _CC := (Val.of_bool (negb (Float32.cmp Clt f1 f2)));
+         _CV := (Val.of_bool (negb (Float32.ordered f1 f2))) |}
+  | _, _ =>
+      {| _CN := Vundef;
+         _CZ := Vundef;
+         _CC := Vundef;
+         _CV := Vundef |}
+  end.
+
+Definition arith_eval_comparison_pp (n: arith_comparison_pp) (v1 v2: val) :=
+  let (v1',v2') := arith_prepare_comparison_pp n v1 v2 in
+  match n with 
+  | Pcmpext _ | Pcmnext _ => v_compare_long v1' v2'
+  | Pfcmp S => v_compare_single v1' v2'
+  | Pfcmp D => v_compare_float v1' v2'
+  end. 
+
 Definition op:=op_wrap.
 
 Definition arith_op_eval (op: arith_op) (l: list value) :=
@@ -105,6 +156,10 @@ Definition arith_op_eval (op: arith_op) (l: list value) :=
   | OArithRR0_XZR n vz, [] => Some (Val (arith_eval_rr0 n vz))
   | OArithARRRR0 n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrrr0 n v1 v2 v3))
   | OArithARRRR0_XZR n vz, [Val v1; Val v2] => Some (Val (arith_eval_arrrr0 n v1 v2 vz))
+  | OArithComparisonPP_CN n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CN)))
+  | OArithComparisonPP_CZ n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CZ)))
+  | OArithComparisonPP_CC n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CC)))
+  | OArithComparisonPP_CV n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CV)))
   | _, _ => None
   end.
 
@@ -153,6 +208,14 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
       match o2 with OArithARRRR0 n2 => phys_eq n1 n2 | _ => RET false end
   | OArithARRRR0_XZR n1 vz1 =>
       match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end
+  | OArithComparisonPP_CN n1 =>
+      match o2 with OArithComparisonPP_CN n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithComparisonPP_CZ n1 =>
+      match o2 with OArithComparisonPP_CZ n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithComparisonPP_CC n1 =>
+      match o2 with OArithComparisonPP_CC n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithComparisonPP_CV n1 =>
+      match o2 with OArithComparisonPP_CV n2 => phys_eq n1 n2 | _ => RET false end
   (*| OArithRR n1 => *)
      (*match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end*)
   (*| OArithRI32 n1 i1 =>*)
@@ -177,6 +240,7 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
      (*match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*)
   (*| OArithARRI64 n1 i1 =>*)
      (*match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*)
+  | _ => RET false
   end.
 
 Ltac my_wlp_simplify := wlp_xsimplify ltac:(intros; subst; simpl in * |- *; congruence || intuition eauto with wlp).
@@ -438,6 +502,10 @@ Definition trans_arith (ai: ar_instruction) : inst :=
                                                                Op(Arith (OArithARRRR0_XZR n vz)) (PReg(#r1) @ PReg(#r2) @ Enil)
                                             end in
                                             [(#rd, lr)]
+  | PArithComparisonPP n r1 r2 => [(#CN, Op(Arith (OArithComparisonPP_CN n)) (PReg(#r1) @ PReg(#r2) @ Enil));
+                                   (#CZ, Op(Arith (OArithComparisonPP_CZ n)) (PReg(#r1) @ PReg(#r2) @ Enil));
+                                   (#CC, Op(Arith (OArithComparisonPP_CC n)) (PReg(#r1) @ PReg(#r2) @ Enil));
+                                   (#CV, Op(Arith (OArithComparisonPP_CV n)) (PReg(#r1) @ PReg(#r2) @ Enil))]
   | _ => []
   (*| PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)]*)
   (*| PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))]*)
@@ -578,12 +646,60 @@ Proof.
   intros; destruct r; discriminate.
 Qed.
 
+Lemma ireg_not_CN: forall r,
+  2 <> ireg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma ireg_not_CZ: forall r,
+  3 <> ireg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma ireg_not_CC: forall r,
+  4 <> ireg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma ireg_not_CV: forall r,
+  5 <> ireg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
 Lemma freg_not_pmem: forall r,
   freg_to_pos r <> pmem.
 Proof.
   intros; destruct r; discriminate.
 Qed.
 
+Lemma freg_not_CN: forall r,
+  2 <> freg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma freg_not_CZ: forall r,
+  3 <> freg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma freg_not_CC: forall r,
+  4 <> freg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
+Lemma freg_not_CV: forall r,
+  5 <> freg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
 Lemma sr_ireg_update_both: forall sr rsr r1 rr v
   (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
   (sr <[ ireg_to_pos r1 <- Val (v) ]>) (#rr) =
@@ -629,6 +745,21 @@ Proof.
     + simpl; try rewrite <- HEQV; unfold ppos; try congruence.
 Qed.
 
+(*Lemma sr_cn_update_both: forall sr rsr rr v*)
+  (*(HEQV: forall r : preg, sr (# r) = Val (rsr r)),*)
+  (*(sr <[ #CN <- Val (v) ]>) (#rr) =*)
+  (*Val (rsr # CN <- v rr).*)
+(*Proof.*)
+  (*intros. unfold assign.*)
+  (*destruct (PregEq.eq CN rr); subst.*)
+  (*- rewrite Pregmap.gss. simpl. reflexivity.*)
+  (*- rewrite Pregmap.gso; eauto.*)
+    (*destruct rr; try congruence.*)
+    (*+ destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.*)
+    (*+ destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.*)
+    (*+ simpl; try rewrite <- HEQV; unfold ppos; try congruence.*)
+(*Qed.*)
+
 Lemma sr_update_overwrite: forall sr pos v1 v2,
   (sr <[ pos <- v1 ]>) <[ pos <- v2 ]> = (sr <[ pos <- v2 ]>).
 Proof.
@@ -644,17 +775,6 @@ Proof.
   destruct (R.eq_dec pos pos) eqn:REQ; try reflexivity; try congruence.
 Qed.
 
-(** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *)
-
-(*Module PChk := ParallelChecks L PosPseudoRegSet.*)
-
-(*Definition bblock_para_check (p: Asmvliw.bblock) : bool :=*)
-  (*PChk.is_parallelizable (trans_block p).*)
-
-(*Section SECT_PAR.*)
-
-(*Import PChk.*)
-
 (*Ltac Simplif :=*)
   (*[>((rewrite nextblock_inv by eauto with asmgen)<]*)
   (*[>|| (rewrite nextblock_inv1 by eauto with asmgen)<]*)
@@ -688,7 +808,15 @@ Ltac DI0N0 ir0 := destruct ir0 as [rr0DIRN0|]; subst; simpl.
 
 Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl.
 
-Ltac DDRN2 dr := destruct dr as [irDDRN2|frDDRN2]; subst; try destruct irDDRN2; simpl.
+Ltac DDRM dr :=
+  destruct dr as [irsDDRF|frDDRF]; 
+      [destruct irsDDRF as [irsDDRF|]
+      | idtac ].
+
+Ltac DDRF dr :=
+  destruct dr as [irsDDRF|frDDRF]; 
+      [destruct irsDDRF as [irsDDRF|]; [destruct irsDDRF|]
+      | destruct frDDRF].
 
 Ltac DPRF pr :=
   destruct pr as [drDPRF|crDPRF|]; 
@@ -702,20 +830,180 @@ Ltac DPRI pr :=
       | idtac
       | idtac ].
 
+Ltac discriminate_ppos :=
+  try apply ireg_not_pmem;
+  try apply freg_not_pmem;
+  try apply ireg_not_CN;
+  try apply ireg_not_CZ;
+  try apply ireg_not_CC;
+  try apply ireg_not_CV;
+  try apply freg_not_CN;
+  try apply freg_not_CZ;
+  try apply freg_not_CC;
+  try apply freg_not_CV;
+  try(simpl; discriminate).
+
+Ltac replace_regs_pos :=
+  try replace (7) with (ppos XSP) by eauto;
+  try replace (2) with (ppos CN) by eauto;
+  try replace (3) with (ppos CZ) by eauto;
+  try replace (4) with (ppos CC) by eauto;
+  try replace (5) with (ppos CV) by eauto.
+
 Ltac TARITH :=
   replace_ppos;
-  try replace (7) with (ppos XSP) by eauto;
+  replace_regs_pos;
   try sr_val_rwrt;
   try (eexists; split; [| split]); eauto;
   try (sr_memstate_rwrt; rewrite assign_diff;
-      try reflexivity; try apply ireg_not_pmem;
-      try apply freg_not_pmem).
+      try reflexivity;
+      discriminate_ppos
+  ).
 
 Ltac SRVUPDATE :=
   try eapply sr_ireg_update_both; eauto;
   try eapply sr_freg_update_both; eauto;
   try eapply sr_xsp_update_both; eauto.
 
+Ltac discriminate_preg_flags := rewrite !assign_diff; try rewrite !Pregmap.gso; discriminate_ppos; sr_val_rwrt; reflexivity.
+
+Ltac validate_crbit_flags c :=
+  destruct c;
+  [
+    do 3 (rewrite assign_diff; discriminate_ppos);
+    do 3 (rewrite Pregmap.gso; try discriminate);
+    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
+    do 2 (rewrite assign_diff; discriminate_ppos);
+    do 2 (rewrite Pregmap.gso; try discriminate);
+    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
+    do 1 (rewrite assign_diff; discriminate_ppos);
+    do 1 (rewrite Pregmap.gso; try discriminate);
+    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
+    rewrite sr_gss; rewrite Pregmap.gss; reflexivity
+  ].
+
+Lemma compare_single_res_aux: forall sr mr rsr rr
+  (HMEM: sr pmem = Memstate mr)
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  ((((sr <[ 2 <- Val (_CN (v_compare_single Vundef Vundef)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_single Vundef Vundef)) ]>) <[ 4 <-
+  Val (_CC (v_compare_single Vundef Vundef)) ]>) <[ 5 <-
+ Val (_CV (v_compare_single Vundef Vundef)) ]>) (# rr) =
+Val
+  ((compare_single rsr Vundef Vundef) rr).
+Proof.
+  intros. unfold v_compare_single, compare_single.
+  (destruct rr;
+    [ DDRF d; discriminate_preg_flags |
+      validate_crbit_flags c |
+      discriminate_preg_flags ]).
+Qed.
+
+Lemma compare_single_res: forall sr mr rsr rr v1 v2
+  (HMEM: sr pmem = Memstate mr)
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  ((((sr <[ 2 <- Val (_CN (v_compare_single v1 v2)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_single v1 v2)) ]>) <[ 4 <-
+  Val (_CC (v_compare_single v1 v2)) ]>) <[ 5 <-
+ Val (_CV (v_compare_single v1 v2)) ]>) (# rr) =
+Val
+  ((compare_single rsr v1 v2) rr).
+Proof.
+  intros.
+  destruct v1; destruct v2;
+  try eapply compare_single_res_aux; eauto.
+  unfold v_compare_single, compare_single.
+  (destruct rr;
+    [ DDRF d; discriminate_preg_flags |
+      validate_crbit_flags c |
+      discriminate_preg_flags ]).
+Qed.
+
+Lemma compare_float_res_aux: forall sr mr rsr rr
+  (HMEM: sr pmem = Memstate mr)
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  ((((sr <[ 2 <- Val (_CN (v_compare_float Vundef Vundef)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_float Vundef Vundef)) ]>) <[ 4 <-
+  Val (_CC (v_compare_float Vundef Vundef)) ]>) <[ 5 <-
+ Val (_CV (v_compare_float Vundef Vundef)) ]>) (# rr) =
+Val
+  ((compare_float rsr Vundef Vundef) rr).
+Proof.
+  intros. unfold v_compare_float, compare_float.
+  (destruct rr;
+    [ DDRF d; discriminate_preg_flags |
+      validate_crbit_flags c |
+      discriminate_preg_flags ]).
+Qed.
+
+Lemma compare_float_res: forall sr mr rsr rr v1 v2
+  (HMEM: sr pmem = Memstate mr)
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  ((((sr <[ 2 <- Val (_CN (v_compare_float v1 v2)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_float v1 v2)) ]>) <[ 4 <-
+  Val (_CC (v_compare_float v1 v2)) ]>) <[ 5 <-
+ Val (_CV (v_compare_float v1 v2)) ]>) (# rr) =
+Val
+  ((compare_float rsr v1 v2) rr).
+Proof.
+  intros.
+  destruct v1; destruct v2;
+  try eapply compare_float_res_aux; eauto.
+  unfold v_compare_float, compare_float.
+  (destruct rr;
+    [ DDRF d; discriminate_preg_flags |
+      validate_crbit_flags c |
+      discriminate_preg_flags ]).
+Qed.
+
+Lemma compare_long_res_aux: forall sr mr rsr rr
+  (HMEM: sr pmem = Memstate mr)
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  ((((sr <[ 2 <- Val (_CN (v_compare_long Vundef Vundef)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_long Vundef Vundef)) ]>) <[ 4 <-
+  Val (_CC (v_compare_long Vundef Vundef)) ]>) <[ 5 <-
+ Val (_CV (v_compare_long Vundef Vundef)) ]>) (# rr) =
+Val
+  ((compare_long rsr Vundef Vundef) rr).
+Proof.
+  intros. unfold v_compare_long, compare_long.
+  (destruct rr;
+    [ DDRF d; discriminate_preg_flags |
+      validate_crbit_flags c |
+      discriminate_preg_flags ]).
+Qed.
+
+Lemma compare_long_res: forall sr mr rsr rr v1 v2
+  (HMEM: sr pmem = Memstate mr)
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  ((((sr <[ 2 <- Val (_CN (v_compare_long v1 v2)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_long v1 v2)) ]>) <[ 4 <-
+  Val (_CC (v_compare_long v1 v2)) ]>) <[ 5 <-
+ Val (_CV (v_compare_long v1 v2)) ]>) (# rr) =
+Val
+  ((compare_long rsr v1 v2) rr).
+Proof.
+  intros.
+  destruct v1; destruct v2;
+  try eapply compare_long_res_aux; eauto;
+  unfold v_compare_long, compare_long;
+  (destruct rr;
+    [ DDRF d; discriminate_preg_flags |
+      validate_crbit_flags c |
+      discriminate_preg_flags ]).
+Qed.
+
+(** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *)
+
+(*Module PChk := ParallelChecks L PosPseudoRegSet.*)
+
+(*Definition bblock_para_check (p: Asmvliw.bblock) : bool :=*)
+  (*PChk.is_parallelizable (trans_block p).*)
+
+(*Section SECT_PAR.*)
+
+(*Import PChk.*)
+
 (*Arguments Pos.add: simpl never.*)
 (*Arguments ppos: simpl never.*)
 
@@ -736,7 +1024,7 @@ Proof.
   induction i.
   all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr.
   - (* PArithP *)
-    DDRN2 rd; TARITH; intros rr; DPRF rr; SRVUPDATE.
+    DIRN1 rd; TARITH; intros rr; DPRF rr; SRVUPDATE.
   - (* PArithPP *)
     DIRN1 rs; DIRN1 rd; TARITH;
     intros rr; DPRI rr; SRVUPDATE.
@@ -756,7 +1044,17 @@ Proof.
     + (* OArithARRRR0 *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE.
     + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE.
   - (* PArithComparisonPP *)
-  all:admit.
+    DIRN1 r2; DIRN1 r1; destruct i;
+    repeat (replace_ppos; replace_regs_pos; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
+    (eexists; split; [| split]; [reflexivity | eauto | idtac]);
+    unfold arith_eval_comparison_pp; destruct arith_prepare_comparison_pp;
+    simpl; intros rr; try destruct sz;
+    try (eapply compare_single_res; eauto);
+    try (eapply compare_long_res; eauto);
+    try (eapply compare_float_res; eauto).
+  - admit.
+           
+     all:admit.
 
   (*
 (* Ploadsymbol *)