pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '121b7352f9'
${ noResults }
infer_clone/infer/tests/codetoanalyze/java/impurity/issues.exp

43 lines
10 KiB
Raw Normal View History Unescape

[impurity] Do not add value history in impurity traces Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories. Reviewed By: skcho Differential Revision: D20362149 fbshipit-source-id: 8a2a6115e
5 years ago
codetoanalyze/java/impurity/GlobalTest.java, GlobalTest$Foo.set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest$Foo.set_impure(),global variable `GlobalTest` modified here]
[impurity] Fix include_value_history Summary: D20362149 missed - to pass the optional argument `include_value_history` to the recursive call in `PulseTrace.add_to_errlog`. - to set `include_value_history=false` for skipped calls. This diff fixes these issues. Reviewed By: skcho Differential Revision: D20385604 fbshipit-source-id: 176e4d010
5 years ago
codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.call_set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.call_set_impure(),when calling `void GlobalTest$Foo.set_impure()` here,global variable `GlobalTest` modified here]
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),when calling `void GlobalTest.incr(GlobalTest$Foo,int)` here,global variable `GlobalTest` modified here]
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),when calling `void GlobalTest.incr(GlobalTest$Foo,int)` here,global variable `GlobalTest` modified here]
[impurity] Do not add value history in impurity traces Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories. Reviewed By: skcho Differential Revision: D20362149 fbshipit-source-id: 8a2a6115e
5 years ago
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` modified here]
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` modified here]
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` modified here]
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` modified here]
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` modified here]
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` modified here]
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` modified here]
[pulse][purity] Add more naive models for Java Summary: - Add more naive pulse models for: - `System.arraycopy` - `StringBuilder.setLength` - `StringBuilder.delete` - Model the following as pure - `SparseArrayCompat.valueAt` - `File.get...` - Add a nice test Reviewed By: jvillard Differential Revision: D20513397 fbshipit-source-id: 6d412d13a
5 years ago
codetoanalyze/java/impurity/Localities.java, Localities.get_impure(int):int[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int[] Localities.get_impure(int),global variable `Localities` modified here]
[impurity] Track unique accesses Summary: Impurity domain was tracking all changes to variables (with a list of traces that containing all write/invalid accesses). This results in having long traces with multiple access events for the same variable. For instance, ``` void swap_impure(int[] array, int i, int j) { int tmp = array[i]; array[i] = array[j]; \\ included in the trace array[j] = tmp; \\ included in the trace } ``` here we recorded both array accesses. This diff changes the domain to include accesses so that we only keep track of a single trace per access. Array accesses are only recorded once. Note that we want to record all unique accesses, not just the first one, because impurity will be used for hoisting/cost where we will invalidate impure arguments and consider all the rest as not changing. Reviewed By: jvillard Differential Revision: D20385745 fbshipit-source-id: d3647dad3
5 years ago
codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.incrementAll_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here]
codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list` modified here]
[impurity] Do not add value history in impurity traces Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories. Reviewed By: skcho Differential Revision: D20362149 fbshipit-source-id: 8a2a6115e
5 years ago
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` modified here]
[impurity] Fix include_value_history Summary: D20362149 missed - to pass the optional argument `include_value_history` to the recursive call in `PulseTrace.add_to_errlog`. - to set `include_value_history=false` for skipped calls. This diff fixes these issues. Reviewed By: skcho Differential Revision: D20385604 fbshipit-source-id: 176e4d010
5 years ago
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),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here]
[impurity] Rely on set of skipped functions to determine impurity Summary: Currently, impurity analysis is oblivious to skipped functions which might e.g. return a non-deterministic value, write to memory or have some other side-effect. This diff fixes that by relying on Pulse's skipped functions to determine impurity. Any unknown function which is not modeled to be pure is assumed to be impure. This is a heuristic. We could have assumed them to be pure by default as well. Reviewed By: jvillard Differential Revision: D19428514 fbshipit-source-id: 82efe04f9
5 years ago
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]
[pulse] Add more naive Java models Summary: This diff naively models the following as `StdVector.push_back`: - `StringBuilder.append` - `String.replace` - `Queue.poll` It also adds a FN test for `Iterator.next`. Reviewed By: skcho Differential Revision: D20469786 fbshipit-source-id: 2d8e8d117
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.append_impure(java.lang.StringBuilder):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.append_impure(StringBuilder),parameter `strBuilder` modified here]
[impurity] Consider functions with empty pulse summary as impure Summary: As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by: - discovering aliasing in memory - widening limited number of times in loops and concluding that loop exit conditions are never taken However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts: ``` Pulse: 1 pre/post(s) #0: PRE: { roots={ }; mem ={ }; attrs={ };} POST: { roots={ }; mem ={ }; attrs={ };} SKIPPED_CALLS: { } ``` The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure. Reviewed By: skcho Differential Revision: D20619504 fbshipit-source-id: 3a8502c90
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_impure(int) with empty pulse summary]
[impurity][hoisting] Add more tests Reviewed By: skcho Differential Revision: D20441214 fbshipit-source-id: 5765530a9
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_unrelated_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_unrelated_impure(int,int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here]
[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
5 years ago
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]
[impurity] Consider functions with empty pulse summary as impure Summary: As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by: - discovering aliasing in memory - widening limited number of times in loops and concluding that loop exit conditions are never taken However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts: ``` Pulse: 1 pre/post(s) #0: PRE: { roots={ }; mem ={ }; attrs={ };} POST: { roots={ }; mem ={ }; attrs={ };} SKIPPED_CALLS: { } ``` The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure. Reviewed By: skcho Differential Revision: D20619504 fbshipit-source-id: 3a8502c90
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.constant_loop_pure_FP():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.constant_loop_pure_FP() with empty pulse summary]
[impurity] Do not add value history in impurity traces Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories. Reviewed By: skcho Differential Revision: D20362149 fbshipit-source-id: 8a2a6115e
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_add_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_add_impure(ArrayList),parameter `list` modified here]
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure(java.util.ArrayList,java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1` modified here]
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_set_impure(ArrayList),parameter `list` was potentially invalidated by `std::vector::assign()` here]
[impurity] Rely on set of skipped functions to determine impurity Summary: Currently, impurity analysis is oblivious to skipped functions which might e.g. return a non-deterministic value, write to memory or have some other side-effect. This diff fixes that by relying on Pulse's skipped functions to determine impurity. Any unknown function which is not modeled to be pure is assumed to be impure. This is a heuristic. We could have assumed them to be pure by default as well. Reviewed By: jvillard Differential Revision: D19428514 fbshipit-source-id: 82efe04f9
5 years ago
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]
[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
5 years ago
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]
[pulse] Add more naive Java models Summary: This diff naively models the following as `StdVector.push_back`: - `StringBuilder.append` - `String.replace` - `Queue.poll` It also adds a FN test for `Iterator.next`. Reviewed By: skcho Differential Revision: D20469786 fbshipit-source-id: 2d8e8d117
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.process_queue_impure(java.util.ArrayList,java.util.Queue):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.process_queue_impure(ArrayList,Queue),parameter `queue` modified here]
[impurity] Do not add value history in impurity traces Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories. Reviewed By: skcho Differential Revision: D20362149 fbshipit-source-id: 8a2a6115e
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` modified here]
[pulse] Add more naive Java models Summary: This diff naively models the following as `StdVector.push_back`: - `StringBuilder.append` - `String.replace` - `Queue.poll` It also adds a FN test for `Iterator.next`. Reviewed By: skcho Differential Revision: D20469786 fbshipit-source-id: 2d8e8d117
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.replace_impure(java.lang.String):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.replace_impure(String),parameter `s` modified here]
[impurity] Consider functions with empty pulse summary as impure Summary: As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by: - discovering aliasing in memory - widening limited number of times in loops and concluding that loop exit conditions are never taken However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts: ``` Pulse: 1 pre/post(s) #0: PRE: { roots={ }; mem ={ }; attrs={ };} POST: { roots={ }; mem ={ }; attrs={ };} SKIPPED_CALLS: { } ``` The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure. Reviewed By: skcho Differential Revision: D20619504 fbshipit-source-id: 3a8502c90
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_impure() with empty pulse summary]
[pulse] Take into account skipped calls for state comparison Summary: We forgot to take skipped calls into account for state comparison. This diff fixes that. Reviewed By: skcho Differential Revision: D20282739 fbshipit-source-id: 7b4d84bb0
5 years ago
codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_symb_impure(int),call to skipped function long System.nanoTime() occurs here]
[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
5 years ago
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]
[impurity] Do not add value history in impurity traces Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories. Reviewed By: skcho Differential Revision: D20362149 fbshipit-source-id: 8a2a6115e
5 years ago
codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),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` modified here]
[impurity] Fix include_value_history Summary: D20362149 missed - to pass the optional argument `include_value_history` to the recursive call in `PulseTrace.add_to_errlog`. - to set `include_value_history=false` for skipped calls. This diff fixes these issues. Reviewed By: skcho Differential Revision: D20385604 fbshipit-source-id: 176e4d010
5 years ago
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),when calling `void Test.set_impure(int,int)` here,parameter `this` modified here]
[impurity] Do not add value history in impurity traces Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories. Reviewed By: skcho Differential Revision: D20362149 fbshipit-source-id: 8a2a6115e
5 years ago
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 variable `Test` modified here]
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` modified here]
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` modified here]
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` modified here]
[impurity] Track unique accesses Summary: Impurity domain was tracking all changes to variables (with a list of traces that containing all write/invalid accesses). This results in having long traces with multiple access events for the same variable. For instance, ``` void swap_impure(int[] array, int i, int j) { int tmp = array[i]; array[i] = array[j]; \\ included in the trace array[j] = tmp; \\ included in the trace } ``` here we recorded both array accesses. This diff changes the domain to include accesses so that we only keep track of a single trace per access. Array accesses are only recorded once. Note that we want to record all unique accesses, not just the first one, because impurity will be used for hoisting/cost where we will invalidate impure arguments and consider all the rest as not changing. Reviewed By: jvillard Differential Revision: D20385745 fbshipit-source-id: d3647dad3
5 years ago
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` modified here]
[impurity] Rely on set of skipped functions to determine impurity Summary: Currently, impurity analysis is oblivious to skipped functions which might e.g. return a non-deterministic value, write to memory or have some other side-effect. This diff fixes that by relying on Pulse's skipped functions to determine impurity. Any unknown function which is not modeled to be pure is assumed to be impure. This is a heuristic. We could have assumed them to be pure by default as well. Reviewed By: jvillard Differential Revision: D19428514 fbshipit-source-id: 82efe04f9
5 years ago
codetoanalyze/java/impurity/Test.java, Test.systemNanoTime_impure():long, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function long Test.systemNanoTime_impure(),call to skipped function long System.nanoTime() occurs here]