diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 73df96076..8ea12c753 100644 --- a/infer/src/checkers/purity.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/purity/Localities.java b/infer/tests/codetoanalyze/java/purity/Localities.java new file mode 100644 index 000000000..fde062c77 --- /dev/null +++ b/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 list) { + Iterator listIterator = list.iterator(); + while (listIterator.hasNext()) { + Integer el = listIterator.next(); + if (i.equals(el)) { + return true; + } + } + return false; + } + + // @mod:{list} + void makeAllZero_impure(ArrayList list) { + Iterator listIterator = list.iterator(); + while (listIterator.hasNext()) { + Foo foo = listIterator.next(); + foo.x = 0; + } + } + + // @mod:{list} + void incrementAll_impure(ArrayList list) { + Iterator listIterator = list.iterator(); + while (listIterator.hasNext()) { + Foo foo = listIterator.next(); + foo.inc_impure(); + } + } + + // @pure + void call_impure_with_fresh_args_pure() { + ArrayList list = new ArrayList(); + 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 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; + } +} diff --git a/infer/tests/codetoanalyze/java/purity/issues.exp b/infer/tests/codetoanalyze/java/purity/issues.exp index d5345a0f5..e318d513a 100644 --- a/infer/tests/codetoanalyze/java/purity/issues.exp +++ b/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)]