[pulse][isl] manifest errors

Reviewed By: jvillard

Differential Revision: D27405377

fbshipit-source-id: e69e02c0d

infer/man/man1/infer-full.txt

@@ -1909,6 +1909,10 @@ INTERNAL OPTIONS
            explicit Ok/Error summaries are recorded. For experiments only.
            (Conversely: --no-pulse-isl)
 
+       --pulse-manifest-emp
+           Activates: [Pulse] manifest errors with postive heaps in pre. For
+           experiments only. (Conversely: --no-pulse-manifest-emp)
+
        --pulse-max-disjuncts int
            Under-approximate after int disjunctions in the domain
 

infer/src/base/Config.ml

@@ -1978,6 +1978,11 @@ and pulse_isl =
      For experiments only."
 
 
+and pulse_manifest_emp =
+  CLOpt.mk_bool ~long:"pulse-manifest-emp" ~default:false
+    "[Pulse] manifest errors with postive heaps in pre. For experiments only."
+
+
 and pulse_max_disjuncts =
   CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:20
     "Under-approximate after $(i,int) disjunctions in the domain"
@@ -3235,6 +3240,8 @@ and pulse_intraprocedural_only = !pulse_intraprocedural_only
 
 and pulse_isl = !pulse_isl
 
+and pulse_manifest_emp = !pulse_manifest_emp
+
 and pulse_max_disjuncts = !pulse_max_disjuncts
 
 and pulse_model_abort = RevList.to_list !pulse_model_abort

infer/src/base/Config.mli

@@ -485,6 +485,8 @@ val pulse_intraprocedural_only : bool
 
 val pulse_isl : bool
 
+val pulse_manifest_emp : bool
+
 val pulse_max_disjuncts : int
 
 val pulse_model_abort : string list

infer/src/pulse/PulseAbductiveDomain.ml

@@ -684,6 +684,27 @@ let invalidate_locals pdesc astate : t =
   else {astate with post= PostDomain.update astate.post ~attrs:attrs'}
 
 
+let is_isl_without_allocation astate =
+  BaseStack.for_all
+    (fun _ (addr, _) ->
+      match Memory.find_edge_opt addr HilExp.Access.Dereference astate with
+      | Some (addr, _) -> (
+        match AddressAttributes.find_opt addr astate with
+        | None ->
+            true
+        | Some attrs ->
+            not (Option.is_some (Attribute.Attributes.get_allocation attrs)) )
+      | None ->
+          true )
+    (astate.post :> base_domain).stack
+
+
+let is_pre_without_isl_abduced astate =
+  BaseAddressAttributes.for_all
+    (fun _ attrs -> match Attributes.get_isl_abduced attrs with None -> true | Some _ -> false)
+    (astate.pre :> base_domain).attrs
+
+
 type summary = t [@@deriving compare, equal, yojson_of]
 
 let is_heap_allocated {post; pre} v =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -183,6 +183,10 @@ val add_skipped_calls : SkippedCalls.t -> t -> t
 
 val set_path_condition : PathCondition.t -> t -> t
 
+val is_isl_without_allocation : t -> bool
+
+val is_pre_without_isl_abduced : t -> bool
+
 (** private type to make sure {!summary_of_post} is always called when creating summaries *)
 type summary = private t [@@deriving compare, equal, yojson_of]
 

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -23,6 +23,8 @@ let compare = Graph.compare AttributesNoRank.compare
 
 let equal = Graph.equal AttributesNoRank.equal
 
+let for_all = Graph.for_all
+
 let yojson_of_t = [%yojson_of: _]
 
 let add_one addr attribute attrs =

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -14,6 +14,8 @@ val empty : t
 
 val filter : (AbstractValue.t -> Attributes.t -> bool) -> t -> t
 
+val for_all : (AbstractValue.t -> Attributes.t -> bool) -> t -> bool
+
 val filter_with_discarded_addrs :
   (AbstractValue.t -> Attributes.t -> bool) -> t -> t * AbstractValue.t list
 

infer/src/pulse/PulseLatentIssue.ml

@@ -31,6 +31,10 @@ let add_call call_and_loc = function
 
 let is_manifest (astate : AbductiveDomain.summary) =
   Arithmetic.has_no_assumptions (astate :> AbductiveDomain.t)
+  && ( (not Config.pulse_isl)
+     || AbductiveDomain.is_isl_without_allocation (astate :> AbductiveDomain.t)
+        && ( (not Config.pulse_manifest_emp)
+           || AbductiveDomain.is_pre_without_isl_abduced (astate :> AbductiveDomain.t) ) )
 
 
 (* require a summary because we don't want to stop reporting because some non-abducible condition is

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -7,6 +7,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEA
 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]
 codetoanalyze/c/pulse/nullptr.c, FN_bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]

infer/tests/codetoanalyze/c/pulse/nullptr.c

@@ -103,3 +103,15 @@ void FN_bug_after_malloc_result_test_bad(int* x) {
     *y = 42;
   }
 }
+
+void bug_after_abduction_bad(int* x) {
+  *x = 42;
+  int* y = NULL;
+  *y = 42;
+}
+
+void bug_with_allocation_bad(int* x) {
+  x = (int*)malloc(sizeof(int*));
+  int* y = NULL;
+  *y = 42;
+}