diff --git a/.gitignore b/.gitignore index ab6482c7..2652bcc7 100644 --- a/.gitignore +++ b/.gitignore @@ -33,6 +33,9 @@ /src/.latex /src/.modules /src/sty/.project +/src/sty/.texlipse /src/sty/*.pdf /src/sty/*.synctex /src/sty/.latex +/src/exec/java-exec-kompiled-bk +/src/prep/java-prep-kompiled-bk diff --git a/src/common/aux-strings.k b/src/common/aux-strings.k index 9e1f94c4..ff7caf9b 100644 --- a/src/common/aux-strings.k +++ b/src/common/aux-strings.k @@ -1,5 +1,5 @@ module AUX-STRINGS -/*@ Auxiliary constructs related to Strings. Extension to string.k.*/ +/*@ Utility functions for string manipulation. No dependencies on other K-Java modules. Extension to string.k.*/ //@Retain the first Count chars in the string syntax KItem ::= retainHead ( String, Int ) [function] diff --git a/src/common/class-syntax.k b/src/common/class-syntax.k index 582256a7..611f488c 100644 --- a/src/common/class-syntax.k +++ b/src/common/class-syntax.k @@ -1,7 +1,7 @@ module CLASS-SYNTAX imports EXP-SYNTAX -//@ \subsection{ClassDeclarations.sdf} +//@ \subsubsection{ClassDeclarations} syntax ClassDecHead ::= AnnoClassModList "class" Id OptionalTypeParams OptionalSuper OptionalInterfaces [klabel('ClassDecHead)] @@ -34,7 +34,7 @@ syntax InterfaceDec syntax SemiColon ::= ";" [klabel('SemiColon)] -//@ \subsection{ConstructorDeclarations.sdf} +//@ \subsubsection{ConstructorDeclarations} syntax ConstrHead ::= AnnoConstrModList OptionalTypeParams Type Id "(" Params ")" OptionalThrows [klabel('ConstrDecHead)] @@ -53,7 +53,7 @@ syntax ConstrMod ::= Public syntax AnnoConstrMod ::= Anno | ConstrMod -//@ \subsection{EnumDeclarations.sdf} +//@ \subsubsection{EnumDeclarations} syntax EnumDecHead ::= AnnoClassModList "enum" Id OptionalInterfaces [klabel('EnumDecHead)] /* Java allows , at the end of List. @@ -71,7 +71,7 @@ syntax EnumConstArgs ::= "(" Exps ")" [bracket syntax EnumBodyDecs ::= ";" ClassBodyDecList [klabel('EnumBodyDecs)] -//@ \subsection{FieldDeclarations.sdf} +//@ \subsubsection{FieldDeclarations} syntax FieldDec ::= AnnoFieldModList Type VarDecList ";" [klabel('FieldDec)] syntax VarDec ::= VarDecId [klabel('VarDec)] @@ -92,7 +92,7 @@ syntax FieldMod ::= Public syntax AnnoFieldMod ::= Anno | FieldMod -//@ \subsection{MethodDeclarations.sdf} +//@ \subsubsection{MethodDeclarations} syntax MethodDecHead ::= AnnoMethodModList OptionalTypeParams Type Id "(" Params ")" OptionalThrows [klabel('MethodDecHead)] @@ -123,11 +123,11 @@ syntax VarMod ::= Final syntax AnnoVarMod ::= Anno | VarMod -//@ \subsection{InstanceInitializers.sdf} +//@ \subsubsection{InstanceInitializers} syntax InstanceInit ::= Block [klabel('InstanceInit)] -//@ \subsection{StaticInitializers.sdf} +//@ \subsubsection{StaticInitializers} syntax StaticInit ::= "static" Block [klabel('StaticInit)] syntax Block diff --git a/src/common/core-classes.k b/src/common/core-classes.k index f3ffc204..4d562b1e 100644 --- a/src/common/core-classes.k +++ b/src/common/core-classes.k @@ -5,27 +5,29 @@ module CORE-CLASSES imports EXP-SYNTAX //for definitions of sort Exp imports STMT-SYNTAX //for definitions of sort Stmt -/*@ Auxiliary functions related to classes and packages. +/*@ This module is a collection of auxiliary functions related to classes and packages. */ -//@ \subsection{Shortcuts for the most frequently used classes within the semantics} +//@ \subsection{Shortcuts for frequently used classes} + +//@Shortcuts for the most frequently used classes that need special treatment within the semantics. syntax KItem ::= "classObject" - [function, latex(\terminal{Object})] + [function, latex(\terminal{class} \terminal{Object} )] rule classObject => class String2Id("java.lang.Object") syntax KItem ::= "classString" - [function, latex(\terminal{String})] + [function, latex(\terminal{class} \terminal{String} )] rule classString => class String2Id("java.lang.String") syntax KItem ::= "classNullPointerException" - [function, latex(\terminal{NullPointerException})] + [function, latex(\terminal{class} \terminal{NullPointerException} )] rule classNullPointerException => class String2Id("java.lang.NullPointerException") syntax KItem ::= "classArrayImpl" [function] rule classArrayImpl => class String2Id("java.lang.ArrayImpl") -//@ \subsection{Packages} +//@ \subsection{Auxiliary functions for packages} /*@A Java package.*/ syntax PackageId ::= packageId ( Id ) @@ -45,7 +47,7 @@ rule getPackage(class ClassId:Id) rfindString(Id2String(ClassId), ".", lengthString(Id2String(ClassId))) )) ) -//@ \subsection{Classes} +//@ \subsection{Auxiliary functions for classes} //@ Converts a pair of PackagId, Id into a fully qualified class name syntax ClassType ::= getClassType ( @@ -77,7 +79,7 @@ rule [getTopLevel]: Class noClass -//@ Restore the content of with the given class +//@ Restore the content of \verb|| with the given class syntax KItem ::= restoreCrntClass ( ClassType //old content of ) @@ -90,42 +92,4 @@ rule [restoreAfterProcessLocalClass]: syntax KItem ::= getConsName ( ClassType ) [function] rule getConsName(class ClassId:Id) => String2Id("$cons$" +String Id2String(ClassId)) -//@ \subsection{Expressions and their subsorts} -syntax Exp ::= NonNumericExp -syntax NonNumericExp ::= "dummyNonNumericExp" - -rule isNonNumericExp('ArrayAccess(_)) => true -rule isNonNumericExp('NewInstance(_)) => true // also in customElabChildren -rule isNonNumericExp('QNewInstance(_)) => true // also in customElabChildren -rule isNonNumericExp('InstanceOf(_)) => true -rule isNonNumericExp('Invoke(_)) => true -rule isNonNumericExp('This(_)) => true -rule isNonNumericExp('QThis(_)) => true -rule isNonNumericExp('AmbName(_)) => true -rule isNonNumericExp('ExprName(_)) => true -rule isNonNumericExp('Field(_)) => true -rule isNonNumericExp('SuperField(_)) => true -rule isNonNumericExp('QSuperField(_)) => true -rule isNonNumericExp('NewArray(_)) => true -rule isNonNumericExp('CastPrim(_)) => true -rule isNonNumericExp('CastRef(_)) => true - - -//@ Since RawVal terms can easily be converted into TypedVal, they are also of sort Exp. -syntax Exp ::= TypedVal | RawVal - -//@ \subsubsection{Computation terms produced during elaboration} - -/*@ These auxiliary terms functions that should be threated as expressions in the elaboration phase. -*/ -syntax Exp ::= AuxTermExp -syntax LHS ::= AuxTermExp -/*@ Wrapper of a statement followed by an expression, to be used in a place where an expression is expected, -such as an anonymous class declaration. Is typed with the type of the expression. -At runtime is rewritten into the statement, that should evaluate into .K, followed by the expression, -that should evaluate to value.*/ -syntax AuxTermExp ::= stmtAndExp ( K, K ) - -syntax AuxTermExp ::= cast ( Type, K ) [strict] //strictness on 1-st arcument - for runtime produced terms - endmodule diff --git a/src/common/core-functions.k b/src/common/core-functions.k index b6e012bf..b55d6930 100644 --- a/src/common/core-functions.k +++ b/src/common/core-functions.k @@ -2,8 +2,10 @@ module CORE-FUNCTIONS imports CORE-SORTS imports CORE-CLASSES +//@ \subsection{Core utility functions} + /*@ Returns the type associated with various K terms. The implementation is scattered among various K files. - For a type - the type itself. For a typed expression - the type component. For some raw values - their most common + For a type --- the type itself. For a typed expression - the type component. For some raw values - their most common type. */ syntax KItem ::= typeOf ( K ) [function] @@ -14,10 +16,10 @@ rule typeOf(null) => nullType rule typeOf(objectRef(_, Class:ClassType)) => Class rule typeOf(arrayRef( arrayOf T:Type, _, _)) => arrayOf T -/* Required by getTypes in elaboration phase, invoked by lookupMethod. */ +/*@ Required by \verb|getTypes()| in elaboration phase, invoked by \verb|lookupMethod()|. */ rule typeOf(cast(T:Type, _)) => T -// Required for getTypes() +//@ Required for \verb|getTypes()| rule typeOf('Param(_:K,, T:Type,, _:Id)) => T /*@The default value for all types. Used for field initializers.*/ @@ -60,7 +62,7 @@ rule getTypes([Ts:KList]) => types(Ts) when isKResult(Ts) -//@ \subsubsection{Other auxiliary constructs} +//@ \subsection{Utilities for general-purpose programming} /*@ Generalized equality with strictness, suitable to compare not only TypedVal-s but any K terms. */ @@ -90,7 +92,7 @@ rule plusAux(Str1:String :: _, Str2:String :: _) => (Str1 +String Str2) :: class */ syntax KResult ::= mapWrap ( Map ) -/*@ The union of two maps. Arguments are of the form mapWrap(Map). In this operation, elements of the second map +/*@ The union of two maps. Arguments are of the form \verb|mapWrap(Map)|. In this operation, elements of the second map overwrite elements of the first map if they collide. */ syntax KItem ::= mapUnion ( @@ -123,7 +125,7 @@ rule isEmpty(.Map) => true /*@A wrapper for sets, similar to the one for maps.*/ syntax KResult ::= setWrap ( Set ) -/*The union of two sets. Arguments are of the form setWrap(Set).*/ +/*@ The union of two sets. Arguments are of the form \verb|setWrap(Set)|.*/ syntax KItem ::= setUnion ( K, //setWrap(Set) K //setWrap(Set) @@ -154,24 +156,7 @@ rule length([Ks:KList]) => length(0, [Ks]) rule length(I:Int, [K:K,, Ks:KList]) => length(I +Int 1, [Ks]) rule length(I:Int, [.KList]) => I -/*@ \subsection{ClassType functions} */ - -//@ Converts a fully qualified class type into a simple name (Id) -syntax KItem ::= getSimpleName ( ClassType ) [function] -rule getSimpleName(class ClassId:Id) - => String2Id(trimHead( - Id2String(ClassId), - rfindString(Id2String(ClassId), ".", lengthString(Id2String(ClassId))) +Int 1 - )) - -/*@ \subsection{Identifiers}*/ - -// 'Id(Str:String) - -/*@Convert the AST representation of an Id into a K Id.*/ -rule 'Id(Str:String) => String2Id(Str) [structural, anywhere] - -/*@ \subsection{Other auxiliary constructs} */ +/*@ \subsubsection{Other auxiliary constructs} */ /*@ \texttt{Generic guard.} A generic computational guard (should be builtin): it allows the computation to continue only if a prefix @@ -180,20 +165,14 @@ rule 'Id(Str:String) => String2Id(Str) [structural, anywhere] syntax KItem ::= "true?" rule true::bool ~> true? => . [structural] -//@ \subsection{Definition-wide rules} - -/*@ Represent a parser form for a sequence of terms. Is desugared into the pretty form [...]*/ -syntax KLabel ::= "'ListWrap" -rule 'ListWrap(Ks:KList) => [Ks] [structural, anywhere] -//todo: both 'KListWrap and 'ListWrap are associted with the same production, so how to get rid of it -syntax KListWrap ::= "[" KList "]" [klabel('KListWrap), latex(\terminal{[} {#1} \terminal{]})] - -//@ Sequence of terms and of any other statements. The first term is moved to the top of computation. -rule [S1:K,, Stmts:KList] => S1 ~> [Stmts] [structural] -rule [.KList] => .K [structural] +/*@ \subsection{ClassType functions} */ -//@ A wrapper over an arbitrary KList, wrapper being of type KResult. -syntax KRListWrap ::= "kr" "[" KList "]" [latex(\terminal{kr[} {#1} \terminal{]})] -syntax KResult ::= KRListWrap +//@ Converts a fully qualified class type into a simple name (Id) +syntax KItem ::= getSimpleName ( ClassType ) [function] +rule getSimpleName(class ClassId:Id) + => String2Id(trimHead( + Id2String(ClassId), + rfindString(Id2String(ClassId), ".", lengthString(Id2String(ClassId))) +Int 1 + )) endmodule diff --git a/src/common/core-sorts.k b/src/common/core-sorts.k index fb8dca26..84d351af 100644 --- a/src/common/core-sorts.k +++ b/src/common/core-sorts.k @@ -7,6 +7,12 @@ module CORE-SORTS imports LEXICAL-SYNTAX imports LITERAL-SYNTAX +/*@This module contains general-purpose utilities for the whole K-Java, both preprocessing and execution. + This is the lowest-level module of the whole semantics, imported by almost all other modules. + Because if its high accessibility status, it was somewhat abused, in a sense that I placed here some random + stuff for the lack of better place. +*/ + //@ \subsection{Computation phases} /*@ The computation Global Phase. See configuration documentation for details. @@ -92,20 +98,9 @@ syntax StaticInitStatus ::= "StaticUninitialized" | StaticInitializing ( Int ) | "StaticInitialized" - -/*@ A method signature. Required to be KResult by rules in METHOD-INVOKE.*/ -syntax Signature ::= sig ( Id, Types ) -syntax KResult ::= Signature - - -/*@ The member accessibility context of the current method - either static or instance.*/ -syntax ContextType ::= "staticCT" [latex(\terminal{static})] - | "instanceCT" [latex(\terminal{instance})] -syntax KResult ::= ContextType - //@ \subsection{Values} -/* Represents a java value. May be either primitive - int, float, bool, of reference. The values nothing and undefined +/* Represents a Java value. May be either primitive --- int, float, bool, of reference. The values nothing and undefined are special cases required by the semantics. The value nothing is associated with the return type void. The value undefined is the initial value of uninitialized local variables, before the first assignment. */ @@ -113,13 +108,13 @@ syntax RawVal ::= Int | Float | Bool | RawRefVal | "nothing" | "undefined" [latex(\bot)] -/*@ A reference value, in its four forms - as regular object, array, null or String. As mentioned previously +/*@ A reference value, in its four forms --- as regular object, array, null or String. As mentioned previously String values have special treatment in this semantics and are implemented as regular strings. The object closure has the following structure: \begin{itemize} -\item OL:Int -- the object location -\item List -- the object content, of the form +\item OL:Int --- the object location +\item List --- the object content, of the form \begin{verbatim} ListItem(layer( Class, @@ -138,9 +133,9 @@ syntax ObjectRef ::= objectRef ( /*@ The arrayRef has the following structure: \begin{itemize} -\item Type -- type of the array -\item Int -- location of the first element -\item Int -- array length +\item Type --- type of the array +\item Int --- location of the first element +\item Int --- array length \end{itemize} */ syntax ArrayRef ::= arrayRef ( @@ -156,11 +151,28 @@ syntax RawRefVal ::= ObjectRef | ArrayRef | String | NullLiteral */ syntax TypedVal ::= RawVal "::" Type +//@ Since RawVal terms can easily be converted into TypedVal, they are also of sort Exp. +syntax Exp ::= TypedVal | RawVal + /*@ The three most common forms of computation result are Typed value or Type. Those are most common results we will encounter during elaboration. Other result types are more context-specific. */ syntax KResult ::= TypedVal | Type +syntax KResult ::= "noValue" [latex(\dotCt{K} )] + +//@ \subsection{Class and member attributes} + +/*@ A method signature. Required to be KResult by rules in METHOD-INVOKE.*/ +syntax Signature ::= sig ( Id, Types ) +syntax KResult ::= Signature + + +/*@ The member accessibility context of the current method --- either static or instance.*/ +syntax ContextType ::= "staticCT" [latex(\terminal{static} )] + | "instanceCT" [latex(\terminal{instance} )] +syntax KResult ::= ContextType + /*@ Member access modes*/ syntax AccessMode ::= Public | Protected | Private | "package" syntax KResult ::= AccessMode @@ -169,10 +181,10 @@ syntax KResult ::= AccessMode syntax MethodMetaType ::= "methodMMT" | "constructorMMT" /*@ The two possibilities for a type represented by an objectRef: class or interface.*/ -syntax ClassMetaType ::= "classCMT" [latex(\terminal{class})] - | "interfaceCMT" [latex(\terminal{interface})] +syntax ClassMetaType ::= "classCMT" [latex(\terminal{class} )] + | "interfaceCMT" [latex(\terminal{interface} )] -syntax KResult ::= "noValue" [latex({\dotCt{K}})] +//@ \subsection{Misc definitions} /*@ Represents a reference to a method or constructor. */ syntax MethodRef ::= methodRef( @@ -180,7 +192,7 @@ syntax MethodRef ::= methodRef( RefType //Usually Class - class defining the method // Could also be array type, because we may invoke methods over arrays. ) - | "noMethodRef" [latex({\dotCt{K}})] + | "noMethodRef" [latex(\dotCt{K} )] syntax KResult ::= MethodRef syntax MethodName ::= MethodRef @@ -190,7 +202,7 @@ syntax Types ::= types ( ) syntax KResult ::= Types -//Location type of each store location - either local variable or field +//@Location type of each store location --- either local variable or field syntax LocMetadata ::= "LocalLocMetadata" [latex(\terminal{Local})] | "FieldLocMetadata" [latex(\terminal{Field})] @@ -203,7 +215,12 @@ syntax ClassInstanceCreationExp ::= "new" ClassType "(" Exps ")" //Denis' syntax syntax ClassOrName ::= Id | ClassType //Denis' syntax -syntax ClassType ::= "class" Id | "noClass" [latex({\dotCt{K}})] + +/*@ A fully qualified class name, or noClass where no valid class exists in the current context.*/ +syntax ClassType ::= "class" Id | "noClass" [latex(\dotCt{K} )] + +/*@ \subsection{Random unsorted content, syntax converters}*/ + //Denis' syntax syntax Param ::= Type Id [klabel('ParamImpl)] @@ -216,4 +233,38 @@ syntax RefType ::= ClassType | "nullType" | "arrayOf" Type rule 'ArrayType(T:Type) => arrayOf T [anywhere] rule 'ClassOrInterfaceType(TypeK:K,, _) => TypeK [anywhere] + +/*@Convert the AST representation of an Id into a K Id.*/ +rule 'Id(Str:String) => String2Id(Str) [structural, anywhere] + +//@ \subsubsection{ListWrap and KListWrap} + +/*@ Represent a parser form for a sequence of terms. Is desugared into the pretty form [...]*/ +syntax KLabel ::= "'ListWrap" +rule 'ListWrap(Ks:KList) => [Ks] [structural, anywhere] +//todo: both 'KListWrap and 'ListWrap are associted with the same production, so how to get rid of it +syntax KListWrap ::= "[" KList "]" [klabel('KListWrap), latex(\terminal{[} {#1}\terminal{]} )] + +//@ Sequence of terms and of any other statements. The first term is moved to the top of computation. +rule [S1:K,, Stmts:KList] => S1 ~> [Stmts] [structural] +rule [.KList] => .K [structural] + +//@ A wrapper over an arbitrary KList, wrapper being of type KResult. +syntax KRListWrap ::= "kr" "[" KList "]" [latex(\terminal{kr[} {#1}\terminal{]} )] +syntax KResult ::= KRListWrap + +//@ \subsubsection{Computation terms produced during elaboration} + +/*@ These auxiliary terms functions that should be threated as expressions in the elaboration phase. +*/ +syntax Exp ::= AuxTermExp +syntax LHS ::= AuxTermExp +/*@ Wrapper of a statement followed by an expression, to be used in a place where an expression is expected, +such as an anonymous class declaration. Is typed with the type of the expression. +At runtime is rewritten into the statement, that should evaluate into .K, followed by the expression, +that should evaluate to value.*/ +syntax AuxTermExp ::= stmtAndExp ( K, K ) + +syntax AuxTermExp ::= cast ( Type, K ) [strict] //strictness on 1-st arcument - for runtime produced terms + endmodule diff --git a/src/common/exp-syntax.k b/src/common/exp-syntax.k index e9aeaaa9..03166469 100644 --- a/src/common/exp-syntax.k +++ b/src/common/exp-syntax.k @@ -1,11 +1,10 @@ module EXP-SYNTAX imports TYPE-SYNTAX - imports SHARED-SYNTAX syntax Exp ::= StmtExp syntax StmtExp ::= PrefixPostfixExp | AssignExp | MethodInvokeExp | ClassInstanceCreationExp -//@ \subsection{MethodInvocation.sdf} +//@ \subsubsection{MethodInvocation} syntax MethodInvokeExp ::= MethodSpec "(" Exps ")" [klabel('Invoke)] syntax MethodSpec ::= MethodName [klabel('Method)] | Exp "." OptionalTypeArgs Id [klabel('Method)] @@ -14,7 +13,7 @@ syntax MethodSpec ::= MethodName [klabel( | AmbName "." TypeArgs Id [klabel('GenericMethod)] -//@ \subsection{ClassInstanceCreation.sdf} +//@ \subsubsection{ClassInstanceCreation} syntax ClassInstanceCreationExp ::= "new" OptionalTypeArgs ClassOrInterfaceType "(" Exps ")" OptionalClassBody [klabel('NewInstance)] @@ -23,8 +22,9 @@ syntax ClassInstanceCreationExp ::= [klabel('QNewInstance)] -//@ \subsection{AssignmentOperators.sdf} +//@ \subsubsection{AssignmentOperators} syntax LHS ::= ExprName | FieldAccess | ArrayAccess +syntax Exp ::= LHS syntax AssignExp ::= LHS "=" Exp [klabel('Assign)] syntax AssignExp ::= CompoundAssignExp @@ -42,7 +42,7 @@ syntax CompoundAssignExp ::= LHS "*=" Exp [klabel(' | LHS "|=" Exp [klabel('AssignOr)] -//@ \subsection{UnaryOperators.sdf} +//@ \subsubsection{UnaryOperators} syntax Exp ::= "(" PrimType ")" Exp [klabel('CastPrim)] syntax Exp ::= "(" RefType ")" Exp [klabel('CastRef)] @@ -51,17 +51,16 @@ syntax Exp ::= "~" Exp [strict, klabel('Complement)] | "+" Exp [strict, klabel('Plus)] | "-" Exp [strict, klabel('Minus)] -//@ Operators with side effects - prefix, postfix ++/-- syntax PrefixPostfixExp ::= "++" Exp [klabel('PreIncr)] | "--" Exp [klabel('PreDecr)] -//@ \subsection{Postfix.sdf} +//@ \subsubsection{Postfix} syntax PrefixPostfixExp ::= Exp "++" [klabel('PostIncr)] | Exp "--" [klabel('PostDecr)] -//@ \subsection{BinaryOperators.sdf} +//@ \subsubsection{BinaryOperators} syntax Exp ::= Exp "*" Exp [seqstrict, klabel('Mul)] | Exp "/" Exp [seqstrict, klabel('Div)] | Exp "%" Exp [seqstrict, klabel('Remain)] @@ -87,20 +86,18 @@ syntax Exp ::= Exp "?" Exp ":" Exp [klabel('Cond)] syntax Exp ::= Exp "instanceof" RefType [strict, klabel('InstanceOf)] -//@ \subsection{FieldAccess.sdf} -syntax Exp ::= FieldAccess +//@ \subsubsection{FieldAccess} syntax FieldAccess ::= Exp "." Id [klabel('Field)] | "super" "." Id [klabel('SuperField)] | TypeName "." "super" "." Id [klabel('QSuperField)] -//@ \subsection{ArrayAccess.sdf} -syntax Exp ::= ArrayAccess +//@ \subsubsection{ArrayAccess} //syntax ArraySubscript ::= "[" Exp "]" [bracket] syntax ArrayAccess ::= Exp "[" Exp "]" [seqstrict, klabel('ArrayAccess)] -//@ \subsection{ArrayCreation.sdf} +//@ \subsubsection{ArrayCreation} /* Either 'NewArray( T:ElemType,, ['Dim(N1),,'Dim('N2),, ...],, [...,, 'Dim(.KList),, ...] ) Or 'NewArray( T:ElemType,, [...,, 'Dim(.KList),, ...],, 'ArrayInit(_) ) */ @@ -118,12 +115,12 @@ syntax Dim ::= "[" "]" [klabel('Dim syntax DimExp ::= "[" Exp "]" [strict, hybrid, klabel('Dim)] -//@ \subsection{ArrayInitializers.sdf} +//@ \subsubsection{ArrayInitializers} syntax ArrayInit ::= "{" VarInits "}" [klabel('ArrayInit)] syntax ArrayInit ::= "{" VarInits "," "}" [klabel('ArrayInit)] -//@ \subsection{Primary.sdf} +//@ \subsubsection{Primary} syntax Exp ::= Literal [klabel('Lit)] syntax Literal ::= IntLiteral | FloatLiteral @@ -141,4 +138,11 @@ syntax Exp ::= "this" [klabel('Thi syntax Exp ::= "(" Exp ")" [bracket] +/*previously defined elsewhere for ltl-support, now these syntax are also used for Java, +although we don't incorporate ltl for now, let's keep this independent like this +*/ +syntax Exp ::= Exp "<=" Exp [seqstrict, klabel('LtEq)] + | Exp "==" Exp [seqstrict, klabel('Eq)] + | Exp "!=" Exp [klabel('NotEq)] + endmodule diff --git a/src/common/interface-syntax.k b/src/common/interface-syntax.k index a8de4608..e8ed32ed 100644 --- a/src/common/interface-syntax.k +++ b/src/common/interface-syntax.k @@ -1,7 +1,7 @@ module INTERFACE-SYNTAX imports CLASS-SYNTAX -//@ \subsection{AbstractMethodDeclarations.sdf} +//@ \subsubsection{AbstractMethodDeclarations} syntax AbstractMethodDec ::= AnnoAbstractMethodModList OptionalTypeParams Type Id "(" Params ")" OptionalThrows ";" [klabel('AbstractMethodDec)] @@ -10,7 +10,7 @@ syntax AbstractMethodMod ::= Public | Abstract syntax AnnoAbstractMethodMod ::= Anno | AbstractMethodMod -//@ \subsection{Annotations.sdf} +//@ \subsubsection{Annotations} syntax Anno ::= "@" TypeName "(" ElemValPairList ")" [klabel('Anno)] | "@" TypeName "(" ElemVal ")" [klabel('SingleElemAnno)] | "@" TypeName [klabel('MarkerAnno)] @@ -23,7 +23,7 @@ syntax ElemVal ::= Exp syntax ElemValPair ::= Id "=" ElemVal [klabel('ElemValPair)] -//@ \subsection{AnnotationTypes.sdf} +//@ \subsubsection{AnnotationTypes} syntax AnnoDecHead ::= AnnoInterfaceModList "@" "interface" Id [klabel('AnnoDecHead)] syntax AnnoDec ::= AnnoDecHead "{" AnnoElemDecList "}" [klabel('AnnoDec)] @@ -35,7 +35,7 @@ syntax AnnoElemDec ::= AbstractMethodModList Type Id "(" ")" OptionalDefaultVal syntax DefaultVal ::= "default" ElemVal [klabel('DefaultVal)] -//@ \subsection{ConstantDeclarations.sdf} +//@ \subsubsection{ConstantDeclarations} syntax ConstantDec ::= AnnoConstantModList Type VarDecList ";" [klabel('ConstantDec)] syntax ConstantMod ::= Public @@ -45,7 +45,7 @@ syntax ConstantMod ::= Public syntax AnnoConstantMod ::= Anno | ConstantMod -//@ \subsection{InterfaceDeclarations.sdf} +//@ \subsubsection{InterfaceDeclarations} syntax InterfaceDecHead ::= AnnoInterfaceModList "interface" Id OptionalTypeParams OptionalExtendsInterfaces [klabel('InterfaceDecHead)] diff --git a/src/common/java-syntax.k b/src/common/java-syntax.k index d511c216..c493aeac 100644 --- a/src/common/java-syntax.k +++ b/src/common/java-syntax.k @@ -9,7 +9,7 @@ require "interface-syntax.k" require "package-syntax.k" require "optional-syntax.k" require "type-syntax.k" -require "shared-syntax.k" + module JAVA-SYNTAX imports LIST-SYNTAX imports STMT-SYNTAX @@ -22,5 +22,4 @@ module JAVA-SYNTAX imports PACKAGE-SYNTAX imports OPTIONAL-SYNTAX imports TYPE-SYNTAX - imports SHARED-SYNTAX endmodule diff --git a/src/common/lexical-syntax.k b/src/common/lexical-syntax.k index 21c813b7..3cfd7254 100644 --- a/src/common/lexical-syntax.k +++ b/src/common/lexical-syntax.k @@ -1,75 +1,16 @@ module LEXICAL-SYNTAX -//@ \subsection{Comments.sdf} -//no need to define because K provides fixed layout -//@ \subsection{Identifiers.sdf} +//@ \subsubsection{Identifiers} syntax Id ::= ID [klabel('Id)] syntax ID ::= Token{[A-Za-z\_\$][A-Za-z0-9\_\$]*} [onlyLabel] -//@ \subsection{KeyWord.sdf(not needed?)} -/* -syntax Keyword ::= "abstract" - | "assert" - | "boolean" - | "break" - | "byte" - | "case" - | "catch" - | "char" - | "class" - | "const" - | "continue" - | "default" - | "do" - | "double" - | "else" - | "enum" - | "extends" - | "final" - | "finally" - | "float" - | "for" - | "goto" - | "if" - | "implements" - | "import" - | "instanceof" - | "int" - | "interface" - | "long" - | "native" - | "new" - | "package" - | "private" - | "protected" - | "public" - | "return" - | "short" - | "static" - | "strictfp" - | "super" - | "switch" - | "synchronized" - | "this" - | "throw" - | "throws" - | "transient" - | "try" - | "void" - | "volatile" - | "while" -*/ +//@ \subsubsection{LineTerminators} -//@ \subsection{LineTerminators.sdf} -syntax EndOfFile -syntax CarriageReturn ::= Token{[\r]} [onlyLabel] -syntax LineTerminator ::= EndOfFile - | CarriageReturn +syntax LineTerminator ::= Token{[\r]} [onlyLabel] | Token{[\n]} [onlyLabel] | Token{[\r][\n]} [onlyLabel] - -//@ \subsection{Modifiers.sdf} +//@ \subsubsection{Modifiers} syntax Public ::= "public" [klabel('Public)] syntax Private ::= "private" [klabel('Private)] syntax Protected ::= "protected" [klabel('Protected)] @@ -82,22 +23,4 @@ syntax Volatile ::= "volatile" [klabel('Volatile)] syntax StrictFP ::= "strictfp" [klabel('StrictFP)] syntax Synchronized ::= "synchronized" [klabel('Synchronized)] -syntax Modifier ::= Public - | Private - | Protected - | Abstract - | Final - | Static - | Native - | Transient - | Volatile - | StrictFP - | Synchronized - -//@ \subsection{UnicodeEscape.sdf} -syntax UnicodeEscape ::= Token {[\\][u]+ [0-9a-fA-F][0-9a-fA-F][0-9a-fA-F][0-9a-fA-F]} - [onlyLabel, klabel('UnicodeEscape)] - -//@ \subsection{WhiteSpace.sdf} -//no need to define because K provides fixed layout -endmodule \ No newline at end of file +endmodule diff --git a/src/common/literal-syntax.k b/src/common/literal-syntax.k index 0cf2e03e..36d3424c 100644 --- a/src/common/literal-syntax.k +++ b/src/common/literal-syntax.k @@ -2,23 +2,22 @@ module LITERAL-SYNTAX imports LEXICAL-SYNTAX imports LIST-SYNTAX -//@ \subsection{BooleanLiterals.sdf} +//@ \subsubsection{BooleanLiterals} syntax BoolLiteral ::= Boolean [klabel('Bool)] syntax Boolean ::= "true" [onlyLabel, klabel('True)] syntax Boolean ::= "false" [onlyLabel, klabel('False)] -//@ \subsection{CharacterLiterals.sdf} todo -syntax SingleChar// ::= Token{[\r\n\'\\]}//don't understand ^? +//@ \subsubsection{CharacterLiterals} syntax CharContent ::= SingleChar [klabel('Single)] | UnicodeEscape | EscapeSeq -//Problem: Multiple lookahead not fully supported (does not appear when tested in small language) -syntax CharLiteral //::= "'" CharContent "'" [klabel('Char)] +syntax SingleChar +syntax CharLiteral //::= "'" CharContent "'" [klabel('Char)] -//@ \subsection{EscapeSequences.sdf} +//@ \subsubsection{EscapeSequences} syntax EscapeSeq ::= OctaEscape | NamedEscape syntax NamedEscape ::= Token{"\\" [btnfr\"\'\\]} [onlyLabel, klabel('NamedEscape)] @@ -28,11 +27,11 @@ syntax OctaEscape ::= Token{"\\" [0-7]} [onlyLabel, klabel('Oct | Token{"\\" [0-3][0-7][0-7]} [onlyLabel, klabel('OctaEscape3)] -//@ \subsection{FloatingPointLiterals.sdf} todo +//@ \subsubsection{FloatingPointLiterals} syntax FloatLiteral ::= Float [klabel('Float)] -//@ \subsection{IntegerLiterals.sdf} +//@ \subsubsection{IntegerLiterals} syntax DeciLiteral ::= Token{[1-9][0-9]* [lL]?} [onlyLabel] syntax HexaLiteral ::= Token{[0][xX][0-9a-fA-F]+ [lL]?} [onlyLabel] syntax OctaLiteral ::= Token{[0][0-7]+ [lL]?} [onlyLabel] @@ -42,11 +41,11 @@ syntax IntLiteral ::= DeciLiteral [klabel('Deci)] | OctaLiteral [klabel('Octa)] -//@ \subsection{NullLiteral.sdf} +//@ \subsubsection{NullLiteral} syntax NullLiteral ::= "null" [klabel('Null)] -//@ \subsection{StringLiterals.sdf} todo +//@ \subsubsection{StringLiterals} syntax StringLiteral ::= "\"" StringPartList "\"" [klabel('String)] syntax StringPart ::= StringChars [klabel('Chars)] @@ -55,4 +54,8 @@ syntax StringPart ::= StringChars [klabel('Chars)] syntax StringChars //::= Token {~[\"\\\n\13]} -endmodule \ No newline at end of file + +syntax UnicodeEscape ::= Token {[\\][u]+ [0-9a-fA-F][0-9a-fA-F][0-9a-fA-F][0-9a-fA-F]} + [onlyLabel, klabel('UnicodeEscape)] + +endmodule diff --git a/src/common/package-syntax.k b/src/common/package-syntax.k index ce487e9b..71acf3aa 100644 --- a/src/common/package-syntax.k +++ b/src/common/package-syntax.k @@ -1,19 +1,15 @@ module PACKAGE-SYNTAX imports CLASS-SYNTAX -//@ \subsection{CompilationUnits.sdf} syntax CompilationUnit ::= OptionalPackageDec ImportDecList TypeDecList [klabel('CompilationUnit)] -//@ \subsection{TypeDeclarations.sdf} syntax TypeDec ::= ClassDec | InterfaceDec | SemiColon -//@ \subsection{ImportDeclarations.sdf} syntax ImportDec ::= "import" TypeName ";" [klabel('TypeImportDec)] | "import" PackageName "." "*" ";" [klabel('TypeImportOnDemandDec)] | "import" "static" TypeName "." Id ";" [klabel('StaticImportDec)] | "import" "static" TypeName "." "*" ";" [klabel('StaticImportOnDemandDec)] -//@ \subsection{PackageDeclarations.sdf} syntax PackageDec ::= AnnoList "package" PackageName ";" [klabel('PackageDec)] -endmodule \ No newline at end of file +endmodule diff --git a/src/common/primitive-types.k b/src/common/primitive-types.k index 181742d2..183f30bf 100644 --- a/src/common/primitive-types.k +++ b/src/common/primitive-types.k @@ -2,7 +2,7 @@ module PRIMITIVE-TYPES imports CORE-SORTS imports SUBTYPING -//@ \subsection{Integer types normalization} +//@ \subsection{Integer value normalization} syntax Int ::= bitCount ( Type ) [function] rule bitCount(byte) => 8 @@ -11,7 +11,7 @@ rule bitCount(int) => 32 rule bitCount(long) => 64 rule bitCount(char) => 16 -/*@ Symbolic execution limitation: this construct cannot be [function] +/* Symbolic execution limitation: this construct cannot be [function] When conditionals are needed, implementation have to use 'If - the symbolically processed version of if. */ syntax KItem ::= normalize ( TypedVal ) @@ -56,7 +56,7 @@ rule normalizeImpl(I:Int :: T:Type) +Int (1 < ILT diff --git a/src/common/shared-syntax.k b/src/common/shared-syntax.k deleted file mode 100644 index dddcb088..00000000 --- a/src/common/shared-syntax.k +++ /dev/null @@ -1,9 +0,0 @@ -module SHARED-SYNTAX -/*previously defined elsewhere for ltl-support, now these syntax are also used for java, -although we don't incorporate ltl for now, let's keep this independent like this -*/ -syntax Exp ::= Exp "<=" Exp [seqstrict, klabel('LtEq)] - | Exp "==" Exp [seqstrict, klabel('Eq)] - | Exp "!=" Exp [klabel('NotEq)] - -endmodule diff --git a/src/common/sort-predicate-hacks.k b/src/common/sort-predicate-hacks.k new file mode 100644 index 00000000..f162b26b --- /dev/null +++ b/src/common/sort-predicate-hacks.k @@ -0,0 +1,63 @@ +module SORT-PREDICATE-HACKS + +/* +The rules in this module are designed to extend the predicates for basic syntactic sorts like Exp or Stmt, and to +ease the restrictions imposed by those predicates. +For example, the syntactic definition of plus : syntax Exp ::= Exp + Exp, will return true for +isExp('Plus(K1,,K2)) only when both K1 and K2 are valid Exp terms, while a rule isExp('Plus(_)) => true +will produce true for any term whose root node has the label 'Plus. This allows us to use variable subsorting inside +rules, to define more rules syntactically. +*/ + +/* + Workaround: in a correct semantics these rules should not be needed, as all the labels below + are associated with expression syntax. Yet, the predicate isExp generated for sort Exp checks not only the + root label, but also the content of child nodes recursively, and child nodes are sometimes not valid children + of an expression. + + The predicate isExp() is used in elaboration phase by the rule [elabEnd-default-all-except-expressions]. +*/ +rule isExp('ArrayAccess(_)) => true +rule isExp('NewInstance(_)) => true // also in customElabChildren +rule isExp('QNewInstance(_)) => true // also in customElabChildren +rule isExp('InstanceOf(_)) => true +rule isExp('Invoke(_)) => true +rule isExp('This(_)) => true +rule isExp('QThis(_)) => true +rule isExp('AmbName(_)) => true +rule isExp('ExprName(_)) => true +rule isExp('Field(_)) => true +rule isExp('SuperField(_)) => true +rule isExp('QSuperField(_)) => true +rule isExp('NewArray(_)) => true +rule isExp('CastPrim(_)) => true +rule isExp('CastRef(_)) => true + + +// Used to define statements syntactically. +rule isStmt(_:K) => true +//rule isStmt('ClassDecStm(_)) => true +//rule isStmt('Block(_)) => true +//rule isStmt('LocalVarDecStm(_)) => true +//rule isStmt('LocalVarDec(_)) => true +//rule isStmt('If(_)) => true +//rule isStmt('While(_)) => true +//rule isStmt('For(_)) => true +//rule isStmt('ForEach(_)) => true +//rule isStmt('Labeled(_)) => true +//rule isStmt('Empty(_)) => true +//rule isStmt('ExprStm(_)) => true +//rule isStmt('AssertStm(_)) => true +//rule isStmt('Switch(_)) => true +//rule isStmt('DoWhile(_)) => true +//rule isStmt('Try(_)) => true +//rule isStmt('Throw(_)) => true +//rule isStmt('Continue(_)) => true +//rule isStmt('Break(_)) => true +//rule isStmt('Return(_)) => true +//rule isStmt('Synchronized(_)) => true +// +//// Special case, a sequence of statements. Might not be needed, we'll better add it to be sure. +//rule isStmt('ListWrap(_)) => true + +endmodule diff --git a/src/common/stmt-syntax.k b/src/common/stmt-syntax.k index 9365bb50..fa690de1 100644 --- a/src/common/stmt-syntax.k +++ b/src/common/stmt-syntax.k @@ -1,17 +1,17 @@ module STMT-SYNTAX imports CLASS-SYNTAX -//@ \subsection{Blocks.sdf} +//@ \subsubsection{Blocks} syntax BlockStmt ::= Stmt | LocalVarDecStmt | ClassDec [klabel('ClassDecStm)] -syntax Block ::= "{" BlockStmList "}" [klabel('Block)] +syntax Block ::= "{" K "}" [klabel('Block)] //was BlockStmList before -//@ \subsection{LocalVariableDeclaraions.sdf} +//@ \subsubsection{LocalVariableDeclaraions} syntax LocalVarDecStmt ::= LocalVarDec ";" [prefer, klabel('LocalVarDecStm)] syntax LocalVarDec ::= AnnoVarModList Type VarDecList [prefer, klabel('LocalVarDec)] -//@ \subsection{Statements.sdf} +//@ \subsubsection{Statements} syntax Stmt ::= StmtWithoutTrailing | LabeledStmt | IfThenElseStmt @@ -28,13 +28,14 @@ syntax StmtWithoutTrailing ::= Block | TryStmt | StackConsumerStmt | SynchronizedStmt + | ThrowStmt -syntax StackConsumerStmt ::= ThrowStmt | ContinueStmt | BreakStmt | ReturnStmt +syntax StackConsumerStmt ::= ContinueStmt | BreakStmt | ReturnStmt syntax IfThenElseStmt ::= "if" "(" Exp ")" Stmt "else" Stmt [strict(1), klabel('If)] -syntax IfThenStmt ::= "if" "(" Exp ")" Stmt [prefer, strict(1), klabel('If)] +syntax IfThenStmt ::= "if" "(" Exp ")" Stmt [prefer, klabel('If)] -syntax WhileStmt ::= "while" "(" Exp ")" Stmt [strict(1),klabel('While)] +syntax WhileStmt ::= "while" "(" Exp ")" Stmt [klabel('While)] syntax ForStmt ::= "for" "(" LocalVarDec ";" OptionalExp ";" Exps ")" Stmt [klabel('For)] syntax ForStmt ::= "for" "(" Exps ";" OptionalExp ";" Exps ")" Stmt [klabel('For)] diff --git a/src/common/subtyping.k b/src/common/subtyping.k index 2fa6cb61..5ea09aff 100644 --- a/src/common/subtyping.k +++ b/src/common/subtyping.k @@ -10,13 +10,6 @@ syntax KItem ::= subtype ( ) [strict] -/*@ Checks whether the each type in the first list of types is a subtype -of the type at the same position in the second list. -If lists have different size, the function will evaluate to false. -Used in method call overloading resolution. -*/ -syntax KItem ::= subtypeList ( Types, Types ) - rule [subtype-same-type-True]: subtype( T:Type, T ) => true [structural] @@ -143,6 +136,13 @@ rule [subtype-OfNoClass]: /*@ \subsection{Subtyping lists of types}*/ +/*@ Checks whether the each type in the first list of types is a subtype +of the type at the same position in the second list. +If lists have different size, the function will evaluate to false. +Used in method call overloading resolution. +*/ +syntax KItem ::= subtypeList ( Types, Types ) + rule [subtypeList]: subtypeList(types(T1:Type,,Ts:KList), types(Tp1:Type,,Tps:KList)) => andAux( subtype(T1,Tp1), subtypeList(types(Ts), types(Tps)) ) diff --git a/src/common/type-syntax.k b/src/common/type-syntax.k index 3c8542d9..969f11b0 100644 --- a/src/common/type-syntax.k +++ b/src/common/type-syntax.k @@ -2,14 +2,13 @@ module TYPE-SYNTAX imports NAME-SYNTAX imports OPTIONAL-SYNTAX -//@ \subsection{Main.sdf} syntax Type ::= PrimType | RefType /*Denis' syntax: actually in sdf "void" together with Type compose ResultType, since now "void" is Type, there is no need for another syntax of ResultType.*/ | "void" [klabel('Void)] -//@ \subsection{ParameterizedTypes.sdf} +//@ \subsubsection{ParameterizedTypes} syntax TypeArgs ::= "<" ActualTypeArgList ">" [klabel('TypeArgs)] syntax ActualTypeArg ::= Type @@ -19,7 +18,7 @@ syntax WildcardBound ::= "extends" RefType [klabel('WildcardUpperBo | "super" RefType [klabel('WildcardLowerBound)] -//@ \subsection{PrimitiveTypes.sdf} +//@ \subsubsection{PrimitiveTypes} syntax IntOrLongType ::= "int" [klabel('Int)] | "long" [klabel('Long)] syntax IntType ::= "byte" [klabel('Byte)] @@ -34,8 +33,8 @@ syntax NumericType ::= IntType | FloatType syntax PrimType ::= NumericType | "bool" [klabel('Boolean)] //sdf "boolean" -//@ \subsection{ReferenceTypes.sdf} - /*@ A fully qualified class name, or noClass where no valid class could be computed.*/ +//@ \subsubsection{ReferenceTypes} + syntax ClassOrInterfaceType ::= TypeDecSpec OptionalTypeArgs [klabel('ClassOrInterfaceType)] syntax InterfaceType ::= TypeDecSpec OptionalTypeArgs [klabel('InterfaceType)] @@ -51,7 +50,7 @@ syntax ArrayType ::= Type "[" "]" [strict, klabel( syntax RefType ::= ClassOrInterfaceType | ArrayType -//@ \subsection{TypeVariables.sdf} +//@ \subsubsection{TypeVariables} syntax TypeVarId ::= Id syntax TypeBound ::= "extends" ClassOrInterfaceTypeList [klabel('TypeBound)] diff --git a/src/exec/api-core.k b/src/exec/api-core.k index 56bb8c67..cafeb04a 100644 --- a/src/exec/api-core.k +++ b/src/exec/api-core.k @@ -4,12 +4,14 @@ module API-CORE imports ARRAYS // for allocAndInitArray() /*@ -All the methods defined in this module through invokeImpl are native, their body is 'NoMethodBody(\_), thus +This module contains the minimal part of Java API required to perform console read/write operations, +as well as a few other API functions mentioned in JLS. + +All the methods defined in this module through invokeImpl are native, their body is \verb|'NoMethodBody(\_)|, thus they cannot be matched by rules in METHOD-INVOKE. */ -/*@ This module contains the minimal part of java API required to perform console read/write operations, -as well as a few other API functions mentioned in JLS.*/ +//@ \subsection{\texttt{System.in}, \texttt{System.out}, \texttt{Scanner}} //@system-out-print-convert heat argument context @@ -20,7 +22,7 @@ context when Class ==K class String2Id("java.io.PrintWriter") andBool Id2String(MethodName) ==String "print" -//@ System.out.print(). For integers and strings, print their value. For classes, print class type. +//@ System.\verb|out.print()|. For integers and strings, print their value. For classes, print class type. rule [system-out-print-string]: @@ -35,10 +37,10 @@ when Class ==K class String2Id("java.io.PrintWriter") andBool Id2String(MethodName) ==String "print" //With [transition-threading], the time to produce 2 solutions for the test threads_11_two_th_msg is 14s. - //But with [transition-strictness], the same test takes 3m52s, with java heap = 16GB. + //But with [transition-strictness], the same test takes 3m52s, with Java heap = 16GB. [transition-threading] -//@Is only used for primitive type arguments. Object arguments are converted by java code inside the class PrintWriter. +//@Is only used for primitive type arguments. Object arguments are converted by Java code inside the class PrintWriter. rule [system-out-print-convert]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), _, @@ -49,7 +51,7 @@ when andBool (Id2String(MethodName) ==String "print") andBool notBool (isString(RV) ==K true) -/*@Scanner.nextInt(), used to read from the console.*/ +/*@\verb|Scanner.nextInt()|, used to read from the console.*/ rule [scanner-nextInt]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), _, @@ -78,7 +80,9 @@ rule [readString]: readString => Str :: classString ... ListItem(Str:String) => . ... -/*@ object.getClass()*/ +//@ \subsection{Class \texttt{Object}} + +/*@ \verb|object.getClass()|*/ rule [object-getClass-on-object]: invokeImpl( @@ -113,7 +117,7 @@ rule [object-getClass-on-array]: when Class ==K classObject andBool Id2String(MethodName) ==String "getClass" -/*@ String.toString(). For Object.toString() the implementation is in the library java code.*/ +/*@ \verb|String.toString()|. For \verb|Object.toString()| the implementation is in the library Java code.*/ rule [object-toString-on-String]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), Str:String::_, @@ -122,7 +126,7 @@ rule [object-toString-on-String]: when Class ==K classObject andBool Id2String(MethodName) ==String "toString" -/*@Object.hashCode(). Returns the canonical memory location of the objectRef. */ +/*@\verb|Object.hashCode()|. Returns the canonical memory location of the objectRef. */ rule [object-hashCode]: invokeImpl( @@ -139,9 +143,9 @@ rule [object-hashCode]: when Class ==K classObject andBool Id2String(MethodName) ==String "hashCode" -//@\subsection{String methods} +//@ \subsection{Class \texttt{String}} -//@ int String.length() +//@ int \verb|String.length()| rule [String-length]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), @@ -162,7 +166,7 @@ rule [String-charAt]: when Class ==K classString andBool Id2String(MethodName) ==String "charAt" -//@static native String String.valueOf(int i); +//@static native String \verb|String.valueOf(int i)|; rule [String-valueOf]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), @@ -173,7 +177,7 @@ rule [String-valueOf]: when Class ==K classString andBool Id2String(MethodName) ==String "valueOf" -//@boolean String.equals(Object) +//@boolean \verb|String.equals(Object)| rule [String-equals]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), @@ -184,7 +188,7 @@ rule [String-equals]: when Class ==K classString andBool Id2String(MethodName) ==String "equals" -//@String.toString() +//@\verb|String.toString()| rule [String-toString]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), @@ -195,7 +199,7 @@ rule [String-toString]: when Class ==K classString andBool Id2String(MethodName) ==String "toString" -//@ int String.compareTo(Object another) +//@ int \verb|String.compareTo(Object another)| rule [String-compareTo]: invokeImpl( methodRef(sig(MethodName:Id, _), Class:ClassType), @@ -256,10 +260,10 @@ when rule [storeCopy-discard]: storeCopy(_, _, 0) => . -//@\subsection{Class literal - .class} +//@\subsection{Class literal operator --- \texttt{A.class}} /*@ We need to synchronize access to class literals to avoid instantiation of the came .class by multiple threads. - This is done by the term temp in . We cannot use 'Synchronized because it required an + This is done by the term temp in \verb||. We cannot use 'Synchronized because it required an objectRef as argument, and we might not have any objects instantiated at the moment. */ rule [Lit-Class-Instantiate]: @@ -287,7 +291,7 @@ rule [Lit-Class]: 'Lit('Class(T:Type)) => TV ... ... T |-> TV:TypedVal ... -//@Used inside only for synchronization purposes +//@Used inside \verb|| only for synchronization purposes syntax KItem ::= "temp" endmodule diff --git a/src/exec/api-threads.k b/src/exec/api-threads.k index 299522d9..ecf31b08 100644 --- a/src/exec/api-threads.k +++ b/src/exec/api-threads.k @@ -2,11 +2,10 @@ module API-THREADS imports CORE-SORTS imports METHOD-INVOKE-REST //for invokeImpl imports VAR-LOOKUP //for typedLookup - imports API-THREADS-SELECTION /*@Java API related to threads and locks. Just the core part.*/ -//@ \subsection{Method Thread.start()} +//@ \subsection{Method \texttt{Thread.start()}} rule [thread-start]: @@ -90,7 +89,7 @@ rule [monitor-completely-released]: ... (OL:Int |-> 0 => .) ... ... (SetItem(OL) => .) ... -//@ \subsection{Thread.join()} +//@ \subsection{\texttt{Thread.join()}} rule [thread-join]: @@ -120,7 +119,91 @@ when Class ==K class String2Id("java.lang.Thread") andBool Id2String(MethodName) ==String "joinImpl" [transition-threading, transition-sync] -//@ \subsection{Object.wait()} +//@ \subsection{Methods \texttt{wait()} and \texttt{notify()} --- core rules} + +/*@ +When \verb|object.wait()| is called the method call expression is replaced by \verb|waitImpl()| +--- an auxiliary function that is used later to exit from the waiting state. +The id of the current thread (\verb|TId|) has to be registered in the set inside \cellref[]{waitingThreads}. + The cell \cellref[]{holds} attached to each thread stores the number of times the current thread + acquired the lock on each object. Here we use it to make sure that the current thread acquired the lock at least once + (see the side condition). Otherwise calling the method \verb|wait()| is illegal and we have to throw an exception, according + to Java API. The exceptional case is covered by other rules. Another cell matched here is \cellref[]{busy}. It stores + the set of objects that serve as synchronization monitors --- arguments of blocks \verb|synchronized|. When + an object enters the waiting state it have to release the ownership of this monitor, this is reflected by deleting + the entry \verb|OL| from the set. In this rule the cell \cellref[]{thread} is used solely for clarity, to separate + the cells that are attached to a thread from global cells. In fact, if we would delete \cellref[]{thread} here and + keep just what is inside, the semantics of the rule would not change. This is because configuration abstraction + mechanism of \K would infer the surrounding context for each of \cellref[]{k} \cellref[]{tid} and \cellref[]{holds}. + It would know to match them under the same \cellref[]{thread}, even if there are multiple \cellref[]{thread} cells. +*/ +rule [object-wait]: + //added just for clarity, to illustrate the distinctive context of and + + objectRef(OId:Int, _)::_ . methodRef(sig(Method:Id, _), Class:ClassType) (.TypedVals) + => waitImpl(OId) + ... + + TId:Int + ... OId |-> HoldLevel:Int ... + ... + + ... (SetItem(OId) => .) ... + ... (. => TId |-> OId ) ... +when + Class ==K classObject + andBool Id2String(Method) ==String "wait" + andBool HoldLevel >=Int 1 + [transition-threading] + +/*@ +When another thread calls \verb|notify()| we have to make sure that the thread holds the monitor on the target object + (the side condition). Otherwise we have to throw an exception. The actual logic of \verb|notify()| is delegated + to \verb|notifyImpl()|, in order to avoid duplication. The construct \verb|notifyImpl()| requires two rules for two + cases --- the case when there is at least one thread waiting on the target object, and the case when there is no one. +*/ +rule [object-notify]: + + objectRef(OId:Int, _)::_ . methodRef(sig(Method:Id, _), Class:ClassType) (.TypedVals) + => notifyImpl(OId) + ... + + ... OId |-> HoldLevel:Int ... +when + Class ==K classObject + andBool Id2String(Method) ==String "notify" + andBool HoldLevel >=Int 1 + +/*@ +Here we present the rule for the first case. If there is a thread waiting on the current object, then the object + identifier \verb|OId| will be present among the map values of \cellref[]{waitingThreads}. By deleting the whole entry + associated to that value we enable the waiting thread to proceed. If there is no thread waiting for this object then + the term \verb|notifyImpl()| is simply consumed. +*/ +rule [notifyImpl-someone-waiting]: + notifyImpl(OId:Int) => nothing::void ... + ... (_ |-> OId => .Map) ... + [transition-threading] + +/*@ +At this stage the rule for \verb|waitImpl()| could match. The rule checks in its side conditions that the current + thread id \verb|TId| is not among the waiting threads anymore. It also checks that the target object, represented by + \verb|OId| is not busy. This is required because the thread exiting from waiting state have to reacquire the monitor + on the target object. Finally, the rule have to make sure that the thread was not interrupted while it was waiting. + Otherwise another rule will match and will throw the appropriate exception. +*/ +rule [waitImpl-main]: + waitImpl(OId:Int) => nothing::void ... + TId:Int + Busy:Set (. => SetItem(OId)) + false + WT:Map +when + (notBool TId in keys(WT)) + andBool (notBool OId in Busy) + [transition-threading, transition-sync] + +//@ \subsection{\texttt{Object.wait()} --- additional} rule [object-wait-notify-notifyAll-without-sync]: @@ -138,8 +221,8 @@ when ) andBool notBool OL in keys(Holds) -/*@Second part of a wait. Waiting was already registered to . -When the record in will be deleted, waiting itself shall end. +/*@Second part of a wait. Waiting was already registered to \verb||. +When the record in \verb|| will be deleted, waiting itself shall end. */ syntax KItem ::= waitImpl ( Int //Monitor object location @@ -157,9 +240,9 @@ when notBool OL in Busy [transition-threading, transition-sync] -//@ \subsection{Object.notify(), Object.notifyAll()} +//@ \subsection{\texttt{Object.notify()}, \texttt{Object.notifyAll()} --- additional} -/*@Implementation of Object.notify(), extracted here to avoid rule superfluousness*/ +/*@Implementation of \verb|Object.notify()|, extracted here to avoid rule superfluousness*/ syntax KItem ::= notifyImpl ( Int //store key of the monitor object ) @@ -194,7 +277,7 @@ when andBool Id2String(MethodName) ==String "notifyAll" andBool HoldLevel >=Int 1 -/*@Implementation of Object.notifyAll(), extracted here to avoid rule superfluousness*/ +/*@Implementation of \verb|Object.notifyAll()|, extracted here to avoid rule superfluousness*/ syntax KItem ::= objectNotifyAllImpl ( Int //store key of the monitor object ) @@ -217,7 +300,7 @@ when notBool OL in values(WT) [transition-threading] -//@ \subsection{Thread.interrupt()} +//@ \subsection{\texttt{Thread.interrupt()}} rule [thread-interrupt]: @@ -272,8 +355,8 @@ rule [ThreadTermination]: //@ \subsection{Debug aids} -/*@ Dissolve all cells except for the purpose of model checking. We will avoid duplicates caused by the same - but different order of content in other cells.*/ +/*@ Dissolve all cells except \verb|| for the purpose of model checking. We will avoid duplicates caused by the same + \verb|| but different order of content in other cells.*/ rule [DissolveAllExceptOut]: Out:List @@ -285,92 +368,3 @@ rule [DissolveAllExceptOut]: => Out endmodule - -module API-THREADS-SELECTION - imports API-THREADS - -//@ \subsection{Methods wait() and notify()} - -/*@ -When \verb|object.wait()| is called the method call expression is replaced by \verb|waitImpl()| --- an auxiliary function that is used later to exit from the waiting state. -The id of the current thread (\verb|TId|) has to be registered in the set inside \cellref[]{waitingThreads}. - The cell \cellref[]{holds} attached to each thread stores the number of times the current thread - acquired the lock on each object. Here we use it to make sure that the current thread acquired the lock at least once - (see the side condition). Otherwise calling the method \verb|wait()| is illegal and we have to throw an exception, according - to Java API. The exceptional case is covered by other rules. Another cell matched here is \cellref[]{busy}. It stores - the set of objects that serve as synchronization monitors -- arguments of blocks \verb|synchronized|. When - an object enters the waiting state it have to release the ownership of this monitor, this is reflected by deleting - the entry \verb|OL| from the set. In this rule the cell \cellref[]{thread} is used solely for clarity, to separate - the cells that are attached to a thread from global cells. In fact, if we would delete \cellref[]{thread} here and - keep just what is inside, the semantics of the rule would not change. This is because configuration abstraction - mechanism of \K would infer the surrounding context for each of \cellref[]{k} \cellref[]{tid} and \cellref[]{holds}. - It would know to match them under the same \cellref[]{thread}, even if there are multiple \cellref[]{thread} cells. -*/ -rule [object-wait]: - //added just for clarity, to illustrate the distinctive context of and - - objectRef(OId:Int, _)::_ . methodRef(sig(Method:Id, _), Class:ClassType) (.TypedVals) - => waitImpl(OId) - ... - - TId:Int - ... OId |-> HoldLevel:Int ... - ... - - ... (SetItem(OId) => .) ... - ... (. => TId |-> OId ) ... -when - Class ==K classObject - andBool Id2String(Method) ==String "wait" - andBool HoldLevel >=Int 1 - [transition-threading] - -/*@ -When another thread calls \verb|notify()| we have to make sure that the thread holds the monitor on the target object - (the side condition). Otherwise we have to throw an exception. The actual logic of \verb|notify()| is delegated - to \verb|notifyImpl()|, in order to avoid duplication. The construct \verb|notifyImpl()| requires two rules for two - cases -- the case when there is at least one thread waiting on the target object, and the case when there is no one. -*/ -rule [object-notify]: - - objectRef(OId:Int, _)::_ . methodRef(sig(Method:Id, _), Class:ClassType) (.TypedVals) - => notifyImpl(OId) - ... - - ... OId |-> HoldLevel:Int ... -when - Class ==K classObject - andBool Id2String(Method) ==String "notify" - andBool HoldLevel >=Int 1 - -/*@ -Here we present the rule for the first case. If there is a thread waiting on the current object, then the object - identifier \verb|OId| will be present among the map values of \cellref[]{waitingThreads}. By deleting the whole entry - associated to that value we enable the waiting thread to proceed. If there is no thread waiting for this object then - the term \verb|notifyImpl()| is simply consumed. -*/ -rule [notifyImpl-someone-waiting]: - notifyImpl(OId:Int) => nothing::void ... - ... (_ |-> OId => .Map) ... - [transition-threading] - -/*@ -At this stage the rule for \verb|waitImpl()| could match. The rule checks in its side conditions that the current - thread id \verb|TId| is not among the waiting threads anymore. It also checks that the target object, represented by - \verb|OId| is not busy. This is required because the thread exiting from waiting state have to reacquire the monitor - on the target object. Finally, the rule have to make sure that the thread was not interrupted while it was waiting. - Otherwise another rule will match and will throw the appropriate exception. -*/ -rule [waitImpl-main]: - waitImpl(OId:Int) => nothing::void ... - TId:Int - Busy:Set (. => SetItem(OId)) - false - WT:Map -when - (notBool TId in keys(WT)) - andBool (notBool OId in Busy) - [transition-threading, transition-sync] - -endmodule diff --git a/src/exec/arrays.k b/src/exec/arrays.k index 6cdb7628..87bc817d 100644 --- a/src/exec/arrays.k +++ b/src/exec/arrays.k @@ -2,9 +2,12 @@ module ARRAYS imports CORE-SORTS imports SUBTYPING imports EXPRESSIONS + imports VAR-LOOKUP imports SYNTAX-CONVERSIONS imports JAVA-SYNTAX +//@ \subsection{Array access} + /*@ The value in store that corresponds to an array element. The consturction "elem" Type is meant to distinguish between regular memory locations and array elements. Array elements need to be represented separately in order to support array polymorphism. @@ -47,12 +50,29 @@ rule [Field-array-length]: when Id2String(X) ==String "length" -//@ \subsection{New array allocation} -/*@ The dynamic semantics of typed array declarations is -similar to that in untyped SIMPLE, but we have to enforce that the -type of an array declaration be of the form \texttt{arrayOf $T$} -and assign the right type ($T$) to the allocated array locations. */ +//@ \subsection{Assignment to array elements} + +rule [storeImpl-array-elem]: + storeImpl(L:Int, V:RawVal :: T:Type) => . ... + ... L |-> (_ => V) :: elem T:Type ... + +rule [storeImpl-array-location-check-type]: + + storeImpl(L:Int, V:RawVal::T:Type) + => ifAux(subtype(typeOf(V), StoreType), + storeImpl(L, V::StoreType), + throw new class String2Id("java.lang.ArrayStoreException") ( + //the ArrayStoreException argument is the assigned object type + (V::T .((String2Id("getClass")):>MethodName) (.TypedVals)) .((String2Id("getName")):>MethodName) (.TypedVals) + ); + ) + ... + + ... L |-> _ :: elem StoreType:Type ... +when + T =/=K StoreType +//@ \subsection{Array allocation} /* For multi-dimensions arrays, it is expanded from the last DimExp, but currently, the tail element(s) matching is unavailable for user defined lists, so we reverse list for easier matching @@ -83,6 +103,7 @@ rule [NewArray-ArrayInit]: new arrayOf T:Type .Dims {InitContent:VarInits} => arrayInitAlloc((new T [length(InitContent)::int] .Dims), {InitContent}) +//@Length of an array initializer. syntax Int ::= length (VarInits) [function] rule length(V:VarInit, Vs:VarInits) => length(Vs)+Int 1 rule length(.VarInits) => 0 @@ -121,7 +142,7 @@ rule [allocAndInitArray-MultiDim-desugar]: [structural] -/*@ The increment of by one is required to avoid problems with empty arrays. +/*@ The increment of \verb|| by one is required to avoid problems with empty arrays. Two empty arrays allocated one after another should have different starting locations, even if those starting locations are not used. This is required to identify them as two different objects. Their distinction could be tested by the operator ==. @@ -135,13 +156,6 @@ rule [allocAndInitArray]: LI:Int => LI +Int 1 -//@ Maximum of two numbers -syntax KItem ::= max ( Int, Int ) [function] -rule max(I1:Int, I2:Int) => #if I1 >=Int I2 - #then I1 - #else I2 - #fi - /*@ Allocates the given number of elements in the store of the given Type. Used by array instantiation logic. */ syntax KItem ::= allocArray ( @@ -180,28 +194,6 @@ when rule initArray(_, 0, _) => .K [structural] -//@ \subsection{Array element assignment} - -rule [storeImpl-array-elem]: - storeImpl(L:Int, V:RawVal :: T:Type) => . ... - ... L |-> (_ => V) :: elem T:Type ... - -rule [storeImpl-array-location-check-type]: - - storeImpl(L:Int, V:RawVal::T:Type) - => ifAux(subtype(typeOf(V), StoreType), - storeImpl(L, V::StoreType), - throw new class String2Id("java.lang.ArrayStoreException") ( - //the ArrayStoreException argument is the assigned object type - (V::T .((String2Id("getClass")):>MethodName) (.TypedVals)) .((String2Id("getName")):>MethodName) (.TypedVals) - ); - ) - ... - - ... L |-> _ :: elem StoreType:Type ... -when - T =/=K StoreType - //@ \subsection{Array initializer} //@ Allocates the array based on previously computed size, then proceeds to array initialization diff --git a/src/exec/configuration-exec.k b/src/exec/configuration-exec.k index 8e22323e..0b8c6b51 100644 --- a/src/exec/configuration-exec.k +++ b/src/exec/configuration-exec.k @@ -2,92 +2,6 @@ module CONFIGURATION-EXEC imports CORE-SORTS imports CORE-FUNCTIONS -/*@ -The execution configuration consists from the top-level cell \cellref{T}, whose content is divided into three large cell groups. The group \cellref[]{threads} contains one or multiple cells \cellref[]{thread}. Here is included the data related to the execution of a thread, such as the computation, stack, local environment. The second group is contained inside \cellref[]{classes} that have multiple \cellref[]{class} cells -- all the content related to particular classes. The third group consists of the remaining top-level cells. - -\paragraph{Threads} Each execution thread has a corresponding \cellref{thread}. Inside a thread, \cellref[K]{k} is represents the actual computation - the sequence of tasks to be executed. Next cells are \cellref[List]{stack} -- the method call stack, and \cellref{methodContext}. The \cellref{methodContext} holds the local context of the executed method: -\begin{itemize} - \item \cellref[Map{{[}}Id\mapsto{}Int{{]}}]{env} -- the map from local variable names to their location inside \cellref[]{store}. - \item \cellref[ClassType]{crntClass} -- the current class, the type of \verb|this| - \item \cellref[Int]{location} -- The location in memory store of the current object. -\end{itemize} - -On the next line there are 3 cells related to multithreading: -\begin{itemize} - \item \cellref{tid} -- the thread identified, generated when the thread is created. - \item \cellref[Map{{[}}Int\mapsto{}Int{{]}}]{holds} -- a map from Object locations to integer numbers. Map keys are monitor objects on which the current thread has the locks. Map values hold the number of times the lock was acquired. - \item \cellref[Bool]{interrupted} -- boolean value signaling whether the current thread was interrupted. -\end{itemize} - -\paragraph{Classes} The cell \cellref{classes} contains one \cellref{class} for each class in the program, both for supported JDK classes and for user-defined classes. Cell \cellref{class} has the following content: - -\begin{itemize} - \item \cellref[ClassType]{classType} --- the fully qualified class name. This cell serves as identifier for the whole \cellref{class}, thus \cellref{classes} may be seen as a map from class name to \cellref{class} content. - \item \cellref[ClassMetaType]{classMetaType} --- Whether this type is class or interface. Both are referred hereafter as "classes", making the distinctions only when necessary. - \item \cellref[ClassPhase]{classPhase} --- Used during unfolding global phase (see below). - \item \cellref[ClassType]{enclosingClass} --- For inner classes, the direct lexically enclosing class of this class. For top-level classes --- no value. - \item \cellref[ClassType]{extends} --- The base class. - \item \cellref[Set {[} ClassType {]} ]{implTrans} --- the transitive closure of implemented interfaces. - \item \cellref[ Map {[} Signature \mapsto ClassType {]} ]{methods} --- The map of accessible methods. Keys are method signatures, values are classes where methods are defined. Includes both methods declared within this class as well as methods inherited from base classes/ base interfaces. - \item \cellref[Bag]{methodDecs} --- the collection of method declarations (\cellref{methodDec} cells)in the current class. This cell contains only a subset of methods from \cellref{methods}, as the set of accessible methods from \cellref{methods} also includes methods inherited from base classes/interfaces. Hence the need of two separate collections. Each \cellref[Bag]{methodDec} contains the following data: - \begin{itemize} - \item \cellref[Signature]{methodSignature} --- The method signature, acting as identifier of the \cellref{methodDec} - \item \cellref[ List{[} Param {]} ]{methodParams} --- method parameters - \item \cellref[K]{methodBody} --- method body - \item \cellref[AccessMode]{methodAccessMode} --- method access mode - \item \cellref[ContextType]{methodContextType} --- either static or instance - \end{itemize} - \item \cellref[K]{instanceFields} --- The list of instance field declarations, stored as a list of local variable declaration statements, without initializers. Used during object instantiation. - \item \cellref[K]{staticFields} --- The list of static field declarations, in a similar format as \cellref{instanceFields} - \item \cellref[K]{staticInit} --- The list of static initializers and static field initializers concatenated into one block. The content of \cellref{staticFields} and \cellref{staticInit} is executed during class static initialization. - \item \cellref[K]{folded} --- the initial representation of the class in AST format, during unfolding phase (see below). - \item \cellref[StaticInitStatus]{staticInitStatus} --- the static initialization status of the class. May be either uninitialized, initializing or initialized. The content of this class is used to trigger static initialization of the class on first use. - \item \cellref[ Map{[} Id \mapsto Location {]} ]{staticEnv} --- The map from static fields declared in this class to their locations in the store. Populated during static initialization. This cell along with \cellref{staticInitStatus} are the only two cells of \cellref{class} altered during program execution, during static initialization. The rest of the cells are populated before the execution. -\end{itemize} - -\paragraph{The remaining cells} -The first three cells after \cellref{classes} are important at the beginning of computation: -\begin{itemize} - \item \cellref[K]{program} --- The initial AST representation of the program, containing both core classes from JDK and user-defined classes. - \item \cellref[K]{mainClass} --- The class containing the method \verb|main()| --- the starting point of execution. Loaded froma command line argument. - \item \cellref[K]{globalPhase} --- Computation in the execution semantics may be in one of two global phases: Unfolding and Execution. The role of hte unfolding phase is to convert the AST representation of the program stored in \cellref{program} into the collection of cells \cellref{classes}. When this operation is complete, execution phase follows. -\end{itemize} - -The next 4 cells represent the memory model of K-Java: -\begin{itemize} - \item \cellref[Map{[}Location:Int \mapsto Value:TypedVal{]}]{store} --- the program memory. Map from memory locations to actual values. For reference types only the reference is stored in this cell. - \item \cellref[ Map{[} Location:Int \mapsto LocMetadata {]} ]{storeMetadata} --- For each location in \cellref{store}, information whether that location is a local variable or field. Used for performance optimization of multi-threaded model-checking. - \item \cellref[Int]{nextLoc} --- the next available memory location. Incremmented after each allocation. - \item \cellref[ Map{[} Type \mapsto TypedVal {]} ]{classLiteralsMap} --- A map from types T to objects that represent the value of the expression \verb|T.class| . - \item \cellref[Bag]{objectStore} --- Represents runtime state of all the instantiated objects. Multiple references to the same object are modeled through multiple entries in \cellref{store} pointing to the same entry in \cellref{objectStore}. The cell contains multiple \cellref{object} cells, each with the following content: - \begin{itemize} - \item \cellref[Int]{objectId} --- A unique object identifier, pointed by each reference in \cellref{store} - \item \cellref[ClassType]{objectType} --- The runtime type of the object. - \item \cellref[Bag]{layer} --- There could be multiple layer cells inside an \cellref{object}. Each layer represents a concrete class in the inheritance hierarchy, starting from \verb|java.lang.Object| and finishing with \cellref{objectType}. An object layer stores the follosing information: - \begin{itemize} - \item \cellref[ClassType]{layerClass} --- The class represented by this layer. - \item \cellref[Map{[}Id \mapsto Int{]}]{layerEnv} --- A map from instante fields to their loations in the store. - \item \cellref[TypedVal]{layerEnclosingObject} --- A reference to the directly enclosing object if this object represents an instance inner class, or empty for other types of objects (top-level and static inner). - \end{itemize} - \end{itemize} -\end{itemize} - -The following cells represent program I/O: -\begin{itemize} - \item \cellref[List]{in} --- the standard input, represented as pre-parsed list of elements of type Int or String. - \item \cellref[List]{out} --- the standard output. -\end{itemize} - -The next row contains global cells related to multithreading: -\begin{itemize} - \item \cellref[ Set{[} ObjLocation:Int {]} ]{busy} --- the set of busy objects. E.g. monitor objects for which there is a thread holding the monitor. - \item \cellref[ Map{[} ThreadId:Int \mapsto OL:Int {]} ]{waitingThreads} --- The map from threads to monitor objects on which respective threads are blocked in a call to \verb|wait()|. Used by the methods \verb|Object.wait()|, \verb|Object.notify()|, \verb|Object.notifyAll()|. - \item \cellref[Set{[}ThreadId:Int{]}]{terminated} -- the set of identifiers of terminated threads. -\end{itemize} - -The rest of the global cells are used for debugging purposes. -*/ - configuration //Configuration part 1: threads @@ -233,7 +147,7 @@ configuration //Initial cells, loaded by krun and initial configuration. //The initial program loaded by krun. For full mode and preprocessing this is - //the initial java program, for execution mode it is the folded java program. + //the initial Java program, for execution mode it is the folded Java program. $PGM:K //Main class, passed as krun argument. We need it from the outside, just like JDK Java. @@ -330,4 +244,90 @@ configuration +/*@ +The execution configuration consists from the top-level cell \cellref{T}, whose content is divided into three large cell groups. The group \cellref[]{threads} contains one or multiple cells \cellref[]{thread}. Here is included the data related to the execution of a thread, such as the computation, stack, local environment. The second group is contained inside \cellref[]{classes} that have multiple \cellref[]{class} cells --- all the content related to particular classes. The third group consists of the remaining top-level cells. + +\paragraph{Threads} Each execution thread has a corresponding \cellref{thread}. Inside a thread, \cellref[K]{k} is represents the actual computation --- the sequence of tasks to be executed. Next cells are \cellref[List]{stack} --- the method call stack, and \cellref{methodContext}. The \cellref{methodContext} holds the local context of the executed method: +\begin{itemize} + \item \cellref[Map{{[}}Id \mapsto Int{{]}}]{env} --- The map from local variable names to their location inside \cellref[]{store}. + \item \cellref[ClassType]{crntClass} --- The current class, the type of \verb|this|. + \item \cellref[Int]{location} --- The location in memory store of the current object. +\end{itemize} + +On the next line there are 3 cells related to multithreading: +\begin{itemize} + \item \cellref{tid} --- The thread identified, generated when the thread is created. + \item \cellref[Map{{[}}Int \mapsto Int{{]}}]{holds} --- A map from Object locations to integer numbers. Map keys are monitor objects on which the current thread has the locks. Map values hold the number of times the lock was acquired. + \item \cellref[Bool]{interrupted} --- A boolean value signaling whether the current thread was interrupted. +\end{itemize} + +\paragraph{Classes} The cell \cellref{classes} contains one \cellref{class} for each class in the program, both for supported JDK classes and for user-defined classes. Cell \cellref{class} has the following content: + +\begin{itemize} + \item \cellref[ClassType]{classType} --- The fully qualified class name. This cell serves as identifier for the whole \cellref{class}, thus \cellref{classes} may be seen as a map from class name to \cellref{class} content. + \item \cellref[ClassMetaType]{classMetaType} --- Indicates whether this type is class or interface. Both are referred hereafter as "classes", making the distinctions only when necessary. + \item \cellref[ClassPhase]{classPhase} --- Used during unfolding global phase (see below). + \item \cellref[ClassType]{enclosingClass} --- For inner classes, the direct lexically enclosing class of this class. For top-level classes --- no value. + \item \cellref[ClassType]{extends} --- The base class. + \item \cellref[Set {[} ClassType {]} ]{implTrans} --- The transitive closure of implemented interfaces. + \item \cellref[ Map {[} Signature \mapsto ClassType {]} ]{methods} --- The map of accessible methods. Keys are method signatures, values are classes where methods are defined. Includes both methods declared within this class as well as methods inherited from base classes/ base interfaces. + \item \cellref[Bag]{methodDecs} --- The collection of method declarations (\cellref{methodDec} cells)in the current class. This cell contains only a subset of methods from \cellref{methods}, as the set of accessible methods from \cellref{methods} also includes methods inherited from base classes/interfaces. Hence the need of two separate collections. Each \cellref[Bag]{methodDec} contains the following data: + \begin{itemize} + \item \cellref[Signature]{methodSignature} --- The method signature, acting as identifier of the \cellref{methodDec} + \item \cellref[ List{[} Param {]} ]{methodParams} --- The method parameters. + \item \cellref[K]{methodBody} --- method body + \item \cellref[AccessMode]{methodAccessMode} --- The method access mode. + \item \cellref[ContextType]{methodContextType} --- May be either static or instance. + \end{itemize} + \item \cellref[K]{instanceFields} --- The list of instance field declarations, stored as a list of local variable declaration statements, without initializers. Used during object instantiation. + \item \cellref[K]{staticFields} --- The list of static field declarations, in a similar format as \cellref{instanceFields} + \item \cellref[K]{staticInit} --- The list of static initializers and static field initializers concatenated into one block. The content of \cellref{staticFields} and \cellref{staticInit} is executed during class static initialization. + \item \cellref[K]{folded} --- The initial representation of the class in AST format, during unfolding phase (see below). + \item \cellref[StaticInitStatus]{staticInitStatus} --- The static initialization status of the class. May be either uninitialized, initializing or initialized. The content of this class is used to trigger static initialization of the class on first use. + \item \cellref[ Map{[} Id \mapsto Location {]} ]{staticEnv} --- The map from static fields declared in this class to their locations in the store. Populated during static initialization. This cell along with \cellref{staticInitStatus} are the only two cells of \cellref{class} altered during program execution, during static initialization. The rest of the cells are populated before the execution. +\end{itemize} + +\paragraph{The remaining cells} +The first three cells after \cellref{classes} are important at the beginning of computation: +\begin{itemize} + \item \cellref[K]{program} --- The initial AST representation of the program, containing both core classes from JDK and user-defined classes. + \item \cellref[K]{mainClass} --- The class containing the method \verb|main()| --- the starting point of execution. Loaded from a command line argument. + \item \cellref[K]{globalPhase} --- Computation in the execution semantics may be in one of two global phases: Unfolding and Execution. The role of the unfolding phase is to convert the AST representation of the program stored in \cellref{program} into the collection of cells \cellref{classes}. When this operation is complete, execution phase follows. +\end{itemize} + +The next 4 cells represent the memory model of K-Java: +\begin{itemize} + \item \cellref[Map{[}Location:Int \mapsto Value:TypedVal{]}]{store} --- The program memory. Map from memory locations to actual values. For reference types only the reference is stored in this cell. + \item \cellref[ Map{[} Location:Int \mapsto LocMetadata {]} ]{storeMetadata} --- For each location in \cellref{store}, information whether that location is a local variable or field. Used for performance optimization of multi-threaded model-checking. + \item \cellref[Int]{nextLoc} --- the next available memory location. Incremmented after each allocation. + \item \cellref[ Map{[} Type \mapsto TypedVal {]} ]{classLiteralsMap} --- A map from types T to objects that represent the value of the expression \verb|T.class| . + \item \cellref[Bag]{objectStore} --- Represents runtime state of all the instantiated objects. Multiple references to the same object are modeled through multiple entries in \cellref{store} pointing to the same entry in \cellref{objectStore}. The cell contains multiple \cellref{object} cells, each with the following content: + \begin{itemize} + \item \cellref[Int]{objectId} --- A unique object identifier, pointed by each reference in \cellref{store} + \item \cellref[ClassType]{objectType} --- The runtime type of the object. + \item \cellref[Bag]{layer} --- There could be multiple layer cells inside an \cellref{object}. Each layer represents a concrete class in the inheritance hierarchy, starting from \verb|Java.lang.Object| and finishing with \cellref{objectType}. An object layer stores the following information: + \begin{itemize} + \item \cellref[ClassType]{layerClass} --- The class represented by this layer. + \item \cellref[Map{[}Id \mapsto Int{]}]{layerEnv} --- A map from instance fields to their locations in the store. + \item \cellref[TypedVal]{layerEnclosingObject} --- A reference to the directly enclosing object if this object represents an instance inner class, or empty for other types of objects (top-level and static inner). + \end{itemize} + \end{itemize} +\end{itemize} + +The following cells represent program I/O: +\begin{itemize} + \item \cellref[List]{in} --- The standard input, represented as pre-parsed list of elements of type Int or String. + \item \cellref[List]{out} --- The standard output. +\end{itemize} + +The next row contains global cells related to multithreading: +\begin{itemize} + \item \cellref[ Set{[} ObjLocation:Int {]} ]{busy} --- The set of busy objects. E.g. monitor objects for which there is a thread holding the monitor. + \item \cellref[ Map{[} ThreadId:Int \mapsto OL:Int {]} ]{waitingThreads} --- The map from threads to monitor objects on which respective threads are blocked in a call to \verb|wait()|. Used by the methods \verb|Object.wait()|, \verb|Object.notify()|, \verb|Object.notifyAll()|. + \item \cellref[Set{[}ThreadId:Int{]}]{terminated} --- The set of identifiers of terminated threads. +\end{itemize} + +The rest of the global cells are used for debugging purposes. +*/ + endmodule diff --git a/src/exec/core-exec.k b/src/exec/core-exec.k index e7b7bea7..b168bbaa 100644 --- a/src/exec/core-exec.k +++ b/src/exec/core-exec.k @@ -2,15 +2,28 @@ module CORE-EXEC imports CORE-SORTS imports SYNTAX-CONVERSIONS +/*@ +A collection of utility functions that many other, unrelated modules depend on. Grouped here to minimize +the dependencies between other modules. +*/ + //@ ListItem content as a stack layer syntax KItem ::= sl ( K, //K - rest of computation Bag //MethContext - the content of ) -//@ \subsection{Auxiliary methods} +//@Auxiliary constructs used in variable access semantics. +syntax KItem ::= lvalue ( K ) +syntax RawVal ::= loc ( Int ) + +//@Store to the given location in (first argument) the given value (second argument). +syntax KItem ::= store ( + Int, //OL - the store location + K //evaluates to TypedVal - the value to be stored + ) [strict(2)] -//@ Restore the content of the cell +//@ Restore the content of the cell \verb|| syntax KItem ::= restoreMethContext ( Bag //The content of ) @@ -19,9 +32,4 @@ rule [restoreMethContext]: restoreMethContext(MethContext:Bag) => . ... _ => MethContext -/*@ \subsection{lvalue and loc syntax} */ - -syntax KItem ::= lvalue ( K ) -syntax RawVal ::= loc ( Int ) - endmodule diff --git a/src/exec/expressions-classes.k b/src/exec/expressions-classes.k index c18b376f..ef28024d 100644 --- a/src/exec/expressions-classes.k +++ b/src/exec/expressions-classes.k @@ -8,13 +8,13 @@ module EXPRESSIONS-CLASSES /*@ Expressions that operate over objects. */ -/*@ \subsection{Instance Of} */ +/*@ \subsection{Instanceof operator} */ rule [InstanceOf]: V:RawVal::_ instanceof RT2:RefType => (V =/=K null) && subtype(typeOf(V), RT2) -/*@ \subsection{Cast} */ +/*@ \subsection{Cast operator --- reference types} */ rule [cast-RefType]: cast(RT1:RefType, V:RawVal :: RT2:RefType) => ifAux ( subtype(typeOf(V), RT1) , @@ -25,4 +25,8 @@ rule [cast-RefType]: ); ) +/*@ \subsection{Auxiliary constructs produced during elaboration} */ + +rule stmtAndExp(Stmt:K, Exp:K) => Stmt ~> Exp + endmodule diff --git a/src/exec/expressions.k b/src/exec/expressions.k index 50eedce9..41b851c5 100644 --- a/src/exec/expressions.k +++ b/src/exec/expressions.k @@ -5,13 +5,18 @@ module EXPRESSIONS imports PRIMITIVE-TYPES // for normalizeType imports TO-STRING imports VAR-LOOKUP // for lookup +/*@ The module defines expressions operating over primitive types and String. +*/ - -/*@ Used to denote a temporary type of an expression. Such an expression should always be wrapped inside a cast +/*@ Used to denote a placeholder for an expression type, until the proper, normalized type of an expression + is computed. Never referred in the semantics. + An expression containing a placeholder type should always be wrapped inside a cast expression. The cast will then replace tempType with the proper compile-time type. */ syntax Type ::= "tempType" +/*@ \subsection{Boolean operators} */ + rule /* true || _ */ true :: bool || _ => true //We use K:K instead of TE:TypedList because 'LazyAnd is used inside the semantics, not only in the source program. @@ -43,6 +48,8 @@ rule F1:Float :: _ <= F2:Float :: _ => (F1 <=Float F2)::bool rule /* I1 >= I2 */ I1:Int :: _ >= I2:Int :: _ => (I1 >=Int I2)::bool rule F1:Float :: _ >= F2:Float :: _ => (F1 >=Float F2)::bool +/*@ \subsection{Numeric operators} */ + rule /* I1 << I2 */ I1:Int :: NT1:Type << I2:Int :: _ => (I1 <> I2 */ I1:Int :: NT1:Type >> I2:Int :: _ @@ -52,15 +59,6 @@ rule /* I1 >>> I2 */ I1:Int :: NT1:Type >>> I2:Int :: NT2:NumericType rule /* I1 + I2 */ I1:Int::_ + I2:Int::_ => (I1 +Int I2) :: tempType rule /* F1 + F2 */ F1:Float :: _ + F2:Float :: _ => (F1 +Float F2) :: tempType -rule /* Str1 + Str2 */ Str1:String :: _ + Str2:String :: _ => (Str1 +String Str2) :: classString -rule /* Str + KR */ Str:String :: Class:ClassType + ( KR:KResult => toString(KR) ) -when ((typeOf(KR) =/=K classString) - andBool Class ==K classString) - orBool (KR ==K (null::classString)) -rule /* KR + Str */ ( KR:KResult => toString(KR) ) + Str:String :: Class:ClassType -when ((typeOf(KR) =/=K classString) - andBool Class ==K classString) - orBool (KR ==K (null::classString)) rule /* I1 - I2 */ I1:Int :: _ - I2:Int :: _ => (I1 -Int I2) :: tempType rule /* F1 - F2 */ F1:Float :: _ - F2:Float :: _ => (F1 -Float F2) :: tempType @@ -133,13 +131,27 @@ syntax KItem ::= rightTypedNumber ( Int, NumericType ) [function] rule rightTypedNumber(I:Int, IntT:IntType) => I::IntT rule rightTypedNumber(I:Int, FloatT:FloatType) => Int2Float(I)::FloatT +/*@ \subsection{String operators} */ + +rule /* Str1 + Str2 */ Str1:String :: _ + Str2:String :: _ => (Str1 +String Str2) :: classString +rule /* Str + KR */ Str:String :: Class:ClassType + ( KR:KResult => toString(KR) ) +when ((typeOf(KR) =/=K classString) + andBool Class ==K classString) + orBool (KR ==K (null::classString)) +rule /* KR + Str */ ( KR:KResult => toString(KR) ) + Str:String :: Class:ClassType +when ((typeOf(KR) =/=K classString) + andBool Class ==K classString) + orBool (KR ==K (null::classString)) + +/*@ \subsection{Conditional operator} */ + /*@ Conditional expression : ?: . Desugared into an if with cast. The biggest difficulty is computing the expression type, according to JLS1 \$15.24 The whole expression should always come wrapped into a cast, from elaboration. Thus we don't have to worry about proper type conversion here.*/ rule CondExp:Exp ? TrueExp:Exp : FalseExp:Exp => ifAux(CondExp,TrueExp,FalseExp) -/*@ \subsubsection{Assignment operators} +/*@ \subsection{Assignment operators} Both basic assignment and compound assignments like +=, -=, etc. */ context (_:KResult = HOLE)<:AssignExp @@ -148,16 +160,18 @@ syntax LHS ::= TypedVal rule [Assign]: loc(L:Int) :: ResT:Type = V:RawVal :: ResT => store(L, V::ResT) ~> V::ResT -/*@ Desugars compound assign into the underlying operator + assign. +/*@ +Desugars compound assign into the underlying operator + assign. +*/ + +/*Could probably be done during elaboration, this way (not done this way currently!): - Question: Why not during elaboration phase? - Answer: - in the LHS of => location L is referred once - in the RHS of => it is referred twice - - at elaboration phase we would have to rewrite the original expresion that produces L - from one occurence to two occuences. + - at elaboration phase we would have to rewrite the original expresion that produces L from one occurence to two occuences. - if operator LHS expression has side effects, we would end up with the side effect twice. - - Example: v[i++] += 1*/ + - Example: v[i++] += 1 +*/ rule loc(L:Int) :: T:Type *= Exp2:K => loc(L)::T = cast(T, lookup(L, T) * Exp2) rule loc(L:Int) :: T:Type /= Exp2:K => loc(L)::T = cast(T, lookup(L, T) / Exp2) @@ -171,21 +185,21 @@ rule loc(L:Int) :: T:Type &= Exp2:K => loc(L)::T = cast(T, lookup(L, T) & Exp2) rule loc(L:Int) :: T:Type ^= Exp2:K => loc(L)::T = cast(T, lookup(L, T) ^ Exp2) rule loc(L:Int) :: T:Type |= Exp2:K => loc(L)::T = cast(T, lookup(L, T) | Exp2) -/*@ \subsection{primitive types cast} */ +/*@ \subsection{Cast operator --- primitive types} */ //@ The type of RV could either be NumericType or tempType. This rule matches both. rule [cast-Number]: cast(NT:NumericType, RV:RawVal::_) => normalize(RV::NT) rule [cast-Bool]: cast(bool, B:Bool::bool) => B::bool -/*@ \subsubsection{artificial cases of cast, arised during semantics separation} */ +/*@ \subsubsection{Artificial cases of cast, arised during semantics separation} */ rule [cast-void]: cast(void, RV:RawVal::void) => RV::void //Happens for the qualifier of a static method call rule [cast-noValue]: cast(_, noValue) => noValue -/*@ \subsection{lvalue semantics} */ +/*@ \subsection{Heating/cooling rules for lvalue} */ /* We cannot use context rules here because of wrapper-related limitations. If a term is wrapped into lvalue during heating by a context rule, it will be cooled also from lvalue by the cooling rule. This is unacceptable @@ -243,26 +257,4 @@ rule [lvalue-Throw-desugar]: lvalue( throw E:Exp; ) => throw E; [structural] -syntax KItem ::= store ( - Int, //OL - the store location - K //evaluates to TypedVal - the value to be stored - ) [strict(2)] - -//@ Synchronization checkpoint have to be before the actual assignment, like for lookup. -rule [store]: - store(L:Int, V:RawVal :: T:Type) => fieldAccessCheckpoint(L) ~> storeImpl(L, V::T) - -syntax KItem ::= storeImpl ( - Int, //OL - the store location - K //TypedVal - the value to be stored - ) - -rule [storeImpl]: - storeImpl(L:Int, V:RawVal :: T:Type) => . ... - ... L |-> (_ => V) :: T ... - -/*@ \subsection{auxiliary terms produced during elaboration} */ - -rule stmtAndExp(Stmt:K, Exp:K) => Stmt ~> Exp - endmodule diff --git a/src/exec/java-exec.k b/src/exec/java-exec.k index 4f40acb9..0815e382 100644 --- a/src/exec/java-exec.k +++ b/src/exec/java-exec.k @@ -7,6 +7,7 @@ require "../common/core-functions.k" require "../common/primitive-types.k" require "../common/subtyping.k" require "../common/java-syntax.k" +require "../common/sort-predicate-hacks.k" require "core-exec.k" require "syntax-conversions.k" require "to-string.k" @@ -44,5 +45,6 @@ module JAVA-EXEC imports API-THREADS // imports LTL-SUPPORT imports JAVA-SYNTAX + imports SORT-PREDICATE-HACKS endmodule diff --git a/src/exec/ltl-support.k b/src/exec/ltl-support.k index fb519405..48eccf48 100644 --- a/src/exec/ltl-support.k +++ b/src/exec/ltl-support.k @@ -1,9 +1,9 @@ require "builtins/model-checker.k" -require "../common/shared-syntax.k" +require "../common/java-syntax.k" module LTL-SUPPORT-SYNTAX imports SYNTAX-CONVERSIONS - imports SHARED-SYNTAX + imports JAVA-SYNTAX syntax Prop ::= Exp diff --git a/src/exec/method-invoke.k b/src/exec/method-invoke.k index cf2b7a13..94ba7d47 100644 --- a/src/exec/method-invoke.k +++ b/src/exec/method-invoke.k @@ -7,8 +7,7 @@ module METHOD-INVOKE /*@ \subsection{Background} -In this section we present the fragment of configuration used by runtime method - invocation. The figure below contains the cells and their sorts\footnote{$AM^{***}$ = \sortName{AccessMode}, $CT^{***}$ = \sortName{ContextType}}. +In this section we present the fragment of configuration used by runtime method invocation. The figure below contains the cells and their sorts\footnote{$AM^{***}$ = \sortName{AccessMode}, $CT^{***}$ = \sortName{ContextType}}. \vspace{3ex} @@ -60,80 +59,45 @@ In this section we present the fragment of configuration used by runtime method \vspace{3ex} -The cell \cellref[]{k} stores the current computation. The cell \cellref[]{stack} is a list of pairs of the - form (K, Bag), and represents the standard method call stack. The first element - represents the remaining computation at the moment the method was called. The second - element of sort Bag represents the content of cell \cellref[]{methodContext} at the moment - of method call. - -The cell \cellref[]{class} contains various sub-cells holding the content of that class. The - first cell in \cellref[]{classType} of sort ClassType that holds the fully qualified class name. - This cell serves as a key in all rules that match a fragment of a \cellref[]{class}. The value - in the cell \cellref[]{classMetaType} is either "class" or "interface". From now on we will - refer to both meta types as classes, referring to metatype value when distinction - is necessary. The next cell is \cellref[]{methods}. This is a map from method signatures to - classes where the respective signatures are declared. It contains not only the methods - declared in this class, but also those inherited from the base class, but not from the - base interfaces. By "inherited" here we mean all the methods contained in the cell - \cellref[]{methods} of the base class that were not overridden by a method declaration with - the same signature in the current class. This definition is different from the - inheritance rules in JLS \S8.4.6, although the difference is only relevant at the - elaboration time. - -The cell \cellref[]{methodDec} represents a method declared inside the current class. The subcell - \cellref[]{methodSignature} is the key for accessing other cells for this declaration. The other - cells are the parameters, the body, the access mode (private, public etc.) and the - context type (either instance or static). - -In order for strictness and context rules to work we have to define some K productions - as KResult. The most common forms of KResult in Java are the following: +The cell \cellref[]{k} stores the current computation. The cell \cellref[]{stack} is a list of pairs of the form (K, Bag), and represents the standard method call stack. The first element represents the remaining computation at the moment the method was called. The second element of sort Bag represents the content of cell \cellref[]{methodContext} at the moment of method call. -\vspace{3ex} +The cell \cellref[]{class} contains various sub-cells holding the content of that class. The first cell in \cellref[]{classType} of sort ClassType that holds the fully qualified class name. This cell serves as a key in all rules that match a fragment of a \cellref[]{class}. The value in the cell \cellref[]{classMetaType} is either "class" or "interface". From now on we will refer to both meta types as classes, referring to metatype value when distinction is necessary. The next cell is \cellref[]{methods}. This is a map from method signatures to classes where the respective signatures are declared. It contains not only the methods declared in this class, but also those inherited from the base class, but not from the base interfaces. By "inherited" here we mean all the methods contained in the cell \cellref[]{methods} of the base class that were not overridden by a method declaration with the same signature in the current class. This definition is different from the inheritance rules in JLS \S8.4.6, although the difference is only relevant at the elaboration time. + +The cell \cellref[]{methodDec} represents a method declared inside the current class. The subcell \cellref[]{methodSignature} is the key for accessing other cells for this declaration. The other cells are the parameters, the body, the access mode (private, public etc.) and the context type (either instance or static). + +In order for strictness and context rules to work we have to define some K productions as KResult. The most common forms of KResult in Java are the following: -\begin{syntaxBlock}{\nonTerminal{\sort{KResult}}} -\syntax{{\nonTerminal{\sort{ClassType}}}}{} -\syntaxCont{{\nonTerminal{\sort{TypedVal}}}}{} +\begin{syntaxBlock}{KResult} + \syntax{{\nonTerminal{\sort{ClassType}}}}{} + \syntaxCont{{\nonTerminal{\sort{TypedVal}}}}{} \end{syntaxBlock} The first represents a class. Second is a typed value, the result of evaluation of any expression. The forms of typed values relevant for method invocation are object reference and null: -\vspace{3ex} - -\begin{syntaxBlock}{\nonTerminal{\sort{TypedVal}}}\syntax{{}\terminal{objectRef} - ({{\nonTerminal{\sort{Int}}}},{{\nonTerminal{\sort{ClassType}}}}){} - \terminal{::}{{\nonTerminal{\sort{ClassType}}}}}{}\syntaxCont{{}\terminal{null} - {}\terminal{::}{{\nonTerminal{\sort{ClassType}}}}}{} +\begin{syntaxBlock}{TypedVal} + \syntax{\terminal{objectRef} + ({{\nonTerminal{\sort{Int}}}},{{\nonTerminal{\sort{ClassType}}}}){} + \terminal{::}{{\nonTerminal{\sort{ClassType}}}}}{}\syntaxCont{{}\terminal{null} + {}\terminal{::}{{\nonTerminal{\sort{ClassType}}}}}{} \end{syntaxBlock} -The type after four dots (::) separator is the static type associated with that value. The values inside - objectRef() are the address inside the store and the runtime type of the object. +The type after four dots (::) separator is the static type associated with that value. The values inside \verb|objectRef()| are the address inside the store and the runtime type of the object. -For the sake of simplicity we we will also - consider \dotCt{K} - the unit element of K to be KResult. The value \dotCt{K} is often - used in auxiliary functions as a placeholder until some actual value is computed. +For the sake of simplicity we we will also consider \dotCt{K} --- the unit element of K to be KResult. The value \dotCt{K} is often used in auxiliary functions as a placeholder until some actual value is computed. \subsection{Introduction} \begin{markdown} An elaborated method invocation expression may have one of the following forms: - - An invocation of a static method qualified by its class: Class.f(args) - - An invocation of a static method qualified by an expression producing an object: - o.f(args). Even if the method is - static we cannot simply replace the qualifier with its compile-time type at - elaboration phase, because the qualifier - expression still has to be evaluated and might produce side effects. We cannot replace it with - o; class.f(args); either, because o; might be invalid. Not all expressions - valid as qualifiers are valid as expression statements (JLS \S14.8). We wanted the elaboration - result to be a valid Java program, thus we could not afford such a transformation. + - An invocation of a static method qualified by its class: \verb|Class.f(args)| + - An invocation of a static method qualified by an expression producing an object: \verb|o.f(args)|. Even if the method is static we cannot simply replace the qualifier with its compile-time type at elaboration phase, because the qualifier expression still has to be evaluated and might produce side effects. We cannot replace it with \verb|o; class.f(args);| either, because \verb|o;| might be invalid. Not all expressions valid as qualifiers are valid as expression statements (JLS \S14.8). We wanted the elaboration result to be a valid Java program, thus we could not afford such a transformation. - - An invocation of an instance method qualified by a class reference: o.f(args) - - An invocation of an instance method qualified by an interface reference: i.f(args) + - An invocation of an instance method qualified by a class reference: \verb|o.f(args)| + - An invocation of an instance method qualified by an interface reference: \verb|i.f(args)| -The evaluation of the method invocation expression consists from 5 steps outlined below. - Those steps, unless otherwise specified, are common to all the method call forms - enumerated above. +The evaluation of the method invocation expression consists from 5 steps outlined below. Those steps, unless otherwise specified, are common to all the method call forms enumerated above. 1. Evaluation of the qualifier expression 2. Evaluation of method arguments @@ -141,11 +105,7 @@ The evaluation of the method invocation expression consists from 5 steps outline 4. Locating the actual method declaration to be invoked 5. Actual method invocation. -In JLS runtime semantics of method invocation is described in \S15.2.4. Although there - is some correspondence between the steps in our semantics and the steps in JLS, it is - generally not one-to-one. JLS description of method invocation consists of the - following 5 steps. For each step we give the relevant chapter of the JLS and the step - in our semantics. +In JLS runtime semantics of method invocation is described in \S15.2.4. Although there is some correspondence between the steps in our semantics and the steps in JLS, it is generally not one-to-one. JLS description of method invocation consists of the following 5 steps. For each step we give the relevant chapter of the JLS and the step in our semantics. 1. Compute the target reference (\S15.12.4.1), semantics step 1 2. Evaluate arguments (\S15.12.4.2), semantics step 1 @@ -153,78 +113,54 @@ In JLS runtime semantics of method invocation is described in \S15.2.4. Although 4. Locate the actual method code to invoke (\S15.12.4.4), semantics step 3 5. Actual method invocation, semantics step 4. -Generally the rules of K-Java do not follow directly the wording of JLS. The reasons - for this will choice will be given at the end of the section. - The details related to each step are described in the semantics below, above each - rule and auxiliary construct. For each rule we will also refer to the respective - JLS page, if there is a correspondence. +Generally the rules of K-Java do not follow directly the wording of JLS. The reasons for this will choice will be given at the end of the section. The details related to each step are described in the semantics below, above each rule and auxiliary construct. For each rule we will also refer to the respective JLS page, if there is a correspondence. \end{markdown} */ /*@ \subsection{Evaluation of the qualifier and the arguments} -The first two parts of method invocation logic are evaluation of the qualifier expression and evaluation of the - arguments. JLS enforces the following conditions on the order of subexpressions evaluation: - - Arguments have to be evaluated after the qualifier was evaluated. This is ensured - by checking that the qualifier is of sort KResult at the moment when arguments are - heated. - - Arguments are evaluated left to right. To ensure this we add a side condition that - checks that all the arguments before the one being heated (if any) are already of the - sort KResult. +\begin{markdown} +The first two parts of method invocation logic are evaluation of the qualifier expression and evaluation of the arguments. JLS enforces the following conditions on the order of subexpressions evaluation: -While there are two sections dedicated to this logic (\S15.12.4.1, \S15.12.4.2), we don't need any K rules - for it. Instead, subexpressions evaluation ensured by strictness annotations - that accompany the following syntax definitions: + - Arguments have to be evaluated after the qualifier was evaluated. This is ensured by checking that the qualifier is of sort KResult at the moment when arguments are heated. + - Arguments are evaluated left to right. To ensure this we add a side condition that checks that all the arguments before the one being heated (if any) are already of the sort KResult. +\end{markdown} -\vspace{3ex} +While there are two sections dedicated to this logic (\S15.12.4.1, \S15.12.4.2), we don't need any K rules for it. Instead, subexpressions evaluation ensured by strictness annotations that accompany the following syntax definitions: -\begin{syntaxBlock}{ - \nonTerminal{\sort{Exp}}}\syntax{{{\nonTerminal{\sort{K}}}}\terminal{.}{{\nonTerminal{\sort{MethodName}}}} - ({{\nonTerminal{\sort{Exps}}}})}{\kattribute{seqstrict}(1,3)} +\begin{syntaxBlock}{Exp} + \syntax{{{\nonTerminal{\sort{K}}}}\terminal{.}{{\nonTerminal{\sort{MethodName}}}} + ({{\nonTerminal{\sort{Exps}}}})}{\kattribute{seqstrict}(1,3)} \end{syntaxBlock} -\begin{syntaxBlock}{ - \nonTerminal{\sort{MethodName}}}\syntax{{\nonTerminal{\sort{Id}}}}{} +\begin{syntaxBlock}{MethodName} + \syntax{{\nonTerminal{\sort{Id}}}}{} \end{syntaxBlock} -\begin{syntaxBlock}{ - \nonTerminal{\sort{Exps}}}\syntax{List\{{\nonTerminal{\sort{Exp}}}, \mbox{``},\mbox{''}\}}{\kattribute{seqstrict}} +\begin{syntaxBlock}{Exps} + \syntax{List\{{\nonTerminal{\sort{Exp}}}, \mbox{``},\mbox{''}\}}{\kattribute{seqstrict}} \end{syntaxBlock} -The annotation {\kattribute{seqstrict}(1,3)} on the first definition ensures that arguments are evaluated after the - qualifier is evaluated. The qualifier term might be either an expression or a Class. If it is expression, - it will be heated and evaluated. If it is a class (for certain static methods), then it is already a KResult - strictness rule will have no effect on it. -Note that arguments have to be evaluated even in the case when the qualifier evaluated to null. At the same time - that if evaluation of the qualifier or any of the arguments - completes abruptly, the whole method invocation expression completes abruptly for the - same reason. K-Java does not need any special rules to cover those cases. The semantics has a fixed number of rules - for throw statement that ensure the correct propagation of exceptions from any context. +The annotation {\kattribute{seqstrict}(1,3)} on the first definition ensures that arguments are evaluated after the qualifier is evaluated. The qualifier term might be either an expression or a Class. If it is expression, it will be heated and evaluated. If it is a class (for certain static methods), then it is already a KResult strictness rule will have no effect on it. + +Note that arguments have to be evaluated even in the case when the qualifier evaluated to null. At the same time that if evaluation of the qualifier or any of the arguments completes abruptly, the whole method invocation expression completes abruptly for the same reason. K-Java does not need any special rules to cover those cases. The semantics has a fixed number of rules for throw statement that ensure the correct propagation of exceptions from any context. */ /*@ \subsection{Loading method information} \begin{markdown} -During the second step of the method invocation the second argument of the production is replaced with the - auxiliary data - structure methodInfo(). This data structure contains the information required to choose the right method lookup - strategy at the next step. The production methodInfo() contains the following arguments: - - - Method signature Sig - - Qualifying class QualC of the method invocation, e.g. the compile-time type of the qualifier. - - The meta type of QualC - MetaT. It may have one of the two values - class or interface. - - DecC - declaring class, the class where the method was actually declared, as observed by QualT. - E.g. the most derived class in QualC hierarchy where there is a declaration of a method with signature Sig. - - ContextT - the context type of the method. Either static, for static methods, or instance for non-static methods. - - Acc - access modifier (private, package, protected or public). For the purpose of uniformity we use the modifier - package when no access modifier is provided. - -All the information stored in methodInfo() is static. In K-Java we already have - this information computed, but it is stored in various cells inside \cellref[]{class} and \cellref[]{classDec}. - The rules from step 3 simply load the relevant information from configuration - cells to methodInfo() arguments. +During the second step of the method invocation the second argument of the production is replaced with the auxiliary data structure \verb|methodInfo()|. This data structure contains the information required to choose the right method lookup strategy at the next step. The production \verb|methodInfo()| contains the following arguments: + + - Method signature \verb|Sig| + - Qualifying class \verb|QualC| of the method invocation, e.g. the compile-time type of the qualifier. + - The meta type of \verb|QualC| --- \verb|MetaT|. It may have one of the two values - class or interface. + - \verb|DecC| --- declaring class, the class where the method was actually declared, as observed by \verb|QualT|. E.g. the most derived class in \verb|QualC| hierarchy where there is a declaration of a method with signature \verb|Sig|. + - \verb|ContextT| --- the context type of the method. Either static, for static methods, or instance for non-static methods. + - \verb|Acc| --- access modifier (private, package, protected or public). For the purpose of uniformity we use the modifier package when no access modifier is provided. + +All the information stored in \verb|methodInfo()| is static. In K-Java we already have this information computed, but it is stored in various cells inside \cellref[]{class} and \cellref[]{classDec}. The rules from step 3 simply load the relevant information from configuration cells to \verb|methodInfo()| arguments. \end{markdown} */ syntax MethodName ::= methodInfo( Signature, //Sig - method signature @@ -239,11 +175,7 @@ syntax MethodName ::= methodInfo( ) /*@ -The first rule from this step rewrites the method name into a methodInfo() term whose first argument is the method -signature. - The auxiliary function getTypes() computes the list of types from the list of parameter declarations. The second - argument of methodInfo() is also computed at this step - it is the type of the qualifier. The rest of the arguments - are filled in with default values. They will be rewritten into actual values by the following rules. +The first rule from this step rewrites the method name into a \verb|methodInfo()| term whose first argument is the method signature. The auxiliary function \verb|getTypes()| computes the list of types from the list of parameter declarations. The second argument of \verb|methodInfo()| is also computed at this step --- it is the type of the qualifier. The rest of the arguments are filled in with default values. They will be rewritten into actual values by the following rules. */ rule [Invoke-compute-methodInfo-Signature]: Qual:KResult @@ -251,29 +183,23 @@ rule [Invoke-compute-methodInfo-Signature]: (Args:TypedVals) /*@ -Note that in this rule variable Args is defined of type TypedVals instead of Exps. This restriction ensures that - arguments (and consequently the qualifier) are already evaluated at the moment when this rule is invoked. - The sort TypedVals represents a list of typed values, the evaluation result of Exps. It is defined as following: - -\vspace{3ex} +Note that in this rule variable Args is defined of type TypedVals instead of Exps. This restriction ensures that arguments (and consequently the qualifier) are already evaluated at the moment when this rule is invoked. The sort TypedVals represents a list of typed values, the evaluation result of Exps. It is defined as following: -\begin{syntaxBlock}{ - \nonTerminal{\sort{TypedVals}}}\syntax{List\{{\nonTerminal{\sort{TypedVal}}}, \mbox{``},\mbox{''}\}}{} +\begin{syntaxBlock}{TypedVals} + \syntax{List\{{\nonTerminal{\sort{TypedVal}}}, \mbox{``},\mbox{''}\}}{} \end{syntaxBlock} -\begin{syntaxBlock}{ - \nonTerminal{\sort{Exps}}}\syntax{{\nonTerminal{\sort{TypedVals}}}}{} +\begin{syntaxBlock}{Exps} + \syntax{{\nonTerminal{\sort{TypedVals}}}}{} \end{syntaxBlock} Because TypedVal is subsorted to KResult, TypedVals being a list of KResult is implicitly subsorted to KResult. */ -/* Impl: We could combine this rule with the previous one by using getLookupTargetType(), but we'll keep it this way - to keep the core part of method invocation separate from the non object-related part. */ +/* Impl: We could combine this rule with the previous one by using \verb|getLookupTargetType()|, but we'll keep it this way to keep the core part of method invocation separate from the non object-related part. */ /*@ -The second rule for method invocation loads MetaT and DecC. It requires Sig and QualC computed by the previous rule. - +The second rule for method invocation loads \verb|MetaT| and \verb|DecC|. It requires \verb|Sig| and \verb|QualC| computed by the previous rule. */ rule [Invoke-compute-methodInfo-DecC]: @@ -285,16 +211,12 @@ rule [Invoke-compute-methodInfo-DecC]: ... Sig |-> DecC:ClassType ... /*@ \begin{markdown} -There is one case that is not covered by the previous rule - the case when the cell \cellref[]{methods} does not have a key - equal to Sig. This is possible in one of the following situations: +There is one case that is not covered by the previous rule --- the case when the cell \cellref[]{methods} does not have a key equal to \verb|Sig|. This is possible in one of the following situations: - Qualifying type is an interface. - - Qualifying type is an abstract class. The called method is inherited from an interface but is not declared neither - in this class nor in its base classes. + - Qualifying type is an abstract class. The called method is inherited from an interface but is not declared neither in this class nor in its base classes. -In both cases the method is an abstract method in the class QualT. For this case DecC cannot be computed, but we know - for sure that ContextT for an abstract method is instance. Also, because the method was declared in an interface, - it is certainly public. +In both cases the method is an abstract method in the class \verb|QualT|. For this case \verb|DecC| cannot be computed, but we know for sure that \verb|ContextT| for an abstract method is instance. Also, because the method was declared in an interface, it is certainly public. \end{markdown} */ rule [Invoke-compute-methodInfo-unmapped-method-ContextType]: @@ -308,7 +230,7 @@ when notBool Sig in keys(Methods) /*@ -The last rule of step 3 loads ContextT and Acc. It requires DecC, so this rule may only match after the second rule for methodInfo(). +The last rule of step 3 loads \verb|ContextT| and \verb|Acc|. It requires \verb|DecC|, so this rule may only match after the second rule for \verb|methodInfo()|. */ rule [Invoke-compute-methodInfo-ContextType]: @@ -323,33 +245,25 @@ rule [Invoke-compute-methodInfo-ContextType]: /*@ \subsection{Lookup method declaration} -In the third step of the method invocation algorithm, the actual method declaration is chosen. This step starts once all - the fields of methodInfo() were filled in (where possible). The rules of this step rewrite methodInfo() into - methodRef() - another auxiliary data structure. -The production methodRef() is a reference to a method declaration. It contains two fields - Sig and DecC - the - signature and the declaration class. The implementation class is the class that contains the actual method - declaration to be invoked. +In the third step of the method invocation algorithm, the actual method declaration is chosen. This step starts once all the fields of \verb|methodInfo()| were filled in (where possible). The rules of this step rewrite \verb|methodInfo()| into \verb|methodRef()| --- another auxiliary data structure. +The production \verb|methodRef()| is a reference to a method declaration. It contains two fields --- \verb|Sig| and \verb|DecC| --- the signature and the declaration class. The implementation class is the class that contains the actual method declaration to be invoked. -\vspace{3ex} - -\begin{syntaxBlock}{ - \nonTerminal{\sort{MethodName}}}\syntax{{}\terminal{methodRef}({{\nonTerminal{\sort{Signature}}}},{{\nonTerminal{\sort{RefType}}}})}{} +\begin{syntaxBlock}{MethodName} + \syntax{{}\terminal{methodRef}({{\nonTerminal{\sort{Signature}}}},{{\nonTerminal{\sort{RefType}}}})}{} \end{syntaxBlock} \begin{markdown} -Since we already know the signature, this phase amounts to computing DecC. This step contains different rules for the following cases: +Since we already know the signature, this phase amounts to computing \verb|DecC|. This step contains different rules for the following cases: - Static method (JLS \S15.12.4.4 paragraph 2) - Instance method with target being null (JLS \S15.12.4.4 paragraph 3) - Instance method with non-null target, private method (JLS \S15.12.4.4 paragraph 4) - - Instance method with non-null target, access mode is protected or public. This also includes qualifying type - being interface. (JLS \S15.12.4.4 paragraph 6 and point 1) + - Instance method with non-null target, access mode is protected or public. This also includes qualifying type being interface. (JLS \S15.12.4.4 paragraph 6 and point 1) - Instance method with non-null target, access mode is package (no dedicated mention in JLS \S15.12.4.4) -The method below is for the first case. If the method is static, then the declaring type DecC is the qualifying type. - The qualifier is discarded by rewriting it into \dotCt{K} . +The method below is for the first case. If the method is static, then the declaring type \verb|DecC| is the qualifying type. The qualifier is discarded by rewriting it into \dotCt{K} . \end{markdown} */ rule [Invoke-methodInfo-static]: @@ -358,9 +272,7 @@ rule [Invoke-methodInfo-static]: (_) /*@ -If the qualifier value is null and ContextT is instance, then NullPointerException is thrown and method invocation - expression is discarded. It is only at this point that we should check the qualifier whether it is null or not. - If ContextT is static, then the previous rule will match, and no exception will be thrown. +If the qualifier value is null and \verb|ContextT| is instance, then NullPointerException is thrown and method invocation expression is discarded. It is only at this point that we should check the qualifier whether it is null or not. If \verb|ContextT| is static, then the previous rule will match, and no exception will be thrown. */ rule [Invoke-methodInfo-instance-on-null]: /* [Impl] Qualifier type could be either object or array. @@ -379,14 +291,7 @@ rule [Invoke-methodInfo-instance-private]: (_) /*@ -If the method is protected or public, then we should call the version of the method visible to the runtime type of - the qualifying object (ObjC). Recall that the runtime type of an object is stored in the second argument of - objectRef(). - This case also covers qualifying type interface, since interface methods are always public. - The right method will always be the one referred by the signature Sig in the cell \cellref[]{methods} associated with the - actual object class. This is because the unfolding phase populates \cellref[]{methods} with the union of methods inherited - from the base class and methods declared in the current class, the latter overriding the former. - The variable DecC is the class where the right method version is declared. +If the method is protected or public, then we should call the version of the method visible to the runtime type of the qualifying object (\verb|ObjC|). Recall that the runtime type of an object is stored in the second argument of \verb|objectRef()|. This case also covers qualifying type interface, since interface methods are always public. The right method will always be the one referred by the signature \verb|Sig| in the cell \cellref[]{methods} associated with the actual object class. This is because the unfolding phase populates \cellref[]{methods} with the union of methods inherited from the base class and methods declared in the current class, the latter overriding the former. The variable \verb|DecC| is the class where the right method version is declared. */ rule [Invoke-methodInfo-instance-protected-or-public]: @@ -402,22 +307,19 @@ when /*@ \begin{markdown} -The most complex case is for instance methods with package access mode. The precise semantics of overriding for all - access modes is defined in JLS \S8.4.6.1: +The most complex case is for instance methods with package access mode. The precise semantics of overriding for all access modes is defined in JLS \S8.4.6.1: -An instance method derivedM declared in a class Derived overrides another method with the - same signature, baseM, declared in class Base iff both: +An instance method derivedM declared in a class Derived overrides another method with the same signature, baseM, declared in class Base iff both: 1. Derived is a subclass of Base. 2. Either - a. baseM is public, protected, or declared with package access in the same package as derivedM - b. derivedM overrides a method middleM, middleM distinct from baseM and derivedM, - such that middleM overrides baseM + a. baseM is public, protected, or declared with package access in the same package as derivedM. + b. derivedM overrides a method middleM, middleM distinct from baseM and derivedM, such that middleM overrides baseM. The transitive rule for overriding relation (2b) is required specifically for package access mode. Consider the following example: \end{markdown} -\begin{minipage}{\textwidth} +\begin{minipage}{\textwidth-\parindent} \begin{lstlisting} package a; public class A { @@ -441,32 +343,20 @@ public class C extends B { \medskip -The method in class C overrides the method in class A transitively through the method in B. There is no direct - overriding between A and C, because the method is declared with default (package) access mode in A, and class C is - in a different package. Note that if the access mode in B would have been package instead of protected, - there would be no overriding. +The method in class C overrides the method in class A transitively through the method in B. There is no direct overriding between A and C, because the method is declared with default (package) access mode in A, and class C is in a different package. Note that if the access mode in B would have been package instead of protected, there would be no overriding. + +In order to correctly handle such cases we have to analyse all the classes in the inheritance chain between the qualifying type and the qualifier runtime type. + +The algorithm employed in K-Java is significantly different from the one in JLS, but it is much simpler to implement. Yet it yields the correct behaviour and was extensively tested by our test suite. The JLS algorithm involves starting the search from the runtime type of the qualifier and moving upwards in the inheritance tree until we find the FIRST method that overrides the originally called method (or is the originally called method itself). This apparently simple algorithm leads to multiple particular cases when we consider the transitive rule (2b above) for overriding. + +In contrast, the K-Java algorithm starts the search with the qualifying type (e.g. static type of the qualifier expression) and moves downwards in the inheritance chain until it reaches the runtime type of the qualifier. When all classes in the chain were traversed the algorithm returns the LAST found method (e.g. defined in the most derived class) that overrides the original one. + +The rule for package access mode delegates searching for the right method declaration to the auxiliary function \verb|lookupPackageMethod()|. The function takes 3 arguments: \begin{markdown} -In order to correctly handle such cases we have to analyse all the classes in the inheritance chain between the - qualifying type and the qualifier runtime type. - -The algorithm employed in K-Java is significantly different from the one in JLS, but it is much simpler to implement. - Yet it yields the correct behaviour and was extensively tested by our test suite. The JLS algorithm involves starting - the search from the runtime type of the qualifier and moving upwards in the inheritance tree until we find the FIRST - method that overrides the originally called method (or is the originally called method itself). This apparently - simple algorithm leads to multiple particular cases when we consider the transitive rule (2b above) for overriding. - -In contrast, the K-Java algorithm starts the search with the qualifying type (e.g. static type of the qualifier - expression) and moves downwards in the inheritance chain until it reaches the runtime type of the qualifier. - When all classes in the chain were traversed the algorithm returns the LAST found method (e.g. defined in the most - derived class) that overrides the original one. - -The rule for package access mode delegates searching for the right method declaration to the auxiliary function - lookupPackageMethod(). The function takes 3 arguments: - - - method signature Sig - - the list of classes in the inheritance chain between the qualifying class QualC and the actual object class ObjC. - This list is produced by classChain() + - method signature \verb|Sig| + - the list of classes in the inheritance chain between the qualifying class \verb|QualC| and the actual object class \verb|ObjC|. + This list is produced by \verb|classChain()| - the third argument represents the declaring class of the best method found so far. It is initialized with \dotCt{K}. \end{markdown} @@ -484,29 +374,23 @@ rule [Invoke-methodInfo-instance-package]: ... Sig |-> _ ... /*@ -Before the evaluation of lookupPackageMethod() may begin, the term lookupPackageMethod() has to be heated to the top - of computation. The side condition in the context rule below ensured that the second argument of method call - expression is heated only if it contains a term lookupPackageMethod(). If it has other forms, - such as the method name or methodInfo(), it won't be heated. +Before the evaluation of \verb|lookupPackageMethod()| may begin, the term \verb|lookupPackageMethod()| has to be heated to the top of computation. The side condition in the context rule below ensured that the second argument of method call expression is heated only if it contains a term \verb|lookupPackageMethod()|. If it has other forms, such as the method name or \verb|methodInfo()|, it won't be heated. */ context _:K . HOLE (_) when getKLabel(HOLE) ==KLabel 'lookupPackageMethod -/* -Returns the list of classes representing the layer of the given object (by OId), - located between MostBaseClass (exclusively) and MostDerivedClass (inclusively). +/*@ +Returns the list of classes representing the layer of the given object (by OId), located between MostBaseClass (exclusively) and MostDerivedClass (inclusively). */ syntax KItem ::= getClassChain( ClassType, //MostBaseClass ClassTypes //MostDerivedClass at beginning, gradually accumulates //the list of classes ) -/* [Skip] The right signature is already found. -Search for the right implementation is performed from the compile-time type of the target -to more derived types, up to the object type of the target. -This is required in order to respect the rules of inheritance in the presence of access modes. -Evaluates into typed method closure.*/ +/*@ +The right signature is already found. Search for the right implementation is performed from the compile-time type of the target to more derived types, up to the object type of the target. This is required in order to respect the rules of inheritance in the presence of access modes. Evaluates into typed method closure. +*/ syntax KItem ::= lookupPackageMethod ( Signature, //sig(Name, SigTL) - Method signature ClassTypes, //computes Class,... , list of elements of type ClassType, @@ -520,22 +404,14 @@ syntax KItem ::= lookupPackageMethod ( /*@ \begin{markdown} -The rules for lookupPackageMethod() are based on the following two properties of the configuration: - - - if the cell \cellref[]{methods} for a particular class contains a key Sig, then \cellref[]{methods} for all classes derived from it - will contain the key Sig. - - if a particular class contain a method declaration with signature Sig access mode Acc, then all declarations - of Sig in derived classes (that are not necessarily overriding!) will have the access mode equal to either Acc or a - value wider than Acc. - -The first property is ensured by the unfolding algorithm. Because \cellref[]{methods} of a derived class inherit all the \cellref[]{methods} - of the direct base class, the map \cellref[]{methods} may only grow from base classes to derived. The second property is ensured - by restrictions on overriding specified in JLS \S8.4.8.3: "The access modifier (\S6.6) of an overriding or hiding - method must provide at least as much access as the overridden or hidden method". - -The search for the right package method declaration is performed from the base-most class in the chain (the left-most - one) to the most derived one. Every rule matches and deletes the leftmost class in the class chain (CurrentC), - and possibly rewrites the third argument into the current class. +The rules for \verb|lookupPackageMethod()| are based on the following two properties of the configuration: + + - if the cell \cellref[]{methods} for a particular class contains a key \verb|Sig|, then \cellref[]{methods} for all classes derived from it will contain the key \verb|Sig|. + - if a particular class contain a method declaration with signature \verb|Sig| access mode \verb|Acc|, then all declarations of \verb|Sig| in derived classes (that are not necessarily overriding!) will have the access mode equal to either \verb|Acc| or a value wider than \verb|Acc|. + +The first property is ensured by the unfolding algorithm. Because \cellref[]{methods} of a derived class inherit all the \cellref[]{methods} of the direct base class, the map \cellref[]{methods} may only grow from base classes to derived. The second property is ensured by restrictions on overriding specified in JLS \S8.4.8.3: "The access modifier (\S6.6) of an overriding or hiding method must provide at least as much access as the overridden or hidden method". + +The search for the right package method declaration is performed from the base-most class in the chain (the left-most one) to the most derived one. Every rule matches and deletes the leftmost class in the class chain (\verb|CurrentC|), and possibly rewrites the third argument into the current class. The first rule matches when there is no declaring class yet (third argument is \dotCt{K}, the initial case). \end{markdown} */ @@ -552,16 +428,14 @@ rule [lookupPackageMethod-layer-first-dec-found]: ... Sig |-> DecC:ClassType ... /*@ -The second rule matches when we already found a declaring class (OldDecC) and the current class CurrentC has another - method declaration with the right signature. The presence of a declaration with signature Sig inside CurrentC is identified by the - match $\mathrel{}\kall{class}{\kall{classType}{ CurrentC } \mathrel{}\kall{methods}{... Sig \mapsto CurrentC ...} }$, - according to the definition of \cellref[]{methods}. +The second rule matches when we already found a declaring class (\verb|OldDecC|) and the current class \verb|CurrentC| has another method declaration with the right signature. The presence of a declaration with signature \verb|Sig| inside \verb|CurrentC| is identified by the match $\kall{class}{\kall{classType}{ CurrentC } \mathrel{} \kmiddle{methods}{ Sig \mapsto CurrentC } }$, according to the definition of \cellref[]{methods}. + +If the method in \verb|CurrentC| directly overrides the method in \verb|OldDecC|, the declaring class is updated to \verb|CurrentC|. Otherwise the declaring class stays unchanged. The rules for direct overriding (case 1a above) are defined in the auxiliary function \verb|isOverridden()|. The function takes 3 arguments: -If the method in CurrentC directly overrides the method in OldDecC, the declaring class is updated to CurrentC. Otherwise the declaring class stays unchanged. The rules for direct overriding (case 1a above) are defined in the auxiliary function isOverridden(). The function takes three arguments: \begin{markdown} - - The base class OldDecC - - The derived class CurrentC - - The access mode Acc of the definition of Sig in OldDecC. + - The base class \verb|OldDecC| + - The derived class \verb|CurrentC| + - The access mode \verb|Acc| of the definition of \verb|Sig| in \verb|OldDecC|. \end{markdown} */ rule [lookupPackageMethod-new-method]: @@ -585,13 +459,16 @@ rule [lookupPackageMethod-new-method]: ... -/* -Tests if a method declared in class BaseC with access mode Acc is overridden by a method - with the same signature declared in a subclass SubC. +/*@ +\begin{markdown} +Tests if a method declared in class \verb|BaseC| with access mode \verb|Acc| is overridden by a method with the same signature declared in a subclass \verb|SubC|. The method is overridden if either: - - Acc is protected or public - - Acc is package and BaseC and SubC are declared in the same package (JLS \S6.6) + + - \verb|Acc| is protected or public + - \verb|Acc| is package and \verb|BaseC| and \verb|SubC| are declared in the same package (JLS \S6.6) + +\end{markdown} */ syntax KItem ::= isOverridden ( ClassType, //BaseC @@ -609,9 +486,7 @@ rule isOverridden(BaseC:ClassType, package, SubC:ClassType) rule isOverridden(_, private, _) => false /*@ -The third rule represents the case when CurrentC chain does not contain method declarations with signature - Sig. This case is identified by the side condition CurrentC =/=K DecC. Indeed, the two classes are different only - when the entry Sig $\mapsto$ DecC in \cellref[]{methods} was inherited rather than produced by a method in CurrentC. +The third rule represents the case when \verb|CurrentC| chain does not contain method declarations with signature \verb|Sig|. This case is identified by the side condition \verb|CurrentC| =/=K \verb|DecC|. Indeed, the two classes are different only when the entry \verb|Sig| $\mapsto$ \verb|DecC| in \cellref[]{methods} was inherited rather than produced by a method in \verb|CurrentC|. */ rule [lookupPackageMethod-no-new-method]: @@ -628,15 +503,15 @@ when CurrentC =/=K DecC /*@ -The last rule matches when the chain of classes stored in the first argument remains empty. It rewrites the whole - lookupPackageMethod() into a reference to the method that has to be invoked. +The last rule matches when the chain of classes stored in the first argument remains empty. It rewrites the whole \verb|lookupPackageMethod()| into a reference to the method that has to be invoked. */ rule [lookupPackageMethod-end]: lookupPackageMethod( Sig:Signature, .ClassTypes, DecC:ClassType ) => methodRef(Sig, DecC) /*@ -For the code example above, the term lookupPackageMethod() will pass through the following forms during evaluation: +For the code example above, the term \verb|lookupPackageMethod()| will pass through the following forms during evaluation: +\vspace{3ex} \begin{tabular}{ | l | l | } \hline $\mathrel{}\kall{k}{ lookupPackageMethod(f(), (a.A, a.B, b.C), \dotCt{K}) ...}$ &\\ @@ -683,49 +558,31 @@ For the code example above, the term lookupPackageMethod() will pass through the \vspace{3ex} -When the term lookupPackageMethod() is first produced it takes as arguments the method signature (rendered here as f() - for convenience), the chain of classes from the qualifying class A to the runtime class C, - and \dotCt{K} as the third argument. Since the third argument is \dotCt{K} only the third rule can match. This rule deletes A - from the class chain and updates the third argument to the class that defines the version of f() accessible to A. - That class is A. For classes B and C the second rule for lookupMethodM() matches. In both cases the method f() - defined in B and C overrides the previously found one. In the first case classes the method B.f() overrides A.f() - because the access mode is package and both A and B are in the same package. In the second case C.f() - overrides B.f() because B.f() has protected access mode, and is thus always overridden. The final result of - method lookup procedure is the version of method f() declared in the class C. +When the term \verb|lookupPackageMethod()| is first produced it takes as arguments the method signature (rendered here as \verb|f()| for convenience), the chain of classes from the qualifying class A to the runtime class C, and \dotCt{K} as the third argument. Since the third argument is \dotCt{K} only the third rule can match. This rule deletes A from the class chain and updates the third argument to the class that defines the version of \verb|f()| accessible to A. That class is A. For classes B and C the second rule for \verb|lookupMethodM()| matches. In both cases the method \verb|f()| defined in B and C overrides the previously found one. In the first case classes the method \verb|B.f()| overrides \verb|A.f()| because the access mode is package and both A and B are in the same package. In the second case \verb|C.f()| overrides \verb|B.f()| because \verb|B.f()| has protected access mode, and is thus always overridden. The final result of method lookup procedure is the version of method \verb|f()| declared in the class C. */ /*@ \subsection{Actual method invocation} \begin{markdown} -The central rule of method invocation is matched when the second argument of method call expression reaches the form - methodRef(). This rule performs the following operations: +The central rule of method invocation is matched when the second argument of method call expression reaches the form \verb|methodRef()|. This rule performs the following operations: - - saves the rest of computation (RestK) and the content of \cellref[]{methodContext} as a new entry of the cell \cellref[]{stack} - This data is restored back by the rules for return statement. + - saves the rest of computation (\verb|RestK|) and the content of \cellref[]{methodContext} as a new entry of the cell \cellref[]{stack} This data is restored back by the rules for return statement. - Initializes the new method context. - The local variable environment \cellref[]{env} is emptied - current class \cellref[]{crntClass} is initialized to the class declaring the method - - object location \cellref[]{location} is initialized to the location of the qualifier object for instance methods, - or \dotCt{K} for static methods. The extraction of the location from the qualifier value is performed by the - function getOId(). + - object location \cellref[]{location} is initialized to the location of the qualifier object for instance methods, or \dotCt{K} for static methods. The extraction of the location from the qualifier value is performed by the function \verb|getOId()|. - Rewrites the method call expression into a sequence of four terms: - static initialization of the qualifying class - parameters initialization - actual method body - a return statement with no arguments after the method body. -The function staticInit() triggers static initialization of the qualifying class, if this class was not initialized yet. - Repeated calls of this function have no effect. Is required just for static methods and is described in JLS \S12.4. - For an instance method call, the qualifying class will always be initialized already, - so staticInit() will have no effect. +The function \verb|staticInit()| triggers static initialization of the qualifying class, if this class was not initialized yet. Repeated calls of this function have no effect. Is required just for static methods and is described in JLS \S12.4. For an instance method call, the qualifying class will always be initialized already, so \verb|staticInit()| will have no effect. -The function initParams() rewrites each parameter declaration into two statements. First is a local variable - declaration with that parameter name. The second is an assignment to that variable of the actual argument value. +The function \verb|initParams()| rewrites each parameter declaration into two statements. First is a local variable declaration with that parameter name. The second is an assignment to that variable of the actual argument value. -The return statement at the end ensures that there is a return statement on every execution path of the method. The - statement will only be useful for methods with return type void, as methods returning a value are required by JLS - to have an appropriate return statement on every return path. +The return statement at the end ensures that there is a return statement on every execution path of the method. The statement will only be useful for methods with return type void, as methods returning a value are required by JLS to have an appropriate return statement on every return path. \end{markdown} */ rule [Invoke-methodRef]: @@ -754,7 +611,7 @@ syntax KItem ::= getOId( K ) [function] rule getOId( objectRef(OId:Int,_)::_ ) => OId rule getOId( noValue ) => noValue -/* Binds a list of formal parameters to their values. Used by method calls and try-catch. +/*@ Binds a list of formal parameters to their values. Used by method calls and try-catch. */ syntax KItem ::= initParams ( Params, // {T:Type X:Id},... - parameter declarations TypedVals // values @@ -824,11 +681,12 @@ module METHOD-INVOKE-REST imports CORE-FUNCTIONS imports SYNTAX-CONVERSIONS imports METHOD-INVOKE +//@ The module contains additional semantics related to method invocation. -/* [Skip] -The next rule for method invocation is applied when the qualifier type is array. This array type is rewritten - into the auxiliary class ArrayImpl, that is used in K-Java to simulate method invocations over array objects. - This rule is required in order to minimize the number of particular cases involving arrays in the rules that follow. +//@ \subsection{Method information for arrays and strings} + +/*@ +The next rule for method invocation is applied when the qualifier type is array. This array type is rewritten into the auxiliary class \verb|ArrayImpl|, that is used in K-Java to simulate method invocations over array objects. This rule is required in order to minimize the number of particular cases involving arrays in the rules that follow. */ rule [Invoke-compute-methodInfo-arrays]: QualRV:RawVal :: (arrayOf T:Type => classArrayImpl) @@ -843,6 +701,8 @@ rule [Invoke-methodInfo-on-array-or-string]: when isArrayRef(QualRV) ==K true orBool isString(QualRV) ==K true +//@ \subsection{Superclass method access --- \texttt{A.super(...)}} + // 'QSuperMethod(Class:ClassType,, _:K,, Name:Id) rule [Invoke-QSuperMethod]: 'Invoke( @@ -851,7 +711,7 @@ rule [Invoke-QSuperMethod]: ),, _ ) -/* Elaboration result for super keyword in A.super.m() call. Have to be a typed expression. +/*@ Elaboration result for super keyword in A.\verb|super.m()| call. Have to be a typed expression. */ syntax MethodName ::= superMethodImpl ( K ) // is always equal to A.this - used to lookup the right qualifier closure. [strict] @@ -862,7 +722,7 @@ rule [superMethodImpl]: objectRef( OId:Int, //The layers above the layer where method should be searched - // should be discarded in order to implement super.m() functionality. + // should be discarded in order to implement \verb|super.m()| functionality. _ )::Class:ClassType //due to the way term superMethod() is first constructed, this is the upper search layer ) @@ -872,6 +732,8 @@ rule [superMethodImpl]: Class BaseClass:ClassType +//@ \subsection{Auxiliary functions} + rule [getClassChain-process]: getClassChain(MostBaseClass:ClassType, @@ -900,8 +762,7 @@ when notBool ((DecC ==K classObject) andBool (Name ==K String2Id("wait") orBool Name ==K String2Id("notify") orBool Name ==K String2Id("notifyAll"))) -/* [Skip] Auxiliary function for methods that need implementation in the semantics. The implementation - of this production is given in api-core.k and api-threads.k. +/*@ Auxiliary function for methods that need implementation in the semantics. The implementation of this production is given in api-core.k and api-threads.k. */ syntax KItem ::= invokeImpl ( MethodRef, //the method reference diff --git a/src/exec/new-instance.k b/src/exec/new-instance.k index e19359a2..882a8a38 100644 --- a/src/exec/new-instance.k +++ b/src/exec/new-instance.k @@ -8,8 +8,7 @@ module NEW-INSTANCE /*@ \subsection{Background} -In this subsection we present the fragment of configuration used by runtime method - invocation. The figure below contains the cells and their sorts. +In this subsection we present the fragment of configuration used by runtime method invocation. The figure below contains the cells and their sorts. \vspace{3ex} @@ -68,31 +67,13 @@ In this subsection we present the fragment of configuration used by runtime meth \vspace{3ex} -The cell \cellref[]{k} stores the current computation. Inside \cellref[]{env} we store the local environment -- a map - from variable names to their locations in the store. The cell \cellref[]{methodContext} store information about the - current object -- the one accessible through the keyword this. Both \cellref[]{env} and \cellref[]{methodContext} play - a special role in object instantiation. - -The cell \cellref[]{class} contains various sub-cells holding the content of that class. The - first cell in \cellref[]{classType} of sort ClassType that holds the fully qualified class name. - This cell is a unique identifier of a class, and is used as a key to access other cells inside a \cellref[]{class}. - Next relevant cells inside \cellref[]{class} are \cellref[]{enclosingClass} - the directly enclosing class in case - this class is an inner class. The vase class is stored inside \cellref[]{extends} and the list of declarations of - instance fields without identifiers is stored in \cellref[]{instanceFields}. - -The next two cells are related to the store. The cell \cellref[]{store} has a central role in the semantics -- it is - the map from object locations (values in the cell \cellref[]{env}) to their actual typed values. - The cell \cellref[]{nextLoc} is the counter of store locations. - -The remaining big group of cells -- \cellref[]{objectStore} contains the inner structure of objects. - The \cellref[]{objectId} is an unique identifier of the object. Every reference to this object in the store is - a reference to this id. Inside \cellref[]{objectType} is the actual runtime type of the object. Next we have a list - of \cellref[]{layer} cells, each of them representing an inheritance layer of the object. Starting from class - Object and ending with the actual object type. Inside each layer \cellref[]{layerClass} stores its - associated class, \cellref[]{layerEnv} -- the fields and \cellref[]{layerEnclosingObject} -- the enclosing object, - in the case when \cellref[]{layerClass} is a non-static inner class. The complex rules for Java inner classes - allow each layer to have its distinctive enclosing object, and we have tests that specifically target this - requirement. +The cell \cellref[]{k} stores the current computation. Inside \cellref[]{env} we store the local environment --- a map from variable names to their locations in the store. The cell \cellref[]{methodContext} store information about the current object --- the one accessible through the keyword this. Both \cellref[]{env} and \cellref[]{methodContext} play a special role in object instantiation. + +The cell \cellref[]{class} contains various sub-cells holding the content of that class. The first cell in \cellref[]{classType} of sort ClassType that holds the fully qualified class name. This cell is a unique identifier of a class, and is used as a key to access other cells inside a \cellref[]{class}. Next relevant cells inside \cellref[]{class} are \cellref[]{enclosingClass} --- the directly enclosing class in case this class is an inner class. The vase class is stored inside \cellref[]{extends} and the list of declarations of instance fields without identifiers is stored in \cellref[]{instanceFields}. + +The next two cells are related to the store. The cell \cellref[]{store} has a central role in the semantics --- it is the map from object locations (values in the cell \cellref[]{env}) to their actual typed values. The cell \cellref[]{nextLoc} is the counter of store locations. + +The remaining big group of cells --- \cellref[]{objectStore} contains the inner structure of objects. The \cellref[]{objectId} is an unique identifier of the object. Every reference to this object in the store is a reference to this id. Inside \cellref[]{objectType} is the actual runtime type of the object. Next we have a list of \cellref[]{layer} cells, each of them representing an inheritance layer of the object. Starting from class Object and ending with the actual object type. Inside each layer \cellref[]{layerClass} stores its associated class, \cellref[]{layerEnv} --- the fields and \cellref[]{layerEnclosingObject} --- the enclosing object, in the case when \cellref[]{layerClass} is a non-static inner class. The complex rules for Java inner classes allow each layer to have its distinctive enclosing object, and we have tests that specifically target this requirement. */ /*@ \subsection{New instance creation}*/ @@ -117,31 +98,31 @@ When all the subexpressions of new have been evaluated, the main rule for new co First the current value of the counter inside \cellref[]{nextLoc} is used as the location of the newly created object. The counter is incremented for the next use. Inside \cellref[]{objectStore} a new cell \cellref[]{object} is created for the new object. For now it has just two - sub-cells specified -- \cellref[]{objectId} and \cellref[]{objectType}, and no layers. Curiously we don't have + sub-cells specified --- \cellref[]{objectId} and \cellref[]{objectType}, and no layers. Curiously we don't have to specify neither \cellref[]{object} nor \cellref[]{objectStore} cells explicitly here, we have to specify just the cells inside them that are modified. The capability to ignore surrounding cells when they can be automatically inferred is called configuration abstraction, another K feature\cite{k-jlap}. In the cell \cellref[]{store} - a new entry is created with key being L and value - a reference to the newly created object in \cellref[]{object}. + a new entry is created with key being L and value --- a reference to the newly created object in \cellref[]{object}. The content of \cellref[]{methodContext} is reset to a default state. This default state is required by rules that are applied next. Inside \cellref[]{k} the new instance expression is rewritten into a sequence of computations that will be executed - by the following rules. The auxiliary function staticInit() triggers static initialization of the instantiated class, - in case it was not triggered earlier. Next, the function create() populates the layers of the object inside + by the following rules. The auxiliary function \verb|staticInit()| triggers static initialization of the instantiated class, + in case it was not triggered earlier. Next, the function \verb|create()| populates the layers of the object inside \cellref[]{object} This also includes allocation of all instance fields, and their initialization to the default value. - Field initializers are not executed yet. The function setEncloser() sets the enclosing object for the current class, + Field initializers are not executed yet. The function \verb|setEncloser()| sets the enclosing object for the current class, if the current class is an inner class. If some of the base classes are also inner classes, the encloser for their respective \cellref[]{layer} will be set as part of constructor invocation. -The next term in the computation (the one starting with typedLookup(L)) might look a bit weird, but it is in fact +The next term in the computation (the one starting with \verb|typedLookup(L)|) might look a bit weird, but it is in fact the invocation of the constructor. This term represents a mix of Java syntax for method invocation and auxiliary functions defined inside K-Java. It illustrates, among others, the power of K parser. Now, after all memory allocation procedures have been completed, it is the right time for it to be invoked. Preprocessing semantics - transforms all constructors into plain methods. The function typedLookup(L) is evaluated into the object stored - at the location L, that will serve as a qualifier for constructor invocation. The function getConsName() converts + transforms all constructors into plain methods. The function \verb|typedLookup(L)| is evaluated into the object stored + at the location L, that will serve as a qualifier for constructor invocation. The function \verb|getConsName()| converts the class name into the name of the constructor method. What remains is plain Java syntax for method invocation. -The last two terms bring computation to the state required to continue execution. Function restoreMethoContext() +The last two terms bring computation to the state required to continue execution. Function \verb|restoreMethoContext()| restores \cellref[]{methodContext} to the the state before object creation. The last term is the result value of the object instantiation expression. */ @@ -248,6 +229,8 @@ module NEW-INSTANCE-REST imports VAR-LOOKUP //for typedLookup() imports NEW-INSTANCE +/*@Additional semantics of new instance creation. */ + //@\subsection{Instance field declarations} rule [FieldDec-instance]: @@ -257,7 +240,7 @@ rule [FieldDec-instance]: ... . => L |-> FieldLocMetadata ... L:Int => L +Int 1 -//@\subsection{Execution of QSuperConstrInv, AltConstrInv} +//@\subsection{Explicit constructor invocation --- \texttt{this()} and \texttt{super()}} // 'QSuperConstrInv( Qual:K,, _:K,, [ Args:KList ] ) rule [QSuperConstrInv]: diff --git a/src/exec/statements.k b/src/exec/statements.k index cc7ea179..c785bd50 100644 --- a/src/exec/statements.k +++ b/src/exec/statements.k @@ -6,12 +6,7 @@ module STATEMENTS imports METHOD-INVOKE // for initParams imports STMT-SYNTAX -//@ \subsection{isStmt} -rule isStmt('For(_)) => true -rule isStmt('Switch(_)) => true -rule isStmt('Block(_)) => true - -//@ \subsection{Call of main method} +//@ \subsection{Call of the main method} //For now main class may only be placed in the default package. rule [ExecutionPhase-Start]: @@ -30,11 +25,11 @@ rule [ExecutionPhase-Start]: //@ \subsection{Blocks} JLS \$14.2 rule [Block]: - 'Block(S:K) => S ~> env(Env:Map) ... + { S:K } => S ~> env(Env:Map) ... Env [structural] -//@ \texttt{env} Restore the env cell content from env(...) statement argument +//@ \texttt{env} Restore the env cell content from \verb|env(...)| statement argument syntax KItem ::= env ( Map ) rule [env]: @@ -46,7 +41,7 @@ rule [env-double-Discard]: (env(_) => .) ~> env(_) [structural] -/*@ \subsection{Local Variable Declaration Statements} JLS \$14.4 +/*@ \subsection{Local Variable Declarations} JLS \$14.4 Not only local but fields also*/ rule [LocalVarDec]: @@ -59,7 +54,7 @@ rule [LocalVarDec]: //@ \subsection{Empty statement} JLS \$14.6 rule [Empty]: - ;<:EmptyStmt => . + ; :EmptyStmt => . //@ \subsection{Labeled statements} JLS \$14.7 @@ -77,6 +72,9 @@ rule [labeledImpl-Discard]: rule _:TypedVal; => .K //@ \subsection{If statement} +rule [If-Then-Desugar]: + if (E<:Exp) S:Stmt => if (E) S else ( ; ) + rule [If-True]: if (true::bool) S:Stmt else _:Stmt => S [symbolic-rule] @@ -85,36 +83,27 @@ rule [If-False]: if (false::bool) _:Stmt else S:Stmt => S [symbolic-rule] -rule [If-True]: - if (true::bool) S:Stmt => S - [symbolic-rule] - -rule [If-False]: - if (false::bool) _:Stmt => . - [symbolic-rule] - //@ \subsection{Assert statement} //short version: assert exp1; rule [AssertStm-True-OneArg]: - assert true::bool; => . + assert true::bool; => . rule [AssertStm-False-OneArg]: - assert false::bool; - => throw new class String2Id("java.lang.AssertionError") (null::classString); + assert false::bool; + => throw new class String2Id("java.lang.AssertionError") (null::classString); //full version: assert exp1:exp2; rule [AssertStm-FirstTrue-SecondDiscarded]: - assert true::bool : _ ; => . + assert true::bool : _ ; => . context assert false::bool : HOLE; rule [AssertStm-FirstFalse]: - assert (false::bool) : (TV:TypedVal); - => throw new class String2Id("java.lang.AssertionError") (toString(TV)); + assert (false::bool) : (TV:TypedVal); + => throw new class String2Id("java.lang.AssertionError") (toString(TV)); //@ \subsection{Switch statement} - syntax KItem ::= switchImpl ( TypedVal, // TV - switch argument KListWrap, // switch body - list of 'SwitchGroup labels @@ -130,7 +119,7 @@ rule [Switch]: context switchImpl( _,[ 'SwitchGroup(['Case(HOLE),,_:KList],,_),, _:KList ], _) /*@ 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.*/ +a switch statement must be assignable (\$5.2) to the type of the switch Expression.*/ rule [switchImpl-CaseNotMatch]: switchImpl(V:RawVal :: _,[ 'SwitchGroup([ ( 'Case(V2:RawVal :: _) => .KList ),, _:KList ],,_),, _],_) when V =/=K V2 @@ -161,15 +150,15 @@ rule [switchEnd-Discard]: //@ \subsection{While statement} and loop infrastructure. rule [while]: - while(E:Exp)S:Stmt => whileImpl(E, S) [structural] + while (E:Exp) S:Stmt => whileImpl(E, S) [structural] -syntax KItem ::= whileImpl ( +syntax Stmt ::= whileImpl ( K, // E - test expression. In For loop, it is UpdClause ~> testExp K // S - while body ) rule [whileImpl]: - whileImpl(E:K, S:K) => ifAux(E, S ~> whileImpl(E, S), .K) [structural] + whileImpl(E:K, S:K) => if (E) {S ~> whileImpl(E, S)} [structural] //@ \subsection{Do statement} rule [do-while]: @@ -177,7 +166,7 @@ rule [do-while]: //@ \subsection{For statement} //wrapper of certain clauses of for statement -syntax KItem ::= stm ( KListWrap ) +syntax Stmt ::= stm ( KListWrap ) rule [stm-KListWrap-empty]: stm([.KList]) => . [structural] @@ -209,21 +198,14 @@ rule [For]: => 'Block(stm(InitClause) ~> ifAux(TestExp, ('Block(S) ~> whileImpl(stm(UpdClause) ~> TestExp,S)), .K)) [structural] -//totest model check - the argument of 'return and 'Throw must be evaluated. Otherwise some side effects during -// evaluation might be evaluated too late -/*@ Stack consumer stm - Return, Throw, Break or Continue reaches tryFinallySL layer*/ -rule [StackConsumerStmt-in-TryFinally]: - StackCons:StackConsumerStmt ~> finallyBlock(FinallyS:K) - => FinallyS ~> StackCons - -rule [StackConsumerStmt-RestoreEnv]: - StackCons:StackConsumerStmt ~> env(Env:Map) - => env(Env:Map) ~> StackCons - //@ \subsection{Break statement} +/*K limitation: Looks like neither 'None nor 'Some can be expressed syntactically. + Attempts to replace them with syntax, in rules for break, give either compile-time or runtime errors. + This is definitely a K limitation, as such syntax was not used in K before. +*/ + rule [Break-UnlabeledPropagate]: - // 'Break('None(_)) ~> (KL:KLabel(_) => .) break 'None(_); ~> (KL:KLabel(_) => .) when KL =/=KLabel 'env @@ -232,7 +214,6 @@ when andBool KL =/=KLabel 'switchEnd rule [Break-Unlabeled]: - //'Break('None(_)) ~> KL:KLabel(_) => . break 'None(_); ~> KL:KLabel(_) => . when KL ==KLabel 'whileImpl @@ -300,11 +281,7 @@ when KL =/=KLabel 'env andBool KL =/=KLabel 'labeledImpl -/*@\subsection{Return} At method return, we have to check that the type -of the returned -value is a subtype of the expected return type. Moreover, if that is -the case, then we also up-cast the returned value to one of the -expected type. */ +/*@\subsection{Return statement}*/ //context 'Return('Some(HOLE)) context return 'Some(HOLE); @@ -328,7 +305,7 @@ rule [Return-MethodEnd]: _:Bag => MethContext /*@ \subsection{Throw statement} -Exceptions are propagated now until a catch that can bind them is +Exceptions are propagated until a catch compatible with them is encountered. */ rule [Throw]: (. => checkCatch(subtype(typeOf(TV), T))) @@ -336,18 +313,14 @@ rule [Throw]: ~> throw TV:TypedVal; ~> catchBlocks(catchImpl('ParamImpl(T:Type,, X:Id),_) _:CatchClauses) -syntax KItem ::= checkCatch ( K ) -context checkCatch(HOLE) +syntax KItem ::= checkCatch ( K ) [strict] rule [Throw-checkCatch-True]: checkCatch(true::bool) // ~> 'Throw(TV:TypedVal) ~> throw TV:TypedVal; ~> catchBlocks(catchImpl(Param:Param, CatchS:K) _:CatchClauses) - => 'Block([ - initParams(Param, TV),, - CatchS - ]) + => { initParams(Param, TV) ~> CatchS } rule [Throw-checkCatch-False]: (checkCatch(false::bool) => .) @@ -389,50 +362,9 @@ rule [Throw-CausesThreadTermination]: rule [Try-Catch-Finally-Desugar]: try TryS:K (K:CatchClause Ks:CatchClauses) finally FinallyS:K - => try 'Block(try TryS (K Ks)) .CatchClauses finally FinallyS + => try { try TryS (K Ks) } .CatchClauses finally FinallyS [structural] -/*@ \subsubsection{Execution of try-catch} JLS \$14.20.1 -*/ -//macro -rule 'Try(Trys:K,,([Catches:KList] => toCatchClauses([Catches])),,FinallyS:K) [anywhere] -rule 'Try(Trys:K,,([Catches:KList] => toCatchClauses([Catches]))) [anywhere] - -syntax CatchClauses ::= toCatchClauses( KListWrap ) [function] - | toCatchClauses( KListWrap , CatchClauses ) [function] - -rule toCatchClauses([KLCatchClauses:KList]) => toCatchClauses([KLCatchClauses],.CatchClauses) -rule toCatchClauses([KLCatchClauses:KList,, C:CatchClause], CatchClauses:CatchClauses) => toCatchClauses([KLCatchClauses], (C CatchClauses)) -rule toCatchClauses([.KList], CatchClauses:CatchClauses) => CatchClauses - -//resolve the catch clauses of try statement -context try _:K HOLE - -syntax CatchClause ::= "catch" "(" K ")" K [klabel('Catch)] -//resolve 'Param term of the catch clause -context catch(HOLE)_ [result(ExtKResult)] - -rule 'Param(_,, K:Type,, X:Id) => K X [structural] - -rule catch(KR:ExtKResult)S:K => catchImpl(KR,S) - -/*@ Extended K Result. - Represents KLabels that should be treated as KResult during execution phase, but not during elaboration phase. -*/ -syntax ExtKResult ::= "dummy" - -rule isExtKResult(KR:KResult) => true - -rule isExtKResult('ParamImpl(T:Type,, _:Id)) => true - -//@ Internal representation of a preprocessed catch clause -syntax CatchImpl ::= catchImpl ( - K, //'Param(...), - K //the code block - ) -syntax KResult ::= CatchImpl -syntax CatchClause ::= CatchImpl - rule [Try-Catch]: (try TryS:K KRs:CatchClauses => TryS ~> catchBlocks(KRs)) when isKResult(KRs) @@ -447,9 +379,6 @@ syntax KItem ::= catchBlocks ( CatchClauses ) //arg - list of catchImpl rule [catchBlocks-Discard]: catchBlocks(_) => .K -/*@ \subsubsection{Execution of try-finally} JLS \$14.20.2 -*/ - rule [Try-Finally]: try TryS:K .CatchClauses finally FinallyS:K => TryS ~> finallyBlock(FinallyS) @@ -460,4 +389,21 @@ syntax KItem ::= finallyBlock ( K ) //arg - finally block rule [finallyBlock-NormalEnd]: finallyBlock(FinallyS:K) => FinallyS -endmodule \ No newline at end of file +/*@ Only a throw with its value computed is stack consumer, not any throw. If we'll define any throw to be +StackConsumerStmt, then we'll get rare problems with ExceptionInInitializerError. +Other values for StackConsumerStmt are defined in the syntax. +*/ +rule isStackConsumerStmt(throw _:TypedVal;) => true + +//totest model check - the argument of 'return and 'Throw must be evaluated. Otherwise some side effects during +// evaluation might be evaluated too late +/*@ Stack consumer stm - Return, Throw, Break or Continue reaches tryFinallySL layer*/ +rule [StackConsumerStmt-in-TryFinally]: + StackCons:StackConsumerStmt ~> finallyBlock(FinallyS:K) + => FinallyS ~> StackCons + +rule [StackConsumerStmt-RestoreEnv]: + StackCons:StackConsumerStmt ~> env(Env:Map) + => env(Env:Map) ~> StackCons + +endmodule diff --git a/src/exec/static-init.k b/src/exec/static-init.k index 73bcaff0..5cafdf85 100644 --- a/src/exec/static-init.k +++ b/src/exec/static-init.k @@ -3,21 +3,23 @@ module STATIC-INIT imports CORE-CLASSES //for objectClass imports CORE-EXEC //for restoreMethContext -/*@ Triggers static initialization of a class. - -Detailed initialization procedure is described in JLS \$12.4.2. Here we implement an approximation of that algorithm, -that does not use the traditional Java synchronization mechanism, but instead relies on term rewriting +/*@ +Triggers the static initialization of a class. +The detailed initialization procedure is described in JLS \$12.4.2. Here we implement an approximation of that algorithm, +one that does not use the traditional Java synchronization mechanism, but relies instead on term rewriting capabilities to implement locks. This algorithm is required to avoid multithreaded issues during static initialization. This may happen when two threads access an uninitialized class at the same time. -Initialization status of a class may have 3 states: StaticUninitialized, StaticInitializing(TId), StaticInitialized. -//Here TId is the id of the thread that initiated the initializing process. -//Now when we reach staticInit(Class), depending on the initialization status of class we should do the following: -1. status = StaticUninitialized => perform the initialization -2. status = StaticInitializing(TId), TId = this thread => this is a recursive initialization request, discard the term. -3. status = StaticInitializing(TId), IID = another thread => we should wait until the initialization is completed - by another thread. Do not match this case. -4. status = StaticInitialized => the class has already been initialized. Discard the term. +Initialization status of a class may have one of the following 3 states: StaticUninitialized, StaticInitializing(TId), StaticInitialized. +Here TId is the identifier of the thread that initiated the initialization process. +When we reach staticInit(Class), depending on the initialization status of the class (stored in \cellref{staticInitStatus}), we should do one of the following: + +\begin{markdown} + - \verb|status = StaticUninitialized| --- Perform the initialization. + - \verb|status = StaticInitializing(TId), TId = this thread| --- This is a recursive initialization request, discard the term. + - \verb|status = StaticInitializing(TId), TId = another thread| --- We should wait until the initialization is completed by another thread. Do not match this case. + - \verb|status = StaticInitialized| --- The class has already been initialized. Discard the term. +\end{markdown} */ syntax KItem ::= staticInit ( ClassType // Class - the ClassType to be initialized, @@ -31,6 +33,9 @@ rule [staticInit]: StaticFields,, //Static fields have to be allocated before base class is statically initialized, // because during base class initialization those fields might be accessed. staticInit(BaseClass),, + + //Cannot write this statement syntactically, + // because the body of the finally clause cannot be a block. 'Try( StaticInit,, @@ -63,7 +68,7 @@ rule [staticInit]: Class BaseClass:ClassType StaticFields:KListWrap - StaticInit:KListWrap + StaticInit StaticUninitialized => StaticInitializing(TId) rule [staticInit-already-initialized-discard]: diff --git a/src/exec/syntax-conversions.k b/src/exec/syntax-conversions.k index 8890bf34..b4253b67 100644 --- a/src/exec/syntax-conversions.k +++ b/src/exec/syntax-conversions.k @@ -4,21 +4,21 @@ module SYNTAX-CONVERSIONS imports CORE-CLASSES //for cast imports CORE-EXEC -/*@ Defining the syntax for key portions of the semantics, and converting AST terms back int otheir syntactiv form. +/*@ Defining the syntax for key portions of the semantics, and converting AST terms back into their syntactic form. +This whole module is auxiliary, its purpose is to allow defining some portions of the semantics syntactically. +It will disappear once the main syntax of K-Java will be used instead. */ /*@ \subsection{Method parameter}*/ // 'Param(\_:K,, T:Type,, X:Id). Consumed by initParams(). -syntax KItem ::= toParams( KListWrap ) [function] - | toParams( KListWrap , Params ) [function] +syntax KItem ::= toParams( KListWrap , Params ) [function] -rule toParams([KLParams:KList]) => toParams([KLParams], .Params) rule toParams([KLParams:KList,, 'Param(_,, K:K,, X:Id)], Params:Params) => toParams([KLParams], (K X,Params)) rule toParams([.KList], Params:Params) => Params -// Required for getTypes() +//@ Required for getTypes() rule typeOf('ParamImpl(T:Type,, _:Id)) => T /*@ \subsection{Method invocation}*/ @@ -26,6 +26,7 @@ rule typeOf('ParamImpl(T:Type,, _:Id)) => T /* General structure: +\begin{verbatim} 'Invoke( 'Method( 'MethodName( @@ -33,8 +34,9 @@ General structure: Name:Id ) ),, - [Args] - argument expressions + [Args] --- argument expressions ) +\end{verbatim} */ /* 'Method(Qual:K,, \_:K,, Name:Id) @@ -47,8 +49,6 @@ rule 'Invoke('Method( 'MethodName( Qual:K,, Name:Id ) ),, ArgList:KListWrap) => //somehow. //totest - if qualifier evaluates to null, NullPointerException should be thrown after //the evaluation of the arguments -/*@ Method invocation expression -*/ /*@ \subsection{Local variable declaration}*/ @@ -89,7 +89,7 @@ rule [NewInstance-to-QNewInstance-unpack]: new Class:ClassType(ArgExps:Exps) => noValue . new Class:ClassType(ArgExps:Exps) -/*@ \subsection{Syntactic lists - Exps, TypedVals, ClassTypes}*/ +/*@ \subsection{Syntactic lists}*/ /*@ A list of expressions, usually a list of arguments of a method or constructor. @@ -99,8 +99,8 @@ syntax KItem ::= toExps( KListWrap ) [function] | toExps( KListWrap , Exps ) [function] rule toExps([Args:KList]) => toExps([Args], .Exps) -rule toExps([Args:KList,, Arg:Exp], Es:Exps) => toExps([Args], (Arg,Es)) -rule toExps([.KList], Es:Exps) => Es +rule toExps([Args:KList,, Arg<:Exp], Es<:Exps) => toExps([Args], (Arg,Es)) +rule toExps([.KList], Es<:Exps) => Es syntax KItem ::= toKListWrap( Exps ) [function] | toKListWrap( KListWrap , Exps ) [function] @@ -126,4 +126,40 @@ rule getTypes(types(Ts:KList), .TypedVals) => types(Ts) syntax KResult ::= ClassTypes syntax ClassTypes ::= List{ClassType, ","} +//@ \subsubsection{Try/catch} +rule 'Try(Trys:K,, ([Catches:KList] => toCatchClauses([Catches])),, _:KList) [anywhere] + +syntax CatchClauses ::= toCatchClauses( KListWrap ) [function] + | toCatchClauses( KListWrap , CatchClauses ) [function] + +rule toCatchClauses([KLCatchClauses:KList]) => toCatchClauses([KLCatchClauses],.CatchClauses) +rule toCatchClauses([KLCatchClauses:KList,, C:CatchClause], CatchClauses:CatchClauses) + => toCatchClauses([KLCatchClauses], (C CatchClauses)) +rule toCatchClauses([.KList], CatchClauses:CatchClauses) => CatchClauses + +//resolve the catch clauses of try statement +context try _:K HOLE + +syntax CatchClause ::= "catch" "(" K ")" K [klabel('Catch)] +//resolve 'Param term of the catch clause +context catch(HOLE) _ [result(ResultOrParam)] + +rule 'Param(_,, K:Type,, X:Id) => K X [structural] + +rule catch(KR:ResultOrParam) S:K => catchImpl(KR,S) + +/*@ Extended K Result. + Represents KLabels that should be treated as KResult during execution phase, but not during elaboration phase. +*/ +syntax ResultOrParam ::= Param //| KResult - not allowed +rule isResultOrParam(_:KResult) => true // Because KResult cannot be used in a sort definition above. + +//@ Internal representation of a preprocessed catch clause +syntax CatchImpl ::= catchImpl ( + K, //'Param(...), + K //the code block + ) +syntax KResult ::= CatchImpl +syntax CatchClause ::= CatchImpl + endmodule diff --git a/src/exec/to-string.k b/src/exec/to-string.k index c66d3740..dde96f60 100644 --- a/src/exec/to-string.k +++ b/src/exec/to-string.k @@ -18,7 +18,7 @@ rule toString(true::_) => "true" rule toString(false::_) => "false" rule toString(null::_) => "null" -//@ toString(arrayOf T) +//@ \verb|toString(arrayOf T)| rule toString(arrayOf byte) => "[B" rule toString(arrayOf short) => "[S" @@ -68,9 +68,9 @@ rule toString(objectRef(OId:Int, LowestClass:ClassType) :: T:Type) //@ \subsection{Debug helper functions} -syntax KItem ::= debugPrint ( K ) [strict] -rule debugPrint(Str:String::_) => . ... - ... . => ListItem(Str +String "\n") +syntax KItem ::= debugPrint ( K ) +rule debugPrint(K:K) => . ... + ... . => ListItem(K) syntax KItem ::= debugString( K ) [function] | debugStringList( KListWrap ) [function] diff --git a/src/exec/unfolding.k b/src/exec/unfolding.k index 3f55b0bd..310ffba1 100644 --- a/src/exec/unfolding.k +++ b/src/exec/unfolding.k @@ -3,12 +3,16 @@ module UNFOLDING imports CORE-FUNCTIONS imports SYNTAX-CONVERSIONS -/*@At the beginning of execution semantics contains the term unfoldingPhase, is non-empty and the global phase is UnfoldingPhase. +/*@ +The Unfolding phase of the execution semantics, opposite ot the folding phase of the preprocessing semantics. +In this phase the preprocessed program stored in cell is distributed into various cells inside . + +At the beginning of execution semantics \verb|| contains the term unfoldingPhase, \verb|| is non-empty and the global phase is UnfoldingPhase. */ syntax KItem ::= "unfoldingPhase" -//@In the initial configuration the cell is empty, global phase is UnfoldingPhase, is non-empty. +//@In the initial configuration the cell \verb|| is empty, global phase is UnfoldingPhase, \verb|| is non-empty. rule [UnfoldingPhase-start]: . => unfoldingPhase ... @@ -128,7 +132,7 @@ syntax KItem ::= getClassMetaType ( KLabel ) [function] rule getClassMetaType('ClassDec) => classCMT rule getClassMetaType('InterfaceDec) => interfaceCMT -// True if given KListWrap contains a 'MethodDec(\_) term +// True if given KListWrap contains a \verb|'MethodDec(\_)| term syntax KItem ::= containsMethodDecs( KListWrap ) [function] rule containsMethodDecs([_,, 'MethodDec(_),, _]) => true @@ -153,7 +157,7 @@ rule [unfolding-MethodDec]: (.Bag => sig(Name:Id, getTypes([Params])) - toParams([Params:KList]) + toParams([Params:KList], .Params) MethodBody:K Acc:AccessMode CT:ContextType diff --git a/src/exec/var-lookup.k b/src/exec/var-lookup.k index 686a7b22..67bafc47 100644 --- a/src/exec/var-lookup.k +++ b/src/exec/var-lookup.k @@ -1,17 +1,12 @@ module VAR-LOOKUP imports CORE-SORTS imports SUBTYPING - imports STATIC-INIT //for staticInit() + imports STATIC-INIT //for \verb|staticInit()| imports EXPRESSIONS //@ \subsection{Local variable access} -/* Local variable access. At runtime may have one form: - - 'ExprName(X:Id) - local variable -*/ - - -/*@ At execution phase 'ExprName(X) always represent a local variable. +/*@ At execution phase \verb|'ExprName(X)| always represents a local variable. */ rule [ExprName-local]: 'ExprName(X:Id) => typedLookup(L) ... @@ -21,7 +16,7 @@ rule [lvalue-ExprName-local]: lvalue('ExprName(X:Id)) => typedLoc(L) ... ... X |-> L:Int ... -/*@ \subsection{QThis - Self reference} */ +/*@ \subsection{Qualified \texttt{this} --- self reference} */ // 'QThis(Class:ClassType) rule [QThis]: @@ -37,7 +32,7 @@ rule [QThis]: ... -//@ Search for the right value representing QThis(Class) - an expression of type Class.this +//@ Search for the right value representing \verb|QThis(Class)| --- an expression of type Class.this syntax KItem ::= lookupQThis ( ClassType, //the type of this to look for, TypedVal //the objectRef where the type should be found @@ -66,10 +61,9 @@ when /*@ \subsection{Instance field access} */ -/*@ Variable access. May have 2 forms: - - 'ExprName(Class, X:Id) - static field - - 'ExprName(Qual, X:Id) - instance field +/*@ Has the following form: \verb|'ExprName(Qual, X:Id)|. */ + context 'Field(HOLE,, _) context lvalue('Field(HOLE,, _)) @@ -102,7 +96,8 @@ rule [Field-instance-OfNull]: [anywhere] /*@ \subsection{Static field access} */ - +/*@ Has the following form: \verb|'ExprName(Class, X:Id)|. +*/ rule [Field-static]: 'Field( TargetClass:ClassType,, X:Id ) => staticInit(TargetClass) ~> staticFieldLookup(TargetClass, X) @@ -112,7 +107,7 @@ rule [lvalue-Field-static]: => staticInit(TargetClass) ~> lvalue(staticFieldLookup(TargetClass, X)) /*@ The actual implementation of static field lookup. The distinction between this function and - 'Field(Class, X) term is that at the moment when this function is called the target clas is + \verb|'Field(Class, X)| term is that at the moment when this function is called the target clas is surely initialized. */ syntax KItem ::= staticFieldLookup ( ClassType , Id ) @@ -141,7 +136,7 @@ rule [lvalue-Field-static]: TargetClass ... X |-> L:Int ... -/*@ \subsection{lvalue and loc} */ +/*@ \subsection{Functions for accessing the store} */ //@ Typed version of lookup and loc syntax KItem ::= typedLookup ( Int ) @@ -162,11 +157,9 @@ rule [typedLoc]: rule [lvalue-typedLoc]: lvalue(typedLoc(L:Int)) => typedLoc(L) -/*@ \subsection{lookup} */ - /*@ Retrieve a value from the store based on its location and the given compile-time type. - May be wrapped inside lvalue. If lookup is unwrapped, it evaluates to TypedVal - the store value, - of the type T - the second lookup argument. If lookup is wrapped into lvalue, it evaluates to loc(OL)::T. + May be wrapped inside lvalue. If lookup is unwrapped, it evaluates to TypedVal --- the store value, + of the type T --- the second lookup argument. If lookup is wrapped into lvalue, it evaluates to \verb|loc(OL)|::T. */ syntax Exp ::= lookup ( Int, //OL - the store location to lookup @@ -196,4 +189,17 @@ rule [fieldAccessCheckpoint-Field]: ... L |-> FieldLocMetadata ... [transition-threading] +//@ Synchronization checkpoint have to be before the actual assignment, like for lookup. +rule [store]: + store(L:Int, V:RawVal :: T:Type) => fieldAccessCheckpoint(L) ~> storeImpl(L, V::T) + +syntax KItem ::= storeImpl ( + Int, //OL - the store location + K //TypedVal - the value to be stored + ) + +rule [storeImpl]: + storeImpl(L:Int, V:RawVal :: T:Type) => . ... + ... L |-> (_ => V) :: T ... + endmodule diff --git a/src/prep/configuration-prep.k b/src/prep/configuration-prep.k index dcabae38..6fb0808b 100644 --- a/src/prep/configuration-prep.k +++ b/src/prep/configuration-prep.k @@ -3,166 +3,20 @@ module CONFIGURATION-PREP imports CORE-FUNCTIONS /*@ -The Static semantics consists of several phases that analyze the input program, distribute it from the AST form to a set of cells and finally assembles it back to an AST, this time containing just a subset of features of Java. Each phase digs deeper into a program strucutre, and most phases also store their result into new cells. Below is the list of global phases, in their execution order: +The Static semantics consists of several phases that analyze the input program, distribute it from the AST form to a set of cells and finally assembles it back to an AST, this time containing just a subset of features of Java. Each phase digs deeper into a program structure, and most phases also store their result into new cells. Below is the list of global phases, in their execution order: \begin{itemize} - \item Process Type Names - \item Process Compilation Units - \item Process Class Declarations - \item Process Class Members - \item Elaboration - \item Folding + \item Process Type Names + \item Process Compilation Units + \item Process Class Declarations + \item Process Class Members + \item Elaboration + \item Folding \end{itemize} The configuration cells may be divided into 2 categories: cells directly placed inside the all-enclosing cell \cellref{T} (top-level cells), and cells inside \cellref{classes}. The cell \cellref{classes} is a collection of \cellref{class} cells, each representing a Java class (both supported classes from JDK and classes defined by the developer). A \cellref{class} contains all components of a class --- such as extends/implements clauses, imports, fields, methods, etc, each distributed into a separate class, in order to be conveniently accessed when needed. -In the remaining of this section are documented all cells of the configuration, ordered by the global phase in which they are first used. - -\paragraph{Initial state} The first row contains three cells most relevant to computation initial state: -\begin{itemize} - \item \cellref[K]{k} --- Holds the current computation in all phases of the semantics. Initializes with the AST representation of the program. - \item \cellref[K]{program} --- A backup of program AST. Required because the initial AST is needed in both 1st ans 2nd phase of static K-Java, but the first phase destroys the content inside \cellref{k}. Also used in the last phase (Folding) to assemble the preprocessed program. - \item \cellref[GlobalPhase]{globalPhase} --- The current computation global phase. -\end{itemize} - -\paragraph{Process Type Names} During this phase, one global cell is computed: -\begin{itemize} - \item \cellref[Map{[}PackageId\mapsto{}Map{[}Id\mapsto{}ClassType{]}{]}]{namesToClasses} A two-level map. First level is a map from package names to second-level maps. Second-level maps are from simple class names to fully qualified class names within the package. This cell is extensively used through the semantics. The map contains both top-level and inner classes. For inner classes, their enclosing package is the fully qualified class name of the directly enclosing class. -\end{itemize} - -Also during Process Type Names classes are first registered. Again, both top-level and inner classes are covered. In a newly created \cellref[]{class} just a few sub-cells are initialized with data: - -\begin{itemize} - \item \cellref[ClassType]{classType} --- The fully qualified class name. The identifier of the class. - \item \cellref[ClassMetaType]{classMetaType} --- Whether the type stored in this cell is class or interface. To avoid terminology superfluousness, we will refer hereafter to both classes and interfaces as "classes", making distinctions only when necessary. - \item \cellref[ClassAccessMode]{classAccessMode} --- The access modifier of the class, either public or package. - \item \cellref[ClassPhase]{classPhase} --- represents the state of this class. In addition to the global computation phase, each class has its own lifecycle phase. Class phases are required to keep track which classes were processed in the current global phase and which were not. During each global phase all classes should transition to a certain class phase. However, as we shall see, not all global phases change the state of the class. The class phases are: - - \begin{itemize} - \item Discovered --- the initial phase. At the end of Process Type Names all classes are in the state "Discovered". - \item Stored - \item Bases Resolved - \item Declaration Processed - \item Members Processed - \item Folded - \end{itemize} - -\end{itemize} - -\paragraph{Process Compilation Units} At the beginning of this phase computation is again initialized with the initial AST from \cellref{program}. The following new cells are filled in inside each \cellref{class}: - -\begin{itemize} - \item \cellref[ClassType]{enclosingClass} -- the directly enclosing class, for inner classes, or no value for top-level classes. - \item \cellref[K]{rawExtends} -- The extends clause of this class, in its raw (AST) form. - \item \cellref[K]{rawImplements} -- The implements clause, in AST form. - \item \cellref[K]{rawDeclarations} -- The class body, in AST form. - \item \cellref[Map{[}Id\mapsto{}ClassType{]}]{cuImports} -- A map from names accessible inside this class to fully qualified class names they represent. Only computed for top-level classes at this phase. For inner classes this cell remains empty. - \item \cellref[ContextType]{classContextType} --- Either static or instance, for inner classes. Always static for top-level classes. -\end{itemize} - -The class phase changes from Discovered to Stored. As we can see, the cells computed so far contain all the data of the original program. Thus, initial AST representation of the program is no longer needed. In fact, the cell \cellref[]{program} is discarded at the end of Process Compilation Units. The remaining preprocessing phases will use class data in this initial form to compute other cells within \cellref[]{class}, finally used for execution. - - -Also during Process Compilation Units the following global cell is used: - -\begin{itemize} - \item \cellref[Map{[}Id\mapsto{}ClassType{]}]{compUnitImports} A map from all type names accessible in the current compilation unit (Java file) to their respective fully qualified class names. This includes both classes accessible through imports declarations and classes declared in the package of the current compilation unit. Used to compute \cellref{cuImports} of top-level classes. -\end{itemize} - -\paragraph{Process Class Declarations} Here each class passes through two more class phases: Bases Processed and Declarations Processed. First, for each class the semantics attempts to resolve its extends/implements clauses into fully qualified class names. The order in which dependencies are resolved depends on both class inheritance relationships as well as nesting relationships. Once the dependencies of a class are resolved, they are stored into a temporary cell: - -\begin{itemize} -\item \cellref[K]{unprocessedBases} -- Initialized with the list of fully qualified class names for classes mentioned in extends/implements clauses of this class. -\end{itemize} - -Once the content of \cellref[K]{unprocessedBases} is created, the class enters into Bases Resolved phase. It then waits in this phase until all classes referred in extends/implements reach the phase Declarations Processed. The restrictions in JLS related to class dependencies guarantee that classes cannot have cyclic dependencies, thus a class cannot get locked in the waiting state. The cell \cellref[K]{unprocessedBases} is used to determine the moment when the class may exit the waiting state. Once a class reaches the phase Declarations Processed, is is deleted from cells \cellref[K]{unprocessedBases} of other classes. Thus, when all extends/implements dependencies of a class reach the phase Declarations Processed, the content of the its \cellref[K]{unprocessedBases} cell becomes empty. Once in this state, the class enters into the phase Declarations Processed itself and computes three more cells: - -\begin{itemize} -\item \cellref[ClassType]{extends} -- The base class, fully qualified. -\item \cellref[Set{[}ClassType{]}]{implements} -- The list of directly implemented interfaces, fully qualified. -\item \cellref[Map{[}Id\mapsto{}ClassType{]}]{imports} -- The map of classes accessible by simple name within the body of this class. The rules for computing this map are complex and include the following sources: - -\begin{itemize} -\item Imports declarations of the current compilation unit. -\item Classes declared within the package of the current compilation unit. -\item Classes accessible within the body of the directly enclosing class, if the current class is inner class. -\item Inner classes inherited from base classes, e.g. from extends/implements clauses. -\item Inner classes of this class itself. -\end{itemize} - -The need to cover all these cases leads to the intricate order in which class dependencies have to be be resolved. -\end{itemize} - -When a class enters the phase Declarations Processed, the cells \cellref[]{rawExtends}, \cellref[]{rawImplements} and \cellref[K]{unprocessedBases} are no longer needed and are discarded. Once all classes reach this phase the computation proceeds to the next global phase. - -During Process Class Declarations the following global cell is first used: -\begin{itemize} - \item \cellref[ClassType]{crntClass} --- The current class. Used in multiple phases starting from Process Class Declarations. -\end{itemize} - -\paragraph{Process Class Members} During this phase each class processes its members and reaches the state Members Processes. Until then, the class body is stored in \cellref[]{rawDeclarations}. A class member could be one of: - -\begin{itemize} - \item field - \item method - \item constructor - \item static or instance initializer -\end{itemize} - -The following new class cells are produced: - -\begin{itemize} - \item \cellref[Set{[}ClassType{]}]{implTrans} -- The transitive closure of implemented interfaces. In the remaining phases this set is used by the subtyping relationship. - \item \cellref[ Map {[} Signature \mapsto ClassType {]} ]{methods} --- The map of accessible methods. Keys are method signatures, values are classes where methods are defined. Includes both methods declared within this class as well as methods inherited from base classes/ base interfaces. - \item \cellref[Bag]{methodDecs} --- the collection of method declarations (\cellref{methodDec} cells)in the current class. This cell contains only a subset of methods from \cellref{methods}, as the set of accessible methods from \cellref{methods} also includes methods inherited from base classes/interfaces. Hence the need of two separate collections. Each \cellref[Bag]{methodDec} contains the following data: - \begin{itemize} - \item \cellref[Signature]{methodSignature} --- The method signature, acting as identifier of the \cellref{methodDec} - \item \cellref[Type]{methodReturnType} --- Method return type - \item \cellref[ List{[} Param {]} ]{methodParams} --- method parameters - \item \cellref[K]{methodConstrFirstLine} --- the first line of a constructor (if this method is indeed a constructor, for other classes than \verb|Object|). It contains a call to another constructor: either \verb|super()| or \verb|this()|. - \item \cellref[K]{methodBody} --- method body - \item \cellref[AccessMode]{methodAccessMode} --- method access mode - \item \cellref[ContextType]{methodContextType} --- either static or instance - \item \cellref[MethodMetaType]{methodMetaType} --- either method or constructor - \end{itemize} - \item \cellref[K]{instanceFields} --- The list of instance field declarations, stored as a list of local variable declaration statements, without initializers. Used during object instantiation. - \item \cellref[K]{instanceInit} -- The list of instance initializers of the class combined into one big instance initializer. Instance field initializers are also concatenated into this cell in their textual order. - \item \cellref[K]{staticFields} --- The list of static field declarations, in a similar format to \cellref{instanceFields} - \item \cellref[K]{staticInit} --- The list of static initializers and static field initializers concatenated into one block. - \item \cellref[Map{[}Id \mapsto Value{]}]{constantEnv} -- The map from compile-time constants to their actual values. Constants in Java have a slightly different semantics compared to final static fields. In particular, accessing them don't trigger static initialization of the declaring class. -\end{itemize} - -Once all the cells above are computed the class proceeds into the phase Members Processed and the cell \cellref[]{rawDeclarations} is deleted. - -\paragraph{Elaboration} Here all the code blocks are processed --- method and constructor bodies, static and instance initializers. Most of the information traditionally inferred by the compiler is computed at this phase. More precisely the elaboration performs the following transformations: - -\begin{itemize} -\item Each name is resolved into local variable, field, method, class or package. While a method may be distinguished from other cathegories purely syntactically, resolving to other categories requires knowledge of the names existing in the current context. -\item Simple class names are resolved into fully qualified class names. Hereafter all the class names in the code are fully qualified. -\item The compile-time type of each expression is inferred. Thus, when the code reaches execution phase, expressions are no longer in their initial form. The expressions are annotated with their types. -\item For each method call the precise signature in inferred. -\item Local and anonymous classes are processed. The earliest phase where local classes could be discovered is elaboration. Still, local classes have all the features of other classes. Thus they need to be passed through all the preprocessing steps. The whole preprocessing for local classes is performed during the global phase elaboration. -\end{itemize} - -Despite this phase being the most complex preprocessing phase of all, it introduces few new cells. Most of them are related to local classes. Inside \cellref[]{class} just one new cell is introduced: - -\begin{itemize} -\item \cellref[Map{[}Id \mapsto Type{]}]{enclosingLocalEnv} --- The map from local variables of the current block to their types. Used during local classes processing. -\end{itemize} - -Among global cells the following new cells are added: - -\begin{itemize} - \item \cellref[List[mapWrap(Map[Id \mapsto Type])]]{elabEnv} --- A stack where each layer is a map of local variables. Each layer of the stack represents a code block, in the blocks nesting order. Inside each layer, the map is from local variables accessible in that layer to variable types. - \item \cellref[Int]{contextType} --- The context type of the currently elaborated class. Either static or instance. - \item \cellref[List[mapWrap(Map[Id \mapsto ClassType])]]{localTypes} --- A cell similar in structure to \cellref{elabEnv}. This time it contains stack layers which are maps from local class names to local class types. - \item \cellref[Int]{nextLocalId} --- a number used to generate unique fully-qualified class names for local classes. - \item \cellref[K]{elabBuffer} --- a temporary cell used during elaboration of local classes. -\end{itemize} - -During the elaboration phase no cells are consumed. Instead, the code blocks stored inside \cellref[]{methodDecs}, \cellref[]{instanceInit}, \cellref[]{staticInit} are processed and stored back into the same cell. After elaboration the classes remain in the same state --- Members Processed. The state Members Processed is in fact the final state of the cell \cellref[]{class}. - -\paragraph{Folding} During the last phase of static semantics the program is assembled from \cellref{classes} back into the AST form. First the content of each class is assembled into \cellref[K]{folded} of the respective class, and the class phase changes to Folded. Second, the AST representation of each class is appended into \cellref{program}. When this phase ends, the content of \cellref{program} is printed to the standart output. +In the remaining of this section are documented all the cells of the configuration, ordered by the global phase in which they are first used. */ configuration @@ -172,7 +26,7 @@ configuration $PGM:K //The initial program loaded by krun. For full mode and preprocessing this is - //the initial java program, for execution mode it is the folded java program. + //the initial Java program, for execution mode it is the folded Java program. $PGM:K ProcTypeNamesPhase @@ -391,4 +245,152 @@ configuration +/*@ +\paragraph{Initial state} The first row contains three cells most relevant to computation initial state: +\begin{itemize} + \item \cellref[K]{k} --- Holds the current computation in all phases of the semantics. Initializes with the AST representation of the program. + \item \cellref[K]{program} --- A backup of program AST. Required because the initial AST is needed in both 1st ans 2nd phase of static K-Java, but the first phase destroys the content inside \cellref{k}. Also used in the last phase (Folding) to assemble the preprocessed program. + \item \cellref[GlobalPhase]{globalPhase} --- The current computation global phase. +\end{itemize} + +\paragraph{Process Type Names} During this phase, one global cell is computed: +\begin{itemize} + \item \cellref[Map{[}PackageId \mapsto Map{[}Id\mapsto{}ClassType{]}{]}]{namesToClasses} --- A two-level map. First level is a map from package names to second-level maps. Second-level maps are from simple class names to fully qualified class names within the package. This cell is extensively used through the semantics. The map contains both top-level and inner classes. For inner classes, their enclosing package is the fully qualified class name of the directly enclosing class. +\end{itemize} + +Also during Process Type Names classes are first registered. Again, both top-level and inner classes are covered. In a newly created \cellref[]{class} just a few sub-cells are initialized with data: + +\begin{itemize} + \item \cellref[ClassType]{classType} --- The fully qualified class name. The identifier of the class. + \item \cellref[ClassMetaType]{classMetaType} --- Represents whether the type stored in this cell is class or interface. To avoid terminology superfluousness, we will refer hereafter to both classes and interfaces as "classes", making distinctions only when necessary. + \item \cellref[ClassAccessMode]{classAccessMode} --- The access modifier of the class, either public or package. + \item \cellref[ClassPhase]{classPhase} --- Represents the state of this class. In addition to the global computation phase, each class has its own lifecycle phase. Class phases are required to keep track which classes were processed in the current global phase and which were not. During each global phase all classes should transition to a certain class phase. However, as we shall see, not all global phases change the state of the class. The class phases are: + + \begin{itemize} + \item Discovered --- The initial phase. At the end of Process Type Names all classes are in the state "Discovered". + \item Stored + \item Bases Resolved + \item Declaration Processed + \item Members Processed + \item Folded + \end{itemize} + +\end{itemize} + +\paragraph{Process Compilation Units} At the beginning of this phase computation is again initialized with the initial AST from \cellref{program}. The following new cells are filled in inside each \cellref{class}: + +\begin{itemize} + \item \cellref[ClassType]{enclosingClass} --- The directly enclosing class, for inner classes, or no value for top-level classes. + \item \cellref[K]{rawExtends} --- The extends clause of this class, in its raw (AST) form. + \item \cellref[K]{rawImplements} --- The implements clause, in AST form. + \item \cellref[K]{rawDeclarations} --- The class body, in AST form. + \item \cellref[Map{[}Id \mapsto ClassType{]}]{cuImports} --- A map from names accessible inside this class to fully qualified class names they represent. Only computed for top-level classes at this phase. For inner classes this cell remains empty. + \item \cellref[ContextType]{classContextType} --- Either static or instance, for inner classes. Always static for top-level classes. +\end{itemize} + +The class phase changes from Discovered to Stored. As we can see, the cells computed so far contain all the data of the original program. Thus, initial AST representation of the program is no longer needed. In fact, the cell \cellref[]{program} is discarded at the end of Process Compilation Units. The remaining preprocessing phases will use class data in this initial form to compute other cells within \cellref[]{class}, finally used for execution. + + +Also during Process Compilation Units the following global cell is used: + +\begin{itemize} + \item \cellref[Map{[}Id \mapsto ClassType{]}]{compUnitImports} --- A map from all type names accessible in the current compilation unit (Java file) to their respective fully qualified class names. This includes both classes accessible through imports declarations and classes declared in the package of the current compilation unit. Used to compute \cellref{cuImports} of top-level classes. +\end{itemize} + +\paragraph{Process Class Declarations} Here each class passes through two more class phases: Bases Processed and Declarations Processed. First, for each class the semantics attempts to resolve its extends/implements clauses into fully qualified class names. The order in which dependencies are resolved depends on both class inheritance relationships as well as nesting relationships. Once the dependencies of a class are resolved, they are stored into a temporary cell: + +\begin{itemize} + \item \cellref[K]{unprocessedBases} --- Initialized with the list of fully qualified class names for classes mentioned in extends/implements clauses of this class. +\end{itemize} + +Once the content of \cellref[]{unprocessedBases} is created, the class enters into Bases Resolved phase. It then waits in this phase until all classes referred in extends/implements reach the phase Declarations Processed. The restrictions in JLS related to class dependencies guarantee that classes cannot have cyclic dependencies, thus a class cannot get locked in the waiting state. The cell \cellref[]{unprocessedBases} is used to determine the moment when the class may exit the waiting state. Once a class reaches the phase Declarations Processed, is is deleted from cells \cellref[]{unprocessedBases} of other classes. Thus, when all extends/implements dependencies of a class reach the phase Declarations Processed, the content of the its \cellref[]{unprocessedBases} cell becomes empty. Once in this state, the class enters into the phase Declarations Processed itself and computes three more cells: + +\begin{itemize} + \item \cellref[ClassType]{extends} --- The base class, fully qualified. + \item \cellref[Set{[}ClassType{]}]{implements} --- The list of directly implemented interfaces, fully qualified. + \item \cellref[Map{[}Id \mapsto ClassType{]}]{imports} --- The map of classes accessible by simple name within the body of this class. The rules for computing this map are complex and include the following sources: + + \begin{itemize} + \item Imports declarations of the current compilation unit. + \item Classes declared within the package of the current compilation unit. + \item Classes accessible within the body of the directly enclosing class, if the current class is inner class. + \item Inner classes inherited from base classes, e.g. from extends/implements clauses. + \item Inner classes of this class itself. + \end{itemize} + + The need to cover all these cases leads to the intricate order in which class dependencies have to be be resolved. +\end{itemize} + +When a class enters the phase Declarations Processed, the cells \cellref[]{rawExtends}, \cellref[]{rawImplements} and \cellref[]{unprocessedBases} are no longer needed and are discarded. Once all classes reach this phase the computation proceeds to the next global phase. + +During Process Class Declarations the following global cell is first used: +\begin{itemize} + \item \cellref[ClassType]{crntClass} --- The current class. Used in multiple phases starting from Process Class Declarations. +\end{itemize} + +\paragraph{Process Class Members} During this phase each class processes its members and reaches the state Members Processes. Until then, the class body is stored in \cellref[]{rawDeclarations}. A class member could be one of: + +\begin{itemize} + \item field + \item method + \item constructor + \item static or instance initializer +\end{itemize} + +The following new class cells are produced: + +\begin{itemize} + \item \cellref[Set{[}ClassType{]}]{implTrans} --- The transitive closure of implemented interfaces. In the remaining phases this set is used by the subtyping relationship. + \item \cellref[ Map {[} Signature \mapsto ClassType {]} ]{methods} --- The map of accessible methods. Keys are method signatures, values are classes where methods are defined. Includes both methods declared within this class as well as methods inherited from base classes/ base interfaces. + \item \cellref[Bag]{methodDecs} --- The collection of method declarations (\cellref{methodDec} cells)in the current class. This cell contains only a subset of methods from \cellref{methods}, as the set of accessible methods from \cellref{methods} also includes methods inherited from base classes/interfaces. Hence the need of two separate collections. Each \cellref[Bag]{methodDec} contains the following data: + \begin{itemize} + \item \cellref[Signature]{methodSignature} --- The method signature, acting as identifier of the \cellref{methodDec}. + \item \cellref[Type]{methodReturnType} --- The method return type. + \item \cellref[ List{[} Param {]} ]{methodParams} --- The method parameters. + \item \cellref[K]{methodConstrFirstLine} --- the first line of a constructor (if this method is indeed a constructor, for other classes than \verb|Object|). It contains a call to another constructor: either \verb|super()| or \verb|this()|. + \item \cellref[K]{methodBody} --- The method body. + \item \cellref[AccessMode]{methodAccessMode} --- The method access mode. + \item \cellref[ContextType]{methodContextType} --- May be either static or instance. + \item \cellref[MethodMetaType]{methodMetaType} --- May be either method or constructor. + \end{itemize} + \item \cellref[K]{instanceFields} --- The list of instance field declarations, stored as a list of local variable declaration statements, without initializers. Used during object instantiation. + \item \cellref[K]{instanceInit} --- The list of instance initializers of the class combined into one big instance initializer. Instance field initializers are also concatenated into this cell in their textual order. + \item \cellref[K]{staticFields} --- The list of static field declarations, in a similar format to \cellref{instanceFields} + \item \cellref[K]{staticInit} --- The list of static initializers and static field initializers concatenated into one block. + \item \cellref[Map{[}Id \mapsto Value{]}]{constantEnv} --- The map from compile-time constants to their actual values. Constants in Java have a slightly different semantics compared to final static fields. In particular, accessing them don't trigger static initialization of the declaring class. +\end{itemize} + +Once all the cells above are computed the class proceeds into the phase Members Processed and the cell \cellref[]{rawDeclarations} is deleted. + +\paragraph{Elaboration} Here all the code blocks are processed --- method and constructor bodies, static and instance initializers. Most of the information traditionally inferred by the compiler is computed at this phase. More precisely the elaboration performs the following transformations: + +\begin{itemize} + \item Each name is resolved into local variable, field, method, class or package. While a method may be distinguished from other categories purely syntactically, resolving to other categories requires knowledge of the names existing in the current context. + \item Simple class names are resolved into fully qualified class names. Hereafter all the class names in the code are fully qualified. + \item The compile-time type of each expression is inferred. Thus, when the code reaches execution phase, expressions are no longer in their initial form. The expressions are annotated with their types. + \item For each method call the precise signature in inferred. + \item Local and anonymous classes are processed. The earliest phase where local classes could be discovered is elaboration. Still, local classes have all the features of other classes. Thus they need to be passed through all the preprocessing steps. The whole preprocessing for local classes is performed during the global phase elaboration. +\end{itemize} + +Despite this phase being the most complex preprocessing phase of all, it introduces few new cells. Most of them are related to local classes. Inside \cellref[]{class} just one new cell is introduced: + +\begin{itemize} + \item \cellref[Map{[}Id \mapsto Type{]}]{enclosingLocalEnv} --- The map from local variables of the current block to their types. Used during local classes processing. +\end{itemize} + +Among global cells the following new cells are added: + +\begin{itemize} + \item \cellref[List[mapWrap(Map[Id \mapsto Type])]]{elabEnv} --- A stack where each layer is a map of local variables. Each layer of the stack represents a code block, in the blocks nesting order. Inside each layer, the map is from local variables accessible in that layer to variable types. + \item \cellref[Int]{contextType} --- The context type of the currently elaborated class. Either static or instance. + \item \cellref[List[mapWrap(Map[Id \mapsto ClassType])]]{localTypes} --- A cell similar in structure to \cellref{elabEnv}. This time it contains stack layers which are maps from local class names to local class types. + \item \cellref[Int]{nextLocalId} --- A number used to generate unique fully-qualified class names for local classes. + \item \cellref[K]{elabBuffer} --- A temporary cell used during elaboration of local classes. +\end{itemize} + +During the elaboration phase no cells are consumed. Instead, the code blocks stored inside \cellref[]{methodDecs}, \cellref[]{instanceInit}, \cellref[]{staticInit} are processed and stored back into the same cell. After elaboration the classes remain in the same state --- Members Processed. The state Members Processed is in fact the final state of the cell \cellref[]{class}. + +\paragraph{Folding} During the last phase of static semantics the program is assembled from \cellref{classes} back into the AST form. First the content of each class is assembled into \cellref[K]{folded} of the respective class, and the class phase changes to Folded. Second, the AST representation of each class is appended into \cellref{program}. When this phase ends, the content of \cellref{program} is printed to the standard output. +*/ + endmodule diff --git a/src/prep/core-preprocessing.k b/src/prep/core-preprocessing.k index a7af1cbc..b9df9e04 100644 --- a/src/prep/core-preprocessing.k +++ b/src/prep/core-preprocessing.k @@ -2,12 +2,14 @@ module CORE-PREPROCESSING imports CORE-SORTS imports CORE-FUNCTIONS -//@ Auxiliary functions related to preprocessing phases only. +/*@ Most commonly used auxiliary functions related to preprocessing semantics only. +This module is designed to be included in most other modules of preprocessing. +*/ -//@ \subsection{Auxiliary constructs for retrieving a set of classes} +//@ \subsection{Class-related functions} -/*@ Returns a setWrap(Set[ClassType]), containing all top level classes in the program. - Uses to compute the result. Used by the starting rule of several preprocessing phases. +/*@ Returns a \verb|setWrap(Set[ClassType])|, containing all top level classes in the program. + Uses \verb|| to compute the result. Used by the starting rule of several preprocessing phases. */ syntax KItem ::= "getTopLevelClasses" | getTopLevelClasses ( Map, Set ) @@ -35,8 +37,8 @@ rule [getTopLevelClasses-not-top-level]: rule getTopLevelClasses(_ (_ |-> mapWrap(.Map) => .Map), _) rule getTopLevelClasses(.Map, ClassesSet:Set) => setWrap(ClassesSet) -/*@ Returns a setWrap(Set[ClassType]), containing all direct inner classes of the given class. - Uses to compute the result. +/*@ Returns a \verb|setWrap(Set[ClassType])|, containing all direct inner classes of the given class. + Uses \verb|| to compute the result. */ syntax KItem ::= getInnerClasses ( ClassType ) | getInnerClasses ( Map, Set ) @@ -56,6 +58,8 @@ rule [getInnerClasses-no-inners]: when notBool toPackage(Class) in keys(TypeNamesMap) +//@ \subsection{Method-related functions} + //@ Returns the access mode of a method closure given as argument syntax KItem ::= getMethodAccessMode ( MethodRef ) [strict] rule [getMethodAccessMode]: diff --git a/src/prep/elaboration-arrays.k b/src/prep/elaboration-arrays.k index 3765ec9c..d4327e83 100644 --- a/src/prep/elaboration-arrays.k +++ b/src/prep/elaboration-arrays.k @@ -2,7 +2,7 @@ module ELABORATION-ARRAYS imports CORE-SORTS imports ELABORATION-CORE -//@ \subsection{Desugaring of array declarators with c-style dimensions and initializers} +//@ \subsection{Desugaring of c-style array declarators} /*@ C-style array declaration Applied in both elaboration and execution phase @@ -73,7 +73,7 @@ rule [Param-ArrayVarDecId-Discard]: ( 'ArrayVarDecId( X:Id,, [.KList] ) => X ) ) [structural, anywhere] -/*@ \subsection{Elaboration of array-related expressions} */ +/*@ \subsection{Main array-related expressions} */ rule [elabEnd-ArrayAccess]: elabEnd('ArrayAccess(cast(arrayOf T:Type, TargetExp:K),, IndexTE:K)) diff --git a/src/prep/elaboration-categories.k b/src/prep/elaboration-categories.k index feaa1280..ceea524c 100644 --- a/src/prep/elaboration-categories.k +++ b/src/prep/elaboration-categories.k @@ -1,5 +1,10 @@ module ELABORATION-CATEGORIES +/*@ +This module contains a few auxiliary functions governing what AST labels should be processed by default +rules for elaboration, and which ones need custom rules. + +*/ /*@ Java KLabels that are processed by default heating/cooling rules of elaboration. All KLabels that can be part of a code block during elaboration phase, except those members of customElabChildren or isElabNaked groups. @@ -210,10 +215,10 @@ rule defaultElabHeating('Id) => true*/ rule defaultElabHeating('stmtAndExp) => true /*@ Naked terms are those that should be computed directly into KResult during elaboration. - Those are literals, types and packages. They are heated "as is", without being wrapped into elab(). + Those are literals, types and packages. They are heated "as is", without being wrapped into \verb|elab()|. An exception is the class literal that is not executed during elaboration. - Some auxiliary functions are also included in this cathegory in order to reduce the usage of elaboration wrappers. + Some auxiliary functions are also included in this category in order to reduce the usage of elaboration wrappers. */ syntax KItem ::= isElabNaked ( K ) [function] rule isElabNaked(RV:RawVal) => true @@ -227,12 +232,16 @@ rule isElabNaked('PackageOrTypeName(_)) => true rule isElabNaked('Id(_)) => true rule isElabNaked('Lit(InnerKL:KLabel(_))) => InnerKL =/=KLabel 'Class -/*@ Terms that should use custom elaboration rules. For those terms: - - They will not be automatically heated from their parents into the elab() state. - - They will not be automatically passed to elabDispose() state. Instead, those terms should have custom rules - for elaboration start (heating) and elaboration end (cooling). - Since all the automatic elaboration-related rules are an incredible mess, we have to put all the AST terms into this - cathegory one by one, and eliminate automatic elaboration heating/cooling rules altogether. +/*@ +\begin{markdown} +Terms that should use custom elaboration rules. For those terms: + + - They will not be automatically heated from their parents into the \verb|elab()| state. + - They will not be automatically passed to \verb|elabDispose()| state. Instead, those terms should have custom rules for elaboration start (heating) and elaboration end (cooling). + +Since all the automatic elaboration-related rules are an incredible mess, we have to put all the AST terms into this + category one by one, and eliminate automatic elaboration heating/cooling rules altogether. +\end{markdown} */ syntax KItem ::= customElabChildren ( KLabel ) [function] rule customElabChildren(KL:KLabel) => diff --git a/src/prep/elaboration-core.k b/src/prep/elaboration-core.k index 7e640b34..03b5f4f2 100644 --- a/src/prep/elaboration-core.k +++ b/src/prep/elaboration-core.k @@ -5,61 +5,70 @@ module ELABORATION-CORE imports ELABORATION-EXPRESSIONS // for isExpressionLabel /*@ -Elaborate the composition of code blocks of a class - the last step of preprocessing. +\begin{markdown} +\subsection{Elaboration phase --- introduction} + +In this phase we elaborate the content of code blocks inside a class --- the last step of preprocessing +(besides Folding). During this phase we inspect the contents of method bodies, instance initializers and static initializers of a class and perform the following transformations: \begin{itemize} \item each variable name x is resolved into either: \begin{itemize} - \item x - a local var - \item Class.x - a static var defined in the class Class - \item field(obj, Class, x) - a field of object obj declared in the class Class. + \item x --- a local var + \item Class.x --- a static var defined in the class Class + \item \verb|field(obj, Class, x)| --- a field of object obj declared in the class Class. Term obj could also be 'This. \end{itemize} \item each method name is resolved into either: \begin{itemize} - \item Class.m - a static method defined in the class Class - \item method(obj, Class, x) - an instance method of object obj declared in the class Class. + \item Class.m --- a static method defined in the class Class + \item \verb|method(obj, Class, x)| --- an instance method of object obj declared in the class Class. Term obj could also be 'This. The actual version of the method will be looked up at runtime. \end{itemize} \item each method signature is resolved into its appropriate overloaded version. To denote the version, each actual parameter will be casted to the type of the actual parameter. - \item each expression Exp will be replaced with a corresponding typed expression cast(T, Exp), + \item each expression Exp will be replaced with a corresponding typed expression \verb|cast(T, Exp)|, T being the compile-time type of the expression. \end{itemize} - /smallskip - During elaboration, elaborated members will be wrapped into elab(). +\smallskip +During elaboration, elaborated members will be wrapped into \verb|elab()|. + +During elaboration an expression transition through 6 phases: - During elaboration an expression transition through 6 phases: 1. Elaboration heating: elab('CastRef(\_,, 'Minus('ExprName(x)))) => elab('Minus('ExprName(x)) ~> elab('CastRef(\_,, HOLE) Some AST terms, especially some statements require custom elaboration heating rules. If the heated expression should be always computed into a KResult, such as a type, package or certain literal expresssions, then - it is heated in the "naked" form, e.g. not wrapped into elab(). + it is heated in the "naked" form, e.g. not wrapped into \verb|elab()|. 2. Elaboration of children. All the children of the expression are elaborated. After this phase elaborated children - will be typed (if they are expressions) and wrapped into elabRes(). Typed expressions are cast expressions - - like cast(T, Exp). The whole initial term will be converted into: - elab('Minus(elabRes(cast(int, localVar(X))))) ~> elab('CastRef(\_,, HOLE) - 3. Initiation of the step elabDispose. When all children have been elaborated and are either KResult of elabRes(), - the wrapper is changed from elab() to elabDispose(). - elabDispose('Minus(elabRes(cast(int, localVar(X))))) ~> elab('CastRef(\_,, HOLE) - 4. Unwrapping of children. During elabDispose step elaborated children are unwrapped from their elabRes() wrapper. - elabDispose('Minus(cast(int, localVar(X)))) ~> elab('CastRef(\_,, HOLE) + will be typed (if they are expressions) and wrapped into \verb|elabRes()|. Typed expressions are cast expressions - + like \verb|cast(T, Exp)|. The whole initial term will be converted into: + elab('Minus(elabRes(cast(int, localVar(X))))) ~> elab(CastRef(\_,, HOLE) + 3. Initiation of the step elabDispose. When all children have been elaborated and are either KResult of \verb|elabRes()|, + the wrapper is changed from \verb|elab()| to \verb|elabDispose()|. + elabDispose('Minus(elabRes(cast(int, localVar(X))))) ~> elab(CastRef(\_,, HOLE) + 4. Unwrapping of children. During elabDispose step elaborated children are unwrapped from their \verb|elabRes()| wrapper. + elabDispose('Minus(cast(int, localVar(X)))) ~> elab(CastRef(\_,, HOLE) 5. End of the step elabDispose. When all children of the term wrapped into elabDispose have been unwrapped - from their elabRes() wrapper, the root wrapper is replaced from elabDispose to elabEnd. This contributes + from their \verb|elabRes()| wrapper, the root wrapper is replaced from elabDispose to elabEnd. This contributes to more simple rules for the following steps. - elabRes('Minus(cast(int, localVar(X)))) ~> elab('CastRef(\_,, HOLE) + elabRes('Minus(cast(int, localVar(X)))) ~> elab(CastRef(\_,, HOLE) 6. Computation of elaboration result. Now that all children have been elaborated and unwrapped, it is possible to compute the type of the current expression itself. When the expression is fully elaborated, it is wrapped into - elabRes(). This is the step that requires custom rules for most AST terms. - elabRes('Minus(cast(int,cast(int, localVar(X))))) ~> elab('CastRef(\_,, HOLE) - 7. Elaboration cooling. Once the top K Item was wrapped into elabRes, it is ready to be cooled back into its original - context: + \verb|elabRes()|. This is the step that requires custom rules for most AST terms. + elabRes('Minus(cast(int,cast(int, localVar(X))))) ~> elab(CastRef(\_,, HOLE) + 7. Elaboration cooling. Once the top K Item was wrapped into elabRes, it is ready to be cooled back into its original context: elab('CastRef(\_,, elabRes('Minus(cast(int,cast(int, localVar(X))))))) +\end{markdown} + +Module ELABORATION-CORE contains the backbone of elaboration phase. */ +/*@ \subsection{Core auxiliary definitions}*/ + /*@Custom hole used for custom heating/cooling rules in the elaboration phase.*/ syntax KItem ::= "CHOLE" @@ -70,55 +79,6 @@ syntax KItem ::= elab ( K ) syntax ElabKResult ::= elabRes ( K ) rule isElabKResult(KR:KResult) => true -/*@ \subsection{Operator ??}*/ - -/*@ Chain of responsibility pattern. -Evaluate the first argument. if it is KResult (except noValue) or elabRes(), the result of the ?? expression is -the result of the first argument. Otherwise, if the first argument evaluates to noValue, the result of the -?? expression is the result of the second argument. -*/ -syntax KItem ::= K "??" K [right] - -rule [chainOfResponsibility-Heat]: - (. => Arg1) ~> (Arg1:K => CHOLE) ?? _ -when - notBool isElabKResult(Arg1) ==K true - -rule [chainOfResponsibility-Result1]: - ElabRes:ElabKResult ~> (CHOLE ?? _) => ElabRes -when ElabRes =/=K noValue - -rule [chainOfResponsibility-Result2]: - noValue ~> (CHOLE ?? K:K) => K - -/*@ Computes to true if the given argument is a list of elaboration results, false otherwise. - An elaborated result is either: - - KResult - - elabRes(...) - - It is notably NOT a cast() expression. This, together with the fact that cast() has no elaboration heatig rules, - makes the whole elaboration phase non-reentrant. -*/ -syntax KItem ::= isElabKList ( KListWrap ) [function] -rule isElabKList([ElabKR:ElabKResult,, Ks:KList]) => isElabKList([Ks]) -rule isElabKList([.KList]) => true - -//@ Elaborate parameter type, if not elaborated yet. For catch clause. -context elab('Param(_:K,, HOLE,, _:Id)) - -/*@Adds params to the . Used in both ELABORATION-TOP-BLOCKS and ELABORATION-BLOCKS -*/ -rule [elab-Param]: - elab('Param(K1:K,, T:Type,, X:Id)) => elabRes('Param(K1:K,, T:Type,, X:Id)) ... - ListItem(mapWrap((. => X |-> T) _)) ... - -//@Removes the last layer from -syntax KItem ::= "removeLastElabEnv" -rule [removeLastElabEnv]: - removeLastElabEnv => . ... - ListItem(_) => . ... - ListItem(_) => . ... - /*@ \subsection{Elaboration of code blocks} */ /*@ Heating arguments for both expression and statement terms. @@ -126,7 +86,7 @@ The attribute [transition-strictness] is used as transition attribute for testin This is a rule that may lead to unexpected nondeterminism if it is wrongly implemented. In order to expose incorrect nondeterminism we need to model-check a program that exposes the nondeterminism. -Labels that are "naked" should be heated in their pure form. Other terms should be heated wrapped into elab(). +Labels that are "naked" should be heated in their pure form. Other terms should be heated wrapped into \verb|elab()|. */ rule [elab-heat-default]: (. => #if isElabNaked(K) ==K true @@ -144,7 +104,7 @@ rule [elab-cool-default]: (ElabK:ElabKResult => .) ~> elab(_:KLabel(_,, (CHOLE => ElabK),, _)) /*@ Must be true for AST nodes that require elaboration heating of their children. For the arguments KL, Ks, -the original node is of he form KL(KS,,\_) and the heated child is always the last element of Ks. +the original node is of he form \verb|KL(KS,,\_)| and the heated child is always the last element of Ks. Thus it is possible to decide whether the child is allowed to be heated based both on the position of the child in the list of arguments as well as based on the state of previous brothers. @@ -155,12 +115,17 @@ defaultElabHeating. The predicate definition is scattered across modules related to elaboration.*/ syntax KItem ::= customElabHeating ( KLabel, KListWrap ) [function] -/*@ The default algorithm of transforming the term from elab to elabRes, when the children were completely elaborated. +/*@ +\begin{markdown} +The default algorithm of transforming the term from elab to elabRes, when the children were completely elaborated. Deletes elabRes wrappers from children. This algorithm is activated when the following conditions apply: - - term is not customElabChildren - - term children are completely elaborated - isElab(children) - - term is not naked. This case should never be true, but there is some weird case that requires it. - When the default algorithm is not appropriate, the respective term should be in the cathegory customElabChildren + + - term is not customElabChildren + - term children are completely elaborated --- \verb|isElab(children)| + - term is not naked. This case should never be true, but there is some weird case that requires it. + +When the default algorithm is not appropriate, the respective term should be in the category customElabChildren +\end{markdown} */ syntax KItem ::= elabDispose ( K ) @@ -179,7 +144,7 @@ rule [elabDispose-to-elabEnd]: when notBool haveElabRes([Ks]) ==K true -//@ True if given KList has no terms of the form elabRes(...), false otherwise. +//@ True if given KList has no terms of the form \verb|elabRes(...)|, false otherwise. syntax KItem ::= haveElabRes ( KListWrap ) [function] rule haveElabRes([_,, elabRes(_),, _]) => true @@ -187,7 +152,7 @@ rule haveElabRes([_,, elabRes(_),, _]) => true rule haveElabRes([_,, KList2KLabel _,, elabRes(_),, _ (_),, _]) => true /*@ The 3rd elaboration-phase wrapper for expressions. Represents the case when children are completely elaborated and -unwrapped from elabRes(), but root node might not be elaborated yet. The implementation is scattered across all modules +unwrapped from \verb|elabRes()|, but root node might not be elaborated yet. The implementation is scattered across all modules that deal with the elaboration phase. */ syntax KItem ::= elabEnd ( K ) @@ -229,9 +194,25 @@ rule [elabEnd-findQualifierOfType-top-level]: rule [elabEnd-findQualifierOfType-static]: findQualifierOfType(noClass, K:K) => noValue -/*@ \subsection{Elaboration of statements - step elabEnd} */ +/*@ +\begin{markdown} +Computes to true if the given argument is a list of elaboration results, false otherwise. +An elaborated result is either: + + - KResult + - \verb|elabRes(...)| -/*@ Applies to all nodes that are not expressins - statements and non-expression auxiliary functions + It is notably NOT a \verb|cast()| expression. This, together with the fact that \verb|cast()| has no elaboration heatig rules, + makes the whole elaboration phase non-reentrant. +\end{markdown} +*/ +syntax KItem ::= isElabKList ( KListWrap ) [function] +rule isElabKList([ElabKR:ElabKResult,, Ks:KList]) => isElabKList([Ks]) +rule isElabKList([.KList]) => true + +/*@ \subsection{Elaboration of statements --- the step elabEnd} */ + +/*@ Applies to all nodes that are not expressions --- statements and non-expression auxiliary functions */ rule [elabEnd-default-all-except-expressions]: elabEnd(KL:KLabel(Ks:KList)) => elabRes(KL(Ks)) @@ -248,7 +229,7 @@ rule elabEnd( stmtAndExp(Stmt:K, cast(T:Type, Exp:K)) ) #else elabRes(cast(T:Type, Exp:K)) #fi -/*@ \subsection{Elaboration of KListWrap - the list of terms} */ +/*@ \subsection{Elaboration of KListWrap --- the list of terms} */ //K bug: this section is a workaround t a serious K' bug that prevents [...] to be properly heated and cooled rule [elab-heat-KListWrap]: @@ -280,4 +261,34 @@ when rule [elab-to-elabRes-KListWrap-empty]: elab([.KList]) => elabRes([.KList]) +/*@ \subsection{Auxiliary functions for other modules}*/ + +//@Removes the last layer from \verb|| +syntax KItem ::= "removeLastElabEnv" +rule [removeLastElabEnv]: + removeLastElabEnv => . ... + ListItem(_) => . ... + ListItem(_) => . ... + +/*@ \subsubsection{Operator ??}*/ + +/*@ Chain of responsibility pattern. +Evaluate the first argument. if it is KResult (except noValue) or \verb|elabRes()|, the result of the ?? expression is +the result of the first argument. Otherwise, if the first argument evaluates to noValue, the result of the +?? expression is the result of the second argument. +*/ +syntax KItem ::= K "??" K [right] + +rule [chainOfResponsibility-Heat]: + (. => Arg1) ~> (Arg1:K => CHOLE) ?? _ +when + notBool isElabKResult(Arg1) ==K true + +rule [chainOfResponsibility-Result1]: + ElabRes:ElabKResult ~> (CHOLE ?? _) => ElabRes +when ElabRes =/=K noValue + +rule [chainOfResponsibility-Result2]: + noValue ~> (CHOLE ?? K:K) => K + endmodule diff --git a/src/prep/elaboration-expressions.k b/src/prep/elaboration-expressions.k index fec53d0d..5223c96a 100644 --- a/src/prep/elaboration-expressions.k +++ b/src/prep/elaboration-expressions.k @@ -4,13 +4,18 @@ module ELABORATION-EXPRESSIONS imports ELABORATION-CORE imports PRIMITIVE-TYPES -/*@ \subsection{Elaboration of numeric expressions} +/*@ \subsection{Numeric, boolean and String operators} -Expression labels are not converted by the default rule in the phase elabDispose() => elabRes(...) +Expression labels are not converted by the default rule in the phase \verb|elabDispose()| => \verb|elabRes(...)| Each expression needs a specialized rule for disposing, that will compute, among others, the type of the expression. */ +rule [elabEnd-BoolResultBinaryExp]: + elabEnd(KL:KLabel(TE1:K,, TE2:K)) => elabRes(cast(bool, KL(TE1,,TE2))) +when + isBoolResultBinaryExpLabel(KL) ==K true + syntax KItem ::= isBoolResultBinaryExpLabel ( KLabel ) [function] rule isBoolResultBinaryExpLabel('LazyOr) => true rule isBoolResultBinaryExpLabel('LazyAnd) => true @@ -21,11 +26,6 @@ rule isBoolResultBinaryExpLabel('Gt) => true rule isBoolResultBinaryExpLabel('LtEq) => true rule isBoolResultBinaryExpLabel('GtEq) => true -rule [elabEnd-BoolResultBinaryExp]: - elabEnd(KL:KLabel(TE1:K,, TE2:K)) => elabRes(cast(bool, KL(TE1,,TE2))) -when - isBoolResultBinaryExpLabel(KL) ==K true - rule [elabEnd-BoolOnlyResultExp-unary]: elabEnd('Not(TE:K)) => elabRes(cast(bool,'Not(TE))) @@ -71,6 +71,15 @@ rule [elabEnd-StringPlusAny]: when typeOf(TE1) ==K classString orBool typeOf(TE2) ==K classString +/*@ Heats the second argument, that is reduced into a type. + The whole expression is then rewritten into elabRes(cast(SecondArgAsType, FirstArg)) + We cannot eliminate this wrapper because the second argument in all usage places is not a function. +*/ +syntax KItem ::= elabExpAndType ( K, K ) [strict(2)] +rule elabExpAndType(K:K, T:Type) => elabRes(cast(T, K)) + +/*@ \subsection{Conditional operator}*/ + rule [elabEnd-Cond]: elabEnd('Cond(CondTE:K,, TE1:K,, TE2:K)) => elabExpAndType('Cond(CondTE,, TE1,, TE2), condType(typeOf(TE1), typeOf(TE2))) @@ -93,12 +102,7 @@ when rule [condType-FirstChar]: condType(char, T2:Type) => ifAux(subtype(char, T2), T2, int) -/*@ Heats the second argument, that is reduced into a type. - The whole expression is then rewritten into elabRes(cast(SecondArgAsType, FirstArg)) - We cannot eliminate this wrapper because the second argument in all usage places is not a function. -*/ -syntax KItem ::= elabExpAndType ( K, K ) [strict(2)] -rule elabExpAndType(K:K, T:Type) => elabRes(cast(T, K)) +/*@ \subsection{Assignment operator}*/ rule [elabEnd-Assign-SameType]: elabEnd('Assign(cast(T1:Type, Exp1:K),, TExp2:K)) => elabRes(cast(T1, 'Assign(Exp1,, TExp2))) @@ -114,6 +118,9 @@ when // elabEnd(KL:KLabel(cast(T1:Type, Exp1:K),, TE2:K)) => elabRes(cast(T1, KL(Exp1,, TE2))) //when // isCompoundAssignExp(KL(.KList)) ==K true + +/*@ \subsection{Cast operator} */ + rule elabEnd(cast(T1:Type, Exp1:K) *= TE2:K) => elabRes(cast(T1, Exp1 *= TE2)) rule elabEnd(cast(T1:Type, Exp1:K) /= TE2:K) => elabRes(cast(T1, Exp1 /= TE2)) rule elabEnd(cast(T1:Type, Exp1:K) %= TE2:K) => elabRes(cast(T1, Exp1 %= TE2)) @@ -126,8 +133,6 @@ rule elabEnd(cast(T1:Type, Exp1:K) &= TE2:K) => elabRes(cast(T1, Exp1 &= TE2)) rule elabEnd(cast(T1:Type, Exp1:K) ^= TE2:K) => elabRes(cast(T1, Exp1 ^= TE2)) rule elabEnd(cast(T1:Type, Exp1:K) |= TE2:K) => elabRes(cast(T1, Exp1 |= TE2)) -/*@ \subsection{Elaboration of non-numeric expressions} */ - //@ elab cast rule elabEnd('CastPrim(T:Type,, TExp:K) => cast(T, TExp)) [structural] rule elabEnd('CastRef(T:Type,, TExp:K) => cast(T, TExp)) [structural] @@ -135,13 +140,11 @@ rule elabEnd('CastRef(T:Type,, TExp:K) => cast(T, TExp)) [structural] rule [elabEnd-cast]: elabEnd(cast(T1:Type, TExp:K)) => elabRes(cast(T1, TExp)) -/*@ \subsubsection{Elaboration of class instanceof} */ +/*@ \subsection{Expressions over reference types} */ rule [elabEnd-InstanceOf]: elabEnd('InstanceOf(TExp:K,, RT2:RefType)) => elabRes(cast(bool, 'InstanceOf(TExp,, RT2))) -/*@ \subsubsection{Elaboration of class literals} */ - //@ Class literal types are heated by this rule. context elab('Lit('Class(HOLE))) diff --git a/src/prep/elaboration-method-invoke.k b/src/prep/elaboration-method-invoke.k index e74f1c98..c49ad7f6 100644 --- a/src/prep/elaboration-method-invoke.k +++ b/src/prep/elaboration-method-invoke.k @@ -4,6 +4,8 @@ module ELABORATION-METHOD-INVOKE imports SUBTYPING imports ELABORATION-CORE +//@ \subsection{Regular method calls} + rule customElabEnd('Method) => true rule elabEnd('Method(Qual:K,, _:K,, Name:Id)) => elabEnd('Method('MethodName(Qual,, Name))) [structural] @@ -56,11 +58,11 @@ rule containsName((sig(Name, _) |-> _) _:Map, Name:Id) => true rule [elabEnd-findQualifierForName-static]: findQualifierForName(noClass, K:K) => noValue -// 'SuperMethod(_:K,, Name:Id) +//@ \subsection{Superclass method calls: \texttt{super.m()}} rule customElabEnd('SuperMethod) => true -// super.X(_) +//@ \verb|super.X(_)| rule [SuperMethod-desugar]: elabEnd('SuperMethod(K:K,, Name:Id)) => elabEnd('QSuperMethod(Class,, K:K,, Name:Id)) @@ -114,10 +116,12 @@ rule getLookupTargetType(arrayOf _) => classArrayImpl syntax KItem ::= isCastOfQThis ( K ) [function] rule isCastOfQThis(cast(_, 'QThis(_))) => true +//@ \subsection{Method reference lookup} + /*@ Lookup the right methodRef() based on supplied parameters. If the method is not found in the supplied class list, we should search for it in the class list corresponding to the enclosing class of the caller class. -First we search for the signature - lookupSignature construct. +First we search for the signature --- lookupSignature construct. Afterwards we cast the actual arguments to the types expected by the found method signature.*/ syntax KItem ::= lookupMethod ( ClassType,//target class, even for arrays. @@ -217,7 +221,7 @@ syntax KItem ::= methodLookupResult ( /*@ In the past implementation, the non-empty qualifier of a static method call was moved to a separate statement in front of a method call using stmtAndExp(). - But since stmtAndExp() is incompatible with java intermediate form, we keep the non-empty qualifier + But since stmtAndExp() is incompatible with Java intermediate form, we keep the non-empty qualifier as is even for static methods. */ rule [methodProcessArguments-Invoke-end]: @@ -240,6 +244,8 @@ rule [methodProcessArguments-Invoke-end]: ) ) +//@ \subsection{Method signature lookup} + /*Search for the correct method signature to use when calling a given MethodName with the given argument types. computes mapWrap(Sig -> MethodTV)*/ @@ -304,8 +310,12 @@ when rule [lookupSignature-End]: lookupSignature(_,_, .Map,_, MethodRef:MethodRef, _) => MethodRef +//@ \subsection{Method accessibility check} +//@ Interaction between overloading and access modes. +//@ + /*@ Tests whether a method from a given class with a given AccessMode and ContextType -may be called from the current object environment*/ +may be called from the current object environment.*/ syntax KItem ::= isAccessible ( AccessMode, //the method access mode K, //evaluates to ContextType - staticCT or instanceCT diff --git a/src/prep/elaboration-new-instance.k b/src/prep/elaboration-new-instance.k index 5bb06302..c3d6a57f 100644 --- a/src/prep/elaboration-new-instance.k +++ b/src/prep/elaboration-new-instance.k @@ -7,9 +7,7 @@ module ELABORATION-NEW-INSTANCE imports ELABORATION-METHOD-INVOKE // for lookupMethod, methodLookupResult imports PROCESS-LOCAL-CLASSES //for localClassGetExtraArgs -/*@ \subsubsection{Elaboration of 'NewInstance and 'QNewInstance} */ - -/*@ elab('NewInstance()) is strict in arguments 2 and 3 - class name and constrctor arguments. +/*@ elab('NewInstance()) is strict in arguments 2 and 3 --- class name and constrctor arguments. Constrctor arguments have to be heated if this class is anonymous. */ rule customElabHeating('NewInstance, [Ks:KList]) => length([Ks]) in (SetItem(2) SetItem(3)) @@ -33,9 +31,13 @@ rule [elab-NewInstance]: EnclosingClass:ClassType CT:ContextType -/*@ elab('QNewInstance()) is strict in all its arguments except the class name (3) and anonymous body(6). +/*@ +\begin{markdown} +elab('QNewInstance()) is strict in all its arguments except the class name (3) and anonymous body(6): + - Argument (3) is heated if it is not a simple name but a precusros to a type - - Argument (6) is heated if it is 'None() - an empty body. + - Argument (6) is heated if it is 'None() --- an empty body. +\end{markdown} */ rule customElabHeating('QNewInstance, [Ks:KList,,KHole:K]) => length([Ks,,KHole]) in (SetItem(1) SetItem(2) SetItem(4) SetItem(5)) @@ -94,7 +96,7 @@ rule [elabEnd-QNewInstance-to-lookupMethod]: ) ~> elabEnd('QNewInstance(Qual:K,, Arg2:K,, Class:ClassType,, Arg4:K,, [Args:KList],, 'None(.KList))) -/*@ All new instance creation expressions are converted into qualified ones - 'QNewInstance, during elaboration phase. +/*@ All new instance creation expressions are converted into qualified ones --- 'QNewInstance, during elaboration phase. For instance inner classes, the qualifier will be a valid expression for the qualifier. For other classes qualifier will be noValue. At this stage 'QNewInstance is wrapped in elabEnd. */ diff --git a/src/prep/elaboration-statements.k b/src/prep/elaboration-statements.k index d88a84d2..54379cd3 100644 --- a/src/prep/elaboration-statements.k +++ b/src/prep/elaboration-statements.k @@ -4,7 +4,13 @@ module ELABORATION-STATEMENTS imports ELABORATION-METHOD-INVOKE //for lookupMethod imports PROCESS-LOCAL-CLASSES //for localClassGetExtraArgs -//@ Elaboration of 'KListWrap, 'Block, 'For or 'Catch - nodes that may contain variable declarations. +/*@ Only statements that need custom treatment during elaboration are included here. Most statements are elaborated by +generic rules. +*/ + +//@ \subsection{Statements for, block and catch} + +//@ Elaboration of 'KListWrap, 'Block, 'For or 'Catch --- nodes that may contain variable declarations. //K bug: support for KListWrap. This rule was replaced by a special section for elaboration of KListWrap. // See other K-bug-s. @@ -19,7 +25,7 @@ rule isVarDecHolderLabel('For) => true rule isVarDecHolderLabel('Catch) => true /*@ In addition to what defaul elab heating does, when we heat the first argument of 'Block, 'For of 'Catch -we need to save a copy of elaboration environment - e.g. the last entry of . +we need to save a copy of elaboration environment, e.g. the last entry of \verb|| \verb||. This is because these statements are blocks that might declare local variables. */ rule [elab-Block-For-Catch-heat-FirstSubterm]: @@ -42,14 +48,25 @@ rule [elabEnd-Block-For-Catch]: when isVarDecHolderLabel(KL) ==K true -//@ Local var declarations desugaring +/*@ \subsection{Elaboration of catch parameters}*/ + +//@ Elaborate parameter type, if not elaborated yet. For catch clause. +context elab('Param(_:K,, HOLE,, _:Id)) + +/*@Adds params to the \verb||. Used in both ELABORATION-TOP-BLOCKS and ELABORATION-BLOCKS +*/ +rule [elab-Param]: + elab('Param(K1:K,, T:Type,, X:Id)) => elabRes('Param(K1:K,, T:Type,, X:Id)) ... + ListItem(mapWrap((. => X |-> T) _)) ... + +//@ \subsection{Local variable declarations} rule [elab-LocalVarDecStm-desugar]: elab('LocalVarDecStm('LocalVarDec(Ks:KList)) => 'LocalVarDec(Ks) ) [structural] -//@ Resolve the local var type, required to register the var in +//@ Resolve the local var type, required to register the var in \verb|| context elab('LocalVarDec(_:K,, HOLE,, _:K)) rule [elab-LocalVarDec-multi-desugar]: @@ -74,7 +91,7 @@ rule [elab-LocalVarDec]: ListItem(mapWrap((. => X |-> T) _)) ... -//@\subsection{Elaboration of SuperConstrInv, QSuperConstrInv, AltConstrInv} +//@\subsection{Explicit constructor invocations --- \texttt{this()}, \texttt{super()}, \texttt{A.super()}} // 'SuperConstrInv( _:K,, [ Args:KList ] ) //@ Desugaring unqualified superclass constructor invocation into a qualified one diff --git a/src/prep/elaboration-top-blocks.k b/src/prep/elaboration-top-blocks.k index 73dcb1b5..768d9777 100644 --- a/src/prep/elaboration-top-blocks.k +++ b/src/prep/elaboration-top-blocks.k @@ -1,17 +1,18 @@ -/*@ This module initialtes the elaboration phase. It is responsible for elaborating all top-level code blocks - in the program: methods, constructors, static and instance initializers. -*/ module ELABORATION-TOP-BLOCKS imports CORE-SORTS imports CORE-PREPROCESSING imports ELABORATION-CORE +/*@ This module initiates the elaboration phase. It is responsible for elaborating all top-level code blocks + in the program: methods, constructors, static and instance initializers. +*/ + rule [ElaborationPhase-start]: . => elaborateBlocks(getTopLevelClasses) ProcClassMembersPhase => ElaborationPhase /*@ Elaborate the blocks inside all classes. -Argument K = setWrap(Set) - the set of all classes. +Argument K = \verb|setWrap(Set)| --- the set of all classes. */ syntax KItem ::= elaborateBlocks ( K ) [strict] @@ -37,7 +38,7 @@ rule [elaborateBlocks-discard]: elaborateBlocks(setWrap(.)) => . /*@ Elaborates the methods of the current class. The map contains the methods that were not elaborated yet. -When a class elaboration starts, the map is initialized with the contet of - all the methods accessible in +When a class elaboration starts, the map is initialized with the contet of \verb|| --- all the methods accessible in the current class. Only methods declared in the current class are elaborated. The rest are discarded from the map. */ syntax KItem ::= elabMethods ( Map ) @@ -128,7 +129,7 @@ rule [elabStaticInit-End]: Class CHOLE => K -//@Adds a new empty layer to +//@Adds a new empty layer to \verb|| syntax KItem ::= "addElabEnv" rule [addElabEnv]: addElabEnv => . ... diff --git a/src/prep/elaboration-types.k b/src/prep/elaboration-types.k index 7d41a2aa..da93a741 100644 --- a/src/prep/elaboration-types.k +++ b/src/prep/elaboration-types.k @@ -6,8 +6,6 @@ module ELABORATION-TYPES imports ELABORATION-CORE imports PROCESS-TYPE-NAMES // for getNamesMap() -/*@ \subsection{Elaboration of types} */ - rule 'ClassOrInterfaceType(TypeK:K,, _) => TypeK [structural] rule 'InterfaceType(TypeK:K,, _) => TypeK [structural] rule 'ClassType(TypeK:K,, _) => TypeK [structural] diff --git a/src/prep/elaboration-vars.k b/src/prep/elaboration-vars.k index 1ea19db9..01df1268 100644 --- a/src/prep/elaboration-vars.k +++ b/src/prep/elaboration-vars.k @@ -2,11 +2,14 @@ module ELABORATION-VARS imports CORE-SORTS imports ELABORATION-CORE -//@ Elaboration of rules in java-var-lookup +//@ Elaboration of terms defined in var-lookup.k +//@ //@ Both unqualified and qualified AmbName. rule [elabEnd-AmbName]: elabEnd('AmbName(Ks:KList)) => elabEnd('ExprName(Ks)) ?? 'TypeName(Ks) ?? 'PackageName([Ks]) +//@ \subsection{Unqualified variable references} + rule [elabEnd-ExprName-localVar-ok]: elabEnd('ExprName(X:Id)) => elabRes(cast(T, 'ExprName(X))) ... ListItem(mapWrap(X |-> T:Type _)) ... @@ -70,6 +73,22 @@ rule [elabOuterLocalVar-not-found]: when notBool X in keys(EnclosingLocalEnv) +//@ \subsection{Self-references: \texttt{this} and \texttt{A.this}} + +rule [elabEnd-This]: + elabEnd('This(.KList) => 'QThis(Class)) ... + Class:ClassType + +rule [elabEnd-QThis-InstanceCT]: + elabEnd('QThis(Class:ClassType)) => elabRes(cast(Class, 'QThis(Class))) ... + instanceCT + +rule [elabEnd-QThis-StaticCT]: + elabEnd('QThis(_)) => noValue ... + staticCT + +//@ \subsection{Fields} + rule [elabEnd-ExprName-qualified]: elabEnd('ExprName(QualK:K,,X:Id)) => elabEnd('Field(QualK,,X)) @@ -79,7 +98,13 @@ rule [elabEnd-Field-of-package]: rule [elabEnd-Field-of-noValue]: elabEnd('Field( noValue,, _:Id )) => noValue [structural] -//@Computation of instance and static environment of a class, e.g. set of fields +rule [elabEnd-Field-QualRef]: + elabEnd('Field(cast(Class:ClassType, Qual:K),, X:Id)) + => elabFieldImpl(cast(Class, Qual), elabLookup(X, Class)) + +rule [elabEnd-Field-QualClass]: + elabEnd('Field(Class:ClassType,, X:Id)) + => elabFieldImpl(noValue, elabLookup(X, Class)) /*@ Searches the given field name in the given type (set of types), both static and instance context. @@ -150,26 +175,6 @@ syntax KItem ::= nameInVarDecs( rule nameInVarDecs(X:Id, [_,, _:KLabel(.K,, T:Type,, ['VarDec(X)]),, _]) => true -rule [elabEnd-This]: - elabEnd('This(.KList) => 'QThis(Class)) ... - Class:ClassType - -rule [elabEnd-QThis-InstanceCT]: - elabEnd('QThis(Class:ClassType)) => elabRes(cast(Class, 'QThis(Class))) ... - instanceCT - -rule [elabEnd-QThis-StaticCT]: - elabEnd('QThis(_)) => noValue ... - staticCT - -rule [elabEnd-Field-QualRef]: - elabEnd('Field(cast(Class:ClassType, Qual:K),, X:Id)) - => elabFieldImpl(cast(Class, Qual), elabLookup(X, Class)) - -rule [elabEnd-Field-QualClass]: - elabEnd('Field(Class:ClassType,, X:Id)) - => elabFieldImpl(noValue, elabLookup(X, Class)) - // 'SuperField(X:Id) rule [elabEnd-SuperField]: diff --git a/src/prep/folding.k b/src/prep/folding.k index e5a75d13..f45269a5 100644 --- a/src/prep/folding.k +++ b/src/prep/folding.k @@ -7,7 +7,7 @@ rule [FoldingPhase-start]: ElaborationPhase => FoldingPhase (.Bag => [.KList] ) -/*@ The sole content of cell during FoldingPhase +/*@ The sole content of \verb|| cell during FoldingPhase */ syntax KItem ::= "foldingPhase" diff --git a/src/prep/java-prep.k b/src/prep/java-prep.k index 13a8caa8..64a5c720 100644 --- a/src/prep/java-prep.k +++ b/src/prep/java-prep.k @@ -7,6 +7,7 @@ require "../common/aux-strings.k" require "../common/primitive-types.k" require "../common/subtyping.k" require "../common/java-syntax.k" +require "../common/sort-predicate-hacks.k" require "core-preprocessing.k" require "process-type-names.k" require "process-comp-units.k" @@ -54,6 +55,7 @@ module JAVA-PREP imports JAVA-SYNTAX imports LIST-MACRO + imports SORT-PREDICATE-HACKS endmodule diff --git a/src/prep/literals.k b/src/prep/literals.k index 596bea84..1489fb73 100644 --- a/src/prep/literals.k +++ b/src/prep/literals.k @@ -94,7 +94,7 @@ rule [Lit-Octa]: #else normalize(octaToInt(trimHead(Str, 1)) :: int ) #fi -//@ \subsection{float literals} +//@ \subsection{Float literals} rule [Lit-FFloat]: 'Lit('Float(Str:String)) @@ -106,7 +106,7 @@ rule [Lit-FFloat]: #fi #fi -//@ \subsection{bool literals} +//@ \subsection{Boolean literals} /* 'Lit('Bool('True(.KList))) 'Lit('Bool('False(.KList))) @@ -116,8 +116,8 @@ rule 'Lit('Bool('True(.KList))) => true rule 'Lit('Bool('False(.KList))) => false -//@ \subsection{char literals} -//@ Chars are represented as int values, as described in java specification. +//@ \subsection{Char literals} +//@ Chars are represented as int values, as described in Java specification. // 'Lit('Char('Single( I:Int ))) rule 'Lit('Char('Single( I:Int ))) => I :: char diff --git a/src/prep/process-anonymous-classes.k b/src/prep/process-anonymous-classes.k index fd3c2e6d..24266809 100644 --- a/src/prep/process-anonymous-classes.k +++ b/src/prep/process-anonymous-classes.k @@ -116,11 +116,15 @@ rule [processAnonymousClass]: ) ) -/*@ Build the part of the constructor of an anonymous class definition corresponding +/*@ +\begin{markdown} +Build the part of the constructor of an anonymous class definition corresponding to formal params, and arguments of the superclass constructor invocation, respectively -First KList - list of actual arguments -Second KList - the result -Third arg - a counter used to generate var names + + - First KList --- list of actual arguments + - Second KList --- the result + - Third arg --- a counter used to generate var names +\end{markdown} */ syntax KItem ::= buildConstructorFormalParams ( KListWrap, KListWrap, Int ) | buildConstructorFirstLineArgs ( KListWrap, KListWrap, Int ) diff --git a/src/prep/process-class-decs.k b/src/prep/process-class-decs.k index 158d7c6c..2ad8f873 100644 --- a/src/prep/process-class-decs.k +++ b/src/prep/process-class-decs.k @@ -3,8 +3,6 @@ module PROCESS-CLASS-DECS imports CORE-PREPROCESSING imports PROCESS-TYPE-NAMES -/*@ \subsection{Third pass - processing class dependencies and imports} */ - rule [ProcClassDecsPhase-start]: . => processClassDecs(getTopLevelClasses) ProcCompUnitsPhase => ProcClassDecsPhase @@ -15,8 +13,10 @@ syntax KItem ::= processClassDecs ( ) [strict] +/*@ \subsection{Initiate the resolving of class bases}*/ + /*@ Question: how do we know if bases were already resolved for this class or not? - Answer: When resolveBases(Class) is consumed by the rule [resolveBasesEnd], the class + Answer: When \verb|resolveBases(Class)| is consumed by the rule [resolveBasesEnd], the class changes its state: StoredCPhase => BasesResolvedCPhase */ rule [processClassDecs-resolveBases-TopLevel-Start]: @@ -60,7 +60,9 @@ rule [processClassDecs-resolveBases-Inner-Start]: when OuterClassPhase ==K DecsProcessedCPhase orBool OuterClassPhase ==K MembersProcessedCPhase -//@ Process the given class from StoredCPhase to BasesResolvedCPhase. +/*@ \subsection{Resolve bases}*/ + +//@ Process the given class from StoredCPhase to BasesResolvedCPhase. Resolve the base class (arg 2) and interfaces (arg 3) of a class (arg 1). syntax KItem ::= resolveBases ( ClassType, //The class for which we resolve bases K, //Base class @@ -79,6 +81,8 @@ rule [resolveBases]: StoredCPhase => BasesResolvedCPhase when isKResult(ImplTypes) +/*@ \subsection{Processing after bases were resolved}*/ + rule [processClassDecs-mark-Base-Processed]: processClassDecs(_) ... @@ -127,7 +131,7 @@ syntax KItem ::= kListToSet ( KListWrap, //a list of some K Terms rule kListToSet([(K:K => .KList),,_], (_ (.Set => SetItem(K) ))) rule kListToSet([.KList], TypeSet:Set) => setWrap(TypeSet) -//@ Receives a kListToSet term ans saves the resulting set into +//@ Receives a kListToSet term ans saves the resulting set into \verb|| syntax KItem ::= saveImplements ( ClassType, K ) [strict(2)] rule [saveImplements]: @@ -135,9 +139,11 @@ rule [saveImplements]: Class .Set => ImplSet +/*@ \subsection{Computing imports map}*/ + /*@ Computes the full names map used to resolve classes by simple name inside the class specified by the arg 4, - and stores them inside .*/ + and stores them inside \verb||.*/ syntax KItem ::= saveImports ( ClassType, //Class - the actual class ClassType, //The outer class of this class, if any, @@ -186,11 +192,15 @@ rule [saveImports-InheritTypes]: rule [saveImports-Discard-noClass]: saveImports(_,_, [(noClass => .KList),, _], _,_,_) -/*@ Compute the final result - the combined accessible classes map, with this components in order: +/*@ +\begin{markdown} +Compute the final result --- the combined accessible classes map, with this components in order: + - external names - local block names (for local classes only) - inherited names - inner names +\end{markdown} */ rule [saveImports-ComputeResult]: @@ -210,7 +220,7 @@ rule [saveImports-ComputeResult]: BaseClass:ClassType BaseClassMap:Map -//@ Save the computed Imports map into the cell of the given class +//@ Save the computed Imports map into the \verb|| cell of the given class rule [saveImports-end]: saveImports(Class:ClassType, _,_,_,_, mapWrap(Imports:Map)) => . diff --git a/src/prep/process-class-members.k b/src/prep/process-class-members.k index 31241a1e..90693610 100644 --- a/src/prep/process-class-members.k +++ b/src/prep/process-class-members.k @@ -3,8 +3,6 @@ module PROCESS-CLASS-MEMBERS imports CORE-CLASSES imports CORE-PREPROCESSING -/*@ \subsection{Third pass - processing class members} */ - /*@ We need to process Object first. Thus when we will process any interfaces, Object class will already be processed.*/ rule [Start-ProcClassMembersPhase]: @@ -16,6 +14,8 @@ syntax KItem ::= processClasses ( ) [strict] +/*@ \subsection{Triggering the processing of depending types} */ + rule [processClasses]: (. => processTypeWithDepends(Class)) ~> processClasses(setWrap( (SetItem(Class:ClassType) => .) _:Set)) @@ -48,23 +48,29 @@ rule [processTypeWithDepends-Discard]: rule [processTypeWithDepends-Discard2]: processTypeWithDepends(noClass) => .K -syntax KItem ::= processType ( - ClassType //the class to be processed - ) +/*@ \subsection{Initiating class processing} */ -/*@ For each class compute the set of inherited interfaces, inherit all the members, -process inner declarations. Compute the following class cells: - - - - - - temporary cell, deleted after class body is processed. - - +/*@ +\begin{markdown} +For each class computes the set of inherited interfaces, inherits all the members, +processes inner declarations. Computes the following class cells: + + - \verb|| + - \verb|| + - \verb|| + - \verb|| + - \verb|| --- temporary cell, deleted after class body is processed. + - \verb|| + - \verb|| First we inherit methods from interfaces, then from the base class, and in the end we add methods declared in this class. Each new method overwrites previous methods with the same signature. +\end{markdown} */ +syntax KItem ::= processType ( + ClassType //the class to be processed + ) + rule [processType]: processType(Class:ClassType) => computeImplTrans(SetItem(BaseClass) ISet) @@ -102,7 +108,9 @@ rule [processType-discard]: Class MembersProcessedCPhase -//@ Compute cell - interfaces transitively implemented +/*@ \subsection{Inheriting base types} */ + +//@ Compute \verb|| cell --- interfaces transitively implemented syntax KItem ::= computeImplTrans ( Set ) rule [computeImplTrans]: @@ -194,7 +202,7 @@ rule isOverridden(BaseC:ClassType, package, SubC:ClassType) rule isOverridden(_, private, _) => false /*@ Inherit a method by the current class. The inherited method overwrites previous methods - with the same signature in + with the same signature in \verb|| */ syntax KItem ::= inherit ( MethodRef ) @@ -204,7 +212,7 @@ rule [inherit]: Class Env:Map => Env[DecClass/Sig] -/*@ \subsection{Method declaration} +/*@ \subsection{Method declarations} Methods are now typed and we need to store their types in their closures, so that their type contract can be checked at invocation time. The rule below is conceptually similar to that of untyped KOOL; @@ -319,6 +327,7 @@ rule [storeMethod-discard-default-constructor]: Class ... Sig |-> _ ... +/*@ \subsection{Constructor declarations}*/ rule [ConstrDec-SuperCall-Desugar]: @@ -381,6 +390,8 @@ rule [ConstrDec]: Class:ClassType when paramTypesResolved([Params]) +//@ \subsection{Instance fields and instance initializers} + // 'FieldDec(Modifiers:K,, T:Type,, ['VarDec(X:Id,, InitExp:K),, _]) //resolve field declaration type @@ -415,6 +426,21 @@ rule [InstanceInit]: [_,,(.KList => K)] [structural] +syntax KItem ::= "convertInstanceInitIntoMethod" + +rule [convertInstanceInitIntoMethod]: + + convertInstanceInitIntoMethod + => storeMethod([.KList], instanceCT, private, false::bool, methodMMT, noValue, 'Block([InstanceInitKs]), + sig(String2Id("$instance_init"), types(.KList)), void) + ... + + Class:ClassType + Class + ( [InstanceInitKs:KList] => .Bag) + +//@ \subsection{Static fields and static initializers} + /*@ Desugaring a static field declaration with initializer into a declaration without initializer. Followed by a static initializer block, if this field is not a compile-time constant.*/ rule [FieldDec-StaticInit-Desugar]: @@ -459,7 +485,7 @@ rule [ConstantDec-Desugar]: TypeK,, VarDecs ) -/*@Subsection compile-time constants*/ +/*@\subsection{Compile-time constants}*/ //compute the value of a compile-time constant context 'FieldDec(Modifiers:K,, T:Type,, ['VarDec(X:Id,, HOLE) ]) @@ -480,26 +506,15 @@ when getContextType(Modifiers) ==K staticCT andBool isFinalModifiers(Modifiers) +/*@\subsection{Other members}*/ + /*@ Discard inner class declarations at this phase. They are processed when their - respective tag is encountered as part of processClasses. + respective \verb|| tag is encountered as part of processClasses. */ rule [ClassDec-discard]: 'ClassDec(_) => . rule [InterfaceDec-discard]: 'InterfaceDec(_) => . -syntax KItem ::= "convertInstanceInitIntoMethod" - -rule [convertInstanceInitIntoMethod]: - - convertInstanceInitIntoMethod - => storeMethod([.KList], instanceCT, private, false::bool, methodMMT, noValue, 'Block([InstanceInitKs]), - sig(String2Id("$instance_init"), types(.KList)), void) - ... - - Class:ClassType - Class - ( [InstanceInitKs:KList] => .Bag) - -//@ \subsection{Auxiliary functions} +//@ \subsection{Functions for acceessing member modifiers} //@ Evaluates to true::bool if synchronized is among modifiers, false otherwise syntax KItem ::= isSynchronizedModifiers ( diff --git a/src/prep/process-comp-units.k b/src/prep/process-comp-units.k index 2f1ece8a..6939a006 100644 --- a/src/prep/process-comp-units.k +++ b/src/prep/process-comp-units.k @@ -5,33 +5,25 @@ module PROCESS-COMP-UNITS imports PROCESS-IMPORTS //for compUnitImportsStart() /*@ -ProcCompUnitsPhase: - For each CompUnit separately: -1. Process import declarations. Build . - - For each class C in CompUnit separately: -2. For each class save the cell with just the following: - - - since we process CU content recursively, should be available - - - - - just for top-level classes, imports are taken from the . - For inner classes this cell is still empty. - - - content of its 'ClassDec term. When this term is non-empty - then the class has not been preprocessed yet. - -3. Process inner classes of C. - - This way we will have fast access to the declaration of a class, and will be able to -process declarations in a less-restricted order. -*/ +\begin{markdown} +\paragraph{Module Overview} For each Compilation unit: + + - Process import declarations. Build \verb||. + +For each class C in CompUnit: + + - Add to \verb|| containing C the cells mentioned in configuration doc. + - Process inner classes of C. -/*@ \subsection{Second pass - processing declarations} */ +\end{markdown} +*/ rule [ProcCompUnitsPhase-start]: . => Program ( Program:K => .) ProcTypeNamesPhase => ProcCompUnitsPhase -//ImpDecs will be processed in the module PROCESS-IMPORTS +//@ Import declarations are processed in the module PROCESS-IMPORTS rule [CompilationUnit]: 'CompilationUnit('Some('PackageDec(_:K,, Pack:PackageId)),, @@ -62,15 +54,16 @@ rule [processTypeDecsInPCUPhase-ElemDiscard]: processTypeDecsInPCUPhase([Label:KLabel(_)], _,_) => . when notBool( Label ==KLabel 'ClassDec orBool Label ==KLabel 'InterfaceDec ) -/*@ \subsection{Class declaration processing}*/ - rule [processTypeDecsInPCUPhase-typeDec-ComputeFullName]: processTypeDecsInPCUPhase( [KL:KLabel(_:KLabel(_:K,, (SimpleClass:Id => getClassType(Pack,SimpleClass)),, _:KList),, _)], Pack:PackageId, _ ) [structural] -/* +/*@ +Structure of 'ClassDec: + +\begin{verbatim} 'ClassDec( 'ClassDecHead( [Modifiers],, @@ -79,8 +72,9 @@ rule [processTypeDecsInPCUPhase-typeDec-ComputeFullName]: 'Some('SuperDec( BaseClassRaw - extends declaration )),, 'Some('ImplementsDec([ ImplTypesRaw - implements declarations ])) ),, - 'ClassBody( [ Decls - member declarations ] ) + 'ClassBody( [ Decls --- member declarations ] ) ) +\end{verbatim} */ rule [ClassDec-NoExtendsDesugar]: @@ -180,7 +174,7 @@ rule [processTypeDecsInPCUPhase-IInterfaceDec]: _ => [Decls] _ => staticCT -/*@ If the given type is top-level, then save from the cell. +/*@ If the given type is top-level, then save \verb|| from the \verb|| cell. Otherwise do nothing.*/ syntax KItem ::= saveImportsInPCUPhase ( K //is processed into TypeName diff --git a/src/prep/process-imports.k b/src/prep/process-imports.k index cfd64418..283f759e 100644 --- a/src/prep/process-imports.k +++ b/src/prep/process-imports.k @@ -35,7 +35,7 @@ rule [TypeImportOnDemandDec]: ... Pack |-> mapWrap(PackMap:Map) ... Imp:Map -//@ Imports to cell public classes from the given map. Classes with package access are ignored. +//@ Imports to \verb|| cell public classes from the given map. Classes with package access are ignored. syntax KItem ::= importOnDemandImpl ( Map //Map[X |-> Class] - classes to consider for importing. ) diff --git a/src/prep/process-local-classes.k b/src/prep/process-local-classes.k index 6a138737..c85900ac 100644 --- a/src/prep/process-local-classes.k +++ b/src/prep/process-local-classes.k @@ -6,6 +6,8 @@ module PROCESS-LOCAL-CLASSES imports PROCESS-CLASS-MEMBERS //for processTypeWithDepends imports ELABORATION-VARS //for elabLookup +//@\subsection{Main rules} + // ClassDecStm('ClassDec(...)) rule [elab-ClassDecStm]: @@ -132,9 +134,13 @@ when rule [localClassGetAccessibleOuterEnv-end]: localClassGetAccessibleOuterEnv( Class:ClassType, .Map, NewOuterEnv:Map, _, noValue ) => mapWrap(NewOuterEnv) -/*@ Convert the given local class into an equivalent inner class, with the following transformations: +/*@ +\begin{markdown} +Convert the given local class into an equivalent inner class, with the following transformations: + - Add a field to the class for each outer local variable - For each constructor add an argument for each outer local variable +\end{markdown} */ syntax KItem ::= localClassTransformIntoInner ( ClassType, //the local class @@ -155,7 +161,7 @@ rule [localClassTransformIntoInner]: #fi /*@ Same as localClassTransformIntoInner but AccessibleLocalEnv has one more entry - - the field LocaClass@LocalEnv\_obj that will be created later, a self reference required when a local class + --- the field LocaClass@LocalEnv\_obj that will be created later, a self reference required when a local class instantiates either itself or an enclosing local class. See tests 957, 958. */ syntax KItem ::= localClassTransformIntoInnerImpl ( @@ -307,7 +313,7 @@ rule haveUnaugmentedConstructors(ConsName:Id, LocalEnvClass:ClassType, when notBool getLastKListElement([TList]) ==K LocalEnvClass -//@ Elaborates the given node and saves it to +//@ Elaborates the given node and saves it to \verb|| syntax KItem ::= appendToElabBuffer ( K ) //[strict, context(result(ElabKResult))] //K bug generalized strictness context appendToElabBuffer ( HOLE ) [result(ElabKResult)] @@ -321,12 +327,12 @@ rule [loadElabBuffer]: loadElabBuffer => elabRes(ElabBuffer) ... ElabBuffer:K => [.KList] -//@\subsection{Utility functions for other modules} +//@\subsection{Auxiliary functions for other modules} syntax KItem ::= localClassGetExtraArgs( ClassType ) -/*@ When is not empty (only possible for certain local classes), - we add one more argument to the consturctor call - the local environment object. */ +/*@ When \verb|| is not empty (only possible for certain local classes), + we add one more argument to the consturctor call --- the local environment object. */ rule [elab-QNewInstance-local-augment-arguments]: localClassGetExtraArgs(Class:ClassType) diff --git a/src/prep/process-type-names.k b/src/prep/process-type-names.k index 0a5528c6..1d4559ce 100644 --- a/src/prep/process-type-names.k +++ b/src/prep/process-type-names.k @@ -7,9 +7,9 @@ module PROCESS-TYPE-NAMES /*@ First pass - collecting globally accessible names in the program. This includes packages, top-level classes and inner classes. In each compilation unit just class declarations -(both global and inner) are processed. Results are stored in the cell . +(both global and inner) are processed. Results are stored in the cell \verb||. -The initial configuration contains the initial program in cells and , and global phase is ProcTypeNamesPhase. +The initial configuration contains the initial program in cells \verb|| and \verb||, and global phase is ProcTypeNamesPhase. */ /*@ \subsection{Compilation units}*/ @@ -33,7 +33,7 @@ rule [CompilationUnit]: ProcTypeNamesPhase -/*@ \subsection{Packages}*/ +/*@ \subsection{Package declarations}*/ // 'PackageName([Ks]) @@ -72,9 +72,14 @@ rule [processTypeNames-AddPackage]: PackMap:Map => PackMap[mapWrap(.Map) / PackId] when notBool PackId in keys(PackMap) -/*@ A type name is either class or interface name. Anonymous labels will be one of: - - 'ClassDec('ClassDecHead(...)) - - 'InterfaceDec('InterfaceDecHead(...))*/ +/*@ +\begin{markdown} +A type name is either class or interface name. Anonymous labels will be one of: + + - 'ClassDec('ClassDecHead(...)) + - 'InterfaceDec('InterfaceDecHead(...)) +\end{markdown} +*/ rule [processTypeNames]: processTypeNames( @@ -104,7 +109,7 @@ rule [processTypeNames-ElemDiscard]: processTypeNames([(Label:KLabel(_) => .KList),, _], _) when notBool( (Label ==KLabel 'ClassDec) orBool (Label ==KLabel 'InterfaceDec) ) -//We match PackId in just to be sure that the package was added to the map. +//@We match PackId in \verb|| just to be sure that the package was added to the map. rule [processTypeNames-Discard]: processTypeNames([.KList], PackId:PackageId) => .K ... ... PackId |-> _ ... diff --git a/src/sty/custom-commands.tex b/src/sty/custom-commands.tex index f2affcc4..dddf27d0 100644 --- a/src/sty/custom-commands.tex +++ b/src/sty/custom-commands.tex @@ -2,25 +2,50 @@ %\documentclass[a4paper, landscape]{article} %\usepackage[style=bubble, tight]{k} -% Reduces page borders, now we can put more characters in one line -%\usepackage{fullpage} - %Font set latin modern is not compatible with large angular brackets (package yhmath), so we cannot use it. %\usepackage{lmodern} +%For TOC fix +\usepackage{etoolbox} + +%%% Adding TOC to PDF bookmarks. +% Source: http://tex.stackexchange.com/questions/1820/contents-in-pdf-bookmarks +\makeatletter +\pretocmd{\tableofcontents}{% + \if@openright\cleardoublepage\else\clearpage\fi + \pdfbookmark[0]{\contentsname}{toc}% +}{}{}% +\makeatother + + +%%% MARKDOWN ENV + +\newcounter{MarkdownId} + %Required package fancyvrb already imported by k.sty \newenvironment{markdown}% - {\VerbatimEnvironment\begin{VerbatimOut}{tmp.markdown}}% + {\stepcounter{MarkdownId}% + \VerbatimEnvironment\begin{VerbatimOut}{tmp\theMarkdownId.markdown}% + }% {\end{VerbatimOut}% - \immediate\write18{pandoc .latex\string\\tmp.markdown -t latex -o .latex\string\\tmp.tex}% - \input{.latex\string\\tmp.tex}} + \immediate\write18{pandoc .latex\string\\tmp\theMarkdownId.markdown -t latex -o .latex\string\\tmp\theMarkdownId.tex}% + \input{.latex\string\\tmp\theMarkdownId.tex}% + } +%%% JAVA LSTLISTINGS SETUP \lstset{language=Java,captionpos=t,tabsize=3,frame=no,keywordstyle=\color{blue}, commentstyle=\color{gray},stringstyle=\color{red}, breaklines=true,showstringspaces=false,emph={label}, basicstyle=\ttfamily} +\makeatletter +% Call this in front of a \begin{itemize} to prevent page break before the list +% Doesn't work. +% http://tex.stackexchange.com/questions/2644/how-to-prevent-a-page-break-before-an-itemize-list +\newcommand{\nolisttopbreak}{\vspace{\topsep}\nobreak\@afterheading} +\makeatother + % #1 = sort, #2 = name \newcommand{\cellref}[2][]{% %\kall{#2}{\ifthenelse{\isempty{#1}}{}{$\sortName{#1}$}}%doesn't work @@ -31,12 +56,28 @@ } %Wraps a group of cells and properly aligns them. -\newcommand{\kwrap}[1]{% +\newcommand{\kwrap}[1]{{%Additional braces to confine the scope of setkeys to this macro \setkeys{k}{ruleHangindent=0pt,StartVspace=0ex,EndVspace=0ex}% \ksentence[]{}{}{#1}{}{}{}% -} +}} % Environment "kdefinition" have effect only in poster style, thus in math style may be safely deleted. -%Disable text justification, will eliminate overfulls inside text. -\raggedright + +%%% Rendering the paragraphs without overfull hbox-es. + +% v1. \raggedright, no parskip, vspace between paragraphs. +%Terrible solution. Both wanted and unwanted vertical spaces are increased. Empty pages appear. +%Document size increased by from 214 to 234 pages! +%\usepackage{parskip} %with \raggedright + +% v2. \raggedright + parindent. Zero bad boxes. +%\raggedright + +% Better than without. Just paragraph indentation. +%\setlength{\parindent}{2em} + +% v3. Best solution: \sloppy. Is enough for 0 bad boxes. +% Source: http://tex.stackexchange.com/questions/10377/texttt-overfull-hbox-problem +\setlength{\parindent}{2em} +\sloppy diff --git a/src/sty/k-java.tex b/src/sty/k-java.tex index e819593f..fddea688 100644 --- a/src/sty/k-java.tex +++ b/src/sty/k-java.tex @@ -10,25 +10,17 @@ \usepackage{fullpage} -\title{JAVA-EXEC} \begin{document} -\chapter{K-Java Common modules} - -\input{../.modules/core-sorts.tex} -\input{../.modules/core-functions.tex} -\input{../.modules/core-classes.tex} -\input{../.modules/primitive-types.tex} -\input{../.modules/subtyping.tex} -\input{../.modules/aux-strings.tex} +\tableofcontents \chapter{K-Java Dynamic semantics} \input{../.modules/configuration-exec.tex} -\input{../.modules/core-exec.tex} \input{../.modules/expressions.tex} \input{../.modules/expressions-classes.tex} \input{../.modules/statements.tex} +\input{../.modules/core-exec.tex} \input{../.modules/var-lookup.tex} \input{../.modules/arrays.tex} \input{../.modules/new-instance.tex} @@ -37,25 +29,33 @@ \chapter{K-Java Dynamic semantics} \input{../.modules/method-invoke-rest.tex} \input{../.modules/static-init.tex} \input{../.modules/api-core.tex} -\input{../.modules/api-threads-selection.tex} \input{../.modules/api-threads.tex} \input{../.modules/unfolding.tex} \input{../.modules/to-string.tex} \input{../.modules/syntax-conversions.tex} +\chapter{K-Java Common modules} + +\input{../.modules/core-sorts.tex} +\input{../.modules/core-functions.tex} +\input{../.modules/core-classes.tex} +\input{../.modules/primitive-types.tex} +\input{../.modules/subtyping.tex} +\input{../.modules/aux-strings.tex} + \chapter{K-Java Static semantics} \input{../.modules/configuration-prep.tex} -\input{../.modules/core-preprocessing.tex} \input{../.modules/process-type-names.tex} \input{../.modules/process-comp-units.tex} \input{../.modules/process-imports.tex} \input{../.modules/process-class-decs.tex} \input{../.modules/process-class-members.tex} +\input{../.modules/core-preprocessing.tex} \input{../.modules/elaboration-core.tex} \input{../.modules/elaboration-top-blocks.tex} -\input{../.modules/elaboration-types.tex} \input{../.modules/elaboration-statements.tex} +\input{../.modules/elaboration-types.tex} \input{../.modules/elaboration-expressions.tex} \input{../.modules/elaboration-vars.tex} \input{../.modules/elaboration-method-invoke.tex} @@ -68,6 +68,7 @@ \chapter{K-Java Static semantics} \input{../.modules/folding.tex} \chapter{K-Java Syntax} +\input{syntax-intro.tex} \input{../.modules/exp-syntax.tex} \input{../.modules/stmt-syntax.tex} @@ -80,7 +81,6 @@ \chapter{K-Java Syntax} \input{../.modules/lexical-syntax.tex} \input{../.modules/literal-syntax.tex} \input{../.modules/optional-syntax.tex} -\input{../.modules/shared-syntax.tex} \end{document} @@ -89,3 +89,4 @@ \chapter{K-Java Syntax} % \input{../.modules/java-prep.tex} % \input{../.modules/java-syntax.tex} % \input{../.modules/list-macro.tex} +% \input{../.modules/sort-predicate-hacks.tex} diff --git a/src/sty/syntax-intro.tex b/src/sty/syntax-intro.tex new file mode 100644 index 00000000..d6d33a3b --- /dev/null +++ b/src/sty/syntax-intro.tex @@ -0,0 +1,10 @@ +This chapter contains the entire semantics of Java 5. +This syntax was developed by Shijiao Yuwen from Formal Systems Laboratory of UIUC. +It is an adaptation of Java-Front~\cite{java-front}, the same syntax definition used to produce the external parser for K-Java. +Although the syntax is fairly complete, it might still contain errors. +This is because at the moment of writing it was not yet used to produce a parser for Java, consequently it was not yet used to parse programs. +Also, only a small part of K-Java is now defined over Java syntax. +The rest of the semantics is still in AST form. +Thus, most of this syntax was not put to use yet. +Yet, the part of this syntax that \textit{is} used is expressions, statements, and for the rest of the syntax, the attributes (strictness and \texttt{klabel}). +Syntax definition was added to K-Java at a later stage of development, when the semantics for Java 1.4 was already complete. diff --git a/tools/jenkins/k-java-latex-test.sh b/tools/jenkins/k-java-latex-test.sh new file mode 100644 index 00000000..bf66f352 --- /dev/null +++ b/tools/jenkins/k-java-latex-test.sh @@ -0,0 +1,17 @@ +#!/bin/sh + +export TOOLS_DIR=$WORKSPACE/tools +export PATH=/home/denis.bogdanas/k-framework-stable/bin:\ +$TOOLS_DIR:\ +$PATH + +echo "Using K Framework version:" +krun --version +echo "krun command:" +cat /home/denis.bogdanas/k-framework-stable/bin/krun + +rm -rf $WORKSPACE/* +cp -rf $WORKSPACE/../k-java-latex/* $WORKSPACE + +cd $WORKSPACE/src +aux-kjtest.sh -mode run -threads 12 -timeout 120 -encodeXML true -clean true ../tests diff --git a/tools/kjkompile.sh b/tools/kjkompile.sh index 2468827a..3e935d15 100755 --- a/tools/kjkompile.sh +++ b/tools/kjkompile.sh @@ -198,48 +198,28 @@ case "$OPTION" in ;; "--prep-latex") $KOMPILE_CMD -d prep --backend latex --doc-style "style=math,modulesAsSections" prep/java-prep.k - mv prep/java-prep.tex . - mv prep/k.sty . - ;; -"--prep-pdf") - $KOMPILE_CMD -d prep --backend pdf --doc-style "style=math,modulesAsSections" prep/java-prep.k - mv prep/java-prep.tex . + remove-kblock.sh prep/java-prep.tex > java-prep.tex + rm prep/java-prep.tex mv prep/k.sty . ;; "--exec-latex") $KOMPILE_CMD -d exec --backend latex --doc-style "style=math,modulesAsSections" exec/java-exec.k - mv exec/java-exec.tex . - mv exec/k.sty . - ;; -"--exec-pdf") - $KOMPILE_CMD -d exec --backend pdf --doc-style "style=math,modulesAsSections" exec/java-exec.k - mv exec/java-exec.tex . + remove-kblock.sh exec/java-exec.tex > java-exec.tex + rm exec/java-exec.tex mv exec/k.sty . ;; "--methods-latex") - $KOMPILE_CMD -d exec --backend latex --doc-style "style=math,modulesAsSections" exec/java-exec.k + kjkompile.sh $EXTRA_OPTS --exec-latex extract-module.sh -m METHOD-INVOKE -o method-invoke.tex java-exec.tex mv exec/java-exec.tex . mv exec/k.sty . ;; -"--methods-pdf") - kjkompile.sh $EXTRA_OPTS --methods-latex - mkdir -p .latex - pdflatex -synctex=-1 -max-print-line=120 -interaction=nonstopmode -shell-escape \ - --aux-directory=.latex method-invoke.tex - ;; "--new-latex") - $KOMPILE_CMD -d exec --backend latex --doc-style "style=math,modulesAsSections" exec/java-exec.k + kjkompile.sh $EXTRA_OPTS --exec-latex extract-module.sh -m NEW-INSTANCE -o new-instance.tex java-exec.tex mv exec/java-exec.tex . mv exec/k.sty . ;; -"--new-pdf") - kjkompile.sh $EXTRA_OPTS --new-latex - mkdir -p .latex - pdflatex -synctex=-1 -max-print-line=120 -interaction=nonstopmode -shell-escape \ - --aux-directory=.latex new-instance.tex - ;; "--modules-latex") echo "Preprocessing semantics:" # "&> file" redirects both stdin and stderr to the given file diff --git a/tools/remove-kblock.sh b/tools/remove-kblock.sh new file mode 100644 index 00000000..a19c1764 --- /dev/null +++ b/tools/remove-kblock.sh @@ -0,0 +1,13 @@ +#!/bin/sh + +#removes \begin{kblock}, \end{kblock} from the given file +if [ $# == 0 ]; then + echo "Usage: `basename $0` " + exit 1 +fi + +# http://www.cyberciti.biz/faq/howto-delete-word-using-sed-under-unix-linux-bsd-appleosx/ +# http://stackoverflow.com/questions/2369314/why-does-sed-require-3-backslashes-for-a-regular-backslash +# http://stackoverflow.com/questions/1251999/sed-how-can-i-replace-a-newline-n + +sed -e ':a;N;$!ba; s/\\begin{kblock}\[text\]\s*\n*\s*//g; s/\\end{kblock}\n//g' $1