[topl] Fixed an eggregious performance issue (repeated summaries).

Summary:
Makes sure that topl summaries don't repeat. Previously this happened
when two posts led to the same summary when procedure-local variables
were killed. Such repeated summaries quickly lead to exponential
explosion. (For example, the added test -- `ManyLoops.java` -- didn't
finish in any reasonable time.)

Reviewed By: jvillard

Differential Revision: D25209623

fbshipit-source-id: 04b1a3e12

infer/src/pulse/PulsePathCondition.ml

@@ -229,6 +229,7 @@ let and_callee subst phi ~callee:phi_callee =
 type operand = Formula.operand =
   | LiteralOperand of IntLit.t
   | AbstractValueOperand of AbstractValue.t
+[@@deriving compare]
 
 let pp_operand f = function
   | LiteralOperand i ->

infer/src/pulse/PulsePathCondition.mli

@@ -44,6 +44,7 @@ val and_callee :
 (** {2 Operations} *)
 
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
+[@@deriving compare]
 
 val pp_operand : Formatter.t -> operand -> unit
 

infer/src/pulse/PulseTopl.ml

@@ -9,11 +9,12 @@ open! IStd
 open PulseBasicInterface
 module L = Logging
 
-type value = AbstractValue.t
+type value = AbstractValue.t [@@deriving compare]
 
 type event =
   | ArrayWrite of {aw_array: value; aw_index: value}
   | Call of {return: value option; arguments: value list; procname: Procname.t}
+[@@deriving compare]
 
 let pp_comma_seq f xs = Pp.comma_seq ~print_env:Pp.text_break f xs
 
@@ -26,14 +27,14 @@ let pp_event f = function
         (pp_comma_seq AbstractValue.pp) arguments
 
 
-type vertex = ToplAutomaton.vindex
+type vertex = ToplAutomaton.vindex [@@deriving compare]
 
-type register = ToplAst.register_name
+type register = ToplAst.register_name [@@deriving compare]
 
 (* TODO(rgrigore): Change the memory assoc list to a Map. *)
-type configuration = {vertex: vertex; memory: (register * value) list}
+type configuration = {vertex: vertex; memory: (register * value) list} [@@deriving compare]
 
-type predicate = Binop.t * PathCondition.operand * PathCondition.operand
+type predicate = Binop.t * PathCondition.operand * PathCondition.operand [@@deriving compare]
 
 type step =
   { step_location: Location.t
@@ -47,7 +48,8 @@ and simple_state =
   { pre: configuration  (** at the start of the procedure *)
   ; post: configuration  (** at the current program point *)
   ; pruned: predicate list  (** path-condition for the automaton *)
-  ; last_step: step option  (** for trace error reporting *) }
+  ; last_step: step option [@compare.ignore]  (** for trace error reporting *) }
+[@@deriving compare]
 
 (* TODO: include a hash of the automaton in a summary to avoid caching problems. *)
 (* TODO: limit the number of simple_states to some configurable number (default ~5) *)
@@ -389,8 +391,11 @@ let large_step ~call_location ~callee_proc_name ~substitution ~condition ~callee
   in
   let _updated_substitution, callee_prepost = sub_state (substitution, callee_prepost) in
   (* TODO(rgrigore): may be worth optimizing the cartesian_product *)
-  let state = List.filter_map ~f:seq (List.cartesian_product state callee_prepost) in
-  drop_infeasible condition state
+  let new_state = List.filter_map ~f:seq (List.cartesian_product state callee_prepost) in
+  let result = drop_infeasible condition new_state in
+  L.d_printfln "@[<2>PulseTopl.large_step:@;callee_prepost=%a@;%a@ -> %a@]" pp_state callee_prepost
+    pp_state state pp_state result ;
+  result
 
 
 let filter_for_summary path_condition state =
@@ -414,7 +419,8 @@ let simplify ~keep state =
     let pruned = List.filter ~f:is_live_predicate pruned in
     {pre; post; pruned; last_step}
   in
-  List.map ~f:simplify_simple_state state
+  let state = List.map ~f:simplify_simple_state state in
+  List.dedup_and_sort ~compare:compare_simple_state state
 
 
 let description_of_step_data step_data =

infer/src/topl/ToplAst.ml

@@ -9,7 +9,7 @@ open! IStd
 
 type property_name = string [@@deriving compare, hash, sexp]
 
-type register_name = string
+type register_name = string [@@deriving compare]
 
 type variable_name = string
 

infer/src/topl/ToplAutomaton.ml

@@ -21,7 +21,7 @@ end
 
 type vname = Vname.t
 
-type vindex = int
+type vindex = int [@@deriving compare]
 
 type tindex = int
 

infer/src/topl/ToplAutomaton.mli

@@ -23,9 +23,11 @@ open! IStd
 *)
 type t
 
-type vindex = int (* from 0 to vcount()-1, inclusive *)
+(** from 0 to vcount()-1, inclusive *)
+type vindex = int [@@deriving compare]
 
-type tindex = int (* from 0 to tcount()-1, inclusive *)
+(** from 0 to tcount()-1, inclusive *)
+type tindex = int
 
 type transition = {source: vindex; target: vindex; label: ToplAst.label option}
 

infer/tests/codetoanalyze/java/topl/baos/issues.exp

@@ -1,5 +1,5 @@
-codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ByteArrayOutputStream.<init>(int),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()]
-codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ByteArrayOutputStream.<init>(int),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()]
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to GZIPOutputStream.<init>(OutputStream),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()]
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to GZIPOutputStream.<init>(OutputStream),call to void FilterOutputStream.write(byte[]),call to byte[] ByteArrayOutputStream.toByteArray()]
 codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ObjectOutputStream.<init>(OutputStream),call to void ObjectOutputStream.writeObject(Object),call to byte[] ByteArrayOutputStream.toByteArray()]
 codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to ObjectOutputStream.<init>(OutputStream),call to void ObjectOutputStream.writeObject(Object),call to byte[] ByteArrayOutputStream.toByteArray()]
 codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to DataOutputStream.<init>(OutputStream),call to void DataOutputStream.writeLong(long),call to byte[] ByteArrayOutputStream.toByteArray()]

infer/tests/codetoanalyze/java/topl/hasnext/ManyLoops.java

@@ -0,0 +1,31 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * 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.*;
+
+class ManyLoops {
+
+  /** Test for performance. */
+  void fOk() {
+    Set<String> xs = new HashSet<String>();
+    go(xs);
+    go(xs);
+    go(xs);
+    go(xs);
+    go(xs);
+    go(xs);
+    go(xs);
+    go(xs);
+    go(xs);
+    go(xs);
+  }
+
+  void go(Set<String> xs) {
+    for (String x : xs) {
+      System.out.println(x);
+    }
+  }
+}