From 397dfb4cd5d207fcbffbfc54a9a4f9a8b756598d Mon Sep 17 00:00:00 2001
From: Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>
Date: Mon, 6 Jul 2020 15:37:42 +0200
Subject: aarch64/Asmblock: Merge PArithCRRR and PArithCFFF

---
 aarch64/Asmblock.v | 35 ++++++++++++-----------------------
 1 file changed, 12 insertions(+), 23 deletions(-)

(limited to 'aarch64/Asmblock.v')

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index b0358b6e..ffe24832 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -398,10 +398,11 @@ Inductive arith_ppp : Type :=
   | Pfsub (sz: fsize)                                (**r subtraction *)
 .
 
-(* TODO matching case in ar_instruction *)
-Inductive arith_c_rrr : Type :=
+Inductive arith_c_ppp : Type :=
   (** Conditional data processing *)
   | Pcsel                                             (**r int conditional move *)
+  (** Floating-point conditional select *)
+  | Pfsel
 .
 
 Inductive arith_w_rr0r : Type :=
@@ -430,12 +431,6 @@ Inductive arith_x_rr0r : Type :=
   | PornX (s: shift_op)                               (**r or-not *)
 .
 
-(* TODO matching case in ar_instruction *)
-Inductive arith_c_fff : Type :=
-  (** Floating-point conditional select *)
-  | Pfsel
-.
-
 Inductive arith_w_rr0 : Type :=
   (** Logical, immediate *)
   | PandimmW (n: Z)                                 (**r and *)
@@ -499,7 +494,7 @@ Inductive ar_instruction : Type :=
   | PArithCP (i : arith_c_p) (rd : preg) (c : testcond)
   | PArithPP (i : arith_pp) (rd rs : preg)
   | PArithPPP (i : arith_ppp) (rd r1 r2 : preg)
-  | PArithCRRR (i : arith_c_rrr) (rd r1 r2 : ireg) (c : testcond)
+  | PArithCPPP (i : arith_c_ppp) (rd r1 r2 : preg) (c : testcond)
   | PArithWRR0R (i : arith_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithXRR0R (i : arith_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithWRR0 (i : arith_w_rr0) (rd : ireg) (r1 : ireg0)
@@ -508,7 +503,6 @@ Inductive ar_instruction : Type :=
   | PArithXARRRR0 (i : arith_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
   | PArithSWFR0 (i : arith_sw_fr0) (rd : freg) (rs : ireg0)
   | PArithDXFR0 (i : arith_dx_fr0) (rd : freg) (rs : ireg0)
-  | PArithCFFF (i : arith_c_fff) (rd r1 r2 : freg) (c : testcond)
   | PArithAFFF (i : arith_afff) (rd r1 r2 : freg)
   (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm
   | PArithAFFFF (i : arith_affff) (rd r1 r2 r3 : freg) *)
@@ -1339,7 +1333,7 @@ Definition arith_eval_ppp i v1 v2 :=
   | Pfsub D => Val.subf v1 v2
   end.
 
-Definition arith_eval_c_rrr (i : arith_c_rrr) (v1 v2 : val) (c : option bool) :=
+Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) :=
   match i with
   | Pcsel =>
     (match c with
@@ -1347,6 +1341,12 @@ Definition arith_eval_c_rrr (i : arith_c_rrr) (v1 v2 : val) (c : option bool) :=
     | Some false => v2
     | None => Vundef
     end)
+  | Pfsel =>
+    (match c with
+    | Some true => v1
+    | Some false => v2
+    | None => Vundef
+    end)
   end.
 
 (* obtain v1 by rs##r1 *)
@@ -1417,16 +1417,6 @@ Definition arith_eval_dx_fr0 i v :=
   | PfmoviDX => float64_of_bits v
   end.
 
-Definition arith_eval_c_fff (i : arith_c_fff) (v1 v2 : val) (c : option bool) :=
-  match i with
-  | Pfsel =>
-    (match c with
-    | Some true => v1
-    | Some false => v2
-    | None => Vundef
-    end)
-  end.
-
 Definition arith_eval_afff i v1 v2 :=
   match i with
   | Pfnmul S => Val.negfs (Val.mulfs v1 v2)
@@ -1472,7 +1462,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | 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)
-  | PArithCRRR i d s1 s2 c => rs#d <- (arith_eval_c_rrr i rs#s1 rs#s2 (eval_testcond c rs))
+  | PArithCPPP i d s1 s2 c => rs#d <- (arith_eval_c_ppp i rs#s1 rs#s2 (eval_testcond c rs))
 
   | PArithWRR0R i d s1 s2 => rs#d <- (arith_eval_w_rr0r i rs##s1 rs#s2)
   | PArithXRR0R i d s1 s2 => rs#d <- (arith_eval_x_rr0r i rs###s1 rs#s2)
@@ -1486,7 +1476,6 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithSWFR0 i d s => rs#d <- (arith_eval_sw_fr0 i rs##s)
   | PArithDXFR0 i d s => rs#d <- (arith_eval_dx_fr0 i rs###s)
 
-  | PArithCFFF i d s1 s2 c => rs#d <- (arith_eval_c_fff i rs#s1 rs#s2 (eval_testcond c rs))
   | PArithAFFF i d s1 s2 => rs#d <- (arith_eval_afff i rs#s1 rs#s2)
 
   | PArithComparisonPP i s1 s2 =>
-- 
cgit