From 1827b42f68016f1ed67a8a30e6bcefe5ad0a0e43 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 19 Dec 2018 08:20:01 -0800 Subject: [PATCH] [inferbo] Improve traces of binary operators when nothing changes Reviewed By: ezgicicek Differential Revision: D13517607 fbshipit-source-id: 960d4e993 --- infer/src/bufferoverrun/bufferOverrunDomain.ml | 18 ++++++++++++++++-- .../codetoanalyze/c/bufferoverrun/arith.c | 2 -- .../codetoanalyze/c/bufferoverrun/issues.exp | 4 ++-- .../codetoanalyze/cpp/bufferoverrun/issues.exp | 9 ++++----- 4 files changed, 22 insertions(+), 11 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index e23b2fd44..4e7b88209 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -173,8 +173,22 @@ module Val = struct let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool; sym= Relation.Sym.top} let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t = - fun f ?(f_trace = TraceSet.join) x y -> - {bot with itv= f x.itv y.itv; traces= f_trace x.traces y.traces} + fun f ?f_trace x y -> + let itv = f x.itv y.itv 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; traces} let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index d26588456..d4a393603 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -536,8 +536,6 @@ void shift_right_zero_Good(int x) { arr[0 >> x] = 1; } -/* This also exhibits an overapproximation of traces, here [x] doesn't influence - * the result */ void shift_right_zero_Bad(int x) { int arr[1]; arr[1 + (0 >> x)] = 1; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index a69030e24..75f636d59 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -35,7 +35,7 @@ codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Bad, 3, INTEGER 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] codetoanalyze/c/bufferoverrun/arith.c, scan_hex_Good, 8, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/arith.c, shift_right_zero_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x`,,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/arith.c, shift_right_zero_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binary operation: (85 × 4294967295):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Assignment,Assignment,,Assignment,Binary operation: ([0, +oo] + [0, 80]):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32] @@ -224,7 +224,7 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_sub2` ] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 06c5485dc..fdb8f7605 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -61,8 +61,8 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_O codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `*o`,Call,Parameter `*k`,Call,Parameter `*k`,Assignment,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Call,Parameter `*o`,Call,Parameter `*k`,Call,Parameter `*k`,Assignment,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ] codetoanalyze/cpp/bufferoverrun/repro1.cpp, gal_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] @@ -86,9 +86,8 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,,Parameter `this->infer_size`,,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [45, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Unknown value from: std::distance_>,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Unknown value from: std::distance_>,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,,Parameter `this->infer_size`,,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]