[pulse] more type-safety around summary and latent issues creation

Summary:
This makes sure we call `AbductiveDomain.summary_of_post` exactly once
per post-condition. Notice in particular in the diff:
- in Pulse.ml we remove a now-certified-useless "is_unsat_expensive"
  call
- in PulseOperations.ml we add a previously-missing call to
  `summary_of_post` (it's needed to remove local variables from the
  symbolic state + normalize)

The price to pay is ugly type annotations and down-casting peppered in a
few places, in reasonable number.

Reviewed By: da319

Differential Revision: D24078564

fbshipit-source-id: 3102cacf0

infer/src/checkers/impurity.ml

@@ -142,8 +142,10 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai
     match exec_state with
     | ExitProgram astate ->
         (astate, true)
-    | AbortProgram astate | ContinueProgram astate | LatentAbortProgram {astate} ->
+    | ContinueProgram astate ->
         (astate, false)
+    | AbortProgram astate | LatentAbortProgram {astate} ->
+        ((astate :> AbductiveDomain.t), false)
   in
   let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in
   let post = AbductiveDomain.get_post astate in
@@ -162,7 +164,8 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai
   {modified_globals; modified_params; skipped_calls; exited}
 
 
-let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} pulse_summary_opt =
+let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log}
+    (pulse_summary_opt : PulseSummary.t option) =
   let proc_name = Procdesc.get_proc_name proc_desc in
   let pname_loc = Procdesc.get_loc proc_desc in
   match pulse_summary_opt with
@@ -182,8 +185,9 @@ let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} pulse_summary_opt
         IssueType.impure_function impure_fun_desc
   | Some pre_posts ->
       let (ImpurityDomain.{modified_globals; modified_params; skipped_calls} as impurity_astate) =
-        List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc exec_state ->
-            let modified = extract_impurity tenv proc_desc exec_state in
+        List.fold pre_posts ~init:ImpurityDomain.pure
+          ~f:(fun acc (exec_state : ExecutionDomain.summary) ->
+            let modified = extract_impurity tenv proc_desc (exec_state :> ExecutionDomain.t) in
             ImpurityDomain.join acc modified )
       in
       if PurityChecker.should_report proc_name && not (ImpurityDomain.is_pure impurity_astate) then

infer/src/pulse/Pulse.ml

@@ -23,29 +23,26 @@ let check_error_transform {InterproceduralAnalysis.proc_desc; err_log} ~f = func
   | Ok astate ->
       f astate
   | Error (diagnostic, astate) -> (
-      let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
-      if is_unsat then []
+      let astate_summary = AbductiveDomain.summary_of_post proc_desc astate in
+      if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then []
       else
-        let astate = AbductiveDomain.of_post proc_desc astate in
-        if PulseArithmetic.is_unsat_cheap astate then []
-        else
-          match LatentIssue.should_report_diagnostic astate diagnostic with
-          | `ReportNow ->
-              report proc_desc err_log diagnostic ;
-              [ExecutionDomain.AbortProgram astate]
-          | `DelayReport latent_issue ->
-              ( if Config.pulse_report_latent_issues then
-                (* HACK: report latent issues with a prominent message to distinguish them from
-                   non-latent. Useful for infer's own tests. *)
-                let diagnostic = LatentIssue.to_diagnostic latent_issue in
-                let extra_trace =
-                  let depth = 0 in
-                  let tags = [] in
-                  let location = Diagnostic.get_location diagnostic in
-                  [Errlog.make_trace_element depth location "*** LATENT ***" tags]
-                in
-                report ~extra_trace proc_desc err_log diagnostic ) ;
-              [ExecutionDomain.LatentAbortProgram {astate; latent_issue}] )
+        match LatentIssue.should_report_diagnostic astate_summary diagnostic with
+        | `ReportNow ->
+            report proc_desc err_log diagnostic ;
+            [ExecutionDomain.AbortProgram astate_summary]
+        | `DelayReport latent_issue ->
+            ( if Config.pulse_report_latent_issues then
+              (* HACK: report latent issues with a prominent message to distinguish them from
+                 non-latent. Useful for infer's own tests. *)
+              let diagnostic = LatentIssue.to_diagnostic latent_issue in
+              let extra_trace =
+                let depth = 0 in
+                let tags = [] in
+                let location = Diagnostic.get_location diagnostic in
+                [Errlog.make_trace_element depth location "*** LATENT ***" tags]
+              in
+              report ~extra_trace proc_desc err_log diagnostic ) ;
+            [ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}] )
 
 
 let check_error_continue analysis_data result =
@@ -72,13 +69,14 @@ module PulseTransferFunctions = struct
     AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals
 
 
-  let interprocedural_call {InterproceduralAnalysis.analyze_dependency} ret call_exp actuals
-      call_loc astate =
+  let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc} ret call_exp
+      actuals call_loc astate =
     match proc_name_of_call call_exp with
     | Some callee_pname when not Config.pulse_intraprocedural_only ->
         let formals_opt = get_pvar_formals callee_pname in
         let callee_data = analyze_dependency callee_pname in
-        PulseOperations.call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt astate
+        PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret
+          ~actuals ~formals_opt astate
     | _ ->
         L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ;
         PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals

infer/src/pulse/PulseAbductiveDomain.ml

@@ -432,7 +432,9 @@ let invalidate_locals pdesc astate : t =
   else {astate with post= PostDomain.update astate.post ~attrs:attrs'}
 
 
-let of_post pdesc astate =
+type summary = t
+
+let summary_of_post pdesc astate =
   let astate = filter_for_summary astate in
   let astate, live_addresses, _ = discard_unreachable astate in
   let astate =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -158,7 +158,12 @@ val add_skipped_calls : SkippedCalls.t -> t -> t
 
 val set_path_condition : PathCondition.t -> t -> t
 
-val of_post : Procdesc.t -> t -> t
+(** private type to make sure {!summary_of_post} is always called when creating summaries *)
+type summary = private t
+
+val summary_of_post : Procdesc.t -> t -> summary
+(** trim the state down to just the procedure's interface (formals and globals), and simplify and
+    normalize the state *)
 
 val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t
 (** directly set the edges for the given address, bypassing abduction altogether *)

infer/src/pulse/PulseExecutionDomain.ml

@@ -12,11 +12,17 @@ open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 module LatentIssue = PulseLatentIssue
 
-type t =
-  | AbortProgram of AbductiveDomain.t
-  | ContinueProgram of AbductiveDomain.t
-  | ExitProgram of AbductiveDomain.t
-  | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t}
+(* The type variable is needed to distinguish summaries from plain states.
+
+   Some of the variants have summary-typed states instead of plain states, to ensure we have
+   normalized them and don't need to normalize them again. *)
+type 'abductive_domain_t base_t =
+  | ContinueProgram of 'abductive_domain_t
+  | ExitProgram of 'abductive_domain_t
+  | AbortProgram of AbductiveDomain.summary
+  | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
+
+type t = AbductiveDomain.t base_t
 
 let continue astate = ContinueProgram astate
 
@@ -24,13 +30,14 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
 
 let leq ~lhs ~rhs =
   match (lhs, rhs) with
-  | AbortProgram astate1, AbortProgram astate2
-  | ContinueProgram astate1, ContinueProgram astate2
-  | ExitProgram astate1, ExitProgram astate2 ->
-      AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
+  | AbortProgram astate1, AbortProgram astate2 ->
+      AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
+  | ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram astate2 ->
+      AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
   | ( LatentAbortProgram {astate= astate1; latent_issue= issue1}
     , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) ->
-      LatentIssue.equal issue1 issue2 && AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
+      LatentIssue.equal issue1 issue2
+      && AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
   | _ ->
       false
 
@@ -39,36 +46,40 @@ let pp fmt = function
   | ContinueProgram astate ->
       AbductiveDomain.pp fmt astate
   | ExitProgram astate ->
-      F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp astate
+      F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
   | AbortProgram astate ->
-      F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp astate
+      F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
   | LatentAbortProgram {astate; latent_issue} ->
       let diagnostic = LatentIssue.to_diagnostic latent_issue in
       let message = Diagnostic.get_message diagnostic in
       let location = Diagnostic.get_location diagnostic in
       F.fprintf fmt "{LatentAbortProgram(%a: %s) %a}" Location.pp location message
-        AbductiveDomain.pp astate
+        AbductiveDomain.pp
+        (astate :> AbductiveDomain.t)
 
 
 let map ~f exec_state =
   match exec_state with
-  | AbortProgram astate ->
-      AbortProgram (f astate)
   | ContinueProgram astate ->
       ContinueProgram (f astate)
   | ExitProgram astate ->
       ExitProgram (f astate)
+  | AbortProgram astate ->
+      AbortProgram astate
   | LatentAbortProgram {astate; latent_issue} ->
-      LatentAbortProgram {astate= f astate; latent_issue}
+      LatentAbortProgram {astate; latent_issue}
+
 
+type summary = AbductiveDomain.summary base_t
 
-let of_posts pdesc posts =
+let summary_of_posts pdesc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
-      let ( AbortProgram astate
-          | ContinueProgram astate
-          | ExitProgram astate
-          | LatentAbortProgram {astate} ) =
-        exec_state
+      let astate =
+        match exec_state with
+        | AbortProgram astate | LatentAbortProgram {astate} ->
+            (astate :> AbductiveDomain.t)
+        | ContinueProgram astate | ExitProgram astate ->
+            astate
       in
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
       let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in
@@ -77,4 +88,4 @@ let of_posts pdesc posts =
         Some
           (map exec_state ~f:(fun _astate ->
                (* prefer [astate] since it is an equivalent state that has been normalized *)
-               AbductiveDomain.of_post pdesc astate )) )
+               AbductiveDomain.summary_of_post pdesc astate )) )

infer/src/pulse/PulseExecutionDomain.mli

@@ -9,18 +9,22 @@ open! IStd
 module AbductiveDomain = PulseAbductiveDomain
 module LatentIssue = PulseLatentIssue
 
-type t =
-  | AbortProgram of AbductiveDomain.t
+type 'abductive_domain_t base_t =
+  | ContinueProgram of 'abductive_domain_t  (** represents the state at the program point *)
+  | ExitProgram of 'abductive_domain_t  (** represents the state originating at exit/divergence. *)
+  | AbortProgram of AbductiveDomain.summary
       (** represents the state at the program point that caused an error *)
-  | ContinueProgram of AbductiveDomain.t  (** represents the state at the program point *)
-  | ExitProgram of AbductiveDomain.t  (** represents the state originating at exit/divergence. *)
-  | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t}
+  | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
       (** this path leads to an error but we don't have conclusive enough data to report it yet *)
 
+type t = AbductiveDomain.t base_t
+
 include AbstractDomain.NoJoin with type t := t
 
 val continue : AbductiveDomain.t -> t
 
-val of_posts : Procdesc.t -> t list -> t list
-
 val mk_initial : Procdesc.t -> t
+
+type summary = AbductiveDomain.summary base_t
+
+val summary_of_posts : Procdesc.t -> t list -> summary list

infer/src/pulse/PulseLatentIssue.ml

@@ -7,6 +7,8 @@
 
 open! IStd
 open PulseBasicInterface
+module AbductiveDomain = PulseAbductiveDomain
+module Arithmetic = PulseArithmetic
 
 type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriving equal]
 
@@ -20,9 +22,13 @@ let add_call call_and_loc = function
       AccessToInvalidAddress {access with calling_context= call_and_loc :: access.calling_context}
 
 
-let should_report astate = PulseArithmetic.has_no_assumptions astate
+let should_report (astate : AbductiveDomain.summary) =
+  Arithmetic.has_no_assumptions (astate :> AbductiveDomain.t)
 
-let should_report_diagnostic astate (diagnostic : Diagnostic.t) =
+
+(* require a summary because we don't want to stop reporting because some non-abducible condition is
+   not true as calling context cannot possibly influence such conditions *)
+let should_report_diagnostic (astate : AbductiveDomain.summary) (diagnostic : Diagnostic.t) =
   match diagnostic with
   | MemoryLeak _ | StackVariableAddressEscape _ ->
       (* these issues are reported regardless of the calling context, not sure if that's the right

infer/src/pulse/PulseLatentIssue.mli

@@ -7,6 +7,7 @@
 
 open! IStd
 open PulseBasicInterface
+module AbductiveDomain = PulseAbductiveDomain
 
 (** A subset of [PulseDiagnostic] that can be "latent", i.e. there is a potential issue in the code
     but we want to delay reporting until we see the conditions for the bug manifest themselves in
@@ -16,9 +17,9 @@ type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriv
 
 val to_diagnostic : t -> Diagnostic.t
 
-val should_report : PulseAbductiveDomain.t -> bool
+val should_report : AbductiveDomain.summary -> bool
 
 val should_report_diagnostic :
-  PulseAbductiveDomain.t -> Diagnostic.t -> [`ReportNow | `DelayReport of t]
+  AbductiveDomain.summary -> Diagnostic.t -> [`ReportNow | `DelayReport of t]
 
 val add_call : CallEvent.t * Location.t -> t -> t

infer/src/pulse/PulseModels.ml

@@ -456,7 +456,7 @@ end
 module StdFunction = struct
   let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals :
       model =
-   fun {analyze_dependency} ~callee_procname:_ location ~ret astate ->
+   fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate ->
     let havoc_ret (ret_id, _) astate =
       let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in
       [PulseOperations.havoc_id ret_id [event] astate]
@@ -475,7 +475,7 @@ module StdFunction = struct
           :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} ->
                  (arg_payload, typ) )
         in
-        PulseOperations.call
+        PulseOperations.call ~caller_proc_desc:proc_desc
           ~callee_data:(analyze_dependency callee_proc_name)
           location callee_proc_name ~ret ~actuals ~formals_opt:None astate
 

infer/src/pulse/PulseOperations.ml

@@ -437,8 +437,8 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate =
   |> havoc_ret ret |> add_skipped_proc
 
 
-let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_with_actuals ~formals
-    ~actuals astate =
+let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
+    ~captured_vars_with_actuals ~formals ~actuals astate =
   let apply callee_prepost ~f =
     PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals
       ~formals ~actuals astate
@@ -467,13 +467,18 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit
   | ExitProgram astate ->
       apply astate ~f:(fun astate -> Ok (Some (ExitProgram astate)))
   | LatentAbortProgram {astate; latent_issue} ->
-      apply astate ~f:(fun astate ->
-          let latent_issue =
-            LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
-          in
-          if LatentIssue.should_report astate then
-            Error (LatentIssue.to_diagnostic latent_issue, astate)
-          else Ok (Some (LatentAbortProgram {astate; latent_issue})) )
+      apply
+        (astate :> AbductiveDomain.t)
+        ~f:(fun astate ->
+          let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in
+          if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Ok None
+          else
+            let latent_issue =
+              LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
+            in
+            if LatentIssue.should_report astate_summary then
+              Error (LatentIssue.to_diagnostic latent_issue, (astate_summary :> AbductiveDomain.t))
+            else Ok (Some (LatentAbortProgram {astate= astate_summary; latent_issue})) )
 
 
 let get_captured_actuals location ~captured_vars ~actual_closure astate =
@@ -488,8 +493,9 @@ let get_captured_actuals location ~captured_vars ~actual_closure astate =
   (astate, captured_vars_with_actuals)
 
 
-let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t)
-    : (ExecutionDomain.t list, Diagnostic.t * t) result =
+let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc
+    callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) :
+    (ExecutionDomain.t list, Diagnostic.t * t) result =
   match callee_data with
   | Some (callee_proc_desc, exec_states) ->
       let formals =
@@ -516,12 +522,14 @@ let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate :
             Str.string_match regex (Procname.to_string callee_pname) 0 )
       in
       (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
-      IContainer.fold_result_until exec_states ~fold:List.fold ~init:[]
+      IContainer.fold_result_until
+        (exec_states :> ExecutionDomain.t list)
+        ~fold:List.fold ~init:[]
         ~f:(fun posts callee_exec_state ->
           (* apply all pre/post specs *)
           match
-            apply_callee callee_pname call_loc callee_exec_state ~captured_vars_with_actuals
-              ~formals ~actuals ~ret astate
+            apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state
+              ~captured_vars_with_actuals ~formals ~actuals ~ret astate
           with
           | Ok None ->
               (* couldn't apply pre/post pair *)

infer/src/pulse/PulseOperations.mli

@@ -124,7 +124,8 @@ val check_address_escape :
   Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result
 
 val call :
-     callee_data:(Procdesc.t * PulseSummary.t) option
+     caller_proc_desc:Procdesc.t
+  -> callee_data:(Procdesc.t * PulseSummary.t) option
   -> Location.t
   -> Procname.t
   -> ret:Ident.t * Typ.t

infer/src/pulse/PulseSummary.ml

@@ -9,17 +9,17 @@ open! IStd
 module F = Format
 open PulseDomainInterface
 
-type t = ExecutionDomain.t list
+type t = ExecutionDomain.summary list
 
 let pp fmt summary =
   F.open_vbox 0 ;
   F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ;
-  List.iteri summary ~f:(fun i pre_post ->
-      F.fprintf fmt "#%d: @[%a@]@;" i ExecutionDomain.pp pre_post ) ;
+  List.iteri summary ~f:(fun i (pre_post : ExecutionDomain.summary) ->
+      F.fprintf fmt "#%d: @[%a@]@;" i ExecutionDomain.pp (pre_post :> ExecutionDomain.t) ) ;
   F.close_box ()
 
 
 let of_posts pdesc posts =
   AnalysisCallbacks.html_debug_new_node_session (Procdesc.get_exit_node pdesc)
     ~pp_name:(fun fmt -> F.pp_print_string fmt "pulse summary creation")
-    ~f:(fun () -> ExecutionDomain.of_posts pdesc posts)
+    ~f:(fun () -> ExecutionDomain.summary_of_posts pdesc posts)

infer/src/pulse/PulseSummary.mli

@@ -8,7 +8,7 @@
 open! IStd
 open PulseDomainInterface
 
-type t = ExecutionDomain.t list
+type t = ExecutionDomain.summary list
 
 val of_posts : Procdesc.t -> ExecutionDomain.t list -> t
 

infer/src/topl/Topl.ml

@@ -304,10 +304,10 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi
     List.iter ~f:handle_preposts preposts
 
 
-let add_errors_pulse {InterproceduralAnalysis.proc_desc; err_log} pulse_summary =
+let add_errors_pulse {InterproceduralAnalysis.proc_desc; err_log} (pulse_summary : PulseSummary.t) =
   let pulse_summary =
     let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in
-    List.filter_map ~f pulse_summary
+    List.filter_map ~f (pulse_summary :> PulseExecutionDomain.t list)
   in
   let proc_name = Procdesc.get_proc_name proc_desc in
   if not (ToplUtils.is_synthesized proc_name) then