exinferbo] check end of procedure for unreachability

Summary:
Calling exit at the end of a proc does not create unreachable code, prior to this commit inferbo reports that it does.

We extend collect_instrs to detect when we're at the end of a procedure in C and not report on unreachable code if we call a procedure there.

Reviewed By: mbouaziz

Differential Revision: D5623637

fbshipit-source-id: 0d5f326

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -462,14 +462,44 @@ module Report = struct
       L.(debug BufferOverrun Verbose) "@]@\n" ;
       L.(debug BufferOverrun Verbose) "================================@\n@."
 
-  let is_last_statement_of_if_branch rem_instrs node =
-    if rem_instrs <> [] then false
-    else
+  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 (_ :: _ :: _)
+       -> 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
+      &&
       match Procdesc.Node.get_succs node with
       | [succ] -> (
-        match Procdesc.Node.get_preds succ with _ :: _ :: _ -> true | _ -> false )
+        match CFG.instrs succ with
+        | []
+         -> List.is_empty (Procdesc.Node.get_succs succ)
+        | _
+         -> false )
       | _
        -> false
+  end
 
   let rec collect_instrs
       : extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate -> Dom.ConditionSet.t
@@ -509,9 +539,15 @@ module Report = struct
                     Exceptions.Condition_always_true_false (desc, not true_branch, __POS__)
                   in
                   Reporting.log_warning_deprecated pname ~loc 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
+               -> ()
               | Sil.Call (_, Const Cfun pname, _, _, _)
                 when String.equal (Typ.Procname.get_method pname) "exit"
-                     && is_last_statement_of_if_branch rem_instrs node
+                     && ExitStatement.has_multiple_sibling_nodes_and_one_successor node
                -> ()
               | _
                -> let loc = Sil.instr_get_loc instr in

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

@@ -53,7 +53,6 @@ codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRU
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [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_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,11 +41,16 @@ 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 exit_at_end_of_proc_good_local_var() {
+  int a = 57;
+  exit(5);
+}
+
 void FN_useless_else_bad() {
   if (__infer_nondet_int()) {
     exit(0);