diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index f48597e60..3d1cc13a1 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -47,6 +47,16 @@ OPTIONS reactive analysis should start. Source files should be specified relative to project root or be absolute + --config-checks-between-markers + Activates: checker config-checks-between-markers: [EXPERIMENTAL] + Collects config checks between marker start and end. (Conversely: + --no-config-checks-between-markers) + + --config-checks-between-markers-only + Activates: Enable config-checks-between-markers and disable all + other checkers (Conversely: + --no-config-checks-between-markers-only) + --continue-analysis Activates: Continue the analysis after more targets are captured by --continue. The other analysis options should be given the same diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 598ac48a8..0228aace6 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -242,6 +242,16 @@ OPTIONS line count and component kit file cyclomatic complexity (Conversely: --no-compute-analytics) See also infer-capture(1) and infer-run(1). + --config-checks-between-markers + Activates: checker config-checks-between-markers: [EXPERIMENTAL] + Collects config checks between marker start and end. (Conversely: + --no-config-checks-between-markers) See also infer-analyze(1). + + --config-checks-between-markers-only + Activates: Enable config-checks-between-markers and disable all + other checkers (Conversely: + --no-config-checks-between-markers-only) See also infer-analyze(1). + --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.txt b/infer/man/man1/infer.txt index 8bf1f854d..dba76b4dd 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -242,6 +242,16 @@ OPTIONS line count and component kit file cyclomatic complexity (Conversely: --no-compute-analytics) See also infer-capture(1) and infer-run(1). + --config-checks-between-markers + Activates: checker config-checks-between-markers: [EXPERIMENTAL] + Collects config checks between marker start and end. (Conversely: + --no-config-checks-between-markers) See also infer-analyze(1). + + --config-checks-between-markers-only + Activates: Enable config-checks-between-markers and disable all + other checkers (Conversely: + --no-config-checks-between-markers-only) See also infer-analyze(1). + --continue Activates: Continue the capture for the reactive analysis, increasing the changed files/procedures. (If a procedure was diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 4691c8055..0aa4d12b8 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -77,6 +77,10 @@ end module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted module TopLiftedUtils : sig + val leq : leq:(lhs:'a -> rhs:'a -> bool) -> lhs:'a top_lifted -> rhs:'a top_lifted -> bool + + val pp : pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a top_lifted -> unit + val pp_top : Format.formatter -> unit end diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 9185e4ab2..ee9d4541e 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -13,6 +13,7 @@ type t = ; biabduction: BiabductionSummary.t option ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option + ; config_checks_between_markers: ConfigChecksBetweenMarkers.Summary.t option ; cost: CostDomain.summary option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho_required_props: LithoDomain.summary option @@ -38,6 +39,8 @@ let fields = ~biabduction:(fun f -> mk_pe f "Biabduction" BiabductionSummary.pp) ~buffer_overrun_analysis:(fun f -> mk f "BufferOverrunAnalysis" BufferOverrunAnalysisSummary.pp) ~buffer_overrun_checker:(fun f -> mk f "BufferOverrunChecker" BufferOverrunCheckerSummary.pp) + ~config_checks_between_markers:(fun f -> + mk f "ConfigChecksBetweenMarkers" ConfigChecksBetweenMarkers.Summary.pp ) ~cost:(fun f -> mk f "Cost" CostDomain.pp_summary) ~litho_required_props:(fun f -> mk f "Litho Required Props" LithoDomain.pp_summary) ~pulse:(fun f -> mk f "Pulse" PulseSummary.pp) @@ -61,6 +64,7 @@ let empty = ; biabduction= None ; buffer_overrun_analysis= None ; buffer_overrun_checker= None + ; config_checks_between_markers= None ; cost= None ; lab_resource_leaks= None ; litho_required_props= None diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index d737d8024..8c45af601 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -17,6 +17,7 @@ include sig ; biabduction: BiabductionSummary.t option ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option + ; config_checks_between_markers: ConfigChecksBetweenMarkers.Summary.t option ; cost: CostDomain.summary option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho_required_props: LithoDomain.summary option diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index d7d057995..4ef4763d4 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -185,7 +185,14 @@ let all_checkers = (let annot_reach = interprocedural Payloads.Fields.annot_map AnnotationReachability.checker in - [(annot_reach, Java); (annot_reach, Clang)] ) } ] + [(annot_reach, Java); (annot_reach, Clang)] ) } + ; { checker= ConfigChecksBetweenMarkers + ; callbacks= + (let checker = + interprocedural Payloads.Fields.config_checks_between_markers + ConfigChecksBetweenMarkers.checker + in + [(checker, Java)] ) } ] let get_active_checkers () = diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml index ec8d8ea92..0f1d4dfbc 100644 --- a/infer/src/base/Checker.ml +++ b/infer/src/base/Checker.ml @@ -13,6 +13,7 @@ type t = | Biabduction | BufferOverrunAnalysis | BufferOverrunChecker + | ConfigChecksBetweenMarkers | Cost | Eradicate | FragmentRetainsView @@ -69,6 +70,9 @@ let config_unsafe checker = let supports_java (language : Language.t) = match language with Clang -> NoSupport | Java -> Support in + let supports_java_experimental (language : Language.t) = + match language with Clang -> NoSupport | Java -> ExperimentalSupport + in match checker with | AnnotationReachability -> { id= "annotation-reachability" @@ -119,6 +123,14 @@ let config_unsafe checker = ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [BufferOverrunAnalysis] } + | ConfigChecksBetweenMarkers -> + { id= "config-checks-between-markers" + ; kind= Internal + ; support= supports_java_experimental + ; short_documentation= "[EXPERIMENTAL] Collects config checks between marker start and end." + ; cli_flags= Some {deprecated= []; show_in_help= true} + ; enabled_by_default= false + ; activates= [] } | Cost -> { id= "cost" ; kind= diff --git a/infer/src/base/Checker.mli b/infer/src/base/Checker.mli index fe664f555..e5d5bce15 100644 --- a/infer/src/base/Checker.mli +++ b/infer/src/base/Checker.mli @@ -12,6 +12,7 @@ type t = | Biabduction | BufferOverrunAnalysis | BufferOverrunChecker + | ConfigChecksBetweenMarkers | Cost | Eradicate | FragmentRetainsView diff --git a/infer/src/checkers/ConfigChecksBetweenMarkers.ml b/infer/src/checkers/ConfigChecksBetweenMarkers.ml new file mode 100644 index 000000000..c3b2fe190 --- /dev/null +++ b/infer/src/checkers/ConfigChecksBetweenMarkers.ml @@ -0,0 +1,236 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open AbstractDomain.Types +module F = Format + +module ConfigName = struct + type t = {config_class: Pvar.t; config_name: Fieldname.t} [@@deriving compare, equal] + + (** For readability, this prints short name of config. *) + let pp f {config_name} = F.fprintf f "%a" Fieldname.pp config_name +end + +module ConfigTopLifted = struct + type t = ConfigName.t top_lifted + + let pp = AbstractDomain.TopLiftedUtils.pp ~pp:ConfigName.pp + + let leq = AbstractDomain.TopLiftedUtils.leq ~leq:(fun ~lhs ~rhs -> ConfigName.equal lhs rhs) + + let join x y = + match (x, y) with + | Top, _ | _, Top -> + Top + | NonTop x', NonTop y' -> + if ConfigName.equal x' y' then x else Top + + + let widen ~prev ~next ~num_iters:_ = join prev next +end + +module ConfigWithLocation = struct + type t = ConfigName.t * Location.t [@@deriving compare] + + let pp f (config, location) = F.fprintf f "%a at %a" ConfigName.pp config Location.pp location +end + +module Mem = AbstractDomain.Map (Ident) (ConfigTopLifted) + +module MarkerSet = struct + include AbstractDomain.FiniteSet (IntLit) + + let pp f x = + if is_empty x then F.pp_print_string f "{ }" + else ( + F.fprintf f "@[{ " ; + let is_first = ref true in + iter + (fun marker -> + if !is_first then is_first := false else F.fprintf f ",@ " ; + IntLit.pp f marker ) + x ; + F.fprintf f " }@]" ) +end + +module InvMarkerSet = AbstractDomain.InvertedSet (IntLit) + +module Context = struct + (** We use opposite orders in collecting the sets of started and ended markers. This is because we + want to keep the analyzer sound in design. In program points where multiple control flows + join, we want to know "the markers that have been started, at least, one of the control flow" + (i.e. may-started) and "the markers that have been ended in all of the control flows" (i.e. + must-ended). *) + type t = {started_markers: MarkerSet.t; ended_markers: InvMarkerSet.t} + + let pp f {started_markers; ended_markers} = + F.fprintf f "@[@[started markers: %a@]@\n@[ended markers: %a@]@]" MarkerSet.pp started_markers + InvMarkerSet.pp ended_markers + + + let leq ~lhs ~rhs = + MarkerSet.leq ~lhs:lhs.started_markers ~rhs:rhs.started_markers + && InvMarkerSet.leq ~lhs:lhs.ended_markers ~rhs:rhs.ended_markers + + + let join x y = + { started_markers= MarkerSet.join x.started_markers y.started_markers + ; ended_markers= InvMarkerSet.join x.ended_markers y.ended_markers } + + + let widen ~prev ~next ~num_iters = + { started_markers= + MarkerSet.widen ~prev:prev.started_markers ~next:next.started_markers ~num_iters + ; ended_markers= InvMarkerSet.widen ~prev:prev.ended_markers ~next:next.ended_markers ~num_iters + } + + + let init = {started_markers= MarkerSet.bottom; ended_markers= InvMarkerSet.top} + + let call_marker_start marker {started_markers; ended_markers} = + { started_markers= MarkerSet.add marker started_markers + ; ended_markers= InvMarkerSet.remove marker ended_markers } + + + let call_marker_end marker {started_markers; ended_markers} = + { started_markers= MarkerSet.remove marker started_markers + ; ended_markers= InvMarkerSet.add marker ended_markers } + + + let instantiate_callee ~callee_context ~caller_context = + let started_markers = + MarkerSet.join callee_context.started_markers caller_context.started_markers + |> InvMarkerSet.fold MarkerSet.remove callee_context.ended_markers + in + let ended_markers = + InvMarkerSet.join caller_context.ended_markers callee_context.ended_markers + |> MarkerSet.fold InvMarkerSet.remove callee_context.started_markers + in + {started_markers; ended_markers} +end + +module ConfigChecks = struct + include AbstractDomain.Map (ConfigWithLocation) (Context) + + let weak_add k v location m = + update (k, location) (function None -> Some v | Some v' -> Some (Context.join v v')) m +end + +module Summary = struct + type t = {context: Context.t; config_checks: ConfigChecks.t} + + let pp f {context; config_checks} = + F.fprintf f "@[@[%a@]@\n@[config checks:@ %a@]@]" Context.pp context ConfigChecks.pp + config_checks +end + +module Dom = struct + type t = {mem: Mem.t; context: Context.t; config_checks: ConfigChecks.t} + + let pp f {mem; context; config_checks} = + F.fprintf f "@[@[mem:@ %a@]@\n@[%a@]@\n@[config checks:@ %a@]@]" Mem.pp mem Context.pp context + ConfigChecks.pp config_checks + + + let init = {mem= Mem.bottom; context= Context.init; config_checks= ConfigChecks.bottom} + + let join x y = + { mem= Mem.join x.mem y.mem + ; context= Context.join x.context y.context + ; config_checks= ConfigChecks.join x.config_checks y.config_checks } + + + let widen ~prev ~next ~num_iters = + { mem= Mem.widen ~prev:prev.mem ~next:next.mem ~num_iters + ; context= Context.widen ~prev:prev.context ~next:next.context ~num_iters + ; config_checks= ConfigChecks.widen ~prev:prev.config_checks ~next:next.config_checks ~num_iters + } + + + let leq ~lhs ~rhs = + Mem.leq ~lhs:lhs.mem ~rhs:rhs.mem + && Context.leq ~lhs:lhs.context ~rhs:rhs.context + && ConfigChecks.leq ~lhs:lhs.config_checks ~rhs:rhs.config_checks + + + let load_config id ~config_class ~config_name ({mem} as astate) = + {astate with mem= Mem.add id (NonTop {ConfigName.config_class; config_name}) mem} + + + let call_marker_start marker ({context} as astate) = + {astate with context= Context.call_marker_start marker context} + + + let call_marker_end marker ({context} as astate) = + {astate with context= Context.call_marker_end marker context} + + + let call_config_check id location ({mem; context; config_checks} as astate) = + match Mem.find_opt id mem with + | Some (NonTop config) -> + {astate with config_checks= ConfigChecks.weak_add config context location config_checks} + | _ -> + astate + + + let instantiate_callee + ~callee_summary:{Summary.context= callee_context; config_checks= callee_config_checks} + location ({context= caller_context; config_checks= caller_config_checks} as astate) = + let context = Context.instantiate_callee ~callee_context ~caller_context in + let config_checks = + ConfigChecks.fold + (fun (config, _) callee_context acc -> + let context = Context.instantiate_callee ~callee_context ~caller_context in + ConfigChecks.weak_add config context location acc ) + callee_config_checks caller_config_checks + in + {astate with context; config_checks} + + + let to_summary {context; config_checks} = {Summary.context; config_checks} +end + +type analysis_data = {tenv: Tenv.t; get_summary: Procname.t -> Summary.t option} + +module TransferFunctions = struct + module CFG = ProcCfg.NormalOneInstrPerNode + module Domain = Dom + + type nonrec analysis_data = analysis_data + + let exec_instr astate {tenv; get_summary} _node instr = + match (instr : Sil.instr) with + | Load {id; e= Lfield (Lvar config_class, config_name, _)} + when FbGKInteraction.is_config_class config_class -> + Dom.load_config id ~config_class ~config_name astate + | Call (_, Const (Cfun callee), _ :: (Const (Cint marker), _) :: _, _, _) + when FbGKInteraction.is_marker_start tenv callee -> + Dom.call_marker_start marker astate + | Call (_, Const (Cfun callee), _ :: (Const (Cint marker), _) :: _, _, _) + when FbGKInteraction.is_marker_end tenv callee -> + Dom.call_marker_end marker astate + | Call (_, Const (Cfun callee), _ :: (Var id, _) :: _, location, _) + when FbGKInteraction.is_config_check tenv callee -> + Dom.call_config_check id location astate + | Call (_, Const (Cfun callee), _, location, _) -> + Option.value_map (get_summary callee) ~default:astate ~f:(fun callee_summary -> + Dom.instantiate_callee ~callee_summary location astate ) + | _ -> + astate + + + let pp_session_name node fmt = + F.fprintf fmt "Config checks between markers %a" CFG.Node.pp_id (CFG.Node.id node) +end + +module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions) + +let checker {InterproceduralAnalysis.proc_desc; tenv; analyze_dependency} = + let open IOption.Let_syntax in + let get_summary pname = analyze_dependency pname >>| snd in + Analyzer.compute_post {tenv; get_summary} ~initial:Dom.init proc_desc >>| Dom.to_summary diff --git a/infer/src/checkers/ConfigChecksBetweenMarkers.mli b/infer/src/checkers/ConfigChecksBetweenMarkers.mli new file mode 100644 index 000000000..4aa985eb1 --- /dev/null +++ b/infer/src/checkers/ConfigChecksBetweenMarkers.mli @@ -0,0 +1,16 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * 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 Summary : sig + type t + + val pp : Format.formatter -> t -> unit +end + +val checker : Summary.t InterproceduralAnalysis.t -> Summary.t option diff --git a/infer/src/opensource/FbGKInteraction.ml b/infer/src/opensource/FbGKInteraction.ml new file mode 100644 index 000000000..8c3967b86 --- /dev/null +++ b/infer/src/opensource/FbGKInteraction.ml @@ -0,0 +1,14 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +let is_config_class _ = false + +let is_config_check _ _ = false + +let is_marker_start _ _ = false + +let is_marker_end _ _ = false diff --git a/infer/src/opensource/FbGKInteraction.mli b/infer/src/opensource/FbGKInteraction.mli new file mode 100644 index 000000000..e1574dfe7 --- /dev/null +++ b/infer/src/opensource/FbGKInteraction.mli @@ -0,0 +1,14 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +val is_config_class : 'pvar -> bool + +val is_config_check : 'tenv -> 'pname -> bool + +val is_marker_start : 'tenv -> 'pname -> bool + +val is_marker_end : 'tenv -> 'pname -> bool