[pulse][minor] update documentation for AbductiveDomain.t

Summary: A few cosmetic changes and documentation.

Reviewed By: da319

Differential Revision: D26020884

fbshipit-source-id: 2ec1aab29

infer/src/pulse/PulseAbductiveDomain.ml

@@ -86,30 +86,31 @@ end
 (** represents the inferred pre-condition at each program point, biabduction style *)
 module PreDomain : BaseDomainSig = PostDomain
 
-module PostStatus = struct
-  type t = ISLOk | ISLError [@@deriving equal]
+type isl_status = ISLOk | ISLError [@@deriving equal, yojson_of]
 
-  let pp f s =
+let pp_isl_status f s =
+  if Config.pulse_isl then
     match s with
     | ISLOk ->
         F.pp_print_string f "ISLOk:"
     | ISLError ->
         F.pp_print_string f "ISLError:"
-end
+  else ()
+
 
-(** biabduction-style pre/post state + skipped calls *)
+(* see documentation in this file's .mli *)
 type t =
-  { post: PostDomain.t  (** state at the current program point*)
-  ; pre: PreDomain.t  (** inferred pre at the current program point *)
-  ; topl: (PulseTopl.state[@yojson.opaque])
-  ; skipped_calls: SkippedCalls.t  (** set of skipped calls *)
+  { post: PostDomain.t
+  ; pre: PreDomain.t
   ; path_condition: PathCondition.t
-  ; isl_status: (PostStatus.t[@yojson.opaque]) }
+  ; topl: (PulseTopl.state[@yojson.opaque])
+  ; skipped_calls: SkippedCalls.t
+  ; isl_status: isl_status }
 [@@deriving yojson_of]
 
 let pp f {post; pre; topl; path_condition; skipped_calls; isl_status} =
   F.fprintf f "@[<v>%a@;%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp
-    path_condition PostStatus.pp isl_status PostDomain.pp post PreDomain.pp pre SkippedCalls.pp
+    path_condition pp_isl_status isl_status PostDomain.pp post PreDomain.pp pre SkippedCalls.pp
     skipped_calls PulseTopl.pp_state topl
 
 
@@ -119,7 +120,7 @@ let set_path_condition path_condition astate = {astate with path_condition}
 
 let leq ~lhs ~rhs =
   SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls
-  && PostStatus.equal lhs.isl_status rhs.isl_status
+  && equal_isl_status lhs.isl_status rhs.isl_status
   &&
   match
     BaseDomain.isograph_map BaseDomain.empty_mapping

infer/src/pulse/PulseAbductiveDomain.mli

@@ -52,24 +52,33 @@ module PostDomain : BaseDomainSig
     collapse into one. * *)
 module PreDomain : BaseDomainSig
 
-module PostStatus : sig
-  type t = ISLOk | ISLError [@@deriving equal]
-end
-
-(** biabduction-style pre/post state + skipped calls *)
+(** Execution status, similar to {!PulseExecutionDomain} but for ISL (Incorrectness Separation
+    Logic) mode, where {!PulseExecutionDomain.ContinueProgram} can also contain "error specs" that
+    describe what happens when some addresses are invalid explicitly instead of relying on
+    [MustBeValid] attributes. *)
+type isl_status =
+  | ISLOk  (** ok triple: the program executes without error *)
+  | ISLError
+      (** Error specification: an invalid address recorded in the precondition will cause an error *)
+[@@deriving equal]
+
+(** pre/post on a single program path *)
 type t = private
   { post: PostDomain.t  (** state at the current program point*)
-  ; pre: PreDomain.t  (** inferred pre at the current program point *)
-  ; topl: PulseTopl.state  (** state at of the Topl monitor at the current program point *)
-  ; skipped_calls: SkippedCalls.t  (** set of skipped calls *)
-  ; path_condition: PathCondition.t  (** arithmetic facts *)
-  ; isl_status: PostStatus.t  (** isl summary status *) }
+  ; pre: PreDomain.t  (** inferred procedure pre-condition leading to the current program point *)
+  ; path_condition: PathCondition.t
+        (** arithmetic facts true along the path (holding for both [pre] and [post] since abstract
+            values are immutable) *)
+  ; topl: PulseTopl.state
+        (** state at of the Topl monitor at the current program point, when Topl is enabled *)
+  ; skipped_calls: SkippedCalls.t  (** metadata: procedure calls for which no summary was found *)
+  ; isl_status: isl_status }
 
 val leq : lhs:t -> rhs:t -> bool
 
 val pp : Format.formatter -> t -> unit
 
-val set_isl_status : PostStatus.t -> t -> t
+val set_isl_status : isl_status -> t -> t
 
 val mk_initial : Procdesc.t -> t
 

infer/src/pulse/PulseInterproc.ml

@@ -637,9 +637,9 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
 let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location
     {AbductiveDomain.pre; _} pre_astate astate =
   match astate.AbductiveDomain.isl_status with
-  | AbductiveDomain.PostStatus.ISLOk ->
+  | ISLOk ->
       Ok astate
-  | AbductiveDomain.PostStatus.ISLError ->
+  | ISLError ->
       AbstractValue.Map.fold
         (fun addr_pre (addr_caller, hist_caller) astate_result ->
           let mk_access_trace callee_access_trace =