From ec7b096ff66e10aca4cfbefbe4e05d8d22f7eb70 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 2 Jun 2017 15:18:00 -0700 Subject: [PATCH] [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 | 3 + infer/src/IR/Exceptions.mli | 1 + infer/src/IR/Localise.ml | 6 + infer/src/IR/Localise.mli | 3 + infer/src/backend/errdesc.ml | 3 + infer/src/backend/errdesc.mli | 2 + .../src/bufferoverrun/bufferOverrunChecker.ml | 90 +++++++---- .../codetoanalyze/c/bufferoverrun/issues.exp | 36 +++++ .../codetoanalyze/c/bufferoverrun/models.c | 4 +- .../c/bufferoverrun/unreachable.c | 149 ++++++++++++++++++ 10 files changed, 265 insertions(+), 32 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index ac57e33d4..cd9507614 100644 --- a/infer/src/IR/Exceptions.ml +++ b/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) diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 53f4f0ff9..abef52364 100644 --- a/infer/src/IR/Exceptions.mli +++ b/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 diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 4caffe594..f2e6fdefd 100644 --- a/infer/src/IR/Localise.ml +++ b/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; diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 188955543..d6ee69765 100644 --- a/infer/src/IR/Localise.mli +++ b/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 diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index eadfa991a..3485b1c6a 100644 --- a/infer/src/backend/errdesc.ml +++ b/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 diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index ad44a7fff..7766144ec 100644 --- a/infer/src/backend/errdesc.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a63c720b4..d71fe415a 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index e991cd26c..4d3c83e04 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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]] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c index 7c25c5953..2c3065f52 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -9,10 +9,10 @@ #include #include -void exit_good() { +void exit_bo_good_unreachable_bad() { int arr[1]; exit(1); - // unreachable + // unreachable so no buffer overrun arr[42] = 42; } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c b/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c new file mode 100644 index 000000000..b451444e6 --- /dev/null +++ b/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 + +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(); + } +}