[inferbo/unreachable] Fix FPs with exit at end of block/procedure

Summary: The heuristics to determine the end of a block/procedure was too brittle, the new one ignores non significant instructions.

Reviewed By: jvillard

Differential Revision: D6845380

fbshipit-source-id: feab557

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -340,43 +340,33 @@ module Report = struct
 
 
   module ExitStatement = struct
-    let successors node = Procdesc.Node.get_succs node
-
-    let predecessors node = Procdesc.Node.get_preds node
-
-    let preds_of_singleton_successor node =
-      match successors node with [succ] -> Some (predecessors succ) | _ -> None
-
-
-    (* last statement in if branch *)
-    (* do we transfer control to a node with multiple predecessors *)
-    let has_multiple_sibling_nodes_and_one_successor node =
-      match preds_of_singleton_successor node with
-      (* we need at least 2 predecessors *)
-      | Some (_ :: _ :: _) ->
+    let non_significant_instr = function
+      | Sil.(Abstract _ | Nullify _ | Remove_temps _) ->
           true
       | _ ->
           false
 
 
-    (* check that we are the last instruction in the current node
-     * and that the current node is followed by a unique successor
-     * with no instructions.
-     *
-     * this is our proxy for being the last statement in a procedure.
-     * The tests pass, but it's kind of a hack and depends on an internal
-     * detail of SIL that could change in the future. *)
-    let is_last_in_node_and_followed_by_empty_successor node rem_instrs =
-      List.is_empty rem_instrs
+    (* check that we are the last significant instruction
+     * of a procedure (no more significant instruction)
+     * or of a block (goes directly to a node with multiple predecessors)
+     *)
+    let rec is_end_of_block_or_procedure node rem_instrs =
+      List.for_all rem_instrs ~f:non_significant_instr
       &&
       match Procdesc.Node.get_succs node with
-      | [succ] -> (
-        match CFG.instrs succ with
-        | [] ->
-            List.is_empty (Procdesc.Node.get_succs succ)
-        | _ ->
-            false )
-      | _ ->
+      | [] ->
+          true
+      | [succ]
+        -> (
+          is_end_of_block_or_procedure succ (CFG.instrs succ)
+          ||
+          match Procdesc.Node.get_preds succ with
+          | _ :: _ :: _ ->
+              true (* [succ] is a join, i.e. [node] is the end of a block *)
+          | _ ->
+              false )
+      | _ :: _ :: _ ->
           false
   end
 
@@ -424,15 +414,10 @@ module Report = struct
                     Exceptions.Condition_always_true_false (desc, not true_branch, __POS__)
                   in
                   Reporting.log_warning summary ~loc:location exn
-              (* special case for when we're at the end of a procedure *)
-              | Sil.Call (_, Const Cfun pname, _, _, _)
-                when String.equal (Typ.Procname.get_method pname) "exit"
-                     && ExitStatement.is_last_in_node_and_followed_by_empty_successor node
-                          rem_instrs ->
-                  ()
+              (* special case for `exit` when we're at the end of a block / procedure *)
               | Sil.Call (_, Const Cfun pname, _, _, _)
                 when String.equal (Typ.Procname.get_method pname) "exit"
-                     && ExitStatement.has_multiple_sibling_nodes_and_one_successor node ->
+                     && ExitStatement.is_end_of_block_or_procedure node rem_instrs ->
                   ()
               | _ ->
                   let location = Sil.instr_get_loc instr in

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

@@ -13,7 +13,6 @@ codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRU
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]]
-codetoanalyze/c/bufferoverrun/for_loop.c, safealloc, 10, UNREACHABLE_CODE, []
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
@@ -78,8 +77,6 @@ codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRU
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/unreachable.c, FP_exit_at_end_of_proc_good, 2, UNREACHABLE_CODE, []
-codetoanalyze/c/bufferoverrun/unreachable.c, FP_exit_at_end_of_proc_good_local_var, 2, UNREACHABLE_CODE, []
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, []
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_exit_good, 1, CONDITION_ALWAYS_TRUE, []

infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c

@@ -41,12 +41,12 @@ void exit_at_end_of_if_good() {
   }
 }
 
-void FP_exit_at_end_of_proc_good() {
+void exit_at_end_of_proc_good() {
   nop();
   exit(5);
 }
 
-void FP_exit_at_end_of_proc_good_local_var() {
+void exit_at_end_of_proc_good_local_var() {
   int a = 57;
   exit(5);
 }