From 94ff44ed57a7a2d082bf89bc39e821654724ccea Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Fri, 8 Sep 2017 14:09:32 -0700 Subject: [PATCH] [infer][biabduction] add skipped functions to the trace when known Summary: With this diff, the analysis trace will jump to the definition of the skipped methods when the location is known. This is especially useful when the analysis is relying on the method annotations. Reviewed By: sblackshear Differential Revision: D5783428 fbshipit-source-id: 561b739 --- infer/src/backend/paths.ml | 23 +++++++++++++------ infer/src/backend/paths.mli | 4 ++-- infer/src/backend/symExec.ml | 7 +++++- infer/tests/build_systems/buck/issues.exp | 2 +- .../tests/codetoanalyze/java/infer/issues.exp | 2 +- 5 files changed, 26 insertions(+), 12 deletions(-) diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index 37c5ab2aa..1f985259c 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -26,8 +26,8 @@ module Path : sig val add_call : bool -> t -> Typ.Procname.t -> t -> t (** add a call with its sub-path, the boolean indicates whether the subtrace for the procedure should be included *) - val add_skipped_call : t -> Typ.Procname.t -> string -> t - (** add a call to a procname that's had to be skipped, along with the reason *) + val add_skipped_call : t -> Typ.Procname.t -> string -> Location.t option -> t + (** add a call to a procname that's had to be skipped, along with the reason and the location of the procname when known *) val contains : t -> t -> bool (** check whether a path contains another path *) @@ -99,7 +99,7 @@ end = struct let compare__string_option _ _ = 0 type _path_exec = - | ExecSkipped of string (** call was skipped with a reason *) + | ExecSkipped of string * Location.t option (** call was skipped with a reason *) | ExecCompleted of t (** call was completed *) and t = @@ -153,7 +153,8 @@ end = struct let add_call include_subtrace p pname p_sub = if include_subtrace then Pcall (p, pname, ExecCompleted p_sub, get_dummy_stats ()) else p - let add_skipped_call p pname reason = Pcall (p, pname, ExecSkipped reason, get_dummy_stats ()) + let add_skipped_call p pname reason loc_opt = + Pcall (p, pname, ExecSkipped (reason, loc_opt), get_dummy_stats ()) (** functions in this module either do not assume, or do not re-establish, the invariant on dummy stats *) @@ -419,7 +420,7 @@ end = struct -> F.fprintf fmt "(%a + %a)" (doit (n - 1)) path1 (doit (n - 1)) path2 | Pcall (path1, _, ExecCompleted path2, _) -> F.fprintf fmt "(%a{%a})" (doit (n - 1)) path1 (doit (n - 1)) path2 - | Pcall (path, _, ExecSkipped reason, _) + | Pcall (path, _, ExecSkipped (reason, _), _) -> F.fprintf fmt "(%a: %s)" (doit (n - 1)) path reason in let print_delayed () = @@ -443,13 +444,21 @@ end = struct let trace = ref [] in let g level path _ exn_opt = match (path, curr_node path) with - | Pcall (_, pname, ExecSkipped reason, _), Some curr_node + | Pcall (_, pname, ExecSkipped (reason, loc_opt), _), Some curr_node -> let curr_loc = Procdesc.Node.get_loc curr_node in let descr = Format.sprintf "Skipping %s: %s" (Typ.Procname.to_simplified_string pname) reason in let node_tags = [] in - trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace + trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace ; + Option.iter + ~f:(fun loc -> + if Typ.Procname.is_java pname && loc.Location.line > 0 then + let definition_descr = + Format.sprintf "Definition of %s" (Typ.Procname.to_simplified_string pname) + in + trace := Errlog.make_trace_element (level + 1) loc definition_descr [] :: !trace) + loc_opt | _, Some curr_node -> ( let curr_loc = Procdesc.Node.get_loc curr_node in diff --git a/infer/src/backend/paths.mli b/infer/src/backend/paths.mli index 4625d58a8..f37e383d6 100644 --- a/infer/src/backend/paths.mli +++ b/infer/src/backend/paths.mli @@ -21,8 +21,8 @@ module Path : sig val add_call : bool -> t -> Typ.Procname.t -> t -> t (** add a call with its sub-path, the boolean indicates whether the subtrace for the procedure should be included *) - val add_skipped_call : t -> Typ.Procname.t -> string -> t - (** add a call to a procname that's had to be skipped, along with the reason *) + val add_skipped_call : t -> Typ.Procname.t -> string -> Location.t option -> t + (** add a call to a procname that's had to be skipped, along with the reason and the location of the procname when known *) val contains : t -> t -> bool (** check whether a path contains another path *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 7a8787be9..c98159e90 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1596,7 +1596,12 @@ and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots Attribute.mark_vars_as_undefined tenv pre_final ~ret_exp_opt ~undefined_actuals_by_ref callee_pname ret_annots loc path_pos in - let skip_path = Paths.Path.add_skipped_call path callee_pname reason in + let callee_loc_opt = + Option.map + ~f:(fun attributes -> attributes.ProcAttributes.loc) + (Specs.proc_resolve_attributes callee_pname) + in + let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in [(prop_with_undef_attr, skip_path)] and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos) diff --git a/infer/tests/build_systems/buck/issues.exp b/infer/tests/build_systems/buck/issues.exp index 603b0f30f..fe0074f42 100644 --- a/infer/tests/build_systems/buck/issues.exp +++ b/infer/tests/build_systems/buck/issues.exp @@ -1,5 +1,5 @@ infer/tests/build_systems/genrule/module1/Class1.java, void Class1.localNPE1(), 2, NULL_DEREFERENCE, [start of procedure localNPE1()] -infer/tests/build_systems/genrule/module2/Class2.java, void Class2.followMethodDeclarationOnlyBad(SkipImplementationClass1), 2, NULL_DEREFERENCE, [start of procedure followMethodDeclarationOnlyBad(...),Skipping annotatedNullable(): method has no implementation] +infer/tests/build_systems/genrule/module2/Class2.java, void Class2.followMethodDeclarationOnlyBad(SkipImplementationClass1), 2, NULL_DEREFERENCE, [start of procedure followMethodDeclarationOnlyBad(...),Skipping annotatedNullable(): method has no implementation,Definition of annotatedNullable()] infer/tests/build_systems/genrule/module2/Class2.java, void Class2.interTargetAbstractNPE(Class1), 2, NULL_DEREFERENCE, [start of procedure interTargetAbstractNPE(...),Skipping abstractMayReturnNull(): abstract method] infer/tests/build_systems/genrule/module2/Class2.java, void Class2.interTargetNPE(), 2, NULL_DEREFERENCE, [start of procedure interTargetNPE(),start of procedure returnsNull(),return from a call to String Class1.returnsNull()] infer/tests/build_systems/genrule/module2/Class2.java, void Class2.interTargetNativeNPE(Class1), 2, NULL_DEREFERENCE, [start of procedure interTargetNativeNPE(...),Skipping nativeMayReturnNull(): method has no implementation] diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index d85221241..2502e7b64 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -16,7 +16,7 @@ codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipFunctionInLo codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(), 2, DIVIDE_BY_ZERO, [start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero()] codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(), 2, DIVIDE_BY_ZERO, [start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...)] codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(), 3, DIVIDE_BY_ZERO, [start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method] -codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 26, DIVIDE_BY_ZERO, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetObj(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to Object AnalysisStops.skipPointerDerefPreventsSpecInferenceRetObj(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),return from a call to void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...),return from a call to void AnalysisStops.divideByParam(int),return from a call to void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),return from a call to void AnalysisStops.castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),Skipping toString(): unknown method,return from a call to void AnalysisStops.callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,start of procedure retZero(),return from a call to int AnalysisStops$MyObj.retZero(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure retOne(),return from a call to int AnalysisStops$MyObj.retOne(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldWriteOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldWriteOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldReadOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldReadOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalsePositive(),start of procedure recursiveAngelicTypesMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.recursiveAngelicTypesMayCauseFalseNegative(),Skipping recursiveAngelicTypesMayCauseFalsePositive(): empty list of specs,start of procedure infiniteMaterializationMayCauseFalseNegative(...),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalseNegative(boolean),start of procedure infiniteMaterializationMayCauseFalsePositive(...),Skipping externalFunc2(): method has no implementation,Taking false branch,Skipping toString(): unknown method,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalsePositive(boolean),start of procedure primitiveFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalsePositive(),start of procedure primitiveFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalseNegative(),start of procedure heapFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalsePositive(),start of procedure heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping fieldReadAferCastMayCauseFalseNegative(...): empty list of specs,start of procedure fieldReadInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeMayCauseFalsePositive(),start of procedure fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),start of procedure accessPathInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure accessPathOnParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.accessPathOnParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.accessPathInCalleeMayCauseFalsePositive()] +codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 26, DIVIDE_BY_ZERO, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetObj(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to Object AnalysisStops.skipPointerDerefPreventsSpecInferenceRetObj(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),return from a call to void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...),return from a call to void AnalysisStops.divideByParam(int),return from a call to void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),return from a call to void AnalysisStops.castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),Skipping toString(): unknown method,return from a call to void AnalysisStops.callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,start of procedure retZero(),return from a call to int AnalysisStops$MyObj.retZero(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure retOne(),return from a call to int AnalysisStops$MyObj.retOne(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldWriteOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldWriteOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldReadOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldReadOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalsePositive(),start of procedure recursiveAngelicTypesMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.recursiveAngelicTypesMayCauseFalseNegative(),Skipping recursiveAngelicTypesMayCauseFalsePositive(): empty list of specs,Definition of recursiveAngelicTypesMayCauseFalsePositive(),start of procedure infiniteMaterializationMayCauseFalseNegative(...),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalseNegative(boolean),start of procedure infiniteMaterializationMayCauseFalsePositive(...),Skipping externalFunc2(): method has no implementation,Taking false branch,Skipping toString(): unknown method,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalsePositive(boolean),start of procedure primitiveFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalsePositive(),start of procedure primitiveFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalseNegative(),start of procedure heapFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalsePositive(),start of procedure heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping fieldReadAferCastMayCauseFalseNegative(...): empty list of specs,Definition of fieldReadAferCastMayCauseFalseNegative(...),start of procedure fieldReadInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeMayCauseFalsePositive(),start of procedure fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),start of procedure accessPathInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure accessPathOnParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.accessPathOnParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.accessPathInCalleeMayCauseFalsePositive()] codetoanalyze/java/infer/ArrayOutOfBounds.java, int ArrayOutOfBounds.arrayOutOfBounds(), 2, ARRAY_OUT_OF_BOUNDS_L1, [start of procedure arrayOutOfBounds()] codetoanalyze/java/infer/Builtins.java, void Builtins.causeError(Object), 2, NULL_DEREFERENCE, [start of procedure causeError(...),Taking true branch] codetoanalyze/java/infer/Builtins.java, void Builtins.doNotBlockError(Object), 3, NULL_DEREFERENCE, [start of procedure doNotBlockError(...),Taking true branch]