Commit e0f31eb5 by Julien Signoles

### [Interval_system] drastic simplification of its API

parent c8f85d9f
 ... ... @@ -192,38 +192,7 @@ let rec infer t = (* TODO: should not be necessary to distinguish the recursive case. Stack overflow if not distingued *) if Misc.is_recursive li then (* 1) Build a system of interval equations that constrain the solution: do so by returning a variable when encoutering a call of a recursive function instead of performing the usual interval inference. BEWARE: we might be tempted to memoize the solution for a given function signature HOWEVER: it cannot be done in a straightforward manner due to the cases of functions that use C (global) variables in their definition (as the values of those variables can change between two function calls). TODO: I do not understand the remark above. The interval of a C global variable is computed from its type. *) 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 without being too computationally expensive: simply iterate over a finite set of pre-defined intervals. See [Interval_system_solver.solve] for details. *) let chain_of_ivalmax = [| Integer.one; Integer.billion_one; Integer.max_int64 |] (* This set can be changed based on experimental evidences, but it works fine for now. *) in 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 Interval_system.build_and_solve ~infer t else begin (* non-recursive case *) (* add the arguments to the context *) List.iter2 ... ...
 ... ... @@ -59,8 +59,6 @@ module Ivar = let hash iv = Datatype.String.hash iv.iv_name + 7 * LT_List.hash iv.iv_types end) type t = ival_exp Ivar.Map.t (**************************************************************************) (***************************** Solver *************************************) (**************************************************************************) ... ... @@ -184,8 +182,7 @@ let build ~infer t = | _ -> Iunsupported, ieqs, ivars in let iexp, ieqs, _ = aux Ivar.Map.empty [] t in iexp, ieqs aux Ivar.Map.empty [] t (* Normalize the expression. ... ... @@ -331,3 +328,31 @@ let solve ieqs ivar chain_of_ivalmax = iterate_till_post_fixpoint ieqs bottom chain_of_ivalmax in get_ival_of_iconst ivar post_fixpoint let build_and_solve ~infer t = (* 1) Build a system of interval equations that constrain the solution: do so by returning a variable when encoutering a call of a recursive function instead of performing the usual interval inference. BEWARE: we might be tempted to memoize the solution for a given function signature HOWEVER: it cannot be done in a straightforward manner due to the cases of functions that use C (global) variables in their definition (as the values of those variables can change between two function calls). TODO: I do not understand the remark above. The interval of a C global variable is computed from its type. *) let iexp, ieqs, _ = build ~infer t in (* 2) Solve it: The problem is probably undecidable in the general case. Thus we just look for reasonably precise approximations without being too computationally expensive: simply iterate over a finite set of pre-defined intervals. See [Interval_system_solver.solve] for details. *) let chain_of_ivalmax = [| Integer.one; Integer.billion_one; Integer.max_int64 |] (* This set can be changed based on experimental evidences, but it works fine for now. *) in match iexp with | Ivar ivar -> solve ieqs ivar chain_of_ivalmax | Iconst _ | Ibinop _ | Iunsupported -> assert false
 ... ... @@ -22,64 +22,17 @@ open Cil_types (** Fixpoint equation solver for infering intervals of recursively defined logic functions *) (** Fixpoint equation solver for infering intervals of recursively defined logic functions. *) (**************************************************************************) (******************************* 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 ivar | Ibinop of ival_binop * ival_exp * ival_exp | Iunsupported type t (** type of systems of equations over [ival_exp] expressions in which the variables to be found are the [Ivar] constructs. [Equations.t] can be viewed as a fixpoint equation in the sense that the left-hand side of the equation MUST be an [Ivar]: solving the system [(S): x1=f1(x1, ..., xn) /\ ... /\ xn=fn(x1, ..., xn)] is equivalent to solving the fixpoint equation [(E): X=F(X)] where X=(x1, ..., xn) and F=(f1, ..., fn). *) (**************************************************************************) (*************************** Constructors *********************************) (**************************************************************************) val build: infer:(term -> Ival.t) -> term -> ival_exp * t (**************************************************************************) (***************************** Solver *************************************) (**************************************************************************) 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. For chain=[n1; n2; ...; nk] where n1 < ... < nk, [solve] will consider the following set S of intervals as potential solution: S={[-n1, n1], [-n2, n2]... [-nk; nk]}. Then [solve] will iteratively affect intervals from S to the different variables of [ieqs], starting from the smallest interval [-n1, n1] to the biggest one [-nk, nk], until finding the smallest combination that satisfies [ieqs]. If no combination is found then [solve] returns Z. *) (**************************************************************************) (****************************** Utils *************************************) (**************************************************************************) val build_and_solve: infer:(term -> Ival.t) -> term -> Ival.t (** @return the interval of the given term denoting a recursive function. *) (* the following functions should be defined in [Interval] but are here to break mutual module dependencies *) (*/*) (** 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 (*/*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!