From 27acb0fe4e4602d6e5e9316b65ba6252d40eac84 Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Mon, 25 Jan 2021 03:43:09 -0800 Subject: [PATCH] [pulse] Modeling Java Integer class Summary: Adding support for Java Integer class in Pulse. Reviewed By: ezgicicek Differential Revision: D25953596 fbshipit-source-id: ce7206db3 --- infer/src/pulse/PulseModels.ml | 67 +++++++++++++++++++ .../java/biabduction/IntegerExample.java | 65 +++++++++++++++--- .../codetoanalyze/java/biabduction/issues.exp | 5 +- .../java/pulse/IntegerExample.java | 65 +++++++++++++++--- .../tests/codetoanalyze/java/pulse/issues.exp | 8 +-- 5 files changed, 187 insertions(+), 23 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 14cdee24d..cfcc1c92d 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -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") + &:: "" $ 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" diff --git a/infer/tests/codetoanalyze/java/biabduction/IntegerExample.java b/infer/tests/codetoanalyze/java/biabduction/IntegerExample.java index 8ff9c3821..0ea875eba 100644 --- a/infer/tests/codetoanalyze/java/biabduction/IntegerExample.java +++ b/infer/tests/codetoanalyze/java/biabduction/IntegerExample.java @@ -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(); + } + } } diff --git a/infer/tests/codetoanalyze/java/biabduction/issues.exp b/infer/tests/codetoanalyze/java/biabduction/issues.exp index d2aea5180..5d72f5bbf 100644 --- a/infer/tests/codetoanalyze/java/biabduction/issues.exp +++ b/infer/tests/codetoanalyze/java/biabduction/issues.exp @@ -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)] diff --git a/infer/tests/codetoanalyze/java/pulse/IntegerExample.java b/infer/tests/codetoanalyze/java/pulse/IntegerExample.java index 5c763954a..0ea875eba 100644 --- a/infer/tests/codetoanalyze/java/pulse/IntegerExample.java +++ b/infer/tests/codetoanalyze/java/pulse/IntegerExample.java @@ -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(); + } + } } diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 04ec050e4..92c012143 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -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]