From 42c4fde7209c55d37e898638a68189891730c7d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 14 Oct 2019 11:55:35 -0700 Subject: [PATCH] [impurity] Add initial Java support and don't run pulse twice Summary: Let's add basic Java support to impurity checker. Since impurity checker relies on pulse, we need to add Java with Pulse callback as well. Pulse doesn't officially support Java yet, but we can enable it for impurity checker for now. Many Java primitives/operations are not yet modeled (such as creation of new objects, support for collections etc.). Still, it is good to run impurity checker on the existing tests of the purity checker. Also, it is nice to see that we can identify most of the impure functions correctly in the purity dir. There are a lot of FNs though. Reviewed By: skcho Differential Revision: D17906237 fbshipit-source-id: 15308d285 --- Makefile | 1 + infer/src/checkers/registerCheckers.ml | 8 +- .../java/impurity/GlobalTest.java | 45 +++++ .../java/impurity/Localities.java | 156 ++++++++++++++++++ .../codetoanalyze/java/impurity/Makefile | 13 ++ .../java/impurity/PurityModeled.java | 18 ++ .../codetoanalyze/java/impurity/Test.java | 91 ++++++++++ .../codetoanalyze/java/impurity/issues.exp | 20 +++ 8 files changed, 350 insertions(+), 2 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/impurity/GlobalTest.java create mode 100644 infer/tests/codetoanalyze/java/impurity/Localities.java create mode 100644 infer/tests/codetoanalyze/java/impurity/Makefile create mode 100644 infer/tests/codetoanalyze/java/impurity/PurityModeled.java create mode 100644 infer/tests/codetoanalyze/java/impurity/Test.java create mode 100644 infer/tests/codetoanalyze/java/impurity/issues.exp 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]