Up to index of Isabelle/HOL/SafeImp
theory SVM2JVM(* Title: Translation from Safe Virtual Machine to JVM
Author: Delfin Rup'erez and Ricardo Pe~na
Copyright: June 2008, Universidad Complutense de Madrid
*)
header {* Translation from SVM to JVM *}
theory SVM2JVM
imports "../JVMSAFE/JVMInstructions" SVMState RTSCore HaskellLib
begin
types pc = nat
codeMap = "PC \<rightharpoonup> pc"
contMap = "CodeLabel \<rightharpoonup> nat"
consMap = "Constructor \<rightharpoonup> nat"
subsection {* Initialisation code *}
text{* Initialise cell creation, region stack, and machine stack.
The corresponding initialisation method of each class is called. *}
constdefs initSizeTable :: "SizesTable => bytecode"
"initSizeTable st ≡ (
case st of (c,r,s) =>
[LitPush (Intg (int c)),
Invoke_static dirCellC makeDirectory [PrimT Integer],
LitPush (Intg (int r)),
Invoke_static heapC makeHeap [PrimT Integer],
LitPush (Intg (int s)),
Invoke_static stackC setmaxSize [PrimT Integer]])"
text {* Initialise the runtime constructor table. *}
(* It fills the type of argument j of the current constructor *)
constdefs auxOneArg :: "(ArgType × nat) => bytecode"
"auxOneArg arT ≡
(let j = snd arT;
argTyp = (case (fst arT) of
IntArg => 1
| BoolArg => 2
| NonRecursive => 3
| Recursive => 4)
in [Dup,
LitPush (Intg (int j)),
LitPush (Intg argTyp),
ArrStore])"
(* It fills all the fields of constructor i *)
constdefs fillsOneConstructor :: "((nat × nat × ArgType list) × nat)
=> instr list"
"fillsOneConstructor tuple ≡
(let ((tagl,nargs,argTypes),i) = tuple;
typePairs = zip argTypes [0..<nargs];
codePairs = map auxOneArg typePairs
in [Getstatic tablef consTableC,
LitPush (Intg (int i)),
ArrLoad,
Dup, Dup,
LitPush (Intg (int tagl)),
Putfield tagLf consDataC,
LitPush (Intg (int nargs)),
Putfield nargsf consDataC,
Getfield tipoArgsf consDataC]
@ concat codePairs @ [Pop])"
constdefs initConsTable :: "ConstructorTableType => instr list"
"initConsTable ct ≡
(let len = length ct;
tuples = map (% (C,(n,tag,atypes)) . (tag,n,atypes)) ct;
fillCode = map fillsOneConstructor (zip tuples [0..<len])
in [LitPush (Intg (int len)),
Invoke_static consTableC makeConsTable [PrimT Integer]]
@ concat fillCode)"
subsection{* Generic translation functions *}
text{* The translation functions are:
\begin{itemize}
\item {\sl trSVM2JVM} translates a complete SafeImp program into a JVM
program consisting in a single class ''PSafe'', with a single method called
''PSafeMain'', containing the in-line JVM code of the translation.
\item {\sl trCodeStore} takes the code store part of the SafeImp program
and produces the bytecode part of the JVM program, together with a code map
mapping SVM program counters into JVM ones, and a continuation map mapping
each SafeImp continuation code label into a distinct natural number global
to the program. The first part of the bytecode is a function table solving
forward references in the code, and a continuation switch translating the
continuation natural numbers into jumps to the correponding continuation
code labels.
\item {\sl trSeq} translates a single SafeImp sequence of SVM
instructions. It receives the next available JVM pc and returns the next
not used pc. It also updates the current code and continuation maps.
\item {\sl trInstrAux} translates a single SVM instruction into a bytecode
sequence. It updates the next available JVM pc and the codemap. The actual
bytecode generation is done by {\sl trInstr}.
\end{itemize}
*}
consts
trInstr :: "[pc,codeMap,contMap,consMap,pc,SafeInstr] => instr list"
text{* Translate Constructor Table: Each constructor is given a
distinct number *}
constdefs trConsTable :: "ConstructorTableType => consMap"
"trConsTable ct ≡ (
let len = length ct
in map_of (zip (map fst ct) [0..<len]))"
constdefs
trInstrAux :: "[CodeLabel,contMap,consMap,pc,pc×nat×codeMap,SafeInstr]
=> (pc×nat×codeMap) × instr list"
"trInstrAux p ctmap com pcc state safeinstr == (
case state of (pc,i,cdmap) =>
let cdmap' = cdmap ((p,i) \<mapsto> pc);
instrs = trInstr pc cdmap' ctmap com pcc safeinstr;
n = length instrs
in ((pc+n,i+1,cdmap'),instrs))"
constdefs
trSeq :: "[contMap,consMap,pc,pc×codeMap,CodeLabel×CodeSequence×FunName]
=> (pc×codeMap)× instr list"
"trSeq ctmap com pcc state seq == (
let (pc,cdmap) = state;
(p,svms,f) = seq;
((pc',n,cdmap'),instss) =
mapAccumL (trInstrAux p ctmap com pcc) (pc,0,cdmap) svms
in ((pc',cdmap'),concat instss))"
(* This axiom reflects properties that the SVM code must satisfy *)
axioms svms_good:
"distinct (map fst (svms::SVMCode))"
constdefs
trCodeStore :: "[CodeLabel,pc,ContinuationMap,consMap,SVMCode]
=> instr list × codeMap × contMap"
"trCodeStore inip inipc ctmap com svmss == (
let (fs,ps,contss) = unzip3 ctmap;
conts = concat contss;
nc = length conts;
nf = length fs;
cdini = map_of (zip (zip ps (replicate nf 0))[inipc+1..<inipc+nf+1]);
ctm = map_of (zip conts [1..<nc+1]);
pcc = inipc + nf + 1;
((pc,cdm),iss) = mapAccumL (trSeq ctm com pcc) (pcc + 1,cdini) svmss;
funJumps = zipWith (% p n. int(the(cdm (p,0)))-int n)
ps [inipc+1..<inipc+nf+1];
funTable = map Goto funJumps;
contSwitch = Tableswitch 1 (int nc) (map
((% n. n-int pcc) o int o the o cdm o (% p.(p,0)))
conts)
in (Goto (int (the (cdm (inip,0)))-int inipc) # funTable
@ (contSwitch # concat iss),cdm,ctm))"
-- "Names and signature of the translated program single class and method"
constdefs
safeP :: cname
"safeP ≡ Cname ''SafeP''"
safeMain :: mname
"safeMain ≡ ''PSafeMain''"
sigSafeMain :: sig
"sigSafeMain ≡ (safeMain,[])"
text{* It generates code to initialize the runtime system by creating
the constructor table, the cells, the heap and the stack. Then, it
translates the SVM instructions. *}
constdefs
trSVM2JVM :: "SafeImpProg => jvm_prog × codeMap × contMap
× consMap"
"trSVM2JVM prog == (
let ((svms,ctmap),ini,constable,sizeTable) = prog;
instrConsTable = initConsTable constable;
lenCT = length instrConsTable;
comap = trConsTable constable;
instrSizeTable = initSizeTable sizeTable;
lenST = length instrSizeTable;
(instrs,cdm,ctm) = trCodeStore ini (lenCT+lenST) ctmap comap svms;
method = (sigSafeMain,PrimT Void,
(10,10,instrConsTable @ instrSizeTable @ instrs,[]));
classes = [(safeP,objectC,[],[method])]
in (classes @ Prog_RTS,cdm,ctm,comap))"
(* Extract bytecode of safeMain method *)
constdefs
extractBytecode :: "jvm_prog => bytecode"
"extractBytecode P ≡ (fst (snd (snd (snd (snd (the (method' (P, safeP) sigSafeMain)))))))"
subsection{* Specific translation from each SafeImp instruction to bytecode *}
text{* Auxiliary functions of trInstr *}
text{* {\sl trAddr} translates two absolute addresses into a relative one.
Used in JVM instructions Goto and Tableswitch. *}
constdefs
trAddr :: "[nat,nat] => int"
"trAddr addr1 addr2 == int addr1 - int addr2"
text{* {\sl nat2Str} translates a nat into a string *}
constdefs
nat2Str :: "nat => string"
"nat2Str v == (if v = 1 then ''1''
else if v = 2 then ''2''
else if v = 3 then ''3''
else if v = 4 then ''4''
else if v = 5 then ''5''
else if v = 6 then ''6''
else if v = 7 then ''7''
else ''8'')"
text{* PC Increases *}
constdefs
incCall :: nat
"incCall ≡ 1"
incPop :: nat
"incPop ≡ 24"
incMatchN :: nat
"incMatchN ≡ 7"
text{* These are fragments of MATCH and MATCHD translations. *}
consts
endlabel1 :: int
endlabel2 :: int
endlabel3 :: int
endlabel4 :: int
endlabel5 :: int
endlabel6 :: int
endlabel7 :: int
endlabel8 :: int
label1 :: int
label2 :: int
label3 :: int
label4 :: int
label5 :: int
label6 :: int
label7 :: int
label8 :: int
labelEndLoop :: int
labelLoop :: int
constdefs
InstLabel1 :: "instr list"
"InstLabel1 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg1 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg1 cellC,
ArrStore,
Goto endlabel1]"
nlab1 :: nat
"nlab1 ≡ length InstLabel1"
InstLabel2 :: "instr list"
"InstLabel2 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg2 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg2 cellC,
ArrStore,
Goto endlabel2]"
nlab2 :: nat
"nlab2 ≡ length InstLabel2"
InstLabel3 :: "instr list"
"InstLabel3 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg3 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg3 cellC,
ArrStore,
Goto endlabel3]"
nlab3 :: nat
"nlab3 ≡ length InstLabel3"
InstLabel4 :: "instr list"
"InstLabel4 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg4 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg4 cellC,
ArrStore,
Goto endlabel4]"
nlab4 :: nat
"nlab4 ≡ length InstLabel4"
InstLabel5 :: "instr list"
"InstLabel5 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg5 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg5 cellC,
ArrStore,
Goto endlabel5]"
nlab5 :: nat
"nlab5 ≡ length InstLabel5"
InstLabel6 :: "instr list"
"InstLabel6 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg6 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg6 cellC,
ArrStore,
Goto endlabel6]"
nlab6 :: nat
"nlab6 ≡ length InstLabel6"
InstLabel7 :: "instr list"
"InstLabel7 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg7 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg7 cellC,
ArrStore,
Goto endlabel7]"
nlab7 :: nat
"nlab7 ≡ length InstLabel7"
InstLabel8 :: "instr list"
"InstLabel8 ≡ [Getstatic Sf stackC, (* S[top-i] \<leftarrow> o.arg8 *)
Getstatic topf stackC,
Load 5,
BinOp Substract,
Load 6,
Getfield arg8 cellC,
ArrStore,
Goto endlabel8]"
nlab8 :: nat
"nlab8 ≡ length InstLabel8"
Match11 :: "nat => instr list"
"Match11 l ≡ [Getstatic Sf stackC, (* load S!l *)
Getstatic topf stackC,
LitPush (Intg (int l)),
BinOp Substract,
ArrLoad,
Store 1, (* local1 \<leftarrow> b *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Store 6, (* local6 \<leftarrow> o *)
Load 6,
Getfield tagGf cellC,
Store 2, (* local2 \<leftarrow> TagG *)
Getstatic tablef consTableC,
Load 2,
ArrLoad,
Dup,
Getfield tagLf consDataC,
Store 3, (* local3 \<leftarrow> tagL *)
Getfield nargsf consDataC,
Store 4, (* local4 \<leftarrow> nargs *)
LitPush (Intg 0), (* i \<leftarrow> 0 *)
Store 5, (* local5 \<leftarrow> i*)
Getstatic topf stackC,
Load 4,
BinOp Add,
Putstatic topf stackC (* top \<leftarrow> top + nargs *)]"
nMatch11 :: nat
"nMatch11 ≡ length (Match11 0)"
Match12 :: "instr list"
"Match12 ≡ [Load 4, (* nargs *)
Load 5, (* i *)
Ifcmp GreaterEqual labelEndLoop, (* i ≥ nargs ? *)
Load 5, (* no, load argument i *)
Tableswitch 0 7 [label1,label2,label3,label4,
label5,label6,label7,label8]]"
nMatch12 :: nat
"nMatch12 ≡ length Match12"
Match2 :: "instr list"
"Match2 ≡ [Load 5,
LitPush (Intg 1),
BinOp Add,
Store 5, (* i = i + 1 *)
Goto labelLoop]"
nMatch2 :: nat
"nMatch2 ≡ 5"
text{* PC increases for MATCH and MATCHD *}
defs
endlabel1_def: "endlabel1 ≡ int (nlab2 + nlab3 + nlab4 + nlab5 + nlab6 + nlab7 + nlab8 + 1)"
endlabel2_def: "endlabel2 ≡ int (nlab3 + nlab4 + nlab5 + nlab6 + nlab7 + nlab8 + 1)"
endlabel3_def: "endlabel3 ≡ int (nlab4 + nlab5 + nlab6 + nlab7 + nlab8 + 1)"
endlabel4_def: "endlabel4 ≡ int (nlab5 + nlab6 + nlab7 + nlab8 + 1)"
endlabel5_def: "endlabel5 ≡ int (nlab6 + nlab7 + nlab8 + 1)"
endlabel6_def: "endlabel6 ≡ int (nlab7 + nlab8 + 1)"
endlabel7_def: "endlabel7 ≡ int (nlab8 + 1)"
endlabel8_def: "endlabel8 ≡ 1"
defs
label1_def: "label1 ≡ 1"
label2_def: "label2 ≡ int (nlab1 + 1)"
label3_def: "label3 ≡ int (nlab1 + nlab2 + 1)"
label4_def: "label4 ≡ int (nlab1 + nlab2 + nlab3 + 1)"
label5_def: "label5 ≡ int (nlab1 + nlab2 + nlab3 + nlab4 + 1)"
label6_def: "label6 ≡ int (nlab1 + nlab2 + nlab3 + nlab4 + nlab5 + 1)"
label7_def: "label7 ≡ int (nlab1 + nlab2 + nlab3 + nlab4 + nlab5 + nlab6 + 1)"
label8_def: "label8 ≡ int (nlab1 + nlab2 + nlab3 + nlab4 + nlab5 + nlab6 + nlab7 + 1)"
defs
labelEndLoop_def: "labelEndLoop ≡ int (nlab1 + nlab2 + nlab3 + nlab4 + nlab5 + nlab6 + nlab7
+ nlab8 + 3 + nMatch2)"
defs
labelLoop_def: "labelLoop ≡ -int (nlab1 + nlab2 + nlab3 + nlab4 + nlab5 + nlab6 + nlab7
+ nlab8 + nMatch2 + nMatch12) + 1"
constdefs
incMatch :: nat
"incMatch ≡ nMatch11 + nMatch12 + nlab1 + nlab2 + nlab3 + nlab4 + nlab5 + nlab6 + nlab7
+ nlab8 + nMatch2 + 1"
incMatchD :: nat
"incMatchD ≡ nMatch11 + nMatch12 + nlab1 + nlab2 + nlab3 + nlab4 + nlab5 + nlab6 + nlab7
+ nlab8 + nMatch2 + 3"
text{* These are fragments of BUILDENV and BUILDCLS translations *}
consts
pushAux' :: "Item => nat => instr list"
primrec
"pushAux' (ItemConst v) i =
[Getstatic Sf stackC,
Load 1, (* load top+n *)
LitPush (Intg (int i)),
BinOp Substract,
(if (isBool v = True)
then LitPush (Bool (the_BoolT v))
else LitPush (Intg (the_IntT v))),
ArrStore (* S[top+n-i] \<leftarrow> v *)
]"
"pushAux' (ItemVar l) i =
[Getstatic Sf stackC,
Getstatic topf stackC,
LitPush (Intg (int l)),
BinOp Substract,
ArrLoad,
Store 2, (* v \<leftarrow> S!l *)
Getstatic Sf stackC,
Load 1, (* load top+n *)
LitPush (Intg (int i)),
BinOp Substract,
Load 2, (* load v *)
ArrStore (* S[top+n-i] \<leftarrow> v *)
]"
"pushAux' (ItemRegSelf) i =
[Getstatic Sf stackC,
Load 1, (* load top+n *)
LitPush (Intg (int i)),
BinOp Substract,
Getstatic kf heapC,
ArrStore (* S[top+n-i] \<leftarrow> k *)
]"
constdefs
pushAux :: "Item × nat => instr list"
"pushAux pair == case pair of (it,i) => pushAux' it i"
text{* {\sl regAux} selects the region where to insert the fresh cell *}
consts
regAux :: "Item => instr list"
primrec
"regAux (ItemRegSelf) =
[Getstatic kf heapC,
Store 3]" (* local3 \<leftarrow> k *)
"regAux (ItemVar l) =
[Getstatic Sf stackC,
Getstatic topf stackC,
LitPush (Intg (int l)),
BinOp Substract,
ArrLoad,
Store 3]" (* local3 \<leftarrow> S!l *)
text{* {\sl fillAux'} fills the cell *}
consts
fillAux' :: "Item => nat => instr list"
primrec
"fillAux' (ItemVar l) i =
[Load 2, (* Load object Cell *)
Getstatic Sf stackC, (* load S!l *)
Getstatic topf stackC,
LitPush (Intg (int l)),
BinOp Substract,
ArrLoad,
Putfield (VName (''arg''@ nat2Str i)) cellC]"
"fillAux' (ItemConst v) i =
[Load 2, (* load object Cell *)
(if (isBool v = True) then LitPush (Bool (the_BoolT v))
else LitPush (Intg (the_IntT v))),
Putfield (VName (''arg''@ nat2Str i)) cellC]"
constdefs
fillAux :: "Item × nat => instr list"
"fillAux pair == case pair of (it,i) => fillAux' it i"
text{* Translation to bytecode of each SafeImp Instruction *}
primrec
"trInstr pc cdm ctm com pcc DECREGION =
[Invoke_static heapC decregion []]"
"trInstr pc cdm ctm com pcc (SLIDE m n) =
[LitPush (Intg (int m)),
LitPush (Intg (int n)),
Invoke_static stackC slide [PrimT Integer,
PrimT Integer]]"
"trInstr pc cdm ctm com pcc (CALL p) = (
let pc1 = the(cdm(p,0));
offset = trAddr pc1 (pc + incCall)
in [Invoke_static heapC pushRegion [],
Goto offset] )"
"trInstr pc cdm ctm com pcc (PRIMOP oper) =
[Getstatic Sf stackC, (* load S[top - 1] *)
Getstatic topf stackC,
LitPush (Intg 1),
BinOp Substract,
Dup2, (* Dup 2 top opstack *)
ArrLoad,
Store 1, (* save v2 *)
Getstatic Sf stackC,
Getstatic topf stackC,
ArrLoad,
Load 1, (* push v2 on top of v1 *)
BinOp oper, (* compute v1 op v2 *)
ArrStore, (* store it at S[top - 1] *)
Getstatic topf stackC, (* top <- top - 1 *)
LitPush (Intg 1),
BinOp Substract,
Putstatic topf stackC]"
"trInstr pc cdm ctm com pcc REUSE =
[Getstatic Sf stackC,
Getstatic topf stackC,
ArrLoad,
Invoke_static heapC copyCell [PrimT Integer],
Store 1, (* local1 <- p *)
Getstatic Sf stackC,
Getstatic topf stackC,
Load 1, (* S[top] <- p *)
ArrStore]"
"trInstr pc cdm ctm com pcc COPY =
[Getstatic Sf stackC,
Getstatic topf stackC,
ArrLoad,
Store 1, (* local1 <- b *)
Getstatic Sf stackC,
Getstatic topf stackC,
LitPush (Intg 1),
BinOp Substract,
ArrLoad,
Store 2,
Load 1, (* local2 <- j *)
Load 2,
Invoke_static heapC copyRTS [PrimT Integer,
PrimT Integer],
Store 3, (* local3 <- b' *)
Getstatic topf stackC,
LitPush (Intg 1),
BinOp Substract,
Putstatic topf stackC, (* top <- top - 1 *)
Getstatic Sf stackC,
Getstatic topf stackC,
Load 3,
ArrStore]" (* S[top] <- b' *)
"trInstr pc cdm ctm com pcc POPCONT =
[Getstatic Sf stackC,
Getstatic topf stackC,
Dup2,
Dup2,
Dup2,
ArrLoad,
Store 1, (* local1 <- b *)
LitPush (Intg 1),
BinOp Substract,
ArrLoad,
Store 2, (* local2 <- k' *)
LitPush (Intg 2),
BinOp Substract,
ArrLoad,
Store 3, (* local3 <- p *)
LitPush (Intg 2),
BinOp Substract,
Dup,
Putstatic topf stackC, (* top <- top - 2 *)
Load 1,
ArrStore, (* S[top] <- b *)
Load 2,
Putstatic k0f heapC, (* k0 <- k' *)
Load 3, (* jump to continuation *)
Goto (trAddr pcc (pc + incPop))]"
"trInstr pc cdm ctm com pcc (PUSHCONT p) =
( let n = the(ctm(p))
in
[Getstatic topf stackC,
LitPush (Intg 1),
BinOp Add,
Putstatic topf stackC, (* top <- top + 1 *)
Getstatic Sf stackC,
Getstatic topf stackC,
LitPush (Intg (int n)),
ArrStore, (* S[top] <- p' *)
Getstatic topf stackC,
LitPush (Intg 1),
BinOp Add,
Putstatic topf stackC, (* top <- top + 1 *)
Getstatic Sf stackC,
Getstatic topf stackC,
Getstatic k0f heapC,
ArrStore, (* S[top] <- k0 *)
Getstatic kf heapC, (* k0 <- k *)
Putstatic k0f heapC])"
"trInstr pc cdm ctm com pcc (MATCHN l v m ps) =
(let pcs = map (%p.(the(cdm(p,0)))) ps;
pcs' = map (%n.(trAddr n (pc + incMatchN))) pcs
in [Getstatic Sf stackC, (* load S!l *)
Getstatic topf stackC,
LitPush (Intg (int l)),
BinOp Substract,
ArrLoad,
LitPush (Intg (int v)), (* substract v *)
BinOp Substract,
Tableswitch 0 (int (m + 1)) pcs'])"
"trInstr pc cdm ctm com pcc (MATCH l ps) =
(let len = length ps;
pcs = map (%p.(the(cdm(p,0)))) ps;
pcs' = map (%n.(trAddr n(pc + incMatch))) pcs
in Match11 l @ Match12 @
InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @
Match2 @
[Load 3, (* Load tagL *)
Tableswitch 0 (int (len - 1)) pcs'])"
"trInstr pc cdm ctm com pcc (MATCHD l ps) =
(let len = length ps;
pcs = map (%p.(the(cdm(p,0)))) ps;
pcs' = map (%n.(trAddr n(pc + incMatchD))) pcs
in Match11 l @ Match12 @
InstLabel1 @ InstLabel2 @ InstLabel3 @ InstLabel4 @
InstLabel5 @ InstLabel6 @ InstLabel7 @ InstLabel8 @
Match2 @
[Load 1, (* release Cell b *)
Invoke_static dirCellC releaseCell [PrimT Integer],
Load 3, (* Load tagL *)
Tableswitch 0 (int (len - 1)) pcs'])"
"trInstr pc cdm ctm com pcc (BUILDENV its) =
(let n = length its;
genCode = map pushAux (zip its [0..<n])
in [Getstatic topf stackC,
LitPush (Intg (int n)),
BinOp Add,
Store 1] (* local1 \<leftarrow> top + n *)
@ concat genCode
@ [Load 1, Putstatic topf stackC])"
"trInstr pc cdm ctm com pcc (BUILDCLS c its item) =
(let tagg = the(com c);
n = length its;
codRes = [Invoke_static dirCellC reserveCell [],
Store 1, (* local1 \<leftarrow> p *)
Getstatic safeDirf dirCellC,
Load 1,
ArrLoad,
Store 2, (* local2 \<leftarrow> o cell *)
Load 2,
LitPush (Intg (int tagg)),
Putfield tagGf cellC]; (* o.tagG = tagg *)
codFil = map fillAux (zip its [1..<n+1]);
codIns = [Load 3,
Load 1,
Invoke_static heapC insertCell [PrimT Integer,
PrimT Integer],
Getstatic topf stackC,
LitPush (Intg 1),
BinOp Add,
Putstatic topf stackC, (* top \<leftarrow> top + 1 *)
Getstatic Sf stackC,
Getstatic topf stackC,
Load 1,
ArrStore] (* S[top] \<leftarrow> b *)
in codRes @ regAux item @ concat codFil @ codIns)"
(* Activate to generate the compiler pass *)
(* export_code trSVM2JVM in Haskell file "./codeJ" *)
end