diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 295e29b96..309f4f772 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -357,3 +357,5 @@ let untrusted_url_risk = from_string "UNTRUSTED_URL_RISK" let untrusted_variable_length_array = from_string "UNTRUSTED_VARIABLE_LENGTH_ARRAY" let wrong_argument_number = from_string "Wrong_argument_number" ~hum:"Wrong Argument Number" + +let zero_execution_time_call = from_string ~enabled:false "ZERO_EXECUTION_TIME_CALL" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index a4bca6a14..efc0880a5 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -270,3 +270,5 @@ val untrusted_variable_length_array : t val user_controlled_sql_risk : t val wrong_argument_number : t + +val zero_execution_time_call : t diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 212cd6dc9..faf4d4dc3 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -368,6 +368,8 @@ module NonNegativePolynomial = struct let is_top = function Top -> true | _ -> false + let is_zero = function NonTop p when NonNegativeNonTopPolynomial.is_zero p -> true | _ -> false + let top_lifted_increasing ~f p1 p2 = match (p1, p2) with Top, _ | _, Top -> Top | NonTop p1, NonTop p2 -> NonTop (f p1 p2) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 5c1fb2bc9..60fff7778 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -43,6 +43,8 @@ module NonNegativePolynomial : sig val is_top : astate -> bool + val is_zero : astate -> bool + val plus : astate -> astate -> astate val mult : astate -> astate -> astate diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index fa0c028e5..57a649aa0 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -974,17 +974,24 @@ end module AnalyzerWCET = AbstractInterpreter.MakeNoCFG (InstrCFGScheduler) (TransferFunctionsWCET) -let check_and_report_infinity cost proc_desc summary = - if BasicCost.is_top cost then - let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in - let message = - F.asprintf "The execution time of the function %a cannot be computed" Typ.Procname.pp - (Procdesc.get_proc_name proc_desc) - in - let exn = - Exceptions.Checkers (IssueType.infinite_execution_time_call, Localise.verbatim_desc message) - in - Reporting.log_error ~loc ~extras:(compute_errlog_extras cost) summary exn +let check_and_report_top_and_bottom cost proc_desc summary = + let message = + F.asprintf "The execution time of the function %a %s" Typ.Procname.pp + (Procdesc.get_proc_name proc_desc) + in + let exn_opt = + if BasicCost.is_top cost then + let msg = message "cannot be computed" in + Some + (Exceptions.Checkers (IssueType.infinite_execution_time_call, Localise.verbatim_desc msg)) + else if BasicCost.is_zero cost then + let msg = message "is zero" in + Some (Exceptions.Checkers (IssueType.zero_execution_time_call, Localise.verbatim_desc msg)) + else None + in + let loc () = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in + Option.iter exn_opt + ~f:(Reporting.log_error ~loc:(loc ()) ~extras:(compute_errlog_extras cost) summary) let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = @@ -1068,7 +1075,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = (Procdesc.get_proc_name proc_desc) (Container.length ~fold:NodeCFG.fold_nodes node_cfg) pp_extra BasicCost.pp exit_cost ; - check_and_report_infinity exit_cost proc_desc summary ; + check_and_report_top_and_bottom exit_cost proc_desc summary ; Payload.update_summary {post= exit_cost} summary | None -> if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then ( diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c index 785e7aa2c..7ccad66b7 100644 --- a/infer/tests/codetoanalyze/c/performance/cost_test.c +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -126,3 +126,5 @@ void call_while_upto20_minus100_bad() { while_upto20_bad(-100); } void call_while_upto20_10_good() { while_upto20_bad(10); } void call_while_upto20_unsigned_good(unsigned x) { while_upto20_bad(x); } + +void zero_cost_function() {} diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 232489281..cc532b6b4 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -46,6 +46,7 @@ codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_C codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 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 1 + 5 * (-m.lb + 20), degree = 1] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * (-m.lb + 20), degree = 1] +codetoanalyze/c/performance/cost_test.c, zero_cost_function, 0, ZERO_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1204, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1204, degree = 0] diff --git a/infer/tests/codetoanalyze/java/performance/Cost_test.java b/infer/tests/codetoanalyze/java/performance/Cost_test.java index a4ccc81d5..6ac491015 100644 --- a/infer/tests/codetoanalyze/java/performance/Cost_test.java +++ b/infer/tests/codetoanalyze/java/performance/Cost_test.java @@ -116,4 +116,7 @@ public class Cost_test { k4 = bar_OK() + foo_OK() + cond_OK(19) * 3; return 0; } + + // Cost: 0 + private static void zeroCostFunction() {} } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 58dd8b1fc..38b7aeacb 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -48,6 +48,7 @@ codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop3(int), 2, EXPE codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 237, degree = 0] codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 205, degree = 0] codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 243, degree = 0] +codetoanalyze/java/performance/Cost_test.java, void Cost_test.zeroCostFunction(), 0, ZERO_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.if_bad_loop(), 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.loop_despite_inferbo(int), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.loop_despite_inferbo(int), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1302, degree = 0]