diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 10:21:17 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 10:21:17 +0100 |
commit | d2159e300b2d5e017a3144c747d34949b2ff2769 (patch) | |
tree | 2186636bc3f2e85b5effd19f9e7c23f4183545aa /riscV/Asmexpand.ml | |
parent | e0f1a90c2dcf7c43137064470ce4b12368b8435d (diff) | |
download | compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.tar.gz compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.zip |
begin implementing select
Diffstat (limited to 'riscV/Asmexpand.ml')
-rw-r--r-- | riscV/Asmexpand.ml | 15 |
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)); |