equation.mli

(** Representing equation system *)

(* This file is part of the Interproc analyzer, released under GPL license.
   Please read the COPYING file packaged in the distribution.

   Copyright (C) Mathias Argoud, Gaël Lalire, Bertrand Jeannet 2007.
*)

(*  ********************************************************************* *)
(** {2 Hypergraphs} *)
(*  ********************************************************************* *)

(** Comparison for polymorhic sets and graphs *)
val compare_point : Spl_syn.point -> Spl_syn.point -> int


(** A variable in an equation = a control point *)
type vertex = Spl_syn.point
val vertex_dummy : vertex

(** A function in an equation: identified by an integer *)
type hedge = int
val hedge_dummy : hedge

(** Creation of hypergraphs representing equation systems. Vertex identifiers
  are control points, (Hyper)edge identifiers are just integers. An hyperedge
  [([|x1;x2|],i,[|y|])] represents an inequation [y >= f_i(x1,x2)] where [f_i]
  is the function associated to the hyperedge identifier [i]. *)

val create : int -> 'c -> (vertex,hedge,'a,'b,'c) PSHGraph.t

(*  ********************************************************************* *)
(** {2 Preprocessed information} *)
(*  ********************************************************************* *)

(** Useful information associated to a procedure *)
type procinfo = {
  pname : string;        (** Procedure name *)
  pstart: Spl_syn.point; (** Procedure start point *)
  pexit: Spl_syn.point;  (** Procedure exit point *)
  pinput: Apron.Var.t array;  (** Array of input variables *)
  poutput: Apron.Var.t array; (** Array of output variables *)
  plocal: Apron.Var.t array;  (** Array of other variables *)
  penv: Apron.Environment.t;  (** Environment of the procedure *)
  poutput_tmp: Apron.Var.t array; (** Array of renamed output variables *)
}

(** Useful information for the program *)
type info = {
  procinfo : (string, procinfo) Hashhe.t;
    (** Hashtable [procedure name -> procinfo].
	Main procedure has empty name *)
  callret : (Spl_syn.point,Spl_syn.point) DHashhe.t;
    (** Two-way association call points/return points generated by procedure
      calls. *)
  pointenv : (Spl_syn.point,Apron.Environment.t) Hashhe.t;
    (** Hashtable [point -> environment of the enclosing procedure]. *)
  mutable counter : int;
    (** Last free hyperedge identifier (used by [add_equation]). *)
}

(*  ********************************************************************* *)
(** {2 Equation system} *)
(*  ********************************************************************* *)

(** A variable in an equation = a control point *)
type var = Spl_syn.point

(** Information associated to hyperedges/functions used in equations *)
type transfer =
  | Lassign of Apron.Var.t * Apron.Linexpr1.t
      (** Assignement by a linear expression *)
  | Tassign of Apron.Var.t * Apron.Texpr1.t
      (** Assignement by a tree expression *)
  | Condition of Apron.Tcons1.earray Boolexpr.t
      (** Filtering of a predicate by a Boolean expression *)
  | Call of procinfo * procinfo * (Apron.Var.t array) * (Apron.Var.t array)
      (** Procedure call, of the form
	[Call(callerinfo,calleeinfo,actual input parameters,actual output parameters)] *)
  | Return of procinfo * procinfo * (Apron.Var.t array) * (Apron.Var.t array)
      (** Procedure return, of the form
	[Call(callerinfo,calleeinfo,actual input parameters,actual output parameters)] *)

(** Equation system, represented by a graph, where vertex identifiers are
control point, and hyperedge identifiers are integers, with which are
associated objects of type [transfer]. Global information associated with the
graph is of type [info]. *)
type graph = (vertex,hedge,unit,transfer,info) PSHGraph.t

(*  ********************************************************************* *)
(** {2 Functions} *)
(*  ********************************************************************* *)

val add_equation : graph -> var array -> transfer -> var -> unit
  (** [add_equation graph [|x1;x2|] transfer y] adds the inequation [y >=
    transfer(x1,x2)] to the equation graph. In practice, the array is of size 1
    or 2. *)

(*  ===================================================================== *)
(** {3 Printing functions} *)
(*  ===================================================================== *)

val print_procinfo :Format.formatter -> procinfo -> unit
val print_info : Format.formatter -> info -> unit
val print_transfer : Format.formatter -> transfer -> unit