From 33071b82b5dfc8651af26bd4d5c488a8beb9b0b4 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Wed, 2 Dec 2020 01:14:21 -0800 Subject: [PATCH] [topl] Interprocedural analysis (in Pulse) Summary: PulseTopl.large_step is now implemented All active tests are migrated now to topl-in-pulse. Reviewed By: jvillard Differential Revision: D25179556 fbshipit-source-id: dc1136bab --- infer/src/pulse/Pulse.ml | 4 +- infer/src/pulse/PulseAbductiveDomain.ml | 12 +- infer/src/pulse/PulseAbductiveDomain.mli | 6 +- infer/src/pulse/PulseInterproc.ml | 4 +- infer/src/pulse/PulseTopl.ml | 166 +++++++++++++++--- infer/src/pulse/PulseTopl.mli | 9 +- infer/src/topl/ToplAutomaton.ml | 16 +- infer/src/topl/ToplAutomaton.mli | 6 +- infer/tests/codetoanalyze/java/topl/Makefile | 2 +- .../java/topl/compareArgs/Makefile | 2 +- .../java/topl/compareArgs/issues.exp | 4 +- .../codetoanalyze/java/topl/hasnext/Makefile | 2 +- .../java/topl/hasnext/issues.exp | 6 +- .../codetoanalyze/java/topl/skip/Makefile | 12 +- .../codetoanalyze/java/topl/slowIter/Makefile | 2 +- .../java/topl/slowIter/issues.exp | 4 +- 16 files changed, 179 insertions(+), 78 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 393b09bd0..44cd4f29b 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -109,8 +109,8 @@ module PulseTransferFunctions = struct let return = Var.of_id return in let do_astate astate = let return = Option.map ~f:fst (Stack.find_opt return astate) in - let topl_event = PulseTopl.Call {return; arguments; procname; loc} in - AbductiveDomain.Topl.small_step topl_event astate + let topl_event = PulseTopl.Call {return; arguments; procname} in + AbductiveDomain.Topl.small_step loc topl_event astate in let do_one_exec_state (exec_state : Domain.t) : Domain.t = match exec_state with diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index c9ef25858..64f2c7b61 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -490,12 +490,16 @@ let get_pre {pre} = (pre :> BaseDomain.t) let get_post {post} = (post :> BaseDomain.t) module Topl = struct - let small_step event astate = - {astate with topl= PulseTopl.small_step astate.path_condition event astate.topl} + let small_step loc event astate = + {astate with topl= PulseTopl.small_step loc astate.path_condition event astate.topl} - let large_step ~substitution ?(condition = PathCondition.true_) ~callee_prepost astate = - {astate with topl= PulseTopl.large_step ~substitution ~condition ~callee_prepost astate.topl} + let large_step ~call_location ~callee_proc_name ~substitution ?(condition = PathCondition.true_) + ~callee_prepost astate = + { astate with + topl= + PulseTopl.large_step ~call_location ~callee_proc_name ~substitution ~condition + ~callee_prepost astate.topl } let get {topl} = topl diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 01e3f83cb..bf9150bf2 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -181,10 +181,12 @@ val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCo {!PathCondition.false_}. *) module Topl : sig - val small_step : PulseTopl.event -> t -> t + val small_step : Location.t -> PulseTopl.event -> t -> t val large_step : - substitution:(AbstractValue.t * ValueHistory.t) AbstractValue.Map.t + call_location:Location.t + -> callee_proc_name:Procname.t + -> substitution:(AbstractValue.t * ValueHistory.t) AbstractValue.Map.t -> ?condition:PathCondition.t -> callee_prepost:PulseTopl.state -> t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 0b6cb2c20..44c4688d5 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -565,8 +565,8 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post in let astate = if Topl.is_deep_active () then - AbductiveDomain.Topl.large_step ~substitution:call_state.subst - ~condition:call_state.astate.path_condition + AbductiveDomain.Topl.large_step ~call_location ~callee_proc_name + ~substitution:call_state.subst ~condition:call_state.astate.path_condition ~callee_prepost:pre_post.AbductiveDomain.topl call_state.astate else call_state.astate in diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 0ae9299de..183b1a30c 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -11,8 +11,7 @@ module L = Logging type value = AbstractValue.t -type event = - | Call of {return: value option; arguments: value list; procname: Procname.t; loc: Location.t} +type event = Call of {return: value option; arguments: value list; procname: Procname.t} let pp_comma_seq f xs = Pp.comma_seq ~print_env:Pp.text_break f xs @@ -26,16 +25,17 @@ type vertex = ToplAutomaton.vindex type register = ToplAst.register_name +(* TODO(rgrigore): Change the memory assoc list to a Map. *) type configuration = {vertex: vertex; memory: (register * value) list} type predicate = Binop.t * PathCondition.operand * PathCondition.operand type step = - { step_event: event + { step_location: Location.t ; step_predecessor: simple_state (** state before this step *) - ; step_type: step_type } + ; step_data: step_data } -and step_type = SmallStep +and step_data = SmallStep of event | LargeStep of (Procname.t * (* post *) simple_state) (* TODO(rgrigore): | LargeStep of simple_state *) and simple_state = @@ -70,12 +70,14 @@ let pp_state f = Format.fprintf f "@[<2>[ %a ]@]" (pp_comma_seq pp_simple_state) let start () = let mk_simple_states () = let a = Topl.automaton () in - let starts = ToplAutomaton.starts a in - let mk_memory = - let registers = ToplAutomaton.registers a in - fun () -> List.map ~f:(fun r -> (r, AbstractValue.mk_fresh ())) registers + let memory = + List.map ~f:(fun r -> (r, AbstractValue.mk_fresh ())) (ToplAutomaton.registers a) + in + let configurations = + let n = ToplAutomaton.vcount a in + let f acc vertex = {vertex; memory} :: acc in + IContainer.forto n ~init:[] ~f in - let configurations = List.map ~f:(fun vertex -> {vertex; memory= mk_memory ()}) starts in List.map ~f:(fun c -> {pre= c; post= c; pruned= []; last_step= None}) configurations in if Topl.is_deep_active () then mk_simple_states () else (* Avoids work later *) [] @@ -220,12 +222,18 @@ let skip_pruned_of_nonskip_pruned nonskip_list = IList.product (List.map ~f:(List.map ~f:negate_predicate) nonskip_list) -let small_step path_condition event simple_states = +let drop_infeasible path_condition state = + let f {pruned} = not (is_unsat path_condition pruned) in + List.filter ~f state + + +let small_step loc path_condition event simple_states = let tmatches = static_match event in let evolve_transition (old : simple_state) (transition, tcontext) : state = let mk ?(memory = old.post.memory) ?(pruned = []) significant = let last_step = - if significant then Some {step_event= event; step_predecessor= old; step_type= SmallStep} + if significant then + Some {step_location= loc; step_predecessor= old; step_data= SmallStep event} else old.last_step in (* NOTE: old pruned is discarded, because evolve_simple_state needs to see only new prunes @@ -246,19 +254,17 @@ let small_step path_condition event simple_states = in let evolve_simple_state old = let path_condition = conjoin_pruned path_condition old.pruned in - let simplify result = - let f {pruned} = not (is_unsat path_condition pruned) in - List.filter ~f result - in let tmatches = List.filter ~f:(fun (t, _) -> Int.equal old.post.vertex t.ToplAutomaton.source) tmatches in - let nonskip = simplify (List.concat_map ~f:(evolve_transition old) tmatches) in + let nonskip = + drop_infeasible path_condition (List.concat_map ~f:(evolve_transition old) tmatches) + in let skip = let nonskip_pruned_list = List.map ~f:(fun {pruned} -> pruned) nonskip in let skip_pruned_list = skip_pruned_of_nonskip_pruned nonskip_pruned_list in let f pruned = {old with pruned} (* keeps last_step from old *) in - simplify (List.map ~f skip_pruned_list) + drop_infeasible path_condition (List.map ~f skip_pruned_list) in let add_old_pruned s = {s with pruned= List.rev_append s.pruned old.pruned} in List.map ~f:add_old_pruned (List.rev_append nonskip skip) @@ -268,7 +274,99 @@ let small_step path_condition event simple_states = result -let large_step ~substitution:_ ~condition:_ ~callee_prepost:_ _state = (* TODO *) [] +let sub_value (sub, value) = + match AbstractValue.Map.find_opt value sub with + | Some (v, _history) -> + (sub, v) + | None -> + let v = AbstractValue.mk_fresh () in + let sub = AbstractValue.Map.add value (v, []) sub in + (sub, v) + + +let sub_list sub_elem (sub, xs) = + let f (sub, xs) x = + let sub, x = sub_elem (sub, x) in + (sub, x :: xs) + in + let sub, xs = List.fold ~init:(sub, []) ~f xs in + (sub, List.rev xs) + + +let of_unequal = + List.Or_unequal_lengths.( + function + | Ok x -> + x + | Unequal_lengths -> + L.die InternalError "PulseTopl expected lists to be of equal lengths") + + +let sub_configuration (sub, {vertex; memory}) = + let keys, values = List.unzip memory in + let sub, values = sub_list sub_value (sub, values) in + let memory = of_unequal (List.zip keys values) in + (sub, {vertex; memory}) + + +let sub_predicate (sub, predicate) = + let avo x : PathCondition.operand = AbstractValueOperand x in + match (predicate : predicate) with + | op, AbstractValueOperand l, AbstractValueOperand r -> + let sub, l = sub_value (sub, l) in + let sub, r = sub_value (sub, r) in + (sub, (op, avo l, avo r)) + | op, AbstractValueOperand l, r -> + let sub, l = sub_value (sub, l) in + (sub, (op, avo l, r)) + | op, l, AbstractValueOperand r -> + let sub, r = sub_value (sub, r) in + (sub, (op, l, avo r)) + | _ -> + (sub, predicate) + + +let sub_pruned = sub_list sub_predicate + +(* Does not substitute in [last_step]: not usually needed, and takes much time. *) +let sub_simple_state (sub, {pre; post; pruned; last_step}) = + let sub, pre = sub_configuration (sub, pre) in + let sub, post = sub_configuration (sub, post) in + let sub, pruned = sub_pruned (sub, pruned) in + (sub, {pre; post; pruned; last_step}) + + +let sub_state = sub_list sub_simple_state + +let large_step ~call_location ~callee_proc_name ~substitution ~condition ~callee_prepost state = + let seq ((p : simple_state), (q : simple_state)) = + if not (Int.equal p.post.vertex q.pre.vertex) then None + else + let add_eq eqs (register, value_a) = + let value_b = + match List.Assoc.find ~equal:String.equal q.pre.memory register with + | Some x -> + x + | None -> + L.die InternalError "PulseTopl expects all registers in memory" + in + let op x = PathCondition.AbstractValueOperand x in + (Binop.Eq, op value_a, op value_b) :: eqs + in + let pruned = List.fold ~init:(p.pruned @ q.pruned) ~f:add_eq p.post.memory in + let last_step = + Some + { step_location= call_location + ; step_predecessor= p + ; step_data= LargeStep (callee_proc_name, q) } + in + Some {pre= p.pre; post= q.post; pruned; last_step} + 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 filter_for_summary path_condition state = List.filter ~f:(fun x -> not (is_unsat path_condition x.pruned)) state @@ -294,25 +392,37 @@ let simplify ~keep state = List.map ~f:simplify_simple_state state +let description_of_step_data step_data = + let procname = + match step_data with SmallStep (Call {procname}) | LargeStep (procname, _) -> procname + in + Format.fprintf Format.str_formatter "@[call to %a@]" Procname.pp procname ; + Format.flush_str_formatter () + + let report_errors proc_desc err_log state = let a = Topl.automaton () in - let rec make_trace acc q = + let rec make_trace nesting acc q = match q.last_step with | None -> acc - | Some {step_event; step_predecessor; step_type= SmallStep} -> - let (Call {loc; procname}) = step_event in - let description = - Format.fprintf Format.str_formatter "@[call to %a@]" Procname.pp procname ; - Format.flush_str_formatter () + | Some {step_location; step_predecessor; step_data} -> + let description = description_of_step_data step_data in + let acc = + Errlog.make_trace_element nesting step_location description [] + :: + ( match step_data with + | SmallStep _ -> + acc + | LargeStep (_, qq) -> + make_trace (nesting + 1) acc qq ) in - let e = Errlog.make_trace_element 0 loc description [] in - make_trace (e :: acc) step_predecessor + make_trace nesting acc step_predecessor in let report_simple_state q = if ToplAutomaton.is_start a q.pre.vertex && ToplAutomaton.is_error a q.post.vertex then let loc = Procdesc.get_loc proc_desc in - let ltr = make_trace [] q in + let ltr = make_trace 0 [] q in let message = Format.asprintf "%a" ToplAutomaton.pp_message_of_state (a, q.post.vertex) in Reporting.log_issue proc_desc err_log ~loc ~ltr ToplOnPulse IssueType.topl_pulse_error message in diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli index 42e833119..aba4ececf 100644 --- a/infer/src/pulse/PulseTopl.mli +++ b/infer/src/pulse/PulseTopl.mli @@ -9,18 +9,19 @@ open! IStd type value = PulseAbstractValue.t -type event = - | Call of {return: value option; arguments: value list; procname: Procname.t; loc: Location.t} +type event = Call of {return: value option; arguments: value list; procname: Procname.t} type state val start : unit -> state (** Return the initial state of [Topl.automaton ()]. *) -val small_step : PulsePathCondition.t -> event -> state -> state +val small_step : Location.t -> PulsePathCondition.t -> event -> state -> state val large_step : - substitution:(PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t + call_location:Location.t + -> callee_proc_name:Procname.t + -> substitution:(PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t -> condition:PulsePathCondition.t -> callee_prepost:state -> state diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index 52e8b8708..d3f7208dd 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -166,17 +166,6 @@ let get_start_error_pairs a = Hashtbl.data pairs -let pp_message_of_state fmt (a, i) = - let property, state = vname a i in - Format.fprintf fmt "property %s reaches state %s" property state - - -let starts a = - (* TODO(rgrigore): cache *) - let f i (_property, vname) = if String.equal vname "start" then Some i else None in - Array.to_list (Array.filter_mapi ~f a.states) - - let registers a = (* TODO(rgrigore): cache *) let do_assignment acc (r, _v) = String.Set.add acc r in @@ -192,6 +181,11 @@ let registers a = String.Set.to_list (Array.fold ~init:String.Set.empty ~f:do_transition a.transitions) +let pp_message_of_state fmt (a, i) = + let property, state = vname a i in + Format.fprintf fmt "property %s reaches state %s" property state + + let tfilter_map a ~f = Array.to_list (Array.filter_map ~f a.transitions) let pp_transition f {source; target; label} = diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index 012118826..2af1b1006 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/infer/src/topl/ToplAutomaton.mli @@ -54,13 +54,11 @@ val get_start_error_pairs : t -> (vindex * vindex) list vertex names, where [p] ranges over property names. POST: no vertex index occurs more than once in the result. *) +val registers : t -> ToplAst.register_name list + val pp_message_of_state : Format.formatter -> t * tindex -> unit (** Print "property P reaches state E". *) -val starts : t -> vindex list - -val registers : t -> ToplAst.register_name list - val is_start : t -> vindex -> bool val is_error : t -> vindex -> bool diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile index fb8e658f6..d6dc01c3f 100644 --- a/infer/tests/codetoanalyze/java/topl/Makefile +++ b/infer/tests/codetoanalyze/java/topl/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../.. -SUBDIRS = baos compareArgs hasnext skip servlet slowIter +SUBDIRS = baos compareArgs hasnext servlet slowIter test-%: $(MAKE) -C $* test diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile index fdb0cd519..74902bccc 100644 --- a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile +++ b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --pulse-max-disjuncts 50 --topl-properties CompareArgs.topl --topl-pulse-only +INFER_OPTIONS = --topl-properties CompareArgs.topl --pulse-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp index eeb35e163..1e7649911 100644 --- a/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int),call to int CompareArgs.max(int[],int,int)] +codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int CompareArgs.max(int[],int,int),call to int CompareArgs.max(int[],int,int)] diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile index f829e5cd4..ca72641cd 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile +++ b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --pulse-max-disjuncts 50 --topl-properties hasnext.topl --topl-pulse-only +INFER_OPTIONS = --topl-properties hasnext.topl --pulse-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp b/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp index e88c895c8..2d0e83612 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp @@ -1,3 +1,3 @@ -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Iterator List.iterator(),call to Object Iterator.next()] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Iterator List.iterator(),call to void Iterators.getSingleElementOk(Iterator),call to Object Iterator.next()] +codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Scanner ScannerFail.getScanner(),call to Scanner.(InputStream),call to String Scanner.next()] diff --git a/infer/tests/codetoanalyze/java/topl/skip/Makefile b/infer/tests/codetoanalyze/java/topl/skip/Makefile index cb5d14635..f7ff9003a 100644 --- a/infer/tests/codetoanalyze/java/topl/skip/Makefile +++ b/infer/tests/codetoanalyze/java/topl/skip/Makefile @@ -6,17 +6,9 @@ TESTS_DIR = ../../../.. INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 100000 --topl-properties SkipAfterRemove.topl --topl-biabd-only +#INFER_OPTIONS = --topl-properties SkipAfterRemove.topl --pulse-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) -# include $(TESTS_DIR)/javac.make - -.PHONY: test -test: ; - -.PHONY: replace -replace: ; - -.PHONY: clean -clean: ; +include $(TESTS_DIR)/javac.make diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile index 2d1443872..840a1a2a9 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile +++ b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --pulse-max-disjuncts 1500 --topl-properties slowIter.topl --topl-pulse-only +INFER_OPTIONS = --topl-properties slowIter.topl --pulse-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp b/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp index 8d2923e99..264bb46ac 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.aBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.bBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.aBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Set Map.keySet(),call to Iterator Set.iterator(),call to Object Iterator.next(),call to Object Map.get(Object)] +codetoanalyze/java/topl/slowIter/SlowIterTests.java, SlowIterTests.bBad(java.util.Map):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to Set Map.keySet(),call to Iterator Set.iterator(),call to Object Iterator.next(),call to void SlowIterTests.print(Object,Map),call to Object Map.get(Object)]