[pulse] refactor initial state creation

Summary:
The creation of the inital state has evolved several times recently,
time for a refactor:
- do not create then pass the initial state around when callees can
  create it instead
- slightly hackish assertions that creating the initial state conditions
  cannot fail to simplify the types (could eventually be moved in
  AbductiveDomain.ml to avoid breaking abstraction layers like this, but
  trivial enough that it doesn't really matter I think)

Reviewed By: skcho

Differential Revision: D29550319

fbshipit-source-id: 63919ae71

infer/src/pulse/Pulse.ml

@@ -471,25 +471,25 @@ let with_debug_exit_node proc_desc ~f =
     ~f
 
 
+let initial tenv proc_desc =
+  [ ( ContinueProgram (PulseObjectiveCSummary.mk_initial_with_positive_self tenv proc_desc)
+    , PathContext.initial ) ]
+
+
 let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) =
   AbstractValue.State.reset () ;
-  let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in
-  let initial_self_positive =
-    PulseObjectiveCSummary.append_objc_self_positive analysis_data initial_astate
-  in
-  let initial = List.map ~f:(fun initial -> (initial, PathContext.initial)) initial_self_positive in
-  match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with
+  match
+    DisjunctiveAnalyzer.compute_post analysis_data ~initial:(initial tenv proc_desc) proc_desc
+  with
   | Some posts ->
       (* forget path contexts, we don't propagate them across functions *)
       let posts = List.map ~f:fst posts in
       with_debug_exit_node proc_desc ~f:(fun () ->
-          let updated_posts =
-            PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts
-          in
+          let objc_nil_summary = PulseObjectiveCSummary.mk_nil_messaging_summary tenv proc_desc in
           let summary =
             PulseSummary.of_posts tenv proc_desc err_log
               (Procdesc.get_exit_node proc_desc |> Procdesc.Node.get_loc)
-              updated_posts
+              (Option.to_list objc_nil_summary @ posts)
           in
           report_topl_errors proc_desc err_log summary ;
           Some summary )

infer/src/pulse/PulseCallOperations.ml

@@ -285,8 +285,7 @@ let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.
       astate_unknown
     in
     let result_unknown_nil =
-      PulseObjectiveCSummary.mk_objc_method_nil_summary tenv procdesc
-        (ExecutionDomain.mk_initial tenv procdesc)
+      PulseObjectiveCSummary.mk_nil_messaging_summary tenv procdesc
       |> Option.value_map ~default:[] ~f:(fun nil_summary ->
              call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals procdesc
                [nil_summary] astate )

infer/src/pulse/PulseExecutionDomain.ml

@@ -32,8 +32,6 @@ type t = AbductiveDomain.t base_t
 
 let continue astate = ContinueProgram astate
 
-let mk_initial tenv pdesc = ContinueProgram (AbductiveDomain.mk_initial tenv pdesc)
-
 let leq ~lhs ~rhs =
   phys_equal lhs rhs
   ||

infer/src/pulse/PulseExecutionDomain.mli

@@ -35,8 +35,6 @@ include AbstractDomain.Disjunct with type t := t
 
 val continue : AbductiveDomain.t -> t
 
-val mk_initial : Tenv.t -> Procdesc.t -> t
-
 val is_unsat_cheap : t -> bool
 (** see {!PulsePathCondition.is_unsat_cheap} *)
 

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -38,10 +38,11 @@ let init_fields_zero tenv path location ~zero addr typ astate =
 
 (** Constructs summary [{self = 0} {return = self}] when [proc_desc] returns a POD type. This allows
     us to connect invalidation with invalid access in the trace *)
-let mk_objc_method_nil_summary_aux tenv proc_desc astate =
+let mk_nil_messaging_summary_aux tenv proc_desc =
   let path = PathContext.initial in
   let location = Procdesc.get_loc proc_desc in
   let self = mk_objc_self_pvar proc_desc in
+  let astate = AbductiveDomain.mk_initial tenv proc_desc in
   (* HACK: we are operating on an "empty" initial state and do not expect to create any alarms
      (nothing is Invalid in the initial state) or unsatisfiability (we won't create arithmetic
      contradictions) *)
@@ -71,12 +72,13 @@ let mk_objc_method_nil_summary_aux tenv proc_desc astate =
       |> assert_ok
 
 
-let mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate =
-  (* same HACK as above *)
-  let assert_ok = function Ok x -> x | Error _ -> assert false in
+let mk_latent_non_POD_nil_messaging tenv proc_desc =
   let path = PathContext.initial in
   let location = Procdesc.get_loc proc_desc in
   let self = mk_objc_self_pvar proc_desc in
+  let astate = AbductiveDomain.mk_initial tenv proc_desc in
+  (* same HACK as above *)
+  let assert_ok = function Ok x -> x | Error _ -> assert false in
   let astate, (self_value, _self_history) =
     PulseOperations.eval_deref path location (Lvar self) astate |> assert_ok
   in
@@ -94,50 +96,41 @@ let mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate =
         ; calling_context= [] }
 
 
-let mk_objc_method_nil_summary tenv proc_desc initial =
+let mk_nil_messaging_summary tenv proc_desc =
   let proc_name = Procdesc.get_proc_name proc_desc in
-  match (initial, proc_name) with
-  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
+  match proc_name with
+  | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
       if Procdesc.is_ret_type_pod proc_desc then
         (* In ObjC, when a method is called on nil, there is no NPE,
            the method is actually not called and the return value is 0/false/nil.
            We create a nil summary to avoid reporting NPE in this case.
            However, there is an exception in the case where the return type is non-POD.
            In that case it's UB and we want to report an error. *)
-        let astate = mk_objc_method_nil_summary_aux tenv proc_desc astate in
+        let astate = mk_nil_messaging_summary_aux tenv proc_desc in
         Some (ContinueProgram astate)
       else
-        let summary = mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate in
+        let summary = mk_latent_non_POD_nil_messaging tenv proc_desc in
         Some summary
-  | ContinueProgram _, _
-  | ExitProgram _, _
-  | AbortProgram _, _
-  | LatentAbortProgram _, _
-  | LatentInvalidAccess _, _
-  | ISLLatentMemoryError _, _ ->
+  | _ ->
       None
 
 
-let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} astate =
+let mk_initial_with_positive_self tenv proc_desc =
   let location = Procdesc.get_loc proc_desc in
   let self = mk_objc_self_pvar proc_desc in
   let proc_name = Procdesc.get_proc_name proc_desc in
-  match (astate, proc_name) with
-  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
-      let result =
-        let* astate, value =
-          PulseOperations.eval_deref PathContext.initial location (Lvar self) astate
-        in
-        PulseArithmetic.and_positive (fst value) astate
+  let initial_astate = AbductiveDomain.mk_initial tenv proc_desc in
+  (* same HACK as above *)
+  let assert_ok = function Ok x -> x | Error _ -> assert false in
+  match proc_name with
+  | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
+      let astate, value =
+        PulseOperations.eval_deref PathContext.initial location (Lvar self) initial_astate
+        |> assert_ok
       in
-      PulseReport.report_result tenv proc_desc err_log location result
-  | ContinueProgram _, _
-  | ExitProgram _, _
-  | AbortProgram _, _
-  | LatentAbortProgram _, _
-  | LatentInvalidAccess _, _
-  | ISLLatentMemoryError _, _ ->
-      [astate]
+      PulseArithmetic.and_positive (fst value) astate |> assert_ok
+  | _ ->
+      initial_astate
 
 
 let append_objc_actual_self_positive procdesc self_actual astate =
@@ -148,11 +141,3 @@ let append_objc_actual_self_positive procdesc self_actual astate =
           PulseArithmetic.prune_positive self astate )
   | _ ->
       Ok astate
-
-
-let update_objc_method_posts {InterproceduralAnalysis.tenv; proc_desc} ~initial_astate ~posts =
-  match mk_objc_method_nil_summary tenv proc_desc initial_astate with
-  | None ->
-      posts
-  | Some nil_summary ->
-      nil_summary :: posts

infer/src/pulse/PulseObjectiveCSummary.mli

@@ -9,24 +9,14 @@ open! IStd
 open PulseBasicInterface
 open PulseDomainInterface
 
-val update_objc_method_posts :
-     PulseSummary.t InterproceduralAnalysis.t
-  -> initial_astate:ExecutionDomain.t
-  -> posts:ExecutionDomain.t list
-  -> ExecutionDomain.t list
-(** For ObjC instance methods: appends additional nil summary and replaces must be valid reason for
-    non-pod return type. Does nothing to posts for other kinds of methods *)
-
 val append_objc_actual_self_positive :
      Procdesc.t
   -> ((AbstractValue.t * ValueHistory.t) * Typ.t) option
   -> AbductiveDomain.t
   -> AbductiveDomain.t AccessResult.t
 
-val append_objc_self_positive :
-  PulseSummary.t InterproceduralAnalysis.t -> ExecutionDomain.t -> ExecutionDomain.t list
-(** For ObjC instance methods: adds path condition `self > 0` to a given post. Does nothing to posts
-    for other kinds of methods *)
+val mk_initial_with_positive_self : Tenv.t -> Procdesc.t -> AbductiveDomain.t
+(** The initial state of the analysis, with the additional path condition [self > 0] for Objective-C
+    instance methods. *)
 
-val mk_objc_method_nil_summary :
-  Tenv.t -> Procdesc.t -> ExecutionDomain.t -> ExecutionDomain.t option
+val mk_nil_messaging_summary : Tenv.t -> Procdesc.t -> ExecutionDomain.t option

infer/src/pulse/PulseReport.mli

@@ -8,13 +8,7 @@
 open! IStd
 open PulseDomainInterface
 
-val report_result :
-     Tenv.t
-  -> Procdesc.t
-  -> Errlog.t
-  -> Location.t
-  -> AbductiveDomain.t AccessResult.t
-  -> ExecutionDomain.t list
+[@@@warning "-32"]
 
 val report_summary_error :
      Tenv.t
@@ -23,6 +17,14 @@ val report_summary_error :
   -> AbductiveDomain.summary AccessResult.error
   -> _ ExecutionDomain.base_t
 
+val report_result :
+     Tenv.t
+  -> Procdesc.t
+  -> Errlog.t
+  -> Location.t
+  -> AbductiveDomain.t AccessResult.t
+  -> ExecutionDomain.t list
+
 val report_results :
      Tenv.t
   -> Procdesc.t