From b2189c1c170f29028b4b7a6598ccbb3a388d6630 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 2 Nov 2018 09:16:41 -0700 Subject: [PATCH] [inferbo] Loosen similar bounds condition Summary: For more deduplications of issues, this diff loosens the condition of similar bounds. The previous condition of similar bounds was too strict, so [0,0] and [0,+oo] were not similar. Depends on D10851762 Reviewed By: mbouaziz Differential Revision: D10866127 fbshipit-source-id: 4ba912a88 --- infer/src/bufferoverrun/bounds.ml | 12 +----------- .../codetoanalyze/c/bufferoverrun/issue_kinds.c | 12 ++++++++++++ infer/tests/codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../tests/codetoanalyze/java/performance/issues.exp | 1 - 4 files changed, 14 insertions(+), 12 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 92f2747d2..aa49f65ae 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -782,17 +782,7 @@ module Bound = struct Symb.SymbolSet.singleton s - let are_similar b1 b2 = - match (b1, b2) with - | MInf, MInf -> - true - | PInf, PInf -> - true - | (Linear _ | MinMax _), (Linear _ | MinMax _) -> - true - | _ -> - false - + let are_similar b1 b2 = Symb.SymbolSet.equal (get_symbols b1) (get_symbols b2) let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index 6d8d40f26..d7a410489 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -262,3 +262,15 @@ void two_safety_conditions(int n) { } void call_two_safety_conditions_l1_and_l2_Bad() { two_safety_conditions(10); } + +/* issue1 and issue2 are deduplicated since the offset of issue2 + ([10,+oo]) subsumes that of issue1 ([10,10]). */ +void deduplicate_issues_Bad() { + int a[10]; + int x = 10; + a[x] = 0; // issue1: [10,10] < [10,10] + x = unknown_function(); + if (x >= 10) { + a[x] = 0; // issue2: [10,+oo] < [10,10] + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 006f4c580..cdcab09b5 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -87,6 +87,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Ba codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Binop: (100000000 + [0, +oo]):signed32 by call to `alloc_may_be_big2_Silenced` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 10 Size: 10 by call to `two_safety_conditions` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ] +codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: [10, +oo] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Assignment,Binop: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 3fa9ddb15..43f61b927 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -126,7 +126,6 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils. codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] (= [-oo, +oo] + [0, +oo]) Size: [0, +oo]] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []