]> xenbits.xensource.com Git - libvirt.git/commitdiff
Added an optional OCaml+CIL test program for mutex lock validation
authorDaniel P. Berrange <berrange@redhat.com>
Tue, 19 May 2009 10:17:17 +0000 (10:17 +0000)
committerDaniel P. Berrange <berrange@redhat.com>
Tue, 19 May 2009 10:17:17 +0000 (10:17 +0000)
.hgignore
ChangeLog
configure.in
src/.cvsignore
src/.gitignore
src/Makefile.am
tests/.cvsignore
tests/.gitignore
tests/Makefile.am
tests/object-locking.ml [new file with mode: 0644]

index 5cb3f7a1c7e8f5aa3127881d6afb5f724355db6b..34b995f030c6e344aee81828323ae569aafb6107 100644 (file)
--- a/.hgignore
+++ b/.hgignore
@@ -235,9 +235,11 @@ src/*.exe
 src/*.gcda
 src/*.gcno
 src/*.gcov
+src/*.i
 src/*.la
 src/*.lo
 src/*.loT
+src/*.s
 src/.deps
 src/.libs
 src/Makefile
@@ -264,6 +266,10 @@ tests/conftest
 tests/eventtest
 tests/nodedevxml2xmltest
 tests/nodeinfotest
+tests/object-locking
+tests/object-locking-files.txt
+tests/object-locking.cmi
+tests/object-locking.cmx
 tests/qemuxml2argvtest
 tests/qemuxml2xmltest
 tests/qparamtest
index 8504f611f6c20b75814b565f487e767834cdb817..9caa9fec2b368b686f11dced65a69fdbb73e5cd8 100644 (file)
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,16 @@
+Tue May 19 11:10:22 BST 2009 Daniel P. Berrange <berrange@redhat.com>
+
+       Add an optional OCaml+CIL mutex lock checker
+       * .hgignore, src/.cvsignore, src/.gitignore, tests/.gitignore,
+       tests/.cvsignore: Ignore binary files from ocaml build. Ignore
+       .i and .s files from gcc -save-temps
+       * configure.in: Add --enable-test-locking arg to turn on build
+       of OCaml/CIL mutex locking test
+       * src/Makefile.am: Add $(LOCK_CHECKING_CFLAGS) used when lock
+       checking tests are enabled.
+       * tests/Makefile.am, tests/object-locking.ml: Add OCaml/CIL
+       program for validating mutex locking correctness
+
 Mon May 18 16:10:22 BST 2009 Daniel P. Berrange <berrange@redhat.com>
 
        * src/qemu_conf.c: Declare support for migration in capabilities
index 8116fc8e6e4b023571b2c871927f80ef4a818fe9..50b4761ffffbdc98a169d853de7a84422d4cc700 100644 (file)
@@ -1132,6 +1132,22 @@ if test "${enable_oom}" = yes; then
   AC_DEFINE([TEST_OOM], 1, [Whether malloc OOM checking is enabled])
 fi
 
+
+AC_ARG_ENABLE([test-locking],
+[  --enable-test-locking       thread locking tests using CIL],
+[case "${enableval}" in
+   yes|no) ;;
+   *)      AC_MSG_ERROR([bad value ${enableval} for test-locking option]) ;;
+ esac],
+              [enableval=no])
+enable_locking=$enableval
+
+if test "$enable_locking" = "yes"; then
+  LOCK_CHECKING_CFLAGS="-Dbool=char -D_Bool=char -save-temps"
+  AC_SUBST([LOCK_CHECKING_CFLAGS])
+fi
+AM_CONDITIONAL([WITH_CIL],[test "$enable_locking" = "yes"])
+
 dnl Enable building the proxy?
 
 AC_ARG_WITH([xen-proxy],
index 537340f61f79c70248d88352f2f1bded9a6145f6..e00ce8fe007f2c6ecc59d633372ff6c83579c96b 100644 (file)
@@ -16,3 +16,5 @@ libvirt_lxc
 virsh-net-edit.c
 virsh-pool-edit.c
 libvirt.syms
+*.i
+*.s
index 537340f61f79c70248d88352f2f1bded9a6145f6..e00ce8fe007f2c6ecc59d633372ff6c83579c96b 100644 (file)
@@ -16,3 +16,5 @@ libvirt_lxc
 virsh-net-edit.c
 virsh-pool-edit.c
 libvirt.syms
+*.i
+*.s
index fd692b41984c3b052fc6d6819d56e31f0cb19ec9..5490089a270c44ac4dafce5e2d2d6c8e4baf3f4c 100644 (file)
@@ -16,7 +16,8 @@ INCLUDES = \
           -DLOCALEBASEDIR=\""$(datadir)/locale"\" \
            -DLOCAL_STATE_DIR=\""$(localstatedir)"\" \
            -DGETTEXT_PACKAGE=\"$(PACKAGE)\" \
-          $(WARN_CFLAGS)
+          $(WARN_CFLAGS) \
+          $(LOCK_CHECKING_CFLAGS)
 
 confdir = $(sysconfdir)/libvirt/
 conf_DATA = qemu.conf
@@ -662,5 +663,5 @@ if WITH_NETWORK
 endif
 
 
-CLEANFILES = *.gcov .libs/*.gcda .libs/*.gcno *.gcno *.gcda
+CLEANFILES = *.gcov .libs/*.gcda .libs/*.gcno *.gcno *.gcda *.i *.s
 DISTCLEANFILES = $(BUILT_SOURCES)
index 6a3c555e806ba07b927e7406ff007821589e02e4..60f77229fcf08909bbb7dfa6465321fa1fd77bec 100644 (file)
@@ -20,3 +20,7 @@ eventtest
 *.gcda
 *.gcno
 *.exe
+object-locking
+object-locking.cmi
+object-locking.cmx
+object-locking-files.txt
index 6a3c555e806ba07b927e7406ff007821589e02e4..60f77229fcf08909bbb7dfa6465321fa1fd77bec 100644 (file)
@@ -20,3 +20,7 @@ eventtest
 *.gcda
 *.gcno
 *.exe
+object-locking
+object-locking.cmi
+object-locking.cmx
+object-locking-files.txt
index 3cb7056199427ca70c7919230a4044b728a8c2bc..d375bcf00e383079a5f79337dd47caa962c0c3cb 100644 (file)
@@ -68,6 +68,10 @@ if WITH_SECDRIVER_SELINUX
 noinst_PROGRAMS += seclabeltest
 endif
 
+if WITH_CIL
+noinst_PROGRAMS += object-locking
+endif
+
 noinst_PROGRAMS += nodedevxml2xmltest
 
 test_scripts = \
@@ -234,4 +238,25 @@ eventtest_SOURCES = \
 eventtest_LDADD = -lrt $(LDADDS)
 endif
 
-CLEANFILES = *.cov *.gcov .libs/*.gcda .libs/*.gcno *.gcno *.gcda
+if WITH_CIL
+CILOPTFLAGS =
+CILOPTINCS =
+CILOPTPACKAGES = -package unix,str,cil
+CILOPTLIBS = -linkpkg
+
+object_locking_SOURCES = object-locking.ml
+
+%.cmx: %.ml
+       ocamlfind ocamlopt $(CILOPTFLAGS) $(CILOPTINCS) $(CILOPTPACKAGES) -c $<
+
+object-locking: object-locking.cmx object-locking-files.txt
+       ocamlfind ocamlopt $(CILOPTFLAGS) $(CILOPTINCS) $(CILOPTPACKAGES) $(CILOPTLIBS) $< -o $@
+
+object-locking-files.txt:
+       find $(top_builddir)/src/ -name '*.i' > $@
+
+else
+EXTRA_DIST += object-locking.ml
+endif
+
+CLEANFILES = *.cov *.gcov .libs/*.gcda .libs/*.gcno *.gcno *.gcda object-locking-files.txt
diff --git a/tests/object-locking.ml b/tests/object-locking.ml
new file mode 100644 (file)
index 0000000..39305ba
--- /dev/null
@@ -0,0 +1,827 @@
+(*
+ * Analyse libvirt driver API methods for mutex locking mistakes
+ *
+ * Copyright 2008-2009 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, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA
+ *
+ * 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 wierd 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"
+]
+
+(*
+ * The methods which globally unlock an entire driver
+ *)
+let driverUnlockMethods = [
+    "qemuDriverUnlock";
+    "openvzDriverUnlock";
+    "testDriverUnlock";
+    "lxcDriverUnlock";
+    "umlDriverUnlock";
+    "nodedevDriverUnlock";
+    "networkDriverUnlock";
+    "storageDriverUnlock"
+]
+
+(*
+ * 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";
+]
+
+
+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, intialize 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;
+
+