Revert "[inferbo] Instantiate symbolic locations in function parameters"

Reviewed By: ngorogiannis

Differential Revision: D13301231

fbshipit-source-id: c763a158b

infer/src/bufferoverrun/absLoc.ml

@@ -73,8 +73,6 @@ module Allocsite = struct
   let unknown = Unknown
 
   let get_path = function Unknown -> None | Param path -> Some path | Known {path} -> path
-
-  let get_param_path = function Param path -> Some path | Unknown | Known _ -> None
 end
 
 module Loc = struct
@@ -150,15 +148,6 @@ module Loc = struct
         Allocsite.get_path allocsite
     | Field (l, fn) ->
         Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
-
-
-  let rec get_param_path = function
-    | Var _ ->
-        None
-    | Allocsite allocsite ->
-        Allocsite.get_param_path allocsite
-    | Field (l, fn) ->
-        Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
 end
 
 module PowLoc = struct
@@ -184,13 +173,6 @@ module PowLoc = struct
 
 
   type eval_locpath = Symb.SymbolPath.partial -> t
-
-  let subst_loc l (eval_locpath : eval_locpath) =
-    match Loc.get_param_path l with None -> singleton l | Some path -> eval_locpath path
-
-
-  let subst x (eval_locpath : eval_locpath) =
-    fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty
 end
 
 (** unsound but ok for bug catching *)

infer/src/bufferoverrun/arrayBlk.ml

@@ -153,19 +153,8 @@ let get_pow_loc : t -> PowLoc.t =
   fold pow_loc_of_allocsite array PowLoc.bot
 
 
-let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> t =
+let subst : t -> Bound.eval_sym -> t =
- fun a eval_sym eval_locpath ->
+ fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
-  let subst1 l info acc =
-    let info' = ArrInfo.subst info eval_sym in
-    match Allocsite.get_param_path l with
-    | None ->
-        add l info' acc
-    | Some path ->
-        let locs = eval_locpath path in
-        let add_allocsite l acc = match l with Loc.Allocsite a -> add a info' acc | _ -> acc in
-        PowLoc.fold add_allocsite locs acc
-  in
-  fold subst1 a empty
 
 
 let get_symbols : t -> Itv.SymbolSet.t =

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -183,14 +183,12 @@ module TransferFunctions = struct
 
   type nonrec extras = extras
 
-  let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem
+  let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace mem location =
-      ({Dom.eval_locpath} as eval_sym_trace) mem location =
+    let copy_reachable_new_locs_from locs mem =
-    let copy_reachable_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 locs = PowLoc.subst_loc loc eval_locpath in
             let v = Dom.Val.subst v eval_sym_trace location in
-            PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc )
+            Dom.Mem.add_heap loc v acc )
       in
       let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in
       PowLoc.fold copy reachable_locs mem
@@ -199,7 +197,7 @@ module TransferFunctions = struct
       let subst_loc l =
         Option.find_map (Loc.get_path l) ~f:(fun partial ->
             try
-              let locs = eval_locpath partial in
+              let locs = eval_sym_trace.Dom.eval_locpath partial in
               match PowLoc.is_singleton_or_more locs with
               | IContainer.Singleton loc ->
                   Some loc
@@ -211,18 +209,54 @@ module TransferFunctions = struct
         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 ret_id l mem)
+      Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias id l mem)
     in
-    let ret_var = Loc.of_var (Var.of_id ret_id) in
+    let ret_var = Loc.of_var (Var.of_id id) in
     let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in
-    let formals =
+    Dom.Val.subst ret_val eval_sym_trace location
-      List.fold (Dom.get_formals callee_pdesc) ~init:PowLoc.bot ~f:(fun acc (formal, _) ->
+    |> Fn.flip (Dom.Mem.add_stack ret_var) mem
-          let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in
-          PowLoc.join acc (Dom.Val.get_all_locs v) )
-    in
-    Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem
     |> instantiate_ret_alias
-    |> copy_reachable_locs_from (PowLoc.join formals (Dom.Val.get_all_locs ret_val))
+    |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
+
+
+  let instantiate_param tenv integer_type_widths pdesc params callee_exit_mem eval_sym_trace
+      location mem =
+    let formals = Dom.get_formals pdesc in
+    let actuals = List.map ~f:(fun (a, _) -> Sem.eval integer_type_widths a mem) params in
+    let f mem formal actual =
+      match (snd formal).Typ.desc with
+      | Typ.Tptr (typ, _) -> (
+        match typ.Typ.desc with
+        | Typ.Tstruct typename -> (
+          match Tenv.lookup tenv typename with
+          | Some str ->
+              let formal_locs =
+                Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem
+                |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
+              in
+              let instantiate_fld mem (fn, _, _) =
+                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 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
+          | _ ->
+              mem )
+        | _ ->
+            let formal_locs =
+              Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem
+              |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
+            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 eval_sym_trace location
+            |> Fn.flip (Dom.Mem.strong_update actual_locs) mem )
+      | _ ->
+          mem
+    in
+    try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem
 
 
   let forget_ret_relation ret callee_pname mem =
@@ -251,8 +285,9 @@ module TransferFunctions = struct
       Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem
     in
     let caller_mem =
-      instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace
+      instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem location
-        caller_mem location
+      |> instantiate_param tenv integer_type_widths 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

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -323,7 +323,7 @@ module Val = struct
 
 
   let subst : t -> eval_sym_trace -> Location.t -> t =
-   fun x {eval_sym; trace_of_sym; eval_locpath} location ->
+   fun x {eval_sym; trace_of_sym} location ->
     let symbols = get_symbols x in
     let traces_caller =
       Itv.SymbolSet.fold
@@ -331,11 +331,7 @@ module Val = struct
         symbols TraceSet.empty
     in
     let traces = TraceSet.call location ~traces_caller ~traces_callee:x.traces in
-    { x with
+    {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces}
-      itv= Itv.subst x.itv eval_sym
-    ; powloc= PowLoc.subst x.powloc eval_locpath
-    ; arrayblk= ArrayBlk.subst x.arrayblk eval_sym eval_locpath
-    ; traces }
     (* normalize bottom *)
     |> normalize
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -327,7 +327,6 @@ let rec eval_sympath_partial params p mem =
 
 
 and eval_locpath params p mem =
-  let res =
   match p with
   | Symb.SymbolPath.Pvar _ ->
       let v = eval_sympath_partial params p mem in
@@ -338,12 +337,6 @@ and eval_locpath params p mem =
   | Symb.SymbolPath.Field (fn, p) ->
       let locs = eval_locpath params p mem in
       PowLoc.append_field ~fn locs
-  in
-  if PowLoc.is_empty res then (
-    L.(debug BufferOverrun Verbose)
-      "Location value for %a is not found.@\n" Symb.SymbolPath.pp_partial p ;
-    PowLoc.unknown )
-  else res
 
 
 let eval_sympath params sympath mem =

infer/src/bufferoverrun/symb.mli

@@ -29,8 +29,6 @@ module SymbolPath : sig
 
   val pp_mark : markup:bool -> F.formatter -> t -> unit
 
-  val pp_partial : F.formatter -> partial -> unit
-
   val pp_partial_paren : paren:bool -> F.formatter -> partial -> unit
 
   val of_pvar : Pvar.t -> partial

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

@@ -3,9 +3,7 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2,
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
-codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
-codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]

infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp

@@ -296,7 +296,7 @@ class my_class6 {
 
   void dummy_function() {}
 
-  void set_x_two_Good() {
+  void set_x_two_Good_FP() {
     int arr[5];
     *x = 0;
     dummy_function();
@@ -312,7 +312,7 @@ class my_class6 {
 
   void set_x_three() { *x = 3; }
 
-  void call_set_x_three_Good() {
+  void call_set_x_three_Good_FP() {
     int arr[5];
     set_x_three();
     arr[*x] = 0;

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

@@ -18,8 +18,10 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRU
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
 codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `x->b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 3]
-codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
+codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -125,6 +125,7 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.
 codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Call,Unknown value from: StringBuilder StringBuilder.append(String),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []