From ab30cdb3798f4f10be5ea46293a48c700344b6bd Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 11 Apr 2019 03:55:34 -0700
Subject: [PATCH] [pulse] allow models to return disjuncts

Summary:
This is useful for the model of `exit` that returns 0 disjuncts. All
other models return 1 disjunct for now, but in the future things like
`malloc()` will need to return 2 possible states for instance.

Reviewed By: ngorogiannis

Differential Revision: D14753491

fbshipit-source-id: 3e7387d6d
---
 infer/src/pulse/Pulse.ml        |  2 +-
 infer/src/pulse/PulseModels.ml  | 39 +++++++++++++++++++--------------
 infer/src/pulse/PulseModels.mli |  2 +-
 3 files changed, 24 insertions(+), 19 deletions(-)

diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index c8a25ee64..5de1f0df5 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -178,7 +178,7 @@ module PulseTransferFunctions = struct
     in
     match model with
     | Some model ->
-        model call_loc ~ret ~actuals astate >>| fun post -> [post]
+        model call_loc ~ret ~actuals astate
     | None -> (
         (* do interprocedural call then destroy objects going out of scope *)
         PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index df428b095..4fabff7d6 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -12,12 +12,12 @@ type exec_fun =
   -> ret:Var.t * Typ.t
   -> actuals:HilExp.t list
   -> PulseAbductiveDomain.t
-  -> PulseAbductiveDomain.t PulseOperations.access_result
+  -> PulseAbductiveDomain.t list PulseOperations.access_result
 
 type model = exec_fun
 
 module Misc = struct
-  let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok PulseAbductiveDomain.empty
+  let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok []
 end
 
 module C = struct
@@ -28,8 +28,9 @@ module C = struct
         PulseOperations.invalidate
           (PulseTrace.Immediate {imm= PulseInvalidation.CFree deleted_access; location})
           location deleted_access astate
+        >>| List.return
     | _ ->
-        Ok astate
+        Ok [astate]
 end
 
 module Cplusplus = struct
@@ -42,8 +43,9 @@ module Cplusplus = struct
         PulseOperations.invalidate
           (PulseTrace.Immediate {imm= PulseInvalidation.CppDelete deleted_access; location})
           location deleted_access astate
+        >>| List.return
     | _ ->
-        Ok astate
+        Ok [astate]
 
 
   let operator_call : model =
@@ -57,9 +59,10 @@ module Cplusplus = struct
         PulseOperations.Closures.check_captured_addresses location lambda (fst address) astate
     | _ ->
         Ok astate )
-    >>| PulseOperations.havoc_var
-          [PulseTrace.Call {f= `Model "<lambda>"; actuals; location}]
-          ret_var
+    >>| fun astate ->
+    [ PulseOperations.havoc_var
+        [PulseTrace.Call {f= `Model "<lambda>"; actuals; location}]
+        ret_var astate ]
 
 
   let placement_new : model =
@@ -73,11 +76,11 @@ module Cplusplus = struct
         PulseOperations.read location expr astate
         >>= fun (astate, (address, trace)) ->
         PulseOperations.write_var ret_var (address, crumb :: trace) astate
-        |> read_all other_actuals
+        |> read_all other_actuals >>| List.return
     | _ :: other_actuals ->
-        read_all other_actuals astate >>| PulseOperations.havoc_var [crumb] ret_var
+        read_all other_actuals astate >>| PulseOperations.havoc_var [crumb] ret_var >>| List.return
     | [] ->
-        Ok (PulseOperations.havoc_var [crumb] ret_var astate)
+        Ok [PulseOperations.havoc_var [crumb] ret_var astate]
 end
 
 module StdVector = struct
@@ -118,9 +121,9 @@ module StdVector = struct
             ; actuals
             ; location }
         in
-        reallocate_internal_array [crumb] vector vector_f location astate
+        reallocate_internal_array [crumb] vector vector_f location astate >>| List.return
     | _ ->
-        Ok astate
+        Ok [astate]
 
 
   let at : model =
@@ -136,8 +139,9 @@ module StdVector = struct
           (HilExp.AccessExpression.base ret)
           (addr, crumb :: trace)
           astate
+        >>| List.return
     | _ ->
-        Ok (PulseOperations.havoc_var [crumb] (fst ret) astate)
+        Ok [PulseOperations.havoc_var [crumb] (fst ret) astate]
 
 
   let reserve : model =
@@ -147,8 +151,9 @@ module StdVector = struct
         let crumb = PulseTrace.Call {f= `Model "std::vector::reserve"; actuals; location} in
         reallocate_internal_array [crumb] vector Reserve location astate
         >>= PulseOperations.StdVector.mark_reserved location vector
+        >>| List.return
     | _ ->
-        Ok astate
+        Ok [astate]
 
 
   let push_back : model =
@@ -161,12 +166,12 @@ module StdVector = struct
         if is_reserved then
           (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
              (a perfect analysis would also make sure we don't exceed the reserved size) *)
-          Ok astate
+          Ok [astate]
         else
           (* simulate a re-allocation of the underlying array every time an element is added *)
-          reallocate_internal_array [crumb] vector PushBack location astate
+          reallocate_internal_array [crumb] vector PushBack location astate >>| List.return
     | _ ->
-        Ok astate
+        Ok [astate]
 end
 
 module ProcNameDispatcher = struct
diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli
index 109bbbd50..5188e17df 100644
--- a/infer/src/pulse/PulseModels.mli
+++ b/infer/src/pulse/PulseModels.mli
@@ -11,7 +11,7 @@ type exec_fun =
   -> ret:Var.t * Typ.t
   -> actuals:HilExp.t list
   -> PulseAbductiveDomain.t
-  -> PulseAbductiveDomain.t PulseOperations.access_result
+  -> PulseAbductiveDomain.t list PulseOperations.access_result
 
 type model = exec_fun