search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
452 stars 149 forks source link

[K-Bug] NullPointerException in kompile #4141

Open virgil-serbanuta opened 7 months ago

virgil-serbanuta commented 7 months ago

What component is the issue in?

Front-End

Which command

What K Version?

K version: v6.3.27-0-g2f6f074988-dirty Build date: Ma mar 19 23:40:38 EET 2024

Operating System

Linux

K Definitions (If Possible)

No response

Steps to Reproduce

I didn't find a way to produce this reliably. As far as I can tell, all the following need to happen at the same time:

The error message looks something like this:

[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/runtimeverification/k/issues
(NullPointerException: Cannot invoke "scala.Tuple2._1()" because the return
value of "java.util.Map.get(Object)" is null)

Expected Results

A normal error message

Baltoli commented 7 months ago

@virgil-serbanuta Can you pass the --debug flag through your build system to kompile? That will get us a stack trace for the crash, which would be a helpful first step to reproducing / understanding this issue.

It would also be good to know exactly which semantics, at which commit, and what command you're running to build it.

Baltoli commented 7 months ago

@gtrepta will try to run these reproduction steps to see if he can reproduce it

virgil-serbanuta commented 7 months ago

@Baltoli I'm using kbuild, I didn't figure out yet how to make it pass --debug to kompile. I tried running kompile separately, but, for our project, it's hard and I didn't manage to make it crash yet.

gtrepta commented 7 months ago

I wasn't able to reproduce by playing around with the steps listed.

Looking at the error message, it seems a lookup on a Map that has Scala Tuple2s as values is failing somewhere. The only places I see that datatype are in Scanner and the GeneralTransformer that the frontend parsers use. This is an area of the frontend that does a lot of caching, so it's possible there's a bug there somewhere.

Of course, the exception could be getting thrown somewhere entirely unrelated. Without a stack trace, it's hard to learn much more about the problem.

virgil-serbanuta commented 7 months ago

It stopped happening for me, also. I'm currently using --debug for all my builds, if I manage to reproduce it again I'll post a stack trace.

Baltoli commented 7 months ago

Thanks @virgil-serbanuta; will mark this as blocked but if it resurfaces we can take another look.

virgil-serbanuta commented 7 months ago

FWIW, I didn't use --debug once and I got the same crash. I'm not sure if it was just a coincidence, or --debug actually makes things work for some reason.

Baltoli commented 7 months ago

Strange! I see looking back at the original issue that we don't have any context on the actual semantics you're building here; can you perhaps share the precise commands / related context that produces the issue for you?

virgil-serbanuta commented 7 months ago

IIRC, this was a post on Slack, and Bruce Collie requested "just so it gets prioritised properly can you write that message verbatim into a K issue", which I did, but that meant it didn't include many details. See the messages around this one:

https://runtimeverification.slack.com/archives/C7E701MFG/p1711567180101229

Full instructions (may not always work):

  1. Clone https://github.com/runtimeverification/mx-backend
  2. Use the int64-encoding branch.
  3. Init submodules. To save time, do not do that recursively, instead init them once in the root of the repository and a second time in kmxwasm/k-src/mx-semantics.
  4. cd kmxwasm/k-src
  5. Edit kmxwasm/k-src/mx-lemmas.md and remove (I don't know if commenting out works), say, these staements: requires "lemmas/int-encoding-lemmas.md", imports INT-ENCODING-BASIC and imports private INT-ENCODING-LEMMAS.
  6. kbuild kompile haskell (this should work)
  7. Introduce an error in kmxwasm/k-src/lemmas/int-encoding-lemmas.md, e.g. remove the imports CEILS-SYNTAX statement from the INT-ENCODING-LEMMAS module.
  8. Revert the changes to kmxwasm/k-src/mx-lemmas.md
  9. kbuild kompile haskell (this may produce an exception)

If it does not work, you may try the same process with other private imports like BYTES-NORMALIZATION-LEMMAS. You can also try introducing errors without removing the imports first.

FWIW, I didn't manage to reproduce this today.

Baltoli commented 7 months ago

That's perfect, thanks Virgil - should let us see if we can get this reproduced locally in someone else's environment

virgil-serbanuta commented 2 months ago

FWIW, I think I managed to catch a this crash when using the --debug flag. I'm working on a different semantics now.

java.lang.NullPointerException
        at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
        at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:77)
        at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
        at java.base/java.lang.reflect.Constructor.newInstanceWithCaller(Constructor.java:500)
        at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:481)
        at java.base/java.util.concurrent.ForkJoinTask.getThrowableException(ForkJoinTask.java:564)
        at java.base/java.util.concurrent.ForkJoinTask.reportException(ForkJoinTask.java:591)
        at java.base/java.util.concurrent.ForkJoinTask.invoke(ForkJoinTask.java:689)
        at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateParallel(ReduceOps.java:927)
        at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:233)
        at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
        at org.kframework.kompile.DefinitionParsing.resolveNonConfigBubbles(DefinitionParsing.java:633)
        at org.kframework.kompile.DefinitionParsing.lambda$resolveNonConfigBubbles$31(DefinitionParsing.java:588)
        at scala.collection.parallel.AugmentedIterableIterator.map2combiner(RemainsIterator.scala:107)
        at scala.collection.parallel.AugmentedIterableIterator.map2combiner$(RemainsIterator.scala:104)
        at scala.collection.parallel.immutable.ParHashSet$ParHashSetIterator.map2combiner(ParHashSet.scala:77)
        at scala.collection.parallel.ParIterableLike$Map.leaf(ParIterableLike.scala:1020)
        at scala.collection.parallel.Task.$anonfun$tryLeaf$1(Tasks.scala:52)
        at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
        at scala.util.control.Breaks$$anon$1.catchBreak(Breaks.scala:97)
        at scala.collection.parallel.Task.tryLeaf(Tasks.scala:55)
        at scala.collection.parallel.Task.tryLeaf$(Tasks.scala:49)
        at scala.collection.parallel.ParIterableLike$Map.tryLeaf(ParIterableLike.scala:1017)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.internal(Tasks.scala:159)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.internal$(Tasks.scala:156)
        at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$AWSFJTWrappedTask.internal(Tasks.scala:304)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.compute(Tasks.scala:149)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.compute$(Tasks.scala:148)
        at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$AWSFJTWrappedTask.compute(Tasks.scala:304)
        at java.base/java.util.concurrent.RecursiveAction.exec(RecursiveAction.java:194)
        at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:373)
        at java.base/java.util.concurrent.ForkJoinPool.helpJoin(ForkJoinPool.java:1883)
        at java.base/java.util.concurrent.ForkJoinTask.awaitDone(ForkJoinTask.java:440)
        at java.base/java.util.concurrent.ForkJoinTask.join(ForkJoinTask.java:670)
        at scala.collection.parallel.ForkJoinTasks$FJTWrappedTask.sync(Tasks.scala:243)
        at scala.collection.parallel.ForkJoinTasks$FJTWrappedTask.sync$(Tasks.scala:243)
        at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$AWSFJTWrappedTask.sync(Tasks.scala:304)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.internal(Tasks.scala:173)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.internal$(Tasks.scala:156)
        at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$AWSFJTWrappedTask.internal(Tasks.scala:304)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.compute(Tasks.scala:149)
        at scala.collection.parallel.AdaptiveWorkStealingTasks$AWSTWrappedTask.compute$(Tasks.scala:148)
        at scala.collection.parallel.AdaptiveWorkStealingForkJoinTasks$AWSFJTWrappedTask.compute(Tasks.scala:304)
        at java.base/java.util.concurrent.RecursiveAction.exec(RecursiveAction.java:194)
        at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:373)
        at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1182)
        at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1655)
        at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1622)
        at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:165)
Caused by: java.lang.NullPointerException: Cannot invoke "scala.Tuple2._1()" because the return value of "java.util.Map.get(Object)" is null
        at org.kframework.parser.inner.kernel.Scanner.resolve(Scanner.java:383)
        at org.kframework.parser.inner.kernel.EarleyParser.toEarley(EarleyParser.java:714)
        at org.kframework.parser.inner.kernel.EarleyParser.getProductions(EarleyParser.java:692)
        at org.kframework.parser.inner.kernel.EarleyParser.<init>(EarleyParser.java:628)
        at org.kframework.parser.inner.ParseInModule.getParser(ParseInModule.java:303)
        at org.kframework.parser.inner.ParseInModule.parseStringTerm(ParseInModule.java:387)
        at org.kframework.parser.inner.ParseInModule.parseString(ParseInModule.java:340)
        at org.kframework.kompile.DefinitionParsing.parseBubble(DefinitionParsing.java:955)
        at org.kframework.kompile.DefinitionParsing.lambda$resolveNonConfigBubbles$37(DefinitionParsing.java:631)
        at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:273)
        at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
        at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
        at java.base/java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:992)
        at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
        at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
        at java.base/java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:960)
        at java.base/java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:934)
        at java.base/java.util.stream.AbstractTask.compute(AbstractTask.java:327)
        at java.base/java.util.concurrent.CountedCompleter.exec(CountedCompleter.java:754)
        ... 5 more
[Error] Internal: Uncaught exception thrown of type NullPointerException
(NullPointerException: null)

Also:

$ kompile --version
K version:    v7.1.104-0-g34892bf1cc
Build date:   Mi aug 14 01:57:38 EEST 2024

FWIW, this is not blocking, but it's happening often enough that it's making development fairly annoying. It's also non-deterministic, so I don't have a reliable way of reproducing it besides "Develop your own semantics that uses many modules and many private imports".

virgil-serbanuta commented 2 months ago

I moved this back to triage since the additional information may be good enough to get it unblocked.

virgil-serbanuta commented 2 months ago

I instrumented K so I got a few more details from one specific crash:

I have this syntax statement in the semantics:

    syntax MxInstructions ::= transferESDT
                                  ( source: String
                                  , destination: String
                                  , token: String
                                  , nonce: Int
                                  , value: Int
                                  )
                            | checkAccountExists(address: String)
                            | checkESDTBalance(account: String, token: String, value: Int)
                            | addToESDTBalance(account: String, token: String, delta: Int, allowNew: Bool)

In this crash, when I call Kompile, it builds a org.kframework.parser.inner.kernel.Scanner object which will cause the crash above. The module passed to this scanner only contains the first three constructor definitions in the syntax statement above, it is missing the addToESDTBalance one. Later, this scanner is used to parse an allowNew projection generated from the statement above, which fails because the scanner does not find the allowNew token (which is to be expected given the module it received).