From 0e25db1398c133142201bda218f53a8756443c75 Mon Sep 17 00:00:00 2001
From: Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>
Date: Mon, 6 Jul 2020 15:28:19 +0200
Subject: aarch64/Asmblock: Merge PArithComparisonRR and PArithComparisonFF

---
 aarch64/Asmblock.v | 32 +++++++++++---------------------
 1 file changed, 11 insertions(+), 21 deletions(-)

(limited to 'aarch64/Asmblock.v')

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index be3389c4..e79c2733 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -359,13 +359,10 @@ Inductive arith_comparison_x_r0r : Type :=
   | PtstX (s: shift_op)             (**r and, then set flags *)
 .
 
-Inductive arith_comparison_rr : Type :=
+Inductive arith_comparison_pp : Type :=
   (** Integer arithmetic, extending register *)
   | Pcmpext (x: extend_op)                      (**r int64-int32 cmp *)
   | Pcmnext (x: extend_op)                      (**r int64-int32 cmn *)
-.
-
-Inductive arith_comparison_ff : Type :=
   (** Floating-point comparison *)
   | Pfcmp (sz: fsize)                                 (**r compare [r1] and [r2] *)
 .
@@ -525,11 +522,10 @@ Inductive ar_instruction : Type :=
   | PArithAFFFF (i : arith_affff) (rd r1 r2 r3 : freg) *)
   (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
   | PArithAAFFFF (i : arith_aaffff) (rd r1 r2 r3 : freg) *)
-  | PArithComparisonRR (i : arith_comparison_rr) (r1 r2 : ireg)
+  | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg)
   | PArithComparisonWR0R (i : arith_comparison_w_r0r) (r1 : ireg0) (r2 : ireg)
   | PArithComparisonXR0R (i : arith_comparison_x_r0r) (r1 : ireg0) (r2 : ireg)
   | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
-  | PArithComparisonFF (i : arith_comparison_ff) (rd rs : freg)
 .
 
 Inductive basic : Type :=
@@ -1453,10 +1449,11 @@ Definition arith_eval_afff i v1 v2 :=
   | Pfnmul D => Val.negf (Val.mulf v1 v2)
   end.
 
-Definition arith_prepare_comparison_rr i (v1 v2 : val) :=
+Definition arith_prepare_comparison_pp i (v1 v2 : val) :=
   match i with
   | Pcmpext x => (v1, (eval_extend v2 x))
   | Pcmnext x => (v1, (Val.negl (eval_extend v2 x)))
+  | Pfcmp _ => (v1, v2)
   end.
 
 Definition arith_prepare_comparison_w_r0r i v1 v2 :=
@@ -1485,11 +1482,6 @@ Definition arith_prepare_comparison_p i v :=
   | Pfcmp0 D => (v, (Vfloat Float.zero))
   end.
 
-Definition arith_prepare_comparison_ff i (v1 v2 : val) :=
-  match i with
-  | Pfcmp _ => (v1, v2)
-  end.
-
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithP i d => rs#d <- (arith_eval_p i)
@@ -1516,9 +1508,13 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | 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)
 
-  | PArithComparisonRR i s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_rr i rs#s1 rs#s2 in
-      compare_long rs v1 v2
+  | PArithComparisonPP i s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in
+      (match i with
+      | Pcmpext _ | Pcmnext _ => compare_long rs v1 v2
+      | Pfcmp S => compare_single rs v1 v2
+      | Pfcmp D => compare_float rs v1 v2
+      end)
   | PArithComparisonWR0R i s1 s2 =>
     let (v1, v2) := arith_prepare_comparison_w_r0r i rs##s1 rs#s2 in
       compare_int rs v1 v2
@@ -1533,12 +1529,6 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
       | Pfcmp0 S => compare_single rs v1 v2
       | Pfcmp0 D => compare_float rs v1 v2
       end)
-  | PArithComparisonFF i s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_ff i rs#s1 rs#s2 in
-    (match i with
-    | Pfcmp S => compare_single rs v1 v2
-    | Pfcmp D => compare_float rs v1 v2
-    end)
   end.
 
 (* basic exec *)
-- 
cgit