From 18ea3f99d8aed9a5e132e19a96c92b681c84ddb2 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 12 Mar 2018 07:25:40 -0700 Subject: [PATCH] [inferbo][bugfix] Plus semantics of interval domain Summary: It corrects a precision bug in the interval domain, with adding some test cases. Reviewed By: mbouaziz Differential Revision: D7230918 fbshipit-source-id: 3ec641a --- infer/src/bufferoverrun/itv.ml | 44 +++++++++++++------ .../codetoanalyze/c/bufferoverrun/arith.c | 32 ++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 3 ++ 3 files changed, 65 insertions(+), 14 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 1ed20a68f..468cf998d 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -711,8 +711,8 @@ module Bound = struct let subst_ub x map = subst ~subst_pos:SubstUpperBound x map - let plus : default:t -> t -> t -> t = - fun ~default x y -> + let plus_common : f:(t -> t -> t) -> t -> t -> t = + fun ~f x y -> match (x, y) with | _, _ when is_zero x -> y @@ -724,19 +724,35 @@ module Bound = struct | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1) when SymLinear.is_zero x2 -> mk_MinMax (c1 + c2, sign, min_max, d1, x1) - | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2) - | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) -> - Linear (c1 + d1 + c2, x2) - | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2) - | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) -> - Linear (c1 - d1 + c2, x2) - | _, _ -> - default - - - let plus_l = plus ~default:MInf + | _ -> + f x y + + + let plus_l : t -> t -> t = + plus_common ~f:(fun x y -> + match (x, y) with + | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) -> + Linear (c1 + d1 + c2, x2) + | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) -> + Linear (c1 - d1 + c2, x2) + | _, _ -> + MInf ) + + + let plus_u : t -> t -> t = + plus_common ~f:(fun x y -> + match (x, y) with + | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) -> + Linear (c1 + d1 + c2, x2) + | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) -> + Linear (c1 - d1 + c2, x2) + | _, _ -> + PInf ) - let plus_u = plus ~default:PInf let mult_const : t -> NonZeroInt.t -> t option = fun x n -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 20fa32822..20f15a301 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -80,3 +80,35 @@ int division_of_zero_Good(int x) { i /= 2; return i; } + +/* While the most precise return value is + - "2*i+1" if 0 <= i < 10, + - "0" o.w. + Inferbo returns [1+min(-1,s0),10+max(-10,s1)] where i is [s0,s1]. */ +int plus_linear_min(int i) { /* i |-> [s0,s1] */ + int linear = i + 1; /* linear |-> [s0+1,s1+1] */ + if (i >= 0 && i < 10) { /* i |-> [max(0,s0),min(9,s1)] */ + return linear + i; /* return |-> [s0+1,s1+10] */ + } + return 0; +} + +void plus_linear_min_Good() { + int a[20]; + a[plus_linear_min(9)] = 1; +} + +void plus_linear_min_Bad() { + int a[19]; + a[plus_linear_min(9)] = 1; +} + +void plus_linear_min2_Good_FP() { + int a[10]; + a[plus_linear_min(4)] = 1; +} + +void plus_linear_min3_Good_FP() { + int a[20]; + a[plus_linear_min(15)] = 1; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index e85186e11..dc89322a6 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,5 +1,8 @@ codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]] codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: [20, 20]] +codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: [19, 19]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, ERROR, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]] codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [20, 20] Size: [10, 10]] codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: [-1, -1] Size: [2, 2]]