aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Asmblock.v')
-rw-r--r--aarch64/Asmblock.v101
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 =>
generated by cgit (git 2.34.1) at 2024-06-13 10:31:41 +0000