# Theory JVMExecInstr

```(*  Title:      JinjaThreads/JVM/JVMExecInstr.thy
Author:     Cornelia Pusch, Gerwin Klein, Andreas Lochbihler
*)

section ‹JVM Instruction Semantics›

theory JVMExecInstr
imports
JVMInstructions
JVMHeap
"../Common/ExternalCall"
begin

primrec extRet2JVM ::
"nat ⇒ 'heap ⇒ 'addr val list ⇒ 'addr val list ⇒ cname ⇒ mname ⇒ pc ⇒ 'addr frame list
⇒ 'addr extCallRet ⇒ ('addr, 'heap) jvm_state"
where
"extRet2JVM n h stk loc C M pc frs (RetVal v) = (None, h, (v # drop (Suc n) stk, loc, C, M, pc + 1) # frs)"
| "extRet2JVM n h stk loc C M pc frs (RetExc a) = (⌊a⌋, h, (stk, loc, C, M, pc) # frs)"
| "extRet2JVM n h stk loc C M pc frs RetStaySame = (None, h, (stk, loc, C, M, pc) # frs)"

lemma eq_extRet2JVM_conv [simp]:
"(xcp, h', frs') = extRet2JVM n h stk loc C M pc frs va ⟷
h' = h ∧ (case va of RetVal v ⇒ xcp = None ∧ frs' = (v # drop (Suc n) stk, loc, C, M, pc + 1) # frs
| RetExc a ⇒ xcp = ⌊a⌋ ∧ frs' = (stk, loc, C, M, pc) # frs
| RetStaySame ⇒ xcp = None ∧ frs' = (stk, loc, C, M, pc) # frs)"
by(cases va) auto

definition extNTA2JVM :: "'addr jvm_prog ⇒ (cname × mname × 'addr) ⇒ 'addr jvm_thread_state"
where "extNTA2JVM P ≡ (λ(C, M, a). let (D,M',Ts,meth) = method P C M; (mxs,mxl0,ins,xt) = the meth
in (None, [([],Addr a # replicate mxl0 undefined_value, D, M, 0)]))"

abbreviation extTA2JVM ::
"'addr jvm_prog ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action"
where "extTA2JVM P ≡ convert_extTA (extNTA2JVM P)"

context JVM_heap_base begin

primrec exec_instr ::
"'addr instr ⇒ 'addr jvm_prog ⇒ 'thread_id ⇒ 'heap ⇒ 'addr val list ⇒ 'addr val list
⇒ cname ⇒ mname ⇒ pc ⇒ 'addr frame list ⇒
(('addr, 'thread_id, 'heap) jvm_thread_action × ('addr, 'heap) jvm_state) set"
where
exec_instr_Load:
"exec_instr (Load n) P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (None, h, ((loc ! n) # stk, loc, C⇩0, M⇩0, pc+1)#frs))}"

| "exec_instr (Store n) P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (None, h, (tl stk, loc[n:=hd stk], C⇩0, M⇩0, pc+1)#frs))}"

| exec_instr_Push:
"exec_instr (Push v) P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (None, h, (v # stk, loc, C⇩0, M⇩0, pc+1)#frs))}"

| exec_instr_New:
"exec_instr (New C) P t h stk loc C⇩0 M⇩0 pc frs =
(let HA = allocate h (Class_type C)
in if HA = {} then {(ε, ⌊addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)}
else (λ(h', a). (⦃NewHeapElem a (Class_type C)⦄, None, h', (Addr a # stk, loc, C⇩0, M⇩0, pc + 1)#frs)) ` HA)"

| exec_instr_NewArray:
"exec_instr (NewArray T) P t h stk loc C0 M0 pc frs =
(let si = the_Intg (hd stk);
i = nat (sint si)
in (if si <s 0
then {(ε, ⌊addr_of_sys_xcpt NegativeArraySize⌋, h, (stk, loc, C0, M0, pc) # frs)}
else let HA = allocate h (Array_type T i)
in if HA = {} then {(ε, ⌊addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C0, M0, pc) # frs)}
else (λ(h', a). (⦃NewHeapElem a (Array_type T i)⦄, None, h', (Addr a # tl stk, loc, C0, M0, pc + 1) # frs)) ` HA))"

| exec_instr_ALoad:
"exec_instr ALoad P t h stk loc C0 M0 pc frs =
(let i = the_Intg (hd stk);
va = hd (tl stk);
a = the_Addr va;
len = alen_of_htype (the (typeof_addr h a))
in (if va = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
else if i <s 0 ∨ int len ≤ sint i then
{(ε, ⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)}
else {(⦃ReadMem a (ACell (nat (sint i))) v⦄, None, h, (v # tl (tl stk), loc, C0, M0, pc + 1) # frs) | v.
heap_read h a (ACell (nat (sint i))) v }))"

| exec_instr_AStore:
"exec_instr AStore P t h stk loc C0 M0 pc frs =
(let ve = hd stk;
vi = hd (tl stk);
va = hd (tl (tl stk))
in (if va = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
else (let i = the_Intg vi;
idx = nat (sint i);
a = the_Addr va;
hT = the (typeof_addr h a);
T = ty_of_htype hT;
len = alen_of_htype hT;
U = the (typeof⇘h⇙ ve)
in (if i <s 0 ∨ int len ≤ sint i then
{(ε, ⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)}
else if P ⊢ U ≤ the_Array T then
{(⦃WriteMem a (ACell idx) ve⦄, None, h', (tl (tl (tl stk)), loc, C0, M0, pc+1) # frs)
| h'. heap_write h a (ACell idx) ve h'}
else {(ε, (⌊addr_of_sys_xcpt ArrayStore⌋, h, (stk, loc, C0, M0, pc) # frs))}))))"

| exec_instr_ALength:
"exec_instr ALength P t h stk loc C0 M0 pc frs =
{(ε, (let va = hd stk
in if va = Null
then (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)
else (None, h, (Intg (word_of_int (int (alen_of_htype (the (typeof_addr h (the_Addr va)))))) # tl stk, loc, C0, M0, pc+1) # frs)))}"

| "exec_instr (Getfield F C) P t h stk loc C⇩0 M⇩0 pc frs =
(let v = hd stk
in if v = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)}
else let a = the_Addr v
in {(⦃ReadMem a (CField C F) v'⦄, None, h, (v' # (tl stk), loc, C⇩0, M⇩0, pc + 1) # frs) | v'.
heap_read h a (CField C F) v'})"

| "exec_instr (Putfield F C) P t h stk loc C⇩0 M⇩0 pc frs =
(let v = hd stk;
r = hd (tl stk)
in if r = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)}
else let a = the_Addr r
in {(⦃WriteMem a (CField C F) v⦄, None, h', (tl (tl stk), loc, C⇩0, M⇩0, pc + 1) # frs) | h'.
heap_write h a (CField C F) v h'})"

| "exec_instr (CAS F C) P t h stk loc C0 M0 pc frs =
(let v'' = hd stk; v' = hd (tl stk); v = hd (tl (tl stk))
in if v = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
else let a = the_Addr v
in {(⦃ReadMem a (CField C F) v', WriteMem a (CField C F) v''⦄, None, h', (Bool True # tl (tl (tl stk)), loc, C0, M0, pc + 1) # frs) | h' .
heap_read h a (CField C F) v' ∧ heap_write h a (CField C F) v'' h'} ∪
{(⦃ReadMem a (CField C F) v''⦄, None, h, (Bool False # tl (tl (tl stk)), loc, C0, M0, pc + 1) # frs) | v''.
heap_read h a (CField C F) v'' ∧ v'' ≠ v'})"

| "exec_instr (Checkcast T) P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, let U = the (typeof⇘h⇙ (hd stk))
in if P ⊢ U ≤ T then (None, h, (stk, loc, C⇩0, M⇩0, pc + 1) # frs)
else (⌊addr_of_sys_xcpt ClassCast⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs))}"

| "exec_instr (Instanceof T) P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, None, h, (Bool (hd stk ≠ Null ∧ P ⊢ the (typeof⇘h⇙ (hd stk)) ≤ T) # tl stk, loc, C⇩0, M⇩0, pc + 1) # frs)}"

| exec_instr_Invoke:
"exec_instr (Invoke M n) P t h stk loc C0 M0 pc frs =
(let ps = rev (take n stk);
r = stk ! n;
a = the_Addr r;
T = the (typeof_addr h a)
in (if r = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
else
let C = class_type_of T;
(D,M',Ts,meth)= method P C M
in case meth of
Native ⇒
{(extTA2JVM P ta, extRet2JVM n h' stk loc C0 M0 pc frs va) | ta va h'.
(ta, va, h') ∈ red_external_aggr P t a M ps h}
| ⌊(mxs,mxl⇩0,ins,xt)⌋ ⇒
let f' = ([],[r]@ps@(replicate mxl⇩0 undefined_value),D,M,0)
in {(ε, None, h, f' # (stk, loc, C0, M0, pc) # frs)}))"

| "exec_instr Return P t h stk⇩0 loc⇩0 C⇩0 M⇩0 pc frs =
{(ε, (if frs=[] then (None, h, []) else
let v = hd stk⇩0;
(stk,loc,C,m,pc) = hd frs;
n = length (fst (snd (method P C⇩0 M⇩0)))
in (None, h, (v#(drop (n+1) stk),loc,C,m,pc+1)#tl frs)) )}"

| "exec_instr Pop P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (None, h, (tl stk, loc, C⇩0, M⇩0, pc+1)#frs) )}"

| "exec_instr Dup P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (None, h, (hd stk # stk, loc, C⇩0, M⇩0, pc+1)#frs) )}"

| "exec_instr Swap P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (None, h, (hd (tl stk) # hd stk # tl (tl stk), loc, C⇩0, M⇩0, pc+1)#frs) )}"

| "exec_instr (BinOpInstr bop) P t h stk loc C0 M0 pc frs =
{(ε,
case the (binop bop (hd (tl stk)) (hd stk)) of
Inl v ⇒ (None, h, (v # tl (tl stk), loc, C0, M0, pc+1) # frs)
| Inr a ⇒ (Some a, h, (stk, loc, C0, M0, pc) # frs))}"

| "exec_instr (IfFalse i) P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (let pc' = if hd stk = Bool False then nat(int pc+i) else pc+1
in (None, h, (tl stk, loc, C⇩0, M⇩0, pc')#frs)) )}"

| exec_instr_Goto:
"exec_instr (Goto i) P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (None, h, (stk, loc, C⇩0, M⇩0, nat(int pc+i))#frs) )}"

| "exec_instr ThrowExc P t h stk loc C⇩0 M⇩0 pc frs =
{(ε, (let xp' = if hd stk = Null then ⌊addr_of_sys_xcpt NullPointer⌋ else ⌊the_Addr(hd stk)⌋
in (xp', h, (stk, loc, C⇩0, M⇩0, pc)#frs)) )}"

| exec_instr_MEnter:
"exec_instr MEnter P t h stk loc C⇩0 M⇩0 pc frs =
{let v = hd stk
in if v = Null
then (ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)
else (⦃Lock→the_Addr v, SyncLock (the_Addr v)⦄, None, h, (tl stk, loc, C⇩0, M⇩0, pc + 1) # frs)}"

| exec_instr_MExit:
"exec_instr MExit P t h stk loc C⇩0 M⇩0 pc frs =
(let v = hd stk
in if v = Null
then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc)#frs)}
else {(⦃Unlock→the_Addr v, SyncUnlock (the_Addr v)⦄, None, h, (tl stk, loc, C⇩0, M⇩0, pc + 1) # frs),
(⦃UnlockFail→the_Addr v⦄, ⌊addr_of_sys_xcpt IllegalMonitorState⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)})"

end

end
```