-- $Id: java_stat_execution.ty,v 1.13 10/.0/.2 .1:.1:.4 mrusso Exp $
-- /***************************************************************************/
-- /* Copyright (C) 1997-1999 INRIA Sophia-Antipolis */
-- /* I. Attali, D. Caromel and M. Russo */
-- /* Projet OASIS */
-- /* Rt. des Lucioles, BP 93, */
-- /* F-06902 Sophia Antipolis cedex */
-- /* (+33) 4 92 38 76 31 */
-- /* All rights reserved */
-- /***************************************************************************/
program java_stat_execution is
use java;
use PSP;
import
executeOneInstruction (
Objects, ClassVariablesL, ObjectId |- Clr -> Objects, ClassVariablesL, Clr, ThreadStatus )
from java_concurrency;
import
ENVaddTheCrossedReferencesToTheInteractionStacks (
ObjectId, ObjectId ) , ENVchangeObjectStatusInStatusList ( ObjectId )
, ENVsendException ( Exception ) ,
ENVsendObjectAndClassVariableLists ( Objects, ClassVariablesL ) ,
ENVsendRemoveLockOnObject ( ObjectId ) ,
ENVupdateEnvIfNonDormantOrBlockedThreadOnObject (
ObjectId, Objects, integer ) from java_environment;
import
evaluateExpression (
Objects, ClassVariablesL, Env, ObjectId, ObjectId, Identifier |-
SemExpression -> Objects, ClassVariablesL, Env, SemExpression, Insts, ThreadStatus ) ,
isValue ( SemExpression -> Bool )
from java_expr_evaluation;
import isMyAncestor ( Type |- Type -> Bool )
from java_inheritance;
import
getInstructionsAndLocalVariables (
Insts, Locs |- Block => Insts, Locs ) ,
getNumberOfDormantAndBlockedThreadsOnTheGivenObject (
ObjectId |- Objects -> integer, integer ) ,
getObjectLockInformation (
ObjectId |- Objects -> ObjectId, integer ) ,
releaseObjectLock ( ObjectId |- Objects -> Objects ) ,
setLock (
ObjectId, ObjectId, Val |- Objects -> Objects ) ,
getObjectType ( ObjectId |- Objects -> Type )
from java_object_list;
import
appendtree ( _, _, _ ) , diff ( _, _ ) , emit_tree ( _, _ ) , eq ( _, _ ) , plus ( _, _, _ ) , sub ( _, _, _ ) , not_eq ( _, _ )
from prolog() ;
var TVValue: Val;
var TVBl: Block;
var TVObjId: ObjectId;
var TVVarDecl: LocalVariableDeclaration;
var TVInitExprs: ArgumentList;
set executeANonExpression is
--RC:
--RC:
--RC: Concerned Statements:
--RC: * Synchronized methods or blocks
--RC: * Return statement
--RC: * If, Else Block
--RC: * Try, Catch or Finally Blocks
--JC:
judgement
Objects, ClassVariablesL, ObjectId |- Clr -> Objects, ClassVariablesL, Clr, ThreadStatus;
SkipEmptyStatement:
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[none().InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
SynchronizedStatement_ConversionIntoASynchroComp:
--BSC: Synchronized Statement
--
--CS: synchronized(Expr) Statement
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env, insts[synchroBegin(Expr, Statement).InstL]) -> ObjL1_1, ClVarL1_1, Clr, ThStatus
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env, insts[synchro(Expr, Statement).InstL]) -> ObjL1_1, ClVarL1_1, Clr, ThStatus ;
SynchronizedStatement_HasTheObjectReference:
--CS: synchronized(#8) Statement
ObjL1, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[synchroLock(TVObjId, Statement).InstL]) -> ObjL1_1, ClVarL_1, Clr, ThStatus
--------------------------------
ObjL1, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[synchroBegin(TVObjId, Statement).InstL]) -> ObjL1_1, ClVarL_1, Clr, ThStatus ;
SynchronizedStatement_EvaluateExpressionToGetTheObjectReference:
--CS: synchronized(Obj.getObj2()) Statement
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[synchroBegin(Expr1_1, Statement).InstL1], InstL3 )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env1, insts[synchroBegin(Expr1, Statement).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, Env1_1, InstL3), ThStatus ;
SynchronizedStatement_GetTheLockOrBeBlocked:
--CS: synchronized(#8) Statement
getObjectLockInformation(
ObjId2 |- ObjL1 -> OThId2, nbLocks ) &
getTheLockOrBeBlocked(
OThId1, ObjId2, Statement, ObjL1, ClVarL |- OThId2, nbLocks -> ObjL1_1, Inst, ThStatus )
--------------------------------
ObjL1, ClVarL, OThId1 |-
clr(ObjId1, Mode, MethName, Env, insts[synchroLock(ObjId2, Statement).InstL]) ->
ObjL1_1, ClVarL, clr(ObjId1, Mode, MethName, Env, insts[Inst.InstL]), ThStatus ;
SynchronizedStatement_BeginBlockExecution:
appendtree( insts[Statement, synchroEnd(ObjId2)], InstL1, InstL2 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId1, Mode, MethName, Env, insts[synchroExecution(ObjId2, Statement).InstL1]) ->
ObjL, ClVarL, clr(ObjId1, Mode, MethName, Env, InstL2), runnable() ;
SynchronizedStatement_AfterANotify:
--RC: The current executing thread retrieves the lock(s) that it had
--RC: before the wait() method call on the given object.
getObjectLockInformation( ObjId2 |- ObjL1 -> _, 0 )
&
setLock(
ObjId2, OThId, nbLocks |- ObjL1 -> ObjL1_1 )
--------------------------------
ObjL1, ClVarL, OThId |-
clr(ObjId1, Mode, MethName, Env, insts[synchroWaitEndRelock(ObjId2, nbLocks).InstL]) ->
ObjL1_1, ClVarL, clr(ObjId1, Mode, MethName, Env, InstL), runnable() ;
do
ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL );
EndSynchronizedStatementWithOneLock_RemoveLock:
getObjectLockInformation( ObjId2 |- ObjL1 -> OThId, 1 )
&
releaseObjectLock( ObjId2 |- ObjL1 -> ObjL1_1 )
--------------------------------
ObjL1, ClVarL, OThId |-
clr(ObjId1, Mode, MethName, Env, insts[synchroEnd(ObjId2).InstL]) ->
ObjL1_1, ClVarL, clr(ObjId1, Mode, MethName, Env, InstL), runnable() ;
do
ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL )
&
ENVupdateEnvIfNonDormantOrBlockedThreadOnObject(
ObjId2, ObjL1_1, 0 ) &
ENVchangeObjectStatusInStatusList( ObjId2 );
EndSynchronizedStatementWithSeveralLocks_RemoveOneLock:
--ESC: End Synchronized
--
getObjectLockInformation(
ObjId2 |- ObjL1 -> OThId, nbLocks1 ) & diff( integer nbLocks1, integer 1 )
& sub( nbLocks1, 1, nbLocks1_1 ) &
setLock(
ObjId2, OThId, integer nbLocks1_1 |- ObjL1 -> ObjL1_1 )
--------------------------------
ObjL1, ClVarL, OThId |-
clr(ObjId1, Mode, MethName, Env, insts[synchroEnd(ObjId2).InstL]) ->
ObjL1_1, ClVarL, clr(ObjId1, Mode, MethName, Env, InstL), runnable() ;
do
ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL );
ReturnAnExpression_FirstStepExpressionEvaluation:
--BSC: Return Statement
--
--CS: return(Obj4.foo());
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[semReturn(Expr1_1).InstL1], InstL3 )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env1, insts[return(Expr1).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, Env1_1, InstL3), ThStatus ;
provided diff( Expr1, none() );
ReturnNothing_LeaveTheBlock_GetTheSynchroEndOfTheBlockAndTheClosure:
--RC: Retrieves from the block all the "synchroEnd" instructions before
--RC: leaving this block. Retrieves also all the "synchroEnd" instruction
--RC: present in the current closure.
--
--CS: return;
getSynchroEndInstructions( InstL2 -> InstL3 ) &
getSynchroEndInstructions( InstL1 -> InstL4 ) &
appendtree( insts[semBlock(insts[], blockEnv(ParamL, LocVarL, BlLocVarL)).InstL3], InstL4, InstL5 ) &
appendtree( InstL5, insts[return(none())], InstL5_1 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semBlock(insts[return(none()).InstL2], blockEnv(ParamL, LocVarL, BlLocVarL)).InstL1])
->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL5_1), runnable() ;
ReturnAValue_LeaveTheBlock_GetTheSynchroEndOfTheBlockAndTheClosure:
--RC: Retrieves from the block all the "synchroEnd" instructions before
--RC: leaving this block. Retrieves also all the "synchroEnd" instruction
--RC: present in the current closure.
--
--CS: return(33);
getSynchroEndInstructions( InstL2 -> InstL3 ) &
getSynchroEndInstructions( InstL1 -> InstL4 ) &
appendtree( insts[semBlock(insts[], blockEnv(ParamL, LocVarL, BlLocVarL)).InstL3], InstL4, InstL5 ) &
appendtree( InstL5, insts[return(TVValue)], InstL5_1 )
--------------------------------
ObjL, ClVarL, _ |-
clr(
ObjId, Mode, MethName, env(ParamL, LocVarL),
insts[semBlock(insts[return(TVValue).InstL2], blockEnv(ParamL, LocVarL, BlLocVarL)).InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, env(ParamL, LocVarL), InstL5_1), runnable() ;
ReturnAnExpression_ExpressionEvaluation:
--CS: return(#5.foo());
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[semReturn(Expr1_1).InstL1], InstL3 )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env1, insts[semReturn(Expr1).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, Env1_1, InstL3), ThStatus ;
provided diff( Expr1, none() );
ReturnAnEvaluatedExpression_LeaveTheBlock:
--CS: return(Obj3);
getSynchroEndInstructions( InstL2 -> InstL3 ) &
getSynchroEndInstructions( InstL1 -> InstL4 ) &
appendtree( insts[semBlock(insts[], blockEnv(ParamL, LocVarL, BlLocVarL)).InstL3], InstL4, InstL5 ) &
appendtree( InstL5, insts[semReturn(TVValue)], InstL5_1 )
--------------------------------
ObjL, ClVarL, _ |-
clr(
ObjId, Mode, MethName, env(ParamL, LocVarL),
insts[semBlock(insts[semReturn(TVValue).InstL2], blockEnv(ParamL, LocVarL, BlLocVarL)).InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, env(ParamL, LocVarL), InstL5_1), runnable() ;
ReturnNothing_LeaveTheClosure:
getSynchroEndInstructions( InstL2 -> InstL3 ) &
appendtree( insts[clr(ObjId2, Mode2, MethName2, Env2, insts[]).InstL3], InstL1, InstL4 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2, insts[return(none()).InstL2]).InstL1]) ->
ObjL, ClVarL, clr(ObjId1, Mode1, MethName1, Env1, InstL4), runnable() ;
ReturnAnEvaluatedExpression_LeaveTheClosure:
getSynchroEndInstructions( InstL2 -> InstL3 ) &
isReturnBeTheFirstLocalVariable( Env1 -> true() )
&
appendtree(
insts[clr(ObjId2, Mode2, MethName2, Env2, insts[]).InstL3],
insts[semAssign(empty(), identifier "7RETURN", assignment(), TVValue).InstL1], InstL4 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2, insts[semReturn(TVValue).InstL2]).InstL1])
->
ObjL, ClVarL, clr(ObjId1, Mode1, MethName1, Env1, InstL4), runnable() ;
ReturnAValue_LeaveTheClosure:
getSynchroEndInstructions( InstL2 -> InstL3 ) &
isReturnBeTheFirstLocalVariable( Env1 -> true() )
&
appendtree(
insts[clr(ObjId2, Mode2, MethName2, Env2, insts[]).InstL3], insts[binaryAssign(identifier "7RETURN", assignment(), TVValue).InstL1],
InstL4 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2, insts[return(TVValue).InstL2]).InstL1]) ->
ObjL, ClVarL, clr(ObjId1, Mode1, MethName1, Env1, InstL4), runnable() ;
ReturnAnEvaluatedExpressionNotUseful_LeaveTheClosure:
getSynchroEndInstructions( InstL2 -> InstL3 ) &
isReturnBeTheFirstLocalVariable( Env1 -> false() )
& appendtree( insts[clr(ObjId2, Mode2, MethName2, Env2, insts[]).InstL3], InstL1, InstL4 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2, insts[semReturn(TVValue).InstL2]).InstL1])
->
ObjL, ClVarL, clr(ObjId1, Mode1, MethName1, Env1, InstL4), runnable() ;
ReturnAValueNotUseful_LeaveTheClosure:
--ESC: Return Statement
--
getSynchroEndInstructions( InstL2 -> InstL3 ) &
isReturnBeTheFirstLocalVariable( Env1 -> false() )
& appendtree( insts[clr(ObjId2, Mode2, MethName2, Env2, insts[]).InstL3], InstL1, InstL4 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2, insts[return(TVValue).InstL2]).InstL1]) ->
ObjL, ClVarL, clr(ObjId1, Mode1, MethName1, Env1, InstL4), runnable() ;
IfExpressionThenElse_EvaluateExpression:
--BSC: If Statement
--
--CS: if(Obj2.foo() > 9) Statement1 else Statement2;
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[if(Expr1_1, Stat1, Stat2).InstL1], InstL3 )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId1, Mode, MethName, Env1, insts[if(Expr1, Stat1, Stat2).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId1, Mode, MethName, Env1_1, InstL3), ThStatus ;
provided diff( Expr1, true() ) & diff( Expr1, false() );
IfFalseWithoutElse_NothingToDo:
--CS: if(false) Statement;
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[if(false(), _, none()).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
IfFalse_ExecuteTheElseStatement:
--CS: if(false) Statement1 else Statement2;
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[if(false(), _, ElseStatement).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[ElseStatement.InstL]), runnable() ;
IfTrue_ExecuteTheThenStatement:
--CS: if(true) Statement;
--
--ESC: If Statement
--
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[if(true(), ThenStatement, _).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[ThenStatement.InstL]), runnable() ;
SwitchExecution_EvaluateExpression:
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[switch(Expr_1, SwitchBlk).InstL1], InstL3 )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[switch(Expr, SwitchBlk).InstL1]) ->
ObjL_1, ClVarL_1, clr(ObjId, Mode, MethName, Env_1, InstL3), ThStatus ;
provided isValue( Expr -> false() );
SwitchExecution_FindStatements:
selectSwitchStatements( Expr, SwitchBlk -> Block )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[switch(Expr, SwitchBlk).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[Block.InstL]), runnable() ;
provided isValue( Expr -> true() );
WhileExpression_Conversion:
--BSC: While Statement
--
--CS: while(Obj.getAttr() == 5) {Statement}
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[while(Expr, WhileStatement).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[semWhile(Expr, WhileStatement, Expr).InstL]), runnable() ;
DoExpression_Conversion:
--BSC: Do Statement - transform to while.
--
--CS: do {Statement} while(Obj.getAttr() == 5)
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[doloop(DoStatement, Expr).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[DoStatement, semWhile(Expr, DoStatement, Expr).InstL]), runnable() ;
WhileExpression_EvaluateExpression:
--CS: while(Expression) {Statement};
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[semWhile(Expr1_1, WhileStatement, Expr2).InstL1], InstL3 )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env1, insts[semWhile(Expr1, WhileStatement, Expr2).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, Env1_1, InstL3), ThStatus ;
provided diff( Expr1, true() ) & diff( Expr1, false() );
WhileTrue_ExecuteStatement:
--CS: while(true) {Statement};
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semWhile(true(), WhileStatement, Expr).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[WhileStatement, semWhile(Expr, WhileStatement, Expr).InstL]), runnable() ;
WhileFalse_ExecuteStatement:
--CS: while(false) {Statement};
--
--ESC: While statement
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semWhile(false(), _, _).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
ForConversion_NoNewLocals:
--BSC: Convert a for statement which does not introduce new local
--BSC: variables into a (possibly empty) list of initialization
--BSC: instructions and a semFor.
--
--CS: for (x = 1; x < 10; x++) stmt
convertArgumentListToInsts( TVInitExprs -> InitExprs_1 )
& unoptOptExpr( MaybePred, true() -> Pred )
& appendtree( InitExprs_1, insts[semFor(Pred, ForStmt, UpdExprs, Pred).InstL1], InstL2 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[for(TVInitExprs, MaybePred, UpdExprs, ForStmt).InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL2), runnable() ;
ForConversion_NewLocals:
--BSC: Convert a for statement which does introduce new local
--BSC: variables into a block containing a semFor.
--
--CS: for (int x = 1; x < 10; x++) stmt
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[block[TVVarDecl, for(arguments[], MaybePred, UpdExprs, ForStmt)].InstL]) ->
ObjL_1, ClVarL_1, Clr, ThStatus
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[for(TVVarDecl, MaybePred, UpdExprs, ForStmt).InstL]) ->
ObjL_1, ClVarL_1, Clr, ThStatus ;
ForExecution_EvaluatePredicate:
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Pred1 -> ObjL_1, ClVarL_1, Env_1, Pred1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[semFor(Pred1_1, ForStmt, UpdExprs, Pred).InstL1], InstL3 )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[semFor(Pred1, ForStmt, UpdExprs, Pred).InstL1]) ->
ObjL_1, ClVarL_1, clr(ObjId, Mode, MethName, Env_1, InstL3), ThStatus ;
provided diff( Pred1, true() ) & diff( Pred1, false() );
ForExecution_True:
convertArgumentListToInsts( UpdExprs -> UpdExprs_1 )
& appendtree( insts[ForStmt.UpdExprs_1], insts[semFor(Pred, ForStmt, UpdExprs, Pred).InstL1], InstL2 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semFor(true(), ForStmt, UpdExprs, Pred).InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL2), runnable() ;
ForExecution_False:
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semFor(false(), _, _, _).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
Block_GetInstructionsAndEnvironment:
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- TVBl => InstL2, locs[BlLocVarL._] ) &
appendtree( insts[semBlock(InstL2, blockEnv(ParamL, LocVarL, BlLocVarL))], InstL1, InstL3 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, env(ParamL, LocVarL), insts[TVBl.InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, env(ParamL, LocVarL), InstL3), runnable() ;
NoMoreInstructionInTheBlock:
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semBlock(insts[], _).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
NoMoreClosureInstructionInTheBlock:
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semBlock(insts[clr(_, _, _, _, insts[]).InstL2], EnvBlock).InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[semBlock(InstL2, EnvBlock).InstL1]), runnable() ;
BreakInBlock_GetSynchroEndInstructions:
getSynchroEndInstructions( InstL2 -> InstL3 ) &
appendtree( insts[semBlock(insts[], EnvBlock).InstL3], InstL1, InstL4 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[semBlock(insts[break(none()).InstL2], EnvBlock).InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL4), runnable() ;
Except:
getSynchroEndInstructions( InstL1 -> InstL2 ) &
appendtree( InstL2, insts[exception(OThId, ObjId1, MethName, except(ClName, ObjId2, ExceptText))], InstL3 )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId1, Mode, MethName, Env, insts[except(ClName, ObjId2, ExceptText).InstL1]) ->
ObjL, ClVarL, clr(ObjId1, Mode, MethName, Env, InstL3), runnable() ;
ExceptInBlock_GetSynchroEndInBlockAndClosure:
--RC: Gets the synchronized blocks ends instructions in the current
--RC: block and in the current closure. The new instruction list is made
--RC: of the empty block, the release locks instructions and of the
--RC: exception instruction.
getSynchroEndInstructions( InstL2 -> InstL3 ) &
getSynchroEndInstructions( InstL1 -> InstL4 ) &
appendtree( insts[semBlock(insts[], EnvBlock).InstL3], InstL4, InstL5 ) &
appendtree( InstL5, insts[exception(OThId, ObjId1, MethName, except(ClName, ObjId2, ExceptText))], InstL6 )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId1, Mode, MethName, Env, insts[semBlock(insts[except(ClName, ObjId2, ExceptText).InstL2], EnvBlock).InstL1]) ->
ObjL, ClVarL, clr(ObjId1, Mode, MethName, Env, InstL6), runnable() ;
ExceptInClosure_GetSynchroEndInClosure:
--RC: Gets the release lock instructions of the current closure.
--RC: Put them in front of the instruction list before the empty
--RC: closure and the exception.
--
--ESC: Except Statement
getSynchroEndInstructions( InstL2 -> InstL3 ) &
appendtree(
InstL3,
insts[clr(ObjId2, Mode2, MethName2, Env2, insts[]), exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)).InstL1],
InstL4 )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2, insts[except(ClName, ObjId3, ExceptText).InstL2]).InstL1])
->
ObjL, ClVarL, clr(ObjId1, Mode1, MethName1, Env1, InstL4), runnable() ;
NonCaughtExceptionInMainMethod:
--BSC: Exception Statement
--
--RC: As the exception is uncaught, the thread execution
--RC: is aborted (empty instruction list) and the exception
--RC: is sent to the environment.
ObjL, ClVarL, OThId |-
clr(OThId, Mode, identifier "main", Env, insts[exception(OThId, ObjId1, MethName, except(ClName, ObjId2, ExceptText))._])
->
ObjL, ClVarL, clr(OThId, Mode, identifier "main", Env, insts[]), runnable() ;
do
ENVsendException(
exception(OThId, ObjId1, MethName, except(ClName, ObjId2, ExceptText)) );
NonCaughtExceptionInRunMethod:
--RC: As the exception is uncaught, the thread execution
--RC: is aborted (empty instruction list) and the exception
--RC: is sent to the environment.
ObjL, ClVarL, OThId |-
clr(OThId, Mode, identifier "run", Env, insts[exception(OThId, ObjId1, MethName, except(ClName, ObjId2, ExceptText))._])
->
ObjL, ClVarL, clr(OThId, Mode, identifier "run", Env, insts[]), runnable() ;
do
ENVsendException(
exception(OThId, ObjId1, MethName, except(ClName, ObjId2, ExceptText)) );
ExceptionInBlock_GetSynchroEndInBlockAndClosure:
--RC: Gets the synchronized blocks ends instructions in the current
--RC: block and in the current closure. The new instruction list is made
--RC: of the empty block, the release locks instructions and of the
--RC: exception instruction.
getSynchroEndInstructions( InstL2 -> InstL3 ) &
getSynchroEndInstructions( InstL1 -> InstL4 ) &
appendtree( insts[semBlock(insts[], EnvBlock).InstL3], InstL4, InstL5 ) &
appendtree( InstL5, insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText))], InstL6 )
--------------------------------
ObjL, ClVarL, OThId |-
clr(
ObjId1, Mode, MethName1, Env,
insts[semBlock(insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)).InstL2], EnvBlock).InstL1])
->
ObjL, ClVarL, clr(ObjId1, Mode, MethName1, Env, InstL6), runnable() ;
ExceptionInClosure_GetSynchroEndInClosure:
--RC: Gets the synchronized blocks ends instructions in the current
--RC: closure. The new instruction list is made of the closure with
--RC: the release locks instructions and of the exception instruction.
--
--ESC: Exception Statement
getSynchroEndInstructions( InstL2 -> InstL3 )
--------------------------------
ObjL, ClVarL, OThId |-
clr(
ObjId1, Mode1, MethName1, Env1,
insts[
clr(ObjId2, Mode2, MethName2, Env2, insts[exception(OThId, ObjId3, MethName3, except(ClName, ObjId4, ExceptText)).InstL2]).InstL1])
->
ObjL, ClVarL,
clr(
ObjId1, Mode1, MethName1, Env1,
insts[clr(ObjId2, Mode2, MethName2, Env2, InstL3), exception(OThId, ObjId3, MethName3, except(ClName, ObjId4, ExceptText)).InstL1]),
runnable() ;
TryExpression_GetInstructionAndLocalVariables:
--BSC: Try Statement
--
--CS: try{ Bl }
--CS: catch(Type){ Bl1 }*
--CS: finally{ Bln }
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- TVBl => InstL2, locs[BlLocVarL._] ) &
appendtree( insts[tryBlockExecution(semBlock(InstL2, blockEnv(ParamL, LocVarL, BlLocVarL)), CatchL, Final)], InstL1, InstL3 )
--------------------------------
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, env(ParamL, LocVarL), insts[try(TVBl, CatchL, Final).InstL1]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, env(ParamL, LocVarL), InstL3), runnable() ;
EndTryBlockWithoutFinallyBlock:
--RC: End of the execution of the try block without an exception.
--RC: There is no finally block to execute.
--
--CS: try{}
--CS: catch(Type){ Bl1 }*
--CS: finally{}
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[tryBlockExecution(semBlock(insts[], _), _, none()).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
EndTryBlockWithFinally_ExecuteTheFinallyBlock:
--RC: End of the execution of the try block without an exception.
--RC: There is a finally block to execute before exiting the try
--RC: expression execution.
--
--CS: try{ }
--CS: catch(Type){ Bl1 }*
--CS: finally{ Bln }
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[tryBlockExecution(semBlock(insts[], _), _, TVBl).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[tryFinallyExecutionBegin(TVBl).InstL]), runnable() ;
ExceptionInTryBlock_CatchTheException:
--RC: There is a good catch clause so it will be executed at the next
--RC: execution step of the current executing thread 'OThId'.
getTheCatchClauseIfPossible( ClName |- CatchL -> Catch, true() )
--------------------------------
ObjL, ClVarL, OThId |-
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryBlockExecution(semBlock(insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText))], EnvBlock), CatchL, Final).
InstL]) ->
ObjL, ClVarL,
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryBlockExecution(semBlock(insts[], EnvBlock), catches[], none()),
tryCatchBlockExecutionBegin(exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)), Catch, Final).InstL]),
runnable() ;
TryCatchBlock_GetInstructionsAndLocalVariables:
--CS: catch(ClName2 Ident){ Bl }
--CS: finally{ Fin }
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- TVBl => InstL2, locs[BlLocVarL._] )
--------------------------------
ObjL, ClVarL, OThId |-
clr(
ObjId1, Mode, MethName1, env(ParamL, LocVarL),
insts[
tryCatchBlockExecutionBegin(
exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)), catch(parameter(_, _, Param), TVBl), Final).InstL1])
->
ObjL, ClVarL,
clr(
ObjId1, Mode, MethName1, env(ParamL, LocVarL),
insts[
tryCatchBlockExecution(
exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)),
semBlock(InstL2, blockEnv(pairs[pair(Param, ObjId3).ParamL], LocVarL, BlLocVarL)), Final).InstL1]), runnable() ;
EndCatchBlockWithAnException_WithoutFinallyBlock:
--RC: End of the execution of the catch block with an exception.
--RC: There is no finally block to execute.
--
--CS: try{}
--CS: catch(Type){ Exception }
--CS: finally{}
ObjL, ClVarL, _ |-
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryCatchBlockExecution(_, semBlock(insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText))], _), none()).InstL])
->
ObjL, ClVarL,
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryCatchBlockExecution(_, semBlock(insts[], _), none()), exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)).
InstL]), runnable() ;
EndCatchBlockWithAnException_WithFinallyBlock:
--RC: End of the execution of the catch block with an exception.
--RC: There is a finally block to execute before treating the exception.
--
--CS: try{}
--CS: catch(Type){ Exception }
--CS: finally{ Bl }
ObjL, ClVarL, _ |-
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryCatchBlockExecution(_, semBlock(insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText))], _), TVBl).InstL])
->
ObjL, ClVarL,
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryCatchBlockExecution(_, semBlock(insts[], _), none()), tryFinallyExecutionBegin(TVBl),
exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)).InstL]), runnable() ;
EndCatchBlockWithoutFinallyBlock:
--RC: End of the execution of the catch block without an exception.
--RC: There is no finally block to execute.
--
--CS: try{}
--CS: catch(Type){ }
--CS: finally{}
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[tryCatchBlockExecution(_, semBlock(insts[], _), none()).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
EndCatchBlock_ExecuteTheFinallyBlock:
--RC: End of the execution of the catch block without an exception.
--RC: There is a finally block to execute before exiting the try
--RC: expression execution.
--
--CS: try{ Bl }
--CS: catch(Type){ }
--CS: finally{ Bln }
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, env(ParamL, LocVarL), insts[tryCatchBlockExecution(_, semBlock(insts[], _), TVBl).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, env(ParamL, LocVarL), insts[tryFinallyExecutionBegin(TVBl).InstL]), runnable() ;
Catch_ExecuteOneInstruction:
--CS: try{ Bl }
--CS: catch(Type){ Bl1 }*
--CS: finally{ Bln }
executeOneInstruction(
ObjL1, ClVarL1, OThId |-
clr(ObjId1, Mode, MethName1, env(pairs[Param.ParamL1], locs[BlLocVarL1.LocVarL1]), insts[Inst.InstL2]) ->
ObjL1_1, ClVarL1_1, clr(ObjId1, Mode, MethName1, env(pairs[Param.ParamL1_1], locs[BlLocVarL1_1.LocVarL1_1]), InstL3), ThStatus )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(
ObjId1, Mode, MethName1, env(ParamL1, LocVarL1),
insts[
tryCatchBlockExecution(
exception(OThId, ObjId2, MethName2, except(ClName1, ObjId3, ExceptText)),
semBlock(insts[Inst.InstL2], blockEnv(pairs[Param], LocVarL1, BlLocVarL1)), Final).InstL1]) ->
ObjL1_1, ClVarL1_1,
clr(
ObjId1, Mode, MethName1, env(ParamL1_1, LocVarL1_1),
insts[
tryCatchBlockExecution(
exception(OThId, ObjId2, MethName2, except(ClName1, ObjId3, ExceptText)),
semBlock(InstL3, blockEnv(pairs[Param], LocVarL1_1, BlLocVarL1_1)), Final).InstL1]), ThStatus ;
EndTryWithAnException_NoCorrespondingCatchClauseOrFinally_ThrowTheException:
getTheCatchClauseIfPossible( ClName |- CatchL -> _, false() )
--------------------------------
ObjL, ClVarL, OThId |-
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryBlockExecution(semBlock(insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText))], _), CatchL, none()).InstL])
->
ObjL, ClVarL, clr(ObjId1, Mode, MethName1, Env, insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)).InstL]),
runnable() ;
EndTryWithAnException_NoCorrespondingCatchClause_ExecuteTheFinallyBlock:
getTheCatchClauseIfPossible( ClName |- CatchL -> _, false() )
--------------------------------
ObjL, ClVarL, OThId |-
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryBlockExecution(semBlock(insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText))], _), CatchL, Final).InstL])
->
ObjL, ClVarL,
clr(ObjId1, Mode, MethName1, Env, insts[Final, exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)).InstL]),
runnable() ;
provided diff( Final, none() );
TryBlock_executeOneInstruction:
--CS: try{ Bl }
--CS: catch(Type){ Bl1 }*
--CS: finally{ Bln }
executeOneInstruction(
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, env(ParamL1, locs[BlLocVarL1.LocVarL1]), insts[Inst.InstL2]) ->
ObjL1_1, ClVarL1_1, clr(ObjId1, Mode, MethName, env(ParamL1_1, locs[BlLocVarL1_1.LocVarL1_1]), InstL3), ThStatus )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(
ObjId, Mode, MethName, env(ParamL1, LocVarL1),
insts[tryBlockExecution(semBlock(insts[Inst.InstL2], blockEnv(ParamL1, LocVarL1, BlLocVarL1)), CatchL, Final).InstL1])
->
ObjL1_1, ClVarL1_1,
clr(
ObjId, Mode, MethName, env(ParamL1_1, LocVarL1_1),
insts[tryBlockExecution(semBlock(InstL3, blockEnv(ParamL1_1, LocVarL1_1, BlLocVarL1_1)), CatchL, Final).InstL1]), ThStatus ;
EnterInAFinallyBlock:
--CS: try{}
--CS: catch(Type){ Bl1 }*
--CS: finally{ Bl }
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- TVBl => InstL2, locs[BlLocVarL._] )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, env(ParamL, LocVarL), insts[tryFinallyExecutionBegin(TVBl).InstL1]) ->
ObjL, ClVarL,
clr(
ObjId, Mode, MethName, env(ParamL, LocVarL),
insts[tryFinallyExecution(semBlock(InstL2, blockEnv(ParamL, LocVarL, BlLocVarL))).InstL1]), runnable() ;
FinallyBlock_ExecuteOneInstruction:
--CS: try{ Bl }
--CS: catch(Type){ Bl1 }*
--CS: finally{ Bln }
executeOneInstruction(
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, env(ParamL1, locs[BlLocVarL1.LocVarL1]), insts[Inst.InstL2]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, env(ParamL1_1, locs[BlLocVarL1_1.LocVarL1_1]), InstL3), ThStatus )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(
ObjId, Mode, MethName, env(ParamL1, LocVarL1),
insts[tryFinallyExecution(semBlock(insts[Inst.InstL2], blockEnv(ParamL1, LocVarL1, BlLocVarL1))).InstL1]) ->
ObjL1_1, ClVarL1_1,
clr(
ObjId, Mode, MethName, env(ParamL1_1, LocVarL1_1),
insts[tryFinallyExecution(semBlock(InstL3, blockEnv(ParamL1_1, LocVarL1_1, BlLocVarL1_1))).InstL1]), ThStatus ;
ExceptionDuringFinallyBlockExecution:
--CS: finally{ Exception }
ObjL, ClVarL, _ |-
clr(
ObjId1, Mode, MethName1, Env,
insts[tryFinallyExecution(semBlock(insts[exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText))], EnvBlock)).InstL])
->
ObjL, ClVarL,
clr(
ObjId1, Mode, MethName1, Env,
insts[
tryFinallyExecution(semBlock(insts[], EnvBlock)), exception(OThId, ObjId2, MethName2, except(ClName, ObjId3, ExceptText)).InstL]),
runnable() ;
EndFinallyBlockExecutionWithoutAnException:
--CS: finally{ }
--
--ESC: Try statement
ObjL, ClVarL, _ |-
clr(ObjId, Mode, MethName, Env, insts[tryFinallyExecution(semBlock(insts[], EnvBlock)).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable() ;
ThrowExpression_EvaluatedExpression:
--BSC: Throw Statement
--
--CS: throw #4
getObjectType( TVObjId |- ObjL -> ClName )
--------------------------------
ObjL, ClVarL, OThId |-
clr(ObjId, Mode, MethName, Env, insts[semThrow(TVObjId).InstL]) ->
ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, insts[except(ClName, TVObjId, exceptText "thrown exception").InstL]), runnable() ;
ThrowExpression_EvaluateExpression:
--CS: throw Expr;
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[semThrow(Expr1_1).InstL1], InstL3 )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env1, insts[semThrow(Expr1).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, Env1_1, InstL3), ThStatus ;
ThrowExpression_EvaluateExpression:
--CS: throw Expr;
--
--ESC: Throw Statement
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL2, ThStatus ) &
appendtree( InstL2, insts[semThrow(Expr1_1).InstL1], InstL3 )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, Env1, insts[throw(Expr1).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, Env1_1, InstL3), ThStatus ;
NoMoreInstructionInTheClosure:
ObjL, ClVarL, OThId |-
clr(ObjId1, Mode, MethName, Env, insts[clr(ObjId2, _, _, _, insts[]).InstL]) ->
ObjL, ClVarL, clr(ObjId1, Mode, MethName, Env, InstL), runnable() ;
do
ENVaddTheCrossedReferencesToTheInteractionStacks(
OThId, ObjId2 );
InstructionInBlock:
--CS: {Inst1;InstL2}
executeOneInstruction(
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, env(ParamL1, locs[BlLocVarL1.LocVarL1]), insts[Inst.InstL2]) ->
ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, env(ParamL1_1, locs[BlLocVarL1_1.LocVarL1_1]), InstL3), ThStatus )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId, Mode, MethName, env(ParamL1, LocVarL1), insts[semBlock(insts[Inst.InstL2], blockEnv(ParamL1, LocVarL1, BlLocVarL1)).InstL1])
->
ObjL1_1, ClVarL1_1,
clr(ObjId, Mode, MethName, env(ParamL1_1, LocVarL1_1), insts[semBlock(InstL3, blockEnv(ParamL1_1, LocVarL1_1, BlLocVarL1_1)).InstL1]),
ThStatus ;
InstructionInClosure:
executeOneInstruction(
ObjL1, ClVarL1, OThId |-
clr(ObjId2, Mode2, MethName2, Env2, insts[Inst.InstL2]) ->
ObjL1_1, ClVarL1_1, clr(ObjId2, Mode2, MethName2, Env2_1, InstL3), ThStatus )
--------------------------------
ObjL1, ClVarL1, OThId |-
clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2, insts[Inst.InstL2]).InstL1]) ->
ObjL1_1, ClVarL1_1, clr(ObjId1, Mode1, MethName1, Env1, insts[clr(ObjId2, Mode2, MethName2, Env2_1, InstL3).InstL1]), ThStatus ;
provided
ENVaddTheCrossedReferencesToTheInteractionStacks(
OThId, ObjId2 );
set getTheLockOrBeBlocked is
--SC: Locks the given object if it is not already locked.
--SC: If the given object is already locked by
--SC: 1] by the current thread, the number of locks on this object is
--SC: increased by one.
--SC: 2] by an other thread, the current existing thread is blocked to
--SC: wait the unlock of the object
--
--JC: Current executing thread reference, Reference of the object to lock,
--JC: Statement, Objects, Class variables (only used for the environment)
--JC: |- Thread that demands the lock on the given object,
--JC: Number of existing locks on the given object
--JC: -> modified object list, Instruction,
--JC: New current executing thread status
judgement
ObjectId, ObjectId, Statement, Objects, ClassVariablesL |-
ObjectId, integer -> Objects, Inst, ThreadStatus;
UnlockedObject:
setLock(
ObjId, OThId, integer 1 |- ObjL1 -> ObjL1_1 )
--------------------------------
OThId, ObjId, Statement, ObjL1, ClVarL |-
_, 0 -> ObjL1_1, synchroExecution(ObjId, Statement), runnable() ;
do
ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL );
ObjectLockedByAnotherThread:
OThId1, ObjId, Statement, ObjL1, _ |-
OThId2, nbLocks -> ObjL1, synchroLock(ObjId, Statement), blocked(ObjId) ;
provided diff( nbLocks, 0 ) & diff( OThId1, OThId2 );
ObjectLockedByTheCurrentThread:
plus( nbLocks1, 1, nbLocks1_1 ) &
setLock(
ObjId, OThId, integer nbLocks1_1 |- ObjL1 -> ObjL1_1 )
--------------------------------
OThId, ObjId, Statement, ObjL1, ClVarL |-
OThId, nbLocks1 -> ObjL1_1, synchroExecution(ObjId, Statement), runnable() ;
provided diff( nbLocks, 0 );
do
ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL );
end getTheLockOrBeBlocked ;
end executeANonExpression;
set getTheCatchClauseIfPossible is
--SC: Retrives from the catch blocks the first catch block that has the
--SC: corresponding exception type (or sub-type) as argument
--SC: Returns false if no corresponding catch block is found.
--
--JC: Class name of the exception that needs to be catched
--JC: |- Catch blocks of the try
--JC: -> found catch block, true/false if not found
judgement Identifier |- Catches -> Catch, Bool;
NoMoreCatchBlock: ClName |- catches[] -> _, false() ;
HasFoundTheCatchBlock_SameType:
ClName |- catches[catch(parameter(ModL, ClName, ParamName), TVBl)._] ->
catch(parameter(ModL, ClName, ParamName), TVBl), true() ;
HasFoundTheCatchBlock_SubType:
isMyAncestor( ClName2 |- ClName1 -> true() )
--------------------------------
ClName1 |- catches[catch(parameter(ModL, ClName2, Ident), TVBl)._] ->
catch(parameter(ModL, ClName2, Ident), TVBl), true() ;
provided diff( ClName1, ClName2 );
RecursiveRule:
isMyAncestor( ClName2 |- ClName1 -> false() )
& ClName1 |- CatchL -> Catch, TV
--------------------------------
ClName1 |- catches[catch(parameter(_, ClName2, _), _).CatchL] -> Catch, TV ;
provided diff( ClName1, ClName2 );
end getTheCatchClauseIfPossible;
set getSynchroEndInstructions is
--SC: Retrieves from an instruction list, all the "synchroEnd" instructions
--SC: useful for removing locks set for a synchronized block or method.
--SC: (the "synchroEnd" instructions are added during the program
--SC: interpretation)
--
--JC: Instruction list
--JC: -> Instruction list that only contains the synchroEnd instructions.
judgement (Insts -> Insts);
NoMoreInstruction: (insts[] -> insts[]) ;
SynchroEndAddedToTheInstrL_RecursiveRule:
(InstL1 -> InstL2)
--------------------------------
(insts[synchroEnd(ObjId1).InstL1] -> insts[synchroEnd(ObjId1).InstL2]) ;
NotASynchroEndInst_RecursiveRule:
(InstL1 -> InstL2)
--------------------------------
(insts[Inst.InstL1] -> InstL2) ;
provided not_eq( Inst, synchroEnd(_) );
end getSynchroEndInstructions;
set isReturnBeTheFirstLocalVariable is
--SC: Checks if the 7RETURN variable (used to return a value from a closure)
--SC: is the first variable in the current local variable list
--
--JC1: Closure environment (i.e. parameters and local variables)
--JC1: -> True if 7RETURN present/False otherwise
judgement (Env -> Bool);
--JC2: set of local variable lists (only the first one is checked)
--JC2: => True/False
judgement (Locs => Bool);
--JC3: current local variable list (only the first variable will be checked)
--JC3: =:> True/false
judgement (Pairs =:> Bool);
GetSetOfLocalVariableLists:
(LocVarL => TF)
--------------------------------
(env(_, LocVarL) -> TF) ;
GetTheFirstLocalVariableList:
(LocVarL =:> TF)
--------------------------------
(locs[LocVarL._] => TF) ;
TheFirstLocalVariableIsNotTheRETURN:
(pairs[pair(LocVarName, _)._] =:> false()) ;
provided diff( LocVarName, identifier "7RETURN" );
EmptyList_RETURNAbsent: (pairs[] =:> false()) ;
RETURNPresentAsFirstLocalVariable:
(pairs[pair(identifier "7RETURN", _)._] =:> true()) ;
end isReturnBeTheFirstLocalVariable;
set selectSwitchStatements is
--SC: Computes a block of the relevant declarations and instructions
--SC: from a switch block given the value of the switch expressions.
--SC: Note that declarations that are not executed are still in scope!
--SC:
--SC: Limitation: The case labels are assumed to be literal constants.
--SC: The reason is that they must be compile time constants. Thus
--SC: it is strictly speaking wrong to evaluate them dynamically using
--SC: a small-setp semantics. A large-step constant expression evaluation
--SC: relation would be needed. Furthermore, evaluating using a small
--SC: step semantics and searching simultaneously seems complicated.
--SC: Maybe a pre-pass which evaluated all labels would be an adequate
--SC: temporary solution.
judgement (SemExpression, SwitchStatements -> Block);
SelectSwitchStatements_LabelFound:
getDeclsBeforeLabel( Label, SwStmts -> Decls, SwStmts_1 )
&
convertSwitchStatementsToBlock( SwStmts_1 -> SelStmts )
& appendtree( Decls, SelStmts, DeclsAndSelStmts )
--------------------------------
(Label, SwStmts -> DeclsAndSelStmts) ;
provided
labelInSwitchBlock( Label, SwStmts -> true() );
--RC: This rule applies even if there is no default.
SelectSwitchStatements_LabelNotFound:
getDeclsBeforeDefault( SwStmts -> Decls, SwStmts_1 ) &
convertSwitchStatementsToBlock( SwStmts_1 -> SelStmts )
& appendtree( Decls, SelStmts, DeclsAndSelStmts )
--------------------------------
(Label, SwStmts -> DeclsAndSelStmts) ;
provided
labelInSwitchBlock( Label, SwStmts -> false() );
end selectSwitchStatements;
set getDeclsBeforeLabel is
--SC: Extracts all declarations from a switch block which occurs before
--SC: the given label, less their initializations. Returns the
--SC: remaining part of the switch block as well as the declarations in
--SC: the form of a Block.
judgement (SemExpression, SwitchStatements -> Block, SwitchStatements);
GetDeclsBeforeLabel_LabelNotFound:
(_, switchStatements[] -> block[], switchStatements[]) ;
GetDeclsBeforeLabel_LabelFound:
(Label, switchStatements[case(Labels, Block).SwStmts] -> block[], switchStatements[case(Labels, Block).SwStmts]) ;
provided
labelInLabelGroup( Label, Labels -> true() );
GetDeclsBeforeLabel_RecursiveCase:
getDeclsFromBlock( Block -> Decls1 ) &
(Label, SwStmts -> Decls2, SwStmts_1) & appendtree( Decls1, Decls2, Decls3 )
--------------------------------
(Label, switchStatements[case(Labels, Block).SwStmts] -> Decls3, SwStmts_1) ;
provided
labelInLabelGroup( Label, Labels -> false() );
end getDeclsBeforeLabel;
set getDeclsBeforeDefault is
--SC: Extracts all declarations from a switch block which occurs before
--SC: the default label, less their initializations. Returns the
--SC: remaining part of the switch block as well as the declarations in
--SC: the form of a Block.
judgement (SwitchStatements -> Block, SwitchStatements);
GetDeclsBeforeDefault_DefaultNotFound:
(switchStatements[] -> block[], switchStatements[]) ;
GetDeclsBeforeDefault_DefaultFound:
(switchStatements[case(Labels, Block).SwStmts] -> block[], switchStatements[case(Labels, Block).SwStmts]) ;
provided defaultInLabelGroup( Labels -> true() );
GetDeclsBeforeDefault_RecursiveCase:
getDeclsFromBlock( Block -> Decls1 ) &
(SwStmts -> Decls2, SwStmts_1) & appendtree( Decls1, Decls2, Decls3 )
--------------------------------
(switchStatements[case(Labels, Block).SwStmts] -> Decls3, SwStmts_1) ;
provided
defaultInLabelGroup( Labels -> false() );
end getDeclsBeforeDefault;
set getDeclsFromBlock is
--SC: Extracts and declarationsfrom a block, less initialization
--SC: expressions.
judgement (Block -> Block);
(block[] -> block[]) ;
(Stmts -> Decls)
--------------------------------
(block[Stmt.Stmts] -> Decls) ;
provided not_eq( Stmt, localVariableDeclaration(_, _, _) );
(Stmts -> Decls) &
removeInitializers( VarDecls -> VarDecls_1 )
--------------------------------
(block[localVariableDeclaration(OptMod, Type, VarDecls).Stmts] ->
block[localVariableDeclaration(OptMod, Type, VarDecls_1).Decls]) ;
end getDeclsFromBlock;
set removeInitializers is
judgement (VariableDeclarators -> VariableDeclarators);
RemoveInitializers_BaseCase1:
(variableDeclarators[initializedVariable(VarDeclId, _)] -> variableDeclarators[VarDeclId]) ;
RemoveInitializers_BaseCase2:
(variableDeclarators[VarDecl] -> variableDeclarators[VarDecl]) ;
provided not_eq( VarDecl, initializedVariable(_, _) );
RemoveInitializers_RecursiveCase1:
(VarDecls -> VarDecls_1)
--------------------------------
(variableDeclarators[initializedVariable(VarDeclId, _).VarDecls] -> variableDeclarators[VarDeclId.VarDecls_1]) ;
RemoveInitializers_RecursiveCase2:
(VarDecls -> VarDecls_1)
--------------------------------
(variableDeclarators[VarDecl.VarDecls] -> variableDeclarators[VarDecl.VarDecls_1]) ;
provided not_eq( VarDecl, initializedVariable(_, _) );
end removeInitializers;
set convertSwitchStatementsToBlock is
--SC: Extracts and concatenates all blocks in a sequence of switch
--SC: statements.
judgement (SwitchStatements -> Block);
(switchStatements[] -> block[]) ;
(SwStmts -> Block2) & appendtree( Block1, Block2, Block3 )
--------------------------------
(switchStatements[case(_, Block1).SwStmts] -> Block3) ;
end convertSwitchStatementsToBlock;
set labelInSwitchBlock is
--SC: Checks if the label occurs among the labels in SwitchStatements.
judgement (SemExpression, SwitchStatements -> Bool);
LabelInSwitchBlock_NotFound: (_, switchStatements[] -> false()) ;
LabelInSwitchBlock_Found:
labelInLabelGroup( Label, Labels -> true() )
--------------------------------
(Label, switchStatements[case(Labels, _)._] -> true()) ;
LabelInSwitchBlock_Found:
labelInLabelGroup( Label, Labels -> false() ) &
(Label, SwitchStatements -> TF)
--------------------------------
(Label, switchStatements[case(Labels, _).SwitchStatements] -> TF) ;
end labelInSwitchBlock;
set labelInLabelGroup is
--SC: Predicates which tests for a given label in a group of labels.
judgement (SemExpression, SwitchLabels -> Bool);
labelInLabelGroup_NotFound: (_, switchLabels[] -> false()) ;
labelInLabelGroup_Found:
(Label, switchLabels[switchLabel(Label)._] -> true()) ;
labelInLabelGroup_RecursiveCase1:
(Label1, Labels -> TF)
--------------------------------
(Label1, switchLabels[switchLabel(Label2).Labels] -> TF) ;
provided diff( Label1, Label2 );
labelInLabelGroup_RecursiveCase2:
(Label1, Labels -> TF)
--------------------------------
(Label1, switchLabels[default().Labels] -> TF) ;
end labelInLabelGroup;
set defaultInLabelGroup is
--SC: Predicates which tests for a default label in a group of labels.
judgement (SwitchLabels -> Bool);
defaultInLabelGroup_NotFound: (switchLabels[] -> false()) ;
defaultInLabelGroup_Found:
(switchLabels[default()._] -> true()) ;
defaultInLabelGroup_RecursiveCase:
(Labels -> TF)
--------------------------------
(switchLabels[Label.Labels] -> TF) ;
provided diff( Label, default() );
end defaultInLabelGroup;
set convertArgumentListToInsts is
--SC: Converts an argument list (i.e. an expression list which may be
--SC: empty) into an instruction list.
--
judgement (ArgumentList -> Insts);
EmptyExpressionList: (arguments[] -> insts[]) ;
RecursiveConversionRule:
(ExprL -> InstL)
--------------------------------
(arguments[Expr.ExprL] -> insts[Expr.InstL]) ;
end convertArgumentListToInsts;
set unoptOptExpr is
--SC: Substitutes the given default expression for none().
--
judgement (OptExpression, Expression -> Expression);
NoExpression: (none(), Default -> Default) ;
AnExpression:
(Expr, _ -> Expr) ;
provided diff( Expr, none() );
end unoptOptExpr;
end java_stat_execution