[pulse] manage path contexts (no use yet)

Summary:
Keep track of which conditionals the current instruction is being
affected by:

```
if (x) { // (1)
  a = 1; // affected by (1)
  if (y) { // (2)
    b = 1; // affected by (1) and (2)
  }
}
c = 1; // affected by no conditionals
```

Reviewed By: skcho

Differential Revision: D31479142

fbshipit-source-id: b2e749ba0

infer/src/pulse/Pulse.ml

@@ -398,18 +398,6 @@ module PulseTransferFunctions = struct
                 astates
           in
           (PulseReport.report_results tenv proc_desc err_log loc result, path, astate_n)
-      | Prune (condition, loc, _is_then_branch, _if_kind) ->
-          let results =
-            (let<*> astate = PulseOperations.prune path loc ~condition astate in
-             if PulseArithmetic.is_unsat_cheap astate then
-               (* [condition] is known to be unsatisfiable: prune path *)
-               []
-             else
-               (* [condition] is true or unknown value: go into the branch *)
-               [Ok (ContinueProgram astate)] )
-            |> PulseReport.report_exec_results tenv proc_desc err_log loc
-          in
-          (results, path, astate_n)
       | Call (ret, call_exp, actuals, loc, call_flags) ->
           let astates =
             dispatch_call analysis_data path ret call_exp actuals loc call_flags astate
@@ -419,6 +407,40 @@ module PulseTransferFunctions = struct
           , path
           , PulseNonDisjunctiveOperations.add_copies loc call_exp actuals call_flags astates
               astate_n )
+      | Prune (condition, loc, is_then_branch, if_kind) ->
+          let result, path =
+            match PulseOperations.prune path loc ~condition astate with
+            | Ok (astate, hist) ->
+                let path =
+                  if Sil.is_terminated_if_kind if_kind then
+                    let hist =
+                      ValueHistory.ConditionPassed
+                        {if_kind; is_then_branch; location= loc; timestamp}
+                      :: hist
+                    in
+                    {path with conditions= hist :: path.conditions}
+                  else path
+                in
+                (Ok astate, path)
+            | Error _ as err ->
+                (err, path)
+          in
+          let results =
+            let<*> astate = result in
+            if PulseArithmetic.is_unsat_cheap astate then
+              (* [condition] is known to be unsatisfiable: prune path *)
+              []
+            else
+              (* [condition] is true or unknown value: go into the branch *)
+              [Ok (ContinueProgram astate)]
+          in
+          (PulseReport.report_exec_results tenv proc_desc err_log loc results, path, astate_n)
+      | Metadata EndBranches ->
+          (* We assume that terminated conditions are well-parenthesised, hence an [EndBranches]
+             instruction terminates the most recently seen terminated conditional. The empty case
+             shouldn't happen but let's not crash by the fault of possible errors in frontends. *)
+          let path = {path with conditions= List.tl path.conditions |> Option.value ~default:[]} in
+          ([ContinueProgram astate], path, astate_n)
       | Metadata (ExitScope (vars, location)) ->
           let remove_vars vars astates =
             List.map astates ~f:(fun (exec_state : ExecutionDomain.t) ->
@@ -458,7 +480,6 @@ module PulseTransferFunctions = struct
       | Metadata
           ( Abstract _
           | CatchEntry _
-          | EndBranches
           | Nullify _
           | Skip
           | TryEntry _

infer/src/pulse/PulseOperations.ml

@@ -278,22 +278,33 @@ let eval path mode location exp0 astate =
   eval path mode exp0 astate
 
 
-let eval_to_operand path mode location exp astate =
+let eval_to_operand path location exp astate =
   match (exp : Exp.t) with
   | Const (Cint i) ->
-      Ok (astate, PulseArithmetic.LiteralOperand i)
+      Ok (astate, PulseArithmetic.LiteralOperand i, [])
   | exp ->
-      let+ astate, (value, _) = eval path mode location exp astate in
-      (astate, PulseArithmetic.AbstractValueOperand value)
+      let+ astate, (value, hist) = eval path Read location exp astate in
+      (astate, PulseArithmetic.AbstractValueOperand value, hist)
 
 
 let prune path location ~condition astate =
   let rec prune_aux ~negated exp astate =
     match (exp : Exp.t) with
     | BinOp (bop, exp_lhs, exp_rhs) ->
-        let* astate, lhs_op = eval_to_operand path Read location exp_lhs astate in
-        let* astate, rhs_op = eval_to_operand path Read location exp_rhs astate in
-        PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate
+        let* astate, lhs_op, lhs_hist = eval_to_operand path location exp_lhs astate in
+        let* astate, rhs_op, rhs_hist = eval_to_operand path location exp_rhs astate in
+        let+ astate = PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate in
+        let hist =
+          match (lhs_hist, rhs_hist) with
+          | [], hist | hist, [] ->
+              (* if one history is empty then just propagate the other one (which could also be
+                 empty) *)
+              hist
+          | _ ->
+              (* TODO: merge histories *)
+              lhs_hist
+        in
+        (astate, hist)
     | UnOp (LNot, exp', _) ->
         prune_aux ~negated:(not negated) exp' astate
     | exp ->

infer/src/pulse/PulseOperations.mli

@@ -117,7 +117,8 @@ val eval_structure_isl :
 (** Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states
     (ISLOk and ISLErs); The boolean indicates whether it is data structures or not. *)
 
-val prune : PathContext.t -> Location.t -> condition:Exp.t -> t -> t AccessResult.t
+val prune :
+  PathContext.t -> Location.t -> condition:Exp.t -> t -> (t * ValueHistory.t) AccessResult.t
 
 val eval_deref :
      PathContext.t

infer/src/pulse/PulsePathContext.ml

@@ -9,16 +9,22 @@ open! IStd
 module F = Format
 open PulseBasicInterface
 
-type t = {timestamp: Timestamp.t} [@@deriving compare, equal]
+type t = {conditions: ValueHistory.t list; timestamp: Timestamp.t} [@@deriving compare, equal]
 
 (** path contexts is metadata that do not contribute to the semantics *)
 let leq ~lhs:_ ~rhs:_ = true
 
 (** see [leq] *)
 let equal_fast _ _ = true
 
-let pp fmt ({timestamp} [@warning "+9"]) = F.fprintf fmt "timestamp= %a" Timestamp.pp timestamp
+let pp fmt ({conditions; timestamp} [@warning "+9"]) =
+  let pp_condition fmt hist =
+    if Config.debug_level_analysis >= 3 then F.fprintf fmt "[%a]" ValueHistory.pp hist
+  in
+  F.fprintf fmt "conditions= [%a]@;timestamp= %a" (Pp.seq ~sep:";" pp_condition) conditions
+    Timestamp.pp timestamp
 
-let initial = {timestamp= Timestamp.t0}
 
-let post_exec_instr {timestamp} = {timestamp= Timestamp.incr timestamp}
+let initial = {conditions= []; timestamp= Timestamp.t0}
+
+let post_exec_instr {conditions; timestamp} = {conditions; timestamp= Timestamp.incr timestamp}

infer/src/pulse/PulsePathContext.mli

@@ -9,7 +9,13 @@ open! IStd
 module F = Format
 open PulseBasicInterface
 
-type t = {timestamp: Timestamp.t  (** step number in an intra-procedural analysis *)}
+type t =
+  { conditions: ValueHistory.t list
+        (** Each history represents a conditional that is affecting the path currently, with the
+            most recent conditional first. The idea is to add these histories to the histories of
+            all variables and memory locations modified while under the influence of these
+            conditionals. *)
+  ; timestamp: Timestamp.t  (** step number in an intra-procedural analysis *) }
 [@@deriving compare, equal]
 
 val leq : lhs:t -> rhs:t -> bool

infer/src/pulse/PulseValueHistory.ml

@@ -20,8 +20,8 @@ type event =
       ; mode: CapturedVar.capture_mode
       ; location: Location.t
       ; timestamp: Timestamp.t }
-  | Conditional of
-      {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t; timestamp: Timestamp.t}
+  | ConditionPassed of
+      {if_kind: Sil.if_kind; is_then_branch: bool; location: Location.t; timestamp: Timestamp.t}
   | CppTemporaryCreated of Location.t * Timestamp.t
   | FormalDeclared of Pvar.t * Location.t * Timestamp.t
   | Invalidated of PulseInvalidation.t * Location.t * Timestamp.t
@@ -38,7 +38,7 @@ let location_of_event = function
   | Assignment (location, _)
   | Call {location}
   | Capture {location}
-  | Conditional {location}
+  | ConditionPassed {location}
   | CppTemporaryCreated (location, _)
   | FormalDeclared (_, location, _)
   | Invalidated (_, location, _)
@@ -58,7 +58,7 @@ let rec iter_event event ~f =
   | Allocation _
   | Assignment _
   | Capture _
-  | Conditional _
+  | ConditionPassed _
   | CppTemporaryCreated _
   | FormalDeclared _
   | Invalidated _
@@ -93,11 +93,11 @@ let pp_event_no_location fmt event =
       F.pp_print_string fmt "assigned"
   | Call {f} ->
       F.fprintf fmt "in call to %a" CallEvent.pp f
-  | Capture {captured_as; mode; location= _} ->
+  | Capture {captured_as; mode} ->
       F.fprintf fmt "value captured %s as `%a`"
         (CapturedVar.string_of_capture_mode mode)
         Pvar.pp_value_non_verbose captured_as
-  | Conditional {is_then_branch; if_kind; location= _} ->
+  | ConditionPassed {is_then_branch; if_kind} ->
       F.fprintf fmt "expression in %a condition is %b" Sil.pp_if_kind if_kind is_then_branch
   | CppTemporaryCreated _ ->
       F.pp_print_string fmt "C++ temporary created"

infer/src/pulse/PulseValueHistory.mli

@@ -18,8 +18,8 @@ type event =
       ; mode: CapturedVar.capture_mode
       ; location: Location.t
       ; timestamp: Timestamp.t }
-  | Conditional of
-      {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t; timestamp: Timestamp.t}
+  | ConditionPassed of
+      {if_kind: Sil.if_kind; is_then_branch: bool; location: Location.t; timestamp: Timestamp.t}
   | CppTemporaryCreated of Location.t * Timestamp.t
   | FormalDeclared of Pvar.t * Location.t * Timestamp.t
   | Invalidated of PulseInvalidation.t * Location.t * Timestamp.t