Regroup ar_instructions by access to "data" registers (dreg)

A dreg is either a floating poing, integer register, SP, or XZR. This
way we can combine a few more varaints in ar_instruction.

However, now every dreg case has to deal with the complications of ireg0
by giving, for every instruction, the expected integer register width if
it were to use an ireg0.
Right now instructions that do not care about this, because the
instructions in aarch64/Asm do not use an ireg0, return W and simply
should not hit the XZR case.

Also causes a warning due to ambiguous coercions: ireg coerces to both
ireg0 and iregsp, and both of those coerce to dreg.

1 files changed, 128 insertions, 113 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 1abe7d90..63d590e6 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -88,6 +88,19 @@ Inductive crbit: Type :=
 Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
+Inductive dreg : Type :=
+  | DRSP: iregsp -> dreg
+  | DR0: ireg0 -> dreg
+  | DFR: freg -> dreg
+  .
+
+Coercion DRSP: iregsp >-> dreg.
+(* Causes ambiguity warning
+ * ireg can be coerced to either ireg0 or iregsp and both coerce to dreg
+ * However I also want to coerce both XZR and XSP to dreg *)
+Coercion DR0: ireg0 >-> dreg.
+Coercion DFR: freg >-> dreg.
+
 (** We model the following registers of the ARM architecture. *)
 
 Inductive preg: Type :=
@@ -199,7 +212,7 @@ Inductive cf_instruction : Type :=
   | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label)                  (**r branch if bit n is zero *)
   (** Pseudo-instructions *)
   | Pbtbl (r1: ireg) (tbl: list label)                                (**r N-way branch through a jump table *)
-  . 
+  .
 
 (*
 A builtin is considered as a control-flow instruction, because it could emit a trace (cf. Machblock semantics).
@@ -284,7 +297,7 @@ Inductive arith_p : Type :=
   | Pfmovimmd (f: float)                                   (**r load float64 constant *)
 .
 
-Inductive arith_comparison_p : Type :=
+Inductive arith_comparison_d : Type :=
   (** Floating-point comparison *)
   | Pfcmp0 (sz: fsize)                                     (**r compare [r1] and [+0.0] *)
   (** Integer arithmetic, immediate *)
@@ -294,7 +307,7 @@ Inductive arith_comparison_p : Type :=
   | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
 .
 
-Inductive arith_pp : Type :=
+Inductive arith_pd : Type :=
   (** Move integer register *)
   | Pmov
   (** Move wide immediate *)
@@ -332,25 +345,26 @@ Inductive arith_pp : Type :=
   (** Integer arithmetic, immediate *)
   | Paddimm (sz: isize) (n: Z)                        (**r addition *)
   | Psubimm (sz: isize) (n: Z)                        (**r subtraction *)
+  (** Logical, immediate *)
+  | Pandimm (sz: isize) (n: Z)                        (**r and *)
+  | Peorimm (sz: isize) (n: Z)                        (**r xor *)
+  | Porrimm (sz: isize) (n: Z)                        (**r or *)
 .
 
-Inductive arith_comparison_r0r : Type :=
-  (** Integer arithmetic, shifted register *)
-  | Pcmp (is:isize) (s: shift_op)             (**r compare *)
-  | Pcmn (is:isize) (s: shift_op)             (**r compare negative *)
-  (** Logical, shifted register *)
-  | Ptst (is:isize) (s: shift_op)             (**r and, then set flags *)
-.
-
-Inductive arith_comparison_pp : Type :=
+Inductive arith_comparison_dd : Type :=
   (** Integer arithmetic, extending register *)
-  | Pcmpext (x: extend_op)                      (**r int64-int32 cmp *)
-  | Pcmnext (x: extend_op)                      (**r int64-int32 cmn *)
+  | Pcmpext (x: extend_op)                            (**r int64-int32 cmp *)
+  | Pcmnext (x: extend_op)                            (**r int64-int32 cmn *)
   (** Floating-point comparison *)
   | Pfcmp (sz: fsize)                                 (**r compare [r1] and [r2] *)
+  (** Integer arithmetic, shifted register *)
+  | Pcmp (is:isize) (s: shift_op)                     (**r compare *)
+  | Pcmn (is:isize) (s: shift_op)                     (**r compare negative *)
+  (** Logical, shifted register *)
+  | Ptst (is:isize) (s: shift_op)                     (**r and, then set flags *)
 .
 
-Inductive arith_ppp : Type :=
+Inductive arith_pdd : Type :=
   (** Variable shifts *)
   | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
   | Plslv (sz: isize)                                 (**r left shift *)
@@ -369,9 +383,6 @@ Inductive arith_ppp : Type :=
   | Pfdiv (sz: fsize)                                (**r division *)
   | Pfmul (sz: fsize)                                (**r multiplication *)
   | Pfsub (sz: fsize)                                (**r subtraction *)
-.
-
-Inductive arith_rr0r : Type :=
   (** Integer arithmetic, shifted register *)
   | Padd (sz:isize) (s: shift_op)                               (**r addition *)
   | Psub (sz:isize) (s: shift_op)                               (**r subtraction *)
@@ -384,15 +395,7 @@ Inductive arith_rr0r : Type :=
   | Porn (sz:isize) (s: shift_op)                               (**r or-not *)
 .
 
-
-Inductive arith_rr0 : Type :=
-  (** Logical, immediate *)
-  | Pandimm (sz: isize) (n: Z)                     (**r and *)
-  | Peorimm (sz: isize) (n: Z)                     (**r xor *)
-  | Porrimm (sz: isize) (n: Z)                     (**r or *)
-.
-
-Inductive arith_arrrr0 : Type :=
+Inductive arith_apddd : Type :=
   (** Integer multiply/divide *)
   | Pmadd (sz: isize)                               (**r multiply-add *)
   | Pmsub (sz: isize)                               (**r multiply-sub *)
@@ -427,18 +430,15 @@ Inductive arith_arrrr0 : Type :=
  *)
 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)
-  | 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)
+  | PArithPD (i : arith_pd) (rd : preg) (rs : dreg)
+  | PArithPDD (i : arith_pdd) (rd : preg) (r1 r2 : dreg)
+  | PArithAPDDD (i : arith_apddd) (rd : preg) (r1 r2 r3 : dreg)
   (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm
   | PArithAPPPP (i : arith_apppp) (rd r1 r2 r3 : preg) *)
   (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
   | PArithAAPPPP (i : arith_aapppp) (rd r1 r2 r3 : preg) *)
-  | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg)
-  | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg)
-  | PArithComparisonP (i : arith_comparison_p) (r1 : preg)
+  | PArithComparisonD (i : arith_comparison_d) (r1 : dreg)
+  | PArithComparisonDD (i : arith_comparison_dd) (r1 r2 : dreg)
   (* 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)                                  (**r set to 1/0 if cond is true/false *)
@@ -697,15 +697,23 @@ Definition genv := Genv.t fundef unit.
 (** The value of an [ireg0] is either the value of the integer register,
     or 0. *)
 
-Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end.
+Definition dr (is:isize) (rs: regset) (dr: dreg) : val :=
+  match dr with
+  | DFR r => rs (FR r)
+  | DRSP r => rs (IR r)
+  | DR0 r0 =>
+    match r0 with
+    | RR0 r => rs (IR r)
+    | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero
+    end
+  end.
 
 (** Concise notations for accessing and updating the values of registers. *)
 
 Notation "a # b" := (a b) (at level 1, only parsing) : asm.
 Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
-Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm.
-Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm.
+Notation "a ## b" := (dr W a b) (at level 1, only parsing) : asm.
+Notation "a ### b" := (dr X a b) (at level 1, only parsing) : asm.
 
 Open Scope asm.
 
@@ -1192,7 +1200,19 @@ Definition if_opt_bool_val (c: option bool) v1 v2: val :=
    | None => Vundef
    end.
 
-Definition arith_eval_pp i v :=
+Definition arith_pd_isize (i : arith_pd) :=
+  match i with
+  | Pandimm is _ | Peorimm is _ | Porrimm is _ => is
+  (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *)
+  | Pmov        | Pmovk _ _ _  | Paddadr _ _ | Psbfiz _ _ _
+  | Psbfx _ _ _ | Pubfiz _ _ _ | Pubfx _ _ _ | Pfmov
+  | Pfcvtds     | Pfcvtsd      | Pfabs _     | Pfneg _
+  | Pscvtf _ _  | Pucvtf _ _   | Pfcvtzs _ _ | Pfcvtzu _ _
+  | Paddimm _ _ | Psubimm _ _
+    => W
+  end.
+
+Definition arith_eval_pd i v :=
   match i with
   | Pmov => v
   | Pmovk W n pos => insert_in_int v n pos 16
@@ -1233,9 +1253,28 @@ Definition arith_eval_pp i v :=
   | Pucvtf D W => Val.maketotal (Val.floatofintu v)
   | Pucvtf S X => Val.maketotal (Val.singleoflongu v)
   | Pucvtf D X => Val.maketotal (Val.floatoflongu v)
+  | Pandimm W n => Val.and v (Vint (Int.repr n))
+  | Pandimm X n => Val.andl v (Vlong (Int64.repr n))
+  | Peorimm W n => Val.xor v (Vint (Int.repr n))
+  | Peorimm X n => Val.xorl v (Vlong (Int64.repr n))
+  | Porrimm W n => Val.or v (Vint (Int.repr n))
+  | Porrimm X n => Val.orl v (Vlong (Int64.repr n))
+  end.
+
+Definition arith_pdd_isize (i: arith_pdd) :=
+  match i with
+  | Padd is _ | Psub is _ | Pand is _ | Pbic is _
+  | Peon is _ | Peor is _ | Porr is _ | Porn is _
+    => is
+  (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *)
+  | Pasrv _   | Plslv _   | Plsrv _  | Prorv _
+  | Psmulh    | Pumulh    | Psdiv _  | Pudiv _
+  | Paddext _ | Psubext _ | Pfadd _  | Pfdiv _
+  | Pfmul _   | Pfsub _
+    => W
   end.
 
-Definition arith_eval_ppp i v1 v2 :=
+Definition arith_eval_pdd i v1 v2 :=
   match i with
   | Pasrv W => Val.shr v1 v2
   | Pasrv X => Val.shrl v1 v2
@@ -1261,23 +1300,6 @@ Definition arith_eval_ppp i v1 v2 :=
   | Pfmul D => Val.mulf v1 v2
   | Pfsub S => Val.subfs v1 v2
   | Pfsub D => Val.subf v1 v2
-  end.
-
-Definition arith_rr0r_isize (i: arith_rr0r) :=
-  match i with
-  | Padd is _ => is
-  | Psub is _ => is
-  | Pand is _ => is
-  | Pbic is _ => is
-  | Peon is _ => is
-  | Peor is _ => is
-  | Porr is _ => is
-  | Porn is _ => is
-  end.
-
-(* obtain v1 by [ir0 (arith_rr0r_isize i) rs s1] *)
-Definition arith_eval_rr0r i v1 v2 :=
-  match i with
   | Padd W s => Val.add v1 (eval_shift_op_int v2 s)
   | Padd X s => Val.addl v1 (eval_shift_op_long v2 s)
   | Psub W s => Val.sub v1 (eval_shift_op_int v2 s)
@@ -1296,29 +1318,12 @@ Definition arith_eval_rr0r i v1 v2 :=
   | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s))
   end.
 
-Definition arith_rr0_isize (i : arith_rr0) :=
-  match i with
-  | Pandimm is _ | Peorimm is _ | Porrimm is _ => is
-  end.
-
-(* obtain v by [ir0 (arith_rr0_isize i) rs s] *)
-Definition arith_eval_rr0 i v :=
-  match i with
-  | Pandimm W n => Val.and v (Vint (Int.repr n))
-  | Pandimm X n => Val.andl v (Vlong (Int64.repr n))
-  | Peorimm W n => Val.xor v (Vint (Int.repr n))
-  | Peorimm X n => Val.xorl v (Vlong (Int64.repr n))
-  | Porrimm W n => Val.or v (Vint (Int.repr n))
-  | Porrimm X n => Val.orl v (Vlong (Int64.repr n))
-  end.
-
-Definition arith_arrrr0_isize (i : arith_arrrr0) :=
+Definition arith_apddd_isize (i : arith_apddd) :=
   match i with
   | Pmadd is | Pmsub is => is
   end.
 
-(* obtain v3 by [ir0 (arith_arrrr0_isize i) rs s3] *)
-Definition arith_eval_arrrr0 i v1 v2 v3 :=
+Definition arith_eval_apddd i v1 v2 v3 :=
   match i with
   | Pmadd W => Val.add v3 (Val.mul v1 v2)
   | Pmadd X => Val.addl v3 (Val.mull v1 v2)
@@ -1326,22 +1331,20 @@ Definition arith_eval_arrrr0 i v1 v2 v3 :=
   | Pmsub X => Val.subl v3 (Val.mull v1 v2)
   end.
 
-Definition arith_prepare_comparison_pp i (v1 v2 : val) :=
+Definition arith_comparison_dd_isize i :=
   match i with
-  | Pcmpext x => (v1, (eval_extend v2 x))
-  | Pcmnext x => (v1, (Val.negl (eval_extend v2 x)))
-  | Pfcmp _ => (v1, v2)
+  | Pcmp is _ | Pcmn is _ | Ptst is _
+    => is
+  (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *)
+  | Pcmpext _ | Pcmnext _ | Pfcmp _
+    => W
   end.
 
-Definition arith_comparison_r0r_isize i :=
-  match i with
-  | Pcmp is _ => is
-  | Pcmn is _ => is
-  | Ptst is _ => is
-  end.
-
-Definition arith_prepare_comparison_r0r i v1 v2 :=
+Definition arith_prepare_comparison_dd 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)
   | Pcmp W s => (v1, (eval_shift_op_int v2 s))
   | Pcmp X s => (v1, (eval_shift_op_long v2 s))
   | Pcmn W s => (v1, (Val.neg (eval_shift_op_int v2 s)))
@@ -1350,7 +1353,14 @@ Definition arith_prepare_comparison_r0r i v1 v2 :=
   | Ptst X s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
   end.
 
-Definition arith_prepare_comparison_p i v :=
+Definition arith_comparison_d_isize i :=
+  match i with
+  (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *)
+  | Pcmpimm _ _ | Pcmnimm _ _ | Ptstimm _ _ | Pfcmp0 _
+    => W
+  end.
+
+Definition arith_prepare_comparison_d i v :=
   match i with
   | Pcmpimm W n => (v, (Vint (Int.repr n)))
   | Pcmpimm X n => (v, (Vlong (Int64.repr n)))
@@ -1362,14 +1372,17 @@ Definition arith_prepare_comparison_p i v :=
   | Pfcmp0 D => (v, (Vfloat Float.zero))
   end.
 
-Definition arith_comparison_pp_compare i :=
+Definition arith_comparison_dd_compare i :=
   match i with
-  | Pcmpext _ | Pcmnext _ => compare_long
+  | Pcmp W _ | Pcmn W _ | Ptst W _
+    => compare_int
+  | Pcmp X _ | Pcmn X _ | Ptst X _ | Pcmpext _ | Pcmnext _
+    => compare_long
   | Pfcmp S => compare_single
   | Pfcmp D => compare_float
   end.
 
-Definition arith_comparison_p_compare i :=
+Definition arith_comparison_d_compare i :=
    match i with
    | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int
    | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long
@@ -1380,26 +1393,28 @@ 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)
-  | 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)
-
-  | PArithRR0R i d s1 s2 => rs#d <- (arith_eval_rr0r i (ir0 (arith_rr0r_isize i) rs s1) rs#s2)
-
-  | PArithRR0 i d s => rs#d <- (arith_eval_rr0 i (ir0 (arith_rr0_isize i) rs s))
-
-  | PArithARRRR0 i d s1 s2 s3 =>
-    rs#d <- (arith_eval_arrrr0 i rs#s1 rs#s2 (ir0 (arith_arrrr0_isize i) rs s3))
-
-  | PArithComparisonPP i s1 s2 =>
-    let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in
-    arith_comparison_pp_compare i rs v1 v2
-  | PArithComparisonR0R i s1 s2 =>
-    let is := arith_comparison_r0r_isize i in
-    let (v1, v2) := arith_prepare_comparison_r0r i (ir0 is rs s1) rs#s2 in
-    (if is (* is W *) then compare_int else compare_long) rs v1 v2
-  | PArithComparisonP i s =>
-    let (v1, v2) := arith_prepare_comparison_p i rs#s in
-    arith_comparison_p_compare i rs v1 v2
+  | PArithPD i d s =>
+    let is := arith_pd_isize i in
+    let get_val := (dr is rs) in
+    rs#d <- (arith_eval_pd i (get_val s))
+  | PArithPDD i d s1 s2 =>
+    let is := arith_pdd_isize i in
+    let get_val := (dr is rs) in
+    rs#d <- (arith_eval_pdd i (get_val s1) (get_val s2))
+  | PArithAPDDD i d s1 s2 s3 =>
+    let is := arith_apddd_isize i in
+    let get_val := (dr is rs) in
+    rs#d <- (arith_eval_apddd i (get_val s1) (get_val s2) (get_val s3))
+  | PArithComparisonDD i s1 s2 =>
+    let is := arith_comparison_dd_isize i in
+    let get_val := (dr is rs) in
+    let (v1, v2) := arith_prepare_comparison_dd i (get_val s1) (get_val s2) in
+    arith_comparison_dd_compare i rs v1 v2
+  | PArithComparisonD i s =>
+    let is := arith_comparison_d_isize i in
+    let get_val := (dr is rs) in
+    let (v1, v2) := arith_prepare_comparison_d i (get_val s) in
+    arith_comparison_d_compare i rs v1 v2
   | 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)