refactoring annotation reachability checker to allow custom src/sink annotations

Reviewed By: jeremydubreil

Differential Revision: D3295582

fbshipit-source-id: 41884ea

facebook-clang-plugins

@@ -1 +1 @@
-Subproject commit ba3d4b9066cc57c413581d2efe909add94b4366f
+Subproject commit f5c1bd411f95ba797e0e0e5c15a562d91eb6a6c9

infer/src/IR/Sil.re

@@ -107,6 +107,11 @@ let item_annotation_to_string ann => {
 let pp_method_annotation s fmt (ia, ial) =>
   F.fprintf fmt "%a %s(%a)" pp_item_annotation ia s (pp_seq pp_item_annotation) ial;
 
+let module AnnotMap = PrettyPrintable.MakePPMap {
+    type t = annotation;
+    let compare = annotation_compare;
+    let pp_key = pp_annotation;
+};
 
 /** Return the value of the FA_sentinel attribute in [attr_list] if it is found */
 let get_sentinel_func_attribute_value attr_list =>

infer/src/IR/Sil.rei

@@ -355,6 +355,8 @@ let module TypSet: Set.S with type elt = typ;
 let module TypMap: Map.S with type key = typ;
 
 
+let module AnnotMap : PrettyPrintable.PPMap with type key = annotation;
+
 /** Sets of expressions. */
 let module ExpSet: Set.S with type elt = exp;
 

infer/src/backend/specs.ml

@@ -307,12 +307,24 @@ type phase = FOOTPRINT | RE_EXECUTION
 
 type dependency_map_t = int Procname.Map.t
 
-type call = Procname.t * Location.t
+(* name of callee + location of the call *)
+type call_site = Procname.t * Location.t
 
-type call_summary = {
+let compare_call_site (pname1, loc1) (pname2, loc2) =
-  expensive_calls: call list;
+  let n = Procname.compare pname1 pname2 in
-  allocations: call list
+  if n <> 0
-}
+  then n
+  else Location.compare loc1 loc2
+
+let pp_call_site fmt (pname, loc) = F.fprintf fmt "%a at %a" Procname.pp pname Location.pp loc
+
+module CallSiteSet = PrettyPrintable.MakePPSet(struct
+    type t = call_site
+    let compare = compare_call_site
+    let pp_element = pp_call_site
+  end)
+
+type call_summary = CallSiteSet.t Sil.AnnotMap.t
 
 (** Payload: results of some analysis *)
 type payload =

infer/src/backend/specs.mli

@@ -118,13 +118,11 @@ type phase = FOOTPRINT | RE_EXECUTION
 type dependency_map_t = int Procname.Map.t
 
 (** Type for calls consiting in the name of the callee and the location of the call *)
-type call = Procname.t * Location.t
+type call_site = Procname.t * Location.t
 
-(** Collection of first step calls toward expensive call stacks or call stack allocating memory *)
+module CallSiteSet : PrettyPrintable.PPSet with type elt = call_site
-type call_summary = {
+
-  expensive_calls: call list;
+type call_summary = CallSiteSet.t Sil.AnnotMap.t
-  allocations: call list
-}
 
 (** Payload: results of some analysis *)
 type payload =

infer/src/checkers/annotationReachability.ml

@@ -12,38 +12,50 @@ open! Utils
 module F = Format
 module L = Logging
 
-let compare_call (pname1, loc1) (pname2, loc2) =
+module CallSiteSet = AbstractDomain.FiniteSet (Specs.CallSiteSet)
-  let n = Procname.compare pname1 pname2 in
+module CallsDomain = AbstractDomain.Map (Sil.AnnotMap) (CallSiteSet)
-  if n <> 0
+
-  then n
+let dummy_constructor_annot = "__infer_is_constructor"
-  else Location.compare loc1 loc2
+
-
+let annotation_of_str annot_str =
-let pp_call fmt (pname, loc) = F.fprintf fmt "%a at %a" Procname.pp pname Location.pp loc
+  { Sil.class_name = annot_str; parameters = []; }
-
+
-module CallSet = PrettyPrintable.MakePPSet(struct
+(* TODO: read custom source/sink pairs from user code here *)
-    type t = Specs.call
+let src_snk_pairs () =
-    let compare = compare_call
+  let specs =
-    let pp_element = pp_call
+    [
-  end)
+      ([Annotations.performance_critical], Annotations.expensive);
-
+      ([Annotations.no_allocation], dummy_constructor_annot);
-module CallSetDomain = AbstractDomain.FiniteSet(CallSet)
+    ] in
+  IList.map
+    (fun (src_annot_str_list, snk_annot_str) ->
+       IList.map annotation_of_str src_annot_str_list, annotation_of_str snk_annot_str)
+    specs
 
 module Domain = struct
-  module CallsDomain = AbstractDomain.Pair(CallSetDomain)(CallSetDomain)
   module TrackingVar = AbstractDomain.FiniteSet (Var.Set)
-  module TrackingDomain =
+  module TrackingDomain = AbstractDomain.Pair (CallsDomain) (TrackingVar)
-    AbstractDomain.Pair(CallsDomain)(TrackingVar)
   include AbstractDomain.BottomLifted (TrackingDomain)
 
-  let add_expensive call = function
+  let initial =
-    | Bottom -> Bottom
+    let init_map =
-    | NonBottom ((expensive_calls, allocations), vars) ->
+      IList.fold_left
-        NonBottom ((CallSetDomain.add call expensive_calls, allocations), vars)
+        (fun astate_acc (_, snk_annot) -> CallsDomain.add snk_annot CallSiteSet.empty astate_acc)
+        CallsDomain.initial
+        (src_snk_pairs ()) in
+    NonBottom
+      (init_map, TrackingVar.empty)
 
-  let add_allocation alloc = function
+  let add_call key call = function
     | Bottom -> Bottom
-    | NonBottom ((expensive_calls, allocations), vars) ->
+    | NonBottom (call_map, vars) as astate ->
-        NonBottom ((expensive_calls, CallSetDomain.add alloc allocations), vars)
+        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 call_set' == call_set
+        then astate
+        else NonBottom (CallsDomain.add key call_set' call_map, vars)
 
   let stop_tracking (_ : astate) = Bottom
 
@@ -61,7 +73,6 @@ module Domain = struct
     | Bottom -> false
     | NonBottom (_, vars) ->
         TrackingVar.mem var vars
-
 end
 
 module Summary = Summary.Make (struct
@@ -69,24 +80,17 @@ module Summary = Summary.Make (struct
 
     let call_summary_of_astate = function
       | Domain.Bottom -> assert false
-      | Domain.NonBottom ((astate_expensive, astate_allocations), _) ->
+      | Domain.NonBottom (call_map, _) ->
-          let expensive_calls = CallSet.elements astate_expensive in
+          call_map
-          let allocations = CallSet.elements astate_allocations in
-          { Specs.expensive_calls; allocations; }
 
     let update_payload astate payload =
-      let call_summary = call_summary_of_astate astate in
+      let calls = Some (call_summary_of_astate astate) in
-      { payload with Specs.calls = Some call_summary }
+      { payload with Specs.calls; }
 
     let read_from_payload payload =
       match payload.Specs.calls with
-      | Some call_summary ->
+      | Some call_summary -> Domain.NonBottom (call_summary, Domain.TrackingVar.empty)
-          Domain.NonBottom
-            ((CallSet.of_list call_summary.Specs.expensive_calls,
-              CallSet.of_list call_summary.Specs.allocations),
-             Domain.TrackingVar.initial)
       | None -> Domain.initial
-
   end)
 
 (* Warning name when a performance critical method directly or indirectly
@@ -104,6 +108,8 @@ let allocates_memory =
 let expensive_overrides_unexpensive =
   "CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED"
 
+let annotation_reachability_error = "CHECKERS_ANNOTATION_REACHABILITY_ERROR"
+
 let is_modeled_expensive =
   let matcher =
     lazy (Inferconfig.ModeledExpensiveMatcher.load_matcher Config.inferconfig_json) in
@@ -116,6 +122,19 @@ let is_modeled_expensive =
     | _ ->
         false
 
+let is_allocator tenv pname =
+  match pname with
+  | Procname.Java pname_java ->
+      let is_throwable () =
+        let class_name =
+          Typename.Java.from_string (Procname.java_get_class_name pname_java) in
+        PatternMatch.is_throwable tenv class_name in
+      Procname.is_constructor pname
+      && not (Builtin.is_registered pname)
+      && not (is_throwable ())
+  | _ ->
+      false
+
 let check_attributes check tenv pname =
   let check_class_attributes check tenv = function
     | Procname.Java java_pname ->
@@ -138,18 +157,6 @@ let check_attributes check tenv pname =
         check ret_annotation in
   check_class_attributes check tenv pname || check_method_attributes check pname
 
-let is_expensive tenv pname =
-  check_attributes Annotations.ia_is_expensive tenv pname
-
-
-let method_is_performance_critical tenv pname =
-  check_attributes Annotations.ia_is_performance_critical tenv pname
-
-
-let method_is_no_allocation tenv pname =
-  check_attributes Annotations.ia_is_no_allocation tenv pname
-
-
 let method_overrides is_annotated tenv pname =
   let overrides () =
     let found = ref false in
@@ -160,70 +167,28 @@ let method_overrides is_annotated tenv pname =
   is_annotated tenv pname ||
   overrides ()
 
-let method_overrides_performance_critical tenv pname =
+let method_has_annot annot tenv pname =
-  method_overrides method_is_performance_critical tenv pname
+  let has_annot ia = Annotations.ia_ends_with ia annot.Sil.class_name in
-
+  if Annotations.annot_ends_with annot dummy_constructor_annot
-let method_overrides_no_allocation tenv pname =
+  then is_allocator tenv pname
-  method_overrides method_is_no_allocation tenv pname
+  else if Annotations.annot_ends_with annot Annotations.expensive
-
+  then check_attributes has_annot tenv pname || is_modeled_expensive tenv pname
-let method_is_expensive tenv pname =
+  else check_attributes has_annot tenv pname
-  is_modeled_expensive tenv pname ||
-  check_attributes Annotations.ia_is_expensive tenv pname
-
-let lookup_call_summary pname =
-  match Specs.get_summary pname with
-  | None -> None
-  | Some summary -> summary.Specs.payload.Specs.calls
-
-let lookup_expensive_calls pname =
-  match lookup_call_summary pname with
-  | None -> []
-  | Some { Specs.expensive_calls } -> expensive_calls
-
-let lookup_allocations pname =
-  match lookup_call_summary pname with
-  | None -> []
-  | Some { Specs.allocations } -> allocations
-
-let method_calls_expensive tenv pname =
-  let calls_expensive () =
-    match lookup_call_summary pname with
-    | Some { Specs.expensive_calls } ->
-        expensive_calls <> []
-    | None -> false in
-  method_is_expensive tenv pname ||
-  calls_expensive ()
-
-let is_allocator tenv pname = match pname with
-  | Procname.Java pname_java ->
-      let is_throwable () =
-        let class_name =
-          Typename.Java.from_string (Procname.java_get_class_name pname_java) in
-        PatternMatch.is_throwable tenv class_name in
-      Procname.is_constructor pname
-      && not (Builtin.is_registered pname)
-      && not (is_throwable ())
-  | _ ->
-      false
 
-let method_allocates tenv pname =
+let method_overrides_annot annot tenv pname =
-  let annotated_ignore_allocation =
+  method_overrides (method_has_annot annot) tenv pname
-    check_attributes Annotations.ia_is_ignore_allocations tenv pname in
-  let allocates () =
-    match lookup_call_summary pname with
-    | Some { Specs.allocations } ->
-        allocations <> []
-    | None -> false in
-  not annotated_ignore_allocation
-  && (is_allocator tenv pname || allocates ())
 
-let lookup_location pname =
+let lookup_annotation_calls annot pname =
   match Specs.get_summary pname with
-  | None -> Location.dummy
+  | Some { Specs.payload = { Specs.calls = Some call_map; }; } ->
-  | Some summary -> summary.Specs.attributes.ProcAttributes.loc
+      begin
-
+        try
-let string_of_pname =
+          Sil.AnnotMap.find annot call_map
-  Procname.to_simplified_string ~withclass:true
+          |> Specs.CallSiteSet.elements
+        with Not_found ->
+          []
+      end
+  | _ -> []
 
 let update_trace loc trace =
   if Location.equal loc Location.dummy then trace
@@ -236,21 +201,8 @@ let update_trace loc trace =
     } in
     trace_elem :: trace
 
-let report_expensive_call_stack pname loc trace stack_str expensive_pname call_loc =
+let string_of_pname =
-  let final_trace = IList.rev (update_trace call_loc trace) in
+  Procname.to_simplified_string ~withclass:true
-  let exp_pname_str = string_of_pname expensive_pname in
-  let description =
-    Printf.sprintf
-      "Method `%s` annotated with `@%s` calls `%s%s` where `%s` is annotated with `@%s`"
-      (Procname.to_simplified_string pname)
-      Annotations.performance_critical
-      stack_str
-      exp_pname_str
-      exp_pname_str
-      Annotations.expensive in
-  let exn =
-    Exceptions.Checkers (calls_expensive_method, Localise.verbatim_desc description) in
-  Reporting.log_error pname ~loc: (Some loc) ~ltr: (Some final_trace) exn
 
 let report_allocation_stack pname fst_call_loc trace stack_str constructor_pname call_loc =
   let final_trace = IList.rev (update_trace call_loc trace) in
@@ -267,7 +219,35 @@ let report_allocation_stack pname fst_call_loc trace stack_str constructor_pname
     Exceptions.Checkers (allocates_memory, Localise.verbatim_desc description) in
   Reporting.log_error pname ~loc: (Some fst_call_loc) ~ltr: (Some final_trace) exn
 
+let report_annotation_stack src_annot snk_annot src_pname loc trace stack_str snk_pname call_loc =
+  if src_annot = Annotations.no_allocation
+  then report_allocation_stack src_pname loc trace stack_str snk_pname call_loc
+  else
+    let final_trace = IList.rev (update_trace call_loc trace) in
+    let exp_pname_str = string_of_pname snk_pname in
+    let description =
+      Printf.sprintf
+        "Method `%s` annotated with `@%s` calls `%s%s` where `%s` is annotated with `@%s`"
+        (Procname.to_simplified_string src_pname)
+        src_annot
+        stack_str
+        exp_pname_str
+        exp_pname_str
+        snk_annot in
+    let msg =
+      if src_annot = Annotations.performance_critical
+      then calls_expensive_method
+      else annotation_reachability_error in
+    let exn =
+      Exceptions.Checkers (msg, Localise.verbatim_desc description) in
+    Reporting.log_error src_pname ~loc: (Some loc) ~ltr: (Some final_trace) exn
+
 let report_call_stack end_of_stack lookup_next_calls report pname loc calls =
+  (* TODO: stop using this; we can use the call site instead *)
+  let lookup_location pname =
+    match Specs.get_summary pname with
+    | None -> Location.dummy
+    | Some summary -> summary.Specs.attributes.ProcAttributes.loc in
   let rec loop fst_call_loc visited_pnames (trace, stack_str) (callee_pname, call_loc) =
     if end_of_stack callee_pname then
       report pname fst_call_loc trace stack_str callee_pname call_loc
@@ -290,16 +270,6 @@ let report_call_stack end_of_stack lookup_next_calls report pname loc calls =
        loop fst_call_loc Procname.Set.empty (start_trace, "") (fst_callee_pname, fst_call_loc))
     calls
 
-let report_expensive_calls tenv pname loc calls =
-  report_call_stack
-    (method_is_expensive tenv) lookup_expensive_calls
-    report_expensive_call_stack pname loc calls
-
-let report_allocations pname loc calls =
-  report_call_stack
-    Procname.is_constructor lookup_allocations
-    report_allocation_stack pname loc calls
-
 module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
@@ -331,23 +301,51 @@ module TransferFunctions = struct
     | _ ->
         false
 
+  let method_has_ignore_allocation_annot tenv pname =
+    check_attributes Annotations.ia_is_ignore_allocations tenv pname
+
+  (* TODO: generalize this to allow sanitizers for other annotation types, store it in [extras] so
+     we can compute it just once *)
+  let method_is_sanitizer annot tenv pname =
+    if annot.Sil.class_name = dummy_constructor_annot
+    then method_has_ignore_allocation_annot tenv pname
+    else false
+
+  let add_call call_map tenv callee_pname caller_pname call_site astate =
+    let add_call_for_annot annot _ astate =
+      let calls =
+        try Sil.AnnotMap.find annot call_map
+        with Not_found -> Specs.CallSiteSet.empty in
+      if (not (Specs.CallSiteSet.is_empty calls) || method_has_annot annot tenv callee_pname) &&
+         (not (method_is_sanitizer annot tenv caller_pname))
+      then
+        Domain.add_call annot call_site astate
+      else
+        astate in
+    match astate with
+    | Domain.Bottom -> astate
+    | Domain.NonBottom (map, _) ->
+        (* for each annotation type T in domain(astate), check if method calls something annotated
+           with T *)
+        Sil.AnnotMap.fold add_call_for_annot map astate
+
   let exec_instr astate { ProcData.pdesc; tenv; } = function
     | Sil.Call ([id], Const (Cfun callee_pname), _, _, _)
       when is_unlikely callee_pname ->
         Domain.add_tracking_var (Var.of_id id) astate
     | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) ->
-        (* Run the analysis of callee_pname if not already analyzed *)
+        let caller_pname = Cfg.Procdesc.get_proc_name pdesc in
-        ignore (Summary.read_summary pdesc callee_pname);
+        let call_site = callee_pname, call_loc in
-        let add_expensive_calls astate =
+        begin
-          if method_calls_expensive tenv callee_pname
+          (* Runs the analysis of callee_pname if not already analyzed *)
-          then Domain.add_expensive (callee_pname, call_loc) astate
+          match Summary.read_summary pdesc callee_pname with
-          else astate in
+          | Some Domain.NonBottom (call_map, _) ->
-        let add_allocations astate =
+              add_call call_map tenv callee_pname caller_pname call_site astate
-          if method_allocates tenv callee_pname
+          | None ->
-          then Domain.add_allocation (callee_pname, call_loc) astate
+              add_call Sil.AnnotMap.empty tenv callee_pname caller_pname call_site astate
-          else astate in
+          | Some Domain.Bottom ->
-        add_expensive_calls astate
+              astate
-        |> add_allocations
+        end
     | Sil.Letderef (id, exp, _, _)
       when is_tracking_exp astate exp ->
         Domain.add_tracking_var (Var.of_id id) astate
@@ -363,7 +361,6 @@ module TransferFunctions = struct
         failwith "Expecting a singleton for the return value"
     | _ ->
         astate
-
 end
 
 module Analyzer =
@@ -376,14 +373,16 @@ module Analyzer =
 module Interprocedural = struct
   include Analyzer.Interprocedural(Summary)
 
+  let is_expensive tenv pname =
+    check_attributes Annotations.ia_is_expensive tenv pname
+
+  let method_is_expensive tenv pname =
+    is_modeled_expensive tenv pname || is_expensive tenv pname
+
   let check_and_report ({ Callbacks.proc_desc; proc_name; tenv; } as proc_data) =
     let loc = Cfg.Procdesc.get_loc proc_desc in
-    let expensive = is_expensive tenv proc_name
+    let expensive = is_expensive tenv proc_name in
-    and performance_critical =
+    (* TODO: generalize so we can check subtyping on arbitrary annotations *)
-      method_overrides_performance_critical tenv proc_name
-    and no_allocation =
-      method_overrides_no_allocation tenv proc_name in
-
     let check_expensive_subtyping_rules overridden_pname =
       if not (method_is_expensive tenv overridden_pname) then
         let description =
@@ -401,17 +400,31 @@ module Interprocedural = struct
       PatternMatch.proc_iter_overridden_methods
         check_expensive_subtyping_rules tenv proc_name;
 
-    match checker proc_data ProcData.empty_extras with
+    let report_src_snk_paths call_map (src_annot_list, snk_annot) =
-    | Some astate ->
+      let extract_calls_with_annot annot call_map =
-        begin
+        try
-          match astate with
+          Sil.AnnotMap.find annot call_map
-          | Domain.Bottom -> ()
+          |> Specs.CallSiteSet.elements
-          | Domain.NonBottom ((expensive_calls, allocations), _) ->
+        with Not_found -> [] in
-              if performance_critical then
+      let report_src_snk_path calls src_annot =
-                report_expensive_calls tenv proc_name loc (CallSet.elements expensive_calls);
+        if method_overrides_annot src_annot tenv proc_name
-              if no_allocation then
+        then
-                report_allocations proc_name loc (CallSet.elements allocations)
+          let f_report =
-        end
+            report_annotation_stack src_annot.Sil.class_name snk_annot.Sil.class_name in
-    | None -> ()
+          report_call_stack
+            (method_has_annot snk_annot tenv)
+            (lookup_annotation_calls snk_annot)
+            f_report
+            proc_name
+            loc
+            calls in
+      let calls = extract_calls_with_annot snk_annot call_map in
+      if not (IList.length calls = 0)
+      then IList.iter (report_src_snk_path calls) src_annot_list in
 
+    match checker proc_data ProcData.empty_extras with
+    | Some Domain.NonBottom (call_map, _) ->
+        IList.iter (report_src_snk_paths call_map) (src_snk_pairs ())
+    | Some Domain.Bottom | None ->
+        ()
 end

infer/src/checkers/annotations.ml

@@ -129,6 +129,8 @@ let expensive = "Expensive"
 let performance_critical = "PerformanceCritical"
 let no_allocation = "NoAllocation"
 let ignore_allocations = "IgnoreAllocations"
+
+
 let suppress_warnings = "SuppressWarnings"
 let privacy_source = "PrivacySource"
 let privacy_sink = "PrivacySink"

infer/src/checkers/annotations.mli

@@ -64,11 +64,11 @@ val nullable : string
 (** Return true if [annot] ends with [ann_name] *)
 val annot_ends_with : Sil.annotation -> string -> bool
 
-val ia_contains : Sil.item_annotation -> string -> bool
-
 (** Check if there is an annotation in [ia] which ends with the given name *)
 val ia_ends_with : Sil.item_annotation -> string -> bool
 
+val ia_contains : Sil.item_annotation -> string -> bool
+
 val ia_has_annotation_with : Sil.item_annotation -> (Sil.annotation -> bool) -> bool
 
 val ia_get_strict : Sil.item_annotation -> Sil.annotation option