Arith inst OK for the verifier

1 files changed, 191 insertions, 61 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index e1a49a55..88cca121 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -242,13 +242,12 @@ Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) :=
       end
   end.
 
-Definition cset_eval (c: testcond) (vCN vCZ vCC vCV: val) :=
+Definition csetsel_eval (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) (is_set: bool) :=
   let res := flags_testcond_value c vCN vCZ vCC vCV in
-    (if_opt_bool_val res (Vint Int.one) (Vint Int.zero)).
-
-Definition csel_eval (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) :=
-  let res := flags_testcond_value c vCN vCZ vCC vCV in
-    (if_opt_bool_val res v1 v2).
+  (if is_set then
+    (if_opt_bool_val res (Vint Int.one) (Vint Int.zero))
+  else
+    (if_opt_bool_val res v1 v2)).
 
 Definition fmovi_eval (fsz: fsize) (v: val) :=
   match fsz with
@@ -270,6 +269,23 @@ Definition fnmul_eval (fsz: fsize) (v1 v2: val) :=
 
 Definition op:=op_wrap.
 
+Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is_set: bool) :=
+  match c, l with
+  | TCeq, [Val vCZ] => Some (Val (csetsel_eval TCeq v1 v2 Vundef vCZ Vundef Vundef is_set))
+  | TCne, [Val vCZ] => Some (Val (csetsel_eval TCne v1 v2 Vundef vCZ Vundef Vundef is_set))
+  | TChs, [Val vCC] => Some (Val (csetsel_eval TChs v1 v2 Vundef Vundef vCC Vundef is_set))
+  | TClo, [Val vCC] => Some (Val (csetsel_eval TClo v1 v2 Vundef Vundef vCC Vundef is_set))
+  | TCmi, [Val vCN] => Some (Val (csetsel_eval TCmi v1 v2 vCN Vundef Vundef Vundef is_set))
+  | TCpl, [Val vCN] => Some (Val (csetsel_eval TCpl v1 v2 vCN Vundef Vundef Vundef is_set))
+  | TChi, [Val vCZ; Val vCC] => Some (Val (csetsel_eval TChi v1 v2 Vundef vCZ vCC Vundef is_set))
+  | TCls, [Val vCZ; Val vCC] => Some (Val (csetsel_eval TCls v1 v2 Vundef vCZ vCC Vundef is_set))
+  | TCge, [Val vCN; Val vCV] => Some (Val (csetsel_eval TCge v1 v2 vCN Vundef Vundef vCV is_set))
+  | TClt, [Val vCN; Val vCV] => Some (Val (csetsel_eval TClt v1 v2 vCN Vundef Vundef vCV is_set))
+  | TCgt, [Val vCN; Val vCZ; Val vCV] => Some (Val (csetsel_eval TCgt v1 v2 vCN vCZ Vundef vCV is_set))
+  | TCle, [Val vCN; Val vCZ; Val vCV] => Some (Val (csetsel_eval TCle v1 v2 vCN vCZ Vundef vCV is_set))
+  | _, _ => None
+  end.
+
 Definition arith_op_eval (op: arith_op) (l: list value) :=
   match op, l with
   | OArithP n, [] => Some (Val (arith_eval_p Ge.(_lk) n))
@@ -297,10 +313,10 @@ Definition arith_op_eval (op: arith_op) (l: list value) :=
   | OArithComparisonP_CZ n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CZ)))
   | OArithComparisonP_CC n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CC)))
   | OArithComparisonP_CV n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CV)))
-  | Ocset c, [Val vCN; Val vCZ; Val vCC; Val vCV] => Some (Val (cset_eval c vCN vCZ vCC vCV))
+  | Ocset c, l => cflags_eval c l Vundef Vundef true
   | Ofmovi fsz, [Val v] => Some (Val (fmovi_eval fsz v))
   | Ofmovi_XZR fsz, [] => Some (Val (fmovi_eval_xzr fsz))
-  | Ocsel c, [Val v1; Val v2; Val vCN; Val vCZ; Val vCC; Val vCV] => Some (Val (csel_eval c v1 v2 vCN vCZ vCC vCV))
+  | Ocsel c, Val v1 :: Val v2 :: l' => cflags_eval c l' v1 v2 false
   | Ofnmul fsz, [Val v1; Val v2] => Some (Val (fnmul_eval fsz v1 v2))
   | _, _ => None
   end.
@@ -330,6 +346,107 @@ Definition op_eval (op: op) (l:list value) :=
   (*| _, _ => None*)
   end.
 
+Definition vz_eq (vz1 vz2: val) : ?? bool :=
+  RET (match vz1 with
+       | Vint i1 => match vz2 with
+                    | Vint i2 => Int.eq i1 i2
+                    | _ => false
+                    end
+       | Vlong l1 => match vz2 with
+                     | Vlong l2 => Int64.eq l1 l2
+                     | _ => false
+                     end
+       | _ => false
+       end).
+
+Lemma vz_eq_correct vz1 vz2:
+  WHEN vz_eq vz1 vz2 ~> b THEN b = true -> vz1 = vz2.
+Proof.
+  wlp_simplify.
+  destruct vz1; destruct vz2; trivial; try discriminate.
+  - eapply f_equal; apply Int.same_if_eq; auto.
+  - eapply f_equal. apply Int64.same_if_eq; auto.
+Qed.
+Hint Resolve vz_eq_correct: wlp.
+
+Definition is_eq (is1 is2: isize) : ?? bool :=
+  RET (match is1 with
+       | W => match is2 with
+              | W => true
+              | _ => false
+              end
+       | X => match is2 with
+              | X => true
+              | _ => false
+              end
+       end).
+
+Lemma is_eq_correct is1 is2:
+  WHEN is_eq is1 is2 ~> b THEN b = true -> is1 = is2.
+Proof.
+  wlp_simplify; destruct is1; destruct is2; trivial; try discriminate.
+Qed.
+Hint Resolve is_eq_correct: wlp.
+
+(*Definition testcond_eq (c1 c2: testcond) : ?? bool :=*)
+  (*RET (match c1 with*)
+       (*| TCeq => match c2 with*)
+                 (*| TCeq => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TCne => match c2 with*)
+                 (*| TCne => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TChs => match c2 with*)
+                 (*| TChs => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TClo => match c2 with*)
+                 (*| TClo => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TCmi => match c2 with*)
+                 (*| TCmi => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TCpl => match c2 with*)
+                 (*| TCpl => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TChi => match c2 with*)
+                 (*| TChi => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TCls => match c2 with*)
+                 (*| TCls => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TCge => match c2 with*)
+                 (*| TCge => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TClt => match c2 with*)
+                 (*| TClt => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TCgt => match c2 with*)
+                 (*| TCgt => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*| TCle => match c2 with*)
+                 (*| TCle => true*)
+                 (*| _ => false*)
+                 (*end*)
+       (*end).*)
+
+(*Lemma testcond_eq_correct c1 c2:*)
+  (*WHEN testcond_eq c1 c2 ~> b THEN b = true -> c1 = c2.*)
+(*Proof.*)
+  (*wlp_simplify; destruct c1; destruct c2; trivial; try discriminate.*)
+(*Qed.*)
+(*Hint Resolve testcond_eq_correct: wlp.*)
+
 Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   match o1 with
   | OArithP n1 =>
@@ -341,15 +458,15 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   | OArithRR0R n1 =>
       match o2 with OArithRR0R n2 => phys_eq n1 n2 | _ => RET false end
   | OArithRR0R_XZR n1 vz1 =>
-      match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end
+      match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end
   | OArithRR0 n1 =>
       match o2 with OArithRR0 n2 => phys_eq n1 n2 | _ => RET false end
   | OArithRR0_XZR n1 vz1 =>
-      match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end
+      match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end
   | OArithARRRR0 n1 =>
       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
+      match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_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 =>
@@ -359,21 +476,21 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   | 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
+      match o2 with OArithComparisonR0R_CN n2 is2 => iandb (phys_eq n1 n2) (is_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
+      match o2 with OArithComparisonR0R_CZ n2 is2 => iandb (phys_eq n1 n2) (is_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
+      match o2 with OArithComparisonR0R_CC n2 is2 => iandb (phys_eq n1 n2) (is_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
+      match o2 with OArithComparisonR0R_CV n2 is2 => iandb (phys_eq n1 n2) (is_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
+      match o2 with OArithComparisonR0R_CN_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_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
+      match o2 with OArithComparisonR0R_CZ_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_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
+      match o2 with OArithComparisonR0R_CC_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_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
+      match o2 with OArithComparisonR0R_CV_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end
   | OArithComparisonP_CN n1 =>
       match o2 with OArithComparisonP_CN n2 => phys_eq n1 n2 | _ => RET false end
   | OArithComparisonP_CZ n1 =>
@@ -383,13 +500,13 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   | OArithComparisonP_CV n1 =>
       match o2 with OArithComparisonP_CV n2 => phys_eq n1 n2 | _ => RET false end
   | Ocset c1 =>
-      match o2 with Ocset c2 => phys_eq c1 c2 | _ => RET false end
+      match o2 with Ocset c2 => struct_eq c1 c2 | _ => RET false end
   | Ofmovi fsz1 =>
       match o2 with Ofmovi fsz2 => phys_eq fsz1 fsz2 | _ => RET false end
   | Ofmovi_XZR fsz1 =>
       match o2 with Ofmovi_XZR fsz2 => phys_eq fsz1 fsz2 | _ => RET false end
   | Ocsel c1 =>
-      match o2 with Ocsel c2 => phys_eq c1 c2 | _ => RET false end
+      match o2 with Ocsel c2 => struct_eq c1 c2 | _ => RET false end
   | Ofnmul fsz1 =>
       match o2 with Ofnmul fsz2 => phys_eq fsz1 fsz2 | _ => RET false end
   end.
@@ -399,7 +516,10 @@ Ltac my_wlp_simplify := wlp_xsimplify ltac:(intros; subst; simpl in * |- *; cong
 Lemma arith_op_eq_correct o1 o2:
   WHEN arith_op_eq o1 o2 ~> b THEN b = true -> o1 = o2.
 Proof.
-  destruct o1, o2; my_wlp_simplify; try congruence.
+  destruct o1, o2; my_wlp_simplify; try congruence;
+  try (destruct vz; destruct vz0); try (destruct is; destruct is0);
+  repeat apply f_equal; try congruence;
+  try apply Int.same_if_eq; try apply Int64.same_if_eq; try auto.
 Qed.
 Hint Resolve arith_op_eq_correct: wlp.
 Opaque arith_op_eq_correct.
@@ -621,6 +741,22 @@ Definition trans_exit (ex: option control) : L.inst :=
   end
 .
 
+Definition get_testcond_rlocs (c: testcond) :=
+  match c with
+  | TCeq => (PReg(#CZ) @ Enil)
+  | TCne => (PReg(#CZ) @ Enil)
+  | TChs => (PReg(#CC) @ Enil)
+  | TClo => (PReg(#CC) @ Enil)
+  | TCmi => (PReg(#CN) @ Enil)
+  | TCpl => (PReg(#CN) @ Enil)
+  | TChi => (PReg(#CZ) @ PReg(#CC) @ Enil)
+  | TCls => (PReg(#CZ) @ PReg(#CC) @ Enil)
+  | TCge => (PReg(#CN) @ PReg(#CV) @ Enil)
+  | TClt => (PReg(#CN) @ PReg(#CV) @ Enil)
+  | TCgt => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil)
+  | TCle => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil)
+  end.
+
 Definition trans_arith (ai: ar_instruction) : inst :=
   match ai with
   | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)]
@@ -670,14 +806,18 @@ Definition trans_arith (ai: ar_instruction) : inst :=
        (#CZ, Op(Arith (OArithComparisonP_CZ n)) (PReg(#r1) @ Enil));
        (#CC, Op(Arith (OArithComparisonP_CC n)) (PReg(#r1) @ Enil));
        (#CV, Op(Arith (OArithComparisonP_CV n)) (PReg(#r1) @ Enil))]
-  | Pcset rd c => [(#rd, Op(Arith (Ocset c)) (PReg(#CN) @ PReg(#CZ) @ PReg(#CC) @ PReg(#CV) @ Enil))]
+  | Pcset rd c =>
+      let lr := get_testcond_rlocs c in
+      [(#rd, Op(Arith (Ocset c)) lr)]
   | Pfmovi fsz rd r1 =>
       let lr := match r1 with
                 | RR0 r1' => Op(Arith (Ofmovi fsz)) (PReg(#r1') @ Enil)
                 | XZR => Op(Arith (Ofmovi_XZR fsz)) Enil
                 end in
       [(#rd, lr)]
-  | Pcsel rd r1 r2 c => [(#rd, Op(Arith (Ocsel c)) (PReg(#r1) @ PReg(#r2) @ PReg(#CN) @ PReg(#CZ) @ PReg(#CC) @ PReg(#CV) @ Enil))]
+  | Pcsel rd r1 r2 c =>
+      let lr := get_testcond_rlocs c in
+      [(#rd, Op(Arith (Ocsel c)) (PReg(#r1) @ PReg (#r2) @ lr))]
   | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))]
   end.
 
@@ -909,21 +1049,6 @@ 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.
@@ -1194,21 +1319,6 @@ Proof.
       discriminate_preg_flags ]).
 Qed.
 
-Lemma if_opt_bool_val_cond: forall sr mr (rd r1 r2: dreg) c rsr rr
-  (HMEM: sr pmem = Memstate mr)
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  (sr <[ #rd <- Val
-   (if_opt_bool_val
-      (flags_testcond_value c (rsr CN) (rsr CZ) (rsr CC) (rsr CV)) 
-      (rsr r1) (rsr r2)) ]>) (# rr) =
-  Val (rsr # rd <- (if_opt_bool_val (eval_testcond c rsr) (rsr r1) (rsr r2)) rr).
-Proof.
-  intros. unfold flags_testcond_value, eval_testcond.
-  destruct c; destruct (rsr _);
-  try (DIRN1 rd; DPRI rr; SRVUPDATE;
-  rewrite Pregmap.gso; unfold assign; try destruct (R.eq_dec); sr_val_rwrt; auto; discriminate_ppos).
-Qed.
-
 (** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *)
 
 (*Module PChk := ParallelChecks L PosPseudoRegSet.*)
@@ -1288,7 +1398,8 @@ Proof.
     try (eapply compare_int_res; eauto);
     try (eapply compare_float_res; eauto).
   - (* Pcset *)
-    simpl; (*DI0N0 rd.*) unfold eval_testcond, cset_eval; destruct c;
+    simpl; (*DI0N0 rd.*) unfold eval_testcond, get_testcond_rlocs, cflags_eval;
+    unfold csetsel_eval; unfold flags_testcond_value, list_exp_eval; destruct c; simpl;
     repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
     destruct (rsr CZ); simpl;
     (eexists; split; [| split]; [reflexivity | DI0N0 rd; eauto | idtac]);
@@ -1297,10 +1408,13 @@ Proof.
   - (* Pfmovi *)
     simpl; destruct r1; simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE.
   - (* Pcsel *)
-    simpl; DIRN1 r1; DIRN1 r2; unfold csel_eval;
+    simpl.
+    unfold eval_testcond, cflags_eval. DIRN1 r1; DIRN1 r2; destruct c; simpl;
     repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
-    (eexists; split; [| split]; [reflexivity | DDRF rd; eauto | idtac]);
-    intros; erewrite <- if_opt_bool_val_cond; eauto.
+    (eexists; split; [| split]; [reflexivity | DDRF rd; eauto | idtac]).
+    all: intros rr; destruct (PregEq.eq rr rd);
+    [ subst; erewrite Pregmap.gss; erewrite sr_gss; reflexivity |
+    try erewrite Pregmap.gso; try erewrite assign_diff; try rewrite H0; try fold (ppos rd); try eapply ppos_discr; eauto ].
   - (* Pfnmul *)
     simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE.
 Qed.
@@ -2037,7 +2151,7 @@ Definition string_of_name_ArithComparisonP_CZ (n: arith_comparison_p) : pstring
   end.
 
 Definition string_of_name_ArithComparisonP_CC (n: arith_comparison_p) : pstring :=
-match n with
+  match n with
   | Pfcmp0 _ => "ArithComparisonP_CC=>Pfcmp0"
   | Pcmpimm _ _ => "ArithComparisonP_CC=>Pcmpimm"
   | Pcmnimm _ _ => "ArithComparisonP_CC=>Pcmnimm"
@@ -2045,13 +2159,29 @@ match n with
   end.
 
 Definition string_of_name_ArithComparisonP_CV (n: arith_comparison_p) : pstring :=
-match n with
+  match n with
   | Pfcmp0 _ => "ArithComparisonP_CV=>Pfcmp0"
   | Pcmpimm _ _ => "ArithComparisonP_CV=>Pcmpimm"
   | Pcmnimm _ _ => "ArithComparisonP_CV=>Pcmnimm"
   | Ptstimm _ _ => "ArithComparisonP_CV=>Ptstimm"
   end.
 
+Definition string_of_name_cset (c: testcond) : pstring :=
+  match c with
+  | TCeq => "Cset=>TCeq"
+  | TCne => "Cset=>TCne"
+  | TChs => "Cset=>TChs"
+  | TClo => "Cset=>TClo"
+  | TCmi => "Cset=>TCmi"
+  | TCpl => "Cset=>TCpl"
+  | TChi => "Cset=>TChi"
+  | TCls => "Cset=>TCls"
+  | TCge => "Cset=>TCge"
+  | TClt => "Cset=>TClt"
+  | TCgt => "Cset=>TCgt"
+  | TCle => "Cset=>TCle"
+  end.
+
 Definition string_of_arith (op: arith_op): pstring :=
   match op with
   | OArithP n => string_of_name_ArithP n
@@ -2079,7 +2209,7 @@ Definition string_of_arith (op: arith_op): pstring :=
   | OArithComparisonP_CZ n => string_of_name_ArithComparisonP_CZ n
   | OArithComparisonP_CC n => string_of_name_ArithComparisonP_CC n
   | OArithComparisonP_CV n => string_of_name_ArithComparisonP_CV n
-  | Ocset _ => "Ocset"
+  | Ocset c => string_of_name_cset c
   | Ofmovi _ => "Ofmovi"
   | Ofmovi_XZR _ => "Ofmovi_XZR"
   | Ocsel _ => "Ocsel"