From e945d78dc65718de6bb63efd00173e6954d77997 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Sat, 14 Aug 2021 17:05:23 +0200
Subject: [PATCH] [e-acsl:interval] simplify the case of \sum
---
src/plugins/e-acsl/src/analyses/interval.ml | 59 +++++++++++----------
1 file changed, 32 insertions(+), 27 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 5b5927ab5c7..91807d502aa 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -351,36 +351,41 @@ let extended_interv_of_typ ty = match interv_of_typ ty with
of the lower (resp. upper) bound and [name] is the identifier of the extended
quantifier (\sum, \product or \numof). The returned ival is the interval of
the extended quantifier. *)
-let interv_of_extended_quantifier lambda i j name =
- match lambda, i, j, name.lv_name with
- | Ival lbd_iv, Ival i_iv, Ival j_iv, "\\sum" ->
+let interv_of_extended_quantifier lambda lb up name =
+ match lambda, lb, up, name.lv_name with
+ | Ival lbd_iv, Ival lb_iv, Ival ub_iv, "\\sum" ->
(try
let min_lambda, max_lambda = Ival.min_and_max lbd_iv in
- let i_lb, i_ub = Ival.min_and_max i_iv in
- let j_lb, j_ub = Ival.min_and_max j_iv in
- let compute_bound bound_lambda is_lower_bound =
- let cond = match bound_lambda with
- | Some lambda ->
- (is_lower_bound && Z.compare lambda Z.zero = 1) ||
- (not is_lower_bound && Z.compare lambda Z.zero = -1)
- | None -> false
- in
- match bound_lambda, i_lb, i_ub, j_lb, j_ub with
- | Some lambda, _, Some i_ub, Some j_lb, _ when cond->
- Some (Z.mul lambda (Z.max (Z.sub j_lb i_ub) Z.zero))
- | _, _, _, _, _ when cond -> Some Z.zero
- | Some lambda, Some i_lb, _, _, Some j_ub ->
- Some (Z.mul lambda (Z.max (Z.sub j_ub i_lb) Z.zero))
- | Some lambda, _, _ , _, _ when Z.compare lambda Z.zero = 0 ->
- Some Z.zero
- | None, Some i_lb, _, _, Some j_ub when Z.compare j_ub i_lb = 0 ->
- Some Z.zero
- | _, _, _, _, _ -> None
+ let min_lb, min_ub = Ival.min_and_max lb_iv in
+ let max_lb, max_ub = Ival.min_and_max ub_iv in
+ (* the number of iterations is the distance between the upper bound and
+ the lower bound, or 0 if it is negative. *)
+ let delta a b = Z.max Z.zero (Z.sub a b) in
+ let min_iteration_number =
+ (* the minimum number of iterations is the distance between the
+ smallest upper bound and the biggest lower bound. *)
+ match min_ub, max_lb with
+ | Some mub, Some mlb -> delta mub mlb
+ | _, None | None, _ -> Z.zero
+ in
+ let max_iteration_number =
+ (* the maximum number of iterations is the distance between the
+ biggest upper bound and the smallest lower bound. *)
+ match max_ub, min_lb with
+ | Some mub, Some mlb -> Some (delta mub mlb)
+ | _, None | None, _ -> None
in
- Ival
- (Ival.inject_range
- (compute_bound min_lambda true)
- (compute_bound max_lambda false))
+ (* the lower (resp. upper) bound is the min (resp. max) value of
+ the lambda term times the min (resp. max) number of iterations *)
+ let lower_bound = match min_lambda with
+ | None -> None
+ | Some z -> Some (Z.mul z min_iteration_number)
+ in
+ let upper_bound = match max_lambda, max_iteration_number with
+ | None, _ | _, None -> None
+ | Some z, Some n -> Some (Z.mul z n)
+ in
+ Ival (Ival.inject_range lower_bound upper_bound)
with Abstract_interp.Error_Bottom ->
bottom)
| _, _, _, "\\product" -> Error.not_yet "product"
--
GitLab