diff options
Diffstat (limited to 'backend/Selection.v')
-rw-r--r-- | backend/Selection.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 5cec6e00..ae9da0a7 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -203,12 +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. @@ -270,7 +281,7 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := end) | Cminor.Sbuiltin optid ef args => OK (if builtin_is_annot ef optid - then Sannot ef (List.map (fun e => annot_arg (sel_expr e)) args) + 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 |