src/HOL/MicroJava/BV/BVSpec.thy
author nipkow
Thu Nov 11 12:23:45 1999 +0100 (1999-11-11)
changeset 8011 d14c4e9e9c8e
child 8023 3e5ddca613dd
permissions -rw-r--r--
*** empty log message ***
nipkow@8011
     1
(*  Title:      HOL/MicroJava/BV/BVSpec.thy
nipkow@8011
     2
    ID:         $Id$
nipkow@8011
     3
    Author:     Cornelia Pusch
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
nipkow@8011
     5
nipkow@8011
     6
Specification of bytecode verifier
nipkow@8011
     7
*)
nipkow@8011
     8
nipkow@8011
     9
BVSpec = Convert +
nipkow@8011
    10
nipkow@8011
    11
types
nipkow@8011
    12
 method_type 	= "state_type list"
nipkow@8011
    13
 class_type	= "sig \\<Rightarrow> method_type"
nipkow@8011
    14
 prog_type	= "cname \\<Rightarrow> class_type"
nipkow@8011
    15
nipkow@8011
    16
consts
nipkow@8011
    17
 wt_LS	:: "[load_and_store,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
nipkow@8011
    18
primrec
nipkow@8011
    19
"wt_LS (Load idx) G phi max_pc pc =
nipkow@8011
    20
	(let (ST,LT) = phi ! pc
nipkow@8011
    21
	 in
nipkow@8011
    22
	 pc+1 < max_pc \\<and>
nipkow@8011
    23
	 idx < length LT \\<and>
nipkow@8011
    24
	 (\\<exists>ts. (LT ! idx) = Some ts \\<and> 
nipkow@8011
    25
	       G \\<turnstile> phi ! (pc+1) >>>= (ts # ST , LT)))"
nipkow@8011
    26
nipkow@8011
    27
"wt_LS (Store idx) G phi max_pc pc =
nipkow@8011
    28
	(let (ST,LT) = phi ! pc
nipkow@8011
    29
	 in
nipkow@8011
    30
	 pc+1 < max_pc \\<and>
nipkow@8011
    31
	 idx < length LT \\<and>
nipkow@8011
    32
	 (\\<exists>ts ST'. ST = ts # ST' \\<and>
nipkow@8011
    33
		   G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT[idx:=Some ts])))"
nipkow@8011
    34
nipkow@8011
    35
"wt_LS (Bipush i) G phi max_pc pc =
nipkow@8011
    36
	(let (ST,LT) = phi ! pc
nipkow@8011
    37
	 in
nipkow@8011
    38
	 pc+1 < max_pc \\<and>
nipkow@8011
    39
	 G \\<turnstile> phi ! (pc+1) >>>= ((PrimT Integer) # ST , LT))"
nipkow@8011
    40
nipkow@8011
    41
"wt_LS (Aconst_null) G phi max_pc pc =
nipkow@8011
    42
	(let (ST,LT) = phi ! pc
nipkow@8011
    43
	 in
nipkow@8011
    44
	 pc+1 < max_pc \\<and>
nipkow@8011
    45
	 G \\<turnstile> phi ! (pc+1) >>>= (NT # ST , LT))"
nipkow@8011
    46
nipkow@8011
    47
consts
nipkow@8011
    48
 wt_MO	:: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
nipkow@8011
    49
primrec
nipkow@8011
    50
"wt_MO (Getfield F C) G phi max_pc pc =
nipkow@8011
    51
	(let (ST,LT) = phi ! pc
nipkow@8011
    52
	 in
nipkow@8011
    53
	 pc+1 < max_pc \\<and>
nipkow@8011
    54
	 is_class G C \\<and>
nipkow@8011
    55
	 (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
nipkow@8011
    56
                       ST = oT # ST' \\<and> 
nipkow@8011
    57
		       G \\<turnstile> oT \\<preceq> (Class C) \\<and>
nipkow@8011
    58
		       G \\<turnstile> phi ! (pc+1) >>>= (T # ST' , LT)))"
nipkow@8011
    59
nipkow@8011
    60
"wt_MO (Putfield F C) G phi max_pc pc =
nipkow@8011
    61
	(let (ST,LT) = phi ! pc
nipkow@8011
    62
	 in
nipkow@8011
    63
	 pc+1 < max_pc \\<and>
nipkow@8011
    64
	 is_class G C \\<and> 
nipkow@8011
    65
	 (\\<exists>T vT oT ST'.
nipkow@8011
    66
             cfield (G,C) F = Some(C,T) \\<and>
nipkow@8011
    67
             ST = vT # oT # ST' \\<and> 
nipkow@8011
    68
             G \\<turnstile> oT \\<preceq> (Class C) \\<and>
nipkow@8011
    69
	     G \\<turnstile> vT \\<preceq> T  \\<and>
nipkow@8011
    70
             G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT)))"
nipkow@8011
    71
nipkow@8011
    72
nipkow@8011
    73
consts 
nipkow@8011
    74
 wt_CO	:: "[create_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
nipkow@8011
    75
primrec
nipkow@8011
    76
"wt_CO (New C) G phi max_pc pc =
nipkow@8011
    77
	(let (ST,LT) = phi ! pc
nipkow@8011
    78
	 in
nipkow@8011
    79
	 pc+1 < max_pc \\<and>
nipkow@8011
    80
	 is_class G C \\<and>
nipkow@8011
    81
	 G \\<turnstile> phi ! (pc+1) >>>= ((Class C) # ST , LT))"
nipkow@8011
    82
nipkow@8011
    83
consts
nipkow@8011
    84
 wt_CH	:: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
nipkow@8011
    85
primrec
nipkow@8011
    86
"wt_CH (Checkcast C) G phi max_pc pc = 
nipkow@8011
    87
	(let (ST,LT) = phi ! pc
nipkow@8011
    88
	 in
nipkow@8011
    89
	 pc+1 < max_pc \\<and>
nipkow@8011
    90
	 is_class G C \\<and> 
nipkow@8011
    91
	 (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
nipkow@8011
    92
                   G \\<turnstile> phi ! (pc+1) >>>= (Class C # ST' , LT)))"
nipkow@8011
    93
nipkow@8011
    94
consts 
nipkow@8011
    95
 wt_OS	:: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
nipkow@8011
    96
primrec
nipkow@8011
    97
"wt_OS Pop G phi max_pc pc =
nipkow@8011
    98
	(let (ST,LT) = phi ! pc
nipkow@8011
    99
	 in
nipkow@8011
   100
	 \\<exists>ts ST'. pc+1 < max_pc \\<and>
nipkow@8011
   101
		ST = ts # ST' \\<and> 	 
nipkow@8011
   102
		G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT))"
nipkow@8011
   103
nipkow@8011
   104
"wt_OS Dup G phi max_pc pc =
nipkow@8011
   105
	(let (ST,LT) = phi ! pc
nipkow@8011
   106
	 in
nipkow@8011
   107
	 pc+1 < max_pc \\<and>
nipkow@8011
   108
	 (\\<exists>ts ST'. ST = ts # ST' \\<and> 	 
nipkow@8011
   109
		   G \\<turnstile> phi ! (pc+1) >>>= (ts # ts # ST' , LT)))"
nipkow@8011
   110
nipkow@8011
   111
"wt_OS Dup_x1 G phi max_pc pc =
nipkow@8011
   112
	(let (ST,LT) = phi ! pc
nipkow@8011
   113
	 in
nipkow@8011
   114
	 pc+1 < max_pc \\<and>
nipkow@8011
   115
	 (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and> 	 
nipkow@8011
   116
		   G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts1 # ST' , LT)))"
nipkow@8011
   117
nipkow@8011
   118
"wt_OS Dup_x2 G phi max_pc pc =
nipkow@8011
   119
	(let (ST,LT) = phi ! pc
nipkow@8011
   120
	 in
nipkow@8011
   121
	 pc+1 < max_pc \\<and>
nipkow@8011
   122
	 (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and> 	 
nipkow@8011
   123
		   G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts3 # ts1 # ST' , LT)))"
nipkow@8011
   124
nipkow@8011
   125
"wt_OS Swap G phi max_pc pc =
nipkow@8011
   126
	(let (ST,LT) = phi ! pc
nipkow@8011
   127
	 in
nipkow@8011
   128
	 pc+1 < max_pc \\<and>
nipkow@8011
   129
	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
nipkow@8011
   130
		       G \\<turnstile> phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))"
nipkow@8011
   131
nipkow@8011
   132
consts 
nipkow@8011
   133
 wt_BR	:: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
nipkow@8011
   134
primrec
nipkow@8011
   135
"wt_BR (Ifcmpeq branch) G phi max_pc pc =
nipkow@8011
   136
	(let (ST,LT) = phi ! pc
nipkow@8011
   137
	 in
nipkow@8011
   138
	 pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and> 
nipkow@8011
   139
	 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>  ts = ts' \\<and>
nipkow@8011
   140
		       G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT) \\<and>
nipkow@8011
   141
		       G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
nipkow@8011
   142
"wt_BR (Goto branch) G phi max_pc pc =
nipkow@8011
   143
	(let (ST,LT) = phi ! pc
nipkow@8011
   144
	 in
nipkow@8011
   145
	 (nat(int pc+branch)) < max_pc \\<and> 
nipkow@8011
   146
	 G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST , LT))"
nipkow@8011
   147
nipkow@8011
   148
consts
nipkow@8011
   149
 wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
nipkow@8011
   150
primrec
nipkow@8011
   151
"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc =
nipkow@8011
   152
	(let (ST,LT) = phi ! pc
nipkow@8011
   153
	 in
nipkow@8011
   154
         pc+1 < max_pc \\<and>
nipkow@8011
   155
         (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
nipkow@8011
   156
         length apTs = length fpTs \\<and>
nipkow@8011
   157
         (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
nipkow@8011
   158
         (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
nipkow@8011
   159
         G \\<turnstile> phi ! (pc+1) >>>= (rT # ST' , LT))))"
nipkow@8011
   160
nipkow@8011
   161
constdefs
nipkow@8011
   162
 wt_MR	:: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
nipkow@8011
   163
"wt_MR G rT phi pc \\<equiv>
nipkow@8011
   164
	(let (ST,LT) = phi ! pc
nipkow@8011
   165
	 in
nipkow@8011
   166
	 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
nipkow@8011
   167
nipkow@8011
   168
nipkow@8011
   169
constdefs
nipkow@8011
   170
 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool"
nipkow@8011
   171
 "wt_instr instr G rT phi max_pc pc \\<equiv>
nipkow@8011
   172
	case instr of
nipkow@8011
   173
	  LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc
nipkow@8011
   174
	| CO  ins \\<Rightarrow> wt_CO ins G phi max_pc pc
nipkow@8011
   175
	| MO  ins \\<Rightarrow> wt_MO ins G phi max_pc pc
nipkow@8011
   176
	| CH  ins \\<Rightarrow> wt_CH ins G phi max_pc pc
nipkow@8011
   177
	| MI  ins \\<Rightarrow> wt_MI ins G phi max_pc pc
nipkow@8011
   178
	| MR      \\<Rightarrow> wt_MR     G rT phi pc
nipkow@8011
   179
	| OS  ins \\<Rightarrow> wt_OS ins G phi max_pc pc
nipkow@8011
   180
	| BR  ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
nipkow@8011
   181
nipkow@8011
   182
nipkow@8011
   183
constdefs
nipkow@8011
   184
 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
nipkow@8011
   185
 "wt_start G C pTs mxl phi \\<equiv> 
nipkow@8011
   186
    G \\<turnstile> phi!0 >>>= ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))"
nipkow@8011
   187
nipkow@8011
   188
nipkow@8011
   189
 wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
nipkow@8011
   190
 "wt_method G cn pTs rT mxl ins phi \\<equiv>
nipkow@8011
   191
	let max_pc = length ins
nipkow@8011
   192
        in
nipkow@8011
   193
	0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and> 
nipkow@8011
   194
	(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
nipkow@8011
   195
nipkow@8011
   196
 wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
nipkow@8011
   197
"wt_jvm_prog G phi \\<equiv>
nipkow@8011
   198
   wf_prog (\\<lambda>G C (sig,rT,maxl,b).
nipkow@8011
   199
              wt_method G C (snd sig) rT maxl b (phi C sig)) G"
nipkow@8011
   200
nipkow@8011
   201
end