From cd1c9750f40fe7abb819cbd3ae1a752bbe7ec3d5 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 16 Dec 2016 14:02:03 -0800 Subject: [PATCH] [infer] models for common types of Java Lists Reviewed By: cristianoc Differential Revision: D4325120 fbshipit-source-id: 8af01d3 --- .../java/src/java/util/AbstractList.java | 65 +++++++++++++++ .../models/java/src/java/util/ArrayList.java | 44 +++++++++++ .../models/java/src/java/util/LinkedList.java | 44 +++++++++++ infer/models/java/src/java/util/Vector.java | 2 +- infer/tests/build_systems/ant/issues.exp | 3 + infer/tests/build_systems/buck/issues.exp | 3 + .../tests/codetoanalyze/java/infer/Lists.java | 79 +++++++++++++++++++ .../tests/codetoanalyze/java/infer/issues.exp | 4 + 8 files changed, 243 insertions(+), 1 deletion(-) create mode 100644 infer/models/java/src/java/util/AbstractList.java create mode 100644 infer/models/java/src/java/util/ArrayList.java create mode 100644 infer/models/java/src/java/util/LinkedList.java create mode 100644 infer/tests/codetoanalyze/java/infer/Lists.java diff --git a/infer/models/java/src/java/util/AbstractList.java b/infer/models/java/src/java/util/AbstractList.java new file mode 100644 index 000000000..996f08c7e --- /dev/null +++ b/infer/models/java/src/java/util/AbstractList.java @@ -0,0 +1,65 @@ +/* + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package java.util; + +import com.facebook.infer.builtins.InferUndefined; + +// could make List an abstract class directly instead, but that breaks other models +public abstract class AbstractList extends AbstractCollection implements List { + + // need three-value state for unknown (-1), false (0), or true (1) + // the reason we can't use a bool is that we want to return either true or false each time we call + // isEmpty, and we want to get the same result each time + private int mIsEmpty; + + native T any(); + + public AbstractList() { + mIsEmpty = 1; + } + + @Override + public boolean isEmpty() { + if (mIsEmpty < 0) { + if (InferUndefined.boolean_undefined()) { + mIsEmpty = 1; + } else { + mIsEmpty = 0; + } + } + return mIsEmpty == 1; + } + + @Override + public void add(int index, T toAdd) { + mIsEmpty = 0; + } + + @Override + public T remove(int index) { + mIsEmpty = -1; + return any(); + } + + @Override + public boolean remove(Object o) { + boolean result = InferUndefined.boolean_undefined(); + if (result) { + mIsEmpty = -1; + } + return result; + } + + @Override + public void clear() { + mIsEmpty = 1; + } + +} diff --git a/infer/models/java/src/java/util/ArrayList.java b/infer/models/java/src/java/util/ArrayList.java new file mode 100644 index 000000000..9d63c4364 --- /dev/null +++ b/infer/models/java/src/java/util/ArrayList.java @@ -0,0 +1,44 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package java.util; + +import java.io.Serializable; + +// abstract so we don't have to implement every method of List +public abstract class ArrayList + extends AbstractList + implements List, RandomAccess, Cloneable, Serializable { + + @Override + public boolean isEmpty() { + return super.isEmpty(); + } + + @Override + public void add(int index, T toAdd) { + super.add(index, toAdd); + } + + @Override + public T remove(int index) { + return super.remove(index); + } + + @Override + public boolean remove(Object o) { + return super.remove(o); + } + + @Override + public void clear() { + super.clear(); + } + +} diff --git a/infer/models/java/src/java/util/LinkedList.java b/infer/models/java/src/java/util/LinkedList.java new file mode 100644 index 000000000..92f82b423 --- /dev/null +++ b/infer/models/java/src/java/util/LinkedList.java @@ -0,0 +1,44 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package java.util; + +import java.io.Serializable; + +// abstract so we don't have to implement every method of List +public abstract class LinkedList + extends AbstractSequentialList + implements Serializable, Cloneable, Iterable, Collection, Deque, List, Queue { + + @Override + public boolean isEmpty() { + return super.isEmpty(); + } + + @Override + public void add(int index, T toAdd) { + super.add(index, toAdd); + } + + @Override + public T remove(int index) { + return super.remove(index); + } + + @Override + public boolean remove(Object o) { + return super.remove(o); + } + + @Override + public void clear() { + super.clear(); + } + +} diff --git a/infer/models/java/src/java/util/Vector.java b/infer/models/java/src/java/util/Vector.java index f0da4db63..54eb0482c 100644 --- a/infer/models/java/src/java/util/Vector.java +++ b/infer/models/java/src/java/util/Vector.java @@ -11,7 +11,7 @@ package java.util; import com.facebook.infer.builtins.InferUndefined; -public class Vector extends AbstractList { +public abstract class Vector extends AbstractList { protected Object[] elementData; diff --git a/infer/tests/build_systems/ant/issues.exp b/infer/tests/build_systems/ant/issues.exp index a9ebf2a58..66b294d8c 100644 --- a/infer/tests/build_systems/ant/issues.exp +++ b/infer/tests/build_systems/ant/issues.exp @@ -71,6 +71,9 @@ codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getTwoIntegers codetoanalyze/java/infer/IntegerExample.java, void IntegerExample.testIntegerEqualsBad(), 6, NULL_DEREFERENCE, [start of procedure testIntegerEqualsBad(),Taking true branch] codetoanalyze/java/infer/InvokeDynamic.java, int InvokeDynamic.lambda$npeInLambdaBad$1(String,String), 1, NULL_DEREFERENCE, [start of procedure lambda$npeInLambdaBad$1(...)] codetoanalyze/java/infer/InvokeDynamic.java, void InvokeDynamic.invokeDynamicThenNpeBad(List), 5, NULL_DEREFERENCE, [start of procedure invokeDynamicThenNpeBad(...)] +codetoanalyze/java/infer/Lists.java, void Lists.clearCausesEmptinessNPE(List,int), 5, NULL_DEREFERENCE, [start of procedure clearCausesEmptinessNPE(...),Taking true branch,Taking true branch] +codetoanalyze/java/infer/Lists.java, void Lists.getElementNPE(List), 4, NULL_DEREFERENCE, [start of procedure getElementNPE(...),Taking false branch,start of procedure getElement(...),Taking true branch,return from a call to Object Lists.getElement(List)] +codetoanalyze/java/infer/Lists.java, void Lists.removeInvalidatesNonEmptinessNPE(List,int), 5, NULL_DEREFERENCE, [start of procedure removeInvalidatesNonEmptinessNPE(...),Taking true branch,Taking true branch] codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.hashmapNPE(HashMap,Object), 1, NULL_DEREFERENCE, [start of procedure hashmapNPE(...)] codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.nullTryLock(FileChannel), 2, NULL_DEREFERENCE, [start of procedure nullTryLock(...)] codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.testSystemGetPropertyArgument(), 1, NULL_DEREFERENCE, [start of procedure testSystemGetPropertyArgument()] diff --git a/infer/tests/build_systems/buck/issues.exp b/infer/tests/build_systems/buck/issues.exp index dbde139dd..fff3cc519 100644 --- a/infer/tests/build_systems/buck/issues.exp +++ b/infer/tests/build_systems/buck/issues.exp @@ -71,6 +71,9 @@ infer/tests/codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.ge infer/tests/codetoanalyze/java/infer/IntegerExample.java, void IntegerExample.testIntegerEqualsBad(), 6, NULL_DEREFERENCE, [start of procedure testIntegerEqualsBad(),Taking true branch] infer/tests/codetoanalyze/java/infer/InvokeDynamic.java, int InvokeDynamic.lambda$npeInLambdaBad$1(String,String), 1, NULL_DEREFERENCE, [start of procedure lambda$npeInLambdaBad$1(...)] infer/tests/codetoanalyze/java/infer/InvokeDynamic.java, void InvokeDynamic.invokeDynamicThenNpeBad(List), 5, NULL_DEREFERENCE, [start of procedure invokeDynamicThenNpeBad(...)] +infer/tests/codetoanalyze/java/infer/Lists.java, void Lists.clearCausesEmptinessNPE(List,int), 5, NULL_DEREFERENCE, [start of procedure clearCausesEmptinessNPE(...),Taking true branch,Taking true branch] +infer/tests/codetoanalyze/java/infer/Lists.java, void Lists.getElementNPE(List), 4, NULL_DEREFERENCE, [start of procedure getElementNPE(...),Taking false branch,start of procedure getElement(...),Taking true branch,return from a call to Object Lists.getElement(List)] +infer/tests/codetoanalyze/java/infer/Lists.java, void Lists.removeInvalidatesNonEmptinessNPE(List,int), 5, NULL_DEREFERENCE, [start of procedure removeInvalidatesNonEmptinessNPE(...),Taking true branch,Taking true branch] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.hashmapNPE(HashMap,Object), 1, NULL_DEREFERENCE, [start of procedure hashmapNPE(...)] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.nullTryLock(FileChannel), 2, NULL_DEREFERENCE, [start of procedure nullTryLock(...)] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.testSystemGetPropertyArgument(), 1, NULL_DEREFERENCE, [start of procedure testSystemGetPropertyArgument()] diff --git a/infer/tests/codetoanalyze/java/infer/Lists.java b/infer/tests/codetoanalyze/java/infer/Lists.java new file mode 100644 index 000000000..ff7d8f196 --- /dev/null +++ b/infer/tests/codetoanalyze/java/infer/Lists.java @@ -0,0 +1,79 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package codetoanalyze.java.infer; + +import java.util.ArrayList; +import java.util.List; + +class Lists { + + void emptyRemembersOk(List l) { + boolean empty = l.isEmpty(); + Object o = null; + if (empty != l.isEmpty()) { + o.toString(); + } + } + + void removeInvalidatesNonEmptinessNPE(List l, int i) { + if (!l.isEmpty()) { + l.remove(i); + Object o = null; + if (l.isEmpty()) { + o.toString(); + } + } + } + + void clearCausesEmptinessNPE(List l, int i) { + if (!l.isEmpty()) { + l.clear(); + Object o = null; + if (l.isEmpty()) { + o.toString(); + } + } + } + + // it would be too noisy to report here + void plainGetOk(List l, int i) { + l.get(i).toString(); + } + + Object getElement(List l) { + return l.isEmpty() ? null : l.get(0); + } + + void getElementOk(List l) { + if (l.isEmpty()) { + return; + } + getElement(l).toString(); + } + + void getElementNPE(List l) { + if (!l.isEmpty()) { + return; + } + getElement(l).toString(); + } + + // don't fully understand why we don't get this one; model should allow it + void FN_addInvalidatesEmptinessNPE(List l) { + if (l.isEmpty()) { + l.add(0, new Object()); + Object o = null; + if (!l.isEmpty()) { + o.toString(); + } + } + } + +} diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index eeb9e40c8..db873ddf6 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -146,6 +146,10 @@ codetoanalyze/java/infer/InvokeDynamic.java, int InvokeDynamic.lambda$npeInLambd codetoanalyze/java/infer/InvokeDynamic.java, void InvokeDynamic.invokeDynamicThenNpeBad(List), 5, NULL_DEREFERENCE, [start of procedure invokeDynamicThenNpeBad(...)] codetoanalyze/java/infer/JunitAssertion.java, void JunitAssertion.consistentAssertion(JunitAssertion$A), 1, PRECONDITION_NOT_MET, [start of procedure consistentAssertion(...),Taking false branch] codetoanalyze/java/infer/JunitAssertion.java, void JunitAssertion.inconsistentAssertion(JunitAssertion$A), 2, NULL_DEREFERENCE, [start of procedure inconsistentAssertion(...),Taking false branch] +codetoanalyze/java/infer/Lists.java, void Lists.clearCausesEmptinessNPE(List,int), 5, NULL_DEREFERENCE, [start of procedure clearCausesEmptinessNPE(...),Taking true branch,Taking true branch] +codetoanalyze/java/infer/Lists.java, void Lists.getElementNPE(List), 4, NULL_DEREFERENCE, [start of procedure getElementNPE(...),Taking false branch,start of procedure getElement(...),Taking true branch,return from a call to Object Lists.getElement(List)] +codetoanalyze/java/infer/Lists.java, void Lists.removeInvalidatesNonEmptinessNPE(List,int), 2, RETURN_VALUE_IGNORED, [start of procedure removeInvalidatesNonEmptinessNPE(...),Taking true branch] +codetoanalyze/java/infer/Lists.java, void Lists.removeInvalidatesNonEmptinessNPE(List,int), 5, NULL_DEREFERENCE, [start of procedure removeInvalidatesNonEmptinessNPE(...),Taking true branch,Taking true branch] codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.hashmapNPE(HashMap,Object), 1, NULL_DEREFERENCE, [start of procedure hashmapNPE(...)] codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.nullTryLock(FileChannel), 2, NULL_DEREFERENCE, [start of procedure nullTryLock(...)] codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.testSystemGetPropertyArgument(), 1, NULL_DEREFERENCE, [start of procedure testSystemGetPropertyArgument()]