diff --git a/infer/tests/codetoanalyze/java/hoisting/HoistModeled.java b/infer/tests/codetoanalyze/java/hoisting/HoistModeled.java index 8f2ca9e0f..71737acc6 100644 --- a/infer/tests/codetoanalyze/java/hoisting/HoistModeled.java +++ b/infer/tests/codetoanalyze/java/hoisting/HoistModeled.java @@ -8,7 +8,7 @@ import com.fasterxml.jackson.core.JsonParser; import com.fasterxml.jackson.databind.DeserializationContext; import com.fasterxml.jackson.databind.JsonDeserializer; import java.io.IOException; -import java.util.List; +import java.util.*; class HoistModeled { @@ -33,4 +33,21 @@ class HoistModeled { o = specDeserializer.deserialize(p, ctx); } } + + boolean contains_pure_FN(Integer i, ArrayList list) { + Iterator listIterator = list.iterator(); + while (listIterator.hasNext()) { + Integer el = listIterator.next(); + if (i.equals(el)) { + return true; + } + } + return false; + } + + void call_contains_pure_hoist_FN(int b, ArrayList list) { + for (int i = 0; i < b; i++) { + contains_pure_FN(b, list); + } + } } diff --git a/infer/tests/codetoanalyze/java/hoisting/HoistUnmodeled.java b/infer/tests/codetoanalyze/java/hoisting/HoistUnmodeled.java index adfb73022..420471f44 100644 --- a/infer/tests/codetoanalyze/java/hoisting/HoistUnmodeled.java +++ b/infer/tests/codetoanalyze/java/hoisting/HoistUnmodeled.java @@ -8,8 +8,8 @@ class HoistUnmodeled { // Any unmodeled (e.g. timing) call is assumed to be modifying global // state - void timing_calls_dont_hoist() { - for (int i = 0; i < 10; i++) { + void timing_calls_dont_hoist(int x) { + for (int i = 0; i < x; i++) { System.nanoTime(); } } @@ -20,9 +20,9 @@ class HoistUnmodeled { // It should be ok to hoist harmless_pure() since it doesn't read // from global state. - void harmless_hoist_FN() { - for (int i = 0; i < 10; i++) { - timing_calls_dont_hoist(); // don't hoist + void harmless_hoist_FN(int b) { + for (int i = 0; i < b; i++) { + timing_calls_dont_hoist(b); // don't hoist harmless_pure(); // ok to hoist } } diff --git a/infer/tests/codetoanalyze/java/hoisting/issues.exp b/infer/tests/codetoanalyze/java/hoisting/issues.exp index b6908347a..db9054682 100644 --- a/infer/tests/codetoanalyze/java/hoisting/issues.exp +++ b/infer/tests/codetoanalyze/java/hoisting/issues.exp @@ -58,6 +58,7 @@ codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate$Item.while_don codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.get_length(int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistInvalidate.get_length(int[])] codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.get_x(int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistInvalidate.get_x(int[])] codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.loop_indirect_hoist(java.util.ArrayList,int,int[]):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistInvalidate.get_length(int[]) at line 52 is loop-invariant] +codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.call_contains_pure_hoist_FN(int,java.util.ArrayList):void, 1, INVARIANT_CALL, no_bucket, ERROR, [The call to Integer Integer.valueOf(int) at line 50 is loop-invariant] codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.deserialize_hoist(com.fasterxml.jackson.databind.JsonDeserializer,com.fasterxml.jackson.core.JsonParser,com.fasterxml.jackson.databind.DeserializationContext):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.deserialize_hoist(JsonDeserializer,JsonParser,DeserializationContext)] codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.deserialize_hoist(com.fasterxml.jackson.databind.JsonDeserializer,com.fasterxml.jackson.core.JsonParser,com.fasterxml.jackson.databind.DeserializationContext):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to Object JsonDeserializer.deserialize(JsonParser,DeserializationContext) at line 33 is loop-invariant] codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistModeled.list_contains_hoist(List,String)] diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 11e3e7316..9cb67e089 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -91,12 +91,34 @@ class PurityModeled { } } + // Since n is symbolic, pruning doesn't result in infeasible path, + // but we assume that the parameter [n] must be 3 due to constant(4) + // "widening" in pulse. void timing_call_in_loop_symb_impure(int n) { for (int i = 0; i < n; i++) { System.nanoTime(); } } + // Due to getting the wrong summary for the callee (a=3), Pulse ends + // up thinking that the parameter [a] must be 3 in the loop. Hence, as + // a result of pruning, exit node becomes infeasible and we get + // empty summary. + void call_timing_symb_impure_FN(int a) { + for (int i = 0; i < a; i++) { + timing_call_in_loop_symb_impure(a); + } + } + + // The relation between the parameter and the argument to the callee + // is broken. Although, the final pulse summary for this function is + // still wrong. + void call_timing_symb_unrelated_impure(int a, int b) { + for (int i = 0; i < a; i++) { + timing_call_in_loop_symb_impure(b); + } + } + enum Color { RED, GREEN, diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 8ffcf5b2d..afaa2d689 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -15,6 +15,7 @@ codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(j 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] 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[]),call to skipped function void System.arraycopy(Object,int,Object,int,int) occurs here] +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] 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.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]