[pulse] remove traces from interval domain

Summary:
The idea was to keep track of why we know certain facts but actually
these traces are never read. Other arithmetic facts (BoItv and the path
condition) don't have histories so remove them from concrete intervals
too.

Reviewed By: dulmarod

Differential Revision: D21303353

fbshipit-source-id: eecf07b05

infer/src/pulse/Pulse.ml

@@ -177,8 +177,8 @@ module PulseTransferFunctions = struct
                 Ok astate
           in
           check_error_continue summary result
-      | Prune (condition, loc, is_then_branch, if_kind) ->
+      | Prune (condition, loc, _is_then_branch, _if_kind) ->
-          PulseOperations.prune ~is_then_branch if_kind loc ~condition astate
+          PulseOperations.prune loc ~condition astate
           |> check_error_transform summary ~f:(fun (exec_state, cond_satisfiable) ->
                  if cond_satisfiable then
                    (* [condition] is true or unknown value: go into the branch *)

infer/src/pulse/PulseAbductiveDomain.mli

@@ -137,7 +137,7 @@ module AddressAttributes : sig
 
   val std_vector_reserve : AbstractValue.t -> t -> t
 
-  val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option
+  val get_citv : AbstractValue.t -> t -> CItv.t option
 
   val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
 

infer/src/pulse/PulseArithmetic.ml

@@ -22,21 +22,21 @@ let and_term t astate =
   AbductiveDomain.set_path_condition phi astate
 
 
-let and_nonnegative trace v astate =
+let and_nonnegative v astate =
   AddressAttributes.add_one v (BoItv Itv.ItvPure.nat) astate
-  |> AddressAttributes.add_one v (CItv (CItv.zero_inf, trace))
+  |> AddressAttributes.add_one v (CItv CItv.zero_inf)
   |> and_term PathCondition.Term.(le zero (of_absval v))
 
 
-let and_positive trace v astate =
+let and_positive v astate =
   AddressAttributes.add_one v (BoItv Itv.ItvPure.pos) astate
-  |> AddressAttributes.add_one v (CItv (CItv.ge_to IntLit.one, trace))
+  |> AddressAttributes.add_one v (CItv (CItv.ge_to IntLit.one))
   |> and_term PathCondition.Term.(lt zero (of_absval v))
 
 
-let and_eq_int trace v i astate =
+let and_eq_int v i astate =
   AddressAttributes.add_one v (BoItv (Itv.ItvPure.of_int_lit i)) astate
-  |> AddressAttributes.add_one v (CItv (CItv.equal_to i, trace))
+  |> AddressAttributes.add_one v (CItv (CItv.equal_to i))
   |> and_eq_terms (PathCondition.Term.of_absval v) (PathCondition.Term.of_intlit i)
 
 
@@ -44,13 +44,13 @@ let and_eq_int trace v i astate =
 
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
 
-let eval_citv_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
+let eval_citv_operand binop_addr bop op_lhs op_rhs astate =
   let citv_of_op op astate =
     match op with
     | LiteralOperand i ->
         Some (CItv.equal_to i)
     | AbstractValueOperand v ->
-        AddressAttributes.get_citv v astate |> Option.map ~f:fst
+        AddressAttributes.get_citv v astate
   in
   match
     Option.both (citv_of_op op_lhs astate) (citv_of_op op_rhs astate)
@@ -59,8 +59,7 @@ let eval_citv_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
   | None ->
       astate
   | Some binop_a ->
-      let binop_trace = Trace.Immediate {location; history= binop_hist} in
+      let astate = AddressAttributes.add_one binop_addr (CItv binop_a) astate in
-      let astate = AddressAttributes.add_one binop_addr (CItv (binop_a, binop_trace)) astate in
       astate
 
 
@@ -91,26 +90,20 @@ let eval_path_condition_binop binop_addr binop op_lhs op_rhs astate =
     astate
 
 
-let eval_binop location binop op_lhs op_rhs binop_hist astate =
+let eval_binop binop_addr binop op_lhs op_rhs astate =
-  let binop_addr = AbstractValue.mk_fresh () in
-  let astate =
   eval_path_condition_binop binop_addr binop op_lhs op_rhs astate
-    |> eval_citv_operand location binop_addr binop_hist binop op_lhs op_rhs
+  |> eval_citv_operand binop_addr binop op_lhs op_rhs
   |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs
-  in
-  (astate, (binop_addr, binop_hist))
 
 
-let eval_unop_citv location unop_addr unop operand_addr unop_hist astate =
+let eval_unop_citv unop_addr unop operand_addr astate =
   match
-    AddressAttributes.get_citv operand_addr astate
+    AddressAttributes.get_citv operand_addr astate |> Option.bind ~f:(fun a -> CItv.unop unop a)
-    |> Option.bind ~f:(function a, _ -> CItv.unop unop a)
   with
   | None ->
       astate
   | Some unop_a ->
-      let unop_trace = Trace.Immediate {location; history= unop_hist} in
+      AddressAttributes.add_one unop_addr (CItv unop_a) astate
-      AddressAttributes.add_one unop_addr (CItv (unop_a, unop_trace)) astate
 
 
 let eval_unop_bo_itv unop_addr unop operand_addr astate =
@@ -128,14 +121,10 @@ let eval_path_condition_unop unop_addr unop addr astate =
     astate
 
 
-let eval_unop location unop addr unop_hist astate =
+let eval_unop unop_addr unop addr astate =
-  let unop_addr = AbstractValue.mk_fresh () in
-  let astate =
   eval_path_condition_unop unop_addr unop addr astate
-    |> eval_unop_citv location unop_addr unop addr unop_hist
+  |> eval_unop_citv unop_addr unop addr
   |> eval_unop_bo_itv unop_addr unop addr
-  in
-  (astate, (unop_addr, unop_hist))
 
 
 let prune_with_bop ~negated v_opt arith bop arith' astate =
@@ -157,13 +146,9 @@ let prune_with_bop ~negated v_opt arith bop arith' astate =
       (astate, true)
 
 
-let eval_operand location astate = function
+let eval_operand astate = function
   | LiteralOperand i ->
-      ( None
+      (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, PathCondition.Term.of_intlit i)
-      , Some
-          (CItv.equal_to i, Trace.Immediate {location; history= [ValueHistory.Assignment location]})
-      , Itv.ItvPure.of_int_lit i
-      , PathCondition.Term.of_intlit i )
   | AbstractValueOperand v ->
       ( Some v
       , AddressAttributes.get_citv v astate
@@ -171,32 +156,21 @@ let eval_operand location astate = function
       , PathCondition.Term.of_absval v )
 
 
-let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate =
+let record_abduced addr_opt arith_opt astate =
   match Option.both addr_opt arith_opt with
   | None ->
       astate
   | Some (addr, arith) ->
-      let trace =
+      let attribute = Attribute.CItv arith in
-        match orig_arith_hist_opt with
-        | None ->
-            Trace.Immediate {location; history= [event]}
-        | Some (_, trace) ->
-            Trace.add_event event trace
-      in
-      let attribute = Attribute.CItv (arith, trace) in
       AddressAttributes.abduce_attribute addr attribute astate
       |> AddressAttributes.add_one addr attribute
 
 
 let bind_satisfiable ~satisfiable astate ~f = if satisfiable then f astate else (astate, false)
 
-let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op astate =
+let prune_binop ~negated bop lhs_op rhs_op astate =
-  let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs =
+  let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = eval_operand astate lhs_op in
-    eval_operand location astate lhs_op
+  let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand astate rhs_op in
-  in
-  let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs =
-    eval_operand location astate rhs_op
-  in
   let astate =
     let path_condition =
       let t_positive = PathCondition.Term.of_binop bop path_cond_lhs path_cond_rhs in
@@ -205,17 +179,12 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta
     in
     AbductiveDomain.set_path_condition path_condition astate
   in
-  match
+  match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with
-    CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
-      (Option.map ~f:fst arith_rhs_opt)
-  with
   | Unsatisfiable ->
       (astate, false)
   | Satisfiable (abduced_lhs, abduced_rhs) ->
-      let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in
       let astate =
-        record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate
+        record_abduced value_lhs_opt abduced_lhs astate |> record_abduced value_rhs_opt abduced_rhs
-        |> record_abduced event location value_rhs_opt arith_rhs_opt abduced_rhs
       in
       let satisfiable =
         match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with
@@ -240,8 +209,7 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta
 (** {2 Queries} *)
 
 let is_known_zero astate v =
-  ( AddressAttributes.get_citv v astate
+  AddressAttributes.get_citv v astate |> Option.value_map ~default:false ~f:CItv.is_equal_to_zero
-  |> function Some (arith, _) -> CItv.is_equal_to_zero arith | None -> false )
   || (let phi = astate.AbductiveDomain.path_condition in
       PathCondition.is_known_zero (PathCondition.Term.of_absval v) phi )
   || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv v astate)

infer/src/pulse/PulseArithmetic.mli

@@ -11,13 +11,13 @@ module AbductiveDomain = PulseAbductiveDomain
 
 (** {2 Building arithmetic constraints} *)
 
-val and_nonnegative : Trace.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
+val and_nonnegative : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
-(** [and_nonnegative trace v astate] is [astate ∧ v≥0] *)
+(** [and_nonnegative v astate] is [astate ∧ v≥0] *)
 
-val and_positive : Trace.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
+val and_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
 (** [and_positive v astate] is [astate ∧ v>0] *)
 
-val and_eq_int : Trace.t -> AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t
+val and_eq_int : AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t
 (** [and_eq_int v i astate] is [astate ∧ v=i] *)
 
 (** {2 Operations} *)
@@ -25,32 +25,13 @@ val and_eq_int : Trace.t -> AbstractValue.t -> IntLit.t -> AbductiveDomain.t ->
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
 
 val eval_binop :
-     Location.t
+  AbstractValue.t -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t
-  -> Binop.t
-  -> operand
-  -> operand
-  -> ValueHistory.t
-  -> AbductiveDomain.t
-  -> AbductiveDomain.t * (AbstractValue.t * ValueHistory.t)
 
 val eval_unop :
-     Location.t
+  AbstractValue.t -> Unop.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t
-  -> Unop.t
-  -> AbstractValue.t
-  -> ValueHistory.t
-  -> AbductiveDomain.t
-  -> AbductiveDomain.t * (AbstractValue.t * ValueHistory.t)
 
 val prune_binop :
-     is_then_branch:bool
+  negated:bool -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t * bool
-  -> Sil.if_kind
-  -> Location.t
-  -> negated:bool
-  -> Binop.t
-  -> operand
-  -> operand
-  -> AbductiveDomain.t
-  -> AbductiveDomain.t * bool
 
 (** {2 Queries} *)
 

infer/src/pulse/PulseAttribute.ml

@@ -29,7 +29,7 @@ module Attribute = struct
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
     | Allocated of Procname.t * Trace.t
-    | CItv of CItv.t * Trace.t
+    | CItv of CItv.t
     | BoItv of Itv.ItvPure.t
     | Closure of Procname.t
     | Invalid of Invalidation.t * Trace.t
@@ -63,7 +63,7 @@ module Attribute = struct
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 
-  let const_rank = Variants.to_rank (CItv (CItv.equal_to IntLit.zero, dummy_trace))
+  let citv_rank = Variants.to_rank (CItv (CItv.equal_to IntLit.zero))
 
   let bo_itv_rank = Variants.to_rank (BoItv Itv.ItvPure.zero)
 
@@ -87,8 +87,8 @@ module Attribute = struct
         F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv
     | Closure pname ->
         Procname.pp f pname
-    | CItv (phi, trace) ->
+    | CItv phi ->
-        F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> CItv.pp fmt phi)) trace
+        F.fprintf f "Arith %a" CItv.pp phi
     | Invalid (invalidation, trace) ->
         F.fprintf f "Invalid %a"
           (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
@@ -156,10 +156,10 @@ module Attributes = struct
 
 
   let get_citv attrs =
-    Set.find_rank attrs Attribute.const_rank
+    Set.find_rank attrs Attribute.citv_rank
     |> Option.map ~f:(fun attr ->
-           let[@warning "-8"] (Attribute.CItv (a, trace)) = attr in
+           let[@warning "-8"] (Attribute.CItv a) = attr in
-           (a, trace) )
+           a )
 
 
   let get_bo_itv attrs =
@@ -190,14 +190,16 @@ let is_suitable_for_pre = function
 let map_trace ~f = function
   | Allocated (procname, trace) ->
       Allocated (procname, f trace)
-  | CItv (arith, trace) ->
-      CItv (arith, f trace)
   | Invalid (invalidation, trace) ->
       Invalid (invalidation, f trace)
   | MustBeValid trace ->
       MustBeValid (f trace)
   | WrittenTo trace ->
       WrittenTo (f trace)
-  | (AddressOfCppTemporary _ | AddressOfStackVariable _ | BoItv _ | Closure _ | StdVectorReserve) as
+  | ( AddressOfCppTemporary _
-    attr ->
+    | AddressOfStackVariable _
+    | BoItv _
+    | CItv _
+    | Closure _
+    | StdVectorReserve ) as attr ->
       attr

infer/src/pulse/PulseAttribute.mli

@@ -16,7 +16,7 @@ type t =
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
   | Allocated of Procname.t * Trace.t
       (** the {!Procname.t} is the function causing the allocation, eg [malloc] *)
-  | CItv of CItv.t * Trace.t
+  | CItv of CItv.t
   | BoItv of Itv.ItvPure.t
   | Closure of Procname.t
   | Invalid of Invalidation.t * Trace.t
@@ -41,7 +41,7 @@ module Attributes : sig
 
   val get_allocation : t -> (Procname.t * Trace.t) option
 
-  val get_citv : t -> (CItv.t * Trace.t) option
+  val get_citv : t -> CItv.t option
 
   val get_bo_itv : t -> Itv.ItvPure.t option
 

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -32,7 +32,7 @@ val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.
 
 val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
-val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option
+val get_citv : AbstractValue.t -> t -> CItv.t option
 
 val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
 

infer/src/pulse/PulseInterproc.ml

@@ -238,8 +238,8 @@ let eval_sym_of_subst astate subst s bound_end =
 
 let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee =
   match (attr : Attribute.t) with
-  | CItv (arith_callee, hist) -> (
+  | CItv arith_callee -> (
-      let arith_caller_opt = AddressAttributes.get_citv addr_caller astate |> Option.map ~f:fst in
+      let arith_caller_opt = AddressAttributes.get_citv addr_caller astate in
       match CItv.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) with
       | Unsatisfiable ->
           raise
@@ -251,7 +251,7 @@ let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee =
                   ; arith_callee= Some arith_callee
                   ; call_state }))
       | Satisfiable (Some abduce_caller, _abduce_callee) ->
-          Attribute.CItv (abduce_caller, hist)
+          Attribute.CItv abduce_caller
       | Satisfiable (None, _) ->
           attr )
   | BoItv itv -> (

infer/src/pulse/PulseModels.ml

@@ -40,19 +40,17 @@ module Misc = struct
 
 
   let return_int : Int64.t -> model =
-   fun i64 ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+   fun i64 ~caller_summary:_ ~callee_procname:_ _location ~ret:(ret_id, _) astate ->
     let i = IntLit.of_int64 i64 in
     let ret_addr = AbstractValue.Constants.get_int i in
-    let astate = PulseArithmetic.and_eq_int (Immediate {location; history= []}) ret_addr i astate in
+    let astate = PulseArithmetic.and_eq_int ret_addr i astate in
     PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue
 
 
   let return_unknown_size : model =
-   fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+   fun ~caller_summary:_ ~callee_procname:_ _location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
-    let astate =
+    let astate = PulseArithmetic.and_nonnegative ret_addr astate in
-      PulseArithmetic.and_nonnegative (Immediate {location; history= []}) ret_addr astate
-    in
     PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue
 
 
@@ -86,19 +84,17 @@ module C = struct
 
   let malloc _ : model =
    fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate ->
-    let hist =
-      [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]
-    in
-    let immediate_hist = Trace.Immediate {location; history= hist} in
     let ret_addr = AbstractValue.mk_fresh () in
-    let ret_value = (ret_addr, hist) in
+    let ret_value =
+      (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}])
+    in
     let astate = PulseOperations.write_id ret_id ret_value astate in
     let astate_alloc =
-      PulseArithmetic.and_positive immediate_hist ret_addr astate
+      PulseArithmetic.and_positive ret_addr astate
       |> PulseOperations.allocate callee_procname location ret_value
     in
     let+ astate_null =
-      PulseArithmetic.and_eq_int immediate_hist ret_addr IntLit.zero astate
+      PulseArithmetic.and_eq_int ret_addr IntLit.zero astate
       |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value
     in
     [ExecutionDomain.ContinueProgram astate_alloc; ExecutionDomain.ContinueProgram astate_null]
@@ -107,14 +103,12 @@ module C = struct
   let malloc_not_null _ : model =
    fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
-    let hist =
+    let ret_value =
-      [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]
+      (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}])
     in
-    let ret_value = (ret_addr, hist) in
-    let immediate_hist = Trace.Immediate {location; history= hist} in
     let astate = PulseOperations.write_id ret_id ret_value astate in
     PulseOperations.allocate callee_procname location ret_value astate
-    |> PulseArithmetic.and_positive immediate_hist ret_addr
+    |> PulseArithmetic.and_positive ret_addr
     |> PulseOperations.ok_continue
 
 
@@ -173,15 +167,15 @@ module StdAtomicInteger = struct
 
 
   let arith_bop prepost location event ret_id bop this operand astate =
-    let* astate, int_addr, (old_int, old_int_hist) = load_backing_int location this astate in
+    let* astate, int_addr, (old_int, hist) = load_backing_int location this astate in
-    let astate, (new_int, hist) =
+    let bop_addr = AbstractValue.mk_fresh () in
-      PulseArithmetic.eval_binop location bop (AbstractValueOperand old_int) operand old_int_hist
+    let astate =
-        astate
+      PulseArithmetic.eval_binop bop_addr bop (AbstractValueOperand old_int) operand astate
     in
     let+ astate =
-      PulseOperations.write_deref location ~ref:int_addr ~obj:(new_int, event :: hist) astate
+      PulseOperations.write_deref location ~ref:int_addr ~obj:(bop_addr, event :: hist) astate
     in
-    let ret_int = match prepost with `Pre -> new_int | `Post -> old_int in
+    let ret_int = match prepost with `Pre -> bop_addr | `Post -> old_int in
     PulseOperations.write_id ret_id (ret_int, event :: hist) astate
 
 
@@ -478,9 +472,7 @@ module StdVector = struct
    fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::vector::begin()"; location; in_call= []} in
     let index_zero = AbstractValue.mk_fresh () in
-    let astate =
+    let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in
-      PulseArithmetic.and_eq_int (Immediate {location; history= []}) index_zero IntLit.zero astate
-    in
     let* astate, ((arr_addr, _) as arr) =
       GenericArrayBackedCollection.eval location vector astate
     in

infer/src/pulse/PulseOperations.ml

@@ -135,7 +135,7 @@ let eval location exp0 astate =
     | Const (Cint i) ->
         let v = AbstractValue.Constants.get_int i in
         let astate =
-          PulseArithmetic.and_eq_int (Immediate {location; history= []}) v i astate
+          PulseArithmetic.and_eq_int v i astate
           |> AddressAttributes.invalidate
                (v, [ValueHistory.Assignment location])
                (ConstantDereference i) location
@@ -143,17 +143,16 @@ let eval location exp0 astate =
         Ok (astate, (v, []))
     | UnOp (unop, exp, _typ) ->
         let+ astate, (addr, hist) = eval exp astate in
-        PulseArithmetic.eval_unop location unop addr hist astate
+        let unop_addr = AbstractValue.mk_fresh () in
+        (PulseArithmetic.eval_unop unop_addr unop addr astate, (unop_addr, hist))
     | BinOp (bop, e_lhs, e_rhs) ->
         let* astate, (addr_lhs, hist_lhs) = eval e_lhs astate in
-        let+ ( astate
+        (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
-             , ( addr_rhs
+        let+ astate, (addr_rhs, _hist_rhs) = eval e_rhs astate in
-               , (* NOTE: arbitrarily track only the history of the lhs, maybe not the brightest idea *)
+        let binop_addr = AbstractValue.mk_fresh () in
-               _ ) ) =
+        ( PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
-          eval e_rhs astate
+            (AbstractValueOperand addr_rhs) astate
-        in
+        , (binop_addr, hist_lhs) )
-        PulseArithmetic.eval_binop location bop (AbstractValueOperand addr_lhs)
-          (AbstractValueOperand addr_rhs) hist_lhs astate
     | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in
@@ -169,14 +168,13 @@ let eval_to_operand location exp astate =
       (astate, PulseArithmetic.AbstractValueOperand value)
 
 
-let prune ~is_then_branch if_kind location ~condition astate =
+let prune 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 location exp_lhs astate in
         let+ astate, rhs_op = eval_to_operand location exp_rhs astate in
-        PulseArithmetic.prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op
+        PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate
-          astate
     | UnOp (LNot, exp', _) ->
         prune_aux ~negated:(not negated) exp' astate
     | exp ->

infer/src/pulse/PulseOperations.mli

@@ -27,13 +27,7 @@ val eval : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t))
     Return an error state if it traverses some known invalid address or if the end destination is
     known to be invalid. *)
 
-val prune :
+val prune : Location.t -> condition:Exp.t -> t -> (t * bool) access_result
-     is_then_branch:bool
-  -> Sil.if_kind
-  -> Location.t
-  -> condition:Exp.t
-  -> t
-  -> (t * bool) access_result
 
 val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** Like [eval] but evaluates [*exp]. *)

infer/src/pulse/PulseTrace.ml

@@ -36,13 +36,6 @@ let rec pp ~pp_immediate fmt trace =
         F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp ~pp_immediate) in_call
 
 
-let add_event event = function
-  | Immediate {location; history} ->
-      Immediate {location; history= event :: history}
-  | ViaCall {f; in_call; location; history} ->
-      ViaCall {f; in_call; location; history= event :: history}
-
-
 let rec add_to_errlog ?(include_value_history = true) ~nesting ~pp_immediate trace errlog =
   match trace with
   | Immediate {location; history} ->

infer/src/pulse/PulseTrace.mli

@@ -27,8 +27,6 @@ val get_outer_location : t -> Location.t
 val get_start_location : t -> Location.t
 (** initial step in the history if not empty, or else same as {!get_outer_location} *)
 
-val add_event : ValueHistory.event -> t -> t
-
 val add_to_errlog :
      ?include_value_history:bool
   -> nesting:int