NoSuchElementException

[kheradmand]

I have this k file (mop-compiler.k):

require "mop-syntax.k"

module MOP-COMPILER-SYNTAX
    imports MOP-SYNTAX
endmodule

module MOP-COMPILER
    imports MOP-COMPILER-SYNTAX
    configuration <T> <k> $PGM:MOP </k> </T>
endmodule

When I try to kompile mop-syntax.k I get:

[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues

Here is the stack trace:

java.util.NoSuchElementException: next on empty iterator
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:39)
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:37)
    at scala.collection.IterableLike$class.head(IterableLike.scala:107)
    at scala.collection.AbstractIterable.head(Iterable.scala:54)
    at org.kframework.compile.ConfigurationInfoFromModule.<init>(ConfigurationInfoFromModule.scala:63)
    at org.kframework.kompile.Kompile.addImplicitComputationCellTransformer(Kompile.java:210)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at org.kframework.kompile.Kompile.lambda$defaultSteps$10(Kompile.java:170)
    at org.kframework.backend.java.symbolic.JavaBackend.lambda$steps$101(JavaBackend.java:28)
    at org.kframework.kompile.Kompile.run(Kompile.java:141)
    at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)
java.util.NoSuchElementException: next on empty iterator
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:39)
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:37)
    at scala.collection.IterableLike$class.head(IterableLike.scala:107)
    at scala.collection.AbstractIterable.head(Iterable.scala:54)
    at org.kframework.compile.ConfigurationInfoFromModule.<init>(ConfigurationInfoFromModule.scala:63)
    at org.kframework.kompile.Kompile.addImplicitComputationCellTransformer(Kompile.java:210)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at org.kframework.kompile.Kompile.lambda$defaultSteps$10(Kompile.java:170)
    at org.kframework.backend.java.symbolic.JavaBackend.lambda$steps$101(JavaBackend.java:28)
    at org.kframework.kompile.Kompile.run(Kompile.java:141)
    at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)

I was wondering what is the problem.

[kheradmand]

@k-oncall I'd be really thankful if somebody could help me with this.

[cos]

@kheradmand, it would be helpful to have the mop-syntax.k that you're trying to compile.

[kheradmand]

Unfortunately I could not isolate the problem. Here is mop-syntax.k but it depends on many other files which you can find here:

require "domains.k"
require "../common/common-syntax.k"
require "advice-syntax.k"

module MOP-SYNTAX
    imports COMMON-SYNTAX
    imports ADVICE-SYNTAX

    //top level sort (aka CompilationUnit)
    syntax MOP ::= OptionalPackageDec ImportDecList SpecDec

    syntax SpecDec ::= SpecDecHead SpecBody
    syntax SpecDecHead ::= Id "(" Params ")"

    syntax SpecBody ::= "{"  DecBubbleList EventDecList  PropertyDecList "}"

    syntax EventDec ::= EventDecHead EventBody
    syntax EventDecHead ::= EventModifier "event" Id AdviceHeader
    syntax EventBody ::= BlockBubble
    syntax EventModifier ::= "creation" | None

syntax EventDecList          ::= List{EventDec, ""}

endmodule

[kheradmand]

@k-oncall any thoughts ?

[kheradmand]

So I managed to isolate the problem:

module TEST-SYNTAX

    syntax NoBracket ::= r"[^{}]+" [token]

endmodule

module TEST
    imports TEST-SYNTAX

    configuration <T> <k> $PGM:NoBracket </k> </T>
endmodule

when kompiled:

Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: syntax NoBracket ::= r"[^{}]+"
[Location(#token("5",Int),#token("26",Int),#token("5",Int),#token("42",Int))
Source(#token("./test.k",KString)) klabel(#token("",KString))
token(#token("",AttributeValue))]
    #token(NoBracket,"<T> <k> $PGM:NoBracket </k> </T>")
2: syntax Cell ::= "<" #CellName #CellProperties ">" K "</" #CellName ">"
[Location(#token("94",Int),#token("19",Int),#token("94",Int),#token("94",Int))
Source(#token("/Users/ali/FSL/kbuild/lib/java/../../include/builtin/kast.k",KString))
klabel(#token("#configCell",AttributeValue))
klabel(#token("#configCell",KString))]

#configCell(#token(#CellName,"T"),#cellPropertyListTerminator(),#configCell(#token(#CellName,"k"),#cellPropertyListTerminator(),#SemanticCastToNoBracket(#token(KConfigVar,"$PGM")),#token(#CellName,"k")),#token(#CellName,"T"))
    Source(./test.k)
    Location(13,19,13,51)

and the stack trace:

java.util.NoSuchElementException: next on empty iterator
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:39)
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:37)
    at scala.collection.IterableLike$class.head(IterableLike.scala:107)
    at scala.collection.AbstractIterable.head(Iterable.scala:54)
    at org.kframework.compile.ConfigurationInfoFromModule.<init>(ConfigurationInfoFromModule.scala:63)
    at org.kframework.kompile.Kompile.addImplicitComputationCellTransformer(Kompile.java:212)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at org.kframework.kompile.Kompile.lambda$defaultSteps$10(Kompile.java:172)
    at org.kframework.backend.java.symbolic.JavaBackend.lambda$null$5ca3f9c9$1(JavaBackend.java:76)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at org.kframework.backend.java.symbolic.JavaBackend.lambda$steps$119(JavaBackend.java:87)
    at org.kframework.kompile.Kompile.run(Kompile.java:143)
    at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)
java.util.NoSuchElementException: next on empty iterator
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:39)
    at scala.collection.Iterator$$anon$2.next(Iterator.scala:37)
    at scala.collection.IterableLike$class.head(IterableLike.scala:107)
    at scala.collection.AbstractIterable.head(Iterable.scala:54)
    at org.kframework.compile.ConfigurationInfoFromModule.<init>(ConfigurationInfoFromModule.scala:63)
    at org.kframework.kompile.Kompile.addImplicitComputationCellTransformer(Kompile.java:212)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at org.kframework.kompile.Kompile.lambda$defaultSteps$10(Kompile.java:172)
    at org.kframework.backend.java.symbolic.JavaBackend.lambda$null$5ca3f9c9$1(JavaBackend.java:76)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
    at org.kframework.backend.java.symbolic.JavaBackend.lambda$steps$119(JavaBackend.java:87)
    at org.kframework.kompile.Kompile.run(Kompile.java:143)
    at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)

[cos]

could you try this on https://github.com/kframework/k/pull/1871? Just making sure I retained the bug after refactoring :-D

[kheradmand]

@cos could you send me a compiled version of that pull request?

[cos]

Kind of hard to sent it as the k-distribution is 1.5Gb. You can either pull cos:hotfix/compile-refactoring from my k repo and compile it yourself, or I'll try to replicate your experiment tomorrow.

[kheradmand]

I have problems compiling K on my personal computer could you test it yourself?

module TEST-SYNTAX

    syntax NoBracket ::= r"[^{}]+" [token]

endmodule

module TEST
    imports TEST-SYNTAX

    configuration <T> <k> $PGM:NoBracket </k> </T>
endmodule

[kheradmand]

@cos @k-oncall And the problem is not just limited to configuration. There is the same problem with rules. In general, things like r"[^{}]+" or r"[^()]+" are causing ambiguities with K's internal syntax. I don't know how to tell K to disambiguate such thing (prefer K's syntax over alternatives) (I can not do this using prefer or avoid because I have used this stuff to disambiguate my own syntax)

[dwightguth]

In general it's going to be pretty difficult for you to disambiguate rules if you have such a general production in your syntax. I think likely the best thing for you to do would be to define this as part of the syntax of your language but not import that syntax into the rest of the definition, like so:

module TEST-COMMON
  syntax NoBracket
  // other language syntax here
endmodule

module TEST-SYNTAX
    imports TEST-COMMON
    syntax NoBracket ::= r"[^{}]+" [token]

endmodule

module TEST
    imports TEST-COMMON

    configuration <T> <k> $PGM:NoBracket </k> </T>
endmodule

[dwightguth]

If you go this route, you will have to use abstract syntax for NoBracket tokens, like so:

#token("123", "NoBracket")

But this is probably the most reasonable compromise you are going to get when you have a token that can represent such a wide range of characters.

[dwightguth]

That said, we will look into this stack trace because at the very least that should definitely not be happening.

[kheradmand]

I did so (on my project not the sample I provided) but now unfortunately krun hangs (does not produce result after 15 minutes on input that it used to produce result for in less that 5 seconds)

[dwightguth]

@radumereuta could this be because of the start symbol thing?

[radumereuta]

It is possible. I've tested Test.rvm and it is ambiguous if I don't specify the sort to kast. @kheradmand can you tell me if you get the expected result if you call krun with the parser option something like: kast -s RVM path/to/spec.rvm.

P.S. I didn't find any instructions on how to run a module. All I found was how to compile the syntax module.

[kheradmand]

Could you please test MOP instead of RVM? I'm working on MOP right now and it is not ambiguous if you don't specify sort to kast.

kompile —syntax-module MOP-SYNTAX path/to/src/mop/mop-syntax.k
kast ./path/to/test/mop/test.mop

The master branch only contains the syntax modules.

For configuration and rules please check out the "compiler" branch and

kompile path/to/src/mop/mop-compiler.k

Which does not kompile right now.

This is mop-compiler.k:

require "mop-syntax.k"
require "domains.k"

module MOP-COMPILER-SYNTAX
    imports MOP-SYNTAX
    syntax NoBracket ::= r"[^<{}][^{}]*" [token, klabel('NoBracket)]
    syntax ParamsBubble ::= r"\\([^\\)]*\\)" [token, avoid, klabel('ParamsBubble)]
    syntax VarInitBubble ::=  r"[^<;][^;]*" [token, avoid, klabel('VarInitBubble)]
    syntax NoParentheses ::= r"[^()<][^()]*" [token, klabel('NoParentheses)]
endmodule

module MOP-COMPILER
    imports MOP-SYNTAX
    imports DOMAINS
    configuration <T> <k> $PGM:MOP  </k> </T>

    rule <k> (Pac:OptionalPackageDec Imp:ImportDecList Spec:SpecDec) => (.)</k>
endmodule

[kheradmand]

@k-oncall @radumereuta @dwightguth Any news on this? I am really stuck with it.

[kheradmand]

why does this fail to kompile :

require "domains.k"

module MOP-COMPILER-SYNTAX
    imports DOMAINS-SYNTAX
    syntax ImportDec ::= "import" Id
endmodule

module MOP-COMPILER
    imports MOP-COMPILER-SYNTAX
    imports DOMAINS

    configuration <T> <k> $PGM:ImportDec  </k> </T>

    rule <k> (Imp:ImportDec) => Imp</k>
endmodule

[dwightguth]

Your language syntax does not include brackets. You can use backticks if you want (`Imp:ImportDec => Imp), you can declare brackets for you sort (syntax ImportDec ::= "(" ImportDec ")" [bracket]), or you can declare universal parentheses as brackets if you are sure it will not conflict with the syntax of your language (syntax KBott ::= "(" K ")" [bracket]`)

[kheradmand]

I don't really know what's going on

require "domains.k"

module MOP-COMPILER-SYNTAX
    imports DOMAINS-SYNTAX
    syntax ImportDec ::= "import" Id
endmodule

module MOP-COMPILER
    imports MOP-COMPILER-SYNTAX
    imports DOMAINS

    configuration <T> <k> $PGM:ImportDec  </k> </T>

    rule <k> `Imp:ImportDec` => Imp </k>
endmodule

[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: syntax Id ::= r"(?<![A-Za-z0-9\\_])[A-Za-z\\_][A-Za-z0-9\\_]*"
[Location(#token("481",Int),#token("17",Int),#token("481",Int),#token("100",Int))
Source(#token("/home/ali/FSL/kbuild3/lib/java/../../include/builtin/domains.k",KString))
autoReject(#token("",AttributeValue)) klabel(#token("",KString))
notInRules(#token("",AttributeValue)) token(#token("",AttributeValue))]
    #token(Id,"Imp")
2: syntax ImportDec ::= ImportDec ":ImportDec"
[klabel(#token("#SemanticCastToImportDec",KString))
sort(#token("ImportDec",KString))]
    #SemanticCastToImportDec(#token(#KVariable,"Imp"))
    Source(/home/ali/FSL/rvmKparser/src/mop/././mop-compiler.k)
    Location(15,33,15,36)

[dwightguth]

DOMAINS-SYNTAX contains the concrete syntax of identifiers which is intended to be inculded in program syntax but not rule syntax (because it conflicts with the syntax of variables). However, you are importing MOP-COMPILER-SYNTAX into MOP-COMPILER. I suggest you take a look at some of the examples in the tutorial that have been converted to K 4.0 to get a better idea of how they use a <DEFINITION>-COMMON module to bridge the gap here.

[kheradmand]

@dwightguth Thanks a lot. That problem I guess is now solved. Now I kompile this without any problem:

module MOP-COMPILER
    imports MOP-CCOMMON
    imports DOMAINS
    configuration <T> <k> $PGM:MOP  </k> </T>

    rule <k> `Pac:OptionalPackageDec Imp:ImportDecList Spec:SpecDec` => Spec </k> [structural]
endmodule

But when I krun I get the following output:

<T> <k> _279 </k> </T>

What's that?

[grosu]

What input program did you pass it? _nnn are anonymous variables.

[kheradmand]

@grosu A very simple MOP spec. To be more precise this:

package mop;

import java.io.*;
import java.lang.*;
import com.runtimeverification.rvmonitor.java.rt.RVMLogging;
import com.runtimeverification.rvmonitor.java.rt.RVMLogging.Level;

String_UseStringBuilder() {
    event constructor_create after() returning(String b):
        call(String.new(StringBuilder)) {
               RVMLogging.out.println(Level.CRITICAL, __DEFAULT_MESSAGE );              
        }
}

this is the output of kast for it:

`MOP`(`PackageDec`(`PackageName`(`IdList`(#token("mop","Id"),`.List{"'IdList"}`(.KList)))),`ImportDecList`(`TypeImportOnDemandDec`(`PackageName`(`IdList`(#token("java","Id"),`IdList`(#token("io","Id"),`.List{"'IdList"}`(.KList))))),`ImportDecList`(`TypeImportOnDemandDec`(`PackageName`(`IdList`(#token("java","Id"),`IdList`(#token("lang","Id"),`.List{"'IdList"}`(.KList))))),`ImportDecList`(`TypeImportDec`(`TypeName`(`PackageOrTypeName`(`PackageOrTypeName`(`PackageOrTypeName`(`PackageOrTypeName`(`PackageOrTypeName`(#token("com","Id")),#token("runtimeverification","Id")),#token("rvmonitor","Id")),#token("java","Id")),#token("rt","Id")),#token("RVMLogging","Id"))),`ImportDecList`(`TypeImportDec`(`TypeName`(`PackageOrTypeName`(`PackageOrTypeName`(`PackageOrTypeName`(`PackageOrTypeName`(`PackageOrTypeName`(`PackageOrTypeName`(#token("com","Id")),#token("runtimeverification","Id")),#token("rvmonitor","Id")),#token("java","Id")),#token("rt","Id")),#token("RVMLogging","Id")),#token("Level","Id"))),`.List{"'ImportDecList"}`(.KList))))),`__`(`_(_)`(#token("String_UseStringBuilder","Id"),`.List{"'FormalParamList"}`(.KList)),`{___}`(#token("","DecBubbleList"),`EventDecList`(`__`(`_event__`(`None`(.KList),#token("constructor_create","Id"),`___:_`(`None`(.KList),`after(_)_`(`.List{"'Formals"}`(.KList),`returning_`(`(_)`(`__`(`TypeName`(#token("String","Id")),#token("b","Id"))))),`None`(.KList),`__`(`call(_)`(`__new(_)_`(`.List{"'ModifierList"}`(.KList),`_.`(`___`(#token("String","IdPattern"),`None`(.KList),`.List{"'__"}`(.KList))),`TypePatternDoubleDotList`(`___`(#token("StringBuilder","IdPattern"),`None`(.KList),`.List{"'__"}`(.KList)),`.List{"'TypePatternDoubleDotList"}`(.KList)),`None`(.KList))),`None`(.KList)))),#token("{\n               RVMLogging.out.println(Level.CRITICAL, __DEFAULT_MESSAGE);\n        }","BlockBubble")),`.List{"'EventDecList"}`(.KList)),`.List{"'PropertyDecList"}`(.KList))))

and this is the output of krun if I don't specify any rules:

<T> initKCell ( $IO |-> "on" $PGM |-> ` package mop . .IdList ; ` import java . ` io . .IdList ` . * ;  ` import java . ` lang . .IdList ` . * ;  ` import ` ` ` ` com . runtimeverification ` . rvmonitor ` . java ` . rt ` . RVMLogging ;  ` import ` ` ` ` ` com . runtimeverification ` . rvmonitor ` . java ` . rt ` . RVMLogging ` . Level ;  .ImportDecList ` ` ` ` ` String_UseStringBuilder ( .Params ) {  ` `  event constructor_create `  ` after ( .Formals ) returning ( String b ) `  : ` call ( .ModifierList ` ` String  .Dims ` . ` new ( ` StringBuilder  .Dims ` , .TypePatternDoubleDotList )  )  ` ` ` {
               RVMLogging.out.println(Level.CRITICAL, __DEFAULT_MESSAGE);
        } `  .EventDecList .PropertyDecList } ` ` $STDIN |-> "" ) </T>

[daejunpark]

initKCell should have been resolved into the term associated with $PGM. I suspect that the term is not considered (parsed) as of the sort MOP. To narrow down the problem, @kheradmand could you try with a simpler program? e.g., a program including only the first line package mop;, or the imports, and so on.

[kheradmand]

@daejunpark tested with

package mop;

test () {

}

kast:

`MOP`(`PackageDec`(`PackageName`(`IdList`(#token("mop","Id"),`.List{"'IdList"}`(.KList)))),`.List{"'ImportDecList"}`(.KList),`__`(`_(_)`(#token("test","Id"),`.List{"'FormalParamList"}`(.KList)),`{___}`(#token("","DecBubbleList"),`.List{"'EventDecList"}`(.KList),`.List{"'PropertyDecList"}`(.KList))))

krun got

[Error] Internal: Uncaught exception thrown of type NullPointerException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues

And the stack trace:

java.lang.NullPointerException
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:170)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:95)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:78)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:132)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
    at org.kframework.krun.KRun.run(KRun.java:76)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:91)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)
java.lang.NullPointerException
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:170)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:95)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:78)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:132)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
    at org.kframework.krun.KRun.run(KRun.java:76)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:91)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)

[msaxena2]

@kheradmand I couldn't reproduce the NPE, but I did try running the program above with the files at https://github.com/Formal-Systems-Laboratory/rvm-parser under branch compiler. It seems like this is an issue with sorts. KRun can't figure out that sort OptionalPackageDec is a subsort of sort PackageDec. @cos @radumereuta any Ideas?

[msaxena2]

@kheradmand I believe that this issue doesn't have to do with K. This may have to do with the manner in which you organize and import modules. Here's why I think K doesn't know the subsorts: In mop-compiler.k, module MOP-COMPILER you include MOP-COMMON. in MOP-COMMON you include COMMON-CCOMMON, In COMMON-CCOMMON, you include PACKAGE-COMMON where you have syntax OptionalPackageDec, but no subsorting between OptionalPackageDec and PackageDec. Your rule thus parses, but your match fails.

I suggest, as @dwightguth had earlier, that you take a look at the examples that have already been translated to K, to see how the module structure works. You may also want to consider refactoring some of the code. If there are any issues with that process, let me know.

[dwightguth]

before we rule out the possibility of a NPE which would definitely be a bug in K, I'd like to confirm the exact krun command used and the commit hashes for the k and mop repos.

[msaxena2]

@kheradmand might be able to help us provide the command and the hashes on which K crashed.

[kheradmand]

could not reproduce the NPE don't know why! I am testing this commit of my project. I use two builds of K: first is from d87bc11. This one gives me

<T> <k> _279 </k> </T>

The second build is from 2dfd395. This one gives me

<T> <k> package mop . .IdList ; .ImportDecList ` test ( .Params ) {  .EventDecList .PropertyDecList } ` </k> </T>

I run the following commands on each:

kompile src/mop/mop-kompiler.k
krun test.mop

where test.mop is:

package mop;

test () {

}

[kheradmand]

@msaxena2 could you please point me to some specific examples for module structures? I don't know much about what is going on I just do this stuff by trial and error.

[kheradmand]

ah OK if I comment out the only rule in src/mop/mop-kompiler.k:

//rule <k> `Pac:OptionalPackageDec Imp:ImportDecList Spec:SpecDec` => Spec </k> [structural]

with d87bc11 I get

<T> initKCell ( $IO |-> "on" $PGM |-> ` package mop . .IdList ; .ImportDecList ` test ( .Params ) {  .EventDecList .PropertyDecList } ` ` $STDIN |-> "" ) </T>

with 2dfd395 and f773299 I get NPE.

So to reproduce the problem, get my project in compiler branch, comment out the rule, kompile, and krun with input:

package mop;

test () {

}

[msaxena2]

Thanks @kheradmand .This sounds like a bug in K, that'll need looking into. Although, the behavior with one rule seems normal, and this issue should not block you. Try moving stuff you need for rules from the -syntax modules to the -common module (since your main module includes stuff from the -common module). On Dec 18, 2015 12:00 AM, "Ali Kheradmand" notifications@github.com wrote:

ah OK if I comment out the only rule in src/mop/mop-kompiler.k:

//rule Pac:OptionalPackageDec Imp:ImportDecList Spec:SpecDec => Spec [structural]

with d87bc11 https://github.com/kframework/k/commit/d87bc11ece2d20ed2daf7bc3cd9f743f6e9b2319 I get

initKCell ( $IO |-> "on" $PGM |-> `package mop . .IdList ; .ImportDecList` test ( .Params ) { .EventDecList .PropertyDecList } ` ` $STDIN |-> "" )

with 2dfd395 https://github.com/kframework/k/commit/2dfd39501d81f0169d0d8dfb8903f7b856469b65 and f773299 https://github.com/kframework/k/commit/f77329976448141a33096bdcd73dbc4194036b11 I get NPE.

So to reproduce the problem, get my project in compiler branch, comment out the rule, kompile, and krun with input:

package mop;

test () {

}

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1863#issuecomment-165680807.

[kheradmand]

I move stuff from syntax to ccommon and I get ambiguities with K's internal syntax. I keep them and I have this problem. It's really annoying. I wish there was a better way to resolve the ambiguities.

[kheradmand]

@msaxena2 I was wondering how did you figure out that "KRun can't figure out that sort OptionalPackageDec is a subsort of sort PackageDec."?

[msaxena2]

I ran intellij's debugger on K running your program, set a breakpoint at the match to see why it failed. On Dec 21, 2015 10:36 AM, "Ali Kheradmand" notifications@github.com wrote:

@msaxena2 https://github.com/msaxena2 I was wondering how did you figure out that "KRun can't figure out that sort OptionalPackageDec is a subsort of sort PackageDec."?

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1863#issuecomment-166352887.

[kheradmand]

@msaxena2 Is there any mechanism to figure out this stuff as a user?

[msaxena2]

The debugger can help you figure out whether a match succeeded or not, but finding out why it didn't succeed would be slightly tricky. I'm not sure but K's --audit flag may help. It's something that we should incorporate into audit (and we also plan to have auditing as part of the debugger as well). On Dec 21, 2015 10:44 AM, "Ali Kheradmand" notifications@github.com wrote:

@msaxena2 https://github.com/msaxena2 Is there any mechanism to figure out this stuff as a user?

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1863#issuecomment-166355497.

[kheradmand]

@msaxena2 Don't know how to work with audit. is there any documentation? I did something else, I moved a minimal set of productions to common.

But still does not work. Can you checkout the branch "compiler-new" in my project and test it with

package mop;

test () {

}

[msaxena2]

@kheradmand Running krun with the -X flag will output help for all the experimental features. You will be able to find instructions about running an audit there. You'll have to use the --audit-file flag to specify the k file you'd like to audit, the --audit-step flag to specify a step number, and the --audit-line flag to specify the rule you'd like to be considered within the k file.

[kheradmand]

@msaxena2 What does audit do exactly? It is going to help with my situation? I also got k source code and I can now run it in debug mode. Can you help me on where to put breakpoints and what to look for to know what's going on inside? Also if you can test "compiler-new" branch yourself that would be probably faster.

[kheradmand]

@msaxena2 @dwightguth So right now as I said only a minimal set of productions are excluded from the semantics module.

I am running K in debug mode and this is the value of program before line 74 in KRun.java

initTCell(_Map_(_Map_(_Map_(.Map(),_|->_(#token("$STDIN",KConfigVar),#token("\"\"",String))),_|->_(#token("$IO",KConfigVar),#token("\"on\"",String))),_|->_(#token("$PGM",KConfigVar),MOP(PackageDec(PackageName(IdList(#token("mop",Id),.List{"'IdList"}()))),.List{"'ImportDecList"}(),__(_(_)(#token("test",Id),.List{"'FormalParamList"}()),{___}(#token("",DecBubbleList),.List{"'EventDecList"}(),.List{"'PropertyDecList"}()))))))

note the PackageDec(PackageName(IdList(#token("mop",Id),.List{"'IdList"}()))) part

The relevant part of syntax is :

syntax MOP ::= OptionalPackageDec ImportDecList SpecDec [prefer, klabel('MOP)]
syntax OptionalPackageDec ::= PackageDec | None
syntax PackageDec ::=  "package" PackageName ";"     [klabel('PackageDec)]
syntax PackageName ::= IdList                           [klabel('PackageName)]
syntax IdList                    ::= List{Id,"."}   [klabel('IdList)]

I have tested these two rules:

rule <k> `X:OptionalPackageDec => .K` ...</k>

and

rule <k> `X:PackageDec => .K` ...</k>

None of them works.

[kheradmand]

Although this works:

require "domains.k"

module TEST-COMMON
    imports DOMAINS-COMMON
    syntax MOP ::= OptionalPackageDec [prefer, klabel('MOP)]
    syntax OptionalPackageDec ::= PackageDec | None
    syntax PackageDec ::=  "package" PackageName ";"     [klabel('PackageDec)]
    syntax PackageName ::= IdList                           [klabel('PackageName)]
    syntax IdList                    ::= List{Id,"."}   [klabel('IdList)]
    syntax None ::= ""
endmodule

module TEST-SYNTAX
    imports TEST-COMMON
    imports DOMAINS-SYNTAX

endmodule

module TEST
    imports TEST-COMMON
    imports DOMAINS
    configuration <T> <k> $PGM:MOP  </k> </T>

    rule <k> `X:OptionalPackageDec => .K` </k>
endmodule

[kheradmand]

the match tries to match subject

<T>(<k>(MOP(PackageDec(PackageName(IdList(Id(#"mop"),, .List{"'IdList"}(.KList)))),, .List{"'ImportDecList"}(.KList),, __(_(_)(Id(#"test"),, .List{"'FormalParamList"}(.KList)),, {___}(DecBubbleList(#""),, .List{"'EventDecList"}(.KList),, .List{"'PropertyDecList"}(.KList)))))) /\ Bool(#"true")

with pattern

<T>(<k>(#KRewrite(#KSequence( OR (TypeName(HOLE:PackageOrTypeName,, K1:Id),org.kframework.utils.OneWordBitSet@518ddd3b) OR (PackageOrTypeName(HOLE:PackageOrTypeName,, K1:Id),org.kframework.utils.OneWordBitSet@939ff41) OR (X:OptionalPackageDec,org.kframework.utils.OneWordBitSet@5cbd94b2) OR (HOLE:PackageOrTypeName,org.kframework.utils.OneWordBitSet@506aabf6),,  OR (#KSequence( OR (#freezer1(K1:Id),org.kframework.utils.OneWordBitSet@6e0e5dec) OR (#freezer0(K1:Id),org.kframework.utils.OneWordBitSet@48a663e9),, DotVar1:K),org.kframework.utils.OneWordBitSet@777d0bc3) OR (DotVar1:K,org.kframework.utils.OneWordBitSet@7c1447b5) OR (DotVar1:K,org.kframework.utils.OneWordBitSet@49e4c2d5)),, org.kframework.backend.java.kil.InnerRHSRewrite@1d06af1e)))

and it can't.

[msaxena2]

@kheradmand I'll take a look into what's going on with this. In the meanwhile, if you'd like to set breakpoints within K, look at the file org/kframework/backend/java/symbolic/FastRuleMatcher.java. Specifically the mainMatch function. Within the function is a call to a private match function. The match function is supposed to return the substitution of the match operation. If the substitution returned is correct, but the rewrite still fails, then the problem probably is a failed side condition.

[kheradmand]

@msaxena2 I already did that. It seems that nothing is matching. I traced the execution until

   private void checkVarLabelPatterns(Term subject, BitSet ruleMask, scala.collection.immutable.List<Integer> path, RuleAutomatonDisjunction automatonDisjunction, BitSet returnSet) {
        List<Pair<KItem, BitSet>> varLabelPatterns = automatonDisjunction.getKItemPatternByArity(((KItem) subject).klist().size());
...

with

subject=MOP(PackageDec(PackageNameSingle(Id(#"mop"))),, .List{"'ImportDecList"}(.KList),, __(_(_)(Id(#"test"),, .List{"'FormalParamList"}(.KList)),, {___}(DecBubbleList(#""),, .List{"'EventDecList"}(.KList),, .List{"'PropertyDecList"}(.KList))))

and

automatonDisjunction= OR (PackageNameMulti(HOLE:PackageName,, K1:Id),org.kframework.utils.OneWordBitSet@65bad087) OR (X:OptionalPackageDec,org.kframework.utils.OneWordBitSet@6d0be7ab) OR (HOLE:PackageName,org.kframework.utils.OneWordBitSet@3c9c6245)

This :

((KItem) subject).klist().size()

returns 3 and

automatonDisjunction.getKItemPatternByArity(3)

returns null because varKItemDisjunctionsMap is empty

[kheradmand]

@msaxena2

            // try to match the subject as-if it is a singleton kseq, i.e. subject ~> .K
            if (!(subject instanceof KItem && ((KItem) subject).kLabel() == kSeqLabel)) {
                matchInside(subject, ruleMask, path, returnSet, automatonDisjunction.getKItemPatternForKLabel(kSeqLabel));
            }

            // TODO: hack for threads to behave like the kseq above; remove once AC works
            if (!(subject instanceof KItem && ((KItem) subject).kLabel() == threadCellBagLabel) && threadCellBagLabel.ordinal() < automatonDisjunction.getKLabelMaxOrdinal()) {
                matchInside(subject, ruleMask, path, returnSet, automatonDisjunction.getKItemPatternForKLabel(threadCellBagLabel));
            }

            if (subject instanceof KItem) {
                // main match of KItem
                matchInside(subject, ruleMask, path, returnSet, automatonDisjunction.getKItemPatternForKLabel((KLabelConstant) ((KItem) subject).kLabel()));
                checkVarLabelPatterns(subject, ruleMask, path, automatonDisjunction, returnSet);

it goes into the first and third "if", but nothing matches

[msaxena2]

@kheradmand is compiler-new still the most recent relevant branch? (The one that the errors are happening on)