src/HOL/MicroJava/JVM/JVMInstructions.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 41589 bbd861837ebc
permissions -rw-r--r--
Name.uu, Name.aT;
kleing@9376
     1
(*  Title:      HOL/MicroJava/JVM/JVMInstructions.thy
kleing@9376
     2
    ID:         $Id$
kleing@9376
     3
    Author:     Gerwin Klein
kleing@9376
     4
    Copyright   2000 Technische Universitaet Muenchen
kleing@9376
     5
*)
kleing@9376
     6
kleing@12911
     7
header {* \isaheader{Instructions of the JVM} *}
kleing@10057
     8
kleing@10057
     9
haftmann@16417
    10
theory JVMInstructions imports JVMState begin
kleing@9376
    11
kleing@9550
    12
kleing@9376
    13
datatype 
kleing@12519
    14
  instr = Load nat                  -- "load from local variable"
kleing@12519
    15
        | Store nat                 -- "store into local variable"
kleing@12519
    16
        | LitPush val               -- "push a literal (constant)"
kleing@12519
    17
        | New cname                 -- "create object"
kleing@12519
    18
        | Getfield vname cname      -- "Fetch field from object"
kleing@12519
    19
        | Putfield vname cname      -- "Set field in object    "
kleing@12519
    20
        | Checkcast cname           -- "Check whether object is of given type"
kleing@12519
    21
        | Invoke cname mname "(ty list)"  -- "inv. instance meth of an object"
kleing@12519
    22
        | Return                    -- "return from method"
kleing@12519
    23
        | Pop                       -- "pop top element from opstack"
kleing@12519
    24
        | Dup                       -- "duplicate top element of opstack"
kleing@13676
    25
        | Dup_x1                    -- "duplicate top element and push 2 down"
kleing@13676
    26
        | Dup_x2                    -- "duplicate top element and push 3 down"
kleing@12519
    27
        | Swap                      -- "swap top and next to top element"
kleing@12519
    28
        | IAdd                      -- "integer addition"
kleing@12519
    29
        | Goto int                  -- "goto relative address"
kleing@12519
    30
        | Ifcmpeq int               -- "branch if int/ref comparison succeeds"
kleing@12519
    31
        | Throw                     -- "throw top of stack as exception"
kleing@9376
    32
kleing@9376
    33
types
kleing@9376
    34
  bytecode = "instr list"
kleing@12519
    35
  exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
kleing@12519
    36
                  -- "start-pc, end-pc, handler-pc, exception type"
kleing@12519
    37
  exception_table = "exception_entry list"
kleing@12519
    38
  jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
kleing@13676
    39
   -- "max stacksize, size of register set, instruction sequence, handler table"
kleing@12519
    40
  jvm_prog = "jvm_method prog" 
kleing@9376
    41
kleing@9376
    42
end