diff options
Diffstat (limited to 'backend/Selection.v')
-rw-r--r-- | backend/Selection.v | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 11125856..ae9da0a7 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -203,6 +203,23 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := end end. +(** Annotations *) + +Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool := + match ef, optid with + | EF_annot _ _, None => true + | _, _ => false + end. + +Function sel_annot_arg (e: Cminor.expr) : AST.annot_arg expr := + match e with + | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => AA_addrglobal id ofs + | Cminor.Econst (Cminor.Oaddrstack ofs) => AA_addrstack ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrsymbol id ofs)) => AA_loadglobal chunk id ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrstack ofs)) => AA_loadstack chunk ofs + | _ => annot_arg (sel_expr e) + end. + (** Conversion of Cminor [switch] statements to decision trees. *) Parameter compile_switch: Z -> nat -> table -> comptree. @@ -263,7 +280,9 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args) end) | Cminor.Sbuiltin optid ef args => - OK (Sbuiltin optid ef (sel_exprlist args)) + OK (if builtin_is_annot ef optid + then Sannot ef (List.map sel_annot_arg args) + else Sbuiltin optid ef (sel_exprlist args)) | Cminor.Stailcall sg fn args => OK (match classify_call ge fn with | Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args) |