[starvation] fix handling of static synchronized methods and static locks

Reviewed By: sblackshear

Differential Revision: D7427365

fbshipit-source-id: f23795f

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

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();
+  }
+}

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*]