/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
endif WITH_VMWARE
if WITH_CIL
-test_programs += object-locking
+test_programs += objectlocking
endif WITH_CIL
if WITH_YAJL
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
+++ /dev/null
-(*
- * 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;
--- /dev/null
+(*
+ * 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;