[inferbo] Simplify instantiate_ret_alias

Summary: It simplifies instantiataion of `ret_alias`. While it got `ret_alias` values by iterating caller's and callee's memory, now it gets `ret_alias` by evaluating symbol paths included in location values.

Reviewed By: mbouaziz

Differential Revision: D9569606

fbshipit-source-id: a3326bb81

infer/src/bufferoverrun/absLoc.ml

@@ -12,7 +12,14 @@ open! IStd
 module F = Format
 
 module Allocsite = struct
-  type t = Unknown | Known of {proc_name: string; node_hash: int; inst_num: int; dimension: int}
+  type t =
+    | Unknown
+    | Known of
+        { proc_name: string
+        ; node_hash: int
+        ; inst_num: int
+        ; dimension: int
+        ; path: Symb.SymbolPath.partial option }
   [@@deriving compare]
 
   let pp fmt = function
@@ -24,12 +31,20 @@ module Allocsite = struct
 
   let to_string x = F.asprintf "%a" pp x
 
-  let make : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> t =
+  let make :
-   fun proc_name ~node_hash ~inst_num ~dimension ->
+         Typ.Procname.t
-    Known {proc_name= Typ.Procname.to_string proc_name; node_hash; inst_num; dimension}
+      -> node_hash:int
+      -> inst_num:int
+      -> dimension:int
+      -> path:Symb.SymbolPath.partial option
+      -> t =
+   fun proc_name ~node_hash ~inst_num ~dimension ~path ->
+    Known {proc_name= Typ.Procname.to_string proc_name; node_hash; inst_num; dimension; path}
 
 
   let unknown = Unknown
+
+  let get_path = function Unknown -> None | Known {path} -> path
 end
 
 module Loc = struct
@@ -84,6 +99,16 @@ module Loc = struct
 
 
   let is_field_of ~loc ~field_loc = match field_loc with Field (l, _) -> equal loc l | _ -> false
+
+  let rec get_path = function
+    | Var (LogicalVar _) ->
+        None
+    | Var (ProgramVar pvar) ->
+        Some (Symb.SymbolPath.of_pvar pvar)
+    | Allocsite allocsite ->
+        Allocsite.get_path allocsite
+    | Field (l, fn) ->
+        Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
 end
 
 module PowLoc = struct

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -34,7 +34,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type extras = Itv.SymbolTable.t
 
-  let instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace mem ret_alias location =
+  let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace
+      eval_locs_sympath_partial mem 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 ->
@@ -47,15 +48,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in
       PowLoc.fold copy reachable_locs mem
     in
-    let id = fst ret in
+    let instantiate_ret_alias mem =
+      let subst_loc l =
+        Option.find_map (Loc.get_path l) ~f:(fun partial ->
+            try
+              let locs = eval_locs_sympath_partial partial in
+              if PowLoc.is_singleton locs then Some (PowLoc.choose locs) else None
+            with Caml.Not_found -> None )
+      in
+      let ret_alias =
+        Option.find_map (Dom.Mem.find_ret_alias callee_exit_mem) ~f:(fun alias_target ->
+            Dom.AliasTarget.loc_map alias_target ~f:subst_loc )
+      in
+      Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias id l mem)
+    in
     let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
     let ret_val = Dom.Mem.find ret_loc callee_exit_mem in
     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 eval_sym_trace location
     |> Dom.Val.add_trace_elem (Trace.Return location)
     |> Fn.flip (Dom.Mem.add_stack ret_var) mem
+    |> instantiate_ret_alias
     |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
 
 
@@ -116,12 +129,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       -> Dom.Mem.astate =
    fun tenv ret callee_pdesc callee_pname params caller_mem summary location ->
     let callee_exit_mem = Dom.Summary.get_output summary in
-    let ret_alias, 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_exit_mem
+    let eval_sym_trace, eval_locpath = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in
-    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 eval_sym_trace caller_mem ret_alias
+      instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace eval_locpath caller_mem
         location
       |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location
       |> forget_ret_relation ret callee_pname
@@ -496,10 +507,10 @@ module Report = struct
    fun tenv callee_pdesc params caller_mem summary location ->
     let callee_exit_mem = Dom.Summary.get_output summary in
     let callee_cond = Dom.Summary.get_cond_set summary in
-    let _, rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in
+    let rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in
     let pname = Procdesc.get_proc_name callee_pdesc in
     let caller_rel = Dom.Mem.get_relation caller_mem in
-    let eval_sym_trace = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in
+    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
 
 

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -348,7 +348,12 @@ module AliasTarget = struct
 
   let use l = function Simple l' | Empty l' -> Loc.equal l l'
 
-  let replace l = function Simple _ -> Simple l | Empty _ -> Empty l
+  let loc_map x ~f =
+    match x with
+    | Simple l ->
+        Option.map (f l) ~f:(fun l -> Simple l)
+    | Empty l ->
+        Option.map (f l) ~f:(fun l -> Empty l)
 end
 
 (* Relations between values of logical variables(registers) and

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -109,7 +109,8 @@ let malloc size_exp =
     let typ, stride, length0, dyn_length = get_malloc_info size_exp in
     let length = Sem.eval length0 mem in
     let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in
+    let path = Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path in
+    let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in
     let offset, size = (Itv.zero, Dom.Val.get_itv length) in
     let size_exp_opt =
       let size_exp = Option.value dyn_length ~default:length0 in
@@ -120,7 +121,7 @@ let malloc size_exp =
     |> Dom.Mem.add_stack (Loc.of_id id) v
     |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt
     |> set_uninitialized location typ (Dom.Val.get_array_locs v)
-    |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v)
+    |> BoUtils.Exec.init_array_fields tenv pname path ~node_hash typ (Dom.Val.get_array_locs v)
          ?dyn_length
   and check = check_alloc_size size_exp in
   {exec; check}
@@ -219,7 +220,8 @@ let set_array_length array length_exp =
     | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
         let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
         let stride = Option.map ~f:IntLit.to_int_exn stride in
-        let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in
+        let path = Some (Symb.SymbolPath.of_pvar array_pvar) in
+        let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in
         let v = Dom.Val.of_array_alloc allocsite ~stride ~offset:Itv.zero ~size:length in
         mem
         |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
@@ -349,7 +351,10 @@ module Collection = struct
   let new_list _ =
     let exec {pname; node_hash; location} ~ret:(id, _) mem =
       let loc = Loc.of_id id in
-      let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in
+      let path =
+        Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path
+      in
+      let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in
       let alloc_loc = Loc.of_allocsite allocsite in
       let init_size = Dom.Val.of_int 0 in
       let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces init_size) in

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -347,11 +347,12 @@ let mk_eval_sym_trace callee_pdesc actual_exps caller_mem =
   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 eval_locpath partial = eval_locpath params partial caller_mem in
+  ((eval_sym, trace_of_sym), eval_locpath)
 
 
 let mk_eval_sym callee_pdesc actual_exps caller_mem =
-  fst (mk_eval_sym_trace callee_pdesc actual_exps caller_mem)
+  fst (fst (mk_eval_sym_trace callee_pdesc actual_exps caller_mem))
 
 
 let get_sym_f mem e = Val.get_sym (eval e mem)
@@ -510,9 +511,8 @@ let get_matching_pairs :
     -> Typ.t
     -> Mem.astate
     -> Mem.astate
-    -> AliasTarget.t option * (Relation.Var.t * Relation.SymExp.t option) list =
+    -> (Relation.Var.t * Relation.SymExp.t option) list =
  fun tenv callee_v actual actual_exp_opt typ caller_mem callee_exit_mem ->
-  let callee_ret_alias = Mem.find_ret_alias callee_exit_mem 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
@@ -523,17 +523,6 @@ let get_matching_pairs :
     let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in
     Mem.find_set locs mem
   in
-  let ret_alias = ref None in
-  let add_ret_alias v1 v2 =
-    match callee_ret_alias with
-    | Some ret_loc ->
-        if
-          PowLoc.is_singleton v1 && PowLoc.is_singleton v2
-          && AliasTarget.use (PowLoc.min_elt v1) ret_loc
-        then ret_alias := Some (AliasTarget.replace (PowLoc.min_elt v2) ret_loc)
-    | None ->
-        ()
-  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 =
@@ -548,20 +537,17 @@ let get_matching_pairs :
         (var, Relation.SymExp.of_sym s2) :: l )
   in
   let add_pair_val v1 v2 ~e2_opt rel_pairs =
-    add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
     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
   let add_pair_field v1 v2 pairs fn =
-    add_ret_alias (append_field v1 fn) (append_field v2 fn) ;
     let v1' = deref_field v1 fn callee_exit_mem in
     let v2' = deref_field v2 fn caller_mem in
     add_pair_val v1' v2' ~e2_opt:None pairs
   in
   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
@@ -577,10 +563,7 @@ let get_matching_pairs :
     | _ ->
         pairs
   in
-  let rel_pairs =
   [] |> add_pair_val callee_v actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ callee_v actual
-  in
-  (!ret_alias, rel_pairs)
 
 
 let subst_map_of_rel_pairs :
@@ -612,23 +595,18 @@ let rec list_fold2_def :
 
 
 let get_subst_map :
-       Tenv.t
+    Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> Relation.SubstMap.t =
-    -> Procdesc.t
-    -> (Exp.t * 'a) list
-    -> Mem.astate
-    -> Mem.astate
-    -> AliasTarget.t option * Relation.SubstMap.t =
  fun tenv callee_pdesc params caller_mem callee_exit_mem ->
-  let add_pair (formal, typ) (actual, actual_exp) (ret_alias, rel_l) =
+  let add_pair (formal, typ) (actual, actual_exp) rel_l =
     let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in
-    let ret_alias', new_rel_matching =
+    let new_rel_matching =
       get_matching_pairs tenv callee_v actual actual_exp typ caller_mem callee_exit_mem
     in
-    (Option.first_some ret_alias ret_alias', List.rev_append new_rel_matching rel_l)
+    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 ret_alias, rel_pairs =
+  let 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:[]
   in
-  (ret_alias, subst_map_of_rel_pairs rel_pairs)
+  subst_map_of_rel_pairs rel_pairs

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -57,7 +57,8 @@ module Exec = struct
    fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem ->
     let offset = Itv.zero in
     let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in
+    let path = Loc.get_path loc in
+    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in
     let arr =
       Dom.Val.of_array_alloc allocsite ~stride ~offset ~size
       |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
@@ -83,7 +84,8 @@ module Exec = struct
       -> Dom.Mem.astate
       -> Dom.Mem.astate * int =
    fun pname ~node_hash location loc ~inst_num ~dimension mem ->
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in
+    let path = Loc.get_path loc in
+    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in
     let alloc_loc = Loc.of_allocsite allocsite in
     let alist =
       Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc)
@@ -141,7 +143,9 @@ module Exec = struct
     in
     let alloc_num = Itv.Counter.next new_alloc_num in
     let elem = Trace.SymAssign (loc, location) in
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num in
+    let allocsite =
+      Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path)
+    in
     let arr =
       Dom.Val.of_array_alloc allocsite ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem
     in
@@ -149,9 +153,7 @@ module Exec = struct
       mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc
       |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
     in
-    let deref_loc =
+    let deref_loc = Loc.of_allocsite allocsite in
-      Loc.of_allocsite (Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num)
-    in
     let path = Itv.SymbolPath.index path in
     decl_sym_val pname path tenv ~node_hash location ~depth deref_loc typ mem
 
@@ -174,7 +176,9 @@ module Exec = struct
        mem ->
     let alloc_num = Itv.Counter.next new_alloc_num in
     let elem = Trace.SymAssign (loc, location) in
-    let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num in
+    let allocsite =
+      Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path)
+    in
     let alloc_loc = Loc.of_allocsite allocsite in
     let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.add_trace_elem elem in
     let mem = Dom.Mem.add_heap loc v mem in
@@ -199,8 +203,9 @@ module Exec = struct
     Dom.Mem.add_heap loc size mem
 
 
-  let init_array_fields tenv pname ~node_hash typ locs ?dyn_length mem =
+  let init_array_fields tenv pname path ~node_hash typ locs ?dyn_length mem =
-    let rec init_field locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) =
+    let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) =
+      let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in
       let field_loc = PowLoc.append_field locs ~fn:field_name in
       let mem =
         match field_typ.Typ.desc with
@@ -212,28 +217,30 @@ module Exec = struct
                   Itv.plus i length )
             in
             let stride = Option.map stride ~f:IntLit.to_int_exn in
-            let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in
+            let allocsite =
+              Allocsite.make pname ~node_hash ~inst_num ~dimension ~path:field_path
+            in
             let offset, size = (Itv.zero, length) in
             let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size in
             mem |> Dom.Mem.strong_update field_loc v
             |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
         | _ ->
-            init_fields field_typ field_loc dimension ?dyn_length mem
+            init_fields field_path field_typ field_loc dimension ?dyn_length mem
       in
       (mem, inst_num + 1)
-    and init_fields typ locs dimension ?dyn_length mem =
+    and init_fields path typ locs dimension ?dyn_length mem =
       match typ.Typ.desc with
       | Tstruct typename -> (
         match Tenv.lookup tenv typename with
         | Some str ->
-            let f = init_field locs (dimension + 1) in
+            let f = init_field path locs (dimension + 1) in
             IList.fold_last ~f ~f_last:(f ?dyn_length) ~init:(mem, 1) str.Typ.Struct.fields |> fst
         | None ->
             mem )
       | _ ->
           mem
     in
-    init_fields typ locs 1 ?dyn_length mem
+    init_fields path typ locs 1 ?dyn_length mem
 
 
   let rec set_dyn_length tenv typ locs dyn_length mem =

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -110,6 +110,7 @@ module Exec : sig
   val init_array_fields :
        Tenv.t
     -> Typ.Procname.t
+    -> Itv.SymbolPath.partial option
     -> node_hash:int
     -> Typ.t
     -> PowLoc.t

infer/src/bufferoverrun/symb.mli

@@ -17,6 +17,7 @@ end
 
 module SymbolPath : sig
   type partial = private Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial
+  [@@deriving compare]
 
   type t = private Normal of partial | Offset of partial | Length of partial