From 22c0520b4683749898407c09bdcaf7cf1e5557c6 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 4 Oct 2017 03:03:07 -0700 Subject: [PATCH] [inferbo] Do not report duplicate issues Summary: Merge safety conditions that are exactly the same, keep the earliest location. Reviewed By: jvillard Differential Revision: D5953981 fbshipit-source-id: 874eee1 --- .../bufferOverrunProofObligations.ml | 32 ++++++++++++++++++- infer/src/bufferoverrun/itv.ml | 2 ++ .../codetoanalyze/c/bufferoverrun/issues.exp | 3 -- .../cpp/bufferoverrun/issues.exp | 2 -- 4 files changed, 33 insertions(+), 6 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index a026b42d6..f0b369902 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -20,6 +20,8 @@ module Condition = struct let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size + let eq c1 c2 = ItvPure.equal c1.idx c2.idx && ItvPure.equal c1.size c2.size + let set_size_pos : t -> t = fun c -> let size' = ItvPure.make_positive c.size in @@ -162,9 +164,37 @@ module ConditionSet = struct type t = condition_with_trace list + (* invariant: add_one of one of the elements should return the original list *) + let empty = [] - let join condset1 condset2 = condset1 @ condset2 + let compare_by_location cwt1 cwt2 = + Location.compare (ConditionTrace.get_location cwt1.trace) + (ConditionTrace.get_location cwt2.trace) + + let try_merge ~existing ~new_ = + if Condition.eq existing.cond new_.cond then + (* keep the first one in the code *) + if compare_by_location existing new_ <= 0 then `KeepExistingAndStop + else `RemoveExistingAddNewAndStop + else `KeepGoingFinallyAddNew + + let add_one condset new_ = + let rec aux ~new_ acc = function + | [] + -> new_ :: condset + | existing :: rest -> + match try_merge ~existing ~new_ with + | `KeepExistingAndStop + -> condset + | `RemoveExistingAddNewAndStop + -> new_ :: List.rev_append acc rest + | `KeepGoingFinallyAddNew + -> aux ~new_ (existing :: acc) rest + in + aux ~new_ [] condset + + let join condset1 condset2 = List.fold_left ~f:add_one condset1 ~init:condset2 let add_bo_safety pname loc id ~idx ~size val_traces condset = match Condition.make ~idx ~size with diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index bee8ddba6..12209a23c 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -633,6 +633,8 @@ module ItvPure = struct type t = astate + let equal = [%compare.equal : astate] + let initial : t = (Bound.initial, Bound.initial) let lb : t -> Bound.t = fst diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 1fb5af523..15844b2ac 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -6,13 +6,10 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [4, 4] Size: [4, 4]] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,Call,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] -codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,Call,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN, [ArrayDeclaration,Call,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:11:7 by call `two_accesses()` ] -codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN, [ArrayDeclaration,Call,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:12:5 by call `two_accesses()` ] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 7, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [20, 20] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 8, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]] codetoanalyze/c/bufferoverrun/for_loop.c, safealloc, 10, UNREACHABLE_CODE, [] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index a1482cda2..df86a4104 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -3,7 +3,6 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRU codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [20, 20] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, [] @@ -17,7 +16,6 @@ codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [ArrayD codetoanalyze/cpp/bufferoverrun/vector.cpp, call_safe_access4_Good_FP, 2, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Call,Assignment,Return,Call,Assignment,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13]] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]]