From 77084782e180f5144bf9dae9c00994971c6d1265 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 23 Aug 2019 01:14:22 -0700 Subject: [PATCH] [inferbo] Fix bug in integer pruning by pointer Summary: This diff avoids that an integer value is pruned to the bottom by comparing to a pointer. For example, before this diff, assume((int*)x == p); assume((int*)x != p); where x is an integer, x is pruned to the bottom in both of the assume cases. So, there were some, unintentional and false, unreachable code. Depends on D16960199 Reviewed By: ezgicicek Differential Revision: D16964735 fbshipit-source-id: 90a3c8c80 --- infer/src/bufferoverrun/bufferOverrunDomain.ml | 11 ++++++++++- infer/tests/codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../tests/codetoanalyze/c/bufferoverrun/prune_alias.c | 8 ++++++++ 3 files changed, 19 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 3f8074b63..09ba6e915 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -288,7 +288,16 @@ module Val = struct let lift_prune2 : (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> t -> t -> t = fun f g x y -> - let itv = f x.itv y.itv in + let itv = + let pruned_itv = f x.itv y.itv in + if + Itv.is_bottom pruned_itv + && (not (Itv.is_bottom x.itv)) + && Itv.is_bottom y.itv + && not (PowLoc.is_bottom (get_all_locs y)) + then x.itv + else pruned_itv + in let itv_thresholds = Option.value_map (Itv.is_const y.itv) ~default:x.itv_thresholds ~f:(fun z -> x.itv_thresholds diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 10838db08..6a69693d7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -264,6 +264,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_AL codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/prune_alias.c, prune_int_by_pointer_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 5 Size: 5] codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index bce597fa1..a5e0a3726 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -377,3 +377,11 @@ void prune_linear_by_minmax(size_t s, size_t t) { void call_prune_linear_by_minmax_Good() { prune_linear_by_minmax(unknown_function(), unknown_function()); } + +void prune_int_by_pointer_Bad(int* p) { + int* x = (int*)100; + if (x == p) { + } + int a[5]; + a[5] = 0; +}