diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 20:19:24 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 20:19:24 +0200 |
| commit | 2dca62f38463b0ebce24fff50666c846df50488e (patch) | |
| tree | 356c1eeb4d084002efd5ea28fdd83ecdf7ed960b /backend/Selection.v | |
| parent | 616f939e3ac7ff052f0eb7bce8c16873730ddf0e (diff) | |
| download | compcert-kvx-2dca62f38463b0ebce24fff50666c846df50488e.tar.gz compcert-kvx-2dca62f38463b0ebce24fff50666c846df50488e.zip | |
attempts at generating builtins, start
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 05a06abf..27c5bd10 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -267,6 +267,11 @@ Definition sel_switch_long := (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. +Definition sel_builtin optid ef args := + Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)). + (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := @@ -278,9 +283,7 @@ 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 |