[inferbo] Copy callee's values that are reachable from parameters

Summary:
At function calls, it copies callee's values that are reachable from parameters.

Depends on D13231291

Reviewed By: mbouaziz

Differential Revision: D13231711

fbshipit-source-id: 1e8aed1c4

infer/src/bufferoverrun/absLoc.ml

@@ -175,15 +175,12 @@ 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) =
-    let subst1 l acc =
+    fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty
-      match Loc.get_param_path l with
-      | None ->
-          add l acc
-      | Some path ->
-          join acc (eval_locpath path)
-    in
-    fold subst1 x empty
 end
 
 (** unsound but ok for bug catching *)

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -183,12 +183,14 @@ module TransferFunctions = struct
 
   type nonrec extras = extras
 
-  let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace mem location =
+  let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem
-    let copy_reachable_new_locs_from locs mem =
+      ({Dom.eval_locpath} as eval_sym_trace) mem location =
+    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
-            Dom.Mem.add_heap loc v acc )
+            PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc )
       in
       let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in
       PowLoc.fold copy reachable_locs mem
@@ -197,7 +199,7 @@ module TransferFunctions = struct
       let subst_loc l =
         Option.find_map (Loc.get_path l) ~f:(fun partial ->
             try
-              let locs = eval_sym_trace.Dom.eval_locpath partial in
+              let locs = eval_locpath partial in
               match PowLoc.is_singleton_or_more locs with
               | IContainer.Singleton loc ->
                   Some loc
@@ -209,55 +211,18 @@ 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 id l mem)
+      Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias ret_id l mem)
     in
-    let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
+    let ret_var = Loc.of_var (Var.of_id ret_id) in
-    let ret_val = Dom.Mem.find ret_loc callee_exit_mem in
+    let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in
-    let ret_var = Loc.of_var (Var.of_id id) in
+    let formals =
-    Dom.Val.subst ret_val eval_sym_trace location
+      List.fold (Sem.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
-    |> instantiate_ret_alias
+          PowLoc.join acc (Dom.Val.get_all_locs v) )
-    |> 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 = Sem.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
+    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))
 
 
   let forget_ret_relation ret callee_pname mem =
@@ -286,9 +251,8 @@ module TransferFunctions = struct
       Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem
     in
     let caller_mem =
-      instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem location
+      instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace
-      |> instantiate_param tenv integer_type_widths callee_pdesc params callee_exit_mem
+        caller_mem location
-           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/tests/codetoanalyze/cpp/bufferoverrun/class.cpp

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

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

@@ -18,8 +18,7 @@ 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_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 3]
+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_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_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 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]

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

@@ -125,7 +125,6 @@ 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, []