From 87dd2047ec3ae8bb5024c7a0b8c33cd56ccf8a81 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 30 Oct 2018 06:57:06 -0700 Subject: [PATCH] [infer] Use big int in IntLit Reviewed By: mbouaziz Differential Revision: D12838124 fbshipit-source-id: e1fa08727 --- infer/src/IR/IntLit.ml | 76 ++++++++++--------- infer/src/IR/IntLit.mli | 2 + infer/src/clang/cTrans.ml | 4 +- .../codetoanalyze/c/bufferoverrun/arith.c | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../c/frontend/arithmetic/int_const.c.dot | 2 +- .../cpp/bufferoverrun/issues.exp | 2 + .../cpp/bufferoverrun/std_array.cpp | 2 +- 8 files changed, 50 insertions(+), 41 deletions(-) diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml index 341e746c6..01fccc957 100644 --- a/infer/src/IR/IntLit.ml +++ b/infer/src/IR/IntLit.ml @@ -10,7 +10,7 @@ module F = Format module L = Logging (** signed and unsigned integer literals *) -type t = bool * Int64.t * bool +type t = bool * Z.t * bool exception OversizedShift @@ -18,7 +18,7 @@ exception OversizedShift and the second whether it is a pointer *) let area u i = - match (i < 0L, u) with + match (Z.(i < zero), u) with | true, false -> (* only representable as signed *) 1 | false, _ -> @@ -34,11 +34,11 @@ let to_signed (unsigned, i, ptr) = let compare (unsigned1, i1, _) (unsigned2, i2, _) = let n = Bool.compare unsigned1 unsigned2 in - if n <> 0 then n else Int64.compare i1 i2 + if n <> 0 then n else Z.compare i1 i2 let compare_value (unsigned1, i1, _) (unsigned2, i2, _) = - [%compare: int * Int64.t] (area unsigned1 i1, i1) (area unsigned2 i2, i2) + [%compare: int * Z.t] (area unsigned1 i1, i1) (area unsigned2 i2, i2) let eq i1 i2 = Int.equal (compare_value i1 i2) 0 @@ -53,21 +53,27 @@ let geq i1 i2 = compare_value i1 i2 >= 0 let gt i1 i2 = compare_value i1 i2 > 0 -let of_int64 i = (false, i, false) +let of_z z_of_int i = (false, z_of_int i, false) -let of_int32 i = of_int64 (Int64.of_int32 i) +let of_int64 = of_z Z.of_int64 -let of_int i = of_int64 (Int64.of_int i) +let of_int32 = of_z Z.of_int32 -let to_int (_, i, _) = Int64.to_int i +let of_int = of_z Z.of_int -let to_int_exn (_, i, _) = Int64.to_int_exn i +let of_string = of_z Z.of_string -let to_big_int (_, i, _) = Z.of_int64 i +let z_to_int_opt i = try Some (Z.to_int i) with Z.Overflow -> None -let to_float (_, i, _) = Int64.to_float i +let to_int (_, i, _) = z_to_int_opt i -let null = (false, 0L, true) +let to_int_exn (_, i, _) = Z.to_int i + +let to_big_int (_, i, _) = i + +let to_float (_, i, _) = Z.to_float i + +let null = (false, Z.zero, true) let zero = of_int 0 @@ -77,17 +83,17 @@ let two = of_int 2 let minus_one = of_int (-1) -let isone (_, i, _) = Int64.equal i 1L +let isone (_, i, _) = Z.(equal i one) -let iszero (_, i, _) = Int64.equal i 0L +let iszero (_, i, _) = Z.(equal i zero) -let isnull (_, i, ptr) = Int64.equal i 0L && ptr +let isnull (_, i, ptr) = Z.(equal i zero) && ptr -let isminusone (unsigned, i, _) = (not unsigned) && Int64.equal i (-1L) +let isminusone (unsigned, i, _) = (not unsigned) && Z.(equal i minus_one) -let isnegative (unsigned, i, _) = (not unsigned) && i < 0L +let isnegative (unsigned, i, _) = (not unsigned) && Z.(lt i zero) -let neg (unsigned, i, ptr) = (unsigned, Int64.neg i, ptr) +let neg (unsigned, i, ptr) = (unsigned, Z.neg i, ptr) let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) = (unsigned1 || unsigned2, binop i1 i2, ptr1 || ptr2) @@ -95,48 +101,46 @@ let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) = let lift1 unop (unsigned, i, ptr) = (unsigned, unop i, ptr) -let add i1 i2 = lift Int64.( + ) i1 i2 +let add i1 i2 = lift Z.( + ) i1 i2 -let mul i1 i2 = lift Int64.( * ) i1 i2 +let mul i1 i2 = lift Z.( * ) i1 i2 -let div i1 i2 = lift Int64.( / ) i1 i2 +let div i1 i2 = lift Z.( / ) i1 i2 -let rem i1 i2 = lift Int64.rem i1 i2 +let rem i1 i2 = lift Z.rem i1 i2 -let logand i1 i2 = lift Int64.bit_and i1 i2 +let logand i1 i2 = lift Z.logand i1 i2 -let logor i1 i2 = lift Int64.bit_or i1 i2 +let logor i1 i2 = lift Z.logor i1 i2 -let logxor i1 i2 = lift Int64.bit_xor i1 i2 +let logxor i1 i2 = lift Z.logxor i1 i2 -let lognot i = lift1 Int64.bit_not i +let lognot i = lift1 Z.lognot i let sub i1 i2 = add i1 (neg i2) let shift_left (unsigned1, i1, ptr1) (_, i2, _) = - match Int64.to_int i2 with + match z_to_int_opt i2 with | None -> - L.(die InternalError) "Shifting failed with operand %a" Int64.pp i2 + L.(die InternalError) "Shifting failed with operand %a" Z.pp_print i2 | Some i2 -> if i2 < 0 || i2 >= 64 then raise OversizedShift ; - let res = Int64.shift_left i1 i2 in + let res = Z.shift_left i1 i2 in (unsigned1, res, ptr1) let shift_right (unsigned1, i1, ptr1) (_, i2, _) = - match Int64.to_int i2 with + match z_to_int_opt i2 with | None -> - L.(die InternalError) "Shifting failed with operand %a" Int64.pp i2 + L.(die InternalError) "Shifting failed with operand %a" Z.pp_print i2 | Some i2 -> if i2 < 0 || i2 >= 64 then raise OversizedShift ; - let res = Int64.shift_right i1 i2 in + let res = Z.shift_right i1 i2 in (unsigned1, res, ptr1) -let pp f (unsigned, n, ptr) = - if ptr && Int64.equal n 0L then F.pp_print_string f "null" - else if unsigned then F.fprintf f "%Lu" n - else F.fprintf f "%Ld" n +let pp f (_, n, ptr) = + if ptr && Z.(equal n zero) then F.pp_print_string f "null" else Z.pp_print f n let to_string i = F.asprintf "%a" pp i diff --git a/infer/src/IR/IntLit.mli b/infer/src/IR/IntLit.mli index 097a54195..231071efe 100644 --- a/infer/src/IR/IntLit.mli +++ b/infer/src/IR/IntLit.mli @@ -33,6 +33,8 @@ val of_int32 : int32 -> t val of_int64 : int64 -> t +val of_string : string -> t + val geq : t -> t -> bool val gt : t -> t -> bool [@@warning "-32"] diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index be67dc0c5..26616ef3a 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -370,8 +370,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let typ = CType_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in let exp = try - let i = Int64.of_string integer_literal_info.Clang_ast_t.ili_value in - let exp = Exp.int (IntLit.of_int64 i) in + let i = IntLit.of_string integer_literal_info.Clang_ast_t.ili_value in + let exp = Exp.int i in exp with Failure _ -> (* Parse error: return a nondeterministic value *) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 64eb9638b..bacb0222d 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -172,7 +172,7 @@ void use_uint64_max_Good() { arr[x - y] = 0; } -void use_uint64_max_Bad_FN() { +void use_uint64_max_Bad() { char arr[10]; uint64_t x = UINT64_MAX; uint64_t y = UINT64_MAX - 15; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 4f945d16f..3f4a24ea3 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -20,6 +20,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERR codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: 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,Binop: ([-oo, 9223372036854775807] + 1):signed64] codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10] +codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] diff --git a/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c.dot b/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c.dot index 6e88a5079..c8d337078 100644 --- a/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c.dot +++ b/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c.dot @@ -11,7 +11,7 @@ digraph cfg { "main.fad58de7366495db4650cfefac2fcd61_3" -> "main.fad58de7366495db4650cfefac2fcd61_2" ; -"main.fad58de7366495db4650cfefac2fcd61_4" [label="4: DeclStmt \n *&overflow_int:int=n$0 [line 18, column 3]\n " shape="box"] +"main.fad58de7366495db4650cfefac2fcd61_4" [label="4: DeclStmt \n *&overflow_int:int=9223372036854775808 [line 18, column 3]\n " shape="box"] "main.fad58de7366495db4650cfefac2fcd61_4" -> "main.fad58de7366495db4650cfefac2fcd61_3" ; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 168ffb5c3..16db13400 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -54,6 +54,8 @@ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 4611686018427387903] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 9223372036854775807] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 9223372036854775807):unsigned64] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 18446744073709551615] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 18446744073709551615):unsigned64] codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayAccess: Offset: 10 Size: 10] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp index e0ea85b23..7440e710d 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp @@ -34,7 +34,7 @@ void new_int2_Bad() { dst = new int32_t[len]; } -void new_int3_Bad_FN() { +void new_int3_Bad() { uint64_t len = 18446744073709551615; // (1 << 64) - 1 int32_t* dst; dst = new int32_t[len];