Theory SVMState

(*  Title:      Safe Virtual Machine State
    Author:     Ricardo Peña
    Copyright:  March 2008, Universidad Complutense de Madrid
*)

header {* State of the SVM *}

theory SVMState 
imports SafeHeap "../JVMSAFE/BinOP"
begin



subsection {* Sizes Table *}

text{* This gives statically inferred information about the maximum number of heap 
cells, of heap regions, and of stack words needed by the compiled program. *}

types ncell = nat
      sizeRegions = nat
      sizeStackS = nat

types SizesTable = "ncell × sizeRegions × sizeStackS"




subsection {* Stack *}

types
  CodeLabel = nat
  Continuation = "Region × CodeLabel"

datatype StackObject = Val Val | Reg  Region | Cont Continuation

text{* The SVM stack may contain normal form values, region arguments for
functions or constructors, and continuations. A continuation $(k_0,p)$
contains a jump $p$ to a code sequence and an adjustment $k_0$ for the heap
watermark $k_0$ of the SVM state.
*}

types
  Stack = "StackObject list"
  StackOffset = nat



subsection {* Code Store and SafeImp program *}



-- "Items are the components of environments and closures"
datatype Item = ItemConst Val
              | ItemVar StackOffset
              | ItemRegSelf



-- "The SVM instruction repertory"
datatype SafeInstr = DECREGION
                   | POPCONT
                   | PUSHCONT CodeLabel
                   | COPY 
                   | REUSE
                   | CALL CodeLabel
                   | PRIMOP PrimOp
                   | MATCH StackOffset "(CodeLabel list)"
                   | MATCHD StackOffset "(CodeLabel list)"
                   | MATCHN StackOffset nat nat "(CodeLabel list)"
                   | BUILDENV "(Item list)"
                   | BUILDCLS Constructor "(Item list)"  Item 
                   | SLIDE nat nat


fun pushcont :: "SafeInstr => bool"
where
  "pushcont (PUSHCONT p) = True"
| "pushcont _            = False"

fun popcont :: "SafeInstr => bool"
where
  "popcont POPCONT = True"
| "popcont _       = False"

text{* A Safe program, when translated into SafeImp, produces four
components (1) a map from labels to pairs consisting of a code sequence and
a function name.  It is given as a list in order to be able to `traverse'
the map; (2) a map from function names to pairs consisting of a label and a
list of labels. The firts points to the starting sequence of the function
and the second collects, for each function body, the code labels
corresponding to continuations. The map is also given as a list; (3) the
code label of the main expression; and (4) a constructor table collecting
the properties of all the constructors. *}

types
  CodeSequence = "SafeInstr list"
  SVMCode   = "(CodeLabel × CodeSequence × FunName) list"
  ContinuationMap = "(FunName × CodeLabel × CodeLabel list) list"
  CodeStore = "SVMCode  × ContinuationMap"
  SafeImpProg = "CodeStore × CodeLabel × ConstructorTableType × SizesTable"



subsection {* Runtime State *}



types
  PC = "CodeLabel × nat"
  SVMState = "Heap × Region × PC × Stack"


consts
  incrPC :: "PC => PC"

primrec
  "incrPC (l,i) = (l,i+1)"

text{*
This is the correspondence betweeen primitive operators in CoreSafe and SafeImp.
*}

constdefs
   primops :: "string \<rightharpoonup> PrimOp" 

  "primops ≡ map_of [(''+'',Add),
                            (''-'',Substract),
                            (''*'',Times),
                            (''%'',Divide),
                            (''<'',LessThan),
                            (''<='',LessEqual),
                            (''=='',Equal),
                            (''>'',GreaterThan),
                            (''>='',GreaterEqual)
                           ]"

-- "Define primitive operations"
consts
  execOp :: "[PrimOp,Val,Val] => Val"

primrec
   "execOp Equal b1 b2 = BoolT (the_IntT(b1) = the_IntT(b2))"
   "execOp NotEqual b1 b2 = BoolT (the_IntT(b1) ≠ the_IntT(b2))"
   "execOp GreaterEqual b1 b2 = BoolT (the_IntT(b1) ≥ the_IntT(b2))"
   "execOp GreaterThan b1 b2 = BoolT (the_IntT(b1) > the_IntT(b2))"
   "execOp LessThan b1 b2 = BoolT (the_IntT(b1) < the_IntT(b2))"
   "execOp LessEqual b1 b2 = BoolT (the_IntT(b1) ≤ the_IntT(b2))"

   "execOp Add b1 b2 = IntT (the_IntT(b1) + the_IntT(b2))"
   "execOp Substract b1 b2 = IntT (the_IntT(b1) - the_IntT(b2))"
   "execOp Times b1 b2 = IntT (the_IntT(b1) * the_IntT(b2))"
   "execOp Divide  b1 b2 = IntT (the_IntT(b1) div the_IntT(b2))"


end