From 6a29b1bfce0bfa9f0438bf8ac77ac95bd10914ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 7 Apr 2020 20:04:24 +0200
Subject: [PATCH] [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).
---
.../value/partitioning/auto_loop_unroll.ml | 43 +++++++++++++++++++
.../oracle/auto_loop_unroll.1.res.oracle | 29 ++++---------
2 files changed, 51 insertions(+), 21 deletions(-)
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index defdb8a340d..9ede36c8b41 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/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]
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 624e97c523d..942c4164039 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/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}
--
GitLab