[inferbo] Add warnings and errors for unreachable code

Summary:
Warnings for conditions always true/false
Errors for other unreachable statements (should help debugging inferbo)

Reviewed By: sblackshear

Differential Revision: D5047883

fbshipit-source-id: 65a78ca

infer/src/IR/Exceptions.ml

@@ -98,6 +98,7 @@ exception Tainted_value_reaching_sensitive_function of Localise.error_desc * L.m
 exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * L.ml_loc
 exception Uninitialized_value of Localise.error_desc * L.ml_loc
 exception Unknown_proc
+exception Unreachable_code_after of Localise.error_desc * L.ml_loc
 exception Unsafe_guarded_by_access of Localise.error_desc * L.ml_loc
 exception Use_after_free of Localise.error_desc * L.ml_loc
 exception Wrong_argument_number of L.ml_loc
@@ -301,6 +302,8 @@ let recognize_exception exn =
     | Unknown_proc ->
         (Localise.from_string "Unknown_proc" ~hum:"Unknown Procedure",
          Localise.no_desc, None, Exn_developer, Low, None, Nocat)
+    | Unreachable_code_after (desc, ml_loc) ->
+        (Localise.unreachable_code_after, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
     | Unsafe_guarded_by_access (desc, ml_loc) ->
         (Localise.unsafe_guarded_by_access,
          desc, Some ml_loc, Exn_user, High, None, Prover)

infer/src/IR/Exceptions.mli

@@ -93,6 +93,7 @@ exception Tainted_value_reaching_sensitive_function of Localise.error_desc * Log
 exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * Logging.ml_loc
 exception Uninitialized_value of Localise.error_desc * Logging.ml_loc
 exception Unknown_proc
+exception Unreachable_code_after of Localise.error_desc * Logging.ml_loc
 exception Unsafe_guarded_by_access of Localise.error_desc * Logging.ml_loc
 exception Use_after_free of Localise.error_desc * Logging.ml_loc
 exception Wrong_argument_number of Logging.ml_loc

infer/src/IR/Localise.ml

@@ -128,6 +128,7 @@ let thread_safety_violation = from_string "THREAD_SAFETY_VIOLATION"
 let unary_minus_applied_to_unsigned_expression =
   from_string "UNARY_MINUS_APPLIED_TO_UNSIGNED_EXPRESSION"
 let uninitialized_value = from_string "UNINITIALIZED_VALUE"
+let unreachable_code_after = from_string "UNREACHABLE_CODE"
 let unsafe_guarded_by_access = from_string "UNSAFE_GUARDED_BY_ACCESS"
 let use_after_free = from_string "USE_AFTER_FREE"
 
@@ -701,6 +702,11 @@ let desc_condition_always_true_false i cond_str_opt loc =
       (at_line tags loc) in
   { no_desc with descriptions = [description]; tags = !tags }
 
+let desc_unreachable_code_after loc =
+  let tags = Tags.create () in
+  let description = "Unreachable code after statement " ^ at_line tags loc in
+  { no_desc with descriptions = [description]}
+
 let desc_deallocate_stack_variable var_str proc_name loc =
   let tags = Tags.create () in
   Tags.update tags Tags.value var_str;

infer/src/IR/Localise.mli

@@ -99,6 +99,7 @@ val tainted_value_reaching_sensitive_function : t
 val thread_safety_violation : t
 val unary_minus_applied_to_unsigned_expression : t
 val uninitialized_value : t
+val unreachable_code_after : t
 val unsafe_guarded_by_access : t
 val use_after_free : t
 
@@ -243,6 +244,8 @@ val desc_condition_is_assignment : Location.t -> error_desc
 
 val desc_condition_always_true_false : IntLit.t -> string option -> Location.t -> error_desc
 
+val desc_unreachable_code_after : Location.t -> error_desc
+
 val desc_deallocate_stack_variable : string -> Typ.Procname.t -> Location.t -> error_desc
 
 val desc_deallocate_static_memory : string -> Typ.Procname.t -> Location.t -> error_desc

infer/src/backend/errdesc.ml

@@ -1124,6 +1124,9 @@ let explain_condition_always_true_false tenv i cond node loc =
     | None -> None in
   Localise.desc_condition_always_true_false i cond_str_opt loc
 
+let explain_unreachable_code_after loc =
+  Localise.desc_unreachable_code_after loc
+
 (** explain the escape of a stack variable address from its scope *)
 let explain_stack_variable_address_escape loc pvar addr_dexp_opt =
   let addr_dexp_str = match addr_dexp_opt with

infer/src/backend/errdesc.mli

@@ -91,6 +91,8 @@ val explain_condition_is_assignment : Location.t -> Localise.error_desc
 val explain_condition_always_true_false :
   Tenv.t -> IntLit.t -> Exp.t -> Procdesc.Node.t -> Location.t -> Localise.error_desc
 
+val explain_unreachable_code_after : Location.t -> Localise.error_desc
+
 (** explain the escape of a stack variable address from its scope *)
 val explain_stack_variable_address_escape :
   Location.t -> Pvar.t -> DecompiledExp.t option -> Localise.error_desc

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -390,44 +390,74 @@ struct
          L.out "@]@\n";
          L.out "================================@\n@.")
 
-  let collect_instr
-    : extras ProcData.t -> CFG.node -> Dom.ConditionSet.t * Dom.Mem.astate
-      -> Sil.instr -> Dom.ConditionSet.t * Dom.Mem.astate
-    = fun ({ pdesc; tenv; extras } as pdata) node (cond_set, mem) instr ->
-      let pname = Procdesc.get_proc_name pdesc in
-      let cond_set =
-        match instr with
-        | Sil.Load (_, exp, _, loc)
-        | Sil.Store (exp, _, _, loc) ->
-            add_condition pname node exp loc mem cond_set
-        | Sil.Call (_, Const (Cfun callee_pname), params, loc, _) ->
-            (match Summary.read_summary pdesc callee_pname with
-             | Some summary ->
-                 let callee = extras callee_pname in
-                 instantiate_cond tenv pname callee params mem summary loc
-                 |> Dom.ConditionSet.rm_invalid
-                 |> Dom.ConditionSet.join cond_set
-             | _ -> cond_set)
-        | _ -> cond_set
-      in
-      let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in
-      print_debug_info instr mem cond_set;
-      (cond_set, mem)
-
-  let collect_instrs
+  let is_last_statement_of_if_branch rem_instrs node =
+    if rem_instrs <> [] then false
+    else
+      match Procdesc.Node.get_succs node with
+      | [succ] ->
+          (match Procdesc.Node.get_preds succ with
+           | _ :: _ :: _ -> true
+           | _ -> false)
+      | _ -> false
+
+  let rec collect_instrs
     : extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate
       -> Dom.ConditionSet.t -> Dom.ConditionSet.t
-    = fun pdata node instrs mem cond_set ->
-      List.fold ~f:(collect_instr pdata node) ~init:(cond_set, mem) instrs
-      |> fst
+    = fun ({ pdesc; tenv; extras } as pdata) node instrs mem cond_set ->
+      match instrs with
+      | [] -> cond_set
+      | instr :: rem_instrs ->
+          let pname = Procdesc.get_proc_name pdesc in
+          let cond_set =
+            match instr with
+            | Sil.Load (_, exp, _, loc)
+            | Sil.Store (exp, _, _, loc) ->
+                add_condition pname node exp loc mem cond_set
+            | Sil.Call (_, Const (Cfun callee_pname), params, loc, _) ->
+                (match Summary.read_summary pdesc callee_pname with
+                 | Some summary ->
+                     let callee = extras callee_pname in
+                     instantiate_cond tenv pname callee params mem summary loc
+                     |> Dom.ConditionSet.rm_invalid
+                     |> Dom.ConditionSet.join cond_set
+                 | _ -> cond_set)
+            | _ -> cond_set
+          in
+          let mem' = Analyzer.TransferFunctions.exec_instr mem pdata node instr in
+          let () =
+            match mem, mem' with
+            | NonBottom _, Bottom ->
+                (match instr with
+                 | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) -> ()
+                 | Sil.Prune (cond, loc, true_branch, _) ->
+                     let i = match cond with
+                       | Exp.Const (Const.Cint i) -> i
+                       | _ -> IntLit.zero in
+                     let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
+                     let exn =
+                       Exceptions.Condition_always_true_false (desc, not true_branch, __POS__) in
+                     Reporting.log_warning pname ~loc exn
+                 | Sil.Call (_, Const (Cfun pname), _, _, _) when
+                     String.equal (Typ.Procname.get_method pname) "exit" &&
+                     is_last_statement_of_if_branch rem_instrs node -> ()
+                 | _ ->
+                     let loc = Sil.instr_get_loc instr in
+                     let desc = Errdesc.explain_unreachable_code_after loc in
+                     let exn = Exceptions.Unreachable_code_after (desc, __POS__) in
+                     Reporting.log_error pname ~loc exn)
+            | _ -> ()
+          in
+          print_debug_info instr mem' cond_set;
+          collect_instrs pdata node rem_instrs mem' cond_set
 
   let collect_node
     : extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t ->
       CFG.node -> Dom.ConditionSet.t
     = fun pdata inv_map cond_set node ->
-      let instrs = CFG.instr_ids node |> List.map ~f:fst in
       match Analyzer.extract_pre (CFG.id node) inv_map with
-      | Some mem -> collect_instrs pdata node instrs mem cond_set
+      | Some mem ->
+          let instrs = CFG.instrs node in
+          collect_instrs pdata node instrs mem cond_set
       | _ -> cond_set
 
   let collect : extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t

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

@@ -1,20 +1,56 @@
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]]
+codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
 codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10]]
+codetoanalyze/c/bufferoverrun/for_loop.c, safealloc, 10, UNREACHABLE_CODE, []
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call `arr_access()` ]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, []
 codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN, [Offset: [0, 255] Size: [255, 255]]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN, [Offset: [-1, 255] Size: [10000, 10000]]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1]]
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_exp_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_ge_Ok, 3, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_gt_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_le_Ok, 3, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_lt_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_ne_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 3, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]]
 codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
+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, []
+codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_return_good, 1, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_unreachable_good, 1, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_false_bad, 1, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_bad, 1, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad, 1, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, []
+codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, []
 codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10]]

infer/tests/codetoanalyze/c/bufferoverrun/models.c

@@ -9,10 +9,10 @@
 #include <stdio.h>
 #include <stdlib.h>
 
-void exit_good() {
+void exit_bo_good_unreachable_bad() {
   int arr[1];
   exit(1);
-  // unreachable
+  // unreachable so no buffer overrun
   arr[42] = 42;
 }
 

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

@@ -0,0 +1,149 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#include <stdlib.h>
+
+int __infer_nondet_int() {
+  int ret;
+  return ret;
+}
+
+void nop() {}
+
+void condition_always_true_bad() {
+  if (1) {
+    nop();
+  }
+}
+
+void condition_always_false_bad() {
+  if (0) {
+    nop();
+  }
+}
+
+void condition_always_true_with_else_bad() {
+  if (1) {
+    nop();
+  } else {
+    nop();
+  }
+}
+
+void exit_at_end_of_if_good() {
+  if (__infer_nondet_int()) {
+    exit(4);
+  }
+}
+
+void FN_useless_else_bad() {
+  if (__infer_nondet_int()) {
+    exit(0);
+  } else {
+    nop();
+  }
+}
+
+void never_loops_bad() {
+  while (0) {
+    nop();
+  }
+}
+
+void infinite_loop_bad() {
+  while (1) {
+    nop();
+  }
+}
+
+void FP_loop_with_break_good() {
+  while (1) {
+    if (__infer_nondet_int()) {
+      break;
+    }
+  }
+}
+
+void FP_loop_with_return_good() {
+  while (1) {
+    if (__infer_nondet_int()) {
+      return;
+    }
+  }
+}
+
+void FP_loop_with_exit_good() {
+  while (1) {
+    if (__infer_nondet_int()) {
+      exit(1);
+    }
+  }
+}
+
+void FP_loop_with_unreachable_good() {
+  while (1) {
+    if (__infer_nondet_int()) {
+      infinite_loop_bad();
+    }
+  }
+}
+
+void FN_loop_once_break_bad() {
+  while (__infer_nondet_int()) {
+    break;
+  }
+}
+
+void FN_loop_once_return_bad() {
+  while (__infer_nondet_int()) {
+    return;
+  }
+}
+
+void FN_loop_once_exit_bad() {
+  while (__infer_nondet_int()) {
+    exit(2);
+  }
+}
+
+void FN_loop_once_unreachable_bad() {
+  while (__infer_nondet_int()) {
+    infinite_loop_bad();
+  }
+}
+
+void FN_unreachable_statement_call_bad() {
+  infinite_loop_bad();
+  nop();
+}
+
+void unreachable_statement_exit_bad() {
+  exit(2);
+  nop();
+}
+
+void FN_unreachable_statement_return_bad() {
+  return;
+  nop();
+}
+
+void FN_unreachable_statement_break_bad() {
+  while (__infer_nondet_int()) {
+    if (__infer_nondet_int()) {
+      break;
+      nop();
+    }
+  }
+}
+
+void FN_unreachable_statement_continue_bad() {
+  while (__infer_nondet_int()) {
+    continue;
+    nop();
+  }
+}