diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-12 12:41:49 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-12 12:41:49 +0200 |
commit | 644814b1b266f5492e6ffd24776fc87c30acd57b (patch) | |
tree | 2e2f38d9274fbe3d8c25ab8a8e5dc5dcdb22b483 /mppa_k1c/Asmvliw.v | |
parent | 41cac0e437d63399f46ac3c4b5c7ad2c23f88c5e (diff) | |
download | compcert-kvx-644814b1b266f5492e6ffd24776fc87c30acd57b.tar.gz compcert-kvx-644814b1b266f5492e6ffd24776fc87c30acd57b.zip |
standardize semantics, 1
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
-rw-r--r-- | mppa_k1c/Asmvliw.v | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 9a933741..886228ad 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1071,9 +1071,8 @@ Definition arith_eval_rrr n v1 v2 := | Paddxw shift => ExtValues.addx (int_of_shift1_4 shift) v1 v2 | Paddxl shift => ExtValues.addxl (int_of_shift1_4 shift) v1 v2 - | Prevsubxw shift => Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))) - - | Prevsubxl shift => Val.subl v2 (Val.shll v1 (Vint (int_of_shift1_4 shift))) + | Prevsubxw shift => ExtValues.revsubx (int_of_shift1_4 shift) v1 v2 + | Prevsubxl shift => ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2 end. Definition arith_eval_rri32 n v i := @@ -1100,7 +1099,7 @@ Definition arith_eval_rri32 n v i := | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) | Paddxiw shift => ExtValues.addx (int_of_shift1_4 shift) v (Vint i) - | Prevsubxiw shift => Val.sub (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift))) + | Prevsubxiw shift => ExtValues.revsubx (int_of_shift1_4 shift) v (Vint i) end. Definition arith_eval_rri64 n v i := @@ -1117,8 +1116,8 @@ Definition arith_eval_rri64 n v i := | Pnxoril => Val.notl (Val.xorl v (Vlong i)) | Pandnil => Val.andl (Val.notl v) (Vlong i) | Pornil => Val.orl (Val.notl v) (Vlong i) - | Paddxil shift => Val.addl (Vlong i) (Val.shll v (Vint (int_of_shift1_4 shift))) - | Prevsubxil shift => Val.subl (Vlong i) (Val.shll v (Vint (int_of_shift1_4 shift))) + | Paddxil shift => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i) + | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i) end. Definition arith_eval_arrr n v1 v2 v3 := |