[infer] always run all the pre-analysis passes independently form the checkers that are being run

Summary:
It seems that the abstraction instructions were not previously added the the CFG.

This is a functional changes to make sure that the abstraction state is always added. We can simplify the code later and just run this step before storing the CFG instead of after loading them.

Reviewed By: sblackshear, jvillard

Differential Revision: D6383672

fbshipit-source-id: cedcb8a
master
Jeremy Dubreil 7 years ago committed by Facebook Github Bot
parent ca3f71a8b3
commit 7b8a5a1a2b

@ -614,4 +614,3 @@ let pp_proc_signatures fmt cfg =
F.fprintf fmt "METHOD SIGNATURES@\n@." ;
let sorted_procs = List.sort ~cmp:Procdesc.compare (get_all_procs cfg) in
List.iter ~f:(fun pdesc -> F.fprintf fmt "%a@." Procdesc.pp_signature pdesc) sorted_procs

@ -95,7 +95,7 @@ struct
module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig))
let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial =
if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv ;
Preanal.do_preanalysis pdesc None tenv ;
let initial' = (initial, IdAccessPathMapDomain.empty) in
Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial')

@ -1341,10 +1341,7 @@ let perform_transition proc_cfg tenv proc_name =
let analyze_procedure_aux cg_opt tenv proc_desc =
let proc_name = Procdesc.get_proc_name proc_desc in
let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
if not (Procdesc.did_preanalysis proc_desc) then (
Preanal.do_liveness proc_desc tenv ;
Preanal.do_abstraction proc_desc ;
Option.iter cg_opt ~f:(fun cg -> Preanal.do_dynamic_dispatch proc_desc cg tenv) ) ;
Preanal.do_preanalysis proc_desc cg_opt tenv ;
let summaryfp = Config.run_in_footprint_mode (analyze_proc tenv) proc_cfg in
Specs.add_summary proc_name summaryfp ;
perform_transition proc_cfg tenv proc_name ;

@ -237,6 +237,8 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
node_add_nullify_instructions exit_node (AddressTaken.Domain.elements address_taken_vars)
(** perform liveness analysis and insert Nullify/Remove_temps instructions into the IR to make it
easy for analyses to do abstract garbage collection *)
let do_liveness pdesc tenv =
let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in
let initial = Liveness.Domain.empty in
@ -249,11 +251,14 @@ let do_liveness pdesc tenv =
Procdesc.signal_did_preanalysis pdesc
(** add Abstract instructions into the IR to give hints about when abstraction should be
performed *)
let do_abstraction pdesc =
add_abstraction_instructions pdesc ;
Procdesc.signal_did_preanalysis pdesc
(** add possible dynamic dispatch targets to the call_flags of each call site *)
let do_dynamic_dispatch pdesc cg tenv =
( match Config.dynamic_dispatch with
| Interface | Sound ->
@ -263,3 +268,10 @@ let do_dynamic_dispatch pdesc cg tenv =
() ) ;
Procdesc.signal_did_preanalysis pdesc
let do_preanalysis pdesc cg_opt tenv =
if not (Procdesc.did_preanalysis pdesc) then (
do_liveness pdesc tenv ;
do_abstraction pdesc ;
Option.iter cg_opt ~f:(fun cg -> do_dynamic_dispatch pdesc cg tenv) )

@ -10,15 +10,5 @@
open! IStd
val do_preanalysis : Procdesc.t -> Cg.t option -> Tenv.t -> unit
(** Various preanalysis passes for transforming the IR in useful ways *)
val do_liveness : Procdesc.t -> Tenv.t -> unit
(** perform liveness analysis and insert Nullify/Remove_temps instructions into the IR to make it
easy for analyses to do abstract garbage collection *)
val do_abstraction : Procdesc.t -> unit
(** add Abstract instructions into the IR to give hints about when abstraction should be
performed *)
val do_dynamic_dispatch : Procdesc.t -> Cg.t -> Tenv.t -> unit
(** add possible dynamic dispatch targets to the call_flags of each call site *)

@ -535,11 +535,10 @@ let checker : Callbacks.proc_callback_args -> Specs.summary =
fun {proc_desc; tenv; summary; get_proc_desc} ->
let proc_name = Specs.get_proc_name summary in
let proc_data = ProcData.make proc_desc tenv get_proc_desc in
if not (Procdesc.did_preanalysis proc_desc) then Preanal.do_liveness proc_desc tenv ;
Preanal.do_preanalysis proc_desc None tenv ;
match compute_post proc_data with
| Some post ->
if Config.bo_debug >= 1 then print_summary proc_name post ;
Summary.update_summary post summary
| None ->
summary

@ -1,6 +1,6 @@
codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.fieldReadInCalleeMayCauseFalseNegative(), 3, NULL_DEREFERENCE, [start of procedure fieldReadInCalleeMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Definition of externalFunc2(),start of procedure derefParam(...),Skipping toString(): unknown method]
codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.fieldReadInCalleeWithAngelicObjFieldMayCauseFalseNegative(), 3, NULL_DEREFERENCE, [start of procedure fieldReadInCalleeWithAngelicObjFieldMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Definition of externalFunc2(),start of procedure derefParam(...),Skipping toString(): unknown method]
codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipFunctionInLoopMayCauseFalseNegative(), 5, NULL_DEREFERENCE, [start of procedure skipFunctionInLoopMayCauseFalseNegative(),Taking true branch,Skipping externalFunc(): method has no implementation,Definition of externalFunc(),Taking true branch,Skipping externalFunc(): method has no implementation,Definition of externalFunc(),Taking false branch]
codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipFunctionInLoopMayCauseFalseNegative(), 5, NULL_DEREFERENCE, [start of procedure skipFunctionInLoopMayCauseFalseNegative(),Taking true branch,Skipping externalFunc(): method has no implementation,Definition of externalFunc(),Taking false branch]
codetoanalyze/java/infer/AutoGenerated.java, void AutoGenerated.npe(), 2, NULL_DEREFERENCE, [start of procedure npe()]
codetoanalyze/java/infer/Builtins.java, void Builtins.doNotBlockError(Object), 3, NULL_DEREFERENCE, [start of procedure doNotBlockError(...),Taking true branch]
codetoanalyze/java/infer/CloseableAsResourceExample.java, T CloseableAsResourceExample.sourceOfNullWithResourceLeak(), 1, RESOURCE_LEAK, [start of procedure sourceOfNullWithResourceLeak(),start of procedure SomeResource(),return from a call to SomeResource.<init>()]
@ -17,12 +17,12 @@ codetoanalyze/java/infer/ContextLeaks.java, void ContextLeaks.directLeak(), 2, C
codetoanalyze/java/infer/ContextLeaks.java, void ContextLeaks.indirectLeak(), 4, CONTEXT_LEAK, [start of procedure indirectLeak(),start of procedure ContextLeaks$Obj(),return from a call to ContextLeaks$Obj.<init>(),return from a call to void ContextLeaks.indirectLeak()]
codetoanalyze/java/infer/ContextLeaks.java, void ContextLeaks.leakAfterInstanceFieldWrite(), 3, CONTEXT_LEAK, [start of procedure leakAfterInstanceFieldWrite(),return from a call to void ContextLeaks.leakAfterInstanceFieldWrite()]
codetoanalyze/java/infer/ContextLeaks.java, void ContextLeaks.nonStaticInnerClassLeak(), 2, CONTEXT_LEAK, [start of procedure nonStaticInnerClassLeak(),start of procedure ContextLeaks$NonStaticInner(...),return from a call to ContextLeaks$NonStaticInner.<init>(ContextLeaks),return from a call to void ContextLeaks.nonStaticInnerClassLeak()]
codetoanalyze/java/infer/CursorLeaks.java, Object CursorLeaks.cursorClosedCheckNullCheckClosed_FP(SQLiteDatabase), 17, RESOURCE_LEAK, [start of procedure cursorClosedCheckNullCheckClosed_FP(...),Taking false branch,Skipping getString(...): unknown method,Taking true branch,Taking false branch]
codetoanalyze/java/infer/CursorLeaks.java, Object CursorLeaks.cursorClosedCheckNullCheckClosed_FP(SQLiteDatabase), 13, RESOURCE_LEAK, [start of procedure cursorClosedCheckNullCheckClosed_FP(...),Taking false branch,Skipping getString(...): unknown method,Taking true branch,Taking false branch]
codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.completeDownloadNotClosed(DownloadManager), 8, RESOURCE_LEAK, [start of procedure completeDownloadNotClosed(...),Taking false branch,Skipping getColumnIndex(...): unknown method]
codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.cursorNotClosed(SQLiteDatabase), 4, RESOURCE_LEAK, [start of procedure cursorNotClosed(...),Skipping getCount(): unknown method]
codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.getBucketCountNotClosed(), 10, RESOURCE_LEAK, [start of procedure getBucketCountNotClosed(),Taking false branch,Taking false branch]
codetoanalyze/java/infer/CursorLeaks.java, int CursorLeaks.getImageCountHelperNotClosed(String), 13, RESOURCE_LEAK, [start of procedure getImageCountHelperNotClosed(...),Taking true branch,Skipping getInt(...): unknown method]
codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.loadPrefsFromContentProviderNotClosed(), 15, RESOURCE_LEAK, [start of procedure loadPrefsFromContentProviderNotClosed(),Taking false branch,Taking true branch,return from a call to void CursorLeaks.loadPrefsFromContentProviderNotClosed()]
codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.loadPrefsFromContentProviderNotClosed(), 11, RESOURCE_LEAK, [start of procedure loadPrefsFromContentProviderNotClosed(),Taking false branch,Taking true branch]
codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.queryUVMLegacyDbNotClosed(), 4, RESOURCE_LEAK, [start of procedure queryUVMLegacyDbNotClosed(),Skipping setTables(...): unknown method,Taking true branch]
codetoanalyze/java/infer/CursorNPEs.java, int CursorNPEs.cursorFromDownloadManagerNPE(DownloadManager), 5, NULL_DEREFERENCE, [start of procedure cursorFromDownloadManagerNPE(...)]
codetoanalyze/java/infer/CursorNPEs.java, void CursorNPEs.cursorFromContentResolverNPE(String), 12, NULL_DEREFERENCE, [start of procedure cursorFromContentResolverNPE(...)]
@ -123,6 +123,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.
codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNullableRet(boolean), 2, NULL_DEREFERENCE, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)]
codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefUndefNullableRet(), 2, NULL_DEREFERENCE, [start of procedure derefUndefNullableRet(),Skipping undefNullableRet(): method has no implementation,Definition of undefNullableRet()]
codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefUndefNullableRetWrapper(), 1, NULL_DEREFERENCE, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): method has no implementation,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper()]
codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L), 2, NULL_DEREFERENCE, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock1(Lock), 4, NULL_DEREFERENCE, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method]
codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock2(Lock), 6, NULL_DEREFERENCE, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method]
codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullDerefernceReturnOfSkippedFunctionBad(), 3, NULL_DEREFERENCE, [start of procedure nullDerefernceReturnOfSkippedFunctionBad(),Skipping unknownFunc(): method has no implementation,Definition of unknownFunc(),Taking true branch]
@ -164,8 +165,8 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.deflaterLeak(),
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileInputStreamNotClosedAfterRead(), 6, RESOURCE_LEAK, [start of procedure fileInputStreamNotClosedAfterRead(),exception java.io.IOException]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamNotClosed(), 1, RESOURCE_LEAK, [start of procedure fileOutputStreamNotClosed()]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamNotClosedAfterWrite(), 7, RESOURCE_LEAK, [start of procedure fileOutputStreamNotClosedAfterWrite(),exception java.io.IOException]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamOneLeak(), 5, RESOURCE_LEAK, [start of procedure fileOutputStreamOneLeak(),Taking true branch,return from a call to void ResourceLeaks.fileOutputStreamOneLeak()]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamTwoLeaks2(), 5, RESOURCE_LEAK, [start of procedure fileOutputStreamTwoLeaks2(),Taking true branch]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamOneLeak(), 2, RESOURCE_LEAK, [start of procedure fileOutputStreamOneLeak(),Taking true branch]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamTwoLeaks2(), 2, RESOURCE_LEAK, [start of procedure fileOutputStreamTwoLeaks2(),Taking true branch]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.fileOutputStreamTwoLeaks2(), 5, RESOURCE_LEAK, [start of procedure fileOutputStreamTwoLeaks2(),Taking true branch]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.inflaterLeak(), 1, RESOURCE_LEAK, [start of procedure inflaterLeak()]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.jarInputStreamLeak(), 3, RESOURCE_LEAK, [start of procedure jarInputStreamLeak()]
@ -187,6 +188,7 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.parseFromStringA
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.pipedInputStreamNotClosedAfterRead(PipedOutputStream), 6, RESOURCE_LEAK, [start of procedure pipedInputStreamNotClosedAfterRead(...),exception java.io.IOException]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.pipedOutputStreamNotClosedAfterWrite(), 7, RESOURCE_LEAK, [start of procedure pipedOutputStreamNotClosedAfterWrite(),exception java.io.IOException]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.scannerNotClosed(), 1, RESOURCE_LEAK, [start of procedure scannerNotClosed()]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.serverSocketNotClosed(), 12, RESOURCE_LEAK, [start of procedure serverSocketNotClosed(),Skipping ServerSocket(...): unknown method,exception java.io.IOException]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.socketNotClosed(), 1, RESOURCE_LEAK, [start of procedure socketNotClosed()]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.themeObtainTypedArrayAndLeak(Resources$Theme), 2, RESOURCE_LEAK, [start of procedure themeObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(TypedArray)]
codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResources(), 11, RESOURCE_LEAK, [start of procedure twoResources(),Taking true branch,exception java.io.IOException]

@ -78,6 +78,8 @@ codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRU
codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
codetoanalyze/c/bufferoverrun/unreachable.c, FP_exit_at_end_of_proc_good, 2, UNREACHABLE_CODE, []
codetoanalyze/c/bufferoverrun/unreachable.c, FP_exit_at_end_of_proc_good_local_var, 2, UNREACHABLE_CODE, []
codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, []
codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, []
codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_exit_good, 1, CONDITION_ALWAYS_TRUE, []

@ -41,12 +41,12 @@ void exit_at_end_of_if_good() {
}
}
void exit_at_end_of_proc_good() {
void FP_exit_at_end_of_proc_good() {
nop();
exit(5);
}
void exit_at_end_of_proc_good_local_var() {
void FP_exit_at_end_of_proc_good_local_var() {
int a = 57;
exit(5);
}

@ -41,4 +41,4 @@ codetoanalyze/cpp/nullable/method.cpp, reportsViolationInNullBranchBad, 2, NULL_
codetoanalyze/cpp/nullable/method.cpp, reportsViolationOutsideOfNullCheckBad, 1, NULL_TEST_AFTER_DEREFERENCE, [start of procedure reportsViolationOutsideOfNullCheckBad(),start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is false]
codetoanalyze/cpp/nullable/method.cpp, reportsViolationOutsideOfNullCheckBad, 2, NULL_DEREFERENCE, [start of procedure reportsViolationOutsideOfNullCheckBad(),start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is true,start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject]
codetoanalyze/cpp/nullable/method.cpp, reportsViolationOutsideOfNullCheckBad, 4, NULLABLE_DEREFERENCE, [dereferencing the return of mayReturnNullObject,definition of mayReturnNullObject]
codetoanalyze/cpp/nullable/method.cpp, reportsViolationOutsideOfNullCheckBad, 4, NULL_DEREFERENCE, [start of procedure reportsViolationOutsideOfNullCheckBad(),start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is true,start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,start of procedure doSomething,return from a call to T_doSomething,start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject]
codetoanalyze/cpp/nullable/method.cpp, reportsViolationOutsideOfNullCheckBad, 4, NULL_DEREFERENCE, [start of procedure reportsViolationOutsideOfNullCheckBad(),start of procedure mayReturnNullObject,Condition is true,return from a call to T_mayReturnNullObject,Condition is false,start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject]

Loading…
Cancel
Save