[inferbo] Prune more for "(x + e1) < e2" cases

Reviewed By: mbouaziz

Differential Revision: D13095472

fbshipit-source-id: 21aef560a

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.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as c), e1, e2)
-    | Exp.BinOp ((Binop.Gt as c), e', Exp.Var x)
+      ->
-    | Exp.BinOp ((Binop.Le as c), e', Exp.Var x)
+        prune_binop_left (Exp.BinOp (comp_rev c, e2, e1)) astate
-    | 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
     | _ ->
         astate
 

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]

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); }

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 + 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 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, 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 + 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 + 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 + 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 + 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 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 + 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 + 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 + 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 + 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]