[pulse][join] execute over-approx state from callees

Summary:
Go inter-procedural with the over-approximate domain! Apply callee's
over-approximate parts of their summaries too.

One tricky bit is that this creates known-over-approx states from
executing disjuncts, which is the first instance of this. This can be a
problem if we need to do more things within one instruction than
applying the callee's summary: right now the execution monad doesn't
take the over-approximate state into account. TODO.

Reviewed By: davidpichardie

Differential Revision:
D66974777

Privacy Context Container: L1208441

fbshipit-source-id: 392e73dcca8351c2b4fc2a8330cded6237618a84

infer/src/pulse/PulseCallOperations.ml

@@ -508,13 +508,25 @@ let call_aux disjunct_limit ({InterproceduralAnalysis.tenv} as analysis_data) pa
     NonDisjDomain.apply_summary ~callee_pname ~call_loc ~skip_transitive_accesses non_disj_caller
       non_disj_callee
   in
-  (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
+  (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary, and to the
+     over-approximate pre/post if we are currently executing the over-approximate part of the
+     current state *)
+  let exec_states_callee =
+    if path.PathContext.is_non_disj then
+      match NonDisjDomain.Summary.get_pre_post non_disj_callee with
+      | Bottom ->
+          exec_states_callee
+      | NonBottom astate_over_approx ->
+          exec_states_callee @ [ContinueProgram astate_over_approx]
+    else exec_states_callee
+  in
   let posts, contradiction =
     List.fold ~init:([], None) exec_states_callee
       ~f:(fun (posts, contradiction) callee_exec_state ->
         if
-          Option.exists disjunct_limit ~f:(fun limit -> List.length posts >= limit)
-          || (should_keep_at_most_one_disjunct && not (List.is_empty posts))
+          (not path.PathContext.is_non_disj)
+          && ( Option.exists disjunct_limit ~f:(fun limit -> List.length posts >= limit)
+             || (should_keep_at_most_one_disjunct && not (List.is_empty posts)) )
         then (posts, contradiction)
         else (
           (* apply one pre/post spec, check for timeouts in-between each pre/post spec from the callee
@@ -530,6 +542,35 @@ let call_aux disjunct_limit ({InterproceduralAnalysis.tenv} as analysis_data) pa
           | Sat post, new_contradiction ->
               (post :: posts, PulseInterproc.merge_contradictions contradiction new_contradiction) ) )
   in
+  (* We always apply the non-disj part of the summary from the current state, even if it we are
+     inside a disjunct and not the non-disj part of the current state. We then put the result
+     directly into the non-disjunctive part of the state, which will be joined with the results from
+     other disjuncts and whatever over-approximate state was already there. *)
+  let non_disj =
+    match NonDisjDomain.Summary.get_pre_post non_disj_callee with
+    | NonBottom callee_astate_over_approx
+      when not path.PathContext.is_non_disj (* already executed above in this case *) ->
+        let (non_disj_caller : _ AbstractDomain.Types.bottom_lifted) =
+          match
+            apply_callee analysis_data path callee_pname call_loc call_flags
+              (ContinueProgram callee_astate_over_approx) ~captured_formals ~captured_actuals
+              ~formals ~actuals ~ret astate
+          with
+          | Sat (Ok (ContinueProgram post)), _new_contradiction ->
+              NonBottom (post, path)
+          | Sat (Recoverable (ContinueProgram post, _)), _new_contradiction ->
+              (* TODO: report errors *)
+              NonBottom (post, path)
+          | Sat (FatalError _), _ ->
+              (* TODO: report errors, recover after errors *)
+              Bottom
+          | _, _new_contradiction ->
+              Bottom
+        in
+        NonDisjDomain.join_to_astate non_disj_caller non_disj
+    | _ ->
+        non_disj
+  in
   (posts, (non_disj, contradiction))
 
 

infer/src/pulse/PulseNonDisjunctiveDomain.ml

@@ -845,6 +845,8 @@ let exec non_disj ~exec_instr =
     | NonBottom (astate, path) ->
         (* move the abstract state from the non-disjunctive part into a single disjunct *)
         let non_disj = {non_disj with astate= Bottom} in
+        (* set the context to "non-disjunctive" *)
+        let path = {path with is_non_disj= true} in
         let exec_states_paths, non_disj =
           exec_instr ((ExecutionDomain.ContinueProgram astate, path), non_disj)
         in
@@ -862,6 +864,10 @@ let exec non_disj ~exec_instr =
   else non_disj
 
 
+let join_to_astate astate non_disj =
+  {non_disj with astate= OverApproxDomain.join non_disj.astate astate}
+
+
 type summary =
   { transitive_info: InterDom.t
   ; has_dropped_disjuncts: AbstractDomain.BooleanOr.t
@@ -930,4 +936,6 @@ module Summary = struct
 
 
   let has_dropped_disjuncts {has_dropped_disjuncts} = has_dropped_disjuncts
+
+  let get_pre_post {astate} = astate
 end

infer/src/pulse/PulseNonDisjunctiveDomain.mli

@@ -8,6 +8,7 @@
 open! IStd
 module F = Format
 open PulseBasicInterface
+module AbductiveDomain = PulseAbductiveDomain
 module BaseMemory = PulseBaseMemory
 module DecompilerExpr = PulseDecompilerExpr
 module ExecutionDomain = PulseExecutionDomain
@@ -46,6 +47,9 @@ val exec :
        ((ExecutionDomain.t * PathContext.t) * t -> (ExecutionDomain.t * PathContext.t) list * t)
   -> t
 
+val join_to_astate :
+  (AbductiveDomain.t * PathContext.t) AbstractDomain.Types.bottom_lifted -> t -> t
+
 val for_disjunct_exec_instr : t -> t
 
 val pp_with_kind : Pp.print_kind -> F.formatter -> t -> unit
@@ -66,6 +70,8 @@ module Summary : sig
   val get_transitive_info_if_not_top : t -> TransitiveInfo.t option
 
   val has_dropped_disjuncts : t -> bool
+
+  val get_pre_post : t -> AbductiveDomain.Summary.t AbstractDomain.Types.bottom_lifted
 end
 
 val add_var :

infer/src/pulse/PulsePathContext.ml

@@ -9,15 +9,17 @@ open! IStd
 module F = Format
 open PulseBasicInterface
 
-type t = {timestamp: Timestamp.t} [@@deriving compare, equal]
+type t = {timestamp: Timestamp.t; is_non_disj: bool} [@@deriving compare, equal]
 
 (** path contexts is metadata that do not contribute to the semantics *)
 let leq ~lhs:_ ~rhs:_ = true
 
 (** see [leq] *)
 let equal_fast _ _ = true
 
-let join {timestamp= ts1} {timestamp= ts2} = {timestamp= Timestamp.max ts1 ts2}
+let join {timestamp= ts1; is_non_disj= nd1} {timestamp= ts2; is_non_disj= nd2} =
+  {timestamp= Timestamp.max ts1 ts2; is_non_disj= nd1 || nd2}
+
 
 let is_normal _ = true
 
@@ -27,10 +29,11 @@ let is_executable _ = true
 
 let exceptional_to_normal x = x
 
-let pp fmt ({timestamp} [@warning "+missing-record-field-pattern"]) =
-  F.fprintf fmt "timestamp= %a" Timestamp.pp timestamp
+let pp fmt ({timestamp; is_non_disj} [@warning "+missing-record-field-pattern"]) =
+  F.fprintf fmt "timestamp= %a%s" Timestamp.pp timestamp
+    (if is_non_disj then " NON-DISJUNCTIVE EXECUTION" else "")
 
 
-let initial = {timestamp= Timestamp.t0}
+let initial = {timestamp= Timestamp.t0; is_non_disj= false}
 
-let post_exec_instr {timestamp} = {timestamp= Timestamp.incr timestamp}
+let post_exec_instr path = {path with timestamp= Timestamp.incr path.timestamp}

infer/src/pulse/PulsePathContext.mli

@@ -8,7 +8,11 @@
 open! IStd
 open PulseBasicInterface
 
-type t = {timestamp: Timestamp.t  (** step number in an intra-procedural analysis *)}
+type t =
+  { timestamp: Timestamp.t  (** step number in an intra-procedural analysis *)
+  ; is_non_disj: bool
+        (** whether we are currently executing the abstract state inside the non-disjunctive
+            (=over-approximate) part of the state *) }
 [@@deriving compare, equal]
 
 include AbstractDomain.Disjunct with type t := t

infer/tests/codetoanalyze/c/pulse-over-only/attributes.c

@@ -52,13 +52,13 @@ void maybe_deref_pointer(int a, int* p) {
   }
 }
 
-// no interproc yet
-void FN_interproc_joined_invalid_deref_bad() {
+void interproc_joined_invalid_deref_bad() {
   int* p = get_maybe_invalid_pointer(random());
   maybe_deref_pointer(random(), p);
 }
 
-void interproc_path_sensitive_valid_deref_ok() {
+// the price of over-approximation!
+void FP_interproc_path_sensitive_valid_deref_ok() {
   int* p = get_maybe_invalid_pointer(10);
   maybe_deref_pointer(10, p);
 }

infer/tests/codetoanalyze/c/pulse-over-only/issues.exp

@@ -1,5 +1,7 @@
 codetoanalyze/c/pulse-over-only/attributes.c, init_one_branch_only_bad, 5, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
 codetoanalyze/c/pulse-over-only/attributes.c, FNsuppressed_invalid_one_branch_only_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,invalid access occurs here]
+codetoanalyze/c/pulse-over-only/attributes.c, interproc_joined_invalid_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,when calling `get_maybe_invalid_pointer` here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,in call to `get_maybe_invalid_pointer`,assigned,when calling `maybe_deref_pointer` here,parameter `p` of maybe_deref_pointer,invalid access occurs here]
+codetoanalyze/c/pulse-over-only/attributes.c, FP_interproc_path_sensitive_valid_deref_ok, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,when calling `get_maybe_invalid_pointer` here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,in call to `get_maybe_invalid_pointer`,assigned,when calling `maybe_deref_pointer` here,parameter `p` of maybe_deref_pointer,invalid access occurs here]
 codetoanalyze/c/pulse-over-only/formula.c, FP_same_facts_different_branches_ok, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse-over-only/formula.c, FP_same_facts_different_branches_ok, 23, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse-over-only/join.c, join_valid_invalid_pointers, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `p` of join_valid_invalid_pointers,invalid access occurs here]