[infer][java] Simplify the abstract domain for the annotation reachability checker

Summary: It seems that we were not really using the `Bottom` part of the domain as a pair of (empty call map, empty tracking var map) was already acting as bottom.

Reviewed By: sblackshear

Differential Revision: D4759757

fbshipit-source-id: 53dedfe

infer/src/checkers/annotationReachability.ml

@@ -47,53 +47,39 @@ let src_snk_pairs () =
 module Domain = struct
   module TrackingVar = AbstractDomain.FiniteSet (Var.Set)
   module TrackingDomain = AbstractDomain.Pair (CallsDomain) (TrackingVar)
-  include AbstractDomain.BottomLifted (TrackingDomain)
+  include TrackingDomain
 
-  let add_call key call = function
+  let add_call key call ((call_map, vars) as astate) =
-    | Bottom -> Bottom
-    | NonBottom (call_map, vars) as astate ->
     let call_set =
       try CallsDomain.find key call_map
       with Not_found -> CallSiteSet.empty in
     let call_set' = CallSiteSet.add call call_set in
     if phys_equal call_set' call_set
     then astate
-        else NonBottom (CallsDomain.add key call_set' call_map, vars)
+    else (CallsDomain.add key call_set' call_map, vars)
 
-  let stop_tracking (_ : astate) = Bottom
+  let stop_tracking (_ : astate) =
+    (* The empty call map here prevents any subsequent calls to be added *)
+    (CallsDomain.empty, TrackingVar.empty)
 
-  let add_tracking_var var = function
+  let add_tracking_var var (calls, previous_vars) =
-    | Bottom -> Bottom
+    (calls, TrackingVar.add var previous_vars)
-    | NonBottom (calls, previous_vars) ->
-        NonBottom (calls, TrackingVar.add var previous_vars)
 
-  let remove_tracking_var var = function
+  let remove_tracking_var var (calls, previous_vars) =
-    | Bottom -> Bottom
+    (calls, TrackingVar.remove var previous_vars)
-    | NonBottom (calls, previous_vars) ->
-        NonBottom (calls, TrackingVar.remove var previous_vars)
 
-  let is_tracked_var var = function
+  let is_tracked_var var (_, vars) =
-    | Bottom -> false
-    | NonBottom (_, vars) ->
     TrackingVar.mem var vars
 end
 
 module Summary = Summary.Make (struct
-    type summary = Domain.astate
+    type summary = CallsDomain.astate
 
-    let call_summary_of_astate = function
+    let update_payload call_map payload =
-      | Domain.Bottom -> assert false
+      { payload with Specs.calls = Some call_map }
-      | Domain.NonBottom (call_map, _) ->
-          call_map
-
-    let update_payload astate payload =
-      let calls = Some (call_summary_of_astate astate) in
-      { payload with Specs.calls; }
 
     let read_from_payload payload =
-      match payload.Specs.calls with
+      payload.Specs.calls
-      | Some call_summary -> Some (Domain.NonBottom (call_summary, Domain.TrackingVar.empty))
-      | None -> None
   end)
 
 (* Warning name when a performance critical method directly or indirectly
@@ -283,10 +269,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     then method_has_ignore_allocation_annot tenv pname
     else false
 
-  let add_call call_map tenv callee_pname caller_pname call_site astate =
+  let merge_call_map
+      callee_call_map tenv callee_pname caller_pname call_site ((call_map, _) as astate) =
     let add_call_for_annot annot _ astate =
       let calls =
-        try Annot.Map.find annot call_map
+        try Annot.Map.find annot callee_call_map
         with Not_found -> CallSiteSet.empty in
       if (not (CallSiteSet.is_empty calls) || method_has_annot annot tenv callee_pname) &&
          (not (method_is_sanitizer annot tenv caller_pname))
@@ -294,12 +281,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         Domain.add_call annot call_site astate
       else
         astate in
-    match astate with
+    (* for each annotation type T in domain(astate), check if method calls
-    | Domain.Bottom -> astate
+       something annotated with T *)
-    | Domain.NonBottom (map, _) ->
+    Annot.Map.fold add_call_for_annot call_map astate
-        (* for each annotation type T in domain(astate), check if method calls something annotated
-           with T *)
-        Annot.Map.fold add_call_for_annot map astate
 
   let exec_instr astate { ProcData.pdesc; tenv; } _ = function
     | Sil.Call (Some (id, _), Const (Cfun callee_pname), _, _, _)
@@ -311,12 +295,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         begin
           (* Runs the analysis of callee_pname if not already analyzed *)
           match Summary.read_summary pdesc callee_pname with
-          | Some Domain.NonBottom (call_map, _) ->
+          | Some call_map ->
-              add_call call_map tenv callee_pname caller_pname call_site astate
+              merge_call_map call_map tenv callee_pname caller_pname call_site astate
           | None ->
-              add_call Annot.Map.empty tenv callee_pname caller_pname call_site astate
+              merge_call_map Annot.Map.empty tenv callee_pname caller_pname call_site astate
-          | Some Domain.Bottom ->
-              astate
         end
     | Sil.Load (id, exp, _, _)
       when is_tracking_exp astate exp ->
@@ -395,16 +377,17 @@ module Interprocedural = struct
               CallsDomain.add snk_annot CallSiteSet.empty astate_acc)
           ~init:CallsDomain.empty
           (src_snk_pairs ()) in
-      Domain.NonBottom
       (init_map, Domain.TrackingVar.empty) in
+    let compute_post proc_data =
+      Option.map ~f:fst (Analyzer.compute_post ~initial proc_data) in
     begin
       match compute_and_store_post
-              ~compute_post:(Analyzer.compute_post ~initial)
+              ~compute_post:compute_post
               ~make_extras:ProcData.make_empty_extras
               proc_data with
-      | Some Domain.NonBottom (call_map, _) ->
+      | Some call_map ->
           List.iter ~f:(report_src_snk_paths call_map) (src_snk_pairs ())
-      | Some Domain.Bottom | None ->
+      | None ->
           ()
     end;
     Specs.get_summary_unsafe "AnnotationReachability.checker" proc_name

infer/tests/codetoanalyze/java/checkers/NoAllocationExample.java

@@ -75,4 +75,15 @@ public class NoAllocationExample {
     }
   }
 
+  native boolean anotherRareCase();
+
+  @NoAllocation
+  void nestedUnlikely() {
+    if (Branch.unlikely(rareCase())) {
+      if (!Branch.unlikely(anotherRareCase())) {
+        allocates();
+      }
+    }
+  }
+
 }