]> xenbits.xensource.com Git - libvirt.git/commitdiff
tests: cleanup object-locking test
authorMartin Kletzander <mkletzan@redhat.com>
Thu, 13 Feb 2014 14:20:04 +0000 (15:20 +0100)
committerMartin Kletzander <mkletzan@redhat.com>
Tue, 18 Mar 2014 09:20:49 +0000 (10:20 +0100)
When ran, cil is throwing out some errors and warnings for obsolete
'or' unused variables and wrong module name (it should not contain a
hyphen; hence the rename).

Signed-off-by: Martin Kletzander <mkletzan@redhat.com>
.gitignore
tests/Makefile.am
tests/object-locking.ml [deleted file]
tests/objectlocking.ml [new file with mode: 0644]

index 027c2032466c313984fe361e2287d27d7d10ff9f..0513a339a391b0f3ebd21c097102480ab3819454 100644 (file)
 /tests/*test
 !/tests/*schematest
 !/tests/virt-aa-helper-test
-/tests/object-locking
-/tests/object-locking-files.txt
-/tests/object-locking.cm[ix]
+/tests/objectlocking
+/tests/objectlocking-files.txt
+/tests/objectlocking.cm[ix]
 /tests/reconnect
 /tests/ssh
 /tests/test_conf
index 17454694029e15369f5fa7370da043a4c339b8ed..f80e7ad3209dcd763aaf34714c3b66c929b6c2e1 100644 (file)
@@ -228,7 +228,7 @@ test_programs += vmwarevertest
 endif WITH_VMWARE
 
 if WITH_CIL
-test_programs += object-locking
+test_programs += objectlocking
 endif WITH_CIL
 
 if WITH_YAJL
@@ -1016,21 +1016,21 @@ CILOPTINCS =
 CILOPTPACKAGES = -package unix,str,cil
 CILOPTLIBS = -linkpkg
 
-object_locking_SOURCES = object-locking.ml
+object_locking_SOURCES = objectlocking.ml
 
 %.cmx: %.ml
        ocamlfind ocamlopt $(CILOPTFLAGS) $(CILOPTINCS) $(CILOPTPACKAGES) -c $<
 
-object-locking: object-locking.cmx object-locking-files.txt
+objectlocking: objectlocking.cmx objectlocking-files.txt
        ocamlfind ocamlopt $(CILOPTFLAGS) $(CILOPTINCS) $(CILOPTPACKAGES) \
          $(CILOPTLIBS) $< -o $@
 
-object-locking-files.txt:
+objectlocking-files.txt:
        find $(top_builddir)/src/ -name '*.i' > $@
 
 else ! WITH_CIL
-EXTRA_DIST += object-locking.ml
+EXTRA_DIST += objectlocking.ml
 endif ! WITH_CIL
 
 CLEANFILES = *.cov *.gcov .libs/*.gcda .libs/*.gcno *.gcno *.gcda *.cmi *.cmx \
-       object-locking-files.txt
+       objectlocking-files.txt
diff --git a/tests/object-locking.ml b/tests/object-locking.ml
deleted file mode 100644 (file)
index 009b8f8..0000000
+++ /dev/null
@@ -1,828 +0,0 @@
-(*
- * 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";
-  "virNodeDeviceDriver";
-(*  "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";
-      "virNodeDeviceState";
-      "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;
diff --git a/tests/objectlocking.ml b/tests/objectlocking.ml
new file mode 100644 (file)
index 0000000..2476731
--- /dev/null
@@ -0,0 +1,826 @@
+(*
+ * Analyse libvirt driver API methods for mutex locking mistakes
+ *
+ * Copyright (C) 2008-2010, 2012, 2014 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";
+  "virNodeDeviceDriver";
+(*  "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";
+      "virNodeDeviceState";
+      "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 "objectlocking-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 *)
+      if isDriverTable varinfo then
+        true
+      else
+         false
+    | _ -> false
+  ) file.globals in
+
+  let driverVarFuncs = List.map (
+    function
+    | GVar (varinfo, initinfo, loc) -> (* global variable *)
+      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 || 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 || lockObjectOrdering || useDriverUnlocked || useObjectUnlocked || 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;