aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmexpand.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-02-02 10:21:17 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-02-02 10:21:17 +0100
commitd2159e300b2d5e017a3144c747d34949b2ff2769 (patch)
tree2186636bc3f2e85b5effd19f9e7c23f4183545aa /riscV/Asmexpand.ml
parente0f1a90c2dcf7c43137064470ce4b12368b8435d (diff)
downloadcompcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.tar.gz
compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.zip
begin implementing select
Diffstat (limited to 'riscV/Asmexpand.ml')
-rw-r--r--riscV/Asmexpand.ml15
1 files changed, 14 insertions, 1 deletions
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 810514a3..9dd8cac9 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -582,9 +582,22 @@ let expand_builtin_inline name args res =
raise (Error ("unrecognized builtin " ^ name))
(* Expansion of instructions *)
-
+
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
| Pallocframe (sz, ofs) ->
let sg = get_current_function_sig() in
emit (Pmv (X30, X2));