(* Title: Specification of SAFE RTS CORE
Author: Delfin Ruperez and Ricardo Pe~na
Copyright: July 2008, Universidad Complutense de Madrid
*)
header {* Specification Core RTS *}
theory RTSCore
imports "../JVMSAFE/JVMInstructions"
begin
-- "Run-time system class name"
constdefs
System :: cname
"System ≡ Cname ''java/lang/System''"
objectC :: cname
"objectC ≡ Cname ''Object''"
heapC :: cname
"heapC ≡ Cname ''rtsCore/Heap''"
stackC :: cname
"stackC ≡ Cname ''rtsCore/Stack_S''"
dirCellC :: cname
"dirCellC ≡ Cname ''rtsCore/DirectoryCell''"
consTableC :: cname
"consTableC ≡ Cname ''rtsCore/ConsTable''"
consDataC :: cname
"consDataC ≡ Cname ''rtsCore/ConsData''"
cellC :: cname
"cellC ≡ Cname ''rtsCore/Cell''"
-- "Run-time system method name"
Init :: mname
"Init ≡ ''<init>''"
exitM :: mname
"exitM ≡ ''exit''"
decregion :: mname
"decregion ≡ ''decregion''"
slide :: mname
"slide ≡ ''slide''"
pushRegion :: mname
"pushRegion ≡ ''pushRegion''"
popRegion :: mname
"popRegion ≡ ''popRegion''"
copyCell :: mname
"copyCell ≡ ''copyCell''"
copyCellAux :: mname
"copyCellAux ≡ ''copyCellAux''"
clone :: mname
"clone ≡ ''clone''"
copyRTS :: mname
"copyRTS ≡ ''copy''"
reserveCell :: mname
"reserveCell ≡ ''reserveCell''"
releaseCell :: mname
"releaseCell ≡ ''releaseCell''"
insertCell :: mname
"insertCell ≡ ''insertCell''"
makeHeap :: mname
"makeHeap ≡ ''makeHeap''"
makeDirectory :: mname
"makeDirectory ≡ ''makeDirectory''"
setmaxSize :: mname
"setmaxSize ≡ ''setmaxSize''"
makeConsTable :: mname
"makeConsTable ≡ ''makeConsTable''"
-- " Run-time system field name"
constdefs
izqf :: vname
"izqf ≡ VName ''izq''"
derf :: vname
"derf ≡ VName ''der''"
idf :: vname
"idf ≡ VName ''id''"
freef :: vname
"freef ≡ VName ''free''"
tipoArgsf :: vname
"tipoArgsf ≡ VName ''tipoArgs''"
Sf :: vname
"Sf ≡ VName ''S''"
topf :: vname
"topf ≡ VName ''top''"
k0f :: vname
"k0f ≡ VName ''k0''"
kf :: vname
"kf ≡ VName ''k''"
regionsf :: vname
"regionsf ≡ VName ''regions''"
safeDirf :: vname
"safeDirf ≡ VName ''safeDir''"
tagLf :: vname
"tagLf ≡ VName ''tagL''"
tagGf :: vname
"tagGf ≡ VName ''tagG''"
nargsf :: vname
"nargsf ≡ VName ''nargs''"
tablef :: vname
"tablef ≡ VName ''table''"
arg1 :: vname
"arg1 ≡ VName ''arg1''"
arg2 :: vname
"arg2 ≡ VName ''arg2''"
arg3 :: vname
"arg3 ≡ VName ''arg3''"
arg4 :: vname
"arg4 ≡ VName ''arg4''"
arg5 :: vname
"arg5 ≡ VName ''arg5''"
arg6 :: vname
"arg6 ≡ VName ''arg6''"
arg7 :: vname
"arg7 ≡ VName ''arg7''"
arg8 :: vname
"arg8 ≡ VName ''arg8''"
text {* Cell Class *}
-- " Cell Field Declarations"
constdefs cellFdecl :: "fdecl list"
"cellFdecl ≡ [(izqf,RefT (ClassT cellC)),
(derf,RefT (ClassT cellC)),
(idf,PrimT Integer),
(tagGf,PrimT Integer),
(arg1,PrimT Integer),
(arg2,PrimT Integer),
(arg3,PrimT Integer),
(arg4,PrimT Integer),
(arg5,PrimT Integer),
(arg6,PrimT Integer),
(arg7,PrimT Integer),
(arg8,PrimT Integer)]"
text {* ConsTable Class *}
-- "ConsTable Field Declarations"
constdefs consTableFdecl :: "fdecl list"
"consTableFdecl ≡ [(tablef, RefT (ArrayT (RefT (ClassT consDataC))))]"
(* Specification instructions of makeConsTable method *)
constdefs
EndFor1 :: "int"
"EndFor1 ≡ 12"
bucle1 :: "int"
"bucle1 ≡ - 14"
constdefs instMakeConsTable :: "instr list"
"instMakeConsTable ≡
[Load 0,
ArrNew (RefT (ClassT consDataC)),
Putstatic tablef consTableC, (* table = new ConsData[maxCons] *)
LitPush (Intg 0),
Store 1, (* i \<leftarrow> 0 *)
Load 1,
Getstatic tablef consTableC,
ArrLength,
Ifcmp GreaterEqual EndFor1, (* i < table.length ? *)
Getstatic tablef consTableC,
Load 1,
New consDataC,
Dup,
Invoke_special consDataC Init [],
ArrStore,
Load 1,
LitPush (Intg 1),
BinOp Add,
Store 1, (* i \<leftarrow> i + 1 *)
Goto bucle1,
Return_Void
]"
text {* ConsData Class *}
-- " ConsData Field Declarations"
constdefs consDataFdecl :: "fdecl list"
"consDataFdecl ≡ [(tagLf, PrimT Integer),
(nargsf, PrimT Integer),
(tipoArgsf, RefT (ArrayT (PrimT Integer)))]"
(* Specification instructions of ConsData constructor *)
constdefs instInitConsData :: "instr list"
"instInitConsData ≡ [Load 0, (* Load this *)
LitPush (Intg 8),
ArrNew (PrimT Integer), (* tipoArgs \<leftarrow> new int[8] *)
Putfield tipoArgsf consDataC,
Return_Void]"
text {* Stack_S Class *}
-- "Stack_S Field Declarations"
constdefs stackSFdecl :: "fdecl list"
"stackSFdecl ≡ [(Sf, RefT (ArrayT (PrimT Integer))),(topf, PrimT Integer)]"
(* Specification instructions of setmaxSize method *)
constdefs instSetMaxSize :: "instr list"
"instSetMaxSize ≡ [Load 0,
ArrNew (PrimT Integer),
Putstatic Sf stackC, (* S \<leftarrow> new int[maxSize] *)
LitPush (Intg -1),
Putstatic topf stackC, (* top \<leftarrow> -1 *)
Return_Void
]"
(* Instructions of slide method *)
constdefs
EndFor2 :: "int"
"EndFor2 ≡ 16 "
Bucle2 :: "int"
"Bucle2 ≡ -17"
constdefs instSlide :: "instr list"
"instSlide ≡ [Getstatic topf stackC,
Load 0, (* Load local0 = m *)
BinOp Substract,
Load 1, (* Load local1 = n *)
BinOp Substract,
LitPush (Intg 1),
BinOp Add,
Store 2, (* local2\<leftarrow> top - m - n + 1 *)
Getstatic topf stackC,
Load 0,
BinOp Substract,
LitPush (Intg 1),
BinOp Add,
Store 3, (* local3 \<leftarrow>top - m + 1 *)
Load 3, (* Label Bucle2 *)
Getstatic topf stackC,
Ifcmp GreaterThan EndFor2, (* local3 <= top ? *)
Getstatic Sf stackC,
Load 2,
Getstatic Sf stackC,
Load 3,
ArrLoad,
ArrStore, (* S[local2] \<leftarrow> S[local3] *)
Load 2,
LitPush (Intg 1),
BinOp Add,
Store 2, (* local2 \<leftarrow> local2 + 1 *)
Load 3,
LitPush (Intg 1),
BinOp Add,
Store 3, (* local3 \<leftarrow> local3 + 1 *)
Goto Bucle2,
Getstatic topf stackC, (* Label EndFor2 *)
Load 1,
BinOp Substract,
Putstatic topf stackC, (* top \<leftarrow> top - n *)
Return_Void
]"
text {* DirectoryCell Class *}
-- "DirectoryCell Field Declarations"
constdefs dirCFdecl :: "fdecl list"
"dirCFdecl ≡ [(safeDirf, RefT (ArrayT (RefT (ClassT cellC)))),
(freef, RefT (ClassT cellC))]"
(* Instructions of makeDirectory Method *)
constdefs
EndFor3 :: "int"
"EndFor3 ≡ 77"
If1 :: "int"
"If1 ≡ 25"
If2 :: "int"
"If2 ≡ 19"
If3 :: "int"
"If3 ≡ 32"
EndIf2 :: "int"
"EndIf2 ≡ 38"
Bucle3 :: "int"
"Bucle3 ≡ -82"
-- "Instructions List"
constdefs instMakeDirectory :: "instr list"
"instMakeDirectory ≡ [
Load 0,
ArrNew (Class cellC),
Putstatic safeDirf dirCellC, (* safeDir \<leftarrow> new Cell[maxCell] *)
LitPush (Intg 0),
Store 1, (* i \<leftarrow> 0 *)
Load 1,
Getstatic safeDirf dirCellC,
ArrLength,
Ifcmp GreaterEqual EndFor3, (* i < safeDir.length ? *)
Getstatic safeDirf dirCellC,
Load 1,
New cellC,
Dup,
Invoke_special cellC Init [],
ArrStore, (* safeDir[i] \<leftarrow> new Cell() *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Load 1,
Putfield idf cellC, (* safeDir[i].id \<leftarrow> i *)
Load 1,
LitPush (Intg 0),
Ifcmp LessEqual If1, (* i > 0 ? *)
Load 1,
Getstatic safeDirf dirCellC,
ArrLength,
LitPush (Intg 1),
BinOp Substract,
Ifcmp GreaterThan If2, (* i < safeDir.length - 1 *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Getstatic safeDirf dirCellC,
Load 1,
LitPush (Intg 1),
BinOp Substract,
ArrLoad,
Putfield izqf cellC, (* safeDir[i].izq \<leftarrow> safeDir[i - 1] *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Getfield izqf cellC,
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Putfield derf cellC, (* safeDir[i].izq.der \<leftarrow> safeDir[i] *)
Goto EndIf2,
Load 1,
Getstatic safeDirf dirCellC,
ArrLength,
LitPush (Intg 1),
BinOp Substract,
Ifcmp NotEqual If3, (* i = safeDir.length - 1 ? *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Getstatic safeDirf dirCellC,
Load 1,
LitPush (Intg 1),
BinOp Substract,
ArrLoad,
Putfield izqf cellC, (* safeDir[i].izq \<leftarrow> safeDir[i - 1] *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Getstatic izqf cellC,
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Putfield derf cellC, (* safeDir[i].izq.der \<leftarrow> safeDir[i] *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Getstatic safeDirf dirCellC,
LitPush (Intg 0),
ArrLoad,
Putfield derf cellC, (* safeDir[i].der \<leftarrow> safeDir[0] *)
Getstatic safeDirf dirCellC,
LitPush (Intg 0),
ArrLoad,
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Putfield izqf cellC, (* safeDir[0].izq \<leftarrow> safeDir[i] *)
Load 1,
LitPush (Intg 1),
BinOp Add,
Store 1, (* i \<leftarrow> i + 1 *)
Goto Bucle3,
Getstatic safeDirf dirCellC,
LitPush (Intg 0),
ArrLoad,
Putstatic freef cellC, (* free \<leftarrow> safeDir[0] *)
Return_Void
]"
constdefs
If4 :: "int"
"If4 ≡ 18"
EndIf4 :: "int"
"EndIf4 ≡ 3"
constdefs instReserveCell :: "instr list"
"instReserveCell ≡ [
Getstatic freef cellC,
Getfield derf cellC,
Store 0, (* p \<leftarrow> free.der *)
Load 0,
Getstatic freef cellC,
Ifcmpeq If4, (* p ≠ free ? *)
Load 0,
Getfield derf cellC,
Store 1, (* p2 \<leftarrow> p.der *)
Getstatic freef cellC,
Load 1,
Putfield derf cellC, (* free.der \<leftarrow> p2 *)
Load 1,
Load 0,
Getfield izqf cellC,
Putfield izqf cellC, (* p2.izq \<leftarrow> p.izq *)
Load 0,
Load 0,
LitPush (Null),
Dup_x1,
Putfield derf cellC, (* p.der \<leftarrow> null *)
Putfield izqf cellC, (* p.izq \<leftarrow> null *)
Goto EndIf4,
LitPush(Intg 1),
Invoke_static System exitM [PrimT Integer], (* Abort program *)
Load 0,
Getfield idf cellC,
Return (* return p.id *)
]"
constdefs instReleaseCell :: "instr list"
"instReleaseCell ≡ [
Getstatic safeDirf dirCellC,
Load 0,
ArrLoad,
Store 1, (* cell \<leftarrow> safeDir[index] *)
Load 1,
Getfield izqf cellC,
Store 2, (* temp1 \<leftarrow> cell.izq *)
Load 1,
Getfield derf cellC,
Store 3, (* temp2 \<leftarrow> cell.der *)
Load 2,
Load 1,
Getfield derf cellC,
Putfield derf cellC, (* temp1.der \<leftarrow> cell.der *)
Load 3,
Load 1,
Getfield izqf cellC,
Putfield izqf cellC, (* temp2.izq \<leftarrow> cell.izq *)
Load 1,
Getstatic freef dirCellC,
Getfield derf cellC,
Putfield derf cellC, (* cell.der \<leftarrow> free.der *)
Getstatic freef dirCellC,
Getfield derf cellC,
Load 1,
Putfield izqf cellC, (* free.der.izq \<leftarrow> cell *)
Getstatic freef cellC,
Load 1,
Putfield derf cellC, (* free.der \<leftarrow> cell *)
Load 1,
Getstatic freef dirCellC,
Putfield izqf cellC, (* cell.izq \<leftarrow> free *)
Return_Void
]"
-- " Heap Field Declarations"
constdefs heapFdecl :: "fdecl list"
"heapFdecl ≡ [(regionsf, RefT (ArrayT (RefT (ClassT cellC)))),
(kf, PrimT Integer),
(k0f,PrimT Integer)]"
(* Instructions of MakeHeap Method *)
constdefs instMakeHeap :: "instr list"
"instMakeHeap ≡ [
Load 0,
ArrNew (Class cellC),
Putstatic regionsf heapC, (* regions \<leftarrow> new Cell[maxRegions] *)
LitPush (Intg -1),
Putstatic kf heapC, (* k \<leftarrow> -1 *)
LitPush (Intg -1),
Putstatic k0f heapC, (* k0 \<leftarrow> -1 *)
Return_Void
]"
(* Instructions of Decregion Method *)
constdefs
bucle5 :: "int"
"bucle5 ≡ 3"
endbucle5 :: "int"
"endbucle5 ≡ -4"
constdefs instDecregion :: "instr list"
"instDecregion ≡ [
Getstatic kf heapC,
Getstatic k0f heapC,
Ifcmp LessEqual bucle5, (* k > k0 ? *)
Invoke_static heapC popRegion [], (* call PopRegion() method *)
Goto endbucle5,
Return_Void
]"
(* Instructions of PushRegion Method *)
constdefs
labelEnd :: "int"
"labelEnd ≡ 4"
constdefs instPushRegion :: "instr list"
"instPushRegion ≡ [
Getstatic kf heapC,
LitPush (Intg 1),
BinOp Add,
Putstatic kf heapC, (* k \<leftarrow> k + 1 *)
Invoke_static dirCellC reserveCell [],
Store 0, (* cell \<leftarrow> reserveCell() *)
Getstatic regionsf heapC,
Getstatic kf heapC,
Getstatic safeDirf dirCellC,
Load 0,
ArrLoad,
ArrStore, (* regions[k] \<leftarrow> safeDir[cell] *)
Getstatic regionsf heapC,
Getstatic kf heapC,
ArrLoad,
Getstatic regionsf heapC,
Getstatic kf heapC,
ArrLoad,
Getstatic regionsf heapC,
Getstatic kf heapC,
ArrLoad,
Dup_x1,
Putfield izqf cellC, (* regions[k].izq \<leftarrow> regions[k] *)
Putfield derf cellC, (* regions[k].der <- regions[k].izq *)
Goto labelEnd,
Store 0, (* Exception e *)
LitPush (Intg 1),
Invoke_static System exitM [PrimT Integer], (* Abort program with error *)
Return_Void
]"
(* Instructions of PopRegion Method *)
constdefs instPopRegion :: "instr list"
"instPopRegion ≡ [
Getstatic freef dirCellC,
Getfield izqf cellC,
Getstatic regionsf heapC,
Getstatic kf heapC,
ArrLoad,
Putfield derf cellC, (* free.izq.der \<leftarrow> regions[k] *)
Getstatic freef dirCellC,
Getfield izqf cellC,
Store 0, (* c1 \<leftarrow> free.izq *)
Getstatic regionsf heapC,
Getstatic kf heapC,
ArrLoad,
Getfield izqf cellC,
Store 1, (* c2 \<leftarrow> regions[k].izq *)
Getstatic freef cellC,
Load 1,
Putfield izqf cellC, (* free.izq \<leftarrow> c2 *)
Load 1,
Getstatic freef cellC,
Putfield derf cellC, (* c2.der \<leftarrow> free *)
Getstatic regionsf heapC,
Getstatic kf heapC,
ArrLoad,
Load 0,
Putfield izqf cellC, (* regions[k].izq \<leftarrow> c1 *)
Getstatic regionsf heapC,
Getstatic kf heapC,
LitPush (Null),
ArrStore, (* regions[k] \<leftarrow> NULL *)
Getstatic kf heapC,
LitPush(Intg 1),
BinOp Substract,
Putstatic kf heapC, (* k \<leftarrow> k - 1 *)
Return_Void
]"
(* Instructions of InsertCell Method *)
constdefs instInsertCell :: "instr list"
"instInsertCell ≡ [
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Store 2, (* cell \<leftarrow> safeDir[p] *)
Load 2,
Getstatic regionsf heapC,
Load 0,
Getfield izqf cellC,
Putfield izqf cellC, (* cell.izq \<leftarrow> regions[r].izq *)
Getstatic regionsf heapC,
Load 0,
ArrLoad,
Getfield izqf cellC,
Load 2,
Putfield derf cellC, (* regions[r].izq.der \<leftarrow> cell *)
Getstatic regionsf heapC,
Load 0,
ArrLoad,
Load 2,
Putfield izqf cellC, (* regions[r].izq \<leftarrow> cell *)
Load 2,
Getstatic regionsf heapC,
Load 0,
ArrLoad,
Putfield derf cellC, (* cell.der \<leftarrow> regions[r] *)
Return_Void
]"
(* Instructions of CopyCell Method *)
constdefs instCopyCell :: "instr list"
"instCopyCell ≡ [
Invoke_static dirCellC reserveCell [],
Store 1, (* freshCell \<leftarrow> reserveCell() *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Store 2, (* target \<leftarrow> safeDir[freshCell] *)
Getstatic safeDirf dirCellC,
Load 0,
ArrLoad,
Store 3, (* source \<leftarrow> safeDir[p] *)
Load 3,
Load 2,
Invoke_static dirCellC copyCellAux [Class cellC,
Class cellC], (* copyCellAux(source,target) *)
Load 0,
Invoke_static dirCellC releaseCell [PrimT Integer], (* releaseCell(p) *)
Load 2,
Getfield derf cellC,
Load 2,
Putfield izqf cellC, (* target.der.izq \<leftarrow> target *)
Load 2,
Getfield izqf cellC,
Load 2,
Putfield derf cellC, (* target.izq.der \<leftarrow> target *)
Load 1,
Return (* devuelve freshCell *)
]"
(* Instructions of Clone Method *)
constdefs instClone :: "instr list"
"instClone ≡ [
Invoke_static dirCellC reserveCell [],
Store 2, (* freshCell \<leftarrow> reserveCell() *)
Getstatic safeDirf dirCellC,
Load 2,
ArrLoad,
Store 3, (* target \<leftarrow> safeDir[freshCell] *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Store 4, (* source \<leftarrow> safeDir[p] *)
Load 4,
Load 3,
Invoke_static heapC copyCellAux [Class cellC,
Class cellC], (* copyCellAux(source,target) *)
Load 0,
Load 2,
Invoke_static heapC insertCell [PrimT Integer,
PrimT Integer], (* insertCell(reg,freshCell) *)
Load 2,
Return (* devuelve entero freshCell *)
]"
(* Instructions of CopyCellAux Method *)
constdefs instCopyCellAux :: "instr list"
"instCopyCellAux ≡ [
Load 1,
Load 0,
Getfield derf cellC,
Putfield derf cellC, (* c2.der \<leftarrow> c1.der *)
Load 1,
Load 0,
Getfield izqf cellC,
Putfield izqf cellC, (* c2.izq \<leftarrow> c1.izq *)
Load 1,
Load 0,
Getfield tagGf cellC,
Putfield tagGf cellC, (* c2.tagG \<leftarrow> c1.tagG *)
Load 1,
Load 0,
Getfield arg1 cellC,
Putfield arg1 cellC, (* c2.arg1 \<leftarrow> c1.arg1 *)
Load 1,
Load 0,
Getfield arg2 cellC,
Putfield arg2 cellC, (* c2.arg2 \<leftarrow> c1.arg2 *)
Load 1,
Load 0,
Getfield arg3 cellC,
Putfield arg3 cellC, (* c2.arg3 \<leftarrow> c1.arg3 *)
Load 1,
Load 0,
Getfield arg4 cellC,
Putfield arg4 cellC, (* c2.arg4 \<leftarrow> c1.arg4 *)
Load 1,
Load 0,
Getfield arg5 cellC,
Putfield arg5 cellC, (* c2.arg5 \<leftarrow> c1.arg5 *)
Load 1,
Load 0,
Getfield arg6 cellC,
Putfield arg6 cellC, (* c2.arg6 \<leftarrow> c1.arg6 *)
Load 1,
Load 0,
Getfield arg7 cellC,
Putfield arg7 cellC, (* c2.arg7 \<leftarrow> c1.arg7 *)
Load 1,
Load 0,
Getfield arg8 cellC,
Putfield arg8 cellC (* c2.arg8 \<leftarrow> c1.arg8 *)
]"
(* Intructions of Copy Method *)
constdefs
endBucle6 :: "int"
"endBucle6 ≡ 72"
If5 :: "int"
"If5 ≡ 62 "
lab1 :: "int"
"lab1 ≡ 1"
endlab1 :: "int"
"endlab1 ≡ 49"
lab2 :: "int"
"lab2 ≡ lab1 + 7"
endlab2 :: "int"
"endlab2 ≡ endlab1 - 7"
lab3 :: "int"
"lab3 ≡ lab2 + 7"
endlab3 :: "int"
"endlab3 ≡ endlab2 - 7"
lab4 :: "int"
"lab4 ≡ lab3 + 7"
endlab4 :: "int"
"endlab4 ≡ endlab3 - 7"
lab5 :: "int"
"lab5 ≡ lab4 + 7"
endlab5 :: "int"
"endlab5 ≡ endlab4 - 7"
lab6 :: "int"
"lab6 ≡ lab5 + 7"
endlab6 :: "int"
"endlab6 ≡ endlab5 - 7"
lab7 :: "int"
"lab7 ≡ lab6 + 7"
endlab7 :: "int"
"endlab7 ≡ endlab6 - 7"
lab8 :: "int"
"lab8 ≡ lab7 + 7"
ldef :: "int"
"ldef ≡ lab8 + 6"
bucle6 :: "int"
"bucle6 ≡ -77"
constdefs instCopy :: "instr list"
"instCopy ≡ [
Load 1,
Load 0,
Invoke_static heapC clone [PrimT Integer,
PrimT Integer],
Store 2, (* target \<leftarrow> clone (j,b) *)
Getstatic safeDirf dirCellC,
Load 0,
ArrLoad,
Store 3, (* source \<leftarrow> safeDir[b] *)
Getstatic tablef consDataC,
Load 3,
Getfield tagGf cellC,
ArrLoad,
Store 4, (* info \<leftarrow> table[source.tagG] *)
LitPush (Intg 0),
Store 5, (* i \<leftarrow> 0 *)
Load 5,
Load 4,
Getfield nargsf consDataC,
Ifcmp GreaterEqual endBucle6, (* i < info.nargs ? *)
Load 4,
Getfield tipoArgsf consDataC,
Load 5,
ArrLoad, (* Integer Array *)
Store 6, (* tipo \<leftarrow> info.tipoArgs[i] *)
Load 6,
LitPush (Intg 4),
Ifcmp NotEqual If5,
Getstatic safeDirf dirCellC,
Load 2,
ArrLoad,
Store 7, (* targ \<leftarrow> safeDir[target] *)
Load 5, (* Load local5 = i *)
Tableswitch 0 7 [lab1,
lab2,
lab3,
lab4,
lab5,
lab6,
lab7,
lab8,
ldef],
Load 7, (* label 1 *)
Load 3,
Getfield arg1 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg1 cellC, (* targ.arg1 \<leftarrow> copy(source.arg1,j) *)
Goto endlab1, (* end label 1 *)
Load 7, (* label 2 *)
Load 3,
Getfield arg2 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg2 cellC, (* targ.arg2 \<leftarrow> copy(source.arg2,j) *)
Goto endlab2, (* end label 2 *)
Load 7, (* label 3 *)
Load 3,
Getfield arg3 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg3 cellC, (* targ.arg3 \<leftarrow> copy(source.arg3,j) *)
Goto endlab3, (* end label 3 *)
Load 7, (* label 4 *)
Load 3,
Getfield arg4 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg4 cellC, (* targ.arg4 \<leftarrow> copy(source.arg4,j) *)
Goto endlab4, (* end label 4 *)
Load 7, (* label 5 *)
Load 3,
Getfield arg5 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg5 cellC, (* targ.arg5 \<leftarrow> copy(source.arg5,j) *)
Goto endlab5, (* end label 5 *)
Load 7, (* label 6 *)
Load 3,
Getfield arg6 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg6 cellC, (* targ.arg6 \<leftarrow> copy(source.arg6,j) *)
Goto endlab6, (* end label 6 *)
Load 7, (* label 7 *)
Load 3,
Getfield arg7 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg7 cellC, (* targ.arg1 \<leftarrow> copy(source.arg1,j) *)
Goto endlab7, (* end label 7 *)
Load 7, (* label 8 *)
Load 3,
Getfield arg8 cellC,
Load 1,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Putfield arg8 cellC, (* targ.arg8 \<leftarrow> copy(source.arg8,j) *)
Load 5,
LitPush (Intg 1),
BinOp Add,
Store 5, (* i \<leftarrow> i + 1 *)
Goto bucle6,
Load 2,
Return (* return target *)
]"
-- " Program RTS with all Class declarations"
constdefs Prog_RTS :: "jvm_prog"
"Prog_RTS ≡
(let
classCell = (cellC,objectC,cellFdecl,[]);
consTableMethod = ((makeConsTable,[PrimT Integer]), PrimT Void,(4,2,instMakeConsTable,[]));
classConsTable = (consTableC,objectC,consTableFdecl,[consTableMethod]);
initConsDataMethod = ( (Init, []), PrimT Void, (2,1,instInitConsData,[]));
classConsData =(consDataC,objectC,consDataFdecl,[initConsDataMethod]);
setMaxSizeM = ((setmaxSize,[PrimT Integer]), PrimT Void, (1,1,instSetMaxSize,[]));
slideM = ((slide,[PrimT Integer,PrimT Integer]), PrimT Void, (4,4,instSlide,[]));
classStackS = (stackC, objectC,stackSFdecl,[setMaxSizeM,slideM]);
makeDirM = ((makeDirectory, [PrimT Integer]), PrimT Void, (4,2,instMakeDirectory,[]));
reserM = ((reserveCell,[]), PrimT Integer, (4,2,instReserveCell ,[]));
releaM = ((releaseCell,[PrimT Integer]), PrimT Void, (2,4,instReleaseCell ,[]));
classDir = (dirCellC, objectC,dirCFdecl,[makeDirM,reserM,releaM]);
makeHeapM = ((makeHeap,[PrimT Integer]),PrimT Void, (1,1,instMakeHeap,[]));
decregionM = ((decregion,[]),PrimT Void,(2,0,instDecregion,[]));
pushRegionM = ((pushRegion,[]),PrimT Void,(4,1,instPushRegion,[(0,23,26,
Xcpt ArrayIndexOutOfBounds)]));
popRegionM = ((popRegion,[]),PrimT Void,(3,2,instPopRegion,[]));
insertCellM = ((insertCell,[PrimT Integer,PrimT Integer]), PrimT Void,(3,3,instInsertCell,[]));
copyCellM = ((copyCell,[PrimT Integer]),PrimT Integer,(2,4,instCopyCell,[]));
cloneM = ((clone,[PrimT Integer,PrimT Integer]),PrimT Integer,(2,5,instClone,[]));
copyCellAuxM = ((copyCellAux,[RefT (ClassT cellC),RefT (ClassT cellC)]),
PrimT Void,(2,2,instCopyCellAux,[]));
copyM = ((copyRTS,[PrimT Integer,PrimT Integer]),PrimT Integer,(3,8,instCopy,[]));
classHeap = (heapC, objectC, heapFdecl,[makeHeapM,decregionM,pushRegionM,popRegionM,
insertCellM,copyCellM,cloneM,copyCellAuxM,copyM])
in [classCell,classConsTable,classConsData,classStackS,classDir,classHeap])"
end