diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index ab919cef6..075f3d55a 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -560,3 +560,6 @@ let get_fields_nullified procdesc = ~init:(Fieldname.Set.empty, Ident.Set.empty) in nullified_flds + + +let is_entry_point proc_name = String.equal (Procname.get_method proc_name) "main" diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index 3c60f25e9..2c31f278f 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -217,3 +217,6 @@ module ObjectiveC : sig val is_modelled_as_release : Tenv.t -> string -> bool end + +val is_entry_point : Procname.t -> bool +(** Does the function name correspond to a known entry point? Currently only matches ["main"] *) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index adfa95be7..fcbc45a77 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -555,7 +555,7 @@ let mk_initial tenv proc_desc = BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []}, None)) attrs ) - else (PreDomain.empty :> base_domain).attrs + else BaseDomain.empty.attrs in let pre = PreDomain.update ~stack:initial_stack ~heap:initial_heap ~attrs:initial_attrs PreDomain.empty @@ -859,7 +859,7 @@ let canonicalize astate = {astate with pre; post} -let filter_for_summary tenv astate0 = +let filter_for_summary tenv proc_name astate0 = let open SatUnsat.Import in L.d_printfln "Canonicalizing...@\n" ; let* astate_before_filter = canonicalize astate0 in @@ -871,12 +871,18 @@ let filter_for_summary tenv astate0 = let astate = restore_formals_for_summary astate_before_filter in let astate = {astate with topl= PulseTopl.filter_for_summary astate.path_condition astate.topl} in let astate, pre_live_addresses, post_live_addresses, _ = discard_unreachable astate in + let can_be_pruned = + if PatternMatch.is_entry_point proc_name then + (* report all latent issues at entry points *) + AbstractValue.Set.empty + else pre_live_addresses + in let live_addresses = AbstractValue.Set.union pre_live_addresses post_live_addresses in let+ path_condition, new_eqs = PathCondition.simplify tenv ~get_dynamic_type: (BaseAddressAttributes.get_dynamic_type (astate_before_filter.post :> BaseDomain.t).attrs) - ~can_be_pruned:pre_live_addresses ~keep:live_addresses astate.path_condition + ~can_be_pruned ~keep:live_addresses astate.path_condition in ({astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl}, new_eqs) @@ -894,7 +900,7 @@ let summary_of_post tenv pdesc astate = let* () = if is_unsat then Unsat else Sat () in let astate = {astate with path_condition} in let* astate, error = incorporate_new_eqs astate new_eqs in - let* astate, new_eqs = filter_for_summary tenv astate in + let* astate, new_eqs = filter_for_summary tenv (Procdesc.get_proc_name pdesc) astate in let+ astate, error = match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error) in diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index d0e5cc34b..60c82246b 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -4,6 +4,11 @@ codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid2_bad, 0, NULLPTR_ codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here] codetoanalyze/c/pulse/interprocedural.c, if_freed_invalid_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `y` of if_freed_invalid_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of if_freed_invalid_latent,invalid access occurs here] codetoanalyze/c/pulse/interprocedural.c, test_modified_value_then_error_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] +codetoanalyze/c/pulse/latent.c, FN_nonlatent_use_after_free_bad, 6, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of FN_nonlatent_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FN_nonlatent_use_after_free_bad,invalid access occurs here] +codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] +codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] +codetoanalyze/c/pulse/latent.c, main, 3, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] +codetoanalyze/c/pulse/latent.c, manifest_use_after_free, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] diff --git a/infer/tests/codetoanalyze/c/pulse/latent.c b/infer/tests/codetoanalyze/c/pulse/latent.c new file mode 100644 index 000000000..b8c2a123f --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse/latent.c @@ -0,0 +1,40 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include + +void latent_use_after_free(int b, int* x) { + if (b) { + free(x); + } + *x = 42; + if (!b) { + // just to avoid memory leaks + free(x); + } +} + +void manifest_use_after_free(int* x) { latent_use_after_free(1, x); } + +// FN because it's flagged only as latent at the moment +void FN_nonlatent_use_after_free_bad(int b, int* x) { + // the branch is independent of the issue here, so we should report the issue + // in this function + if (b) { + } + free(x); + *x = 42; +} + +// all latent issues that reach main are manifest, so this should be called +// "main_bad" but that would defeat the actual point :) +int main(int argc, char** argv) { + int* x = malloc(sizeof(int)); + if (x) { + latent_use_after_free(argc, x); + } +}