1
(**************************************************************************)
3
(* Copyright (C) 2001-2003, *)
4
(* George C. Necula <necula@cs.berkeley.edu> *)
5
(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
6
(* Wes Weimer <weimer@cs.berkeley.edu> *)
7
(* Ben Liblit <liblit@cs.berkeley.edu> *)
8
(* All rights reserved. *)
10
(* Redistribution and use in source and binary forms, with or without *)
11
(* modification, are permitted provided that the following conditions *)
14
(* 1. Redistributions of source code must retain the above copyright *)
15
(* notice, this list of conditions and the following disclaimer. *)
17
(* 2. Redistributions in binary form must reproduce the above copyright *)
18
(* notice, this list of conditions and the following disclaimer in the *)
19
(* documentation and/or other materials provided with the distribution. *)
21
(* 3. The names of the contributors may not be used to endorse or *)
22
(* promote products derived from this software without specific prior *)
23
(* written permission. *)
25
(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
26
(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
27
(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
28
(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
29
(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
30
(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
31
(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
32
(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
33
(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
34
(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
35
(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
36
(* POSSIBILITY OF SUCH DAMAGE. *)
38
(* File modified by CEA (Commissariat � l'�nergie Atomique). *)
39
(**************************************************************************)
43
* Copyright (c) 2001-2002,
44
* George C. Necula <necula@cs.berkeley.edu>
45
* Scott McPeak <smcpeak@cs.berkeley.edu>
46
* Wes Weimer <weimer@cs.berkeley.edu>
47
* All rights reserved.
49
* Redistribution and use in source and binary forms, with or without
50
* modification, are permitted provided that the following conditions are
53
* 1. Redistributions of source code must retain the above copyright
54
* notice, this list of conditions and the following disclaimer.
56
* 2. Redistributions in binary form must reproduce the above copyright
57
* notice, this list of conditions and the following disclaimer in the
58
* documentation and/or other materials provided with the distribution.
60
* 3. The names of the contributors may not be used to endorse or promote
61
* products derived from this software without specific prior written
64
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
65
* IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
66
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
67
* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
68
* OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
69
* EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
70
* PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
71
* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
72
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
73
* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
74
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
80
* Weimer: an AST Slicer for use in Daniel's Delta Debugging Algorithm.
85
* This type encapsulates a mapping form program tsets to names
86
* in our naming convention.
88
type enumeration_info = {
89
statements : (stmt, string) Hashtbl.t ;
90
instructions : (instr, string) Hashtbl.t ;
93
(**********************************************************************
96
* Given a cil file, enumerate all of the statement names in it using
98
**********************************************************************)
99
let enumerate out (f : Cil.file) =
100
let st_ht = Hashtbl.create 32767 in
101
let in_ht = Hashtbl.create 32767 in
103
let emit base i ht elt =
104
let str = Printf.sprintf "%s.%d" base !i in
105
Printf.fprintf out "%s\n" str ;
106
Hashtbl.add ht elt str ;
109
let emit_call base i str2 ht elt =
110
let str = Printf.sprintf "%s.%d" base !i in
111
Printf.fprintf out "%s - %s\n" str str2 ;
112
Hashtbl.add ht elt str ;
116
let res = (Printf.sprintf "%s.%d" base !i),(ref 0) in
119
let rec doBlock b base i =
120
doStmtList b.bstmts base i
121
and doStmtList sl base i =
122
List.iter (fun s -> match s.skind with
123
| Instr(il) -> doIL il base i
127
| Break(_) -> emit base i st_ht s
129
emit base i st_ht s ;
131
Printf.fprintf out "(\n" ;
132
let base',i' = descend base i in
133
doBlock b1 base' i' ;
134
Printf.fprintf out ") (\n" ;
135
let base'',i'' = descend base i in
136
doBlock b2 base'' i'' ;
137
Printf.fprintf out ")\n" ;
142
emit base i st_ht s ;
144
let base',i' = descend base i in
145
Printf.fprintf out "(\n" ;
147
Printf.fprintf out ")\n" ;
149
| TryExcept _ | TryFinally _ ->
150
E.s (E.unimp "astslicer:enumerate")
153
List.iter (fun ins -> match ins with
155
| Asm _ -> emit base i in_ht ins
156
| Call(_,(Lval(Var(vi),NoOffset)),_,_) ->
157
emit_call base i vi.vname in_ht ins
158
| Call(_,f,_,_) -> emit_call base i "*" in_ht ins
161
let doGlobal g = match g with
163
Printf.fprintf out "%s (\n" (!Cil.output_ident fd.svar.vname) ;
165
doBlock fd.sbody fd.svar.vname cur ;
166
Printf.fprintf out ")\n" ;
170
List.iter doGlobal f.globals ;
171
{ statements = st_ht ;
172
instructions = in_ht ; }
174
(**********************************************************************
177
* Given a cil file and some enumeration information, do a log-calls-like
178
* transformation on it that prints out our names as you reach them.
179
**********************************************************************)
181
* This is the visitor that handles annotations
183
let print_it pfun name =
184
((Call(None,Lval(Var(pfun),NoOffset),
185
[mkString (name ^ "\n")],locUnknown)))
187
class enumVisitor pfun st_ht in_ht = object
188
inherit nopCilVisitor
190
if Hashtbl.mem in_ht i then begin
191
let name = Hashtbl.find in_ht i in
192
let newinst = print_it pfun name in
193
ChangeTo([newinst ; i])
197
if Hashtbl.mem st_ht s then begin
198
let name = Hashtbl.find st_ht s in
199
let newinst = print_it pfun name in
200
let newstmt = mkStmtOneInstr newinst in
201
let newblock = mkBlock [newstmt ; s] in
202
let replace_with = mkStmt (Block(newblock)) in
203
ChangeDoChildrenPost(s,(fun i -> replace_with))
207
let newinst = print_it pfun f.svar.vname in
208
let newstmt = mkStmtOneInstr newinst in
209
let new_f = { f with sbody = { f.sbody with
210
bstmts = newstmt :: f.sbody.bstmts }} in
211
ChangeDoChildrenPost(new_f,(fun i -> i))
214
let annotate (f : Cil.file) ei = begin
215
(* Create a prototype for the logging function *)
217
let fdec = emptyFunction "printf" in
218
let argf = makeLocalVar fdec "format" charConstPtrType in
219
fdec.svar.vtype <- TFun(intType, Some [ ("format", charConstPtrType, [])],
223
let visitor = (new enumVisitor printfFun.svar ei.statements
225
visitCilFileSameGlobals visitor f;
229
(**********************************************************************
232
* Perform a transitive-closure-like operation on the parts of the program
233
* that the user wants to keep. We use a CIL visitor to walk around
234
* and a number of hash tables to keep track of the things we want to keep.
235
**********************************************************************)
239
* wi - wanted instructions
240
* wt - wanted typeinfo
241
* wc - wanted compinfo
242
* we - wanted enuminfo
243
* wv - wanted varinfo
246
let mode = ref false (* was our parented wanted? *)
247
let finished = ref true (* set to false if we update something *)
249
(* In the given hashtable, mark the given element was "wanted" *)
251
if Hashtbl.mem ht elt && (Hashtbl.find ht elt = true) then ()
253
Hashtbl.add ht elt true ;
257
(* Handle a particular stage of the AST tree walk. Use "mode" (i.e.,
258
* whether our parent was wanted) and the hashtable (which tells us whether
259
* the user had any special instructions for this element) to determine
261
let handle ht elt rep =
263
if Hashtbl.mem ht elt && (Hashtbl.find ht elt = false) then begin
264
(* our parent is Wanted but we were told to ignore this subtree,
265
* so we won't be wanted. *)
267
ChangeDoChildrenPost(rep,(fun elt -> mode := true ; elt))
269
(* we were not told to ignore this subtree, and our parent is
270
* Wanted, so we will be Wanted too! *)
274
end else if Hashtbl.mem ht elt && (Hashtbl.find ht elt = true) then begin
275
(* our parent was not wanted but we were wanted, so turn the
278
ChangeDoChildrenPost(rep,(fun elt -> mode := false ; elt))
282
let handle_no_default ht elt rep old_mode =
283
if Hashtbl.mem ht elt && (Hashtbl.find ht elt = true) then begin
284
(* our parent was not wanted but we were wanted, so turn the
287
ChangeDoChildrenPost(rep,(fun elt -> mode := old_mode ; elt))
290
ChangeDoChildrenPost(rep,(fun elt -> mode := old_mode ; elt))
294
* This is the visitor that handles elements (marks them as wanted)
296
class transVisitor ws wi wt wc we wv = object
297
inherit nopCilVisitor
299
method vvdec vi = handle_no_default wv vi vi !mode
300
method vvrbl vi = handle wv vi vi
301
method vinst i = handle wi i [i]
302
method vstmt s = handle ws s s
303
method vfunc f = handle wv f.svar f
304
method vglob g = begin
306
| GType(ti,_) -> handle wt ti [g]
308
| GCompTagDecl(ci,_) -> handle wc ci [g]
310
| GEnumTagDecl(ei,_) -> handle we ei [g]
312
| GVar(vi,_,_) -> handle wv vi [g]
313
| GFun(f,_) -> handle wv f.svar [g]
316
method vtype t = begin
318
| TNamed(ti,_) -> handle wt ti t
319
| TComp(ci,_) -> handle wc ci t
320
| TEnum(ei,_) -> handle we ei t
325
(**********************************************************************
328
* Eliminate all of the elements from the program that are not marked
330
**********************************************************************)
332
* This is the visitor that throws away elements
334
let handle ht elt keep drop =
335
if (Hashtbl.mem ht elt) && (Hashtbl.find ht elt = true) then
336
(* DoChildren *) ChangeDoChildrenPost(keep,(fun a -> a))
340
class dropVisitor ws wi wt wc we wv = object
341
inherit nopCilVisitor
343
method vinst i = handle wi i [i] []
344
method vstmt s = handle ws s s (mkStmt (Instr([])))
345
method vglob g = begin
347
| GType(ti,_) -> handle wt ti [g] []
349
| GCompTagDecl(ci,_) -> handle wc ci [g] []
351
| GEnumTagDecl(ei,_) -> handle we ei [g] []
353
| GVar(vi,_,_) -> handle wv vi [g] []
355
let new_locals = List.filter (fun vi ->
356
Hashtbl.mem wv vi && (Hashtbl.find wv vi = true)) f.slocals in
357
let new_fundec = { f with slocals = new_locals} in
358
handle wv f.svar [(GFun(new_fundec,l))] []
363
(**********************************************************************
366
* Mark up the file with user-given information about what to keep and
368
**********************************************************************)
369
type mark = Wanted | Unwanted | Unspecified
370
(* Given a cil file and a list of strings, mark all of the given ASTSlicer
371
* points as wanted or unwanted. *)
372
let mark_file (f : Cil.file) (names : (string, mark) Hashtbl.t) =
373
let ws = Hashtbl.create 32767 in
374
let wi = Hashtbl.create 32767 in
375
let wt = Hashtbl.create 32767 in
376
let wc = Hashtbl.create 32767 in
377
let we = Hashtbl.create 32767 in
378
let wv = Hashtbl.create 32767 in
379
if !debug then Printf.printf "Applying user marks to file ...\n" ;
381
let res = (Printf.sprintf "%s.%d" base !i),(ref 0) in
384
let check base i (default : mark) =
385
let str = Printf.sprintf "%s.%d" base !i in
386
if !debug then Printf.printf "Looking for [%s]\n" str ;
387
try Hashtbl.find names str
390
let mark ht stmt wanted = match wanted with
391
Unwanted -> Hashtbl.replace ht stmt false
392
| Wanted -> Hashtbl.replace ht stmt true
395
let rec doBlock b base i default =
396
doStmtList b.bstmts base i default
397
and doStmtList sl base i default =
398
List.iter (fun s -> match s.skind with
399
| Instr(il) -> doIL il base i default
404
mark ws s (check base i default) ; incr i
406
let inside = check base i default in
408
let base',i' = descend base i in
409
doBlock b1 base' i' inside ;
410
let base'',i'' = descend base i in
411
doBlock b2 base'' i'' inside ;
416
let inside = check base i default in
418
let base',i' = descend base i in
419
doBlock b base' i' inside ;
421
| TryExcept _ | TryFinally _ ->
422
E.s (E.unimp "astslicer: mark")
424
and doIL il base i default =
425
List.iter (fun ins -> mark wi ins (check base i default) ; incr i) il
427
let doGlobal g = match g with
430
if Hashtbl.mem names fd.svar.vname then begin
431
if Hashtbl.find names fd.svar.vname = Wanted then begin
432
Hashtbl.replace wv fd.svar true ;
433
doBlock fd.sbody fd.svar.vname cur (Wanted);
435
Hashtbl.replace wv fd.svar false ;
436
doBlock fd.sbody fd.svar.vname cur (Unspecified);
439
doBlock fd.sbody fd.svar.vname cur (Unspecified);
443
List.iter doGlobal f.globals ;
445
Hashtbl.iter (fun k v ->
446
ignore (Pretty.printf "want-s %b %a\n" v d_stmt k)) ws ;
447
Hashtbl.iter (fun k v ->
448
ignore (Pretty.printf "want-i %b %a\n" v d_instr k)) wi ;
449
Hashtbl.iter (fun k v ->
450
ignore (Pretty.printf "want-v %b %s\n" v (!Cil.output_ident k.vname)))
454
* Now repeatedly mark all other things that must be kept.
456
let visitor = (new transVisitor ws wi wt wc we wv) in
458
if !debug then (Printf.printf "\nPerforming Transitive Closure\n\n" );
459
while not !finished do
461
visitCilFileSameGlobals visitor f
464
Hashtbl.iter (fun k v ->
465
if v then ignore (Pretty.printf "want-s %a\n" d_stmt k)) ws ;
466
Hashtbl.iter (fun k v ->
467
if v then ignore (Pretty.printf "want-i %a\n" d_instr k)) wi ;
468
Hashtbl.iter (fun k v ->
469
if v then ignore (Pretty.printf "want-t %s\n" k.tname)) wt ;
470
Hashtbl.iter (fun k v ->
471
if v then ignore (Pretty.printf "want-c %s\n" k.cname)) wc ;
472
Hashtbl.iter (fun k v ->
473
if v then ignore (Pretty.printf "want-e %s\n" k.ename)) we ;
474
Hashtbl.iter (fun k v ->
475
if v then ignore (Pretty.printf "want-v %s\n" k.vname)) wv ;
479
* Now drop everything we didn't need.
481
if !debug then (Printf.printf "Dropping Unwanted Elements\n" );
482
let visitor = (new dropVisitor ws wi wt wc we wv) in
483
visitCilFile visitor f
added
removed
cil/src/ext/astslicer.ml
