PArithCmpR0R in checker

1 files changed, 130 insertions, 36 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index df9586c1..29d91d1c 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -91,7 +91,14 @@ Inductive arith_op :=
   | 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)
+  | OArithComparisonR0R_CN (n: arith_comparison_r0r) (is: isize)
+  | OArithComparisonR0R_CZ (n: arith_comparison_r0r) (is: isize)
+  | OArithComparisonR0R_CC (n: arith_comparison_r0r) (is: isize)
+  | OArithComparisonR0R_CV (n: arith_comparison_r0r) (is: isize)
+  | OArithComparisonR0R_CN_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
+  | OArithComparisonR0R_CZ_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
+  | OArithComparisonR0R_CC_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
+  | OArithComparisonR0R_CV_XZR (n: arith_comparison_r0r) (is: isize) (vz: val)
   | OArithComparisonP (n: arith_comparison_p)
 .
 
@@ -101,6 +108,12 @@ Inductive op_wrap :=
   | Control (co: control_op)
 .
 
+Definition v_compare_int (v1 v2: val) : CRflags :=
+  {| _CN := (Val.negative (Val.sub v1 v2));
+     _CZ := (Val_cmpu Ceq v1 v2);
+     _CC := (Val_cmpu Cge v1 v2);
+     _CV := (Val.sub_overflow v1 v2) |}.
+
 Definition v_compare_long (v1 v2: val) : CRflags :=
   {| _CN := (Val.negativel (Val.subl v1 v2));
      _CZ := (Val_cmplu Ceq v1 v2);
@@ -141,7 +154,11 @@ Definition arith_eval_comparison_pp (n: arith_comparison_pp) (v1 v2: val) :=
   | Pcmpext _ | Pcmnext _ => v_compare_long v1' v2'
   | Pfcmp S => v_compare_single v1' v2'
   | Pfcmp D => v_compare_float v1' v2'
-  end. 
+  end.
+
+Definition arith_eval_comparison_r0r (n: arith_comparison_r0r) (v1 v2: val) (is: isize) :=
+  let (v1',v2') := arith_prepare_comparison_r0r n v1 v2 in
+  if is then v_compare_int v1' v2' else v_compare_long v1' v2'.
 
 Definition op:=op_wrap.
 
@@ -160,6 +177,14 @@ Definition arith_op_eval (op: arith_op) (l: list value) :=
   | 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)))
+  | OArithComparisonR0R_CN n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CN)))
+  | OArithComparisonR0R_CZ n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CZ)))
+  | OArithComparisonR0R_CC n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CC)))
+  | OArithComparisonR0R_CV n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CV)))
+  | OArithComparisonR0R_CN_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CN)))
+  | OArithComparisonR0R_CZ_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CZ)))
+  | OArithComparisonR0R_CC_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CC)))
+  | OArithComparisonR0R_CV_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CV)))
   | _, _ => None
   end.
 
@@ -216,6 +241,22 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
       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
+  | OArithComparisonR0R_CN n1 is1 =>
+      match o2 with OArithComparisonR0R_CN n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end
+  | OArithComparisonR0R_CZ n1 is1 =>
+      match o2 with OArithComparisonR0R_CZ n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end
+  | OArithComparisonR0R_CC n1 is1 =>
+      match o2 with OArithComparisonR0R_CC n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end
+  | OArithComparisonR0R_CV n1 is1 =>
+      match o2 with OArithComparisonR0R_CV n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end
+  | OArithComparisonR0R_CN_XZR n1 is1 vz1 =>
+      match o2 with OArithComparisonR0R_CN_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end
+  | OArithComparisonR0R_CZ_XZR n1 is1 vz1 =>
+      match o2 with OArithComparisonR0R_CZ_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end
+  | OArithComparisonR0R_CC_XZR n1 is1 vz1 =>
+      match o2 with OArithComparisonR0R_CC_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end
+  | OArithComparisonR0R_CV_XZR n1 is1 vz1 =>
+      match o2 with OArithComparisonR0R_CV_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end
   (*| OArithRR n1 => *)
      (*match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end*)
   (*| OArithRI32 n1 i1 =>*)
@@ -475,37 +516,45 @@ Definition trans_arith (ai: ar_instruction) : inst :=
   | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)]
   | PArithPP n rd r1 => [(#rd, Op(Arith (OArithPP n)) (PReg(#r1) @ Enil))]
   | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))]
-  | PArithRR0R n rd r1 r2 => let lr := match r1 with
-                                       | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil)
-                                       | XZR => let vz := match arith_rr0r_isize n with
-                                                          | W => Vint Int.zero
-                                                          | X => Vlong Int64.zero
-                                                          end in
-                                                          Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil)
-                                       end in
-                                       [(#rd,  lr)]
-  | PArithRR0 n rd r1 => let lr := match r1 with
-                                   | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil)
-                                   | XZR => let vz := match arith_rr0_isize n with
-                                                      | W => Vint Int.zero
-                                                      | X => Vlong Int64.zero
-                                                      end in
-                                                      Op(Arith (OArithRR0_XZR n vz)) (Enil)
-                                   end in
-                                   [(#rd, lr)]
-  | PArithARRRR0 n rd r1 r2 r3 => let lr := match r3 with
-                                            | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil)
-                                            | XZR => let vz := match arith_arrrr0_isize n with
-                                                               | W => Vint Int.zero
-                                                               | X => Vlong Int64.zero
-                                                               end in
-                                                               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))]
+  | PArithRR0R n rd r1 r2 =>
+      let lr := match r1 with
+                | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil)
+                | XZR => let vz := if arith_rr0r_isize n then Vint Int.zero else Vlong Int64.zero in
+                         Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil)
+                end in
+      [(#rd,  lr)]
+  | PArithRR0 n rd r1 =>
+      let lr := match r1 with
+                | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil)
+                | XZR => let vz := if arith_rr0_isize n then Vint Int.zero else Vlong Int64.zero in
+                         Op(Arith (OArithRR0_XZR n vz)) (Enil)
+                end in
+      [(#rd, lr)]
+  | PArithARRRR0 n rd r1 r2 r3 =>
+      let lr := match r3 with
+                | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil)
+                | XZR => let vz := if arith_arrrr0_isize n then Vint Int.zero else Vlong Int64.zero in
+                         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))]
+  | PArithComparisonR0R n r1 r2 =>
+      let is := arith_comparison_r0r_isize n in
+      match r1 with
+      | RR0 r1' => [(#CN, Op(Arith (OArithComparisonR0R_CN n is)) (PReg(#r1') @ PReg(#r2) @ Enil));
+                    (#CZ, Op(Arith (OArithComparisonR0R_CZ n is)) (PReg(#r1') @ PReg(#r2) @ Enil));
+                    (#CC, Op(Arith (OArithComparisonR0R_CC n is)) (PReg(#r1') @ PReg(#r2) @ Enil));
+                    (#CV, Op(Arith (OArithComparisonR0R_CV n is)) (PReg(#r1') @ PReg(#r2) @ Enil))]
+      | XZR => let vz := if is then Vint Int.zero else Vlong Int64.zero in
+          [(#CN, Op(Arith (OArithComparisonR0R_CN_XZR n is vz)) (PReg(#r2) @ Enil));
+                (#CZ, Op(Arith (OArithComparisonR0R_CZ_XZR n is vz)) (PReg(#r2) @ Enil));
+                (#CC, Op(Arith (OArithComparisonR0R_CC_XZR n is vz)) (PReg(#r2) @ Enil));
+                (#CV, Op(Arith (OArithComparisonR0R_CV_XZR n is vz)) (PReg(#r2) @ Enil))]
+      end
   | _ => []
   (*| PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)]*)
   (*| PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))]*)
@@ -804,7 +853,7 @@ Ltac replace_ppos :=
   try erewrite !ireg_pos_ppos;
   try erewrite !freg_pos_ppos.
 
-Ltac DI0N0 ir0 := destruct ir0 as [rr0DIRN0|]; subst; simpl.
+Ltac DI0N0 ir0 := destruct ir0; subst; simpl.
 
 Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl.
 
@@ -993,6 +1042,43 @@ Proof.
       discriminate_preg_flags ]).
 Qed.
 
+Lemma compare_int_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_int Vundef Vundef)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_int Vundef Vundef)) ]>) <[ 4 <-
+  Val (_CC (v_compare_int Vundef Vundef)) ]>) <[ 5 <-
+ Val (_CV (v_compare_int Vundef Vundef)) ]>) (# rr) =
+Val
+  ((compare_int rsr Vundef Vundef) rr).
+Proof.
+  intros. unfold v_compare_int, compare_int.
+  (destruct rr;
+    [ DDRF d; discriminate_preg_flags |
+      validate_crbit_flags c |
+      discriminate_preg_flags ]).
+Qed.
+
+Lemma compare_int_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_int v1 v2)) ]>) <[ 3 <-
+   Val (_CZ (v_compare_int v1 v2)) ]>) <[ 4 <-
+  Val (_CC (v_compare_int v1 v2)) ]>) <[ 5 <-
+ Val (_CV (v_compare_int v1 v2)) ]>) (# rr) =
+Val
+  ((compare_int rsr v1 v2) rr).
+Proof.
+  intros.
+  destruct v1; destruct v2;
+  try eapply compare_int_res_aux; eauto;
+  unfold v_compare_int, compare_int;
+  (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.*)
@@ -1052,8 +1138,16 @@ Proof.
     try (eapply compare_single_res; eauto);
     try (eapply compare_long_res; eauto);
     try (eapply compare_float_res; eauto).
-  - admit.
-           
+  - (* PArithComparisonR0R *)
+    simpl. destruct r1; (
+      simpl; 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_r0r, arith_comparison_r0r_isize; destruct arith_prepare_comparison_r0r; destruct is;
+      simpl; intros rr; try destruct sz;
+      try (eapply compare_long_res; eauto);
+      try (eapply compare_int_res; eauto)).
+  - 
      all:admit.
 
   (*