[class loading] initial commit

Summary: First version of an analyzer collecting classes transitively touched.

Reviewed By: mbouaziz

Differential Revision: D10448025

fbshipit-source-id: 0ddfefd46

infer/man/man1/infer-analyze.txt

@@ -55,6 +55,13 @@ OPTIONS
            Activates: Enable --check-nullable and disable all other checkers
            (Conversely: --no-check-nullable-only)
 
+       --classloads
+           Activates: class loading analysis (Conversely: --no-classloads)
+
+       --classloads-only
+           Activates: Enable --classloads and disable all other checkers
+           (Conversely: --no-classloads-only)
+
        --continue
            Activates: Continue the capture for the reactive analysis,
            increasing the changed files/procedures. (If a procedure was

infer/man/man1/infer-full.txt

@@ -147,6 +147,14 @@ OPTIONS
            Specify a file containing the AST of the program, in biniou format       
     See also infer-capture(1).
 
+       --classloads
+           Activates: class loading analysis (Conversely: --no-classloads)       
+    See also infer-analyze(1).
+
+       --classloads-only
+           Activates: Enable --classloads and disable all other checkers
+           (Conversely: --no-classloads-only)           See also infer-analyze(1).
+
        --compilation-database +path
            File that contain compilation commands (can be specified multiple
            times)           See also infer-capture(1).

infer/man/man1/infer.txt

@@ -147,6 +147,14 @@ OPTIONS
            Specify a file containing the AST of the program, in biniou format       
     See also infer-capture(1).
 
+       --classloads
+           Activates: class loading analysis (Conversely: --no-classloads)       
+    See also infer-analyze(1).
+
+       --classloads-only
+           Activates: Enable --classloads and disable all other checkers
+           (Conversely: --no-classloads-only)           See also infer-analyze(1).
+
        --compilation-database +path
            File that contain compilation commands (can be specified multiple
            times)           See also infer-capture(1).

infer/src/backend/Payloads.ml

@@ -12,41 +12,45 @@ type t =
   { annot_map: AnnotReachabilityDomain.astate option
   ; biabduction: BiabductionSummary.t option
   ; buffer_overrun: BufferOverrunSummary.t option
+  ; class_loads: ClassLoadsDomain.summary option
+  ; cost: CostDomain.summary option
   ; crashcontext_frame: Stacktree_t.stacktree option
   ; litho: LithoDomain.astate option
+  ; purity: PurityDomain.summary option
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option
   ; resources: ResourceLeakDomain.summary option
   ; siof: SiofDomain.Summary.astate option
-  ; typestate: TypeState.t option
-  ; uninit: UninitDomain.Summary.t option
-  ; cost: CostDomain.summary option
   ; starvation: StarvationDomain.summary option
-  ; purity: PurityDomain.summary option }
+  ; typestate: TypeState.t option
+  ; uninit: UninitDomain.Summary.t option }
 
 let pp pe fmt
-    { biabduction
+    { annot_map
-    ; typestate
+    ; biabduction
+    ; buffer_overrun
+    ; class_loads
+    ; cost
     ; crashcontext_frame
+    ; litho
+    ; purity
     ; quandary
-    ; siof
     ; racerd
-    ; litho
+    ; siof
-    ; buffer_overrun
-    ; annot_map
-    ; uninit
-    ; cost
     ; starvation
-    ; purity } =
+    ; typestate
+    ; uninit } =
   let pp_opt prefix pp fmt = function
     | Some x ->
         F.fprintf fmt "%s: %a@\n" prefix pp x
     | None ->
         ()
   in
-  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a@\n"
+  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a%a@\n"
     (pp_opt "Biabduction" (BiabductionSummary.pp pe))
     biabduction (pp_opt "TypeState" TypeState.pp) typestate
+    (pp_opt "ClassLoads" ClassLoadsDomain.pp_summary)
+    class_loads
     (pp_opt "CrashContext" Crashcontext.pp_stacktree)
     crashcontext_frame
     (pp_opt "Quandary" QuandarySummary.pp)
@@ -70,17 +74,18 @@ let pp pe fmt
 
 
 let empty =
-  { biabduction= None
+  { annot_map= None
-  ; typestate= None
+  ; biabduction= None
-  ; annot_map= None
+  ; class_loads= None
+  ; buffer_overrun= None
   ; crashcontext_frame= None
+  ; cost= None
+  ; litho= None
+  ; purity= None
   ; quandary= None
+  ; racerd= None
   ; resources= None
   ; siof= None
-  ; racerd= None
-  ; litho= None
-  ; buffer_overrun= None
-  ; uninit= None
-  ; cost= None
   ; starvation= None
-  ; purity= None }
+  ; typestate= None
+  ; uninit= None }

infer/src/backend/Payloads.mli

@@ -12,17 +12,18 @@ type t =
   { annot_map: AnnotReachabilityDomain.astate option
   ; biabduction: BiabductionSummary.t option
   ; buffer_overrun: BufferOverrunSummary.t option
+  ; class_loads: ClassLoadsDomain.summary option
+  ; cost: CostDomain.summary option
   ; crashcontext_frame: Stacktree_t.stacktree option
   ; litho: LithoDomain.astate option
+  ; purity: PurityDomain.summary option
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option
   ; resources: ResourceLeakDomain.summary option
   ; siof: SiofDomain.Summary.astate option
-  ; typestate: TypeState.t option
-  ; uninit: UninitDomain.Summary.t option
-  ; cost: CostDomain.summary option
   ; starvation: StarvationDomain.summary option
-  ; purity: PurityDomain.summary option }
+  ; typestate: TypeState.t option
+  ; uninit: UninitDomain.Summary.t option }
 
 val pp : Pp.env -> Format.formatter -> t -> unit
 

infer/src/base/Config.ml

@@ -587,6 +587,7 @@ and ( annotation_reachability
     , biabduction
     , bufferoverrun
     , check_nullable
+    , class_loads
     , cost
     , crashcontext
     , eradicate
@@ -630,6 +631,7 @@ and ( annotation_reachability
   and check_nullable =
     mk_checker ~long:"check-nullable"
       "checks that values annotated with nullable are always checked for null before dereference"
+  and class_loads = mk_checker ~long:"classloads" ~default:false "class loading analysis"
   and cost = mk_checker ~long:"cost" ~default:false "checker for performance cost analysis"
   and crashcontext =
     mk_checker ~long:"crashcontext"
@@ -712,6 +714,7 @@ and ( annotation_reachability
   , biabduction
   , bufferoverrun
   , check_nullable
+  , class_loads
   , cost
   , crashcontext
   , eradicate
@@ -2509,6 +2512,8 @@ and clang_include_to_override_regex = !clang_include_to_override_regex
 
 and classpath = !classpath
 
+and class_loads = !class_loads
+
 and compute_analytics = !compute_analytics
 
 and continue_capture = !continue

infer/src/base/Config.mli

@@ -69,6 +69,8 @@ val classnames_dir_name : string
 
 val classpath : string option
 
+val class_loads : bool
+
 val costs_report_json : string
 
 val cpp_extra_include_dir : string

infer/src/checkers/registerCheckers.ml

@@ -129,7 +129,9 @@ let all_checkers =
     ; active= Config.purity
     ; callbacks=
         [(Procedure Purity.checker, Language.Clang); (Procedure Purity.checker, Language.Java)] }
-  ]
+  ; { name= "Class loading analysis"
+    ; active= Config.class_loads
+    ; callbacks= [(Procedure ClassLoads.analyze_procedure, Language.Java)] } ]
 
 
 let get_active_checkers () =

infer/src/concurrency/classLoads.ml

@@ -0,0 +1,51 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+module L = Logging
+
+module Payload = SummaryPayload.Make (struct
+  type t = ClassLoadsDomain.summary
+
+  let update_payloads post (payloads : Payloads.t) = {payloads with class_loads= Some post}
+
+  let of_payloads (payloads : Payloads.t) = payloads.class_loads
+end)
+
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = ClassLoadsDomain
+
+  type extras = unit
+
+  let exec_instr (astate : Domain.astate) {ProcData.pdesc} _ (instr : HilInstr.t) =
+    match instr with
+    | Call (_, Direct callee, _, _, loc) ->
+        Payload.read pdesc callee
+        |> Option.value_map ~default:astate ~f:(Domain.integrate_summary astate callee loc)
+    | _ ->
+        astate
+
+
+  let pp_session_name _node fmt = F.pp_print_string fmt "class loads"
+end
+
+module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions)
+
+let die_if_not_java proc_desc =
+  let is_java =
+    Procdesc.get_proc_name proc_desc |> Typ.Procname.get_language |> Language.(equal Java)
+  in
+  if not is_java then L.(die InternalError "Not supposed to run on non-Java code yet.")
+
+
+let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
+  die_if_not_java proc_desc ;
+  let initial = ClassLoadsDomain.empty in
+  let proc_data = ProcData.make proc_desc tenv () in
+  Analyzer.compute_post proc_data ~initial
+  |> Option.value_map ~default:summary ~f:(fun astate -> Payload.update_summary astate summary)

infer/src/concurrency/classLoads.mli

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+val analyze_procedure : Callbacks.proc_callback_t

infer/src/concurrency/classLoadsDomain.ml

@@ -0,0 +1,38 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+module ClassLoad = String
+module Event = ExplicitTrace.MakeTraceElem (ClassLoad)
+include Event.FiniteSet
+
+let add ({Event.trace} as x) astate =
+  match find_opt x astate with
+  | None ->
+      add x astate
+  | Some ({Event.trace= trace'} as x') ->
+      if Int.( <= ) (List.length trace') (List.length trace) then astate
+      else remove x' astate |> add x
+
+
+let union xs ys = fold add xs ys
+
+let integrate_summary astate callee_pname loc callee_summary =
+  match callee_pname with
+  | Typ.Procname.Java java_pname ->
+      let clazz = Typ.Procname.Java.get_class_name java_pname in
+      let new_event = Event.make clazz loc in
+      let callsite = CallSite.make callee_pname loc in
+      let summary = with_callsite callee_summary callsite in
+      add new_event astate |> union summary
+  | _ ->
+      astate
+
+
+type summary = astate
+
+let pp_summary = pp

infer/src/concurrency/classLoadsDomain.mli

@@ -0,0 +1,16 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+
+include AbstractDomain.WithBottom
+
+type summary = astate
+
+val pp_summary : F.formatter -> summary -> unit
+
+val integrate_summary : astate -> Typ.Procname.t -> Location.t -> summary -> astate