Skip to content
Snippets Groups Projects
Commit a20bcac6 authored by Julien Signoles's avatar Julien Signoles
Browse files

[interval] improve implementation of \product and \numof

parent 2fb3f8f6
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/libraries/stdlib/extlib.ml
+ 4
− 0
View file @ a20bcac6
......@@ -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 *)
(* ************************************************************************* *)
......
src/libraries/stdlib/extlib.mli
+ 5
− 0
View file @ a20bcac6
......@@ -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} *)
(* ************************************************************************* *)
......
src/plugins/e-acsl/src/analyses/interval.ml
+ 110
− 142
View file @ a20bcac6
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment