diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
commit | 202bc495442a1a8fa184b73ac0063bdbbbcdf846 (patch) | |
tree | 46c6920201b823bf47252bc52864b0bf60f3233e /backend/PrintAnnot.ml | |
parent | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (diff) | |
download | compcert-kvx-202bc495442a1a8fa184b73ac0063bdbbbcdf846.tar.gz compcert-kvx-202bc495442a1a8fa184b73ac0063bdbbbcdf846.zip |
Constant propagation within __builtin_annot.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/PrintAnnot.ml')
-rw-r--r-- | backend/PrintAnnot.ml | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml new file mode 100644 index 00000000..1ebb51f5 --- /dev/null +++ b/backend/PrintAnnot.ml @@ -0,0 +1,76 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Printing annotations in asm syntax *) + +open Printf +open Datatypes +open Integers +open Floats +open Camlcoq +open AST +open Memdata +open Asm + +let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" + +type arg_value = + | Reg of preg + | Stack of memory_chunk * Int.int + | Intconst of Int.int + | Floatconst of float + +let print_annot_text print_preg sp_reg_name oc txt args = + 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 + match List.nth args (n-1) with + | Reg r -> + print_preg oc r + | Stack(chunk, ofs) -> + fprintf oc "mem(%s + %ld, %ld)" + sp_reg_name + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | Intconst n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Floatconst n -> + fprintf oc "%.18g" (camlfloat_of_coqfloat n) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_annot_param txt); + fprintf oc "\n" + +let rec annot_args tmpl args = + match tmpl, args with + | [], _ -> [] + | AA_arg _ :: tmpl', APreg r :: args' -> + Reg r :: annot_args tmpl' args' + | AA_arg _ :: tmpl', APstack(chunk, ofs) :: args' -> + Stack(chunk, ofs) :: annot_args tmpl' args' + | AA_arg _ :: tmpl', [] -> [] (* should never happen *) + | AA_int n :: tmpl', _ -> + Intconst n :: annot_args tmpl' args + | AA_float n :: tmpl', _ -> + Floatconst n :: annot_args tmpl' args + +let print_annot_stmt print_preg sp_reg_name oc txt tmpl args = + print_annot_text print_preg sp_reg_name oc txt (annot_args tmpl args) + +let print_annot_val print_preg oc txt args = + print_annot_text print_preg "<internal error>" oc txt + (List.map (fun r -> Reg r) args) |