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

(* talctxt.ml
 * Contexts for verification of TAL kinds, type constructors, and terms.
 *
 *)

open Numtypes;;
open Identifier;;
open Tal;;

(*** Locations ***)

type tal_loc =
    Loctop 
  | Loccon of identifier   (* Imported/Exported type label *)
  | Locval of identifier   (* Imported/Exported value label *)
  | Loccb of identifier    (* Con block l *)
  | Locc of identifier*int (* Code block l instruction i *)
  | Locd of identifier*int (* Data block l item i *)
;;

(*** Verification Errors *)

type verify_error =
    Undefined_label of identifier
  | Undefined_var of identifier
  | Undefined_reg of reg
  | Redefined_label of identifier
  | Kindleq of kind*kind
  | Kindeq of kind*kind
  | Kindmeet of kind*kind
  | Kindjoin of kind*kind
  | Conwf of con*string
  | Neqcon of con*con
  | Nleqcon of con*con
  | Rsnleq of reg*register_state*register_state
  | Conmeet of con*con
  | Conjoin of con*con
  | Rsmeet of register_state*register_state
  | Rsjoin of register_state*register_state
  | BadUnroll of con  (* con is not unrollable *)
  | Unknown_size of con
  | Bad_offset of int32 (* -n means n bytes before a field/slot
                           +n means n bytes after last valid field/slot *)
  | Bad_depth of int
  | Not_tail of con*con
  | Readonly
  | Stack_write_alignment
  | Coercion of con*string*coercion
  | No_stack_type
  | Genop of string*genop
  | Both_mem of genop*genop
  | Inst_form of string
  | Data_form of string
  | Fallsthru
  | Cyclic_imports of int_ref
  | Doesnt_export
  | Ndisjoint_exports of identifier
  | Multiple_exports
  | Con_def_nleq
  | Intt_nleq of string
  | Label_requires_type of identifier
  | Fallsthru_unlabelled
  | Backward_branch of identifier
  | Undefined_tla
;;

exception Talfail;;   (* The verifier could not recover from errors *)

(* stuff that changes infrequently *)
type ctxt0 = 
    { ge : ctxt -> verify_error -> unit;
      (* ctxt |- l : k  -- for constructor labels *)
      cheap : (identifier,kind) Dict.dict;
      (* ctxt |- l : c  -- for value labels *)
      vheap : (identifier,con option) Dict.dict;
      (* ctxt |- l = c : k -- for transparent constructor labels *)
      lenv : (identifier,int_con_def) Dict.dict
    } 
and ctxt = {
    ctxt0 : ctxt0;
    loc : tal_loc;
    vc : string;
    (* ctxt |- a : k  -- for constructor variables *)
    delta : (identifier,kind) Dict.dict;
    (* ctxt |- r : c *)
    gamma : register_state;
    (* Abbreviations *)
    abbrevs : (identifier,con) Dict.dict
  }
;;

(* A context is well formed if:
 *   con is well formed
 *   All l in Dom(psi):    con.labs |- psi(l) : Ktype
 *   All a in Dom(kappa):  con      |- kappa(a) : k
 *   All l in Dom(lenv):   con.labs |- lenv(l) : k
 *   All r in Dom(gamma):  con      |- gamma(r) : K4byte
 *
 * NOTE: The tal terms which contain constructors may have free variables
 *       in them.  These free variables belong to Dom(srcdelta) and
 *       Dom(srcdelta) is disjoint from Dom(delta).  Dom(kappa) is a subset
 *       of Dom(srcdelta).  Thus, before finding the kind of a constructor
 *       in a tal term, apply the substitution kappa to map variables in
 *       Dom(srcdelta) to Dom(delta). 
 *)

exception Talverify of ctxt * verify_error;;
exception Talfail;;

let empty_ctxt0 =
  { ge=(fun ctxt ve -> raise (Talverify (ctxt,ve)));
    cheap=Dict.empty id_compare; 
    vheap=Dict.empty id_compare;
    lenv=Dict.empty id_compare
  }
let empty_ctxt =
  { ctxt0=empty_ctxt0;
    loc=Loctop; 
    vc=""; 
    delta=Dict.empty id_compare; 
    gamma=rs_empty;
    abbrevs=Dict.empty id_compare
  }
;;

let get_loc ctxt = ctxt.loc;;
let get_verify_ctxt ctxt = ctxt.vc;;
let generate_error ctxt ve = ctxt.ctxt0.ge ctxt ve;;
let get_var_map ctxt = ctxt.delta

let get_label_kind ctxt l =
  try 
    Dict.lookup ctxt.ctxt0.cheap l
  with Dict.Absent -> generate_error ctxt (Undefined_label l); k4byte
;;

let get_variable_kind ctxt v =
  try Dict.lookup ctxt.delta v
  with Dict.Absent -> generate_error ctxt (Undefined_var v); k4byte
;;

let get_abbrevs ctxt = ctxt.abbrevs;;

let get_label_def ctxt l =
  try Dict.lookup ctxt.ctxt0.lenv l
  with Dict.Absent -> generate_error ctxt (Undefined_label l); AbsCon
;;

let get_label_con ctxt l =
  try
    (match Dict.lookup ctxt.ctxt0.vheap l with
      Some c -> c
    | None -> generate_error ctxt (Label_requires_type l); chptr [] None)
  with Dict.Absent ->
    generate_error ctxt (Undefined_label l); chptr [] None
;;

let get_label_con_opt ctxt l =
  try Dict.lookup ctxt.ctxt0.vheap l
  with Dict.Absent ->
    generate_error ctxt (Undefined_label l); Some(chptr [] None)
;;

let get_reg_con ctxt r =
  try rs_get_reg ctxt.gamma r
  with Dict.Absent -> generate_error ctxt (Undefined_reg r); cbyte4
;;

let get_register_state ctxt = ctxt.gamma;;

let get_tla_con ctxt =
  match rs_get_tla ctxt.gamma with
    None -> generate_error ctxt (Undefined_tla); cbyte4
  | Some c -> c
;;

let get_cc ctxt = rs_get_cc ctxt.gamma;;

let set_loc ctxt loc =
  { ctxt0=ctxt.ctxt0; loc=loc; vc=ctxt.vc; delta=ctxt.delta; gamma=ctxt.gamma;
    abbrevs=ctxt.abbrevs }
;;

let set_verify_ctxt ctxt vc =
  { ctxt0=ctxt.ctxt0; loc=ctxt.loc; vc=vc; delta=ctxt.delta; gamma=ctxt.gamma;
    abbrevs=ctxt.abbrevs }
;;

let error_handler ctxt ge =
  let ctxt0 = ctxt.ctxt0 in
  { ctxt0 = { ge=ge; cheap=ctxt0.cheap; vheap=ctxt0.vheap; lenv=ctxt0.lenv };
    loc=ctxt.loc; vc=ctxt.vc; delta=ctxt.delta; gamma=ctxt.gamma;
    abbrevs=ctxt.abbrevs
  }
;;

let add_con ctxt l k =
  let ctxt0 = ctxt.ctxt0 in
  if Dict.member ctxt0.cheap l then generate_error ctxt (Redefined_label l);
  let cheap = Dict.insert ctxt0.cheap l k in
  { ctxt0 = { ge=ctxt0.ge; cheap=cheap; vheap=ctxt0.vheap; lenv=ctxt0.lenv };
    loc=ctxt.loc; vc=ctxt.vc; delta=ctxt.delta; gamma=ctxt.gamma;
    abbrevs=ctxt.abbrevs
  }
;;

let add_con_def ctxt l cd =
  let ctxt0 = ctxt.ctxt0 in
  let lenv = Dict.insert ctxt0.lenv l cd in
  { ctxt0 = { ge=ctxt0.ge; cheap=ctxt0.cheap; vheap=ctxt0.vheap; lenv=lenv };
    loc=ctxt.loc; vc=ctxt.vc; delta=ctxt.delta; gamma=ctxt.gamma;
    abbrevs=ctxt.abbrevs
  }
;;

let add_var ctxt v k =
  let delta = Dict.insert ctxt.delta v k in
  let abbrevs = Dict.delete ctxt.abbrevs v in
  { ctxt0=ctxt.ctxt0; loc=ctxt.loc; vc=ctxt.vc; delta=delta; gamma=ctxt.gamma;
    abbrevs=abbrevs }
;;

let set_abbrevs ctxt abbrevs =
  { ctxt0=ctxt.ctxt0; loc=ctxt.loc; vc=ctxt.vc; delta=Dict.empty id_compare;
    gamma=ctxt.gamma; abbrevs=abbrevs }
;;

let add_abbrev ctxt v c =
  let delta = Dict.delete ctxt.delta v in
  let abbrevs = Dict.insert ctxt.abbrevs v c in
  { ctxt0=ctxt.ctxt0; loc=ctxt.loc; vc=ctxt.vc; delta=delta; gamma=ctxt.gamma;
    abbrevs=abbrevs }
;;

let add_val ctxt l c =
  let ctxt0 = ctxt.ctxt0 in
  if Dict.member ctxt0.vheap l then generate_error ctxt (Redefined_label l);
  let vheap = Dict.insert ctxt0.vheap l c in
  { ctxt0 = { ge=ctxt0.ge; cheap=ctxt0.cheap; vheap=vheap; lenv=ctxt0.lenv };
    loc=ctxt.loc; vc=ctxt.vc; delta=ctxt.delta; gamma=ctxt.gamma;
    abbrevs=ctxt.abbrevs
  }
;;

let set_val ctxt l c =
  let ctxt0 = ctxt.ctxt0 in
  let vheap = Dict.insert ctxt0.vheap l c in
  { ctxt0 = { ge=ctxt0.ge; cheap=ctxt0.cheap; vheap=vheap; lenv=ctxt0.lenv };
    loc=ctxt.loc; vc=ctxt.vc; delta=ctxt.delta; gamma=ctxt.gamma;
    abbrevs=ctxt.abbrevs
  }
;;

let add_reg ctxt r c =
  let gamma = rs_set_reg ctxt.gamma r c in
  { ctxt0=ctxt.ctxt0; loc=ctxt.loc; vc=ctxt.vc; delta=ctxt.delta; gamma=gamma;
    abbrevs=ctxt.abbrevs }
;;

let set_register_state ctxt gamma =
  { ctxt0=ctxt.ctxt0; loc=ctxt.loc; vc=ctxt.vc; delta=ctxt.delta; gamma=gamma;
    abbrevs=ctxt.abbrevs }
;;

let set_tla_con ctxt c = { ctxt with gamma=rs_set_tla ctxt.gamma c };;
let set_cc ctxt cc = { ctxt with gamma=rs_set_cc ctxt.gamma cc };;
let restore_cc ctxt = rs_restore_cc ctxt.gamma;;

(* Cyclone *)
(* This REDEFINES the same-named functions from Tal; maybe not a good idea.
   There should probably be a special verify_error for Cyclone errors.
   We should check that the variance is always ReadWrite. *)
let get_cyclone_field ctxt =
  try
    match get_cyclone_field ctxt.gamma with
      None -> generate_error ctxt (Undefined_tla); None
    | Some(c,v) -> Some(c,v)
  with Failure _ -> generate_error ctxt (Undefined_tla); None
let set_cyclone_field ctxt c v =
  try
    set_register_state ctxt
      (Tal.set_cyclone_field ctxt.gamma c v)
  with Failure _ -> generate_error ctxt (Undefined_tla); ctxt
let get_cyclone_con ctxt =
  try
    match get_cyclone_field ctxt with
      None -> generate_error ctxt (Undefined_tla); cbyte4
    | Some(c,v) -> c
  with Failure _ -> generate_error ctxt (Undefined_tla); cbyte4
let set_cyclone_con ctxt c =
  set_cyclone_field ctxt c ReadWrite
(* End Cyclone *)

(* EOF: talctxt.ml *)
