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

(* tal.mli
 * 
 * This is a fairly complete specification of the abstract syntax for
 * a typed version of 32-bit (flat-model) iNTEL 80386, Pentium, Pentium Pro,
 * and/or Pentium II assembly language.  
 *
 * TODO:  1. floating point
 *
 *)

(**********************************************************************)
(* Miscellanous stuff *)

open Utilities;;
open Identifier;;

type scale = Byte1 | Byte2 | Byte4 | Byte8
val scale_to_int : scale -> int
type reg = Eax | Ebx | Ecx | Edx | Esi | Edi | Ebp | Esp | Virt of identifier
val compare_regs : reg -> reg -> int

(**********************************************************************)
(* Kinds *)

(* Kbyte <= Ktype, Kmemi <= Kmem *)
type kind = 
    Kbyte of scale	  (* describes types of 8/16/32/64 bit values *)
  | Ktype   		  (* describes types of all values *)
  | Kmemi of int          (* types for memory of size i *)
  | Kmem                  (* types for memory or heap blocks *)
  | Kstack  		  (* describes types of the stack & pointers into it *)
  | Kint                  (* integer "sort" for array indices *)
  | Karrow of kind * kind (* functions from constructors to constructors *)
  | Kprod of kind list    (* tuples of constructors *)
;;

val k4byte : kind;; (* 32 bit values *)

(**********************************************************************)
(* Type Constructors *)

(* primitive constructors *)
type primcon = 
    PCbytes of scale      (* : Kbyte s *)
  | PCjunk of int         (* : Uninitialized junk on the stack or in memory *)
  | PCexn                 (* : K4byte *)
  | PCexnname             (* : K4byte -> K4byte *)
  | PCint of int          (* : Kint *)

(* fields in tuples & arrays have variances:
     readonly, writeonly, readwrite, or uninitialised. *)
type variance = Read | Write | ReadWrite | Uninit;;

type rcon = 
(* the language portion of con's *)
    Cvar of identifier
  | Clam of identifier * kind * con
  | Capp of con * con
  | Ctuple of con list
  | Cproj of int * con
(* the "type" portion of con's *)
  | Clab of identifier
  | Cprim of primcon                    (* see above *)
  | Crec of (identifier * kind * con) list
  | Cforall of identifier * kind * con
  | Cexist of identifier * kind * con
  | Ccode of register_state
  | Chptr of int list*con option        (* Kmem -> K4byte *)
  | Cfield of con*variance              (* Kbyte i -> Kmem i *)
  | Cprod of con list
  | Csum of con list
  | Carray of con*con        		(* Kint,Kmem -> Kmem *)
  | Csing of con             		(* Kint -> K4byte *)
(* the "stack" portion of con's *)
  | Csptr of con                        (* Kstack -> K4byte *)
  | Cempty
  | Ccons of con * con                  (* Kmem/Kbyte,Kstack -> Kstack *)
  | Cappend of con * con                (* Kstack,Kstack -> Kstack *)
and con = 
  { mutable rcon     : rcon;   (* "raw" constructor *)
    mutable isnorm   : bool;   (* true only if rcon is in (full) normal form *)
    mutable freevars : identifier Set.set option} (* free vars of rcon *)

and register_state;;

val defcon : rcon -> con

val pcbytes : scale -> con
val cbyte4 : con
val pcjunk : int -> con
val pcexn : con
val pcexnname : con
val pcint : int -> con

val cvar : identifier -> con
val clam : identifier -> kind -> con -> con
val capp : con -> con -> con
val ctuple : con list -> con
val cproj : con -> int -> con
val clab : identifier -> con
val crec : (identifier * kind * con) list -> con
val cforall : identifier -> kind -> con -> con
val cexist : identifier -> kind -> con -> con
val ccode : register_state -> con
val ccode_l : (reg * con) list -> con
val chptr : int list -> con option -> con
val cptr : con -> con
val cfield : con -> variance -> con
val cprod : con list -> con
val cprod_b : con list -> con   (* Boxed product *)
val csum : con list -> con
val carray : con -> con -> con
val carray_s : identifier -> con -> con  (* E[v:Sint].^*[S(v)^r,array(v,c)] *)
val csing : con -> con
val csptr : con -> con
val cempty : con
val ccons : con -> con -> con
val cappend : con -> con -> con

val rs_empty : register_state;;
val rs_get_reg : register_state -> reg -> con;; (* throws Dict.Absent *)
val rs_set_reg : register_state -> reg -> con -> register_state;;
val rs_set_regs : register_state -> (reg * con) list -> register_state;;
val rs_del_reg : register_state -> reg -> register_state;;
val rs_del_regs : register_state -> reg list -> register_state;;
val rs_map_reg : (con -> con) -> register_state -> register_state;;
val rs_app_reg : (reg -> con -> 'a) -> register_state -> unit;;
val rs_fold_reg : (reg -> con -> 'a -> 'a) -> register_state -> 'a -> 'a;;

(* Pointer integers *)
val min_pointer_integer : int;;
val is_non_pointer_integer : int -> bool;;

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

(* various coercions that only affect the type of a value/reg/path/etc *)
type coercion =
    Pack of con * con  (* abstract a type: first con is hidden,
	      		  second con is existential *)
  | Tapp of con        (* instantiate type var *)
  | Roll of con        (* introduce recursive type *)
  | Unroll             (* eliminate recursive type *)
  | Tosum of con       (* coerce record/tag to a sum *)
  | Fromsum            (* coerce a unary-sum to a record *)
  | RollTosum of con   (* combined Tosum followed by Roll *)
  | Toexn              (* coerce a record to an exn *)
  | Toarray of int*int (* coerce a record to an array/vector (offset,depth) *)
  | Slot of int*int    (* coerce stack slot to junk *)
  | Subsume of con     (* subsumption *)

type 'a coerce = 'a * coercion list (* (r,[c1;...;cn]) is c1(...cn(r)...) *)

(* Operands for most instructions *)
type genop =
    Immed of int
  | Tag of int                    (* tag introduction *)
  | Reg of reg
  | Addr of identifier
  | Prjr of reg coerce * int
  | Prjl of identifier coerce * int

(* Note: Above/Below are unsigned, Greater/Less are signed *)
type condition = 
    Above | AboveEq | Below | BelowEq | Eq | Greater | GreaterEq | Less
  | LessEq | NotEq | NotOverflow | NotSign | Overflow | ParityEven
  | ParityOdd | Sign

type arithbin = 
    Adc 
  | Add   (* (Un)signed Add *)
  | And   (* Bitwise And *)
  | Imul2 (* Signed Multiply, 2 operands *)
  | Or    (* Bitwise Or *)
  | Sbb   
  | Sub   (* (Un)signed Subtract *)
  | Xor   (* Bitwise Xor *)
type arithun = 
    Dec    
  | Inc 
  | Neg   (* 0 - op *)
  | Not   (* 1's complement *)
type arithmd = 
    Div   (* Unsigned *)
  | Idiv  (* Signed divide. Quotient -> Eax, Remainder -> Edx *) 
  | Imul1 (* Signed multiply. Result -> Edx Eax *)
  | Mul   (* Unsigned *)
type arithsr = 
    Rcl 
  | Rcr 
  | Rol 
  | Ror 
  | Sal   (* Signed *) 
  | Sar   (* Signed *)
  | Shl   (* Unsigned *)
  | Shr   (* Unsigned *)

(* note: the move sign/zero extend ops can only do 8/16 -> 16/32 moves *)
type conv =
    Cbw | Cdq | Cwd | Cwde
  | Movsx of reg*scale*genop*scale (* move with sign extend *)
  | Movzx of reg*scale*genop*scale (* move with zero extend *)

(* Malloc allocates a peice of memory that is either a nested set or products
 * of fields or an exnname.  For conciseness we provide bytearrays as an
 * alternative to a product of n byte fields and a later Toarray coercion.
 *)
type mallocarg = 
    Mprod of mallocarg list
  | Mfield of con 
  | Mbytearray of scale * int
  | Mexnname of con
val malloc_prod : con list -> mallocarg;;

(* This is a subset of the x86 32-bit instructions that we might want to
 * cover.  Does not include floating-point support yet.
 *)
type instruction = 
    ArithBin of arithbin * genop * genop
	                        (* binary arithmetic operation *)
  | ArithUn of arithun * genop  (* unary arithmetic operation *)
  | ArithMD of arithmd * genop  (* multiply/division *)
  | ArithSR of arithsr * genop * int option (* NONE = ECX, shift/rotate *)
  | Bswap of reg                (* toggle endianess *)
  | Call of genop coerce        (* push return addr, jump to label *)
  | Clc                      	(* clear carry flag *)
  | Cmc                      	(* toggle carry flag *)
  | Cmovcc of condition * reg * genop coerce
	                        (* conditional move *)
  | Cmp of genop * genop     	(* compare *)
  | Conv of conv                (* various 8/16/32 -> 16/32/64 ops *)
  | Imul3 of reg * genop * int  (* signed multiply 3 arg form *)
  | Int of int               	(* interrupt:  system call *)
  | Into                        (* interrupt if overflow set *)
  | Jcc of condition * identifier coerce
	                        (* jump on condition *)
  | Jecxz of identifier coerce  (* jump if ECX is zero *)
  | Jmp of genop coerce      	(* jump *)
  | Lahf                     	(* move flags into Eax (exc. overflow) *)
  | Lea of reg * genop          (* move effective address into register *)
  | Loopd of identifier coerce * bool option
                                (* decrement ECX and if result nonzero jump
				   if bool present jump only if
				     nonzero Z flag equals the boolean *)
  | Mov of genop * (genop coerce)
                                (* move, load, store *)
  | Nop                      	(* no-op *)
  | Pop of genop             	(* stack pop *)
  | Popad                    	(* pop all registers (32-bit) *)
  | Popfd                    	(* pop eflags *)
  | Push of genop coerce     	(* push onto stack *)
  | Pushad                   	(* push all registers (32-bit) *)
  | Pushfd                   	(* push eflags *)
  | Retn of int option       	(* return "near" (i.e., doesn't touch CS) *)
  | Sahf                     	(* move ah into flags (exc. overflow) *)
  | Setcc of condition * genop	(* set dest=1/0 if condition is true/false *)
  | Shld of genop * reg * int option (* NONE = ECX, shift 64 *)
  | Shrd of genop * reg * int option (* NONE = ECX, shift 64 *)
  | Stc                      	(* set carry flag *)
  | Test of genop * genop    	(* test *)
  | Xchg of genop * reg         (* exchange *)
(* operations specific to x86tal *)
  | Asub of reg * genop * int * reg * genop
    (* r1:=genop1[r2] where genop1 is an array of size genop2 and elt size i *)
  | Aupd of genop * int * reg * reg * genop
    (* genop1[r1]:=r2 where genop1 is an array of size genop2 and elt size i *)
  | Bexn of reg * genop * identifier coerce
                                (* r.exname != op branch to label *)
  | Btagi of reg * int * identifier coerce * condition
	                        (* Compare tag and branch on condition *)
  | Btagvar of reg * int * int * identifier coerce * condition
	                        (* Comp tag in rec and branch on condition *)
  | Coerce of reg coerce        (* Coerce register *)
  | Comment of string
  | Fallthru of con list  
       (* only valid when preceeding a label L.  effectively, 
	* a jmp L[c1,...,cn]. *)
  | Malloc of int * mallocarg 
        (* allocate tuple,exn_name,bytearray of size i into register eax *)
  | Unpack of identifier * reg * genop coerce
                                (* effectively a move *)

(* Notes on incompleteness:

+ No floating point support.
+ No BCD ops - who wants them?
+ No string ops - ditto.
+ No ENTER/LEAVE - ditto.
+ No BOUND - ditto.
+ No system ops - we're supporting user space applications only for now.
+ No concurrentcy ops (xadd, cmpxchg, lock, ...)
   - not supporting concurrency yet.
+ No bit ops - not sure if these are useful.
+ No XLAT - ditto.
+ No CPUID.
+ No far ops - supporting flat model only.
*)

type code_block = identifier * con * instruction vector

(**********************************************************************)
(* Static Data *)

type data_item =
    Dlabel of identifier coerce
  | Dtag of int coerce
  | Dbytes of string
  | D2bytes of int
  | D4bytes of int
  | Djunk
  | Dexnname of con
  | Dup
  | Ddown
;;

(* A datablock is one of the following:
 *   Exnname:
 *     Dexnname
 *     Cannot coerce
 *   Tuple:
 *     (Dlabel | Dtag | Dbytes | D2bytes | D4bytes | Djunk)^*
 *     Which may then be coerced.
 *)

type data_block = identifier * con option * (data_item list) coerce

(**********************************************************************)
(* Compilation Units *)

type int_ref = string

type con_abbrev = identifier * con;;

type int_con = identifier * kind * int_con_def
and int_con_def = AbsCon | BoundCon of con | ConcCon of con;;

type tal_int =
    { int_includes : int_ref vector;
      int_cons : int_con vector;
      int_vals : (identifier * con) vector
    }
;;

type tal_int_type = {
    it_cons : int_con list;
    it_vals : (identifier * con) list
  } 
;;

type con_block = (identifier * kind * con);;

type tal_imp =
    { imports : int_ref vector;
      exports : int_ref vector;
      imp_abbrevs : con_abbrev vector;
      con_blocks : con_block vector;
      code_blocks : code_block vector;
      data_blocks : data_block vector
    } 
;;

(* EOF: x86tal.mli *)
