[Eva] Improves the automatic loop unroll when temporary variables are introduced.

If the variable used in the exit condition of the loop is not incremented within
the loop, but is assigned to the value of another lvalue, the heuristic uses
this second lvalue instead.
This is especially useful to deal with some temporary variables introduced
by Frama-C to translate condition such as (i++ < l).

src/plugins/value/partitioning/auto_loop_unroll.ml

@@ -395,6 +395,8 @@ module Make (Abstract: Abstractions.Eva) = struct
       | If (_e, b1, b2, _loc) ->
         join_delta (delta_block acc b1) (delta_block acc b2)
       | Block b -> delta_block acc b
+      | UnspecifiedSequence list ->
+        List.fold_left (fun acc (s, _, _, _, _) -> delta_stmt acc s) acc list
       | _ ->
         (* For other statements, we only check that they do not modify [lval]. *)
         if is_safe lval ~loop stmt then acc else raise NoIncrement
@@ -407,6 +409,43 @@ module Make (Abstract: Abstractions.Eva) = struct
       final_delta delta >> fun d -> Some d
     with NoIncrement -> None
 
+  (* If in the block [loop], [lval] is assigned once to the value of another
+     lvalue, returns this new lvalue. Otherwise, returns [lval]. *)
+  let cross_equality lval loop =
+    (* If no such single equality can be found, return [lval] unchanged. *)
+    let exception No_equality in
+    let rec find_lval acc expr =
+      if acc <> None then raise No_equality else
+        match expr.enode with
+        | Lval lval -> Some lval
+        | Info (e, _) -> find_lval acc e
+        | _ -> raise No_equality
+    in
+    let cross_instr acc = function
+      | Set (lv, expr, _loc) when Cil_datatype.LvalStructEq.equal lv lval ->
+        find_lval acc expr
+      | Local_init (varinfo, AssignInit (SingleInit expr), _loc)
+        when Cil_datatype.LvalStructEq.equal (Cil.var varinfo) lval ->
+        find_lval acc expr
+      | Call (Some lv, _, _, _) when Cil_datatype.LvalStructEq.equal lval lv ->
+        raise No_equality
+      | _ -> acc
+    in
+    let rec cross_stmt acc stmt =
+      match stmt.skind with
+      | Instr instr -> cross_instr acc instr
+      | Block block -> cross_block acc block
+      | UnspecifiedSequence list ->
+        List.fold_left (fun acc (s, _, _, _, _) -> cross_stmt acc s) acc list
+      | _ -> acc
+    and cross_block acc block =
+      List.fold_left cross_stmt acc block.bstmts
+    in
+    match cross_block None loop with
+    | None -> lval
+    | Some lval -> lval
+    | exception No_equality -> lval
+
   (* If [lval] is a varinfo out-of-scope at statement [stmt] of function [kf],
      introduces it to the [state]. *)
   let enter_scope state kf stmt lval =
@@ -443,6 +482,10 @@ module Make (Abstract: Abstractions.Eva) = struct
     (* Reduce [condition] to a sufficient hypothesis over the [lval] value:
        if [lval] ∈ [v_exit] then [condition = positive]. *)
     reduce_to_lval_from_state state lval condition positive >>= fun v_exit ->
+    (* If [lval] is only assigned to the value of another lvalue, uses it
+       instead. This is especially useful to deal with temporary variables
+       introduced by the Frama-C normalization. *)
+    let lval = cross_equality lval loop_block in
     (* Evaluates the initial value [v_init] of [lval] in the loop entry state. *)
     evaluate_lvalue state lval >>= fun v_init ->
     (* Computes an over-approximation [v_delta] of the increment of [lval]

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

@@ -345,13 +345,8 @@
 [eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: {11}
 [eva:loop-unroll] tests/value/auto_loop_unroll.c:197: Automatic loop unrolling.
 [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12}
-[eva] tests/value/auto_loop_unroll.c:203: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:203: Warning: 
-  signed overflow. assert -2147483648 ≤ i_0 - 1;
-[eva] tests/value/auto_loop_unroll.c:206: 
-  Frama_C_show_each_0_13: [0..2147483647]
+[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;
@@ -372,18 +367,10 @@
 [eva] Done for function various_conditions
 [eva] computing for function temporary_variables <- main.
   Called from tests/value/auto_loop_unroll.c:252.
-[eva] tests/value/auto_loop_unroll.c:235: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:235: Warning: 
-  signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:236: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:240: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:241: Warning: 
-  signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: 
-  signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:235: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: {20}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: {21}
 [eva] Recording results for temporary_variables
 [eva] Done for function temporary_variables
 [eva] Recording results for main
@@ -412,8 +399,8 @@
 [eva:final-states] Values at end of function simple_loops:
   res ∈ {100}
 [eva:final-states] Values at end of function temporary_variables:
-  i ∈ [-2147483648..20]
-  res ∈ [0..2147483647]
+  i ∈ {-1}
+  res ∈ {21}
 [eva:final-states] Values at end of function various_conditions:
   i ∈ {12}
   res ∈ {0}