apalache-mc/apalache

Unhandled Exception (java.util.NoSuchElementException: None.get) on empty file input

lemmy opened this issue · 4 comments

lemmy commented

Impact

Workaround: Non-empty file

Input specification

The command line parameters used to run the tool

markus@avocado [15:53:40] [~/src/TLA]
-> % touch empty.tla

markus@avocado [15:53:45] [~/src/TLA]
-> % apalache-mc parse empty.tla
15:53:47.635 [main] INFO at.forsyte.apalache.tla.tooling.opt.ParseCmd -- Loading configuration
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Output directory: /Users/markus/src/TLA/_apalache-out/empty.tla/2024-01-09T15-53-47_3481045725668745826
# APALACHE version: 0.44.2 | build: 3360796                       I@15:53:47.834
Parse empty.tla                                                   I@15:53:47.844
PASS #0: SanyParser                                               I@15:53:47.955
Parsing file /Users/markus/src/TLA/empty.tla
Unhandled exception                                               E@15:53:48.032
java.util.NoSuchElementException: None.get
	at scala.None$.get(Option.scala:627)
	at scala.None$.get(Option.scala:626)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.loadFromTlaFile(SanyParserPassImpl.scala:75)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.$anonfun$loadFromTlaSource$1(SanyParserPassImpl.scala:87)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.parseSource(SanyParserPassImpl.scala:132)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.execute(SanyParserPassImpl.scala:114)
	at at.forsyte.apalache.infra.passes.PassChainExecutor$.exec(PassChainExecutor.scala:64)
	at at.forsyte.apalache.infra.passes.PassChainExecutor$.$anonfun$runPassOnModule$3(PassChainExecutor.scala:53)
	at scala.util.Either.flatMap(Either.scala:352)
	at at.forsyte.apalache.infra.passes.PassChainExecutor$.$anonfun$runPassOnModule$1(PassChainExecutor.scala:51)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor$.runOnPasses(PassChainExecutor.scala:44)
	at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:34)
	at at.forsyte.apalache.tla.tooling.opt.ParseCmd.run(ParseCmd.scala:35)
	at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:138)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:118)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: java.util.NoSuchElementException: None.get
A bug report template has been generated at [/Users/markus/src/TLA/_apalache-out/empty.tla/2024-01-09T15-53-47_3481045725668745826/BugReport.md].
If you choose to use it, please complete the template with a description of the expected behavior and impact.
It took me 0 days  0 hours  0 min  0 sec                          I@15:53:48.037
Total time: 0.200 sec                                             I@15:53:48.037
EXITCODE: ERROR (255)

Expected behavior

Graceful/Meaningful error message

Log files

2024-01-09T15:53:47,834 [main] INFO  a.f.a.t.Tool\$ - # APALACHE version: 0.44.2 | build: 3360796
2024-01-09T15:53:47,844 [main] INFO  a.f.a.t.t.o.ParseCmd - Parse empty.tla
2024-01-09T15:53:47,955 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser
2024-01-09T15:53:48,032 [main] ERROR a.f.a.t.Tool\$ - Unhandled exception
java.util.NoSuchElementException: None.get
	at scala.None\$.get(Option.scala:627)
	at scala.None\$.get(Option.scala:626)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.loadFromTlaFile(SanyParserPassImpl.scala:75)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.\$anonfun\$loadFromTlaSource\$1(SanyParserPassImpl.scala:87)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.parseSource(SanyParserPassImpl.scala:132)
	at at.forsyte.apalache.tla.passes.imp.SanyParserPassImpl.execute(SanyParserPassImpl.scala:114)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.exec(PassChainExecutor.scala:64)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$3(PassChainExecutor.scala:53)
	at scala.util.Either.flatMap(Either.scala:352)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$1(PassChainExecutor.scala:51)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.runOnPasses(PassChainExecutor.scala:44)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:34)
	at at.forsyte.apalache.tla.tooling.opt.ParseCmd.run(ParseCmd.scala:35)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

System information

  • Apalache version: 0.44.2 build 3360796
  • OS: Mac OS X
  • JDK version: 11.0.21

Triage checklist (for maintainers)

  • Reproduce the bug on the main development branch.
  • Add the issue to the apalache GitHub project.
  • If the bug is high impact, ensure someone available is assigned to fix it.
shonfeder commented

Thank you for the report! This should be an easy fix :)

fan-tom commented

@shonfeder in case you won't have time/will, I can take it, the fix is ralteively easy but looks a bit dirty for me

Index: tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala
IDEA additional info:
Subsystem: com.intellij.openapi.diff.impl.patch.CharsetEP
<+>UTF-8
===================================================================
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala
--- a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala	(revision e8c3b166309fe0c7200db26db3225b02fe252c74)
+++ b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala	(date 1705864071162)
@@ -114,7 +114,10 @@
           ModuleTranslator(sourceStore, annotationStore).translate(node))
       }
 
-    (specObj.getName, modmap)
+    specObj.getName match {
+      case null => throw new SanyImporterException("No root module defined in file")
+      case name => (name, modmap)
+    }
   }
 
   /**
Output for empty file 
23:12:07.880 [main] INFO at.forsyte.apalache.tla.tooling.opt.ParseCmd -- Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /Users/alexey/dev/private/tlaplus/apalache/_apalache-out/current.tla/2024-01-21T23-12-08_17552644758555314631
# APALACHE version: v0.44.2-42-g45bdbc6b8 | build: v0.44.2-42-g45bdbc6b8 I@23:12:08.393
Parse current.tla                                                 I@23:12:08.407
PASS #0: SanyParser                                               I@23:12:08.666
Not running from fat JAR and APALACHE_HOME is not set;            W@23:12:08.670
will not be able to find the Apalache standard library.           W@23:12:08.670
Parsing file /Users/alexey/dev/private/tlaplus/apalache/current.tla
Parsing error: No root module defined in file                     E@23:12:08.799
Parser has failed                                                 I@23:12:08.844
It took me 0 days  0 hours  0 min  0 sec                          I@23:12:08.844
Total time: 0.449 sec                                             I@23:12:08.844
EXITCODE: ERROR (255)
shonfeder commented

That looks right. I'd be very grateful if you picked this up! Thanks, @fan-tom. Let me know how I can help :)

shonfeder commented

That seems like a nice fix to me. Looking at https://github.com/tlaplus/tlaplus/blob/238ff3c95a1db3f92eb5daee8800520e0170fc6c/tlatools/org.lamport.tlatools/src/tla2sany/modanalyzer/SpecObj.java I dont see any methods that would obviously be less dirty :)