[pulse][join] avoid fatal errors in over-approx mode

Summary:
We don't want to stop. In the future we'll want to be more precise,
there are cases where we do want to stop but right now we cannot
distinguish if, say, an invalid address is strongly or weakly invalid.
Need more attribute types.

Reviewed By: geralt-encore

Differential Revision:
D67276974

Privacy Context Container: L1208441

fbshipit-source-id: 1b8df6cd0819eef8a2c9a8e687667e8229fb2f04

infer/src/pulse/Pulse.ml

@@ -977,7 +977,8 @@ module PulseTransferFunctions = struct
     ( ( if Option.exists callee_pname ~f:IRAttributes.is_no_return then
           List.filter_map exec_states_res ~f:(fun exec_state_res ->
               (let+ exec_state = exec_state_res in
-               PulseSummary.force_exit_program analysis_data call_loc exec_state |> SatUnsat.sat )
+               PulseSummary.force_exit_program analysis_data path call_loc exec_state
+               |> SatUnsat.sat )
               |> PulseResult.of_some )
         else exec_states_res )
     , non_disj )
@@ -1088,7 +1089,7 @@ module PulseTransferFunctions = struct
                      dispatch_call limit analysis_data path ret call_exp actuals location call_flags
                        astate non_disj
                    in
-                   (PulseReport.report_exec_results analysis_data location execs, non_disj) )
+                   (PulseReport.report_exec_results analysis_data path location execs, non_disj) )
                   |> Option.value ~default:([default_astate], non_disj) )
         in
         (astates, non_disj, !ret_vars) )
@@ -1126,7 +1127,7 @@ module PulseTransferFunctions = struct
                 dispatch_call limit analysis_data path ret call_exp actuals location call_flags
                   astate non_disj
               in
-              (PulseReport.report_exec_results analysis_data location execs, non_disj) )
+              (PulseReport.report_exec_results analysis_data path location execs, non_disj) )
     in
     let dynamic_types_unreachable =
       PulseOperations.get_dynamic_type_unreachable_values vars astate
@@ -1168,7 +1169,7 @@ module PulseTransferFunctions = struct
   let exit_scope limit vars location path astate astate_n
       ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) =
     if Procname.is_java (Procdesc.get_proc_name proc_desc) then
-      (remove_vars vars location [ContinueProgram astate], path, astate_n)
+      (remove_vars vars location [ContinueProgram astate], astate_n)
     else
       (* Some RefCounted variables must not be removed at their ExitScope
          because they may still be referenced by someone and that reference may
@@ -1217,7 +1218,6 @@ module PulseTransferFunctions = struct
          append [vars] to [ret_vars]. *)
       let vars_to_remove = if List.is_empty ret_vars then vars else List.rev_append vars ret_vars in
       ( remove_vars vars_to_remove location astates
-      , path
       , PulseNonDisjunctiveOperations.mark_modified_copies_and_parameters vars astates astate_n )
 
 
@@ -1317,7 +1317,7 @@ module PulseTransferFunctions = struct
             (let++ astate, rhs_addr = PulseOperations.eval path Read loc rhs_exp astate in
              PulseOperations.write_load_id lhs_id (ValueOrigin.unknown rhs_addr) astate )
             |> SatUnsat.to_list
-            |> PulseReport.report_results analysis_data loc
+            |> PulseReport.report_results analysis_data path loc
           in
           (astates, path, astate_n)
       | Load {id= lhs_id; e= rhs_exp; loc; typ} ->
@@ -1340,7 +1340,7 @@ module PulseTransferFunctions = struct
              >>|| PulseOperations.add_static_type_objc_class tenv typ rhs_addr loc
              >>|| PulseOperations.write_load_id lhs_id rhs_vo )
             |> SatUnsat.to_list
-            |> PulseReport.report_results analysis_data loc
+            |> PulseReport.report_results analysis_data path loc
           in
           let astates, astate_n =
             (* call the initializer for certain globals to populate their values, unless we already
@@ -1365,7 +1365,7 @@ module PulseTransferFunctions = struct
                       [ PulseTaintOperations.load procname tenv path loc ~lhs:(lhs_id, typ)
                           ~rhs:rhs_exp astate ]
                     in
-                    PulseReport.report_results analysis_data loc astates
+                    PulseReport.report_results analysis_data path loc astates
                 | _ ->
                     [astate] )
           in
@@ -1433,13 +1433,13 @@ module PulseTransferFunctions = struct
             in
             match lhs_exp with
             | Lvar pvar when Pvar.is_return pvar ->
-                PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate
+                PulseOperations.check_address_escape loc proc_desc path rhs_addr rhs_history astate
             | _ ->
                 Ok astate
           in
           let astate_n = NonDisjDomain.set_captured_variables rhs_exp astate_n in
           let results = SatUnsat.to_list result in
-          let astates = PulseReport.report_results analysis_data loc results in
+          let astates = PulseReport.report_results analysis_data path loc results in
           (List.take astates limit, path, astate_n)
       | Call (ret, call_exp, actuals, loc, call_flags) ->
           let astate_n = check_modified_before_destructor actuals call_exp astate astate_n in
@@ -1481,7 +1481,9 @@ module PulseTransferFunctions = struct
                        , List.length new_astates + n_disjuncts ) )
             in
             let astates_before = !astates_before in
-            (PulseReport.report_exec_results analysis_data loc res, post_astate_n, astates_before)
+            ( PulseReport.report_exec_results analysis_data path loc res
+            , post_astate_n
+            , astates_before )
           in
           if not (CallGlobalForStats.is_node_not_stuck ()) then (
             if Config.log_pulse_coverage then add_verbose_never_return_info proc_desc instr loc ;
@@ -1507,10 +1509,13 @@ module PulseTransferFunctions = struct
             let<++> astate, _ = prune_result in
             astate
           in
-          let astates = PulseReport.report_exec_results analysis_data loc results in
+          let astates = PulseReport.report_exec_results analysis_data path loc results in
           (List.take astates limit, path, astate_n)
       | Metadata (ExitScope (vars, location)) ->
-          exit_scope limit vars location path astate astate_n analysis_data
+          let exec_states, non_disj =
+            exit_scope limit vars location path astate astate_n analysis_data
+          in
+          (exec_states, path, non_disj)
       | Metadata (VariableLifetimeBegins {pvar; typ; loc; is_cpp_structured_binding})
         when not (Pvar.is_global pvar) ->
           let set_uninitialized = (not is_cpp_structured_binding) && not (Typ.is_folly_coro typ) in
@@ -1684,18 +1689,21 @@ let exit_function limit analysis_data location posts non_disj_astate =
         | LatentAbortProgram _
         | LatentInvalidAccess _
         | LatentSpecializedTypeIssue _ ->
-            (exec_state :: acc_astates, astate_n)
+            ((exec_state, path) :: acc_astates, astate_n)
         | ContinueProgram astate ->
             let vars =
               Stack.fold
                 (fun var _ vars -> if Var.is_return var then vars else var :: vars)
                 astate []
             in
-            let astates, _, astate_n =
+            let astates, astate_n =
               PulseTransferFunctions.exit_scope limit vars location path astate astate_n
                 analysis_data
             in
-            (PulseTransferFunctions.remove_vars vars location astates @ acc_astates, astate_n) )
+            ( ( PulseTransferFunctions.remove_vars vars location astates
+              |> List.map ~f:(fun exec_state -> (exec_state, path)) )
+              @ acc_astates
+            , astate_n ) )
   in
   (List.rev astates, astate_n)
 
@@ -1824,8 +1832,8 @@ let analyze specialization ({InterproceduralAnalysis.tenv; proc_desc; exe_env} a
         in
         let posts =
           if convert_normal_to_exceptional then
-            List.map posts ~f:(fun edomain ->
-                match edomain with ContinueProgram x -> ExceptionRaised x | _ -> edomain )
+            List.map posts ~f:(fun ((exec_state, path) as post) ->
+                match exec_state with ContinueProgram x -> (ExceptionRaised x, path) | _ -> post )
           else posts
         in
         let summary =

infer/src/pulse/PulseAccessResult.ml

@@ -11,6 +11,7 @@ module AbductiveDomain = PulseAbductiveDomain
 module DecompilerExpr = PulseDecompilerExpr
 module Decompiler = PulseAbductiveDecompiler
 module Diagnostic = PulseDiagnostic
+module PathContext = PulsePathContext
 
 type error =
   | PotentialInvalidAccess of
@@ -26,13 +27,13 @@ let with_summary result =
   PulseResult.map_error result ~f:(fun (error, summary) -> WithSummary (error, summary))
 
 
-let rec is_fatal = function
+let rec is_fatal path = function
   | PotentialInvalidAccess _ | PotentialInvalidSpecializedCall _ ->
       true
   | ReportableError {diagnostic} ->
-      Diagnostic.aborts_execution diagnostic
+      Diagnostic.aborts_execution path diagnostic
   | WithSummary (error, _) ->
-      is_fatal error
+      is_fatal path error
 
 
 let rec astate_of_error = function
@@ -90,12 +91,12 @@ let of_abductive_summary_result abductive_summary_result =
   |> PulseResult.fatal_of_result
 
 
-let of_error_f error ~f : _ t =
-  if is_fatal error then FatalError (error, []) else Recoverable (f error, [error])
+let of_error_f path error ~f : _ t =
+  if is_fatal path error then FatalError (error, []) else Recoverable (f error, [error])
 
 
-let of_result_f (result : _ result) ~f : _ t =
-  match result with Ok x -> Ok x | Error error -> of_error_f ~f error
+let of_result_f path (result : _ result) ~f : _ t =
+  match result with Ok x -> Ok x | Error error -> of_error_f path ~f error
 
 
-let of_result result = of_result_f ~f:astate_of_error result
+let of_result path result = of_result_f path ~f:astate_of_error result

infer/src/pulse/PulseAccessResult.mli

@@ -10,6 +10,7 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 module DecompilerExpr = PulseDecompilerExpr
 module Diagnostic = PulseDiagnostic
+module PathContext = PulsePathContext
 
 type error =
   | PotentialInvalidAccess of
@@ -47,11 +48,11 @@ type abductive_summary_error =
     * DecompilerExpr.t
     * (Trace.t * Invalidation.must_be_valid_reason option) ]
 
-val of_result_f : ('a, error) result -> f:(error -> 'a) -> 'a t
+val of_result_f : PathContext.t -> ('a, error) result -> f:(error -> 'a) -> 'a t
 
-val of_result : (AbductiveDomain.t, error) result -> AbductiveDomain.t t
+val of_result : PathContext.t -> (AbductiveDomain.t, error) result -> AbductiveDomain.t t
 
-val of_error_f : error -> f:(error -> 'a) -> 'a t
+val of_error_f : PathContext.t -> error -> f:(error -> 'a) -> 'a t
 
 val of_abductive_summary_error : [< abductive_summary_error] -> error * AbductiveDomain.Summary.t
 

infer/src/pulse/PulseCallOperations.ml

@@ -397,7 +397,7 @@ let apply_callee ({InterproceduralAnalysis.tenv; proc_desc} as analysis_data)
               | `ReportNow ->
                   L.d_printfln ~color:Red "issue is now manifest, emitting an error" ;
                   Sat
-                    (AccessResult.of_error_f
+                    (AccessResult.of_error_f path
                        (WithSummary
                           (ReportableError {diagnostic; astate= astate_post_call}, astate_summary)
                        )

infer/src/pulse/PulseDiagnostic.ml

@@ -13,6 +13,7 @@ module CallEvent = PulseCallEvent
 module ConfigName = FbPulseConfigName
 module DecompilerExpr = PulseDecompilerExpr
 module Invalidation = PulseInvalidation
+module PathContext = PulsePathContext
 module TaintItem = PulseTaintItem
 module Trace = PulseTrace
 module TransitiveInfo = PulseTransitiveInfo
@@ -393,7 +394,7 @@ let get_copy_type = function
       None
 
 
-let aborts_execution = function
+let aborts_execution (path : PathContext.t) = function
   | AccessToInvalidAddress _
   | ErlangError
       ( Badarg _
@@ -411,7 +412,7 @@ let aborts_execution = function
       (* these errors either abort the whole program or, if they are false positives, mean that
          pulse is confused and the current abstract state has stopped making sense; either way,
          abort! *)
-      true
+      not path.is_non_disj
   | ConfigUsage _
   | ConstRefableParameter _
   | DynamicTypeMismatch _

infer/src/pulse/PulseDiagnostic.mli

@@ -12,6 +12,7 @@ module CallEvent = PulseCallEvent
 module ConfigName = FbPulseConfigName
 module DecompilerExpr = PulseDecompilerExpr
 module Invalidation = PulseInvalidation
+module PathContext = PulsePathContext
 module TaintItem = PulseTaintItem
 module Trace = PulseTrace
 module TransitiveInfo = PulseTransitiveInfo
@@ -129,7 +130,7 @@ type t =
 
 val pp : F.formatter -> t -> unit
 
-val aborts_execution : t -> bool
+val aborts_execution : PathContext.t -> t -> bool
 (** whether the presence of an error should abort the execution *)
 
 val get_message_and_suggestion : t -> string * string option

infer/src/pulse/PulseInterproc.ml

@@ -1296,20 +1296,21 @@ let apply_summary analysis_data path ~callee_proc_name call_location ~callee_sum
           let pre = AbductiveDomain.Summary.get_pre callee_summary in
           let* astate =
             check_all_valid path callee_proc_name call_location ~pre call_state
-            |> AccessResult.of_result
+            |> AccessResult.of_result path
           in
-          (* if at that stage [call_state.first_error] is set but we haven't error'd then there is
-             a problem; give up because something is wrong *)
+          (* if at that stage [call_state.first_error] is set but we haven't error'd then there is a
+             problem; give up because something is wrong, except in over-approximation mode where we
+             don't want to lose our precious single state because of this *)
           ( match call_state.first_error with
-          | None ->
-              ()
-          | Some v ->
+          | Some v when not path.PathContext.is_non_disj ->
               L.d_printfln
                 "huho, we found an error on accessing invalid address %a when applying the \
                  precondition but did not actually report an error. Abort!"
                 AbstractValue.pp v ;
               (* HACK: abuse [PathCondition], sorry *)
-              raise (Contradiction PathCondition) ) ;
+              raise (Contradiction PathCondition)
+          | _ ->
+              () ) ;
           let* astate = check_config_usage_at_call call_location ~pre call_state.subst astate in
           (* reset [visited] *)
           let call_state = {call_state with astate; visited= AddressSet.empty} in

infer/src/pulse/PulseOperations.ml

@@ -28,7 +28,7 @@ let check_addr_access path ?must_be_valid_reason access_mode location (address,
                    ; access_trace
                    ; must_be_valid_reason }
              ; astate } )
-    |> AccessResult.of_result
+    |> AccessResult.of_result path
   in
   match access_mode with
   | Read ->
@@ -38,7 +38,7 @@ let check_addr_access path ?must_be_valid_reason access_mode location (address,
                { diagnostic=
                    Diagnostic.ReadUninitialized {typ; calling_context= []; trace= access_trace}
                ; astate } )
-      |> AccessResult.of_result_f ~f:(fun _ ->
+      |> AccessResult.of_result_f path ~f:(fun _ ->
              (* do not report further uninitialized reads errors on this value *)
              AddressAttributes.initialize address astate )
   | Write ->
@@ -748,7 +748,7 @@ let rec deep_copy ?depth_max ({PathContext.timestamp} as path) location addr_his
       (astate, copy)
 
 
-let check_address_escape escape_location proc_desc address history astate =
+let check_address_escape escape_location proc_desc path address history astate =
   let is_assigned_to_global address astate =
     let points_to_address pointer address astate =
       Memory.find_edge_opt pointer Dereference astate
@@ -801,7 +801,7 @@ let check_address_escape escape_location proc_desc address history astate =
   let+ () =
     let open Result.Monad_infix in
     check_address_of_cpp_temporary () >>= check_address_of_stack_variable
-    |> AccessResult.of_result_f ~f:(fun _ -> ())
+    |> AccessResult.of_result_f path ~f:(fun _ -> ())
   in
   astate
 

infer/src/pulse/PulseOperations.mli

@@ -312,7 +312,13 @@ val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.t) lis
 val remove_vars : Var.t list -> Location.t -> t -> t SatUnsat.t
 
 val check_address_escape :
-  Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t
+     Location.t
+  -> Procdesc.t
+  -> PathContext.t
+  -> AbstractValue.t
+  -> ValueHistory.t
+  -> t
+  -> t AccessResult.t
 
 type call_kind = ClosureCall of (Exp.t * CapturedVar.t) list | VarCall of Ident.t | ResolvedCall