From c829db496429868f55f977477d513cd36098f359 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Wed, 2 Dec 2020 01:14:34 -0800 Subject: [PATCH] [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 | 1 + infer/src/pulse/PulsePathCondition.mli | 1 + infer/src/pulse/PulseTopl.ml | 24 ++++++++------ infer/src/topl/ToplAst.ml | 2 +- infer/src/topl/ToplAutomaton.ml | 2 +- infer/src/topl/ToplAutomaton.mli | 6 ++-- .../codetoanalyze/java/topl/baos/issues.exp | 4 +-- .../java/topl/hasnext/ManyLoops.java | 31 +++++++++++++++++++ 8 files changed, 56 insertions(+), 15 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/topl/hasnext/ManyLoops.java diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index f5a37cba5..fecf0cd67 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/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 -> diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index abf64ba10..00c79175b 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/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 diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 63bb16c29..070543888 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/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 = diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml index 326aa82ed..f75dd8183 100644 --- a/infer/src/topl/ToplAst.ml +++ b/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 diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index 0fe24cef5..8c9c08f9a 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/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 diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index 2af1b1006..40367d316 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/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} diff --git a/infer/tests/codetoanalyze/java/topl/baos/issues.exp b/infer/tests/codetoanalyze/java/topl/baos/issues.exp index c1c32a14d..1f109b322 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/issues.exp +++ b/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.(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.(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.(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.(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.(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.(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.(OutputStream),call to void DataOutputStream.writeLong(long),call to byte[] ByteArrayOutputStream.toByteArray()] diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/ManyLoops.java b/infer/tests/codetoanalyze/java/topl/hasnext/ManyLoops.java new file mode 100644 index 000000000..8d8c120bb --- /dev/null +++ b/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 xs = new HashSet(); + go(xs); + go(xs); + go(xs); + go(xs); + go(xs); + go(xs); + go(xs); + go(xs); + go(xs); + go(xs); + } + + void go(Set xs) { + for (String x : xs) { + System.out.println(x); + } + } +}