Skip to content

Commit

Permalink
Merge pull request #839 from goblint/issue_718
Browse files Browse the repository at this point in the history
MayLock Analysis & Sanity Checks of Mutex Usage & Analysis of Mutex Types
  • Loading branch information
michael-schwarz authored May 29, 2023
2 parents e56e045 + 01b9841 commit bdb69f0
Showing 27 changed files with 926 additions and 41 deletions.
28 changes: 28 additions & 0 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
@@ -536,6 +536,7 @@ struct
| `Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask gs st v t description) acc) s empty
| `Int _ -> empty
| `Float _ -> empty
| `MutexAttr _ -> empty
| `Thread _ -> empty (* thread IDs are abstract and nothing known can be reached from them *)
| `JmpBuf _ -> empty (* Jump buffers are abstract and nothing known can be reached from them *)
| `Mutex -> empty (* mutexes are abstract and nothing known can be reached from them *)
@@ -677,6 +678,7 @@ struct
ValueDomain.Structs.fold f s (empty, TS.bot (), false)
| `Int _ -> (empty, TS.bot (), false)
| `Float _ -> (empty, TS.bot (), false)
| `MutexAttr _ -> (empty, TS.bot (), false)
| `Thread _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
| `JmpBuf _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
| `Mutex -> (empty, TS.bot (), false) (* TODO: is this right? *)
@@ -1254,6 +1256,12 @@ struct
end
| Q.EvalInt e ->
query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
| Q.EvalMutexAttr e -> begin
let e:exp = Lval (Cil.mkMem ~addr:e ~off:NoOffset) in
match eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
| `MutexAttr a -> a
| v -> MutexAttrDomain.top ()
end
| Q.EvalLength e -> begin
match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
| `Address a ->
@@ -2095,6 +2103,26 @@ struct
| _ -> ()
end;
raise Deadcode
| MutexAttrSetType {attr = attr; typ = mtyp}, _ ->
begin
let get_type lval =
let address = eval_lv (Analyses.ask_of_ctx ctx) gs st lval in
AD.get_type address
in
let dst_lval = mkMem ~addr:(Cil.stripCasts attr) ~off:NoOffset in
let dest_typ = get_type dst_lval in
let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dst_lval in
match eval_rv (Analyses.ask_of_ctx ctx) gs st mtyp with
| `Int x ->
begin
match ID.to_int x with
| Some z ->
if M.tracing then M.tracel "attr" "setting\n";
set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (`MutexAttr (ValueDomain.MutexAttr.of_int z))
| None -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (`MutexAttr (ValueDomain.MutexAttr.top ()))
end
| _ -> set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (`MutexAttr (ValueDomain.MutexAttr.top ()))
end
| Identity e, _ ->
begin match lv with
| Some x -> assign ctx x e
2 changes: 2 additions & 0 deletions src/analyses/libraryDesc.ml
Original file line number Diff line number Diff line change
@@ -54,6 +54,8 @@ type special =
| ThreadExit of { ret_val: Cil.exp; }
| Signal of Cil.exp
| Broadcast of Cil.exp
| MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
| MutexInit of { mutex:Cil.exp; attr: Cil.exp; }
| Wait of { cond: Cil.exp; mutex: Cil.exp; }
| TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
| Math of { fun_args: math; }
2 changes: 2 additions & 0 deletions src/analyses/libraryFunctions.ml
Original file line number Diff line number Diff line change
@@ -147,6 +147,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond);
("pthread_cond_wait", special [__ "cond" []; __ "mutex" []] @@ fun cond mutex -> Wait {cond; mutex});
("pthread_cond_timedwait", special [__ "cond" []; __ "mutex" []; __ "abstime" [r]] @@ fun cond mutex abstime -> TimedWait {cond; mutex; abstime});
("pthread_mutexattr_settype", special [__ "attr" []; __ "type" []] @@ fun attr typ -> MutexAttrSetType {attr; typ});
("pthread_mutex_init", special [__ "mutex" []; __ "attr" []] @@ fun mutex attr -> MutexInit {mutex; attr});
("pthread_attr_destroy", unknown [drop "attr" [f]]);
("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]);
("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
50 changes: 42 additions & 8 deletions src/analyses/mayLocks.ml
Original file line number Diff line number Diff line change
@@ -1,20 +1,43 @@
(** May lockset analysis ([maylocks]). *)

(* TODO: unused *)
(** May lockset analysis and analysis of double locking ([maylocks]). *)

open Analyses
open GoblintCil
module LF = LibraryFunctions

module Arg =
module Arg:LocksetAnalysis.MayArg =
struct
module D = LockDomain.MayLockset
module D = LockDomain.MayLocksetNoRW
module G = DefaultSpec.G
module V = DefaultSpec.V

let add ctx l =
D.add l ctx.local
let add ctx (l,r) =
if D.mem l ctx.local then
let default () =
M.warn ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a (possibly non-recursive) mutex that may be already held";
ctx.local
in
match D.Addr.to_var_offset l with
| Some (v,o) ->
(let mtype = ctx.ask (Queries.MutexType (v, Lval.OffsetNoIdx.of_offs o)) in
match mtype with
| `Lifted MutexAttrDomain.MutexKind.Recursive -> ctx.local
| `Lifted MutexAttrDomain.MutexKind.NonRec ->
M.warn ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a non-recursive mutex that may be already held";
ctx.local
| _ -> default ())
| _ -> default ()
else
D.add l ctx.local

let remove ctx l =
D.remove (l, true) (D.remove (l, false) ctx.local)
if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
match D.Addr.to_var_offset l with
| Some (v,o) ->
(let mtype = ctx.ask (Queries.MutexType (v, Lval.OffsetNoIdx.of_offs o)) in
match mtype with
| `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
| _ -> ctx.local (* we cannot remove them here *))
| None -> ctx.local (* we cannot remove them here *)
end

module Spec =
@@ -23,6 +46,17 @@ struct
let name () = "maylocks"

let exitstate v = D.top () (* TODO: why? *)

let return ctx exp fundec =
if not (D.is_bot ctx.local) && ThreadReturn.is_current (Analyses.ask_of_ctx ctx) then M.warn "Exiting thread while still holding a mutex!";
ctx.local

let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
(match(LF.find f).special args with
| ThreadExit _ -> if not @@ D.is_bot ctx.local then M.warn "Exiting thread while still holding a mutex!"
| _ -> ())
;
ctx.local
end

let _ =
2 changes: 2 additions & 0 deletions src/analyses/mutexAnalysis.ml
Original file line number Diff line number Diff line change
@@ -71,13 +71,15 @@ struct
D.add l ctx.local

let remove ctx l =
if not (D.mem (l,true) ctx.local || D.mem (l,false) ctx.local) then M.warn "unlocking mutex which may not be held";
D.remove (l, true) (D.remove (l, false) ctx.local)

let remove_all ctx =
(* Mutexes.iter (fun m ->
ctx.emit (MustUnlock m)
) (D.export_locks ctx.local); *)
(* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *)
M.warn "unlocking unknown mutex which may not be held";
D.empty ()
end
include LocksetAnalysis.MakeMust (Arg)
75 changes: 75 additions & 0 deletions src/analyses/mutexTypeAnalysis.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
(** An analysis tracking the type of a mutex. *)

open GoblintCil
open Analyses

module MAttr = ValueDomain.MutexAttr
module LF = LibraryFunctions

module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Lattice.Unit =
struct
include Analyses.IdentitySpec

let name () = "pthreadMutexType"
module D = Lattice.Unit
module C = Lattice.Unit

(* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
module O = Lval.OffsetNoIdx

module V = struct
include Printable.Prod(CilType.Varinfo)(O)
let is_write_only _ = false
end

module G = MAttr

(* transfer functions *)
let assign ctx (lval:lval) (rval:exp) : D.t =
match lval with
| (Var v, o) ->
(* There's no way to use the PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP etc for accesses via pointers *)
let rec helper o t = function
| Field ({fname = "__data"; _}, Field ({fname = "__kind"; _}, NoOffset)) when ValueDomain.Compound.is_mutex_type t ->
let kind =
(match Cil.constFold true rval with
| Const (CInt (c, _, _)) -> MAttr.of_int c
| _ -> `Top)
in
ctx.sideg (v,o) kind;
ctx.local
| Index (i,o') ->
let o'' = O.of_offs (`Index (i, `NoOffset)) in
helper (O.add_offset o o'') (Cilfacade.typeOffset t (Index (i,NoOffset))) o'
| Field (f,o') ->
let o'' = O.of_offs (`Field (f, `NoOffset)) in
helper (O.add_offset o o'') (Cilfacade.typeOffset t (Field (f,NoOffset))) o'
| NoOffset -> ctx.local
in
helper `NoOffset v.vtype o
| _ -> ctx.local

let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
let desc = LF.find f in
match desc.special arglist with
| MutexInit {mutex = mutex; attr = attr} ->
let attr = ctx.ask (Queries.EvalMutexAttr attr) in
let mutexes = ctx.ask (Queries.MayPointTo mutex) in
(* It is correct to iter over these sets here, as mutexes need to be intialized before being used, and an analysis that detects usage before initialization is a different analysis. *)
Queries.LS.iter (function (v, o) -> ctx.sideg (v,O.of_offs o) attr) mutexes;
ctx.local
| _ -> ctx.local

let startstate v = D.bot ()
let threadenter ctx lval f args = [D.top ()]
let threadspawn ctx lval f args fctx = ctx.local
let exitstate v = D.top ()

let query ctx (type a) (q: a Queries.t): a Queries.result =
match q with
| Queries.MutexType (v,o) -> (ctx.global (v,o):MutexAttrDomain.t)
| _ -> Queries.Result.top q
end

let _ =
MCP.register_analysis (module Spec : MCPSpec)
1 change: 0 additions & 1 deletion src/analyses/threadAnalysis.ml
Original file line number Diff line number Diff line change
@@ -22,7 +22,6 @@ struct
module P = IdentityP (D)

(* transfer functions *)

let return ctx (exp:exp option) (f:fundec) : D.t =
let tid = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
begin match tid with
2 changes: 1 addition & 1 deletion src/autoTune.ml
Original file line number Diff line number Diff line change
@@ -204,7 +204,7 @@ let activateLongjmpAnalysesWhenRequired () =
let isLongjmp = function
| LibraryDesc.Longjmp _ -> true
| _ -> false
in
in
if hasFunction isLongjmp then (
print_endline @@ "longjmp -> enabling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\"";
enableAnalyses longjmpAnalyses;
30 changes: 10 additions & 20 deletions src/cdomains/lockDomain.ml
Original file line number Diff line number Diff line change
@@ -43,13 +43,7 @@ struct
)
end

(* TODO: use SetDomain.Reverse *)
module ReverseAddrSet = SetDomain.ToppedSet (Lock)
(struct let topname = "All mutexes" end)

module AddrSet = Lattice.Reverse (ReverseAddrSet)

include AddrSet
include SetDomain.Reverse(SetDomain.ToppedSet (Lock) (struct let topname = "All mutexes" end))

let rec may_be_same_offset of1 of2 =
match of1, of2 with
@@ -62,7 +56,7 @@ struct

let add (addr,rw) set =
match (Addr.to_var_offset addr) with
| Some (_,x) when Offs.is_definite x -> ReverseAddrSet.add (addr,rw) set
| Some (_,x) when Offs.is_definite x -> add (addr,rw) set
| _ -> set

let remove (addr,rw) set =
@@ -73,18 +67,9 @@ struct
| None -> false
in
match (Addr.to_var_offset addr) with
| Some (_,x) when Offs.is_definite x -> ReverseAddrSet.remove (addr,rw) set
| Some x -> ReverseAddrSet.filter (collect_diff_varinfo_with x) set
| _ -> AddrSet.top ()

let empty = ReverseAddrSet.empty
let is_empty = ReverseAddrSet.is_empty

let filter = ReverseAddrSet.filter
let fold = ReverseAddrSet.fold
let singleton = ReverseAddrSet.singleton
let mem = ReverseAddrSet.mem
let exists = ReverseAddrSet.exists
| Some (_,x) when Offs.is_definite x -> remove (addr,rw) set
| Some x -> filter (collect_diff_varinfo_with x) set
| _ -> top ()

let export_locks ls =
let f (x,_) set = Mutexes.add x set in
@@ -101,6 +86,11 @@ struct
let bot = Lockset.top
end

module MayLocksetNoRW =
struct
include PreValueDomain.AD
end

module Symbolic =
struct
(* TODO: use SetDomain.Reverse *)
34 changes: 24 additions & 10 deletions src/cdomains/lval.ml
Original file line number Diff line number Diff line change
@@ -443,32 +443,38 @@ struct
end
end

(** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *)
module NormalLatRepr (Idx: IntDomain.Z) =
struct
include NormalLat (Idx)

(* Helper for offsets without abstract values for index offsets, i.e. with unit index offsets.*)
module NoIdxOffsetBase = struct
module UnitIdxDomain =
struct
include Lattice.Unit
let equal_to _ _ = `Top
let to_int _ = None
end

let rec of_offs = function
| `NoOffset -> `NoOffset
| `Field (f,o) -> `Field (f, of_offs o)
| `Index (i,o) -> `Index (UnitIdxDomain.top (), of_offs o)
end

(** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *)
module NormalLatRepr (Idx: IntDomain.Z) =
struct
include NormalLat (Idx)

(** Representatives for lvalue sublattices as defined by {!NormalLat}. *)
module R: DisjointDomain.Representative with type elt = t =
struct
type elt = t
open NoIdxOffsetBase

(* Offset module for representative without abstract values for index offsets, i.e. with unit index offsets.
Reason: The offset in the representative (used for buckets) should not depend on the integer domains,
since different integer domains may be active at different program points. *)
include Normal (UnitIdxDomain)

let rec of_elt_offset: (fieldinfo, Idx.t) offs -> (fieldinfo, UnitIdxDomain.t) offs =
function
| `NoOffset -> `NoOffset
| `Field (f,o) -> `Field (f, of_elt_offset o)
| `Index (_,o) -> `Index (UnitIdxDomain.top (), of_elt_offset o) (* all indices to same bucket *)
let of_elt_offset: (fieldinfo, Idx.t) offs -> (fieldinfo, UnitIdxDomain.t) offs = of_offs

let of_elt (x: elt): t = match x with
| Addr (v, o) -> Addr (v, of_elt_offset o) (* addrs grouped by var and part of offset *)
@@ -628,3 +634,11 @@ struct
end
)
end

module OffsetNoIdx =
struct
include NoIdxOffsetBase
include Offset(UnitIdxDomain)

let name () = "offset without index"
end
Loading

0 comments on commit bdb69f0

Please sign in to comment.