pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] Modeling Java Integer class

Browse Source 
Summary: Adding support for Java Integer class in Pulse.

Reviewed By: ezgicicek

Differential Revision: D25953596

fbshipit-source-id: ce7206db3
master
Gabriela Cunha Sampaio 4 years ago committed by Facebook GitHub Bot
parent e6d50837ba
commit 27acb0fe4e
5 changed files with 187 additions and 23 deletions
Show Stats Download Patch File Download Diff File

67
infer/src/pulse/PulseModels.ml
Unescape View File

@ -962,6 +962,65 @@ module JavaCollection = struct
remove_at coll (index, [])
end
module JavaInteger = struct
let internal_int =
Fieldname.make
(Typ.JavaClass (JavaClassName.make ~package:(Some "java.lang") ~classname:"Integer"))
"__infer_model_backing_int"
let load_backing_int location this astate =
let* astate, obj = PulseOperations.eval_access Read location this Dereference astate in
let* astate, int_addr =
PulseOperations.eval_access Read location obj (FieldAccess internal_int) astate
in
let+ astate, int_val = PulseOperations.eval_access Read location int_addr Dereference astate in
(astate, int_addr, int_val)
let construct this_address init_value event location astate =
let this = (AbstractValue.mk_fresh (), [event]) in
let* astate, int_field =
PulseOperations.eval_access Write location this (FieldAccess internal_int) astate
in
let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in
PulseOperations.write_deref location ~ref:this_address ~obj:this astate
let constructor this_address init_value : model =
fun _ ~callee_procname:_ location ~ret:_ astate ->
let event = ValueHistory.Call {f= Model "Integer.init"; location; in_call= []} in
let+ state = construct this_address init_value event location astate in
[ExecutionDomain.continue state]
let equals this arg : model =
fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
let* astate, _int_addr1, (int1, hist) = load_backing_int location this astate in
let* astate, _int_addr2, (int2, _) = load_backing_int location arg astate in
let binop_addr = AbstractValue.mk_fresh () in
let astate =
PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1)
(AbstractValueOperand int2) astate
in
PulseOperations.write_id ret_id (binop_addr, hist) astate |> ok_continue
let int_val this : model =
fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
let* astate, _int_addr1, int_value_hist = load_backing_int location this astate in
PulseOperations.write_id ret_id int_value_hist astate |> ok_continue
let value_of init_value : model =
fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
let event = ValueHistory.Call {f= Model "Integer.valueOf"; location; in_call= []} in
let new_alloc = (AbstractValue.mk_fresh (), [event]) in
let+ astate = construct new_alloc init_value event location astate in
let astate = PulseOperations.write_id ret_id new_alloc astate in
[ExecutionDomain.continue astate]
end
module StringSet = Caml.Set.Make (String)
module ProcNameDispatcher = struct
@ -1241,6 +1300,14 @@ module ProcNameDispatcher = struct
; +map_context_tenv (PatternMatch.Java.implements_lang "String")
&::+ (fun _ str -> StringSet.mem str pushback_modeled)
<>$ capt_arg_payload $+...$--> StdVector.push_back
; +map_context_tenv (PatternMatch.Java.implements_lang "Integer")
&:: "<init>" $ capt_arg_payload $+ capt_arg_payload $--> JavaInteger.constructor
; +map_context_tenv (PatternMatch.Java.implements_lang "Integer")
&:: "equals" $ capt_arg_payload $+ capt_arg_payload $--> JavaInteger.equals
; +map_context_tenv (PatternMatch.Java.implements_lang "Integer")
&:: "intValue" <>$ capt_arg_payload $--> JavaInteger.int_val
; +map_context_tenv (PatternMatch.Java.implements_lang "Integer")
&:: "valueOf" <>$ capt_arg_payload $--> JavaInteger.value_of
; +map_context_tenv PatternMatch.Java.implements_iterator
&:: "remove" <>$ capt_arg_payload
$+...$--> JavaIterator.remove ~desc:"remove"

65
infer/tests/codetoanalyze/java/biabduction/IntegerExample.java
Unescape View File

@ -9,7 +9,7 @@ package codetoanalyze.java.infer;
public class IntegerExample {
private static void testIntegerEqualsGood() {
private static void testIntegerEqualsMethodGood() {
Integer a = new Integer(42);
Integer b = new Integer(42);
Integer c = null;
@ -17,13 +17,9 @@ public class IntegerExample {
if (!a.equals(b)) {
c.intValue();
}
if (a != 42) {
c.intValue();
}
}
private static void testIntegerEqualsBad() {
private static void testIntegerEqualsMethodBad() {
Integer a = new Integer(42);
Integer b = new Integer(42);
Integer c = null;
@ -33,13 +29,64 @@ public class IntegerExample {
}
}
private static void testIntegerEqualsOk() {
/*
* Assignments of the form Integer a = n triggers the method valueOf.
* The valueOf method caches values between -128 and 127 (inclusive).
*/
private static void FP_testIntegerBuiltInEqualOperatorCachedValuesOk() {
Integer a = new Integer(42);
Integer b = new Integer(42);
Integer b = 127;
Integer c = 127;
Integer d = null;
if (a != 42) {
d.intValue();
}
if (b != 127) {
d.intValue();
}
/* This is wrong according to the semantics of valueOf.
* (b==c should hold in this case as 127 is in the cache interval)
*/
if (b != c) {
d.intValue();
}
}
/*
* Assignments of the form Integer a = n triggers the method valueOf.
* The valueOf method caches values between -128 and 127 (inclusive).
*/
private static void testIntegerBuiltInEqualOperatorNonCachedValuesBad() {
Integer a = 128;
Integer b = 128;
Integer c = null;
if (a == b) {
// This is correct (a!=b should hold in this case as 128 is out of the cached interval)
if (a != b) {
c.intValue();
}
}
private static void testIntegerEqualsMethodMaxValueBad() {
Integer a = new Integer(2147483647);
Integer b = new Integer(2147483647);
Integer c = null;
if (a.equals(b)) {
c.intValue();
}
}
private static void testIntegerBuiltInEqualOperatorMaxValueOk() {
Integer a = new Integer(2147483647);
Integer b = null;
if (a != 2147483647) {
b.intValue();
}
}
}

5
infer/tests/codetoanalyze/java/biabduction/issues.exp
Unescape View File

@ -76,7 +76,10 @@ codetoanalyze/java/biabduction/HashMapExample.java, codetoanalyze.java.infer.Has
codetoanalyze/java/biabduction/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getFromKeySetGood_FP(java.util.HashMap):void, 3, NULL_DEREFERENCE, B2, ERROR, [start of procedure getFromKeySetGood_FP(...),Taking true branch]
codetoanalyze/java/biabduction/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getOneIntegerWithoutCheck():int, 6, NULL_DEREFERENCE, B1, ERROR, [start of procedure getOneIntegerWithoutCheck()]
codetoanalyze/java/biabduction/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getTwoIntegersWithOneCheck(java.lang.Integer,java.lang.Integer):void, 8, NULL_DEREFERENCE, B2, ERROR, [start of procedure getTwoIntegersWithOneCheck(...),Taking true branch,Taking true branch]
codetoanalyze/java/biabduction/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsBad():void, 6, NULL_DEREFERENCE, B1, ERROR, [start of procedure testIntegerEqualsBad(),Taking true branch]
codetoanalyze/java/biabduction/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerBuiltInEqualOperatorCachedValuesOk():void, 19, NULL_DEREFERENCE, B1, ERROR, [start of procedure FP_testIntegerBuiltInEqualOperatorCachedValuesOk(),Taking false branch,Taking false branch,Taking true branch]
codetoanalyze/java/biabduction/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerBuiltInEqualOperatorNonCachedValuesBad():void, 7, NULL_DEREFERENCE, B1, ERROR, [start of procedure testIntegerBuiltInEqualOperatorNonCachedValuesBad(),Taking true branch]
codetoanalyze/java/biabduction/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodBad():void, 6, NULL_DEREFERENCE, B1, ERROR, [start of procedure testIntegerEqualsMethodBad(),Taking true branch]
codetoanalyze/java/biabduction/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodMaxValueBad():void, 6, NULL_DEREFERENCE, B1, ERROR, [start of procedure testIntegerEqualsMethodMaxValueBad(),Taking true branch]
codetoanalyze/java/biabduction/InvokeDynamic.java, codetoanalyze.java.infer.InvokeDynamic.invokeDynamicThenNpeBad(java.util.List):void, 7, NULL_DEREFERENCE, B1, ERROR, [start of procedure invokeDynamicThenNpeBad(...),start of procedure callsite_codetoanalyze.java.infer.InvokeDynamic$Lambda$_3_3(),return from a call to Comparator InvokeDynamic.callsite_codetoanalyze.java.infer.InvokeDynamic$Lambda$_3_3(),Skipping sort(...): unknown method]
codetoanalyze/java/biabduction/InvokeDynamic.java, codetoanalyze.java.infer.InvokeDynamic.lambda$npeInLambdaBad$1(java.lang.String,java.lang.String):int, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure lambda$npeInLambdaBad$1(...)]
codetoanalyze/java/biabduction/InvokeDynamic.java, codetoanalyze.java.infer.InvokeDynamic.npeViaSimpleCapture():java.lang.Integer, 3, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure npeViaSimpleCapture(),start of procedure callsite_codetoanalyze.java.infer.InvokeDynamic$Lambda$_10_3(...),return from a call to Function InvokeDynamic.callsite_codetoanalyze.java.infer.InvokeDynamic$Lambda$_10_3(String)]

65
infer/tests/codetoanalyze/java/pulse/IntegerExample.java
Unescape View File

@ -9,7 +9,7 @@ package codetoanalyze.java.infer;
public class IntegerExample {
private static void FP_testIntegerEqualsGood() {
private static void testIntegerEqualsMethodGood() {
Integer a = new Integer(42);
Integer b = new Integer(42);
Integer c = null;
@ -17,13 +17,9 @@ public class IntegerExample {
if (!a.equals(b)) {
c.intValue();
}
if (a != 42) {
c.intValue();
}
}
private static void testIntegerEqualsBad() {
private static void testIntegerEqualsMethodBad() {
Integer a = new Integer(42);
Integer b = new Integer(42);
Integer c = null;
@ -33,13 +29,64 @@ public class IntegerExample {
}
}
private static void testIntegerEqualsFN() {
/*
* Assignments of the form Integer a = n triggers the method valueOf.
* The valueOf method caches values between -128 and 127 (inclusive).
*/
private static void FP_testIntegerBuiltInEqualOperatorCachedValuesOk() {
Integer a = new Integer(42);
Integer b = new Integer(42);
Integer b = 127;
Integer c = 127;
Integer d = null;
if (a != 42) {
d.intValue();
}
if (b != 127) {
d.intValue();
}
/* This is wrong according to the semantics of valueOf.
* (b==c should hold in this case as 127 is in the cache interval)
*/
if (b != c) {
d.intValue();
}
}
/*
* Assignments of the form Integer a = n triggers the method valueOf.
* The valueOf method caches values between -128 and 127 (inclusive).
*/
private static void testIntegerBuiltInEqualOperatorNonCachedValuesBad() {
Integer a = 128;
Integer b = 128;
Integer c = null;
if (a == b) {
// This is correct (a!=b should hold in this case as 128 is out of the cached interval)
if (a != b) {
c.intValue();
}
}
private static void testIntegerEqualsMethodMaxValueBad() {
Integer a = new Integer(2147483647);
Integer b = new Integer(2147483647);
Integer c = null;
if (a.equals(b)) {
c.intValue();
}
}
private static void testIntegerBuiltInEqualOperatorMaxValueOk() {
Integer a = new Integer(2147483647);
Integer b = null;
if (a != 2147483647) {
b.intValue();
}
}
}

8
infer/tests/codetoanalyze/java/pulse/issues.exp
Unescape View File

@ -14,10 +14,10 @@ codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicD
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Subtype.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Subtype.foo()`,return from call to `Object DynamicDispatch$Subtype.foo()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicResolutionWithVariadicMethodBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,return from call to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Impl.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Impl.foo()`,return from call to `Object DynamicDispatch$Impl.foo()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerEqualsGood():void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerEqualsGood():void, 10, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsBad():void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsFN():void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerBuiltInEqualOperatorCachedValuesOk():void, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerBuiltInEqualOperatorNonCachedValuesBad():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodBad():void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodMaxValueBad():void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/InvokeDynamic.java, codetoanalyze.java.infer.InvokeDynamic.invokeDynamicThenNpeBad(java.util.List):void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/InvokeDynamic.java, codetoanalyze.java.infer.InvokeDynamic.lambda$npeInLambdaBad$1(java.lang.String,java.lang.String):int, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
codetoanalyze/java/pulse/Lists.java, codetoanalyze.java.infer.Lists.FP_emptyRemembersOk(java.util.List):void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]

Write Preview
Loading…
Cancel
Save