[pulse] substitute inferbo attributes in callee summaries

Summary:
The introduction of inferbo intervals as pulse attributes creates the
first relational attributes. To make sense of inferbo intervals
appearing in summaries when in a caller context, we need to substitute
the abstract values they contain in the callee with the abstract values
they correspond to in the caller.

This has a significant consequence: we have to delay the check that
arithmetic constraints in the callee are satisfiable at the call-site
until *after* we have discovered all the relationships between callee
values and caller values from the heap. To solve this, we now run an
arithmetic constraints check *after* having materialised all the
addresses.

We also need to translate the abstract values in the attributes in the
post before recording them in the caller, for the same reasons.

Quite some code in this diff is concerned with substituting pulse values
inside inferbo intervals. There is a complication there too: even after
having discovered relationships between caller and callee abstract
values induced by the heap shapes, there could be abstract values in the
callee's attributes that we haven't seen yet. We need to make up new
values for these in the caller, so this substitution has to return a
potentially extended substitution.

Reviewed By: skcho

Differential Revision: D18745695

fbshipit-source-id: 077ae7670

infer/src/bufferoverrun/bounds.ml

@@ -209,6 +209,14 @@ 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
@@ -1137,6 +1145,15 @@ 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,6 +125,11 @@ 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

@@ -394,6 +394,16 @@ 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 _ ->
@@ -734,6 +744,19 @@ 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,6 +243,11 @@ 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

@@ -359,6 +359,13 @@ module Symbol = struct
         SymbolPath.is_global path
 
 
+  let is_pulse_value : t -> bool = function
+    | PulseValue _ ->
+        true
+    | OneValue _ | BoundEnd _ ->
+        false
+
+
   (* This should be called on non-pulse bound as of now. *)
   let path = function PulseValue _ -> assert false | OneValue {path} | BoundEnd {path} -> path
 
@@ -380,6 +387,23 @@ 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

@@ -121,6 +121,13 @@ module Symbol : sig
   val of_pulse_value : PulseAbstractValue.t -> t
 
   val exists_str : f:(string -> bool) -> t -> bool
+
+  val is_pulse_value : t -> bool
+
+  val subst_pulse_value :
+       (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
+    -> t
+    -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t
 end
 
 module SymbolSet : sig

infer/src/istd/PrettyPrintable.ml

@@ -221,6 +221,8 @@ module type PPUniqRankSet = sig
 
   val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum
 
+  val fold_map : t -> init:'accum -> f:('accum -> elt -> 'accum * elt) -> 'accum * t
+
   val is_empty : t -> bool
 
   val is_singleton : t -> bool
@@ -273,6 +275,17 @@ module MakePPUniqRankSet (Val : PrintableRankedType) : PPUniqRankSet with type e
       m
 
 
+  let fold_map m ~init ~f =
+    let accum = ref init in
+    let m' =
+      map m ~f:(fun value ->
+          let acc', v' = f !accum value in
+          accum := acc' ;
+          v' )
+    in
+    (!accum, m')
+
+
   let pp ?(print_rank = false) fmt map =
     if print_rank then Map.pp fmt map
     else pp_collection ~pp_item:Val.pp fmt (Map.bindings map |> List.map ~f:snd)

infer/src/istd/PrettyPrintable.mli

@@ -172,6 +172,8 @@ module type PPUniqRankSet = sig
 
   val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum
 
+  val fold_map : t -> init:'accum -> f:('accum -> elt -> 'accum * elt) -> 'accum * t
+
   val is_empty : t -> bool
 
   val is_singleton : t -> bool

infer/src/pulse/PulseAbductiveDomain.ml

@@ -446,43 +446,6 @@ module PrePost = struct
     Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call}
 
 
-  let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
-      ~addr_hist_caller call_state =
-    match Attributes.get_arithmetic attrs_pre with
-    | None ->
-        call_state
-    | Some (arith_callee, arith_callee_hist) -> (
-        let addr_caller, hist_caller = addr_hist_caller in
-        let astate = call_state.astate in
-        let arith_caller_opt = Memory.get_arithmetic addr_caller astate |> Option.map ~f:fst in
-        (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes
-           for that address in the post since abstract values are immutable *)
-        match
-          Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee)
-        with
-        | Unsatisfiable ->
-            raise
-              (CannotApplyPre
-                 (Arithmetic
-                    { addr_caller
-                    ; addr_callee= addr_pre
-                    ; arith_caller= arith_caller_opt
-                    ; arith_callee= Some arith_callee }))
-        | Satisfiable (abduce_caller, _abduce_callee) ->
-            let new_astate =
-              Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller ->
-                  let attribute =
-                    Attribute.Arithmetic
-                      ( abduce_caller
-                      , add_call_to_trace callee_proc_name call_location hist_caller
-                          arith_callee_hist )
-                  in
-                  Memory.abduce_attribute addr_caller attribute astate
-                  |> Memory.add_attribute addr_caller attribute )
-            in
-            {call_state with astate= new_astate} )
-
-
   (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in
      [call_state.astate] starting from address [addr_caller]. Report an error if some invalid
      addresses are traversed in the process. *)
@@ -495,11 +458,7 @@ module PrePost = struct
       match BaseMemory.find_opt addr_pre pre.BaseDomain.heap with
       | None ->
           Ok call_state
-      | Some (edges_pre, attrs_pre) ->
+      | Some (edges_pre, _attrs_pre) ->
-          let call_state =
-            solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
-              ~addr_hist_caller call_state
-          in
           Container.fold_result
             ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold)
             ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) ->
@@ -574,15 +533,92 @@ module PrePost = struct
           ~addr_pre ~addr_hist_caller call_state )
 
 
+  let translate_attributes attrs_callee subst =
+    let translate_attribute subst attr =
+      match (attr : Attribute.t) with
+      | BoItv itv ->
+          let subst, itv' = Itv.subst_pulse_values subst itv in
+          (subst, Attribute.BoItv itv')
+      | AddressOfCppTemporary _
+      | AddressOfStackVariable _
+      | Arithmetic _
+      | Closure _
+      | Invalid _
+      | MustBeValid _
+      | StdVectorReserve
+      | WrittenTo _ ->
+          (* non-relational attributes *)
+          (subst, attr)
+    in
+    Attributes.fold_map attrs_callee ~init:subst ~f:translate_attribute
+
+
+  let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
+      ~addr_hist_caller call_state =
+    match Attributes.get_arithmetic attrs_pre with
+    | None ->
+        call_state
+    | Some (arith_callee, arith_callee_hist) -> (
+        let addr_caller, hist_caller = addr_hist_caller in
+        let astate = call_state.astate in
+        let arith_caller_opt = Memory.get_arithmetic addr_caller astate |> Option.map ~f:fst in
+        (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes
+           for that address in the post since abstract values are immutable *)
+        match
+          Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee)
+        with
+        | Unsatisfiable ->
+            raise
+              (CannotApplyPre
+                 (Arithmetic
+                    { addr_caller
+                    ; addr_callee= addr_pre
+                    ; arith_caller= arith_caller_opt
+                    ; arith_callee= Some arith_callee }))
+        | Satisfiable (abduce_caller, _abduce_callee) ->
+            let new_astate =
+              Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller ->
+                  let attribute =
+                    Attribute.Arithmetic
+                      ( abduce_caller
+                      , add_call_to_trace callee_proc_name call_location hist_caller
+                          arith_callee_hist )
+                  in
+                  Memory.abduce_attribute addr_caller attribute astate
+                  |> Memory.add_attribute addr_caller attribute )
+            in
+            {call_state with astate= new_astate} )
+
+
+  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
+      solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
+        ~addr_hist_caller {call_state with subst}
+    in
+    (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *)
+    AddressMap.fold
+      (fun addr_callee addr_hist_caller call_state ->
+        match BaseMemory.find_opt addr_callee (pre_post.pre :> BaseDomain.t).heap with
+        | None ->
+            call_state
+        | Some (_edges, callee_attrs) ->
+            one_address_sat addr_callee callee_attrs addr_hist_caller call_state )
+      call_state.subst call_state
+
+
   let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state =
+    let ( >>= ) x f = Option.map x ~f:(Result.bind ~f) in
+    let ( >>| ) x f = Option.map x ~f:(Result.map ~f) in
     PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ;
     let r =
+      (* first make as large a mapping as we can between callee values and caller values... *)
       materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
         call_state
-      |> Option.map
+      >>= materialize_pre_for_globals callee_proc_name call_location pre_post
-           ~f:
+      >>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in
-             (Result.bind ~f:(fun call_state ->
+             terms of the caller's values *)
-                  materialize_pre_for_globals callee_proc_name call_location pre_post call_state ))
+      apply_arithmetic_constraints callee_proc_name call_location pre_post
     in
     PerfEvent.(log (fun logger -> log_end_event logger ())) ;
     r
@@ -627,21 +663,26 @@ module PrePost = struct
             old_post_edges edges_pre )
 
 
-  let add_call_to_attr proc_name call_location caller_history attr =
+  let add_call_to_attributes proc_name call_location caller_history attrs call_state =
-    match (attr : Attribute.t) with
+    let add_call_to_attribute attr =
-    | Invalid (invalidation, trace) ->
+      match (attr : Attribute.t) with
-        Attribute.Invalid
+      | Invalid (invalidation, trace) ->
-          (invalidation, add_call_to_trace proc_name call_location caller_history trace)
+          Attribute.Invalid
-    | Arithmetic (arith, trace) ->
+            (invalidation, add_call_to_trace proc_name call_location caller_history trace)
-        Attribute.Arithmetic (arith, add_call_to_trace proc_name call_location caller_history trace)
+      | Arithmetic (arith, trace) ->
-    | AddressOfCppTemporary (_, _)
+          Attribute.Arithmetic
-    | AddressOfStackVariable (_, _, _)
+            (arith, add_call_to_trace proc_name call_location caller_history trace)
-    | BoItv _
+      | AddressOfCppTemporary (_, _)
-    | Closure _
+      | AddressOfStackVariable (_, _, _)
-    | MustBeValid _
+      | BoItv _
-    | StdVectorReserve
+      | Closure _
-    | WrittenTo _ ->
+      | MustBeValid _
-        attr
+      | StdVectorReserve
+      | WrittenTo _ ->
+          attr
+    in
+    let call_state, attrs = translate_attributes attrs call_state in
+    (call_state, Attributes.map attrs ~f:(fun attr -> add_call_to_attribute attr))
 
 
   let record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt
@@ -650,16 +691,14 @@ module PrePost = struct
       delete_edges_in_callee_pre_from_caller ~addr_callee ~cell_pre_opt ~addr_caller call_state
     in
     let heap = (call_state.astate.post :> base_domain).heap in
-    let heap =
+    let subst, heap =
-      let attrs_post_caller =
+      let subst, attrs_post_caller =
-        Attributes.map attrs_post ~f:(fun attr ->
+        add_call_to_attributes callee_proc_name call_loc hist_caller attrs_post call_state.subst
-            add_call_to_attr callee_proc_name call_loc hist_caller attr )
       in
-      BaseMemory.set_attrs addr_caller attrs_post_caller heap
+      (subst, BaseMemory.set_attrs addr_caller attrs_post_caller heap)
     in
     let subst, translated_post_edges =
-      BaseMemory.Edges.fold_map ~init:call_state.subst edges_post
+      BaseMemory.Edges.fold_map ~init:subst edges_post ~f:(fun subst (addr_callee, trace_post) ->
-        ~f:(fun subst (addr_callee, trace_post) ->
           let subst, (addr_curr, hist_curr) =
             subst_find_or_new subst addr_callee ~default_hist_caller:hist_caller
           in
@@ -812,28 +851,25 @@ module PrePost = struct
 
   let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state =
     let heap0 = (call_state.astate.post :> base_domain).heap in
-    let heap =
+    let subst, heap =
       BaseMemory.fold_attrs
-        (fun addr_callee attrs heap ->
+        (fun addr_callee attrs (subst, heap) ->
           if AddressSet.mem addr_callee call_state.visited then
-            (* already recorded the attributes when we were walking the edges map *) heap
+            (* already recorded the attributes when we were walking the edges map *)
+            (subst, heap)
           else
             match AddressMap.find_opt addr_callee call_state.subst with
             | None ->
-                (* callee address has no meaning for the caller *) heap
+                (* callee address has no meaning for the caller *) (subst, heap)
             | Some (addr_caller, history) ->
-                let attrs' =
+                let subst, attrs' =
-                  Attributes.map
+                  add_call_to_attributes callee_proc_name call_loc history attrs subst
-                    ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc history attr)
-                    attrs
                 in
-                BaseMemory.set_attrs addr_caller attrs' heap )
+                (subst, BaseMemory.set_attrs addr_caller attrs' heap) )
-        (pre_post.post :> BaseDomain.t).heap heap0
+        (pre_post.post :> BaseDomain.t).heap (call_state.subst, heap0)
     in
-    if phys_equal heap heap0 then call_state
+    let post = Domain.make (call_state.astate.post :> BaseDomain.t).stack heap in
-    else
+    {call_state with subst; astate= {call_state.astate with post}}
-      let post = Domain.make (call_state.astate.post :> BaseDomain.t).stack heap in
-      {call_state with astate= {call_state.astate with post}}
 
 
   let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state =