[Pulse] explicit Ok/Error summaries: bi-abduction for memory read

Summary: [Pulse] explicit Ok/Error summaries: bi-abduction for LOAD

Reviewed By: jvillard

Differential Revision: D25543300

fbshipit-source-id: 6b3a80525

infer/src/base/Config.mli

@@ -467,7 +467,7 @@ val pulse_cut_to_one_path_procedures_pattern : Str.regexp option
 
 val pulse_intraprocedural_only : bool
 
-val pulse_isl : bool [@@warning "-32"]
+val pulse_isl : bool
 
 val pulse_max_disjuncts : int
 

infer/src/checkers/impurity.ml

@@ -163,9 +163,9 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur
     match exec_state with
     | ExitProgram astate ->
         ((astate :> AbductiveDomain.t), true)
-    | ContinueProgram astate ->
+    | ContinueProgram astate | ISLLatentMemoryError astate ->
         (astate, false)
-    | ISLLatentMemoryError astate | AbortProgram astate | LatentAbortProgram {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

@@ -24,7 +24,7 @@ let exec_list_of_list_result = function
 
 let report_on_error {InterproceduralAnalysis.proc_desc; err_log} result =
   PulseReport.report_error proc_desc err_log result
-  >>| (fun post -> [ExecutionDomain.ContinueProgram post])
+  >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post)
   |> exec_list_of_list_result
 
 
@@ -285,13 +285,27 @@ module PulseTransferFunctions = struct
     | ExitProgram _ ->
         (* program already exited, simply propagate the exited state upwards  *)
         [astate]
-    | ContinueProgram astate -> (
+    | ContinueProgram ({isl_status= ISLError} as astate) -> (
+      match instr with
+      | Prune (_, _, is_then_branch, _) when is_then_branch ->
+          []
+      | _ ->
+          [ContinueProgram astate] )
+    | ContinueProgram ({isl_status= ISLOk} as astate) -> (
       match instr with
       | Load {id= lhs_id; e= rhs_exp; loc} ->
           (* [lhs_id := *rhs_exp] *)
           let result =
-            let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
-            PulseOperations.write_id lhs_id rhs_addr_hist astate
+            let+ astate_rhs_addr_hists =
+              if Config.pulse_isl then
+                let+ astate_rhs_addr_hists = PulseOperations.eval_deref_isl loc rhs_exp astate in
+                astate_rhs_addr_hists
+              else
+                let+ astate_rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
+                [astate_rhs_addr_hist]
+            in
+            List.map astate_rhs_addr_hists ~f:(fun (astate, rhs_addr_hist) ->
+                PulseOperations.write_id lhs_id rhs_addr_hist astate )
           in
           report_on_error analysis_data result
       | Store {e1= lhs_exp; e2= rhs_exp; loc} ->
@@ -313,9 +327,12 @@ module PulseTransferFunctions = struct
             in
             match lhs_exp with
             | Lvar pvar when Pvar.is_return pvar ->
+                let+ astate =
                   PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate
+                in
+                [astate]
             | _ ->
-                Ok astate
+                Ok [astate]
           in
           report_on_error analysis_data result
       | Prune (condition, loc, _is_then_branch, _if_kind) ->
@@ -339,7 +356,11 @@ module PulseTransferFunctions = struct
                     astate :: astates
                 | ContinueProgram astate ->
                     let astate =
-                      PulseOperations.remove_vars vars location astate
+                      ( match PulseOperations.remove_vars vars location astate with
+                      | Ok astate ->
+                          Ok [astate]
+                      | Error _ as error ->
+                          error )
                       |> report_on_error analysis_data
                     in
                     List.rev_append astate astates )

infer/src/pulse/PulseAbductiveDomain.ml

@@ -86,24 +86,40 @@ 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]
+
+  let pp f s =
+    match s with
+    | ISLOk ->
+        F.pp_print_string f "ISLOk:"
+    | ISLError ->
+        F.pp_print_string f "ISLError:"
+end
+
 (** biabduction-style pre/post state + skipped calls *)
 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 *)
-  ; path_condition: PathCondition.t }
+  ; path_condition: PathCondition.t
+  ; isl_status: (PostStatus.t[@yojson.opaque]) }
 [@@deriving yojson_of]
 
-let pp f {post; pre; topl; path_condition; skipped_calls} =
-  F.fprintf f "@[<v>%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp path_condition
-    PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls PulseTopl.pp_state topl
+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
+    skipped_calls PulseTopl.pp_state topl
 
 
+let set_isl_error_status astate = {astate with isl_status= PostStatus.ISLError}
+
 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
   &&
   match
     BaseDomain.isograph_map BaseDomain.empty_mapping
@@ -154,7 +170,8 @@ module Stack = struct
           ; pre
           ; topl= astate.topl
           ; skipped_calls= astate.skipped_calls
-          ; path_condition= astate.path_condition }
+          ; path_condition= astate.path_condition
+          ; isl_status= astate.isl_status }
         , addr_hist )
 
 
@@ -271,6 +288,53 @@ module AddressAttributes = struct
 
   let find_opt address astate =
     BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs
+
+
+  let check_valid_isl access_trace addr ?(null_noop = false) astate =
+    L.d_printfln "*****check_valid_isl: addr*** %a@\n" AbstractValue.pp addr ;
+    match BaseAddressAttributes.get_invalid addr (astate.post :> BaseDomain.t).attrs with
+    | None -> (
+      match
+        BaseAddressAttributes.get_must_be_valid_or_allocated_isl addr
+          (astate.post :> BaseDomain.t).attrs
+      with
+      | None ->
+          let is_eq_null = PathCondition.is_known_zero astate.path_condition addr in
+          let null_astates =
+            if PathCondition.is_known_neq_zero astate.path_condition addr then []
+            else
+              let null_attr =
+                Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace)
+              in
+              let null_astate =
+                {astate with isl_status= (if null_noop then astate.isl_status else ISLError)}
+                |> add_one addr null_attr
+              in
+              let null_astate =
+                if is_eq_null then null_astate else abduce_attribute addr null_attr null_astate
+              in
+              [null_astate]
+          in
+          if is_eq_null then Ok null_astates
+          else
+            let valid_astate =
+              let abdalloc = Attribute.ISLAbduced access_trace in
+              let valid_attr = Attribute.MustBeValid access_trace in
+              add_one addr abdalloc astate |> abduce_attribute addr valid_attr
+              |> abduce_attribute addr abdalloc
+            in
+            let invalid_free =
+              (*C or Cpp?*)
+              let invalid_attr = Attribute.Invalid (CFree, access_trace) in
+              {astate with isl_status= ISLError}
+              |> abduce_attribute addr invalid_attr
+              |> add_one addr invalid_attr
+            in
+            Ok ([valid_astate; invalid_free] @ null_astates)
+      | Some _ ->
+          Ok [astate] )
+    | Some (invalidation, invalidation_trace) ->
+        Error (invalidation, invalidation_trace, {astate with isl_status= ISLError})
 end
 
 module Memory = struct
@@ -314,7 +378,8 @@ module Memory = struct
           ; pre= PreDomain.update astate.pre ~heap:foot_heap
           ; topl= astate.topl
           ; skipped_calls= astate.skipped_calls
-          ; path_condition= astate.path_condition }
+          ; path_condition= astate.path_condition
+          ; isl_status= astate.isl_status }
         , addr_hist_dst )
 
 
@@ -361,31 +426,58 @@ let mk_initial proc_desc =
   let proc_name = Procdesc.get_proc_name proc_desc in
   let location = Procdesc.get_loc proc_desc in
   let formals_and_captured =
-    let init_var mangled =
+    let init_var mangled typ =
       let pvar = Pvar.mk mangled proc_name in
-      (Var.of_pvar pvar, (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]))
+      ( Var.of_pvar pvar
+      , typ
+      , (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) )
     in
     let formals =
-      Procdesc.get_formals proc_desc |> List.map ~f:(fun (mangled, _) -> init_var mangled)
+      Procdesc.get_formals proc_desc |> List.map ~f:(fun (mangled, typ) -> init_var mangled typ)
     in
     let captured =
-      Procdesc.get_captured proc_desc |> List.map ~f:(fun {CapturedVar.name} -> init_var name)
+      Procdesc.get_captured proc_desc
+      |> List.map ~f:(fun {CapturedVar.name; CapturedVar.typ} -> init_var name typ)
     in
     captured @ formals
   in
   let initial_stack =
     List.fold formals_and_captured ~init:(PreDomain.empty :> BaseDomain.t).stack
-      ~f:(fun stack (formal, addr_loc) -> BaseStack.add formal addr_loc stack)
+      ~f:(fun stack (formal, _, addr_loc) -> BaseStack.add formal addr_loc stack)
   in
-  let pre =
   let initial_heap =
+    let register heap (_, _, (addr, _)) = BaseMemory.register_address addr heap in
+    let isl_register_and_add_edge heap ((_, typ, (addr, _)) as arg) =
+      let heap = register heap arg in
+      match typ.Typ.desc with
+      | Typ.Tptr _ ->
+          let addr_dst = AbstractValue.mk_fresh () in
+          BaseMemory.add_edge addr Dereference (addr_dst, []) heap
+          |> BaseMemory.register_address addr_dst
+      | _ ->
+          heap
+    in
     List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).heap
-        ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap)
+      ~f:(if Config.pulse_isl then isl_register_and_add_edge else register)
   in
-    PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty
+  let initial_attrs =
+    if Config.pulse_isl then
+      List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).attrs
+        ~f:(fun attrs (_, _, (addr, _)) ->
+          BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []})) attrs )
+    else (PreDomain.empty :> base_domain).attrs
+  in
+  let pre =
+    PreDomain.update ~stack:initial_stack ~heap:initial_heap ~attrs:initial_attrs PreDomain.empty
   in
   let locals = Procdesc.get_locals proc_desc in
-  let post = PostDomain.update ~stack:initial_stack PostDomain.empty in
+  let initial_heap, initial_attrs =
+    if Config.pulse_isl then (initial_heap, initial_attrs)
+    else ((PreDomain.empty :> base_domain).heap, (PreDomain.empty :> base_domain).attrs)
+  in
+  let post =
+    PostDomain.update ~stack:initial_stack ~heap:initial_heap ~attrs:initial_attrs PostDomain.empty
+  in
   let post =
     List.fold locals ~init:post ~f:(fun (acc : PostDomain.t) {ProcAttributes.name; typ} ->
         set_uninitialized_post (`LocalDecl (Pvar.mk name proc_name, None)) typ location acc )
@@ -394,7 +486,8 @@ let mk_initial proc_desc =
   ; post
   ; topl= PulseTopl.start ()
   ; skipped_calls= SkippedCalls.empty
-  ; path_condition= PathCondition.true_ }
+  ; path_condition= PathCondition.true_
+  ; isl_status= ISLOk }
 
 
 let add_skipped_call pname trace astate =
@@ -435,7 +528,10 @@ let discard_unreachable ({pre; post} as astate) =
 
 let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var)
 
-let set_post_edges addr edges astate = Memory.map_post_heap astate ~f:(BaseMemory.add addr edges)
+let set_post_edges addr edges astate =
+  if BaseMemory.Edges.is_empty edges then astate
+  else Memory.map_post_heap astate ~f:(BaseMemory.add addr edges)
+
 
 (* {3 Helper functions to traverse the two maps at once } *)
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -52,18 +52,25 @@ 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 *)
 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 *) }
+  ; path_condition: PathCondition.t  (** arithmetic facts *)
+  ; isl_status: PostStatus.t  (** isl summary status *) }
 
 val leq : lhs:t -> rhs:t -> bool
 
 val pp : Format.formatter -> t -> unit
 
+val set_isl_error_status : t -> t
+
 val mk_initial : Procdesc.t -> t
 
 val get_pre : t -> BaseDomain.t
@@ -147,6 +154,13 @@ module AddressAttributes : sig
   val std_vector_reserve : AbstractValue.t -> t -> t
 
   val find_opt : AbstractValue.t -> t -> Attributes.t option
+
+  val check_valid_isl :
+       Trace.t
+    -> AbstractValue.t
+    -> ?null_noop:bool
+    -> t
+    -> (t list, Invalidation.t * Trace.t * t) result
 end
 
 val is_local : Var.t -> t -> bool

infer/src/pulse/PulseAttribute.ml

@@ -32,6 +32,7 @@ module Attribute = struct
     | DynamicType of Typ.Name.t
     | EndOfCollection
     | Invalid of Invalidation.t * Trace.t
+    | ISLAbduced of Trace.t
     | MustBeInitialized of Trace.t
     | MustBeValid of Trace.t
     | StdVectorReserve
@@ -72,6 +73,8 @@ module Attribute = struct
 
   let end_of_collection_rank = Variants.to_rank EndOfCollection
 
+  let isl_abduced_rank = Variants.to_rank (ISLAbduced dummy_trace)
+
   let uninitialized_rank = Variants.to_rank Uninitialized
 
   let must_be_initialized_rank = Variants.to_rank (MustBeInitialized dummy_trace)
@@ -100,6 +103,8 @@ module Attribute = struct
         F.fprintf f "Invalid %a"
           (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
           trace
+    | ISLAbduced trace ->
+        F.fprintf f "ISLAbduced %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "ISLAbduced")) trace
     | MustBeInitialized trace ->
         F.fprintf f "MustBeInitialized %a"
           (Trace.pp ~pp_immediate:(pp_string_if_debug "read"))
@@ -174,6 +179,13 @@ module Attributes = struct
            (procname, trace) )
 
 
+  let get_isl_abduced attrs =
+    Set.find_rank attrs Attribute.isl_abduced_rank
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.ISLAbduced trace) = attr in
+           trace )
+
+
   let get_dynamic_type attrs =
     Set.find_rank attrs Attribute.dynamic_type_rank
     |> Option.map ~f:(fun attr ->
@@ -196,13 +208,13 @@ include Attribute
 let is_suitable_for_pre = function
   | MustBeValid _ | MustBeInitialized _ ->
       true
+  | Invalid _ | Allocated _ | ISLAbduced _ ->
+      Config.pulse_isl
   | AddressOfCppTemporary _
   | AddressOfStackVariable _
-  | Allocated _
   | Closure _
   | DynamicType _
   | EndOfCollection
-  | Invalid _
   | StdVectorReserve
   | Uninitialized
   | WrittenTo _ ->
@@ -212,6 +224,8 @@ let is_suitable_for_pre = function
 let map_trace ~f = function
   | Allocated (procname, trace) ->
       Allocated (procname, f trace)
+  | ISLAbduced trace ->
+      ISLAbduced (f trace)
   | Invalid (invalidation, trace) ->
       Invalid (invalidation, f trace)
   | MustBeValid trace ->

infer/src/pulse/PulseAttribute.mli

@@ -19,6 +19,7 @@ type t =
   | DynamicType of Typ.Name.t
   | EndOfCollection
   | Invalid of Invalidation.t * Trace.t
+  | ISLAbduced of Trace.t  (** The allocation is abduced so as the analysis could run normally *)
   | MustBeInitialized of Trace.t
   | MustBeValid of Trace.t
   | StdVectorReserve
@@ -48,6 +49,8 @@ module Attributes : sig
 
   val get_invalid : t -> (Invalidation.t * Trace.t) option
 
+  val get_isl_abduced : t -> Trace.t option
+
   val get_must_be_valid : t -> Trace.t option
 
   val get_written_to : t -> Trace.t option

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -112,8 +112,22 @@ let initialize address attrs =
 
 let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
 
+let get_invalid = get_attribute Attributes.get_invalid
+
 let get_must_be_valid = get_attribute Attributes.get_must_be_valid
 
+let get_must_be_valid_or_allocated_isl address attrs =
+  match get_must_be_valid address attrs with
+  | Some trace ->
+      Some trace
+  | None -> (
+    match get_attribute Attributes.get_allocation address attrs with
+    | Some (_, trace) ->
+        Some trace
+    | None ->
+        get_attribute Attributes.get_isl_abduced address attrs )
+
+
 let get_must_be_initialized = get_attribute Attributes.get_must_be_initialized
 
 let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -37,8 +37,12 @@ val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.
 
 val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
+val get_invalid : AbstractValue.t -> t -> (Invalidation.t * Trace.t) option
+
 val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
 
+val get_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> Trace.t option
+
 val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option
 
 val std_vector_reserve : AbstractValue.t -> t -> t

infer/src/pulse/PulseCItv.ml

@@ -174,6 +174,13 @@ let is_equal_to_zero = function
       false
 
 
+let is_not_equal_to_zero = function
+  | Outside (l, u) ->
+      IntLit.iszero l && IntLit.iszero u
+  | _ ->
+      false
+
+
 let as_int = function Between (Int l, Int u) when IntLit.eq l u -> IntLit.to_int l | _ -> None
 
 let has_empty_intersection a1 a2 =

infer/src/pulse/PulseCItv.mli

@@ -15,6 +15,9 @@ val equal_to : IntLit.t -> t
 
 val is_equal_to_zero : t -> bool
 
+val is_not_equal_to_zero : t -> bool
+(** whether this is literally [≠0] *)
+
 val as_int : t -> int option
 (** [as_int v] returns [Some x] if [v] is known to be [x] *)
 

infer/src/pulse/PulseExecutionDomain.ml

@@ -21,7 +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
+  | ISLLatentMemoryError of 'abductive_domain_t
 [@@deriving yojson_of]
 
 type t = AbductiveDomain.t base_t
@@ -32,11 +32,10 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
 
 let leq ~lhs ~rhs =
   match (lhs, rhs) with
-  | AbortProgram astate1, AbortProgram astate2
-  | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2
-  | ExitProgram astate1, ExitProgram astate2 ->
+  | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 ->
       AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
-  | ContinueProgram astate1, ContinueProgram astate2 ->
+  | ContinueProgram astate1, ContinueProgram astate2
+  | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 ->
       AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
   | ( LatentAbortProgram {astate= astate1; latent_issue= issue1}
     , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) ->
@@ -50,7 +49,7 @@ let pp fmt = function
   | ContinueProgram astate ->
       AbductiveDomain.pp fmt astate
   | ISLLatentMemoryError astate ->
-      F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
+      F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp astate
   | ExitProgram astate ->
       F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
   | AbortProgram astate ->
@@ -67,12 +66,9 @@ let pp fmt = function
 (* do not export this function as there lies wickedness: clients should generally care about what
    kind of state they are manipulating so let's not encourage them not to *)
 let get_astate : t -> AbductiveDomain.t = function
-  | ContinueProgram astate ->
+  | ContinueProgram astate | ISLLatentMemoryError astate ->
       astate
-  | ISLLatentMemoryError astate
-  | ExitProgram astate
-  | AbortProgram astate
-  | LatentAbortProgram {astate} ->
+  | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} ->
       (astate :> AbductiveDomain.t)
 
 
@@ -84,15 +80,13 @@ let summary_of_posts_common ~continue_program pdesc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
       match exec_state with
-      | ContinueProgram astate -> (
+      | ContinueProgram astate | ISLLatentMemoryError astate -> (
         match AbductiveDomain.summary_of_post pdesc astate with
         | Unsat ->
             None
         | 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 ->
@@ -102,7 +96,12 @@ let summary_of_posts_common ~continue_program pdesc posts =
 
 
 let summary_of_posts =
-  summary_of_posts_common ~continue_program:(fun astate -> ContinueProgram astate)
+  summary_of_posts_common ~continue_program:(fun astate ->
+      match (astate :> AbductiveDomain.t).isl_status with
+      | ISLOk ->
+          ContinueProgram astate
+      | ISLError ->
+          ISLLatentMemoryError astate )
 
 
 let force_exit_program =

infer/src/pulse/PulseExecutionDomain.mli

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

infer/src/pulse/PulseOperations.ml

@@ -36,6 +36,38 @@ let check_addr_access access_mode location (address, history) astate =
       Ok astate
 
 
+let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false)
+    astate =
+  let access_trace = Trace.Immediate {location; history} in
+  let* astates =
+    AddressAttributes.check_valid_isl access_trace address ~null_noop astate
+    |> Result.map_error ~f:(fun (invalidation, invalidation_trace, astate) ->
+           ( Diagnostic.AccessToInvalidAddress
+               {calling_context= []; invalidation; invalidation_trace; access_trace}
+           , astate ) )
+  in
+  match access_mode with
+  | Read ->
+      List.fold_result astates ~init:[] ~f:(fun astates astate ->
+          match AddressAttributes.check_initialized access_trace address astate with
+          | Error _ ->
+              Error
+                ( Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}
+                , AbductiveDomain.set_isl_error_status astate )
+          | Ok ok_astate ->
+              Ok (ok_astate :: astates) )
+  | Write ->
+      Ok
+        (List.map astates ~f:(fun astate ->
+             match astate.AbductiveDomain.isl_status with
+             | ISLOk ->
+                 AbductiveDomain.initialize address astate
+             | ISLError ->
+                 astate ))
+  | NoAccess ->
+      Ok astates
+
+
 module Closures = struct
   module Memory = AbductiveDomain.Memory
 
@@ -115,6 +147,21 @@ let eval_access mode location addr_hist access astate =
   Memory.eval_edge addr_hist access astate
 
 
+let eval_access_biad_isl mode location addr_hist access astate =
+  let map_ok addr_hist access astates =
+    List.map
+      ~f:(fun astate ->
+        match astate.AbductiveDomain.isl_status with
+        | ISLOk ->
+            Memory.eval_edge addr_hist access astate
+        | ISLError ->
+            (astate, addr_hist) )
+      astates
+  in
+  let+ astates = check_and_abduce_addr_access_isl mode location addr_hist astate in
+  map_ok addr_hist access astates
+
+
 let eval mode location exp0 astate =
   let rec eval mode exp astate =
     match (exp : Exp.t) with
@@ -196,6 +243,61 @@ let eval_deref location exp astate =
   Memory.eval_edge addr_hist Dereference astate
 
 
+let eval_structure_isl mode loc exp astate =
+  match (exp : Exp.t) with
+  | Lfield (exp', field, _) ->
+      let* astate, addr_hist = eval mode loc exp' astate in
+      let+ astates =
+        eval_access_biad_isl mode loc addr_hist (HilExp.Access.FieldAccess field) astate
+      in
+      (false, astates)
+  | Lindex (exp', exp_index) ->
+      let* astate, addr_hist_index = eval mode loc exp_index astate in
+      let* astate, addr_hist = eval mode loc exp' astate in
+      let+ astates =
+        eval_access_biad_isl mode loc addr_hist
+          (HilExp.Access.ArrayAccess (StdTyp.void, fst addr_hist_index))
+          astate
+      in
+      (false, astates)
+  | _ ->
+      let+ astate, (addr, history) = eval mode loc exp astate in
+      (true, [(astate, (addr, history))])
+
+
+let eval_deref_biad_isl location access addr_hist astate =
+  let+ astates = check_and_abduce_addr_access_isl Read location addr_hist astate in
+  List.map
+    ~f:(fun astate ->
+      match astate.AbductiveDomain.isl_status with
+      | ISLOk ->
+          Memory.eval_edge addr_hist access astate
+      | ISLError ->
+          (astate, addr_hist) )
+    astates
+
+
+let eval_deref_isl location exp astate =
+  let* is_structured, ls_astate_addr_hist = eval_structure_isl Read location exp astate in
+  let eval_deref_function (astate, addr_hist) =
+    if is_structured then eval_deref_biad_isl location Dereference addr_hist astate
+    else
+      let+ astate = eval_deref location exp astate in
+      [astate]
+  in
+  List.fold ls_astate_addr_hist ~init:(Ok []) ~f:(fun acc ((astate, _) as astate_addr) ->
+      match acc with
+      | Ok acc_astates -> (
+        match astate.AbductiveDomain.isl_status with
+        | ISLOk ->
+            let+ astates = eval_deref_function astate_addr in
+            acc_astates @ astates
+        | ISLError ->
+            Ok (acc_astates @ [astate_addr]) )
+      | Error _ as a ->
+          a )
+
+
 let realloc_pvar pvar typ location astate =
   let addr = AbstractValue.mk_fresh () in
   let astate =
@@ -487,19 +589,15 @@ 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)))
-  | ISLLatentMemoryError astate
-  | AbortProgram astate
-  | ExitProgram astate
-  | LatentAbortProgram {astate} ->
+  | ISLLatentMemoryError astate ->
+      map_call_result astate ~f:(fun astate -> Sat (Ok (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 _ ->
+          | ContinueProgram _ | ISLLatentMemoryError _ ->
               assert false
           | AbortProgram _ ->
               Ok (AbortProgram astate_summary)

infer/src/pulse/PulseOperations.mli

@@ -43,6 +43,9 @@ val prune : Location.t -> condition:Exp.t -> t -> t access_result
 val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** Like [eval] but evaluates [*exp]. *)
 
+val eval_deref_isl :
+  Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) list access_result
+
 val eval_access :
      access_mode
   -> Location.t

infer/src/pulse/PulsePathCondition.ml

@@ -401,6 +401,10 @@ let is_known_zero phi v =
   || Formula.is_known_zero phi.formula v
 
 
+let is_known_neq_zero phi v =
+  CItvs.find_opt v phi.citvs |> Option.exists ~f:CItv.is_not_equal_to_zero
+
+
 let is_unsat_cheap phi = phi.is_unsat
 
 let is_unsat_expensive phi =

infer/src/pulse/PulsePathCondition.mli

@@ -62,6 +62,11 @@ val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> t * new_
 val is_known_zero : t -> AbstractValue.t -> bool
 (** [is_known_zero phi t] returns [true] if [phi |- t = 0], [false] if we don't know for sure *)
 
+val is_known_neq_zero : t -> AbstractValue.t -> bool
+(** [is_known_neq_zero phi t] returns [true] if [phi |- t != 0], [false] if we don't know for sure *)
+
+(* this only consults the concrete intervals domain for now *)
+
 val is_unsat_cheap : t -> bool
 (** whether the state contains a contradiction, call this as often as you want *)