[infer][java] simplify the domain logic of the annotation reachability checker

Summary: The analysis logic was split between the treatment of the instructions and the definition of the domain, making the code more complicated that it should. This diff moves more of the logic into the domain definition and change to variable names to more descriptive ones

Reviewed By: sblackshear

Differential Revision: D4936414

fbshipit-source-id: ff59de7

infer/src/backend/specs.ml

@@ -324,7 +324,7 @@ type payload =
   {
     preposts : NormSpec.t list option; (** list of specs *)
     typestate : unit TypeState.t option; (** final typestate *)
-    calls: AnnotReachabilityDomain.astate option;
+    annot_map : AnnotReachabilityDomain.astate option;
     crashcontext_frame: Stacktree_t.stacktree option;
     (** Proc location and blame_range info for crashcontext analysis *)
     quandary : QuandarySummary.t option;
@@ -444,7 +444,7 @@ let pp_summary_no_stats_specs fmt summary =
 
 let pp_payload pe fmt
     { preposts; typestate; crashcontext_frame;
-      quandary; siof; threadsafety; buffer_overrun; calls } =
+      quandary; siof; threadsafety; buffer_overrun; annot_map } =
   let pp_opt prefix pp fmt = function
     | Some x -> F.fprintf fmt "%s: %a\n" prefix pp x
     | None -> () in
@@ -456,7 +456,7 @@ let pp_payload pe fmt
     (pp_opt "Siof" SiofDomain.pp) siof
     (pp_opt "ThreadSafety" ThreadSafetyDomain.pp_summary) threadsafety
     (pp_opt "BufferOverrun" BufferOverrunDomain.Summary.pp) buffer_overrun
-    (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp) calls
+    (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp) annot_map
 
 
 let pp_summary_text fmt summary =
@@ -709,7 +709,7 @@ let empty_payload =
   {
     preposts = None;
     typestate = None;
-    calls = None;
+    annot_map = None;
     crashcontext_frame = None;
     quandary = None;
     siof = None;

infer/src/backend/specs.mli

@@ -134,7 +134,7 @@ type payload =
   {
     preposts : NormSpec.t list option; (** list of specs *)
     typestate : unit TypeState.t option; (** final typestate *)
-    calls: AnnotReachabilityDomain.astate option; (** list of calls of the form (call, loc) *)
+    annot_map: AnnotReachabilityDomain.astate option; (** list of calls of the form (call, loc) *)
     crashcontext_frame: Stacktree_j.stacktree option;
     (** Procedure location and blame_range info for crashcontext analysis *)
     quandary : QuandarySummary.t option;

infer/src/checkers/annotationReachability.ml

@@ -18,7 +18,7 @@ let dummy_constructor_annot = "__infer_is_constructor"
 let annotation_of_str annot_str =
   { Annot.class_name = annot_str; parameters = []; }
 
-let src_snk_pairs () =
+let src_snk_pairs =
   (* parse user-defined specs from .inferconfig *)
   let parse_user_defined_specs = function
     | `List user_specs ->
@@ -43,40 +43,52 @@ let src_snk_pairs () =
 
 module Domain = struct
   module TrackingVar = AbstractDomain.FiniteSet (Var.Set)
-  module TrackingDomain = AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingVar)
+  module TrackingDomain = AbstractDomain.BottomLifted (TrackingVar)
-  include TrackingDomain
+  include AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingDomain)
-
+
-  let add_call key call ((call_map, vars) as astate) =
+  let add_call_site annot call_site ((annot_map, previous_vstate) as astate) =
-    let call_set =
+    match previous_vstate with
-      try AnnotReachabilityDomain.find key call_map
+    | TrackingDomain.Bottom -> astate
-      with Not_found -> CallSite.SetDomain.empty in
+    | TrackingDomain.NonBottom _ ->
-    let call_set' = CallSite.SetDomain.add call call_set in
+        let call_set =
-    if phys_equal call_set' call_set
+          try AnnotReachabilityDomain.find annot annot_map
-    then astate
+          with Not_found -> CallSite.SetDomain.empty in
-    else (AnnotReachabilityDomain.add key call_set' call_map, vars)
+        let call_set' = CallSite.SetDomain.add call_site call_set in
-
+        if phys_equal call_set' call_set
-  let stop_tracking (_ : astate) =
+        then astate
-    (* The empty call map here prevents any subsequent calls to be added *)
+        else (AnnotReachabilityDomain.add annot call_set' annot_map, previous_vstate)
-    (AnnotReachabilityDomain.empty, TrackingVar.empty)
+
-
+  let stop_tracking (annot_map, _ : astate) =
-  let add_tracking_var var (calls, previous_vars) =
+    (annot_map, TrackingDomain.Bottom)
-    (calls, TrackingVar.add var previous_vars)
+
-
+  let add_tracking_var var ((annot_map, previous_vstate) as astate) =
-  let remove_tracking_var var (calls, previous_vars) =
+    match previous_vstate with
-    (calls, TrackingVar.remove var previous_vars)
+    | TrackingDomain.Bottom -> astate
-
+    | TrackingDomain.NonBottom vars ->
-  let is_tracked_var var (_, vars) =
+        (annot_map, TrackingDomain.NonBottom (TrackingVar.add var vars))
-    TrackingVar.mem var vars
+
+  let remove_tracking_var var ((annot_map, previous_vstate) as astate) =
+    match previous_vstate with
+    | TrackingDomain.Bottom -> astate
+    | TrackingDomain.NonBottom vars ->
+        (annot_map, TrackingDomain.NonBottom (TrackingVar.remove var vars))
+
+  let is_tracked_var var (_, vstate) =
+    match vstate with
+    | TrackingDomain.Bottom -> false
+    | TrackingDomain.NonBottom vars ->
+        TrackingVar.mem var vars
+
 end
 
 module Summary = Summary.Make (struct
     type payload = AnnotReachabilityDomain.astate
 
-    let update_payload call_map (summary : Specs.summary) =
+    let update_payload annot_map (summary : Specs.summary) =
-      { summary with payload = { summary.payload with calls = Some call_map }}
+      { summary with payload = { summary.payload with annot_map = Some annot_map }}
 
     let read_payload (summary : Specs.summary) =
-      summary.payload.calls
+      summary.payload.annot_map
   end)
 
 (* Warning name when a performance critical method directly or indirectly
@@ -139,10 +151,10 @@ let method_overrides_annot annot tenv pname =
 
 let lookup_annotation_calls caller_pdesc annot pname : CallSite.SetDomain.t =
   match Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc pname with
-  | Some { Specs.payload = { Specs.calls = Some call_map; }; } ->
+  | Some { Specs.payload = { Specs.annot_map = Some annot_map; }; } ->
       begin
         try
-          Annot.Map.find annot call_map
+          Annot.Map.find annot annot_map
         with Not_found ->
           CallSite.SetDomain.empty
       end
@@ -210,7 +222,7 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site ca
       let callee_pname_str = string_of_pname callee_pname in
       let new_stack_str = stack_str ^ callee_pname_str ^ " -> " in
       let new_trace = update_trace call_loc trace |> update_trace callee_def_loc in
-      let unseen_pnames, updated_visited =
+      let unseen_callees, visited_callees =
         CallSite.SetDomain.fold
           (fun call_site ((unseen, visited) as accu) ->
              let p = CallSite.pname call_site in
@@ -219,7 +231,7 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site ca
              else ((p, loc) :: unseen, Typ.Procname.Set.add p visited))
           next_calls
           ([], visited_pnames) in
-      List.iter ~f:(loop fst_call_loc updated_visited (new_trace, new_stack_str)) unseen_pnames in
+      List.iter ~f:(loop fst_call_loc visited_callees (new_trace, new_stack_str)) unseen_callees in
   CallSite.SetDomain.iter
     (fun fst_call_site ->
        let fst_callee_pname = CallSite.pname fst_call_site in
@@ -267,21 +279,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     then method_has_ignore_allocation_annot tenv pname
     else false
 
-  let merge_call_map
+  let check_call tenv callee_pname caller_pname call_site astate =
-      callee_call_map tenv callee_pname caller_pname call_site ((call_map, _) as astate) =
+    List.fold
-    let add_call_for_annot annot _ astate =
+      ~init:astate
-      let calls =
+      ~f:(fun astate (_, annot) ->
-        try Annot.Map.find annot callee_call_map
+          if method_has_annot annot tenv callee_pname &&
-        with Not_found -> CallSite.SetDomain.empty in
+             not (method_is_sanitizer annot tenv caller_pname)
-      if (not (CallSite.SetDomain.is_empty calls) || method_has_annot annot tenv callee_pname) &&
+          then Domain.add_call_site annot call_site astate
-         (not (method_is_sanitizer annot tenv caller_pname))
+          else astate)
-      then
+      src_snk_pairs
-        Domain.add_call annot call_site astate
+
-      else
+  let merge_callee_map call_site pdesc callee_pname astate =
-        astate in
+    match Summary.read_summary pdesc callee_pname with
-    (* for each annotation type T in domain(astate), check if method calls
+    | None -> astate
-       something annotated with T *)
+    | Some callee_call_map ->
-    Annot.Map.fold add_call_for_annot call_map astate
+        Annot.Map.fold
+          (fun annot calls astate ->
+             if CallSite.SetDomain.is_empty calls
+             then astate
+             else Domain.add_call_site annot call_site astate)
+          callee_call_map
+          astate
 
   let exec_instr astate { ProcData.pdesc; tenv; } _ = function
     | Sil.Call (Some (id, _), Const (Cfun callee_pname), _, _, _)
@@ -290,14 +308,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) ->
         let caller_pname = Procdesc.get_proc_name pdesc in
         let call_site = CallSite.make callee_pname call_loc in
-        begin
+        check_call tenv callee_pname caller_pname call_site astate
-          (* Runs the analysis of callee_pname if not already analyzed *)
+        |> merge_callee_map call_site pdesc callee_pname
-          match Summary.read_summary pdesc callee_pname with
-          | Some call_map ->
-              merge_call_map call_map tenv callee_pname caller_pname call_site astate
-          | None ->
-              merge_call_map Annot.Map.empty tenv callee_pname caller_pname call_site astate
-        end
     | Sil.Load (id, exp, _, _)
       when is_tracking_exp astate exp ->
         Domain.add_tracking_var (Var.of_id id) astate
@@ -329,7 +341,6 @@ module Interprocedural = struct
   let check_and_report ({ Callbacks.proc_desc; tenv; summary } as proc_data) : Specs.summary =
     let proc_name = Procdesc.get_proc_name proc_desc in
     let loc = Procdesc.get_loc proc_desc in
-    let expensive = is_expensive tenv proc_name in
     (* TODO: generalize so we can check subtyping on arbitrary annotations *)
     let check_expensive_subtyping_rules overridden_pname =
       if not (method_is_expensive tenv overridden_pname) then
@@ -344,14 +355,10 @@ module Interprocedural = struct
             (expensive_overrides_unexpensive, Localise.verbatim_desc description) in
         Reporting.log_error_from_summary summary ~loc exn in
 
-    if expensive then
+    if is_expensive tenv proc_name then
       PatternMatch.override_iter check_expensive_subtyping_rules tenv proc_name;
 
-    let report_src_snk_paths call_map (src_annot_list, (snk_annot: Annot.t)) =
+    let report_src_snk_paths annot_map (src_annot_list, (snk_annot: Annot.t)) =
-      let extract_calls_with_annot annot call_map =
-        try
-          Annot.Map.find annot call_map
-        with Not_found -> CallSite.SetDomain.empty in
       let report_src_snk_path (calls : CallSite.SetDomain.t) (src_annot: Annot.t) =
         if method_overrides_annot src_annot tenv proc_name
         then
@@ -364,18 +371,13 @@ module Interprocedural = struct
             f_report
             (CallSite.make proc_name loc)
             calls in
-      let calls = extract_calls_with_annot snk_annot call_map in
+      try
-      if not (CallSite.SetDomain.is_empty calls)
+        let sink_map = Annot.Map.find snk_annot annot_map in
-      then List.iter ~f:(report_src_snk_path calls) src_annot_list in
+        List.iter ~f:(report_src_snk_path sink_map) src_annot_list
+      with Not_found -> () in
 
     let initial =
-      let init_map =
+      (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) in
-        List.fold
-          ~f:(fun astate_acc (_, snk_annot) ->
-              AnnotReachabilityDomain.add snk_annot CallSite.SetDomain.empty astate_acc)
-          ~init:AnnotReachabilityDomain.empty
-          (src_snk_pairs ()) in
-      (init_map, Domain.TrackingVar.empty) in
     let compute_post proc_data =
       Option.map ~f:fst (Analyzer.compute_post ~initial proc_data) in
     let updated_summary : Specs.summary =
@@ -384,9 +386,9 @@ module Interprocedural = struct
         ~make_extras:ProcData.make_empty_extras
         proc_data in
     begin
-      match updated_summary.payload.calls with
+      match updated_summary.payload.annot_map with
-      | Some call_map ->
+      | Some annot_map ->
-          List.iter ~f:(report_src_snk_paths call_map) (src_snk_pairs ())
+          List.iter ~f:(report_src_snk_paths annot_map) src_snk_pairs
       | None ->
           ()
     end;