diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 15:44:38 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 15:44:38 +0100 |
commit | 225e51bcf9bfe4029e0d9ca5617ad288326e68c9 (patch) | |
tree | 73ac6c5821ddf4a74f74d23e379c593bc43fd217 | |
parent | efe858437dae74e6de2b52e7676ae9f976a22941 (diff) | |
download | compcert-kvx-225e51bcf9bfe4029e0d9ca5617ad288326e68c9.tar.gz compcert-kvx-225e51bcf9bfe4029e0d9ca5617ad288326e68c9.zip |
implement for another register configuration
-rw-r--r-- | riscV/Asmexpand.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index f23db36e..1f6597d1 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -592,7 +592,14 @@ let expand_instruction instr = if not (ireg0_eq rt rf) then if (ireg0_eq (X rd) rt) - then failwith "Pselectl rd=rt" + then + begin + emit (Psubl(X31, X0, rb)); + emit (Pandl(X31, X X31, rt)); + emit (Paddil(rd, rb, Int64.mone)); + emit (Pandl(rd, X rd, rf)); + emit (Porl(rd, X rd, X X31)) + end else if (ireg0_eq (X rd) rf) then |