mod TYPES is protecting INT . sorts Type TypeList . subsort Type < TypeList . op emptyTypeList : -> TypeList . op __ : TypeList TypeList -> TypeList [assoc id: emptyTypeList] . --- Primitive Types op int : -> Type . op byte : -> Type . op short : -> Type . op float : -> Type . op double : -> Type . op long : -> Type . op char : -> Type . op boolean : -> Type . op type : Int -> Type . eq type(10) = int . eq type(8) = byte . eq type(9) = short . eq type(6) = float . eq type(7) = double . eq type(11) = long . eq type(5) = char . eq type(4) = boolean . endm mod BYTECODE-SYNTAX is protecting QID . protecting TYPES . sorts Pgm Instruction . subsort Instruction < Pgm . op emptyPgm : -> Pgm . op __ : Pgm Pgm -> Pgm [assoc id: emptyPgm] . sorts Reference Index Value . subsort Int < Index . subsort Int < Value . op Null : -> Value . op size : Instruction -> Int . --- number of bytes that the instruction will occupy in memory including its operands --- NOP op nop : -> Instruction . eq size(nop) = 1 . --- ICONST : pushes constants onto operand stack op iconstm1 : -> Instruction . op iconst0 : -> Instruction . op iconst1 : -> Instruction . op iconst2 : -> Instruction . op iconst3 : -> Instruction . op iconst4 : -> Instruction . op iconst5 : -> Instruction . eq size(iconstm1) = 1 . eq size(iconst1) = 1 . eq size(iconst0) = 1 . eq size(iconst2) = 1 . eq size(iconst3) = 1 . eq size(iconst4) = 1 . eq size(iconst5) = 1 . --- ACONST_NULL : pushes a null object onto the operand stack op aconstNull : -> Instruction . eq size(aconstNull) = 1 . --- BIPUSH : pushes an integer -127 < x < 127 on the operand-stack op bipush : Int -> Instruction . eq size(bipush(I)) = 2 . --- POP : pops the top word from the operand stack op pop : -> Instruction . eq size(pop) = 1 . --- SWAP : swaps the top two words of the operand stack op swap : -> Instruction . eq size(swap) = 1 . --- DUP : duplicates the top word of the operand stack op dup : -> Instruction . eq size(dup) = 1 . --- ILOAD : pushes int from local variable position index op iload_ : Index -> Instruction . op iload0 : -> Instruction . op iload1 : -> Instruction . op iload2 : -> Instruction . op iload3 : -> Instruction . vars I J : Int . eq size(iload(I)) = 2 . eq size(iload0) = 1 . eq size(iload1) = 1 . eq size(iload2) = 1 . eq size(iload3) = 1 . --- ALOAD : pushes object reference from local variable position index op aload_ : Index -> Instruction . op aload0 : -> Instruction . op aload1 : -> Instruction . op aload2 : -> Instruction . op aload3 : -> Instruction . eq size(aload(I)) = 2 . eq size(aload0) = 1 . eq size(aload1) = 1 . eq size(aload2) = 1 . eq size(aload3) = 1 . --- ISTORE : pops int from local variable position index op istore_ : Index -> Instruction . op istore0 : -> Instruction . op istore1 : -> Instruction . op istore2 : -> Instruction . op istore3 : -> Instruction . eq size(istore(I)) = 2 . eq size(istore0) = 1 . eq size(istore1) = 1 . eq size(istore2) = 1 . eq size(istore3) = 1 . --- ASTORE : pops object reference from local variable position index op astore_ : Index -> Instruction . op astore0 : -> Instruction . op astore1 : -> Instruction . op astore2 : -> Instruction . op astore3 : -> Instruction . eq size(astore(I)) = 2 . eq size(astore0) = 1 . eq size(astore1) = 1 . eq size(astore2) = 1 . eq size(astore3) = 1 . --- we could add "wide" here to extend the indexing of local variables from 256 to 65536. Not yet I think! --- IADD : pops two ints, adds them, and pushes the int result op iadd : -> Instruction . eq size(iadd) = 1 . --- ISUB : pops two ints, subtracts them, and pushes the int result op isub : -> Instruction . eq size(isub) = 1 . --- IMUL : pops two ints, multiplies them, and pushes the int result op imul : -> Instruction . eq size(imul) = 1 . --- IDIV : pops two ints, divides them, and pushes the int result op idiv : -> Instruction . eq size(idiv) = 1 . --- IREM : pops two ints, divides them, and pushes the int remainder op irem : -> Instruction . eq size(irem) = 1 . --- INEG : pops an int, negates it, and pushes the result op ineg : -> Instruction . eq size(ineg) = 1 . --- IAND : boolean ANDs two ints op iand : -> Instruction . eq size(iand) = 1 . --- IOR : boolean ORs two ints op ior : -> Instruction . eq size(ior) = 1 . --- IAND : boolean XORs two ints op ixor : -> Pgm . eq size(ixor) = 1 . --- IFEQ : pop int value, if value == 0, branch to offset op ifeq_ : Int -> Instruction . eq size(ifeq(I)) = 3 . --- IFNE : pop int value, if value != 0, branch to offset op ifne_ : Int -> Instruction . eq size(ifne(I)) = 3 . --- IFLT : pop int value, if value < 0, branch to offset op iflt_ : Int -> Instruction . eq size(iflt(I)) = 3 . --- IFLE : pop int value, if value <= 0, branch to offset op ifle_ : Int -> Instruction . eq size(ifle(I)) = 3 . --- IFGT : pop int value, if value > 0, branch to offset op ifgt_ : Int -> Instruction . eq size(ifgt(I)) = 3 . --- IFGE : pop int value, if value >= 0, branch to offset op ifge_ : Int -> Instruction . eq size(ifge(I)) = 3 . --- IFICMPEQ : pop int v1 and v2, if v1 == v2, branch to offset op ificmpeq_ : Int -> Instruction . eq size(ificmpeq(I)) = 3 . --- IFICMPNE : pop int v1 and v2, if v1 != v2, branch to offset op ificmpne_ : Int -> Instruction . eq size(ificmpne(I)) = 3 . --- IFICMPLT : pop int v1 and v2, if v1 < v2, branch to offset op ificmplt_ : Int -> Instruction . eq size(ificmplt(I)) = 3 . --- IFICMPLE : pop int v1 and v2, if v1 <= v2, branch to offset op ificmple_ : Int -> Instruction . eq size(ificmple(I)) = 3 . --- IFICMPGT : pop int v1 and v2, if v1 > v2, branch to offset op ificmpgt_ : Int -> Instruction . eq size(ificmpgt(I)) = 3 . --- IFICMPGE : pop int v1 and v2, if v1 >= v2, branch to offset op ificmpge_ : Int -> Instruction . eq size(ificmpge(I)) = 3 . --- NEW : creates a new object on the heap, pushes the reference op new_ : Index -> Instruction . eq size(new(I)) = 3 . --- PUTFIELD : sets field, indicated by index, of object to value (both taken from stack) op putfield : Index -> Instruction . eq size(putfield(I)) = 3 . --- GETFIELD : pushes field, indicated by index, of object (taken from stack) op getfield : Index -> Instruction . eq size(getfield(I)) = 3 . --- PUTSTATIC : sets static field, indicated by index, to value (taken from stack) op putstatic : Index -> Instruction . eq size(putstatic(I)) = 3 . --- GETSTATIC : pushes static field, indicated by index op getstatic : Index -> Instruction . eq size(getstatic(I)) = 3 . --- INVOKEVIRTUAL : pop objectref and args , invoke instance method at constant pool index op invokevirtual : Index -> Instruction . eq size(invokevirtual(I)) = 3 . --- INVOKESTATIC : pop args , invoke class method at constant pool index op invokestatic : Index -> Instruction . eq size(invokestatic(I)) = 3 . --- INVOKESPECIAL : pop objectref and args , invoke instance method at constant pool index op invokespecial : Index -> Instruction . eq size(invokespecial(I)) = 3 . --- INVOKEINTERFACE : pop objectref and args , invoke class method at constant pool index op invokeinterface : Index -> Instruction . eq size(invokeinterface(I)) = 3 . --- IRETURN : pop int, push onto stack of calling method and return op ireturn : -> Instruction . eq size(ireturn) = 1 . --- RETURN : return void op return : -> Instruction . eq size(return) = 1 . --- MONITORENTER : enter and acquire object monitor - pop objectref and acquire the lock associated with objectref . op monitorenter : -> Instruction . eq size(monitorenter) = 1 . --- MONITOREXIT : release and exit object monitor - pop objectref and release the lock associated with objectref . op monitorexit : -> Instruction . eq size(monitorexit) = 1 . --- ARRAY OPCODES var T : Type . --- NEWARRAY : pops length, allocates new array of primitive types of type indicated by atype, pushes objectref of new array. op newarray : Type -> Instruction . eq size(newarray(T)) = 2 . --- ANEWARRAY : pops length, allocates new array of object class indicated by index, pushes objectref of new array. op anewarray : Int -> Instruction . eq size(anewarray(I)) = 3 . --- MULTIANEWARRAY : pops dimension number of array lenghts, .... op multianewarray : Int Int -> Instruction . eq size(multianewarray(I, J)) = 4 . --- ARRAYLENGHT : pops objectref of an array and pushes the length of that array. op arraylength : -> Instruction . eq size(arraylength) = 1 . --- BALOAD : pops index and arrayref of an array of bytes or booleans, pushes arrayref[index]. op baload : -> Instruction . eq size(baload) = 1 . --- CALOAD : pops index and arrayref of an array of chars, pushes arrayref[index]. op caload : -> Instruction . eq size(caload) = 1 . --- SALOAD : pops index and arrayref of an array of shorts, pushes arrayref[index]. op saload : -> Instruction . eq size(saload) = 1 . --- IALOAD : pops index and arrayref of an array of ints, pushes arrayref[index]. op iaload : -> Instruction . eq size(iaload) = 1 . --- LALOAD : pops index and arrayref of an array of longs, pushes arrayref[index]. op laload : -> Instruction . eq size(laload) = 1 . --- FALOAD : pops index and arrayref of an array of floats, pushes arrayref[index]. op faload : -> Instruction . eq size(faload) = 1 . --- DALOAD : pops index and arrayref of an array of doubles, pushes arrayref[index]. op daload : -> Instruction . eq size(daload) = 1 . --- AALOAD : pops index and arrayref of an array of objectrefs, pushes arrayref[index]. op aaload : -> Instruction . eq size(aaload) = 1 . --- BASTORE : pops index and arrayref of an array of bytes or booleans, assigns arrayref[index] = value. op bastore : -> Instruction . eq size(bastore) = 1 . --- CASTORE : pops index and arrayref of an array of chars, assigns arrayref[index] = value. op castore : -> Instruction . eq size(castore) = 1 . --- SASTORE : pops index and arrayref of an array of shorts, assigns arrayref[index] = value. op sastore : -> Instruction . eq size(sastore) = 1 . --- IASTORE : pops index and arrayref of an array of ints, assigns arrayref[index] = value. op iastore : -> Instruction . eq size(iastore) = 1 . --- LASTORE : pops index and arrayref of an array of longs, assigns arrayref[index] = value. op lastore : -> Instruction . eq size(lastore) = 1 . --- FASTORE : pops index and arrayref of an array of floats, assigns arrayref[index] = value. op fastore : -> Instruction . eq size(fastore) = 1 . --- DASTORE : pops index and arrayref of an array of doubles, assigns arrayref[index] = value. op dastore : -> Instruction . eq size(dastore) = 1 . --- AASTORE : pops index and arrayref of an array of objectrefs, assigns arrayref[index] = value. op aastore : -> Instruction . eq size(aastore) = 1 . --- ACCEPTIONS op athrow : -> Instruction . eq size(athrow) = 1 . --- SPECIAL INSTRUCTIONS --- PRINT : prints the value on top of the operand stack op print : -> Instruction . eq size(print) = 1 . --- READ : reads the next input and puts it on top of the operand stack op read : -> Instruction . eq size(read) = 1 . --- START THREAD op start : -> Instruction . eq size(start) = 1 . --- WAIT THREAD op wait : -> Instruction . eq size(wait) = 1 . --- NOTIFYALL THREADS op notifyAll : -> Instruction . eq size(notifyAll) = 1 . --- WAKEUP THREADS op wakeup : -> Instruction . eq size(wakeup) = 1 . --- GOTO op goto : Int -> Instruction . eq size(goto(I)) = 3 . endm mod JAVA-CLASSES is protecting BYTECODE-SYNTAX . including CONFIGURATION . sort FieldName . subsort Qid < FieldName . sorts ClassName ClassDecl . ---subsort ClassName < Type . subsort Qid < ClassName . subsort ClassName < Oid . sorts ConstantPool . --- The Constant Pool : At this point we are assuming we have 3 different kinds in it : Integers, References, Strings . op REF_ : Index -> Reference . subsort Int < Value . subsort Qid < Value . --- Might change to String later subsort Reference < Value . subsort ClassName < Value . sort CPEntry . subsort CPEntry < ConstantPool . op [_,_] : Int Value -> CPEntry . op emptyConstantPool : -> ConstantPool . op __ : ConstantPool ConstantPool -> ConstantPool [assoc comm id: emptyConstantPool] . op _[_] : ConstantPool Index -> Value . op _[_<-_] : ConstantPool Index Value -> ConstantPool . sort FieldInfo . --- Required Information for a static field in the constant pool op {_,_} : ClassName FieldName -> FieldInfo . subsort FieldInfo < Value . ---op className : FieldInfo -> ClassName . ---op fieldName : FieldInfo -> FieldName . op className : Value -> ClassName . op fieldName : Value -> FieldName . vars V V' : Value . var I : Index . var Pool : ConstantPool . eq ([I, V] Pool)[I] = V . eq ([I, V'] Pool)[I <- V] = ([I, V] Pool) . var FieldName : FieldName . vars ClName ClassName : ClassName . eq className({ClassName, FieldName}) = ClassName . eq fieldName({ClassName, FieldName}) = FieldName . sort Method . --- Method sort MethodName . subsort Qid < MethodName . sort MethodFormals . --- incomplete subsort TypeList < MethodFormals . sort MethodSync . subsort Bool < MethodSync . sort LabeledPgm . sort ExceptionTable . op {_,_,_,_,_} : MethodName MethodFormals MethodSync LabeledPgm Int -> Method . op methodName : Method -> MethodName . op methodFormals : Method -> MethodFormals . op methodSync : Method -> MethodSync . op methodPgm : Method -> LabeledPgm . op numLocals : Method -> Int . vars MethodName MN : MethodName . var MethodFormals : MethodFormals . var MethodSync : MethodSync . var MethodPgm : LabeledPgm . eq methodName ({ MethodName, MethodFormals, MethodSync, MethodPgm, I}) = MethodName . eq methodFormals({MethodName, MethodFormals, MethodSync, MethodPgm, I}) = MethodFormals . eq methodSync({MethodName, MethodFormals, MethodSync, MethodPgm, I}) = MethodSync . eq methodPgm({MethodName, MethodFormals, MethodSync, MethodPgm, I}) = MethodPgm . eq numLocals({MethodName, MethodFormals, MethodSync, MethodPgm, I}) = I . sort ExceptionEntry . subsort ExceptionEntry < ExceptionTable . op {_,_,_,_} : Int Int Int Int -> ExceptionEntry . op emptyExceptionTable : -> ExceptionTable . op __ : ExceptionTable ExceptionTable -> ExceptionTable [assoc id: emptyExceptionTable] . op match : ExceptionTable Int -> Int . vars J K L M N : Int . var ET : ExceptionTable . eq match(emptyExceptionTable, J) = - 1 . eq match({J, K, M, N} ET, L) = if (L >= J) and (L < K) then M else match(ET, L) fi . op _[_] : MethodList MethodName -> Bool . var ML : MethodList . eq emptyMethodList[MethodName] = false . ---eq ({ MethodName, MethodFormals, MethodSync, MethodPgm, I}, ML)[MN] = if MethodName == MN then true else ML[MN] fi . eq ({ MethodName, MethodFormals, MethodSync, MethodPgm, I}, ML)[MethodName] = true . eq ML[MN] = false [owise] . sort MethodList . subsort Method < MethodList . op emptyMethodList : -> MethodList . op _,_ : MethodList MethodList -> MethodList [assoc comm id: emptyMethodList] . sort FieldNameList . subsort FieldName < FieldNameList . op emptyFieldNameList : -> FieldNameList . op _,_ : FieldNameList FieldNameList -> FieldNameList [assoc comm id: emptyFieldNameList] . ---subsort QidList < FieldNameList . eq FieldName, FieldName = FieldName . sort ClassNameList . subsort ClassName < ClassNameList . op emptyClassNameList : -> ClassNameList . op _;_ : ClassNameList ClassNameList -> ClassNameList [assoc id: emptyClassNameList] . ---subsort QidList < ClassNameList . ---subsort ClassNameList < SuperClasses . sort MethodInfo . subsort MethodInfo < Value . op {_,_,_] : Int MethodName ClassName -> MethodInfo . op methodName : MethodInfo -> MethodName . op nargs : MethodInfo -> Int . op className : MethodInfo -> ClassName . eq nargs({I, MethodName, ClassName]) = I . eq methodName({I, MethodName, ClassName]) = MethodName . eq className({I, MethodName, ClassName]) = ClassName . sort FieldPairList . sort FieldValues . sort OidList . subsort Oid < OidList . op emptyOidList : -> OidList . op _||_ : OidList OidList -> OidList [assoc comm id: emptyOidList] . sort Lock . ---op Lock : Oid Int -> Lock . op Lock : OidList Oid Int -> Lock . op NoThread : -> Oid . --- injaa sort FlatFNL . sort FlatPair . subsort FlatPair < FlatFNL . op emptyFlatFNL : -> FlatFNL . op [{_|_}] : ClassName FieldNameList -> FlatPair . op _~_ : FlatFNL FlatFNL -> FlatFNL [assoc comm id: emptyFlatFNL] . --- remove this later ... sort SuperClasses . subsort ClassNameList < SuperClasses . sort JavaClass . op JavaClass : -> JavaClass . subsort JavaClass < Cid . op SupClass :_ : ClassName -> Attribute . op StaticFields :_ : FieldNameList -> Attribute . op Fields :_ : FieldNameList -> Attribute . op ConstPool :_ : ConstantPool -> Attribute . op Methods :_ : MethodList -> Attribute . op StaticFieldValues :_ : FieldPairList -> Attribute . op Lock :_ : Lock -> Attribute . op StaticFieldValues :_ : FieldValues -> Attribute . op Fields :_ : FlatFNL -> Attribute . ---class JavaClass | SupClasses : SuperClasses , StaticFields : FieldNameList, Fields : FieldNameList, ConstPool : ConstantPool, Methods : MethodList , StaticFieldValues : FieldPairList , Lock : Lock . --- seperating the constant part oSf the class --- the constant part consists of SuperClass, Fields, StaticFields, and Methods sort JavaClassC . op JavaClassC : -> JavaClassC . subsort JavaClassC < Cid . sort JavaClassV . op JavaClassV : -> JavaClassV . subsort JavaClassV < Cid . --- Auxiliary operations for the constant part op superClass : ClassName Configuration -> ClassName [memo] . op numMethodLocals : ClassName MethodName Configuration -> Int [memo] . op methodBody : ClassName MethodName Configuration -> LabeledPgm [memo] . op methodSyncFlag : ClassName MethodName Configuration -> MethodSync [memo] . op fields : ClassName Configuration -> FlatFNL . op getMethod : ClassName MethodName Configuration -> Method [memo] . var Conf : Configuration . var CName : ClassName . var ATT : AttributeSet . var X : Int . var FNL : FlatFNL . op ConstantClasses : -> Configuration . eq getMethod(ClassName, MethodName, < ClassName : JavaClassC | SupClass : ClName, Methods : ({MethodName, MethodFormals, MethodSync, MethodPgm, X}, ML), ATT > Conf) = {MethodName, MethodFormals, MethodSync, MethodPgm, X} . eq getMethod(ClassName, MethodName, < ClassName : JavaClassC | SupClass : ClName, Methods : (ML), ATT > Conf) = getMethod(ClName, MethodName, Conf) [owise] . eq superClass(ClassName, < ClassName : JavaClassC | SupClass : CName, ATT > Conf) = CName . eq fields(ClassName, < ClassName : JavaClassC | Fields : FNL , ATT > Conf) = FNL . eq numMethodLocals(ClassName, MethodName, Conf) = numLocals(getMethod(ClassName, MethodName, Conf)) . eq methodBody(ClassName, MethodName, Conf) = methodPgm(getMethod(ClassName, MethodName, Conf)) . eq methodSyncFlag(ClassName, MethodName, Conf) = methodSync(getMethod(ClassName, MethodName, Conf)) . endm mod JAVA-OBJECTS is protecting JAVA-CLASSES . ---sort FieldValue . ---subsort Value < FieldValue . sort FieldPair . subsort FieldPair < FieldPairList . sort ClassFields . ---sort FieldValues . subsort ClassFields < FieldValues . op emptyFieldValues : -> FieldValues . op __ : FieldValues FieldValues -> FieldValues [assoc comm id: emptyFieldValues] . op [[_,_]] : FieldName Value -> FieldPair . op emptyFieldPairList : -> FieldPairList . op __ : FieldPairList FieldPairList -> FieldPairList [assoc comm id: emptyFieldPairList] . op _[_] : FieldPairList FieldName -> Value . op {_,_} : ClassName FieldPairList -> ClassFields . op _[_,_] : FieldValues ClassName FieldName -> Value . op _[_<-_] : FieldPairList FieldName Value -> FieldPairList . op _[_,_<-_] : FieldValues ClassName FieldName Value -> FieldValues . vars FN FN' : FieldName . vars FV FV' : Value . vars FPL FPL' : FieldPairList . var FP : FieldPair . var CF : ClassFields . var FVS : FieldValues . vars ClassName ClassName' : ClassName . eq FP FP = FP . eq emptyFieldPairList[FN] = 0 . --- OR something like it eq ([[FN, FV]] FPL)[FN] = FV . --- if FN == FN' then FV else FPL[FN'] fi . eq emptyFieldValues[ClassName, FN] = 0 . --- or something like it eq ({ClassName, FPL} FVS)[ClassName , FN] = FPL[FN] . eq emptyFieldPairList[FN <- FV ] = emptyFieldPairList . eq ([[FN, FV]] FPL)[FN <- FV'] = [[FN, FV']] FPL . eq emptyFieldValues[ClassName, FN <- FV] = emptyFieldValues . eq ({ClassName, FPL} FVS)[ClassName , FN <- FV] = {ClassName, FPL[FN <- FV]} FVS . ---( eq emptyFieldValues[ClassName, FN] = 0 . --- or something like it eq ({ClassName, FPL} FVS)[ClassName' , FN] = if ClassName == ClassName' then FPL[FN] else FVS[ClassName', FN] fi . eq emptyFieldValues[ClassName, FN <- FV] = emptyFieldValues . eq ({ClassName, FPL} FVS)[ClassName' , FN <- FV] = if ClassName == ClassName' then ({ClassName, FPL[FN <- FV]} FVS) else FVS[ClassName', FN <- FV] fi . ) op addToAll : FieldNameList FlatFNL -> FlatFNL . op addToAll : FieldPairList FieldValues -> FieldValues . eq addToAll(FNL, emptyFlatFNL) = emptyFlatFNL . eq addToAll(FNL, [{ ClassName | FNL'}] ~ FFNL) = [{ClassName | FNL, FNL'}] ~ addToAll(FNL, FFNL) . eq addToAll(FPL, emptyFieldValues) = emptyFieldValues . eq addToAll(FPL, {ClassName, FPL'} FVS) = {ClassName, FPL FPL'} addToAll(FPL, FVS) . sort HeapAddress . subsort Int < HeapAddress . sort JavaObject . op JavaObject : -> JavaObject . subsort JavaObject < Cid . op Addr :_ : HeapAddress -> Attribute . op FieldValues :_ : FieldValues -> Attribute . op CName :_ : ClassName -> Attribute . ---op Lock :_ : Lock -> Attribute . ---class JavaObject | Addr : HeapAddress , FieldValues : FieldValues , CName : ClassName , Lock : Lock . op initFieldPairList : FieldNameList -> FieldPairList . var FieldName : FieldName . vars FNL FNL' : FieldNameList . eq initFieldPairList(emptyFieldNameList) = emptyFieldPairList . eq initFieldPairList(FN , FNL) = [[FN, 0]] initFieldPairList(FNL) . var FFNL : FlatFNL . op initFieldValues : FlatFNL -> FieldValues . eq initFieldValues(emptyFlatFNL) = emptyFieldValues . eq initFieldValues([{ClassName | FNL}] ~ FFNL) = {ClassName, initFieldPairList(FNL)} initFieldValues(FFNL) . endm mod CLASS-FLATTENER is protecting JAVA-OBJECTS . subsort Qid < Oid . op NoClass : -> ClassName . sort FieldAccumulator . op FieldAccumulator : -> FieldAccumulator . subsort FieldAccumulator < Cid . op StaticFields :_ : FlatFNL -> Attribute . op ClassName :_ : ClassName -> Attribute . sort StaticFieldAccumulator . op StaticFieldAccumulator : -> StaticFieldAccumulator . subsort StaticFieldAccumulator < Cid . sort FieldValueAccumulator . op FieldValueAccumulator : -> FieldValueAccumulator . subsort FieldValueAccumulator < Cid . ---class FieldAccumulator | SupClass : ClassName, Fields : FlatFNL, ClassName : ClassName . ---class StaticFieldAccumulator | SupClass : ClassName, Fields : FlatFNL, ClassName : ClassName . ---class FieldValueAccumulator | SupClass : ClassName, FieldValues : FieldValues, ClassName : ClassName . vars SFA FA : Oid . var FVA : Oid . vars CName ClName ClassName : ClassName . vars Fields SFields : FlatFNL . vars FNL SFNL : FieldNameList . var SFV : FieldPairList . var FV : FieldValues . var ConstantPool : ConstantPool . var L : Lock . var ML : MethodList . eq < ClassName : JavaClass | SupClass : CName, Fields : FNL , StaticFields : SFNL, StaticFieldValues : SFV , Lock : Lock(emptyOidList, NoThread, 0) , ATT > = < ClassName : JavaClass | SupClass : CName, Fields : FNL , StaticFields : SFNL, StaticFieldValues : SFV , Lock : Lock(emptyOidList, NoThread, 1) , ATT > < qid(string(ClassName) + char(83)) : StaticFieldAccumulator | SupClass : CName, Fields : [{ClassName | SFNL}], ClassName : ClassName > < qid(string(ClassName) + char(86)) : FieldValueAccumulator | SupClass : CName, FieldValues : {ClassName , SFV} , ClassName : ClassName > < qid(string(ClassName) + char(70)) : FieldAccumulator | SupClass : CName, Fields : [{ClassName | FNL}], ClassName : ClassName > . --- Flattening the instance fields eq < FA : FieldAccumulator | SupClass : ClassName , Fields : Fields , ClassName : ClName > < ClassName : JavaClass | SupClass : CName, Fields : FNL , ATT > = < FA : FieldAccumulator | SupClass : CName , Fields : (addToAll(FNL, Fields) ~ [{ClassName | FNL}]) , ClassName : ClName > < ClassName : JavaClass | SupClass : CName, Fields : FNL , ATT > . --- Flattening the static fields eq < FA : StaticFieldAccumulator | SupClass : ClassName , Fields : Fields , ClassName : ClName > < ClassName : JavaClass | SupClass : CName, StaticFields : FNL , ATT > = < FA : StaticFieldAccumulator | SupClass : CName , Fields : (addToAll(FNL, Fields) ~ [{ClassName | FNL}]) , ClassName : ClName > < ClassName : JavaClass | SupClass : CName, StaticFields : FNL , ATT > . --- Flattening the static field values eq < FVA : FieldValueAccumulator | SupClass : ClassName , FieldValues : FV , ClassName : ClName > < ClassName : JavaClass | SupClass : CName, StaticFieldValues : SFV , ATT > = < FVA : FieldValueAccumulator | SupClass : CName , FieldValues : (addToAll(SFV, FV) {ClassName, SFV}) , ClassName : ClName > < ClassName : JavaClass | SupClass : CName, StaticFieldValues : SFV , ATT > . ----eq < ClassName : JavaClass | Lock : Lock(emptyOidList, NoThread, 1) > = none . eq < FA : FieldAccumulator | SupClass : NoClass , Fields : Fields , ClassName : ClassName > < SFA : StaticFieldAccumulator | SupClass : NoClass , Fields : SFields , ClassName : ClassName > < FVA : FieldValueAccumulator | SupClass : NoClass , FieldValues : FV , ClassName : ClassName > < ClassName : JavaClass | SupClass : CName, Fields : FNL , StaticFields : SFNL, StaticFieldValues : SFV , Lock : Lock(emptyOidList, NoThread, 1) , Methods : ML, ConstPool : ConstantPool > = < ClassName : JavaClassV | StaticFieldValues : FV , Lock : Lock(emptyOidList, NoThread, 0), ConstPool : ConstantPool > < ClassName : JavaClassC | SupClass : CName, Fields : Fields , StaticFields : SFields, Methods : ML > < ClassName : JavaClass | SupClass : CName, Fields : FNL , StaticFields : SFNL, StaticFieldValues : SFV , Lock : Lock(emptyOidList, NoThread, -1) , Methods : ML, ConstPool : ConstantPool > . sort Other . op Other : -> Other . subsort Other < Cid . subsort JavaObject < Other . op constClass : Configuration -> Configuration [memo] . op varClass : Configuration -> Configuration [memo] . op other : Configuration -> Configuration [memo] . var ATT : AttributeSet . var Conf : Configuration . var O : Oid . var X : Other . eq constClass(none) = none . eq constClass(< ClassName : JavaClass | ATT > Conf ) = constClass(Conf) . eq constClass(< ClassName : JavaClassV | ATT > Conf ) = constClass(Conf) . eq constClass(< ClassName : JavaClassC | ATT > Conf ) = < ClassName : JavaClassC | ATT > constClass(Conf) . eq constClass(< O : X | ATT > Conf ) = constClass(Conf) . eq varClass(none) = none . eq varClass(< ClassName : JavaClass | ATT > Conf ) = varClass(Conf) . eq varClass(< ClassName : JavaClassC | ATT > Conf ) = varClass(Conf) . eq varClass(< ClassName : JavaClassV | ATT > Conf ) = < ClassName : JavaClassV | ATT > varClass(Conf) . eq varClass(< O : X | ATT > Conf ) = varClass(Conf) . eq other(none) = none . eq other(< ClassName : JavaClass | ATT > Conf ) = other(Conf) . eq other(< ClassName : JavaClassC | ATT > Conf ) = other(Conf) . eq other(< ClassName : JavaClassV | ATT > Conf ) = other(Conf) . eq other(< O : X | ATT > Conf ) = < O : X | ATT > other(Conf) . endm mod JAVA-ARRAYS is protecting CLASS-FLATTENER . sort IntList . subsort Int < IntList . op emptyIntList : -> IntList . op _@_ : IntList IntList -> IntList [assoc id: emptyIntList] . sorts Cell Cells . subsort Cell < Cells . sort ArrayIndex . subsort IntList < ArrayIndex . subsort Value < Cell . op emptyCells : -> Cells . op <_,_> : Int Cells -> Cell . op _$_ : Cells Cells -> Cells [assoc comm id: emptyCells] . op _[_] : Cells ArrayIndex -> Cells . op _[_<-_] : Cells ArrayIndex Value -> Cells . op value : Cells -> Value . op initCells : Int -> Cells . vars Cells C : Cells . var Cell : Cell . var AI : IntList . var I : Int . eq emptyCells[AI] = Null . eq Cells[emptyIntList] = Cells . eq (< I , C > $ Cells)[I] = C . ---eq Cells[I @ AI] = (Cells[I])[AI] . eq value(I) = I . eq value(C) = Null . eq initCells(0) = emptyCells . eq initCells(I) = initCells(I - 1) $ < I - 1 , 0 > . var V : Value . eq (< I , C > $ Cells)[I <- V] = < I , V > $ Cells . ---eq Cells[I @ AI <- V] = (Cells[I])[AI <- V] . sort JavaArray . op JavaArray : -> JavaArray . subsort JavaArray < Cid . op Length :_ : Int -> Attribute . op Type :_ : Type -> Attribute . op Cells :_ : Cells -> Attribute . subsort JavaArray < JavaObject . --- REMINDER : THE REWRITE RULES FOR JAVA OBJECTS TO COVER THE ARRAYS AS WELL . ---class JavaArray | Length : Int , Type : Type , Cells : Cells . ---subclass JavaArray < JavaObject . endm mod JAVA-THREADS is protecting JAVA-ARRAYS . sorts CallStack CallStackStat . ---subsort HeapAddress < ObjectRef . --- Might change (Oid or HeapAddr?) ---subsort ObjectRef < HeapAddress . sort Frame . subsort Frame < CallStack . --- *Frame = (PC, Program, local-variables, oprand-stack, sync-flag, current-class) sorts LocalVar LocalVars . --- * Incomplete subsort LocalVar < LocalVars . subsort Int < Value . op {{_,_}} : Int Value -> LocalVar . op emptyLocalVars : -> LocalVars . op _,_ : LocalVars LocalVars -> LocalVars [assoc comm id: emptyLocalVars] . op _[_] : LocalVars Int -> Value . op _[_<-_] : LocalVars Int Value -> LocalVars . vars V V' : Value . var LV : LocalVars . var K : Int . var X : Int . eq ({{K, V}} , LV)[K] = V . eq ({{K, V}} , LV)[K <- V'] = ({{K, V'}} , LV) . --- Make a list (of LocalVars form) of argmuments of a function which are on the operand-stack op popLocalVars : Int OperandStack -> LocalVars . op multipop : Int OperandStack -> OperandStack . op fillLocalVars : Int Int LocalVars -> LocalVars . op addLocalVars : LocalVars Int Int -> LocalVars . var OStackItem : Value . eq popLocalVars(0, OperandStack) = emptyLocalVars . eq popLocalVars(K, OStackItem # OperandStack) = {{K - 1, OStackItem}} , popLocalVars(K - 1 , OperandStack) . eq multipop(0, OperandStack) = OperandStack . eq multipop(K, OStackItem # OperandStack) = multipop(K - 1, OperandStack) . eq fillLocalVars(X, K, LV) = if X <= K then LV else addLocalVars(LV, K, X - K) fi . eq addLocalVars(LV, K, 0) = LV . eq addLocalVars(LV, K, X) = {{K , 0}} , addLocalVars(LV, K + 1, X - 1) . sorts OperandStack . ---subsort OStackItem < OperandStack . ---subsort Int < OStackItem . ---subsort Reference < OStackItem . subsort Reference < Value . --- Should it ? ---subsort OStackItem < Value . ---subsort Value < OStackItem . subsort Value < OperandStack . op REF_ : HeapAddress -> Reference . op int : Reference -> Int . eq int(REF K) = K . op emptyOperandStack : -> OperandStack . op _#_ : OperandStack OperandStack -> OperandStack [assoc id: emptyOperandStack] . op push : Value OperandStack -> OperandStack . op pop : OperandStack -> OperandStack . var E : Value . var OperandStack : OperandStack . eq push(E, OperandStack) = (E # OperandStack) . eq pop(E # OperandStack) = OperandStack . --- Possible Error ---sort LabeledPgm . sort SyncFlag . op LOCKED : -> SyncFlag . op SLOCKED : -> SyncFlag . op UNLOCKED : -> SyncFlag . op [_,_,_,_,_,_,_] : Int Instruction LabeledPgm LocalVars OperandStack SyncFlag ClassName -> Frame . op pc : Frame -> Int . op pgm : Frame -> LabeledPgm . op localVars : Frame -> LocalVars . op operandStack : Frame -> OperandStack . op syncFlag : Frame -> SyncFlag . op className : Frame -> ClassName . var PC : Int . var Pgm : LabeledPgm . var LocalVars : LocalVars . var SyncFlag : SyncFlag . var Inst : Instruction . var ClassName : ClassName . eq pc([PC, Inst, Pgm, LocalVars, OperandStack, SyncFlag, ClassName]) = PC . eq pgm([PC, Inst, Pgm, LocalVars, OperandStack, SyncFlag, ClassName]) = Pgm . eq localVars([PC, Inst, Pgm, LocalVars, OperandStack, SyncFlag, ClassName]) = LocalVars . eq operandStack([PC, Inst, Pgm, LocalVars, OperandStack, SyncFlag, ClassName]) = OperandStack . eq syncFlag([PC, Inst, Pgm, LocalVars, OperandStack, SyncFlag, ClassName]) = SyncFlag . eq className([PC, Inst, Pgm, LocalVars, OperandStack, SyncFlag, ClassName]) = ClassName . op emptyCallStack : -> CallStack . op __ : CallStack CallStack -> CallStack [assoc id: emptyCallStack] . op topFrame : CallStack -> Frame . var Frame : Frame . var CallStack : CallStack . eq topFrame(Frame CallStack) = Frame . --- CallStackStat op scheduled : -> CallStackStat . op waiting : -> CallStackStat . op waitOnObject : -> CallStackStat . op unscheduled : -> CallStackStat . sort JavaThread . op JavaThread : -> JavaThread . subsort JavaThread < Cid . op callStack :_ : CallStack -> Attribute [prec 0] . op Status :_ : CallStackStat -> Attribute . op ORef :_ : HeapAddress -> Attribute . subsort JavaThread < Other . ---class JavaThread | callStack : CallStack , Status : CallStackStat , ORef : HeapAddress . --- MethodInvocation -> Memory Management sort LabeledInstruction . subsort LabeledInstruction < LabeledPgm . op [_,_] : Int Instruction -> LabeledInstruction . op emptyLabeledPgm : -> LabeledPgm . op __ : LabeledPgm LabeledPgm -> LabeledPgm [assoc comm id: emptyLabeledPgm] . op LoadPgm : Pgm Int -> LabeledPgm . op _[_] : LabeledPgm Int -> Instruction . var LPgm : LabeledPgm . var P : Pgm . op noInstruction : -> Instruction . eq ([K, Inst] LPgm)[K] = Inst . eq LoadPgm(emptyPgm, K) = emptyLabeledPgm . eq LoadPgm((Inst P), K) = [K, Inst] LoadPgm(P, (K + size(Inst))) . endm mod POOL-MANAGER is protecting JAVA-THREADS . protecting STRING . op idg : Int -> String . op oidg : Int -> String . op tidg : Int -> String . var I : Int . eq idg(0) = "0" . eq idg(1) = "1" . eq idg(I) = if (I rem 2) == 0 then idg(I quo 2) + char(48) else idg(I quo 2) + char(49) fi . eq oidg(I) = char(79) + idg(I) . eq tidg(I) = char(84) + idg(I) . sort HeapManager . op HeapManager : -> HeapManager . subsort HeapManager < Cid . op FirstAvailable :_ : Int -> Attribute . subsort HeapManager < Other . ---class HeapManager | FirstAvailable : Int . sort ThreadManager . op ThreadManager : -> ThreadManager . subsort ThreadManager < Cid . op FirstAvailable :_ : Int -> Attribute . subsort ThreadManager < Other . ---class ThreadManager | FirstAvailable : Int . ---( sort FieldAccumulator . op FieldAccumulator : -> FieldAccumulator . subsort FieldAccumulator < Cid . ) op SuperClass :_ : ClassName -> Attribute . op Fields :_ : FieldValues -> Attribute . op Thread :_ : Oid -> Attribute . ---class FieldAccumulator | SuperClass : SuperClasses , Fields : FieldValues , Thread : Oid . sort Output . op Output : -> Output . subsort Output < Cid . op output :_ : IntList -> Attribute . subsort Output < Other . sort Input . op Input : -> Input . subsort Input < Cid . op input :_ : IntList -> Attribute . subsort Input < Other . ---class Input | input : IntList . ---class Output | output : IntList . endm mod BYTECODE-SEMANTICS is protecting POOL-MANAGER . ---protecting JAVA-ARRAYS . subsort Qid < Oid . vars PC PC' : Int . var LI : LabeledInstruction . var Pgm : LabeledPgm . var LocalVars : LocalVars . vars OperandStack OperandStack' : OperandStack . var SyncFlag : SyncFlag . vars ClassName C : ClassName . var CallStack : CallStack . var OR : HeapAddress . vars Cl T O : Oid . vars OS OS' : Value . vars I J : Int . var R : Reference . var HeapAddr : HeapAddress . var Inst : Instruction . var OIL : OidList . eq < T : JavaThread | callStack : ([PC, nop, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . eq < T : JavaThread | callStack : ([PC, iconst0, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(0 , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . eq < T : JavaThread | callStack : ([PC, iconst1, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(1 , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ICONST2] : eq < T : JavaThread | callStack : ([PC, iconst2, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(2 , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ICONST3] : eq < T : JavaThread | callStack : ([PC, iconst3, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(3 , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ICONST4] : eq < T : JavaThread | callStack : ([PC, iconst4, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(4 , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ICONST5] : eq < T : JavaThread | callStack : ([PC, iconst5, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(5 , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ICONSTM1] : eq < T : JavaThread | callStack : ([PC, iconstm1, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(-1 , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [BIPUSH] : eq < T : JavaThread | callStack : ([PC, bipush(I), Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(I , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . --- Integer Operations ---rl [POP] : eq < T : JavaThread | callStack : ([PC, pop, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, pop(OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [SWAP] : eq < T : JavaThread | callStack : ([PC, swap, Pgm, LocalVars, (OS # OS' # OperandStack) , SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (OS' # OS # OperandStack) , SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [DUP1] : eq < T : JavaThread | callStack : ([PC, dup, Pgm, LocalVars, I # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, I # I # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [DUP2] : eq < T : JavaThread | callStack : ([PC, dup, Pgm, LocalVars, REF(I) # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, REF(I) # REF(I) # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IADD] : eq < T : JavaThread | callStack : ([PC, iadd, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (I + J) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ISUB] : eq < T : JavaThread | callStack : ([PC, isub, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (J - I) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . eq < T : JavaThread | callStack : ([PC, imul, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (I * J) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IDIV] : eq < T : JavaThread | callStack : ([PC, idiv, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (J quo I) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IREM] : eq < T : JavaThread | callStack : ([PC, irem, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (J rem I) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [INEG] : eq < T : JavaThread | callStack : ([PC, ineg, Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (- I) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IAND] : eq < T : JavaThread | callStack : ([PC, iand, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (I & J) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IOR] : eq < T : JavaThread | callStack : ([PC, ior, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (I | J) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IXOR] : eq < T : JavaThread | callStack : ([PC, ixor, Pgm, LocalVars, (I # J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, ( (I xor J) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . --- Stack and Local Variables ---rl [ILOAD] : eq < T : JavaThread | callStack : ([PC, iload(I), Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(LocalVars[I] , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ILOAD0] : eq < T : JavaThread | callStack : ([PC, iload0, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(LocalVars[0] , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ILOAD1] : eq < T : JavaThread | callStack : ([PC, iload1, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(LocalVars[1] , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ILOAD2] : eq < T : JavaThread | callStack : ([PC, iload2, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(LocalVars[2] , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ILOAD3] : eq < T : JavaThread | callStack : ([PC, iload3, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(LocalVars[3] , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ALOAD] : eq < T : JavaThread | callStack : ([PC, aload(I), Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(REF(int(LocalVars[I])) , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ALOAD0] : eq < T : JavaThread | callStack : ([PC, aload0, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(REF(int(LocalVars[0])) , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ALOAD1] : eq < T : JavaThread | callStack : ([PC, aload1, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(REF(int(LocalVars[1])) , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ALOAD2] : eq < T : JavaThread | callStack : ([PC, aload2, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(REF(int(LocalVars[2])) , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ALOAD3] : eq < T : JavaThread | callStack : ([PC, aload3, Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, push(REF(int(LocalVars[3])) , OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ISTORE] : eq < T : JavaThread | callStack : ([PC, istore(I), Pgm, LocalVars, (J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[I <- J] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ISTORE0] : eq < T : JavaThread | callStack : ([PC, istore0, Pgm, LocalVars, (J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[0 <- J] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ISTORE1] : eq < T : JavaThread | callStack : ([PC, istore1, Pgm, LocalVars, (J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[1 <- J] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ISTORE2] : eq < T : JavaThread | callStack : ([PC, istore2, Pgm, LocalVars, (J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[2 <- J] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ISTORE3] : eq < T : JavaThread | callStack : ([PC, istore3, Pgm, LocalVars, (J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[3 <- J] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ASTORE] : eq < T : JavaThread | callStack : ([PC, astore(I), Pgm, LocalVars, (R # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[I <- R] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ASTORE0] : eq < T : JavaThread | callStack : ([PC, astore0, Pgm, LocalVars, (R # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[0 <- R] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ASTORE1] : eq < T : JavaThread | callStack : ([PC, astore1, Pgm, LocalVars, (R # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[1 <- R] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ASTORE2] : eq < T : JavaThread | callStack : ([PC, astore2, Pgm, LocalVars, (R # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[2 <- R] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [ASTORE3] : eq < T : JavaThread | callStack : ([PC, astore3, Pgm, LocalVars, (R # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars[3 <- R] , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . vars SFNL FNL SFNL' FNL' : FlatFNL . vars ConstantPool CP CP' : ConstantPool . ---vars SuperClasses SC : SuperClasses . vars MethodList ML ML' : MethodList . var OT : Oid . vars SFV SFV' : FieldValues . vars FV FV' : FieldValues . var HM : Oid . var K : Int . --- Branches ---rl [GOTO] : eq < T : JavaThread | callStack : ([PC, goto(I), Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([I , Pgm[I], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFEQ] : eq < T : JavaThread | callStack : ([PC, ifeq(J), Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I == 0 then J else (PC + size(Pgm[PC])) fi, Pgm[if I == 0 then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFNE] : eq < T : JavaThread | callStack : ([PC, ifne(J), Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I =/= 0 then J else (PC + size(Pgm[PC])) fi, Pgm[if I =/= 0 then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFlT] : eq < T : JavaThread | callStack : ([PC, iflt(J), Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I < 0 then J else (PC + size(Pgm[PC])) fi, Pgm[if I < 0 then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFLE] : eq < T : JavaThread | callStack : ([PC, ifle(J), Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I <= 0 then J else (PC + size(Pgm[PC])) fi, Pgm[if I <= 0 then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFGT] : eq < T : JavaThread | callStack : ([PC, ifgt(J), Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I > 0 then J else (PC + size(Pgm[PC])) fi, Pgm[if I > 0 then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFGE] : eq < T : JavaThread | callStack : ([PC, ifge(J), Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I >= 0 then J else (PC + size(Pgm[PC])) fi, Pgm[if I >= 0 then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFICMPEQ] : eq < T : JavaThread | callStack : ([PC, ificmpeq(J), Pgm, LocalVars, (K # I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I == K then J else (PC + size(Pgm[PC])) fi, Pgm[if I == K then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFICMPNE] : eq < T : JavaThread | callStack : ([PC, ificmpne(J), Pgm, LocalVars, (K # I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I =/= K then J else (PC + size(Pgm[PC])) fi, Pgm[if I =/= K then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFICMPLT] : eq < T : JavaThread | callStack : ([PC, ificmplt(J), Pgm, LocalVars, (K # I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I < K then J else (PC + size(Pgm[PC])) fi, Pgm[if I < K then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFICMPLE] : eq < T : JavaThread | callStack : ([PC, ificmple(J), Pgm, LocalVars, (K # I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I <= K then J else (PC + size(Pgm[PC])) fi, Pgm[if I <= K then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFICMPGT] : eq < T : JavaThread | callStack : ([PC, ificmpgt(J), Pgm, LocalVars, (K # I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I > K then J else (PC + size(Pgm[PC])) fi, Pgm[if I > K then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [IFICMPGE] : eq < T : JavaThread | callStack : ([PC, ificmpge(J), Pgm, LocalVars, (K # I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : ([if I >= K then J else (PC + size(Pgm[PC])) fi, Pgm[if I >= K then J else (PC + size(Pgm[PC])) fi], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---( msg SetField_ofObject_ofClass_to_forThread_ : FieldName HeapAddress ClassName Value Oid -> Msg . --- a message to set the value of some instant field msg GetField_ofObject_ofClass_forThread_ : FieldName HeapAddress ClassName Oid -> Msg . --- asking for value of some instant field msg ValueofField_ofObject_forThread_is_ : FieldName HeapAddress Oid Value -> Msg . --- sending the value of some instant field to the requesting thread msg FieldValueSetforThread_ : Oid -> Msg . ) var Value : Value . var V : Value . var FieldName : FieldName . vars CName ClName : ClassName . vars L L' : Lock . var FM : Oid . rl [PUTFIELD1] : < T : JavaThread | callStack : ([PC, putfield(I), Pgm, LocalVars , (V # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {CName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : L' > => < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {CName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < O : JavaObject | Addr : K , FieldValues : (FV[CName, FieldName <- V]) , CName : ClName , Lock : L' > . ---( (SetField FieldName ofObject K ofClass ClName to V forThread T) . rl [PUTFIELD2] : < O : JavaObject | Addr : K , FieldValues : FV , CName : ClassName , Lock : L > (SetField FieldName ofObject K ofClass ClName to Value forThread T) => < O : JavaObject | Addr : K , FieldValues : FV[ClName , FieldName <- Value] , CName : ClassName , Lock : L > (FieldValueSetforThread T) . ---rl [PUTFIELD3] : eq < T : JavaThread | callStack : [PC, putfield(I), Pgm, LocalVars , (V # REF(K) # OperandStack), SyncFlag, ClassName] CallStack , Status : waiting , ORef : OR > (FieldValueSetforThread T) = < T : JavaThread | callStack : [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack , Status : scheduled , ORef : OR > . ) rl [GETFIELD1] : < T : JavaThread | callStack : ([PC, getfield(I), Pgm, LocalVars , REF(K) # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < O : JavaObject | Addr : K , FieldValues : FV , CName : CName , Lock : L' > => < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , (FV[ClName, FieldName]) # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < O : JavaObject | Addr : K , FieldValues : FV , CName : CName , Lock : L' > . ---( (GetField FieldName ofObject K ofClass ClName forThread T) . rl [GETFIELD2] : < O : JavaObject | Addr : K , FieldValues : FV , CName : ClassName , Lock : L > (GetField FieldName ofObject K ofClass ClassName forThread T) => < O : JavaObject | Addr : K , FieldValues : FV , CName : ClassName , Lock : L > (ValueofField FieldName ofObject K forThread T is FV[ClassName, FieldName]) . ---rl [GETFIELD3] : eq < T : JavaThread | callStack : [PC, getfield(I), Pgm, LocalVars , (REF(K) # OperandStack), SyncFlag, ClassName] CallStack , Status : waiting , ORef : OR > (ValueofField FieldName ofObject K forThread T is V) = < T : JavaThread | callStack : [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , (V # OperandStack), SyncFlag, ClassName] CallStack , Status : scheduled , ORef : OR > . ) op SetStaticField_ofClass_to_forThread_ : FieldName ClassName Value Oid -> Msg . --- a message to set the value of some instant field op GetStaticField_ofClass_forThread_ : FieldName ClassName Oid -> Msg . --- asking for value of some instant field op ValueofStaticField_ofClass_forThread_is_ : FieldName ClassName Oid Value -> Msg . --- sending the value of some instant field to the requesting thread op StaticValueSetforThread_ : Oid -> Msg . rl [PUTSTATIC0] : < T : JavaThread | callStack : ([PC, putstatic(I), Pgm, LocalVars , (V # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > => < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : (SFV'[ClName, FieldName <- V]) , Lock : L' > . rl [PUTSTATIC1] : < T : JavaThread | callStack : ([PC, putstatic(I), Pgm, LocalVars , (V # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClassName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > => < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClassName, FieldName}] ConstantPool) , StaticFieldValues : (SFV[ClassName, FieldName <- V]) , Lock : L > . ---( rl [PUTSTATIC2] : < C : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > (SetStaticField FieldName ofClass C to Value forThread T) => < C : JavaClassV | ConstPool : CP , StaticFieldValues : (SFV'[FieldName <- Value]) , Lock : L' > (StaticValueSetforThread T) . ---rl [PUTSTATIC3] : eq (StaticValueSetforThread T) < T : JavaThread | callStack : ([PC, putstatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ) rl [GETSTATIC0] : < T : JavaThread | callStack : ([PC, getstatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > => < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , ((SFV'[ClName, FieldName]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > . rl [GETSTATIC1] : < T : JavaThread | callStack : ([PC, getstatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClassName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > => < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , ((SFV[ClassName, FieldName]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {ClassName, FieldName}] ConstantPool) , StaticFieldValues : SFV , Lock : L > . ---( rl [GETSTATIC2] : < Cl : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > (GetStaticField FieldName ofClass Cl forThread T) => < Cl : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > (ValueofStaticField FieldName ofClass Cl forThread T is SFV'[FieldName]) . ---rl [GETSTATIC3] : eq < T : JavaThread | callStack : ([PC, getstatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > (ValueofStaticField FieldName ofClass C forThread T is Value) = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , (Value # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ) ---( ---rl [NEW0] : eq < T : JavaThread | callStack : ([PC, new(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I , ClassName] ConstantPool) , StaticFieldValues : SFV , Lock : L > < HM : HeapManager | FirstAvailable : K > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , push(REF(K), OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < HM : HeapManager | FirstAvailable : (K + 1) > < ClassName : JavaClassV | ConstPool : ([I , ClassName] ConstantPool) , StaticFieldValues : SFV , Lock : L > < qid(idg(K)) : JavaObject | Addr : K , FieldValues : initFieldValues(fields(ClassName, ConstantClasses)) , CName : (ConstantPool[I]) , Lock : Lock(emptyOidList, NoThread, 0) > . ) ---rl [NEW1] : eq < T : JavaThread | callStack : ([PC, new(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I , ClName] ConstantPool) , StaticFieldValues : SFV , Lock : L > < HM : HeapManager | FirstAvailable : K > = < T : JavaThread | callStack : ([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , push(REF(K), OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I , ClName] ConstantPool) , StaticFieldValues : SFV , Lock : L > < qid(idg(K)) : JavaObject | Addr : K , FieldValues : initFieldValues(fields(ClName, ConstantClasses)) , CName : ClName , Lock : Lock(emptyOidList, NoThread, 0) > < HM : HeapManager | FirstAvailable : (K + 1) > . --------- INVOCATIONS var MethodName : MethodName . var MethodFormals MethodFormals' : MethodFormals . var MethodSync : MethodSync . vars MPgm MPgm' : LabeledPgm . var LV : LocalVars . var SF : SyncFlag . var CSK : CallStack . vars X X' Y : Int . var TM : Oid . var LL : Lock . --------- SPECIAL INVOCATIONS ----- Thread Start Method eq < T : JavaThread | callStack : ([PC, start, Pgm, {{0, REF K}}, (OperandStack), SyncFlag, ClName] CallStack) , Status : scheduled , ORef : OR > < TM : ThreadManager | FirstAvailable : Y > = < qid(tidg(Y)) : JavaThread | callStack : ([0, ((methodBody(ClName, 'run$1$2, ConstantClasses))[0]), (methodBody(ClName, 'run$1$2, ConstantClasses)), fillLocalVars((numMethodLocals(ClName, 'run$1$2, ConstantClasses)), 1 , {{0, REF K}}), emptyOperandStack, UNLOCKED, ClName]) , Status : scheduled , ORef : K > < TM : ThreadManager | FirstAvailable : (Y + 1) > < T : JavaThread | callStack : ([PC + size(start), Pgm[PC + size(start)], Pgm , {{0, REF K}}, OperandStack, SyncFlag, ClName] CallStack) , Status : scheduled , ORef : OR > . ----------------------------------------------------------------------------------------------------------------- ---------------------------------------- GENERAL INVOCATIONS --------------------------------------------------- ----------------------------------------------------------------------------------------------------------------- op GetMethod_ofClass_ArgSize_forThread_OriginalClass_ : MethodName ClassName Int Oid ClassName -> Msg [message] . op Method_ofClass_ArgSize_Locals_forThread_is_ : MethodName ClassName Int Int Oid LabeledPgm -> Msg [message] . ---crl [INVOKEVIRTUAL1] : ceq < T : JavaThread | callStack : ([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, CName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : LL > = < T : JavaThread | callStack : ([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : LL > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, CName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > (GetMethod MethodName ofClass ClName ArgSize J forThread T OriginalClass ClName) if K == int((popLocalVars(J + 1, OperandStack))[0]) . ---rl [GETMETHOD1] : eq (GetMethod MethodName ofClass ClName ArgSize J forThread T OriginalClass ClassName) = if methodSyncFlag(ClName, MethodName, ConstantClasses) == false then (Method MethodName ofClass ClassName ArgSize J Locals numMethodLocals(ClName, MethodName, ConstantClasses) forThread T is methodBody(ClName, MethodName, ConstantClasses) ) else (SynchronizedMethod MethodName ofClass ClName ArgSize J Locals numMethodLocals(ClName, MethodName, ConstantClasses) forThread T is methodBody(ClName, MethodName, ConstantClasses) ) fi . ---( should be changed after flattening ---crl [GETMETHOD2] : ceq (GetMethod MethodName ofClass ClName ArgSize J forThread T OriginalClass CName) < ClName : JavaClassV | SupClasses : (SC ; ClassName) , StaticFields : SFNL' , Fields : FNL' , ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > = < ClName : JavaClassV | SupClasses : (SC ; ClassName) , StaticFields : SFNL' , Fields : FNL' , ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > (GetMethod MethodName ofClass ClassName ArgSize J forThread T OriginalClass CName) if not(ML[MethodName]) . ) ---rl [INVOKEVIRTUAL10] : eq < T : JavaThread | callStack : ([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > (Method MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) = < T : JavaThread | callStack : ([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, UNLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---c[rl [INVOKEVIRTUAL2] : ceq < T : JavaThread | callStack : ([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, CName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClassName , Lock : L' > = < T : JavaThread | callStack : ([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClassName , Lock : L' > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, CName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > (GetMethod MethodName ofClass ClassName ArgSize J forThread T OriginalClass ClassName) if K == int((popLocalVars(J + 1, OperandStack))[0]) . ---rl [INVOKEVIRTUAL20] : eq < T : JavaThread | callStack :([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > (Method MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) = < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, UNLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [INVOKESPECIAL1] : eq < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > = < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > (GetMethod MethodName ofClass ClName ArgSize J forThread T OriginalClass ClName) . ---rl [INVOKESPECIAL10] : eq < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > (Method MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) = < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, UNLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [INVOKESPECIAL2] : eq < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClassName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > = < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClassName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > (GetMethod MethodName ofClass ClassName ArgSize J forThread T OriginalClass ClassName) . ---rl [INVOKESPECIAL20] : eq < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > (Method MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) = < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, UNLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [INVOKESTATIC1] : eq < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > = < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > < ClName : JavaClassV | ConstPool : CP , StaticFieldValues : SFV' , Lock : L' > (GetMethod MethodName ofClass ClName ArgSize J forThread T OriginalClass ClName) . ---rl [INVOKESTATIC10] : eq < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > (Method MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) = < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J, popLocalVars(J, OperandStack)), emptyOperandStack, UNLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ---rl [INVOKESTATIC2] : eq < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClassName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > = < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < ClassName : JavaClassV | ConstPool : ([I, {J, MethodName, ClassName]] ConstantPool) , StaticFieldValues : SFV , Lock : L > (GetMethod MethodName ofClass ClassName ArgSize J forThread T OriginalClass ClassName) . ---rl [INVOKESTATIC20] : eq < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > (Method MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) = < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J, popLocalVars(J, OperandStack)), emptyOperandStack, UNLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . ----------------------------------------------------------------------------------------------------------------- ---------------------------------------- SYNCHRONIZATION SUPPORT ---------------------------------------------- ----------------------------------------------------------------------------------------------------------------- var NI : NzInt . op SynchronizedMethod_ofClass_ArgSize_Locals_forThread_is_ : MethodName ClassName Int Int Oid LabeledPgm -> Msg [message] . ---( ---rl [GETSYNCMETHOD] : eq (GetMethod MethodName ofClass ClName ArgSize J forThread T OriginalClass CName) < ClName : JavaClassV | ConstPool : CP , Methods : ({MethodName, MethodFormals, true, MPgm, X} , ML) , StaticFieldValues : SFV' , Lock : L' > = < ClName : JavaClassV | ConstPool : CP , Methods : ({MethodName, MethodFormals, true, MPgm, X} , ML) , StaticFieldValues : SFV' , Lock : L' > (SynchronizedMethod MethodName ofClass CName ArgSize J Locals X forThread T is MPgm ) . ) crl [INVOKEVIRTUAL3] : < T : JavaThread | callStack :([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > (SynchronizedMethod MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) => < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, LOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > if K == int((popLocalVars(J + 1, OperandStack))[0]) . crl [INVOKEVIRTUAL4] : < T : JavaThread | callStack :([PC, invokevirtual(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > (SynchronizedMethod MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) => < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, UNLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI + 1) > if K == int((popLocalVars(J + 1, OperandStack))[0]) . crl [INVOKESPECIAL3] : < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > (SynchronizedMethod MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) => < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, LOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > if K == int((popLocalVars(J + 1, OperandStack))[0]) . crl [INVOKESPECIAL4] : < T : JavaThread | callStack :([PC, invokespecial(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : waiting , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > (SynchronizedMethod MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) => < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J + 1, popLocalVars(J + 1, OperandStack)), emptyOperandStack, LOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J + 1,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI + 1) > if K == int((popLocalVars(J + 1, OperandStack))[0]) . rl [INVOKESTATIC4] : < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, NoThread, 0) > (SynchronizedMethod MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) => < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J, popLocalVars(J, OperandStack)), emptyOperandStack, SLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, 1) > . rl [INVOKESTATIC5] : < T : JavaThread | callStack :([PC, invokestatic(I), Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, NI) > (SynchronizedMethod MethodName ofClass ClName ArgSize J Locals X forThread T is MPgm ) => < T : JavaThread | callStack :([0, MPgm[0], MPgm, fillLocalVars(X, J, popLocalVars(J, OperandStack)), emptyOperandStack, SLOCKED, ClName] [PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , multipop(J,OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, NI + 1) > . -------------------- ---rl [IRETURN] : eq < T : JavaThread | callStack :([PC, ireturn, Pgm, LocalVars , (I # OperandStack), UNLOCKED, ClassName] [PC', Inst, MPgm, LV, OperandStack', SF, ClName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack :([PC', Inst, MPgm, LV, I # OperandStack', SF, ClName] CallStack) , Status : scheduled , ORef : OR > . ---rl [RETURN] : eq < T : JavaThread | callStack :([PC, return, Pgm, LocalVars , OperandStack, UNLOCKED, ClassName] CallStack) , Status : scheduled , ORef : OR > = < T : JavaThread | callStack : CallStack , Status : scheduled , ORef : OR > . ---( crl [IRETURNL1] : < T : JavaThread | callStack :([PC, ireturn, Pgm, LocalVars , (I # OperandStack), LOCKED, ClassName] [PC', Inst, MPgm, LV, OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > => < T : JavaThread | callStack :([PC', Inst, MPgm, LV, I # OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > if int(LocalVars[0]) == K . ) ---rl [IRETURNL1] : eq < T : JavaThread | callStack :([PC, ireturn, Pgm, ({{0, REF K}}, LocalVars) , I # OperandStack, LOCKED, ClassName] [PC', Inst, MPgm, LV, OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > = < T : JavaThread | callStack :([PC', Inst, MPgm, LV, I # OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > . ---( crl [IRETURNL2] : < T : JavaThread | callStack :([PC, ireturn, Pgm, LocalVars , (I # OperandStack), LOCKED, ClassName] [PC', Inst, MPgm, LV, OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI + 1) > => < T : JavaThread | callStack :([PC', Inst, MPgm, LV, I # OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > if int(LocalVars[0]) == K . ) ---rl [IRETURNL2] : eq < T : JavaThread | callStack :([PC, ireturn, Pgm, ({{0, REF K}}, LocalVars) , I # OperandStack, LOCKED, ClassName] [PC', Inst, MPgm, LV, OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI + 1) > = < T : JavaThread | callStack :([PC', Inst, MPgm, LV, I # OperandStack', SF, CName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > . ---( crl [RETURNL1] : < T : JavaThread | callStack :([PC, return, Pgm, LocalVars , OperandStack, LOCKED, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > => < T : JavaThread | callStack : CallStack , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > if int(LocalVars[0]) == K . ) ---rl [RETURNL1] : eq < T : JavaThread | callStack :([PC, return, Pgm, ({{0, REF K}}, LocalVars) , OperandStack, LOCKED, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > = < T : JavaThread | callStack : CallStack , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > . ---( crl [RETURNL2] : < T : JavaThread | callStack :([PC, return, Pgm, LocalVars , OperandStack, LOCKED, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI + 1) > => < T : JavaThread | callStack : CallStack , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > if int(LocalVars[0]) == K . ) ---rl [RETURNL2] : eq < T : JavaThread | callStack :([PC, return, Pgm, ({{0, REF K}}, LocalVars) , OperandStack, LOCKED, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI + 1) > = < T : JavaThread | callStack : CallStack , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > . ---rl [IRETURNS1] : eq < T : JavaThread | callStack :([PC, ireturn, Pgm, LocalVars , (I # OperandStack), SLOCKED, ClassName] [PC', Inst, MPgm, LV, OperandStack', SF, ClName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, 1) > = < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, NoThread, 0) > < T : JavaThread | callStack :([PC', Inst, MPgm, LV, I # OperandStack', SF, ClName] CallStack) , Status : scheduled , ORef : OR > . ----rl [IRETURNS2] : eq < T : JavaThread | callStack :([PC, ireturn, Pgm, LocalVars , (I # OperandStack), SLOCKED, ClassName] [PC', Inst, MPgm, LV, OperandStack', SF, ClName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, NI + 1) > = < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, NI) > < T : JavaThread | callStack :([PC', Inst, MPgm, LV, I # OperandStack', SF, ClName] CallStack) , Status : scheduled , ORef : OR > . ---rl [RETURNS1] : eq < T : JavaThread | callStack :([PC, return, Pgm, LocalVars , OperandStack, SLOCKED, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, 1) > = < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, NoThread, 0) > < T : JavaThread | callStack : CallStack , Status : scheduled , ORef : OR > . ---rl [RETURNS2] : eq < T : JavaThread | callStack :([PC, return, Pgm, LocalVars , OperandStack, SLOCKED, ClassName] CallStack) , Status : scheduled , ORef : OR > < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, NI + 1) > = < ClassName : JavaClassV | ConstPool : ConstantPool , StaticFieldValues : SFV , Lock : Lock(OIL, T, NI) > < T : JavaThread | callStack : CallStack , Status : scheduled , ORef : OR > . ---rl[ENDING] : eq < T : JavaThread | callStack : emptyCallStack , Status : scheduled , ORef : OR > = none . --- SYNCHRONIZATION SUPPORT rl [MONITORENTER1] : < T : JavaThread | callStack :([PC, monitorenter, Pgm, LocalVars , (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > . rl [MONITORENTER2] : < T : JavaThread | callStack :([PC, monitorenter, Pgm, LocalVars , (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, I) > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, I + 1) > . ---rl [MONITOREXIT1] : eq < T : JavaThread | callStack :([PC, monitorexit, Pgm, LocalVars , (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, 1) > = < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > . ---rl [MONITOREXIT2] : eq < T : JavaThread | callStack :([PC, monitorexit, Pgm, LocalVars , (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI + 1) > = < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars , OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > . --- EXCEPTIONS ---rl [ATHROW] : eq < T : JavaThread | callStack :([PC, athrow, Pgm, LocalVars , (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > = none . ----------------------------------------------------------------------------------------------------------------- ---------------------------------------- ARRAY OPERATIONS ---------------------------------------------------- ----------------------------------------------------------------------------------------------------------------- var A : Oid . var Cells : Cells . var aType : Type . var AI : ArrayIndex . rl [ARRAYLENGTH] : < T : JavaThread | callStack :([PC, arraylength, Pgm, LocalVars, REF(K) # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : aType , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, I # OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : aType , Cells : Cells > . rl [BALOAD] : < T : JavaThread | callStack :([PC, baload, Pgm, LocalVars, (J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : byte , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (value(Cells[J]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : byte , Cells : Cells > . rl [SALOAD] : < T : JavaThread | callStack :([PC, saload, Pgm, LocalVars, (J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : short , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (value(Cells[J]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : short , Cells : Cells > . rl [IALOAD] : < T : JavaThread | callStack :([PC, iaload, Pgm, LocalVars, (J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : int , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (value(Cells[J]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : int , Cells : Cells > . rl [FALOAD] : < T : JavaThread | callStack :([PC, faload, Pgm, LocalVars, (J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : float , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (value(Cells[J]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : float , Cells : Cells > . rl [DALOAD] : < T : JavaThread | callStack :([PC, daload, Pgm, LocalVars, (J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : double , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (value(Cells[J]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : double , Cells : Cells > . rl [LALOAD] : < T : JavaThread | callStack :([PC, baload, Pgm, LocalVars, (J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : long , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (value(Cells[J]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : long , Cells : Cells > . rl [CALOAD] : < T : JavaThread | callStack :([PC, caload, Pgm, LocalVars, (J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : char , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (value(Cells[J]) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : char , Cells : Cells > . rl [BASTORE] : < T : JavaThread | callStack :([PC, bastore, Pgm, LocalVars, (Value # J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : byte , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : byte , Cells : (Cells[J <- Value]) > . rl [CASTORE] : < T : JavaThread | callStack :([PC, castore, Pgm, LocalVars, (Value # J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : char , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : char , Cells : (Cells[J <- Value]) > . rl [SASTORE] : < T : JavaThread | callStack :([PC, sastore, Pgm, LocalVars, (Value # J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : short , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : short , Cells : (Cells[J <- Value]) > . rl [IASTORE] : < T : JavaThread | callStack :([PC, iastore, Pgm, LocalVars, (Value # J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : int , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : int , Cells : (Cells[J <- Value]) > . rl [LASTORE] : < T : JavaThread | callStack :([PC, lastore, Pgm, LocalVars, (Value # J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : long , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : long , Cells : (Cells[J <- Value]) > . rl [FASTORE] : < T : JavaThread | callStack :([PC, fastore, Pgm, LocalVars, (Value # J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : float , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : float , Cells : (Cells[J <- Value]) > . rl [DASTORE] : < T : JavaThread | callStack :([PC, dastore, Pgm, LocalVars, (Value # J # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : double , Cells : Cells > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < A : JavaArray | Addr : K , FieldValues : FV , CName : 'array , Lock : L , Length : I , Type : double , Cells : (Cells[J <- Value]) > . var Type : Type . rl [NEWARRAY] : < T : JavaThread | callStack :([PC, newarray(Type), Pgm, LocalVars, (I # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < HM : HeapManager | FirstAvailable : K > => < T : JavaThread | callStack :([PC + size(Pgm[PC]), Pgm[PC + size(Pgm[PC])], Pgm, LocalVars, (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < qid(idg(K)) : JavaArray | Addr : K , FieldValues : emptyFieldValues , CName : 'array , Lock : Lock(emptyOidList, NoThread, 0) , Length : I , Type : Type , Cells : initCells(I) > < HM : HeapManager | FirstAvailable : (K + 1) > . ---( class JavaArray | Length : Int , Type : Type , Cells : Cells . --- ARRAY OPCODES --- ANEWARRAY : pops length, allocates new array of object class indicated by index, pushes objectref of new array. op anewarray : Int -> Instruction . --- MULTIANEWARRAY : pops dimension number of array lenghts, .... multianewarray : Int Int -> Instruction. --- AALOAD : pops index and arrayref of an array of objectrefs, pushes arrayref[index]. op aaload : -> Instruction . --- AASTORE : pops index and arrayref of an array of objectrefs, assigns arrayref[index] = value. op aastore : -> Instruction . ) ---- INPUT OUTPUT MANAGEMENT vars IL IL' : IntList . ---rl [PRINT] : eq < T : JavaThread | callStack :([PC, print, Pgm, LocalVars, (J # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : Output | output : IL > = < O : Output | output : (IL @ J) > < T : JavaThread | callStack :([PC + size(print), Pgm[PC + size(print)], Pgm , LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . rl [WAIT] : < T : JavaThread | callStack :([PC, wait, Pgm, LocalVars, (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > => < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock( T || OIL, NoThread, 0) > < T : JavaThread | callStack :([PC + size(wait), Pgm[PC + size(wait)], Pgm , LocalVars, (NI # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : waitOnObject , ORef : OR > . op NotifyThreads_ : OidList -> Msg [message] . ---rl [NOTIFYALL] : eq < T : JavaThread | callStack :([PC, notifyAll, Pgm, LocalVars, (REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > = < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(emptyOidList, T, NI) > < T : JavaThread | callStack :([PC + size(notifyAll), Pgm[PC + size(notifyAll)], Pgm , LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > (NotifyThreads OIL) . rl [NOTIFYALL1] : < T : JavaThread | callStack :([PC, wakeup, Pgm, LocalVars, (NI # REF(K) # OperandStack), SyncFlag, ClassName] CallStack) , Status : waitOnObject , ORef : OR > ( NotifyThreads (T || OIL) ) < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, NoThread, 0) > => < T : JavaThread | callStack :([PC + size(wakeup), Pgm[PC + size(wakeup)], Pgm , LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : JavaObject | Addr : K , FieldValues : FV , CName : ClName , Lock : Lock(OIL, T, NI) > ( NotifyThreads OIL ) . eq (NotifyThreads emptyOidList) = none . rl [READ] : < T : JavaThread | callStack :([PC, read , Pgm, LocalVars, OperandStack, SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > < O : Input | input : (J @ IL) > => < O : Input | input : IL > < T : JavaThread | callStack :([PC + size(print), Pgm[PC + size(print)], Pgm , LocalVars, (J # OperandStack) , SyncFlag, ClassName] CallStack) , Status : scheduled , ORef : OR > . including MODEL-CHECKER . including LTL-SIMPLIFIER . ---protecting BYTECODE-SEMANTICS . ---including SATISFACTION . subsort Configuration < State . var Conf : Configuration . var SV : FieldPairList . op F : -> Formula . op check : Oid -> Prop . op Check : Oid Int -> Prop . op TG : Int -> Prop . op contains : Int IntList -> Bool . op Contains : IntList IntList -> Bool . op makeList : Int -> IntList . op ModelCheck : State Formula -> Bool . sort TransListPair . sort RuleNameList . sort RuleNameListPair . subsort RuleName < RuleNameList . subsort Bool < TransListPair . subsort Bool < RuleNameListPair . op emptyRuleNameList : -> RuleNameList . op _!_ : RuleNameList RuleNameList -> RuleNameList [assoc id: emptyRuleNameList] . op `{`[_`,_`]`} : TransitionList TransitionList -> TransListPair . op `{`[_`,_`]`} : RuleNameList RuleNameList -> RuleNameListPair . op transList : ModelCheckResult -> RuleNameListPair . op getRuleName : Transition -> RuleName . op getRuleNameListPair : TransListPair -> RuleNameListPair . op convert : TransitionList -> RuleNameList . op prettyprint : ModelCheckResult -> RuleNameListPair . vars TL1 TL2 : TransitionList . var RN : RuleName . var TR : Transition . var MCR : ModelCheckResult . op thread1 : Configuration -> Int . op thread2 : Configuration -> Int . var CSS : CallStackStat . eq transList(true) = true . eq transList(false) = false . eq transList(counterexample(TL1, TL2)) = getRuleNameListPair( {[ TL1 , TL2 ]} ) . eq getRuleName({S, RN}) = RN . eq convert(nil) = emptyRuleNameList . eq convert(TR TL1) = getRuleName(TR) ! convert(TL1) . eq getRuleNameListPair(true) = true . eq getRuleNameListPair(false) = false . eq getRuleNameListPair({[ TL1 , TL2 ]}) = {[convert(TL1) , convert(TL2)]} . eq prettyprint(MCR) = transList(MCR) . var f : Formula . var S : State . ---var O : Oid . ---vars I J : Int . ---vars IL IL' : IntList . ---eq S = (< 'o : Output | output : 3 >) . ---eq F = [] True . eq ModelCheck(S, f) = if modelCheck(S, f) == true then true else false fi . eq contains(I , emptyIntList) = false . eq contains(I, J @ IL) = if I == J then true else contains(I , IL) fi . eq Contains(emptyIntList, IL') = true . eq Contains(IL, emptyIntList) = false . eq Contains(I @ IL, IL') = ( contains(I, IL') and Contains(IL, IL') ) . eq makeList(0) = emptyIntList . eq makeList(I) = makeList(I - 1) @ I . eq < O : Output | output : emptyIntList > Conf |= check(O) = false . eq < O : Output | output : (I @ IL) > Conf |= check(O) = true . eq < O : Output | output : IL > Conf |= Check(O, I) = Contains(makeList(I), IL) . eq < 'Process : JavaClassV | ConstPool : ([1,{0,'java.lang.Thread$1$2,'java.lang.Thread]] [2,{'Process,'c}]),Lock : Lock(emptyOidList, NoThread, 0),StaticFieldValues : ({'java.lang.Thread,emptyFieldPairList} {'Process,[['c,I]]}) > Conf |= TG(J) = if I == J then true else false fi . op c1stop : -> Prop . op stage1return : -> Prop . var ATS : AttributeSet . eq < 'CheckPoints : JavaClassV | ATS ,StaticFieldValues : ({'java.lang.Object, emptyFieldPairList} {'CheckPoints,[['sreturn,I]] [['stop,1]]}) > Conf |= c1stop = true . eq Conf |= c1stop = false [owise] . eq < 'CheckPoints : JavaClassV | ATS ,StaticFieldValues : ({'java.lang.Object, emptyFieldPairList} {'CheckPoints,[['sreturn,1]] [['stop,I]]}) > Conf |= stage1return = true . eq Conf |= stage1return = false [owise] . endm