(*
 *	Copyright (c) 2002 by Laboratoire Spécification et Vérification (LSV),
 *	CNRS UMR 8643 & ENS Cachan.
 *	Written by Jean Goubault-Larrecq.  Not derived from licensed software.
 *
 *	Permission is granted to anyone to use this software for any
 *	purpose on any computer system, and to redistribute it freely,
 *	subject to the following restrictions:
 *
 *	1. Neither the author nor its employer is responsible for the consequences of use of
 *		this software, no matter how awful, even if they arise
 *		from defects in it.
 *
 *	2. The origin of this software must not be misrepresented, either
 *		by explicit claim or by omission.
 *
 *	3. Altered versions must be plainly marked as such, and must not
 *		be misrepresented as being the original software.
 *
 *	4. This software is restricted to non-commercial use only.  Commercial
 *		use is subject to a specific license, obtainable from LSV.
 *)

open Intervalle

exception Zone (* lancee pour retourner top. *)

type zone = Z_NULL (* le pointeur NULL *)
   | Z_GLOBAL of string * itv (* Z_GLOBAL (x, [m, n]): une zone reservee
			       pour la variable globale de nom x,
			       qui s'etend sur un nombre d'octets
			       compris entre m et n. *)
   | Z_HEAP of Control.ppoint (* Z_HEAP (pp): une zone de
				memoire allouee au point de programme pp.
				On ne garde pas sa taille ici. *)
   | Z_STACK of string * itv * string * Control.loc_ppoint option
     (* Z_STACK (x, [m, n], f, pp): une zone de memoire allouee pour
      la variable locale x, s'etendant sur de m a n octets.
      La variable locale x est definie dans la fonction f, qui est
      appelee depuis le point de programme local pp
      (ou None si f est le point d'entree principal main du programme). *)
   | Z_STRING of string (* une zone reservee pour la constante chaine
			 fournie en argument; si n est la longueur de
			 la chaine, le type de cette constante est
			 const unsigned char [n+1]; les ecritures dans
			 cette zone echouent. *)
   | Z_FUN of string (* Z_FUN f: une zone reservee pour le code de la
		      fonction f; on ne sait pas sur combien d'octets
		      ca s'etend; les ecritures dans cette zone echouent. *)

module ZoneTable : Map.S with type key = zone
(*
    type key = zone
    and 'a t
    val empty : 'a t
    val add : key -> 'a -> 'a t -> 'a t
    val find : key -> 'a t -> 'a
    val remove : key -> 'a t -> 'a t
    val mem : key -> 'a t -> bool
    val iter : (key -> 'a -> unit) -> 'a t -> unit
    val map : ('a -> 'b) -> 'a t -> 'b t
    val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
  end
 *)
 			      
type abs_addr = (* une adresse abstraite est en gros une liste de zones
		 possibles.  Comme on peut ajouter n'importe quel entier
		 a un pointeur C, il faudra aussi dire pour chaque zone
		 quels sont les decalages [offsets] possibles de l'adresse
		 par rapport au debut de la zone.
		   En consequence, une adresse abstraite est une table qui
		 a des zones associe des intervalles non vides d'offsets...
		   ou bien None, signifiant un pointeur qui peut aller
		 n'importe ou (top). *)
    itv ZoneTable.t option (* la table zone -> intervalle non vide, ou None. *)

val z_bot : abs_addr (* le bottom du treillis *)
val z_make : zone -> abs_addr (* z_make z calcule l'adresse abstraite qui ne peut pointer
	que vers (le debut de) la zone z. *)
val z_all : itv (* le domaine de variation des offsets en memoire par rapport
	au debut d'une zone: on supposera que c'est celui des entiers du type
	Arith.type_long. *)
val z_top : abs_addr (* le top du treillis *)
val z_union : abs_addr -> abs_addr -> abs_addr (* le sup *)
val z_widen : abs_addr -> abs_addr -> abs_addr (* l'elargissement *)
val z_equal : abs_addr -> abs_addr -> bool (* l'egalite dans le treillis *)
val itv_sizeof : Cparse.q_ctype -> itv (* calcule l'intervalle des tailles
	possibles du type; en general, il n'y a qu'une taille possible,  sauf
	par exemple pour un type toto[] (pas de borne de tableau) ou pour
	un type de fonction. *)
val z_array : string -> Control.loc_ppoint option -> Cparse.q_ctype -> Control.var -> abs_addr
	(* z_array f ctx qtyp a
	calcule l'adresse abstraite du tableau local a de type qtyp,
	telle qu'il est declare dans la fonction f, appelee dans le contexte ctx.
	(qtyp est toujours de la forme TARRAY (...).) *)
val z_fun : string -> abs_addr
	(* z_fun f
	calcule l'adresse abstraite de la fonction f. *)
val z_addr_var : string -> Control.loc_ppoint option -> Cparse.q_ctype -> Control.var -> abs_addr
	(* z_var f ctx qtyp x
	calcule l'adresse abstraite de la variable x de type qtyp,
	telle qu'elle est declaree dans la fonction f, appelee dans le contexte ctx. *)
val z_extent : Cparse.q_ctype -> itv
	(* calcule l'intervalle [0, n-1] ou n est la taille maximale
	du type en argument; si la taille est inconnue, retourne [0, maxint],
	ou maxint les plus grand entier du type TLONG (Arith.type_long). *)
val z_extent_var : string -> Control.loc_ppoint option -> Cparse.q_ctype -> Control.var -> abs_addr
	(* idem, a part qu'il calcule toutes les adresses abstraites qui
	pointent a l'interieur de la variable x; par exemple, si x est d'un
	type de 4 octets de long, alors ce seront toutes les adresses &x, ..., &x+3. *)
val z_cst : string -> abs_addr (* calcule l'adresse abstraite d'une chaine constante *)
val z_add_addr : abs_addr -> itv -> abs_addr
	(* z_add_addr ad i
	additionne un entier (dans l'intervalle i) a
	l'adresse abstraite ad.   Ceci peut donner des adresses en-dehors
	des zones stockees dans ad; la gestion des debordements sera
	effectuee par z_check_bounds et z_purify plus bas. *)
val z_addr_index : Cparse.q_ctype -> abs_addr -> itv -> abs_addr
	(* z_addr_index qtyp a i
	calcule l'adresse de a[i], sachant que a
	est un pointeur vers des objets de type qtyp.
	(On rappelle que &a[i] est i*sizeof(qtyp) octets apres &a[0].) *)
val z_anti_addr_index : Cparse.q_ctype -> abs_addr -> abs_addr -> itv
	(* z_anti_addr_index qtyp a a'
	calcule l'intervalle possible (de type long)
	de la difference a-a', ou a et a' sont deux pointeurs sur qtyp.
	La difference d'adresse entre deux zones (concretes) differentes
	est supposee arbitraire. *)
val z_addr_sel : int -> abs_addr -> abs_addr
	(* z_addr_sel offset a
	calcule l'adresse d'un champ, disons f, dans une
	structure ou une union a l'adresse a; l'offset de f est offset. *)
val z_convert_int : itv -> abs_addr
	(* z_convert itv calcule une adresse absolue comprise entre les
	entiers donnes (l'adresse n etant traduite en l'offset n a
	partir de Z_NULL) *)
val z_int_convert : Arith.int_type -> abs_addr -> itv
	(* z_int_convert it a convert l'adresse abstraite a en un entier
	decrit par le type it.  Toute zone Z_NULL+offset est traduite
	en offset, les autres adresses sont converties en des entiers
	quelconques. *)
val z_addr_le : abs_addr -> abs_addr -> itv
	(* z_addr_le a a' retourne 1 ou 0 selon que a<=a' ou pas. *)
val z_addr_lt : abs_addr -> abs_addr -> itv
	(* z_addr_le a a' retourne 1 ou 0 selon que a<a' ou pas. *)
val z_addr_eq : abs_addr -> abs_addr -> itv
	(* z_addr_le a a' retourne 1 ou 0 selon que a==a' ou pas.
	Attention: cette fonction n'a rien a voir avec z_equal! *)

type heap_size_info = (Control.ppoint, itv) Hashtbl.t

val z_check_bounds : bool -> heap_size_info -> abs_addr -> bool
(* z_check_bounds write heapsizes a
 retourne true s'il est possible qu'en ecrivant
 (lorsque write=true) ou en lisant (lorsque write=false) dans
 la zone memoire decrite par a, on ecrive soit dans des zones interdites
 a l'ecriture (Z_NULL, Z_STRING, Z_FUN), soit on tape en dehors des bornes
 specifiees pour les zones.
 La table de hash heapsizes donne les tailles possibles allouees
 par chaque point de programme qui alloue un Z_HEAP. *)

val z_purify : heap_size_info -> abs_addr -> abs_addr
(* z_purify heapsizes a
 retourne une adresse abstraite a' correspondant aux
 adresses concretes representees par a dans lesquelles on peut ecrire.
 En somme, z_purify a est la plus grande adresse abstraite a' incluse
 dans a telle que z_check_bounds a'=false.
 ... a une exception pres: on prendra z_purify None = None.
	Pour heapsizes, cf. le commentaire de z_check_bounds. *)

val z_functions : abs_addr -> string list * bool
(* z_functions a retourne la liste des fonctions vers lesquelles
 peut pointer a, plus un booleen qui est true si et seulement
 si a peut pointer sur autre chose---incluant des pointeurs
 vers une fonction mais pas au debut du code.
 ... a une exception pres: on supposera que z_functions None=[], true. *)