[pulse] Share subst function of itv

Summary: This diff uses `Itv.subst` for substituting pulse's `BoItv` attributes.

Reviewed By: jvillard

Differential Revision: D18748308

fbshipit-source-id: bed7d4de8

infer/src/bufferoverrun/bounds.ml

@@ -209,14 +209,6 @@ module SymLinear = struct
 
 
   let exists_str ~f x = M.exists (fun k _ -> Symb.Symbol.exists_str ~f k) x
-
-  let subst_pulse_value subst map =
-    M.fold
-      (fun symbol coeff (new_map, new_subst) ->
-        let new_subst, symbol' = Symb.Symbol.subst_pulse_value new_subst symbol in
-        let new_map = M.add symbol' coeff new_map in
-        (new_map, new_subst) )
-      map (M.empty, subst)
 end
 
 module Bound = struct
@@ -1145,15 +1137,6 @@ module Bound = struct
 
   let subst_ub x eval_sym = subst ~subst_pos:Symb.BoundEnd.UpperBound x eval_sym
 
-  let subst_pulse_value subst b =
-    match b with
-    | MInf | PInf | MinMax _ | MinMaxB _ ->
-        (subst, b)
-    | Linear (c, se) ->
-        let se', subst = SymLinear.subst_pulse_value subst se in
-        (subst, Linear (c, se'))
-
-
   (* When a positive bound is expected, min(1,x) can be simplified to 1. *)
   let simplify_min_one b =
     match b with

infer/src/bufferoverrun/bounds.mli

@@ -125,11 +125,6 @@ module Bound : sig
   val get_same_one_symbol : t -> t -> Symb.SymbolPath.t option
 
   val exists_str : f:(string -> bool) -> t -> bool
-
-  val subst_pulse_value :
-       (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
-    -> t
-    -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t
 end
 
 module BoundTrace : sig

infer/src/bufferoverrun/itv.ml

@@ -40,6 +40,10 @@ module ItvPure = struct
 
   let ub : t -> Bound.t = snd
 
+  let get_bound (lb, ub) bound_end =
+    match bound_end with Symb.BoundEnd.LowerBound -> lb | Symb.BoundEnd.UpperBound -> ub
+
+
   let is_lb_infty : t -> bool = fun (l, _) -> Bound.is_minf l
 
   let is_finite : t -> bool =
@@ -394,16 +398,6 @@ module ItvPure = struct
         Bottom
 
 
-  let subst_pulse_values :
-         (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
-      -> t
-      -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t =
-   fun subst (l, u) ->
-    let subst, l' = Bound.subst_pulse_value subst l in
-    let subst, u' = Bound.subst_pulse_value subst u in
-    (subst, (l', u'))
-
-
   let arith_binop bop x y =
     match bop with
     | Binop.PlusA _ ->
@@ -549,14 +543,8 @@ let bot : t = Bottom
 
 let top : t = NonBottom ItvPure.top
 
-let get_bound itv (be : Symb.BoundEnd.t) =
+let get_bound itv bound_end =
-  match (itv, be) with
+  match itv with Bottom -> Bottom | NonBottom x -> NonBottom (ItvPure.get_bound x bound_end)
-  | Bottom, _ ->
-      Bottom
-  | NonBottom x, LowerBound ->
-      NonBottom (ItvPure.lb x)
-  | NonBottom x, UpperBound ->
-      NonBottom (ItvPure.ub x)
 
 
 let false_sem = NonBottom ItvPure.false_sem
@@ -744,19 +732,6 @@ let subst : t -> Bound.eval_sym -> t =
  fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x
 
 
-let subst_pulse_values :
-       (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
-    -> t
-    -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t =
- fun subst x ->
-  match x with
-  | NonBottom x' ->
-      let subst', x'' = ItvPure.subst_pulse_values subst x' in
-      (subst', NonBottom x'')
-  | Bottom ->
-      (subst, x)
-
-
 let is_symbolic = bind1bool ItvPure.is_symbolic
 
 let get_symbols : t -> SymbolSet.t = function

infer/src/bufferoverrun/itv.mli

@@ -243,11 +243,6 @@ val prune_le : t -> t -> t
 
 val subst : t -> Bound.eval_sym -> t
 
-val subst_pulse_values :
-     (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
-  -> t
-  -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t
-
 val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t
 
 val of_normal_path : unsigned:bool -> ?non_int:bool -> Symb.SymbolPath.partial -> t

infer/src/bufferoverrun/symb.ml

@@ -366,6 +366,13 @@ module Symbol = struct
         false
 
 
+  let get_pulse_value_exn : t -> PulseAbstractValue.t = function
+    | PulseValue v ->
+        v
+    | OneValue _ | BoundEnd _ ->
+        assert false
+
+
   (* This should be called on non-pulse bound as of now. *)
   let path = function PulseValue _ -> assert false | OneValue {path} | BoundEnd {path} -> path
 
@@ -387,23 +394,6 @@ module Symbol = struct
         false
     | OneValue {path} | BoundEnd {path} ->
         SymbolPath.exists_str ~f path
-
-
-  let subst_pulse_value subst s =
-    match s with
-    | OneValue _ | BoundEnd _ ->
-        (subst, s)
-    | PulseValue v ->
-        let subst', v' =
-          match PulseAbstractValue.Map.find_opt v subst with
-          | Some (v', _) ->
-              (subst, v')
-          | None ->
-              let v' = PulseAbstractValue.mk_fresh () in
-              let subst' = PulseAbstractValue.Map.add v (v', []) subst in
-              (subst', v')
-        in
-        (subst', PulseValue v')
 end
 
 module SymbolSet = struct

infer/src/bufferoverrun/symb.mli

@@ -124,10 +124,7 @@ module Symbol : sig
 
   val is_pulse_value : t -> bool
 
-  val subst_pulse_value :
+  val get_pulse_value_exn : t -> PulseAbstractValue.t
-       (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
-    -> t
-    -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t
 end
 
 module SymbolSet : sig

infer/src/pulse/PulseAbductiveDomain.ml

@@ -533,12 +533,23 @@ module PrePost = struct
           ~addr_pre ~addr_hist_caller call_state )
 
 
-  let translate_attributes attrs_callee subst =
+  let subst_attributes attrs_callee {astate; subst} =
-    let translate_attribute subst attr =
+    let eval_sym_of_subst subst s bound_end =
+      let v = Symb.Symbol.get_pulse_value_exn s in
+      match PulseAbstractValue.Map.find_opt v !subst with
+      | Some (v', _) ->
+          Itv.get_bound (Memory.get_bo_itv v' astate) bound_end
+      | None ->
+          let v' = PulseAbstractValue.mk_fresh () in
+          subst := PulseAbstractValue.Map.add v (v', []) !subst ;
+          AbstractDomain.Types.NonBottom (Bounds.Bound.of_pulse_value v')
+    in
+    let subst_attribute subst attr =
       match (attr : Attribute.t) with
       | BoItv itv ->
-          let subst, itv' = Itv.subst_pulse_values subst itv in
+          let subst = ref subst in
-          (subst, Attribute.BoItv itv')
+          let itv' = Itv.subst itv (eval_sym_of_subst subst) in
+          (!subst, Attribute.BoItv itv')
       | AddressOfCppTemporary _
       | AddressOfStackVariable _
       | Arithmetic _
@@ -550,7 +561,7 @@ module PrePost = struct
           (* non-relational attributes *)
           (subst, attr)
     in
-    Attributes.fold_map attrs_callee ~init:subst ~f:translate_attribute
+    Attributes.fold_map attrs_callee ~init:subst ~f:subst_attribute
 
 
   let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
@@ -592,7 +603,7 @@ module PrePost = struct
 
   let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state =
     let one_address_sat addr_pre callee_attrs addr_hist_caller call_state =
-      let subst, attrs_pre = translate_attributes callee_attrs call_state.subst in
+      let subst, attrs_pre = subst_attributes callee_attrs call_state in
       solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
         ~addr_hist_caller {call_state with subst}
     in
@@ -681,7 +692,7 @@ module PrePost = struct
       | WrittenTo _ ->
           attr
     in
-    let call_state, attrs = translate_attributes attrs call_state in
+    let call_state, attrs = subst_attributes attrs call_state in
     (call_state, Attributes.map attrs ~f:(fun attr -> add_call_to_attribute attr))
 
 
@@ -693,7 +704,7 @@ module PrePost = struct
     let heap = (call_state.astate.post :> base_domain).heap in
     let subst, heap =
       let subst, attrs_post_caller =
-        add_call_to_attributes callee_proc_name call_loc hist_caller attrs_post call_state.subst
+        add_call_to_attributes callee_proc_name call_loc hist_caller attrs_post call_state
       in
       (subst, BaseMemory.set_attrs addr_caller attrs_post_caller heap)
     in
@@ -863,7 +874,8 @@ module PrePost = struct
                 (* callee address has no meaning for the caller *) (subst, heap)
             | Some (addr_caller, history) ->
                 let subst, attrs' =
-                  add_call_to_attributes callee_proc_name call_loc history attrs subst
+                  add_call_to_attributes callee_proc_name call_loc history attrs
+                    {call_state with subst}
                 in
                 (subst, BaseMemory.set_attrs addr_caller attrs' heap) )
         (pre_post.post :> BaseDomain.t).heap (call_state.subst, heap0)