diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-01 08:36:03 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-01 08:36:03 +0000 |
commit | 99f47c7a99b11c9cc3429fc0e5d0e21ae3707518 (patch) | |
tree | f452a9d6f8ec4c4573a7ca55581a0060d315f510 /arm/PrintAsm.ml | |
parent | 1b8e228a2c5d8f63ffa28c1fcef68f64a0408900 (diff) | |
download | compcert-99f47c7a99b11c9cc3429fc0e5d0e21ae3707518.tar.gz compcert-99f47c7a99b11c9cc3429fc0e5d0e21ae3707518.zip |
Adding __builtin_annotation
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r-- | arm/PrintAsm.ml | 34 |
1 files changed, 33 insertions, 1 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index c2fc8a9e..9e1cae75 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -284,6 +284,35 @@ let print_builtin_function oc s = fprintf oc "%s end %s\n" comment (extern_atom s); n +let re_builtin_annotation = Str.regexp "__builtin_annotation_\"\\(.*\\)\"$" + +let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" + +let print_annotation oc txt args res = + fprintf oc "%s annotation: " comment; + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + preg oc (List.nth args (n-1)) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_annot_param txt); + fprintf oc "\n"; + begin match args, res with + | [], _ -> () + | IR src :: _, IR dst -> + if dst <> src then fprintf oc " mr %a, %a\n" ireg dst ireg src + | FR src :: _, FR dst -> + if dst <> src then fprintf oc " fmr %a, %a\n" freg dst freg src + | _, _ -> assert false + end; + 0 + (* Printing of instructions *) let shift_op oc = function @@ -482,7 +511,10 @@ let print_instruction oc labels = function tbl; 2 + List.length tbl | Pbuiltin(ef, args, res) -> - print_builtin_inlined oc (extern_atom ef.ef_id) args res + let name = extern_atom ef.ef_id in + if Str.string_match re_builtin_annotation name 0 + then print_annotation oc (Str.matched_group 1 name) args res + else print_builtin_inlined oc name args res let no_fallthrough = function | Pb _ -> true |