2 * Copyright 2012, INRIA
3 * Julia Lawall, Gilles Muller
4 * Copyright 2010-2011, INRIA, University of Copenhagen
5 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
6 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
7 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
8 * This file is part of Coccinelle.
10 * Coccinelle is free software: you can redistribute it and/or modify
11 * it under the terms of the GNU General Public License as published by
12 * the Free Software Foundation, according to version 2 of the License.
14 * Coccinelle is distributed in the hope that it will be useful,
15 * but WITHOUT ANY WARRANTY; without even the implied warranty of
16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17 * GNU General Public License for more details.
19 * You should have received a copy of the GNU General Public License
20 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
22 * The authors reserve the right to distribute this or future versions of
23 * Coccinelle under other licenses.
27 #
0 "./externalanalysis.ml"
28 (* Support code for the integration of results
29 * from external analysis tools.
31 * the file should contain a result per line, where each line
33 * filename;begin_row;begin_column;end_row;end_column;data
35 * E;n;int_1;...;int_n (an integer set)
36 * I;bnd;bnd (integer bounds, either integer or empty)
39 * Note: for the moment the analysis results are assumed to be
40 * integer ranges or sets. Other types of analysis results will
41 * be regarded as a plain string.
43 * Todo: implement a proper querying facility that keeps different
44 * types of analysis apart.
48 (* provides a search structure for providing a map from posl to
49 * some value, and search operations that find the nearest posl.
50 * This is mainly a hack for backwards compatibility with older
51 * ocaml versions that provide only limited functionality on
54 module PoslMap
= struct
57 let compare = Ast_c.compare_posl
60 module PMap
= Map.Make
(PComp
)
61 module PSet
= Set.Make
(PComp
)
63 type 'a t
= (PSet.t
* 'a
PMap.t
)
65 let empty = (PSet.empty, PMap.empty)
66 let mem x
(s
, _
) = PSet.mem x s
67 let find k
(_
, m
) = PMap.find k m
68 let add k v
(s
, m
) = (PSet.add k s
, PMap.add k v m
)
70 (* throws Not_found if such a key does not exist *)
71 let nearest_key find_smaller k s
=
72 match PSet.split k s
with
74 | (smaller
, false, greater
) ->
75 match find_smaller
with
76 true -> PSet.max_elt smaller
77 | false -> PSet.min_elt greater
79 (* throws Not_found if such an entry does not exist *)
80 let find_nearest find_smaller
(s
, m
) k
=
81 PMap.find (nearest_key find_smaller k s
) m
84 module StringMap
= Map.Make
(String
)
86 module Int64Set
= Set.Make
(Int64
)
88 (* bound: either concrete or unbounded *)
89 type bound
= int64
option
91 (* The type of analysis results, which for the moment focusses on integers.
92 * The lower bound should be smaller or equal to the upper bound (not enforced)
96 | IntBounds
of bound
* bound
103 | Some i
-> Printf.sprintf
"%Ld" i
105 let show_result result
=
106 let out = Buffer.create
120 in
107 begin match result
with
109 Buffer.add_string
out "{";
110 Int64Set.iter
(fun i
->
111 Buffer.add_string
out (Printf.sprintf
"%Ld;" i
)) s
;
112 Buffer.add_string
out "}"
113 | IntBounds
(l
, u
) ->
114 Buffer.add_string
out (show_bound l
);
115 Buffer.add_string
out "-";
116 Buffer.add_string
out (show_bound u
)
118 Buffer.add_string
out s
122 (* search structure for results *)
123 type result_map
= (((result list
) PoslMap.t
) PoslMap.t
) StringMap.t
125 let empty_map : result_map
= StringMap.empty
127 (* this module is organized that it contains the analysis results as a singleton. *)
128 let current_map = ref empty_map
130 (* regular expressions for extracting results from the .csv file *)
131 let loc_regexp = Str.regexp
"\\([^;]*\\);\\([0-9]+\\);\\([0-9]+\\);\\([0-9]+\\);\\([0-9]+\\);\\(.+\\)"
132 let intset_regexp = Str.regexp
"E;\\([0-9]+\\)\\(\\(;[0-9]+\\)*\\)"
133 let intbounds_regexp = Str.regexp
"I;\\([0-9]*\\);\\([0-9]*\\)"
134 let split_regexp = Str.regexp
"[;]"
136 (* Loading of results from a .cvs-like format.
137 * Skips over unparsable entries without reporting an error.
139 let load_external_results filename
=
140 let chan = open_in filename
in
142 let line = input_line
chan in
143 match Str.string_match
loc_regexp line 0 with
146 let s_file = Str.matched_group
1 line in
147 let s_lbegin = Str.matched_group
2 line in
148 let s_cbegin = Str.matched_group
3 line in
149 let s_lend = Str.matched_group
4 line in
150 let s_cend = Str.matched_group
5 line in
151 let s_data = Str.matched_group
6 line in
152 let mk_posl s_row s_col
=
153 (int_of_string s_row
, int_of_string s_col
) in
154 let posl_begin = mk_posl s_lbegin s_cbegin in
155 let posl_end = mk_posl s_lend s_cend in
157 (* map the line to a value *)
159 match Str.string_match
intset_regexp s_data 0 with
161 let n_fields = int_of_string
(Str.matched_group
1 s_data) in
162 let s_fields = Str.matched_group
2 s_data in
163 let strs = Str.bounded_split
split_regexp s_fields n_fields in
164 let ints = List.map
Int64.of_string
strs in
165 let set = List.fold_right
Int64Set.add ints Int64Set.empty in
168 match Str.string_match
intbounds_regexp s_data 0 with
169 true -> let mk_bound s
=
170 match String.length s
== 0 with
172 | false -> Some
(Int64.of_string s
) in
173 IntBounds
(mk_bound (Str.matched_group
1 s_data),
174 mk_bound (Str.matched_group
2 s_data))
175 | false -> Other
s_data in
177 (* add the new value to the current map *)
178 let ensure_str m k f
=
179 let v = match StringMap.mem k m
with
180 true -> f
(StringMap.find k m
)
181 | false -> f
PoslMap.empty in
182 StringMap.add k
v m
in
183 let ensure_posl k e f m
=
184 let v = match PoslMap.mem k m
with
185 true -> f
(PoslMap.find k m
)
189 current_map := ensure_str !current_map s_file
190 (ensure_posl posl_begin PoslMap.empty
191 (ensure_posl posl_end [] (fun xs
-> value :: xs
)))
192 done with End_of_file
-> ();
197 (* finds all nearest results in the map that enclose the given position *)
198 let find_results filename p_begin p_end
=
200 let m_begin = StringMap.find filename
!current_map in
201 let m_end = PoslMap.find_nearest true m_begin p_begin
in
202 let results = PoslMap.find_nearest false m_end p_end
in
208 * some convenience functions on analysis results.
211 let within_bounds c l u
=
214 | (None
, Some k
) -> c
<= k
215 | (Some k
, None
) -> k
<= c
216 | (Some k
, Some n
) -> k
<= c
&& c
<= n
218 let contains_bounds m n l u
=
222 | (Some k
, Some i
) -> k
<= i
227 | (Some q
, Some j
) -> j
<= q
231 (* given two result values, computes their intersection. An empty intersection
232 is indicated with a None result value.
234 let intersect_results r1 r2
=
236 match Int64Set.inter s1 s2
with
237 s
when Int64Set.is_empty s
-> None
238 | s
-> Some
(IntSet s
) in
239 let bounds_set r l u s
=
240 if Int64Set.for_all
(fun c
-> within_bounds c l u
) s
243 let bounds r m n l u
=
244 if contains_bounds m n l u
250 IntSet s2
-> sets s1 s2
251 | IntBounds
(l
, u
) -> bounds_set r2 l u s1
254 | IntBounds
(l
, u
) -> begin
256 IntSet s2
-> bounds_set r1 l u s2
257 | IntBounds
(m
, n
) -> bounds r1 l u m n
262 (* a predicate over the analysis results *)
263 let satisfy f filename p_begin p_end
=
264 try f
(find_results filename p_begin p_end
)
265 with Not_found
-> false
267 (* satisfy, but with the intersection of all analysis results. *)
272 | Some s
-> intersect_results r s
in
278 match List.fold_left
inter (Some x
) xs
with
283 let has_any_result = satisfy (fun rs
-> List.length rs
> 0)
285 let for_all p
= satisfy (List.for_all p
)
287 let for_all1 p
= satisfy
288 (fun rs
-> List.length rs
> 0 && List.for_all p rs
)
290 let exists p
= satisfy (List.exists p
)
294 | IntSet s
when Int64Set.is_empty s
-> true (* unreachable memory, thus any propery holds *)
295 | IntSet s
-> Int64Set.equal
(Int64Set.singleton c
) s
296 | IntBounds
(Some l
, Some u
) -> l
== c
&& u
== c
299 let contains_int c r
=
301 IntSet s
-> Int64Set.mem c s
302 | IntBounds
(l
, u
) -> within_bounds c l u
305 let has_only_nul = for_all1 (single_int Int64.zero
)
306 let has_also_nul = exists (contains_int Int64.zero
)
307 let has_also_int c
= exists (contains_int c
)