diff options
Diffstat (limited to 'backend/RTLgen.v')
-rw-r--r-- | backend/RTLgen.v | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 26f51e3f..b1c36513 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -455,6 +455,39 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) transl_expr map b r nc end. +(** Translation of arguments to annotations. *) + +Definition exprlist_of_expr_list (l: list expr) : exprlist := + List.fold_right Econs Enil l. + +Fixpoint convert_annot_arg {A: Type} (a: annot_arg expr) (rl: list A) : annot_arg A * list A := + match a with + | AA_base a => + match rl with + | r :: rs => (AA_base r, rs) + | nil => (AA_int Int.zero, nil) (**r never happens *) + end + | AA_int n => (AA_int n, rl) + | AA_long n => (AA_long n, rl) + | AA_float n => (AA_float n, rl) + | AA_single n => (AA_single n, rl) + | AA_loadstack chunk ofs => (AA_loadstack chunk ofs, rl) + | AA_addrstack ofs => (AA_addrstack ofs, rl) + | AA_loadglobal chunk id ofs => (AA_loadglobal chunk id ofs, rl) + | AA_addrglobal id ofs => (AA_addrglobal id ofs, rl) + | AA_longofwords hi lo => + let (hi', rl1) := convert_annot_arg hi rl in + let (lo', rl2) := convert_annot_arg lo rl1 in + (AA_longofwords hi' lo', rl2) + end. + +Fixpoint convert_annot_args {A: Type} (al: list (annot_arg expr)) (rl: list A) : list (annot_arg A) := + match al with + | nil => nil + | a1 :: al => + let (a1', rl1) := convert_annot_arg a1 rl in a1' :: convert_annot_args al rl1 + end. + (** Auxiliary for translating exit expressions. *) Definition transl_exit (nexits: list node) (n: nat) : mon node := @@ -558,6 +591,11 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do r <- alloc_optreg map optid; do n1 <- add_instr (Ibuiltin ef rargs r nd); transl_exprlist map al rargs n1 + | Sannot ef args => + let al := exprlist_of_expr_list (params_of_annot_args args) in + do rargs <- alloc_regs map al; + do n1 <- add_instr (Iannot ef (convert_annot_args args rargs) nd); + transl_exprlist map al rargs n1 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret |