flat instruction set, op. semantics now in JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/Control.thy Mon Jul 17 14:00:53 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: HOL/MicroJava/JVM/Control.thy
- ID: $Id$
- Author: Cornelia Pusch
- Copyright 1999 Technische Universitaet Muenchen
-
-(Un)conditional branch instructions
-*)
-
-Control = JVMState +
-
-datatype branch = Goto int
- | Ifcmpeq int (** Branch if int/ref comparison succeeds **)
-
-
-consts
- exec_br :: "[branch,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)"
-
-primrec
- "exec_br (Ifcmpeq i) stk pc =
- (let (val1,val2) = (hd stk, hd (tl stk));
- pc' = if val1 = val2 then nat(int pc+i) else pc+1
- in
- (tl (tl stk),pc'))"
- "exec_br (Goto i) stk pc = (stk, nat(int pc+i))"
-
-end
--- a/src/HOL/MicroJava/JVM/LoadAndStore.thy Mon Jul 17 14:00:53 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: HOL/MicroJava/JVM/LoadAndStore.thy
- ID: $Id$
- Author: Cornelia Pusch
- Copyright 1999 Technische Universitaet Muenchen
-
-Load and store instructions
-*)
-
-LoadAndStore = JVMState +
-
-(** load and store instructions transfer values between local variables
- and operand stack. Values must all be of the same size (or tagged) **)
-
-datatype load_and_store =
- Load nat (* load from local variable *)
-| Store nat (* store into local variable *)
-| Bipush int (* push int *)
-| Aconst_null (* push null *)
-
-
-consts
- exec_las :: "[load_and_store,opstack,locvars,p_count] \\<Rightarrow> (opstack \\<times> locvars \\<times> p_count)"
-primrec
- "exec_las (Load idx) stk vars pc = ((vars ! idx) # stk , vars , pc+1)"
-
- "exec_las (Store idx) stk vars pc = (tl stk , vars[idx:=hd stk] , pc+1)"
-
- "exec_las (Bipush ival) stk vars pc = (Intg ival # stk , vars , pc+1)"
-
- "exec_las Aconst_null stk vars pc = (Null # stk , vars , pc+1)"
-
-end
--- a/src/HOL/MicroJava/JVM/Method.thy Mon Jul 17 14:00:53 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: HOL/MicroJava/JVM/Method.thy
- ID: $Id$
- Author: Cornelia Pusch
- Copyright 1999 Technische Universitaet Muenchen
-
-Method invocation
-*)
-
-Method = JVMState +
-
-(** method invocation and return instructions **)
-
-datatype
- meth_inv =
- Invoke mname (ty list) (** inv. instance meth of an object **)
-
-consts
- exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count]
- \\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)"
-primrec
- "exec_mi (Invoke mn ps) G hp stk pc =
- (let n = length ps;
- argsoref = take (n+1) stk;
- oref = last argsoref;
- xp' = raise_xcpt (oref=Null) NullPointer;
- dynT = fst(the(hp(the_Addr oref)));
- (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
- frs' = if xp'=None
- then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
- else []
- in
- (xp' , frs' , drop (n+1) stk , pc+1))"
-
-
-datatype
- meth_ret = Return
-
-consts
- exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list"
-primrec
- "exec_mr Return stk0 frs =
- (if frs=[] then []
- else let val = hd stk0; (stk,loc,C,sig,pc) = hd frs
- in (val#stk,loc,C,sig,pc)#tl frs)"
-
-end
--- a/src/HOL/MicroJava/JVM/Object.thy Mon Jul 17 14:00:53 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(* Title: HOL/MicroJava/JVM/Object.thy
- ID: $Id$
- Author: Cornelia Pusch
- Copyright 1999 Technische Universitaet Muenchen
-
-Get and putfield instructions
-*)
-
-Object = JVMState +
-
-datatype
- create_object = New cname
-
-consts
- exec_co :: "[create_object,'code prog,aheap,opstack,p_count] \\<Rightarrow>
- (xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
-
-
-primrec
- "exec_co (New C) G hp stk pc =
- (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
- oref = newref hp;
- fs = init_vars (fields(G,C));
- hp' = if xp'=None then hp(oref \\<mapsto> (C,fs)) else hp;
- stk' = if xp'=None then (Addr oref)#stk else stk
- in (xp' , hp' , stk' , pc+1))"
-
-
-datatype
- manipulate_object =
- Getfield vname cname (* Fetch field from object *)
- | Putfield vname cname (* Set field in object *)
-
-consts
- exec_mo :: "[manipulate_object,aheap,opstack,p_count] \\<Rightarrow>
- (xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
-
-primrec
- "exec_mo (Getfield F C) hp stk pc =
- (let oref = hd stk;
- xp' = raise_xcpt (oref=Null) NullPointer;
- (oc,fs) = the(hp(the_Addr oref));
- stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk
- in
- (xp' , hp , stk' , pc+1))"
-
- "exec_mo (Putfield F C) hp stk pc =
- (let (fval,oref)= (hd stk, hd(tl stk));
- xp' = raise_xcpt (oref=Null) NullPointer;
- a = the_Addr oref;
- (oc,fs) = the(hp a);
- hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp
- in
- (xp' , hp' , tl (tl stk), pc+1))"
-
-
-datatype
- check_object =
- Checkcast cname (* Check whether object is of given type *)
-
-consts
- exec_ch :: "[check_object,'code prog,aheap,opstack,p_count]
- \\<Rightarrow> (xcpt option \\<times> opstack \\<times> p_count)"
-
-primrec
- "exec_ch (Checkcast C) G hp stk pc =
- (let oref = hd stk;
- xp' = raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast;
- stk' = if xp'=None then stk else tl stk
- in
- (xp' , stk' , pc+1))"
-
-end
--- a/src/HOL/MicroJava/JVM/Opstack.thy Mon Jul 17 14:00:53 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* Title: HOL/MicroJava/JVM/Opstack.thy
- ID: $Id$
- Author: Cornelia Pusch
- Copyright 1999 Technische Universitaet Muenchen
-
-Manipulation of operand stack
-*)
-
-Opstack = JVMState +
-
-(** instructions for the direct manipulation of the operand stack **)
-
-datatype
- op_stack =
- Pop
- | Dup
- | Dup_x1
- | Dup_x2
- | Swap
- | IAdd
-
-consts
- exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)"
-
-primrec
- "exec_os Pop stk pc = (tl stk , pc+1)"
-
- "exec_os Dup stk pc = (hd stk # stk , pc+1)"
-
- "exec_os Dup_x1 stk pc = (hd stk # hd (tl stk) # hd stk # (tl (tl stk)) , pc+1)"
-
- "exec_os Dup_x2 stk pc = (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))) , pc+1)"
-
- "exec_os Swap stk pc =
- (let (val1,val2) = (hd stk,hd (tl stk))
- in
- (val2#val1#(tl (tl stk)) , pc+1))"
-
- "exec_os IAdd stk pc =
- (let (val1,val2) = (hd stk,hd (tl stk))
- in
- (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))"
-
-end