"Report infinity as error per function"

Reviewed By: mbouaziz

Differential Revision: D7600383

fbshipit-source-id: d6387ca

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]
 

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"

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

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 (

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]