[pulse] check MustBeValid from preconditions all at once at the end

Summary:
Instead of checking that each address in the pre that must be valid is
not invalid in the caller (and error out if it turns out it is invalid)
as we discover them, save these checks for after we are sure that the
precondition can be applied. It is in fact a bug that we can report an
error when trying to apply a precondition that is actually not
satisfiable in the current state for other reasons than lifetime issues.

We still want to skip calls in case of weird issues like mismatch in
number of formals vs actuals.

This will have more obvious effects later when we also check that
arithmetic facts in preconditions are satisfied at the call site: if a
pre mandates "x=1" and "y must be valid" and we have "x=0" and "y
invalid" then we shouldn't report an error.

Reviewed By: skcho

Differential Revision: D18115229

fbshipit-source-id: ad4ce72ff

infer/src/pulse/PulseAbductiveDomain.ml

@@ -426,28 +426,14 @@ module PrePost = struct
      addresses are traversed in the process. *)
   let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre
       ~addr_hist_caller call_state =
-    let add_call trace =
-      Trace.ViaCall
-        { in_call= trace
-        ; f= Call callee_proc_name
-        ; location= call_location
-        ; history= snd addr_hist_caller }
-    in
     match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with
     | `AlreadyVisited, call_state ->
         Ok call_state
     | `NotAlreadyVisited, call_state -> (
-        (let open Option.Monad_infix in
-        BaseMemory.find_opt addr_pre pre.BaseDomain.heap
-        >>= fun (edges_pre, attrs_pre) ->
-        Attributes.get_must_be_valid attrs_pre
-        >>| fun callee_access_trace ->
-        let access_trace = add_call callee_access_trace in
-        match Memory.check_valid access_trace (fst addr_hist_caller) call_state.astate with
-        | Error invalidated_by ->
-            Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace})
-        | Ok astate ->
-            let call_state = {call_state with astate} in
+      match BaseMemory.find_opt addr_pre pre.BaseDomain.heap with
+      | None ->
+          Ok call_state
+      | Some (edges_pre, _attrs_pre) ->
           Container.fold_result
             ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold)
             ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) ->
@@ -456,8 +442,7 @@ module PrePost = struct
               in
               let call_state = {call_state with astate} in
               materialize_pre_from_address callee_proc_name call_location ~pre
-                  ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state ))
-        |> function Some result -> result | None -> Ok call_state )
+                ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state ) )
 
 
   (** materialize subgraph of [pre] rooted at the address represented by a [formal] parameter that
@@ -804,6 +789,32 @@ module PrePost = struct
     r
 
 
+  let check_all_valid callee_proc_name call_location {pre; post= _} call_state =
+    AddressMap.fold
+      (fun addr_pre (addr_caller, hist_caller) astate_result ->
+        match astate_result with
+        | Error _ ->
+            astate_result
+        | Ok astate -> (
+          match BaseMemory.get_must_be_valid addr_pre (pre :> BaseDomain.t).heap with
+          | None ->
+              astate_result
+          | Some callee_access_trace ->
+              let access_trace =
+                Trace.ViaCall
+                  { in_call= callee_access_trace
+                  ; f= Call callee_proc_name
+                  ; location= call_location
+                  ; history= hist_caller }
+              in
+              Memory.check_valid access_trace addr_caller astate
+              |> Result.map_error ~f:(fun invalidated_by ->
+                     L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
+                     Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace}
+                 ) ) )
+      call_state.subst (Ok call_state.astate)
+
+
   (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff
        in the *current* pre as appropriate so that callers of the current procedure will also know
        about the deeper reads)
@@ -835,13 +846,17 @@ module PrePost = struct
     | None ->
         (* couldn't apply the pre for some technical reason (as in: not by the fault of the
            programmer as far as we know) *)
-        Ok None
+        Ok (Some (astate, None))
     | Some (Error _ as error) ->
         (* error: the function call requires to read some state known to be invalid *)
         error
     | Some (Ok call_state) ->
+        L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ;
+        let open Result.Monad_infix in
+        check_all_valid callee_proc_name call_location pre_post call_state
+        >>= fun astate ->
         (* reset [visited] *)
-        let call_state = {call_state with visited= AddressSet.empty} in
+        let call_state = {call_state with astate; visited= AddressSet.empty} in
         (* apply the postcondition *)
         Ok (Some (apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state))
 end

infer/src/pulse/PulseBaseMemory.ml

@@ -91,6 +91,8 @@ let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
 
 let get_constant = get_attribute Attributes.get_constant
 
+let get_must_be_valid = get_attribute Attributes.get_must_be_valid
+
 let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory
 
 let is_std_vector_reserved address memory =

infer/src/pulse/PulseBaseMemory.mli

@@ -62,6 +62,8 @@ val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
 val get_constant : AbstractValue.t -> t -> Const.t option
 
+val get_must_be_valid : AbstractValue.t -> t -> unit Trace.t option
+
 val std_vector_reserve : AbstractValue.t -> t -> t
 
 val is_std_vector_reserved : AbstractValue.t -> t -> bool