(**********************************************************************)
(* (c) Greg Morrisett, Neal Glew, David Walker,                       *)
(*     June 1998, all rights reserved.                                *)
(**********************************************************************)

(* talverify.mli
 * TAL Verifier
 *
 * Checks operands, instructions, interfaces, and implementations for well
 * formedness.
 *)

open Utilities;;
open Identifier;;
open Tal;;
open Talctxt;;

(* Coercions *)
val coercion_con : ctxt -> coercion -> con -> con
val coerce_con : (ctxt -> 'a -> con) -> ctxt -> 'a * coercion list -> con

(* Operands *)
val current_stack_con : ctxt -> con
val valid_stack_con : ctxt -> con -> con -> con
val coerce_reg_con : ctxt -> reg coerce -> con
val coerce_label_con : ctxt -> identifier coerce -> con
val genop_con : bool -> ctxt -> genop -> con
val coerce_genop_con : bool -> ctxt -> genop coerce -> con
val genop_write_at : ctxt -> genop -> con -> ctxt
val valid_binops : ctxt -> genop -> genop -> unit
val valid_cbinops : ctxt -> genop -> genop coerce -> unit

(* Instructions & Code Blocks *)
exception Terminal_Jmp
exception Fall_Thru of ctxt * con list
(* verify_instr add_block ctxt instr 
 *   Returns the context ctxt' that is the strongest post-condition
 *   of the instruction instr under the pre-condition context ctxt.
 *   The function add_block is called with the appropriate context
 *   and label, if the instruction jumps to a label that does not
 *   have a type.  This can be used to manage a work-list of blocks
 *   that need to be verified later (see verify_code_tree).  If the
 *   instruction is a terminal jump then there is no resulting post-
 *   condition, so the exception Terminal_Jmp is raised.  Similarly,
 *   if the instruction is a "Fallthru" to the next block, the 
 *   exception Fall_Thru is raised with the current context and
 *   the instantiation of the next block's constructor variables.
 *)
val verify_instr : (ctxt -> identifier -> unit) -> ctxt -> instruction -> ctxt
val add_code_labels : ctxt -> code_block vector -> ctxt
(* verify_code_tree label_map cbv ctxt i
 *   Verifies the tree of code blocks starting at index i.  The label at
 *   index i must have a type on it.  All blocks without a label that are
 *   reached by forward branches are also verified.  The label_map is used
 *   to find code blocks in cbv and to verify that branches to untyped
 *   labels are forward branches only.
 *)  
val verify_code_tree :
    (identifier,int) Dict.dict -> code_block vector -> ctxt -> int
(* Cyclone *)
      -> (con option) option
(* End Cyclone *)
        -> unit
val verify_code_blocks : ctxt -> code_block vector
(* Cyclone *)
      -> (con option) option
(* End Cyclone *)
        -> unit
val add_data_labels : ctxt -> data_block vector -> ctxt
val verify_data_block : ctxt -> data_block -> con
val verify_data_blocks : ctxt -> data_block vector -> unit

(* Compilation Units *)
type ref2int = int_ref -> tal_int
val process_impexps :
    ref2int -> int_ref vector -> ((identifier,con) Dict.dict * tal_int) vector
val verify_imp : ref2int -> ctxt -> tal_imp -> tal_int_type * tal_int_type

(* EOF: talverify.mli *)
