kframework / k-legacy

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

--no-prelude crashes with `java.util.NoSuchElementException: None.get` #2219

Open radumereuta opened 8 years ago

radumereuta commented 8 years ago

kompile --no-prelude

┆Issue is synchronized with this Asana task

HelenRouty commented 8 years ago

Hello, we tried to recreate this bug but could not. What we did is: kompile --no-prelude --debug k-distribution/tutorial/1_k/2_imp/lesson_4/imp.k. However, we only got an expected errorjava.lang.AssertionError: While defining module IMP-SYNTAX: Could not find symbol Id as a result of not importing prelude.k . Could you give us more specific instructions on how to reproduce the NoSuchElementException error?

Also, what is the expected result for this test?

Thank you!

cos commented 8 years ago

@radumereuta, you reported this originally. Can you give any more details on reproducing it?

radumereuta commented 8 years ago

Try it on this:

module TEST
endmodule

Just a simple empty module. Also, I've tested this on windows 10, 64 bits, if that helps.

HelenRouty commented 8 years ago

@radumereuta Thanks to your explanation, I found the same NoSuchElementException error. What should be the expected result when having an empty module? Should we throw an exception or warning or should we simply return a CompiledDefinition with a topCellInitializer of null value?

Currently, after adding three checks, we are able to kompile an empty module with an exit code 0, a warning of no corresponding syntax module, and a CompiledDefinition with KLabel of null value. Is this an expected result? Is there more that should be considered?

Thank you!

radumereuta commented 8 years ago

I'm not sure what should happen. I added this issue because I needed to create a parsing module in which nothing was included automatically. @cos suggested using this option, but I'm not even sure how this would work in the later stages of kompile. What I know for sure is that, in order for the program parser to be clean and correct, I need a way to specify that nothing should be included automatically in that module, because it would taint my grammars with productions or sorts from K. The rest of the modules I don't care.

One possible solution that was discussed at one point was to create a special suffix (-SYNTAX or -PROGRAM-PARSING) that would act as a marker for the automatic inclusion of builtin stuff.

cos commented 8 years ago

Currently, after adding three checks, we are able to kompile an empty module with an exit code 0, a warning of no corresponding syntax module,

This is good.

and a CompiledDefinition with KLabel of null value.

Which KLabel are you referring to?

HelenRouty commented 8 years ago

The KLabel topCellInitializer in CompiledDefinition

cos commented 8 years ago

what does it say on krun?

HelenRouty commented 8 years ago

We haven't checked with krun. Yeah, there might be problems with krun if we set topCellInitializer to be null. We will probably need to add several more checks.