Pulse with explicit Ok/Error summaries

Reviewed By: jvillard

Differential Revision: D25428280

fbshipit-source-id: c6faf58ea

infer/man/man1/infer-full.txt

@@ -1767,6 +1767,11 @@ INTERNAL OPTIONS
            experimentations only. (Conversely:
            --no-pulse-intraprocedural-only)
 
+       --pulse-isl
+           Activates: [Pulse] Incorrectness Separation Logic (ISL) mode:
+           explicit Ok/Error summaries are recorded. For experiments only.
+           (Conversely: --no-pulse-isl)
+
        --pulse-max-disjuncts int
            Under-approximate after int disjunctions in the domain
 

infer/src/base/Config.ml

@@ -1865,17 +1865,17 @@ and pulse_cut_to_one_path_procedures_pattern =
      large procedures to prevent too-big states from being produced."
 
 
-and pulse_recency_limit =
-  CLOpt.mk_int ~long:"pulse-recency-limit" ~default:32
-    "Maximum number of array elements and structure fields to keep track of for a given array \
-     address."
-
-
 and pulse_intraprocedural_only =
   CLOpt.mk_bool ~long:"pulse-intraprocedural-only"
     "Disable inter-procedural analysis in Pulse. Used for experimentations only."
 
 
+and pulse_isl =
+  CLOpt.mk_bool ~long:"pulse-isl" ~default:false
+    "[Pulse] Incorrectness Separation Logic (ISL) mode: explicit Ok/Error summaries are recorded. \
+     For experiments only."
+
+
 and pulse_max_disjuncts =
   CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:20
     "Under-approximate after $(i,int) disjunctions in the domain"
@@ -1918,6 +1918,12 @@ and pulse_model_transfer_ownership =
      are method or namespace::method"
 
 
+and pulse_recency_limit =
+  CLOpt.mk_int ~long:"pulse-recency-limit" ~default:32
+    "Maximum number of array elements and structure fields to keep track of for a given array \
+     address."
+
+
 and pulse_report_latent_issues =
   CLOpt.mk_bool ~long:"pulse-report-latent-issues"
     "Only use for testing, there should be no need to turn this on for regular code analysis. \
@@ -3098,10 +3104,10 @@ and pulse_cut_to_one_path_procedures_pattern =
   Option.map ~f:Str.regexp !pulse_cut_to_one_path_procedures_pattern
 
 
-and pulse_recency_limit = !pulse_recency_limit
-
 and pulse_intraprocedural_only = !pulse_intraprocedural_only
 
+and pulse_isl = !pulse_isl
+
 and pulse_max_disjuncts = !pulse_max_disjuncts
 
 and pulse_model_abort = !pulse_model_abort
@@ -3135,6 +3141,8 @@ and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership =
   List.partition_map ~f:aux models
 
 
+and pulse_recency_limit = !pulse_recency_limit
+
 and pulse_report_latent_issues = !pulse_report_latent_issues
 
 and pulse_widen_threshold = !pulse_widen_threshold

infer/src/base/Config.mli

@@ -461,10 +461,10 @@ val project_root : string
 
 val pulse_cut_to_one_path_procedures_pattern : Str.regexp option
 
-val pulse_recency_limit : int
-
 val pulse_intraprocedural_only : bool
 
+val pulse_isl : bool [@@warning "-32"]
+
 val pulse_max_disjuncts : int
 
 val pulse_model_abort : string list
@@ -483,6 +483,8 @@ val pulse_model_transfer_ownership : string list
 
 val pulse_report_latent_issues : bool
 
+val pulse_recency_limit : int
+
 val pulse_widen_threshold : int
 
 val pure_by_default : bool

infer/src/checkers/impurity.ml

@@ -165,7 +165,7 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur
         ((astate :> AbductiveDomain.t), true)
     | ContinueProgram astate ->
         (astate, false)
-    | AbortProgram astate | LatentAbortProgram {astate} ->
+    | ISLLatentMemoryError astate | AbortProgram astate | LatentAbortProgram {astate} ->
         ((astate :> AbductiveDomain.t), false)
   in
   let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in

infer/src/pulse/Pulse.ml

@@ -105,7 +105,7 @@ module PulseTransferFunctions = struct
         (* invalidate [&x] *)
         PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate
         >>| ExecutionDomain.continue
-    | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
+    | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
         Ok exec_state
 
 
@@ -123,7 +123,7 @@ module PulseTransferFunctions = struct
       match exec_state with
       | ContinueProgram astate ->
           ContinueProgram (do_astate astate)
-      | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ ->
+      | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ ->
           exec_state
     in
     Result.map ~f:(List.map ~f:do_one_exec_state) exec_state_res
@@ -254,7 +254,7 @@ module PulseTransferFunctions = struct
         ~f:(fun astates (astate : Domain.t) ->
           let astate =
             match astate with
-            | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
+            | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
                 [astate]
             | ContinueProgram astate ->
                 dispatch_call analysis_data ret call_exp actuals location call_flags astate
@@ -278,7 +278,7 @@ module PulseTransferFunctions = struct
   let exec_instr_aux (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
       _cfg_node (instr : Sil.instr) : Domain.t list =
     match astate with
-    | AbortProgram _ | LatentAbortProgram _ ->
+    | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ ->
         (* We can also continue the analysis with the error state here
                  but there might be a risk we would get nonsense. *)
         [astate]
@@ -335,7 +335,7 @@ module PulseTransferFunctions = struct
             List.fold
               ~f:(fun astates (astate : Domain.t) ->
                 match astate with
-                | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
+                | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
                     [astate]
                 | ContinueProgram astate ->
                     let astate =

infer/src/pulse/PulseExecutionDomain.ml

@@ -21,6 +21,7 @@ type 'abductive_domain_t base_t =
   | ExitProgram of AbductiveDomain.summary
   | AbortProgram of AbductiveDomain.summary
   | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
+  | ISLLatentMemoryError of AbductiveDomain.summary
 [@@deriving yojson_of]
 
 type t = AbductiveDomain.t base_t
@@ -31,7 +32,9 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
 
 let leq ~lhs ~rhs =
   match (lhs, rhs) with
-  | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 ->
+  | AbortProgram astate1, AbortProgram astate2
+  | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2
+  | ExitProgram astate1, ExitProgram astate2 ->
       AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
   | ContinueProgram astate1, ContinueProgram astate2 ->
       AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
@@ -46,6 +49,8 @@ let leq ~lhs ~rhs =
 let pp fmt = function
   | ContinueProgram astate ->
       AbductiveDomain.pp fmt astate
+  | ISLLatentMemoryError astate ->
+      F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
   | ExitProgram astate ->
       F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
   | AbortProgram astate ->
@@ -64,7 +69,10 @@ let pp fmt = function
 let get_astate : t -> AbductiveDomain.t = function
   | ContinueProgram astate ->
       astate
-  | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} ->
+  | ISLLatentMemoryError astate
+  | ExitProgram astate
+  | AbortProgram astate
+  | LatentAbortProgram {astate} ->
       (astate :> AbductiveDomain.t)
 
 
@@ -83,6 +91,8 @@ let summary_of_posts_common ~continue_program pdesc posts =
         | Sat astate ->
             Some (continue_program astate) )
       (* already a summary but need to reconstruct the variants to make the type system happy *)
+      | ISLLatentMemoryError astate ->
+          Some (ISLLatentMemoryError astate)
       | AbortProgram astate ->
           Some (AbortProgram astate)
       | ExitProgram astate ->

infer/src/pulse/PulseExecutionDomain.mli

@@ -17,6 +17,9 @@ type 'abductive_domain_t base_t =
       (** represents the state at the program point that caused an error *)
   | 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 *)
+  | ISLLatentMemoryError of AbductiveDomain.summary
+      (** represents the state at the program point that might cause an error; used for
+          {!Config.pulse_isl} *)
 
 type t = AbductiveDomain.t base_t
 

infer/src/pulse/PulseOperations.ml

@@ -487,12 +487,18 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
   match callee_exec_state with
   | ContinueProgram astate ->
       map_call_result astate ~f:(fun astate -> Sat (Ok (ContinueProgram astate)))
-  | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} ->
+  | ISLLatentMemoryError astate
+  | AbortProgram astate
+  | ExitProgram astate
+  | LatentAbortProgram {astate} ->
       map_call_result
         (astate :> AbductiveDomain.t)
         ~f:(fun astate ->
           let+ astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in
           match callee_exec_state with
+          | ISLLatentMemoryError _ ->
+              (* TODO: check invalid of inter-procedural analysis *)
+              Ok (ISLLatentMemoryError astate_summary)
           | ContinueProgram _ ->
               assert false
           | AbortProgram _ ->