blob: f4dab4c9164cc2a48e2e0cf59075eba44eb61266 (
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
open AST
open Camlcoq
open Diagnostics
open Memdata
open Printf
type t =
| Label of int
| String of string
| Symbol of ident
let offset ofs =
let ofs = camlint_of_coqint ofs in
if ofs = 0l then "" else sprintf " + %ld" ofs
let size_chunk c =
sprintf "%ld" (camlint_of_coqint (size_chunk c))
let addr_global id ofs =
let addr_o = "("
and addr_e = sprintf "%s)" (offset ofs) in
[String addr_o;Symbol id;String addr_e]
exception Bad_parameter of string
exception Unknown_parameter of string
exception Unknown_type of char
let ais_expr_arg lval preg_string sp_reg_name arg =
let preg reg = sprintf "reg(\"%s\")" (preg_string reg)
and sp = sprintf "reg(\"%s\")" sp_reg_name
and simple s = [String s]
and lval ty =
if lval then
let msg = sprintf "expected register or memory cell but found %s" ty in
raise (Bad_parameter msg)
in
let rec ais_arg = function
| BA x -> simple (preg x)
| BA_int n -> lval "constant"; simple (sprintf "%ld" (camlint_of_coqint n))
| BA_long n ->lval "constant"; simple (sprintf "%Ld" (camlint64_of_coqint n))
| BA_float _
| BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
| BA_loadstack(chunk, ofs) ->
let loadstack = sprintf "mem(%s%s, %s)" sp
(offset ofs)
(size_chunk chunk) in
simple loadstack
| BA_addrstack ofs ->
lval "stack cell";
let addrstack = sprintf "(%s%s)" sp (offset ofs) in
simple addrstack
| BA_loadglobal(chunk, id, ofs) ->
let mem_o = "mem("
and mem_e = sprintf "%s, %s)"
(offset ofs)
(size_chunk chunk) in
[String mem_o;Symbol id;String mem_e]
| BA_addrglobal(id, ofs) ->
lval "global address";
addr_global id ofs
| BA_splitlong(hi, lo) ->
combine " * 0x100000000 + " hi lo
| BA_addptr(a1, a2) ->
combine " + " a1 a2
and combine mid arg1 arg2 =
lval "pointer computation";
let op_br = simple "("
and mid = simple mid
and cl_br = simple ")"
and arg1 = ais_arg arg1
and arg2 = ais_arg arg2 in
op_br@arg1@mid@arg2@cl_br in
ais_arg arg
let ais_annot_list: (t list) list ref = ref []
let get_ais_annots () =
let annots = !ais_annot_list in
ais_annot_list := [];
List.rev annots
let re_loc_param = Str.regexp "# file:\\([^ ]+\\) line:\\([^ ]+\\)"
let loc_of_txt txt =
try
let pos = String.index txt '\n' in
let txt = String.sub txt 0 (pos -1) in
if Str.string_partial_match re_loc_param txt 0 then
let file = Str.matched_group 1 txt
and line = int_of_string (Str.matched_group 2 txt) in
file,line
else
no_loc
with _ ->
no_loc
let re_ais_annot_param = Str.regexp "%%\\|%[aelp][1-9][0-9]*\\|%here\\|\007"
let add_ais_annot lbl preg_string sp_reg_name txt args =
let fragment = function
| Str.Delim "%here" ->
[Label lbl]
| Str.Text s ->
[String s]
| Str.Delim "%%" ->
[String "%"]
| Str.Delim "\007" ->
[String "\007\000"]
| Str.Delim s ->
let typ = String.get s 1
and n = int_of_string (String.sub s 2 (String.length s - 2)) in
let arg = try
List.nth args (n-1)
with _ ->
raise (Unknown_parameter s) in
begin match typ with
| 'e' -> ais_expr_arg false preg_string sp_reg_name arg
| 'l' -> ais_expr_arg true preg_string sp_reg_name arg
| _ -> raise (Unknown_type typ)
end
in
let loc = loc_of_txt txt in
let warn t s =
warning loc Wrong_ais_parameter "%s %s" t s; []
in
let annot =
try
List.concat (List.map fragment (Str.full_split re_ais_annot_param txt))
with
| Bad_parameter s ->
warn "wrong ais parameter" s
| Unknown_parameter s ->
warn "unknown parameter" s
| Unknown_type c ->
warn "unknown format argument" (String.make 1 c)
in
let rec merge acc = function
| [] -> List.rev acc
| (Label _ as lbl):: rest -> merge (lbl::acc) rest
| (Symbol _ as sym) :: rest -> merge (sym::acc) rest
| String s1 :: String s2 :: rest ->
merge acc (String (s1 ^ s2) :: rest)
| String s:: rest -> merge ((String s)::acc) rest
in
let annot = merge [] annot in
if annot <> [] then
ais_annot_list := (annot)::!ais_annot_list
|
