[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

infer/src/pulse/PulseAbductiveDomain.ml

@@ -93,6 +93,11 @@ type t =
 let pp f {post; pre} = F.fprintf f "@[<v>%a@;PRE=[%a]@]" Domain.pp post InvertedDomain.pp pre
 
 let leq ~lhs ~rhs =
+  (* We only care about post state for skipped calls. TODO: Pull
+     skipped calls out of BaseDomain to here. *)
+  BaseDomain.SkippedCalls.leq ~lhs:(lhs.post :> BaseDomain.t).skipped_calls
+    ~rhs:(rhs.post :> BaseDomain.t).skipped_calls
+  &&
   match
     BaseDomain.isograph_map BaseDomain.empty_mapping
       ~lhs:(rhs.pre :> BaseDomain.t)

infer/src/pulse/PulseBaseDomain.ml

@@ -18,9 +18,16 @@ module SkippedTrace = struct
   let pp fmt =
     PulseTrace.pp fmt ~pp_immediate:(fun fmt ->
         F.pp_print_string fmt "call to skipped function occurs here" )
+
+
+  let leq ~lhs ~rhs = phys_equal lhs rhs
+
+  let join _ _ = assert false
+
+  let widen ~prev:_ ~next:_ ~num_iters:_ = assert false
 end
 
-module SkippedCalls = PrettyPrintable.MakePPMonoMap (Procname) (SkippedTrace)
+module SkippedCalls = AbstractDomain.Map (Procname) (SkippedTrace)
 
 (* {2 Abstract domain description } *)
 

infer/src/pulse/PulseBaseDomain.mli

@@ -13,8 +13,7 @@ module SkippedTrace : sig
   type t = PulseTrace.t
 end
 
-module SkippedCalls :
-  PrettyPrintable.PPMonoMap with type key = Procname.t and type value = SkippedTrace.t
+module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t
 
 type t =
   { heap: PulseBaseMemory.t

infer/tests/codetoanalyze/java/impurity/PurityModeled.java

@@ -82,9 +82,18 @@ class PurityModeled {
     list.set(0, "e");
   }
 
+  // Pulse can only widen a fixed number of times, hence it thinks
+  // that the exit of the loop never reaches and results in empty
+  // post.
   void timing_call_in_loop_impure_FN() {
     for (int i = 0; i < 10; i++) {
       System.nanoTime();
     }
   }
+
+  void timing_call_in_loop_symb_impure(int n) {
+    for (int i = 0; i < n; i++) {
+      System.nanoTime();
+    }
+  }
 }

infer/tests/codetoanalyze/java/impurity/issues.exp

@@ -22,6 +22,7 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(ja
 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),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.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` of void PurityModeled.remove_impure(Iterator),parameter `i` modified here]
+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]
 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]