summaryrefslogtreecommitdiff
blob: 88485fcd2798cd33389d6730fdd982deb5b1971b (plain)
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
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
(*
 * Analyse libvirt driver API methods for mutex locking mistakes
 *
 * Copyright (C) 2008-2010, 2012 Red Hat, Inc.
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2.1 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library.  If not, see
 * <http://www.gnu.org/licenses/>.
 *
 * Author: Daniel P. Berrange <berrange@redhat.com>
 *)

open Pretty
open Cil

(*
 * Convenient routine to load the contents of a file into
 * a list of strings
 *)
let input_file filename =
  let chan = open_in filename in
  let lines = ref [] in
  try while true; do lines := input_line chan :: !lines done; []
  with
    End_of_file -> close_in chan; List.rev !lines

module DF = Dataflow
module UD = Usedef
module IH = Inthash
module E = Errormsg
module VS = UD.VS

let debug = ref false


let driverTables = [
  "virDriver";
  "virNetworkDriver";
  "virStorageDriver";
  "virDeviceMonitor";
(*  "virStateDriver"; Disable for now, since shutdown/startup have weird locking rules *)
]

(*
 * This is the list of all libvirt methods which return
 * pointers to locked objects
 *)
let lockedObjMethods = [
   "virDomainFindByID";
   "virDomainFindByUUID";
   "virDomainFindByName";
   "virDomainAssignDef";

   "virNetworkFindByUUID";
   "virNetworkFindByName";
   "virNetworkAssignDef";

   "virNodeDeviceFindByName";
   "virNodeDeviceAssignDef";

   "virStoragePoolObjFindByUUID";
   "virStoragePoolObjFindByName";
   "virStoragePoolObjAssignDef"
]


(*
 * This is the list of all libvirt methods which
 * can release an object lock. Technically we
 * ought to pair them up correctly with previous
 * ones, but the compiler can already complain
 * about passing a virNetworkObjPtr to a virDomainObjUnlock
 * method so lets be lazy
 *)
let objectLockMethods = [
   "virDomainObjLock";
   "virNetworkObjLock";
   "virStoragePoolObjLock";
   "virNodeDevObjLock"
]

(*
 * This is the list of all libvirt methods which
 * can release an object lock. Technically we
 * ought to pair them up correctly with previous
 * ones, but the compiler can already complain
 * about passing a virNetworkObjPtr to a virDomainObjUnlock
 * method so lets be lazy
 *)
let objectUnlockMethods = [
   "virDomainObjUnlock";
   "virNetworkObjUnlock";
   "virStoragePoolObjUnlock";
   "virNodeDevObjUnlock"
]

(*
 * The data types that the previous two sets of
 * methods operate on
 *)
let lockableObjects = [
      "virDomainObjPtr";
      "virNetworkObjPtr";
      "virStoragePoolObjPtr";
      "virNodeDevObjPtr"
]



(*
 * The methods which globally lock an entire driver
 *)
let driverLockMethods = [
    "qemuDriverLock";
    "openvzDriverLock";
    "testDriverLock";
    "lxcDriverLock";
    "umlDriverLock";
    "nodedevDriverLock";
    "networkDriverLock";
    "storageDriverLock";
    "oneDriverLock"
]

(*
 * The methods which globally unlock an entire driver
 *)
let driverUnlockMethods = [
    "qemuDriverUnlock";
    "openvzDriverUnlock";
    "testDriverUnlock";
    "lxcDriverUnlock";
    "umlDriverUnlock";
    "nodedevDriverUnlock";
    "networkDriverUnlock";
    "storageDriverUnlock";
    "oneDriverUnlock"
]

(*
 * The data types that the previous two sets of
 * methods operate on. These may be structs or
 * typedefs, we don't care
 *)
let lockableDrivers = [
      "qemud_driver";
      "openvz_driver";
      "testConnPtr";
      "lxc_driver_t";
      "uml_driver";
      "virStorageDriverStatePtr";
      "network_driver";
      "virDeviceMonitorState";
      "one_driver_t";
]


let isFuncCallLval lval methodList =
   match lval with
      Var vi, o ->
          List.mem vi.vname methodList
      | _ -> false

let isFuncCallExp exp methodList =
   match exp with
       Lval lval ->
          isFuncCallLval lval methodList
       | _ -> false

let isFuncCallInstr instr methodList =
   match instr with
       Call (retval,exp,explist,srcloc) ->
         isFuncCallExp exp methodList
       | _ -> false



let findDriverFunc init =
   match init with
       SingleInit (exp) -> (
         match exp with
           AddrOf (lval) -> (
              match lval with
                  Var vi, o ->
                    true
                | _ -> false
           )
           | _ -> false
       )
     | _ ->false

let findDriverFuncs init =
   match init with
      CompoundInit (typ, list) ->
           List.filter (
              fun l ->
                 match l with
                   (offset, init) ->
                       findDriverFunc init

          ) list;
      | _ -> ([])


let getDriverFuncs initinfo =
   match initinfo.init with
      Some (i) ->
        let ls = findDriverFuncs i in
        ls
     | _ -> []

let getDriverFuncName init =
   match init with
       SingleInit (exp) -> (
         match exp with
           AddrOf (lval) -> (
              match lval with
                Var vi, o ->

                    vi.vname
                | _ -> "unknown"
           )
           | _ -> "unknown"
       )
     | _ -> "unknown"


let getDriverFuncNames initinfo =
   List.map (
       fun l ->
         match l with
            (offset, init) ->
               getDriverFuncName init
   ) (getDriverFuncs initinfo)


(*
 * Convenience methods which take a Cil.Instr object
 * and ask whether its associated with one of the
 * method sets defined earlier
 *)
let isObjectFetchCall instr =
   isFuncCallInstr instr lockedObjMethods

let isObjectLockCall instr =
   isFuncCallInstr instr objectLockMethods

let isObjectUnlockCall instr =
   isFuncCallInstr instr objectUnlockMethods

let isDriverLockCall instr =
   isFuncCallInstr instr driverLockMethods

let isDriverUnlockCall instr =
   isFuncCallInstr instr driverUnlockMethods


let isWantedType typ typeList =
    match typ with
      TNamed (tinfo, attrs) ->
         List.mem tinfo.tname typeList
      | TPtr (ptrtyp, attrs) ->
         let f = match ptrtyp with
           TNamed (tinfo2, attrs) ->
               List.mem tinfo2.tname typeList
           | TComp (cinfo, attrs) ->
               List.mem cinfo.cname typeList
           | _ ->
               false in
         f
      | _ -> false

(*
 * Convenience methods which take a Cil.Varinfo object
 * and ask whether it matches a variable datatype that
 * we're interested in tracking for locking purposes
 *)
let isLockableObjectVar varinfo =
    isWantedType varinfo.vtype lockableObjects

let isLockableDriverVar varinfo =
    isWantedType varinfo.vtype lockableDrivers

let isDriverTable varinfo =
    isWantedType varinfo.vtype driverTables


(*
 * Take a Cil.Exp object (ie an expression) and see whether
 * the expression corresponds to a check for NULL against
 * one of our interesting objects
 * eg
 *
 *     if (!vm) ...
 *
 * For a variable 'virDomainObjPtr vm'
 *)
let isLockableThingNull exp funcheck =
   match exp with
     | UnOp (op,exp,typ) -> (
         match op with
           LNot -> (
             match exp with
               Lval (lhost, off) -> (
                  match lhost with
                    Var vi ->
                      funcheck vi
                    | _ -> false
                 )
               | _ -> false
            )
          | _ -> false
         )
      | _ ->
          false

let isLockableObjectNull exp =
   isLockableThingNull exp isLockableObjectVar

let isLockableDriverNull exp =
   isLockableThingNull exp isLockableDriverVar


(*
 * Prior to validating a function, initialize these
 * to VS.empty
 *
 * They contain the list of driver and object variables
 * objects declared as local variables
 *
 *)
let lockableObjs: VS.t ref  = ref VS.empty
let lockableDriver: VS.t ref  = ref VS.empty

(*
 * Given a Cil.Instr object (ie a single instruction), get
 * the list of all used & defined variables associated with
 * it. Then caculate intersection with the driver and object
 * variables we're interested in tracking and return four sets
 *
 * List of used driver variables
 * List of defined driver variables
 * List of used object variables
 * List of defined object variables
 *)
let computeUseDefState i =
    let u, d = UD.computeUseDefInstr i in
    let useo = VS.inter u !lockableObjs in
    let defo = VS.inter d !lockableObjs in
    let used = VS.inter u !lockableDriver in
    let defd = VS.inter d !lockableDriver in
    (used, defd, useo, defo)


(* Some crude helpers for debugging this horrible code *)
let printVI vi =
    ignore(printf "      | %a %s\n" d_type vi.vtype vi.vname)

let printVS vs =
    VS.iter printVI vs


let prettyprint2 stmdat () (_, ld, ud, lo, ui, uud, uuo, loud, ldlo, dead) =
     text ""


type ilist = Cil.instr list

(*
 * This module implements the Cil.DataFlow.ForwardsTransfer
 * interface. This is what 'does the interesting stuff'
 * when walking over a function's code paths
 *)
module Locking = struct
  let name = "Locking"
  let debug = debug

  (*
   * Our state currently consists of
   *
   *  The set of driver variables that are locked
   *  The set of driver variables that are unlocked
   *  The set of object variables that are locked
   *  The set of object variables that are unlocked
   *
   * Lists of Cil.Instr for:
   *
   *   Instrs using an unlocked driver variable
   *   Instrs using an unlocked object variable
   *   Instrs locking a object variable while not holding a locked driver variable
   *   Instrs locking a driver variable while holding a locked object variable
   *   Instrs causing deadlock by fetching a lock object, while an object is already locked
   *
   *)
  type t = (unit * VS.t * VS.t * VS.t * VS.t * ilist * ilist * ilist * ilist * ilist)

  (* This holds an instance of our state data, per statement *)
  let stmtStartData = IH.create 32

  let pretty =
    prettyprint2 stmtStartData

  let copy (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
      ((), ld, ud, lo, uo, uud, uuo, loud, ldlo, dead)

  let computeFirstPredecessor stm (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
    ((), ld, ud, lo, uo, uud, uuo, loud, ldlo, dead)


  (*
   * Merge existing state for a statement, with new state
   *
   * If new and old state is the same, this returns None,
   * If they are different, then returns the union.
   *)
  let combinePredecessors (stm:stmt) ~(old:t) ((_, ldn, udn, lon, uon, uudn, uuon, loudn, ldlon, deadn):t) =
     match old with (_, ldo, udo, loo,uoo, uudo, uuoo, loudo, ldloo, deado)-> begin
     let lde= (VS.equal ldo ldn) || ((VS.is_empty ldo) && (VS.is_empty ldn)) in
     let ude= VS.equal udo udn || ((VS.is_empty udo) && (VS.is_empty udn)) in
     let loe= VS.equal loo lon || ((VS.is_empty loo) && (VS.is_empty lon)) in
     let uoe= VS.equal uoo uon || ((VS.is_empty uoo) && (VS.is_empty uon)) in

     if lde && ude && loe && uoe then
         None
     else (
         let ldret = VS.union ldo ldn in
         let udret = VS.union udo udn in
         let loret = VS.union loo lon in
         let uoret = VS.union uoo uon in
         Some ((), ldret, udret, loret, uoret, uudn, uuon, loudn, ldlon, deadn)
     )
     end


  (*
   * This handles a Cil.Instr object. This is sortof a C level statement.
   *)
  let doInstr i (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
     let transform (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
         let used, defd, useo, defo = computeUseDefState i in


         if isDriverLockCall i then (
            (*
             * A driver was locked, so add to the list of locked
	     * driver variables, and remove from the unlocked list
	     *)
            let retld = VS.union ld used in
            let retud = VS.diff ud used in

            (*
	     * Report if any objects are locked already since
	     * thats a deadlock risk
	     *)
            if VS.is_empty lo then
               ((), retld, retud, lo, uo, uud, uuo, loud, ldlo, dead)
            else
               ((), retld, retud, lo, uo, uud, uuo, loud, List.append ldlo [i], dead)
         ) else if isDriverUnlockCall i then (
            (*
             * A driver was unlocked, so add to the list of unlocked
	     * driver variables, and remove from the locked list
	     *)
            let retld = VS.diff ld used in
            let retud = VS.union ud used in

            ((), retld, retud, lo, uo, uud, uuo, loud, ldlo, dead);
         ) else if isObjectFetchCall i then (
            (*
             * A object was fetched & locked, so add to the list of
	     * locked driver variables. Nothing to remove from unlocked
	     * list here.
	     *
	     * XXX, not entirely true. We should check if they're
	     * blowing away an existing non-NULL value in the lval
	     * really.
	     *)
            let retlo = VS.union lo defo in

            (*
	     * Report if driver is not locked, since that's a safety
	     * risk
	     *)
            if VS.is_empty ld then (
	       if VS.is_empty lo then (
                 ((), ld, ud, retlo, uo, uud, uuo, List.append loud [i], ldlo, dead)
               ) else (
                 ((), ld, ud, retlo, uo, uud, uuo, List.append loud [i], ldlo, List.append dead [i])
               )
            ) else (
	       if VS.is_empty lo then (
                 ((), ld, ud, retlo, uo, uud, uuo, loud, ldlo, dead)
               ) else (
                 ((), ld, ud, retlo, uo, uud, uuo, loud, ldlo, List.append dead [i])
               )
            )
         ) else if isObjectLockCall i then (
            (*
             * A driver was locked, so add to the list of locked
	     * driver variables, and remove from the unlocked list
	     *)
            let retlo = VS.union lo useo in
            let retuo = VS.diff uo useo in

            (*
	     * Report if driver is not locked, since that's a safety
	     * risk
	     *)
            if VS.is_empty ld then
               ((), ld, ud, retlo, retuo, uud, uuo, List.append loud [i], ldlo, dead)
            else
               ((), ld, ud, retlo, retuo, uud, uuo, loud, ldlo, dead)
         ) else if isObjectUnlockCall i then (
            (*
             * A object was unlocked, so add to the list of unlocked
	     * driver variables, and remove from the locked list
	     *)
            let retlo = VS.diff lo useo in
            let retuo = VS.union uo useo in
            ((), ld, ud, retlo, retuo, uud, uuo, loud, ldlo, dead);
         ) else (
            (*
             * Nothing special happened, at best an assignment.
	     * So add any defined variables to the list of unlocked
	     * object or driver variables.
	     * XXX same edge case as isObjectFetchCall about possible
	     * overwriting
	     *)
            let retud = VS.union ud defd in
            let retuo = VS.union uo defo in

	    (*
	     * Report is a driver is used while unlocked
	     *)
            let retuud =
               if not (VS.is_empty used) && (VS.is_empty ld) then
                  List.append uud [i]
               else
                  uud in
	    (*
	     * Report is a object is used while unlocked
	     *)
            let retuuo =
               if not (VS.is_empty useo) && (VS.is_empty lo) then
                  List.append uuo [i]
               else
                  uuo in

            ((), ld, retud, lo, retuo, retuud, retuuo, loud, ldlo, dead)
         );
       in

    DF.Post transform

  (*
   * This handles a Cil.Stmt object. This is sortof a C code block
   *)
  let doStmt stm (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
     DF.SUse ((), ld, ud, lo, uo, [], [], [], [], [])


  (*
   * This handles decision making for a conditional statement,
   * ie an if (foo). It is called twice for each conditional
   * ie, once per possible choice.
   *)
  let doGuard exp (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
     (*
      * If we're going down a branch where our object variable
      * is set to NULL, then we must remove it from the
      * list of locked objects. This handles the case of...
      *
      * vm = virDomainFindByUUID(..)
      * if (!vm) {
      *     .... this code branch ....
      * } else {
      *     .... leaves default handling for this branch ...
      * }
      *)
     let lonull = UD.computeUseExp exp in

     let loret =
       if isLockableObjectNull exp then
          VS.diff lo lonull
       else
          lo in
     let uoret =
       if isLockableObjectNull exp then
          VS.union uo lonull
       else
          uo in
     let ldret =
       if isLockableDriverNull exp then
          VS.diff ld lonull
       else
          ld in
     let udret =
       if isLockableDriverNull exp then
          VS.union ud lonull
       else
          ud in

     DF.GUse ((), ldret, udret, loret, uoret, uud, uuo, loud, ldlo, dead)

  (*
   * We're not filtering out any statements
   *)
  let filterStmt stm = true

end

module L = DF.ForwardsDataFlow(Locking)

let () =
  (* Read the list of files from "libvirt-files". *)
  let files = input_file "object-locking-files.txt" in

  (* Load & parse each input file. *)
  let files =
    List.map (
      fun filename ->
	(* Why does parse return a continuation? *)
	let f = Frontc.parse filename in
	f ()
    ) files in

  (* Merge them. *)
  let file = Mergecil.merge files "test" in

  (* Do control-flow-graph analysis. *)
  Cfg.computeFileCFG file;

  print_endline "";

  let driverVars = List.filter (
    function
    | GVar (varinfo, initinfo, loc) -> (* global variable *)
      let name = varinfo.vname in
      if isDriverTable varinfo then
        true
      else
         false
    | _ -> false
  ) file.globals in

  let driverVarFuncs = List.map (
    function
    | GVar (varinfo, initinfo, loc) -> (* global variable *)
      let name = varinfo.vname in
      if isDriverTable varinfo then
        getDriverFuncNames initinfo
      else
        []
    | _ -> []
  ) driverVars in

  let driverFuncsAll = List.flatten driverVarFuncs in
  let driverFuncsSkip = [
      "testClose";
      "openvzClose";
  ] in
  let driverFuncs = List.filter (
     fun st ->
         if List.mem st driverFuncsSkip then
            false
         else
            true
  ) driverFuncsAll in

  (*
   * Now comes our fun.... iterate over every global symbol
   * definition Cfg found..... but...
   *)
  List.iter (
    function
    (* ....only care about functions *)
    | GFun (fundec, loc) -> (* function definition *)
      let name = fundec.svar.vname in

      if List.mem name driverFuncs then (
         (* Initialize list of driver & object variables to be empty *)
	 ignore (lockableDriver = ref VS.empty);
	 ignore (lockableObjs = ref VS.empty);

         (*
          * Query all local variables, and figure out which correspond
          * to interesting driver & object variables we track
          *)
         List.iter (
              fun var ->
                if isLockableDriverVar var then
                   lockableDriver := VS.add var !lockableDriver
                else if isLockableObjectVar var then
                   lockableObjs := VS.add var !lockableObjs;
          ) fundec.slocals;

         List.iter (
              fun gl ->
                 match gl with
                   GVar (vi, ii, loc) ->
                     if isLockableDriverVar vi then
                        lockableDriver := VS.add vi !lockableDriver
                  | _ -> ()
         ) file.globals;

         (*
          * Initialize the state for each statement (ie C code block)
          * to be empty
          *)
         List.iter (
         fun st ->
             IH.add Locking.stmtStartData st.sid ((),
                       VS.empty, VS.empty, VS.empty, VS.empty,
                       [], [], [], [], [])
         ) fundec.sallstmts;

         (*
          * This walks all the code paths in the function building
          * up the state for each statement (ie C code block)
          * ie, this is invoking the "Locking" module we created
          * earlier
          *)
         L.compute fundec.sallstmts;

         (*
          * Find all statements (ie C code blocks) which have no
          * successor statements. This means they are exit points
          * in the function
          *)
         let exitPoints = List.filter (
                     fun st ->
                       List.length st.succs = 0
                    ) fundec.sallstmts in

         (*
          * For each of the exit points, check to see if there are
          * any with locked driver or object variables & grab them
          *)
         let leaks = List.filter (
		       fun st ->
			   let (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
                                   IH.find Locking.stmtStartData st.sid in
			   let leakDrivers = not (VS.is_empty ld) in
			   let leakObjects = not (VS.is_empty lo) in
			   leakDrivers or leakObjects
                     ) exitPoints in

         let mistakes = List.filter (
		       fun st ->
			   let (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
                                   IH.find Locking.stmtStartData st.sid in
                           let lockDriverOrdering = (List.length ldlo) > 0 in
                           let lockObjectOrdering = (List.length loud) > 0 in

                           let useDriverUnlocked = (List.length uud) > 0 in
                           let useObjectUnlocked = (List.length uuo) > 0 in

			   let deadLocked = (List.length dead) > 0 in

			   lockDriverOrdering or lockObjectOrdering or useDriverUnlocked or useObjectUnlocked or deadLocked
                     ) fundec.sallstmts in

         if (List.length leaks) > 0 || (List.length mistakes) > 0 then (
		print_endline "================================================================";
		ignore (printf "Function: %s\n" name);
		print_endline "----------------------------------------------------------------";
		ignore (printf "  - Total exit points with locked vars: %d\n" (List.length leaks));

		(*
		 * Finally tell the user which exit points had locked varaibles
		 * And show them the line number and code snippet for easy fixing
		 *)
		List.iter (
			fun st ->
			    ignore (Pretty.printf "  - At exit on %a\n^^^^^^^^^\n" d_stmt st);
			    let (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
                            IH.find Locking.stmtStartData st.sid in
			    print_endline "    variables still locked are";
			    printVS ld;
			    printVS lo
			    ) leaks;


		ignore (printf "  - Total blocks with lock ordering mistakes: %d\n" (List.length mistakes));
		List.iter (
			fun st ->
			    let (_, ld, ud, lo, uo, uud, uuo, loud, ldlo, dead) =
			    IH.find Locking.stmtStartData st.sid in
			    List.iter (
				fun i ->
				    ignore (Pretty.printf "  - Driver locked while object is locked on %a\n" d_instr i);
				) ldlo;
			    List.iter (
				fun i ->
				    ignore (Pretty.printf "  - Object locked while driver is unlocked on %a\n" d_instr i);
				) loud;
			    List.iter (
				fun i ->
				    ignore (Pretty.printf "  - Driver used while unlocked on %a\n" d_instr i);
				) uud;
			    List.iter (
				fun i ->
				    ignore (Pretty.printf "  - Object used while unlocked on %a\n" d_instr i);
			    ) uuo;
			    List.iter (
				fun i ->
				    ignore (Pretty.printf "  - Object fetched while locked objects exist %a\n" d_instr i);
			    ) dead;
		) mistakes;
		print_endline "================================================================";
		print_endline "";
		print_endline "";
	  );

         ()
      )
    | _ -> ()
  ) file.globals;