From 960d7fb5612c517047a11c7798574f2c45f5a0af Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 15 Jun 2020 12:29:00 -0700 Subject: [PATCH] [CCBM] Add a new checker config-checks-beween-markers (1/3) Summary: This diff adds a prototype of a new checker that collects config checkings between markers. Basically, what the checker is doing is a taint analysis. * Taint source: function calls of "marker start" * Taint sink: function calls of config checking * Taint remove: function calls of "marker end" By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending. I am separating the diff into three steps: (1/3) Add basic abstract semantics (2/3) Add trace information (3/3) Add reporting with test examples Reviewed By: jvillard Differential Revision: D21935546 fbshipit-source-id: 092abb92c --- infer/man/man1/infer-analyze.txt | 10 + infer/man/man1/infer-full.txt | 10 + infer/man/man1/infer.txt | 10 + infer/src/absint/AbstractDomain.mli | 4 + infer/src/backend/Payloads.ml | 4 + infer/src/backend/Payloads.mli | 1 + infer/src/backend/registerCheckers.ml | 9 +- infer/src/base/Checker.ml | 12 + infer/src/base/Checker.mli | 1 + .../checkers/ConfigChecksBetweenMarkers.ml | 236 ++++++++++++++++++ .../checkers/ConfigChecksBetweenMarkers.mli | 16 ++ infer/src/opensource/FbGKInteraction.ml | 14 ++ infer/src/opensource/FbGKInteraction.mli | 14 ++ 13 files changed, 340 insertions(+), 1 deletion(-) create mode 100644 infer/src/checkers/ConfigChecksBetweenMarkers.ml create mode 100644 infer/src/checkers/ConfigChecksBetweenMarkers.mli create mode 100644 infer/src/opensource/FbGKInteraction.ml create mode 100644 infer/src/opensource/FbGKInteraction.mli 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