From b7ee374d003ef990b51cdf2df26b85b9a207a2d6 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 24 May 2021 05:05:13 -0700 Subject: [PATCH] [pulse] values equal to live values are not dead Summary: This fixes a memory leak false positive. When collecting unreachable values we should be careful to take the equality relation into account. Equal values are normally canonicalised but only with respect to "known" equalities. This makes sure variables that are live thanks to the "pruned" equalities are not discarded from the state. Reviewed By: skcho Differential Revision: D28382642 fbshipit-source-id: 2b898d754 --- infer/src/pulse/PulseAbductiveDomain.ml | 16 +++++++++++++--- infer/src/pulse/PulseFormula.ml | 4 +++- infer/src/pulse/PulseFormula.mli | 8 ++++++-- infer/src/pulse/PulsePathCondition.ml | 4 +++- infer/src/pulse/PulsePathCondition.mli | 9 +++++++-- infer/tests/codetoanalyze/c/pulse/issues.exp | 1 - infer/tests/codetoanalyze/c/pulse/memory_leak.c | 2 +- 7 files changed, 33 insertions(+), 11 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index afc8b111a..fd08cb1f3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -637,11 +637,21 @@ let discard_unreachable_ ~for_summary ({pre; post} as astate) = PreDomain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address pre_addresses) pre in let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in + let canon_addresses = + AbstractValue.Set.map (PathCondition.get_both_var_repr astate.path_condition) pre_addresses + |> AbstractValue.Set.fold + (fun addr acc -> + AbstractValue.Set.add (PathCondition.get_both_var_repr astate.path_condition addr) acc ) + post_addresses + in let post_new, dead_addresses = PostDomain.filter_addr_with_discarded_addrs ~heap_only:(not for_summary) ~f:(fun address -> - AbstractValue.Set.mem address pre_addresses || AbstractValue.Set.mem address post_addresses - ) + AbstractValue.Set.mem address pre_addresses + || AbstractValue.Set.mem address post_addresses + || + let canon_addr = PathCondition.get_both_var_repr astate.path_condition address in + AbstractValue.Set.mem canon_addr canon_addresses ) post in (* note: we don't call {!PulsePathCondition.simplify} *) @@ -880,7 +890,7 @@ let incorporate_new_eqs astate new_eqs = (** it's a good idea to normalize the path condition before calling this function *) let canonicalize astate = let open SatUnsat.Import in - let get_var_repr v = PathCondition.get_var_repr astate.path_condition v in + let get_var_repr v = PathCondition.get_known_var_repr astate.path_condition v in let canonicalize_pre (pre : PreDomain.t) = (* (ab)use canonicalization to filter out empty edges in the heap and detect aliasing contradictions *) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index f1dcfc247..64895b274 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1904,4 +1904,6 @@ let has_no_assumptions phi = Atom.Set.for_all (fun atom -> Formula.Normalizer.implies_atom phi.known atom) phi.pruned -let get_var_repr phi v = (Formula.Normalizer.get_repr phi.known v :> Var.t) +let get_known_var_repr phi v = (Formula.Normalizer.get_repr phi.known v :> Var.t) + +let get_both_var_repr phi v = (Formula.Normalizer.get_repr phi.both v :> Var.t) diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index eea52e431..cbb352435 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -75,5 +75,9 @@ val is_known_zero : t -> Var.t -> bool val has_no_assumptions : t -> bool -val get_var_repr : t -> Var.t -> Var.t -(** get the canonical representative for the variable according to the equality relation *) +val get_known_var_repr : t -> Var.t -> Var.t +(** get the canonical representative for the variable according to the known/post equality relation *) + +val get_both_var_repr : t -> Var.t -> Var.t +(** get the canonical representative for the variable according to the both/pre+post equality + relation *) diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 0da486144..3f20598ea 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -434,4 +434,6 @@ let is_unsat_expensive tenv ~get_dynamic_type phi = let has_no_assumptions phi = Formula.has_no_assumptions phi.formula -let get_var_repr phi v = Formula.get_var_repr phi.formula v +let get_known_var_repr phi v = Formula.get_known_var_repr phi.formula v + +let get_both_var_repr phi v = Formula.get_both_var_repr phi.formula v diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 62d3c6faa..d8a6da69e 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -87,5 +87,10 @@ val is_unsat_expensive : val has_no_assumptions : t -> bool (** whether the current path is independent of any calling context *) -val get_var_repr : t -> AbstractValue.t -> AbstractValue.t -(** get the canonical representative for the variable according to the equality relation *) +val get_known_var_repr : t -> AbstractValue.t -> AbstractValue.t +(** get the canonical representative for the variable according to the equality relation in the + "known" part of the formula *) + +val get_both_var_repr : t -> AbstractValue.t -> AbstractValue.t +(** get the canonical representative for the variable according to the equality relation in the + "both" (known + pruned) part of the formula *) diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 1087745e4..b1a410575 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -14,7 +14,6 @@ codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, NULLPTR_DEREFERENCE, n 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, alias_ptr_free_FP, 10, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_formal_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable 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 `malloc` 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 `malloc` here,memory becomes unreachable here] diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c index 501ca07c5..f87e6135d 100644 --- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c +++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c @@ -82,7 +82,7 @@ void malloc_ptr_free_ptr_ok() { free_via_ptr(p); } -void alias_ptr_free_FP(int* out, int flag) { +void alias_ptr_free_ok(int* out, int flag) { int* y; if (flag) { y = (int*)malloc(sizeof(int));