[purity] Add tests for locality

Reviewed By: ngorogiannis

Differential Revision: D15373797

fbshipit-source-id: 8cb0de6b5

infer/src/checkers/purity.ml

@@ -233,4 +233,9 @@ let checker {Callbacks.tenv; summary; proc_desc; integer_type_widths} : Summary.
   let get_callee_summary = Payload.read proc_desc in
   let astate = compute_summary proc_desc tenv get_callee_summary inferbo_invariant_map in
   report_errors proc_desc astate summary ;
-  match astate with Some astate -> Payload.update_summary astate summary | None -> summary
+  match astate with
+  | Some astate ->
+      debug "Purity summary :%a \n" PurityDomain.pp astate ;
+      Payload.update_summary astate summary
+  | None ->
+      summary

infer/tests/codetoanalyze/java/purity/Localities.java

@@ -0,0 +1,155 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * 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;
+import java.util.Iterator;
+
+class Localities {
+  // @pure
+  boolean contains_pure_FN(Integer i, ArrayList<Integer> list) {
+    Iterator<Integer> listIterator = list.iterator();
+    while (listIterator.hasNext()) {
+      Integer el = listIterator.next();
+      if (i.equals(el)) {
+        return true;
+      }
+    }
+    return false;
+  }
+
+  // @mod:{list}
+  void makeAllZero_impure(ArrayList<Foo> list) {
+    Iterator<Foo> listIterator = list.iterator();
+    while (listIterator.hasNext()) {
+      Foo foo = listIterator.next();
+      foo.x = 0;
+    }
+  }
+
+  // @mod:{list}
+  void incrementAll_impure(ArrayList<Foo> list) {
+    Iterator<Foo> listIterator = list.iterator();
+    while (listIterator.hasNext()) {
+      Foo foo = listIterator.next();
+      foo.inc_impure();
+    }
+  }
+
+  // @pure
+  void call_impure_with_fresh_args_pure() {
+    ArrayList<Foo> list = new ArrayList<Foo>();
+    makeAllZero_impure(list);
+  }
+
+  class Bar {
+    int p;
+  }
+
+  class Foo {
+    int x;
+    Bar bar;
+
+    // @mod:{this}
+    void inc_impure() {
+      x++;
+    }
+  }
+
+  class Counter {
+
+    int i = 0;
+    // @mod:{this}
+    // only modifies fields of its receiver object
+    void inc_impure() {
+      i++;
+    }
+
+    // @pure, @loc:{}
+    int get_i_pure() {
+      return i;
+    }
+  }
+
+  // @pure, @loc:{}
+  int length_pure(ArrayList<Integer> list) {
+    Counter c = new Counter();
+    for (Integer i : list) {
+      c.inc_impure();
+    }
+    return c.i;
+  }
+
+  class HasCounter {
+    Counter counter = new Counter();
+
+    // @loc:{this}
+    Counter getCounter_pure() {
+      return counter;
+    }
+  }
+
+  // @loc:{}
+  public static int[] setFreshArrayEntry_pure(int index, int value) {
+    int[] arr = new int[] {1, 2, 3};
+    if (index > 0) {
+      arr[index % 3] = value;
+    }
+    return arr;
+  }
+
+  // @loc: T
+  private int newHashCode_impure() {
+    return new Object().hashCode();
+  }
+
+  // @loc:{c}
+  HasCounter mkHC_pure(Counter c) {
+    HasCounter hc = new HasCounter();
+    hc.counter = c;
+    return hc;
+  }
+
+  // @mod:{array}, @loc:{array,f}
+  Foo get_f_impure(Foo[] array, int i, Foo f) {
+    Foo tmp = array[i];
+    tmp.x = f.x;
+    return tmp;
+  }
+
+  // @mod:{array}, @loc:{array,f}
+  Foo[] get_array_impure(Foo[] array, int i, Foo f) {
+    Foo tmp = array[i];
+    tmp.x = f.x;
+    return array;
+  }
+
+  // @mod:{array}, @loc:{p}
+  Bar get_foo_via_tmp_impure(Foo[] array, int i, Foo f, Foo p) {
+    Foo tmp = array[i];
+    tmp.bar = f.bar;
+    Foo tmp2 = tmp;
+    tmp2.bar = p.bar;
+    return tmp.bar;
+  }
+
+  // @pure, @loc:{}
+  boolean copy_ref_pure_FN(int[] a, int b) {
+    int[] local = a; // copy reference
+    a = new int[1]; //  can't detect that a becomes fresh
+    a[0] = local[0]; // not modification
+    return true;
+  }
+
+  // @mod:{a}, @loc:{}
+  boolean copy_ref_impure(int[] a, int b) {
+    int[] local = a; // copy reference
+    a = new int[1]; // overwrite reference
+    a[0] = local[0]; // not modification
+    local[0] = b; // modify arg a
+    b = a[0]; // not modification
+    return true;
+  }
+}

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

@@ -1,3 +1,9 @@
+codetoanalyze/java/purity/Localities.java, Localities$Counter.get_i_pure():int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Localities$Counter.get_i_pure()]
+codetoanalyze/java/purity/Localities.java, Localities$HasCounter.getCounter_pure():Localities$Counter, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function Localities$Counter Localities$HasCounter.getCounter_pure()]
+codetoanalyze/java/purity/Localities.java, Localities.call_impure_with_fresh_args_pure():void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Localities.call_impure_with_fresh_args_pure()]
+codetoanalyze/java/purity/Localities.java, Localities.length_pure(java.util.ArrayList):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Localities.length_pure(ArrayList)]
+codetoanalyze/java/purity/Localities.java, Localities.mkHC_pure(Localities$Counter):Localities$HasCounter, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function Localities$HasCounter Localities.mkHC_pure(Localities$Counter)]
+codetoanalyze/java/purity/Localities.java, Localities.setFreshArrayEntry_pure(int,int):int[], 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int[] Localities.setFreshArrayEntry_pure(int,int)]
 codetoanalyze/java/purity/Test.java, Test.call_pure_ok(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Test.call_pure_ok(int)]
 codetoanalyze/java/purity/Test.java, Test.emptyList_bad_FP():java.util.ArrayList, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function ArrayList Test.emptyList_bad_FP()]
 codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_alloc_ok(int,int)]