diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 4443953f1..052a97615 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -397,6 +397,7 @@ OPTIONS CROSS_SITE_SCRIPTING (enabled by default), Cannot_star (enabled by default), DANGLING_POINTER_DEREFERENCE (disabled by default), + DANGLING_POINTER_DEREFERENCE_MAYBE (disabled by default), DEADLOCK (enabled by default), DEAD_STORE (enabled by default), DEALLOCATE_STACK_VARIABLE (enabled by default), @@ -466,6 +467,7 @@ OPTIONS LOGGING_PRIVATE_DATA (enabled by default), Leak_after_array_abstraction (enabled by default), Leak_in_footprint (enabled by default), + Leak_unknown_origin (disabled by default), MEMORY_LEAK (enabled by default), MISSING_REQUIRED_PROP (enabled by default), MIXED_SELF_WEAKSELF (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 13350c923..64e6e713f 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -123,6 +123,7 @@ OPTIONS CROSS_SITE_SCRIPTING (enabled by default), Cannot_star (enabled by default), DANGLING_POINTER_DEREFERENCE (disabled by default), + DANGLING_POINTER_DEREFERENCE_MAYBE (disabled by default), DEADLOCK (enabled by default), DEAD_STORE (enabled by default), DEALLOCATE_STACK_VARIABLE (enabled by default), @@ -192,6 +193,7 @@ OPTIONS LOGGING_PRIVATE_DATA (enabled by default), Leak_after_array_abstraction (enabled by default), Leak_in_footprint (enabled by default), + Leak_unknown_origin (disabled by default), MEMORY_LEAK (enabled by default), MISSING_REQUIRED_PROP (enabled by default), MIXED_SELF_WEAKSELF (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 59a863c9d..e1c397296 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -397,6 +397,7 @@ OPTIONS CROSS_SITE_SCRIPTING (enabled by default), Cannot_star (enabled by default), DANGLING_POINTER_DEREFERENCE (disabled by default), + DANGLING_POINTER_DEREFERENCE_MAYBE (disabled by default), DEADLOCK (enabled by default), DEAD_STORE (enabled by default), DEALLOCATE_STACK_VARIABLE (enabled by default), @@ -466,6 +467,7 @@ OPTIONS LOGGING_PRIVATE_DATA (enabled by default), Leak_after_array_abstraction (enabled by default), Leak_in_footprint (enabled by default), + Leak_unknown_origin (disabled by default), MEMORY_LEAK (enabled by default), MISSING_REQUIRED_PROP (enabled by default), MIXED_SELF_WEAKSELF (enabled by default), diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 84fb02ca0..a5a9ee0c3 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -75,7 +75,13 @@ exception Inherently_dangerous_function of Localise.error_desc exception Internal_error of Localise.error_desc -exception Leak of bool * (visibility * Localise.error_desc) * bool * PredSymb.resource * L.ocaml_pos +exception + Leak of + bool + * (bool (* is it user visible? *) * Localise.error_desc) + * bool + * PredSymb.resource + * L.ocaml_pos exception Missing_fld of Fieldname.t * L.ocaml_pos @@ -208,12 +214,11 @@ let recognize_exception exn = ; visibility= Exn_developer ; severity= Some Info } | Dangling_pointer_dereference (user_visible, desc, ocaml_pos) -> - let visibility = if user_visible then Exn_user else Exn_developer in - { issue_type= IssueType.dangling_pointer_dereference - ; description= desc - ; ocaml_pos= Some ocaml_pos - ; visibility - ; severity= None } + let issue_type, visibility = + if user_visible then (IssueType.dangling_pointer_dereference, Exn_user) + else (IssueType.dangling_pointer_dereference_maybe, Exn_developer) + in + {issue_type; description= desc; ocaml_pos= Some ocaml_pos; visibility; severity= None} | Deallocate_stack_variable desc -> { issue_type= IssueType.deallocate_stack_variable ; description= desc @@ -290,7 +295,7 @@ let recognize_exception exn = ; ocaml_pos= None ; visibility= Exn_developer ; severity= None } - | Leak (fp_part, (exn_vis, error_desc), done_array_abstraction, resource, ocaml_pos) -> + | Leak (fp_part, (user_visible, error_desc), done_array_abstraction, resource, ocaml_pos) -> if done_array_abstraction then { issue_type= IssueType.leak_after_array_abstraction ; description= error_desc @@ -303,6 +308,12 @@ let recognize_exception exn = ; ocaml_pos= Some ocaml_pos ; visibility= Exn_developer ; severity= None } + else if not user_visible then + { issue_type= IssueType.leak_unknown_origin + ; description= error_desc + ; ocaml_pos= Some ocaml_pos + ; visibility= Exn_developer + ; severity= None } else let issue_type = match resource with @@ -318,7 +329,7 @@ let recognize_exception exn = { issue_type ; description= error_desc ; ocaml_pos= Some ocaml_pos - ; visibility= exn_vis + ; visibility= Exn_user ; severity= None } | Missing_fld (fld, ocaml_pos) -> let desc = Localise.verbatim_desc (Fieldname.to_full_string fld) in diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 67d602210..ac2f420bf 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -77,7 +77,12 @@ exception Inherently_dangerous_function of Localise.error_desc exception Internal_error of Localise.error_desc exception - Leak of bool * (visibility * Localise.error_desc) * bool * PredSymb.resource * Logging.ocaml_pos + Leak of + bool + * (bool (* is it user visible? *) * Localise.error_desc) + * bool + * PredSymb.resource + * Logging.ocaml_pos exception Missing_fld of Fieldname.t * Logging.ocaml_pos diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 6c84731d8..dd7be6d9e 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -293,6 +293,10 @@ let dangling_pointer_dereference = register_from_string ~enabled:false ~id:"DANGLING_POINTER_DEREFERENCE" Biabduction +let dangling_pointer_dereference_maybe = + register_from_string ~enabled:false ~id:"DANGLING_POINTER_DEREFERENCE_MAYBE" Biabduction + + let dead_store = register_from_string ~id:"DEAD_STORE" Liveness let deadlock = register_from_string ~id:"DEADLOCK" Starvation @@ -492,6 +496,8 @@ let leak_after_array_abstraction = let leak_in_footprint = register_from_string ~id:"Leak_in_footprint" Biabduction +let leak_unknown_origin = register_from_string ~enabled:false ~id:"Leak_unknown_origin" Biabduction + let lock_consistency_violation = register_from_string ~id:"LOCK_CONSISTENCY_VIOLATION" RacerD let lockless_violation = register_from_string ~id:"LOCKLESS_VIOLATION" Starvation diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 894eebf72..2e13ac2d8 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -147,6 +147,8 @@ val cross_site_scripting : t val dangling_pointer_dereference : t +val dangling_pointer_dereference_maybe : t + val dead_store : t val deadlock : t @@ -254,6 +256,8 @@ val leak_after_array_abstraction : t val leak_in_footprint : t +val leak_unknown_origin : t + val lockless_violation : t val lock_consistency_violation : t diff --git a/infer/src/biabduction/errdesc.ml b/infer/src/biabduction/errdesc.ml index 029a9d6c0..592cae316 100644 --- a/infer/src/biabduction/errdesc.ml +++ b/infer/src/biabduction/errdesc.ml @@ -524,20 +524,21 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = L.d_ln () ) ; value_str_from_pvars_vpath [] vpath in - let exn_cat, bucket = + let is_user_visible, bucket = (* decide whether Exn_user or Exn_developer *) match resource_opt with | Some _ -> (* we know it has been allocated *) - (Exceptions.Exn_user, bucket) + (true, bucket) | None -> if leak_from_list_abstraction hpred prop && Option.is_some value_str then (* we don't know it's been allocated, but it's coming from list abstraction and we have a name *) - (Exceptions.Exn_user, bucket) - else (Exceptions.Exn_developer, Some Mleak_buckets.ml_bucket_unknown_origin) + (true, bucket) + else (false, Some Mleak_buckets.ml_bucket_unknown_origin) in - (exn_cat, Localise.desc_leak hpred_typ_opt value_str resource_opt res_action_opt loc bucket) + ( is_user_visible + , Localise.desc_leak hpred_typ_opt value_str resource_opt res_action_opt loc bucket ) (** find the dexp, if any, where the given value is stored also return the type of the value if diff --git a/infer/src/biabduction/errdesc.mli b/infer/src/biabduction/errdesc.mli index 12b94551b..b1391c2c4 100644 --- a/infer/src/biabduction/errdesc.mli +++ b/infer/src/biabduction/errdesc.mli @@ -95,7 +95,7 @@ val explain_leak : -> 'a Prop.t -> PredSymb.t option -> string option - -> Exceptions.visibility * Localise.error_desc + -> bool (* should the leak be reported to the user? *) * Localise.error_desc (** Produce a description of a leak by looking at the current state. If the current instruction is a variable nullify, blame the variable. If it is an abstraction, blame any variable nullify at the current node. If there is an alloc attribute, print the function call and line number. *)