From 4fdaf257ae9625617e7141a8280f76b030e43fc4 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 30 Jan 2018 08:14:19 -0800 Subject: [PATCH] [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 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 59 +++++++------------ .../codetoanalyze/c/bufferoverrun/issues.exp | 3 - .../c/bufferoverrun/unreachable.c | 4 +- 3 files changed, 24 insertions(+), 42 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 9fa6049b6..c86a81378 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 1f73f5965..1c2447745 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c b/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c index 477ddb0e1..57829f427 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c +++ b/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); }