diff --git a/Makefile b/Makefile index 71d53b4cb..dc4893e32 100644 --- a/Makefile +++ b/Makefile @@ -154,6 +154,7 @@ DIRECT_TESTS += \ java_nullsafe-default \ java_hoisting \ java_hoistingExpensive \ + java_impurity \ java_inefficientKeysetIterator \ java_infer \ java_litho \ diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index ed9b5a469..7e7583d36 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -81,7 +81,11 @@ let all_checkers = ; callbacks= [ (Procedure NullabilitySuggest.checker, Language.Java) ; (Procedure NullabilitySuggest.checker, Language.Clang) ] } - ; {name= "pulse"; active= Config.pulse; callbacks= [(Procedure Pulse.checker, Language.Clang)]} + ; { name= "pulse" + ; active= Config.pulse || Config.impurity + ; callbacks= + (Procedure Pulse.checker, Language.Clang) + :: (if Config.impurity then [(Procedure Pulse.checker, Language.Java)] else []) } ; { name= "quandary" ; active= Config.quandary || Config.quandaryBO ; callbacks= @@ -131,7 +135,7 @@ let all_checkers = ; { name= "impurity" ; active= Config.impurity ; callbacks= - [(Procedure Impurity.checker, Language.Clang); (Procedure Pulse.checker, Language.Clang)] + [(Procedure Impurity.checker, Language.Java); (Procedure Impurity.checker, Language.Clang)] } ; { name= "purity" ; active= Config.purity || Config.loop_hoisting diff --git a/infer/tests/codetoanalyze/java/impurity/GlobalTest.java b/infer/tests/codetoanalyze/java/impurity/GlobalTest.java new file mode 100644 index 000000000..af7574059 --- /dev/null +++ b/infer/tests/codetoanalyze/java/impurity/GlobalTest.java @@ -0,0 +1,45 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +class GlobalTest { + public static int s = 0; + public static Foo foo; + + class Foo { + + int x = 0; + // modifies global var 's' hence impure + void set_impure() { + s = 10; + } + } + + void incr(Foo foo, int i) { + foo.x += i; + } + + // calls foo which modifies global var + void call_set_impure() { + Foo f = new Foo(); + f.set_impure(); + } + + // foo is global which is modified by incr. + void global_mod_via_argument_passing_impure(int size, Foo f) { + for (int i = 0; i < size; i++) { + incr(foo, i); + } + } + + // aliased_foo is aliasing a global and then is modified by incr. + void global_mod_via_argument_passing_impure_aliased(int size, Foo f) { + Foo aliased_foo = foo; // Inferbo can't recognize aliasing here + // and assumes aliased_foo is in [-oo,+oo] not in foo + for (int i = 0; i < size; i++) { + incr(aliased_foo, i); + } + } +} diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java new file mode 100644 index 000000000..67ebc5221 --- /dev/null +++ b/infer/tests/codetoanalyze/java/impurity/Localities.java @@ -0,0 +1,156 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * 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(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_FN(ArrayList list) { + Iterator listIterator = list.iterator(); + while (listIterator.hasNext()) { + Foo foo = listIterator.next(); + foo.x = 0; + } + } + + // @mod:{list} + void incrementAll_impure_FN(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_FN(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_FN() { + 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; + } + + // This behavior seems to be different than C++ + // @pure, @loc:{} + boolean copy_ref_pure_FP(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/impurity/Makefile b/infer/tests/codetoanalyze/java/impurity/Makefile new file mode 100644 index 000000000..1ef6a83aa --- /dev/null +++ b/infer/tests/codetoanalyze/java/impurity/Makefile @@ -0,0 +1,13 @@ +# Copyright (c) Facebook, Inc. and its affiliates. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +INFER_OPTIONS = --impurity-only --debug-exceptions +INFERPRINT_OPTIONS = --issues-tests +SOURCES = $(wildcard *.java) + +include $(TESTS_DIR)/javac.make diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java new file mode 100644 index 000000000..f844127c9 --- /dev/null +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -0,0 +1,18 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +class PurityModeled { + + double math_random_impure_FN() { + return Math.random(); + } + + void arraycopy_pure(int[] src) { + int[] dst = {5, 10, 20, 30, 40, 50}; + // copies an array from the specified source array + System.arraycopy(src, 0, dst, 0, 1); + } +} diff --git a/infer/tests/codetoanalyze/java/impurity/Test.java b/infer/tests/codetoanalyze/java/impurity/Test.java new file mode 100644 index 000000000..c032b987c --- /dev/null +++ b/infer/tests/codetoanalyze/java/impurity/Test.java @@ -0,0 +1,91 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * 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 Test { + + private int a = 0; + static Integer[] global_arr; + + void Test(int size) { + global_arr = new Integer[size]; + } + + void set_impure(int x, int y) { + a = x + y; + } + + void global_array_set_impure(int x, int y) { + global_arr[0] = x + y; + } + + int local_write_pure(int x, int y) { + int k = x + y; + k++; + return k; + } + + void call_pure_pure(int size) { + for (int i = 0; i < size; i++) { + local_write_pure(i, size); + } + } + + void call_impure_impure(int size) { + int d = 0; + for (int i = 0; i < size; i++) { + set_impure(i, size); + } + } + + // no change to outside state, the local allocation is ok. + int local_alloc_pure(int x, int y) { + ArrayList list = new ArrayList(x + y); + for (Integer el : list) { + call_pure_pure(el); + } + return list.size(); + } + + void parameter_field_write_impure(Test test, boolean b) { + int c = b ? 0 : 1; + test.a = c; + } + + int parameter_field_access_pure(Test test) { + return test.a; + } + + // expected to be impure since y points to x + void local_field_write_impure(Test x) { + Test y = x; + y.a = 0; + } + + void swap_impure(int[] array, int i, int j) { + int tmp = array[i]; + array[i] = array[j]; + array[j] = tmp; + } + + void alias_impure(int[] array, int i, int j) { + int[] a = array; + a[j] = i; + } + + // Currently, we can't distinguish between returning new Objects or + // creating new Objects locally. Ideally, the latter should be fine + // as long as it doesn't leak to the result. + public ArrayList emptyList_impure_FN() { + return new ArrayList(); + } + + // All unmodeled calls should be considered impure + static long systemNanoTime_impure_FN() { + return System.nanoTime(); + } +} diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp new file mode 100644 index 000000000..0c4078e73 --- /dev/null +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -0,0 +1,20 @@ +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest$Foo.set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest$Foo.set_impure(),global var 'GlobalTest' is modified at line 16] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.call_set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.call_set_impure(),global var 'GlobalTest' is modified when calling `GlobalTest$Foo.set_impure()` at line 27,global var 'GlobalTest' is modified at line 16] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo),global var 'GlobalTest' is modified when calling `GlobalTest.incr(...)` at line 33,global var 'GlobalTest' is modified at line 21] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo),global var 'GlobalTest' is modified when calling `GlobalTest.incr(...)` at line 42,global var 'GlobalTest' is modified at line 21] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter 'foo' is modified at line 21] +codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter 'this' is modified at line 67] +codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter 'this' is modified at line 57] +codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter 'a' is modified at line 150] +codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_pure_FP(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_pure_FP(int[],int),parameter 'a' is modified at line 142] +codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter 'array' is modified at line 125] +codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter 'array' is modified at line 118] +codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter 'array' is modified at line 134,parameter 'array' is modified at line 132] +codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global var 'Test' is modified at line 15] +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' is modified at line 77] +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' is modified when calling `Test.set_impure(...)` at line 41,parameter 'this' is modified at line 19] +codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.global_array_set_impure(int,int),global var 'Test' is modified at line 23] +codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter 'x' is modified at line 66] +codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter 'test' is modified at line 56] +codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter 'this' is modified at line 19] +codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter 'array' is modified at line 71,parameter 'array' is modified at line 71,parameter 'array' is modified at line 72,parameter 'array' is modified at line 71]