[inferbo] Add models for Java's Integer

Summary: Add models for Java's Integer class.

Reviewed By: skcho

Differential Revision: D16668118

fbshipit-source-id: 05b3c8736

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -490,6 +490,11 @@ module Val = struct
           let allocsite = Allocsite.make_symbol deref_path in
           let length = Itv.of_length_path ~is_void:false path in
           of_java_array_alloc allocsite ~length ~traces
+      | Some JavaInteger ->
+          let l = Loc.of_path path in
+          let traces = traces_of_loc l in
+          let unsigned = Typ.is_unsigned_int typ in
+          of_itv ~traces (Itv.of_normal_path ~unsigned path)
       | None ->
           let l = Loc.of_path path in
           let traces = traces_of_loc l in

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -712,6 +712,35 @@ module StdVector = struct
     {exec; check= no_check}
 end
 
+(** Java's integers are modeled with an indirection to a memory
+   location that holds the actual integer value *)
+module JavaInteger = struct
+  let intValue exp =
+    let exec _ ~ret:(id, _) mem =
+      let powloc = Sem.eval_locs exp mem in
+      let v = if PowLoc.is_empty powloc then Dom.Val.Itv.top else Dom.Mem.find_set powloc mem in
+      model_by_value v id mem
+    in
+    {exec; check= no_check}
+
+
+  let valueOf exp =
+    let exec {pname; node_hash; location; integer_type_widths} ~ret:(id, _) mem =
+      let represents_multiple_values = false in
+      let int_allocsite =
+        Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:0 ~path:None
+          ~represents_multiple_values
+      in
+      let v = Sem.eval integer_type_widths exp mem in
+      let int_loc = Loc.of_allocsite int_allocsite in
+      mem |> Dom.Mem.add_heap int_loc v
+      |> Dom.Mem.add_stack (Loc.of_id id)
+           ( int_loc |> PowLoc.singleton
+           |> Dom.Val.of_pow_loc ~traces:Trace.(Set.singleton location JavaIntDecleration) )
+    in
+    {exec; check= no_check}
+end
+
 (* Java's Collections are represented like arrays. But we don't care about the elements.
 - when they are constructed, we set the size to 0
 - each time we add an element, we increase the length of the array
@@ -1081,5 +1110,9 @@ module Call = struct
       ; +PatternMatch.implements_org_json "JSONArray"
         &:: "length" <>$ capt_exp $!--> Collection.size
       ; +PatternMatch.implements_org_json "JSONArray"
-        &:: "<init>" <>$ capt_var_exn $+ capt_exp $--> Collection.init ]
+        &:: "<init>" <>$ capt_var_exn $+ capt_exp $--> Collection.init
+      ; +PatternMatch.implements_lang "Integer"
+        &:: "intValue" <>$ capt_exp $--> JavaInteger.intValue
+      ; +PatternMatch.implements_lang "Integer" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf
+      ]
 end

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -16,6 +16,7 @@ module BoTrace = struct
 
   type elem =
     | ArrayDeclaration
+    | JavaIntDecleration
     | Assign of PowLoc.t
     | Global of Loc.t
     | Parameter of Loc.t
@@ -77,6 +78,8 @@ module BoTrace = struct
   let pp_elem f = function
     | ArrayDeclaration ->
         F.pp_print_string f "ArrayDeclaration"
+    | JavaIntDecleration ->
+        F.pp_print_string f "JavaIntDeclaration"
     | Assign locs ->
         F.fprintf f "Assign `%a`" PowLoc.pp locs
     | Global loc ->
@@ -115,7 +118,7 @@ module BoTrace = struct
   let has_unknown = final_exists ~f:(function UnknownFrom _ -> true)
 
   let elem_has_risky = function
-    | ArrayDeclaration | Assign _ | Global _ | Parameter _ ->
+    | JavaIntDecleration | ArrayDeclaration | Assign _ | Global _ | Parameter _ ->
         false
     | Through {risky_fun} ->
         Option.is_some risky_fun
@@ -155,6 +158,8 @@ module BoTrace = struct
 
 
   let elem_err_desc = function
+    | JavaIntDecleration ->
+        "int declaration (java)"
     | ArrayDeclaration ->
         "Array declaration"
     | Assign _ ->

infer/src/bufferoverrun/bufferOverrunTypModels.ml

@@ -11,6 +11,7 @@ type typ_model =
   | CArray of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t}
   | CppStdVector of {element_typ: Typ.t}
   | JavaCollection
+  | JavaInteger
 
 let std_array element_typ length =
   CArray {element_typ; deref_kind= Symb.SymbolPath.Deref_ArrayIndex; length= IntLit.of_int64 length}
@@ -23,13 +24,18 @@ let std_vector element_typ = CppStdVector {element_typ}
 - each time we add an element, we increase the length of the array
 - each time we delete an element, we decrease the length of the array *)
 
-let collection = JavaCollection
+module Java = struct
+  let collection = JavaCollection
+
+  let integer = JavaInteger
+end
 
 let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher =
   let open ProcnameDispatcher.TypName in
   make_dispatcher
     [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> std_array
     ; -"std" &:: "vector" < capt_typ `T &+ any_typ >--> std_vector
-    ; +PatternMatch.implements_collection &::.*--> collection
+    ; +PatternMatch.implements_collection &::.*--> Java.collection
-    ; +PatternMatch.implements_iterator &::.*--> collection
+    ; +PatternMatch.implements_iterator &::.*--> Java.collection
-    ; +PatternMatch.implements_org_json "JSONArray" &::.*--> collection ]
+    ; +PatternMatch.implements_lang "Integer" &::.*--> Java.integer
+    ; +PatternMatch.implements_org_json "JSONArray" &::.*--> Java.collection ]

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -59,7 +59,7 @@ module Exec = struct
       | Some (CArray {element_typ; length}) ->
           decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num
             ~represents_multiple_values ~dimension mem
-      | Some (CppStdVector _) | Some JavaCollection | None ->
+      | Some (CppStdVector _) | Some JavaCollection | Some JavaInteger | None ->
           (mem, inst_num) )
     | _ ->
         (mem, inst_num)

infer/tests/codetoanalyze/java/bufferoverrun/issues.exp

@@ -7,4 +7,4 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
 codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `this.yy`,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]
-codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int Integer.intValue(),Assignment,<RHS trace>,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]

infer/tests/codetoanalyze/java/performance/ArrayListTest.java

@@ -187,7 +187,8 @@ public class ArrayListTest {
   }
 
   // Control vars include element which is some intValue and list
-  // length. Hence, we get quadratic bound.
+  // length. The result of intValue depends on the list element which
+  // is not modeled. Hence we get bottom for its value ans 0 cost.
   // Simplified version of real code https://fburl.com/a3gge1b7
   public boolean iterate_over_arraylist_shortcut_FP(ArrayList<Integer> list) {
     for (Integer element : list) {

infer/tests/codetoanalyze/java/performance/IntTest.java

@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+class IntTest {
+  void intValue_linear(Integer mKBytesToSend) {
+    for (int count = 0; count < mKBytesToSend; count++) {}
+  }
+
+  static Integer static_Integer;
+
+  static void static_Integer_top() {
+    for (int count = 0; count < static_Integer; count++) {}
+  }
+
+  static void valueOf_linear(int p) {
+    Integer x = p; // call to valueOf
+    for (int count = 0; count < x; count++) {}
+  }
+}

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -32,18 +32,18 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 245,{l.length + list.length},Loop at line 245]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 246,{l.length + list.length},Loop at line 246]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 252,{l.length + list.length},Loop at line 252]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 253,{l.length + list.length},Loop at line 253]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 227,{list.length},Loop at line 227]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 228,{list.length},Loop at line 228]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), degree = 1,{list.length + 5},Loop at line 238,{list.length + 4},Loop at line 238]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), degree = 1,{list.length + 5},Loop at line 239,{list.length + 4},Loop at line 239]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 14]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 3 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2,{-Integer.intValue().lb + 11},Loop at line 193,{list.length},Loop at line 193,{-Integer.intValue().lb + 11},Loop at line 193,{list.length - 1},Loop at line 193]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, []
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ (list1.length - 1) + 3 ⋅ list1.length, degree = 1,{list1.length},Loop at line 184,{list1.length - 1},Loop at line 184]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 19]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},Loop at line 176,{list.length - 1},Loop at line 176]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},Loop at line 170,{list.length - 1},Loop at line 170]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.max_linear(java.util.ArrayList):Person, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length, degree = 1,{people.length},Modeled call to Collections.max]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (this.list.length - 1) + 3 ⋅ this.list.length, degree = 1,{this.list.length},Loop at line 216,{this.list.length - 1},Loop at line 216]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (this.list.length - 1) + 3 ⋅ this.list.length, degree = 1,{this.list.length},Loop at line 217,{this.list.length - 1},Loop at line 217]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},Modeled call to Collections.sort,{list.length},Modeled call to Collections.sort]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sort_comparator_nlogn(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), degree = 1 + 1⋅log,{people.length},Modeled call to Collections.sort,{people.length},Modeled call to Collections.sort]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12]
@@ -108,6 +108,10 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 545, degree = 0]
 codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 15]
 codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a, degree = 1,{test.a},Loop at line 16]
+codetoanalyze/java/performance/IntTest.java, IntTest.intValue_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ mKBytesToSend + 3 ⋅ (1+max(0, mKBytesToSend)), degree = 1,{1+max(0, mKBytesToSend)},Loop at line 9,{mKBytesToSend},Loop at line 9]
+codetoanalyze/java/performance/IntTest.java, IntTest.static_Integer_top():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 15]
+codetoanalyze/java/performance/IntTest.java, IntTest.static_Integer_top():void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/java/performance/IntTest.java, IntTest.valueOf_linear(int):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p + 3 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},Loop at line 20,{p},Loop at line 20]
 codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1,{max(1, k)},Loop at line 58,{k - 1},Loop at line 58]
 codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 31]
 codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,<RHS trace>,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32]