aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Selection.v')
-rw-r--r--backend/Selection.v34
1 files changed, 29 insertions, 5 deletions
diff --git a/backend/Selection.v b/backend/Selection.v
index 4520cb0c..499c26a1 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -43,6 +43,12 @@ Function condexpr_of_expr (e: expr) : condexpr :=
| _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil)
end.
+Function condition_of_expr (e: expr) : condition * exprlist :=
+ match e with
+ | Eop (Ocmp c) el => (c, el)
+ | _ => (Ccompuimm Cne Int.zero, e ::: Enil)
+ end.
+
(** Conversion of loads and stores *)
Definition load (chunk: memory_chunk) (e1: expr) :=
@@ -156,6 +162,13 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
| Cminor.Ocmplu c => cmplu c arg1 arg2
end.
+Definition sel_select (ty: typ) (arg1 arg2 arg3: expr) : expr :=
+ let (cond, args) := condition_of_expr arg1 in
+ match select ty cond args arg2 arg3 with
+ | Some e => e
+ | None => Econdition (condexpr_of_expr arg1) arg2 arg3
+ end.
+
(** Conversion from Cminor expression to Cminorsel expressions *)
Fixpoint sel_expr (a: Cminor.expr) : expr :=
@@ -221,6 +234,20 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident :=
| Some id => BR id
end.
+Definition sel_builtin_default (optid: option ident) (ef: external_function)
+ (args: list Cminor.expr) :=
+ Sbuiltin (sel_builtin_res optid) ef
+ (sel_builtin_args args (Machregs.builtin_constraints ef)).
+
+Function sel_builtin (optid: option ident) (ef: external_function)
+ (args: list Cminor.expr) :=
+ match ef, optid, args with
+ | EF_select ty, Some id, e1 :: e2 :: e3 :: nil =>
+ Sassign id (sel_select ty (sel_expr e1) (sel_expr e2) (sel_expr e3))
+ | _, _, _ =>
+ sel_builtin_default optid ef args
+ end.
+
(** Conversion of Cminor [switch] statements to decision trees. *)
Parameter compile_switch: Z -> nat -> table -> comptree.
@@ -278,13 +305,10 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt :=
OK (match classify_call fn with
| Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)
| Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args)
- | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef
- (sel_builtin_args args
- (Machregs.builtin_constraints ef))
+ | Call_builtin ef => sel_builtin optid ef args
end)
| Cminor.Sbuiltin optid ef args =>
- OK (Sbuiltin (sel_builtin_res optid) ef
- (sel_builtin_args args (Machregs.builtin_constraints ef)))
+ OK (sel_builtin optid ef args)
| Cminor.Stailcall sg fn args =>
OK (match classify_call fn with
| Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args)