equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/JVM/LoadAndStore.thy |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 |
|
6 Load and store instructions |
|
7 *) |
|
8 |
|
9 LoadAndStore = JVMState + |
|
10 |
|
11 (** load and store instructions transfer values between local variables |
|
12 and operand stack. Values must all be of the same size (or tagged) **) |
|
13 |
|
14 datatype load_and_store = |
|
15 Load nat (* load from local variable *) |
|
16 | Store nat (* store into local variable *) |
|
17 | Bipush int (* push int *) |
|
18 | Aconst_null (* push null *) |
|
19 |
|
20 |
|
21 consts |
|
22 exec_las :: "[load_and_store,opstack,locvars,p_count] \\<Rightarrow> (opstack \\<times> locvars \\<times> p_count)" |
|
23 primrec |
|
24 "exec_las (Load idx) stk vars pc = ((vars ! idx) # stk , vars , pc+1)" |
|
25 |
|
26 "exec_las (Store idx) stk vars pc = (tl stk , vars[idx:=hd stk] , pc+1)" |
|
27 |
|
28 "exec_las (Bipush ival) stk vars pc = (Intg ival # stk , vars , pc+1)" |
|
29 |
|
30 "exec_las Aconst_null stk vars pc = (Null # stk , vars , pc+1)" |
|
31 |
|
32 end |
|