diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-08 10:44:34 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-08 10:44:34 +0200 |
| commit | 2246044e99569fcf1c2172f0e710134123be8b49 (patch) | |
| tree | df56ebe23cb71259f346ee1f73fafe3f9a96e476 /powerpc/Asm.v | |
| parent | 73e20bd6e0586e38fbc7d87d8c306fad7b578418 (diff) | |
| download | compcert-kvx-2246044e99569fcf1c2172f0e710134123be8b49.tar.gz compcert-kvx-2246044e99569fcf1c2172f0e710134123be8b49.zip | |
Added builtin for isel.
The builtin_isel function takes a _Bool as first argument and returns
either the second or the third depending on the value of the _Bool.
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 796bad3d..3c7bdd15 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -207,6 +207,7 @@ Inductive instruction : Type := | Pfrsqrte: freg -> freg -> instruction (**r approximate reciprocal of square root *) | Pfres: freg -> freg -> instruction (**r approximate inverse *) | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) + | Pisel: ireg -> ireg -> ireg -> crbit -> instruction (**r integer select *) | Pisync: instruction (**r ISYNC barrier *) | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) | Picbtls: int -> ireg -> ireg -> instruction (**r instruction cache block touch and lock set *) @@ -893,6 +894,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfrsqrte _ _ | Pfres _ _ | Pfsel _ _ _ _ + | Pisel _ _ _ _ | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ |