[pulse] report latent issues in "main"

Summary:
In main() all latent issues are manifest issues as the only parameters
are user-controlled.

Reviewed By: skcho

Differential Revision: D28121535

fbshipit-source-id: eab54d5bc

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"

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

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

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]

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 <stdlib.h>
+
+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);
+  }
+}