(*
 *	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 Control
open Cparse
open Sigs
open Zones
open Intervalle

type abs_value = ITV_INT of itv (* un intervalle entier *)
    | ITV_FLOAT of (itv * bool) (* un intervalle reel, plus un booleen disant
				 si on trouve aussi des choses qui ne sont pas
				 des nombres dans les valeurs possibles (des "NaN"). *)
    | ABS_ADDR of abs_addr (* une zone d'adresses memoire abstraites. *)

module AbsEnv : Map.S with type key = string

(*
module AbsEnv :
  sig
    type key = string
    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_env = abs_value AbsEnv.t (* : var-globale --> abs_value *)
    * abs_value AbsEnv.t (* : var-locale --> abs_value *)
    (* Note: si la variable x n'est envoyee vers rien par abs_env,
     c'est qu'elle vaut le top de son type (itv_int_top qtyp
     si qtyp est entier, itv_float_top qtyp si qtyp est flottant,
     z_top si pointeur). *)

val av_union : abs_value -> abs_value -> abs_value
val av_widen : q_ctype -> abs_value -> abs_value -> abs_value
	(* effectue un elargissement sur deux valeurs abstraites de type donne
	en premier argument. *)

val av_equal : abs_value -> abs_value -> bool
val av_top : q_ctype -> abs_value
val ae_union_1 : abs_value AbsEnv.t -> abs_value AbsEnv.t -> abs_value AbsEnv.t
val ae_union : abs_env -> abs_env -> abs_env
val ae_widen : (var, q_ctype) Hashtbl.t -> abs_env -> abs_env -> abs_env
	(* effectue un elargissement sur deux environnements abstraits;
	on donne l'environnement de typage (statique) en premier argument. *)
val ae_equal : abs_env -> abs_env -> bool

type abs_effect = abs_env * abs_addr * sig_set
    (* l'effet d'une instruction, c'est de retourner:
     - un nouvel environnement envoyant les variables globales/locales
     vers leurs valeurs possibles,
     - une adresse abstraite recouvrant toutes les adresses possibles qui
     ont ete ecrites par l'instruction,
     - un ensemble de signaux possibles lances par l'execution de cette instruction
     ([i1, ..., ik] represente l'ensemble {i1, ..., ik}, [0, ..., nsignals-1] = tous les signaux
     possibles).
     *)

val ae_assign : string -> loc_ppoint option -> abs_env ->
  var -> abs_value -> q_ctype -> abs_effect
	(* ae_assign func ctx ae x v qtyp
	effectue l'affectation de la variable x a la valeur abstraite v de type qtyp
	dans l'environnement ae; le nom de la fonction courante est func et son
	contexte d'appel est ctx. *)
val ae_value : abs_env -> var -> q_ctype -> abs_value
	(* ae_value ae x qtyp recupere la valeur abstraite de x dans
	l'environnement ae; x est de type qtyp. *)

val ae_set_array :  string -> loc_ppoint option -> abs_env ->
  var -> var -> q_ctype -> abs_effect
	(* ae_set_array func ctx ae x a qtyp
	effectue x:=a : qtyp etc., ou a est un nom de tableau;
	ceci met simplement l'adresse de a dans x. *)
val ae_set_fun : string -> loc_ppoint option -> abs_env ->
  var -> string -> q_ctype -> abs_effect
	(* ae_set_fun func ctx ae x f qtyp
	effectue x:=f : qtyp etc., ou f est un nom de fonction;
	ceci met simplement l'adresse de f dans x. *)
val ae_set_cst : string -> loc_ppoint option -> abs_env ->
  var -> constant_val -> q_ctype -> abs_effect
	(* ae_set_cst func ctx ae x cst qtyp
	effectue x:=cst : qtyp. *)
val ae_wipe : string -> loc_ppoint option -> abs_env -> abs_addr -> abs_env
	(* ae_wipe func ctx ae a
	calcule l'environnement obtenu a partir de ae en supprimant toutes
	les entrees de variables qui peuvent changer de valeur lorsqu'on ecrit
	a l'adresse a; autrement dit, on met ces variables possiblement modifiees
	a top.  Comme ci-dessus, func est la fonction courante, et ctx le contexte
	d'appel. *)
val ae_copy : heap_size_info -> string -> loc_ppoint option ->
	abs_env -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_copy heapsizes func ctx ae xval yval qtyp
	effectue *xval:=*yval : qtyp;
	noter que si la lecture est interdite dans yval ou l'ecriture est
	interdite dans xval, alors le signal sig_segv est lance (utiliser
	Zones.z_check_bounds). *)
val ae_ptr : heap_size_info -> string -> loc_ppoint option ->
	abs_env -> var -> abs_value -> q_ctype -> q_ctype -> abs_effect
	(* ae_ptr heapsizes func ctx ae x yval qtypy qtypx
	effectue x:=*yval, ou x:qtypx et yval:qtypy;
	noter que ceci lance le signal sig_segv si la lecture est interdite dans yval. *)
val ae_set_ptr : heap_size_info -> string -> loc_ppoint option ->
	abs_env -> abs_value -> abs_value -> q_ctype -> q_ctype -> abs_effect
	(* ae_set_ptr func ctx ae xval yval qtypx qtypy
	effectue *xval:=yval, ou xval:qtypx, yval:qtypy;
	ceci lance le signal sig_segv si l'ecriture est interdite dans xval. *)
val ae_addr_var : string -> loc_ppoint option -> abs_env ->
  var -> var -> q_ctype -> abs_effect
	(* ae_addr_var func ctx ae x y qtyp
	effectue x:=&y, ou y:qtyp. *)
val ae_addr_index : string -> loc_ppoint option -> abs_env ->
  var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_addr_index func ctx ae x yval zval qtyp
	effectue x:=&yval[zval], ou x et yval sont de type pointeur vers qtyp;
	noter que ceci ne lance jamais aucun signal. *)
val ae_anti_addr_index : string -> loc_ppoint option -> abs_env ->
  var -> abs_value -> abs_value -> q_ctype -> abs_effect
	(* ae_anti_addr_index func ctx ae x yval zval qtyp
	effectue x:=yval-zval, ou yval et zval sont de type pointeur vers qtyp;
	ceci ne lance jamais aucun signal. *)
val ae_addr_sel : string -> loc_ppoint option -> abs_env ->
  var -> abs_value -> string -> int -> q_ctype -> q_ctype -> abs_effect
	(* ae_addr_sel func ctx ae x yval f offset qtypy qtypx
	calcule x:=&yval->f, ou yval:qtypy, x:qtypx;
	ceci ne lance jamais aucun signal. *)
val ae_convert : string -> loc_ppoint option -> abs_env ->
  var -> q_ctype -> q_ctype -> abs_value -> abs_effect
	(* ae_convert func ctx ae x qtypx qtypy yval
	calcule x:=(qtypx)yval [conversion, pas cast, cf. I_CONVERT dans control.ml],
	ou yval : qtypy;
	ceci ne lance jamais aucun signal. *)
val ae_cast : string -> loc_ppoint option -> abs_env ->
  var -> q_ctype -> q_ctype -> abs_value -> abs_effect
	(* ae_cast func ctx ae x qtypx qtypy yval
	calcule x:=(qtypx)yval [cast, pas conversion, cf. I_CAST dans control.ml],
	ou yval : qtypy;
	ceci ne lance jamais aucun signal. *)