pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

explicit inter-checker dependencies

Browse Source 
Summary:
Before: `RegisterCheckers` activates each checker based on a boolean
condition about which other checkers can enable it, eg for pulse:
```
(* registerCheckers.ml *)
active= Config.(is_checker_enabled Pulse || is_checker_enabled Impurity)
```

After: `Checker` declares for each checker the list of its dependencies,
eg for impurity:
```
(* Checker.ml *)
  name= "impurity";
  activates= [Pulse]
```

Now `Config` computes for each checker whether it was transitively
activated by other checkers or not. It saves us from having to encode
the logic from before everywhere we want to know "is checker X
running?"; this was prone to errors.

It will also allow us to display which checkers actually run to the user
more easily.

Reviewed By: ezgicicek

Differential Revision: D21622198

fbshipit-source-id: 004931192
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent 2bbd25087c
commit 248eaf87c7
6 changed files with 277 additions and 232 deletions
Show Stats Download Patch File Download Diff File

96
infer/src/backend/registerCheckers.ml
Unescape View File

@ -71,30 +71,23 @@ let intraprocedural_with_field_dependency payload_field checker =
Procedure (CallbackOfChecker.intraprocedural_with_field_dependency payload_field checker) Procedure (CallbackOfChecker.intraprocedural_with_field_dependency payload_field checker)
type callback = callback_fun * Language.t type checker = {checker: Checker.t; callbacks: (callback_fun * Language.t) list}
type checker = {name: string; active: bool; callbacks: callback list}
let all_checkers = let all_checkers =
(* The order of the list is important for those checkers that depend on other checkers having run (* The order of the list is important for those checkers that depend on other checkers having run
before them. *) before them. *)
[ { name= "Self captured in block checker" [ {checker= SelfInBlock; callbacks= [(intraprocedural SelfInBlock.checker, Clang)]}
; active= Config.is_checker_enabled SelfInBlock ; { checker= ClassLoads
; callbacks= [(intraprocedural SelfInBlock.checker, Clang)] }
; { name= "Class loading analysis"
; active= Config.is_checker_enabled ClassLoads
; callbacks= [(interprocedural Payloads.Fields.class_loads ClassLoads.analyze_procedure, Java)] ; callbacks= [(interprocedural Payloads.Fields.class_loads ClassLoads.analyze_procedure, Java)]
} }
; { name= "purity" ; { checker= Purity
; active= Config.(is_checker_enabled Purity || is_checker_enabled LoopHoisting)
; callbacks= ; callbacks=
(let purity = (let purity =
interprocedural2 Payloads.Fields.purity Payloads.Fields.buffer_overrun_analysis interprocedural2 Payloads.Fields.purity Payloads.Fields.buffer_overrun_analysis
Purity.checker Purity.checker
in in
[(purity, Java); (purity, Clang)] ) } [(purity, Java); (purity, Clang)] ) }
; { name= "Starvation analysis" ; { checker= Starvation
; active= Config.is_checker_enabled Starvation
; callbacks= ; callbacks=
(let starvation = interprocedural Payloads.Fields.starvation Starvation.analyze_procedure in (let starvation = interprocedural Payloads.Fields.starvation Starvation.analyze_procedure in
let starvation_file_reporting = let starvation_file_reporting =
@ -104,8 +97,7 @@ let all_checkers =
; (starvation_file_reporting, Java) ; (starvation_file_reporting, Java)
; (starvation, Clang) ; (starvation, Clang)
; (starvation_file_reporting, Clang) ] ) } ; (starvation_file_reporting, Clang) ] ) }
; { name= "loop hoisting" ; { checker= LoopHoisting
; active= Config.is_checker_enabled LoopHoisting
; callbacks= ; callbacks=
(let hoisting = (let hoisting =
interprocedural3 interprocedural3
@ -115,102 +107,74 @@ let all_checkers =
Hoisting.checker Hoisting.checker
in in
[(hoisting, Clang); (hoisting, Java)] ) } [(hoisting, Clang); (hoisting, Java)] ) }
; { name= "cost analysis" ; { checker= Cost
; active=
Config.(
is_checker_enabled Cost
|| (is_checker_enabled LoopHoisting && hoisting_report_only_expensive))
; callbacks= ; callbacks=
(let checker = (let checker =
interprocedural3 ~set_payload:(Field.fset Payloads.Fields.cost) Payloads.Fields.cost interprocedural3 ~set_payload:(Field.fset Payloads.Fields.cost) Payloads.Fields.cost
Payloads.Fields.buffer_overrun_analysis Payloads.Fields.purity Cost.checker Payloads.Fields.buffer_overrun_analysis Payloads.Fields.purity Cost.checker
in in
[(checker, Clang); (checker, Java)] ) } [(checker, Clang); (checker, Java)] ) }
; { name= "uninitialized variables" ; {checker= Uninit; callbacks= [(interprocedural Payloads.Fields.uninit Uninit.checker, Clang)]}
; active= Config.is_checker_enabled Uninit ; {checker= SIOF; callbacks= [(interprocedural Payloads.Fields.siof Siof.checker, Clang)]}
; callbacks= [(interprocedural Payloads.Fields.uninit Uninit.checker, Clang)] } ; { checker= LithoRequiredProps
; { name= "SIOF"
; active= Config.is_checker_enabled SIOF
; callbacks= [(interprocedural Payloads.Fields.siof Siof.checker, Clang)] }
; { name= "litho-required-props"
; active= Config.is_checker_enabled LithoRequiredProps
; callbacks= [(interprocedural Payloads.Fields.litho_required_props RequiredProps.checker, Java)] ; callbacks= [(interprocedural Payloads.Fields.litho_required_props RequiredProps.checker, Java)]
} }
; (* toy resource analysis to use in the infer lab, see the lab/ directory *) ; (* toy resource analysis to use in the infer lab, see the lab/ directory *)
{ name= "resource leak" { checker= ResourceLeakLabExercise
; active= Config.is_checker_enabled ResourceLeakLabExercise
; callbacks= ; callbacks=
[ ( (* the checked-in version is intraprocedural, but the lab asks to make it [ ( (* the checked-in version is intraprocedural, but the lab asks to make it
interprocedural later on *) interprocedural later on *)
interprocedural Payloads.Fields.lab_resource_leaks ResourceLeaks.checker interprocedural Payloads.Fields.lab_resource_leaks ResourceLeaks.checker
, Java ) ] } , Java ) ] }
; { name= "RacerD" ; { checker= RacerD
; active= Config.is_checker_enabled RacerD
; callbacks= ; callbacks=
(let racerd_proc = interprocedural Payloads.Fields.racerd RacerD.analyze_procedure in (let racerd_proc = interprocedural Payloads.Fields.racerd RacerD.analyze_procedure in
let racerd_file = file RacerDIssues Payloads.Fields.racerd RacerD.file_analysis in let racerd_file = file RacerDIssues Payloads.Fields.racerd RacerD.file_analysis in
[(racerd_proc, Clang); (racerd_proc, Java); (racerd_file, Clang); (racerd_file, Java)] ) } [(racerd_proc, Clang); (racerd_proc, Java); (racerd_file, Clang); (racerd_file, Java)] ) }
; { name= "quandary" ; { checker= Quandary
; active= Config.(is_checker_enabled Quandary)
; callbacks= ; callbacks=
[ (interprocedural Payloads.Fields.quandary JavaTaintAnalysis.checker, Java) [ (interprocedural Payloads.Fields.quandary JavaTaintAnalysis.checker, Java)
; (interprocedural Payloads.Fields.quandary ClangTaintAnalysis.checker, Clang) ] } ; (interprocedural Payloads.Fields.quandary ClangTaintAnalysis.checker, Clang) ] }
; { name= "pulse" ; { checker= Pulse
; active= Config.(is_checker_enabled Pulse || is_checker_enabled Impurity)
; callbacks= ; callbacks=
(let pulse = interprocedural Payloads.Fields.pulse Pulse.checker in (let pulse = interprocedural Payloads.Fields.pulse Pulse.checker in
[(pulse, Clang); (pulse, Java)] ) } [(pulse, Clang); (pulse, Java)] ) }
; { name= "impurity" ; { checker= Impurity
; active= Config.is_checker_enabled Impurity
; callbacks= ; callbacks=
(let impurity = (let impurity =
intraprocedural_with_field_dependency Payloads.Fields.pulse Impurity.checker intraprocedural_with_field_dependency Payloads.Fields.pulse Impurity.checker
in in
[(impurity, Java); (impurity, Clang)] ) } [(impurity, Java); (impurity, Clang)] ) }
; { name= "printf args" ; {checker= PrintfArgs; callbacks= [(intraprocedural PrintfArgs.checker, Java)]}
; active= Config.is_checker_enabled PrintfArgs ; {checker= Liveness; callbacks= [(intraprocedural Liveness.checker, Clang)]}
; callbacks= [(intraprocedural PrintfArgs.checker, Java)] } ; { checker= InefficientKeysetIterator
; { name= "liveness"
; active= Config.is_checker_enabled Liveness
; callbacks= [(intraprocedural Liveness.checker, Clang)] }
; { name= "inefficient keyset iterator"
; active= Config.is_checker_enabled InefficientKeysetIterator
; callbacks= [(intraprocedural InefficientKeysetIterator.checker, Java)] } ; callbacks= [(intraprocedural InefficientKeysetIterator.checker, Java)] }
; { name= "immutable cast" ; { checker= ImmutableCast
; active= Config.is_checker_enabled ImmutableCast
; callbacks= ; callbacks=
[(intraprocedural_with_payload Payloads.Fields.nullsafe ImmutableChecker.analyze, Java)] } [(intraprocedural_with_payload Payloads.Fields.nullsafe ImmutableChecker.analyze, Java)] }
; { name= "fragment retains view" ; { checker= FragmentRetainsView
; active= Config.is_checker_enabled FragmentRetainsView
; callbacks= [(intraprocedural FragmentRetainsViewChecker.callback_fragment_retains_view, Java)] ; callbacks= [(intraprocedural FragmentRetainsViewChecker.callback_fragment_retains_view, Java)]
} }
; { name= "eradicate" ; { checker= Eradicate
; active= Config.is_checker_enabled Eradicate
; callbacks= ; callbacks=
[ (intraprocedural_with_payload Payloads.Fields.nullsafe Eradicate.analyze_procedure, Java) [ (intraprocedural_with_payload Payloads.Fields.nullsafe Eradicate.analyze_procedure, Java)
; (file NullsafeFileIssues Payloads.Fields.nullsafe FileLevelAnalysis.analyze_file, Java) ] ; (file NullsafeFileIssues Payloads.Fields.nullsafe FileLevelAnalysis.analyze_file, Java) ]
} }
; { name= "buffer overrun checker" ; { checker= BufferOverrunChecker
; active= Config.(is_checker_enabled BufferOverrun)
; callbacks= ; callbacks=
(let bo_checker = (let bo_checker =
interprocedural2 Payloads.Fields.buffer_overrun_checker interprocedural2 Payloads.Fields.buffer_overrun_checker
Payloads.Fields.buffer_overrun_analysis BufferOverrunChecker.checker Payloads.Fields.buffer_overrun_analysis BufferOverrunChecker.checker
in in
[(bo_checker, Clang); (bo_checker, Java)] ) } [(bo_checker, Clang); (bo_checker, Java)] ) }
; { name= "buffer overrun analysis" ; { checker= BufferOverrunAnalysis
; active=
Config.(
is_checker_enabled BufferOverrun || is_checker_enabled Cost
|| is_checker_enabled LoopHoisting || is_checker_enabled Purity)
; callbacks= ; callbacks=
(let bo_analysis = (let bo_analysis =
interprocedural Payloads.Fields.buffer_overrun_analysis interprocedural Payloads.Fields.buffer_overrun_analysis
BufferOverrunAnalysis.analyze_procedure BufferOverrunAnalysis.analyze_procedure
in in
[(bo_analysis, Clang); (bo_analysis, Java)] ) } [(bo_analysis, Clang); (bo_analysis, Java)] ) }
; { name= "biabduction" ; { checker= Biabduction
; active= Config.(is_checker_enabled Biabduction || is_checker_enabled TOPL)
; callbacks= ; callbacks=
(let biabduction = (let biabduction =
dynamic_dispatch Payloads.Fields.biabduction dynamic_dispatch Payloads.Fields.biabduction
@ -219,8 +183,7 @@ let all_checkers =
else Interproc.analyze_procedure ) else Interproc.analyze_procedure )
in in
[(biabduction, Clang); (biabduction, Java)] ) } [(biabduction, Clang); (biabduction, Java)] ) }
; { name= "annotation reachability" ; { checker= AnnotationReachability
; active= Config.is_checker_enabled AnnotationReachability
; callbacks= ; callbacks=
(let annot_reach = (let annot_reach =
interprocedural Payloads.Fields.annot_map AnnotationReachability.checker interprocedural Payloads.Fields.annot_map AnnotationReachability.checker
@ -229,12 +192,13 @@ let all_checkers =
let get_active_checkers () = let get_active_checkers () =
let filter_checker {active} = active in let filter_checker {checker} = Config.is_checker_enabled checker in
List.filter ~f:filter_checker all_checkers List.filter ~f:filter_checker all_checkers
let register checkers = let register checkers =
let register_one {name; callbacks} = let register_one {checker; callbacks} =
let name = (Checker.config checker).name in
let register_callback (callback, language) = let register_callback (callback, language) =
match callback with match callback with
| Procedure procedure_cb -> | Procedure procedure_cb ->
@ -252,12 +216,12 @@ let register checkers =
module LanguageSet = Caml.Set.Make (Language) module LanguageSet = Caml.Set.Make (Language)
let pp_checker fmt {name; callbacks} = let pp_checker fmt {checker; callbacks} =
let langs_of_callbacks = let langs_of_callbacks =
List.fold_left callbacks ~init:LanguageSet.empty ~f:(fun langs (_, lang) -> List.fold_left callbacks ~init:LanguageSet.empty ~f:(fun langs (_, lang) ->
LanguageSet.add lang langs ) LanguageSet.add lang langs )
|> LanguageSet.elements |> LanguageSet.elements
in in
F.fprintf fmt "%s (%a)" name F.fprintf fmt "%s (%a)" (Checker.config checker).name
(Pp.seq ~sep:", " (Pp.of_string ~f:Language.to_string)) (Pp.seq ~sep:", " (Pp.of_string ~f:Language.to_string))
langs_of_callbacks langs_of_callbacks

236
infer/src/base/Checker.ml
Unescape View File

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

23
infer/src/base/Checker.mli
Unescape View File

@ -10,7 +10,8 @@ open! IStd
type t = type t =
| AnnotationReachability | AnnotationReachability
| Biabduction | Biabduction
| BufferOverrun | BufferOverrunAnalysis
| BufferOverrunChecker
| ClassLoads | ClassLoads
| Cost | Cost
| Eradicate | Eradicate
@ -45,15 +46,21 @@ type support =
(** the checker is for teaching purposes only (like experimental but with no plans to improve (** the checker is for teaching purposes only (like experimental but with no plans to improve
it) *) it) *)
type cli_flags =
{ long: string
(** The flag to enable this option on the command line, without the leading "--" (like the
[~long] argument of {!CommandLineOption} functions). *)
; deprecated: string list
(** More command-line flags, similar to [~deprecated] arguments in {!CommandLineOption}. *)
; show_in_help: bool }
type config = type config =
{ support: Language.t -> support { name: string
; support: Language.t -> support
; short_documentation: string ; short_documentation: string
; cli_flag: string ; cli_flags: cli_flags option
(** the flag to enable this option on the command line, without the leading "--" (like the (** If [None] then the checker cannot be enabled/disabled from the command line. *)
[~long] argument of [CommandLineOption] functions) *)
; show_in_help: bool
; enabled_by_default: bool ; enabled_by_default: bool
; cli_deprecated_flags: string list ; activates: t list (** TODO doc *) }
(** more command-line flags, similar to [~deprecated] arguments *) }
val config : t -> config val config : t -> config

95
infer/src/base/Config.ml
Unescape View File

@ -531,34 +531,41 @@ and analyzer =
instance, to enable only the biabduction analysis, run with $(b,--biabduction-only)." instance, to enable only the biabduction analysis, run with $(b,--biabduction-only)."
and _checkers = (* checkers *)
and () =
let open Checker in let open Checker in
let in_analyze_help = InferCommand.[(Analyze, manual_generic)] in let in_analyze_help = InferCommand.[(Analyze, manual_generic)] in
let mk_checker ?f checker = let mk_checker ?f checker =
let config = Checker.config checker in let config = Checker.config checker in
let in_help = if config.show_in_help then in_analyze_help else [] in
let var = let var =
CLOpt.mk_bool ?f ~long:config.cli_flag ~in_help ~default:config.enabled_by_default match config.cli_flags with
~deprecated:config.cli_deprecated_flags config.short_documentation | None ->
(* HACK: return a constant ref if the checker cannot be enabled/disabled from the command line *)
ref config.enabled_by_default
| Some {long; deprecated; show_in_help} ->
let in_help = if show_in_help then in_analyze_help else [] in
CLOpt.mk_bool ?f ~long ~in_help ~default:config.enabled_by_default ~deprecated
config.short_documentation
in in
all_checkers := (checker, config, var) :: !all_checkers all_checkers := (checker, config, var) :: !all_checkers
in in
List.iter Checker.all ~f:mk_checker ; List.iter Checker.all ~f:mk_checker ;
let mk_only (_checker, config, var) = let mk_only (_checker, config, var) =
let (_ : bool ref) = Option.iter config.cli_flags ~f:(fun {long; show_in_help} ->
CLOpt.mk_bool_group ~long:(config.cli_flag ^ "-only") let (_ : bool ref) =
~in_help:InferCommand.[(Analyze, manual_generic)] CLOpt.mk_bool_group ~long:(long ^ "-only")
~f:(fun b -> ~in_help:InferCommand.[(Analyze, manual_generic)]
disable_all_checkers () ; ~f:(fun b ->
var := b ; disable_all_checkers () ;
b ) var := b ;
( if config.show_in_help then b )
Printf.sprintf "Enable $(b,--%s) and disable all other checkers" config.cli_flag ( if show_in_help then
else "" ) Printf.sprintf "Enable $(b,--%s) and disable all other checkers" long
[] (* do all the work in ~f *) [] else "" )
(* do all the work in ~f *) [] (* do all the work in ~f *) []
in (* do all the work in ~f *)
() in
() )
in in
List.iter ~f:mk_only !all_checkers ; List.iter ~f:mk_only !all_checkers ;
let _default_checkers : bool ref = let _default_checkers : bool ref =
@ -568,8 +575,11 @@ and _checkers =
( "Default checkers: " ( "Default checkers: "
^ ( List.rev_filter_map ^ ( List.rev_filter_map
~f:(fun (_, config, _) -> ~f:(fun (_, config, _) ->
if config.enabled_by_default then Some (Printf.sprintf "$(b,--%s)" config.cli_flag) match config.cli_flags with
else None ) | Some {long} when config.enabled_by_default ->
Some (Printf.sprintf "$(b,--%s)" long)
| _ ->
None )
!all_checkers !all_checkers
|> String.concat ~sep:", " ) ) |> String.concat ~sep:", " ) )
~f:(fun b -> ~f:(fun b ->
@ -3101,10 +3111,47 @@ and xcpretty = !xcpretty
(** Configuration values derived from command-line options *) (** Configuration values derived from command-line options *)
let is_checker_enabled c = let mem_checkers enabled_checkers (c : Checker.t) = List.mem ~equal:Checker.equal enabled_checkers c
List.find_map_exn checkers ~f:(fun (checker, enabled) ->
if Checker.equal checker c then Some enabled else None ) let enabled_checkers =
(* invariant: [newly_enabled_checkers] is *included* in [enabled_checkers] and [enabled_checkers]
has at most one occurrence of each checker.
NOTE: the complexity of this is quadratic in the number of checkers but this is fine as we
don't have hundreds of checkers (yet). Also we have few dependencies and shallow dependency
chains so we don't even get close to the worst case. *)
let rec fixpoint newly_enabled_checkers enabled_checkers =
let newly_enabled_checkers, enabled_checkers' =
List.fold newly_enabled_checkers ~init:([], enabled_checkers)
~f:(fun (newly_enabled_checkers, enabled_checkers) checker ->
let to_enable =
(Checker.config checker).activates
|> List.filter ~f:(fun checker_dep -> not (mem_checkers enabled_checkers checker_dep))
in
match to_enable with
| [] ->
(newly_enabled_checkers, enabled_checkers)
| _ :: _ ->
(to_enable @ newly_enabled_checkers, to_enable @ enabled_checkers) )
in
if List.is_empty newly_enabled_checkers then enabled_checkers
else fixpoint newly_enabled_checkers enabled_checkers'
in
let enabled_checkers =
let enabled0 =
List.filter_map checkers ~f:(fun (checker, active) -> if active then Some checker else None)
in
fixpoint enabled0 enabled0
in
if
hoisting_report_only_expensive
&& mem_checkers enabled_checkers LoopHoisting
&& not (mem_checkers enabled_checkers Cost)
then fixpoint [Checker.Cost] (Checker.Cost :: enabled_checkers)
else enabled_checkers
let is_checker_enabled c = mem_checkers enabled_checkers c
let clang_frontend_action_string = let clang_frontend_action_string =
let text = if capture then ["translating"] else [] in let text = if capture then ["translating"] else [] in
@ -3123,7 +3170,7 @@ let clang_frontend_action_string =
a call to unknown code and true triggers lazy dynamic dispatch. The latter mode follows the 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 JVM semantics and creates procedure descriptions during symbolic execution using the type
information found in the abstract state *) information found in the abstract state *)
let dynamic_dispatch = is_checker_enabled Biabduction || is_checker_enabled TOPL let dynamic_dispatch = is_checker_enabled Biabduction
(** Check if a Java package is external to the repository *) (** Check if a Java package is external to the repository *)
let java_package_is_external package = let java_package_is_external package =

57
infer/src/base/IssueType.ml
Unescape View File

@ -137,23 +137,29 @@ let assert_failure = register_from_string ~id:"Assert_failure" [Biabduction]
let bad_footprint = register_from_string ~id:"Bad_footprint" [Biabduction] let bad_footprint = register_from_string ~id:"Bad_footprint" [Biabduction]
let buffer_overrun_l1 = register_from_string ~id:"BUFFER_OVERRUN_L1" [BufferOverrun] let buffer_overrun_l1 = register_from_string ~id:"BUFFER_OVERRUN_L1" [BufferOverrunChecker]
let buffer_overrun_l2 = register_from_string ~id:"BUFFER_OVERRUN_L2" [BufferOverrun] let buffer_overrun_l2 = register_from_string ~id:"BUFFER_OVERRUN_L2" [BufferOverrunChecker]
let buffer_overrun_l3 = register_from_string ~id:"BUFFER_OVERRUN_L3" [BufferOverrun] let buffer_overrun_l3 = register_from_string ~id:"BUFFER_OVERRUN_L3" [BufferOverrunChecker]
let buffer_overrun_l4 = register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_L4" [BufferOverrun] let buffer_overrun_l4 =
register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_L4" [BufferOverrunChecker]
let buffer_overrun_l5 = register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_L5" [BufferOverrun]
let buffer_overrun_r2 = register_from_string ~id:"BUFFER_OVERRUN_R2" [BufferOverrun] let buffer_overrun_l5 =
register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_L5" [BufferOverrunChecker]
let buffer_overrun_s2 = register_from_string ~id:"BUFFER_OVERRUN_S2" [BufferOverrun]
let buffer_overrun_t1 = register_from_string ~id:"BUFFER_OVERRUN_T1" [BufferOverrun] let buffer_overrun_r2 = register_from_string ~id:"BUFFER_OVERRUN_R2" [BufferOverrunChecker]
let buffer_overrun_s2 = register_from_string ~id:"BUFFER_OVERRUN_S2" [BufferOverrunChecker]
let buffer_overrun_t1 = register_from_string ~id:"BUFFER_OVERRUN_T1" [BufferOverrunChecker]
let buffer_overrun_u5 =
register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_U5" [BufferOverrunChecker]
let buffer_overrun_u5 = register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_U5" [BufferOverrun]
let cannot_star = register_from_string ~id:"Cannot_star" [Biabduction] let cannot_star = register_from_string ~id:"Cannot_star" [Biabduction]
@ -219,11 +225,12 @@ let component_with_unconventional_superclass =
let condition_always_false = let condition_always_false =
register_from_string ~enabled:false ~id:"CONDITION_ALWAYS_FALSE" [Biabduction; BufferOverrun] register_from_string ~enabled:false ~id:"CONDITION_ALWAYS_FALSE"
[Biabduction; BufferOverrunChecker]
let condition_always_true = let condition_always_true =
register_from_string ~enabled:false ~id:"CONDITION_ALWAYS_TRUE" [Biabduction; BufferOverrun] register_from_string ~enabled:false ~id:"CONDITION_ALWAYS_TRUE" [Biabduction; BufferOverrunChecker]
let constant_address_dereference = let constant_address_dereference =
@ -379,20 +386,24 @@ let inefficient_keyset_iterator =
register_from_string ~id:"INEFFICIENT_KEYSET_ITERATOR" [InefficientKeysetIterator] register_from_string ~id:"INEFFICIENT_KEYSET_ITERATOR" [InefficientKeysetIterator]
let inferbo_alloc_is_big = register_from_string ~id:"INFERBO_ALLOC_IS_BIG" [BufferOverrun] let inferbo_alloc_is_big = register_from_string ~id:"INFERBO_ALLOC_IS_BIG" [BufferOverrunChecker]
let inferbo_alloc_is_negative =
register_from_string ~id:"INFERBO_ALLOC_IS_NEGATIVE" [BufferOverrunChecker]
let inferbo_alloc_is_negative = register_from_string ~id:"INFERBO_ALLOC_IS_NEGATIVE" [BufferOverrun] let inferbo_alloc_is_zero = register_from_string ~id:"INFERBO_ALLOC_IS_ZERO" [BufferOverrunChecker]
let inferbo_alloc_is_zero = register_from_string ~id:"INFERBO_ALLOC_IS_ZERO" [BufferOverrun] let inferbo_alloc_may_be_big =
register_from_string ~id:"INFERBO_ALLOC_MAY_BE_BIG" [BufferOverrunChecker]
let inferbo_alloc_may_be_big = register_from_string ~id:"INFERBO_ALLOC_MAY_BE_BIG" [BufferOverrun]
let inferbo_alloc_may_be_negative = let inferbo_alloc_may_be_negative =
register_from_string ~id:"INFERBO_ALLOC_MAY_BE_NEGATIVE" [BufferOverrun] register_from_string ~id:"INFERBO_ALLOC_MAY_BE_NEGATIVE" [BufferOverrunChecker]
let inferbo_alloc_may_be_tainted = let inferbo_alloc_may_be_tainted =
register_from_string ~id:"INFERBO_ALLOC_MAY_BE_TAINTED" [BufferOverrun] register_from_string ~id:"INFERBO_ALLOC_MAY_BE_TAINTED" [BufferOverrunChecker]
let infinite_cost_call ~kind = register_from_cost_string ~enabled:false "INFINITE_%s" ~kind let infinite_cost_call ~kind = register_from_cost_string ~enabled:false "INFINITE_%s" ~kind
@ -403,18 +414,18 @@ let inherently_dangerous_function =
let insecure_intent_handling = register_from_string ~id:"INSECURE_INTENT_HANDLING" [Quandary] let insecure_intent_handling = register_from_string ~id:"INSECURE_INTENT_HANDLING" [Quandary]
let integer_overflow_l1 = register_from_string ~id:"INTEGER_OVERFLOW_L1" [BufferOverrun] let integer_overflow_l1 = register_from_string ~id:"INTEGER_OVERFLOW_L1" [BufferOverrunChecker]
let integer_overflow_l2 = register_from_string ~id:"INTEGER_OVERFLOW_L2" [BufferOverrun] let integer_overflow_l2 = register_from_string ~id:"INTEGER_OVERFLOW_L2" [BufferOverrunChecker]
let integer_overflow_l5 = let integer_overflow_l5 =
register_from_string ~enabled:false ~id:"INTEGER_OVERFLOW_L5" [BufferOverrun] register_from_string ~enabled:false ~id:"INTEGER_OVERFLOW_L5" [BufferOverrunChecker]
let integer_overflow_r2 = register_from_string ~id:"INTEGER_OVERFLOW_R2" [BufferOverrun] let integer_overflow_r2 = register_from_string ~id:"INTEGER_OVERFLOW_R2" [BufferOverrunChecker]
let integer_overflow_u5 = let integer_overflow_u5 =
register_from_string ~enabled:false ~id:"INTEGER_OVERFLOW_U5" [BufferOverrun] register_from_string ~enabled:false ~id:"INTEGER_OVERFLOW_U5" [BufferOverrunChecker]
let interface_not_thread_safe = register_from_string ~id:"INTERFACE_NOT_THREAD_SAFE" [RacerD] let interface_not_thread_safe = register_from_string ~id:"INTERFACE_NOT_THREAD_SAFE" [RacerD]
@ -544,7 +555,7 @@ let unary_minus_applied_to_unsigned_expression =
let uninitialized_value = register_from_string ~id:"UNINITIALIZED_VALUE" [Uninit] let uninitialized_value = register_from_string ~id:"UNINITIALIZED_VALUE" [Uninit]
let unreachable_code_after = register_from_string ~id:"UNREACHABLE_CODE" [BufferOverrun] let unreachable_code_after = register_from_string ~id:"UNREACHABLE_CODE" [BufferOverrunChecker]
let use_after_delete = register_from_string ~id:"USE_AFTER_DELETE" [Pulse] let use_after_delete = register_from_string ~id:"USE_AFTER_DELETE" [Pulse]

2
infer/src/biabduction/errdesc.ml
Unescape View File

@ -135,7 +135,7 @@ let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t opti
in in
Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags)) Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags))
| Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Var id0} | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Var id0}
when Config.(is_checker_enabled Biabduction || is_checker_enabled TOPL) when Config.is_checker_enabled Biabduction
&& Ident.equal id id0 && Ident.equal id id0
&& not (Pvar.is_frontend_tmp pvar) -> && not (Pvar.is_frontend_tmp pvar) ->
(* this case is a hack to make bucketing continue to work in the presence of copy (* this case is a hack to make bucketing continue to work in the presence of copy

Write Preview
Loading…
Cancel
Save