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` ]