[pulse] Add more models for Java

Summary: Adding naive models.

Reviewed By: skcho

Differential Revision: D19743521

fbshipit-source-id: a5a080a85

infer/src/pulse/PulseModels.ml

@@ -354,10 +354,26 @@ module StdVector = struct
       reallocate_internal_array [crumb] vector PushBack location astate >>| List.return
 end
 
+module JavaCollection = struct
+  let set coll index new_elem : model =
+   fun ~caller_summary:_ location ~ret astate ->
+    let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in
+    StdVector.element_of_internal_array location coll (fst index) astate
+    >>= fun (astate, ((old_addr, old_hist) as old_elem)) ->
+    PulseOperations.write_deref location ~ref:new_elem
+      ~obj:(old_addr, ValueHistory.Assignment location :: old_hist)
+      astate
+    >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem
+    >>| fun astate -> [PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate]
+end
+
+module StringSet = Caml.Set.Make (String)
+
 module ProcNameDispatcher = struct
   let dispatch : (Tenv.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
     let match_builtin builtin _ s = String.equal s (Procname.get_method builtin) in
+    let pushback_modeled = StringSet.of_list ["add"; "put"; "addAll"; "putAll"; "remove"] in
     make_dispatcher
       [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
       ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
@@ -422,19 +438,35 @@ module ProcNameDispatcher = struct
       ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload
         $--> StdVector.invalidate_references ShrinkToFit
       ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_collection
+        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+        <>$ capt_arg_payload $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload
+        $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back
+      ; +PatternMatch.implements_map &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back
       ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve
       ; +PatternMatch.implements_collection
         &:: "get" <>$ capt_arg_payload $+ capt_arg_payload
         $--> StdVector.at ~desc:"Collection.get()"
+      ; +PatternMatch.implements_list &:: "set" <>$ capt_arg_payload $+ capt_arg_payload
+        $+ capt_arg_payload $--> JavaCollection.set
       ; +PatternMatch.implements_iterator &:: "hasNext"
         &--> Misc.nondet ~fn_name:"Iterator.hasNext()"
+      ; +PatternMatch.implements_enumeration
+        &:: "hasMoreElements"
+        &--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()"
       ; +PatternMatch.implements_lang "Object"
         &:: "equals"
         &--> Misc.nondet ~fn_name:"Object.equals"
       ; +PatternMatch.implements_lang "Iterable"
         &:: "iterator" <>$ capt_arg_payload $+...$--> Misc.id_first_arg
       ; ( +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload
-        $!--> fun x -> StdVector.at ~desc:"Iterator.next" x (AbstractValue.mk_fresh (), []) ) ]
+        $!--> fun x -> StdVector.at ~desc:"Iterator.next" x (AbstractValue.mk_fresh (), []) )
+      ; ( +PatternMatch.implements_enumeration
+        &:: "nextElement" <>$ capt_arg_payload
+        $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), [])
+        ) ]
 end
 
 let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args

infer/tests/codetoanalyze/java/impurity/PurityModeled.java

@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  */
 import java.util.ArrayList;
+import java.util.Enumeration;
+import java.util.Iterator;
 
 class PurityModeled {
 
@@ -51,4 +53,32 @@ class PurityModeled {
   void list_size_pure(ArrayList<String> list) {
     for (int i = 0; i < list.size(); i++) {}
   }
+
+  void list_add_impure(ArrayList<String> list) {
+    list.add("a");
+  }
+
+  void list_addall_impure(ArrayList<String> list1, ArrayList<String> list2) {
+    list1.addAll(list2);
+  }
+
+  void enum_loop_pure(Enumeration<String> e) {
+
+    for (; e.hasMoreElements(); ) {
+      Object o = e.nextElement();
+    }
+  }
+
+  void remove_impure(Iterator<String> i) {
+    while (i.hasNext()) {
+      if (i.next().equals("Orange")) {
+        i.remove();
+        break;
+      }
+    }
+  }
+
+  void list_set_impure(ArrayList<String> list) {
+    list.set(0, "e");
+  }
 }

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

@@ -16,8 +16,12 @@ codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(j
 codetoanalyze/java/impurity/Localities.java, Localities.newHashCode_impure():int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.newHashCode_impure(),call to skipped function int Object.hashCode() occurs here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),call to skipped function void System.arraycopy(Object,int,Object,int,int) occurs here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_add_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_add_impure(ArrayList),parameter `list` of void PurityModeled.list_add_impure(ArrayList),parameter `list` modified here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure(java.util.ArrayList,java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1` of void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1` modified here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_set_impure(ArrayList),parameter `list` of void PurityModeled.list_set_impure(ArrayList),parameter `list` was potentially invalidated by `std::vector::assign()` here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_impure():double, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double PurityModeled.math_random_impure(),call to skipped function double Math.random() occurs here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here]
+codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` of void PurityModeled.remove_impure(Iterator),parameter `i` modified here]
 codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),call to skipped function void PrintStream.write(byte[],int,int) occurs here]
 codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` accessed here,global variable `Test` modified here]
 codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here]