[cost] Rename ZERO_* to *_UNREACHABLE_AT_EXIT

Summary:
This diff renames `ZERO_XXX` issues to more appropriately named and descriptive
`XXX_UNREACHABLE_AT_EXIT` and replaces bottom with
unreachable in cost kinds and issues.

Reviewed By: skcho

Differential Revision: D20140301

fbshipit-source-id: eb6076b30

infer/man/man1/infer-full.txt

@@ -427,6 +427,7 @@ OPTIONS
            default),
              EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD (enabled by
            default),
+             EXECUTION_TIME_UNREACHABLE_AT_EXIT (disabled by default),
              EXPENSIVE_EXECUTION_TIME (disabled by default),
              EXPENSIVE_EXECUTION_TIME_COLD_START (disabled by default),
              EXPENSIVE_EXECUTION_TIME_UI_THREAD (disabled by default),
@@ -523,8 +524,7 @@ OPTIONS
              Unknown_proc (enabled by default),
              VECTOR_INVALIDATION (enabled by default),
              WEAK_SELF_IN_NO_ESCAPE_BLOCK (enabled by default),
-             Wrong_argument_number (enabled by default),
-             ZERO_EXECUTION_TIME (disabled by default).
+             Wrong_argument_number (enabled by default).
            
            See also infer-report(1).
 

infer/man/man1/infer-report.txt

@@ -149,6 +149,7 @@ OPTIONS
            default),
              EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD (enabled by
            default),
+             EXECUTION_TIME_UNREACHABLE_AT_EXIT (disabled by default),
              EXPENSIVE_EXECUTION_TIME (disabled by default),
              EXPENSIVE_EXECUTION_TIME_COLD_START (disabled by default),
              EXPENSIVE_EXECUTION_TIME_UI_THREAD (disabled by default),
@@ -245,8 +246,7 @@ OPTIONS
              Unknown_proc (enabled by default),
              VECTOR_INVALIDATION (enabled by default),
              WEAK_SELF_IN_NO_ESCAPE_BLOCK (enabled by default),
-             Wrong_argument_number (enabled by default),
-             ZERO_EXECUTION_TIME (disabled by default).
+             Wrong_argument_number (enabled by default).
            
 
        --enable-issue-type +issue_type

infer/man/man1/infer.txt

@@ -427,6 +427,7 @@ OPTIONS
            default),
              EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD (enabled by
            default),
+             EXECUTION_TIME_UNREACHABLE_AT_EXIT (disabled by default),
              EXPENSIVE_EXECUTION_TIME (disabled by default),
              EXPENSIVE_EXECUTION_TIME_COLD_START (disabled by default),
              EXPENSIVE_EXECUTION_TIME_UI_THREAD (disabled by default),
@@ -523,8 +524,7 @@ OPTIONS
              Unknown_proc (enabled by default),
              VECTOR_INVALIDATION (enabled by default),
              WEAK_SELF_IN_NO_ESCAPE_BLOCK (enabled by default),
-             Wrong_argument_number (enabled by default),
-             ZERO_EXECUTION_TIME (disabled by default).
+             Wrong_argument_number (enabled by default).
            
            See also infer-report(1).
 

infer/src/backend/Differential.ml

@@ -204,8 +204,8 @@ module CostItem = struct
     Format.fprintf fmt "Cost is %t (degree is %a)" pp_cost (pp_degree ~only_bigO:false) curr_item
 end
 
-let issue_of_cost kind CostIssues.{complexity_increase_issue; zero_issue; infinite_issue} ~delta
-    ~prev_item
+let issue_of_cost kind CostIssues.{complexity_increase_issue; unreachable_issue; infinite_issue}
+    ~delta ~prev_item
     ~curr_item:
       ({CostItem.cost_item= cost_info; degree_with_term= curr_degree_with_term} as curr_item) =
   let file = cost_info.Jsonbug_t.loc.file in
@@ -224,7 +224,7 @@ let issue_of_cost kind CostIssues.{complexity_increase_issue; zero_issue; infini
   let source_file = SourceFile.create ~warn_on_error:false file in
   let issue_type =
     if CostItem.is_top curr_item then infinite_issue
-    else if CostItem.is_unreachable curr_item then zero_issue
+    else if CostItem.is_unreachable curr_item then unreachable_issue
     else
       let is_on_cold_start = ExternalPerfData.in_profiler_data_map procname in
       complexity_increase_issue ~is_on_cold_start ~is_on_ui_thread

infer/src/base/CostIssues.ml

@@ -12,9 +12,9 @@ type issue_spec =
   ; threshold: int option
   ; complexity_increase_issue: is_on_cold_start:bool -> is_on_ui_thread:bool -> IssueType.t
   ; expensive_issue: is_on_cold_start:bool -> is_on_ui_thread:bool -> IssueType.t
-  ; zero_issue: IssueType.t
+  ; unreachable_issue: IssueType.t
   ; infinite_issue: IssueType.t
-  ; top_and_bottom: bool }
+  ; top_and_unreachable: bool }
 
 module CostKindMap = struct
   include PrettyPrintable.MakePPMap (CostKind)
@@ -34,7 +34,7 @@ end
 
 let enabled_cost_map =
   List.fold CostKind.enabled_cost_kinds ~init:CostKindMap.empty
-    ~f:(fun acc CostKind.{kind; top_and_bottom} ->
+    ~f:(fun acc CostKind.{kind; top_and_unreachable} ->
       let kind_spec =
         { name= Format.asprintf "The %a" CostKind.pp kind
         ; threshold= (if Config.use_cost_threshold then CostKind.to_threshold kind else None)
@@ -45,8 +45,8 @@ let enabled_cost_map =
         ; expensive_issue=
             (fun ~is_on_cold_start ~is_on_ui_thread ->
               IssueType.expensive_cost_call ~kind ~is_on_cold_start ~is_on_ui_thread )
-        ; zero_issue= IssueType.zero_cost_call ~kind
+        ; unreachable_issue= IssueType.unreachable_cost_call ~kind
         ; infinite_issue= IssueType.infinite_cost_call ~kind
-        ; top_and_bottom }
+        ; top_and_unreachable }
       in
       CostKindMap.add kind kind_spec acc )

infer/src/base/CostIssues.mli

@@ -13,9 +13,9 @@ type issue_spec =
   ; threshold: int option
   ; complexity_increase_issue: is_on_cold_start:bool -> is_on_ui_thread:bool -> IssueType.t
   ; expensive_issue: is_on_cold_start:bool -> is_on_ui_thread:bool -> IssueType.t
-  ; zero_issue: IssueType.t
+  ; unreachable_issue: IssueType.t
   ; infinite_issue: IssueType.t
-  ; top_and_bottom: bool }
+  ; top_and_unreachable: bool }
 
 module CostKindMap : sig
   include PrettyPrintable.PPMap with type key = CostKind.t

infer/src/base/IssueType.ml

@@ -506,14 +506,16 @@ let wrong_argument_number =
   register_from_string "Wrong_argument_number" ~hum:"Wrong Argument Number"
 
 
-let zero_cost_call ~kind = register_from_cost_string ~enabled:false ~kind "ZERO_%s"
+let unreachable_cost_call ~kind =
+  register_from_cost_string ~enabled:false ~kind "%s_UNREACHABLE_AT_EXIT"
+
 
 (* register enabled cost issues *)
 let () =
   List.iter CostKind.enabled_cost_kinds ~f:(fun CostKind.{kind} ->
       List.iter [true; false] ~f:(fun is_on_cold_start ->
           List.iter [true; false] ~f:(fun is_on_ui_thread ->
-              let _ = zero_cost_call ~kind in
+              let _ = unreachable_cost_call ~kind in
               let _ = expensive_cost_call ~kind ~is_on_cold_start ~is_on_ui_thread in
               let _ = infinite_cost_call ~kind in
               let _ = complexity_increase ~kind ~is_on_cold_start ~is_on_ui_thread in

infer/src/base/IssueType.mli

@@ -354,4 +354,4 @@ val weak_self_in_noescape_block : t
 
 val wrong_argument_number : t
 
-val zero_cost_call : kind:CostKind.t -> t
+val unreachable_cost_call : kind:CostKind.t -> t

infer/src/base/costKind.ml

@@ -53,6 +53,6 @@ let to_json_cost_info c = function
    Currently it's set randomly to 200 for OperationCost and 3 for AllocationCost. *)
 let to_threshold = function OperationCost -> Some 200 | AllocationCost -> Some 3 | IOCost -> None
 
-type kind_spec = {kind: t; (* for non-diff analysis *) top_and_bottom: bool}
+type kind_spec = {kind: t; (* for non-diff analysis *) top_and_unreachable: bool}
 
-let enabled_cost_kinds = [{kind= OperationCost; top_and_bottom= true}]
+let enabled_cost_kinds = [{kind= OperationCost; top_and_unreachable= true}]

infer/src/base/costKind.mli

@@ -9,7 +9,7 @@ open! IStd
 
 type t = OperationCost | AllocationCost | IOCost [@@deriving compare]
 
-type kind_spec = {kind: t; (* for non-diff analysis *) top_and_bottom: bool}
+type kind_spec = {kind: t; (* for non-diff analysis *) top_and_unreachable: bool}
 
 val compare : t -> t -> int
 

infer/src/cost/cost.ml

@@ -254,7 +254,8 @@ module Check = struct
       ~extras:(compute_errlog_extras cost) report_issue_type message
 
 
-  let report_top_and_bottom pname loc summary ~name ~cost CostIssues.{zero_issue; infinite_issue} =
+  let report_top_and_unreachable pname loc summary ~name ~cost
+      CostIssues.{unreachable_issue; infinite_issue} =
     let report issue suffix =
       let message = F.asprintf "%s of the function %a %s" name Procname.pp pname suffix in
       Reporting.log_error ~loc
@@ -262,7 +263,9 @@ module Check = struct
         ~extras:(compute_errlog_extras cost) summary issue message
     in
     if BasicCost.is_top cost then report infinite_issue "cannot be computed"
-    else if BasicCost.is_unreachable cost then report zero_issue "is zero(unreachable)"
+    else if BasicCost.is_unreachable cost then
+      report unreachable_issue
+        "cannot be computed since the program's exit state is never reachable"
 
 
   let check_and_report ~is_on_ui_thread WorstCaseCost.{costs; reports} proc_desc summary =
@@ -277,9 +280,9 @@ module Check = struct
             report_threshold pname summary ~name ~location ~cost kind_spec
               ~threshold:(Option.value_exn threshold) ~is_on_ui_thread ) ;
       CostIssues.CostKindMap.iter2 CostIssues.enabled_cost_map costs
-        ~f:(fun _kind (CostIssues.{name; top_and_bottom} as issue_spec) cost ->
-          if top_and_bottom then report_top_and_bottom pname proc_loc summary ~name ~cost issue_spec
-      ) )
+        ~f:(fun _kind (CostIssues.{name; top_and_unreachable} as issue_spec) cost ->
+          if top_and_unreachable then
+            report_top_and_unreachable pname proc_loc summary ~name ~cost issue_spec ) )
 end
 
 type bound_map = BasicCost.t Node.IdMap.t

infer/tests/codetoanalyze/c/performance/exit.c

@@ -4,12 +4,12 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
-void exit_unreachable_zero() {
+void exit_unreachable_unreachable() {
   exit(0); // modeled as unreachable
 }
 
-// constraint solver resolves all nodes to 0 cost
-void compute_exit_unreachable_zero() {
+// constraint solver resolves all nodes to unreachable cost
+void compute_exit_unreachable_unreachable() {
   int k = 0;
   exit(0);
 }
@@ -19,7 +19,7 @@ void linear(int p) {
   }
 }
 
-void call_exit_unreachable_zero(int p) {
+void call_exit_unreachable_unreachable(int p) {
   linear(p);
   exit(0);
 }
@@ -32,4 +32,4 @@ void inline_exit_unreachable_FP(int p) {
   exit(0);
 }
 
-void call_unreachable_constant() { exit_unreachable_zero(); }
+void call_unreachable_constant() { exit_unreachable_unreachable(); }

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -48,9 +48,9 @@ codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, INTEGER_OVERF
 codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 12, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 215, O(1), degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([3, +oo] + 1):signed32]
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 546, O(1), degree = 0]
-codetoanalyze/c/performance/exit.c, call_exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node]
-codetoanalyze/c/performance/exit.c, compute_exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node]
-codetoanalyze/c/performance/exit.c, exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node]
+codetoanalyze/c/performance/exit.c, call_exit_unreachable_unreachable, 0, EXECUTION_TIME_UNREACHABLE_AT_EXIT, no_bucket, ERROR, [Unreachable node]
+codetoanalyze/c/performance/exit.c, compute_exit_unreachable_unreachable, 0, EXECUTION_TIME_UNREACHABLE_AT_EXIT, no_bucket, ERROR, [Unreachable node]
+codetoanalyze/c/performance/exit.c, exit_unreachable_unreachable, 0, EXECUTION_TIME_UNREACHABLE_AT_EXIT, no_bucket, ERROR, [Unreachable node]
 codetoanalyze/c/performance/exit.c, inline_exit_unreachable_FP, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 ⋅ p + 2 ⋅ (1+max(0, p)), O(p), degree = 1,{1+max(0, p)},Loop at line 30, column 3,{p},Loop at line 30, column 3]
 codetoanalyze/c/performance/exit.c, linear, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ p + 2 ⋅ (1+max(0, p)), O(p), degree = 1,{1+max(0, p)},Loop at line 18, column 3,{p},Loop at line 18, column 3]
 codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14006, O(1), degree = 0]

infer/tests/codetoanalyze/java/performance/UnreachableAtExitTest.java

@@ -6,17 +6,17 @@
  */
 import com.google.common.base.Preconditions;
 
-class Zero {
+class UnreachableAtExitTest {
 
   // cost: 1
   void unit_cost() {};
 
-  public void infeasible_path_zero() {
+  public void infeasible_path_unreachable() {
     Preconditions.checkState(false); // pruned to bottom
   }
 
   // we can't handle doubles properly in Inferbo
-  public void double_prune_FN(double fpp) {
+  public void double_prune_unreachable_FN(double fpp) {
     Preconditions.checkArgument(fpp > 0.0 && fpp < 0.0);
   }
 }

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -219,5 +219,5 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ 2⋅byteCount, O(2⋅byteCount), degree = 1,{2⋅byteCount},Loop at line 33]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.throw_exception():int, 0, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 61,{list.length},Loop at line 61]
-codetoanalyze/java/performance/Zero.java, Zero.infeasible_path_zero():void, 0, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
-codetoanalyze/java/performance/Zero.java, Zero.infeasible_path_zero():void, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node]
+codetoanalyze/java/performance/UnreachableAtExitTest.java, UnreachableAtExitTest.infeasible_path_unreachable():void, 0, EXECUTION_TIME_UNREACHABLE_AT_EXIT, no_bucket, ERROR, [Unreachable node]
+codetoanalyze/java/performance/UnreachableAtExitTest.java, UnreachableAtExitTest.infeasible_path_unreachable():void, 0, UNREACHABLE_CODE, no_bucket, ERROR, [Here]