src/HOL/MicroJava/JVM/JVMExecInstr.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 28524 644b62cf678f
permissions -rw-r--r--
Name.uu, Name.aT;
kleing@9376
     1
(*  Title:      HOL/MicroJava/JVM/JVMExecInstr.thy
kleing@9376
     2
    ID:         $Id$
kleing@9376
     3
    Author:     Cornelia Pusch, Gerwin Klein
kleing@9376
     4
    Copyright   1999 Technische Universitaet Muenchen
kleing@9376
     5
*)
kleing@9376
     6
kleing@10057
     7
kleing@12911
     8
header {* \isaheader{JVM Instruction Semantics} *}
kleing@10057
     9
kleing@10057
    10
haftmann@16417
    11
theory JVMExecInstr imports JVMInstructions JVMState begin
kleing@10057
    12
kleing@9376
    13
kleing@9376
    14
consts
kleing@10056
    15
  exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
kleing@10056
    16
                  cname, sig, p_count, frame list] => jvm_state"
kleing@9376
    17
primrec
kleing@9376
    18
 "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
kleing@9376
    19
      (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
kleing@9376
    20
kleing@9376
    21
 "exec_instr (Store idx) G hp stk vars Cl sig pc frs = 
kleing@9376
    22
      (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)"
kleing@9376
    23
kleing@10897
    24
 "exec_instr (LitPush v) G hp stk vars Cl sig pc frs = 
kleing@10897
    25
      (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
kleing@9376
    26
kleing@9376
    27
 "exec_instr (New C) G hp stk vars Cl sig pc frs = 
kleing@12519
    28
  (let (oref,xp') = new_Addr hp;
kleing@12519
    29
       fs   = init_vars (fields(G,C));
kleing@12519
    30
       hp'  = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
kleing@12519
    31
       pc'  = if xp'=None then pc+1 else pc
kleing@12519
    32
   in 
kleing@13677
    33
      (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))"
kleing@9376
    34
kleing@9376
    35
 "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
kleing@12519
    36
  (let oref = hd stk;
kleing@12519
    37
       xp'  = raise_system_xcpt (oref=Null) NullPointer;
kleing@12519
    38
       (oc,fs)  = the(hp(the_Addr oref));
kleing@12519
    39
       pc'  = if xp'=None then pc+1 else pc
kleing@12519
    40
   in
kleing@13677
    41
      (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))"
kleing@9376
    42
kleing@9376
    43
 "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = 
kleing@12519
    44
  (let (fval,oref)= (hd stk, hd(tl stk));
kleing@12519
    45
       xp'  = raise_system_xcpt (oref=Null) NullPointer;
kleing@12519
    46
       a    = the_Addr oref;
kleing@12519
    47
       (oc,fs)  = the(hp a);
kleing@12519
    48
       hp'  = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp;
kleing@12519
    49
       pc'  = if xp'=None then pc+1 else pc
kleing@12519
    50
   in
kleing@12519
    51
      (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))"
kleing@9376
    52
kleing@9376
    53
 "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
kleing@12519
    54
  (let oref = hd stk;
kleing@12519
    55
       xp'  = raise_system_xcpt (\<not> cast_ok G C hp oref) ClassCast; 
kleing@12519
    56
       stk' = if xp'=None then stk else tl stk;
kleing@12519
    57
       pc'  = if xp'=None then pc+1 else pc
kleing@12519
    58
   in
kleing@12519
    59
      (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
kleing@9376
    60
kleing@9550
    61
 "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
kleing@12519
    62
  (let n    = length ps;
kleing@12519
    63
       argsoref = take (n+1) stk;
kleing@12519
    64
       oref = last argsoref;
kleing@12519
    65
       xp'  = raise_system_xcpt (oref=Null) NullPointer;
kleing@12519
    66
       dynT = fst(the(hp(the_Addr oref)));
kleing@12519
    67
       (dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps));
kleing@12519
    68
       frs' = if xp'=None then 
kleing@10056
    69
                [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
kleing@12519
    70
              else []
kleing@12519
    71
   in 
kleing@12519
    72
      (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" 
kleing@12519
    73
  -- "Because exception handling needs the pc of the Invoke instruction,"
kleing@12519
    74
  -- "Invoke doesn't change stk and pc yet (@{text Return} does that)."
kleing@9376
    75
kleing@9376
    76
 "exec_instr Return G hp stk0 vars Cl sig0 pc frs =
kleing@12519
    77
  (if frs=[] then 
kleing@9376
    78
     (None, hp, [])
kleing@9376
    79
   else 
kleing@12519
    80
     let val = hd stk0; (stk,loc,C,sig,pc) = hd frs;
kleing@12519
    81
         (mn,pt) = sig0; n = length pt
kleing@12519
    82
   in 
kleing@12519
    83
      (None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))"
kleing@12519
    84
  -- "Return drops arguments from the caller's stack and increases"
kleing@12519
    85
  -- "the program counter in the caller"
kleing@9376
    86
kleing@9376
    87
 "exec_instr Pop G hp stk vars Cl sig pc frs = 
kleing@9376
    88
      (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)"
kleing@9376
    89
kleing@9376
    90
 "exec_instr Dup G hp stk vars Cl sig pc frs = 
kleing@9376
    91
      (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
kleing@9376
    92
kleing@9376
    93
 "exec_instr Dup_x1 G hp stk vars Cl sig pc frs = 
kleing@10056
    94
      (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), 
kleing@10056
    95
                  vars, Cl, sig, pc+1)#frs)"
kleing@9376
    96
kleing@9376
    97
 "exec_instr Dup_x2 G hp stk vars Cl sig pc frs = 
kleing@10056
    98
      (None, hp, 
kleing@10056
    99
       (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
kleing@10056
   100
       vars, Cl, sig, pc+1)#frs)"
kleing@9376
   101
kleing@9376
   102
 "exec_instr Swap G hp stk vars Cl sig pc frs =
kleing@12519
   103
  (let (val1,val2) = (hd stk,hd (tl stk))
kleing@9376
   104
   in
kleing@12519
   105
      (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
kleing@9376
   106
kleing@9376
   107
 "exec_instr IAdd G hp stk vars Cl sig pc frs =
kleing@9376
   108
  (let (val1,val2) = (hd stk,hd (tl stk))
kleing@9376
   109
   in
kleing@10056
   110
      (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), 
kleing@10056
   111
       vars, Cl, sig, pc+1)#frs))"
kleing@9376
   112
kleing@9376
   113
 "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
kleing@12519
   114
  (let (val1,val2) = (hd stk, hd (tl stk));
kleing@9376
   115
     pc' = if val1 = val2 then nat(int pc+i) else pc+1
kleing@12519
   116
   in
kleing@12519
   117
      (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
kleing@9376
   118
kleing@9376
   119
 "exec_instr (Goto i) G hp stk vars Cl sig pc frs =
kleing@9376
   120
      (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)"
kleing@9376
   121
kleing@12519
   122
 "exec_instr Throw G hp stk vars Cl sig pc frs =
kleing@12519
   123
  (let xcpt  = raise_system_xcpt (hd stk = Null) NullPointer;
kleing@12519
   124
       xcpt' = if xcpt = None then Some (hd stk) else xcpt
kleing@12519
   125
   in
kleing@12519
   126
      (xcpt', hp, (stk, vars, Cl, sig, pc)#frs))"
kleing@12519
   127
kleing@12519
   128
end