From 9591276541579c897429abdad412cdde9210c87d Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Thu, 27 Aug 2020 04:38:25 -0700 Subject: [PATCH] [topl] Cheap port to Pulse. Summary: Report errors found by running Topl on top of Pulse, when using --topl-pulse. Topl tests now run on top of Pulse. Reviewed By: jvillard Differential Revision: D23030771 fbshipit-source-id: 8770c2902 --- infer/man/man1/infer-full.txt | 3 +- infer/man/man1/infer-report.txt | 3 +- infer/man/man1/infer.txt | 3 +- infer/src/base/IssueType.ml | 8 ++- infer/src/base/IssueType.mli | 4 +- infer/src/pulse/PulseCItv.ml | 2 + infer/src/pulse/PulseCItv.mli | 3 + infer/src/pulse/PulseFormula.ml | 7 +++ infer/src/pulse/PulseFormula.mli | 2 + infer/src/pulse/PulsePathCondition.ml | 7 +++ infer/src/pulse/PulsePathCondition.mli | 4 ++ infer/src/topl/Topl.ml | 63 ++++++++++++++++--- infer/src/topl/ToplUtils.ml | 7 ++- infer/src/topl/ToplUtils.mli | 2 + infer/tests/codetoanalyze/java/topl/Makefile | 2 +- .../codetoanalyze/java/topl/baos/Makefile | 2 +- .../codetoanalyze/java/topl/baos/issues.exp | 10 +-- .../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/servlet/Makefile | 2 +- .../java/topl/servlet/issues.exp | 6 +- .../codetoanalyze/java/topl/slowIter/Makefile | 2 +- .../java/topl/slowIter/SlowIterTests.java | 5 +- .../java/topl/slowIter/issues.exp | 2 + 26 files changed, 122 insertions(+), 41 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/topl/slowIter/issues.exp diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index f8f36483a..cade5c054 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -495,7 +495,8 @@ OPTIONS STRONG_SELF_NOT_CHECKED (enabled by default), Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), - TOPL_ERROR (enabled by default), + TOPL_BIABD_ERROR (enabled by default), + TOPL_PULSE_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index f16e2b5e9..070a6844a 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -214,7 +214,8 @@ OPTIONS STRONG_SELF_NOT_CHECKED (enabled by default), Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), - TOPL_ERROR (enabled by default), + TOPL_BIABD_ERROR (enabled by default), + TOPL_PULSE_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 137d42a91..2721c7bf7 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -495,7 +495,8 @@ OPTIONS STRONG_SELF_NOT_CHECKED (enabled by default), Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), - TOPL_ERROR (enabled by default), + TOPL_BIABD_ERROR (enabled by default), + TOPL_PULSE_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), UNREACHABLE_CODE (enabled by default), UNTRUSTED_BUFFER_ACCESS (disabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index a20b2177a..0d8f2cb45 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -860,8 +860,12 @@ let complexity_increase ~kind ~is_on_ui_thread = register_cost ~kind ~is_on_ui_thread "%s_COMPLEXITY_INCREASE" -let topl_error = - register ~id:"TOPL_ERROR" Error ToplOnBiabduction ~user_documentation:"Experimental." +let topl_biabd_error = + register ~id:"TOPL_BIABD_ERROR" Error ToplOnBiabduction ~user_documentation:"Experimental." + + +let topl_pulse_error = + register ~id:"TOPL_PULSE_ERROR" Error ToplOnPulse ~user_documentation:"Experimental." let uninitialized_value = diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index ac17c9651..a3c7dc1f2 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -308,7 +308,9 @@ val symexec_memory_error : t val thread_safety_violation : t -val topl_error : t +val topl_biabd_error : t + +val topl_pulse_error : t val uninitialized_value : t diff --git a/infer/src/pulse/PulseCItv.ml b/infer/src/pulse/PulseCItv.ml index fbd3dbb50..b04f5fa65 100644 --- a/infer/src/pulse/PulseCItv.ml +++ b/infer/src/pulse/PulseCItv.ml @@ -174,6 +174,8 @@ let is_equal_to_zero = function false +let as_int = function Between (Int l, Int u) when IntLit.eq l u -> IntLit.to_int l | _ -> None + let has_empty_intersection a1 a2 = match (a1, a2) with | Outside _, Outside _ -> diff --git a/infer/src/pulse/PulseCItv.mli b/infer/src/pulse/PulseCItv.mli index a70ecd2d9..3a52ed98c 100644 --- a/infer/src/pulse/PulseCItv.mli +++ b/infer/src/pulse/PulseCItv.mli @@ -15,6 +15,9 @@ val equal_to : IntLit.t -> t val is_equal_to_zero : t -> bool +val as_int : t -> int option +(** [as_int v] returns [Some x] if [v] is known to be [x] *) + val pp : F.formatter -> t -> unit type abduction_result = diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 240149d01..c72ebab7d 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1383,3 +1383,10 @@ let simplify ~keep phi = let is_known_zero phi v = Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs |> Option.exists ~f:LinArith.is_zero + + +let as_int phi v = + let maybe_int q = if Z.equal (Q.den q) Z.one then Q.to_int q else None in + let open Option.Monad_infix in + Var.Map.find_opt (VarUF.find phi.var_eqs v :> Var.t) phi.linear_eqs + >>= LinArith.get_as_const >>= maybe_int diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index 97eabb0e1..47bc9e3f8 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -56,6 +56,8 @@ val and_fold_subst_variables : val is_known_zero : t -> Var.t -> bool +val as_int : t -> Var.t -> int option + (** {3 Notations} *) include sig diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 1532d1875..0a5b25303 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -378,3 +378,10 @@ let is_unsat_expensive phi = (false_, true) | Sat formula -> ({phi with formula}, false) + + +let as_int phi v = + (* TODO(rgrigore): Ask BoItvs too. *) + IList.force_until_first_some + [ lazy (CItvs.find_opt v phi.citvs |> Option.value_map ~default:None ~f:CItv.as_int) + ; lazy (Formula.as_int phi.formula v) ] diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 5c135928f..160c0a925 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -57,3 +57,7 @@ val is_unsat_cheap : t -> bool val is_unsat_expensive : t -> t * bool (** whether the state contains a contradiction, only call this when you absolutely have to *) + +val as_int : t -> AbstractValue.t -> int option +(** [as_int phi t] returns an integer x such that [phi |- t = x], if known for sure; see also + [is_known_zero] *) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 47f56128b..336e7b4bb 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -227,6 +227,11 @@ let conjoin_props env post pre = List.fold ~init:post ~f:(Prop.prop_atom_and env) (Prop.get_pure pre) +let message_of_state state = + let property, _vname = ToplAutomaton.vname (Lazy.force automaton) state in + Printf.sprintf "property %s reaches error" property + + (** For each (pre, post) pair of symbolic heaps and each (start, error) pair of Topl automata states, define @@ -252,8 +257,8 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi L.die InternalError "Topl.add_errors should only be called after RE_EXECUTION" in let extract_specs x = BiabductionSummary.(normalized_specs_to_specs x.preposts) in - Option.iter ~f:check_phase biabduction_summary ; - Option.value_map ~default:[] ~f:extract_specs biabduction_summary + check_phase biabduction_summary ; + extract_specs biabduction_summary in let subscript varname sub = Printf.sprintf "%s_%s" varname sub in let subscript_pre varname = subscript varname "pre" in @@ -279,11 +284,10 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi let phi = conjoin_props tenv post pre_start in let psi = Prop.conjoin_neq tenv error_exp state_post_value phi in if (not (is_inconsistent tenv phi)) && is_inconsistent tenv psi then ( - let property, _vname = ToplAutomaton.vname (Lazy.force automaton) error in - let message = Printf.sprintf "property %s reaches error" property in + let message = message_of_state error in tt "WARN@\n" ; - Reporting.log_issue proc_desc err_log ToplOnBiabduction IssueType.topl_error ~loc - message ) + Reporting.log_issue proc_desc err_log ToplOnBiabduction IssueType.topl_biabd_error + ~loc message ) in (* Don't warn if [lookup_static_var] fails. *) Option.iter ~f:handle_state_post_value (lookup_static_var tenv state_var post) @@ -300,9 +304,48 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi List.iter ~f:handle_preposts preposts -let add_errors_pulse _analysis_data _summary = - (* TODO(rgrigore): Do something similar to add_errors_biabduction, but for pulse summaries. *) - () +let add_errors_pulse {InterproceduralAnalysis.proc_desc; err_log} pulse_summary = + let pulse_summary = + let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in + List.filter_map ~f pulse_summary + in + let proc_name = Procdesc.get_proc_name proc_desc in + if not (ToplUtils.is_synthesized proc_name) then + let start_to_error = + Lazy.force automaton |> ToplAutomaton.get_start_error_pairs |> Int.Table.of_alist_exn + in + let topl_property_var = Var.of_pvar ToplUtils.topl_class_pvar in + let topl_state_field = HilExp.Access.FieldAccess (ToplUtils.make_field ToplName.state) in + let check_pre_post pre_post = + let open IOption.Let_syntax in + let path_condition = pre_post.PulseAbductiveDomain.path_condition in + let get_topl_state_opt pulse_state = + let stack = pulse_state.PulseBaseDomain.stack in + let heap = pulse_state.PulseBaseDomain.heap in + let* topl_property_addr, _ = PulseBaseStack.find_opt topl_property_var stack in + let* state_addr, _ = + PulseBaseMemory.find_edge_opt topl_property_addr topl_state_field heap + in + let* state_val, _ = + PulseBaseMemory.find_edge_opt state_addr HilExp.Access.Dereference heap + in + PulsePathCondition.as_int path_condition state_val + in + let* pre_topl = get_topl_state_opt (pre_post.PulseAbductiveDomain.pre :> PulseBaseDomain.t) in + let* post_topl = + get_topl_state_opt (pre_post.PulseAbductiveDomain.post :> PulseBaseDomain.t) + in + let* error_topl = Int.Table.find start_to_error pre_topl in + if Int.equal post_topl error_topl then Some error_topl else None + in + let errors = List.filter_map ~f:check_pre_post pulse_summary in + let errors = Int.Set.to_list (Int.Set.of_list errors) in + let loc = Procdesc.get_loc proc_desc in + let report error_state = + let m = message_of_state error_state in + Reporting.log_issue proc_desc err_log ToplOnPulse IssueType.topl_pulse_error ~loc m + in + List.iter ~f:report errors let sourcefile () = @@ -318,7 +361,7 @@ let cfg () = let analyze_with analyze postprocess analysis_data = if is_active () then instrument analysis_data ; let summary = analyze analysis_data in - if is_active () then postprocess analysis_data summary ; + if is_active () then Option.iter ~f:(postprocess analysis_data) summary ; summary diff --git a/infer/src/topl/ToplUtils.ml b/infer/src/topl/ToplUtils.ml index 9a8f898db..388f1c04e 100644 --- a/infer/src/topl/ToplUtils.ml +++ b/infer/src/topl/ToplUtils.ml @@ -28,12 +28,13 @@ let topl_call ret_id (ret_typ : Typ.desc) loc method_name arg_ts : Sil.instr = Sil.Call ((ret_id, Typ.mk ret_typ), e_fun, arg_ts, loc, CallFlags.default) -let topl_class_exp = +let topl_class_pvar = let class_name = Mangled.from_string ToplName.topl_property in - let var_name = Pvar.mk_global class_name in - Exp.Lvar var_name + Pvar.mk_global class_name +let topl_class_exp = Exp.Lvar topl_class_pvar + let make_field field_name = Fieldname.make (Typ.Name.Java.from_string ToplName.topl_property) field_name diff --git a/infer/src/topl/ToplUtils.mli b/infer/src/topl/ToplUtils.mli index 898df46a5..a9d45161d 100644 --- a/infer/src/topl/ToplUtils.mli +++ b/infer/src/topl/ToplUtils.mli @@ -17,6 +17,8 @@ val topl_class_name : Typ.Name.t val topl_class_typ : Typ.t +val topl_class_pvar : Pvar.t + val static_var : string -> Exp.t val local_var : Procname.t -> string -> Exp.t diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile index fcc22df4f..fb8e658f6 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 +SUBDIRS = baos compareArgs hasnext skip servlet slowIter test-%: $(MAKE) -C $* test diff --git a/infer/tests/codetoanalyze/java/topl/baos/Makefile b/infer/tests/codetoanalyze/java/topl/baos/Makefile index 97a75295d..9e575075c 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/Makefile +++ b/infer/tests/codetoanalyze/java/topl/baos/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 13000 --topl-properties baos.topl --topl-biabd-only +INFER_OPTIONS = --pulse-max-disjuncts 400 --topl-properties baos.topl --topl-pulse-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/baos/issues.exp b/infer/tests/codetoanalyze/java/topl/baos/issues.exp index 7831016ed..407d07d02 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_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile b/infer/tests/codetoanalyze/java/topl/compareArgs/Makefile index 7775a698f..fdb0cd519 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 = --seconds-per-iteration 10 --symops-per-iteration 4000 --topl-properties CompareArgs.topl --topl-biabd-only +INFER_OPTIONS = --pulse-max-disjuncts 50 --topl-properties CompareArgs.topl --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 521c632e2..eeb35e163 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_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] +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, [] diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/Makefile b/infer/tests/codetoanalyze/java/topl/hasnext/Makefile index 1c2a9ea6c..f829e5cd4 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 = --seconds-per-iteration 100 --symops-per-iteration 10000 --topl-properties hasnext.topl --topl-biabd-only +INFER_OPTIONS = --pulse-max-disjuncts 50 --topl-properties hasnext.topl --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 27167c274..e88c895c8 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_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] +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, [] diff --git a/infer/tests/codetoanalyze/java/topl/servlet/Makefile b/infer/tests/codetoanalyze/java/topl/servlet/Makefile index be0119489..91d84bafd 100644 --- a/infer/tests/codetoanalyze/java/topl/servlet/Makefile +++ b/infer/tests/codetoanalyze/java/topl/servlet/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../../.. -INFER_OPTIONS = --seconds-per-iteration 20 --symops-per-iteration 60000 --topl-properties servlet.topl --topl-biabd-only +INFER_OPTIONS = --pulse-max-disjuncts 100 --topl-properties servlet.topl --topl-pulse-only INFERPRINT_OPTIONS = --issues-tests TEST_CLASSPATH = javax.servlet-api-4.0.1.jar diff --git a/infer/tests/codetoanalyze/java/topl/servlet/issues.exp b/infer/tests/codetoanalyze/java/topl/servlet/issues.exp index ce8e099f5..f4becec2d 100644 --- a/infer/tests/codetoanalyze/java/topl/servlet/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/servlet/issues.exp @@ -1,3 +1,3 @@ -codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.aBad(javax.servlet.ServletResponse):void, 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.bBad(javax.servlet.ServletResponse):void, 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.cBad(javax.servlet.ServletRequest,javax.servlet.ServletResponse,javax.servlet.RequestDispatcher):void, 0, TOPL_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.aBad(javax.servlet.ServletResponse):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.bBad(javax.servlet.ServletResponse):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/servlet/ServletTests.java, ServletTests.cBad(javax.servlet.ServletRequest,javax.servlet.ServletResponse,javax.servlet.RequestDispatcher):void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile index e68c16dfc..2d1443872 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 = --seconds-per-iteration 10 --symops-per-iteration 20000 --topl-properties slowIter.topl --topl-biabd-only +INFER_OPTIONS = --pulse-max-disjuncts 1500 --topl-properties slowIter.topl --topl-pulse-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java b/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java index 465566a22..4e523e922 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java +++ b/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java @@ -8,8 +8,7 @@ import java.util.Map; class SlowIterTests { - // T62611635 - static void FN_aBad(Map m) { + static void aBad(Map m) { for (K k : m.keySet()) { System.out.printf("%s -> %s\n", k, m.get(k)); } @@ -22,7 +21,7 @@ class SlowIterTests { } // Inter-procedural variant of aBad. - static void FN_bBad(Map m) { + static void bBad(Map m) { for (K k : m.keySet()) { print(k, m); } diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp b/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp new file mode 100644 index 000000000..8d2923e99 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/slowIter/issues.exp @@ -0,0 +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, []