From a1a3c551865edd5b3f75ac9e304dae5bc37a5abc Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 26 Mar 2020 05:20:28 -0700 Subject: [PATCH] [inferbo] Fix a bug in interval prune Summary: This diff avoids that an invalid interval value, e.g. [0, -1], is genrated by interval pruning. Reviewed By: ezgicicek Differential Revision: D20645488 fbshipit-source-id: 6516c75d1 --- infer/src/bufferoverrun/itv.ml | 49 +++++++++---------- .../java/bufferoverrun/ArrayListTest.java | 15 +++--- .../java/bufferoverrun/issues.exp | 6 +-- 3 files changed, 36 insertions(+), 34 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 48bfdab8e..a09aa9e5e 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -459,18 +459,22 @@ module ItvPure = struct let arith_unop (unop : Unop.t) x = match unop with Neg -> Some (neg x) | BNot | LNot -> None - let prune_le : t -> t -> t = fun (l1, u1) (_, u2) -> (l1, Bound.overapprox_min u1 u2) + let prune_le : t -> t -> t bottom_lifted = + fun (l1, u1) (_, u2) -> normalize (l1, Bound.overapprox_min u1 u2) - let prune_ge : t -> t -> t = fun (l1, u1) (l2, _) -> (Bound.underapprox_max l1 l2, u1) - let prune_lt : t -> t -> t = fun x y -> prune_le x (minus y one) + let prune_ge : t -> t -> t bottom_lifted = + fun (l1, u1) (l2, _) -> normalize (Bound.underapprox_max l1 l2, u1) - let prune_gt : t -> t -> t = fun x y -> prune_ge x (plus y one) + + let prune_lt : t -> t -> t bottom_lifted = fun x y -> prune_le x (minus y one) + + let prune_gt : t -> t -> t bottom_lifted = fun x y -> prune_ge x (plus y one) let prune_diff : t -> Bound.t -> t bottom_lifted = fun ((l, u) as itv) b -> - if Bound.le b l then normalize (prune_gt itv (of_bound b)) - else if Bound.le u b then normalize (prune_lt itv (of_bound b)) + if Bound.le b l then prune_gt itv (of_bound b) + else if Bound.le u b then prune_lt itv (of_bound b) else NonBottom itv @@ -480,20 +484,17 @@ module ItvPure = struct fun c x y -> if is_invalid y then NonBottom x else - let x = - match c with - | Le -> - prune_le x y - | Ge -> - prune_ge x y - | Lt -> - prune_lt x y - | Gt -> - prune_gt x y - | _ -> - assert false - in - normalize x + match c with + | Le -> + prune_le x y + | Ge -> + prune_ge x y + | Lt -> + prune_lt x y + | Gt -> + prune_gt x y + | _ -> + assert false let prune_eq : t -> t -> t bottom_lifted = @@ -502,9 +503,7 @@ module ItvPure = struct let prune_eq_zero : t -> t bottom_lifted = - fun x -> - let x' = prune_le x zero in - prune_ge x' zero |> normalize + fun x -> match prune_le x zero with Bottom -> Bottom | NonBottom x' -> prune_ge x' zero let prune_ne : t -> t -> t bottom_lifted = @@ -787,9 +786,9 @@ let prune_ge_one : t -> t = bind1 ItvPure.prune_ge_one let prune_binop : Binop.t -> t -> t -> t = fun comp -> bind2 (ItvPure.prune_binop comp) -let prune_lt : t -> t -> t = lift2 ItvPure.prune_lt +let prune_lt : t -> t -> t = bind2 ItvPure.prune_lt -let prune_le : t -> t -> t = lift2 ItvPure.prune_le +let prune_le : t -> t -> t = bind2 ItvPure.prune_le let prune_eq : t -> t -> t = bind2 ItvPure.prune_eq diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java index 954aa2ba5..c99acf30e 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java @@ -251,7 +251,7 @@ class ArrayListTest { ArrayList unknown_array_list1; ArrayList unknown_array_list2; - void loop_on_unknown_iterator_FN(MyI x, int j) { + void loop_on_unknown_iterator(MyI x, int j) { ArrayList a = new ArrayList<>(); ArrayList b; if (unknown_bool) { @@ -259,16 +259,19 @@ class ArrayListTest { } else { b = x.mk_unknown(); } - // `b` points to an zero-sized array and `Unknown` pointer here. By `b.hasNext()`, the size of - // the array list is pruned incorrectly to [0,-1]. + // `b` points to an zero-sized array and `Unknown` pointer. Thus, the size of array list should + // be evaluated to [0,+oo] in a sound design. However, this would harm overall analysis + // precision with introducing a lot of FPs. To avoie that, we ignore the size of `Unknown` + // array list here, instead we get some FNs. for (Integer i : b) { - // Both branches are unreachable since `a.size()` is an invalid [0,-1]. + // `a.size()` is evaluated to bottom, rather than [0,+oo] here, but which does not make + // branches unreachable. if (a.size() <= -1) { int[] c = new int[5]; c[5] = 0; } else { - int[] c = new int[5]; - c[5] = 0; + int[] c = new int[10]; + c[10] = 0; } } } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index bb77f1b74..057f62ff6 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -20,9 +20,9 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_i codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 10, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 11, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: [0, 2]] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] -codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 9, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: ArrayList ArrayListTest$MyI.mk_unknown(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 11, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: ArrayList ArrayListTest$MyI.mk_unknown(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 16, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 5 Size: 5] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 19, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.multi_adds_in_loop_iterator_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Array declaration,Array access: Offset: b.length + 1 Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 13, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]