[pulse][RFC] count reachable nodes with 0 disjuncts

Summary:
we only count nodes reachable from the start node,
not following exceptional edges.

Hence we use a simple depth-first-search.

It we count nodes in catch blocks, this makes difficult to understand the results because this is expected that our analysis will never enter in some of them.

Reviewed By: nbenton

Differential Revision:
D55082611

Privacy Context Container: L1208441

fbshipit-source-id: 34fa381bee09550fbd018a81b537b42955329f5a

infer/man/man1/infer-analyze.txt

@@ -232,6 +232,10 @@ OPTIONS
  Pulse disjuncts. (Conversely:
  --no-log-pulse-disjunct-increase-after-model-call)
 
+ --log-pulse-unreachable-nodes
+ Activates: Log for each function and each summary, the ratio of
+ unreached nodes. (Conversely: --no-log-pulse-unreachable-nodes)
+
  --loop-hoisting
  Activates: loop-hoisting checker: Detect opportunities to hoist
  function calls that are invariant outside of loop bodies for

infer/man/man1/infer-full.txt

@@ -1204,6 +1204,11 @@ OPTIONS
  --no-log-pulse-disjunct-increase-after-model-call)
  See also infer-analyze(1).
 
+ --log-pulse-unreachable-nodes
+ Activates: Log for each function and each summary, the ratio of
+ unreached nodes. (Conversely: --no-log-pulse-unreachable-nodes)
+ See also infer-analyze(1).
+
  --loop-hoisting
  Activates: loop-hoisting checker: Detect opportunities to hoist
  function calls that are invariant outside of loop bodies for

infer/man/man1/infer.txt

@@ -1204,6 +1204,11 @@ OPTIONS
  --no-log-pulse-disjunct-increase-after-model-call)
  See also infer-analyze(1).
 
+ --log-pulse-unreachable-nodes
+ Activates: Log for each function and each summary, the ratio of
+ unreached nodes. (Conversely: --no-log-pulse-unreachable-nodes)
+ See also infer-analyze(1).
+
  --loop-hoisting
  Activates: loop-hoisting checker: Detect opportunities to hoist
  function calls that are invariant outside of loop bodies for

infer/src/base/Config.ml

@@ -2142,6 +2142,12 @@ and log_pulse_disjunct_increase_after_model_call =
  "Log which model did increase the current number of Pulse disjuncts."
 
 
+and log_pulse_unreachable_nodes =
+ CLOpt.mk_bool ~long:"log-pulse-unreachable-nodes" ~default:false
+ ~in_help:InferCommand.[(Analyze, manual_generic)]
+ "Log for each function and each summary, the ratio of unreached nodes."
+
+
 and log_missing_deps =
  CLOpt.mk_bool ~long:"log-missing-deps" ~default:false
  ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -4246,6 +4252,8 @@ and lock_model = !lock_model
 
 and log_pulse_disjunct_increase_after_model_call = !log_pulse_disjunct_increase_after_model_call
 
+and log_pulse_unreachable_nodes = !log_pulse_unreachable_nodes
+
 and log_missing_deps = !log_missing_deps
 
 and margin_html = !margin_html

infer/src/base/Config.mli

@@ -518,6 +518,8 @@ val lock_model : Yojson.Safe.t
 
 val log_pulse_disjunct_increase_after_model_call : bool
 
+val log_pulse_unreachable_nodes : bool
+
 val log_missing_deps : bool
 
 val margin_html : int

infer/src/pulse/Pulse.ml

@@ -1644,6 +1644,41 @@ let log_summary_count proc_name summary =
  Out_channel.output_char (Lazy.force summary_count_channel) '\n'
 
 
+let log_number_of_unreachable_nodes proc_desc invariant_map =
+ let proc_name = Procdesc.get_proc_name proc_desc in
+ let nodes = Procdesc.get_nodes proc_desc in
+ let nodes_reachable_from_entry =
+ let open Procdesc in
+ let rec visit seen node =
+ if NodeSet.mem node seen then seen
+ else
+ let seen = NodeSet.add node seen in
+ Node.get_succs node |> List.fold ~init:seen ~f:visit
+ in
+ get_start_node proc_desc |> visit NodeSet.empty
+ in
+ let nb_nodes_reachable_from_entry =
+ Procdesc.NodeSet.cardinal nodes_reachable_from_entry |> float_of_int
+ in
+ let has_node_0_disjunct node =
+ let id = Procdesc.Node.get_id node in
+ if Procdesc.NodeSet.mem node nodes_reachable_from_entry |> not then false
+ else if DisjunctiveAnalyzer.InvariantMap.mem id invariant_map |> not then true
+ else
+ let {AbstractInterpreter.State.pre= disjs, _} =
+ DisjunctiveAnalyzer.InvariantMap.find id invariant_map
+ in
+ List.is_empty disjs
+ in
+ let nb_nodes_without_disjuncts = List.count nodes ~f:has_node_0_disjunct |> float_of_int in
+ let unreachable_ratio = nb_nodes_without_disjuncts /. nb_nodes_reachable_from_entry in
+ if Float.(unreachable_ratio > 0.10) then
+ L.debug Analysis Quiet
+ "[Unreachability warning] At %a, function %a, %.2f%% of CFG nodes are unreachable\n"
+ Location.pp_file_pos (Procdesc.get_loc proc_desc) Procname.pp proc_name
+ (100. *. unreachable_ratio)
+
+
 let analyze specialization
  ({InterproceduralAnalysis.tenv; proc_desc; err_log; exe_env} as analysis_data) =
  let proc_name = Procdesc.get_proc_name proc_desc in
@@ -1662,6 +1697,7 @@ let analyze specialization
  (initial_disjuncts, initial_non_disj) )
  in
  let invariant_map = DisjunctiveAnalyzer.exec_pdesc analysis_data ~initial proc_desc in
+ if Config.log_pulse_unreachable_nodes then log_number_of_unreachable_nodes proc_desc invariant_map ;
  let process_postconditions node posts_opt ~convert_normal_to_exceptional =
  match posts_opt with
  | Some (posts, non_disj_astate) ->

infer/tests/codetoanalyze/hack/pulse/Makefile

@@ -7,7 +7,7 @@ TESTS_DIR = ../../..
 
 INFER_OPTIONS = --pulse-only --debug-exceptions --pulse-specialization-partial \
  --pulse-monitor-transitive-callees --pulse-monitor-transitive-missed-captures \
- --pulse-max-disjuncts 8 \
+ --pulse-max-disjuncts 8 --log-pulse-unreachable-nodes \
  --pulse-transitive-access-config transitive-access-config.json \
  --pulse-transitive-access-config transitive-access-config-extra.json
 INFERPRINT_OPTIONS = --issues-tests

infer/tests/codetoanalyze/java/pulse/CountDeadCode.java

@@ -0,0 +1,66 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+package codetoanalyze.java.infer;
+
+/*
+ This is a test file specific to the unreachability counting
+*/
+
+public class CountDeadCode {
+
+ public int no_deadcode() {
+ int i = 0;
+ int x = 0;
+ if (i == 0) {
+ x = 1;
+ }
+ return x;
+ }
+
+ public int else_with_deadcode() {
+ int i = 0;
+ int x;
+ if (i == 0) {
+ x = 0;
+ } else { // only this part
+ x = 1; // is counted as unreachable
+ }
+ return x;
+ }
+
+ public int long_catch_block() {
+ try {
+ int i = 0;
+ int x;
+ if (i == 0) {
+ x = 0;
+ } else { // only this part
+ x = 1; // is counted as unreachable
+ }
+ return x;
+ } catch (Exception e) { // the unreachability count
+ int i = 0; // will not take into account
+ i++; // this block
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ i++;
+ return 0;
+ }
+ }
+}