# HG changeset patch # User kleing # Date 963835329 -7200 # Node ID 59dc5c4d1a57c457599a823a45edd292a6e4c6cb # Parent c32c5696ec2a65767670412522def1439c336e2d flat instruction set, op. semantics now in JVMExecInstr.thy diff -r c32c5696ec2a -r 59dc5c4d1a57 src/HOL/MicroJava/JVM/Control.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] \\ (opstack \\ 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 diff -r c32c5696ec2a -r 59dc5c4d1a57 src/HOL/MicroJava/JVM/LoadAndStore.thy --- 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] \\ (opstack \\ locvars \\ 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 diff -r c32c5696ec2a -r 59dc5c4d1a57 src/HOL/MicroJava/JVM/Method.thy --- 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 \\ 'c)prog,aheap,opstack,p_count] - \\ (xcpt option \\ frame list \\ opstack \\ 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] \\ 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 diff -r c32c5696ec2a -r 59dc5c4d1a57 src/HOL/MicroJava/JVM/Object.thy --- 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] \\ - (xcpt option \\ aheap \\ opstack \\ p_count)" - - -primrec - "exec_co (New C) G hp stk pc = - (let xp' = raise_xcpt (\\x. hp x \\ None) OutOfMemory; - oref = newref hp; - fs = init_vars (fields(G,C)); - hp' = if xp'=None then hp(oref \\ (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] \\ - (xcpt option \\ aheap \\ opstack \\ 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 \\ (oc, fs((F,C) \\ 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] - \\ (xcpt option \\ opstack \\ p_count)" - -primrec - "exec_ch (Checkcast C) G hp stk pc = - (let oref = hd stk; - xp' = raise_xcpt (\\ cast_ok G C hp oref) ClassCast; - stk' = if xp'=None then stk else tl stk - in - (xp' , stk' , pc+1))" - -end diff -r c32c5696ec2a -r 59dc5c4d1a57 src/HOL/MicroJava/JVM/Opstack.thy --- 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] \\ (opstack \\ 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