diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-17 10:22:15 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-17 10:22:15 +0100 |
| commit | 471a8363c185e073fdfb8aefeb863b215870285d (patch) | |
| tree | 511160c38944b6bea7c64359ca0e890d8c5c7bbf /aarch64/Asm.v | |
| parent | a71ed69400fbd8f6533a32c117e7063f6b083049 (diff) | |
| parent | a644da350c329d302150310a0995ccf1f72937e5 (diff) | |
| download | compcert-kvx-471a8363c185e073fdfb8aefeb863b215870285d.tar.gz compcert-kvx-471a8363c185e073fdfb8aefeb863b215870285d.zip | |
Merge branch 'kvx-work' into aarch64-peephole
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 5d9cf601..30bac2a4 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -255,6 +255,7 @@ Inductive instruction: Type := | Pclz (sz: isize) (rd r1: ireg) (**r count leading zero bits *) | Prev (sz: isize) (rd r1: ireg) (**r reverse bytes *) | Prev16 (sz: isize) (rd r1: ireg) (**r reverse bytes in each 16-bit word *) + | Prbit (sz: isize) (rd r1: ireg) (**r reverse bits *) (** Conditional data processing *) | Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond) (**r int conditional move *) | Pcset (rd: ireg) (c: testcond) (**r set to 1/0 if cond is true/false *) @@ -300,6 +301,8 @@ Inductive instruction: Type := | Pfmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = r3 - r1 * r2] *) | Pfnmadd (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 - r1 * r2] *) | Pfnmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 + r1 * r2] *) + | Pfmax (sz: fsize) (rd r1 r2: freg) (**r maximum *) + | Pfmin (sz: fsize) (rd r1 r2: freg) (**r minimum *) (** Floating-point comparison *) | Pfcmp (sz: fsize) (r1 r2: freg) (**r compare [r1] and [r2] *) | Pfcmp0 (sz: fsize) (r1: freg) (**r compare [r1] and [+0.0] *) @@ -1304,7 +1307,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Vint n => match list_nth_z tbl (Int.unsigned n) with | None => Stuck - | Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m + | Some lbl => goto_label f lbl (rs#X16 <- Vundef) m end | _ => Stuck end @@ -1324,11 +1327,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pclz _ _ _ | Prev _ _ _ | Prev16 _ _ _ + | Prbit _ _ _ | Pfsqrt _ _ _ | Pfmadd _ _ _ _ _ | Pfmsub _ _ _ _ _ | Pfnmadd _ _ _ _ _ | Pfnmsub _ _ _ _ _ + | Pfmax _ _ _ _ + | Pfmin _ _ _ _ | Pcfi_adjust _ | Pcfi_rel_offset _ => Stuck @@ -1351,7 +1357,7 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge vargs m t vres m' -> rs' = nextinstr (set_res res vres - (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> + (undef_regs (DR X16 :: DR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', |