From 8ea92c51e04cb8c0105062627456e88edb027d2a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 19 Feb 2019 01:51:19 -0800 Subject: [PATCH] [inferbo] Suppress ALLOC_IS_ZERO for C++'s array object Reviewed By: mbouaziz Differential Revision: D14122889 fbshipit-source-id: d0c99a5e6 --- .../src/bufferoverrun/bufferOverrunModels.ml | 30 +++---- .../bufferOverrunProofObligations.ml | 88 +++++++++++-------- .../bufferOverrunProofObligations.mli | 1 + .../cpp/bufferoverrun/issues.exp | 1 + .../cpp/bufferoverrun/std_array.cpp | 4 + .../java/bufferoverrun/Array.java | 2 +- .../java/bufferoverrun/issues.exp | 1 - 7 files changed, 72 insertions(+), 55 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index b4b818f3e..f65cd5707 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -52,7 +52,7 @@ let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = fun (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None) -let check_alloc_size size_exp {location; integer_type_widths} mem cond_set = +let check_alloc_size ~can_be_zero size_exp {location; integer_type_widths} mem cond_set = let _, _, length0, _ = get_malloc_info size_exp in let v_length = Sem.eval integer_type_widths length0 mem in match Dom.Val.get_itv v_length with @@ -61,7 +61,7 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set = | NonBottom length -> let traces = Dom.Val.get_traces v_length in let latest_prune = Dom.Mem.get_latest_prune mem in - PO.ConditionSet.add_alloc_size location ~length traces latest_prune cond_set + PO.ConditionSet.add_alloc_size location ~can_be_zero ~length traces latest_prune cond_set let fgets str_exp num_exp = @@ -90,7 +90,7 @@ let fgets str_exp num_exp = {exec; check} -let malloc size_exp = +let malloc ~can_be_zero size_exp = let exec ({pname; node_hash; location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in @@ -114,7 +114,7 @@ let malloc size_exp = |> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size ~size_exp_opt |> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length - and check = check_alloc_size size_exp in + and check = check_alloc_size ~can_be_zero size_exp in {exec; check} @@ -243,17 +243,17 @@ let realloc src_exp size_exp = Option.value_map dyn_length ~default:mem ~f:(fun dyn_length -> let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in BoUtils.Exec.set_dyn_length model_env typ (Dom.Val.get_array_locs v) dyn_length mem ) - and check = check_alloc_size size_exp in + and check = check_alloc_size ~can_be_zero:false size_exp in {exec; check} let placement_new size_exp (src_exp1, t1) src_arg2_opt = match (t1.Typ.desc, src_arg2_opt) with | Tint _, None | Tint _, Some (_, {Typ.desc= Tint _}) -> - malloc (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1)) + malloc ~can_be_zero:true (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1)) | Tstruct (CppClass (name, _)), None when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] -> - malloc size_exp + malloc ~can_be_zero:true size_exp | _, _ -> let exec {integer_type_widths} ~ret:(id, _) mem = let src_exp = @@ -317,7 +317,7 @@ let inferbo_set_size e1 e2 = let locs = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_pow_loc in let length = Sem.eval integer_type_widths e2 mem in Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length) locs mem - and check = check_alloc_size e2 in + and check = check_alloc_size ~can_be_zero:true e2 in {exec; check} @@ -402,7 +402,7 @@ let set_array_length array length_exp = Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem | _ -> L.(die InternalError) "Unexpected type of first argument for __set_array_length() " - and check = check_alloc_size length_exp in + and check = check_alloc_size ~can_be_zero:false length_exp in {exec; check} @@ -503,7 +503,7 @@ end module StdBasicString = struct (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) let constructor_from_char_ptr tgt src len = - let {exec= malloc_exec; check= malloc_check} = malloc len in + let {exec= malloc_exec; check= malloc_check} = malloc ~can_be_zero:true len in let exec model_env ~ret:((ret_id, _) as ret) mem = let mem = malloc_exec model_env ~ret mem in let v = Dom.Mem.find (Loc.of_id ret_id) mem in @@ -653,7 +653,7 @@ module Collection = struct let exec {integer_type_widths} ~ret:_ mem = let itr = Sem.eval integer_type_widths rhs_exp mem in model_by_value itr lhs_id mem - and check = check_alloc_size rhs_exp in + and check = check_alloc_size ~can_be_zero:true rhs_exp in {exec; check} @@ -730,13 +730,13 @@ module Call = struct ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 ; -"fgets" <>$ capt_exp $+ capt_exp $+...$--> fgets ; -"infer_print" <>$ capt_exp $!--> infer_print - ; -"malloc" <>$ capt_exp $+...$--> malloc - ; -"calloc" <>$ capt_exp $+ capt_exp $!--> calloc + ; -"malloc" <>$ capt_exp $+...$--> malloc ~can_be_zero:false + ; -"calloc" <>$ capt_exp $+ capt_exp $!--> calloc ~can_be_zero:false ; -"__new" <>$ capt_exp_of_typ (+PatternMatch.implements_collection) $+...$--> Collection.new_collection - ; -"__new" <>$ capt_exp $+...$--> malloc - ; -"__new_array" <>$ capt_exp $+...$--> malloc + ; -"__new" <>$ capt_exp $+...$--> malloc ~can_be_zero:true + ; -"__new_array" <>$ capt_exp $+...$--> malloc ~can_be_zero:true ; -"__placement_new" <>$ capt_exp $+ capt_arg $+? capt_arg $!--> placement_new ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc ; -"__get_array_length" <>$ capt_exp $!--> get_array_length diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 9c5965f8e..1f13381b5 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -103,55 +103,62 @@ type report_issue_type = NotIssue | Issue of IssueType.t | SymbolicIssue type checked_condition = {report_issue_type: report_issue_type; propagate: bool} module AllocSizeCondition = struct - type t = ItvPure.t [@@deriving compare] + type t = {length: ItvPure.t; can_be_zero: bool} [@@deriving compare] - let get_symbols = ItvPure.get_symbols + let get_symbols {length} = ItvPure.get_symbols length - let pp fmt length = F.fprintf fmt "alloc(%a)" ItvPure.pp length + let pp fmt {length} = F.fprintf fmt "alloc(%a)" ItvPure.pp length - let pp_description ~markup fmt length = + let pp_description ~markup fmt {length} = F.fprintf fmt "Length: %a" (ItvPure.pp_mark ~markup) length - let make ~length = if ItvPure.is_invalid length then None else Some length + let make ~can_be_zero ~length = + if ItvPure.is_invalid length then None else Some {length; can_be_zero} + + + let have_similar_bounds x y = + ItvPure.have_similar_bounds x.length y.length && Bool.equal x.can_be_zero y.can_be_zero - let have_similar_bounds = ItvPure.have_similar_bounds let xcompare ~lhs ~rhs = - match ItvPure.xcompare ~lhs ~rhs with - | `Equal -> - `Equal - | `NotComparable -> - `NotComparable - | `LeftSubsumesRight -> - `LeftSubsumesRight - | `RightSubsumesLeft -> - `RightSubsumesLeft - | (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp -> - let lpos = ItvPure.le_sem ItvPure.zero lhs in - let rpos = ItvPure.le_sem ItvPure.zero rhs in - if not (Boolean.equal lpos rpos) then `NotComparable - else if Boolean.is_true lpos then - match cmp with - | `LeftSmallerThanRight -> - `RightSubsumesLeft - | `RightSmallerThanLeft -> - `LeftSubsumesRight - else if Boolean.is_false lpos then - match cmp with - | `LeftSmallerThanRight -> - `LeftSubsumesRight - | `RightSmallerThanLeft -> - `RightSubsumesLeft - else `NotComparable + if Bool.equal lhs.can_be_zero rhs.can_be_zero then + match ItvPure.xcompare ~lhs:lhs.length ~rhs:rhs.length with + | `Equal -> + `Equal + | `NotComparable -> + `NotComparable + | `LeftSubsumesRight -> + `LeftSubsumesRight + | `RightSubsumesLeft -> + `RightSubsumesLeft + | (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp -> + let lpos = ItvPure.le_sem ItvPure.zero lhs.length in + let rpos = ItvPure.le_sem ItvPure.zero rhs.length in + if not (Boolean.equal lpos rpos) then `NotComparable + else if Boolean.is_true lpos then + match cmp with + | `LeftSmallerThanRight -> + `RightSubsumesLeft + | `RightSmallerThanLeft -> + `LeftSubsumesRight + else if Boolean.is_false lpos then + match cmp with + | `LeftSmallerThanRight -> + `LeftSubsumesRight + | `RightSmallerThanLeft -> + `RightSubsumesLeft + else `NotComparable + else `NotComparable let itv_big = ItvPure.of_int 1_000_000 - let check length = + let check {length; can_be_zero} = match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with | `Equal | `RightSubsumesLeft -> - {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false} + if can_be_zero then {report_issue_type= NotIssue; propagate= false} + else {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false} | `LeftSmallerThanRight -> {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false} | _ -> ( @@ -181,8 +188,12 @@ module AllocSizeCondition = struct else {report_issue_type= NotIssue; propagate} ) ) - let subst eval_sym length = - match ItvPure.subst length eval_sym with NonBottom length -> Some length | Bottom -> None + let subst eval_sym {length; can_be_zero} = + match ItvPure.subst length eval_sym with + | NonBottom length -> + Some {length; can_be_zero} + | Bottom -> + None end module ArrayAccessCondition = struct @@ -908,8 +919,9 @@ module ConditionSet = struct latest_prune condset - let add_alloc_size location ~length val_traces latest_prune condset = - AllocSizeCondition.make ~length |> Condition.make_alloc_size + let add_alloc_size location ~can_be_zero ~length val_traces latest_prune condset = + AllocSizeCondition.make ~can_be_zero ~length + |> Condition.make_alloc_size |> add_opt location (ValTrace.Issue.alloc location val_traces) latest_prune condset diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 97c022d27..a99f2eaad 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -50,6 +50,7 @@ module ConditionSet : sig val add_alloc_size : Location.t + -> can_be_zero:bool -> length:ItvPure.t -> BufferOverrunTrace.Set.t -> BufferOverrunDomain.LatestPrune.t diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index b55f25ef7..24ee3be17 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -83,6 +83,7 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_back_Bad, 3, BUFFER_OV codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_front_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 11] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, malloc_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp index 357a5a7f9..6ff28311e 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp @@ -137,3 +137,7 @@ void array_rev_iter_Bad() { } a[a[0]] = 0; } + +void malloc_zero_Bad() { int* a = (int*)malloc(sizeof(int) * 0); } + +void new_array_zero_Good() { int* a = new int[0]; } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java index 838272db8..971a0fe6b 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java @@ -61,7 +61,7 @@ class Array { a = new ArrayList<>(-1); } - void zero_alloc_Good_FP() { + void zero_alloc_Good() { a = new ArrayList<>(0); } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 00dfb85fb..83da763af 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -5,6 +5,5 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] -codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.zero_alloc_Good_FP():void, 1, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Assignment,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]