Asmblock.dreg: Use option (monad) for dealing with instruction sizes

This makes it more clear, and explicit, when we care about the expected
register width for an instruction in case an ireg0 will be used.

1 files changed, 62 insertions, 39 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 63d590e6..efaaf839 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -697,14 +697,22 @@ Definition genv := Genv.t fundef unit.
 (** The value of an [ireg0] is either the value of the integer register,
     or 0. *)
 
-Definition dr (is:isize) (rs: regset) (dr: dreg) : val :=
+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 => rs (FR r)
-  | DRSP r => rs (IR r)
+  | DFR r => Some (rs (FR r))
+  | DRSP r => Some (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
+    | 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.
 
@@ -712,8 +720,9 @@ Definition dr (is:isize) (rs: regset) (dr: dreg) : val :=
 
 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" := (dr W a b) (at level 1, only parsing) : asm.
-Notation "a ### b" := (dr X a b) (at level 1, only parsing) : 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.
 
@@ -1200,16 +1209,15 @@ Definition if_opt_bool_val (c: option bool) v1 v2: val :=
    | None => Vundef
    end.
 
-Definition arith_pd_isize (i : arith_pd) :=
+Definition arith_pd_isize (i : arith_pd) : option isize :=
   match i with
-  | Pandimm is _ | Peorimm is _ | Porrimm is _ => is
-  (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *)
+  | 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 _ _
-    => W
+    => None
   end.
 
 Definition arith_eval_pd i v :=
@@ -1261,17 +1269,17 @@ Definition arith_eval_pd i v :=
   | Porrimm X n => Val.orl v (Vlong (Int64.repr n))
   end.
 
-Definition arith_pdd_isize (i: arith_pdd) :=
+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 _
-    => 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 _
-    => W
+    => None
   end.
 
 Definition arith_eval_pdd i v1 v2 :=
@@ -1318,9 +1326,9 @@ 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) :=
+Definition arith_apddd_isize (i : arith_apddd) : option isize :=
   match i with
-  | Pmadd is | Pmsub is => is
+  | Pmadd is | Pmsub is => Some is
   end.
 
 Definition arith_eval_apddd i v1 v2 v3 :=
@@ -1331,13 +1339,12 @@ Definition arith_eval_apddd i v1 v2 v3 :=
   | Pmsub X => Val.subl v3 (Val.mull v1 v2)
   end.
 
-Definition arith_comparison_dd_isize i :=
+Definition arith_comparison_dd_isize (i : arith_comparison_dd) : option isize :=
   match i with
   | Pcmp is _ | Pcmn is _ | Ptst is _
-    => is
-  (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *)
+    => Some is
   | Pcmpext _ | Pcmnext _ | Pfcmp _
-    => W
+    => None
   end.
 
 Definition arith_prepare_comparison_dd i (v1 v2 : val) :=
@@ -1353,11 +1360,10 @@ 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 :=
+Definition arith_comparison_d_isize (i : arith_comparison_d) : option isize :=
   match i with
-  (* Arbitrary isize because in aarch64/Asm these instructions do not use an ireg0 *)
   | Pcmpimm _ _ | Pcmnimm _ _ | Ptstimm _ _ | Pfcmp0 _
-    => W
+    => None
   end.
 
 Definition arith_prepare_comparison_d i v :=
@@ -1390,43 +1396,60 @@ Definition arith_comparison_d_compare i :=
    | Pfcmp0 D => compare_float
    end.
 
-Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
+Definition exec_arith_instr (ai: ar_instruction) (rs: regset): option regset :=
   match ai with
-  | PArithP i d => rs#d <- (arith_eval_p i)
+  | 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
-    rs#d <- (arith_eval_pd i (get_val s))
+    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
-    rs#d <- (arith_eval_pdd i (get_val s1) (get_val s2))
+    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
-    rs#d <- (arith_eval_apddd i (get_val s1) (get_val s2) (get_val s3))
+    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
-    let (v1, v2) := arith_prepare_comparison_dd i (get_val s1) (get_val s2) in
-    arith_comparison_dd_compare i rs v1 v2
+    (* 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
-    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)
-  | 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))
+    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)))
   end.
 
 (* basic exec *)
 Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
   match b with
-  | PArith ai => Next (exec_arith_instr ai rs) m
+  | PArith ai =>
+    SOME rs' <- exec_arith_instr ai rs IN
+    Next 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 =>