[pulse][1/2] new kind of latent issues to remove some FNs

Summary:
This first commit introduces test cases and the new summary type, in
particular how it is propagated during function calls. We don't yet
actually generate these summary types, this is for the next diff.

The goal is to catch this pattern:

```
foo(p) {
  if(p) {}
  *p = 42;
}

goo() { foo(NULL); }
```

We went foo(p) to be a latent error when p=0. Right now we detect a
contradiction p|->- * p=0 |- false. The next diff will fix it.

Reviewed By: skcho

Differential Revision: D26918552

fbshipit-source-id: 6614db17b

infer/src/checkers/impurity.ml

@@ -162,7 +162,10 @@ 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}
+    | LatentInvalidAccess {astate}
+    | ISLLatentMemoryError astate ->
         ((astate :> AbductiveDomain.t), false)
   in
   let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in

infer/src/pulse/Pulse.ml

@@ -86,7 +86,11 @@ module PulseTransferFunctions = struct
         (* invalidate [&x] *)
         PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate
         >>| ExecutionDomain.continue
-    | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
+    | ISLLatentMemoryError _
+    | AbortProgram _
+    | ExitProgram _
+    | LatentAbortProgram _
+    | LatentInvalidAccess _ ->
         Ok exec_state
 
 
@@ -104,7 +108,11 @@ module PulseTransferFunctions = struct
       match exec_state with
       | ContinueProgram astate ->
           ContinueProgram (do_astate astate)
-      | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ ->
+      | ISLLatentMemoryError _
+      | AbortProgram _
+      | LatentAbortProgram _
+      | ExitProgram _
+      | LatentInvalidAccess _ ->
           exec_state
     in
     List.map ~f:(Result.map ~f:do_one_exec_state) exec_state_res
@@ -240,7 +248,11 @@ module PulseTransferFunctions = struct
         call_instr ;
       List.concat_map astate_list ~f:(fun (astate : Domain.t) ->
           match astate with
-          | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
+          | ISLLatentMemoryError _
+          | AbortProgram _
+          | ExitProgram _
+          | LatentAbortProgram _
+          | LatentInvalidAccess _ ->
               [astate]
           | ContinueProgram astate ->
               dispatch_call analysis_data ret call_exp actuals location call_flags astate
@@ -262,9 +274,7 @@ module PulseTransferFunctions = struct
       ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node
       (instr : Sil.instr) : Domain.t list =
     match astate with
-    | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ ->
-        (* We can also continue the analysis with the error state here
-                 but there might be a risk we would get nonsense. *)
+    | AbortProgram _ | ISLLatentMemoryError _ | LatentAbortProgram _ | LatentInvalidAccess _ ->
         [astate]
     | ExitProgram _ ->
         (* program already exited, simply propagate the exited state upwards  *)
@@ -344,7 +354,11 @@ module PulseTransferFunctions = struct
           let remove_vars vars astates =
             List.concat_map astates ~f:(fun (astate : Domain.t) ->
                 match astate with
-                | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
+                | ISLLatentMemoryError _
+                | AbortProgram _
+                | ExitProgram _
+                | LatentAbortProgram _
+                | LatentInvalidAccess _ ->
                     [astate]
                 | ContinueProgram astate ->
                     PulseOperations.remove_vars tenv vars location astate

infer/src/pulse/PulseExecutionDomain.ml

@@ -20,6 +20,11 @@ type 'abductive_domain_t base_t =
   | ExitProgram of AbductiveDomain.summary
   | AbortProgram of AbductiveDomain.summary
   | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
+  | LatentInvalidAccess of
+      { astate: AbductiveDomain.summary
+      ; address: AbstractValue.t
+      ; must_be_valid: (Trace.t[@yojson.opaque])
+      ; calling_context: ((CallEvent.t * Location.t) list[@yojson.opaque]) }
   | ISLLatentMemoryError of AbductiveDomain.summary
 [@@deriving equal, compare, yojson_of]
 
@@ -43,19 +48,23 @@ let leq ~lhs ~rhs =
     , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) ->
       LatentIssue.equal issue1 issue2
       && AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
+  | ( LatentInvalidAccess {astate= astate1; address= v1; must_be_valid= _}
+    , LatentInvalidAccess {astate= astate2; address= v2; must_be_valid= _} ) ->
+      AbstractValue.equal v1 v2
+      && AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t)
   | _ ->
       false
 
 
 let pp fmt = function
+  | AbortProgram astate ->
+      F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
   | 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 ->
-      F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t)
+  | ISLLatentMemoryError astate ->
+      F.fprintf fmt "{ISLLatentMemoryError %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
@@ -63,6 +72,9 @@ let pp fmt = function
       F.fprintf fmt "{LatentAbortProgram(%a: %s) %a}" Location.pp location message
         AbductiveDomain.pp
         (astate :> AbductiveDomain.t)
+  | LatentInvalidAccess {astate; address; must_be_valid= _} ->
+      F.fprintf fmt "{LatentInvalidAccess(%a) %a}" AbstractValue.pp address AbductiveDomain.pp
+        (astate :> AbductiveDomain.t)
 
 
 (* do not export this function as there lies wickedness: clients should generally care about what
@@ -73,6 +85,7 @@ let get_astate : t -> AbductiveDomain.t = function
   | ExitProgram astate
   | AbortProgram astate
   | LatentAbortProgram {astate}
+  | LatentInvalidAccess {astate}
   | ISLLatentMemoryError astate ->
       (astate :> AbductiveDomain.t)
 

infer/src/pulse/PulseExecutionDomain.mli

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+open PulseBasicInterface
 module AbductiveDomain = PulseAbductiveDomain
 module LatentIssue = PulseLatentIssue
 
@@ -17,6 +18,13 @@ 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 *)
+  | LatentInvalidAccess of
+      { astate: AbductiveDomain.summary
+      ; address: AbstractValue.t
+      ; must_be_valid: Trace.t
+      ; calling_context: (CallEvent.t * Location.t) list }
+      (** if [address] is ever observed to be invalid then there is an invalid access because it
+          [must_be_valid] *)
   | ISLLatentMemoryError of AbductiveDomain.summary
       (** represents the state at the program point that might cause an error; used for
           {!Config.pulse_isl} *)

infer/src/pulse/PulseInterproc.ml

@@ -745,10 +745,10 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p
               astate
           else Ok astate
         in
-        (astate, return_caller)
+        (astate, return_caller, call_state.subst)
       with
-      | post ->
-          Sat post
+      | result ->
+          Sat result
       | exception Contradiction reason ->
           L.d_printfln "Cannot apply post-condition: %a" pp_contradiction reason ;
           Unsat )

infer/src/pulse/PulseInterproc.mli

@@ -18,4 +18,15 @@ val apply_prepost :
   -> formals:Var.t list
   -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
   -> AbductiveDomain.t
-  -> (AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) option) AccessResult.t SatUnsat.t
+  -> ( AbductiveDomain.t
+     * (AbstractValue.t * ValueHistory.t) option
+     * (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t )
+     AccessResult.t
+     SatUnsat.t
+(** result of applying one pre/post pair of a callee's summary:
+
+    - {!SatUnsat.Unsat} if that path in the callee is infeasible
+    - otherwise, there can be an error detected
+    - otherwise, the result is a new abstract state, an optional return value, and a substitution
+      [callee_abstract_value -> caller_abstract_value] mapping callee's abstract values to what they
+      became in the new (caller) state *)

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -41,6 +41,7 @@ let mk_objc_method_nil_summary {InterproceduralAnalysis.tenv; proc_desc; err_log
   | ExitProgram _, _
   | AbortProgram _, _
   | LatentAbortProgram _, _
+  | LatentInvalidAccess _, _
   | ISLLatentMemoryError _, _ ->
       None
 
@@ -55,7 +56,11 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log}
         PulseArithmetic.prune_positive (fst value) astate
       in
       PulseReport.report_result tenv proc_desc err_log result
-  | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ ->
+  | ExitProgram _
+  | AbortProgram _
+  | LatentAbortProgram _
+  | LatentInvalidAccess _
+  | ISLLatentMemoryError _ ->
       [astate]
 
 

infer/src/pulse/PulseOperations.ml

@@ -20,6 +20,11 @@ module Import = struct
     | ExitProgram of AbductiveDomain.summary
     | AbortProgram of AbductiveDomain.summary
     | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
+    | LatentInvalidAccess of
+        { astate: AbductiveDomain.summary
+        ; address: AbstractValue.t
+        ; must_be_valid: Trace.t
+        ; calling_context: (CallEvent.t * Location.t) list }
     | ISLLatentMemoryError of AbductiveDomain.summary
 
   type 'astate base_error = 'astate AccessResult.error =
@@ -622,7 +627,7 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
     with
     | (Sat (Error _) | Unsat) as path_result ->
         path_result
-    | Sat (Ok (post, return_val_opt)) ->
+    | Sat (Ok (post, return_val_opt, subst)) ->
         let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in
         let post =
           match return_val_opt with
@@ -631,28 +636,31 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
           | None ->
               havoc_id (fst ret) [event] post
         in
-        f post
+        f subst post
   in
   let open ExecutionDomain in
   let open SatUnsat.Import in
   match callee_exec_state with
   | ContinueProgram astate ->
-      map_call_result ~is_isl_error_prepost:false astate ~f:(fun astate ->
+      map_call_result ~is_isl_error_prepost:false astate ~f:(fun _subst astate ->
           Sat (Ok (ContinueProgram astate)) )
-  | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} ->
+  | AbortProgram astate
+  | ExitProgram astate
+  | LatentAbortProgram {astate}
+  | LatentInvalidAccess {astate} ->
       map_call_result ~is_isl_error_prepost:false
         (astate :> AbductiveDomain.t)
-        ~f:(fun astate ->
-          let+ (astate_summary : AbductiveDomain.summary) =
+        ~f:(fun subst astate ->
+          let* (astate_summary : AbductiveDomain.summary) =
             AbductiveDomain.summary_of_post tenv caller_proc_desc astate
           in
           match callee_exec_state with
           | ContinueProgram _ | ISLLatentMemoryError _ ->
               assert false
           | AbortProgram _ ->
-              Ok (AbortProgram astate_summary)
+              Sat (Ok (AbortProgram astate_summary))
           | ExitProgram _ ->
-              Ok (ExitProgram astate_summary)
+              Sat (Ok (ExitProgram astate_summary))
           | LatentAbortProgram {latent_issue} -> (
               let latent_issue =
                 LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
@@ -660,15 +668,43 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
               let diagnostic = LatentIssue.to_diagnostic latent_issue in
               match LatentIssue.should_report astate_summary diagnostic with
               | `DelayReport latent_issue ->
-                  Ok (LatentAbortProgram {astate= astate_summary; latent_issue})
+                  Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue}))
               | `ReportNow ->
-                  Error
+                  Sat
+                    (Error
                        (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)}))
               )
+          | LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> (
+            match AbstractValue.Map.find_opt address_callee subst with
+            | None ->
+                (* the address became unreachable so the bug can never be reached; drop it *) Unsat
+            | Some (address, _history) -> (
+                let calling_context = (CallEvent.Call callee_pname, call_loc) :: calling_context in
+                match
+                  AbductiveDomain.find_post_cell_opt address (astate_summary :> AbductiveDomain.t)
+                  |> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs)
+                with
+                | None ->
+                    (* still no proof that the address is invalid *)
+                    Sat
+                      (Ok
+                         (LatentInvalidAccess
+                            {astate= astate_summary; address; must_be_valid; calling_context}))
+                | Some (invalidation, invalidation_trace) ->
+                    Sat
+                      (Error
+                         (ReportableError
+                            { diagnostic=
+                                AccessToInvalidAddress
+                                  { calling_context
+                                  ; invalidation
+                                  ; invalidation_trace
+                                  ; access_trace= must_be_valid }
+                            ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) )
   | ISLLatentMemoryError astate ->
       map_call_result ~is_isl_error_prepost:true
         (astate :> AbductiveDomain.t)
-        ~f:(fun astate ->
+        ~f:(fun _subst astate ->
           let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in
           Ok (ISLLatentMemoryError astate_summary) )
 

infer/src/pulse/PulseOperations.mli

@@ -27,6 +27,11 @@ module Import : sig
     | ExitProgram of AbductiveDomain.summary
     | AbortProgram of AbductiveDomain.summary
     | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
+    | LatentInvalidAccess of
+        { astate: AbductiveDomain.summary
+        ; address: AbstractValue.t
+        ; must_be_valid: Trace.t
+        ; calling_context: (CallEvent.t * Location.t) list }
     | ISLLatentMemoryError of AbductiveDomain.summary
 
   type 'astate base_error = 'astate AccessResult.error =

infer/src/pulse/PulseSummary.ml

@@ -37,6 +37,8 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate :
       Some (ExitProgram astate)
   | LatentAbortProgram {astate; latent_issue} ->
       Some (LatentAbortProgram {astate; latent_issue})
+  | LatentInvalidAccess {astate; address; must_be_valid; calling_context} ->
+      Some (LatentInvalidAccess {astate; address; must_be_valid; calling_context})
   | ISLLatentMemoryError astate ->
       Some (ISLLatentMemoryError astate)