From fd3f298156930e1f89e0e1504dffea9d60e26671 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 23 Oct 2018 22:48:13 -0700 Subject: [PATCH] [inferbo] Add narrowing Reviewed By: jvillard Differential Revision: D10334140 fbshipit-source-id: afb247866 --- infer/src/absint/AbstractInterpreter.ml | 115 ++++++++++------- infer/src/absint/AbstractInterpreter.mli | 11 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 11 +- .../codetoanalyze/c/performance/issues.exp | 119 +++++++++--------- .../codetoanalyze/java/performance/issues.exp | 47 ++++--- 6 files changed, 164 insertions(+), 141 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index c14fca8a7..6b64e85c0 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -57,19 +57,24 @@ module type S = sig type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t val compute_post : - ?debug:debug + ?do_narrowing:bool + -> ?debug:debug -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> TransferFunctions.Domain.astate option val exec_cfg : - TransferFunctions.CFG.t + ?do_narrowing:bool + -> TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map val exec_pdesc : - TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map + ?do_narrowing:bool + -> TransferFunctions.extras ProcData.t + -> initial:TransferFunctions.Domain.astate + -> invariant_map val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option @@ -171,7 +176,10 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s else on_instrs instrs - let exec_node ~debug ({ProcData.pdesc} as proc_data) node ~is_loop_head astate_pre inv_map = + (* Note on narrowing operations: we defines the narrowing operations simply to take a smaller one. + So, as of now, the termination of narrowing is not guaranteed in general. *) + let exec_node ~debug ({ProcData.pdesc} as proc_data) node ~is_loop_head ~is_narrowing astate_pre + inv_map = let node_id = Node.id node in let update_inv_map pre ~visit_count = let inv_map' = exec_instrs ~debug proc_data node node_id ~visit_count pre inv_map in @@ -179,8 +187,8 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s in if InvariantMap.mem node_id inv_map then let old_state = InvariantMap.find node_id inv_map in - let widened_pre = - if is_loop_head then ( + let new_pre = + if is_loop_head && not is_narrowing then ( let num_iters = (old_state.State.visit_count :> int) in let prev = old_state.State.pre in let next = astate_pre in @@ -190,10 +198,13 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s res ) else astate_pre in - if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.State.pre then (inv_map, ReachedFixPoint) + if + ((not is_narrowing) && Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) + || (is_narrowing && Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre) + then (inv_map, ReachedFixPoint) else let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in - update_inv_map widened_pre ~visit_count:visit_count' + update_inv_map new_pre ~visit_count:visit_count' else (* first time visiting this node *) update_inv_map astate_pre ~visit_count:VisitCount.first_time @@ -217,15 +228,15 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s (** compute and return an invariant map for [pdesc] *) - let make_exec_pdesc ~exec_cfg_internal ({ProcData.pdesc} as proc_data) ~initial = - exec_cfg_internal ~debug:Default (CFG.from_pdesc pdesc) proc_data ~initial + let make_exec_pdesc ~exec_cfg_internal ({ProcData.pdesc} as proc_data) ~do_narrowing ~initial = + exec_cfg_internal ~debug:Default (CFG.from_pdesc pdesc) proc_data ~do_narrowing ~initial (** compute and return the postcondition of [pdesc] *) let make_compute_post ~exec_cfg_internal ?(debug = Default) ({ProcData.pdesc} as proc_data) - ~initial = + ~do_narrowing ~initial = let cfg = CFG.from_pdesc pdesc in - let inv_map = exec_cfg_internal ~debug cfg proc_data ~initial in + let inv_map = exec_cfg_internal ~debug cfg proc_data ~do_narrowing ~initial in extract_post (Node.id (CFG.exit_node cfg)) inv_map end @@ -244,7 +255,10 @@ struct match compute_pre cfg node inv_map with | Some astate_pre -> ( let is_loop_head = CFG.is_loop_head pdesc node in - match exec_node ~debug proc_data node ~is_loop_head astate_pre inv_map with + match + exec_node ~debug proc_data node ~is_loop_head ~is_narrowing:false astate_pre + inv_map + with | inv_map, ReachedFixPoint -> (inv_map, work_queue') | inv_map, DidNotReachFixPoint -> @@ -258,20 +272,21 @@ struct (* compute and return an invariant map for [cfg] *) - let exec_cfg_internal ~debug cfg proc_data ~initial = + let exec_cfg_internal ~debug cfg proc_data ~do_narrowing:_ ~initial = let start_node = CFG.start_node cfg in let inv_map, _did_not_reach_fix_point = - exec_node ~debug proc_data start_node ~is_loop_head:false initial InvariantMap.empty + exec_node ~debug proc_data start_node ~is_loop_head:false ~is_narrowing:false initial + InvariantMap.empty in let work_queue = Scheduler.schedule_succs (Scheduler.empty cfg) start_node in exec_worklist ~debug cfg proc_data work_queue inv_map - let exec_cfg = exec_cfg_internal ~debug:Default + let exec_cfg ?do_narrowing:_ = exec_cfg_internal ~debug:Default ~do_narrowing:false - let exec_pdesc = make_exec_pdesc ~exec_cfg_internal + let exec_pdesc ?do_narrowing:_ = make_exec_pdesc ~exec_cfg_internal ~do_narrowing:false - let compute_post = make_compute_post ~exec_cfg_internal + let compute_post ?do_narrowing:_ = make_compute_post ~exec_cfg_internal ~do_narrowing:false end module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct @@ -293,57 +308,65 @@ module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct NodePrinter.finish_session underlying_node - let exec_wto_node ~debug cfg proc_data inv_map node ~is_loop_head = + let exec_wto_node ~debug cfg proc_data inv_map node ~is_loop_head ~is_narrowing = match compute_pre cfg node inv_map with | Some astate_pre -> - exec_node ~debug proc_data node ~is_loop_head astate_pre inv_map + exec_node ~debug proc_data node ~is_loop_head ~is_narrowing astate_pre inv_map | None -> L.(die InternalError) "Could not compute the pre of a node" - let rec exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head rest = - match exec_wto_node ~debug cfg proc_data inv_map head ~is_loop_head with + let rec exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head ~is_narrowing rest = + match exec_wto_node ~debug cfg proc_data inv_map head ~is_loop_head ~is_narrowing with | inv_map, ReachedFixPoint -> inv_map | inv_map, DidNotReachFixPoint -> - let inv_map = exec_wto_partition ~debug cfg proc_data inv_map rest in - exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head:true rest + let inv_map = exec_wto_partition ~debug cfg proc_data ~is_narrowing inv_map rest in + exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head:true ~is_narrowing rest - and exec_wto_partition ~debug cfg proc_data inv_map + and exec_wto_partition ~debug cfg proc_data ~is_narrowing inv_map (partition : CFG.Node.t WeakTopologicalOrder.Partition.t) = match partition with | Empty -> inv_map | Node {node; next} -> - let inv_map = exec_wto_node ~debug cfg proc_data inv_map node ~is_loop_head:false |> fst in - exec_wto_partition ~debug cfg proc_data inv_map next - | Component {head; rest; next} -> let inv_map = - exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head:false rest + exec_wto_node ~debug cfg proc_data ~is_narrowing inv_map node ~is_loop_head:false |> fst in - exec_wto_partition ~debug cfg proc_data inv_map next - - - let exec_cfg_internal ~debug cfg proc_data ~initial = - match CFG.wto cfg with - | Empty -> - InvariantMap.empty (* empty cfg *) - | Node {node= start_node; next} as wto -> - if Config.write_html then debug_wto wto start_node ; - let inv_map, _did_not_reach_fix_point = - exec_node ~debug proc_data start_node ~is_loop_head:false initial InvariantMap.empty + exec_wto_partition ~debug cfg proc_data ~is_narrowing inv_map next + | Component {head; rest; next} -> + let inv_map = + exec_wto_component ~debug cfg proc_data inv_map head ~is_loop_head:false ~is_narrowing + rest in - exec_wto_partition ~debug cfg proc_data inv_map next - | Component _ -> - L.(die InternalError) "Did not expect the start node to be part of a loop" + exec_wto_partition ~debug cfg proc_data ~is_narrowing inv_map next + + + let exec_cfg_internal ~debug cfg proc_data ~do_narrowing ~initial = + let wto = CFG.wto cfg in + let exec_cfg ~is_narrowing inv_map = + match wto with + | Empty -> + inv_map (* empty cfg *) + | Node {node= start_node; next} as wto -> + if Config.write_html then debug_wto wto start_node ; + let inv_map, _did_not_reach_fix_point = + exec_node ~debug proc_data start_node ~is_loop_head:false ~is_narrowing initial inv_map + in + exec_wto_partition ~debug cfg proc_data ~is_narrowing inv_map next + | Component _ -> + L.(die InternalError) "Did not expect the start node to be part of a loop" + in + let inv_map = exec_cfg ~is_narrowing:false InvariantMap.empty in + if do_narrowing then exec_cfg ~is_narrowing:true inv_map else inv_map - let exec_cfg = exec_cfg_internal ~debug:Default + let exec_cfg ?(do_narrowing = false) = exec_cfg_internal ~debug:Default ~do_narrowing - let exec_pdesc = make_exec_pdesc ~exec_cfg_internal + let exec_pdesc ?(do_narrowing = false) = make_exec_pdesc ~exec_cfg_internal ~do_narrowing - let compute_post = make_compute_post ~exec_cfg_internal + let compute_post ?(do_narrowing = false) = make_compute_post ~exec_cfg_internal ~do_narrowing end module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index eab9942a2..d2b6489a8 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/infer/src/absint/AbstractInterpreter.mli @@ -27,21 +27,26 @@ module type S = sig type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t val compute_post : - ?debug:debug + ?do_narrowing:bool + -> ?debug:debug -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> TransferFunctions.Domain.astate option (** compute and return the postcondition for the given procedure starting from [initial]. *) val exec_cfg : - TransferFunctions.CFG.t + ?do_narrowing:bool + -> TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map (** compute and return invariant map for the given CFG/procedure starting from [initial]. *) val exec_pdesc : - TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map + ?do_narrowing:bool + -> TransferFunctions.extras ProcData.t + -> initial:TransferFunctions.Domain.astate + -> invariant_map (** compute and return invariant map for the given procedure starting from [initial] *) val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 236b8bdea..362076b67 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -798,7 +798,7 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_ let pdata = ProcData.make proc_desc tenv symbol_table in let cfg = CFG.from_pdesc proc_desc in let initial = Init.initial_state pdata (CFG.start_node cfg) in - let inv_map = Analyzer.exec_pdesc ~initial pdata in + let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in let locals = get_local_decls proc_desc in let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 98722b3c1..1b2432536 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -23,7 +23,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64] codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ] +codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [2, +oo] Size: 2 by call to `array_min_index_from_one_FP` ] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] @@ -32,7 +32,6 @@ codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_O codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2] codetoanalyze/c/bufferoverrun/big_array.c, use_big_array_bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Assignment,Return,Assignment,ArrayAccess: Offset: 999999999 Size: 26460] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: -1 Size: 10] @@ -45,7 +44,6 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10 by call to `do_while_sub` ] -codetoanalyze/c/bufferoverrun/do_while.c, do_while_sub, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: 1 Size: 1 by call to `two_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ] @@ -70,7 +68,7 @@ codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFL codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Assignment,Binop: ([1, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([5, +oo] * 4):unsigned64] codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([0, +oo] + 5):signed32] @@ -136,7 +134,8 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] -codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024] codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] @@ -188,4 +187,4 @@ codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, no_bucket, ERROR, [] -codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index be1cf7e3b..f86cd8176 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -1,23 +1,22 @@ -codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * p.ub, degree = 1] +codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * p.ub + 4 * (1+max(0, p.ub)), degree = 1] codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] -codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 * m.ub, degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * m.ub + 4 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * m.ub + 4 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * m.ub + 4 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * m.ub + 4 * (1+max(0, m.ub)), degree = 1] codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] -codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 603, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] @@ -33,10 +32,10 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3528, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] -codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * p.ub, degree = 1] -codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * p.ub, degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 2 * p.ub + 5 * (1+max(0, p.ub)), degree = 1] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] @@ -48,9 +47,9 @@ codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_ codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0] -codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 12 * k.ub, degree = 1] -codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 12 * k.ub, degree = 1] -codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 12 * k.ub, degree = 1] +codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 10 * k.ub + 2 * (1+max(0, k.ub)), degree = 1] +codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 10 * k.ub + 2 * (1+max(0, k.ub)), degree = 1] +codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 10 * k.ub + 2 * (1+max(0, k.ub)), degree = 1] codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 206, degree = 0] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (-m.lb + 20), degree = 1] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (-m.lb + 20), degree = 1] @@ -109,35 +108,33 @@ codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_ codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 548, degree = 0] codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14006, degree = 0] -codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * (m.ub + -1) * m.ub + 11 * m.ub, degree = 2] -codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * (m.ub + -1) * m.ub + 11 * m.ub, degree = 2] -codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * m.ub + 7 * m.ub^2, degree = 2] -codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * m.ub + 7 * m.ub^2, degree = 2] -codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * n.ub, degree = 1] -codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 7 * n.ub, degree = 1] -codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * n.ub, degree = 1] -codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * n.ub, degree = 1] -codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1] -codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1] -codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2] -codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2] -codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2] -codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2] -codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 9 * n.ub + 5 * (max(1, n.ub)) * (1+max(0, m.ub)), degree = 2] -codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 * p.ub + 17 * (max(1, p.ub)), degree = 1] -codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 * p.ub + 17 * (max(1, p.ub)), degree = 1] -codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 * p.ub + 17 * (max(1, p.ub)), degree = 1] -codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 * p.ub + 17 * (max(1, p.ub)), degree = 1] -codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 * p.ub + 17 * (max(1, p.ub)), degree = 1] +codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub * (max(0, m.ub)) + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2] +codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub * (max(0, m.ub)) + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2] +codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub^2 + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2] +codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * m.ub + 5 * m.ub^2 + 2 * m.ub * (1+max(0, m.ub)) + 2 * (1+max(0, m.ub)), degree = 2] +codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * n.ub + 2 * (1+max(0, n.ub)), degree = 1] +codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * n.ub + 2 * (1+max(0, n.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * n.ub + 2 * (1+max(0, n.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 3 * n.ub + 2 * (1+max(0, n.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * n.ub + 2 * (1+max(0, n.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 * n.ub + 2 * (1+max(0, n.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2] +codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2] +codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2] +codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2] +codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 * (max(1, n.ub)) * (1+max(0, m.ub)) + 2 * (1+max(1, n.ub)) * (2+max(0, m.ub)) + 7 * (2+max(1, n.ub)), degree = 2] +codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1] +codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * p.ub + 17 * (max(1, p.ub)) + 2 * (1+max(1, p.ub)), degree = 1] codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0] codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0] -codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2005, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] -codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 227, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] @@ -154,28 +151,28 @@ codetoanalyze/c/performance/loops.c, if_out_loop, 8, EXPENSIVE_EXECUTION_TIME_CA codetoanalyze/c/performance/loops.c, if_out_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 514, degree = 0] codetoanalyze/c/performance/loops.c, larger_state_FN, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] codetoanalyze/c/performance/loops.c, larger_state_FN, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] -codetoanalyze/c/performance/loops.c, larger_state_FN, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/loops.c, larger_state_FN, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] codetoanalyze/c/performance/loops.c, larger_state_FN, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] -codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] -codetoanalyze/c/performance/switch_continue.c, test_switch, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] -codetoanalyze/c/performance/switch_continue.c, test_switch, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] -codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] -codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604, degree = 0] +codetoanalyze/c/performance/switch_continue.c, test_switch, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601, degree = 0] +codetoanalyze/c/performance/switch_continue.c, test_switch, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601, degree = 0] +codetoanalyze/c/performance/switch_continue.c, test_switch, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601, degree = 0] +codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601, degree = 0] +codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 601, degree = 0] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Binop: (n + [-oo, +oo]):signed32] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 15, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Assignment,Binop: ([-oo, +oo] - 1):signed32] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 14 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 14 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 11 + 14 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * m.ub + 7 * k.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * m.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * m.ub + 7 * k.ub, degree = 1] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 11 + 7 * m.ub + 7 * k.ub, degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 10 * m.ub + 4 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 10 * m.ub + 4 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 10 * m.ub + 4 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * m.ub + 5 * k.ub + 2 * (1+max(0, m.ub)) + 2 * (1+max(0, k.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * m.ub + 5 * k.ub + 2 * (1+max(0, m.ub)) + 2 * (1+max(0, k.ub)), degree = 1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * m.ub + 5 * k.ub + 2 * (1+max(0, m.ub)) + 2 * (1+max(0, k.ub)), degree = 1] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index f6d73938e..ce3ce1ab5 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -1,7 +1,7 @@ codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [2, 8] Size: 8] -codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 * length.ub, degree = 1] -codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 15 * length.ub, degree = 1] -codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 * length.ub, degree = 1] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 * length.ub + 3 * (1+max(0, length.ub)), degree = 1] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * length.ub + 3 * (1+max(0, length.ub)), degree = 1] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * length.ub + 3 * (1+max(0, length.ub)), degree = 1] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * mag.length.ub, degree = 1] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * mag.length.ub, degree = 1] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0] @@ -37,14 +37,14 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_h codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 2 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 * p.ub, degree = 1] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub, degree = 1] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * p.ub, degree = 1] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)), degree = 2] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)), degree = 2] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)), degree = 2] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, -1+max(1, maxI.ub)] + [0, maxJ.ub + -1]):signed32] -codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 9 * maxI.ub + 3 * maxJ.ub * (max(1, maxI.ub)) + 10 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 4 * p.ub + 3 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 * p.ub + 3 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 * p.ub + 3 * (1+max(0, p.ub)), degree = 1] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, max(1, maxI.ub)] + [0, 1+max(0, maxJ.ub)]):signed32] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (max(1, maxI.ub)) * (1+max(0, maxJ.ub)) + 8 * (1+max(1, maxI.ub)) * (2+max(0, maxJ.ub)) + 4 * (2+max(1, maxI.ub)), degree = 2] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] @@ -52,8 +52,8 @@ codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_ codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 * (mSubscribers.length.ub + -1) + 4 * mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 * (mSubscribers.length.ub + -1) + 4 * mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] -codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * m.ub, degree = 1] -codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * m.ub, degree = 1] +codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] +codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 * m.ub + 2 * (1+max(0, m.ub)), degree = 1] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] @@ -103,15 +103,14 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * test.a.ub, degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * (k.ub + -1), degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * (max(1, k.ub)), degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * (max(1, k.ub)), degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * (max(1, k.ub)), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: size,Binop: (size + [-oo, +oo]):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 9 * items.length.ub, degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 * items.length.ub, degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * items.length.ub + 4 * (items.length.ub + 1), degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * items.length.ub + 4 * (items.length.ub + 1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 * (size.ub + 20), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 * (size.ub + 20), degree = 1] @@ -133,18 +132,18 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 251, degree = 0] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 29 * (length.ub + -1), degree = 1] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 * (length.ub + -1), degree = 1] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 * (length.ub + -1), degree = 1] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 26 * (length.ub + -1) + 3 * (max(1, length.ub)), degree = 1] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 26 * (length.ub + -1) + 3 * (max(1, length.ub)), degree = 1] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 26 * (length.ub + -1) + 3 * (max(1, length.ub)), degree = 1] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort_FP(long[],long[],int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort_FP(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (a[*] * b[*]):signed64] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([10, +oo] + 1):signed32] -codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 799, degree = 0] +codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0] +codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []