diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 1c8061227289f992e5e108d0ea2f8c0bbed28119..08f59cbf348cd517a477edcaa61ba1498415b779 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -233,7 +233,7 @@ let rec infer t =
TODO: I do not understand the remark above. The interval of a C
global variable is computed from its type. *)
let ieqs = Interval_system.empty in
- let ivar, ieqs, _ = build_ieqs t ieqs [] in
+ let iexp, ieqs, _ = build_ieqs t ieqs [] in
(* 2) Solve it:
The problem is probably undecidable in the general case.
Thus we just look for reasonably precise approximations
@@ -245,7 +245,13 @@ let rec infer t =
(* This set can be changed based on experimental evidences,
but it works fine for now. *)
in
- Interval_system.solve ieqs ivar chain_of_ivalmax
+ match iexp with
+ | Interval_system.Ivar ivar ->
+ Interval_system.solve ieqs ivar chain_of_ivalmax
+ | Interval_system.Iconst _
+ | Interval_system.Ibinop _
+ | Interval_system.Iunsupported ->
+ assert false
else begin (* non-recursive case *)
(* add the arguments to the context *)
List.iter2
@@ -364,13 +370,16 @@ and build_ieqs t ieqs ivars =
args
in
(* x *)
- let ivar = Interval_system.Ivar(li.l_var_info.lv_name, args_lty) in
+ let ivar =
+ { Interval_system.iv_name = li.l_var_info.lv_name;
+ iv_types = args_lty }
+ in
(* Adding x = g(x) if it is not yet in the system of equations.
Without this check, the algorithm would not terminate. *)
let ieqs, ivars =
if Interval_system.ivars_contains_ivar ivars ivar then ieqs, ivars
else
- let iexp, ieqs, ivars =
+ let (iexp:Interval_system.ival_exp), ieqs, ivars =
build_ieqs (Misc.term_of_li li) ieqs (ivar :: ivars)
in
(* Adding x = g(x) *)
@@ -378,7 +387,7 @@ and build_ieqs t ieqs ivars =
ieqs, ivars
in
List.iter (fun lv -> Env.remove lv) li.l_profile;
- ivar, ieqs, ivars
+ Interval_system.Ivar ivar, ieqs, ivars
end else
(try Interval_system.Iconst(infer t), ieqs, ivars
with Not_an_integer -> Interval_system.Iunsupported, ieqs, ivars)
diff --git a/src/plugins/e-acsl/interval_system.ml b/src/plugins/e-acsl/interval_system.ml
index 16f928f06f7665f1c2d1da095ae008eb27090d4f..9ad95cf582b14f021886b16393915572264b5def 100644
--- a/src/plugins/e-acsl/interval_system.ml
+++ b/src/plugins/e-acsl/interval_system.ml
@@ -22,37 +22,47 @@
open Cil_types
+(**************************************************************************)
+(******************************* Types ************************************)
+(**************************************************************************)
+
type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
+type ivar = { iv_name: string; iv_types: logic_type list }
+
type ival_exp =
| Iconst of Ival.t
- | Ivar of string * logic_type list
+ | Ivar of ivar
| Ibinop of ival_binop * ival_exp * ival_exp
| Iunsupported
-let equal_ivar ivar1 ivar2 = match ivar1, ivar2 with
- | Ivar(str1, ltys1), Ivar(str2, ltys2) ->
- str1 = str2 &&
- List.fold_left2
- (fun b lty1 lty2 -> b && Cil_datatype.Logic_type.equal lty1 lty2)
- true
- ltys1
- ltys2
- | _ ->
- Options.fatal "not an ivar"
+module LT_List =
+ Datatype.List_with_collections
+ (Cil_datatype.Logic_type)
+ (struct let module_name = "E_ACSL.Interval_system.LT_List" end)
+
+module Ivar =
+ Datatype.Make_with_collections(struct
+ type t = ivar
+ let name = "E_ACSL.Interval_system.Ivar"
+ let reprs = [ { iv_name = "a"; iv_types = Cil_datatype.Logic_type.reprs } ]
+ include Datatype.Undefined
+ let compare iv1 iv2 =
+ let n = Datatype.String.compare iv1.iv_name iv2.iv_name in
+ if n = 0 then LT_List.compare iv1.iv_types iv2.iv_types
+ else n
+ let equal = Datatype.from_compare
+ let hash iv = Datatype.String.hash iv.iv_name + 7 * LT_List.hash iv.iv_types
+ end)
+
+type t = ival_exp Ivar.Map.t
-module System = Map.Make(struct
- type t = ival_exp (* an Ivar to be precise *)
- let compare ivar1 ivar2 = if equal_ivar ivar1 ivar2 then 0 else 1
-end)
-
-type t = ival_exp System.t
-
-let empty = System.empty
+(**************************************************************************)
+(***************************** Solver *************************************)
+(**************************************************************************)
-let add_equation ivar iexp ieqs = match ivar with
- | Ivar _ -> System.add ivar iexp ieqs
- | _ -> Options.fatal "left-hand side is NOT an ivar"
+let empty = Ivar.Map.empty
+let add_equation = Ivar.Map.add
(* Normalize the expression.
An expression is said to be normalized if it is:
@@ -71,12 +81,12 @@ let normalize_iexp iexp =
if has_unsupported iexp then Iunsupported else iexp
let normalize_ieqs ieqs =
- System.map (fun iexp -> normalize_iexp iexp) ieqs
+ Ivar.Map.map (fun iexp -> normalize_iexp iexp) ieqs
let ivars_contains_ivar ivars ivar =
- List.fold_left (fun b ivar' -> b || equal_ivar ivar ivar') false ivars
+ List.fold_left (fun b ivar' -> b || Ivar.equal ivar ivar') false ivars
-let get_ival_of_iconst ieqs ivar = match System.find ieqs ivar with
+let get_ival_of_iconst ieqs ivar = match Ivar.Map.find ieqs ivar with
| Iconst i -> i
| Ivar _ | Ibinop _| Iunsupported -> Options.fatal "not an Iconst"
@@ -120,7 +130,7 @@ let iterate indexes max =
let to_iconsts indexes ieqs chain_of_ivalmax =
let max = Array.length chain_of_ivalmax in
let indexes_i = ref 0 in
- System.map
+ Ivar.Map.map
(fun _ ->
let ival =
let index = indexes.(!indexes_i) in
@@ -144,8 +154,8 @@ let rec eval_iexp iexp iconsts =
Iconst (Ival.inject_range None None)
| Iconst _ ->
iexp
- | Ivar _ ->
- System.find iexp iconsts
+ | Ivar iv ->
+ Ivar.Map.find iv iconsts
| Ibinop(_, Iunsupported, _) | Ibinop(_, _, Iunsupported) ->
assert false (* because [iexp] has been normalized *)
| Ibinop(ibinop, iexp1, iexp2) ->
@@ -175,10 +185,10 @@ let equal_iconst iconst1 iconst2 =
in
Ival.is_included i1 i2
-let is_post_fixpoint ieqs iconsts = System.fold
+let is_post_fixpoint ieqs iconsts = Ivar.Map.fold
(fun ivar iexp b ->
let iconst1 = eval_iexp iexp iconsts in
- let iconst2 = System.find ivar iconsts in
+ let iconst2 = Ivar.Map.find ivar iconsts in
b && equal_iconst iconst1 iconst2)
ieqs
true
@@ -194,7 +204,7 @@ let rec iterate_till_post_fixpoint ieqs indexes chain_of_ivalmax =
let solve ieqs ivar chain_of_ivalmax =
let ieqs = normalize_ieqs ieqs in
- let dim = System.cardinal ieqs in
+ let dim = Ivar.Map.cardinal ieqs in
let bottom = Array.make dim 0 in
let post_fixpoint =
iterate_till_post_fixpoint ieqs bottom chain_of_ivalmax
diff --git a/src/plugins/e-acsl/interval_system.mli b/src/plugins/e-acsl/interval_system.mli
index cbfce5bccbd7c12f84b82ce43443e2027c5be5c1..44a179eaf744f1a7aa03975ada2916c6b8f30890 100644
--- a/src/plugins/e-acsl/interval_system.mli
+++ b/src/plugins/e-acsl/interval_system.mli
@@ -31,11 +31,15 @@ open Cil_types
type ival_binop = Ival_add | Ival_min | Ival_mul | Ival_div | Ival_union
+(* variables of the system represents functions of a given names and types for
+ its parameters.
+ No need to store the type of the return value since it is computable from the
+ type of its parameters. *)
+type ivar = { iv_name: string; iv_types: logic_type list }
+
type ival_exp =
| Iconst of Ival.t
- | Ivar of string (* function name *) * logic_type list (* args lty *)
- (** Example: to the function signature f(int, long) corresponds
- the expression Ivar("f", [int; long]) *)
+ | Ivar of ivar
| Ibinop of ival_binop * ival_exp * ival_exp
| Iunsupported
@@ -52,14 +56,13 @@ type t
(**************************************************************************)
val empty: t
-val add_equation:
- ival_exp (* left-hand side, MUST be an [Ivar] *) -> ival_exp -> t -> t
+val add_equation: ivar -> ival_exp -> t -> t
(**************************************************************************)
(***************************** Solver *************************************)
(**************************************************************************)
-val solve: t -> ival_exp -> Integer.t array -> Ival.t
+val solve: t -> ivar -> Integer.t array -> Ival.t
(** [solve ieqs ivar chain] finds an interval for the variable [ivar]
that satisfies the fixpoint equation [ieqs]. The solver is parameterized
by the increasingly sorted array [chain] of positive integers.
@@ -75,6 +78,6 @@ val solve: t -> ival_exp -> Integer.t array -> Ival.t
(****************************** Utils *************************************)
(**************************************************************************)
-val ivars_contains_ivar: ival_exp list -> ival_exp -> bool
+val ivars_contains_ivar: ivar list -> ivar -> bool
(** [contains ivars ivar] checks whether the list of Ivar [ivars] contains the
Ivar [ivar]. *)