From 6338068f09999c117e6f0aa67d6cd78fdd3cacf6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 17 Jun 2020 19:08:26 +0200
Subject: [PATCH] [Eva] The automatic loop unrolling supports nested loop exit
 conditions.

This is required to automatically unroll loops with conditions such as
`nondet && x < 100`, as this is converted by the Frama-C kernel as two
nested conditional statements, where only the second one can be used to
unroll the loop.
---
 .../value/partitioning/auto_loop_unroll.ml    | 29 ++++++++++---------
 .../oracle/auto_loop_unroll.1.res.oracle      |  9 ++----
 2 files changed, 18 insertions(+), 20 deletions(-)

diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index 03af652f8f4..9cb77831f79 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -55,23 +55,24 @@ let is_true = function
   | `True | `TrueReduced _ -> true
   | _ -> false
 
-(* Is a statement a loop exit condition? If so, returns the condition and
-   whether the condition must hold to exit the loop. Otherwise, returns None. *)
-let is_conditional_break stmt =
-  match stmt.skind with
-  | If (cond, {bstmts=[{skind=Break _}]}, _, _) -> Some (cond, true)
-  | If (cond, _, {bstmts=[{skind=Break _}]}, _) -> Some (cond, false)
-  | _ -> None
-
-(* Returns a loop exit condition, as the conditional expression and whether
-   the condition must be zero or non-zero to exit the loop. *)
+(* Does a block exits a loop? *)
+let is_break block =
+  match block.bstmts with
+  | [{skind = Break _}] -> true
+  | _ -> false
+
+(* Returns a list of loop exit conditions. Each condition is expressed as an
+   expression and whether it must be zero or non-zero to exit the loop. *)
 let find_loop_exit_condition loop =
   let rec aux = function
     | [] -> []
     | stmt :: tl ->
-      match is_conditional_break stmt with
-      | Some x -> x :: aux tl
-      | None -> aux tl
+      match stmt.skind with
+      | If (cond, b1, b2, _) when is_break b1 || is_break b2 ->
+        if is_break b1
+        then (cond, true) :: aux (b2.bstmts @ tl)
+        else (cond, false) :: aux (b1.bstmts @ tl)
+      | _ -> aux tl
   in
   aux loop.bstmts
 
@@ -437,6 +438,8 @@ module Make (Abstract: Abstractions.Eva) = struct
       | Block block -> cross_block acc block
       | UnspecifiedSequence list ->
         List.fold_left (fun acc (s, _, _, _, _) -> cross_stmt acc s) acc list
+      | If (_, {bstmts=[{skind=Break _}]}, block, _)
+      | If (_, block, {bstmts=[{skind=Break _}]}, _) -> cross_block acc block
       | _ -> acc
     and cross_block acc block =
       List.fold_left cross_stmt acc block.bstmts
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 942c4164039..a1ed5bef663 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -347,13 +347,8 @@
 [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12}
 [eva:loop-unroll] tests/value/auto_loop_unroll.c:203: Automatic loop unrolling.
 [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_0_13: [0..13]
-[eva] tests/value/auto_loop_unroll.c:208: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:209: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:208: Warning: 
-  signed overflow. assert -2147483648 ≤ i_1 - 1;
-[eva] tests/value/auto_loop_unroll.c:211: 
-  Frama_C_show_each_0_14: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:208: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:211: Frama_C_show_each_0_14: [0..14]
 [eva] tests/value/auto_loop_unroll.c:214: starting to merge loop iterations
 [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning: 
   signed overflow. assert res + 1 ≤ 2147483647;
-- 
GitLab