From 98d05044fbc241635c876e4a1708ddd567134d25 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 6 Dec 2018 06:21:40 -0800 Subject: [PATCH] [inferbo] Visit every nodes at narrowing Reviewed By: mbouaziz Differential Revision: D13320983 fbshipit-source-id: 1b31c3c17 --- infer/src/absint/AbstractInterpreter.ml | 20 +++++++++----- .../codetoanalyze/c/bufferoverrun/issues.exp | 5 ++++ .../c/bufferoverrun/nested_loop.c | 26 +++++++++++++++++++ 3 files changed, 44 insertions(+), 7 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index dd9ca5ffc..c25ba4e91 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -344,15 +344,21 @@ module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct L.(die InternalError) "Could not compute the pre of a node" - let rec exec_wto_component ~pp_instr cfg proc_data inv_map head ~is_loop_head ~is_narrowing rest - = + let rec exec_wto_component ~pp_instr cfg proc_data inv_map head ~is_loop_head ~is_narrowing + ~is_first_visit rest = match exec_wto_node ~pp_instr cfg proc_data inv_map head ~is_loop_head ~is_narrowing with | inv_map, ReachedFixPoint -> - inv_map + if is_narrowing && is_first_visit then + exec_wto_rest ~pp_instr cfg proc_data inv_map head ~is_narrowing rest + else inv_map | inv_map, DidNotReachFixPoint -> - let inv_map = exec_wto_partition ~pp_instr cfg proc_data ~is_narrowing inv_map rest in - exec_wto_component ~pp_instr cfg proc_data inv_map head ~is_loop_head:true ~is_narrowing - rest + exec_wto_rest ~pp_instr cfg proc_data inv_map head ~is_narrowing rest + + + and exec_wto_rest ~pp_instr cfg proc_data inv_map head ~is_narrowing rest = + let inv_map = exec_wto_partition ~pp_instr cfg proc_data ~is_narrowing inv_map rest in + exec_wto_component ~pp_instr cfg proc_data inv_map head ~is_loop_head:true ~is_narrowing + ~is_first_visit:false rest and exec_wto_partition ~pp_instr cfg proc_data ~is_narrowing inv_map @@ -369,7 +375,7 @@ module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct | Component {head; rest; next} -> let inv_map = exec_wto_component ~pp_instr cfg proc_data inv_map head ~is_loop_head:false ~is_narrowing - rest + ~is_first_visit:true rest in exec_wto_partition ~pp_instr cfg proc_data ~is_narrowing inv_map next diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ef718c513..04bb92c36 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -167,6 +167,11 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop_narrowing_Bad, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop_narrowing_Bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop_narrowing_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop_narrowing_Good, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop_narrowing_Good, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c index 26743d5a3..575cc653d 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/nested_loop.c @@ -52,3 +52,29 @@ void nested_loop4_Bad() { } } } + +void nested_loop_narrowing_Good() { + int i = 0; + int a[10]; + + while (1) { + while (1) { + a[i] = 0; + for (i = 0; i < 5; i++) { + } + } + } +} + +void nested_loop_narrowing_Bad() { + int i = 0; + int a[10]; + + while (1) { + while (1) { + a[i] = 0; + for (i = 0; i < 10; i++) { + } + } + } +}