diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 5ad4761a7..002e881b7 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/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 diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index d1ce8b945..2fb7b1960 100644 --- a/infer/man/man1/infer-full.txt +++ b/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). diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 2c3f578d7..a4c3cae91 100644 --- a/infer/man/man1/infer.txt +++ b/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). diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 8fb1ec3e4..331b9d675 100644 --- a/infer/src/backend/Payloads.ml +++ b/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 - ; typestate + { annot_map + ; biabduction + ; buffer_overrun + ; class_loads + ; cost ; crashcontext_frame + ; litho + ; purity ; quandary - ; siof ; racerd - ; litho - ; buffer_overrun - ; annot_map - ; uninit - ; cost + ; siof ; 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 - ; typestate= None - ; annot_map= None + { annot_map= None + ; biabduction= 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 } diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 27c8adfce..44f0497ee 100644 --- a/infer/src/backend/Payloads.mli +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 35c0ed414..de3882648 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 067ad72b9..8c3451d15 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 506cdb5f9..46ea88ddd 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/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 () = diff --git a/infer/src/concurrency/classLoads.ml b/infer/src/concurrency/classLoads.ml new file mode 100644 index 000000000..99f300b47 --- /dev/null +++ b/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) diff --git a/infer/src/concurrency/classLoads.mli b/infer/src/concurrency/classLoads.mli new file mode 100644 index 000000000..79695063e --- /dev/null +++ b/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 diff --git a/infer/src/concurrency/classLoadsDomain.ml b/infer/src/concurrency/classLoadsDomain.ml new file mode 100644 index 000000000..098e28e26 --- /dev/null +++ b/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 diff --git a/infer/src/concurrency/classLoadsDomain.mli b/infer/src/concurrency/classLoadsDomain.mli new file mode 100644 index 000000000..7d2fdec39 --- /dev/null +++ b/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