From 0d2b0e1ab7684daa712ef2838397c788ce33249a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 16 Nov 2018 21:34:55 -0800 Subject: [PATCH] [inferbo] Fix check function for is_collection_add Summary: It fixes the conditions of the `check` function to address `is_collection_add` cases correctly. Reviewed By: mbouaziz Differential Revision: D13081281 fbshipit-source-id: 39ae5ef03 --- .../bufferOverrunProofObligations.ml | 5 ++--- infer/src/bufferoverrun/itv.ml | 2 ++ infer/src/bufferoverrun/itv.mli | 2 ++ .../codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../tests/codetoanalyze/c/bufferoverrun/models.c | 15 +++++++++++++++ 5 files changed, 22 insertions(+), 3 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 10e7f4d56..a7f2be62e 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -250,11 +250,10 @@ module ArrayAccessCondition = struct For arrays : we want to check that 0 <= idx < size For adding into arraylists: we want to check that 0 <= idx <= size *) let real_idx = ItvPure.plus c.offset c.idx in - let size = ItvPure.make_positive c.size in + let size = ItvPure.make_positive (if is_collection_add then ItvPure.succ c.size else c.size) in (* if sl < 0, use sl' = 0 *) let not_overrun = - if is_collection_add then ItvPure.le_sem real_idx size - else if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_ + if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_ else ItvPure.lt_sem real_idx size in let not_underrun = diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index d02478e3e..53897d1ee 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -626,6 +626,8 @@ module ItvPure = struct let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2) + let succ : t -> t = fun x -> plus x one + let mult_const : Z.t -> t -> t = fun n ((l, u) as itv) -> match NonZeroInt.of_big_int n with diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 9c2adbdd2..b5ed7883b 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -146,6 +146,8 @@ module ItvPure : sig val minus : t -> t -> t + val succ : t -> t + val mult : t -> t -> t end diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index be3b0e33d..738b246f3 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -129,6 +129,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_ codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: x,Call,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [-19+min(0, x), -1] Size: 1] codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Offset: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255] codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c index da101fe3d..5fe1f14a0 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -97,6 +97,21 @@ void memcpy_good4() { memcpy(dst, src, sizeof(dst)); } +void memcpy_len(size_t len) { + char dst[len]; + char src[len]; + memcpy(dst, src, len); +} + +void call_memcpy_len1_Good() { memcpy_len(40); } + +extern size_t unknown_uint(); + +void call_memcpy_len2_Good_FP() { + size_t x = unknown(); + memcpy_len(x); +} + void memmove_bad1() { int arr1[10]; int arr2[20];