From 4622f49fd089ae47d0c853343cb0a05f986c962a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 27 Mar 2015 08:55:05 +0100 Subject: Extend annotations so that they can keep track of global variables and local variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet. --- backend/Selection.v | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index 11125856..5cec6e00 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -203,6 +203,12 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := end end. +Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool := + match ef, optid with + | EF_annot _ _, None => true + | _, _ => false + end. + (** Conversion of Cminor [switch] statements to decision trees. *) Parameter compile_switch: Z -> nat -> table -> comptree. @@ -263,7 +269,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 (fun e => annot_arg (sel_expr e)) 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) -- cgit