diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-06 15:45:53 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-06 15:58:59 +0200 |
| commit | af274a2746a6b16ff8946f417dd860da5c0e6740 (patch) | |
| tree | 3c8460ff34c751affded16ffc99466b2116fcba8 /aarch64/Asmblock.v | |
| parent | 397dfb4cd5d207fcbffbfc54a9a4f9a8b756598d (diff) | |
| download | compcert-kvx-af274a2746a6b16ff8946f417dd860da5c0e6740.tar.gz compcert-kvx-af274a2746a6b16ff8946f417dd860da5c0e6740.zip | |
aarch64/Asmblock: Change PArithAFFF to PArithPPP for consistency
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 33 |
1 files changed, 17 insertions, 16 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index ffe24832..09228abc 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -458,22 +458,23 @@ Inductive arith_x_arrrr0 : Type := | PmsubX (**r multiply-sub *) . -Inductive arith_afff : Type := +Inductive arith_appp : Type := (** Floating-point arithmetic *) | Pfnmul (sz: fsize) (**r multiply-negate *) . -Inductive arith_affff : Type := - (** Floating-point arithmetic *) - | Pfmadd (sz: fsize) (**r [rd = r3 + r1 * r2] *) - | Pfmsub (sz: fsize) (**r [rd = r3 - r1 * r2] *) -. +(* Currently not used by the semantics of aarch64/Asm + * Inductive arith_apppp : Type := + * (** Floating-point arithmetic *) + * | Pfmadd (sz: fsize) (**r [rd = r3 + r1 * r2] *) + * | Pfmsub (sz: fsize) (**r [rd = r3 - r1 * r2] *) + * . -Inductive arith_aaffff : Type := - (** Floating-point arithmetic *) - | Pfnmadd (sz: fsize) (**r [rd = - r3 - r1 * r2] *) - | Pfnmsub (sz: fsize) (**r [rd = - r3 + r1 * r2] *) -. + * Inductive arith_aapppp : Type := + * (** Floating-point arithmetic *) + * | Pfnmadd (sz: fsize) (**r [rd = - r3 - r1 * r2] *) + * | Pfnmsub (sz: fsize) (**r [rd = - r3 + r1 * r2] *) + * . *) (* Notes on the naming scheme used here: * R: ireg @@ -503,11 +504,11 @@ Inductive ar_instruction : Type := | PArithXARRRR0 (i : arith_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0) | PArithSWFR0 (i : arith_sw_fr0) (rd : freg) (rs : ireg0) | PArithDXFR0 (i : arith_dx_fr0) (rd : freg) (rs : ireg0) - | PArithAFFF (i : arith_afff) (rd r1 r2 : freg) + | PArithAPPP (i : arith_appp) (rd r1 r2 : preg) (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm - | PArithAFFFF (i : arith_affff) (rd r1 r2 r3 : freg) *) + | PArithAPPPP (i : arith_apppp) (rd r1 r2 r3 : preg) *) (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm - | PArithAAFFFF (i : arith_aaffff) (rd r1 r2 r3 : freg) *) + | PArithAAPPPP (i : arith_aapppp) (rd r1 r2 r3 : preg) *) | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg) | PArithComparisonWR0R (i : arith_comparison_w_r0r) (r1 : ireg0) (r2 : ireg) | PArithComparisonXR0R (i : arith_comparison_x_r0r) (r1 : ireg0) (r2 : ireg) @@ -1417,7 +1418,7 @@ Definition arith_eval_dx_fr0 i v := | PfmoviDX => float64_of_bits v end. -Definition arith_eval_afff i v1 v2 := +Definition arith_eval_appp i v1 v2 := match i with | Pfnmul S => Val.negfs (Val.mulfs v1 v2) | Pfnmul D => Val.negf (Val.mulf v1 v2) @@ -1476,7 +1477,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithSWFR0 i d s => rs#d <- (arith_eval_sw_fr0 i rs##s) | PArithDXFR0 i d s => rs#d <- (arith_eval_dx_fr0 i rs###s) - | PArithAFFF i d s1 s2 => rs#d <- (arith_eval_afff i rs#s1 rs#s2) + | PArithAPPP i d s1 s2 => rs#d <- (arith_eval_appp i rs#s1 rs#s2) | PArithComparisonPP i s1 s2 => let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in |