shaba/libvirt
1
0
Fork 0
mirror of https://gitlab.com/libvirt/libvirt.git synced 2025-01-10 05:17:59 +03:00
Code Releases Activity

Added an optional OCaml+CIL test program for mutex lock validation

Browse Source
This commit is contained in:
Daniel P. Berrange 2009-05-19 10:17:17 +00:00
parent 3ce55d22e4
commit 6962a2dd7e
10 changed files with 903 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.hgignore
View File

@ -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

13
ChangeLog
View File

@ -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

16
configure.in
View 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],

2
src/.cvsignore
View File

@ -16,3 +16,5 @@ libvirt_lxc
virsh-net-edit.c
virsh-pool-edit.c
libvirt.syms
*.i
*.s

2
src/.gitignore vendored
View File

@ -16,3 +16,5 @@ libvirt_lxc
virsh-net-edit.c
virsh-pool-edit.c
libvirt.syms
*.i
*.s

5
src/Makefile.am
View 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)

4
tests/.cvsignore
View File

@ -20,3 +20,7 @@ eventtest
*.gcda
*.gcno
*.exe
object-locking
object-locking.cmi
object-locking.cmx
object-locking-files.txt

4
tests/.gitignore vendored
View File

@ -20,3 +20,7 @@ eventtest
*.gcda
*.gcno
*.exe
object-locking
object-locking.cmi
object-locking.cmx
object-locking-files.txt

27
tests/Makefile.am
View 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

827
tests/object-locking.ml Normal file
View File

@ -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;