From 67a4b73cd082779b13667956a3921cd69d582238 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sat, 18 Jan 2020 03:36:47 -0800 Subject: [PATCH] [inferbo] Revise bit-and semantics on pointer value Summary: Inferbo analyzed some program points unreachable incorrectly, because of unsound semantics of band operator, which did not handle the case when given parameters are pointer values. Reviewed By: ngorogiannis Differential Revision: D19392705 fbshipit-source-id: dd590508c --- .../src/bufferoverrun/bufferOverrunDomain.ml | 43 ++++++++++--------- .../codetoanalyze/c/bufferoverrun/arith.c | 26 +++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 + 3 files changed, 50 insertions(+), 21 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index ca7bf9cee..cdea628fb 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -252,26 +252,27 @@ module Val = struct let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool} - let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t = - fun f ?f_trace x y -> - let itv = f x.itv y.itv in - let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in - let itv_updated_by = ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by in - let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in - let traces = - match f_trace with - | Some f_trace -> - f_trace x.traces y.traces - | None -> ( - match (Itv.eq itv x.itv, Itv.eq itv y.itv) with - | true, false -> - x.traces - | false, true -> - y.traces - | true, true | false, false -> - TraceSet.join x.traces y.traces ) - in - {bot with itv; itv_thresholds; itv_updated_by; modeled_range; traces} + let lift_itv : ?may_ptr:bool -> (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t = + let no_ptr {powloc; arrayblk} = PowLoc.is_bot powloc && ArrayBlk.is_bot arrayblk in + fun ?(may_ptr = false) f ?f_trace x y -> + let itv = if (not may_ptr) || (no_ptr x && no_ptr y) then f x.itv y.itv else Itv.top in + let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in + let itv_updated_by = ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by in + let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in + let traces = + match f_trace with + | Some f_trace -> + f_trace x.traces y.traces + | None -> ( + match (Itv.eq itv x.itv, Itv.eq itv y.itv) with + | true, false -> + x.traces + | false, true -> + y.traces + | true, true | false, false -> + TraceSet.join x.traces y.traces ) + in + {bot with itv; itv_thresholds; itv_updated_by; modeled_range; traces} let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t = @@ -318,7 +319,7 @@ module Val = struct let shiftrt = lift_itv Itv.shiftrt - let band_sem = lift_itv Itv.band_sem + let band_sem = lift_itv ~may_ptr:true Itv.band_sem let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem Boolean.EqualOrder.strict_cmp diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 0a3ee472e..64ceebd7c 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -546,3 +546,29 @@ void shift_right_zero_Bad(int x) { void use_intended_integer_underflow_Good() { unsigned long long x = INTENDED_INTEGER_UNDERFLOW; } + +void ptr_band1_Bad(int x, int* q) { + int a[5]; + int* p; + if (x) { + p = q; + } else { + p = 0; + } + if ((int)p & x) { + a[10] = 0; + } +} + +void ptr_band2_Bad(int x, int* q) { + int a[5]; + int* p; + if (x) { + p = q; + } else { + p = 0; + } + if ((int)p & x) { + } + a[10] = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 6e70e3304..fd2085d38 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -30,6 +30,8 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERR codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 25] Size: 20] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 19] Size: 19] codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Unknown value from: unknown_int,Assignment,Binary operation: ([-oo, 9223372036854775807] + 1):signed64] +codetoanalyze/c/bufferoverrun/arith.c, ptr_band1_Bad, 9, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/arith.c, ptr_band2_Bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([-oo, 9] - 2):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Assignment,Binary operation: ([0, 9] - 1):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, scan_hex_Good, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]