File: externalanalysis.ml

package info (click to toggle)
coccinelle 1.0.8.deb-5
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 26,148 kB
  • sloc: ml: 136,392; ansic: 23,594; sh: 2,189; makefile: 2,157; perl: 1,576; lisp: 840; python: 823; awk: 70; csh: 12
file content (286 lines) | stat: -rw-r--r-- 8,852 bytes parent folder | download
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
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
(*
 * This file is part of Coccinelle, licensed under the terms of the GPL v2.
 * See copyright.txt in the Coccinelle source code for more information.
 * The Coccinelle source code can be obtained at http://coccinelle.lip6.fr
 *)

(* Support code for the integration of results
 * from external analysis tools.
 *
 * the file should contain a result per line, where each line
 * is of the form:
 *   filename;begin_row;begin_column;end_row;end_column;data
 * where data can be:
 *   E;n;int_1;...;int_n      (an integer set)
 *   I;bnd;bnd     (integer bounds, either integer or empty)
 *   other
 *
 * Note: for the moment the analysis results are assumed to be
 * integer ranges or sets. Other types of analysis results will
 * be regarded as a plain string.
 *
 * Todo: implement a proper querying facility that keeps different
 * types of analysis apart.
 *)


(* provides a search structure for providing a map from posl to
 * some value, and search operations that find the nearest posl.
 * This is mainly a hack for backwards compatibility with older
 * ocaml versions that provide only limited functionality on
 * Maps.
 *)
module PoslMap = struct
  module PComp = struct
    type t      = Ast_c.posl
    let compare = Ast_c.compare_posl
  end

  module PMap = Map.Make (PComp)
  module PSet = Set.Make (PComp)

  type 'a t = (PSet.t * 'a PMap.t)

  let empty          = (PSet.empty, PMap.empty)
  let mem x (s, _)   = PSet.mem x s
  let find k (_, m)  = PMap.find k m
  let add k v (s, m) = (PSet.add k s, PMap.add k v m)

  (* throws Not_found if such a key does not exist *)
  let nearest_key find_smaller k s =
    match PSet.split k s with
      (_, true, _) -> k
    | (smaller, false, greater) ->
      match find_smaller with
	true  -> PSet.max_elt smaller
      | false -> PSet.min_elt greater

  (* throws Not_found if such an entry does not exist *)
  let find_nearest find_smaller (s, m) k =
    PMap.find (nearest_key find_smaller k s) m
end

module StringMap = Map.Make (String)

module Int64Set = Set.Make (Int64)

(* bound: either concrete or unbounded *)
type bound = int64 option

(* The type of analysis results, which for the moment focuses on integers.
 * The lower bound should be smaller or equal to the upper bound (not enforced)
 *)
type result =
    IntSet      of Int64Set.t
  | IntBounds   of bound * bound
  | Other       of string

(* for printing *)
let show_bound b =
  match b with
    None   -> "*"
  | Some i -> Printf.sprintf "%Ld" i

let show_result result =
  let out = Buffer.create 120 in
  begin match result with
    IntSet s ->
      Buffer.add_string out "{";
      Int64Set.iter (fun i ->
	Buffer.add_string out (Printf.sprintf "%Ld;" i)) s;
      Buffer.add_string out "}"
  | IntBounds (l, u) ->
      Buffer.add_string out (show_bound l);
      Buffer.add_string out "-";
      Buffer.add_string out (show_bound u)
  | Other s ->
      Buffer.add_string out s
  end;
  Buffer.contents out

(* search structure for results *)
type result_map = (((result list) PoslMap.t) PoslMap.t) StringMap.t

let empty_map : result_map = StringMap.empty

(* this module is organized that it contains the analysis results as a singleton. *)
let current_map = ref empty_map

(* regular expressions for extracting results from the .csv file *)
let loc_regexp       = Str.regexp "\\([^;]*\\);\\([0-9]+\\);\\([0-9]+\\);\\([0-9]+\\);\\([0-9]+\\);\\(.+\\)"
let intset_regexp    = Str.regexp "E;\\([0-9]+\\)\\(\\(;[0-9]+\\)*\\)"
let intbounds_regexp = Str.regexp "I;\\([0-9]*\\);\\([0-9]*\\)"
let split_regexp     = Str.regexp "[;]"

(* Loading of results from a .cvs-like format.
 * Skips over unparsable entries without reporting an error.
 *)
let load_external_results filename =
  let chan = open_in filename in
  try while true do
    let line = input_line chan in
    match Str.string_match loc_regexp line 0 with
      false -> ()
    | true  ->
	let s_file   = Str.matched_group 1 line in
	let s_lbegin = Str.matched_group 2 line in
	let s_cbegin = Str.matched_group 3 line in
	let s_lend   = Str.matched_group 4 line in
	let s_cend   = Str.matched_group 5 line in
	let s_data   = Str.matched_group 6 line in
	let mk_posl s_row s_col =
          (int_of_string s_row, int_of_string s_col) in
	let posl_begin = mk_posl s_lbegin s_cbegin in
	let posl_end   = mk_posl s_lend s_cend in

	(* map the line to a value *)
	let value =
	      match Str.string_match intset_regexp s_data 0 with
		true  ->
		  let n_fields = int_of_string (Str.matched_group 1 s_data) in
		  let s_fields = Str.matched_group 2 s_data in
		  let strs = Str.bounded_split split_regexp s_fields n_fields in
		  let ints = List.map Int64.of_string strs in
		  let set = List.fold_right Int64Set.add ints Int64Set.empty in
		  IntSet set
	      | false ->
		  match Str.string_match intbounds_regexp s_data 0 with
		    true  -> let mk_bound s =
		                   match String.length s == 0 with
				     true  -> None
				   | false -> Some (Int64.of_string s) in
		             IntBounds (mk_bound (Str.matched_group 1 s_data),
					mk_bound (Str.matched_group 2 s_data))
		  | false -> Other s_data in

	(* add the new value to the current map *)
	let ensure_str m k f =
	      let v = match StringMap.mem k m with
		        true  -> f (StringMap.find k m)
	              | false -> f PoslMap.empty in
	      StringMap.add k v m in
	let ensure_posl k e f m =
	      let v = match PoslMap.mem k m with
		        true  -> f (PoslMap.find k m)
	              | false -> f e in
	      PoslMap.add k v m in

	current_map := ensure_str !current_map s_file
	  (ensure_posl posl_begin PoslMap.empty
             (ensure_posl posl_end [] (fun xs -> value :: xs )))
  done with End_of_file -> ();
  close_in chan



(* finds all nearest results in the map that enclose the given position *)
let find_results filename p_begin p_end =
  try
    let m_begin = StringMap.find filename !current_map in
    let m_end   = PoslMap.find_nearest true m_begin p_begin in
    let results = PoslMap.find_nearest false m_end p_end in
    results
  with Not_found -> []


(*
 * some convenience functions on analysis results.
 *)

let within_bounds c l u =
  match (l, u) with
    (None, None)     -> true
  | (None, Some k)   -> c <= k
  | (Some k, None)   -> k <= c
  | (Some k, Some n) -> k <= c && c <= n

let contains_bounds m n l u =
  begin
    match (l, m) with
      (None, None)     -> true
    | (Some k, Some i) -> k <= i
    | _                -> false
  end && begin
    match (u, n) with
      (None, None)     -> true
    | (Some q, Some j) -> j <= q
    | _                -> false
  end

(* given two result values, computes their intersection. An empty intersection
   is indicated with a None result value.
*)
let intersect_results r1 r2 =
  let sets s1 s2 =
    match Int64Set.inter s1 s2 with
      s when Int64Set.is_empty s -> None
    | s                          -> Some (IntSet s) in
  let bounds_set r l u s =
    if Int64Set.for_all (fun c -> within_bounds c l u) s
    then Some r
    else None in
  let bounds r m n l u =
    if contains_bounds m n l u
    then Some r
    else None in
  match r1 with
    IntSet s1 -> begin
      match r2 with
	IntSet s2        -> sets s1 s2
      | IntBounds (l, u) -> bounds_set r2 l u s1
      | Other _          -> None
      end
  | IntBounds (l, u) -> begin
      match r2 with
	IntSet s2        -> bounds_set r1 l u s2
      | IntBounds (m, n) -> bounds r1 l u m n
      | Other _          -> None
      end
  | Other _ -> None

(* a predicate over the analysis results *)
let satisfy f filename p_begin p_end =
  try f (find_results filename p_begin p_end)
  with Not_found -> false

(* satisfy, but with the intersection of all analysis results. *)
let satisfy1 f =
  let inter mbR r =
    match mbR with
      None   -> None
    | Some s -> intersect_results r s in
  satisfy
    begin fun ls ->
      match ls with
        []        -> false
      | (x :: xs) ->
	  match List.fold_left inter (Some x) xs with
	    None   -> false
	  | Some r -> f r
    end

let has_any_result = satisfy (fun rs -> List.length rs > 0)

let for_all p = satisfy (List.for_all p)

let for_all1 p = satisfy
  (fun rs -> List.length rs > 0 && List.for_all p rs)

let exists p = satisfy (List.exists p)

let single_int c r =
  match r with
  | IntSet s when Int64Set.is_empty s -> true  (* unreachable memory, thus any property holds *)
  | IntSet s                   -> Int64Set.equal (Int64Set.singleton c) s
  | IntBounds (Some l, Some u) -> l == c && u == c
  | _                          -> false

let contains_int c r =
  match r with
    IntSet s         -> Int64Set.mem c s
  | IntBounds (l, u) -> within_bounds c l u
  | _                -> false

let has_only_nul = for_all1 (single_int Int64.zero)
let has_also_nul = exists (contains_int Int64.zero)
let has_also_int c = exists (contains_int c)