[infer] Use big int in IntLit

Reviewed By: mbouaziz

Differential Revision: D12838124

fbshipit-source-id: e1fa08727

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

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"]

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 *)

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;

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, []

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" ;

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]

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];