From 1630079c23f12d1c1341deab930339fea280bd8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 7 Apr 2020 17:15:16 +0200
Subject: [PATCH] [Eva] Slightly better heuristic for automatic loop unroll on
some conditions.
---
.../value/partitioning/auto_loop_unroll.ml | 52 ++++++++++++-------
.../oracle/auto_loop_unroll.1.res.oracle | 12 ++---
2 files changed, 36 insertions(+), 28 deletions(-)
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index e6cd5f666aa..0d0a4ec3a1d 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -51,6 +51,10 @@
open Cil_types
+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 =
@@ -262,9 +266,23 @@ module Make (Abstract: Abstractions.Eva) = struct
(* If the new value of [expr] is top, no reduction has been performed. *)
if Val.(equal top value) then None else Some (value, record)
in
- (* Different strategies whether cvalue is present. *)
- match Val.get Main_values.CVal.key with
- | Some get_cvalue ->
+ (* Assumes that [condition] is [positive]. Returns an over-approximation
+ of the values for which [condition] is [positive]. *)
+ reduce positive >>= fun (value, record) ->
+ (* Evaluates [condition] with the hypothesis [expr] ∈ [value], to check
+ whether [expr] ∈ [value] ⇒ [condition] = [positive]. *)
+ let valuation = Valuation.add valuation expr record in
+ fst (Eval.evaluate ~valuation ~reduction:false state condition)
+ >> fun (_valuation, v) ->
+ let satisfied =
+ if positive
+ then not Val.(is_included zero v)
+ else Val.(equal zero v)
+ in
+ (* If the condition is satisfied, returns [value]. Otherwise, uses a
+ specific feature to cvalue (if possible) to compute a better value. *)
+ if satisfied then Some value else
+ Val.get Main_values.CVal.key >>= fun get_cvalue ->
(* Assumes that [condition] is NOT [positive]. *)
reduce (not positive) >>= fun (value, _record) ->
(* [value] is an over-approximation of the values of [expr] for which
@@ -273,21 +291,6 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue = get_cvalue value in
cvalue_complement (Cil.typeOf expr) cvalue >>= fun cvalue ->
Some (Val.set Main_values.CVal.key cvalue Val.top)
- | None ->
- (* Assumes that [condition] is [positive]. Returns an over-approximation
- of the values for which [condition] is [positive]. *)
- reduce positive >>= fun (value, record) ->
- (* Evaluates [condition] with the hypothesis [expr] ∈ [value], to check
- whether [expr] ∈ [value] ⇒ [condition] = [positive]. *)
- let valuation = Valuation.add valuation expr record in
- fst (Eval.evaluate ~valuation ~reduction:false state condition)
- >> fun (_valuation, v) ->
- let satisfied =
- if positive
- then not Val.(is_included zero v)
- else Val.(equal zero v)
- in
- if satisfied then Some value else None
(* Same as [reduce_to_expr] above, but builds the proper valuation from the
[state]. [state] is the entry state of the loop, and [expr] is the only
@@ -431,9 +434,18 @@ module Make (Abstract: Abstractions.Eva) = struct
in one iteration of the loop. *)
compute_delta lval loop_block >>= fun v_delta ->
let typ = Cil.typeOfLval lval in
- let limit = Val.inject_int typ (Integer.of_int limit) in
- (* Checks whether [v_init] + [limit] × [v_delta] ⊂ [v_exit]. *)
let binop op v1 v2 = Bottom.non_bottom (Val.forward_binop typ op v1 v2) in
+ (* Possible iterations numbers to exit the loop. *)
+ let iter_nb = binop Div (binop MinusA v_exit v_init) v_delta in
+ let bound = Abstract_value.Int (Integer.of_int limit) in
+ (* Use the iteration number if it is always smaller than the [limit].
+ Otherwise use [limit]. *)
+ let limit =
+ if is_true (Val.assume_bounded Alarms.Upper_bound bound iter_nb)
+ then iter_nb
+ else Val.inject_int typ (Integer.of_int limit)
+ in
+ (* Checks whether [v_init] + [limit] × [v_delta] ⊂ [v_exit]. *)
let value = binop PlusA v_init (binop Mult limit v_delta) in
Some (Val.is_included value v_exit)
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 8f9e19023f4..624e97c523d 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -341,14 +341,10 @@
[eva] Done for function complex_loops
[eva] computing for function various_conditions <- main.
Called from tests/value/auto_loop_unroll.c:251.
-[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:193: Warning:
- signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:197: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:198: Warning:
- signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:192: Automatic loop unrolling.
+[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;
--
GitLab