From 62d45f9c0167ffc5333dfb44999caa61c98a71ea Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 29 Nov 2018 07:38:19 -0800 Subject: [PATCH] [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 | 13 ++-- .../src/bufferoverrun/bufferOverrunChecker.ml | 72 +++++-------------- .../codetoanalyze/cpp/bufferoverrun/class.cpp | 2 +- .../cpp/bufferoverrun/issues.exp | 3 +- .../codetoanalyze/java/performance/issues.exp | 1 - 5 files changed, 25 insertions(+), 66 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 26143d980..58c015ba8 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/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 = - match Loc.get_param_path l with - | None -> - add l acc - | Some path -> - join acc (eval_locpath path) - in - fold subst1 x empty + fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty end (** unsound but ok for bug catching *) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index dc26cd0ad..6e145171c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 copy_reachable_new_locs_from locs mem = + let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_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_val = Dom.Mem.find ret_loc callee_exit_mem in - let ret_var = Loc.of_var (Var.of_id id) in - Dom.Val.subst ret_val eval_sym_trace 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) - - - 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 + let ret_var = Loc.of_var (Var.of_id ret_id) in + let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in + let formals = + List.fold (Sem.get_formals callee_pdesc) ~init:PowLoc.bot ~f:(fun acc (formal, _) -> + let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in + PowLoc.join acc (Dom.Val.get_all_locs v) ) 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_param tenv integer_type_widths callee_pdesc params callee_exit_mem - eval_sym_trace location + instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace + caller_mem location |> forget_ret_relation ret callee_pname in Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp index a95bdd108..a45c2d5ee 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp +++ b/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; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index e71e41a70..6ab4e2642 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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,,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, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 3] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: 3 Size: 3] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `n`,Assignment,,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, [,Call,Parameter `n`,Assignment,,Call,Parameter `this[*].arr`,Array access: Offset: 10 Size: 10] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index c12605152..dfc37d249 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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, [,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.(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []