[inferbo] Simplify memory instantiation of function call

Summary:
It simplifies abstract memory instantiations of function calls.  Now it instantiates callee memories by directly evaluating symbol paths, rather than constructing `subst_map`.

main changes are:

- no construction of `subst_map` and `trace_map`
- no symbol table in Inferbo's summary
- no `Symbol_not_found` exception (for when a required symbol was unavailable in `subst_map`)

Reviewed By: mbouaziz

Differential Revision: D9495597

fbshipit-source-id: 18cdcd6f7

infer/src/bufferoverrun/arrayBlk.ml

@@ -57,9 +57,9 @@ module ArrInfo = struct
 
   let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset
 
-  let subst : t -> Bound.t bottom_lifted Itv.SymbolMap.t -> t =
+  let subst : t -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) -> t =
-   fun arr subst_map ->
+   fun arr eval_sym ->
-    {arr with offset= Itv.subst arr.offset subst_map; size= Itv.subst arr.size subst_map}
+    {arr with offset= Itv.subst arr.offset eval_sym; size= Itv.subst arr.size eval_sym}
 
 
   let pp : Format.formatter -> t -> unit =
@@ -138,8 +138,8 @@ let get_pow_loc : astate -> PowLoc.t =
   fold pow_loc_of_allocsite array PowLoc.bot
 
 
-let subst : astate -> Bound.t bottom_lifted Itv.SymbolMap.t -> astate =
+let subst : astate -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> astate =
- fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a
+ fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
 
 
 let get_symbols : astate -> Itv.Symbol.t list =

infer/src/bufferoverrun/bounds.ml

@@ -10,8 +10,6 @@ open! AbstractDomain.Types
 module F = Format
 module L = Logging
 
-exception Symbol_not_found of Symb.Symbol.t
-
 exception Not_One_Symbol
 
 open Ints
@@ -708,35 +706,32 @@ module Bound = struct
         NonBottom (f x y)
 
 
-  (** Substitutes ALL symbols in [x] with respect to [map]. Throws [Symbol_not_found] if a symbol in [x] can't be found in [map]. Under/over-Approximate as good as possible according to [subst_pos]. *)
+  (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *)
-  let subst_exn :
+  let subst :
-      subst_pos:Symb.BoundEnd.t -> t -> t bottom_lifted Symb.SymbolMap.t -> t bottom_lifted =
+      subst_pos:Symb.BoundEnd.t -> t -> (Symb.Symbol.t -> t bottom_lifted) -> t bottom_lifted =
-   fun ~subst_pos x map ->
+   fun ~subst_pos x eval_sym ->
-    let get_exn s =
+    let get s =
-      match Symb.SymbolMap.find s map with
+      match eval_sym s with
       | NonBottom x when Symb.Symbol.is_unsigned s ->
           NonBottom (ub ~default:x zero x)
       | x ->
           x
     in
     let get_mult_const s coeff =
-      try
+      if NonZeroInt.is_one coeff then get s
-        if NonZeroInt.is_one coeff then get_exn s
+      else if NonZeroInt.is_minus_one coeff then get s |> lift1 neg
-        else if NonZeroInt.is_minus_one coeff then get_exn s |> lift1 neg
+      else
-        else
+        match eval_sym s with
-          match Symb.SymbolMap.find s map with
+        | Bottom -> (
-          | Bottom ->
+          (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *)
-              Bottom
+          match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with
-          | NonBottom x ->
+          | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false ->
-              let x = mult_const subst_pos coeff x in
+              NonBottom zero
-              if Symb.Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x
+          | _ ->
-      with Caml.Not_found -> (
+              Bottom )
-        (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *)
+        | NonBottom x ->
-        match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with
+            let x = mult_const subst_pos coeff x in
-        | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false ->
+            if Symb.Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x
-            NonBottom zero
-        | _ ->
-            raise (Symbol_not_found s) )
     in
     match x with
     | MInf | PInf ->
@@ -746,15 +741,10 @@ module Bound = struct
           ~init:(NonBottom (of_int c))
           ~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff))
     | MinMax (c, sign, min_max, d, s) -> (
-      match get_exn s with
+      match get s with
       | Bottom ->
-          Bottom
+          Option.value_map (int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
-      | exception Caml.Not_found -> (
+              NonBottom (of_int i) )
-        match int_of_minmax subst_pos x with
-        | Some i ->
-            NonBottom (of_int i)
-        | None ->
-            raise (Symbol_not_found s) )
       | NonBottom x' ->
           let res =
             match (sign, min_max, x') with
@@ -805,9 +795,9 @@ module Bound = struct
           NonBottom res )
 
 
-  let subst_lb_exn x map = subst_exn ~subst_pos:Symb.BoundEnd.LowerBound x map
+  let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym
 
-  let subst_ub_exn x map = subst_exn ~subst_pos:Symb.BoundEnd.UpperBound x map
+  let subst_ub x eval_sym = subst ~subst_pos:Symb.BoundEnd.UpperBound x eval_sym
 
   let simplify_bound_ends_from_paths x =
     match x with

infer/src/bufferoverrun/bounds.mli

@@ -8,8 +8,6 @@
 open! IStd
 module F = Format
 
-exception Symbol_not_found of Symb.Symbol.t
-
 exception Not_One_Symbol
 
 module SymLinear : sig
@@ -119,14 +117,14 @@ module Bound : sig
 
   val is_not_infty : t -> bool
 
-  val subst_lb_exn :
+  val subst_lb :
        t
-    -> t AbstractDomain.Types.bottom_lifted Symb.SymbolMap.t
+    -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted)
     -> t AbstractDomain.Types.bottom_lifted
 
-  val subst_ub_exn :
+  val subst_ub :
        t
-    -> t AbstractDomain.Types.bottom_lifted Symb.SymbolMap.t
+    -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted)
     -> t AbstractDomain.Types.bottom_lifted
 
   val simplify_bound_ends_from_paths : t -> t

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -34,12 +34,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type extras = Itv.SymbolTable.t
 
-  let instantiate_ret ret callee_pname ~callee_exit_mem subst_map mem ret_alias location =
+  let instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace mem ret_alias location =
     let copy_reachable_new_locs_from locs mem =
       let copy loc acc =
         Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v ->
             let v =
-              Dom.Val.subst v subst_map location |> Dom.Val.add_trace_elem (Trace.Return location)
+              Dom.Val.subst v eval_sym_trace location
+              |> Dom.Val.add_trace_elem (Trace.Return location)
             in
             Dom.Mem.add_heap loc v acc )
       in
@@ -52,13 +53,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let ret_var = Loc.of_var (Var.of_id id) in
     let add_ret_alias l = Dom.Mem.load_alias id l mem in
     let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in
-    Dom.Val.subst ret_val subst_map location
+    Dom.Val.subst ret_val eval_sym_trace location
     |> Dom.Val.add_trace_elem (Trace.Return location)
     |> Fn.flip (Dom.Mem.add_stack ret_var) mem
     |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
 
 
-  let instantiate_param tenv pdesc params callee_exit_mem subst_map location mem =
+  let instantiate_param tenv pdesc params callee_exit_mem eval_sym_trace location mem =
     let formals = Sem.get_formals pdesc in
     let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem) params in
     let f mem formal actual =
@@ -76,7 +77,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 let formal_fields = PowLoc.append_field formal_locs ~fn in
                 let v = Dom.Mem.find_set formal_fields callee_exit_mem in
                 let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) ~fn in
-                Dom.Val.subst v subst_map location
+                Dom.Val.subst v eval_sym_trace location
                 |> Fn.flip (Dom.Mem.strong_update actual_fields) mem
               in
               List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields
@@ -89,7 +90,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             in
             let v = Dom.Mem.find_set formal_locs callee_exit_mem in
             let actual_locs = Dom.Val.get_all_locs actual in
-            Dom.Val.subst v subst_map location |> Fn.flip (Dom.Mem.strong_update actual_locs) mem )
+            Dom.Val.subst v eval_sym_trace location
+            |> Fn.flip (Dom.Mem.strong_update actual_locs) mem )
       | _ ->
           mem
     in
@@ -113,15 +115,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       -> Location.t
       -> Dom.Mem.astate =
    fun tenv ret callee_pdesc callee_pname params caller_mem summary location ->
-    let callee_symbol_table = Dom.Summary.get_symbol_table summary in
     let callee_exit_mem = Dom.Summary.get_output summary in
-    let bound_subst_map, ret_alias, rel_subst_map =
+    let ret_alias, rel_subst_map =
-      Sem.get_subst_map tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem
+      Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem
     in
+    let eval_sym_trace = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in
     let caller_mem =
-      instantiate_ret ret callee_pname ~callee_exit_mem bound_subst_map caller_mem ret_alias
+      instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem ret_alias
         location
-      |> instantiate_param tenv callee_pdesc params callee_exit_mem bound_subst_map location
+      |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location
       |> forget_ret_relation ret callee_pname
     in
     Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
@@ -492,15 +494,13 @@ module Report = struct
       -> Location.t
       -> PO.ConditionSet.t =
    fun tenv callee_pdesc params caller_mem summary location ->
-    let callee_symbol_table = Dom.Summary.get_symbol_table summary in
     let callee_exit_mem = Dom.Summary.get_output summary in
     let callee_cond = Dom.Summary.get_cond_set summary in
-    let bound_subst_map, _, rel_subst_map =
+    let _, rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in
-      Sem.get_subst_map tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem
-    in
     let pname = Procdesc.get_proc_name callee_pdesc in
     let caller_rel = Dom.Mem.get_relation caller_mem in
-    PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel pname location
+    let eval_sym_trace = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in
+    PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel pname location
 
 
   let check_instr :
@@ -709,7 +709,7 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
   let summary =
     match exit_mem with
     | Some exit_mem ->
-        let post = (Itv.SymbolTable.summary_of symbol_table, exit_mem, cond_set) in
+        let post = (exit_mem, cond_set) in
         ( if Config.bo_debug >= 1 then
           let proc_name = Procdesc.get_proc_name proc_desc in
           print_summary proc_name post ) ;

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -276,25 +276,22 @@ module Val = struct
 
   let subst :
          t
-      -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t
+      -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) * (Symb.Symbol.t -> TraceSet.t)
       -> Location.t
       -> t =
-   fun x (bound_map, trace_map) location ->
+   fun x (eval_sym, trace_of_sym) location ->
     let symbols = get_symbols x in
     let traces_caller =
       List.fold symbols
-        ~f:(fun traces symbol ->
+        ~f:(fun traces symbol -> TraceSet.join (trace_of_sym symbol) traces)
-          try TraceSet.join (Itv.SymbolMap.find symbol trace_map) traces with Caml.Not_found ->
-            traces )
         ~init:TraceSet.empty
     in
     let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in
-    {x with itv= Itv.subst x.itv bound_map; arrayblk= ArrayBlk.subst x.arrayblk bound_map; traces}
+    {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces}
+    (* normalize bottom *)
     |> normalize
 
 
-  (* normalize bottom *)
-
   let add_trace_elem : Trace.elem -> t -> t =
    fun elem x ->
     let traces = TraceSet.add_elem elem x.traces in
@@ -999,16 +996,13 @@ module Mem = struct
 end
 
 module Summary = struct
-  type t = Itv.SymbolTable.summary_t * Mem.t * PO.ConditionSet.summary_t
+  type t = Mem.t * PO.ConditionSet.summary_t
-
-  let get_symbol_table : t -> Itv.SymbolTable.summary_t = fst3
 
-  let get_output : t -> Mem.t = snd3
+  let get_output : t -> Mem.t = fst
 
-  let get_cond_set : t -> PO.ConditionSet.summary_t = trd3
+  let get_cond_set : t -> PO.ConditionSet.summary_t = snd
 
   let pp : F.formatter -> t -> unit =
-   fun fmt (symbol_table, exit_mem, condition_set) ->
+   fun fmt (exit_mem, condition_set) ->
-    F.fprintf fmt "%a@;%a@;%a" Itv.SymbolTable.pp symbol_table Mem.pp exit_mem
+    F.fprintf fmt "%a@;%a" Mem.pp exit_mem PO.ConditionSet.pp_summary condition_set
-      PO.ConditionSet.pp_summary condition_set
 end

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -93,8 +93,8 @@ module AllocSizeCondition = struct
               {report_issue_type= None; propagate} ) )
 
 
-  let subst bound_map length =
+  let subst eval_sym length =
-    match ItvPure.subst length bound_map with NonBottom length -> Some length | Bottom -> None
+    match ItvPure.subst length eval_sym with NonBottom length -> Some length | Bottom -> None
 end
 
 module ArrayAccessCondition = struct
@@ -266,13 +266,13 @@ module ArrayAccessCondition = struct
 
 
   let subst :
-         Itv.Bound.t bottom_lifted Itv.SymbolMap.t
+         (Symb.Symbol.t -> Bound.t bottom_lifted)
       -> Relation.SubstMap.t
       -> Relation.astate
       -> t
       -> t option =
-   fun bound_map rel_map caller_relation c ->
+   fun eval_sym rel_map caller_relation c ->
-    match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with
+    match (ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym) with
     | NonBottom idx, NonBottom size ->
         let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in
         let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in
@@ -304,11 +304,11 @@ module Condition = struct
         ArrayAccessCondition.get_symbols c
 
 
-  let subst bound_map rel_map caller_relation = function
+  let subst eval_sym rel_map caller_relation = function
     | AllocSize c ->
-        AllocSizeCondition.subst bound_map c |> make_alloc_size
+        AllocSizeCondition.subst eval_sym c |> make_alloc_size
     | ArrayAccess {is_collection_add; c} ->
-        ArrayAccessCondition.subst bound_map rel_map caller_relation c
+        ArrayAccessCondition.subst eval_sym rel_map caller_relation c
         |> make_array_access ~is_collection_add
 
 
@@ -460,24 +460,20 @@ module ConditionWithTrace = struct
         cmp
 
 
-  let subst (bound_map, trace_map) rel_map caller_relation callee_pname call_site cwt =
+  let subst (eval_sym, trace_of_sym) rel_map caller_relation callee_pname call_site cwt =
     let symbols = Condition.get_symbols cwt.cond in
     if List.is_empty symbols then
       L.(die InternalError)
         "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
          the first place?"
         pp_summary cwt Typ.Procname.pp callee_pname Location.pp call_site ;
-    match Condition.subst bound_map rel_map caller_relation cwt.cond with
+    match Condition.subst eval_sym rel_map caller_relation cwt.cond with
     | None ->
         None
     | Some cond ->
         let traces_caller =
           List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol ->
-              match Itv.SymbolMap.find symbol trace_map with
+              ValTraceSet.join (trace_of_sym symbol) val_traces )
-              | symbol_trace ->
-                  ValTraceSet.join symbol_trace val_traces
-              | exception Caml.Not_found ->
-                  val_traces )
         in
         let trace =
           ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace
@@ -606,10 +602,10 @@ module ConditionSet = struct
     |> add_opt location val_traces condset
 
 
-  let subst condset bound_map_trace_map rel_subst_map caller_relation callee_pname call_site =
+  let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site =
     let subst_add_cwt condset cwt =
       match
-        ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation callee_pname
+        ConditionWithTrace.subst eval_sym_trace rel_subst_map caller_relation callee_pname
           call_site cwt
       with
       | None ->

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -52,7 +52,7 @@ module ConditionSet : sig
 
   val subst :
        summary_t
-    -> Bounds.Bound.t bottom_lifted Symb.SymbolMap.t * ValTraceSet.t Symb.SymbolMap.t
+    -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) * (Symb.Symbol.t -> ValTraceSet.t)
     -> Relation.SubstMap.t
     -> Relation.astate
     -> Typ.Procname.t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -268,6 +268,92 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
       Val.bot
 
 
+let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
+ fun pdesc ->
+  let proc_name = Procdesc.get_proc_name pdesc in
+  Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
+
+
+module ParamBindings = struct
+  include PrettyPrintable.MakePPMap (struct
+    include Pvar
+
+    let pp = pp Pp.text
+  end)
+
+  let make formals actuals =
+    let rec add_binding formals actuals acc =
+      match (formals, actuals) with
+      | (formal, _) :: formals', actual :: actuals' ->
+          add_binding formals' actuals' (add formal actual acc)
+      | _, _ ->
+          acc
+    in
+    add_binding formals actuals empty
+end
+
+let rec eval_sympath_partial params p mem =
+  match p with
+  | Symb.SymbolPath.Pvar x ->
+      ParamBindings.find x params
+  | Symb.SymbolPath.Index _ | Symb.SymbolPath.Field _ ->
+      let locs = eval_locpath params p mem in
+      Mem.find_set locs mem
+
+
+and eval_locpath params p mem =
+  match p with
+  | Symb.SymbolPath.Pvar _ ->
+      let v = eval_sympath_partial params p mem in
+      Val.get_all_locs v
+  | Symb.SymbolPath.Index p ->
+      let v = eval_sympath_partial params p mem in
+      Val.get_all_locs v
+  | Symb.SymbolPath.Field (fn, p) ->
+      let locs = eval_locpath params p mem in
+      PowLoc.append_field ~fn locs
+
+
+let eval_sympath params sympath mem =
+  match sympath with
+  | Symb.SymbolPath.Normal p ->
+      let v = eval_sympath_partial params p mem in
+      (Val.get_itv v, Val.get_traces v)
+  | Symb.SymbolPath.Offset p ->
+      let v = eval_sympath_partial params p mem in
+      (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v)
+  | Symb.SymbolPath.Length p ->
+      let v = eval_sympath_partial params p mem in
+      (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v)
+
+
+let mk_eval_sym_trace callee_pdesc actual_exps caller_mem =
+  let formals = get_formals callee_pdesc in
+  let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) actual_exps in
+  let params = ParamBindings.make formals actuals in
+  let eval_sym_traced s =
+    let sympath = Symb.Symbol.path s in
+    let itv, traces = eval_sympath params sympath caller_mem in
+    if Itv.eq itv Itv.bot then (Bottom, TraceSet.empty)
+    else
+      let get_bound =
+        match Symb.Symbol.bound_end s with
+        | Symb.BoundEnd.LowerBound ->
+            Itv.lb
+        | Symb.BoundEnd.UpperBound ->
+            Itv.ub
+      in
+      (NonBottom (get_bound itv), traces)
+  in
+  let eval_sym s = fst (eval_sym_traced s) in
+  let trace_of_sym s = snd (eval_sym_traced s) in
+  (eval_sym, trace_of_sym)
+
+
+let mk_eval_sym callee_pdesc actual_exps caller_mem =
+  fst (mk_eval_sym_trace callee_pdesc actual_exps caller_mem)
+
+
 let get_sym_f mem e = Val.get_sym (eval e mem)
 
 let get_offset_sym_f mem e = Val.get_offset_sym (eval e mem)
@@ -416,31 +502,17 @@ module Prune = struct
     Mem.set_prune_pairs prune_pairs mem
 end
 
-let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
- fun pdesc ->
-  let proc_name = Procdesc.get_proc_name pdesc in
-  Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
-
-
 let get_matching_pairs :
        Tenv.t
-    -> Itv.SymbolPath.partial
     -> Val.t
     -> Val.t
     -> Exp.t option
     -> Typ.t
     -> Mem.astate
-    -> Itv.SymbolTable.summary_t
     -> Mem.astate
-    -> (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
+    -> AliasTarget.t option * (Relation.Var.t * Relation.SymExp.t option) list =
-       * AliasTarget.t option
+ fun tenv callee_v actual actual_exp_opt typ caller_mem callee_exit_mem ->
-       * (Relation.Var.t * Relation.SymExp.t option) list =
- fun tenv formal callee_v actual actual_exp_opt typ caller_mem callee_symbol_table callee_exit_mem ->
-  let open Itv in
   let callee_ret_alias = Mem.find_ret_alias callee_exit_mem in
-  let get_itv v = Val.get_itv v in
-  let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in
-  let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in
   let get_offset_sym v = Val.get_offset_sym v in
   let get_size_sym v = Val.get_size_sym v in
   let get_field_name (fn, _, _) = fn in
@@ -462,14 +534,6 @@ let get_matching_pairs :
     | None ->
         ()
   in
-  let add_pair_itv path1 itv2 traces l =
-    match SymbolTable.find_opt path1 callee_symbol_table with
-    | Some (lb1, ub1) ->
-        if Itv.eq itv2 bot then (lb1, Bottom, TraceSet.empty) :: (ub1, Bottom, TraceSet.empty) :: l
-        else (lb1, NonBottom (lb itv2), traces) :: (ub1, NonBottom (ub itv2), traces) :: l
-    | _ ->
-        l
-  in
   let add_pair_sym_main_value v1 v2 ~e2_opt l =
     Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var ->
         let sym_exp_opt =
@@ -483,63 +547,40 @@ let get_matching_pairs :
     Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var ->
         (var, Relation.SymExp.of_sym s2) :: l )
   in
-  let add_pair_val path1 v1 v2 ~e2_opt (bound_pairs, rel_pairs) =
+  let add_pair_val v1 v2 ~e2_opt rel_pairs =
     add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
-    let bound_pairs =
+    rel_pairs
-      bound_pairs
+    |> add_pair_sym_main_value v1 v2 ~e2_opt
-      |> add_pair_itv (SymbolPath.normal path1) (get_itv v2) (Val.get_traces v2)
+    |> add_pair_sym (get_offset_sym v1) (get_offset_sym v2)
-      |> add_pair_itv (SymbolPath.offset path1) (get_offset v2) (Val.get_traces v2)
+    |> add_pair_sym (get_size_sym v1) (get_size_sym v2)
-      |> add_pair_itv (SymbolPath.length path1) (get_size v2) (Val.get_traces v2)
-    in
-    let rel_pairs =
-      rel_pairs
-      |> add_pair_sym_main_value v1 v2 ~e2_opt
-      |> add_pair_sym (get_offset_sym v1) (get_offset_sym v2)
-      |> add_pair_sym (get_size_sym v1) (get_size_sym v2)
-    in
-    (bound_pairs, rel_pairs)
   in
-  let add_pair_field path1 v1 v2 pairs fn =
+  let add_pair_field v1 v2 pairs fn =
     add_ret_alias (append_field v1 fn) (append_field v2 fn) ;
-    let path1' = SymbolPath.field (SymbolPath.index path1) fn in
     let v1' = deref_field v1 fn callee_exit_mem in
     let v2' = deref_field v2 fn caller_mem in
-    add_pair_val path1' v1' v2' ~e2_opt:None pairs
+    add_pair_val v1' v2' ~e2_opt:None pairs
   in
-  let add_pair_ptr typ path1 v1 v2 pairs =
+  let add_pair_ptr typ v1 v2 pairs =
     add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
     match typ.Typ.desc with
     | Typ.Tptr ({desc= Tstruct typename}, _) -> (
       match Tenv.lookup tenv typename with
       | Some str ->
           let fns = List.map ~f:get_field_name str.Typ.Struct.fields in
-          List.fold ~f:(add_pair_field path1 v1 v2) ~init:pairs fns
+          List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns
       | _ ->
           pairs )
     | Typ.Tptr (_, _) ->
-        let path1' = SymbolPath.index path1 in
         let v1' = deref_ptr v1 callee_exit_mem in
         let v2' = deref_ptr v2 caller_mem in
-        add_pair_val path1' v1' v2' ~e2_opt:None pairs
+        add_pair_val v1' v2' ~e2_opt:None pairs
     | _ ->
         pairs
   in
-  let bound_pairs, rel_pairs =
+  let rel_pairs =
-    ([], [])
+    [] |> add_pair_val callee_v actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ callee_v actual
-    |> add_pair_val formal callee_v actual ~e2_opt:actual_exp_opt
-    |> add_pair_ptr typ formal callee_v actual
-  in
-  (bound_pairs, !ret_alias, rel_pairs)
-
-
-let subst_map_of_bound_pairs :
-       (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
-    -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t =
- fun pairs ->
-  let add_pair (bound_map, trace_map) (formal, actual, traces) =
-    (Itv.SymbolMap.add formal actual bound_map, Itv.SymbolMap.add formal traces trace_map)
   in
-  List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs
+  (!ret_alias, rel_pairs)
 
 
 let subst_map_of_rel_pairs :
@@ -575,25 +616,19 @@ let get_subst_map :
     -> Procdesc.t
     -> (Exp.t * 'a) list
     -> Mem.astate
-    -> Itv.SymbolTable.summary_t
     -> Mem.astate
-    -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t)
+    -> AliasTarget.t option * Relation.SubstMap.t =
-       * AliasTarget.t option
+ fun tenv callee_pdesc params caller_mem callee_exit_mem ->
-       * Relation.SubstMap.t =
+  let add_pair (formal, typ) (actual, actual_exp) (ret_alias, rel_l) =
- fun tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem ->
-  let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) =
     let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in
-    let new_bound_matching, ret_alias', new_rel_matching =
+    let ret_alias', new_rel_matching =
-      get_matching_pairs tenv (Itv.SymbolPath.of_pvar formal) callee_v actual actual_exp typ
+      get_matching_pairs tenv callee_v actual actual_exp typ caller_mem callee_exit_mem
-        caller_mem callee_symbol_table callee_exit_mem
     in
-    ( List.rev_append new_bound_matching bound_l
+    (Option.first_some ret_alias ret_alias', List.rev_append new_rel_matching rel_l)
-    , Option.first_some ret_alias ret_alias'
-    , List.rev_append new_rel_matching rel_l )
   in
   let formals = get_formals callee_pdesc in
   let actuals = List.map ~f:(fun (a, _) -> (eval a caller_mem, Some a)) params in
-  let bound_pairs, ret_alias, rel_pairs =
+  let ret_alias, rel_pairs =
-    list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:([], None, [])
+    list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:(None, [])
   in
-  (subst_map_of_bound_pairs bound_pairs, ret_alias, subst_map_of_rel_pairs rel_pairs)
+  (ret_alias, subst_map_of_rel_pairs rel_pairs)

infer/src/bufferoverrun/itv.ml

@@ -30,7 +30,6 @@ module Boolean = struct
 end
 
 open Ints
-module SymbolMap = Symb.SymbolMap
 module Symbol = Symb.Symbol
 module SymbolPath = Symb.SymbolPath
 module SymbolTable = Symb.SymbolTable
@@ -66,8 +65,8 @@ module NonNegativeBound = struct
           Bounds.Constant (NonNegativeInt.of_int_exn c) )
 
 
-  let subst_exn b map =
+  let subst b map =
-    match Bound.subst_ub_exn b map with
+    match Bound.subst_ub b map with
     | Bottom ->
         Bounds.Constant NonNegativeInt.zero
     | NonBottom b ->
@@ -81,8 +80,10 @@ module type NonNegativeSymbol = sig
 
   val int_ub : t -> NonNegativeInt.t option
 
-  val subst_exn : t -> Bound.t bottom_lifted SymbolMap.t -> (NonNegativeInt.t, t) Bounds.valclass
+  val subst :
-  (** may throw Symbol_not_found *)
+       t
+    -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted)
+    -> (NonNegativeInt.t, t) Bounds.valclass
 
   val pp : F.formatter -> t -> unit
 end
@@ -295,28 +296,26 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
   let subst =
     let exception ReturnTop in
     (* avoids top-lifting everything *)
-    let rec subst {const; terms} map =
+    let rec subst {const; terms} eval_sym =
       M.fold
         (fun s p acc ->
-          match S.subst_exn s map with
+          match S.subst s eval_sym with
           | Constant c -> (
             match PositiveInt.of_int (c :> int) with
             | None ->
                 acc
             | Some c ->
-                let p = subst p map in
+                let p = subst p eval_sym in
                 mult_const_positive p c |> plus acc )
           | ValTop ->
-              let p = subst p map in
+              let p = subst p eval_sym in
               if is_zero p then acc else raise ReturnTop
           | Symbolic s ->
-              let p = subst p map in
+              let p = subst p eval_sym in
-              mult_symb p s |> plus acc
+              mult_symb p s |> plus acc )
-          | exception Bounds.Symbol_not_found _ ->
-              raise ReturnTop )
         terms (of_non_negative_int const)
     in
-    fun p map -> match subst p map with p -> NonTop p | exception ReturnTop -> Top
+    fun p eval_sym -> match subst p eval_sym with p -> NonTop p | exception ReturnTop -> Top
 
 
   let rec degree {terms} : int = M.fold (fun _ p acc -> max acc (degree p + 1)) terms 0
@@ -389,7 +388,9 @@ module NonNegativePolynomial = struct
 
   let widen ~prev ~next ~num_iters:_ = if ( <= ) ~lhs:next ~rhs:prev then prev else Top
 
-  let subst p map = match p with Top -> Top | NonTop p -> NonNegativeNonTopPolynomial.subst p map
+  let subst p eval_sym =
+    match p with Top -> Top | NonTop p -> NonNegativeNonTopPolynomial.subst p eval_sym
+
 
   let degree p =
     match p with Top -> None | NonTop p -> Some (NonNegativeNonTopPolynomial.degree p)
@@ -435,16 +436,13 @@ module ItvPure = struct
 
   let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false
 
-  let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted =
+  let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted =
-   fun (l, u) map ->
+   fun (l, u) eval_sym ->
-    match (Bound.subst_lb_exn l map, Bound.subst_ub_exn u map) with
+    match (Bound.subst_lb l eval_sym, Bound.subst_ub u eval_sym) with
     | NonBottom l, NonBottom u ->
         NonBottom (l, u)
     | _ ->
         Bottom
-    | exception Bounds.Symbol_not_found _ ->
-        (* For now, let's be VERY aggressive. Under-approximate unknown symbols with Bottom. *)
-        Bottom
 
 
   let ( <= ) : lhs:t -> rhs:t -> bool =
@@ -1000,8 +998,8 @@ let prune_eq : t -> t -> t = bind2 ItvPure.prune_eq
 
 let prune_ne : t -> t -> t = bind2 ItvPure.prune_ne
 
-let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t =
+let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t =
- fun x map -> match x with NonBottom x' -> ItvPure.subst x' map | _ -> x
+ fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x
 
 
 let get_symbols : t -> Symbol.t list = function

infer/src/bufferoverrun/itv.mli

@@ -25,7 +25,6 @@ module Boolean : sig
   val is_true : t -> bool
 end
 
-module SymbolMap = Symb.SymbolMap
 module Symbol = Symb.Symbol
 module SymbolPath = Symb.SymbolPath
 module SymbolTable = Symb.SymbolTable
@@ -51,7 +50,7 @@ module NonNegativePolynomial : sig
 
   val min_default_left : astate -> astate -> astate
 
-  val subst : astate -> Bound.t bottom_lifted SymbolMap.t -> astate
+  val subst : astate -> (Symb.Symbol.t -> Bound.t AbstractDomain.Types.bottom_lifted) -> astate
 
   val degree : astate -> int option
 
@@ -121,7 +120,7 @@ module ItvPure : sig
 
   val get_symbols : t -> Symbol.t list
 
-  val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted
+  val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted
 end
 
 include module type of AbstractDomain.BottomLifted (ItvPure)
@@ -224,4 +223,4 @@ val prune_eq : t -> t -> t
 
 val prune_ne : t -> t -> t
 
-val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t
+val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t

infer/src/bufferoverrun/symb.ml

@@ -83,18 +83,14 @@ module Symbol = struct
   let is_unsigned : t -> bool = fun x -> x.unsigned
 
   let path {path} = path
+
+  let bound_end {bound_end} = bound_end
 end
 
 module SymbolTable = struct
   module M = PrettyPrintable.MakePPMap (SymbolPath)
 
-  type summary_t = (Symbol.t * Symbol.t) M.t
+  type t = (Symbol.t * Symbol.t) M.t ref
-
-  let find_opt = M.find_opt
-
-  let pp = M.pp ~pp_value:(fun fmt (lb, ub) -> F.fprintf fmt "[%a, %a]" Symbol.pp lb Symbol.pp ub)
-
-  type t = summary_t ref
 
   let empty () = ref M.empty
 
@@ -109,9 +105,6 @@ module SymbolTable = struct
         in
         symbol_table := M.add path s !symbol_table ;
         s
-
-
-  let summary_of x = !x
 end
 
 module SymbolMap = struct

infer/src/bufferoverrun/symb.mli

@@ -16,9 +16,9 @@ module BoundEnd : sig
 end
 
 module SymbolPath : sig
-  type partial
+  type partial = private Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial
 
-  type t
+  type t = private Normal of partial | Offset of partial | Length of partial
 
   val pp : F.formatter -> t -> unit
 
@@ -49,6 +49,8 @@ module Symbol : sig
   val paths_equal : t -> t -> bool
 
   val path : t -> SymbolPath.t
+
+  val bound_end : t -> BoundEnd.t
 end
 
 module SymbolMap : sig
@@ -60,20 +62,10 @@ module SymbolMap : sig
 end
 
 module SymbolTable : sig
-  module M : PrettyPrintable.PPMap with type key = SymbolPath.t
-
-  type summary_t
-
-  val pp : F.formatter -> summary_t -> unit
-
-  val find_opt : SymbolPath.t -> summary_t -> (Symbol.t * Symbol.t) option
-
   type t
 
   val empty : unit -> t
 
-  val summary_of : t -> summary_t
-
   val lookup :
-    unsigned:bool -> Typ.Procname.t -> M.key -> t -> Counter.t -> SymbolMap.key * SymbolMap.key
+    unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> t -> Counter.t -> Symbol.t * Symbol.t
 end

infer/src/checkers/cost.ml

@@ -42,7 +42,7 @@ module TransferFunctionsNodesBasicCost = struct
 
   let cost_atomic_instruction = BasicCost.one
 
-  let instantiate_cost ~tenv ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
+  let instantiate_cost ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
     match Ondemand.get_proc_desc callee_pname with
     | None ->
         L.(die InternalError)
@@ -54,20 +54,16 @@ module TransferFunctionsNodesBasicCost = struct
           L.(die InternalError)
             "Can't instantiate symbolic cost %a from call to %a (can't get summary)" BasicCost.pp
             callee_cost Typ.Procname.pp callee_pname
-      | Some inferbo_summary ->
+      | Some _ ->
           let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in
-          let callee_symbol_table = BufferOverrunDomain.Summary.get_symbol_table inferbo_summary in
+          let eval_sym =
-          let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in
+            BufferOverrunSemantics.mk_eval_sym callee_pdesc params inferbo_caller_mem
-          let (subst_map, _), _, _ =
-            BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem
-              callee_symbol_table callee_exit_mem
           in
-          BasicCost.subst callee_cost subst_map )
+          BasicCost.subst callee_cost eval_sym )
 
 
   let exec_instr_cost inferbo_mem (astate : CostDomain.NodeInstructionToCostMap.astate)
-      {ProcData.pdesc; tenv} (node : CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate
+      {ProcData.pdesc} (node : CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate =
-      =
     let key = CFG.Node.id node in
     let astate' =
       match instr with
@@ -76,7 +72,7 @@ module TransferFunctionsNodesBasicCost = struct
             match Payload.read pdesc callee_pname with
             | Some {post= callee_cost} ->
                 if BasicCost.is_symbolic callee_cost then
-                  instantiate_cost ~tenv ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem
+                  instantiate_cost ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem
                     ~callee_pname ~params ~callee_cost
                 else callee_cost
             | None ->

infer/tests/codetoanalyze/c/bufferoverrun/get_field.c

@@ -13,7 +13,7 @@ struct st {
 
 int get_field(t* x) { return x->field; }
 
-void FN_call_get_field_cond_Bad() {
+void call_get_field_cond_Bad() {
   int a[5];
   t x = {0};
   if (get_field_wrapper(&x)) {
@@ -23,13 +23,13 @@ void FN_call_get_field_cond_Bad() {
   }
 }
 
-void call_get_field_Good() {
+void FP_call_get_field_Good() {
   int a[5];
   t x = {0};
   a[get_field_wrapper(&x)] = 0;
 }
 
-void FN_call_get_field_Bad() {
+void call_get_field_Bad() {
   int a[5];
   t x = {10};
   a[get_field_wrapper(&x)] = 0;

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -25,8 +25,9 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: 100 Size: 10 by call to `arr_access` ]
-codetoanalyze/c/bufferoverrun/get_field.c, FN_call_get_field_cond_Bad, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/c/bufferoverrun/get_field.c, FN_call_get_field_cond_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]