From 040442c93be8aaeb96d7bf6ebde331c10d1b7872 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 4 Feb 2020 08:40:12 -0800 Subject: [PATCH] [pulse] Don't write through pointer arguments in Java Summary: Pulse has an extra invalidation mechanism (introduced in D18726203) to prevent something invalid (e.g. `null`) to be passed by reference to an initialisation function. Therefore, it havocs formals passed by reference to skipped functions. However, I don't think this makes sense in Java. So, let's turn it off. A nice consequence of this is that in impurity analysis, we do not consider functions that call skipped library calls with object arguments as writing to their formals. Reviewed By: skcho Differential Revision: D19697110 fbshipit-source-id: 6e3a71f2a --- infer/src/pulse/PulseOperations.ml | 8 ++++++-- .../tests/codetoanalyze/java/impurity/PurityModeled.java | 6 ++++++ infer/tests/codetoanalyze/java/impurity/issues.exp | 8 ++++---- 3 files changed, 16 insertions(+), 6 deletions(-) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 51d593cb6..bffaf27c4 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -500,8 +500,12 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate = (* We should not havoc when the corresponding formal is a pointer to const *) - if Typ.is_pointer actual_typ && not (is_ptr_to_const formal_typ_opt) then - (* HACK: write through the pointer even if it is invalid. This is to avoid raising issues when + if + (not (Language.curr_language_is Java)) + && Typ.is_pointer actual_typ + && not (is_ptr_to_const formal_typ_opt) + then + (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when havoc'ing pointer parameters (which normally causes a [check_valid] call. *) let fresh_value = AbstractValue.mk_fresh () in Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index cc1f9b45a..901e8f8ae 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -4,6 +4,8 @@ * 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 PurityModeled { double math_random_impure() { @@ -45,4 +47,8 @@ class PurityModeled { return p; } + + void list_size_pure(ArrayList list) { + for (int i = 0; i < list.size(); i++) {} + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index f59fa7d29..bbb22b2ec 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -14,11 +14,11 @@ codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java. codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list` of void Localities.modify_first_el_impure(ArrayList),passed as argument to `Collection.get()` (modelled),return from call to `Collection.get()` (modelled),assigned,assigned,parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),parameter `list` of void Localities.modify_via_call_impure(ArrayList),passed as argument to `Localities$Foo Localities.get_first_pure(ArrayList)`,return from call to `Localities$Foo Localities.get_first_pure(ArrayList)`,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.newHashCode_impure():int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.newHashCode_impure(),call to skipped function int Object.hashCode() occurs here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` of void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` modified here,call to skipped function void System.arraycopy(Object,int,Object,int,int) occurs here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),global variable `java.lang.System` accessed here,when calling `void PurityModeled.write_impure()` here,global variable `java.lang.System` accessed here,global variable `lang.System` modified here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),call to skipped function void System.arraycopy(Object,int,Object,int,int) occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_impure():double, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double PurityModeled.math_random_impure(),call to skipped function double Math.random() occurs here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),global variable `java.lang.System` accessed here,when calling `void PurityModeled.call_write_impure()` here,global variable `java.lang.System` accessed here,when calling `void PurityModeled.write_impure()` here,global variable `java.lang.System` accessed here,global variable `lang.System` modified here,when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),global variable `java.lang.System` accessed here,global variable `lang.System` modified here,call to skipped function void PrintStream.write(byte[],int,int) occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),call to skipped function void PrintStream.write(byte[],int,int) occurs here] codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` accessed here,global variable `Test` modified here] 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` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here] 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` of void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` of void Test.set_impure(int,int),parameter `this` modified here]