From e912bf2aa58aacf176d5fa659219050abad245bc Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 16 Nov 2018 23:20:49 -0800 Subject: [PATCH] [inferbo] Prune more for "(x + e1) < e2" cases Reviewed By: mbouaziz Differential Revision: D13095472 fbshipit-source-id: 21aef560a --- .../bufferoverrun/bufferOverrunSemantics.ml | 29 +++++++---- .../codetoanalyze/c/bufferoverrun/issues.exp | 2 + .../c/bufferoverrun/prune_constant.c | 48 +++++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 14 +++--- 4 files changed, 78 insertions(+), 15 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 773379b46..3b2f5fbd9 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -405,7 +405,7 @@ module Prune = struct astate - let prune_binop_left : Exp.t -> astate -> astate = + let rec prune_binop_left : Exp.t -> astate -> astate = fun e ({mem} as astate) -> match e with | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e') @@ -435,6 +435,23 @@ module Prune = struct update_mem_in_prune lv v' astate | None -> astate ) + | Exp.BinOp + ( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp) + , Exp.BinOp (Binop.PlusA t, e1, e2) + , e3 ) -> + (* NOTE: The transposition may introduce a new integer overflow or hide an existing one. + Be careful when you take into account integer overflows in the abstract semantics [eval] + in the future. *) + astate + |> prune_binop_left (Exp.BinOp (comp, e1, Exp.BinOp (Binop.MinusA t, e3, e2))) + |> prune_binop_left (Exp.BinOp (comp, e2, Exp.BinOp (Binop.MinusA t, e3, e1))) + | Exp.BinOp + ( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp) + , Exp.BinOp (Binop.MinusA t, e1, e2) + , e3 ) -> + astate + |> prune_binop_left (Exp.BinOp (comp, e1, Exp.BinOp (Binop.PlusA t, e3, e2))) + |> prune_binop_left (Exp.BinOp (comp_rev comp, e2, Exp.BinOp (Binop.MinusA t, e1, e3))) | _ -> astate @@ -442,13 +459,9 @@ module Prune = struct let prune_binop_right : Exp.t -> astate -> astate = fun e astate -> match e with - | Exp.BinOp ((Binop.Lt as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Gt as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Le as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Ge as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Eq as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Ne as c), e', Exp.Var x) -> - prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) astate + | Exp.BinOp (((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as c), e1, e2) + -> + prune_binop_left (Exp.BinOp (comp_rev c, e2, e1)) astate | _ -> astate diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 53a5b9a50..377bc163f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -180,6 +180,8 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALW codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 Size: 10 by call to `prune_add2` ] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 Size: 10 by call to `prune_sub2` ] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index 0888fcffc..9dbf7d8d0 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -80,3 +80,51 @@ void call_fromHex2_200_Good_FP() { int idx = fromHex(200); arr[idx + 1] = 'H'; } + +void prune_add1(unsigned int x) { + int a[10]; + if (x + 1 < 11) { + a[x] = 0; + } +} + +void call_prune_add1_1_Good() { prune_add1(5); } + +void call_prune_add1_2_Good() { prune_add1(10); } + +void prune_add2(unsigned int x) { + int a[10]; + if (x + 1 < 12) { + a[x] = 0; + } +} + +void call_prune_add2_1_Good() { prune_add2(5); } + +void call_prune_add2_2_Bad() { prune_add2(10); } + +void call_prune_add2_3_Good() { prune_add2(100); } + +void prune_sub1(unsigned int x) { + int a[10]; + if (9 > x - 1) { + a[x] = 0; + } +} + +void call_prune_sub1_1_Good() { prune_sub1(5); } + +void call_prune_sub1_2_Good() { prune_sub1(10); } + +void prune_sub2(unsigned int x) { + int a[10]; + if (10 > x - 1) { + a[x] = 0; + } +} + +void call_prune_sub2_1_Good() { prune_sub2(5); } + +void call_prune_sub2_2_Bad() { prune_sub2(10); } + +void call_prune_sub2_3_Good() { prune_sub2(100); } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 06bf1158b..94e7ca5a0 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -41,10 +41,10 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_it codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p.ub, degree = 1] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 ⋅ p.ub, degree = 1] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p.ub, degree = 1] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 8 ⋅ maxI.ub × maxJ.ub + 5 ⋅ maxI.ub × (1+max(0, maxJ.ub)), degree = 2] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ maxI.ub + 8 ⋅ maxI.ub × maxJ.ub + 5 ⋅ maxI.ub × (1+max(0, maxJ.ub)), degree = 2] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 8 ⋅ maxI.ub × maxJ.ub + 5 ⋅ maxI.ub × (1+max(0, maxJ.ub)), degree = 2] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 8 ⋅ maxI.ub × maxJ.ub + 5 ⋅ maxI.ub × (1+max(0, maxJ.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] @@ -111,9 +111,9 @@ codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length.ub + 4 ⋅ (items.length.ub + 1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ items.length.ub + 4 ⋅ (items.length.ub + 1), degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 36 ⋅ (size.ub + 5) + 3 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2] -codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 36 ⋅ (size.ub + 5) + 3 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2] -codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 36 ⋅ (size.ub + 5) + 3 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2] +codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2] +codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2] +codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ (size.ub + 20), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ (size.ub + 20), degree = 1] codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]