[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

@@ -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 *)

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)

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 *)

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

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 *)

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]

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));