diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 13:43:44 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 13:43:44 +0100 |
commit | 3a3e6f61db092f0f81849af6970c771c70df8bce (patch) | |
tree | 976ffb68b5fdfd64d2a9366ec7f9fd37848cfad7 | |
parent | a47d709fd9251f58032444fde27a3ad7e947c26d (diff) | |
download | compcert-kvx-3a3e6f61db092f0f81849af6970c771c70df8bce.tar.gz compcert-kvx-3a3e6f61db092f0f81849af6970c771c70df8bce.zip |
some more cases implemented
-rw-r--r-- | riscV/Asmexpand.ml | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 9dd8cac9..f23db36e 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -586,18 +586,31 @@ let expand_builtin_inline name args res = let expand_instruction instr = match instr with | Pselectl(rd, rb, rt, rf) -> - if not (ireg0_eq rt rf) - then - if (ireg0_eq (X rd) rt) || (ireg0_eq (X rd) rf) - then failwith "Pselectl" - else - begin - emit (Psubl(X31, X0, rb)); - emit (Paddil(rd, rb, Int64.mone)); - emit (Pandl(X31, X X31, rt)); - emit (Pandl(rd, X rd, rf)); - emit (Porl(rd, X rd, X X31)) - end + 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 failwith "Pselectl rd=rt" + else + if (ireg0_eq (X rd) rf) + then + begin + emit (Paddil(X31, rb, Int64.mone)); + emit (Pandl(X31, X X31, rf)); + emit (Psubl(rd, X0, rb)); + emit (Pandl(rd, X rd, rt)); + emit (Porl(rd, X rd, X X31)) + end + else + begin + emit (Psubl(X31, X0, rb)); + emit (Paddil(rd, rb, Int64.mone)); + emit (Pandl(X31, X X31, rt)); + emit (Pandl(rd, X rd, rf)); + emit (Porl(rd, X rd, X X31)) + end | Pallocframe (sz, ofs) -> let sg = get_current_function_sig() in emit (Pmv (X30, X2)); |