diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-04 18:48:28 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-04 18:55:21 +0200 |
| commit | 90be0b41fb084d8c12f78f9ce2d11edcaf93d238 (patch) | |
| tree | bdf69648884541da4d02a63b4d8bdc9ab215f8e6 /aarch64/Asmblock.v | |
| parent | 905d01a91864243ab2ea88ce9a5e5196f8584ae2 (diff) | |
| download | compcert-kvx-90be0b41fb084d8c12f78f9ce2d11edcaf93d238.tar.gz compcert-kvx-90be0b41fb084d8c12f78f9ce2d11edcaf93d238.zip | |
Asmblock: Merge PArithFF32 and PArithFF64 into PArithF
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 28 |
1 files changed, 9 insertions, 19 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index fe98e9f2..06d80425 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -390,14 +390,10 @@ Inductive arith_name_comparison_r : Type := | Ptstimm (sz: isize) (n: Z) (**r and, then set flags *) . -Inductive arith_name_ff32 : Type := +Inductive arith_name_f : Type := (** Floating-point move *) - | Pfmovimms (**r load float32 constant *) -. - -Inductive arith_name_ff64 : Type := - (** Floating-point move *) - | Pfmovimmd (**r load float64 constant *) + | Pfmovimms (f: float32) (**r load float32 constant *) + | Pfmovimmd (f: float) (**r load float64 constant *) . Inductive arith_name_rrr : Type := @@ -542,9 +538,8 @@ Inductive ar_instruction : Type := | PArithRspRsp (i : arith_name_rsprsp) (rd r1 : iregsp) | PArithWARRRR0 (i : arith_name_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0) | PArithXARRRR0 (i : arith_name_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0) + | PArithF (i : arith_name_f) (rd : freg) | PArithFF (i : arith_name_ff) (rd rs : freg) - | PArithFF32 (i : arith_name_ff32) (rd : freg) (f : float32) - | PArithFF64 (i : arith_name_ff64) (rd : freg) (f : float) | PArithFR (i : arith_name_fr) (rd : freg) (rs : ireg) | PArithSWFR0 (i : arith_name_sw_fr0) (rd : freg) (rs : ireg0) | PArithDXFR0 (i : arith_name_dx_fr0) (rd : freg) (rs : ireg0) @@ -1427,14 +1422,10 @@ Definition arith_eval_ff n v := | Pfneg D => Val.negf v end. -Definition arith_eval_ff32 n i := - match n with - | Pfmovimms => Vsingle i - end. - -Definition arith_eval_ff64 n i := - match n with - | Pfmovimmd => Vfloat i +Definition arith_eval_f i := + match i with + | Pfmovimms f => Vsingle f + | Pfmovimmd f => Vfloat f end. Definition arith_eval_fr n v := @@ -1540,9 +1531,8 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithWARRRR0 n d s1 s2 s3 => rs#d <- (arith_eval_w_arrrr0 n rs#s1 rs#s2 rs##s3) | PArithXARRRR0 n d s1 s2 s3 => rs#d <- (arith_eval_x_arrrr0 n rs#s1 rs#s2 rs###s3) + | PArithF n d => rs#d <- (arith_eval_f n) | PArithFF n d s => rs#d <- (arith_eval_ff n rs#s) - | PArithFF32 n d i => rs#d <- (arith_eval_ff32 n i) - | PArithFF64 n d i => rs#d <- (arith_eval_ff64 n i) | PArithFR n d s => rs#d <- (arith_eval_fr n rs#s) | PArithSWFR0 n d s => rs#d <- (arith_eval_sw_fr0 n rs##s) |