[inferbo] Add models for org.json.JSONArray

Reviewed By: jvillard

Differential Revision: D15577727

fbshipit-source-id: 829a93fc0

infer/src/absint/PatternMatch.ml

@@ -90,6 +90,8 @@ let implements_android class_name = implements ("android." ^ class_name)
 
 let implements_jackson class_name = implements ("com.fasterxml.jackson." ^ class_name)
 
+let implements_org_json class_name = implements ("org.json." ^ class_name)
+
 (** The type the method is invoked on *)
 let get_this_type proc_attributes =
   match proc_attributes.ProcAttributes.formals with (_, t) :: _ -> Some t | _ -> None

infer/src/absint/PatternMatch.mli

@@ -52,6 +52,9 @@ val implements_enumeration : Tenv.t -> string -> bool
 val implements_jackson : string -> Tenv.t -> string -> bool
 (** Check whether class implements a class from Jackson *)
 
+val implements_org_json : string -> Tenv.t -> string -> bool
+(** Check whether class implements a class from Json *)
+
 val implements_inject : string -> Tenv.t -> string -> bool
 (** Check whether class implements a Javax Inject *)
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -838,6 +838,10 @@ module Call = struct
       ; -"__new"
         <>$ capt_exp_of_typ (+PatternMatch.implements_map)
         $+...$--> Collection.new_collection
+      ; +PatternMatch.implements_map &:: "size" <>$ capt_exp $!--> Collection.size
+      ; -"__new"
+        <>$ capt_exp_of_typ (+PatternMatch.implements_org_json "JSONArray")
+        $+...$--> Collection.new_collection
       ; -"__new" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
       ; -"__new_array" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
       ; +PatternMatch.implements_arrays &:: "asList" <>$ capt_exp $!--> create_copy_array
@@ -951,6 +955,8 @@ module Call = struct
       ; +PatternMatch.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator
       ; +PatternMatch.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ any_arg
         $--> Collection.put
+      ; +PatternMatch.implements_org_json "JSONArray"
+        &:: "put" <>$ capt_var_exn $+...$--> Collection.put
       ; +PatternMatch.implements_map &:: "putAll" <>$ capt_var_exn $+ capt_exp
         $--> Collection.putAll
       ; +PatternMatch.implements_iterator &:: "hasNext" <>$ capt_exp $!--> Collection.hasNext
@@ -962,5 +968,8 @@ module Call = struct
         &:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp $!--> Collection.addAll_at_index
       ; +PatternMatch.implements_collection &:: "size" <>$ capt_exp $!--> Collection.size
       ; +PatternMatch.implements_pseudo_collection &:: "size" <>$ capt_exp $!--> Collection.size
-      ; +PatternMatch.implements_map &:: "size" <>$ capt_exp $!--> Collection.size ]
+      ; +PatternMatch.implements_org_json "JSONArray"
+        &:: "length" <>$ capt_exp $!--> Collection.size
+      ; +PatternMatch.implements_org_json "JSONArray"
+        &:: "<init>" <>$ capt_var_exn $+ capt_exp $--> Collection.init ]
 end

infer/src/bufferoverrun/bufferOverrunTypModels.ml

@@ -27,4 +27,5 @@ let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher =
   make_dispatcher
     [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> std_array
     ; +PatternMatch.implements_collection &::.*--> collection
-    ; +PatternMatch.implements_iterator &::.*--> collection ]
+    ; +PatternMatch.implements_iterator &::.*--> collection
+    ; +PatternMatch.implements_org_json "JSONArray" &::.*--> collection ]

infer/src/checkers/purityModels.ml

@@ -140,5 +140,9 @@ module ProcName = struct
       ; +PatternMatch.implements_queue &:: "remove" <>--> modifies_first
       ; +PatternMatch.implements_queue &:: "peek" <>--> PurityDomain.pure
       ; +PatternMatch.implements_list &:: "subList" <>--> PurityDomain.pure
-      ; +PatternMatch.implements_arrays &:: "binarySearch" <>--> PurityDomain.pure ]
+      ; +PatternMatch.implements_arrays &:: "binarySearch" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_org_json "JSONArray" &::+ startsWith "get" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_org_json "JSONObject"
+        &::+ startsWith "get" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_org_json "JSONArray" &:: "length" <>--> PurityDomain.pure ]
 end

infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java

@@ -18,9 +18,9 @@ class UnknownCallsTest {
     for (int i = 0; i < length; ++i) {}
   }
 
-  // call to JSONArray.length is not modeled, but we assume it to be
+  public void jsonArray_constant() {
-  // invariant for cost analysis.
+    JSONArray jsonArray = new JSONArray();
-  public void jsonArray(JSONArray jsonArray) {
+    jsonArray.put(1);
     for (int i = 0; i < jsonArray.length(); ++i) {}
   }
 

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

@@ -152,8 +152,7 @@ codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switc
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 52]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray(org.json.JSONArray):void, 0, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ JSONArray.length().ub + 3 ⋅ (1+max(0, JSONArray.length().ub)), degree = 1,{1+max(0, JSONArray.length().ub)},Loop at line 24,{JSONArray.length().ub},Loop at line 24]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ jsonArray.length, degree = 1,{jsonArray.length},Loop at line 18]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ JSONArray.length().ub, degree = 1,{JSONArray.length().ub},Loop at line 18]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},Loop at line 52]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 47]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]