From 0d046c8e7cc851284fe2ca061495867d926841ed Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 27 Feb 2020 02:25:05 -0800 Subject: [PATCH] [inferbo] Ignore float/double constant Summary: Current domain of Inferbo cannot handle float values. This diff evaluates float constants to the top interval. Reviewed By: ezgicicek Differential Revision: D20116361 fbshipit-source-id: e6e398bbd --- .../src/bufferoverrun/bufferOverrunSemantics.ml | 2 -- .../tests/codetoanalyze/c/bufferoverrun/arith.c | 16 ++++++++++++++++ infer/tests/codetoanalyze/c/bufferoverrun/cast.c | 4 ++-- .../codetoanalyze/c/bufferoverrun/issues.exp | 6 ++++-- 4 files changed, 22 insertions(+), 6 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 300be8f24..24f114f4f 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -18,8 +18,6 @@ let eval_const : Typ.IntegerWidths.t -> Const.t -> Val.t = fun integer_type_widths -> function | Const.Cint intlit -> Val.of_big_int (IntLit.to_big_int intlit) - | Const.Cfloat f -> - f |> int_of_float |> Val.of_int | Const.Cstr s -> Val.of_literal_string integer_type_widths s | _ -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 64ceebd7c..4ffccbf3f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -572,3 +572,19 @@ void ptr_band2_Bad(int x, int* q) { } a[10] = 0; } + +void do_not_prune_float_Good_FP() { + int a[5]; + float f = 0.5; + if (f > 1.0 && f < 1.0) { + a[10] = 0; + } +} + +void do_not_prune_float_Bad() { + int a[5]; + float f = 0.5; + if (f > 0.0 && f < 1.0) { + a[10] = 0; + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/cast.c b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c index 37fa35504..7bc2c4d11 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/cast.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c @@ -72,7 +72,7 @@ void cast_signed_to_unsigned2_Bad_FN() { } } -void cast_float_to_int_Good() { +void cast_float_to_int_Good_FP() { char arr[10]; float x = 15.0; int32_t y = (int32_t)x; @@ -81,7 +81,7 @@ void cast_float_to_int_Good() { } } -void cast_float_to_int_Bad_FN() { +void cast_float_to_int_Bad() { char arr[10]; float x = 15000000000.0; int32_t y = (int32_t)x; // y is -2147483648. diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index fd2085d38..ade81dd73 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -12,6 +12,8 @@ codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLO codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,,Call,Assignment,Assignment,,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Parameter `n`,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] +codetoanalyze/c/bufferoverrun/arith.c, do_not_prune_float_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/arith.c, do_not_prune_float_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: (2000000000 + 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([0, 2000000000] + [0, 2000000000]):signed32] @@ -81,8 +83,8 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16 codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/cast.c, cast2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 20 Size: 16] -codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, 9] Size: 10] +codetoanalyze/c/bufferoverrun/cast.c, cast_float_to_int_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, 9] Size: 10] codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned2_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Assignment,,Array declaration,Array access: Offset: 4294967295 Size: 10]