[pulse] stop the analysis when precondition cannot be applied for reasons others than errors

Summary:
If a precondition cannot be applied, it means that this program path
somehow doesn't make sense for the caller and so should be pruned. Right
now we just treat this as skipping over the call instead.

This will become more important when specs start mentioning arithmetic
facts that must be satisfied at the call site. As it is we will only
stop if we discover aliasing in the pre not present at the call site or
vice versa.

Reviewed By: dulmarod

Differential Revision: D18115230

fbshipit-source-id: 4f1c7a583

infer/src/pulse/PulseAbductiveDomain.ml

@@ -831,11 +831,11 @@ module PrePost = struct
     | exception Aliasing ->
         (* can't make sense of the pre-condition in the current context: give up on that particular
            pre/post pair *)
-        Ok (astate, None)
+        Ok None
     | 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 (astate, None)
+        Ok None
     | Some (Error _ as error) ->
         (* error: the function call requires to read some state known to be invalid *)
         error
@@ -843,7 +843,7 @@ module PrePost = struct
         (* reset [visited] *)
         let call_state = {call_state with visited= AddressSet.empty} in
         (* apply the postcondition *)
-        Ok (apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state)
+        Ok (Some (apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state))
 end
 
 let extract_pre {pre} = (pre :> BaseDomain.t)

infer/src/pulse/PulseAbductiveDomain.mli

@@ -97,8 +97,9 @@ module PrePost : sig
     -> formals:Var.t list
     -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
     -> domain_t
-    -> (domain_t * (AbstractValue.t * ValueHistory.t) option, Diagnostic.t) result
+    -> ((domain_t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t) result
-  (** return the abstract state after the call along with an optional return value *)
+  (** return the abstract state after the call along with an optional return value, or [None] if
+      the precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *)
 end
 
 val discard_unreachable : t -> t

infer/src/pulse/PulseOperations.ml

@@ -371,16 +371,21 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
       List.fold_result preposts ~init:[] ~f:(fun posts pre_post ->
           (* apply all pre/post specs *)
           AbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals astate
-          >>| fun (post, return_val_opt) ->
+          >>| function
-          let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in
+          | None ->
-          let post =
+              (* couldn't apply pre/post pair *) posts
-            match return_val_opt with
+          | Some (post, return_val_opt) ->
-            | Some (return_val, return_hist) ->
+              let event =
-                write_id (fst ret) (return_val, event :: return_hist) post
+                ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []}
-            | None ->
+              in
-                havoc_id (fst ret) [event] post
+              let post =
-          in
+                match return_val_opt with
-          post :: posts )
+                | Some (return_val, return_hist) ->
+                    write_id (fst ret) (return_val, event :: return_hist) post
+                | None ->
+                    havoc_id (fst ret) [event] post
+              in
+              post :: posts )
   | None ->
       (* no spec found for some reason (unknown function, ...) *)
       L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;