Inline Pcset in ar_instruction

1 files changed, 4 insertions, 16 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index e0815890..90ca7e05 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -284,15 +284,6 @@ Inductive arith_p : Type :=
   | Pfmovimmd (f: float)                                   (**r load float64 constant *)
 .
 
-(* Arithmetic instructions with conditional execution *)
-Inductive arith_c_p : Type :=
-  (** Conditional data processing *)
-  | Pcset                                       (**r set to 1/0 if cond is true/false *)
-(*
-  | Pcsetm                                      (**r set to -1/0 if cond is true/false *)
-*)
-.
-
 Inductive arith_comparison_p : Type :=
   (** Floating-point comparison *)
   | Pfcmp0 (sz: fsize)                                     (**r compare [r1] and [+0.0] *)
@@ -451,7 +442,6 @@ Inductive arith_appp : Type :=
  *)
 Inductive ar_instruction : Type :=
   | PArithP (i : arith_p) (rd : preg)
-  | PArithCP (i : arith_c_p) (rd : preg) (c : testcond)
   | PArithPP (i : arith_pp) (rd rs : preg)
   | PArithPPP (i : arith_ppp) (rd r1 r2 : preg)
   | PArithCPPP (i : arith_c_ppp) (rd r1 r2 : preg) (c : testcond)
@@ -467,6 +457,9 @@ Inductive ar_instruction : Type :=
   | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg)
   | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg)
   | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
+  (* Instructions without indirection sine they would be the only ones *)
+  (* PArithCP: Pcsetm is commented out by aarch64/Asm, so Pcset is alone *)
+  | Pcset (rd : preg) (c : testcond)
 .
 
 Inductive basic : Type :=
@@ -1211,11 +1204,6 @@ Definition if_opt_bool_val (c: option bool) v1 v2: val :=
    | None => Vundef
    end.
 
-Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val :=
-  match i with
-  | Pcset => if_opt_bool_val c (Vint Int.one) (Vint Int.zero)
-  end.
-
 Definition arith_eval_pp i v :=
   match i with
   | Pmov => v
@@ -1444,7 +1432,6 @@ Definition arith_comparison_p_compare i :=
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithP i d => rs#d <- (arith_eval_p i)
-  | PArithCP i d c => rs#d <- (arith_eval_c_p i (eval_testcond c rs))
   | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s)
   | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp i rs#s1 rs#s2)
   | PArithCPPP i d s1 s2 c => rs#d <- (arith_eval_c_ppp i rs#s1 rs#s2 (eval_testcond c rs))
@@ -1470,6 +1457,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithComparisonP i s =>
     let (v1, v2) := arith_prepare_comparison_p i rs#s in
     arith_comparison_p_compare i rs v1 v2
+  | Pcset d c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero))
   end.
 
 (* basic exec *)