search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Adding <s></s> to a configuration causes krun to throw an exception #2289

Open dfava opened 7 years ago

dfava commented 7 years ago

Adding <s></s> to a configuration causes krun to throw an exception. That happens, I believe, because <s> is defined in domains.k. So, a user defined <s> seems to override the one in domains.k. The problem is fixed if I rename <s> to something else (such as mysettag).

Files to reproduce:

$ cat test.k
require "./myset.k"
module TEST-SYNTAX
  imports MYSET-SYNTAX
  syntax K ::= init(MySet)
endmodule

module TEST
  import TEST-SYNTAX
  configuration <k> $PGM:K </k>
                <s> .MySet </s>
                //<mysettag> .MySet </mysettag>
  rule <k> init(M:MySet) => . </k>
       <s> .MySet => M </s>
       //<mysettag> .MySet => M </mysettag>
endmodule

$ cat myset.k
module MYSET-SYNTAX
  syntax MySet ::= MySet MySet [left, function, assoc, comm, unit(.MySet), idem, element(MySetItem)] // TODO: What is function?  TODO: We are missing hook(), what is that for?  TODO: We are missing klabel, what is that for?
  syntax MySet ::= ".MySet"    [function] // TODO: We are missing hook
  syntax MySet ::= "(" MySet ")" [bracket]
  syntax MySet ::= MySetItem(K)  [function] // TODO: We are missing hook
endmodule

module MYSET
  import MYSET-SYNTAX
  configuration <k> $PGM:K </k>

endmodule

$ cat test001.test
init( MySetItem(1) MySetItem(2) )

Here is the stack trace:

$ kompile --debug test.k
$ krun --debug test001.test
java.util.NoSuchElementException: key not found: #STUCK
    at scala.collection.MapLike.default$(MapLike.scala:232)
    at scala.collection.MapLike.default(MapLike.scala:231)
    at scala.collection.MapLike.apply$(MapLike.scala:141)
    at scala.collection.MapLike.apply(MapLike.scala:140)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:20)
    at org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
    at scala.collection.Iterator.foreach$(Iterator.scala:932)
    at scala.collection.Iterator.foreach(Iterator.scala:932)
    at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
    at scala.collection.IterableLike.foreach(IterableLike.scala:70)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
    at scala.collection.TraversableLike.map(TraversableLike.scala:227)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
    at org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
    at scala.collection.Iterator.foreach$(Iterator.scala:932)
    at scala.collection.Iterator.foreach(Iterator.scala:932)
    at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
    at scala.collection.IterableLike.foreach(IterableLike.scala:70)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
    at scala.collection.TraversableLike.map(TraversableLike.scala:227)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
    at org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
    at scala.collection.Iterator.foreach$(Iterator.scala:932)
    at scala.collection.Iterator.foreach(Iterator.scala:932)
    at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
    at scala.collection.IterableLike.foreach(IterableLike.scala:70)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
    at scala.collection.TraversableLike.map(TraversableLike.scala:227)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
    at org.kframework.unparser.KOREToTreeNodes.apply(KOREToTreeNodes.scala)
    at org.kframework.krun.KRun.unparseTerm(KRun.java:431)
    at org.kframework.krun.KRun.prettyPrint(KRun.java:313)
    at org.kframework.krun.KRun.filterAnonVarsAndPrint(KRun.java:163)
    at org.kframework.krun.KRun.printK(KRun.java:214)
    at org.kframework.krun.KRun.run(KRun.java:107)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
    at org.kframework.main.Main.runApplication(Main.java:414)
    at org.kframework.main.Main.runApplication(Main.java:265)
    at org.kframework.main.Main.main(Main.java:74)
java.util.NoSuchElementException: key not found: #STUCK
    at scala.collection.MapLike.default$(MapLike.scala:232)
    at scala.collection.MapLike.default(MapLike.scala:231)
    at scala.collection.MapLike.apply$(MapLike.scala:141)
    at scala.collection.MapLike.apply(MapLike.scala:140)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:20)
    at org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
    at scala.collection.Iterator.foreach$(Iterator.scala:932)
    at scala.collection.Iterator.foreach(Iterator.scala:932)
    at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
    at scala.collection.IterableLike.foreach(IterableLike.scala:70)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
    at scala.collection.TraversableLike.map(TraversableLike.scala:227)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
    at org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
    at scala.collection.Iterator.foreach$(Iterator.scala:932)
    at scala.collection.Iterator.foreach(Iterator.scala:932)
    at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
    at scala.collection.IterableLike.foreach(IterableLike.scala:70)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
    at scala.collection.TraversableLike.map(TraversableLike.scala:227)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
    at org.kframework.unparser.KOREToTreeNodes$.$anonfun$apply$3(KOREToTreeNodes.scala:21)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
    at scala.collection.Iterator.foreach$(Iterator.scala:932)
    at scala.collection.Iterator.foreach(Iterator.scala:932)
    at scala.collection.IterableLike.foreach$(IterableLike.scala:71)
    at scala.collection.IterableLike.foreach(IterableLike.scala:70)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
    at scala.collection.TraversableLike.map(TraversableLike.scala:227)
    at org.kframework.unparser.KOREToTreeNodes$.apply(KOREToTreeNodes.scala:21)
    at org.kframework.unparser.KOREToTreeNodes.apply(KOREToTreeNodes.scala)
    at org.kframework.krun.KRun.unparseTerm(KRun.java:431)
    at org.kframework.krun.KRun.prettyPrint(KRun.java:313)
    at org.kframework.krun.KRun.filterAnonVarsAndPrint(KRun.java:163)
    at org.kframework.krun.KRun.printK(KRun.java:214)
    at org.kframework.krun.KRun.run(KRun.java:107)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
    at org.kframework.main.Main.runApplication(Main.java:414)
    at org.kframework.main.Main.runApplication(Main.java:265)
    at org.kframework.main.Main.main(Main.java:74)
[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
cos commented 7 years ago

@dfava, yes <s> is reserved for the strategy cell. We should make the error message nicer when it is used for something else. Thanks!