src/HOL/MicroJava/JVM/JVMExec.thy
author nipkow
Thu, 25 Nov 1999 12:01:28 +0100
changeset 8032 1eaae1a2f8ff
parent 8011 d14c4e9e9c8e
child 8034 6fc37b5c5e98
permissions -rw-r--r--
Minor mods.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/MicroJava/JVM/JVMExec.thy
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     Cornelia Pusch
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1999 Technische Universitaet Muenchen
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     5
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     6
Execution of the JVM
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     7
*)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     8
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     9
JVMExec = LoadAndStore + Object + Method + Opstack + Control + 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    10
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    11
datatype
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    12
 instr	= LS load_and_store	
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    13
        | CO create_object	
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    14
        | MO manipulate_object	
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    15
	| CH check_object	
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    16
	| MI meth_inv		
8032
1eaae1a2f8ff Minor mods.
nipkow
parents: 8011
diff changeset
    17
	| MR meth_ret
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    18
	| OS op_stack		
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    19
	| BR branch
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    20
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    21
types
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    22
 bytecode = instr list
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    23
 jvm_prog = "(nat \\<times> bytecode)prog"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    24
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    25
consts
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    26
 exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    27
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    28
(** exec is not recursive. recdef is just used because for pattern matching **)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    29
recdef exec "{}"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    30
 "exec (G, xp, hp, []) = None"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    31
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    32
 "exec (G, None, hp, (stk,loc,cn,ml,pc)#frs) = 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    33
   Some (case snd(snd(snd(the(cmethd (G,cn) ml)))) ! pc of
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    34
      LS ins \\<Rightarrow> (let (stk',loc',pc') = exec_las ins stk loc pc
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    35
		in
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    36
		(None,hp,(stk',loc',cn,ml,pc')#frs))
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    37
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    38
    | CO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_co ins G hp stk pc
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    39
		in
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    40
		(xp',hp',(stk',loc,cn,ml,pc')#frs))	    
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    41
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    42
    | MO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_mo ins hp stk pc
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    43
		in
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    44
		(xp',hp',(stk',loc,cn,ml,pc')#frs))	
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    45
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    46
    | CH ins \\<Rightarrow> (let (xp',stk',pc') = exec_ch ins G hp stk pc
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    47
		in
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    48
		(xp',hp,(stk',loc,cn,ml,pc')#frs))
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    49
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    50
    | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    51
		in
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    52
		(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    53
8032
1eaae1a2f8ff Minor mods.
nipkow
parents: 8011
diff changeset
    54
    | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    55
		(None,hp,frs'))
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    56
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    57
    | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    58
		in
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    59
		(None,hp,(stk',loc,cn,ml,pc')#frs))
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    60
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    61
    | BR ins \\<Rightarrow> (let (stk',pc') = exec_br ins stk pc
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    62
		in
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    63
		(None,hp,(stk',loc,cn,ml,pc')#frs)))"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    64
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    65
 "exec (G, Some xp, hp, f#frs) = Some (Some xp, hp, [])"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    66
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    67
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    68
constdefs
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    69
 exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool"  ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    70
 "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    71
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    72
end