require "java-core.k"

module JAVA-STATEMENTS

imports JAVA-CORE

//@ \section{Program stack}

//ListItem content as a stack layer

syntax K ::=

"("

StackLayerType "," //StackLT - type of stack layer, see StackLayerType

K "," //CatchParam, X - layer param

K "," //CatchStm, FinallyStm, ... - layer statement

K "," //K - rest of computation

Map "," //Env

Bag //C - rest of control

")"

//stack layer types

syntax StackLayerType ::=

"return" //generated by method invocations, consumed by return

| "catch" //generated by TryCatch, consumed by throw

| "finally" //generated by TryFinally, consumed by all flow interruptions

| "loop" //generated by While / DoWhile / For,

// consumed by break, continue

| "forBody" //generated by for, consumed by continue

| "label" //generated by Labeled, consumed by break with label.

// Also used by loop rules

// to prepare context for continue with label.

| "switch" //generated by switch, consumed by break

syntax K ::= "popx" //discard the top stack layer

rule [popx]:

<k> popx => . ...</k>

<stack> _:ListItem => . ...</stack>

//@ \section{Blocks} JLS $14.2

rule [Block]:

<k> 'Block(S:K) => S ~> env(Env) ...</k>

'ListWrap(S1:K,, Ss:List{K}) => S1 ~> 'ListWrap(Ss)

<k> 'ListWrap(.List{K}) => . ...</k>

[structural]

//@ \texttt{env}

//restore the env cell content from env(...) statement argument

syntax K ::= "env" "(" Map ")"

rule [env]:

<k> env(Env:Map) => . ...</k>

<env> _ => Env </env>

[structural]

rule [envDiscard]:

(env(_) => .) ~> env(_)

[structural]

//@ \section{Local Variable Declaration Statements} JLS $14.4

//@ Not only local but fields also

//local var decs and field decs are reduced to a single case

rule [LocalVarDecStmRed]:

'LocalVarDecStm('LocalVarDec(_,, TypeK:K,, 'ListWrap(Ks:List{K})))

=> 'LocalVarDec(TypeK,, 'ListWrap(Ks))

'FieldDec(_,, TypeK:K,, 'ListWrap(Ks:List{K}))

=> 'LocalVarDec(TypeK,, 'ListWrap(Ks))

'LocalVarDec(TypeK:K,, 'ListWrap(Var1:K,, Var2:K,, VarDecs:List{K}))

=> 'LocalVarDec(TypeK,, 'ListWrap(Var1))

~> 'LocalVarDec(TypeK,, 'ListWrap(Var2,, VarDecs))

'LocalVarDec(TypeK:K,, 'ListWrap('VarDec(X1:Id,,K3:K)))

=> 'LocalVarDec(TypeK,, 'ListWrap('VarDec(X1:Id)))

~> 'ExprStm('Assign('ExprName(X1),, K3))

[structural]

/*In Java current version of semantics only int and boolean primitive

types are supported*/

context 'LocalVarDec(HOLE,,_)

<k> 'LocalVarDec(T:Type,,'ListWrap('VarDec(X:Id))) => . ...</k>

<env> Env:Map => Env[L:Int/X] </env>

<store>... . => L |-> unruled(T) :: T ...</store>

<nextLoc> L:Int => L +Int 1 </nextLoc>

//@ \section{Empty statement} JLS $14.6

rule [Empty]:

'Empty(_) => .

<k> ('Labeled(X:Id,, S:K) => S ~> popx) ~> K:K </k>

<control>

<stack> . => ListItem((label, X, S, K, Env, C)) ...</stack>

C:Bag

</control>

<env> Env:Map </env>

//@ \section{Expression statements} JLS $14.8

context 'ExprStm(HOLE)

'ExprStm(_:TypedVal) => .

//@ \section{If statement}

context 'If(HOLE,,_,,_)

'If(true::bool,, S:K,, _) => S

rule [IfFalse]:

'If(false::bool,, _,, S:K) => S

'If(E:K,,S1:K) => 'If(E,,S1,,'Block('ListWrap(.List{K})))

context 'AssertStm(HOLE,,_:List{K})

rule [AssertStmTrueDiscard]:

'AssertStm(true::bool,, _:List{K}) => .

'AssertStm(false::bool) => 'AssertStm(false::bool,, ""::rtString)

context 'AssertStm(false::bool,, HOLE)

rule [AssertStm]:

'AssertStm(false::bool,, TV:TypedVal) => 'Throw('NewInstance(

'None(.List{K}),,

'ClassOrInterfaceType( 'TypeName( String2Id("AssertionError") ),, 'None(.List{K}) ),,

'ListWrap( toString(TV) ),,

'None(.List{K})

List{K} "," // switch body - list of 'SwitchGroup labels

K // DefaultStm - default block, if any

context 'Switch(HOLE,,_)

( 'Switch(TV:TypedVal,, 'SwitchBlock('ListWrap(Ks:List{K}),, TrailingLabels:K))

=> switchImpl TV, (Ks,, 'SwitchGroup(TrailingLabels,, .K)), .K )

( 'SwitchGroup('ListWrap('Case(HOLE),,_:List{K}),,_),, _:List{K} ), _

//the type associated to V and V2 is not important for match, only the value.

//JLS3 $14.11, page 377: Every case constant expression associated with

//a switch statement must be assignable (§5.2) to the type of the switch Expression.

rule [SwitchCaseNotMatch]:

switchImpl V:RawVal :: _, ( 'SwitchGroup('ListWrap(

( 'Case(V2:RawVal :: _) => .List{K} ),,

by it's block. The execution rules for switch will discard switch-related

constructs and will execute the statements. */

rule [SwitchCaseMatch]:

( switchImpl V:RawVal :: _, ('SwitchGroup('ListWrap('Case(V :: _),, _:List{K}),, S:K),,

=> 'ListWrap(S,,Ks)

rule [SwitchDefaultSave]:

switchImpl _:TypedVal, (

'SwitchGroup('ListWrap(

( 'Default(_) => .List{K} ),,

( _:K => 'ListWrap(S,, Ks) )

rule [SwitchGroupDiscard]:

switchImpl _:TypedVal, (

( 'SwitchGroup('ListWrap( .List{K} ),,_) => .List{K} ),,

_), _

rule [SwitchDefaultExec]:

switchImpl _, .List{K}, DefaultStm:K => DefaultStm

rule [SwitchGroupExec]:

'SwitchGroup(_:K,, S:K) => S

<k> ( 'While(E:K,,S:K)

=> saveLoop(loopImpl(E, S, .K), K) ~> loopImpl(E, S, .K) ~> popx )

~> K:K

</k>

[structural]

syntax K ::= "loopImpl" "("

K "," // E - test expression

K "," // S - loop body

K // UpdClause - present for For, empty for other loops.

")"

rule [loopImpl]:

<k> loopImpl(E:K, S:K, UpdClause:K)

=> 'If(E,, 'Block(S ~> UpdClause ~> loopImpl(E, S, UpdClause)),, .K)

...

</k>

[structural]

syntax K ::= "saveLoop" "("

K "," // LoopStm - the whole while / do / for statement

K // K - rest of computation

")"

rule [saveLoop]:

<k> (saveLoop(LoopStm:K, K:K) => .) ...</k>

<control>

<stack>

( . => ListItem((loop, getLoopLabel(ParentLayer), LoopStm, K, Env, C)) )

ListItem(ParentLayer:K)

...

</stack>

C:Bag

</control>

<env> Env:Map </env>

/*@ \texttt{Label propagation} through stack layers, used by

continue statement with label.*/

syntax K ::= "getLoopLabel" "(" K ")" [function]

rule getLoopLabel((label, X:Id, S:K, _,_,_:Bag)) => X

when

getKLabel(S) ==KLabel 'While

orBool getKLabel(S) ==KLabel 'DoWhile

orBool getKLabel(S) ==KLabel 'For [anywhere]

getKLabel(S) ==KLabel 'While

orBool getKLabel(S) ==KLabel 'DoWhile

orBool getKLabel(S) ==KLabel 'For

) [anywhere]

//@ \section{Do statement}

<k> ( 'DoWhile(S:K,,E:K)

stm('ListWrap(.List{K})) => .

[structural]

rule [stmList]:

stm('ListWrap(E:K,, Es:List{K})) => 'ExprStm(E) ~> stm('ListWrap(Es))

<k> stm('LocalVarDec(Ks:List{K})) => 'LocalVarDecStm('LocalVarDec(Ks)) ...</k>

[structural]

rule [ForFirstArgV1Red]:

'For((

'ListWrap(InitExps:List{K}) => stm('ListWrap(InitExps))

'For((

'LocalVarDec(Ks:List{K}) => stm('LocalVarDec(Ks))

),,_:List{K})

[structural]

rule [ForSecondArgRed]:

'For(_:K,,(

'None(.List{K}) => 'Some(true::bool)

'For(_:K,,_:K,,(

'ListWrap(UpdExps:List{K}) => stm('ListWrap(UpdExps))

),,_:K)

[structural]

//this form of resulting while is required for compatibility with continue statement

rule [For]:

<k> ( 'For(stm(InitClause:K),, 'Some(TestExp:K),, stm(UpdClause:K),, S:K)

=> saveLoop(loopImpl(TestExp, S, stm(UpdClause)), K) ~> 'Block(stm(InitClause)

<k> 'Break('None(_)) ~> _:K => K </k>

<k> 'Break('None(_)) ...</k>

<k> 'Break('Some(X:Id)) ~> _:K => K </k>

<k> 'Break('Some(X:Id)) ...</k>

<k> (. => FinallyS) ~> 'Break(_) ...</k>

<control>

<stack> ListItem((finally,_,FinallyS:K,_,Env:Map,C:Bag)) => . ...</stack>

(_ => C)

</control>

<env> _ => Env </env>

//@ \section{Continue statement}

rule [Continue]:

<k> 'Continue('None(_)) ~> _:K => UpdClause ~> loopImpl(E, S, UpdClause) ~> popx ~> K </k>

<control>

<stack>

ListItem((StackLT:StackLayerType, _, loopImpl(E:K, S:K, UpdClause:K), K:K, Env:Map, C:Bag))

...

</stack>

(_ => C)

</control>

<env> _ => Env </env>

when

StackLT ==K loop orBool StackLT ==K forBody

rule [ContinuePassThrough]:

<k> 'Continue('None(_)) ...</k>

<stack>

ListItem((StackLT:StackLayerType,_,_,_,_,_:Bag)) => .

...

</stack>

when

StackLT =/=K loop

andBool StackLT =/=K forBody

andBool StackLT =/=K finally

rule [ContinueLabel]:

<k> 'Continue('Some(X:Id)) ~> _:K => UpdClause ~> loopImpl(E, S, UpdClause) ~> popx ~> K </k>

<control>

<stack>

ListItem((StackLT:StackLayerType, X:Id, loopImpl(E:K, S:K, UpdClause:K), K:K, Env:Map, C:Bag))

...

</stack>

(_ => C)

</control>

<env> _ => Env </env>

when

StackLT ==K loop

orBool StackLT ==K forBody

rule [ContinueLabelPassThrough]:

<k> 'Continue('Some(X:Id)) ...</k>

<stack>

ListItem((StackLT:StackLayerType, StackArg2:K, _,_,_,_:Bag)) => .

...

</stack>

when

(

StackLT =/=K loop

andBool StackLT =/=K forBody

andBool StackLT =/=K finally

)

orBool (

(

StackLT ==K loop

orBool StackLT ==K forBody

)

andBool (

X =/=K StackArg2

)

)

//works for both break with and without label

rule [ContinueAnyInTryFinally]:

<k> (. => FinallyS) ~> 'Continue(_) ...</k>

context 'Return('Some(HOLE))

'Return('None(.List{K}) => 'Some(nothing :: void))

[structural]

rule [Return]:

<k>

'Return('Some(TV:TypedVal)) ~> _

=> subtype typeOf(TV), T ~> true? ~> unsafeCast(TV, T) ~> K:K

</k>

<control>

<stack> ListItem((return,_,_,K:K,Env:Map,C:Bag)) => . ...</stack>

( <return> T:Type </return> _ => C )

</control>

<env> _ => Env </env>

rule [ReturnInTryFinally]:

<k> (. => FinallyS) ~> 'Return('Some(_:TypedVal)) ...</k>

<control>

<stack> ListItem((finally,_,FinallyS:K,_,Env:Map,C:Bag)) => . ...</stack>

(_ => C)

</control>

<env> _ => Env </env>

rule [ReturnPassThrough]:

<k> 'Return('Some(_:TypedVal)) ...</k>

<stack> ListItem((StackLT:StackLayerType,_,_,_,_,_:Bag)) => . ...</stack>

when

StackLT =/=K return

andBool StackLT =/=K finally

/*@ \section{Throw statement}

Exceptions are propagated now until a catch that can bind them is

encountered. */

context 'Throw(HOLE)

(. => checkCatch(typeOf(TV), TypeK)) ~> 'Throw(TV:TypedVal)

...

</k>

<stack>

ListItem((catch, .K, 'ListWrap('Catch('Param(_:K,, TypeK:K,, _:Id),, _),, _),

checkCatch(true::bool) ~> 'Throw(TV:TypedVal) ~> _:K

=> 'Block('ListWrap('LocalVarDecStm('LocalVarDec(

'ListWrap(.List{K}),, TypeK,, 'ListWrap('VarDec(X,, TV)))),,

ListItem((catch, .K, 'ListWrap('Catch(

'Param(_:K,, TypeK:K,, X:Id),, CatchS:K),,_), K:K, Env:Map, C:Bag)) => .

...

</stack>

(_ => C)

</control>

<env> _ => Env </env>

rule [ThrowCheckedFalse]:

<k> (checkCatch(false::bool) => .) ~> 'Throw(_) ...</k>

ListItem((catch, .K, 'ListWrap(

('Catch(_) => .List{K}),,

<k> 'Throw(_:TypedVal) ...</k>

<stack>

ListItem((catch, .K, 'ListWrap(.List{K}), _,_,_)) => .

<k> (. => FinallyS) ~> 'Throw(_:TypedVal) ...</k>

<control>

<stack> ListItem((finally,_,FinallyS:K,_,Env:Map,C:Bag)) => . ...</stack>

(_ => C)

</control>

<env> _ => Env </env>

rule [ThrowPassThrough]:

<k> 'Throw(_:TypedVal) ...</k>

'Throw(TV:TypedVal) ~> _:K

=> 'ExprStm('Invoke(rtSystemOutPrintln,, 'ListWrap(

'Plus("Thread terminated with exception: "::rtString,, TV))))

</k>

<stack> .List </stack>

//@ \section{Try statement}

rule [TryCatchFinallyDesugar]:

'Try(TryS:K,, 'ListWrap(K:K,, Ks:List{K}),,FinallyS:K)

=> 'Try('Try(TryS,,'ListWrap(K,, Ks)),,'ListWrap(.List{K}),,FinallyS)

[structural]

//@ \subsection{Execution of try–catch} JLS 14.20.1

rule [TryCatch]:

<k>

( 'Try(TryS:K,, 'ListWrap(Ks:List{K}))

=> TryS ~> popx )

~> K

</k>

<control>

<stack> . => ListItem((catch, .K, 'ListWrap(Ks), K:K, Env:Map, C:Bag)) ...</stack>

'Try(TryS:K ,,'ListWrap(.List{K}),,FinallyS:K)