From 4b2c65f2e27bf653d7fbb502ee62345a14e3573a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 4 Dec 2018 07:29:12 -0800 Subject: [PATCH] Revert "[inferbo] Instantiate symbolic locations in function parameters" Reviewed By: ngorogiannis Differential Revision: D13301231 fbshipit-source-id: c763a158b --- infer/src/bufferoverrun/absLoc.ml | 18 ----- infer/src/bufferoverrun/arrayBlk.ml | 15 +--- .../src/bufferoverrun/bufferOverrunChecker.ml | 69 ++++++++++++++----- .../src/bufferoverrun/bufferOverrunDomain.ml | 8 +-- .../bufferoverrun/bufferOverrunSemantics.ml | 27 +++----- infer/src/bufferoverrun/symb.mli | 2 - .../codetoanalyze/c/bufferoverrun/issues.exp | 2 - .../codetoanalyze/cpp/bufferoverrun/class.cpp | 4 +- .../cpp/bufferoverrun/issues.exp | 6 +- .../codetoanalyze/java/performance/issues.exp | 1 + 10 files changed, 73 insertions(+), 79 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index edf432871..0514a3261 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/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 *) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 19c0e7350..325c51506 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/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 = - fun a eval_sym eval_locpath -> - 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 subst : t -> Bound.eval_sym -> t = + fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a let get_symbols : t -> Itv.SymbolSet.t = diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index acdf5f0dd..3fdbe9712 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 - ({Dom.eval_locpath} as eval_sym_trace) mem location = - let copy_reachable_locs_from locs mem = + let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace 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 -> - 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 = - List.fold (Dom.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 - Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem + Dom.Val.subst ret_val eval_sym_trace location + |> Fn.flip (Dom.Mem.add_stack ret_var) 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 - caller_mem location + 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 |> 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/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 1c1edbb02..92f2f0d55 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 - itv= Itv.subst x.itv eval_sym - ; powloc= PowLoc.subst x.powloc eval_locpath - ; arrayblk= ArrayBlk.subst x.arrayblk eval_sym eval_locpath - ; traces } + {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces} (* normalize bottom *) |> normalize diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 2c5c18b01..5494baa50 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -327,23 +327,16 @@ 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 - Val.get_all_locs v - | Symb.SymbolPath.Deref (_, 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 - 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 + match p with + | Symb.SymbolPath.Pvar _ -> + let v = eval_sympath_partial params p mem in + Val.get_all_locs v + | Symb.SymbolPath.Deref (_, 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 = diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 75547782f..0d6de8cec 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 97606a43b..ddc423d38 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,Assignment,Assignment,,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, [,Assignment,,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,,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,,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,,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,,Call,Assignment,Assignment,,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,,Parameter `x`,,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, [,Parameter `n`,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp index a45c2d5ee..d9d1d2f3c 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp +++ b/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; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 2712b7293..ee1914aaa 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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,,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, [,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_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_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,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, [,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, [,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] codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index dfc37d249..c12605152 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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, [,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, []