[inferbo] Give semantics for unsigned int casting of minus one

Reviewed By: mbouaziz

Differential Revision: D13167389

fbshipit-source-id: 9ad2c8e23
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 5f925869b6
commit 15b77ee8c8

@ -346,6 +346,8 @@ module Val = struct
let unknown_locs = of_pow_loc PowLoc.unknown ~traces:TraceSet.empty
let is_mone x = Itv.is_mone (get_itv x)
module Itv = struct
let m1_255 = of_itv Itv.m1_255

@ -158,7 +158,13 @@ let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
eval_const c
| Exp.Cast (t, e) ->
let v = eval integer_type_widths e mem in
set_array_stride integer_type_widths t v
let v = set_array_stride integer_type_widths t v in
if Typ.is_unsigned_int t && Val.is_mone v then
(* We treat "(unsigned int)-1" case specially, because programmers often exploit it to get
the max number of the type. *)
let ikind = Option.value_exn (Typ.get_ikind_opt t) in
Val.of_itv (Itv.max_of_ikind integer_type_widths ikind)
else v
| Exp.Lfield (e, fn, _) ->
let v = eval integer_type_widths e mem in
let locs = Val.get_all_locs v |> PowLoc.append_field ~fn in

@ -161,6 +161,8 @@ module ItvPure = struct
let is_one : t -> bool = fun (l, u) -> Bound.eq l Bound.one && Bound.eq u Bound.one
let is_mone : t -> bool = fun (l, u) -> Bound.eq l Bound.mone && Bound.eq u Bound.mone
let is_true : t -> bool = fun (l, u) -> Bound.le Bound.one l || Bound.le u Bound.mone
let is_false : t -> bool = is_zero
@ -410,6 +412,11 @@ module ItvPure = struct
let make_positive : t -> t =
fun ((l, u) as x) -> if Bound.lt l Bound.zero then (Bound.zero, u) else x
let max_of_ikind integer_type_widths ikind =
let _, max = Typ.range_of_ikind integer_type_widths ikind in
of_big_int max
end
include AbstractDomain.BottomLifted (ItvPure)
@ -553,6 +560,8 @@ let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t
let is_const : t -> Z.t option = bind1zo ItvPure.is_const
let is_mone = bind1bool ItvPure.is_mone
let eq_const : Z.t -> t -> bool = fun z -> bind1bool (ItvPure.eq_const z)
let neg : t -> t = lift1 ItvPure.neg
@ -615,3 +624,6 @@ let get_symbols : t -> SymbolSet.t = function
let normalize : t -> t = bind1 ItvPure.normalize
let max_of_ikind integer_type_widths ikind =
NonBottom (ItvPure.max_of_ikind integer_type_widths ikind)

@ -138,6 +138,8 @@ val of_int64 : Int64.t -> t
val is_const : t -> Z.t option
val is_mone : t -> bool
val eq_const : Z.t -> t -> bool
val make_sym :
@ -214,3 +216,5 @@ val prune_eq : t -> t -> t
val prune_ne : t -> t -> t
val subst : t -> Bound.eval_sym -> t
val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t

@ -450,3 +450,78 @@ void band_negative_Bad() {
#define ALMOST_FOUR_GIGABYTES (85 * FOUR_GIGABYTES / 100)
void simple_overflow_Bad() { auto x = ALMOST_FOUR_GIGABYTES; }
unsigned int unused_integer_underflow_Good_FP() {
unsigned int n = 0;
if (n-- == 0) {
return 0;
} else {
return n;
}
}
unsigned int unused_integer_underflow_Bad() {
unsigned int n = 0;
if (n-- == 0) {
return n;
} else {
return n;
}
}
unsigned int unused_integer_underflow2_Good_FP() {
unsigned int n = 0;
return n--;
}
unsigned int unused_integer_underflow2_Bad() {
unsigned int n = 0;
return --n;
}
void recover_integer_underflow_Good_FP() {
for (unsigned int i = 0; i < 10; i++) {
if (unknown_function()) {
i--; // right after this, i++ will be called.
}
}
}
void recover_integer_underflow_Bad() {
for (unsigned int i = 0; i < 10; i++) {
if (unknown_function()) {
i -= 2;
}
}
}
unsigned long scan_hex_Good(char* cp) {
unsigned long num_digits = 0, digit, val = 0;
while (1) {
digit = *cp;
if ((digit - '0') <= 9)
digit -= '0';
else if ((digit - 'a') < 6)
digit -= 'a' - 10;
else if ((digit - 'A') < 6)
digit -= 'A' - 10;
else
break;
val = (val << 4) | digit;
++cp;
}
return val;
}
void call_scan_hex_Good_FP() {
char* cp = "\0";
scan_hex_Good(cp);
}
int check_addition_overflow_Good(unsigned int x, unsigned int y) {
if (((unsigned int)-1) - x < y) {
return 1;
} else {
return 0;
}
}

@ -54,7 +54,7 @@ void cast_signed_to_unsigned_Good() {
}
}
void cast_signed_to_unsigned_Bad_FN() {
void cast_signed_to_unsigned_Bad() {
char arr[10];
int32_t x = -1;
uint32_t y = (uint32_t)x;
@ -63,6 +63,15 @@ void cast_signed_to_unsigned_Bad_FN() {
}
}
void cast_signed_to_unsigned2_Bad_FN() {
char arr[10];
int32_t x = -2;
uint32_t y = (uint32_t)x;
if (y > 0) {
arr[y] = 0;
}
}
void cast_float_to_int_Good() {
char arr[10];
float x = 15.0;

@ -3,6 +3,7 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2,
codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `cp[*]`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([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,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]
@ -25,8 +26,18 @@ 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, [<Offset trace>,Call,Assignment,<Length trace>,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, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 19] Size: 19]
codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Unknown value from: unknown_int,Assignment,Binary operation: ([-oo, 9223372036854775807] + 1):signed64]
codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([-oo, 9] - 2):unsigned32]
codetoanalyze/c/bufferoverrun/arith.c, recover_integer_underflow_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,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, 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, [<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [0, 80]):unsigned32]
codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow2_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
@ -49,7 +60,9 @@ codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 3, BUFFER_OVERRUN_L1, no_bu
codetoanalyze/c/bufferoverrun/cast.c, cast2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,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_signed_to_unsigned_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
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, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 4294967295 Size: 10]
codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
@ -135,18 +148,18 @@ codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_
codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 255] Size: 10000]
codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: -1 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 8 Size: 4]
codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: -1 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 8 Size: 4]
codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: -1 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset added: 8 Size: 4]
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: -1 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40]
codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 8 Size: 4]
codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 10 Size: 5]
codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]

@ -28,3 +28,30 @@ void range_bool_Bad() {
bool x = true + false; // x is 1 (true)
a[x] = 0;
}
void bool_overflow_Good_FP() {
int a[10];
if (((bool)-1) - 1) {
a[10] = 0;
} else {
a[5] = 0;
}
}
void bool_overflow_Bad() {
int a[10];
if (((bool)-1) - 1) {
a[10] = 0;
} else {
a[15] = 0;
}
}
void bool_overflow2_Good_FP() {
int a[10];
if (((bool)-2) - 1) {
a[10] = 0;
} else {
a[5] = 0;
}
}

@ -1,5 +1,11 @@
INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<Int_no_copy,std::allocator<Int_no_copy>>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this[*].infer_size`,<RHS trace>,Unknown value from: std::distance<std::__wrap_iter<const_Int_no_copy_*>_>,Binary operation: (this[*].infer_size - [-oo, +oo]):unsigned64]
INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<int,std::allocator<int>>_insert<std::__list_iterator<int,_void_*>_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this[*].infer_size`,<RHS trace>,Unknown value from: std::distance<std::__list_iterator<int,_void_*>_>,Binary operation: (this[*].infer_size + [-oo, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow2_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow2_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]

Loading…
Cancel
Save