[DRAFT] [starvation] model android::Mutex and recognise custom scoped guards

infer/src/absint/ConcurrencyModels.ml

@@ -12,6 +12,7 @@ type lock_effect =
   | Lock of HilExp.t list
   | Unlock of HilExp.t list
   | LockedIfTrue of HilExp.t list
+  | LockedIfZero of HilExp.t list
   | GuardConstruct of {guard: HilExp.t; lock: HilExp.t; acquire_now: bool}
   | GuardLock of HilExp.t
   | GuardLockedIfTrue of HilExp.t
@@ -32,6 +33,8 @@ let make_unlock = make_lock_action "release" (fun a -> Unlock a)
 
 let make_trylock = make_lock_action "conditionally acquire" (fun a -> LockedIfTrue a)
 
+let make_zero_trylock = make_lock_action "conditionally acquire" (fun a -> LockedIfZero a)
+
 let make_guard_construct procname = function
   | [_guard] ->
       (* constructor is called without a mutex *)
@@ -107,6 +110,7 @@ end = struct
     { classname: string [@default ""]
     ; lock: string list [@default []]
     ; trylock: string list [@default []]
+    ; trylock_zero: string list [@default []]  (** trylocks that return zero on success *)
     ; unlock: string list [@default []]
     ; recursive: bool [@default true] }
   [@@deriving of_yojson]
@@ -115,9 +119,14 @@ end = struct
 
   let lock_models =
     let def =
-      {classname= ""; lock= ["lock"]; trylock= ["try_lock"]; unlock= ["unlock"]; recursive= false}
+      { classname= ""
+      ; lock= ["lock"]
+      ; trylock= ["try_lock"]
+      ; trylock_zero= []
+      ; unlock= ["unlock"]
+      ; recursive= false }
     in
-    let c_rec = {classname= ""; lock= []; trylock= []; unlock= []; recursive= true} in
+    let c_rec = {def with lock= []; trylock= []; unlock= []; recursive= true} in
     let shd =
       { def with
         lock= "lock_shared" :: def.lock
@@ -132,6 +141,7 @@ end = struct
     in
     let config_locks = lock_model_cfg_of_yojson Config.lock_model in
     [ {c_rec with lock= ["pthread_mutex_lock"]; unlock= ["pthread_mutex_unlock"]}
+    ; {def with classname= "android::Mutex"; trylock= []; trylock_zero= ["timedLock"; "tryLock"]}
     ; { def with
         classname= "apache::thrift::concurrency::Monitor"
       ; trylock= "timedlock" :: def.trylock }
@@ -170,7 +180,7 @@ end = struct
     fun pname -> QualifiedCppName.Match.match_qualifiers matcher (Procname.get_qualifiers pname)
 
 
-  let is_lock, is_unlock, is_trylock, is_std_lock =
+  let is_lock, is_unlock, is_trylock, is_zero_trylock, is_std_lock =
     (* TODO std::try_lock *)
     let mk_model_matcher ~f =
       let lock_methods =
@@ -182,6 +192,7 @@ end = struct
     ( mk_model_matcher ~f:(fun mdl -> mdl.lock)
     , mk_model_matcher ~f:(fun mdl -> mdl.unlock)
     , mk_model_matcher ~f:(fun mdl -> mdl.trylock)
+    , mk_model_matcher ~f:(fun mdl -> mdl.trylock_zero)
     , mk_matcher ["std::lock"] )
 
 
@@ -191,6 +202,8 @@ end = struct
   let guards =
     (* TODO std::scoped_lock *)
     [ (* no lock/unlock *)
+      "android::Mutex::Autolock"
+    ; (* no lock/unlock *)
       "apache::thrift::concurrency::Guard"
     ; (* no lock/unlock *)
       "apache::thrift::concurrency::RWGuard"
@@ -270,6 +283,7 @@ end = struct
     else if is_lock pname then make_lock pname fst_arg
     else if is_unlock pname then make_unlock pname fst_arg
     else if is_trylock pname then make_trylock pname fst_arg
+    else if is_zero_trylock pname then make_zero_trylock pname fst_arg
     else if is_guard_constructor pname then make_guard_construct pname actuals
     else if is_guard_lock pname then make_guard_lock pname actuals
     else if is_guard_unlock pname then make_guard_unlock pname actuals

infer/src/absint/ConcurrencyModels.mli

@@ -12,6 +12,8 @@ type lock_effect =
   | Lock of HilExp.t list  (** simultaneously acquire a list of locks *)
   | Unlock of HilExp.t list  (** simultaneously release a list of locks *)
   | LockedIfTrue of HilExp.t list  (** simultaneously attempt to acquire a list of locks *)
+  | LockedIfZero of HilExp.t list
+      (** simultaneously attempt to acquire a list of locks, returning zero on success *)
   | GuardConstruct of {guard: HilExp.t; lock: HilExp.t; acquire_now: bool}
       (** mutex guard construction - clang only *)
   | GuardLock of HilExp.t  (** lock underlying mutex via guard - clang only *)

infer/src/absint/HilExp.ml

@@ -575,6 +575,8 @@ and eval_boolean_exp var = function
       eval_boolean_binop Bool.equal var e1 e2
   | BinaryOperator (Binop.Ne, e1, e2) ->
       eval_boolean_binop Bool.( <> ) var e1 e2
+  | Cast (_, e) ->
+      eval_boolean_exp var e
   | _ ->
       (* non-boolean expression; can't evaluate it *)
       None

infer/src/concurrency/AbstractAddress.ml

@@ -165,12 +165,15 @@ type t =
   | Parameter of {index: int; path: unrooted_path}
       (** method parameter represented by its 0-indexed position, root var is not used in comparison
       *)
+  | Opaque of {path: unrooted_path}
+      (** reached from a value the caller cannot name, eg returned by a call, root var is not used
+          in comparison *)
 [@@deriving compare, equal]
 
 let get_typ tenv = function
   | Class _ ->
       Some StdTyp.Java.pointer_to_java_lang_class
-  | Global {path} | Parameter {path} ->
+  | Global {path} | Parameter {path} | Opaque {path} ->
       get_typ tenv path
 
 
@@ -204,7 +207,8 @@ let rec inner_class_normalise tenv ((typ, (accesses : access_list)) as path) =
 
 let equal_across_threads tenv t1 t2 =
   match (t1, t2) with
-  | Parameter {path= (_, typ1), accesses1}, Parameter {path= (_, typ2), accesses2} ->
+  | ( (Parameter {path= (_, typ1), accesses1} | Opaque {path= (_, typ1), accesses1})
+    , (Parameter {path= (_, typ2), accesses2} | Opaque {path= (_, typ2), accesses2}) ) ->
       (* parameter position/names can be ignored across threads, if types and accesses are equal *)
       let path1 = inner_class_normalise tenv (typ1, accesses1) in
       let path2 = inner_class_normalise tenv (typ2, accesses2) in
@@ -263,12 +267,15 @@ let pp fmt t =
       F.fprintf fmt "C{%s}" (Typ.Name.name typename)
   | Parameter {index; path} ->
       F.fprintf fmt "P<%i>{%a}" index pp_path path
+  | Opaque {path} ->
+      F.fprintf fmt "O{%a}" pp_path path
 
 
 let root_class = function
   | Class {typename} ->
       Some typename
-  | Global {path= (_, {desc}), _} | Parameter {path= (_, {desc}), _} -> (
+  | Global {path= (_, {desc}), _} | Parameter {path= (_, {desc}), _} | Opaque {path= (_, {desc}), _}
+    -> (
     match desc with
     | Tstruct typename | Tptr ({desc= Tstruct typename}, _) ->
         Some typename
@@ -288,7 +295,7 @@ let describe fmt t =
   match t with
   | Class {typename} ->
       MF.wrap_monospaced describe_class_object fmt typename
-  | Global {path} | Parameter {path} ->
+  | Global {path} | Parameter {path} | Opaque {path} ->
       F.fprintf fmt "%a%a" (MF.wrap_monospaced describe_path) path describe_root t
 
 
@@ -298,28 +305,44 @@ let pp_subst fmt subst =
   PrettyPrintable.pp_collection fmt ~pp_item:(Pp.option pp) (Array.to_list subst)
 
 
+(* the address of a local is not opaque: objects on the stack of the caller are not shared *)
+let rec make_opaque (hilexp : HilExp.t) =
+  match hilexp with
+  | AccessExpression access_exp -> (
+    match HilExp.AccessExpression.to_accesses access_exp with
+    | HilExp.AccessExpression.Base base, accesses
+      when not (List.mem accesses MemoryAccess.TakeAddress ~equal:equal_access) ->
+        Some (Opaque {path= (base, accesses)})
+    | _ ->
+        None )
+  | Cast (_, hilexp) ->
+      make_opaque hilexp
+  | _ ->
+      None
+
+
 let make_subst formal_map actuals =
-  let actuals = Array.of_list actuals in
-  let len =
-    (* deal with var args functions *)
-    Int.max (FormalMap.cardinal formal_map) (Array.length actuals)
-  in
-  let subst = Array.create ~len None in
-  FormalMap.iter
-    (fun _base idx ->
-      if idx < Array.length actuals then subst.(idx) <- make formal_map actuals.(idx) )
-    formal_map ;
-  subst
+  Array.of_list_map actuals ~f:(fun actual ->
+      match make formal_map actual with None -> make_opaque actual | address -> address )
+
+
+let without_opaque subst =
+  Array.map subst ~f:(function Some (Opaque _) -> None | address -> address)
 
 
 let apply_subst (subst : subst) t =
   match t with
-  | Global _ | Class _ ->
+  | Global _ | Class _ | Opaque _ ->
       Some t
-  | Parameter {index; path= _, []} -> (
+  | Parameter {index; path= (var, _), []} -> (
     try
       (* Special case for when the parameter is used without additional accesses, eg [x] as opposed to [x.f[].g]. *)
-      subst.(index)
+      match subst.(index) with
+      | Some (Opaque {path= (_, typ), accesses}) ->
+          (* print the parameter rather than the caller's temporary *)
+          Some (Opaque {path= ((var, typ), accesses)})
+      | address ->
+          address
     with Invalid_argument _ -> None )
   | Parameter {index; path} -> (
     try
@@ -338,4 +361,11 @@ let apply_subst (subst : subst) t =
             None )
       | Some (Global global) -> (
         match append ~on_to:global.path path with Some path -> Some (Global {path}) | None -> None )
+      | Some (Opaque {path= (_, typ), accesses}) -> (
+          let (var, _), _ = path in
+          match append ~on_to:((var, typ), accesses) path with
+          | Some path ->
+              Some (Opaque {path})
+          | None ->
+              None )
     with Invalid_argument _ -> None )

infer/src/concurrency/AbstractAddress.mli

@@ -14,19 +14,23 @@ module F = Format
     - rooted at formal parameters (these are identified by the parameter index and the path without
       the root variable, though that variable is kept for pretty printing);
     - rooted at global variables;
-    - non access-path expressions representing class objects (java only).
+    - non access-path expressions representing class objects (java only);
+    - rooted at values passed to a callee that the caller cannot name, eg returned by a call
+      (opaque).
 
-    Notably, there are no addresses rooted at locals (because proving aliasing between those is
-    difficult).
+    Notably, there are no addresses rooted at the address of a local (because proving aliasing
+    between those is difficult).
 
     There are two notions of equality:
 
     - Equality for comparing two addresses within the same thread/process/trace. Under this,
       identical globals and identical class objects compare equal. Parameter-rooted paths compare
-      equal if their parameter indices, types and lists of accesses are equal.
+      equal if their parameter indices, types and lists of accesses are equal. Opaque paths compare
+      equal if their types and lists of accesses are equal.
     - Equality for comparing two addresses in two distinct threads/traces. Globals and class objects
-      are compared in the same way, but parameter-rooted paths need only have equal access lists (ie
-      [x.f.g == y.f.g]). This allows demonically aliasing parameters in *distinct* threads. *)
+      are compared in the same way, but parameter-rooted and opaque paths need only have equal
+      access lists (ie [x.f.g == y.f.g]). This allows demonically aliasing parameters in *distinct*
+      threads. *)
 
 include PrettyPrintable.PrintableOrderedType
 
@@ -50,11 +54,16 @@ val is_class_object : t -> bool
     [static synchronized void foo()] *)
 
 (** A substitution from formal position indices to address options. [None] is used to for actuals
-    that cannot be resolved to an address (eg local-rooted paths or arithmetic expressions). *)
+    that cannot be resolved to an address (eg addresses of locals or arithmetic expressions). *)
 type subst
 
 val pp_subst : F.formatter -> subst -> unit [@@warning "-unused-value-declaration"]
 
 val make_subst : FormalMap.t -> HilExp.t list -> subst
+(** [make_subst formals actuals] maps the position of each actual to its address in terms of the
+    caller's [formals] *)
+
+val without_opaque : subst -> subst
+(** maps the actuals that only have an opaque address to [None] *)
 
 val apply_subst : subst -> t -> t option

infer/src/concurrency/RacerDDomain.ml

@@ -449,7 +449,8 @@ module OwnershipDomain = struct
 end
 
 module Attribute = struct
-  type t = Nothing | Functional | OnMainThread | LockHeld | Synchronized [@@deriving equal]
+  type t = Nothing | Functional | OnMainThread | LockHeld | LockHeldIfZero | Synchronized
+  [@@deriving equal]
 
   let pp fmt t =
     ( match t with
@@ -461,6 +462,8 @@ module Attribute = struct
           "OnMainThread"
       | LockHeld ->
           "LockHeld"
+      | LockHeldIfZero ->
+          "LockHeldIfZero"
       | Synchronized ->
           "Synchronized" )
     |> F.pp_print_string fmt
@@ -733,7 +736,12 @@ let release_lock (astate : t) =
   ; threads= ThreadsDomain.update_for_lock_use astate.threads }
 
 
-let lock_if_true ret_access_exp (astate : t) =
+let add_lock_attribute attribute ret_access_exp (astate : t) =
   { astate with
-    attribute_map= AttributeMapDomain.add ret_access_exp Attribute.LockHeld astate.attribute_map
+    attribute_map= AttributeMapDomain.add ret_access_exp attribute astate.attribute_map
   ; threads= ThreadsDomain.update_for_lock_use astate.threads }
+
+
+let lock_if_true = add_lock_attribute Attribute.LockHeld
+
+let lock_if_zero = add_lock_attribute Attribute.LockHeldIfZero

infer/src/concurrency/RacerDDomain.mli

@@ -115,6 +115,7 @@ module Attribute : sig
     | Functional  (** holds a value returned from a callee marked [@Functional] *)
     | OnMainThread  (** boolean is true if the current procedure is running on the main thread *)
     | LockHeld  (** boolean is true if a lock is currently held *)
+    | LockHeldIfZero  (** value is zero if a lock is currently held *)
     | Synchronized  (** the object is a synchronized data structure *)
 end
 
@@ -201,4 +202,6 @@ val release_lock : t -> t
 
 val lock_if_true : HilExp.access_expression -> t -> t
 
+val lock_if_zero : HilExp.access_expression -> t -> t
+
 val branch_never_returns : unit -> t

infer/src/concurrency/RacerDProcAnalysis.ml

@@ -91,6 +91,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         Domain.release_lock astate
     | LockedIfTrue _ | GuardLockedIfTrue _ ->
         Domain.lock_if_true ret_access_exp astate
+    | LockedIfZero _ ->
+        Domain.lock_if_zero ret_access_exp astate
     | GuardConstruct {acquire_now= false} ->
         astate
     | NoEffect when RacerDModels.proc_is_ignored_by_racerd callee_pname ->
@@ -166,13 +168,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let do_assume formals assume_exp loc tenv (astate : Domain.t) =
     let open Domain in
-    let apply_choice bool_value (acc : Domain.t) = function
+    let rec apply_choice bool_value (acc : Domain.t) = function
       | Attribute.LockHeld ->
           let locks =
             if bool_value then LockDomain.acquire_lock acc.locks
             else LockDomain.release_lock acc.locks
           in
           {acc with locks}
+      | Attribute.LockHeldIfZero ->
+          apply_choice (not bool_value) acc Attribute.LockHeld
       | Attribute.OnMainThread ->
           let threads =
             if bool_value then ThreadsDomain.AnyThreadButSelf else ThreadsDomain.AnyThread
@@ -181,15 +185,40 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | Attribute.(Functional | Nothing | Synchronized) ->
           acc
     in
+    (* trylocks returning zero on success return negative error codes, so [r < 0] means [r != 0] *)
+    let rec zero_status_as_equality (exp : HilExp.t) : HilExp.t =
+      match exp with
+      | BinaryOperator (Lt, e1, e2) when HilExp.is_int_zero e2 ->
+          BinaryOperator (Ne, e1, e2)
+      | BinaryOperator (Ge, e1, e2) when HilExp.is_int_zero e2 ->
+          BinaryOperator (Eq, e1, e2)
+      | BinaryOperator (Gt, e1, e2) when HilExp.is_int_zero e1 ->
+          BinaryOperator (Ne, e1, e2)
+      | BinaryOperator (Le, e1, e2) when HilExp.is_int_zero e1 ->
+          BinaryOperator (Eq, e1, e2)
+      | UnaryOperator (LNot, e, typ) ->
+          UnaryOperator (LNot, zero_status_as_equality e, typ)
+      | Cast (typ, e) ->
+          Cast (typ, zero_status_as_equality e)
+      | _ ->
+          exp
+    in
     let astate = add_access tenv formals loc ~is_write:false astate assume_exp in
     match HilExp.get_access_exprs assume_exp with
     | [access_expr] ->
+        let attribute = AttributeMapDomain.get access_expr astate.attribute_map in
+        let assume_exp =
+          match attribute with
+          | Attribute.LockHeldIfZero ->
+              zero_status_as_equality assume_exp
+          | _ ->
+              assume_exp
+        in
         HilExp.eval_boolean_exp access_expr assume_exp
         |> Option.value_map ~default:astate ~f:(fun bool_value ->
             (* prune (prune_exp) can only evaluate to true if the choice is [bool_value].
                   add the constraint that the choice must be [bool_value] to the state *)
-            AttributeMapDomain.get access_expr astate.attribute_map
-            |> apply_choice bool_value astate )
+            apply_choice bool_value astate attribute )
     | _ ->
         astate