From 275b020154775ef9a1e796ee64f154f862e25304 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 17:20:14 +0100
Subject: [PATCH] [Interval] rename build_ieqs to Interval_system.build
---
src/plugins/e-acsl/interval.ml | 153 ++++---------------------
src/plugins/e-acsl/interval_system.ml | 128 ++++++++++++++++++++-
src/plugins/e-acsl/interval_system.mli | 12 +-
3 files changed, 150 insertions(+), 143 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 7dcf07af3b4..dfc1b52ca6d 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -25,58 +25,25 @@ open Cil_types
(* Implement Figure 3 of J. Signoles' JFLA'15 paper "Rester statique pour
devenir plus rapide, plus précis et plus mince". *)
-exception Not_an_integer
-
(* ********************************************************************* *)
(* Basic datatypes and operations *)
(* ********************************************************************* *)
+exception Not_an_integer = Interval_system.Not_an_integer
+let interv_of_typ = Interval_system.interv_of_typ
+let ikind_of_interv = Interval_system.ikind_of_interv
+
(* constructors *)
let singleton_of_int n = Ival.inject_singleton (Integer.of_int n)
-let rec interv_of_typ ty = match Cil.unrollType ty with
- | TInt (k,_) as ty ->
- let n = Cil.bitsSizeOf ty in
- let l, u =
- if Cil.isSigned k then Cil.min_signed_number n, Cil.max_signed_number n
- else Integer.zero, Cil.max_unsigned_number n
- in
- Ival.inject_range (Some l) (Some u)
- | TEnum(enuminfo, _) -> interv_of_typ (TInt (enuminfo.ekind, []))
- | _ ->
- raise Not_an_integer
-
-let ikind_of_interv i =
- if Ival.is_bottom i then IInt
- else match Ival.min_and_max i with
- | Some l, Some u ->
- let is_pos = Integer.ge l Integer.zero in
- let lkind = Cil.intKindForValue l is_pos in
- let ukind = Cil.intKindForValue u is_pos in
- (* kind corresponding to the interval *)
- let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
- (* convert the kind to [IInt] whenever smaller. *)
- if Cil.intTypeIncluded kind IInt then IInt else kind
- | None, None -> raise Cil.Not_representable (* GMP *)
- | None, Some _ | Some _, None ->
- Kernel.fatal ~current:true "ival: %a" Ival.pretty i
-
-(* TODO: why is it useful? Crash if not here, but why? *)
-(* Return the interval over which ranges the smallest typ containing [i]. *)
-let interv_of_typ_containing_interv i =
- try
- let kind = ikind_of_interv i in
- interv_of_typ (TInt(kind, []))
- with Cil.Not_representable ->
- (* infinity *)
- Ival.inject_range None None
-
let interv_of_unknown_block =
(* since we have no idea of the size of this block, we take the largest
possible one which is unfortunately quite large *)
lazy
- (Ival.inject_range (Some Integer.zero) (Some (Bit_utils.max_byte_address ())))
+ (Ival.inject_range
+ (Some Integer.zero)
+ (Some (Bit_utils.max_byte_address ())))
(* imperative environments *)
module Env: sig
@@ -238,8 +205,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 iexp, ieqs, _ = build_ieqs t ieqs [] in
+ let iexp, ieqs = Interval_system.build ~infer t in
(* 2) Solve it:
The problem is probably undecidable in the general case.
Thus we just look for reasonably precise approximations
@@ -325,18 +291,18 @@ and infer_term_lval (host, offset as tlv) =
and infer_term_host h = match h with
| TVar v ->
(try Env.find v
- with Not_found ->
- match v.lv_type with
- | Linteger ->
- Ival.inject_range None None
- | Ctype (TFloat _) -> (* TODO: handle in MR !226 *)
- raise Not_an_integer
- | Lreal ->
- Error.not_yet "real numbers"
- | Ctype _ ->
- interv_of_typ (Logic_utils.logicCType v.lv_type)
- | Ltype _ | Lvar _ | Larrow _ ->
- Options.fatal "unexpected logic type")
+ with Not_found ->
+ match v.lv_type with
+ | Linteger ->
+ Ival.inject_range None None
+ | Ctype (TFloat _) -> (* TODO: handle in MR !226 *)
+ raise Not_an_integer
+ | Lreal ->
+ Error.not_yet "real numbers"
+ | Ctype _ ->
+ interv_of_typ (Logic_utils.logicCType v.lv_type)
+ | Ltype _ | Lvar _ | Larrow _ ->
+ Options.fatal "unexpected logic type")
| TResult ty -> interv_of_typ ty
| TMem t ->
let ty = Logic_utils.logicCType t.term_type in
@@ -347,85 +313,6 @@ and infer_term_host h = match h with
Printer.pp_typ ty
Printer.pp_term t
-(* Build the system of interval equations for the logic function called
- through [t].
- Example: the following function:
- f(Z n) = n < 0 ? 1 : f(n - 1) * f(n - 2) / f(n - 3)
- when called with f(37)
- will generate the following system of equations:
- X = [1; 1] U Y*Y/Y /\
- Y = [1; 1] U Z*Z/Z /\
- Z = [1; 1] U Z*Z/Z
- where X is the interval for f(int) (since 37 \in int),
- Y the one for f(long) (from int-1, int-2 and int-3)
- and Z the for the f(Z) (from long-1, long-2 and long-3) *)
-and build_ieqs t ieqs ivars =
- match t.term_node with
- | Tapp(li, _, args) ->
- if li.l_type = Some Linteger && Misc.is_recursive li then begin
- let args_lty = List.map2
- (fun lv arg ->
- try
- (* speed-up convergence *)
- let i = interv_of_typ_containing_interv (infer arg) in
- Env.add lv i;
- Ctype (TInt(ikind_of_interv i, []))
- with
- | Cil.Not_representable -> Linteger
- | Not_an_integer -> lv.lv_type)
- li.l_profile
- args
- in
- (* x *)
- 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:Interval_system.ival_exp), ieqs, ivars =
- build_ieqs (Misc.term_of_li li) ieqs (ivar :: ivars)
- in
- (* Adding x = g(x) *)
- let ieqs = Interval_system.add_equation ivar iexp ieqs in
- ieqs, ivars
- in
- List.iter (fun lv -> Env.remove lv) li.l_profile;
- 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)
- | TConst _ ->
- (try Interval_system.Iconst(infer t), ieqs, ivars
- with Not_an_integer -> Interval_system.Iunsupported, ieqs, ivars)
- | TLval(TVar _, _) ->
- (try Interval_system.Iconst(infer t), ieqs, ivars
- with Not_an_integer -> Interval_system.Iunsupported, ieqs, ivars)
- | TBinOp (PlusA, t1, t2) ->
- let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
- let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Interval_system.Ibinop(Interval_system.Ival_add, iexp1, iexp2), ieqs, ivars
- | TBinOp (MinusA, t1, t2) ->
- let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
- let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Interval_system.Ibinop(Interval_system.Ival_min, iexp1, iexp2), ieqs, ivars
- | TBinOp (Mult, t1, t2) ->
- let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
- let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Interval_system.Ibinop(Interval_system.Ival_mul, iexp1, iexp2), ieqs, ivars
- | TBinOp (Div, t1, t2) ->
- let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
- let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Interval_system.Ibinop(Interval_system.Ival_div, iexp1, iexp2), ieqs, ivars
- | Tif(_, t1, t2) ->
- let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
- let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Interval_system.Ibinop(Interval_system.Ival_union, iexp1, iexp2), ieqs, ivars
- | _ ->
- Interval_system.Iunsupported, ieqs, ivars
-
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/interval_system.ml b/src/plugins/e-acsl/interval_system.ml
index 32292572679..fe18fccc670 100644
--- a/src/plugins/e-acsl/interval_system.ml
+++ b/src/plugins/e-acsl/interval_system.ml
@@ -65,8 +65,129 @@ type t = ival_exp Ivar.Map.t
(***************************** Solver *************************************)
(**************************************************************************)
-let empty = Ivar.Map.empty
-let add_equation = Ivar.Map.add
+exception Not_an_integer
+
+let rec interv_of_typ ty = match Cil.unrollType ty with
+ | TInt (k,_) as ty ->
+ let n = Cil.bitsSizeOf ty in
+ let l, u =
+ if Cil.isSigned k then Cil.min_signed_number n, Cil.max_signed_number n
+ else Integer.zero, Cil.max_unsigned_number n
+ in
+ Ival.inject_range (Some l) (Some u)
+ | TEnum(enuminfo, _) -> interv_of_typ (TInt (enuminfo.ekind, []))
+ | _ ->
+ raise Not_an_integer
+
+let ikind_of_interv i =
+ if Ival.is_bottom i then IInt
+ else match Ival.min_and_max i with
+ | Some l, Some u ->
+ let is_pos = Integer.ge l Integer.zero in
+ let lkind = Cil.intKindForValue l is_pos in
+ let ukind = Cil.intKindForValue u is_pos in
+ (* kind corresponding to the interval *)
+ let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+ (* convert the kind to [IInt] whenever smaller. *)
+ if Cil.intTypeIncluded kind IInt then IInt else kind
+ | None, None -> raise Cil.Not_representable (* GMP *)
+ | None, Some _ | Some _, None ->
+ Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+
+let interv_of_typ_containing_interv i =
+ try
+ let kind = ikind_of_interv i in
+ interv_of_typ (TInt(kind, []))
+ with Cil.Not_representable ->
+ (* infinity *)
+ Ival.inject_range None None
+
+let ivars_contains_ivar ivars ivar =
+ List.fold_left (fun b ivar' -> b || Ivar.equal ivar ivar') false ivars
+
+(* Build the system of interval equations for the logic function called
+ through [t].
+ Example: the following function:
+ f(Z n) = n < 0 ? 1 : f(n - 1) * f(n - 2) / f(n - 3)
+ when called with f(37)
+ will generate the following system of equations:
+ X = [1; 1] U Y*Y/Y /\
+ Y = [1; 1] U Z*Z/Z /\
+ Z = [1; 1] U Z*Z/Z
+ where X is the interval for f(int) (since 37 \in int),
+ Y the one for f(long) (from int-1, int-2 and int-3)
+ and Z the for the f(Z) (from long-1, long-2 and long-3) *)
+let build ~infer t =
+ let rec aux ieqs ivars t = match t.term_node with
+ | Tapp(li, _, args) ->
+ if li.l_type = Some Linteger && Misc.is_recursive li then begin
+ let args_lty = List.map2
+ (fun lv arg ->
+ try
+ (* speed-up convergence *)
+ let i = interv_of_typ_containing_interv (infer arg) in
+ (* TODO: *)
+(* Env.add lv i;*)
+ Ctype (TInt(ikind_of_interv i, []))
+ with
+ | Cil.Not_representable -> Linteger
+ | Not_an_integer -> lv.lv_type)
+ li.l_profile
+ args
+ in
+ (* x *)
+ let ivar =
+ { 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 ivars_contains_ivar ivars ivar then ieqs, ivars
+ else
+ let (iexp:ival_exp), ieqs, ivars =
+ aux ieqs (ivar :: ivars) (Misc.term_of_li li)
+ in
+ (* Adding x = g(x) *)
+ let ieqs = Ivar.Map.add ivar iexp ieqs in
+ ieqs, ivars
+ in
+(* List.iter (fun lv -> Env.remove lv) li.l_profile;*)
+ Ivar ivar, ieqs, ivars
+ end else
+ (try Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Iunsupported, ieqs, ivars)
+ | TConst _ ->
+ (try Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Iunsupported, ieqs, ivars)
+ | TLval(TVar _, _) ->
+ (try Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Iunsupported, ieqs, ivars)
+ | TBinOp (PlusA, t1, t2) ->
+ let iexp1, ieqs, ivars = aux ieqs ivars t1 in
+ let iexp2, ieqs, ivars = aux ieqs ivars t2 in
+ Ibinop(Ival_add, iexp1, iexp2), ieqs, ivars
+ | TBinOp (MinusA, t1, t2) ->
+ let iexp1, ieqs, ivars = aux ieqs ivars t1 in
+ let iexp2, ieqs, ivars = aux ieqs ivars t2 in
+ Ibinop(Ival_min, iexp1, iexp2), ieqs, ivars
+ | TBinOp (Mult, t1, t2) ->
+ let iexp1, ieqs, ivars = aux ieqs ivars t1 in
+ let iexp2, ieqs, ivars = aux ieqs ivars t2 in
+ Ibinop(Ival_mul, iexp1, iexp2), ieqs, ivars
+ | TBinOp (Div, t1, t2) ->
+ let iexp1, ieqs, ivars = aux ieqs ivars t1 in
+ let iexp2, ieqs, ivars = aux ieqs ivars t2 in
+ Ibinop(Ival_div, iexp1, iexp2), ieqs, ivars
+ | Tif(_, t1, t2) ->
+ let iexp1, ieqs, ivars = aux ieqs ivars t1 in
+ let iexp2, ieqs, ivars = aux ieqs ivars t2 in
+ Ibinop(Ival_union, iexp1, iexp2), ieqs, ivars
+ | _ ->
+ Iunsupported, ieqs, ivars
+ in
+ let iexp, ieqs, _ = aux Ivar.Map.empty [] t in
+ iexp, ieqs
+
(* Normalize the expression.
An expression is said to be normalized if it is:
@@ -87,9 +208,6 @@ let normalize_iexp iexp =
let normalize_ieqs ieqs =
Ivar.Map.map (fun iexp -> normalize_iexp iexp) ieqs
-let ivars_contains_ivar ivars ivar =
- List.fold_left (fun b ivar' -> b || Ivar.equal ivar ivar') false ivars
-
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"
diff --git a/src/plugins/e-acsl/interval_system.mli b/src/plugins/e-acsl/interval_system.mli
index 44a179eaf74..8487d396fc7 100644
--- a/src/plugins/e-acsl/interval_system.mli
+++ b/src/plugins/e-acsl/interval_system.mli
@@ -55,8 +55,7 @@ type t
(*************************** Constructors *********************************)
(**************************************************************************)
-val empty: t
-val add_equation: ivar -> ival_exp -> t -> t
+val build: infer:(term -> Ival.t) -> term -> ival_exp * t
(**************************************************************************)
(***************************** Solver *************************************)
@@ -78,6 +77,9 @@ val solve: t -> ivar -> Integer.t array -> Ival.t
(****************************** Utils *************************************)
(**************************************************************************)
-val ivars_contains_ivar: ivar list -> ivar -> bool
-(** [contains ivars ivar] checks whether the list of Ivar [ivars] contains the
- Ivar [ivar]. *)
+(* the following functions should be defined in [Interval] but are here to break
+ mutual module dependencies *)
+
+exception Not_an_integer
+val interv_of_typ: typ -> Ival.t
+val ikind_of_interv: Ival.t -> Cil_types.ikind
--
GitLab