isabelle: src/HOL/MicroJava/JVM/JVMInstructions.thy@f8353c722d4e (annotated)

9376 c32c5696ec2a flat instruction set kleing parents: diff changeset	1	(* Title: HOL/MicroJava/JVM/JVMInstructions.thy
c32c5696ec2a flat instruction set kleing parents: diff changeset	2	ID: $Id$
c32c5696ec2a flat instruction set kleing parents: diff changeset	3	Author: Gerwin Klein
c32c5696ec2a flat instruction set kleing parents: diff changeset	4	Copyright 2000 Technische Universitaet Muenchen
c32c5696ec2a flat instruction set kleing parents: diff changeset	5	*)
c32c5696ec2a flat instruction set kleing parents: diff changeset	6
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	7	header {* Instructions of the JVM *}
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	8
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	9
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	10	theory JVMInstructions = JVMState:
9376 c32c5696ec2a flat instruction set kleing parents: diff changeset	11
9550 19a6d1289f5e Invoke instruction gets fully qualified method name (class+name+sig) as kleing parents: 9376 diff changeset	12
9376 c32c5696ec2a flat instruction set kleing parents: diff changeset	13	datatype
c32c5696ec2a flat instruction set kleing parents: diff changeset	14	instr = Load nat (* load from local variable *)
c32c5696ec2a flat instruction set kleing parents: diff changeset	15	\| Store nat (* store into local variable *)
10897 697fab84709e removed instructions Aconst_null+Bipush, introduced LitPush kleing parents: 10591 diff changeset	16	\| LitPush val (* push a literal (constant) *)
9376 c32c5696ec2a flat instruction set kleing parents: diff changeset	17	\| New cname (* create object *)
c32c5696ec2a flat instruction set kleing parents: diff changeset	18	\| Getfield vname cname (* Fetch field from object *)
c32c5696ec2a flat instruction set kleing parents: diff changeset	19	\| Putfield vname cname (* Set field in object *)
c32c5696ec2a flat instruction set kleing parents: diff changeset	20	\| Checkcast cname (* Check whether object is of given type *)
9550 19a6d1289f5e Invoke instruction gets fully qualified method name (class+name+sig) as kleing parents: 9376 diff changeset	21	\| Invoke cname mname "(ty list)" (* inv. instance meth of an object *)
10057 8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	22	\| Return (* return from method *)
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	23	\| Pop (* pop top element from opstack *)
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	24	\| Dup (* duplicate top element of opstack *)
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	25	\| Dup_x1 (* duplicate next to top element *)
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	26	\| Dup_x2 (* duplicate 3rd element *)
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	27	\| Swap (* swap top and next to top element *)
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	28	\| IAdd (* integer addition *)
8c8d2d0d3ef8 converted to Isar, tuned kleing parents: 9550 diff changeset	29	\| Goto int (* goto relative address *)
9376 c32c5696ec2a flat instruction set kleing parents: diff changeset	30	\| Ifcmpeq int (* Branch if int/ref comparison succeeds *)
c32c5696ec2a flat instruction set kleing parents: diff changeset	31
c32c5696ec2a flat instruction set kleing parents: diff changeset	32
c32c5696ec2a flat instruction set kleing parents: diff changeset	33	types
c32c5696ec2a flat instruction set kleing parents: diff changeset	34	bytecode = "instr list"
10591 6d6cb845e841 jvm_progs now also store maximum op_stack depth kleing parents: 10057 diff changeset	35	jvm_prog = "(nat \<times> nat \<times> bytecode) prog"
9376 c32c5696ec2a flat instruction set kleing parents: diff changeset	36
c32c5696ec2a flat instruction set kleing parents: diff changeset	37	end

author	paulson
	Tue, 01 May 2001 17:16:32 +0200
changeset 11276	f8353c722d4e
parent 10897	697fab84709e
child 12519	a955fe2879ba
permissions	-rw-r--r--