9 |
9 |
10 theory JVMInstructions = JVMState: |
10 theory JVMInstructions = JVMState: |
11 |
11 |
12 |
12 |
13 datatype |
13 datatype |
14 instr = Load nat (* load from local variable *) |
14 instr = Load nat -- "load from local variable" |
15 | Store nat (* store into local variable *) |
15 | Store nat -- "store into local variable" |
16 | LitPush val (* push a literal (constant) *) |
16 | LitPush val -- "push a literal (constant)" |
17 | New cname (* create object *) |
17 | New cname -- "create object" |
18 | Getfield vname cname (* Fetch field from object *) |
18 | Getfield vname cname -- "Fetch field from object" |
19 | Putfield vname cname (* Set field in object *) |
19 | Putfield vname cname -- "Set field in object " |
20 | Checkcast cname (* Check whether object is of given type *) |
20 | Checkcast cname -- "Check whether object is of given type" |
21 | Invoke cname mname "(ty list)" (* inv. instance meth of an object *) |
21 | Invoke cname mname "(ty list)" -- "inv. instance meth of an object" |
22 | Return (* return from method *) |
22 | Return -- "return from method" |
23 | Pop (* pop top element from opstack *) |
23 | Pop -- "pop top element from opstack" |
24 | Dup (* duplicate top element of opstack *) |
24 | Dup -- "duplicate top element of opstack" |
25 | Dup_x1 (* duplicate next to top element *) |
25 | Dup_x1 -- "duplicate next to top element" |
26 | Dup_x2 (* duplicate 3rd element *) |
26 | Dup_x2 -- "duplicate 3rd element" |
27 | Swap (* swap top and next to top element *) |
27 | Swap -- "swap top and next to top element" |
28 | IAdd (* integer addition *) |
28 | IAdd -- "integer addition" |
29 | Goto int (* goto relative address *) |
29 | Goto int -- "goto relative address" |
30 | Ifcmpeq int (* Branch if int/ref comparison succeeds *) |
30 | Ifcmpeq int -- "branch if int/ref comparison succeeds" |
31 |
31 | Throw -- "throw top of stack as exception" |
32 |
32 |
33 types |
33 types |
34 bytecode = "instr list" |
34 bytecode = "instr list" |
35 jvm_prog = "(nat \<times> nat \<times> bytecode) prog" |
35 exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" |
|
36 -- "start-pc, end-pc, handler-pc, exception type" |
|
37 exception_table = "exception_entry list" |
|
38 jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table" |
|
39 jvm_prog = "jvm_method prog" |
36 |
40 |
37 end |
41 end |