aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-02-02 15:44:38 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-02-02 15:44:38 +0100
commit225e51bcf9bfe4029e0d9ca5617ad288326e68c9 (patch)
tree73ac6c5821ddf4a74f74d23e379c593bc43fd217
parentefe858437dae74e6de2b52e7676ae9f976a22941 (diff)
downloadcompcert-kvx-225e51bcf9bfe4029e0d9ca5617ad288326e68c9.tar.gz
compcert-kvx-225e51bcf9bfe4029e0d9ca5617ad288326e68c9.zip
implement for another register configuration
-rw-r--r--riscV/Asmexpand.ml9
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