Revert introduction of dreg

This everts commits 91f991ab and df253300

1 files changed, 120 insertions, 158 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index efaaf839..1abe7d90 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -88,19 +88,6 @@ 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 :=
@@ -212,7 +199,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).
@@ -297,7 +284,7 @@ Inductive arith_p : Type :=
   | Pfmovimmd (f: float)                                   (**r load float64 constant *)
 .
 
-Inductive arith_comparison_d : Type :=
+Inductive arith_comparison_p : Type :=
   (** Floating-point comparison *)
   | Pfcmp0 (sz: fsize)                                     (**r compare [r1] and [+0.0] *)
   (** Integer arithmetic, immediate *)
@@ -307,7 +294,7 @@ Inductive arith_comparison_d : Type :=
   | Ptstimm (sz: isize) (n: Z)                        (**r and, then set flags *)
 .
 
-Inductive arith_pd : Type :=
+Inductive arith_pp : Type :=
   (** Move integer register *)
   | Pmov
   (** Move wide immediate *)
@@ -345,26 +332,25 @@ Inductive arith_pd : 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_dd : Type :=
+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 :=
   (** 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_pdd : Type :=
+Inductive arith_ppp : Type :=
   (** Variable shifts *)
   | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
   | Plslv (sz: isize)                                 (**r left shift *)
@@ -383,6 +369,9 @@ Inductive arith_pdd : 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 *)
@@ -395,7 +384,15 @@ Inductive arith_pdd : Type :=
   | Porn (sz:isize) (s: shift_op)                               (**r or-not *)
 .
 
-Inductive arith_apddd : Type :=
+
+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 :=
   (** Integer multiply/divide *)
   | Pmadd (sz: isize)                               (**r multiply-add *)
   | Pmsub (sz: isize)                               (**r multiply-sub *)
@@ -430,15 +427,18 @@ Inductive arith_apddd : Type :=
  *)
 Inductive ar_instruction : Type :=
   | PArithP (i : arith_p) (rd : preg)
-  | 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)
+  | 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)
   (* 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) *)
-  | PArithComparisonD (i : arith_comparison_d) (r1 : dreg)
-  | PArithComparisonDD (i : arith_comparison_dd) (r1 r2 : dreg)
+  | 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 : ireg) (c : testcond)                                  (**r set to 1/0 if cond is true/false *)
@@ -698,23 +698,7 @@ Definition genv := Genv.t fundef unit.
     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: option isize) (rs: regset) (dr: dreg) : option val :=
-  match dr with
-  | DFR r => Some (rs (FR r))
-  | DRSP r => Some (rs (IR r))
-  | DR0 r0 =>
-    match r0 with
-    | RR0 r => Some (rs (IR r))
-    | XZR =>
-      match is with
-      | Some W => Some (Vint Int.zero)
-      | Some X => Some (Vlong Int64.zero)
-      | None => None
-      end
-    end
-  end.
+  match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end.
 
 (** Concise notations for accessing and updating the values of registers. *)
 
@@ -723,7 +707,6 @@ 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.
 
-
 Open Scope asm.
 
 (** Undefining some registers *)
@@ -1209,18 +1192,7 @@ Definition if_opt_bool_val (c: option bool) v1 v2: val :=
    | None => Vundef
    end.
 
-Definition arith_pd_isize (i : arith_pd) : option isize :=
-  match i with
-  | Pandimm is _ | Peorimm is _ | Porrimm is _ => Some is
-  | Pmov        | Pmovk _ _ _  | Paddadr _ _ | Psbfiz _ _ _
-  | Psbfx _ _ _ | Pubfiz _ _ _ | Pubfx _ _ _ | Pfmov
-  | Pfcvtds     | Pfcvtsd      | Pfabs _     | Pfneg _
-  | Pscvtf _ _  | Pucvtf _ _   | Pfcvtzs _ _ | Pfcvtzu _ _
-  | Paddimm _ _ | Psubimm _ _
-    => None
-  end.
-
-Definition arith_eval_pd i v :=
+Definition arith_eval_pp i v :=
   match i with
   | Pmov => v
   | Pmovk W n pos => insert_in_int v n pos 16
@@ -1261,28 +1233,9 @@ Definition arith_eval_pd 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) : option isize :=
-  match i with
-  | Padd is _ | Psub is _ | Pand is _ | Pbic is _
-  | Peon is _ | Peor is _ | Porr is _ | Porn is _
-    => Some 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 _
-    => None
   end.
 
-Definition arith_eval_pdd i v1 v2 :=
+Definition arith_eval_ppp i v1 v2 :=
   match i with
   | Pasrv W => Val.shr v1 v2
   | Pasrv X => Val.shrl v1 v2
@@ -1308,6 +1261,23 @@ Definition arith_eval_pdd 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)
@@ -1326,12 +1296,29 @@ Definition arith_eval_pdd i v1 v2 :=
   | Porn X s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s))
   end.
 
-Definition arith_apddd_isize (i : arith_apddd) : option isize :=
+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
-  | Pmadd is | Pmsub is => Some is
+  | 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_eval_apddd i v1 v2 v3 :=
+Definition arith_arrrr0_isize (i : arith_arrrr0) :=
+  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 :=
   match i with
   | Pmadd W => Val.add v3 (Val.mul v1 v2)
   | Pmadd X => Val.addl v3 (Val.mull v1 v2)
@@ -1339,19 +1326,22 @@ Definition arith_eval_apddd i v1 v2 v3 :=
   | Pmsub X => Val.subl v3 (Val.mull v1 v2)
   end.
 
-Definition arith_comparison_dd_isize (i : arith_comparison_dd) : option isize :=
-  match i with
-  | Pcmp is _ | Pcmn is _ | Ptst is _
-    => Some is
-  | Pcmpext _ | Pcmnext _ | Pfcmp _
-    => None
-  end.
-
-Definition arith_prepare_comparison_dd 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_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 :=
+  match i with
   | 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)))
@@ -1360,13 +1350,7 @@ Definition arith_prepare_comparison_dd i (v1 v2 : val) :=
   | Ptst X s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
   end.
 
-Definition arith_comparison_d_isize (i : arith_comparison_d) : option isize :=
-  match i with
-  | Pcmpimm _ _ | Pcmnimm _ _ | Ptstimm _ _ | Pfcmp0 _
-    => None
-  end.
-
-Definition arith_prepare_comparison_d i v :=
+Definition arith_prepare_comparison_p i v :=
   match i with
   | Pcmpimm W n => (v, (Vint (Int.repr n)))
   | Pcmpimm X n => (v, (Vlong (Int64.repr n)))
@@ -1378,17 +1362,14 @@ Definition arith_prepare_comparison_d i v :=
   | Pfcmp0 D => (v, (Vfloat Float.zero))
   end.
 
-Definition arith_comparison_dd_compare i :=
+Definition arith_comparison_pp_compare i :=
   match i with
-  | Pcmp W _ | Pcmn W _ | Ptst W _
-    => compare_int
-  | Pcmp X _ | Pcmn X _ | Ptst X _ | Pcmpext _ | Pcmnext _
-    => compare_long
+  | Pcmpext _ | Pcmnext _ => compare_long
   | Pfcmp S => compare_single
   | Pfcmp D => compare_float
   end.
 
-Definition arith_comparison_d_compare i :=
+Definition arith_comparison_p_compare i :=
    match i with
    | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int
    | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long
@@ -1396,60 +1377,41 @@ Definition arith_comparison_d_compare i :=
    | Pfcmp0 D => compare_float
    end.
 
-Definition exec_arith_instr (ai: ar_instruction) (rs: regset): option regset :=
+Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
-  | PArithP i d => Some (rs#d <- (arith_eval_p i))
-  | PArithPD i d s =>
-    let is := arith_pd_isize i in
-    let get_val := (dr is rs) in
-    SOME v <- (get_val s) IN
-    Some (rs#d <- (arith_eval_pd i v))
-  | PArithPDD i d s1 s2 =>
-    let is := arith_pdd_isize i in
-    let get_val := (dr is rs) in
-    SOME v1 <- (get_val s1) IN
-    SOME v2 <- (get_val s2) IN
-    Some (rs#d <- (arith_eval_pdd i v1 v2))
-  | PArithAPDDD i d s1 s2 s3 =>
-    let is := arith_apddd_isize i in
-    let get_val := (dr is rs) in
-    SOME v1 <- (get_val s1) IN
-    SOME v2 <- (get_val s2) IN
-    SOME v3 <- (get_val s3) IN
-    Some (rs#d <- (arith_eval_apddd i v1 v2 v3))
-  | PArithComparisonDD i s1 s2 =>
-    let is := arith_comparison_dd_isize i in
-    let get_val := (dr is rs) in
-    (* register values *)
-    SOME rv1 <- (get_val s1) IN
-    SOME rv2 <- (get_val s2) IN
-    let (v1, v2) := arith_prepare_comparison_dd i rv1 rv2 in
-    Some (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
-    SOME rv <- (get_val s) IN
-    let (v1, v2) := arith_prepare_comparison_d i rv in
-    Some (arith_comparison_d_compare i rs v1 v2)
-  | Pcset d c =>
-      Some (rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero)))
-  | Pfmovi S d s =>
-    SOME v <- dr (Some W) rs s IN
-    Some (rs#d <- (float32_of_bits v))
-  | Pfmovi D d s =>
-    SOME v <- dr (Some X) rs s IN
-    Some (rs#d <- (float64_of_bits v))
-  | Pcsel d s1 s2 c => Some (rs#d <- (if_opt_bool_val (eval_testcond c rs) (rs#s1) (rs#s2)))
-  | Pfnmul S d s1 s2 => Some (rs#d <- (Val.negfs (Val.mulfs rs#s1 rs#s2)))
-  | Pfnmul D d s1 s2 => Some (rs#d <- (Val.negf (Val.mulf rs#s1 rs#s2)))
+  | 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
+  | 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))
+  | Pfnmul S d s1 s2 => rs#d <- (Val.negfs (Val.mulfs rs#s1 rs#s2))
+  | Pfnmul D d s1 s2 => rs#d <- (Val.negf (Val.mulf rs#s1 rs#s2))
   end.
 
 (* basic exec *)
 Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
   match b with
-  | PArith ai =>
-    SOME rs' <- exec_arith_instr ai rs IN
-    Next rs' m
+  | PArith ai => Next (exec_arith_instr ai rs) m
   | PLoad ld rd a => exec_load (chunk_load_rd_a ld) (interp_load_rd_a ld) a rd rs m
   | PStore st r a => exec_store (chunk_store_rs_a st) a rs#r rs m
   | Pallocframe sz pos =>