[impurity][hoisting] Add more tests

Reviewed By: skcho

Differential Revision: D20441214

fbshipit-source-id: 5765530a9

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<Integer> list) {
+    Iterator<Integer> 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<Integer> list) {
+    for (int i = 0; i < b; i++) {
+      contains_pure_FN(b, list);
+    }
+  }
 }

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() {
+  void timing_calls_dont_hoist(int x) {
-    for (int i = 0; i < 10; i++) {
+    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() {
+  void harmless_hoist_FN(int b) {
-    for (int i = 0; i < 10; i++) {
+    for (int i = 0; i < b; i++) {
-      timing_calls_dont_hoist(); // don't hoist
+      timing_calls_dont_hoist(b); // don't hoist
       harmless_pure(); // ok to hoist
     }
   }

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)]

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,

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]