[inferbo] Visit every nodes at narrowing

Reviewed By: mbouaziz

Differential Revision: D13320983

fbshipit-source-id: 1b31c3c17

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 ->
+        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
-          rest
+      ~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
 

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, [<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,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]

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++) {
+      }
+    }
+  }
+}