[Eva] Slightly improves the automatic loop unrolling on loops with goto statements.

src/plugins/value/partitioning/auto_loop_unroll.ml

@@ -200,7 +200,7 @@ let is_safe_instruction lval = function
   | Asm _ -> false
 
 (* Returns true if the statement [stmt] of function [kf] does not modify [lval].
-   [lval] is a candidate for the automatic loop unrolling of [loop] [loop]. *)
+   [lval] is a candidate for the automatic loop unrolling of [loop]. *)
 let is_constant kf ~loop lval stmt =
   let rec is_safe_stmt ~goto stmt =
     match stmt.skind with
@@ -224,12 +224,19 @@ let is_constant kf ~loop lval stmt =
          that contains the current loop, which we don't want to unroll. *)
       let dest_blocks = Kernel_function.find_all_enclosing_blocks !dest in
       List.exists (Cil_datatype.Block.equal loop) dest_blocks &&
-      (* Otherwise, the goto stays within the loop: check that the block
-         englobing both the source and the destination is safe. *)
-      let block = Kernel_function.common_block !dest stmt in
-      (* If this block is the loop itself, then it is not safe,
-         as [lval] is modified within the loop. *)
-      not (block == loop) && is_safe_block ~goto:true block
+      (* Otherwise, the goto stays within the loop. *)
+      begin
+        (* If the successors all exits the loop block, then the goto is safe.
+           This is the case for gotos coming from "continue" statement.  *)
+        let all_stmts = Stmts_graph.get_block_stmts loop in
+        let is_outside_loop s = not (Cil_datatype.Stmt.Set.mem s all_stmts) in
+        List.for_all is_outside_loop !dest.succs ||
+        (* Otherwise, check that the block englobing both the source and the
+           destination is safe. If this block is the loop itself, then it is
+           not safe, as [lval] is modified within the loop. *)
+        let block = Kernel_function.common_block !dest stmt in
+        not (block == loop) && is_safe_block ~goto:true block
+      end
     | _ -> false
   (* A block is safe if all its statements are safe. *)
   and is_safe_block ~goto b = List.for_all (is_safe_stmt ~goto) b.bstmts in

tests/value/oracle/auto_loop_unroll.1.res.oracle

@@ -395,21 +395,12 @@
 [eva:alarm] tests/value/auto_loop_unroll.c:291: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
 [eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_top: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:299: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:302: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:304: 
-  Frama_C_show_each_0_35: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning: 
-  signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:314: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:317: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:319: Frama_C_show_each_27: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:299: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_0_35: [0..35]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:307: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: {36}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:314: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:319: Frama_C_show_each_27: {27}
 [eva] Recording results for loops_with_goto
 [eva] Done for function loops_with_goto
 [eva] computing for function non_natural_loops <- main.