diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 18:19:01 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 18:19:01 +0100 |
| commit | afe54de36234834449e72d9dc891a90291aadcb1 (patch) | |
| tree | 540eae7d0c2c4ae2e97125587da8df9f3e6378f3 | |
| parent | 7d60eca51d9f1815834a132eb634b251bdfb6e6b (diff) | |
| download | compcert-kvx-afe54de36234834449e72d9dc891a90291aadcb1.tar.gz compcert-kvx-afe54de36234834449e72d9dc891a90291aadcb1.zip | |
fix problem if rt = rf
| -rw-r--r-- | riscV/Asmexpand.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 1f6597d1..14407bba 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -589,10 +589,13 @@ let expand_instruction instr = if not Archi.ptr64 then failwith "Pselectl not available on RV32, only on RV64" else - if not (ireg0_eq rt rf) - then - if (ireg0_eq (X rd) rt) - then + if ireg0_eq rt rf then + begin + if not (ireg0_eq (X rd) rt) then + emit (Paddil(rd, rt, Int64.zero)) + end + else + if (ireg0_eq (X rd) rt) then begin emit (Psubl(X31, X0, rb)); emit (Pandl(X31, X X31, rt)); @@ -601,8 +604,7 @@ let expand_instruction instr = emit (Porl(rd, X rd, X X31)) end else - if (ireg0_eq (X rd) rf) - then + if (ireg0_eq (X rd) rf) then begin emit (Paddil(X31, rb, Int64.mone)); emit (Pandl(X31, X X31, rf)); |