diff options
Diffstat (limited to 'kvx/Asmvliw.v')
| -rw-r--r-- | kvx/Asmvliw.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index 45b230e6..0ce2ed69 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -472,6 +472,9 @@ Inductive arith_name_rrr : Type := | Pfminw (**r float min word *) | Pfmaxd (**r float max double *) | Pfmaxw (**r float max word *) + + | Pabdw (**r absolute value of difference *) + | Pabdl (**r absolute value of difference *) . Inductive arith_name_rri32 : Type := @@ -499,6 +502,7 @@ Inductive arith_name_rri32 : Type := | Psrlil (**r shift right logical immediate long *) | Psrail (**r shift right arithmetic immediate long *) | Psrxil (**r shift right arithmetic immediate long round to 0*) + | Pabdiw (**r absolute value of difference *) . Inductive arith_name_rri64 : Type := @@ -516,6 +520,7 @@ Inductive arith_name_rri64 : Type := | Pnxoril (**r nxor immediate long *) | Pandnil (**r andn immediate long *) | Pornil (**r orn immediate long *) + | Pabdil (**r absolute value of difference *) . Inductive arith_name_arrr : Type := @@ -1033,6 +1038,9 @@ Definition arith_eval_rrr n v1 v2 := | Prevsubxw shift => ExtValues.revsubx (int_of_shift1_4 shift) v1 v2 | Prevsubxl shift => ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2 + + | Pabdw => ExtValues.absdiff v1 v2 + | Pabdl => ExtValues.absdiffl v1 v2 end. Definition arith_eval_rri32 n v i := @@ -1060,6 +1068,7 @@ Definition arith_eval_rri32 n v i := | Psrail => Val.shrl v (Vint i) | Paddxiw shift => ExtValues.addx (int_of_shift1_4 shift) v (Vint i) | Prevsubxiw shift => ExtValues.revsubx (int_of_shift1_4 shift) v (Vint i) + | Pabdiw => ExtValues.absdiff v (Vint i) end. Definition arith_eval_rri64 n v i := @@ -1078,6 +1087,7 @@ Definition arith_eval_rri64 n v i := | Pornil => Val.orl (Val.notl v) (Vlong i) | Paddxil shift => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i) | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i) + | Pabdil => ExtValues.absdiffl v (Vlong i) end. Definition cmove bt v1 v2 v3 := |