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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
(* is distributed under the terms of the INRIA Non-Commercial *)
(* License Agreement. *)
(* *)
(* *********************************************************************)
open Asm
open Asmexpandaux
open AST
open Camlcoq
(* open Integers *)
let _0 = Integers.Int.zero
(* Options controlling the output of the constants *)
let literals_in_code = ref true (* to be turned into a proper option *)
let vfpv3 = Configuration.model >= "armv7"
(* Record current code position and latest position at which to
emit float and symbol constants. *)
let currpos = ref 0
let size_constants = ref 0
let max_pos_constants = ref max_int
let distance_to_emit_constants () =
if !literals_in_code
then !max_pos_constants - (!currpos + !size_constants)
else max_int
(* Associate labels to floating-point constants and to symbols *)
let float_labels = (Hashtbl.create 39 : (Floats.float, label) Hashtbl.t)
let float32_labels = (Hashtbl.create 39 : (Floats.float32, label) Hashtbl.t)
let symbol_labels =
(Hashtbl.create 39 : (ident * Integers.Int.int, label) Hashtbl.t)
let get_label tbl sz pinc bf =
try
Hashtbl.find tbl bf
with Not_found ->
let lbl' = new_label () in
Hashtbl.add tbl bf lbl';
size_constants := !size_constants + sz;
max_pos_constants := min !max_pos_constants (!currpos + pinc);
lbl'
let label_float = get_label float_labels 8 1024
let label_float32 = get_label float32_labels 4 1024
let label_symbol id ofs = get_label symbol_labels 4 4096 (id,ofs)
let reset_constants () =
Hashtbl.clear float_labels;
Hashtbl.clear float32_labels;
Hashtbl.clear symbol_labels;
size_constants := 0;
max_pos_constants := max_int
(* Recognition of float constants appropriate for VMOV.
a normalized binary floating point encoding with 1 sign bit, 4
bits of fraction and a 3-bit exponent *)
let is_immediate_float64 bits =
let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
let is_immediate_float32 bits =
let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
let mant = Int32.logand bits 0x7F_FFFFl in
exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
let no_fallthrough = function
| Pb _ -> true
| Pbsymb _ -> true
| Pbreg _ -> true
| _ -> false
let estimate_size = function
| Pflid _
| Pflis _ -> 3
| Pfcmpd _
| Pfcmpzd _
| Pfsitod _
| Pfuitod _
| Pftosizd _
| Pftouizd _
| Pfcmps _
| Pfcmpzs _
| Pfsitos _
| Pfuitos _
| Pftosizs _
| Pftouizs _
| Pmovite _ -> 2
| Pbuiltin (ef,_,_) ->
begin match ef with
| EF_inline_asm _ -> 256
| EF_profiling _ -> 40
| _ -> 0 end
| Pcfi_adjust _
| Pcfi_rel_offset _
| Plabel _ -> 0
| Pbtbl (r,tbl) -> 2 + List.length tbl
| _ -> 1
let expand_constants () =
let consts = Hashtbl.fold (fun bf lbl c ->
Float64 (lbl, bf)::c)
float_labels [] in
let consts = Hashtbl.fold (fun bf lbl c ->
Float32 (lbl, bf)::c)
float32_labels consts in
let consts = Hashtbl.fold (fun (id,ofs) lbl c ->
Symbol (lbl,id,ofs)::c)
symbol_labels consts in
if consts <> [] then
emit (Pconstants consts);
reset_constants ()
let expand_instruction = function
| Pflid (r1,f) ->
let f' = camlint64_of_coqint(Floats.Float.to_bits f) in
if vfpv3 && is_immediate_float64 f' then begin
emit (Pflid_imm (r1,f));
1
end else if !literals_in_code then begin
let lbl = label_float f in
emit (Pflid_lbl (r1,lbl,f));
1
end else begin
emit (Pflid (r1,f));
3
end
| Pflis (r1,f) ->
let f' = camlint_of_coqint(Floats.Float32.to_bits f) in
if vfpv3 && is_immediate_float32 f' then begin
emit (Pflis_imm (r1,f));
1
end else if !literals_in_code then begin
let lbl = label_float32 f in
emit (Pflis_lbl (r1,lbl,f));
1
end else begin
let lo = coqint_of_camlint (Int32.logand f' 0xFFFFl)
and hi = coqint_of_camlint (Int32.shift_right_logical f' 16) in
emit (Pmovw (IR14,lo));
emit (Pmovt (IR14,hi));
emit (Pfcpy_fi (r1,IR14));
3
end
| Ploadsymbol(r1, id, ofs) ->
let o = camlint_of_coqint ofs in
if o >= -32768l && o <= 32767l && !Clflags.option_mthumb then begin
emit (Ploadsymbol_imm (r1,id,ofs));
2
end else begin
let lbl = label_symbol id ofs in
emit (Ploadsymbol_lbl (r1,lbl,id,ofs));
1
end
| inst ->
emit inst;
estimate_size inst
let rec expand_instructions no_fall = function
| [] -> ()
| i :: il ->
let estimate = estimate_size i * 4 in
let d = distance_to_emit_constants() - estimate in
if d < 256 && no_fall then
expand_constants ()
else if d < 16 then begin
let lbl = new_label () in
emit (Pb lbl);
expand_constants ();
emit (Plabel lbl)
end;
let n = expand_instruction i in
currpos := !currpos + n * 4;
expand_instructions (no_fallthrough i) il
let expand_constants fn =
reset_constants ();
set_current_function fn;
expand_instructions false fn.fn_code;
expand_constants ();
get_current_function ()
|
