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: 15308d285master
Ezgi Çiçek
5 years ago
committed by
Facebook Github Bot
parent
42470d8809
commit
42c4fde720
@ -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);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -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<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_FN(ArrayList<Foo> list) {
|
||||
Iterator<Foo> listIterator = list.iterator();
|
||||
while (listIterator.hasNext()) {
|
||||
Foo foo = listIterator.next();
|
||||
foo.x = 0;
|
||||
}
|
||||
}
|
||||
|
||||
// @mod:{list}
|
||||
void incrementAll_impure_FN(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_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<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_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;
|
||||
}
|
||||
}
|
||||
@ -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
|
||||
@ -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);
|
||||
}
|
||||
}
|
||||
@ -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<Integer> list = new ArrayList<Integer>(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<Integer> emptyList_impure_FN() {
|
||||
return new ArrayList<Integer>();
|
||||
}
|
||||
|
||||
// All unmodeled calls should be considered impure
|
||||
static long systemNanoTime_impure_FN() {
|
||||
return System.nanoTime();
|
||||
}
|
||||
}
|
||||
@ -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]
|
||||
Loading…
Reference in new issue