From af5265f75d83e2ee8c9bb23240edf256e202daaa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 13 Apr 2018 07:59:47 -0700 Subject: [PATCH] "Report infinity as error per function" Reviewed By: mbouaziz Differential Revision: D7600383 fbshipit-source-id: d6387ca --- infer/src/IR/Procdesc.ml | 2 +- infer/src/base/IssueType.ml | 2 ++ infer/src/base/IssueType.mli | 2 ++ infer/src/checkers/cost.ml | 17 ++++++++++++++++- .../codetoanalyze/c/performance/issues.exp | 2 ++ 5 files changed, 23 insertions(+), 2 deletions(-) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index c19e6764d..28d7e36ce 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -219,7 +219,7 @@ type t = ; mutable nodes: Node.t list (** list of nodes of this procedure *) ; mutable nodes_num: int (** number of nodes *) ; mutable start_node: Node.t (** start node of this procedure *) - ; mutable exit_node: Node.t (** exit node of ths procedure *) + ; mutable exit_node: Node.t (** exit node of this procedure *) ; mutable loop_heads: NodeSet.t option (** loop head nodes of this procedure *) } [@@deriving compare] diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index f193a1907..4ea7d3797 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -249,6 +249,8 @@ let inferbo_alloc_may_be_big = from_string ~enabled:false "INFERBO_ALLOC_MAY_BE_ let inferbo_alloc_may_be_negative = from_string ~enabled:false "INFERBO_ALLOC_MAY_BE_NEGATIVE" +let infinite_execution_time_call = from_string ~enabled:false "INFINITE_EXECUTION_TIME_CALL" + let inherently_dangerous_function = from_string "INHERENTLY_DANGEROUS_FUNCTION" let interface_not_thread_safe = from_string "INTERFACE_NOT_THREAD_SAFE" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 6efbb3134..6a779dd31 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -166,6 +166,8 @@ val inferbo_alloc_may_be_big : t val inferbo_alloc_may_be_negative : t +val infinite_execution_time_call : t + val inherently_dangerous_function : t val interface_not_thread_safe : t diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 732437941..a4bec0f95 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -442,6 +442,8 @@ module TransferFunctionsWCET (CFG : ProcCfg.S) = struct type extras = extras_TransferFunctionsWCET + (* We don't report when the cost is Top as it corresponds to subsequent 'don't know's. + Instead, we report Top cost only at the top level per function when `report_infinity` is set to true *) let report_cost summary instr (cost: Itv.Bound.t) nid reported_so_far = let mk_message () = F.asprintf @@ -481,7 +483,6 @@ module TransferFunctionsWCET (CFG : ProcCfg.S) = struct (cost, reported_so_far) - (* We don't report when the cost is Top as it corresponds to 'don't know'*) (* get a list of nodes and check if we have already reported for at least one of them. In that case no need to report again. *) let should_report preds reported_so_far = @@ -538,6 +539,19 @@ end module AnalyzerWCET = AbstractInterpreter.Make (CFG) (TransferFunctionsWCET) +let check_and_report_infinity cost proc_desc summary = + if not (Itv.Bound.is_not_infty 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 summary exn + + let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = Preanal.do_preanalysis proc_desc tenv ; let proc_data = ProcData.make_default proc_desc tenv in @@ -568,6 +582,7 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = in match AnalyzerWCET.extract_post (CFG.id (CFG.exit_node cfg)) invariant_map_WCETFinal with | Some (exit_cost, _) -> + check_and_report_infinity exit_cost proc_desc summary ; Summary.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/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 6a9e57f29..db69c9772 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -1,3 +1,5 @@ +codetoanalyze/c/performance/cost_test.c, FN_loop2, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, FN_loop3, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002] codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002] codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1004]