From 2824056af58f9952898f141cb010fbd6a4021136 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 26 Oct 2018 06:14:12 -0700 Subject: [PATCH] [inferbo] Normalize intervals after substitution Summary: Gets rid of impossible cases Reviewed By: jvillard Differential Revision: D10487811 fbshipit-source-id: b2966131a --- infer/src/bufferoverrun/itv.ml | 18 ++++----- .../codetoanalyze/c/bufferoverrun/arith.c | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 3 +- .../c/bufferoverrun/prune_alias.c | 39 ++++++++++++++++++- 4 files changed, 49 insertions(+), 13 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index e28b19ed6..08fbf7934 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -454,15 +454,6 @@ module ItvPure = struct let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false - let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted = - fun (l, u) eval_sym -> - match (Bound.subst_lb l eval_sym, Bound.subst_ub u eval_sym) with - | NonBottom l, NonBottom u -> - NonBottom (l, u) - | _ -> - Bottom - - let ( <= ) : lhs:t -> rhs:t -> bool = fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2 @@ -740,6 +731,15 @@ module ItvPure = struct let normalize : t -> t bottom_lifted = fun x -> if is_invalid x then Bottom else NonBottom x + let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted = + fun (l, u) eval_sym -> + match (Bound.subst_lb l eval_sym, Bound.subst_ub u eval_sym) with + | NonBottom l, NonBottom u -> + normalize (l, u) + | _ -> + Bottom + + let prune_le : t -> t -> t = fun x y -> match (x, y) with diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 13d7372f0..0e838cb63 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -291,4 +291,4 @@ void unsigned_prune_gt(unsigned int x, unsigned int y) { } } -void call_unsigned_prune_gt_Good_FP() { unsigned_prune_gt(0, 3); } +void call_unsigned_prune_gt_Good() { unsigned_prune_gt(0, 3); } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 1b2432536..618563df9 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,7 +1,6 @@ codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge2_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge3_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge3_Good` ] -codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_gt_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: ([1, 0] - 3):unsigned32 by call to `unsigned_prune_gt` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_zero1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32] @@ -142,11 +141,11 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFE codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: 10 Size: 5 by call to `pointer_arith3` ] codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 Size: 5 by call to `FN_pointer_arith4_Bad` ] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] -codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: 5 by call to `prune_arrblk_eq` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax1_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Binop: (0 - 1):unsigned32 by call to `prune_minmax1_Ok` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax2_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 2):unsigned32 by call to `prune_minmax2_Ok` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ] +codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [-length.ub + length.lb + 1, length.ub] Size: length] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index fb8832a32..23e74ac7a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -134,7 +134,7 @@ void prune_arrblk_eq(int* x) { } } -void FP_call_prune_arrblk_eq_Ok() { +void call_prune_arrblk_eq_Ok() { int* x = (int*)malloc(sizeof(int) * 5); prune_arrblk_eq(x); } @@ -156,3 +156,40 @@ void prune_minmax2_Ok(unsigned int x, unsigned int y) { } void FP_call_prune_minmax2_Ok() { prune_minmax2_Ok(0, 2); } + +void loop_prune_Good(int length, int j) { + int i; + char a[length]; + + for (i = length - 1; i >= 0; i--) { + if (j >= 0 && j < i) { + /* here we always have i >= 1 */ + a[length - i] = 'Z'; + } + } +} + +void loop_prune2_Good_FP(int length, int j) { + int i; + char a[length]; + + for (i = length - 1; i >= 0; i--) { + /* need a relational domain */ + if (j < i && j >= 0) { + /* here we always have i >= 1 */ + a[length - i] = 'Z'; + } + } +} + +void nested_loop_prune_Good(int length) { + int i, j; + char a[length]; + + for (i = length - 1; i >= 0; i--) { + for (j = 0; j < i; j++) { + /* here we always have i >= 1 */ + a[length - i] = 'Z'; + } + } +}