[pulse] Don't write through pointer arguments in Java

Summary:
Pulse has an extra invalidation mechanism (introduced in D18726203) to prevent something invalid (e.g. `null`) to be passed by reference to an initialisation function. Therefore, it havocs formals passed by reference to skipped functions. However, I don't think this makes sense in Java. So, let's turn it off.

A nice consequence of this is that in impurity analysis, we do not consider functions that call skipped library calls with object arguments as writing to their formals.

Reviewed By: skcho

Differential Revision: D19697110

fbshipit-source-id: 6e3a71f2a

infer/src/pulse/PulseOperations.ml

@@ -500,8 +500,12 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate =
   let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate =
     (* We should not havoc when the corresponding formal is a
        pointer to const *)
-    if Typ.is_pointer actual_typ && not (is_ptr_to_const formal_typ_opt) then
-      (* HACK: write through the pointer even if it is invalid. This is to avoid raising issues when
+    if
+      (not (Language.curr_language_is Java))
+      && Typ.is_pointer actual_typ
+      && not (is_ptr_to_const formal_typ_opt)
+    then
+      (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when
          havoc'ing pointer parameters (which normally causes a [check_valid] call. *)
       let fresh_value = AbstractValue.mk_fresh () in
       Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate

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

@@ -4,6 +4,8 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
+import java.util.ArrayList;
+
 class PurityModeled {
 
   double math_random_impure() {
@@ -45,4 +47,8 @@ class PurityModeled {
 
     return p;
   }
+
+  void list_size_pure(ArrayList<String> list) {
+    for (int i = 0; i < list.size(); i++) {}
+  }
 }

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

@@ -14,11 +14,11 @@ codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.
 codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list` of void Localities.modify_first_el_impure(ArrayList),passed as argument to `Collection.get()` (modelled),return from call to `Collection.get()` (modelled),assigned,assigned,parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),parameter `list` of void Localities.modify_via_call_impure(ArrayList),passed as argument to `Localities$Foo Localities.get_first_pure(ArrayList)`,return from call to `Localities$Foo Localities.get_first_pure(ArrayList)`,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here]
 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[]),parameter `src` of void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` modified here,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(),global variable `java.lang.System` accessed here,when calling `void PurityModeled.write_impure()` here,global variable `java.lang.System` accessed here,global variable `lang.System` modified here,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.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.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),global variable `java.lang.System` accessed here,when calling `void PurityModeled.call_write_impure()` here,global variable `java.lang.System` accessed here,when calling `void PurityModeled.write_impure()` here,global variable `java.lang.System` accessed here,global variable `lang.System` modified here,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.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),global variable `java.lang.System` accessed here,global variable `lang.System` modified here,call to skipped function void PrintStream.write(byte[],int,int) 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.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]
 codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),parameter `this` of void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` of void Test.set_impure(int,int),parameter `this` modified here]