[pulse][join] do not treat calls with an over-approx result as unknown

Summary:
When running in over-approximation mode, a call's effect can be purely
in the over-approx part of the state and the previous heuristic would
think we failed to apply the call in that case and scramble the state
instead.

Reviewed By: hajduakos

Differential Revision:
D67276580

Privacy Context Container: L1208441

fbshipit-source-id: c0773b20c35547e2decdcd1094ef7dbd503bbd88

infer/src/pulse/PulseCallOperations.ml

@@ -968,7 +968,9 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys
         iter_call ~max_iteration ~nth_iteration:0 ~is_pulse_specialization_limit_not_reached
           already_given summary.PulseSummary.main astate
       in
-      let has_continue_program = has_continue_program res in
+      let has_continue_program =
+        has_continue_program res || not (NonDisjDomain.astate_is_bottom non_disj)
+      in
       if has_continue_program then GlobalForStats.node_is_not_stuck () ;
       let res, non_disj =
         if

infer/src/pulse/PulseNonDisjunctiveDomain.ml

@@ -868,6 +868,8 @@ let join_to_astate astate non_disj =
   {non_disj with astate= OverApproxDomain.join non_disj.astate astate}
 
 
+let astate_is_bottom {astate} = OverApproxDomain.is_bottom astate
+
 type summary =
   { transitive_info: InterDom.t
   ; has_dropped_disjuncts: AbstractDomain.BooleanOr.t

infer/src/pulse/PulseNonDisjunctiveDomain.mli

@@ -50,6 +50,8 @@ val exec :
 val join_to_astate :
   (AbductiveDomain.t * PathContext.t) AbstractDomain.Types.bottom_lifted -> t -> t
 
+val astate_is_bottom : t -> bool
+
 val for_disjunct_exec_instr : t -> t
 
 val pp_with_kind : Pp.print_kind -> F.formatter -> t -> unit