Inline Pcsel in ar_instruction

1 files changed, 5 insertions, 28 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 36a0afc0..492387bd 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -371,11 +371,6 @@ Inductive arith_ppp : Type :=
   | Pfsub (sz: fsize)                                (**r subtraction *)
 .
 
-Inductive arith_c_ppp : Type :=
-  (** Conditional data processing *)
-  | Pcsel                                             (**r int/float conditional move *)
-.
-
 Inductive arith_rr0r : Type :=
   (** Integer arithmetic, shifted register *)
   | Padd (sz:isize) (s: shift_op)                               (**r addition *)
@@ -439,7 +434,6 @@ Inductive ar_instruction : Type :=
   | PArithP (i : arith_p) (rd : preg)
   | 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)
   | PArithRR0R (i : arith_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithRR0 (i : arith_rr0) (rd : ireg) (r1 : ireg0)
   | PArithARRRR0 (i : arith_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
@@ -453,9 +447,11 @@ Inductive ar_instruction : Type :=
   | 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 : ireg) (c : testcond)
+  | Pcset (rd : ireg) (c : testcond)                                  (**r set to 1/0 if cond is true/false *)
   (* PArithFR0 *)
-  | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0)
+  | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0)                     (**r copy int reg to FP reg *)
+  (* PArithCPPP *)
+  | Pcsel (rd r1 r2 : preg) (c : testcond)                            (**r int/float conditional move *)
 .
 
 Inductive basic : Type :=
@@ -1271,25 +1267,6 @@ Definition arith_eval_ppp i v1 v2 :=
   | Pfsub D => Val.subf v1 v2
   end.
 
-Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) :=
-  if_opt_bool_val c v1 v2.
- (*
-  match i with
-  | Pcsel => 
-    (match c with
-    | Some true => v1
-    | Some false => v2
-    | None => Vundef
-    end)
-  | Pfsel =>
-    (match c with
-    | Some true => v1
-    | Some false => v2
-    | None => Vundef
-    end)
-  end.
- *)
-
 Definition arith_rr0r_isize (i: arith_rr0r) :=
   match i with
   | Padd is _ => is
@@ -1415,7 +1392,6 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithP i d => rs#d <- (arith_eval_p i)
   | 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))
 
   | PArithRR0R i d s1 s2 => rs#d <- (arith_eval_rr0r i (ir0 (arith_rr0r_isize i) rs s1) rs#s2)
 
@@ -1439,6 +1415,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | Pcset d c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero))
   | Pfmovi S d s => rs#d <- (float32_of_bits rs##s)
   | Pfmovi D d s => rs#d <- (float64_of_bits rs###s)
+  | Pcsel d s1 s2 c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (rs#s1) (rs#s2))
   end.
 
 (* basic exec *)