[config] datatype for checkers

Summary:
The goals are to have all the checker definitions and documentation in one
place (except how to actually run them, since that's not quite the same
concept; for example inferbo is one checker but several analyses depend on its
symbolic execution), and later on to be able to link issues reported by infer
back to the checker that generated them.

This makes apparent that the documentation of our checkers is lacking,
not touching that in this diff.

Not sure if "analysis" would be a better name than "checker" at this
point? For instance "Linters" is one of the checkers, which historically
at least we have not considered to be the case.

Reviewed By: mityal

Differential Revision: D20252386

fbshipit-source-id: fc611bfb7
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent e4602ba0df
commit 8e5ee67fed

@ -103,7 +103,7 @@ OPTIONS
--no-default-checkers
Deactivates: Default checkers: --biabduction,
--fragment-retains-view, --inefficient-keyset-iterator, --linters,
--liveness, --racerd, --siof, --starvation, --self_in_block,
--liveness, --racerd, --siof, --self_in_block, --starvation,
--uninit (Conversely: --default-checkers)
--eradicate
@ -200,14 +200,6 @@ OPTIONS
Activates: Enable --loop-hoisting and disable all other checkers
(Conversely: --no-loop-hoisting-only)
--nullsafe
Activates: [RESERVED] Reserved for nullsafe typechecker, use
--eradicate for now (Conversely: --no-nullsafe)
--nullsafe-only
Activates: Enable --nullsafe and disable all other checkers
(Conversely: --no-nullsafe-only)
--perf-profiler-data-file file
Specify the file containing perf profiler data to read

@ -330,7 +330,7 @@ OPTIONS
--no-default-checkers
Deactivates: Default checkers: --biabduction,
--fragment-retains-view, --inefficient-keyset-iterator, --linters,
--liveness, --racerd, --siof, --starvation, --self_in_block,
--liveness, --racerd, --siof, --self_in_block, --starvation,
--uninit (Conversely: --default-checkers) See also infer-analyze(1).
--no-default-linters
@ -798,14 +798,6 @@ OPTIONS
See also infer-analyze(1).
--nullsafe
Activates: [RESERVED] Reserved for nullsafe typechecker, use
--eradicate for now (Conversely: --no-nullsafe) See also infer-analyze(1).
--nullsafe-only
Activates: Enable --nullsafe and disable all other checkers
(Conversely: --no-nullsafe-only) See also infer-analyze(1).
--only-show
Activates: Show the list of reports and exit (Conversely:
--no-only-show) See also infer-explore(1).
@ -1547,6 +1539,10 @@ INTERNAL OPTIONS
--nullable-annotation-name-reset
Cancel the effect of --nullable-annotation-name.
--nullsafe
Activates: [RESERVED] Reserved for nullsafe typechecker, use
--eradicate for now (Conversely: --no-nullsafe)
--nullsafe-disable-field-not-initialized-in-nonstrict-classes
Activates: Nullsafe: In this mode field not initialized issues
won't be reported unless the class is marked as @NullsafeStrict.

@ -330,7 +330,7 @@ OPTIONS
--no-default-checkers
Deactivates: Default checkers: --biabduction,
--fragment-retains-view, --inefficient-keyset-iterator, --linters,
--liveness, --racerd, --siof, --starvation, --self_in_block,
--liveness, --racerd, --siof, --self_in_block, --starvation,
--uninit (Conversely: --default-checkers) See also infer-analyze(1).
--no-default-linters
@ -798,14 +798,6 @@ OPTIONS
See also infer-analyze(1).
--nullsafe
Activates: [RESERVED] Reserved for nullsafe typechecker, use
--eradicate for now (Conversely: --no-nullsafe) See also infer-analyze(1).
--nullsafe-only
Activates: Enable --nullsafe and disable all other checkers
(Conversely: --no-nullsafe-only) See also infer-analyze(1).
--only-show
Activates: Show the list of reports and exit (Conversely:
--no-only-show) See also infer-explore(1).

@ -31,7 +31,7 @@ type t =
path, with Dpvar being the simplest one *)
type vpath = t option
let eradicate_java () = Config.eradicate && Language.curr_language_is Java
let eradicate_java () = Config.is_checker_enabled Eradicate && Language.curr_language_is Java
let split_var_clang var_name =
match String.rsplit2 ~on:'.' var_name with Some (_, name) -> name | _ -> var_name

@ -910,7 +910,7 @@ let pp_summary_and_issues formats_by_report_kind issue_formats =
all_issues :=
process_summary filters formats_by_report_kind linereader stats summary !all_issues ) ;
all_issues := Issue.sort_filter_issues !all_issues ;
if Config.quandaryBO then all_issues := QuandaryBO.update_issues !all_issues ;
if Config.is_checker_enabled QuandaryBO then all_issues := QuandaryBO.update_issues !all_issues ;
List.iter
~f:(fun ({Issue.proc_name} as issue) ->
let error_filter = error_filter filters proc_name in

@ -188,7 +188,9 @@ let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t opti
in
Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags))
| Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Var id0}
when Config.biabduction && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) ->
when Config.is_checker_enabled Biabduction
&& Ident.equal id id0
&& not (Pvar.is_frontend_tmp pvar) ->
(* this case is a hack to make bucketing continue to work in the presence of copy
propagation. previously, we would have code like:
n1 = foo(); x = n1; n2 = x; n2.toString(), but copy-propagation will optimize this to:

@ -0,0 +1,259 @@
(*
* 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
type t =
| AnnotationReachability
| Biabduction
| BufferOverrun
| ClassLoads
| Cost
| Eradicate
| FragmentRetainsView
| ImmutableCast
| Impurity
| InefficientKeysetIterator
| Linters
| LithoRequiredProps
| Liveness
| LoopHoisting
| NullsafeDeprecated
| PrintfArgs
| Pulse
| Purity
| Quandary
| QuandaryBO
| RacerD
| ResourceLeak
| SIOF
| SelfInBlock
| Starvation
| Uninit
[@@deriving equal, enumerate]
type support = NoSupport | Support | ExperimentalSupport | ToySupport
type config =
{ support: Language.t -> support
; short_documentation: string
; cli_flag: string
; show_in_help: bool
; enabled_by_default: bool
; cli_deprecated_flags: string list }
(* support for languages should be consistent with the corresponding
callbacks registered. Or maybe with the issues reported in link
with each analysis. Some runtime check probably needed. *)
let config checker =
let supports_clang_and_java _ = Support in
let supports_clang_and_java_experimental _ = ExperimentalSupport in
let supports_clang (language : Language.t) =
match language with Clang -> Support | Java -> NoSupport
in
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 ->
{ support= supports_clang_and_java
; short_documentation=
"the annotation reachability checker. Given a pair of source and sink annotation, e.g. \
@PerformanceCritical and @Expensive, this checker will warn whenever some method \
annotated with @PerformanceCritical calls, directly or indirectly, another method \
annotated with @Expensive"
; show_in_help= true
; cli_flag= "annotation-reachability"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| Biabduction ->
{ support= supports_clang_and_java
; short_documentation=
"the separation logic based bi-abduction analysis using the checkers framework"
; show_in_help= true
; cli_flag= "biabduction"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| BufferOverrun ->
{ support= supports_clang_and_java
; short_documentation= "the buffer overrun analysis"
; show_in_help= true
; cli_flag= "bufferoverrun"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| ClassLoads ->
{ support= supports_java
; short_documentation= "Java class loading analysis"
; show_in_help= true
; cli_flag= "class-loads"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| Cost ->
{ support= supports_clang_and_java
; short_documentation= "checker for performance cost analysis"
; show_in_help= true
; cli_flag= "cost"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| Eradicate ->
{ support= supports_java
; short_documentation= "the eradicate @Nullable checker for Java annotations"
; show_in_help= true
; cli_flag= "eradicate"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| FragmentRetainsView ->
{ support= supports_java
; short_documentation=
"detects when Android fragments are not explicitly nullified before becoming unreabable"
; show_in_help= true
; cli_flag= "fragment-retains-view"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| ImmutableCast ->
{ support= supports_java
; short_documentation=
"the detection of object cast from immutable type to mutable type. For instance, it will \
detect cast from ImmutableList to List, ImmutableMap to Map, and ImmutableSet to Set."
; show_in_help= true
; cli_flag= "immutable-cast"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| Impurity ->
{ support= supports_clang_and_java_experimental
; short_documentation= "[EXPERIMENTAL] Impurity analysis"
; show_in_help= true
; cli_flag= "impurity"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| InefficientKeysetIterator ->
{ support= supports_java
; short_documentation=
"Check for inefficient uses of keySet iterator that access both the key and the value."
; show_in_help= true
; cli_flag= "inefficient-keyset-iterator"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| Linters ->
{ support= supports_clang
; short_documentation= "syntactic linters"
; show_in_help= true
; cli_flag= "linters"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| LithoRequiredProps ->
{ support= supports_java_experimental
; short_documentation= "[EXPERIMENTAL] Required Prop check for Litho"
; show_in_help= true
; cli_flag= "litho-required-props"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| Liveness ->
{ support= supports_clang
; short_documentation= "the detection of dead stores and unused variables"
; show_in_help= true
; cli_flag= "liveness"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| LoopHoisting ->
{ support= supports_clang_and_java
; short_documentation= "checker for loop-hoisting"
; show_in_help= true
; cli_flag= "loop-hoisting"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| NullsafeDeprecated ->
{ support= (fun _ -> NoSupport)
; short_documentation= "[RESERVED] Reserved for nullsafe typechecker, use --eradicate for now"
; show_in_help= false
; cli_flag= "nullsafe"
; enabled_by_default= false
; cli_deprecated_flags= ["-check-nullable"; "-suggest-nullable"] }
| PrintfArgs ->
{ support= supports_java
; short_documentation=
"the detection of mismatch between the Java printf format strings and the argument types \
For, example, this checker will warn about the type error in `printf(\"Hello %d\", \
\"world\")`"
; show_in_help= true
; cli_flag= "printf-args"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| Pulse ->
{ support= supports_clang_and_java_experimental
; short_documentation= "[EXPERIMENTAL] C++ lifetime analysis"
; show_in_help= true
; cli_flag= "pulse"
; enabled_by_default= false
; cli_deprecated_flags= ["-ownership"] }
| Purity ->
{ support= supports_clang_and_java_experimental
; short_documentation= "[EXPERIMENTAL] Purity analysis"
; show_in_help= true
; cli_flag= "purity"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| Quandary ->
{ support= supports_clang_and_java
; short_documentation= "the quandary taint analysis"
; show_in_help= true
; cli_flag= "quandary"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| QuandaryBO ->
{ support= supports_clang_and_java_experimental
; short_documentation= "[EXPERIMENTAL] The quandaryBO tainted buffer access analysis"
; show_in_help= true
; cli_flag= "quandaryBO"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| RacerD ->
{ support= supports_clang_and_java
; short_documentation= "the RacerD thread safety analysis"
; show_in_help= true
; cli_flag= "racerd"
; enabled_by_default= true
; cli_deprecated_flags= ["-threadsafety"] }
| ResourceLeak ->
{ support= (fun _ -> ToySupport)
; short_documentation= ""
; show_in_help= false
; cli_flag= "resource-leak"
; enabled_by_default= false
; cli_deprecated_flags= [] }
| SIOF ->
{ support= supports_clang
; short_documentation= "the Static Initialization Order Fiasco analysis (C++ only)"
; show_in_help= true
; cli_flag= "siof"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| SelfInBlock ->
{ support= supports_clang
; short_documentation=
"checker to flag incorrect uses of when Objective-C blocks capture self"
; show_in_help= true
; cli_flag= "self_in_block"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| Starvation ->
{ support= supports_clang_and_java
; short_documentation= "starvation analysis"
; show_in_help= true
; cli_flag= "starvation"
; enabled_by_default= true
; cli_deprecated_flags= [] }
| Uninit ->
{ support= supports_clang
; short_documentation= "checker for use of uninitialized values"
; show_in_help= true
; cli_flag= "uninit"
; enabled_by_default= true
; cli_deprecated_flags= [] }

@ -0,0 +1,59 @@
(*
* 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
type t =
| AnnotationReachability
| Biabduction
| BufferOverrun
| ClassLoads
| Cost
| Eradicate
| FragmentRetainsView
| ImmutableCast
| Impurity
| InefficientKeysetIterator
| Linters
| LithoRequiredProps
| Liveness
| LoopHoisting
| NullsafeDeprecated
| PrintfArgs
| Pulse
| Purity
| Quandary
| QuandaryBO
| RacerD
| ResourceLeak
| SIOF
| SelfInBlock
| Starvation
| Uninit
[@@deriving equal, enumerate]
(** per-language support for each checker *)
type support =
| NoSupport (** checker does not run at all for this language *)
| Support (** checker is expected to give reasonable results *)
| ExperimentalSupport (** checker runs but is not expected to give reasonable results *)
| ToySupport
(** the checker is for teaching purposes only (like experimental but with no plans to improve
it) *)
type config =
{ support: Language.t -> support
; short_documentation: string
; cli_flag: string
(** the flag to enable this option on the command line, without the leading "--" (like the
[~long] argument of [CommandLineOption] functions) *)
; show_in_help: bool
; enabled_by_default: bool
; cli_deprecated_flags: string list
(** more command-line flags, similar to [~deprecated] arguments *) }
val config : t -> config

@ -62,13 +62,10 @@ let to_arg_spec_triple (x, spec, y) = (x, to_arg_spec spec, y)
let to_arg_speclist = List.map ~f:to_arg_spec_triple
(* NOTE: All variants must be also added to `all_parse_modes` below *)
type parse_mode = InferCommand | Javac | NoParse [@@deriving compare]
type parse_mode = InferCommand | Javac | NoParse [@@deriving compare, enumerate]
let equal_parse_mode = [%compare.equal: parse_mode]
let all_parse_modes = [InferCommand; Javac; NoParse]
type anon_arg_action =
{parse_subcommands: bool; parse_argfiles: bool; on_unknown: [`Add | `Reject | `Skip]}
@ -157,7 +154,7 @@ let check_no_duplicates desc_list =
(List.sort ~compare:(fun (x, _, _) (y, _, _) -> String.compare x y) desc_list)
let parse_mode_desc_lists = List.map ~f:(fun parse_mode -> (parse_mode, ref [])) all_parse_modes
let parse_mode_desc_lists = List.map ~f:(fun parse_mode -> (parse_mode, ref [])) all_of_parse_mode
module SectionMap = Caml.Map.Make (struct
type t = String.t

@ -17,33 +17,6 @@ module L = Die
type analyzer = Checkers | Linters [@@deriving compare]
type checkers =
{ annotation_reachability: bool ref
; biabduction: bool ref
; bufferoverrun: bool ref
; class_loads: bool ref
; cost: bool ref
; eradicate: bool ref
; fragment_retains_view: bool ref
; immutable_cast: bool ref
; impurity: bool ref
; inefficient_keyset_iterator: bool ref
; linters: bool ref
; litho_required_props: bool ref
; liveness: bool ref
; loop_hoisting: bool ref
; self_in_block: bool ref
; printf_args: bool ref
; pulse: bool ref
; purity: bool ref
; quandary: bool ref
; quandaryBO: bool ref
; racerd: bool ref
; resource_leak: bool ref
; siof: bool ref
; starvation: bool ref
; uninit: bool ref }
let equal_analyzer = [%compare.equal: analyzer]
let string_to_analyzer = [("checkers", Checkers); ("linters", Linters)]
@ -573,7 +546,11 @@ let anon_args = CLOpt.mk_anon ()
let all_checkers = ref []
let disable_all_checkers () = List.iter !all_checkers ~f:(fun (var, _, _, _) -> var := false)
let disable_all_checkers () = List.iter !all_checkers ~f:(fun (_, _, var) -> var := false)
let enable_checker c =
List.iter !all_checkers ~f:(fun (checker, _, var) -> if Checker.equal checker c then var := true)
let () =
let on_unknown_arg_from_command (cmd : InferCommand.t) =
@ -624,113 +601,30 @@ and analyzer =
instance, to enable only the biabduction analysis, run with $(b,--biabduction-only)."
and { annotation_reachability
; biabduction
; bufferoverrun
; class_loads
; cost
; eradicate
; fragment_retains_view
; immutable_cast
; impurity
; inefficient_keyset_iterator
; linters
; litho_required_props
; liveness
; loop_hoisting
; self_in_block
; printf_args
; pulse
; purity
; quandary
; quandaryBO
; racerd
; resource_leak
; siof
; starvation
; uninit } =
let mk_checker ?(default = false) ?(deprecated = []) ~long ?f doc =
and _checkers =
let open Checker in
let in_analyze_help = InferCommand.[(Analyze, manual_generic)] in
let mk_checker ?f checker =
let config = Checker.config checker in
let in_help = if config.show_in_help then in_analyze_help else [] in
let var =
CLOpt.mk_bool ?f ~long
~in_help:InferCommand.[(Analyze, manual_generic)]
~default ~deprecated doc
CLOpt.mk_bool ?f ~long:config.cli_flag ~in_help ~default:config.enabled_by_default
~deprecated:config.cli_deprecated_flags config.short_documentation
in
all_checkers := (var, long, doc, default) :: !all_checkers ;
var
all_checkers := (checker, config, var) :: !all_checkers
in
let annotation_reachability =
mk_checker ~default:false ~long:"annotation-reachability"
"the annotation reachability checker. Given a pair of source and sink annotation, e.g. \
@PerformanceCritical and @Expensive, this checker will warn whenever some method annotated \
with @PerformanceCritical calls, directly or indirectly, another method annotated with \
@Expensive"
and biabduction =
mk_checker ~long:"biabduction" ~default:true
"the separation logic based bi-abduction analysis using the checkers framework"
and bufferoverrun = mk_checker ~long:"bufferoverrun" "the buffer overrun analysis"
and class_loads = mk_checker ~long:"class-loads" ~default:false "Java class loading analysis"
and cost = mk_checker ~long:"cost" ~default:false "checker for performance cost analysis"
and eradicate =
mk_checker ~long:"eradicate" "the eradicate @Nullable checker for Java annotations"
and fragment_retains_view =
mk_checker ~long:"fragment-retains-view" ~default:true
"detects when Android fragments are not explicitly nullified before becoming unreabable"
and immutable_cast =
mk_checker ~long:"immutable-cast" ~default:false
"the detection of object cast from immutable type to mutable type. For instance, it will \
detect cast from ImmutableList to List, ImmutableMap to Map, and ImmutableSet to Set."
and impurity = mk_checker ~long:"impurity" ~default:false "[EXPERIMENTAL] Impurity analysis"
and inefficient_keyset_iterator =
mk_checker ~long:"inefficient-keyset-iterator" ~default:true
"Check for inefficient uses of keySet iterator that access both the key and the value."
and linters = mk_checker ~long:"linters" ~default:true "syntactic linters"
and litho_required_props =
mk_checker ~long:"litho-required-props" "[EXPERIMENTAL] Required Prop check for Litho"
and liveness =
mk_checker ~long:"liveness" ~default:true "the detection of dead stores and unused variables"
and loop_hoisting = mk_checker ~long:"loop-hoisting" ~default:false "checker for loop-hoisting"
and _nullsafe =
(* TODO make this to be activate nullsafe typechecker when old usages are gone *)
mk_checker ~long:"nullsafe"
~f:(fun b ->
CLOpt.warnf "nullsafe is is a reserved (no-op) checker; use --eradicate\n" ;
b )
~deprecated:["-check-nullable"; "-suggest-nullable"]
"[RESERVED] Reserved for nullsafe typechecker, use --eradicate for now"
and printf_args =
mk_checker ~long:"printf-args" ~default:false
"the detection of mismatch between the Java printf format strings and the argument types \
For, example, this checker will warn about the type error in `printf(\"Hello %d\", \
\"world\")`"
and pulse =
mk_checker ~long:"pulse" ~deprecated:["-ownership"] "[EXPERIMENTAL] C++ lifetime analysis"
and purity = mk_checker ~long:"purity" ~default:false "[EXPERIMENTAL] Purity analysis"
and quandary = mk_checker ~long:"quandary" ~default:false "the quandary taint analysis"
and quandaryBO =
mk_checker ~long:"quandaryBO" ~default:false
"[EXPERIMENTAL] The quandaryBO tainted buffer access analysis"
and racerd =
mk_checker ~long:"racerd" ~deprecated:["-threadsafety"] ~default:true
"the RacerD thread safety analysis"
and resource_leak = mk_checker ~long:"resource-leak" ""
and siof =
mk_checker ~long:"siof" ~default:true
"the Static Initialization Order Fiasco analysis (C++ only)"
and starvation = mk_checker ~long:"starvation" ~default:true "starvation analysis"
and self_in_block =
mk_checker ~long:"self_in_block" ~default:true
"checker to flag incorrect uses of when Objective-C blocks capture self"
and uninit = mk_checker ~long:"uninit" "checker for use of uninitialized values" ~default:true in
let mk_only (var, long, doc, _) =
List.iter Checker.all ~f:mk_checker ;
let mk_only (_checker, config, var) =
let (_ : bool ref) =
CLOpt.mk_bool_group ~long:(long ^ "-only")
CLOpt.mk_bool_group ~long:(config.cli_flag ^ "-only")
~in_help:InferCommand.[(Analyze, manual_generic)]
~f:(fun b ->
disable_all_checkers () ;
var := b ;
b )
( if String.equal doc "" then ""
else Printf.sprintf "Enable $(b,--%s) and disable all other checkers" long )
( if config.show_in_help then
Printf.sprintf "Enable $(b,--%s) and disable all other checkers" config.cli_flag
else "" )
[] (* do all the work in ~f *) []
(* do all the work in ~f *)
in
@ -743,44 +637,23 @@ and { annotation_reachability
~default:true
( "Default checkers: "
^ ( List.rev_filter_map
~f:(fun (_, long, _, default) ->
if default then Some (Printf.sprintf "$(b,--%s)" long) else None )
~f:(fun (_, config, _) ->
if config.enabled_by_default then Some (Printf.sprintf "$(b,--%s)" config.cli_flag)
else None )
!all_checkers
|> String.concat ~sep:", " ) )
~f:(fun b ->
List.iter
~f:(fun (var, _, _, default) ->
var := if b then default || !var else (not default) && !var )
~f:(fun (_, config, var) ->
var :=
if b then config.enabled_by_default || !var
else (not config.enabled_by_default) && !var )
!all_checkers ;
b )
[] (* do all the work in ~f *) []
(* do all the work in ~f *)
in
{ annotation_reachability
; biabduction
; bufferoverrun
; class_loads
; cost
; eradicate
; fragment_retains_view
; immutable_cast
; impurity
; inefficient_keyset_iterator
; linters
; litho_required_props
; liveness
; loop_hoisting
; printf_args
; pulse
; purity
; quandary
; quandaryBO
; racerd
; resource_leak
; self_in_block
; siof
; starvation
; uninit }
()
and annotation_reachability_cxx =
@ -2673,13 +2546,13 @@ let post_parsing_initialization command_opt =
List.rev_map ~f:(fun x -> `Raw x) !compilation_database
|> List.rev_map_append ~f:(fun x -> `Escaped x) !compilation_database_escaped ;
(* set analyzer mode to linters in linters developer mode *)
if !linters_developer_mode then linters := true ;
if !linters_developer_mode then enable_checker Linters ;
if !default_linters then linters_def_file := linters_def_default_file :: !linters_def_file ;
( match !analyzer with
| Linters ->
disable_all_checkers () ;
capture := false ;
linters := true
enable_checker Linters
| Checkers ->
() ) ;
Option.value ~default:InferCommand.Run command_opt
@ -2740,8 +2613,6 @@ and allow_leak = !allow_leak
and analysis_stops = !analysis_stops
and annotation_reachability = !annotation_reachability
and annotation_reachability_cxx = !annotation_reachability_cxx
and annotation_reachability_cxx_sources = !annotation_reachability_cxx_sources
@ -2752,8 +2623,6 @@ and append_buck_flavors = !append_buck_flavors
and array_level = !array_level
and biabduction = !biabduction
and biabduction_model_alloc_pattern = Option.map ~f:Str.regexp !biabduction_model_alloc_pattern
and biabduction_model_free_pattern = Option.map ~f:Str.regexp !biabduction_model_free_pattern
@ -2798,8 +2667,6 @@ and buck_out = !buck_out
and buck_targets_blacklist = !buck_targets_blacklist
and bufferoverrun = !bufferoverrun
and call_graph_schedule = !call_graph_schedule
and capture = !capture
@ -2825,6 +2692,8 @@ and changed_files_index = !changed_files_index
and check_version = !check_version
and checkers = List.map !all_checkers ~f:(fun (checker, _, var) -> (checker, !var))
and clang_biniou_file = !clang_biniou_file
and clang_extra_flags = !clang_extra_flags
@ -2843,8 +2712,6 @@ and clang_libcxx_include_to_override_regex = !clang_libcxx_include_to_override_r
and classpath = !classpath
and class_loads = !class_loads
and class_loads_roots = String.Set.of_list !class_loads_roots
and compute_analytics = !compute_analytics
@ -2853,8 +2720,6 @@ and continue_analysis = !continue_analysis
and continue_capture = !continue
and cost = !cost
and costs_current = !costs_current
and costs_previous = !costs_previous
@ -2891,8 +2756,6 @@ and dotty_cfg_libs = !dotty_cfg_libs
and dump_duplicate_symbols = !dump_duplicate_symbols
and eradicate = !eradicate
and eradicate_condition_redundant = !eradicate_condition_redundant
and eradicate_field_over_annotated = !eradicate_field_over_annotated
@ -2917,8 +2780,6 @@ and filtering = !filtering
and force_delete_results_dir = !force_delete_results_dir
and fragment_retains_view = !fragment_retains_view
and force_integration = !force_integration
and from_json_report = !from_json_report
@ -2941,12 +2802,6 @@ and hoisting_report_only_expensive = !hoisting_report_only_expensive
and icfg_dotty_outfile = !icfg_dotty_outfile
and immutable_cast = !immutable_cast
and impurity = !impurity
and inefficient_keyset_iterator = !inefficient_keyset_iterator
and iphoneos_target_sdk_version = !iphoneos_target_sdk_version
and iphoneos_target_sdk_version_path_regex =
@ -2975,8 +2830,6 @@ and join_cond = !join_cond
and linter = !linter
and linters = !linters
and linters_def_file = !linters_def_file
and linters_def_folder = !linters_def_folder
@ -2987,10 +2840,6 @@ and linters_ignore_clang_failures = !linters_ignore_clang_failures
and linters_validate_syntax_only = !linters_validate_syntax_only
and litho_required_props = !litho_required_props
and liveness = !liveness
and liveness_dangerous_classes = !liveness_dangerous_classes
and load_average =
@ -3005,8 +2854,6 @@ and log_skipped = !log_skipped
and perf_profiler_data_file = !perf_profiler_data_file
and loop_hoisting = !loop_hoisting
and max_nesting = !max_nesting
and method_decls_info = !method_decls_info
@ -3049,8 +2896,6 @@ and only_footprint = !only_footprint
and only_show = !only_show
and self_in_block = !self_in_block
and passthroughs = !passthroughs
and patterns_modeled_expensive = match patterns_modeled_expensive with k, r -> (k, !r)
@ -3065,8 +2910,6 @@ and pmd_xml = !pmd_xml
and precondition_stats = !precondition_stats
and printf_args = !printf_args
and print_active_checkers = !print_active_checkers
and print_builtins = !print_builtins
@ -3111,22 +2954,14 @@ and progress_bar =
and project_root = !project_root
and pulse = !pulse
and pulse_intraprocedural_only = !pulse_intraprocedural_only
and pulse_max_disjuncts = !pulse_max_disjuncts
and pulse_widen_threshold = !pulse_widen_threshold
and purity = !purity
and pure_by_default = !pure_by_default
and quandary = !quandary
and quandaryBO = !quandaryBO
and quandary_endpoints = !quandary_endpoints
and quandary_sanitizers = !quandary_sanitizers
@ -3137,8 +2972,6 @@ and quandary_sinks = !quandary_sinks
and quiet = !quiet
and racerd = !racerd
and racerd_guardedby = !racerd_guardedby
and racerd_unknown_returns_owned = !racerd_unknown_returns_owned
@ -3175,8 +3008,6 @@ and report_suppress_errors = !report_suppress_errors
and reports_include_ml_loc = !reports_include_ml_loc
and resource_leak = !resource_leak
and results_dir = !results_dir
and scheduler = !scheduler
@ -3193,8 +3024,6 @@ and select = !select
and show_buckets = !print_buckets
and siof = !siof
and siof_check_iostreams = !siof_check_iostreams
and siof_safe_methods = !siof_safe_methods
@ -3235,8 +3064,6 @@ and sqlite_vfs = !sqlite_vfs
and sqlite_write_daemon = !sqlite_write_daemon
and starvation = !starvation
and starvation_skip_analysis = !starvation_skip_analysis
and starvation_strict_mode = !starvation_strict_mode
@ -3302,8 +3129,6 @@ and tv_limit_filtered = !tv_limit_filtered
and type_size = !type_size
and uninit = !uninit
and uninit_interproc = !uninit_interproc
and unsafe_malloc = !unsafe_malloc
@ -3326,11 +3151,16 @@ and xcpretty = !xcpretty
(** Configuration values derived from command-line options *)
let is_checker_enabled c =
List.find_map_exn checkers ~f:(fun (checker, enabled) ->
if Checker.equal checker c then Some enabled else None )
let captured_dir = results_dir ^/ captured_dir_name
let clang_frontend_action_string =
let text = if capture then ["translating"] else [] in
let text = if linters then "linting" :: text else text in
let text = if is_checker_enabled Linters then "linting" :: text else text in
let text =
if process_clang_ast && test_determinator then "Test Determinator with" :: text else text
in
@ -3347,10 +3177,10 @@ let procnames_locks_dir = results_dir ^/ procnames_locks_dir_name
a call to unknown code and true triggers lazy dynamic dispatch. The latter mode follows the
JVM semantics and creates procedure descriptions during symbolic execution using the type
information found in the abstract state *)
let dynamic_dispatch = biabduction
let dynamic_dispatch = is_checker_enabled Biabduction
let quandaryBO_filtered_issues =
if quandaryBO then
if is_checker_enabled QuandaryBO then
IssueType.
[ buffer_overrun_u5
; buffer_overrun_l5

@ -212,8 +212,6 @@ val allow_leak : bool
val analysis_stops : bool
val annotation_reachability : bool
val annotation_reachability_cxx : Yojson.Basic.t
val annotation_reachability_cxx_sources : Yojson.Basic.t
@ -224,8 +222,6 @@ val anon_args : string list
val array_level : int
val biabduction : bool
val biabduction_model_alloc_pattern : Str.regexp option
val biabduction_model_free_pattern : Str.regexp option
@ -258,8 +254,6 @@ val buck_out_gen : string
val buck_targets_blacklist : string list
val bufferoverrun : bool
val call_graph_schedule : bool
val capture : bool
@ -291,8 +285,6 @@ val clang_idirafter_to_override_regex : Str.regexp option
val clang_libcxx_include_to_override_regex : string option
val class_loads : bool
val class_loads_roots : String.Set.t
val command : InferCommand.t
@ -303,8 +295,6 @@ val continue_analysis : bool
val continue_capture : bool
val cost : bool
val costs_current : string option
val costs_previous : string option
@ -343,8 +333,6 @@ val dump_duplicate_symbols : bool
val dynamic_dispatch : bool
val eradicate : bool
val eradicate_condition_redundant : bool
val eradicate_field_over_annotated : bool
@ -369,8 +357,6 @@ val force_delete_results_dir : bool
val force_integration : build_system option
val fragment_retains_view : bool
val from_json_report : string option
val frontend_stats : bool
@ -391,12 +377,6 @@ val html : bool
val icfg_dotty_outfile : string option
val immutable_cast : bool
val impurity : bool
val inefficient_keyset_iterator : bool
val infer_is_clang : bool
val infer_is_javac : bool
@ -411,6 +391,8 @@ val iphoneos_target_sdk_version : string option
val iphoneos_target_sdk_version_path_regex : iphoneos_target_sdk_version_path_regex list
val is_checker_enabled : Checker.t -> bool
val issues_fields :
[ `Issue_field_bug_type
| `Issue_field_qualifier
@ -450,8 +432,6 @@ val keep_going : bool
val linter : string option
val linters : bool
val linters_def_file : string list
val linters_def_folder : string list
@ -462,10 +442,6 @@ val linters_ignore_clang_failures : bool
val linters_validate_syntax_only : bool
val litho_required_props : bool
val liveness : bool
val liveness_dangerous_classes : Yojson.Basic.t
val log_events : bool
@ -474,8 +450,6 @@ val log_file : string
val log_skipped : bool
val loop_hoisting : bool
val max_nesting : int option
val merge : bool
@ -513,8 +487,6 @@ val only_footprint : bool
val only_show : bool
val self_in_block : bool
val perf_profiler_data_file : string option
val pmd_xml : bool
@ -533,8 +505,6 @@ val print_types : bool
val print_using_diff : bool
val printf_args : bool
val procedures : bool
val procedures_attributes : bool
@ -559,20 +529,14 @@ val progress_bar : [`MultiLine | `Plain | `Quiet]
val project_root : string
val pulse : bool
val pulse_intraprocedural_only : bool
val pulse_max_disjuncts : int
val pulse_widen_threshold : int
val purity : bool
val pure_by_default : bool
val quandary : bool
val quandary_endpoints : Yojson.Basic.t
val quandary_sanitizers : Yojson.Basic.t
@ -581,12 +545,8 @@ val quandary_sinks : Yojson.Basic.t
val quandary_sources : Yojson.Basic.t
val quandaryBO : bool
val quiet : bool
val racerd : bool
val racerd_guardedby : bool
val racerd_unknown_returns_owned : bool
@ -615,8 +575,6 @@ val report_suppress_errors : string list
val reports_include_ml_loc : bool
val resource_leak : bool
val rest : string list
val results_dir : string
@ -635,8 +593,6 @@ val select : int option
val show_buckets : bool
val siof : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
@ -673,8 +629,6 @@ val sqlite_vfs : string option
val sqlite_write_daemon : bool
val starvation : bool
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
@ -729,8 +683,6 @@ val tv_limit_filtered : int
val type_size : bool
val uninit : bool
val uninit_interproc : bool
val unsafe_malloc : bool

@ -33,7 +33,7 @@ let zip_libraries =
lazy
(let mk_zip_lib zip_filename = {zip_filename; zip_channel= lazy (Zip.open_in zip_filename)} in
if
Config.biabduction
Config.is_checker_enabled Biabduction
&& (not Config.biabduction_models_mode)
&& Sys.file_exists Config.biabduction_models_jar = `Yes
then Some (mk_zip_lib Config.biabduction_models_jar)

@ -16,7 +16,7 @@ Format.sprintf
(flags (%s -open Core -open InferStdlib -open IStd -open InferGenerated))
(ocamlopt_flags (%s))
(libraries %s)
(preprocess (pps ppx_compare))
(preprocess (pps ppx_compare ppx_enumerate))
)
(documentation

@ -31,63 +31,67 @@ let all_checkers =
(* TODO (T24393492): the checkers should run in the order from this list.
Currently, the checkers are run in the reverse order *)
[ { name= "annotation reachability"
; active= Config.annotation_reachability
; active= Config.is_checker_enabled AnnotationReachability
; callbacks=
[ (Procedure AnnotationReachability.checker, Language.Java)
; (Procedure AnnotationReachability.checker, Language.Clang) ] }
; { name= "biabduction"
; active= Config.biabduction
; active= Config.is_checker_enabled Biabduction
; callbacks=
[ (DynamicDispatch Interproc.analyze_procedure, Language.Clang)
; (DynamicDispatch Interproc.analyze_procedure, Language.Java) ] }
; { name= "buffer overrun analysis"
; active=
Config.bufferoverrun || Config.cost || Config.loop_hoisting || Config.purity
|| Config.quandaryBO
Config.(
is_checker_enabled BufferOverrun || is_checker_enabled Cost
|| is_checker_enabled LoopHoisting || is_checker_enabled Purity
|| is_checker_enabled QuandaryBO)
; callbacks=
[ (Procedure BufferOverrunAnalysis.do_analysis, Language.Clang)
; (Procedure BufferOverrunAnalysis.do_analysis, Language.Java) ] }
; { name= "buffer overrun checker"
; active= Config.bufferoverrun || Config.quandaryBO
; active= Config.(is_checker_enabled BufferOverrun || is_checker_enabled QuandaryBO)
; callbacks=
[ (Procedure BufferOverrunChecker.checker, Language.Clang)
; (Procedure BufferOverrunChecker.checker, Language.Java) ] }
; { name= "eradicate"
; active= Config.eradicate
; active= Config.is_checker_enabled Eradicate
; callbacks= [(Procedure Eradicate.callback_eradicate, Language.Java)] }
; { name= "fragment retains view"
; active= Config.fragment_retains_view
; active= Config.is_checker_enabled FragmentRetainsView
; callbacks=
[(Procedure FragmentRetainsViewChecker.callback_fragment_retains_view, Language.Java)] }
; { name= "immutable cast"
; active= Config.immutable_cast
; active= Config.is_checker_enabled ImmutableCast
; callbacks= [(Procedure ImmutableChecker.callback_check_immutable_cast, Language.Java)] }
; { name= "inefficient keyset iterator"
; active= Config.inefficient_keyset_iterator
; active= Config.is_checker_enabled InefficientKeysetIterator
; callbacks= [(Procedure InefficientKeysetIterator.checker, Language.Java)] }
; { name= "liveness"
; active= Config.liveness
; active= Config.is_checker_enabled Liveness
; callbacks= [(Procedure Liveness.checker, Language.Clang)] }
; { name= "printf args"
; active= Config.printf_args
; active= Config.is_checker_enabled PrintfArgs
; callbacks= [(Procedure PrintfArgs.callback_printf_args, Language.Java)] }
; { name= "impurity"
; active= Config.impurity
; active= Config.is_checker_enabled Impurity
; callbacks=
[(Procedure Impurity.checker, Language.Java); (Procedure Impurity.checker, Language.Clang)]
}
; { name= "pulse"
; active= Config.pulse || Config.impurity
; active= Config.(is_checker_enabled Pulse || is_checker_enabled Impurity)
; callbacks=
(Procedure Pulse.checker, Language.Clang)
:: (if Config.impurity then [(Procedure Pulse.checker, Language.Java)] else []) }
::
( if Config.is_checker_enabled Impurity then [(Procedure Pulse.checker, Language.Java)]
else [] ) }
; { name= "quandary"
; active= Config.quandary || Config.quandaryBO
; active= Config.(is_checker_enabled Quandary || is_checker_enabled QuandaryBO)
; callbacks=
[ (Procedure JavaTaintAnalysis.checker, Language.Java)
; (Procedure ClangTaintAnalysis.checker, Language.Clang) ] }
; { name= "RacerD"
; active= Config.racerd
; active= Config.is_checker_enabled RacerD
; callbacks=
[ (Procedure RacerD.analyze_procedure, Language.Clang)
; (Procedure RacerD.analyze_procedure, Language.Java)
@ -97,30 +101,35 @@ let all_checkers =
, Language.Java ) ] }
(* toy resource analysis to use in the infer lab, see the lab/ directory *)
; { name= "resource leak"
; active= Config.resource_leak
; active= Config.is_checker_enabled ResourceLeak
; callbacks=
[ ( (* the checked-in version is intraprocedural, but the lab asks to make it
interprocedural later on *)
Procedure ResourceLeaks.checker
, Language.Java ) ] }
; { name= "litho-required-props"
; active= Config.litho_required_props
; active= Config.is_checker_enabled LithoRequiredProps
; callbacks= [(Procedure RequiredProps.checker, Language.Java)] }
; {name= "SIOF"; active= Config.siof; callbacks= [(Procedure Siof.checker, Language.Clang)]}
; { name= "SIOF"
; active= Config.is_checker_enabled SIOF
; callbacks= [(Procedure Siof.checker, Language.Clang)] }
; { name= "uninitialized variables"
; active= Config.uninit
; active= Config.is_checker_enabled Uninit
; callbacks= [(Procedure Uninit.checker, Language.Clang)] }
; { name= "cost analysis"
; active= Config.cost || (Config.loop_hoisting && Config.hoisting_report_only_expensive)
; active=
Config.(
is_checker_enabled Cost
|| (is_checker_enabled LoopHoisting && hoisting_report_only_expensive))
; callbacks= [(Procedure Cost.checker, Language.Clang); (Procedure Cost.checker, Language.Java)]
}
; { name= "loop hoisting"
; active= Config.loop_hoisting
; active= Config.is_checker_enabled LoopHoisting
; callbacks=
[(Procedure Hoisting.checker, Language.Clang); (Procedure Hoisting.checker, Language.Java)]
}
; { name= "Starvation analysis"
; active= Config.starvation
; active= Config.is_checker_enabled Starvation
; callbacks=
[ (Procedure Starvation.analyze_procedure, Language.Java)
; ( File {callback= Starvation.reporting; issue_dir= Config.starvation_issues_dir_name}
@ -129,14 +138,14 @@ let all_checkers =
; ( File {callback= Starvation.reporting; issue_dir= Config.starvation_issues_dir_name}
, Language.Clang ) ] }
; { name= "purity"
; active= Config.purity || Config.loop_hoisting
; active= Config.(is_checker_enabled Purity || is_checker_enabled LoopHoisting)
; callbacks=
[(Procedure Purity.checker, Language.Java); (Procedure Purity.checker, Language.Clang)] }
; { name= "Class loading analysis"
; active= Config.class_loads
; active= Config.is_checker_enabled ClassLoads
; callbacks= [(Procedure ClassLoads.analyze_procedure, Language.Java)] }
; { name= "Self captured in block checker"
; active= Config.self_in_block
; active= Config.is_checker_enabled SelfInBlock
; callbacks= [(Procedure SelfInBlock.checker, Language.Clang)] } ]

@ -27,7 +27,7 @@ let validate_decl_from_channel chan =
let register_perf_stats_report source_file =
let stats_type =
if Config.capture then PerfStats.ClangFrontend source_file
else if Config.linters then PerfStats.ClangLinters source_file
else if Config.is_checker_enabled Linters then PerfStats.ClangLinters source_file
else if Config.process_clang_ast then PerfStats.ClangProcessAST source_file
else
Logging.(die UserError)
@ -96,7 +96,7 @@ let run_clang_frontend ast_source =
ClangPointers.populate_all_tables ast_decl ;
L.(debug Capture Medium)
"Start %s the AST of %a@\n" Config.clang_frontend_action_string pp_ast_filename ast_source ;
if Config.linters then AL.do_frontend_checks trans_unit_ctx ast_decl ;
if Config.is_checker_enabled Linters then AL.do_frontend_checks trans_unit_ctx ast_decl ;
if Config.process_clang_ast then ProcessAST.process_ast trans_unit_ctx ast_decl ;
if Config.capture then CFrontend.do_source_file trans_unit_ctx ast_decl ;
L.(debug Capture Medium)

@ -175,7 +175,9 @@ let clang_cc1_cmd_sanitizer cmd =
arg
in
let args_defines =
if Config.bufferoverrun && not Config.biabduction then ["-D__INFER_BUFFEROVERRUN"] else []
if Config.is_checker_enabled BufferOverrun && not (Config.is_checker_enabled Biabduction) then
["-D__INFER_BUFFEROVERRUN"]
else []
in
let explicit_sysroot_passed = has_flag cmd "-isysroot" in
(* supply isysroot only when SDKROOT is not set up and explicit isysroot is not provided,

@ -17,7 +17,7 @@ Format.sprintf
(ocamlopt_flags (%s))
(libraries %s)
(modules All_infer_in_one_file)
(preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
(preprocess (pps ppx_compare ppx_enumerate ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check))
)
|}
(String.concat " " common_cflags)

@ -529,7 +529,7 @@ let mode_of_build_command build_cmd (buck_mode : BuckMode.t option) =
error_no_buck_mode_specified ()
| BBuck, Some (ClangCompilationDB deps) ->
BuckCompilationDB (deps, prog, List.append args (List.rev Config.buck_build_args))
| BBuck, Some ClangFlavors when Config.linters ->
| BBuck, Some ClangFlavors when Config.is_checker_enabled Linters ->
L.user_warning
"WARNING: the linters require --buck-compilation-database to be set.@ Alternatively, \
set --no-linters to disable them and this warning.@." ;

@ -119,8 +119,8 @@ let update_issues all_issues =
List.filter
~f:(fun issue ->
let issue_in ls = List.mem ls issue.Issue.err_key.err_name ~equal:IssueType.equal in
(Config.quandary || not (issue_in quandary_issues))
&& (Config.bufferoverrun || not (issue_in inferbo_issues))
(Config.is_checker_enabled Quandary || not (issue_in quandary_issues))
&& (Config.is_checker_enabled BufferOverrun || not (issue_in inferbo_issues))
&& not (issue_in filtered_issues) )
all_issues
in

@ -41,6 +41,7 @@ depends: [
"parmap" {>="1.0-rc8"}
"ppx_compare" {>= "v0.13.0" & < "v0.14"}
"ppx_deriving" {>="4.1"}
"ppx_enumerate" {>="v0.13.0" & < "v0.14"}
"ppx_fields_conv" {>="v0.13.0" & < "v0.14"}
"sawja" {>="1.5.8"}
"sqlite3"

Loading…
Cancel
Save