From 4c0aa1f69d0632fb7b380049956689460366284c Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 29 Mar 2019 06:07:31 -0700 Subject: [PATCH] [inferbo] Revise substitution of array block Summary: Given a pointer-typed parameter, Inferbo assumes that it is an array block. However, when a pointer is given as an actual parameter, it failed the substitution of the array block value of the parameter, thus which made some return values to bottom unexpectedly. This diff revises the substitution of array block, so it can substitute array block values with actual pointers correctly when it is possible. Reviewed By: mbouaziz Differential Revision: D14663475 fbshipit-source-id: 0477de1ba --- infer/src/bufferoverrun/arrayBlk.ml | 34 +++++++++++++++---- .../src/bufferoverrun/bufferOverrunDomain.ml | 6 ++-- infer/src/bufferoverrun/itv.ml | 4 +++ infer/src/bufferoverrun/itv.mli | 4 +++ .../c/bufferoverrun/function_call.c | 20 +++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 ++ 6 files changed, 62 insertions(+), 8 deletions(-) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 005555449..3f9714fbb 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -133,6 +133,17 @@ module ArrInfo = struct AbstractDomain.TopLiftedUtils.pp_top f + let is_pointer : Symb.SymbolPath.partial -> t -> bool = + fun path arr -> + match (path, arr) with + | Deref ((Deref_COneValuePointer | Deref_CPointer), path), C {offset; size} -> + Itv.is_offset_path_of path offset && Itv.is_length_path_of path size + | Deref (Deref_JavaPointer, path), Java {length} -> + Itv.is_length_path_of path length + | _, _ -> + false + + let is_symbolic : t -> bool = fun arr -> match arr with @@ -309,19 +320,30 @@ 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 -> PowLoc.eval_locpath -> PowLoc.t * t = fun a eval_sym eval_locpath -> - let subst1 l info acc = + let subst1 l info (powloc_acc, acc) = let info' = ArrInfo.subst info eval_sym in match Allocsite.get_param_path l with | None -> - add l info' acc + (powloc_acc, 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 + let add_allocsite l (powloc_acc, acc) = + match l with + | Loc.Allocsite a -> + (powloc_acc, add a info' acc) + | _ -> + if ArrInfo.is_pointer path info then (PowLoc.add l powloc_acc, acc) + else ( + if Config.bo_debug >= 3 then + L.d_printfln_escaped "Substitution of array block failed: %a -> %a" Loc.pp l + ArrInfo.pp info ; + (powloc_acc, acc) ) + in + PowLoc.fold add_allocsite locs (powloc_acc, acc) in - fold subst1 a empty + fold subst1 a (PowLoc.empty, empty) let is_symbolic : t -> bool = fun a -> exists (fun _ ai -> ArrInfo.is_symbolic ai) a diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b10f8965e..59d0959b9 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -398,10 +398,12 @@ module Val = struct symbols TraceSet.bottom in let traces = TraceSet.call location ~traces_caller ~traces_callee:x.traces in + let powloc = PowLoc.subst x.powloc eval_locpath in + let powloc_from_arrayblk, arrayblk = ArrayBlk.subst x.arrayblk eval_sym eval_locpath 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 + ; powloc= PowLoc.join powloc powloc_from_arrayblk + ; arrayblk ; traces } (* normalize bottom *) |> normalize diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 57f398d1c..67b07ec97 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -657,3 +657,7 @@ let of_normal_path ~unsigned path = NonBottom (ItvPure.of_normal_path ~unsigned let of_offset_path path = NonBottom (ItvPure.of_offset_path path) let of_length_path path = NonBottom (ItvPure.of_length_path path) + +let is_offset_path_of path x = eq (of_offset_path path) x + +let is_length_path_of path x = eq (of_length_path path) x diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 8b65757a8..263fa97be 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -234,3 +234,7 @@ val of_normal_path : unsigned:bool -> Symb.SymbolPath.partial -> t val of_offset_path : Symb.SymbolPath.partial -> t val of_length_path : Symb.SymbolPath.partial -> t + +val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool + +val is_length_path_of : Symb.SymbolPath.partial -> t -> bool diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c index 384798f3b..63dd1cffa 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c @@ -160,3 +160,23 @@ void call_va_arg_int_Bad() { int a[10]; va_arg_int(a, 10); } + +struct S* id_S(struct S* r) { + return r; +} + +void call_id_S_Good_FP(struct S p) { + int a[10]; + struct S* q = id_S(&p); + if (q == 0) { + a[10] = 0; // should be unreachable + } +} + +void call_id_S_Bad(struct S p) { + int a[10]; + struct S* q = id_S(&p); + if (q != 0) { + a[10] = 0; // should be reachable + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 3fb18e1e4..2e5a57d4b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -115,6 +115,8 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_call_access_index_4_on_S3_Ba codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/function_call.c, call_id_S_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/function_call.c, call_id_S_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_va_arg_int_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Array declaration,Call,,Unknown value from: __builtin_va_arg,Assignment,,Parameter `*a`,Array access: Offset: [-oo, +oo] Size: 10 by call to `va_arg_int` ] codetoanalyze/c/bufferoverrun/function_call.c, call_va_arg_int_Good_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Array declaration,Call,,Unknown value from: __builtin_va_arg,Assignment,,Parameter `*a`,Array access: Offset: [-oo, +oo] Size: 10 by call to `va_arg_int` ] codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*arr`,Assignment,,Parameter `*arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]