From 2ce0c680a79adf7e278c06f9b939da21d35be53e Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 2 Dec 2020 01:13:49 -0800
Subject: [PATCH] [topl] Added a hook for large steps in Pulse.

Summary:
When a procedure is called, we must evolve the topl component of the
PulseAbductiveDomain. This commit just inserts a call to a dummy
PulseTopl.large_step in the right place. The [large_step] function still
needs to be done.

Reviewed By: jvillard

Differential Revision: D24980825

fbshipit-source-id: 0eb280145
---
 infer/src/pulse/PulseAbductiveDomain.ml  |  4 +++-
 infer/src/pulse/PulseAbductiveDomain.mli |  7 +++++++
 infer/src/pulse/PulseInterproc.ml        | 16 +++++++++++++---
 infer/src/pulse/PulseTopl.ml             |  2 ++
 infer/src/pulse/PulseTopl.mli            | 11 +++++++++++
 5 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 22fae223c..b2185c3a7 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -491,5 +491,7 @@ module Topl = struct
   let small_step event astate =
     {astate with topl= PulseTopl.small_step astate.path_condition event astate.topl}
 
-  (* TODO: large_step *)
+
+  let large_step ~substitution ?(condition = PathCondition.true_) ~callee_prepost astate =
+    {astate with topl= PulseTopl.large_step ~substitution ~condition ~callee_prepost astate.topl}
 end
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 04a5faac5..9e6daf6ef 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -182,4 +182,11 @@ val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCo
 
 module Topl : sig
   val small_step : PulseTopl.event -> t -> t
+
+  val large_step :
+       substitution:(AbstractValue.t * ValueHistory.t) AbstractValue.Map.t
+    -> ?condition:PathCondition.t
+    -> callee_prepost:PulseTopl.state
+    -> t
+    -> t
 end
diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml
index 686ca6641..e093bfd75 100644
--- a/infer/src/pulse/PulseInterproc.ml
+++ b/infer/src/pulse/PulseInterproc.ml
@@ -492,7 +492,7 @@ let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actua
     record_post_remaining_attributes callee_proc_name call_location pre_post call_state
     |> record_skipped_calls callee_proc_name call_location pre_post
     |> conjoin_callee_arith pre_post
-    |> fun {astate; _} -> (astate, return_caller)
+    |> fun call_state -> (call_state, return_caller)
   in
   PerfEvent.(log (fun logger -> log_end_event logger ())) ;
   r
@@ -567,8 +567,18 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post
         (* reset [visited] *)
         let call_state = {call_state with astate; visited= AddressSet.empty} in
         (* apply the postcondition *)
-        apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
-          ~actuals call_state
+        let call_state, return_caller =
+          apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals
+            ~actuals call_state
+        in
+        let astate =
+          if Topl.is_deep_active () then
+            AbductiveDomain.Topl.large_step ~substitution:call_state.subst
+              ~condition:call_state.astate.path_condition
+              ~callee_prepost:pre_post.AbductiveDomain.topl call_state.astate
+          else call_state.astate
+        in
+        (astate, return_caller)
       with
       | post ->
           PulseReport.FeasiblePath post
diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml
index bf9d22533..765c0d9a9 100644
--- a/infer/src/pulse/PulseTopl.ml
+++ b/infer/src/pulse/PulseTopl.ml
@@ -35,4 +35,6 @@ let start () = (* TODO *) []
 
 let small_step _condition _event state = (* TODO *) state
 
+let large_step ~substitution:_ ~condition:_ ~callee_prepost:_ _state = (* TODO *) []
+
 let pp_state _formatter _state = (* TODO *) ()
diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli
index 20bf88513..965b14f43 100644
--- a/infer/src/pulse/PulseTopl.mli
+++ b/infer/src/pulse/PulseTopl.mli
@@ -18,4 +18,15 @@ val start : unit -> state
 
 val small_step : PulsePathCondition.t -> event -> state -> state
 
+val large_step :
+     substitution:(PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
+  -> condition:PulsePathCondition.t
+  -> callee_prepost:state
+  -> state
+  -> state
+(** [large_step ~substitution ~condition state ~callee_prepost] updates [state] according to
+    [callee_prepost]. The abstract values in [condition] and [state] are in one scope, and those in
+    [callee_prepost] in another scope: the [substitution] maps from the callee scope to the
+    condition&state scope. *)
+
 val pp_state : Format.formatter -> state -> unit