blob: 1ebb51f58beb6093c53e7d85e582afe2d2e1d34c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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)
|
