From 4e166f3375413842d2dfb0a8082ada8d2e2f22bc Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 28 Nov 2018 23:35:43 -0800 Subject: [PATCH] [inferbo] Instantiate symbolic locations in function parameters Summary: It instantiates not only symbols for bound but also symbols for locations at function calls. Reviewed By: mbouaziz Differential Revision: D13231291 fbshipit-source-id: ce23a943b --- infer/src/bufferoverrun/absLoc.ml | 21 +++++++++++++++ infer/src/bufferoverrun/arrayBlk.ml | 15 +++++++++-- .../src/bufferoverrun/bufferOverrunDomain.ml | 8 ++++-- .../bufferoverrun/bufferOverrunSemantics.ml | 27 ++++++++++++------- .../codetoanalyze/c/bufferoverrun/issues.exp | 4 ++- .../codetoanalyze/cpp/bufferoverrun/class.cpp | 2 +- .../cpp/bufferoverrun/issues.exp | 3 +-- 7 files changed, 62 insertions(+), 18 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 80c56e44b..26143d980 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -70,6 +70,8 @@ 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 @@ -138,6 +140,15 @@ 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 @@ -163,6 +174,16 @@ module PowLoc = struct type eval_locpath = Symb.SymbolPath.partial -> t + + 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 end (** unsound but ok for bug catching *) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 325c51506..19c0e7350 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -153,8 +153,19 @@ let get_pow_loc : t -> PowLoc.t = fold pow_loc_of_allocsite array PowLoc.bot -let subst : t -> Bound.eval_sym -> t = - fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a +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 get_symbols : t -> Itv.SymbolSet.t = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 9cd33b628..272cb1f30 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -317,7 +317,7 @@ module Val = struct let subst : t -> eval_sym_trace -> Location.t -> t = - fun x {eval_sym; trace_of_sym} location -> + fun x {eval_sym; trace_of_sym; eval_locpath} location -> let symbols = get_symbols x in let traces_caller = Itv.SymbolSet.fold @@ -325,7 +325,11 @@ 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; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces} + { 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 } (* normalize bottom *) |> normalize diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index ee21aa97a..ecbce1f21 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -333,16 +333,23 @@ let rec eval_sympath_partial params p mem = and eval_locpath params p mem = - 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 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 let eval_sympath params sympath mem = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 8ee67fec1..f8d07ba78 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -3,7 +3,9 @@ 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, 102] - 87):unsigned64 by call to `scan_hex_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __variable_initialization,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, [Unknown value from: __variable_initialization,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_U5, no_bucket, ERROR, [Unknown value from: __variable_initialization,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 d9d1d2f3c..a95bdd108 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_FP() { + void set_x_two_Good() { int arr[5]; *x = 0; dummy_function(); diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 8c237d842..e71e41a70 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -20,8 +20,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, 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_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_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] codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]