(**********************************************************************)
(* (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 Numtypes;;
open Identifier;;
open Tal;;
open Talctxt;;
open Talcon;;

(* Some types used by the verifier *)
let whcon rc = { rcon=rc; isnorm=false; freevars=None };;
let prcon rc = { rcon=rc; isnorm=true;
                 freevars=Some(Set.empty id_compare) };;
let tag_cons =
  Array.init 20 (fun i -> prcon (Csing (pcint (int_to_int32 i))))
;;

(************************************************************************)
(* Coercions                                                            *)
(************************************************************************)

let raw a : 'a coerce = (a,[]) (* raw: 'a -> 'a coerce *)
let coerce (a,clist : 'a coerce) c : 'a coerce = (a, c:: clist)
   (* coerce: 'a coerce -> coercion -> 'a coerce  *)
let get_raw (raw, clist : 'a coerce) = raw

(* Is c2 an instance of c1 as sums *)
let check_to_sum error ctxt c1 c2 =
  let err () = error "tosum: bad index" in
  let rec aux c1 c2 =
    let c1 = whnorm ctxt c1 and c2 = whnorm ctxt c2 in
    match c1.rcon,c2.rcon with
      Cprod cs1,Cprod cs2 ->
	(try List.iter2 aux cs1 cs2
	with Invalid_argument _ ->
	  error "tosum: products of different lengths")
    | Csum cs1,Csum cs2 ->
	let rec find1 cs1 cs2 =
	  match cs2 with
	    [] -> ()
	  | c2::cs2 -> find2 cs1 (sum_index err c2) c2 cs2
	and find2 cs1 i2 c2 cs2 =
	  match cs1 with
	    [] -> error "tosum: tag not in sum"
	  | c1::cs1 ->
	      let i1 = sum_index err c1 in
	      if i1=i2 then (aux c1 c2; find1 cs1 cs2)
	      else if i1<i2 then find2 cs1 i2 c2 cs2
	      else error "tosum: tag not in sum" in
	find1 cs1 cs2
    | Csum cs1,_ ->
	let i2 = sum_index err c2 in
	let rec find cs1 =
	  match cs1 with
	    [] -> error "tosum: tag not in sum"
	  | c1::cs1 ->
	      let i1 = sum_index err c1 in
	      if i1=i2 then aux c1 c2
	      else if i1<i2 then find cs1
	      else error "tosum: tag not in sum" in
	find cs1
    | _,_ -> leqcon ctxt c2 c1 in
  match c1.rcon with
    Chptr (is1,c1o) ->
      (match c2.rcon with
	Csing {rcon=Cprim (PCint i)} ->
	  if not (List.mem i is1) then error "tosum: tag not in sum"
      |	Chptr (is2,c2o) ->
	  if not (List.for_all (fun i -> List.mem i is1) is2) then
	    error "tosum: some tag not in sum";
	  (match c1o,c2o with
	    _,None -> ()
	  | None,Some _ -> error "tosum: sum has no pointer"
	  | Some c1,Some c2 -> aux c1 c2)
      |	_ -> error "tosum: not a sum instance")
  | _ -> error "tosum: not a sum"
;;

(* In context ctxt return the type constructor resulting from coercion of con
   by coercion.
   con must be normalized.
 *)
let coercion_con ctxt coercion con =
  let error s = generate_error ctxt (Coercion (con,s,coercion)) in
  match coercion with
    Pack (c1,c2) ->
      let ctxt = set_verify_ctxt ctxt "pack coercion" in
      let (k1,c1) = check ctxt c1
      and (k2,c2) = check_whnorm ctxt c2 in
      (match c2.rcon with
	Cexist (v,k,c2') ->
	  kindleq ctxt k1 k;
	  (* let c = subst c1 v c2' in *)
	  leqcon ctxt con (defcon(Capp(whcon(Clam(v,k,c2')),c1)));
	  c2
      | _ -> error "pack: not an existential"; c2)
  | Tapp c ->
      let ctxt = set_verify_ctxt ctxt "tapp coercion" in
      let (k,c) = check_whnorm ctxt c in
      (match (whnorm ctxt con).rcon with
	Cforall (v1,k1,c1) ->
	  kindleq ctxt k k1;
	  defcon(Capp(whcon(Clam(v1,k1,c1)),c))
      |	_ -> error "tapp: not a forall"; raise Talfail)
  | Roll c ->
      let ctxt = set_verify_ctxt ctxt "roll coercion" in
      let (k,c) = check_whnorm ctxt c in
      leqcon ctxt con (unroll_rec true ctxt c); c
  | Unroll ->
      let ctxt = set_verify_ctxt ctxt "unroll coercion" in
      let c = whnorm ctxt con in
      unroll_rec false ctxt c
  | Tosum c ->
      let ctxt = set_verify_ctxt ctxt "tosum coercion" in
      let (k,c) = check_whnorm ctxt c in 
      check_to_sum error ctxt c con; c
  | Fromsum ->
      let ctxt = set_verify_ctxt ctxt "fromsum coercion" in
      from_union ctxt con
  | RollTosum c ->
      let ctxt = set_verify_ctxt ctxt "rollsum coercion" in
      let (k,c) = check_whnorm ctxt c in
      let cunroll = whnorm ctxt (unroll_rec true ctxt c) in 
      check_to_sum error ctxt cunroll con; c
  | Toexn ->
      let ctxt = set_verify_ctxt ctxt "toexn coercion" in
      (match (whnorm ctxt con).rcon with
	Chptr ([],Some c) ->
	  (match (whnorm ctxt c).rcon with
	    Cprod [c1;c2] ->
	      (match (whnorm ctxt c1).rcon with
		Cfield (c1,v) ->
		  if v<>Read & v<>ReadWrite then
		    error "toexn: first component not readable";
		  (match (whnorm ctxt c1).rcon with
		    Capp (c1,cexn) ->
		      (match (whnorm ctxt c1).rcon with
			Cprim PCexnname ->
			  leqcon ctxt (whnorm ctxt c2) cexn
		      |	_ -> error "toexn: first component not an exnname")
		  | _ -> error "toexn: first component not an exnname")
	      |	_ -> error "toexn: first component not a field")
	  | _ -> error "toexn: not a product")
      |	_ -> error "toexn: not a product");
      pcexn
  | Toarray (offset,depth,celt) ->
      let ctxt = set_verify_ctxt ctxt "toarray coercion" in
      let kelt,celt = check_whnorm ctxt celt in
      kindleq ctxt kelt Kmem;
      let f1,c =
        match (whnorm ctxt con).rcon with
          Chptr (is,Some c) -> (fun c -> defcon (Chptr (is,Some c))),c
        | Csptr c -> (fun c -> csptr c),c
	| _ -> error "toarray: not a pointer"; raise Talfail in
      let f2,c = get_mem_offset ctxt (whnorm ctxt c) offset (Some depth) in
      (match (whnorm ctxt c).rcon with
	Cprod cs ->
	  List.iter (fun c2 -> leqcon ctxt c2 celt) cs;
	  f1 (f2 (carray (pcint (int_to_int32 (List.length cs))) celt))
      |	_ -> error "toarray: not an array form"; raise Talfail)
  | Slot (i,s) ->
      (match (whnorm ctxt con).rcon with
        Csptr c -> csptr (write_stack_offset ctxt c i (pcjunk s))
      | _ -> error "slot: not a stack pointer"; raise Talfail)
  | Subsume c ->
      let ctxt = set_verify_ctxt ctxt "subsume coercion" in
      let (_,c) = check_whnorm ctxt c in
      leqcon ctxt con c;
      c
;;
     
let coerce_con f ctxt (raw,clist) =
  let c = f ctxt raw in
  List.fold_right (coercion_con ctxt) clist c
;;

(************************************************************************)
(* Operands                                                             *)
(************************************************************************)

(* get the current stack type *)
let current_stack_con ctxt =
  match (whnorm ctxt (get_reg_con ctxt Esp)).rcon with
    Csptr c -> c
  | _ -> generate_error ctxt No_stack_type; cempty
;;

(* is con a valid stack type if so return the mutator function *)
let valid_stack_con ctxt con =
  verify_stack_tail ctxt con (current_stack_con ctxt)
;;

(* ctxt |- coerce(reg) : c *)
let coerce_reg_con = coerce_con get_reg_con;;

(* ctxt |- coerce(label) : c *)
let coerce_label_con = coerce_con get_label_con;;

let coerce_label_con_opt ctxt (l,clist) =
   match get_label_con_opt ctxt l,clist with
     None,[] -> None
   | None,_ -> generate_error ctxt (Label_requires_type l); None
   | Some c,_ -> Some(List.fold_right (coercion_con ctxt) clist c)
;;

let coerce_label_con_whrcon_opt ctxt lc =
  match coerce_label_con_opt ctxt lc with
    None -> None
  | Some c -> Some((whnorm ctxt c).rcon)

(*** The next two functions check genops for validity and readability and
      optionally for writeability returning the genop's type ***)

(* Verify a projection *)
type prj_ctxt = PRns | PRsp | PRor;;
let verify_prj ctxt error c pr i w =
  let (c,mf) = 
    match c.rcon with
      Chptr (_::_,_) -> error "prj: pointer has tags"; raise Talfail
    | Chptr ([],None) -> error "prj: not pointer"; raise Talfail
    | Chptr ([],Some c) -> (c,true)
    | Csptr c ->
      	if pr = PRns then
 	  failwith "Talverify.verify_prj - should not be a stack pointer"
      	else if pr = PRor then
	  (let _ = valid_stack_con ctxt c in ());
      	(c,false)
    | _ -> error "prj: not a pointer or stack"; raise Talfail in
  let (_,c) = get_mem_offset ctxt (whnorm ctxt c) i None in
  match (whnorm ctxt c).rcon with
    Cfield (c,v) ->
      if w & v<>ReadWrite then
	generate_error ctxt Readonly
      else if (not w) & v<>Read & v<>ReadWrite then
	error "prj: field not readable";
      c
  | _ ->
      if mf then
	error "prj: not a field"
      else
	kindleq ctxt (con_kind ctxt c) k4byte;
      c
;;

(* ctxt |- genop : c *)
let genop_con w ctxt genop = 
  let error s = generate_error ctxt (Genop (s,genop)) in
  match genop with
    Immed i -> if w then generate_error ctxt Readonly; csing (pcint i)
  | Reg r -> get_reg_con ctxt r
  | Addr l -> if w then generate_error ctxt Readonly; get_label_con ctxt l
    (* rc and lc must be either product types or else stack pointer types *)
  | Prjr ((r,_) as rc,i) -> 
      let rc_con = whnorm ctxt (coerce_reg_con ctxt rc) in
      let pr = if r=Esp then PRsp else PRor in
      verify_prj ctxt error rc_con pr i w
  | Prjl (lc,i) -> 
      let lc_con = whnorm ctxt (coerce_label_con ctxt lc) in
      verify_prj ctxt error lc_con PRns i w
;;
let coerce_genop_con w = coerce_con (genop_con w);;
    
(*** Can a con be written to a genop? ***)
(* Checks also that gop is vaild *)

(* Checks to see if a field in a tuple or the stack is writeable with
 * an object of a given type, and updates the type of that object.
 * ctxt: the current context.
 * error: string -> unit -- what to do when something goes wrong
 * c: the type of the object we're trying to write into
 * pr: indicates whether it can be on the stack or not.
 * i: the offset into the object where we're writing.
 * con: the type of the object we're writing
 * upd: a function to update the context, given the updated type
 * check_con: if true checks whether con <= c.  
 *
 * This is only called by Mov (via genop_write_at) and Settla.
 *)
let writeable_prj ctxt error c pr i con upd check_con =
  match c.rcon with
    Chptr (_::_,_) -> error "prj: pointer has tags"; raise Talfail
  | Chptr ([],None) -> error "prj: not pointer"; raise Talfail
  | Chptr ([],Some c) ->
      let (f,c) = get_mem_offset ctxt (whnorm ctxt c) i None in
      (match (whnorm ctxt c).rcon with
	Cfield (c,v) ->
	  if not (v=Write or v=ReadWrite or v=Uninit) then
	    generate_error ctxt Readonly;
	  if check_con then 
	    begin
	      leqcon ctxt con c;
	      if v=Uninit then
	    	upd ctxt (cptr (f (cfield con ReadWrite)))
	      else
	    	ctxt
	    end
	  else 
	    begin
	      upd ctxt (cptr (f (cfield con ReadWrite)))
	    end
      | _ -> error "prj: not a field"; raise Talfail)
  | Csptr c ->
      if pr = PRns then
 	failwith "Talverify.writeable_prj - should not be a stack pointer"
      else if pr = PRor then begin
	let f = valid_stack_con ctxt c in
	let c = write_stack_offset ctxt c i con in
	upd (add_reg ctxt Esp (csptr (f c))) (csptr c)
      end else begin
	let c = write_stack_offset ctxt c i con in
	add_reg ctxt Esp (csptr c)
      end
  | _ -> error "prj: not a pointer or stack"; raise Talfail
;;

let genop_write_at ctxt gop con =
  let error s = generate_error ctxt (Genop (s,gop)) in
  match gop with
    Reg r ->
      kindleq ctxt (con_kind ctxt con) k4byte;
      if r=Esp then begin
	match (whnorm ctxt con).rcon with
	  Csptr c ->
	    let _ = valid_stack_con ctxt c in ()
	| _ -> ()
      end;
      add_reg ctxt r con
  | Prjr ((r,cs) as rc,i) ->
      let rc_con = whnorm ctxt (coerce_reg_con ctxt rc) in
      let pr = if r=Esp then PRsp else PRor in
      let upd =
 	if cs=[] then (fun ctxt c -> add_reg ctxt r c)
 	else (fun ctxt _ -> ctxt) in
      writeable_prj ctxt error rc_con pr i con upd true
  | Prjl (lc,i) ->
      let lc_con = whnorm ctxt (coerce_label_con ctxt lc) in
      writeable_prj ctxt error lc_con PRns i con (fun ctxt _ -> ctxt) true
  | _ -> generate_error ctxt Readonly; ctxt
;;

(*** Miscellaneous Validity Conditions ***)

(* Is operand register or memory? *)
let reg_or_mem_genop ctxt g =
  match g with
    Immed _ -> generate_error ctxt (Genop ("operand is an immediate",g))
  | Reg _ -> ()
  | Addr _ -> generate_error ctxt (Genop ("operand is a label",g))
  | Prjr (_,_) -> ()
  | Prjl (_,_) -> ()
;;

(* verify that only one of the operands is a path to memory *)
let is_mem gop =
  match gop with
    Immed _ -> false
  | Reg _ -> false
  | Addr _ -> false
  | Prjr (_,_) -> true
  | Prjl (_,_) -> true
;;

(* Is operand register or address? *)
let reg_or_addr ctxt g =
  match g with
    Immed _ | Prjr (_,_) | Prjl (_,_) ->
      generate_error ctxt (Genop ("operand is not register or address",g))
  | Reg _ | Addr _ -> ()
;;

let valid_binops ctxt gop1 gop2 = 
  if is_mem gop1 & is_mem gop2 then
    generate_error ctxt (Both_mem (gop1,gop2))
;;

let valid_cbinops ctxt gop1 cgop2 = valid_binops ctxt gop1 (get_raw cgop2);;

(************************************************************************)
(* Condition Code Stuff                                                 *)
(************************************************************************)

(* Based on the current register state's condition code information and a
 * condition code to branch on produce two new contexts specialised for the
 * success & failure respectively of the jump
 *)
let process_cc ctxt cc = ctxt,ctxt
(*
  match get_cc ctxt with
    CCnoinfo -> ctxt,ctxt
  | CCcmp (c1,c2) ->
      (match (whnorm ctxt c1).rcon,(whnorm ctxt c2).rcon with
	(* This is Dave's case *)
	Csing c1,Csing c2 -> ctxt,ctxt
      |	_,_ -> ctxt,ctxt)
  | CCtest (_,_) -> ctxt,ctxt
*)
;;

(************************************************************************)
(* Instructions                                                         *)
(************************************************************************)

let inst_form ctxt s = generate_error ctxt (Inst_form s);;

exception Terminal_Jmp;;
exception Fall_Thru of ctxt * (con list);;

(*** Generic x86 Instructions ***)

(* Normal case: two byte4s, first is writeable, not both mem.
 * Special case: add to stack pointer type is "free"
 * Special case: sub from ESP is a "stack allocate"
 *
 *  ctxt |- genop1 : byte4  ctxt |- genop2 : byte4  
 *     ctxt |- (genop1,genop2) valid binops
 *     ctxt |- genop1 writeable
 *  ----------------------------------------------
 *  ctxt |- ArithBin ab genop1,genop2 : ctxt
 *
 *  ctxt |- r : Stackptr(c1::....::ci::c)
 *  ctxt |- n : byte4  
 *     ctxt |- (genop1,genop2) valid binops
 *     ctxt |- genop1 writeable
 *  ----------------------------------------------(n=sizeof(c1::...::ci))
 *  ctxt |- Add r,n : ctxt[r:Stacpkptr(c)]
 *
 *  ctxt |- ESP : Sptr(c)
 *  ---------------------------------------------------------
 *  ctxt |- Sub ESP,4n : ctxt[ESP:Sptr(junk1::...::junkn::c)]
 *)
   
let verify_ArithBin ctxt ab genop1 genop2 =
  if ab=Sub & genop1=(Reg Esp) then begin
    match genop2 with
      Immed n when n >=$ i32_0 ->
	let cstk = current_stack_con ctxt in
	let cstk = if n =$ i32_0 then cstk else ccons (pcjunk n) cstk in
	add_reg ctxt Esp (csptr cstk)
    | _ -> inst_form ctxt "ESP - non-immed"; raise Talfail
  end else begin
    match ab,genop1,genop2 with
      Xor,Reg r1,Reg r2 when (compare_regs r1 r2)=0 ->
	add_reg ctxt r1 tag_cons.(0)
    | _,_,_ ->
    	valid_binops ctxt genop1 genop2;
	let c1 = whnorm ctxt (genop_con false ctxt genop1) in
    	match c1.rcon with
        (* A normal binop *)
	  Cprim (PCbytes Byte4) | Csing {rcon=Cprim (PCint _)} ->
	    let c2 = genop_con false ctxt genop2 in
	    leqcon ctxt c2 cbyte4;
	    let ctxt =
	      match ab with
		Sub -> set_cc ctxt (CCcmp (c1,c2))
	      |	And -> set_cc ctxt (CCtest (c1,c2))
	      |	_ -> ctxt in
	    genop_write_at ctxt genop1 cbyte4
        (* adjusting a pointer onto the stack -- note that this provides
	 * "stack free" but it's more general in that we can calculate
	 * pointers into the middle of the stack from other pointers into
	 * the middle of the stack, as long as the sizes of the intervening
         * types are known (i.e., there's no intervening append). *)
    	| Csptr c ->
	    (match ab,genop1,genop2 with
	      (Add,Reg r,Immed i) -> 
	    	let c' = get_stack_tail ctxt i c in
            	add_reg ctxt r (csptr c')
	    | (_,_,_) ->
		inst_form ctxt "ArithBin: stack pointer"; raise Talfail)
    	| _ -> inst_form ctxt "ArithBin"; raise Talfail
  end
;;

(* ctxt |- genop : byte4   ctxt |- genop writeable
 * -----------------------------------------------
 * ctxt |- ArithUn arithun genop : ctxt
 *)

let verify_ArithUn ctxt arithun genop =
  let c = genop_con false ctxt genop in
  leqcon ctxt c cbyte4;
  genop_write_at ctxt genop cbyte4
;;

(* Div,IDiv: divides Eax by the operand and puts the quotient in Eax and 
 *  remainder in Edx. (Div is unsigned, IDiv is signed)
 * Mul,Imul1: multiples Eax by the operand and puts the 64-bit result in
 *  Eax and Edx.  (Mul is unsigned, Imul1 is signed)
 * In any of the cases, Eax must be a Byte4, the operand must be a Byte4,
 * and the resulting context maps Edx to Byte4.
 *
 * ctxt |- genop : byte4  ctxt |- Eax : byte4
 * -----------------------------------------------
 * ctxt |- ArithMd arithmd genop : ctxt[Eax,Edx:byte4]
 *)
let verify_ArithMD ctxt arithmd genop =
  leqcon ctxt (genop_con false ctxt genop) cbyte4;
  leqcon ctxt (get_reg_con ctxt Eax) cbyte4;
  add_reg (add_reg ctxt Eax cbyte4) Edx cbyte4
;;

(* Arithmatic shift operations. If iopt is None, then Ecx is used
 * as the shift amount.  Otherwise, the integer immediate is used
 * as the shift amount.
 *
 * ctxt |- genop : byte4  ctxt |- genop writeable
 * ctxt |- Ecx : byte4
 * ----------------------------------------------
 * ctxt |- ArithSR arithsr genop None : ctxt
 *
 * ctxt |- genop : byte4  ctxt |- genop writeable
 * ----------------------------------------------
 * ctxt |- ArithSR arithsr genop (Some i) : ctxt
 *)

let verify_ArithSR ctxt arithsr genop iopt =
  leqcon ctxt (genop_con false ctxt genop) cbyte4;
  (match iopt with
    Some _ -> ()
  | None -> leqcon ctxt (get_reg_con ctxt Ecx) cbyte4);
  genop_write_at ctxt genop cbyte4
;;

(* Byte-swap 
 * ctxt |- reg : byte4
 * ------------------------
 * ctxt |- Bswap reg : ctxt
 *)

let verify_Bswap ctxt reg =
  restore_cc ctxt;
  leqcon ctxt (get_reg_con ctxt reg) cbyte4;
  add_reg ctxt reg cbyte4
;;

(* Call:
 * This is a little delicate.  The called label must have a code type which is
 * a supertype of the current code type with the return address pushed;
 * however, the return address type is garned from the code type of the called
 * label; however, the called label might ignore the return label and there may
 * be no return type.  In the later case we should treat call as a terminal
 * jump.
 *
 * For now: if the called label defines ESP then it must have a code type on
 * top, use it.  Otherwise its a terminal jump.
 * 
 * ctxt |- cgop : Ccode g1
 * ctxt |- g1(ESP) = Sptr (Ccode g2::c')
 * ctxt |- ctxt.gamma [ESP: Sptr (Ccode g2::(ctxt.gamma(ESP)))] <= g1
 * ------------------------------------------------------------------ESP in g1
 * ctxt |- Call cgop : ctxt[gamma: g2]
 *
 * ctxt |- cgop : Ccode g1
 * ctxt |- ctxt.gamma <= g1
 * --------------------------------ESP not in g1
 * ctxt |- Call cgop : terminal jump
 *)

let verify_Call ctxt cgop =
  restore_cc ctxt;
  let c = whnorm ctxt (coerce_genop_con false ctxt cgop) in
  match c.rcon with
    Ccode g2 ->
      let g1 = get_register_state ctxt in
      (try
	let called_st = whnorm ctxt (rs_get_reg g2 Esp) in
        let c = whnorm ctxt (current_stack_con ctxt) in
	match called_st.rcon with
	  Csptr c' ->
            (match (whnorm ctxt c').rcon with
               Ccons(ca,c') -> 
                (match (whnorm ctxt ca).rcon with
                  (Ccode gret) -> 
   	             leqcon ctxt c c';
	             reg_state_leq ctxt (rs_set_reg g1 Esp called_st) g2;
	             set_register_state ctxt gret
                 | _ -> 
                     inst_form ctxt "Call: no return address in pre-condition";
                     raise Talfail)
              | _ -> inst_form ctxt "Call: no return address in pre-condition";
                     raise Talfail)     
	 | _ ->
	    inst_form ctxt "Call: bad return address or stack";
	    raise Talfail
      with Dict.Absent ->
	reg_state_leq ctxt g1 g2; raise Terminal_Jmp)
  | _ -> inst_form ctxt "Call: operand not code"; raise Talfail
;;

(* Conditional move: it must be the case that if cgop : c, then
 * r : c.  This ensures that after the conditional move, r : c.
 *
 * ctxt |- r : c1    ctxt |- cgop : c2    ctxt |- c2<=c1
 * -----------------------------------------------------
 * ctxt |- Cmovcc r,cgop : ctxt
 *)

let verify_Cmovcc ctxt cond r cgop = 
  restore_cc ctxt;
  leqcon ctxt (coerce_genop_con false ctxt cgop) (get_reg_con ctxt r);
  ctxt
;;

(* We generalize to allow comparisons of any two values of equal type.
 * Exception: we also allow S(i) to be compared with a B4 or S(j).
 * 
 * ctxt |- (genop1,genop2) valid binops
 * ctxt |- genop1 reg_or_mem_genop
 * ctxt |- genop1 : c   ctxt |- genop2 : c
 * -----------------------------------------------
 * ctxt |- Cmp genop1,genop2 : byte4
 *)

let verify_Cmp ctxt genop1 genop2 =
  valid_binops ctxt genop1 genop2; reg_or_mem_genop ctxt genop1;
  let c1 = whnorm ctxt (genop_con false ctxt genop1)
  and c2 = whnorm ctxt (genop_con false ctxt genop2) in
  (match c1.rcon,c2.rcon with
    (Cprim (PCbytes Byte4) | Csing {rcon=Cprim (PCint _)}),
    (Cprim (PCbytes Byte4) | Csing {rcon=Cprim (PCint _)}) -> ()
  | _,_ -> eqcon ctxt c1 c2);
  set_cc ctxt (CCcmp (c1,c2))
;;

(* ctxt |- Eax : byte4
 * ----------------------------------
 * ctxt |- Cbw/Cwde : ctxt[Eax:byte4]
 *
 * ctxt |- Eax : byte4
 * -------------------------------------
 * ctxt |- Cdq/Cwd : ctxt[Eax,Edx:byte4]
 *)

let verify_Conv ctxt c =
  restore_cc ctxt;
  match c with
    (Cbw | Cwde) -> 
      leqcon ctxt (get_reg_con ctxt Eax) cbyte4;
      add_reg ctxt Eax cbyte4
  | (Cdq | Cwd) -> 
      leqcon ctxt (get_reg_con ctxt Eax) cbyte4;
      add_reg (add_reg ctxt Eax cbyte4) Edx cbyte4
;;

(* ctxt |- genop : byte4
 * ---------------------------------------
 * ctxt |- Imul3 r,genop,i : ctxt[r:byte4]
 *)

let verify_Imul3 ctxt r genop i =
  leqcon ctxt (genop_con false ctxt genop) cbyte4; add_reg ctxt r cbyte4
;;

(* A jump helper function.
 * verify_jump add_block ctxt lc  iff  ctxt |- jmp lc
 *)
let verify_jmp add_block ctxt (l,_ as lc) =
  match coerce_label_con_opt ctxt lc with
    None -> 
     (* there's no type on the label l, so we must type-check that
      * block under the current context.  Hence, the block and context
      * are added to a work list.
      *)
      add_block ctxt l
  | Some c -> 
      (match (whnorm ctxt c).rcon with
        Ccode rs -> reg_state_leq ctxt (get_register_state ctxt) rs
      | _ -> inst_form ctxt "jmp: label for branch is not code")
;;

(* ctxt |- lc : Ccode(g)    ctxt |- ctxt.gamma <= g
 * ------------------------------------------------
 * ctxt |- Jcc cc,lc : ctxt
 *)
let verify_Jcc add_block ctxt cc lc =
  restore_cc ctxt;
  let ctxt_taken,ctxt_fallthru = process_cc ctxt cc in
  verify_jmp add_block ctxt_taken lc;
  ctxt_fallthru
;;

(* ctxt |- lc : Ccode(g)   ctxt |- ctxt.gamma <= g
 * ctxt |- Ecx : byte4
 * -----------------------------------------------
 * ctxt |- Jecxz lc : ctxt
 *)

let verify_Jecxz add_block ctxt lc =
  restore_cc ctxt;
  leqcon ctxt (get_reg_con ctxt Ecx) cbyte4;
  verify_jmp add_block ctxt lc;
  ctxt
;;

(* ctxt |- gc : Ccode(g)    ctxt |- ctxt.gamma <= g
 * ------------------------------------------------
 * ctxt |- branch lc : ctxt
 *)

let verify_Jmp add_block ctxt gc =
  restore_cc ctxt;
  (match gc with
    (Addr l,cs) -> verify_jmp add_block ctxt (l,cs)
  | _ ->
      (match (whnorm ctxt (coerce_genop_con false ctxt gc)).rcon with
      	Ccode rs -> reg_state_leq ctxt (get_register_state ctxt) rs
      | _ -> inst_form ctxt "Jmp: label for branch is not code"));
  raise Terminal_Jmp
;;

(* this is really only useful for moving an offset from the stack
 * into a register or moving a label into a register which is more
 * easily accomplished via a mov.
 *
 *  ctxt |- l : c
 *  ---------------------------
 *  ctxt |- Lea r,[l+0] : ctxt[r:c]
 *
 *  ctxt |- rc : Cprod(fs)
 *  ----------------------
 *  ctxt |- Lea r,[rc+0] : ctxt[r:Cprod(fs)]
 *
 *  ctxt |- rc : Stackptr(c1::...::cn::c)
 *  Stackptr(c1::...::cn::c) tailof ctxt.gamma(Esp)  <-- not really needed
 *  -----------------------------------------------
 *  ctxt |- Lea r,rc[i] : ctxt[r:Stackptr(c)]
 *)

let verify_Lea ctxt r g =
  restore_cc ctxt;
  match g with
    Immed _ -> inst_form ctxt "Lea: immediate"; raise Talfail
  | Reg _ -> inst_form ctxt "Lea: register"; raise Talfail
  | Addr _ -> inst_form ctxt "Lea: label"; raise Talfail
  | Prjr (rc,i) ->
      let rc_con = coerce_reg_con ctxt rc in
      (match (whnorm ctxt rc_con).rcon with
	Csptr c ->
	  let _ = valid_stack_con ctxt c in
	  add_reg ctxt r
	    (csptr (get_stack_tail ctxt i c))
      |	Chptr ([],_) ->
	  if i <>$ i32_0 then inst_form ctxt "Lea: middle tuple pointer";
	  add_reg ctxt r rc_con
      | _ -> inst_form ctxt "Lea: non pointer type"; raise Talfail)
  | Prjl (lc,i) when i=$i32_0-> add_reg ctxt r (coerce_label_con ctxt lc)
  | Prjl (_,_) -> inst_form ctxt "Lea: middle tuple pointer"; raise Talfail
;;
	      
(* ctxt |- Ecx : B4  ctxt |- lc : code(g)  ctxt |- g<=ctxt.gamma
 * -------------------------------------------------------------------
 * ctxt |- loop lc,bo : if bo=None then Terminal_Jmp else ctxt[Ecx:B4]
 *)

let verify_Loop add_block ctxt lc bo =
  restore_cc ctxt;
  leqcon ctxt (get_reg_con ctxt Ecx) cbyte4;
  let ctxt = add_reg ctxt Ecx cbyte4 in
  verify_jmp add_block ctxt lc;
  match bo with
    None -> raise Terminal_Jmp
  | Some _ -> ctxt
;;

(* NG - I've vastly simplified the move rule by moving all the smarts into
 *      the code for genop_write_at
 *
 *   ctxt |- gop writeable at c
 *   ctxt |- cgop : c
 *   gop,cgop valid binops
 *   --------------------------
 *   ctxt |- Mov gop,cgop
 *)

let verify_Mov ctxt gop cgop =
  restore_cc ctxt;
  valid_cbinops ctxt gop cgop;
  let c_source = coerce_genop_con false ctxt cgop in
  genop_write_at ctxt gop c_source
;;

let verify_Movpart ctxt signext gop1 part1 gop2 part2 =
  failwith "Talverify.verify_Movpart - unimplemented"
;;

(*
  let aux r s1 gop s2 =
    if s1<>Byte4 then inst_form ctxt "Movsx/Movzx: dest must be 32 bit";
    if s2<>Byte2 & s2<>Byte1 then
      inst_form ctxt "Movsx/Movzx: src must be 8/16 bit";
    (match (whnorm ctxt (genop_con false ctxt gop)).rcon with
      Cprim (PCbytes s3) ->
        if s2<>s3 then 
          inst_form ctxt "Movsx/Movzx: operand size does not match scale"
    | _ -> inst_form ctxt "Movsx/Movzx: operand not bytes");
    add_reg ctxt r cbyte4
  in
  | Movsx (r,s1,gop,s2) -> aux r s1 gop s2
  | Movzx (r,s1,gop,s2) -> aux r s1 gop s2
*)

(* Pop
 *
 * Expand to: Mov genop,[esp+0]; Add Esp,4
 *)

let verify_Pop ctxt genop =
  restore_cc ctxt;
  let ctxt = verify_Mov ctxt genop (Prjr ((Esp,[]),i32_0),[]) in
  let ctxt = verify_ArithBin ctxt Add (Reg Esp) (Immed i32_4) in
  ctxt
;;

(* Popad pops all of the registers.  However, the value for the
 * Esp register is discarded.
 *
 * ctxt |- Esp : sptr(c0::c1::c2::c3::c4::c5::c6::c7::c)
 * ctxt |- ci : K4byte 0<=i<=7
 * ---------------------------------------------------------
 * ctxt |- Popad : ctxt[Eax:c7, Ebx:c4, Ecx:c6, Edx:c5,
 *                      Esp:sptr(c), Ebp:c2, Esi:c1, Edi:c0]
 *)

let verify_Popad ctxt =
  restore_cc ctxt;
  let strip_check ctxt r stkcon =
    match (whnorm ctxt stkcon).rcon with
      Ccons (c1,c2) ->
	kindleq ctxt (con_kind ctxt c1) k4byte; (add_reg ctxt r c1,c2)
    | _ -> inst_form ctxt "Popad: stack not a cons"; raise Talfail in
  let stkcon = current_stack_con ctxt in
  let (ctxt,stkcon) = strip_check ctxt Edi stkcon in
  let (ctxt,stkcon) = strip_check ctxt Esi stkcon in
  let (ctxt,stkcon) = strip_check ctxt Ebp stkcon in
  let (ctxt,stkcon) = strip_check ctxt Ebx stkcon in
  let (ctxt,stkcon) = strip_check ctxt Ebx stkcon in
  let (ctxt,stkcon) = strip_check ctxt Edx stkcon in
  let (ctxt,stkcon) = strip_check ctxt Ecx stkcon in
  let (ctxt,stkcon) = strip_check ctxt Eax stkcon in
  add_reg ctxt Esp (csptr stkcon)
;;

(* Popfd pops a 4-byte value into the flags register.  Hence, the
 * stack pointer must point to a byte4 before hand, and afterwards,
 * points to the tail. 
 *   ctxt |- Esp : sptr(byte4::c)
 *   -----------------------------------------
 *   ctxt |- Popfd : ctxt[Esp:Stackptr(c)]
 *)

let verify_Popfd ctxt =
  match (whnorm ctxt (current_stack_con ctxt)).rcon with
    Ccons (c,c') ->
      eqcon ctxt cbyte4 c;
      add_reg ctxt Esp (csptr c')
  | _ -> inst_form ctxt "Popfd: Esp has no top slot"; raise Talfail
;;

(* ctxt |- Esp : sptr(c')
 * ctxt |- gc : c
 * ctxt |- c : T4
 * ----------------------------------------
 * ctxt |- pushd gc : ctxt[Esp:sptr(c::c')]
 *)

(* Support for other sizes needed *)
let verify_Push ctxt gc =
  restore_cc ctxt;
  let c = coerce_genop_con false ctxt gc in
  kindleq ctxt (con_kind ctxt c) k4byte;
  let cstack = ccons c (current_stack_con ctxt) in
  add_reg ctxt Esp (csptr cstack)
;;

(* ctxt |- Eax,Ebx,Ecx,Edx,Esi,Edi,Ebp : c7,c4,c6,c5,c1,c0,c2
 * ctxt |- Esp : sptr(c)
 * -----------------------------------------------------------------------
 * ctxt |- pushad : ctxt[Esp:sptr(c0::c1::c2::sptr(c)::c4::c5::c6::c7::c)]
 *
 * N.B. registers have to have K4byte-s in them.
 *)

let verify_Pushad ctxt = 
  restore_cc ctxt;
  let c3 = (whnorm ctxt (get_reg_con ctxt Esp)) in
  match c3.rcon with
    Csptr cs ->
      let c0 = get_reg_con ctxt Edi
      and c1 = get_reg_con ctxt Esi
      and c2 = get_reg_con ctxt Ebp
      and c4 = get_reg_con ctxt Ebx
      and c5 = get_reg_con ctxt Edx
      and c6 = get_reg_con ctxt Ecx
      and c7 = get_reg_con ctxt Eax in
      let cs = List.fold_right ccons [c0;c1;c2;c3;c4;c5;c6;c7] cs in
      add_reg ctxt Esp (csptr cs)
  | _ -> inst_form ctxt "Pushad: Esp not a stack pointer"; raise Talfail
;;

(* ctxt |- Esp : sptr(c)
 * -----------------------------------------
 * ctxt |- Pushfd : ctxt[Esp:sptr(byte4::c)]
 *)

let verify_Pushfd ctxt =
  restore_cc ctxt;
  let cs = current_stack_con ctxt in
  add_reg ctxt Esp (csptr (ccons cbyte4 cs))
;;

(* Retn: pops the return address off the stack and then pops an additional
 * (optional) i bytes off the stack, then jumps to the return address.
 *
 *  ctxt |- Esp : Ccode(G)::c1::c2::...::cn::ctail'
 *  ctxt |- sizeof(c1) + ... + sizeof(cn) = i
 *  ctxt |- ctxt.gamma[Esp:ctail'] <= G
 *  -----------------------------------------------
 *  ctxt |- Retn (Some i) : ctxt'
 *)

let verify_Retn ctxt iopt =
  restore_cc ctxt;
  (match (whnorm ctxt (current_stack_con ctxt)).rcon with
    Ccons (cg,ctail) ->
      (match (whnorm ctxt cg).rcon with
        Ccode g2 -> 
          let ctail' = 
            match iopt with 
              None -> ctail 
            | Some i -> get_stack_tail ctxt i ctail in
          let newctxt = add_reg ctxt Esp (csptr ctail') in
          reg_state_leq ctxt (get_register_state newctxt) g2
      | _ -> inst_form ctxt "Retn: no return address on stack")
  | _ -> inst_form ctxt "Retn: bad stack pointer (no app)");
  raise Terminal_Jmp
;;

(* Setcc writes a byte into the low part of operand.
 * Therefore gop must be a Chptr (is,None) type where the is
 * contain 1 and values less than 256.
 *
 *   ctxt |- gop writeable   ctxt |- gop : Chptr(is,None)
 *   ----------------------------------------------------0,1 in is;is<256
 *   ctxt |- Setcc gop : ctxt
 *)

let verify_Setcc ctxt cc gop =
  restore_cc ctxt;
  (match (whnorm ctxt (genop_con true ctxt gop)).rcon with
    Chptr (is,None) ->
      if not (List.mem i32_0 is) then
 	inst_form ctxt "Setcc: no 0 tag";
      if not (List.mem i32_1 is) then
 	inst_form ctxt "Setcc: no 1 tag";
      let check_tag i =
 	if (land32 i (lnot32 i32_255)) <>$ i32_0 then
	  inst_form ctxt "Setcc: tag too big" in
      List.iter check_tag is
  | Csing c ->
      (match (whnorm ctxt c).rcon with
	Cprim (PCint i) ->
	  if (land32 i (lnot32 i32_255)) <>$ i32_0 then
	    inst_form ctxt "Setcc: singleton too big"
      |	_ -> inst_form ctxt "Setcc: bad singleton")
  | _ -> inst_form ctxt "Setcc: not sum of tags or S(i)");
  genop_write_at ctxt gop (chptr [i32_0;i32_1] None)
;;

(* shifts: gop must be writeable and a byte4, r must be a byte4
 *         Ecx must be byte4 if it is the shift amount
 *
 * ctxt |- gop : byte4  ctxt |- gop writeable
 * ctxt |- Ecx : byte4    ctxt |- r : byte4
 * ----------------------------------------------
 * ctxt |- Shld/Shrd gop,r,None : ctxt
 *
 * ctxt |- gop : byte4  ctxt |- gop writeable
 * ctxt |- r : byte4
 * ----------------------------------------------
 * ctxt |- Shld/Shrd gop,r,(Some i) : ctxt
 *)

let verify_Shld_Shrd ctxt gop r iopt =
  leqcon ctxt (genop_con false ctxt gop) cbyte4;
  leqcon ctxt (get_reg_con ctxt r) cbyte4;
  (match iopt with
    Some _ -> ()
  | None -> leqcon ctxt (get_reg_con ctxt Ecx) cbyte4);
  genop_write_at (add_reg ctxt r cbyte4) gop cbyte4
;;

(* ctxt |- (gop1,gop2) valid_binops
 * ctxt |- gop1 : byte4  ctxt |- gop2 : byte4
 * ------------------------------------------
 * ctxt |- test gop1,gop2 : ctxt
 *)

let verify_Test ctxt gop1 gop2 =
  valid_binops ctxt gop1 gop2;
  let c1 = genop_con false ctxt gop1
  and c2 = genop_con false ctxt gop2 in
  leqcon ctxt c1 cbyte4; leqcon ctxt c2 cbyte4;
  set_cc ctxt (CCtest (c1,c2))
;;

(* exchange gop1 and gop2.
 *   ctxt |- r : c2
 *   ctxt |- gop1 : c1
 *   ctxt |- gop1 writeable
 *   ctxt |- c2 <= c1
 *   ----------------------------------------------
 *   ctxt |- Xchg gop1,gop2 : ctxt[r:c1]
 *
 * Exception if gop1=r1 then don't require c2<=c1 and return
 *   ctxt[r:c1,r1:c2]
 * NG - could add case where gop1=[r+i] and r:sptr c1' to change the stack
 *      type.  This isn't implemented yet.
 *)

let verify_Xchg ctxt gop1 r =
  restore_cc ctxt;
  let c1 = genop_con true ctxt gop1
  and c2 = get_reg_con ctxt r in
  match gop1 with
    Reg r1 ->
      add_reg (add_reg ctxt r1 c2) r c1
  | _ ->
      leqcon ctxt c2 c1; add_reg ctxt r c1
;;

(*** TAL specific instructions ***)

let verify_array ctxt gop1 es rind gop2 =
  let error s = generate_error ctxt (Genop (s,gop1)) in
  let (c1,pr,offset) =
    match gop1 with
      Prjr ((r,_ as rc),offset) ->
        coerce_reg_con ctxt rc, (if r=Esp then PRsp else PRor), offset
    | Prjl (lc,offset) -> coerce_label_con ctxt lc, PRns, offset
    | _ -> error "Asub/Aupd: array not a projection"; raise Talfail in
  let c1 =
    match (whnorm ctxt c1).rcon with
      Chptr (_::_,_) -> error "prj: pointer has tags"; raise Talfail
    | Chptr ([],None) -> error "prj: not pointer"; raise Talfail
    | Chptr ([],Some c) -> c
    | Csptr c ->
      	if pr = PRns then
 	  failwith "Talverify.verify_array - should not be a stack pointer"
      	else if pr = PRor then
	  (let _ = valid_stack_con ctxt c in ());
      	c
    | _ -> error "prj: not a pointer or stack"; raise Talfail in
  let (_,c1,offset) = get_mem_offset_p ctxt (whnorm ctxt c1) offset None in
  let (csize,celt,v) =
    match (whnorm ctxt c1).rcon with
      Carray (csize,celt) ->
	let _,celt = get_mem_offset ctxt (whnorm ctxt celt) offset None in
	(match (whnorm ctxt celt).rcon with
	  Cfield (c,v) -> (csize,c,v)
	| _ ->
          inst_form ctxt "Asub/Aupd: array element not a field"; raise Talfail)
    | _ -> inst_form ctxt "Asub/Aupd: not an array"; raise Talfail in
  (match (genop_con false ctxt gop2).rcon with
    Csing c2 -> eqcon ctxt csize c2
  | _ -> inst_form ctxt "Asub/Aupd: size not a singleton");
  if es<>(sizeof ctxt celt) then inst_form ctxt "Asub/Aupd: bad element size";
  leqcon ctxt (get_reg_con ctxt rind) cbyte4;
  (celt,v)
;;

(*  ctxt |- gop1 : array(sz,elt_con) + i bytes
 *  ctxt |- elt_con[i] : c1^r
 *  ctxt |- gop2 : S(sz)
 *  ctxt |- size(elt_con)=es
 *  ctxt |- r2 : B4
 *  -----------------------------------------------
 *  ctxt |- Asub r1,gop1,es,r2,genop2 : ctxt[r1:c1]
 *
 *  Exception: if elt_con is B(1|2|8) then ctxt |- r1:B4
 *                                     and result is ctxt[r1:B4]
 *)

let verify_Asub ctxt r1 gop1 es r2 genop2 =
  let (celt,v) = verify_array ctxt gop1 es r2 genop2 in
  if v<>Read & v<>ReadWrite then inst_form ctxt "Asub: field not readable";
  let celt =
    match (whnorm ctxt celt).rcon with
      Cprim (PCbytes s) when s<>Byte4 ->
	leqcon ctxt (get_reg_con ctxt r1) cbyte4; cbyte4
    | _ -> kindleq ctxt (con_kind ctxt celt) k4byte; celt in
  add_reg ctxt r1 celt
;;

(*  ctxt |- gop1 : array(sz,elt_con) + i bytes
 *  ctxt |- elt_con[i] : c1^w
 *  ctxt |- gop2 : S(sz)
 *  ctxt |- size(elt_con)=es
 *  ctxt |- r1 : B4
 *  ctxt |- r2 : elt_con
 *  ------------------------------------------
 *  ctxt |- Aupd gop1,es,r1,r2,genop2 : ctxt
 *
 *  Exception: if elt_con is B(1|2|4|8) then ctxt |- r2 : B4
 *)

let verify_Aupd ctxt gop1 es r1 r2 genop2 =
  let (celt,v) = verify_array ctxt gop1 es r1 genop2 in
  if v<>Write & v<>ReadWrite then inst_form ctxt "Aupd: field not writeable";
  (match (whnorm ctxt celt).rcon with
    Cprim (PCbytes _) -> 
      leqcon ctxt (get_reg_con ctxt r2) cbyte4
  | _ -> 
      leqcon ctxt (get_reg_con ctxt r2) celt);
  ctxt
;;

(* ctxt |- r : exn           ctxt |- gop : exnname(c) 
 * ctxt |- lc : code(G)      ctxt |- ctxt.gamma <= G
 * --------------------------------------------------
 * ctxt |- Bexn r,gop,lc : ctxt[r:^*[(exnname c)^r,c]
 *
 * Operationally, Bexn extracts the exception name from an exception
 * packet in r, compares it to the exception name in gop, and if they're
 * _not_ equal, branches to the (possibly coerced) label lc.  If they
 * are equal, then we fall through and refine the type of r so that
 * it's a pair of an exnname(c) * c value
 *
 * Because of macro gop must be either an address or a register.
 *)

let verify_Bexn add_block ctxt r gop lc =
  reg_or_addr ctxt gop;
  leqcon ctxt (get_reg_con ctxt r) pcexn;
  let cname = whnorm ctxt (genop_con false ctxt gop) in
    match cname.rcon with
      Capp (cexnn,c) ->
        leqcon ctxt cexnn pcexnname;
        (match coerce_label_con_whrcon_opt ctxt lc with
          None -> 
          (* there's no type on the label l, so we must type-check that
	   * block under the current context.  Hence, the block and context
	   * are added to a work list.
	   *)
            add_block ctxt (get_raw lc)
        | Some(Ccode gamma') ->
            reg_state_leq ctxt (get_register_state ctxt) gamma'
        | _ -> inst_form ctxt "Bexn: label is not code");
        let rc = cprod_b [cfield cname Read; c] in
        add_reg ctxt r rc
    | _ -> inst_form ctxt "Bexn: gop not an exnname"; raise Talfail
;;

(* In the branch on tags instructions we need to compare tag values according
 * to a condition, this function does this for us
 *)

let interpret_condition ctxt cc =
  match cc with
    Above -> (>)
  | AboveEq -> (>=)
  | Below -> (<)
  | BelowEq -> (<=)
  | Eq -> (=)
  | NotEq -> (!=)
  | _ ->
      inst_form ctxt "tag comparison: condition code is invalid"; raise Talfail
;;

(* r is either a non-pointer integer or else a pointer,
 * ie has type Chptr (is,co)
 * The "instruction" explodes into the following code:
 *    
 *     cmp r,i
 *     jcc lc
 *
 * The is are split into is1 and is2 according to whether they compare with i
 * or not.  jcc lc is checked with r:Chptr(is2,co2) and the fallthru context
 * has r:Chptr(is1,co1).  The only tricky part is how co1,co2 is computed.
 * Cases:
 *  (i)   i is less than the smallest possible pointer.
 *          co is put into the branch where min_pointer_integer compares.
 *  (ii)  i is a non-pointer integer greater than smallest possible pointer.
 *          if condition is equal or not equal put co in the appropriate branch
 *          otherwise put co in both branches.
 *  (iii) i is a pointer integer.
 *          put co in both branches.
 *
 *  ctxt |- lc : Ccode(G)
 *  ctxt |- ctxt.gamma [r: Chptr(is2,co2)] <= G
 *  --------------------------------------------------
 *  ctxt |- Btagi r,i,lc,cc : ctxt [r: Chptr(is1,co1)]
 *)

let split_condition_tag ctxt cc i st co =
  let f = interpret_condition ctxt cc in
  let condition x = f x i in
  let rec split l matches not_matches =
    match l with
      [] -> (List.rev matches,List.rev not_matches)
    | h::t ->
   	if condition h then split t (h::matches) not_matches
   	else split t matches (h::not_matches) in
  let (tag_matches,tag_not_matches) = split st [] [] in
  let (svt_matches,svt_not_matches) = 
    if i<min_pointer_integer then
      if condition min_pointer_integer then (co,None) else (None,co)
    else if is_non_pointer_integer i then
      (match cc with
   	Eq -> (None,co)
      |	NotEq -> (co,None)
      |	_ -> (co,co))
    else (co,co) in
  (whcon (Chptr (tag_matches,svt_matches)),
   whcon (Chptr (tag_not_matches,svt_not_matches)))
;;
    
let verify_Btagi add_block ctxt r i lc cc =
  match (whnorm ctxt (get_reg_con ctxt r)).rcon with
    Chptr (is,co) ->
      let (sum_branch,sum_fallthru) = split_condition_tag ctxt cc i is co in
      (match coerce_label_con_whrcon_opt ctxt lc with
	Some(Ccode gamma') ->
	  reg_state_leq ctxt
	    (get_register_state (add_reg ctxt r sum_branch)) gamma'
      | None -> 
          (* there's no type on the label l, so we must type-check that
	   * block under the current context.  Hence, the block and context
	   * are added to a work list.
	   *)
	  add_block (add_reg ctxt r sum_branch) (get_raw lc)
      | _ -> inst_form ctxt "Btagi: label not code");
      add_reg ctxt r sum_fallthru
  | _ -> inst_form ctxt "Btagi: register doesn't contain sum"; raise Talfail
;;

(* The immediate i is in the range [0..255].  r is a pointer to a tuple
 * where the first component is an integer in the range [0..255] and has type
 * Sum{sum_tags,vt=Some(Variant[(i1,fs1),...,(in,fsn)])} in the current 
 * context.  The instruction explodes into:
 *    
 *     cmp r[0],i
 *     jcc lc
 *
 * cc is:      lc assigns r:                     fall through assigns r:
 * -------- -----------------------------     --------------------------------
 * Above    Sum{[(j1,fsj1),...,(jm,fsjm)]}    Sum{vt=[(k1,fsk1),...(kp,fskp)]}
 *    where each jl,kl in [i1,...,in] ^ jl > i and kl <= i
 * AboveEq  Sum{[(j1,fsj1),...,(jm,fsjm)]}    Sum{vt=[(k1,fsk1),...(kp,fskp)]}
 *    where each jl,kl in [i1,...,in] ^ jl >= i and kl < i
 * Below    Sum{[(j1,fsj1),...,(jm,fsjm)]}    Sum{vt=[(k1,fsk1),...(kp,fskp)]}
 *    where each jl,kl in [i1,...,in] ^ jl < i and kl >= i
 * BelowEq  Sum{[(j1,fsj1),...,(jm,fsjm)]}    Sum{vt=[(k1,fsk1),...(kp,fskp)]}
 *    where each jl,kl in [i1,...,in] ^ jl <= i and kl > i
 *
 * where we've dropped off the tag, Some, Variant etc. to fit this on the
 * screen 
 *)

(* r is a pointer that at offset offset has a Csum cs.  The instruction expands
 * to:
 *     cmp [r+offset],i
 *     jcc lc
 *
 * Thus we replace Csum cs with Csum cs1 and Csum cs2 in the
 * fallthru and jcc branches respectively.  Each of the cs starts with a tag
 * which is compared with i according to cc and this determines whether it goes
 * in cs1 or cs2.
 *
 *  ctxt |- r : c
 *  ctxt |- c offsest i : Csum cs
 *  ctxt |- lc : Ccode G
 *  ctxt |- ctxt.gamma [r: c[i=Csum cs1]] <= G
 *  ----------------------------------------------------------
 *  ctxt |- Btagvar r,offset,i,lc,cc : ctxt [r: c[i=Csum cs2]]
 *)

let split_sum ctxt offset i cc c =
  let (f,c) = get_mem_offset ctxt c offset None in
  match (whnorm ctxt c).rcon with
    Csum cs ->
      let g = interpret_condition ctxt cc in
      let condition c =
 	g (sum_index (fun () -> inst_form ctxt "Btarvar: bad sum tag") c) i in
      let rec split l matches not_matches =
    	match l with
	  [] -> (List.rev matches,List.rev not_matches)
    	| c::t ->
 	    if condition c then split t (c::matches) not_matches
    	    else split t matches (c::not_matches) in
      let cs1,cs2 = split cs [] [] in
      (f (csum cs1),f (csum cs2))
  | _ -> inst_form ctxt "Btarvar: not a sum"; raise Talfail
;;

let verify_Btagvar add_block ctxt r offset i lc cc =
  let ctxt1,ctxt2 =
    match (whnorm ctxt (get_reg_con ctxt r)).rcon with
      Chptr (_::_,_) ->
 	inst_form ctxt "Btagvar: pointer has tags"; raise Talfail
    | Chptr ([],Some c) ->
	let nc1,nc2 = split_sum ctxt offset i cc c in
	(add_reg ctxt r (cptr nc1),add_reg ctxt r (cptr nc2))
    | Csptr c ->
      	let f = valid_stack_con ctxt c in
      	let nc1,nc2 = split_sum ctxt offset i cc c in
      	let ctxt1 = add_reg ctxt r (csptr nc1) in
	let ctxt1 = add_reg ctxt1 Esp (csptr (f nc1)) in
	let ctxt2 = add_reg ctxt r (csptr nc2) in
	let ctxt2 = add_reg ctxt2 Esp (csptr (f nc2)) in
	(ctxt1,ctxt2)
    | _ -> inst_form ctxt "Btagvar: nonpointer register"; raise Talfail in
  (match coerce_label_con_whrcon_opt ctxt lc with
    Some(Ccode gamma) ->
      reg_state_leq ctxt (get_register_state ctxt1) gamma
  | None -> 
       (* there's no type on the label l, so we must type-check that
        * block under the current context.  Hence, the block and context
	* are added to a work list.
	*)
      add_block ctxt1 (get_raw lc)
  | _ -> inst_form ctxt "Btagvar: label not code");
  ctxt2
;;

(* Coerce: coerce register
 * N.B. the second condition may be redundant
 *
 * ctxt |- coerce(r) : c    ctxt |- c : K4byte
 * -------------------------------------------
 * ctxt |- Coerce coerce(r) : ctxt[r:c]
 *)

let verify_Coerce ctxt (r,_ as arg) =
  restore_cc ctxt;
  let c = coerce_reg_con ctxt arg in
  kindleq ctxt (con_kind ctxt c) k4byte;
  add_reg ctxt r c
;;

(*  ctxt |- ma : c
 *  ctxt |- sizeof(c) = i
 *  ---------------------------------------------------------
 *  ctxt |- Malloc i,ma : ctxt/(Ebx,Ecx,Edx,Esi,Edi)+[Eax:^c]
 *)

(* raw bytes and junk are already initialised everything else is not *)
let malloc_variance c =
  match c.rcon with
    Cprim (PCbytes _) | Cprim (PCjunk _) -> ReadWrite
  | _ -> Uninit
;;

let rec mallocarg_con ctxt s ma =
  match ma with
    Mprod mas ->
      let (cs,s) = foldmap_left (mallocarg_con ctxt) s mas in
      (cprod cs,s)
  | Mfield c ->
      let (k,c) = check ctxt c in
      let c = whnorm ctxt c in
      kindleq ctxt k Ktype;
      (cfield c (malloc_variance c),s+$(sizeof ctxt c))
  | Mbytearray (scale,size) ->
      (carray (pcint size) (cfield (pcbytes scale) ReadWrite),
       s+$(scale_to_int32 scale)*$size)
  | Mexnname _ -> inst_form ctxt "malloc: nested exnname"; raise Talfail
;;

let verify_Malloc ctxt i ma =
  if i <$ i32_0 then inst_form ctxt "malloc of negative value";
  let c =
    match ma with
      Mexnname c ->
	let (k,c) = check ctxt c in
	kindleq ctxt k Kmem;
	if i <>$ i32_4 then 
	  inst_form ctxt "malloc: exnname has size 4";
	capp pcexnname c
    | _ ->
      	let (c,s) = mallocarg_con ctxt i32_0 ma in
      	if i <>$ s then inst_form ctxt "malloc: size mismatch";
	cptr c in
  let rs = get_register_state ctxt in
  let rs = rs_del_regs rs [Eax;Ebx;Ecx;Edx;Esi;Edi] in
  set_register_state ctxt (rs_set_reg rs Eax c)
;;

(* verify gc is an exists, and introduce the new type variable a into
 * scope, as well as moving the value under the existential into the
 * register r.  Also, it's necessary to alpha-convert a so that it
 * is unique and does not conflict with something already in the
 * context...
 *)

let verify_Unpack ctxt a r gc =
  restore_cc ctxt;
  match (whnorm ctxt (coerce_genop_con false ctxt gc)).rcon with
    Cexist(a',k,c') ->
      let a_con = whcon(Cvar a) in
      let c = subst a_con a' c' in
      let ctxt = add_var ctxt a k in
      kindleq ctxt (con_kind ctxt c) k4byte;
      let ctxt = add_reg ctxt r c in
      ctxt
  | _ -> inst_form ctxt "Unpack: genop not an Exists"; raise Talfail
;;

(* This is just like a move.  We type-check this by finding the
 * type ctla of the TLA, and then give r this type, and type-check
 * it as if we're doing a MOV r,coerce([r+i]).  That is, conceptually
 * we're type-checking MOV r,TLA; MOV r,coerce([r+i]) which is essentially
 * how this is implemented.
 *)
let verify_Gettla ctxt r i coercion =
  let ctxt_temp1 = add_reg ctxt r (get_tla_con ctxt) in
  let ctxt_temp2 = verify_Mov ctxt_temp1 (Reg r) (Prjr((r,[]),i),coercion) in
  let c = get_reg_con ctxt_temp2 r in
  add_reg ctxt r c
;;

(* This is much trickier, as we want to allow an arbitrary "field" of
 * the TLA to have its type updated.  Hence, it's much like doing
 * MOV [TLA+i],r except that we want to update the type of the TLA
 * at field (i div 4) with the type of r.  
 *)
let verify_Settla ctxt i r coercion = 
  let c_source = whnorm ctxt (coerce_genop_con false ctxt (Reg r,coercion)) in
  let c_tla = whnorm ctxt (get_tla_con ctxt) in
  let error s = generate_error ctxt (Genop(s,Reg r)) in
  writeable_prj ctxt error c_tla PRns i c_source set_tla_con false
;;    

(* Cyclone *)

(* Auxiliary functions used for verifying fills in Cyclone.
** tp_con should be the con of a pointer to a template copy.
** hole is the label of the hole to fill in that copy.
** fill_con is the con of the value that will fill the hole.
** The return value will be the context with the hole removed.
*)
let verify_fill ctxt tp_con hole fill_con =
  begin
    let cyclone_con = Talctxt.get_cyclone_con ctxt in
    match tp_con.rcon,cyclone_con.rcon with
      Ctptr iv,
      Ctcons({rcon=Ctrgn(pre,post,t)},tl) ->
        let rec aux l =
          match l with
            [] -> (inst_form ctxt "verify_fill 2"; [])
          | (i,labels,holes)::ls ->
            if i<>iv then (i,labels,holes)::(aux ls)
            else
              let rec clobber_hole hs =
                 match hs with
                   [] -> (inst_form ctxt "verify_fill 3"; [])
                 | (h,h_con)::hs ->
                   if h<>hole then (h,h_con)::(clobber_hole hs)
                   else (leqcon ctxt fill_con h_con; hs)
              in (i,labels,clobber_hole holes)::ls
        in
        let t' = aux t in
        set_cyclone_con ctxt (whcon(Ctcons(whcon(Ctrgn(pre, post, t')), tl)))
    | _ -> (inst_form ctxt "verify_fill 1"; ctxt)
  end

let verify_fill_jump ctxt r1 l1a l1b r2 l2a l2b =
  begin
    (* l1a and l2a are template labels, needed by MASM;
    ** if we stick with MASM we should check this. *)

    (* r2,l2a,l2b identify the target; find out its con *)
    match (get_reg_con ctxt r2).rcon, (get_cyclone_con ctxt).rcon with
      Ctptr iv,
      Ctcons({rcon=Ctrgn(pre,post,t)},tl) ->
        begin
          let rec aux l =
            match l with
              [] -> raise Not_found
            | (i,labels,holes)::ls ->
              if i=iv then List.assoc l2b labels
              else aux ls in
          try
            let fill_con = aux t in
            verify_fill ctxt (get_reg_con ctxt r1) l1b fill_con
          with Not_found ->
            (inst_form ctxt "verify_fill_jump 3"; ctxt)
        end
    | _ -> (inst_form ctxt "verify_fill_jump 1"; ctxt)
  end
(* End Cyclone *)

(*** Verify an instruction ***)

(* add_block is called whenever an instruction does a jump to a label
 * that has no type in the current context.
 *)
let verify_instr add_block ctxt i =
  let ctxt = set_cc ctxt CCnoinfo in
  match i with
  (* Generic x86 instructions *)
    ArithBin(ab,g1,g2) -> verify_ArithBin ctxt ab g1 g2
  | ArithUn(au,g) -> verify_ArithUn ctxt au g
  | ArithMD(amd,g) -> verify_ArithMD ctxt amd g
  | ArithSR(sr,g,iopt) -> verify_ArithSR ctxt sr g iopt
  | Bswap(r) -> verify_Bswap ctxt r
  | Call(gc) -> verify_Call ctxt gc
  | Clc -> ctxt
  | Cmc -> ctxt
  | Cmovcc(c,r,gopt) -> verify_Cmovcc ctxt c r gopt
  | Cmp(g1,g2) -> verify_Cmp ctxt g1 g2
  | Conv(c) -> verify_Conv ctxt c
  | Imul3(r,g,i) -> verify_Imul3 ctxt r g i
  | Int i -> inst_form ctxt "interrupt unimplemented"; raise Talfail
  | Into -> inst_form ctxt "interrupt on overflow unimplemented"; raise Talfail
  | Jcc (c,lc) -> verify_Jcc add_block ctxt c lc
  | Jecxz lc -> verify_Jecxz add_block ctxt lc
  | Jmp gc -> verify_Jmp add_block ctxt gc
  | Lahf -> restore_cc ctxt; add_reg ctxt Eax cbyte4
  | Lea (r,g) -> verify_Lea ctxt r g
  | Loopd (lc,bo) -> verify_Loop add_block ctxt lc bo
  | Mov (gop,gcop) -> verify_Mov ctxt gop gcop
  | Movpart (se,gop1,p1,gop2,p2) -> verify_Movpart ctxt se gop1 p1 gop2 p2
  | Nop -> restore_cc ctxt; ctxt
  | Pop genop -> verify_Pop ctxt genop
  | Popad -> verify_Popad ctxt
  | Popfd -> verify_Popfd ctxt
  | Push gc -> verify_Push ctxt gc
  | Pushad -> verify_Pushad ctxt
  | Pushfd -> verify_Pushfd ctxt
  | Retn iopt -> verify_Retn ctxt iopt
  | Sahf -> leqcon ctxt (get_reg_con ctxt Eax) cbyte4; ctxt
  | Setcc (c,g) -> verify_Setcc ctxt c g
  | Shld (gop,r,iopt) -> verify_Shld_Shrd ctxt gop r iopt
  | Shrd (gop,r,iopt) -> verify_Shld_Shrd ctxt gop r iopt
  | Stc -> ctxt
  | Test (gop1,gop2) -> verify_Test ctxt gop1 gop2
  | Xchg (gop,r) -> verify_Xchg ctxt gop r
  (* TAL specific instructions *)
  | Asub (r1,gop1,es,r2,gop2) -> verify_Asub ctxt r1 gop1 es r2 gop2
  | Aupd (gop1,es,r1,r2,gop2) -> verify_Aupd ctxt gop1 es r1 r2 gop2
  | Bexn (r,gop,lc) -> verify_Bexn add_block ctxt r gop lc
  | Btagi (rc,i,lc,cc) -> verify_Btagi add_block ctxt rc i lc cc
  | Btagvar (rc,off,i,lc,cc) -> verify_Btagvar add_block ctxt rc off i lc cc
  | Coerce rc -> verify_Coerce ctxt rc
  | Comment _ -> restore_cc ctxt; ctxt
  | Fallthru cs -> restore_cc ctxt; raise (Fall_Thru (ctxt,cs))
  | Malloc (i,ma) -> verify_Malloc ctxt i ma
  | Unpack (a,r,gc) -> verify_Unpack ctxt a r gc
  | Gettla (r,(i,c)) -> verify_Gettla ctxt r i c
  | Settla (i,(r,c)) -> verify_Settla ctxt i r c
(* Cyclone *)
  | CgStart c ->
      begin
        let (k,c) = check ctxt c in
        kindleq ctxt k k4byte;
        set_cyclone_con ctxt
          (whcon(Ctcons(whcon(Ctrgn(c,Some c,[])),
                        get_cyclone_con ctxt)))
      end
  | CgDump (i1,r,i2) ->
      begin
        match (get_cyclone_con ctxt).rcon with
          Ctcons({rcon=Ctrgn(pre,post_opt,t)},tl) ->
            begin
              match (get_label_con ctxt i2).rcon with
                Ctmpl(beg_con,end_con_opt,labels,holes) ->
                  (match post_opt with
                     None -> ()
                   | Some post ->
                       leqcon ctxt post beg_con);
                  let ctxt0 = add_reg ctxt r (whcon(Ctptr i1)) in
                  set_cyclone_con ctxt0
                    (whcon(Ctcons(whcon(Ctrgn(pre,
                                              end_con_opt,
                                              (i1,labels,holes)::t)),
                                  tl)))
              | _ -> (inst_form ctxt "CGDUMP of non-template"; ctxt)
            end
        | _ -> (inst_form ctxt "CGDUMP with bad cg region"; ctxt)
      end
(* TO FIX: We don't check that holes and fills match up properly,
   that is, CgHole should match up with CgFill, and CgHoleBtagi should
   match up with CgFillBtagi.  We expect this won't be necessary in the
   new assembler (there will only be one kind of hole and fill).
   It's inconvenient to do now with MASM.
*)
  | CgHole (r,i1,i2) ->
      begin (* Hole i2 in template i1 *)
        match (get_label_con ctxt i1).rcon with
          Ctmpl(beg_con,end_con,labels,holes) ->
            begin
              try 
                let hole_con = List.assoc i2 holes in
                genop_write_at ctxt (Reg r) hole_con
              with Not_found ->
                (inst_form ctxt
                   "labels in cghole don't identify a hole in a template";
                 ctxt)
            end
        | _ -> (inst_form ctxt
                  "cghole second argument must be the label of a template";
                ctxt)
      end
  | CgHoleBtagi(rc,i,l,lc,cc) ->
      verify_Btagi add_block ctxt rc i lc cc
  | CgHoleBtagvar(rc,off,i,l,lc,cc) ->
      verify_Btagvar add_block ctxt rc off i lc cc
  | CgHoleJmp(l,(lab,c)) ->
      verify_Jmp add_block ctxt (Addr lab,c)
  | CgHoleJcc(cc,l,lc) ->
      verify_Jcc add_block ctxt cc lc
  | CgFill (r1,tmpl,hole,r2) ->
      begin
        (* tmpl is the template of the label, needed for MASM.  If we
        ** stick with MASM we should check this -- we don't right now. *)
        let tp_con = get_reg_con ctxt r1 in   (* template pointer *)
        let fill_con = get_reg_con ctxt r2 in (* value to fill hole *)
        verify_fill ctxt tp_con hole fill_con
      end
  | CgFillBtag(r1,l1a,l1b,r2,l2a,l2b) ->
      verify_fill_jump ctxt r1 l1a l1b r2 l2a l2b
  | CgFillJmp(r1,l1a,l1b,r2,l2a,l2b) ->
      verify_fill_jump ctxt r1 l1a l1b r2 l2a l2b
  | CgFillJcc(r1,l1a,l1b,r2,l2a,l2b) ->
      verify_fill_jump ctxt r1 l1a l1b r2 l2a l2b
  | CgForget i ->
      begin
        match (get_cyclone_con ctxt).rcon with
          Ctcons({rcon=Ctrgn(pre,post,t)},tl) ->
            if not(List.exists (fun (i',_,_) -> i=i') t)
            then (inst_form ctxt "cgforget 2"; ctxt)
            else
              let t' = List.concat
                         (List.map
                            (fun (i',labels,holes) ->
                              if i<>i' then [(i',labels,holes)]
                              else if List.length holes <> 0
                              then (inst_form ctxt "cgforget 3"; [])
                              else [])
                            t) in
              set_cyclone_con ctxt
                (whcon(Ctcons(whcon(Ctrgn(pre,
                                          post,
                                          t')),
                              tl)))
        | _ -> (inst_form ctxt "cgforget 1"; ctxt)
      end
  | CgAbort n ->
      begin
        let n = int32_to_int n in
        if n<0 then (inst_form ctxt "cgabort 1"; ctxt)
        else
          let rec aux n con =
            if n=0 then set_cyclone_con ctxt con
            else
              match con.rcon with
                Ctcons(_,con) -> aux (n-1) con
              | _ -> (inst_form ctxt "cgabort 2"; ctxt)
          in
          aux n (get_cyclone_con ctxt)
      end
  | CgEnd r ->
      begin
        match (get_cyclone_con ctxt).rcon with
          Ctcons({rcon=Ctrgn(pre,None,t)},tl) ->
            if List.exists (function (_,_,[]) -> false
                              | _ -> true) t
            then (inst_form ctxt "cgend 2"; ctxt)
            else
              add_reg (set_cyclone_con ctxt tl) r pre
        | _ -> (inst_form ctxt "cgend 1"; ctxt)
      end
(* End Cyclone *)
;;

(**********************************************************************)    
(* Code Blocks and Code Trees                                         *)
(**********************************************************************)

(* Add the code labels to psi:
 * Check and normalise the constructor and check it has kind K4byte
 * (if present).
 *)
let add_code_labels ctxt cbv =
  let aux ctxt (l,c,_) =
    let ctxt = 
      set_verify_ctxt (set_loc ctxt (Locc (l,-1))) "adding code labels" in
   (match c with
     None -> add_val ctxt l None
   | Some c -> 
     let (k,c') = check ctxt c in
     kindleq ctxt k k4byte; add_val ctxt l (Some c')) in
  vector_fold aux ctxt cbv
;;

(* We need to verify a code tree starting from a given label (with a type).
 * We keep a list, undone_tree_blocks, of code blocks that have yet to be
 * verified.  The list includes the label of the block, the instructions,
 * the index (in the code block vector) of the code block, and the ctxt
 * under which the instructions should be checked.  The index is used to
 * verify that branches to "untyped" labels are forward branches in order
 * to ensure termination (i.e., that we have no cycles.)
 *
 * We start by adding the appropriate context, index, label, and instructions
 * of the typed block.  We then verify each instruction in that block which
 * in turn may add more blocks to the undone_tree_blocks list (see verify_
 * instruction).  Special care must be taken when a block falls through to 
 * the next block.  
 *)
let verify_code_tree block_mapping cbv ctxt i
(* Cyclone *)
    post_check
(* End Cyclone *)
   =
  let (l,copt,insts) = cbv.(i) in
  let c = get_label_con ctxt l in
  let ctxt = set_loc ctxt (Locc (l,-1)) in
  let (vks,rs) = separate_fun_type ctxt c in
  let f ctxt (v,k) = add_var ctxt v k in
  let ctxt = List.fold_left f ctxt vks in
  let gamma = verify_gamma ctxt rs in
  let ctxt = set_register_state ctxt gamma in
  let undone_tree_blocks = ref [(ctxt,l,i,insts)] in
  let add_block current_index ctxt l = 
    let block_index = Dict.lookup block_mapping l in
    if current_index < block_index then
      let (_,_,insts) = cbv.(block_index) in
      undone_tree_blocks := (ctxt,l,block_index,insts)::(!undone_tree_blocks)
    else generate_error ctxt (Backward_branch l) in
  let verify_block (ctxt,l,current_index,insts) =
    let add_block = add_block current_index in
    let ctxt = set_verify_ctxt ctxt "verifying instructions" in
    let fti = ref 0 in
    (* Verify a vector of instructions.  "Normal" termination is handled
     * when a Terminal_Jmp exception is raised.  If the code falls through
     * to the next block, then we must check that:
     *  (i) the fall through is the last instruction of the block
     *  (ii) "jumping" to the next block is legal in the current context.
     * Note that it is now possible to fall through to the next block without
     * an explicit "Fallthru" instruction when the next block has no type.
     * It is also possible to explicitly Fallthru in this situation.  However,
     * If the next block is labelled with a type that has bound type 
     * variables, then an explicit Fallthru (with instantiation) is 
     * necessary.
     *)
    let rec inst_loop ctxt n i =
      let ctxt = set_loc ctxt (Locc (l,i)) in
      fti := i;
      if i = n then raise (Fall_Thru(ctxt,[])) else
      let ctxt = verify_instr add_block ctxt insts.(i) in
      inst_loop ctxt n (i+1) in
    try
      inst_loop ctxt (Array.length insts) 0
    with 
      Terminal_Jmp -> ()
    | Talfail -> ()
    | Fall_Thru(ctxt,cs) ->
	if !fti < (Array.length insts - 1) then
	  begin
	    generate_error ctxt (Inst_form "fall through in middle of block");
	    ()
	  end
    	else if current_index = (Array.length cbv - 1) then
	  begin
(* Cyclone *)
            match post_check with
              None ->
(* End Cyclone *)
                generate_error ctxt (Inst_form "falls off end of code"); ()
(* Cyclone *)
            | Some(None) -> ()
            | Some(Some post) ->
                let post =
	          List.fold_right (coercion_con ctxt)
                    (List.rev(List.map (fun x -> Tapp x) cs)) post in
                leqcon ctxt post (whcon (Ccode(get_register_state ctxt)));
                ()
(* End Cyclone *)
	  end
	else 
	  begin
	    let (l,_,_) = cbv.(current_index + 1) in
	    let lc = List.fold_left (fun gc c -> coerce gc (Tapp c))
		(raw (Addr l)) cs in
	    try verify_instr add_block ctxt (Jmp lc); ()
	    with 
	      Terminal_Jmp -> ()
	    | Talfail -> ()
	  end
  in let rec verify_blocks () = 
    (match !undone_tree_blocks with
      [] -> ()
    | b::rest -> (undone_tree_blocks := rest; verify_block b; verify_blocks()))
  in verify_blocks()

(* Verify each of the code blocks.  We need a map from labels to integer
 * indices so that verify_code_tree can easily determine when a branch is
 * forward or not.  All of the smarts regarding fallthrus are now
 * encapsulated in the code trees.
 *
 * Note that we only verify code trees that start with a typed label.
 * Hence, the verifier no longer has the property that it can detect
 * dead code.  In particular, completely random code will type-check
 * as long as none of the labels have types (!) because those labels
 * cannot be exported or jumped to etc.
 *)
let verify_code_blocks ctxt cbv
(* Cyclone *)
   post_check
(* End Cyclone *)
   =
  (* used to map labels to the block index in cbv *)
  let block_mapping : (identifier,int) Dict.dict = 
    let rec add_label i d = 
      if i >= Array.length(cbv) then d
      else let (l,_,_) = cbv.(i) in 
      add_label (i+1) (Dict.insert d l i)
    in add_label 0 (Dict.empty id_compare) in
  let ctxt = set_loc ctxt Loctop in
  let ctxt = set_verify_ctxt ctxt "verifying code blocks" in
  (* specialize verify_code_tree to the current block mapping, 
   * code-block vector, and outer context.
   *)
  let verify_ctree i = verify_code_tree block_mapping cbv ctxt i
(* Cyclone *)
      post_check
(* End Cyclone *)
  in
  (* For each block, if the block has a type then it's the 
   * beginning of a code-tree to be verified.  Otherwise, the
   * block is skipped.  *)
  for i = 0 to Array.length(cbv) - 1 do
    match cbv.(i) with
      (_,None,_) -> ()
    | (l,Some c,insts) -> verify_ctree i
  done

(**********************************************************************)    
(* Data Blocks                                                        *)
(**********************************************************************)

(* Infer the type of a data label:
 * For now just look at last coercion and grab any obvious type otherwise fail
 *)
let infer_data_type ctxt l dis clist =
  match clist with
  | (Pack (_,c))::_ -> c
  | (Roll c)::_ -> c
  | (Tosum c)::_ -> c
  | (RollTosum c)::_ -> c
  | Toexn :: _ -> pcexn
  | (Subsume c)::_ -> c
  | _ -> generate_error ctxt (Data_form "needs label type"); raise Talfail
;;

(* Add the data labels to psi:
 * Check and normalise the constructor and check it has kind K4byte
 *)
let add_data_labels ctxt dbv =
  let aux ctxt (l,co,(dis,clist)) =
    let ctxt =
      set_verify_ctxt (set_loc ctxt (Locd (l,-1))) "adding data labels" in
    let c = 
      match co with
	None -> infer_data_type ctxt l dis clist
      |	Some c -> c in
    let (k,c') = check ctxt c in
    kindleq ctxt k k4byte; add_val ctxt l (Some c') in
  vector_fold aux ctxt dbv
;;

let rec myrep i n l =
  if n=0 then l else myrep i (n-1) (i::l)
;;

let verify_data_items ctxt dis =
  let rec aux saved cur dis =
    match dis with
      [] ->
	(match saved with
	  [] -> List.rev cur
	| s::ss -> aux ss ((cprod (List.rev cur))::s) dis)
    | (Dlabel cl)::dis ->
 	aux saved ((cfield (coerce_label_con ctxt cl) ReadWrite)::cur) dis
    | (Dbytes s)::dis ->
	aux
	  saved 
	  (myrep (cfield (pcbytes Byte1) ReadWrite) (String.length s) cur)
	  dis
    | (D2bytes _)::dis ->
	aux saved ((cfield (pcbytes Byte2) ReadWrite)::cur) dis
    | (D4bytes ci)::dis ->
	let aux' ctxt i = prcon (Csing (pcint i)) in
	aux saved ((cfield (coerce_con aux' ctxt ci) ReadWrite)::cur) dis
    | (Djunk)::dis ->
	aux saved ((cfield (pcjunk i32_4) ReadWrite)::cur) dis
    | (Dexnname _)::dis ->
      	generate_error ctxt (Data_form "Dexnname not allowed"); raise Talfail
    | (Dup)::dis -> aux (cur::saved) [] dis
    | (Ddown)::dis ->
	(match saved with
	  [] ->
	    generate_error ctxt (Data_form "too many tal_ends"); raise Talfail
	| s::ss -> aux ss ((cprod (List.rev cur))::s) dis) in
  cprod (aux [] [] dis)
;;

let verify_data_block ctxt (l,co,(dis,clist)) = 
  let ctxt =
    set_verify_ctxt (set_loc ctxt (Locd (l,-1))) "verifying data blocks" in
  let c1 =
    match dis,clist with
      [Dexnname c],[] -> 
	let (k,c') = check ctxt c in
    	kindleq ctxt k Kmem;
 	capp pcexnname c'
    | _,_ ->
	let ctxt = set_verify_ctxt ctxt "verifying data items" in
	let c = verify_data_items ctxt dis in
	List.fold_right (coercion_con ctxt) clist (cptr c) in
  match co with
    None -> c1
  | Some c2 -> let (_,c2) = check ctxt c2 in leqcon ctxt c1 c2; c2
;;

let verify_data_blocks ctxt dbv =
  for i=0 to Array.length dbv - 1 do
    try 
      verify_data_block ctxt dbv.(i); ()
    with Talfail -> ()
  done
;;

(* Cyclone *)

(**********************************************************************)    
(* Templates                                                          *)
(**********************************************************************)

(* Add the template labels to psi:
 * Check and normalise the constructor and check it has kind K4byte
 *)
let add_template_labels ctxt templatev =
  let aux ctxt (template_begin_label,
                template_end_label, (* Ignored by verifier, used by MASM *)
                c,
                cbs) =
    let ctxt =
      set_verify_ctxt
        (set_loc ctxt (Locc (template_begin_label,-1)))
        "adding templates" in
    let (k,c') = check ctxt c in
    kindleq ctxt k k4byte;
    (* Gather actual labels and holes from body of template *)
    let labels1 =
      List.concat
        (List.map
           (function (l,Some c,_) -> [(l,c)]
             | _ -> [])
           cbs) in
    let holes1 = 
      List.concat
        (List.map
           (fun (_,_,is) -> 
              List.concat(
                List.map
                  (fun i ->
                     match i with
                       CgHole(r,lt,lh) -> [lh]
                     | CgHoleBtagi(reg,i,temp,(hole,c),cc) -> [hole]
                     | CgHoleBtagvar(reg,i1,i2,temp,(hole,c),cc) -> [hole]
                     | CgHoleJmp(temp,(hole,c)) -> [hole]
                     | CgHoleJcc(cc,temp,(hole,c)) -> [hole]
                     | _ -> [])
                  (Array.to_list is)))
           cbs) in
    begin
      match c'.rcon with
        (* Extract the labels and holes from the template type *)
        Ctmpl(_,_,labels2,holes2) ->
          begin
            (* Make sure the actual labels of the template match up with
               the labels in the type of the template *)
            (try
              List.iter2
                (fun (l1,c1) (l2,c2) ->
                   if l1<>l2 then
                     inst_form ctxt
                       "labels in the template type and body don't match";
                   let (k1,c1) = check ctxt c1 in
                   (* c2 was checked before, but now we need to compare
                   ** it to c1. *)
                   let (k2,c2) = check ctxt c2 in
                   kindeq ctxt k1 k2;
                   eqcon ctxt c1 c2)
                labels1
                labels2;
            with Invalid_argument _ ->
              inst_form ctxt
                "labels in the template type and body don't match");

            (* Check that each hole in the body of the template appears
            ** in the type of the template.  The kind of each hole in
            ** the template type has been checked already; its type
            ** will be checked later. *)
            try
              List.iter2
                (fun h1 (h2,c2) ->
                  if h1<>h2 then
                    inst_form ctxt
                      "holes in the template type and body don't match")
                holes1
                holes2;
            with Invalid_argument _ ->
              inst_form ctxt
                "holes in the template type and body don't match"
          end
      | _ -> inst_form ctxt "template does not have template type"
    end;
    add_val ctxt template_begin_label (Some c')
  in
  vector_fold aux ctxt templatev
;;

let verify_template ctxt (l,_,_,cbs) =
  let ctxt = set_loc ctxt Loctop in
  let cbv = Array.of_list cbs in
  (* CAREFUL: get template_con from ctxt, because add_templates expands
  ** any type abbrevs before putting it in ctxt. *)
  let template_con = get_label_con ctxt l in
  (* Get the pre- and post-conditions from the template type.  Add the
     labels and holes given by the template type to the context; note
     that this ensures that the labels and holes are distinct. *)
  let (pre,post_opt,ctxt) =
    match template_con.rcon with
      Ctmpl(pre,post_opt,labels,holes) ->
        (pre,
         post_opt,
         List.fold_left
           (fun ctxt (l,c) -> add_val ctxt l (Some c))
           ctxt
           (labels@holes))
    | _ ->
      begin
        inst_form ctxt "template does not have template type";
        raise Talfail
      end
  in
  verify_code_blocks ctxt cbv (Some(post_opt));
  (* Check that precondition holds of first label *)
  try
    let (_,first_label_con_opt,_) = cbv.(0) in
    match first_label_con_opt with
      None ->
        inst_form ctxt "first label of template does not have a type";
        raise Talfail
    | Some con -> 
        let (k,c) = check ctxt con in
        kindleq ctxt k k4byte;
        leqcon ctxt c pre
  with Invalid_argument _ -> (); (* template is empty *)
  ()
;;

let verify_templates ctxt tv =
  for i=0 to Array.length tv - 1 do
    try
      verify_template ctxt tv.(i); ()
    with Talfail -> ()
  done
;;
(* End Cyclone *)

(**********************************************************************)    
(* Interfaces/Implementations                                         *)
(**********************************************************************)

type ref2int = int_ref -> tal_int

(*** Type Abbreviation Processing ***)

let no_abbrevs = Dict.empty id_compare;;

let process_abbrev abbrevs (l,c) =
  Dict.insert abbrevs l (substs abbrevs c)
;;

(*** Get the interfaces being imported/exported and compute their abbrevs ***)

let process_impexp ref2int impexpref =
  let int = ref2int impexpref in
  let abbrevs =
    Array.fold_left process_abbrev no_abbrevs int.int_abbrevs in
  (abbrevs,int)
;;

let process_impexps ref2int impexprefs =
  Array.map (process_impexp ref2int) impexprefs
;;

(*** For building phi from con blocks and imported cons ***)

let add_con_blocks_l ctxt lkcs =
  let aux ctxt (l,k,_) =
    add_con (set_loc ctxt (Loccon l)) l k in
  List.fold_left aux ctxt lkcs
;;

let add_con_blocks ctxt lkcs =
  let aux ctxt (l,k,_) =
    add_con (set_loc ctxt (Loccon l)) l k in
  Array.fold_left aux ctxt lkcs
;;

let add_importexport_cons ctxt (_,int) = add_con_blocks ctxt int.int_cons;;

(*** For verifing the con defs used in term level processing ***)

let verify_int_con_def (ctxt,icons) (l,k,cd) =
  let ctxt = set_loc ctxt (Loccon l) in
  let cd =
    match cd with
      AbsCon -> cd
    | BoundCon c ->
	let (k',c') = check_whnorm ctxt c in
	kindleq ctxt k' k;
	BoundCon c'
    | ConcCon c ->
      	let (k',c') = check_whnorm ctxt c in
      	kindleq ctxt k' k;
      	ConcCon c' in
  (add_con_def ctxt l cd,(l,k,cd)::icons)
;;

let verify_import_con_defs (ctxt,icons) (abbrevs,int) =
  let ctxt = set_abbrevs ctxt abbrevs in
  Array.fold_left verify_int_con_def (ctxt,icons) int.int_cons
;;
  
let verify_con_block ctxt (l,k,c) =
  let ctxt = set_loc ctxt (Loccb l) in
  let (k',c') = check_whnorm ctxt c in
  kindleq ctxt k' k;
  add_con_def ctxt l (ConcCon c')
;;

(*** Building psi ***)

let add_imported_vals (ctxt,ivals) (l,c) =
  let ctxt = set_loc ctxt (Locval l) in
  let (k,c) = check_whnorm ctxt c in
  kindleq ctxt k k4byte;
  (add_val ctxt l (Some c),(l,c)::ivals)
;;

let add_import_vals (ctxt,ivals) (abbrevs,int) =
  let ctxt = set_abbrevs ctxt abbrevs in
  Array.fold_left add_imported_vals (ctxt,ivals) int.int_vals
;;

(*** Verifing Exports ***)

let verify_exports ref2int ctxte ctxti icons ivals tal_imp =
  let exps = process_impexps ref2int tal_imp.exports in
  (* Build context to check exports in *)
  let ctxte = add_con_blocks_l ctxte icons in
  let ctxte = Array.fold_left add_importexport_cons ctxte exps in
  (* Check exported constructors *)
  let f ctxte econs (l,k,cd as lkcd) = 
    let ctxte = set_loc ctxte (Loccon l) in
    let ctxti = set_loc ctxti (Loccon l) in
    let g (l',_,_) = l=l' in
    if not (vector_exists g tal_imp.con_blocks) then
      generate_error ctxte Doesnt_export;
    let lkcd =
      match cd with
      	AbsCon ->
 	  kindleq ctxti (get_label_kind ctxti l) k; lkcd
      | BoundCon c ->
	  let (k1,c1) = check_whnorm ctxte c in
	  kindleq ctxti k1 k;
	  (match get_label_def ctxti l with
	    AbsCon | BoundCon _ -> 
	      (* This shouldn't happen as conblocks are added concrete *)
	      failwith "Talverify.verify_exports - internal error"
	  | ConcCon c2 ->
	      leqcon ctxti c2 c1);
	  (l,k,(BoundCon c1))
      | ConcCon c ->
 	  let (k1,c1) = check_whnorm ctxte c in
	  kindleq ctxti k1 k;
	  (match get_label_def ctxti l with
	    AbsCon | BoundCon _ ->
	      (* This shouldn't happen as conblocks are added concrete *)
	      failwith "Talverify.verify_exports - internal error"
	  | ConcCon c2 ->
	      eqcon ctxti c2 c1);
	  (l,k,(ConcCon c1)) in
    lkcd::econs in
  let aux econs (abbrevs,int) =
    Array.fold_left (f (set_abbrevs ctxte abbrevs)) econs int.int_cons in
  let econs = List.rev (Array.fold_left aux [] exps) in
  (* Check exported labels *)
  let f ctxte evals (l,c) =
    let ctxte = set_loc ctxte (Locval l) in
    let ctxti = set_loc ctxti (Locval l) in
    let (k1,c1) = check_whnorm ctxte c in
    kindleq ctxte k1 k4byte;
    let g (l',_,_) = l=l' in
    if not (vector_exists g tal_imp.code_blocks)
 	& not (vector_exists g tal_imp.data_blocks) then
      generate_error ctxte Doesnt_export;
    leqcon ctxti (get_label_con ctxti l) c1;
    (l,c1)::evals in
  let aux evals (abbrevs,int) =
    Array.fold_left (f (set_abbrevs ctxte abbrevs)) evals int.int_vals in
  let evals = List.rev (Array.fold_left aux [] exps) in
  {it_cons=econs; it_vals=evals}
;;

(*** Verifing Implementations ***)

let verify_imp ref2int ctxt0 tal_imp =
  (* Get imported interface *)
  let imps = process_impexps ref2int tal_imp.imports in
  (* Build phi *)
  let ctxt = Array.fold_left add_importexport_cons ctxt0 imps in
  let ctxt = add_con_blocks ctxt tal_imp.con_blocks in
  (* Process Abbrevs *)
  let impabbrevs =
    Array.fold_left process_abbrev no_abbrevs tal_imp.imp_abbrevs in
  let abbrevs =
    Array.fold_right Dict.update (Array.map fst imps) impabbrevs in
  (* Process label constructor definitions *)
  let (ctxt,icons) = Array.fold_left verify_import_con_defs (ctxt,[]) imps in
  let ctxt = set_abbrevs ctxt abbrevs in
  let ctxt = vector_fold verify_con_block ctxt tal_imp.con_blocks in
  (* Build psi *)
  let (ctxt,ivals) = Array.fold_left add_import_vals (ctxt,[]) imps in
  let ctxt = set_abbrevs ctxt abbrevs in
  let ctxt = add_code_labels ctxt tal_imp.code_blocks in
  let ctxt = add_data_labels ctxt tal_imp.data_blocks in
(* Cyclone *)
  let ctxt = add_template_labels ctxt tal_imp.templates in
  (* Check templates *)
  verify_templates ctxt tal_imp.templates;
(* End Cyclone *)
  (* Check code blocks *)
  verify_code_blocks ctxt tal_imp.code_blocks
(* Cyclone *)
    None
(* End Cyclone *)
    ;
  (* Check data blocks *)
  verify_data_blocks ctxt tal_imp.data_blocks;
  (* Check exports *)
  let ctxte = set_verify_ctxt ctxt0 "verifying exports" in
  let ctxt = set_verify_ctxt ctxt "verifying exports" in
  let icons = List.rev icons and ivals = List.rev ivals in
  let ext = verify_exports ref2int ctxte ctxt icons ivals tal_imp in
  ({it_cons=icons; it_vals=ivals},ext)
;;

(**********************************************************************)    
(* EOF: talverify.ml                                                  *)
(**********************************************************************)
