From 01a83e694b2c55e240753cf1dfa5237faf4472f8 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 8 Nov 2018 20:48:11 -0800 Subject: [PATCH] [inferbo] Improve semantics of binary and Reviewed By: mbouaziz Differential Revision: D12921726 fbshipit-source-id: ed6777e69 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 2 + .../bufferoverrun/bufferOverrunSemantics.ml | 4 +- infer/src/bufferoverrun/itv.ml | 13 +++ infer/src/bufferoverrun/itv.mli | 2 + .../codetoanalyze/c/bufferoverrun/arith.c | 82 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 5 ++ 6 files changed, 107 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 1b3aa42ba..47f1c5389 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -207,6 +207,8 @@ module Val = struct let shiftrt : t -> t -> t = lift_itv Itv.shiftrt + let band_sem : t -> t -> t = lift_itv Itv.band_sem + let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem let gt_sem : t -> t -> t = lift_cmp_itv Itv.gt_sem diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 2905d18df..ad51690dd 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -229,7 +229,9 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = Val.eq_sem v1 v2 | Binop.Ne -> Val.ne_sem v1 v2 - | Binop.BAnd | Binop.BXor | Binop.BOr -> + | Binop.BAnd -> + Val.band_sem v1 v2 + | Binop.BXor | Binop.BOr -> Val.unknown_bit v1 | Binop.LAnd -> Val.land_sem v1 v2 diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 47574e288..dee4aee6f 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -696,6 +696,17 @@ module ItvPure = struct top + let band_sem : t -> t -> t = + fun x y -> + match (is_const x, is_const y) with + | Some x', Some y' -> + if Z.(equal x' y') then x else of_big_int Z.(x' land y') + | _, _ -> + if is_ge_zero x && is_ge_zero y then (Bound.zero, Bound.overapprox_min (ub x) (ub y)) + else if is_le_zero x && is_le_zero y then (Bound.MInf, Bound.overapprox_min (ub x) (ub y)) + else top + + let lt_sem : t -> t -> Boolean.t = fun (l1, u1) (l2, u2) -> if Bound.lt u1 l2 then Boolean.True else if Bound.le u2 l1 then Boolean.False else Boolean.Top @@ -966,6 +977,8 @@ let shiftlt : t -> t -> t = lift2 ItvPure.shiftlt let shiftrt : t -> t -> t = lift2 ItvPure.shiftrt +let band_sem : t -> t -> t = lift2 ItvPure.band_sem + let lt_sem : t -> t -> Boolean.t = bind2b ItvPure.lt_sem let gt_sem : t -> t -> Boolean.t = bind2b ItvPure.gt_sem diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index e5e230c02..5018894d5 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -221,6 +221,8 @@ val shiftlt : t -> t -> t val shiftrt : t -> t -> t +val band_sem : t -> t -> t + val eq_sem : t -> t -> Boolean.t val ge_sem : t -> t -> Boolean.t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 69f8320b9..9d5dc0975 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -335,3 +335,85 @@ void two_safety_conditions2_Bad(uint32_t s) { void call_two_safety_conditions2_Bad() { two_safety_conditions2_Bad(15); // integer overflow L5: [0, +oo] + 15 } + +void band_positive_constant_Good() { + char a[3]; + int x = 6 & 2; // y is 2 + a[x] = 0; +} + +void band_positive_constant_Bad() { + char a[2]; + int x = 6 & 2; // y is 2 + a[x] = 0; +} + +void band_negative_constant_Good() { + char a[1]; + int x = (-3) & (-2); // x is -4 + a[x + 4] = 0; +} + +void band_negative_constant_Bad() { + char a[1]; + int x = (-3) & (-2); // x is -4 + a[x + 5] = 0; +} + +void band_constant_Good() { + char a[2]; + int x = (-3) & 1; // x is 1 + a[x] = 0; +} + +void band_constant_Bad() { + char a[1]; + int x = (-3) & 1; // x is 1 + a[x] = 0; +} + +void band_positive_Good() { + char a[9]; + int x = unknown_nat(); + int y = unknown_nat(); + if (x <= 10 && y <= 8) { + int z = x & y; // z is [0, 8] + a[z] = 0; + } +} + +void band_positive_Bad() { + char a[5]; + int x = unknown_nat(); + int y = unknown_nat(); + if (x <= 10 && y <= 8) { + int z = x & y; // z is [0, 8] + a[z] = 0; + } +} + +void band_negative_Good() { + char a[3]; + int x = unknown_function(); + int y = unknown_function(); + if (x <= -3 && y <= -2) { + int z = x & y; // z is [-oo, -3] + z = z + 5; // z is [-oo, 2] + if (z >= 0) { + a[z] = 0; + } + } +} + +void band_negative_Bad() { + char a[2]; + int x = unknown_function(); + int y = unknown_function(); + if (x <= -3 && y <= -2) { + int z = x & y; // z is [-oo, -3] + z = z + 5; // z is [-oo, 2] + if (z >= 0) { + a[z] = 0; + } + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ec7e9f1be..90c4c0a2e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,3 +1,8 @@ +codetoanalyze/c/bufferoverrun/arith.c, band_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,Assignment,Assignment,ArrayAccess: Offset: [0, 2] Size: 2] +codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 8] Size: 5] +codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] 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, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32]