From c8cd3d017890a250f32463b6dca6571d181a3c22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:35:04 +0200 Subject: selection of builtin.. progress... --- backend/Selection.v | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index e63cbce3..a87578ba 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -267,20 +267,21 @@ Definition sel_switch_long := (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. +Definition sel_builtin_default optid ef args := + OK (Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef))). + Definition sel_builtin optid ef args := match ef with | EF_builtin name sign => (if String.string_dec name "__builtin_ternary_uint" - then Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)) - else Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef))) - | _ => - Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)) + then (match optid with + | None => OK Sskip + | Some id => Error (msg "Selection: ternary uint") + end) + else sel_builtin_default optid ef args) + | _ => sel_builtin_default optid ef args end. (** Conversion from Cminor statements to Cminorsel statements. *) @@ -291,9 +292,9 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - 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) + (match classify_call fn with + | Call_default => OK (Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)) + | Call_imm id => OK (Scall optid sg (inr _ id) (sel_exprlist args)) | Call_builtin ef => sel_builtin optid ef args end) | Cminor.Sbuiltin optid ef args => -- cgit