Commit | Line | Data |
---|---|---|
755320b0 C |
1 | (* |
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. | |
9 | * | |
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. | |
13 | * | |
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. | |
18 | * | |
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/>. | |
21 | * | |
22 | * The authors reserve the right to distribute this or future versions of | |
23 | * Coccinelle under other licenses. | |
24 | *) | |
25 | ||
26 | ||
27 | # 0 "./externalanalysis.ml" | |
28 | (* Support code for the integration of results | |
29 | * from external analysis tools. | |
30 | * | |
31 | * the file should contain a result per line, where each line | |
32 | * is of the form: | |
33 | * filename;begin_row;begin_column;end_row;end_column;data | |
34 | * where data can be: | |
35 | * E;n;int_1;...;int_n (an integer set) | |
36 | * I;bnd;bnd (integer bounds, either integer or empty) | |
37 | * other | |
38 | * | |
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. | |
42 | * | |
43 | * Todo: implement a proper querying facility that keeps different | |
44 | * types of analysis apart. | |
45 | *) | |
46 | ||
47 | ||
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 | |
52 | * Maps. | |
53 | *) | |
54 | module PoslMap = struct | |
55 | module PComp = struct | |
56 | type t = Ast_c.posl | |
57 | let compare = Ast_c.compare_posl | |
58 | end | |
59 | ||
60 | module PMap = Map.Make (PComp) | |
61 | module PSet = Set.Make (PComp) | |
62 | ||
63 | type 'a t = (PSet.t * 'a PMap.t) | |
64 | ||
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) | |
69 | ||
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 | |
73 | (_, true, _) -> k | |
74 | | (smaller, false, greater) -> | |
75 | match find_smaller with | |
76 | true -> PSet.max_elt smaller | |
77 | | false -> PSet.min_elt greater | |
78 | ||
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 | |
82 | end | |
83 | ||
84 | module StringMap = Map.Make (String) | |
85 | ||
86 | module Int64Set = Set.Make (Int64) | |
87 | ||
88 | (* bound: either concrete or unbounded *) | |
89 | type bound = int64 option | |
90 | ||
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) | |
93 | *) | |
94 | type result = | |
95 | IntSet of Int64Set.t | |
96 | | IntBounds of bound * bound | |
97 | | Other of string | |
98 | ||
99 | (* for printing *) | |
100 | let show_bound b = | |
101 | match b with | |
102 | None -> "*" | |
103 | | Some i -> Printf.sprintf "%Ld" i | |
104 | ||
105 | let show_result result = | |
106 | let out = Buffer.create 120 in | |
107 | begin match result with | |
108 | IntSet s -> | |
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) | |
117 | | Other s -> | |
118 | Buffer.add_string out s | |
119 | end; | |
120 | Buffer.contents out | |
121 | ||
122 | (* search structure for results *) | |
123 | type result_map = (((result list) PoslMap.t) PoslMap.t) StringMap.t | |
124 | ||
125 | let empty_map : result_map = StringMap.empty | |
126 | ||
127 | (* this module is organized that it contains the analysis results as a singleton. *) | |
128 | let current_map = ref empty_map | |
129 | ||
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 "[;]" | |
135 | ||
136 | (* Loading of results from a .cvs-like format. | |
137 | * Skips over unparsable entries without reporting an error. | |
138 | *) | |
139 | let load_external_results filename = | |
140 | let chan = open_in filename in | |
141 | try while true do | |
142 | let line = input_line chan in | |
143 | match Str.string_match loc_regexp line 0 with | |
144 | false -> () | |
145 | | true -> | |
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 | |
156 | ||
157 | (* map the line to a value *) | |
158 | let value = | |
159 | match Str.string_match intset_regexp s_data 0 with | |
160 | true -> | |
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 | |
166 | IntSet set | |
167 | | false -> | |
168 | match Str.string_match intbounds_regexp s_data 0 with | |
169 | true -> let mk_bound s = | |
170 | match String.length s == 0 with | |
171 | true -> None | |
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 | |
176 | ||
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) | |
186 | | false -> f e in | |
187 | PoslMap.add k v m in | |
188 | ||
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 -> (); | |
193 | close_in chan | |
194 | ||
195 | ||
196 | ||
197 | (* finds all nearest results in the map that enclose the given position *) | |
198 | let find_results filename p_begin p_end = | |
199 | try | |
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 | |
203 | results | |
204 | with Not_found -> [] | |
205 | ||
206 | ||
207 | (* | |
208 | * some convenience functions on analysis results. | |
209 | *) | |
210 | ||
211 | let within_bounds c l u = | |
212 | match (l, u) with | |
213 | (None, None) -> true | |
214 | | (None, Some k) -> c <= k | |
215 | | (Some k, None) -> k <= c | |
216 | | (Some k, Some n) -> k <= c && c <= n | |
217 | ||
218 | let contains_bounds m n l u = | |
1b9ae606 C |
219 | begin |
220 | match (l, m) with | |
221 | (None, None) -> true | |
222 | | (Some k, Some i) -> k <= i | |
223 | | _ -> false | |
224 | end && begin | |
225 | match (u, n) with | |
226 | (None, None) -> true | |
227 | | (Some q, Some j) -> j <= q | |
228 | | _ -> false | |
229 | end | |
755320b0 C |
230 | |
231 | (* given two result values, computes their intersection. An empty intersection | |
232 | is indicated with a None result value. | |
233 | *) | |
234 | let intersect_results r1 r2 = | |
235 | let sets s1 s2 = | |
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 | |
241 | then Some r | |
242 | else None in | |
243 | let bounds r m n l u = | |
244 | if contains_bounds m n l u | |
245 | then Some r | |
246 | else None in | |
247 | match r1 with | |
248 | IntSet s1 -> begin | |
249 | match r2 with | |
250 | IntSet s2 -> sets s1 s2 | |
251 | | IntBounds (l, u) -> bounds_set r2 l u s1 | |
252 | | Other _ -> None | |
253 | end | |
254 | | IntBounds (l, u) -> begin | |
255 | match r2 with | |
256 | IntSet s2 -> bounds_set r1 l u s2 | |
257 | | IntBounds (m, n) -> bounds r1 l u m n | |
258 | | Other _ -> None | |
259 | end | |
260 | | Other _ -> None | |
261 | ||
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 | |
266 | ||
267 | (* satisfy, but with the intersection of all analysis results. *) | |
268 | let satisfy1 f = | |
269 | let inter mbR r = | |
270 | match mbR with | |
271 | None -> None | |
272 | | Some s -> intersect_results r s in | |
273 | satisfy | |
274 | begin fun ls -> | |
275 | match ls with | |
276 | [] -> false | |
277 | | (x :: xs) -> | |
278 | match List.fold_left inter (Some x) xs with | |
279 | None -> false | |
280 | | Some r -> f r | |
281 | end | |
282 | ||
283 | let has_any_result = satisfy (fun rs -> List.length rs > 0) | |
284 | ||
285 | let for_all p = satisfy (List.for_all p) | |
286 | ||
287 | let for_all1 p = satisfy | |
288 | (fun rs -> List.length rs > 0 && List.for_all p rs) | |
289 | ||
290 | let exists p = satisfy (List.exists p) | |
291 | ||
292 | let single_int c r = | |
293 | match r with | |
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 | |
297 | | _ -> false | |
298 | ||
299 | let contains_int c r = | |
300 | match r with | |
301 | IntSet s -> Int64Set.mem c s | |
302 | | IntBounds (l, u) -> within_bounds c l u | |
303 | | _ -> false | |
304 | ||
305 | let has_only_nul = for_all1 (single_int Int64.zero) | |
306 | let has_also_nul = exists (contains_int Int64.zero) | |
1b9ae606 | 307 | let has_also_int c = exists (contains_int c) |