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 | |
| parent | 41cac0e437d63399f46ac3c4b5c7ad2c23f88c5e (diff) | |
| download | compcert-kvx-644814b1b266f5492e6ffd24776fc87c30acd57b.tar.gz compcert-kvx-644814b1b266f5492e6ffd24776fc87c30acd57b.zip | |
standardize semantics, 1
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 11 | ||||
| -rw-r--r-- | mppa_k1c/ExtValues.v | 8 |
2 files changed, 12 insertions, 7 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 := diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 284d55f3..9169cf13 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -204,4 +204,10 @@ Definition addx sh v1 v2 := Val.add v2 (Val.shl v1 (Vint sh)). Definition addxl sh v1 v2 := - Val.addl v2 (Val.shll v1 (Vint sh)).
\ No newline at end of file + Val.addl v2 (Val.shll v1 (Vint sh)). + +Definition revsubx sh v1 v2 := + Val.sub v2 (Val.shl v1 (Vint sh)). + +Definition revsubxl sh v1 v2 := + Val.subl v2 (Val.shll v1 (Vint sh)).
\ No newline at end of file |