|
8011
|
1 |
(* Title: HOL/MicroJava/JVM/Control.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Cornelia Pusch
|
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
|
5 |
|
|
|
6 |
(Un)conditional branch instructions
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Control = JVMState +
|
|
|
10 |
|
|
|
11 |
datatype branch = Goto int
|
|
|
12 |
| Ifcmpeq int (** Branch if int/ref comparison succeeds **)
|
|
|
13 |
|
|
|
14 |
|
|
|
15 |
consts
|
|
|
16 |
exec_br :: "[branch,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)"
|
|
|
17 |
|
|
|
18 |
primrec
|
|
|
19 |
"exec_br (Ifcmpeq i) stk pc =
|
|
|
20 |
(let (val1,val2) = (hd stk, hd (tl stk));
|
|
|
21 |
pc' = if val1 = val2 then nat(int pc+i) else pc+1
|
|
|
22 |
in
|
|
|
23 |
(tl (tl stk),pc'))"
|
|
|
24 |
"exec_br (Goto i) stk pc = (stk, nat(int pc+i))"
|
|
|
25 |
|
|
|
26 |
end
|