diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index a50053d80..f8ddbfe28 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -9,10 +9,17 @@ open! IStd module F = Format module L = Logging -module MF = MarkupFormatter let debug fmt = F.kasprintf L.d_strln fmt +let is_java_static pname = + match pname with + | Typ.Procname.Java java_pname -> + Typ.Procname.Java.is_static java_pname + | _ -> + false + + module Summary = Summary.Make (struct type payload = StarvationDomain.summary @@ -23,6 +30,16 @@ module Summary = Summary.Make (struct let read_payload (summary: Specs.summary) = summary.payload.starvation end) +(* using an indentifier for a class object, create an access path representing that lock; + this is for synchronizing on class objects only *) +let lock_of_class class_id = + let ident = Ident.create_normal class_id 0 in + let type_name = Typ.Name.Java.from_string "java.lang.Class" in + let typ = Typ.mk (Typ.Tstruct type_name) in + let typ' = Typ.mk (Typ.Tptr (typ, Typ.Pk_pointer)) in + AccessPath.of_id ident typ' + + module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = StarvationDomain @@ -42,6 +59,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> (* ignore paths on local or logical variables *) None ) + | (HilExp.Constant Const.Cclass class_id) :: _ -> + (* this is a synchronized/lock(CLASSNAME.class) construct *) + Some (lock_of_class class_id) | _ -> None in @@ -164,17 +184,22 @@ let report_deadlocks get_proc_desc tenv pdesc summary = let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = + let pname = Procdesc.get_proc_name proc_desc in let formals = FormalMap.make proc_desc in let proc_data = ProcData.make proc_desc tenv formals in let initial = if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.empty else - let attrs = Procdesc.get_attributes proc_desc in - List.hd attrs.ProcAttributes.formals - |> Option.value_map ~default:StarvationDomain.empty ~f:(fun (name, typ) -> - let pvar = Pvar.mk name (Procdesc.get_proc_name proc_desc) in - let path = (AccessPath.base_of_pvar pvar typ, []) in - StarvationDomain.acquire path StarvationDomain.empty (Procdesc.get_loc proc_desc) ) + let loc = Procdesc.get_loc proc_desc in + let lock = + if is_java_static pname then + (* this is crafted so as to match synchronized(CLASSNAME.class) constructs *) + get_class_of_pname pname + |> Option.map ~f:(fun tn -> Typ.Name.name tn |> Ident.string_to_name |> lock_of_class) + else FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) + in + Option.value_map lock ~default:StarvationDomain.empty ~f:(fun path -> + StarvationDomain.acquire path StarvationDomain.empty loc ) in match Analyzer.compute_post proc_data ~initial with | None -> diff --git a/infer/tests/codetoanalyze/java/starvation/StaticLock.java b/infer/tests/codetoanalyze/java/starvation/StaticLock.java new file mode 100644 index 000000000..ec09ed221 --- /dev/null +++ b/infer/tests/codetoanalyze/java/starvation/StaticLock.java @@ -0,0 +1,33 @@ +/* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +class StaticLock { + static synchronized void static_synced() {} + + void lock_same_class_one_way_ok() { + synchronized(StaticLock.class) { + static_synced(); + } + } + + static synchronized void lock_same_class_another_way_ok() { + synchronized(StaticLock.class) { + } + } + + void lock_other_class_one_way_bad() { + synchronized(Object.class) { + synchronized(this) {} + } + } + + synchronized void lock_other_class_another_way_bad() { + static_synced(); + } +} diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index 0603f66fe..23c5f4cc6 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -1,3 +1,4 @@ codetoanalyze/java/starvation/Interclass.java, void Interclass.interclass1_bad(InterclassA), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class Interclass*,Method call: void InterclassA.interclass1_bad(),Lock acquisition: locks this in class InterclassA*,[Trace 2] Lock acquisition: locks this in class InterclassA*,Method call: void Interclass.interclass2_bad(),Lock acquisition: locks this in class Interclass*] codetoanalyze/java/starvation/Interproc.java, void Interproc.interproc1_bad(InterprocA), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class Interproc*,Method call: void Interproc.interproc2_bad(InterprocA),Lock acquisition: locks b in class InterprocA*,[Trace 2] Lock acquisition: locks this in class InterprocA*,Method call: void InterprocA.interproc2_bad(Interproc),Lock acquisition: locks d in class Interproc*] codetoanalyze/java/starvation/Intraproc.java, void IntraprocA.intra_bad(Intraproc), 0, STARVATION, ERROR, [[Trace 1] Method start: void IntraprocA.intra_bad(Intraproc),Lock acquisition: locks this in class IntraprocA*,Lock acquisition: locks o in class Intraproc*,[Trace 2] Method start: void Intraproc.intra_bad(IntraprocA),Lock acquisition: locks this in class Intraproc*,Lock acquisition: locks o in class IntraprocA*] +codetoanalyze/java/starvation/StaticLock.java, void StaticLock.lock_other_class_one_way_bad(), 0, STARVATION, ERROR, [[Trace 1] Method start: void StaticLock.lock_other_class_one_way_bad(),Lock acquisition: locks java.lang.Object$0 in class java.lang.Class*,Lock acquisition: locks this in class StaticLock*,[Trace 2] Lock acquisition: locks this in class StaticLock*,Method call: void StaticLock.static_synced(),Lock acquisition: locks StaticLock$0 in class java.lang.Class*]