From 281385203f115620a7c7a5087970719cf2fb93ca Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 20 Feb 2020 05:19:31 -0800 Subject: [PATCH] [biabduction] kill guarded by check Summary: RacerD now has a check for this, so remove. Reviewed By: jberdine Differential Revision: D19974163 fbshipit-source-id: 06d7a203d --- infer/man/man1/infer-full.txt | 1 - infer/man/man1/infer-report.txt | 1 - infer/man/man1/infer.txt | 1 - infer/src/IR/Exceptions.ml | 9 - infer/src/IR/Exceptions.mli | 2 - infer/src/IR/Localise.ml | 19 - infer/src/IR/Localise.mli | 2 - infer/src/base/Config.ml | 3 - infer/src/base/Config.mli | 2 - infer/src/base/IssueType.ml | 2 - infer/src/base/IssueType.mli | 2 - infer/src/biabduction/Rearrange.ml | 346 +----------------- infer/src/checkers/annotations.mli | 3 - infer/tests/build_systems/ant/issues.exp | 20 - .../tests/codetoanalyze/java/infer/issues.exp | 20 - 15 files changed, 3 insertions(+), 430 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index a4f188ea6..84ce7666c 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -498,7 +498,6 @@ OPTIONS default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), - UNSAFE_GUARDED_BY_ACCESS (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), UNTRUSTED_DESERIALIZATION (enabled by default), UNTRUSTED_DESERIALIZATION_RISK (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index ba673e29f..1a99d07e5 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -227,7 +227,6 @@ OPTIONS default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), - UNSAFE_GUARDED_BY_ACCESS (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), UNTRUSTED_DESERIALIZATION (enabled by default), UNTRUSTED_DESERIALIZATION_RISK (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index acc09c056..3c7a763b8 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -498,7 +498,6 @@ OPTIONS default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), - UNSAFE_GUARDED_BY_ACCESS (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), UNTRUSTED_DESERIALIZATION (enabled by default), UNTRUSTED_DESERIALIZATION_RISK (enabled by default), diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 9bbcfb44f..e36caea7c 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -126,8 +126,6 @@ exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * L. exception Unknown_proc -exception Unsafe_guarded_by_access of Localise.error_desc * L.ocaml_pos - exception Wrong_argument_number of L.ocaml_pos type t = @@ -525,13 +523,6 @@ let recognize_exception exn = ; visibility= Exn_developer ; severity= None ; category= Nocat } - | Unsafe_guarded_by_access (desc, ocaml_pos) -> - { name= IssueType.unsafe_guarded_by_access - ; description= desc - ; ocaml_pos= Some ocaml_pos - ; visibility= Exn_user - ; severity= None - ; category= Prover } | Wrong_argument_number ocaml_pos -> { name= IssueType.wrong_argument_number ; description= Localise.no_desc diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index cf2e52c89..a5ad3ae0f 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -128,8 +128,6 @@ exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * Lo exception Unknown_proc -exception Unsafe_guarded_by_access of Localise.error_desc * Logging.ocaml_pos - exception Wrong_argument_number of Logging.ocaml_pos val severity_string : severity -> string diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 8c4aa76b2..dc03bea13 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -309,25 +309,6 @@ let deref_str_array_bound size_opt index_opt = ; problem_str= "could be accessed with " ^ index_str ^ " out of bounds" } -let desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc = - let line_info = at_line (Tags.create ()) loc in - let accessed_fld_str = Fieldname.to_string accessed_fld in - let annot_str = Printf.sprintf "@GuardedBy(\"%s\")" guarded_by_str in - let syncronized_str = - MF.monospaced_to_string (Printf.sprintf "synchronized(%s)" guarded_by_str) - in - let msg = - Format.asprintf - "The field %a is annotated with %a, but the lock %a is not held during the access to the \ - field %s. Since the current method is non-private, it can be called from outside the \ - current class without synchronization. Consider wrapping the access in a %s block or making \ - the method private." - MF.pp_monospaced accessed_fld_str MF.pp_monospaced annot_str MF.pp_monospaced guarded_by_str - line_info syncronized_str - in - {no_desc with descriptions= [msg]} - - let desc_custom_error loc : error_desc = {no_desc with descriptions= ["detected"; at_line (Tags.create ()) loc]} diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index ae019758c..561883115 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -158,8 +158,6 @@ val desc_inherently_dangerous_function : Procname.t -> error_desc val desc_unary_minus_applied_to_unsigned_expression : string option -> string -> Location.t -> error_desc -val desc_unsafe_guarded_by_access : Fieldname.t -> string -> Location.t -> error_desc - val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc val access_desc : access option -> string list diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index fdc222366..ac43eb31d 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -168,9 +168,6 @@ let classnames_dir_name = "classnames" let costs_report_json = "costs-report.json" -(** Experimental: if true do some specialized analysis of concurrent constructs. *) -let csl_analysis = true - let default_failure_name = "ASSERTION_FAILURE" let default_in_zip_results_dir = "infer" diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index ade54831f..b39520d6d 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -71,8 +71,6 @@ val classpath : string option val costs_report_json : string -val csl_analysis : bool - val default_failure_name : string val default_in_zip_results_dir : string diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 3bb1e20b0..5549a2568 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -468,8 +468,6 @@ let unknown_proc = register_from_string "Unknown_proc" ~hum:"Unknown Procedure" let unreachable_code_after = register_from_string "UNREACHABLE_CODE" -let unsafe_guarded_by_access = register_from_string "UNSAFE_GUARDED_BY_ACCESS" - let use_after_delete = register_from_string "USE_AFTER_DELETE" let use_after_free = register_from_string "USE_AFTER_FREE" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 259c99401..574c75aa0 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -320,8 +320,6 @@ val unknown_proc : t val unreachable_code_after : t -val unsafe_guarded_by_access : t - val use_after_delete : t val use_after_free : t diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 489350972..1ce79d0b5 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -701,336 +701,6 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst = Prop.prop_iter_set_state iter offsets_default -(** If [lexp] is an access to a field that is annotated with @GuardedBy, add constraints to [prop] - expressing the safety conditions for the access. Complain if these conditions cannot be met. *) -let add_guarded_by_constraints tenv prop lexp pdesc = - let lookup = Tenv.lookup tenv in - let pname = Procdesc.get_proc_name pdesc in - let excluded_guardedby_string str = - (* nothing with a space in it can be a valid Java expression, shouldn't warn *) - let is_invalid_exp_str str = String.contains str ' ' in - (* don't warn on @GuardedBy("ui_thread") in any form *) - let is_ui_thread str = - let lowercase_str = String.lowercase str in - String.equal lowercase_str "ui_thread" - || String.equal lowercase_str "ui-thread" - || String.equal lowercase_str "uithread" - in - is_invalid_exp_str str || is_ui_thread str - in - let guarded_by_str_is_this guarded_by_str = String.is_suffix ~suffix:"this" guarded_by_str in - let guarded_by_str_is_class guarded_by_str class_str = - let dollar_normalize s = String.map s ~f:(function '$' -> '.' | c -> c) in - String.is_suffix ~suffix:(dollar_normalize guarded_by_str) - (dollar_normalize (class_str ^ ".class")) - in - let guarded_by_str_is_current_class guarded_by_str = function - | Procname.Java java_pname -> - (* programmers write @GuardedBy("MyClass.class") when the field is guarded by the class *) - guarded_by_str_is_class guarded_by_str (Procname.Java.get_class_name java_pname) - | _ -> - false - in - let guarded_by_str_is_class_this class_name guarded_by_str = - let fully_qualified_this = Printf.sprintf "%s.this" class_name in - String.is_suffix ~suffix:guarded_by_str fully_qualified_this - in - (* return true if [guarded_by_str] is a suffix of ".this" *) - let guarded_by_str_is_super_class_this guarded_by_str pname = - match pname with - | Procname.Java java_pname -> - let current_class_type_name = Procname.Java.get_class_type_name java_pname in - let comparison class_type_name _ = - guarded_by_str_is_class_this (Typ.Name.to_string class_type_name) guarded_by_str - in - PatternMatch.supertype_exists tenv comparison current_class_type_name - | _ -> - false - in - (* return true if [guarded_by_str] is as suffix of ".this" *) - let guarded_by_str_is_current_class_this guarded_by_str = function - | Procname.Java java_pname -> - guarded_by_str_is_class_this (Procname.Java.get_class_name java_pname) guarded_by_str - | _ -> - false - in - let extract_guarded_by_str item_annot = - let annot_extract_guarded_by_str ((annot : Annot.t), _) = - if Annotations.annot_ends_with annot Annotations.guarded_by then - match annot.parameters with - | [Annot.{value= Str guarded_by_str}] when not (excluded_guardedby_string guarded_by_str) -> - Some guarded_by_str - | _ -> - None - else None - in - List.find_map ~f:annot_extract_guarded_by_str item_annot - in - let extract_suppress_warnings_str item_annot = - let annot_suppress_warnings_str ((annot : Annot.t), _) = - if Annotations.annot_ends_with annot Annotations.suppress_lint then - (* TODO: @SuppressLint's param is an array of strings, thus we need to match on - array. But generally logic here is still broken since it only expects 1 value. *) - match annot.parameters with - | [Annot.{value= Array [Str suppr_str; _]}] -> - Some suppr_str - | _ -> - None - else None - in - List.find_map ~f:annot_suppress_warnings_str item_annot - in - (* if [fld] is annotated with @GuardedBy("mLock"), return mLock *) - let get_guarded_by_fld_str fld typ = - match Struct.get_field_type_and_annotation ~lookup fld typ with - | Some (_, item_annot) -> ( - match extract_guarded_by_str item_annot with - | Some "this" -> - (* expand "this" into .this *) - Some (Printf.sprintf "%s.this" (Typ.Name.name (Fieldname.get_class_name fld))) - | guarded_by_str_opt -> - guarded_by_str_opt ) - | _ -> - None - in - (* find A.guarded_by_fld_str |-> B and return Some B, or None if there is no such hpred *) - let find_guarded_by_exp guarded_by_str0 sigma = - let is_guarded_by_fld guarded_by_str fld _ = - (* this comparison needs to be somewhat fuzzy, since programmers are free to write - @GuardedBy("mLock"), @GuardedBy("MyClass.mLock"), or use other conventions *) - String.equal (Fieldname.get_field_name fld) guarded_by_str - || String.equal (Fieldname.to_string fld) guarded_by_str - in - let get_fld_strexp_and_typ typ f flds = - let match_one (fld, strexp) = - match Struct.get_field_type_and_annotation ~lookup fld typ with - | Some (fld_typ, _) when f fld fld_typ -> - Some (strexp, fld_typ) - | _ -> - None - in - List.find_map ~f:match_one flds - in - (* sometimes, programmers will write @GuardedBy("T.f") with the meaning "guarded by the field f - of the object of type T in the current state." note that this is ambiguous when there are - multiple objects of type T, but let's try to respect the intention *) - let match_on_field_type typ flds = - match String.rsplit2 guarded_by_str0 ~on:'.' with - | Some (class_part, field_part) -> ( - let typ_matches_guarded_by _ {Typ.desc} = - match desc with - | Typ.Tptr (ptr_typ, _) -> - String.is_suffix ~suffix:class_part (Typ.to_string ptr_typ) - | _ -> - false - in - match get_fld_strexp_and_typ typ typ_matches_guarded_by flds with - | Some (Predicates.Eexp (matching_exp, _), _) -> - List.find_map - ~f:(function - | Predicates.Hpointsto (lhs_exp, Estruct (matching_flds, _), Sizeof {typ= fld_typ}) - when Exp.equal lhs_exp matching_exp -> - get_fld_strexp_and_typ fld_typ (is_guarded_by_fld field_part) matching_flds - | _ -> - None ) - sigma - | _ -> - None ) - | _ -> - None - in - List.find_map - ~f:(fun hpred -> - (* FIXME: silenced warning may be legit *) - match[@warning "-57"] hpred with - | Predicates.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof {typ}) - | Predicates.Hpointsto - (_, Predicates.Eexp ((Const (Cclass clazz) as lhs_exp), _), Exp.Sizeof {typ}) - when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) -> - Some (Predicates.Eexp (lhs_exp, Predicates.inst_none), typ) - | Predicates.Hpointsto (_, Estruct (flds, _), Exp.Sizeof {typ}) -> ( - (* first, try to find a field that exactly matches the guarded-by string *) - match get_fld_strexp_and_typ typ (is_guarded_by_fld guarded_by_str0) flds with - | None when guarded_by_str_is_this guarded_by_str0 -> - (* if the guarded-by string is "OuterClass.this", look for "this$n" for some n. - note that this is a bit sketchy when there are mutliple this$n's, but there's - nothing we can do to disambiguate them. *) - get_fld_strexp_and_typ typ (fun f _ -> Fieldname.is_java_outer_instance f) flds - | None -> - (* can't find an exact match. try a different convention. *) - match_on_field_type typ flds - | Some _ as res_opt -> - res_opt ) - | Predicates.Hpointsto (Lvar pvar, rhs_exp, Exp.Sizeof {typ}) - when ( guarded_by_str_is_current_class_this guarded_by_str0 pname - || guarded_by_str_is_super_class_this guarded_by_str0 pname ) - && Pvar.is_this pvar -> - Some (rhs_exp, typ) - | _ -> - None ) - sigma - in - (* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *) - let enforce_guarded_access_ accessed_fld guarded_by_str prop = - (* return true if [pdesc] has an annotation that matches [guarded_by_str] *) - let proc_has_matching_annot pdesc guarded_by_str = - match extract_guarded_by_str (Annotations.pdesc_get_return_annot pdesc) with - | Some proc_guarded_by_str -> - (* the lock is not held, but the procedure is annotated with @GuardedBy *) - String.equal proc_guarded_by_str guarded_by_str - | None -> - false - in - let is_synchronized_on_class guarded_by_str = - guarded_by_str_is_current_class guarded_by_str pname - && Procdesc.is_java_synchronized pdesc - && - match pname with Procname.Java java_pname -> Procname.Java.is_static java_pname | _ -> false - in - let warn accessed_fld guarded_by_str = - let loc = State.get_loc_exn () in - let err_desc = Localise.desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc in - let exn = Exceptions.Unsafe_guarded_by_access (err_desc, __POS__) in - Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn - in - let rec is_read_write_lock typ = - let str_is_read_write_lock str = - String.is_suffix ~suffix:"ReadWriteUpdateLock" str - || String.is_suffix ~suffix:"ReadWriteLock" str - in - match typ.Typ.desc with - | Typ.Tstruct name -> - str_is_read_write_lock (Typ.Name.name name) - | Typ.Tptr (typ, _) -> - is_read_write_lock typ - | _ -> - false - in - let has_lock guarded_by_exp = - ( guarded_by_str_is_current_class_this guarded_by_str pname - || guarded_by_str_is_super_class_this guarded_by_str pname ) - && Procdesc.is_java_synchronized pdesc - || ( guarded_by_str_is_current_class guarded_by_str pname - && Procdesc.is_java_synchronized pdesc - && - match pname with - | Procname.Java java_pname -> - Procname.Java.is_static java_pname - | _ -> - false ) - || (* or the prop says we already have the lock *) - List.exists - ~f:(function Predicates.Apred (Alocked, _) -> true | _ -> false) - (Attribute.get_for_exp tenv prop guarded_by_exp) - in - let guardedby_is_self_referential = - String.equal "itself" (String.lowercase guarded_by_str) - || String.is_suffix ~suffix:guarded_by_str (Fieldname.to_string accessed_fld) - in - let proc_has_suppress_guarded_by_annot pdesc = - match extract_suppress_warnings_str (Annotations.pdesc_get_return_annot pdesc) with - | Some suppression_str -> - String.equal suppression_str "InvalidAccessToGuardedField" - | None -> - false - in - let should_warn pdesc = - (* adding this check implements "by reference" semantics for guarded-by rather than "by value" - semantics. if this access is through a local L or field V.f - (where f is not the @GuardedBy field!), we will not warn. - *) - let is_accessible_through_local_ref exp = - List.exists - ~f:(function - | Predicates.Hpointsto (Lvar _, Eexp (rhs_exp, _), _) -> - Exp.equal exp rhs_exp - | Predicates.Hpointsto (_, Estruct (flds, _), _) -> - List.exists - ~f:(fun (fld, strexp) -> - match strexp with - | Predicates.Eexp (rhs_exp, _) -> - Exp.equal exp rhs_exp && not (Fieldname.equal fld accessed_fld) - | _ -> - false ) - flds - | _ -> - false ) - prop.Prop.sigma - in - (not (PredSymb.equal_access (Procdesc.get_access pdesc) Private)) - && (not (Annotations.pdesc_return_annot_ends_with pdesc Annotations.visibleForTesting)) - && (not - ( match Procdesc.get_proc_name pdesc with - | Procname.Java java_pname -> - Procname.Java.is_access_method java_pname - | _ -> - false )) - && (not (is_accessible_through_local_ref lexp)) - && (not guardedby_is_self_referential) - && not (proc_has_suppress_guarded_by_annot pdesc) - in - match find_guarded_by_exp guarded_by_str prop.Prop.sigma with - | Some (Predicates.Eexp (guarded_by_exp, _), typ) -> - if is_read_write_lock typ then - (* TODO: model/understand read-write locks rather than ignoring them *) - prop - else if has_lock guarded_by_exp then - (* we have the lock; no need to add a proof obligation *) - (* TODO: materialize [fld], but don't add [fld] to the footprint. *) - prop - else if (* we don't know if we have the lock or not. *) - should_warn pdesc then ( - (* non-private method; can't ensure that the lock is held. warn. *) - warn accessed_fld guarded_by_str ; - prop ) - else - (* private method. add locked proof obligation to [pdesc] *) - Attribute.add tenv ~footprint:true prop Alocked [guarded_by_exp] - | _ -> - if - (not - ( proc_has_matching_annot pdesc guarded_by_str - || is_synchronized_on_class guarded_by_str )) - && should_warn pdesc - then - (* can't find the object the annotation refers to, and procedure is not annotated. warn *) - warn accessed_fld guarded_by_str - else - (* procedure has same GuardedBy annotation as the field. we would like to add a proof - obligation, but we can't (because we can't find an expression corresponding to the - lock in the current prop). so just be silent. *) - () ; - prop - in - let enforce_guarded_access fld typ prop = - match get_guarded_by_fld_str fld typ with - | Some guarded_by_fld_str -> - enforce_guarded_access_ fld guarded_by_fld_str prop - | None -> - prop - in - let check_fld_locks typ prop_acc (fld, strexp) = - match strexp with - | Predicates.Eexp (exp, _) when Exp.equal exp lexp -> - enforce_guarded_access fld typ prop_acc - | _ -> - prop_acc - in - let hpred_check_flds prop_acc = function - | Predicates.Hpointsto (_, Estruct (flds, _), Sizeof {typ}) -> - List.fold ~f:(check_fld_locks typ) ~init:prop_acc flds - | _ -> - prop_acc - in - match lexp with - | Exp.Lfield (_, fld, typ) -> - (* check for direct access to field annotated with @GuardedBy *) - enforce_guarded_access fld typ prop - | _ -> - (* check for access via alias *) - List.fold ~f:hpred_check_flds ~init:prop prop.Prop.sigma - - (** Add a pointsto for [root(lexp): typ] to the iterator and to the footprint, if it's compatible with the allowed footprint variables. This function ensures that [root(lexp): typ] is the @@ -1724,22 +1394,12 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc : L.d_ln () ; if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc_exn ()) ; let pname = Procdesc.get_proc_name pdesc in - let prop' = - match pname with - | Procname.Java java_pname - when Config.csl_analysis && !BiabductionConfig.footprint - && not (Procname.is_constructor pname || Procname.Java.is_class_initializer java_pname) - -> - add_guarded_by_constraints tenv prop lexp pdesc - | _ -> - prop - in - match Prop.prop_iter_create prop' with + match Prop.prop_iter_create prop with | None -> if !BiabductionConfig.footprint then - [prop_iter_add_hpred_footprint_to_prop pname tenv prop' (nlexp, typ) inst] + [prop_iter_add_hpred_footprint_to_prop pname tenv prop (nlexp, typ) inst] else ( pp_rearrangement_error "sigma is empty" prop nlexp ; raise (Exceptions.Symexec_memory_error __POS__) ) | Some iter -> - iter_rearrange pname tenv nlexp typ prop' iter inst + iter_rearrange pname tenv nlexp typ prop iter inst diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index ec20f9006..a097edfbc 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -114,9 +114,6 @@ val ia_is_worker_thread : Annot.Item.t -> bool val ia_is_uithread_equivalent : Annot.Item.t -> bool -val pdesc_get_return_annot : Procdesc.t -> Annot.Item.t -(** get the list of annotations on the return value of [pdesc] *) - val pdesc_has_return_annot : Procdesc.t -> (Annot.Item.t -> bool) -> bool (** return true if the given predicate evaluates to true on the annotation of [pdesc]'s return value *) diff --git a/infer/tests/build_systems/ant/issues.exp b/infer/tests/build_systems/ant/issues.exp index 8d89d1977..77453ffc8 100644 --- a/infer/tests/build_systems/ant/issues.exp +++ b/infer/tests/build_systems/ant/issues.exp @@ -50,46 +50,26 @@ codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer. codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.gzipOutputStreamNotClosedAfterFlush():void, 4, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure gzipOutputStreamNotClosedAfterFlush(),exception java.io.IOException] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.inflaterOutputStreamNotClosedAfterWrite():void, 7, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure inflaterOutputStreamNotClosedAfterWrite(),exception java.io.IOException] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.printStreamNotClosedAfterWrite():void, 5, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure printStreamNotClosedAfterWrite()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$3.readFromInnerClassBad1():java.lang.String, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad1()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$4.readFromInnerClassBad2():java.lang.String, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad2()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$Sub.badSub():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badSub()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$Sub.badSub():void, 491, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.xForSub`,,access to `this.xForSub`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByNormalLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByNormalLock()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByNormalLock():void, 526, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.guardedbynl`,,access to `this.guardedbynl`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByReentrantLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByReentrantLock()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByReentrantLock():void, 530, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.guardedbyrel`,,access to `this.guardedbyrel`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.byRefTrickyBad():java.lang.Object, 4, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure byRefTrickyBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.byRefTrickyBad():java.lang.Object, 281, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.g`,,access to `this.g`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 573, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.guardedByLock1`,,access to `this.guardedByLock1`] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 574, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.guardedByLock2`,,access to `this.guardedByLock2`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFAfterBlockBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFAfterBlockBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBad():void, 66, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadButSuppressed():void, 71, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadButSuppressedOther():void, 76, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongAnnotation():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongAnnotation()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongAnnotation():void, 109, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongLock()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongLock():void, 85, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFOkMethodAnnotated():void, 114, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFOkSynchronized():void, 127, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readGFromCopyOk():void, 267, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.mCopyOfG`,,access to `this.mCopyOfG`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBadSynchronizedMethodShouldntHelp():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBadSynchronizedMethodShouldntHelp()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.reassignCopyOk():void, 149, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.mCopyOfG`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodReadBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodReadBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodReadBad():void, 138, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodWriteBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodWriteBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedOnThisBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedOnThisBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedOnThisBad():void, 205, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `infer.GuardedByExample.sGuardedByClass`,,access to `infer.GuardedByExample.sGuardedByClass`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFAfterBlockBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFAfterBlockBad():void, 104, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBad()] codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBad():void, 80, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.f`,,access to `this.f`] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBadWrongLock()] codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterClearBad():void, 4, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure getAfterClearBad()] codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterRemovingTheKeyBad():void, 4, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure getAfterRemovingTheKeyBad()] codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getFromKeySetGood_FP(java.util.HashMap):void, 1, INEFFICIENT_KEYSET_ITERATOR, no_bucket, ERROR, [Accessing a value using a key that was retrieved from a `keySet` iterator. It is more efficient to use an iterator on the `entrySet` of the map, avoiding the extra `HashMap.get(key)` lookup.] diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 54dd0ccab..726e10a24 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -72,26 +72,6 @@ codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer. codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.gzipOutputStreamNotClosedAfterFlush():void, 4, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure gzipOutputStreamNotClosedAfterFlush(),exception java.io.IOException] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.inflaterOutputStreamNotClosedAfterWrite():void, 7, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure inflaterOutputStreamNotClosedAfterWrite(),exception java.io.IOException] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.printStreamNotClosedAfterWrite():void, 5, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure printStreamNotClosedAfterWrite()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$3.readFromInnerClassBad1():java.lang.String, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad1()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$4.readFromInnerClassBad2():java.lang.String, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad2()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$Sub.badSub():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badSub()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByNormalLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByNormalLock()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByReentrantLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByReentrantLock()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.byRefTrickyBad():java.lang.Object, 4, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure byRefTrickyBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFAfterBlockBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongAnnotation():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongAnnotation()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongLock()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBadSynchronizedMethodShouldntHelp():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBadSynchronizedMethodShouldntHelp()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodReadBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodReadBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodWriteBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodWriteBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedOnThisBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedOnThisBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFAfterBlockBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBad()] -codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBadWrongLock()] codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterClearBad():void, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure getAfterClearBad()] codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterRemovingTheKeyBad():void, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure getAfterRemovingTheKeyBad()] codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getFromKeySetGood_FP(java.util.HashMap):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure getFromKeySetGood_FP(...),Taking true branch]