From a20bcac6c2150dacb80839c8542ba2a0bfffe9e4 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 20 Aug 2021 19:48:08 +0200
Subject: [PATCH] [interval] improve implementation of \product and \numof
---
src/libraries/stdlib/extlib.ml | 4 +
src/libraries/stdlib/extlib.mli | 5 +
src/plugins/e-acsl/src/analyses/interval.ml | 252 +++++++++-----------
3 files changed, 119 insertions(+), 142 deletions(-)
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index e6267f35c0f..a0a4b588d40 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -256,6 +256,10 @@ let opt_hash hash v = match v with
| None -> 31179
| Some v -> hash v
+let opt_map2 f x y = match x, y with
+ | None, _ | _, None -> None
+ | Some x, Some y -> Some (f x y)
+
(* ************************************************************************* *)
(** Booleans *)
(* ************************************************************************* *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 1ef17c991ac..5b02633a1b2 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -229,6 +229,11 @@ val the: exn:exn -> 'a option -> 'a
val opt_hash: ('a -> int) -> 'a option -> int
(** @since Sodium-20150201 *)
+val opt_map2: ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
+(** @return [f a b] if arguments are [Some a] and [Some b], orelse return
+ [None].
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Booleans} *)
(* ************************************************************************* *)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 08754985e86..91006e19915 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -290,6 +290,24 @@ let cast ~src ~dst = match src, dst with
certainly on purpose . *)
dst
+(* a-b; or 0 if negative *)
+let length a b = Z.max Z.zero (Z.add Z.one (Z.sub a b))
+
+(* minimal distance between two intervals given by their respective lower and
+ upper bounds, i.e. the length between the lower bound of the second interval
+ bound and the upper bound of the first interval. *)
+let min_delta (_, max1) (min2, _) = match max1, min2 with
+ | Some m1, Some m2 -> length m2 m1
+ | _, None | None, _ -> Z.zero
+
+(* maximal distance between between two intervals given by their respective
+ lower and upper bounds, i.e. the length between the upper bound of the second
+ interval and the lower bound of the first interval.
+ @return None for \infty *)
+let max_delta (min1, _) (_, max2) = match min1, max2 with
+ | Some m1, Some m2 -> Some (length m2 m1)
+ | _, None | None, _ -> None
+
(* ********************************************************************* *)
(* constructors and destructors *)
(* ********************************************************************* *)
@@ -346,135 +364,6 @@ let extended_interv_of_typ ty = match interv_of_typ ty with
| Rational | Real | Nan | Float (_,_) as i
-> i
-(*
-(* Compute the interval of the extended quantifier \sum, \product and \numof.
- [lambda] is the interval of the lambda term, [i] (resp. [j]) is the interval
- 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 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 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.add Z.one (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
- (* 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)
- | _ -> Error.not_yet "extended quantifiers with non-integer parameters"
-*)
-
-(* Compute the interval of the extended quantifier \sum, \product and \numof.
- [lbd_ival] is the interval of the lambda term, [k_ival] is the interval of
- the quantifier and [name] is the identifier of the extended quantifier (\sum
- or \product). The returned ival is the interval of the extended quantifier *)
-let interv_of_extended_quantifier lambda i j name =
- match lambda, i, j with
- | Ival lbd_ival, Ival i_ival, Ival j_ival ->
- (try
- let min_lambda, max_lambda = Ival.min_and_max lbd_ival in
- let i_inf, i_sup = Ival.min_and_max i_ival in
- let j_inf, j_sup = Ival.min_and_max j_ival in
- let compute_bound_sum bound_lambda is_inf_bound =
- let cond =
- match bound_lambda with
- | Some lambda ->
- (is_inf_bound && ((Z.compare lambda Z.zero)=1)) ||
- ((not is_inf_bound) && ((Z.compare lambda Z.zero)=(-1)))
- | None -> false
- in
- match bound_lambda, i_inf, i_sup, j_inf, j_sup with
- | Some lambda, _,Some i_sup, Some j_inf, _ when cond->
- Some (Z.mul lambda (Z.max (Z.sub j_inf i_sup) Z.zero))
- | _, _, _, _, _ when cond -> Some Z.zero
- | Some lambda, Some i_inf, _, _, Some j_sup ->
- Some (Z.mul lambda (Z.max (Z.sub j_sup i_inf) Z.zero))
- | Some lambda, _, _ , _, _ when (Z.compare lambda Z.zero) = 0 ->
- Some Z.zero
- | None, Some i_inf, _, _, Some j_sup when (Z.compare j_sup i_inf) = 0 ->
- Some Z.zero
- | _, _, _, _, _ -> None
- in
- let compute_bound_product =
- (try
- match min_lambda, max_lambda, i_inf, i_sup, j_inf, j_sup with
- | _, _, Some i_inf, _, _, Some j_sup
- when (Z.compare i_inf j_sup) = 1 ->
- (Ival.inject_range (Some Z.one) (Some Z.one))
- | Some lambda_inf, Some lambda_sup, Some i_inf, _, _, Some j_sup
- when (Z.compare i_inf j_sup) <= 0 &&
- (Z.compare lambda_inf Z.zero) <= 0 &&
- (Z.compare Z.zero lambda_sup) <= 0 ->
- let exponent = Z.to_int (Z.sub j_sup i_inf) in
- let bound =
- if (Z.compare lambda_sup (Z.neg lambda_inf)) <= 0 then
- (Z.pow (Z.neg lambda_inf) exponent)
- else
- (Z.pow lambda_sup exponent)
- in (Ival.inject_range (Some (Z.neg bound)) (Some bound))
- | Some lambda_inf, Some lambda_sup, Some i_inf, Some i_sup,
- Some j_inf, Some j_sup
- when (Z.compare i_inf j_sup) <= 0 &&
- (Z.compare lambda_inf Z.zero) = 1 &&
- (Z.compare lambda_inf lambda_sup) <= 0 ->
- let exponent= Z.to_int (Z.sub j_sup i_inf) in
- let bound_inf =
- if (Z.compare i_sup j_inf <= 0) then
- Z.pow lambda_inf (Z.to_int (Z.sub j_inf i_sup))
- else
- Z.one
- in
- Ival.inject_range
- (Some bound_inf) (Some (Z.pow lambda_sup exponent))
- | Some lambda_inf, Some lambda_sup, Some i_inf, _, _, Some j_sup
- when (Z.compare i_inf j_sup) <= 0 &&
- (Z.compare lambda_sup Z.zero)=(-1) &&
- (Z.compare lambda_inf lambda_sup) <= 0 ->
- let bound = Z.pow (Z.neg lambda_inf) (Z.to_int (Z.sub j_sup i_inf))
- in
- Ival.inject_range (Some (Z.neg bound)) (Some bound)
- | _ -> Ival.inject_range None None
- with Z.Overflow ->
- (Ival.inject_range None None))
- in
- match name.lv_name with
- | "\\sum" -> Ival (Ival.inject_range
- (compute_bound_sum min_lambda true)
- (compute_bound_sum max_lambda false))
- | "\\product" -> Ival compute_bound_product
- | _ -> assert false (* unreachable branch *)
- with Abstract_interp.Error_Bottom ->
- bottom)
- | _ -> Error.not_yet "extended quantifiers with non-integer parameters"
-
let interv_of_logic_typ = function
| Ctype ty -> interv_of_typ ty
| Linteger -> top_ival
@@ -643,7 +532,7 @@ end = struct
end
(* ********************************************************************* *)
-(* Main algorithm *)
+(* Main functions *)
(* ********************************************************************* *)
let infer_sizeof ty =
@@ -654,6 +543,85 @@ let infer_alignof ty =
try singleton_of_int (Cil.bytesAlignOf ty)
with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
+(* Infer the interval of an extended quantifier \sum or \product.
+ [lambda] is the interval of the lambda term, [min] (resp. [max]) is the
+ interval of the minimum (resp. maximum) and [oper] is the identifier of the
+ extended quantifier (\sum, or \product). The returned ival is the interval of
+ the extended quantifier. *)
+let infer_sum_product oper lambda min max = match lambda, min, max with
+ | Ival lbd_iv, Ival lb_iv, Ival ub_iv ->
+ (try
+ let min_lambda, max_lambda = Ival.min_and_max lbd_iv in
+ let minmax_lb = Ival.min_and_max lb_iv in
+ let minmax_ub = Ival.min_and_max ub_iv in
+ let lb, ub = match oper.lv_name with
+ | "\\sum" ->
+ (* the lower (resp. upper) bound is the min (resp. max) value of the
+ lambda term, times the min (resp. max) distance between them if
+ the sign is positive, or conversely if the sign is negative *)
+ let lb = match min_lambda with
+ | None -> None
+ | Some z ->
+ if Z.sign z = -1
+ then Option.map (Z.mul z) (max_delta minmax_lb minmax_ub)
+ else Some (Z.mul z (min_delta minmax_lb minmax_ub))
+ in
+ let ub = match max_lambda with
+ | None -> None
+ | Some z ->
+ if Z.sign z = -1
+ then Some (Z.mul z (min_delta minmax_lb minmax_ub))
+ else Option.map (Z.mul z) (max_delta minmax_lb minmax_ub)
+ in
+ lb, ub
+ | "\\product" ->
+ (* the lower (resp. upper) bound is the min (resp. max) value of the
+ lambda term in absolute value, power the min (resp. max) distance
+ between them if the sign is positive, or conversely for both the
+ lambda term and the exponent if the sign is negative. If the sign
+ is negative, the minimum is also negative. *)
+ let min, max =
+ match min_lambda, max_lambda with
+ | None, None as res -> res
+ | None, Some m | Some m, None -> Some m, None
+ | Some min, Some max ->
+ let abs_min = Z.abs min in
+ let abs_max = Z.abs max in
+ Some (Z.min abs_min abs_max), Some (Z.max abs_min abs_max)
+ in
+ let lb = match min_lambda with
+ | None -> None
+ | Some z ->
+ if Z.sign z = -1 then
+ (* the lower bound is (possibly) negative *)
+ Extlib.opt_map2
+ (fun m max -> Z.neg (Z.pow max (Z.to_int m)))
+ (max_delta minmax_lb minmax_ub)
+ max
+ else
+ (* all numbers are positive:
+ the lower bound is necessarily positive *)
+ Option.map
+ (fun m -> Z.pow m (Z.to_int (min_delta minmax_lb minmax_ub)))
+ min
+ in
+ let ub =
+ (* the upper bound is always (possibly) positive *)
+ Extlib.opt_map2
+ (fun m max -> Z.pow max (Z.to_int m))
+ (max_delta minmax_lb minmax_ub)
+ max
+ in
+ lb, ub
+ | s ->
+ Options.fatal "unexpect logic function '%s'" s
+ in
+ Ival (Ival.inject_range lb ub)
+ with
+ | Abstract_interp.Error_Bottom -> bottom
+ | Z.Overflow (* if the exponent of \product is too high *) -> top_ival)
+ | _ -> Error.not_yet "extended quantifiers with non-integer parameters"
+
let rec infer t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
match t.term_node with
@@ -776,28 +744,28 @@ let rec infer t =
| LBnone when li.l_var_info.lv_name = "\\sum" ||
li.l_var_info.lv_name = "\\product" ->
(match args with
- | [ t1; t2; {term_node = Tlambda([ k ], _)} as lambda ] ->
- let t1_ival = infer t1 in
- let t2_ival = infer t2 in
- let k_ival = join t1_ival t2_ival in
- Env.add k k_ival;
- let lambda_ival = infer lambda in
+ | [ t1; t2; { term_node = Tlambda([ k ], _) } as lambda ] ->
+ let t1_iv = infer t1 in
+ let t2_iv = infer t2 in
+ let k_iv = join t1_iv t2_iv in
+ Env.add k k_iv;
+ let lambda_iv = infer lambda in
Env.remove k;
let t2incr =
- Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger in
+ Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
+ in
(* it is correct and precise to use k_ival to compute lambda_ival, but
not during the code generation since the type used for k is the
greatest type between the type of t1 and the type of t2+1, that is
why the ival associated to k is updated *)
- Env.add k (join t1_ival (infer t2incr));
+ Env.add k (join t1_iv (infer t2incr));
(* k is removed during code generation, it is needed for generating
the code of the lambda term *)
- interv_of_extended_quantifier
- lambda_ival t1_ival t2_ival li.l_var_info
+ infer_sum_product li.l_var_info lambda_iv t1_iv t2_iv
| _ -> Error.not_yet "extended quantifiers without lambda term")
| LBnone when li.l_var_info.lv_name = "\\numof" ->
(match args with
- | [ t1; t2; {term_node = Tlambda([ k ], predicate)} ] ->
+ | [ t1; t2; { term_node = Tlambda([ k ], p) } ] ->
let logic_info = Cil_const.make_logic_info "\\sum" in
logic_info.l_type <- li.l_type;
logic_info.l_tparams <- li.l_tparams;
@@ -807,7 +775,7 @@ let rec infer t =
let numof_as_sum =
let conditional_term =
Logic_const.term
- (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
+ (Tif(p, Cil.lone (), Cil.lzero ())) Linteger
in
let lambda_term =
Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
--
GitLab