(**********************************************************************)
(* (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;;
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 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,(whnorm ctxt c2).rcon with
		Cfield (c1,Read),Cfield (c2,Read) ->
		  (match (whnorm ctxt c1).rcon with
		    Capp (c1,cexn) ->
		      (match (whnorm ctxt c1).rcon with
			Cprim PCexnname ->
			  leqcon ctxt c2 cexn
		      |	_ -> error "toexn: first component not an exnname")
		  | _ -> error "toexn: first component not an exnname")
	      |	_ -> error "toexn: components not fields")
	  | _ -> error "toexn: not a product")
      |	_ -> error "toexn: not a product");
      pcexn
  | Toarray (offset,depth) ->
      let ctxt = set_verify_ctxt ctxt "toarray coercion" in
      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 [] -> f1 (f2 (carray (pcint 0) c))
      |	Cprod (c1::cs) ->
	  List.iter (fun c2 -> eqcon ctxt c1 c2) cs;
	  f1 (f2 (carray (pcint (List.length cs + 1)) c1))
      |	_ -> 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;;

(*** 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; cbyte4
  | Tag i ->
      if w then generate_error ctxt Readonly;
      (* try to get some sharing out of common tags *)
      if i < (Array.length tag_cons) then tag_cons.(i)
      else 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 *)

(* Returns the new type *)
let writeable_prj ctxt error c pr i con upd =
  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;
	  leqcon ctxt con c;
	  if v=Uninit then
	    upd ctxt (cptr (f (cfield c ReadWrite)))
	  else
	    ctxt
      | _ -> 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; 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
  | 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)
  | _ -> 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))
  | Tag _ -> generate_error ctxt (Genop ("operand is tag",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
  | Tag _ -> false
  | Reg _ -> false
  | Addr _ -> false
  | Prjr (_,_) -> true
  | Prjl (_,_) -> true
;;

(* Is operand register or address? *)
let reg_or_addr ctxt g =
  match g with
    Immed _ | Tag _ | 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);;

(************************************************************************)
(* 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 ->
	let cstk = current_stack_con ctxt in
	let cstk = if n=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
    valid_binops ctxt genop1 genop2;
    match (whnorm ctxt (genop_con true ctxt genop1)).rcon with
      (* A normal binop *)
      Cprim (PCbytes Byte4) ->
	leqcon ctxt (genop_con false ctxt genop2) cbyte4; ctxt
      (* 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 =
  leqcon ctxt (genop_con true ctxt genop) cbyte4;
  ctxt
;;

(* 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[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 ctxt 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 true ctxt genop) cbyte4;
  (match iopt with
    Some _ -> ()
  | None -> leqcon ctxt (get_reg_con ctxt Ecx) cbyte4);
  ctxt
;;

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

let verify_Bswap ctxt reg = eqcon ctxt cbyte4 (get_reg_con ctxt reg); ctxt;;

(* 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 =
  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 = 
  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.
 * 
 * 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;
  eqcon ctxt (genop_con false ctxt genop1) (genop_con false ctxt genop2);
  ctxt
;;

(* ctxt |- Eax : byte4
 * -----------------------
 * ctxt |- Cbw/Cwde : ctxt
 *
 * ctxt |- Eax : byte4
 * ---------------------------------
 * ctxt |- Cdq/Cwd : ctxt[Edx:byte4]
 *
 * ctxt |- gop : bytei
 * --------------------------------------------i is 16 or 8
 * ctxt |- Mov(s/z)x r,32,gop,i : ctxt[r:byte4]
 *)

let verify_Conv ctxt c =
  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
  match c with
    (Cbw | Cwde) -> 
      leqcon ctxt (get_reg_con ctxt Eax) cbyte4; ctxt
  | (Cdq | Cwd) -> 
      leqcon ctxt (get_reg_con ctxt Eax) cbyte4; add_reg ctxt Edx cbyte4
  | Movsx (r,s1,gop,s2) -> aux r s1 gop s2
  | Movzx (r,s1,gop,s2) -> aux r s1 gop s2
;;

(* 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
;;

(* ctxt |- lc : Ccode(g)    ctxt |- ctxt.gamma <= g
 * ------------------------------------------------
 * ctxt |- Jcc cc,lc : ctxt
 *)

let verify_Jcc ctxt lc =
  (match (whnorm ctxt (coerce_label_con ctxt lc)).rcon with
    Ccode rs -> reg_state_leq ctxt (get_register_state ctxt) rs
  | _ -> inst_form ctxt "Jcc: label for branch is not code");
  ctxt
;;

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

let verify_Jecxz ctxt lc =
  leqcon ctxt (get_reg_con ctxt Ecx) cbyte4; verify_Jcc ctxt lc
;;

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

let verify_Jmp ctxt gc =
  (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 =
  match g with
    Immed _ -> inst_form ctxt "Lea: immediate"; raise Talfail
  | Reg _ -> inst_form ctxt "Lea: register"; raise Talfail
  | Tag _ -> inst_form ctxt "Lea: tag"; 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<>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,0) -> add_reg ctxt r (coerce_label_con ctxt lc)
  | Prjl (_,_) -> inst_form ctxt "Lea: middle tuple pointer"; raise Talfail
;;
	      
(* 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 =
  valid_cbinops ctxt gop cgop;
  let c_source = coerce_genop_con false ctxt cgop in
  genop_write_at ctxt gop c_source
;;

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

let verify_Pop ctxt genop =
  let ctxt = verify_Mov ctxt genop (Prjr ((Esp,[]),0),[]) in
  let ctxt = verify_ArithBin ctxt Add (Reg Esp) (Immed 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 =
  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 : K4byte
 * ----------------------------------------
 * ctxt |- pushd gc : ctxt[Esp:sptr(c::c')]
 *)

(* Support for other sizes needed *)
let verify_Push ctxt gc =
  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 = 
  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 =
  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 =
  (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)
 *   ----------------------------------------------------1 in is,is<256
 *   ctxt |- Setcc gop : ctxt
 *)

let verify_Setcc ctxt cc gop =
  (match (whnorm ctxt (genop_con true ctxt gop)).rcon with
    Chptr (is,None) ->
      if not (List.mem 1 is) then inst_form ctxt "Setcc: no 1 tag";
      let check_tag i =
 	if (i land (lnot 255))<>0 then inst_form ctxt "Setcc: tag too big" in
      List.iter check_tag is
  | _ -> inst_form ctxt "Setcc: not sum of tags");
  ctxt
;;

(* 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 true ctxt gop) cbyte4;
  leqcon ctxt (get_reg_con ctxt r) cbyte4;
  (match iopt with
    Some _ -> ()
  | None -> leqcon ctxt (get_reg_con ctxt Ecx) cbyte4);
  ctxt
;;

(* 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;
  leqcon ctxt (genop_con false ctxt gop1) cbyte4;
  leqcon ctxt (genop_con false ctxt gop2) cbyte4;
  ctxt
;;

(* exchange gop1 and gop2.
 *   ctxt |- (gop1,gop2) valid binops  
 *   ctxt |- gop1 writeable  ctxt |- gop2 writeable
 *   ctxt |- gop1 : c   ctxt |- gop2 : c
 *   ----------------------------------------------
 *   ctxt |- Xchg gop1,gop2 : ctxt
 *)

let verify_Xchg ctxt gop1 r =
  let c1 = genop_con true ctxt gop1
  and c2 = get_reg_con ctxt r in
  eqcon ctxt c1 c2;
  ctxt
;;

(*** 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";
  kindleq ctxt (con_kind ctxt celt) k4byte;
  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]
 *
 *  NG - Works only for 4 byte element types.
 *)

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";
  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 : c1
 *  ctxt |- r2 : B4
 *  ------------------------------------------
 *  ctxt |- Aupd gop1,es,r1,r2,genop2 : ctxt
 *
 *  NG - Works only for 4 byte element types.
 *)

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";
  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:Prod<(exnname(c),Read,Init),(c,Read,Init)>]
 *
 * 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 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,
        (whnorm ctxt (coerce_label_con ctxt lc)).rcon with
    Capp (cexnn,c),Ccode gamma' ->
      leqcon ctxt cexnn pcexnname;
      reg_state_leq ctxt (get_register_state ctxt) gamma';
      let rc = cptr (cprod [cfield cname Read; cfield c Read]) in
      add_reg ctxt r rc
  | _ ->
      inst_form ctxt "Bexn: either r not an exn or 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 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 (whnorm ctxt (coerce_label_con ctxt lc)).rcon with
	Ccode gamma' ->
	  reg_state_leq ctxt
	    (get_register_state (add_reg ctxt r sum_branch)) gamma'
      | _ -> 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 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 (whnorm ctxt (coerce_label_con ctxt lc)).rcon with
    Ccode gamma ->
      reg_state_leq ctxt (get_register_state ctxt1) gamma
  | _ -> 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) =
  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_int scale)*size)
  | Mexnname _ -> inst_form ctxt "malloc: nested exnname"; raise Talfail
;;

let verify_Malloc ctxt i ma =
  if i < 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 k4byte;
	if i<>4 then inst_form ctxt "malloc: exnname has size 4";
	capp pcexnname c
    | _ ->
      	let (c,s) = mallocarg_con ctxt 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 =
  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
;;

(*** Verify an instruction ***)

let verify_instr ctxt i =
  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 ctxt lc
  | Jecxz lc -> verify_Jecxz ctxt lc
  | Jmp gc -> verify_Jmp ctxt gc
  | Lahf -> add_reg ctxt Eax cbyte4
  | Lea (r,g) -> verify_Lea ctxt r g
  | Loopd (lc,bo) -> verify_Jecxz ctxt lc (* For typing loop is jecxz *)
  | Mov (gop,gcop) -> verify_Mov ctxt gop gcop
  | Nop -> 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 ctxt r gop lc
  | Btagi (rc,i,lc,cc) -> verify_Btagi ctxt rc i lc cc
  | Btagvar (rc,off,i,lc,cc) -> verify_Btagvar ctxt rc off i lc cc
  | Coerce rc -> verify_Coerce ctxt rc
  | Comment _ -> ctxt
  | Fallthru cs -> raise (Fall_Thru (ctxt,cs))
  | Malloc (i,ma) -> verify_Malloc ctxt i ma
  | Unpack (a,r,gc) -> verify_Unpack ctxt a r gc
;;

(**********************************************************************)    
(* Code Blocks                                                        *)
(**********************************************************************)

(* Add the code labels to psi:
 * Check and normalise the constructor and check it has kind K4byte
 *)
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
    let (k,c') = check ctxt c in
    kindleq ctxt k k4byte; add_val ctxt l c' in
  vector_fold aux ctxt cbv
;;

(* Verifying a code block:
 *   1) build context.
 *     i) seperate the labels type in a (variable,kind) list and register state
 *     ii) add each variable to context left to right
 *     iii) check and normalise register state in this context
 *     iv) make checked and normalised register state the register state
 *   2) check instructions.
 *     i) verify left to right chaining context through
 *     ii) if get to end have a Fallsthru error
 *     iii) otherwise one of two exceptions is raised:
 *       Terminal_Jmp: return None to indicate no fall thru
 *       Fall_Thru d: return Some d to indicate fall thru
 *)

let verify_code_block ctxt (l,c,insts) =
  (* Build ctxt *)
  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
  (* Verify instructions *)
  let ctxt = set_verify_ctxt ctxt "verifying instructions" in
  let rec loop ctxt n i =
    let ctxt = set_loc ctxt (Locc (l,i)) in
    if i=n then
      ()
    else
      let ctxt = verify_instr ctxt insts.(i) in
(*      Talpp.print_register_state Format.std_formatter Talpp.std_options (get_register_state ctxt); Format.print_newline ();*)
      loop ctxt n (i+1) in
  try
    loop ctxt (Array.length insts) 0;
    generate_error ctxt Fallsthru;
    None
  with
    Terminal_Jmp -> None
  | Fall_Thru (ctxt,cs) -> Some (ctxt,cs)
  | Talfail -> None
;;

let verify_code_blocks ctxt cbv =
  let ctxt = set_verify_ctxt ctxt "verifying code blocks" in
  let rec loop ft n i =
    if i=n then
      ft
    else
      let (l,_,_ as cb) = cbv.(i) in
      (match ft with
	None -> ()
      |	Some (ctxt,cs) ->
	  let lc =
	    List.fold_left (fun gc c -> coerce gc (Tapp c))
	      (raw (Addr l)) cs in
	  try verify_instr ctxt (Jmp lc); generate_error ctxt Fallsthru with
	    Terminal_Jmp -> ()
	  | Fall_Thru (_,_) -> generate_error ctxt Fallsthru
	  | Talfail -> ());
      let ft = verify_code_block ctxt cb in
      loop ft n (i+1) in
  match loop None (Array.length cbv) 0 with
    None -> ()
  | Some (_,_) -> generate_error ctxt Fallsthru
;;

(**********************************************************************)    
(* 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 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
    | (Dtag ci)::dis ->
	let tag_con ctxt i = 
	  if i<(Array.length tag_cons) then tag_cons.(i)
 	  else prcon (Csing (pcint i)) in
      	aux saved ((cfield (coerce_con tag_con ctxt ci) 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 _)::dis ->
	aux saved ((cfield (pcbytes Byte4) ReadWrite)::cur) dis
    | (Djunk)::dis ->
	aux saved ((cfield (pcjunk 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 k4byte;
 	whcon (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
;;

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

type ref2int = int_ref -> tal_int

let intrefs2inttype ref2int ctxt refs includes =
  let current = ref []
  and added = ref []
  and cons = ref []
  and vals = ref [] in
  let rec loop intref =
    if List.mem intref !current then
      generate_error ctxt (Cyclic_imports intref);
    if not (List.mem intref !added) then begin
      added := intref :: !added;
      let oldcur = !current in
      current := intref::oldcur;
      let tal_int = ref2int intref in
      if includes then Array.iter loop tal_int.int_includes;
      Array.iter (fun ic -> cons := ic :: !cons) tal_int.int_cons;
      Array.iter (fun lc -> vals := lc :: !vals) tal_int.int_vals;
      current := oldcur
    end in
  Array.iter loop refs;
  {it_cons=List.rev !cons; it_vals=List.rev !vals}
;;

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

let verify_int_con_def ctxt (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
  ((l,k,cd),add_con_def ctxt l cd)
;;

let add_int_con_def ctxt (l,k,cd) =
  let ctxt = set_loc ctxt (Loccon l) in
  add_con_def ctxt l cd
;;

let add_imported_vals ctxt lcs =
  let aux ctxt (l,c) =
    let ctxt = set_loc ctxt (Locval l) in
    let (k,c) = check_whnorm ctxt c in
    kindleq ctxt k k4byte;
    ((l,c),add_val ctxt l c) in
  foldmap_left aux ctxt lcs
;;

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

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')
;;

let verify_exports ref2int ctxte ctxti icons ivals tal_imp =
  let ext = intrefs2inttype ref2int ctxte tal_imp.exports false in
  (* Build context to check exports in *)
  let ctxte = add_imported_cons ctxte icons in
  let ctxte = add_imported_cons ctxte ext.it_cons in
  (* Check exported constructors *)
  let f (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;
    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
  let econs = List.map f ext.it_cons in
  (* Check exported labels *)
  let f (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) in
  let evals = List.map f ext.it_vals in
  {it_cons=econs; it_vals=evals}
;;

let no_abbrevs = Dict.empty id_compare;;

let verify_imp ref2int ctxt0 tal_imp =
  (* Get imported interface *)
  let imt = intrefs2inttype ref2int ctxt0 tal_imp.imports true in
  (* Build phi *)
  let ctxt = add_imported_cons ctxt0 imt.it_cons in
  let ctxt = add_con_blocks ctxt tal_imp.con_blocks in
  (* Process Abbrevs *)
  let process_abbrev abbrevs (l,c) =
    Dict.insert abbrevs l (substs abbrevs c) in
  let abbrevs =
    Array.fold_left process_abbrev no_abbrevs tal_imp.imp_abbrevs in
  (* Process label constructor definitions *)
  let (icons,ctxt) = foldmap_left verify_int_con_def ctxt imt.it_cons 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 = set_abbrevs ctxt no_abbrevs in
  let (ivals,ctxt) = add_imported_vals ctxt imt.it_vals 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
  (* Check code blocks *)
  verify_code_blocks ctxt tal_imp.code_blocks;
  (* Check data blocks *)
  verify_data_blocks ctxt tal_imp.data_blocks;
  (* Check exports *)
  let ctxte = set_verify_ctxt ctxt0 "verifying exports" in
  let ext = verify_exports ref2int ctxte ctxt icons ivals tal_imp in
  ({it_cons=icons; it_vals=ivals},ext)
;;

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