From f86675499a3851e2936a5cd496dd3b62b21e54ef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 7 Apr 2020 18:51:40 +0200
Subject: [PATCH] [Eva] Auto loop unroll: do not fail when a varinfo is not in
scope.
The exit condition of a loop can refer to a temporary variable that is not in
scope at the beginning of the loop. In this case, the exit condition cannot be
properly evaluated in the entry state of the loop, unless the variable is
introduced into the state.
---
.../value/partitioning/auto_loop_unroll.ml | 19 +++++++++++++++++--
1 file changed, 17 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index 0d0a4ec3a1d..defdb8a340d 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -407,6 +407,18 @@ module Make (Abstract: Abstractions.Eva) = struct
final_delta delta >> fun d -> Some d
with NoIncrement -> None
+ (* 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 =
+ match lval with
+ | Var vi, _ when not (vi.vglob || vi.vformal
+ || Kernel_function.var_is_in_scope stmt vi) ->
+ let kind = Abstract_domain.Local kf in
+ let state = Abstract.Dom.enter_scope kind [vi] state in
+ let location = Abstract.Loc.eval_varinfo vi in
+ Abstract.Dom.logic_assign None location state
+ | _ -> state
+
(* Evaluates the lvalue [lval] in the state [state]. Returns None if the value
may be undeterminate. *)
let evaluate_lvalue state lval =
@@ -417,7 +429,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Is the number of iterations of a loop bounded by [limit]?
[state] is the loop entry state, and [loop_block] the block of the loop. *)
- let is_bounded_loop state limit loop_block =
+ let is_bounded_loop kf stmt state limit loop_block =
(* Computes the effect of the loop. Stops if it contains assembly code. *)
loop_effect_visitor#compute_effect loop_block >>= fun loop_effect ->
(* Finds the first loop exit condition, or stops. *)
@@ -425,6 +437,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Finds the unique integer lvalue modified within the loop in [condition].
Stops if it does not exist is not a good candidate for the heuristic. *)
find_lonely_candidate loop_effect condition >>= fun lval ->
+ (* If [lval] is not in scope at [stmt], introduces it into [state] so that
+ [lval] can be properly evaluated in [state]. *)
+ let state = enter_scope state kf stmt lval in
(* 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 ->
@@ -457,7 +472,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let loop_stmt = Kernel_function.find_enclosing_loop kf stmt in
match loop_stmt.skind with
| Loop (_code_annot, block, _loc, _, _) ->
- is_bounded_loop state max_unroll block >>= fun bounded ->
+ is_bounded_loop kf stmt state max_unroll block >>= fun bounded ->
if bounded then Some max_unroll else None
| _ -> None
with Not_found -> None
--
GitLab