From 31ab607695f9266884c7d8605e3debb0159029c8 Mon Sep 17 00:00:00 2001 From: sjx Date: Fri, 3 Feb 2023 08:57:12 +0000 Subject: [PATCH 1/3] [inferbo] Fix an ignored case when the upper bounds of offset is +oo, and the upper bound of size is smaller than +oo Summary: The buffer overrun checker misses to handle the case when the upper bound of offset is +oo, and the upper bound of array size is less than +oo, which will causes false negative in some test cases. For instance, for the following program, ``` int a[1]; for(int i=0; a[i]; i++) {} ``` The variable `i` will eventually be equal 1 and causes an overrun error within the loop statement. However, this error was missed by buffer overrun checker. --- infer/src/bufferoverrun/bufferOverrunProofObligations.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index e37fb638e31..165653092e0 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -347,6 +347,10 @@ module ArrayAccessCondition = struct Bound.is_not_infty (ItvPure.ub real_idx) && Bound.le (ItvPure.ub size) (ItvPure.ub real_idx) then {report_issue_type= Issue IssueType.buffer_overrun_l2; propagate= false} (* symbolic il >= sl, probably an error *) + else if + Bound.is_infty (ItvPure.ub real_idx) && Bound.is_not_infty (ItvPure.ub size) + then {report_issue_type= Issue IssueType.buffer_overrun_l3; propagate= false} + (* su < iu = +oo, probably an error *) else if Bound.is_symbolic (ItvPure.lb real_idx) && Bound.le (ItvPure.lb size) (ItvPure.lb real_idx) then {report_issue_type= Issue IssueType.buffer_overrun_s2; propagate= true} From fd0a4e63db79d140e7e3ba91c1570ba055bcbd82 Mon Sep 17 00:00:00 2001 From: sjx Date: Mon, 6 Feb 2023 01:57:33 +0000 Subject: [PATCH 2/3] [inferbo] Make a more precise upper/lower bound when adding two upper/lower bounds --- infer/src/bufferoverrun/bounds.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index c91209d99f2..52090502a23 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -950,12 +950,12 @@ module Bound = struct let plus_l : weak:bool -> t -> t -> t = plus_exact ~otherwise:(fun x y -> match (x, y) with - | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2) - | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) -> - Linear (Z.(c1 + d1 + c2), x2) - | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2) - | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) -> - Linear (Z.(c1 - d1 + c2), x2) + | MinMax (c1, Plus, Max, d1, x1), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Plus, Max, d1, x1) -> + mk_MinMaxB (Max, (Linear (Z.(c1 + d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_one x1) x2))) + | MinMax (c1, Minus, Min, d1, x1), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Minus, Min, d1, x1) -> + mk_MinMaxB (Max, (Linear (Z.(c1 - d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_minus_one x1) x2))) | _, _ -> MInf ) @@ -963,12 +963,12 @@ module Bound = struct let plus_u : weak:bool -> t -> t -> t = plus_exact ~otherwise:(fun x y -> match (x, y) with - | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2) - | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) -> - Linear (Z.(c1 + d1 + c2), x2) - | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2) - | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) -> - Linear (Z.(c1 - d1 + c2), x2) + | MinMax (c1, Plus, Min, d1, x1), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Plus, Min, d1, x1) -> + mk_MinMaxB (Min, (Linear (Z.(c1 + d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_one x1) x2))) + | MinMax (c1, Minus, Max, d1, x1), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Minus, Max, d1, x1) -> + mk_MinMaxB (Min, (Linear (Z.(c1 - d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_minus_one x1) x2))) | _, _ -> PInf ) From 347d391252a06ed91653083f209964c981310cd1 Mon Sep 17 00:00:00 2001 From: jiaxin song Date: Fri, 24 Feb 2023 10:43:41 +0800 Subject: [PATCH 3/3] [inferbo] Initialize locations for arrays within struct typed variables --- infer/src/bufferoverrun/bufferOverrunUtils.ml | 26 ++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index fbee9e3b930..484a13314d4 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -16,6 +16,7 @@ module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace module TraceSet = Trace.Set module TypModels = BufferOverrunTypModels +module BoField = BufferOverrunField module ModelEnv = struct type model_env = @@ -52,7 +53,23 @@ module Exec = struct mem - let rec decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values + let rec decl_local_struct_fields_loc: ModelEnv.model_env -> Loc.t -> Struct.fields -> Dom.Mem.t * int -> Dom.Mem.t * int = + fun model_env loc fields (mem, inst_num) -> + match fields with + | field :: tl -> ( + match field with + | (fn, typ, _) -> ( + match typ.desc with + | Tarray {elt= _; length; stride} -> + let child_loc = BoField.Field {prefix= loc; fn; typ = (Some typ)} in + let stride = Option.map ~f:IntLit.to_int_exn stride in + let (mem, inst_num) = decl_local_array model_env child_loc typ ~length ?stride ~inst_num + ~represents_multiple_values:false ~dimension:1 mem + in + decl_local_struct_fields_loc model_env loc tl (mem, inst_num) + | _ -> decl_local_struct_fields_loc model_env loc tl (mem, inst_num))) + | [] -> (mem, inst_num) + and decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values ~dimension mem = match typ.Typ.desc with | Typ.Tarray {elt= typ; length; stride} -> @@ -60,6 +77,13 @@ module Exec = struct decl_local_array model_env loc typ ~length ?stride ~inst_num ~represents_multiple_values ~dimension mem | Typ.Tstruct typname -> ( + let mem = ( + match Tenv.lookup tenv typname with + | Some {fields} -> + let (mem, _) = decl_local_struct_fields_loc model_env loc fields (mem, 1) in mem + | None -> mem + ) + in match TypModels.dispatch tenv typname with | Some (CArray {element_typ; length}) -> decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num