search

Saloed / smtlib-intellij-plugin

Plugin for Intellij Idea to work with Smt-Lib language
4 stars 0 forks source link

Exception: Too many element types registered #1

Open Columpio opened 2 years ago

Columpio commented 2 years ago

I got the following exception while opening a file (in attachment: file.log; change extension to .smt2)

java.lang.Throwable: Too many element types registered. Out of (short) range. Most of element types (11564) were registered for 'Language: SmtLib': <INVALID>, Comment, '(', ')', ';', String, QuotedSymbol, 'not', 'Bool', 'continued-execution', 'error', 'false', 'immediate-exit', 'incomplete', 'logic', 'memout', 'sat', 'success', 'theory', 'true', 'unknown', 'unsupported', 'unsat', 'assert', 'check-sat', 'check-sat-assuming', 'declare-const', 'de...
    at com.intellij.openapi.diagnostic.Logger.error(Logger.java:182)
    at com.intellij.psi.tree.IElementType.<init>(IElementType.java:120)
    at com.intellij.psi.tree.IElementType.<init>(IElementType.java:98)
    at com.intellij.psi.tree.ILazyParseableElementType.<init>(ILazyParseableElementType.java:29)
    at com.intellij.psi.tree.IFileElementType.<init>(IFileElementType.java:30)
    at org.jetbrains.research.smtlib.parser.SmtLibParserDefinition.getFileNodeType(SmtLibParserDefinition.kt:50)
    at com.intellij.extapi.psi.PsiFileBase.<init>(PsiFileBase.java:29)
    at org.jetbrains.research.smtlib.psi.SmtLibFileRoot.<init>(SmtLibFileRoot.kt:9)
    at org.jetbrains.research.smtlib.parser.SmtLibParserDefinition.createFile(SmtLibParserDefinition.kt:52)
    at org.jetbrains.research.smtlib.parser.SmtLibParserDefinition.createFile(SmtLibParserDefinition.kt:27)
    at com.intellij.psi.AbstractFileViewProvider.createFile(AbstractFileViewProvider.java:144)
    at com.intellij.psi.AbstractFileViewProvider.createFile(AbstractFileViewProvider.java:128)
    at com.intellij.psi.AbstractFileViewProvider.createFile(AbstractFileViewProvider.java:117)
    at com.intellij.psi.SingleRootFileViewProvider.createFile(SingleRootFileViewProvider.java:144)
    at com.intellij.psi.SingleRootFileViewProvider.getPsiInner(SingleRootFileViewProvider.java:100)
    at com.intellij.psi.AbstractFileViewProvider.getPsi(AbstractFileViewProvider.java:194)
    at com.intellij.psi.impl.file.impl.FileManagerImpl.findFile(FileManagerImpl.java:362)
    at com.intellij.psi.impl.PsiManagerImpl.findFile(PsiManagerImpl.java:154)
    at com.jetbrains.rider.projectView.ProjectModelIconsKt$calculateProjectFileIcon$1.compute(ProjectModelIcons.kt:179)
    at com.jetbrains.rider.projectView.ProjectModelIconsKt$calculateProjectFileIcon$1.compute(ProjectModelIcons.kt)
    at com.intellij.openapi.application.impl.ApplicationImpl.runReadAction(ApplicationImpl.java:852)
    at com.jetbrains.rider.projectView.ProjectModelIconsKt.k(ProjectModelIcons.kt:178)
    at com.jetbrains.rider.projectView.ProjectModelIconsKt.calculateIcon(ProjectModelIcons.kt:81)
    at com.jetbrains.rider.projectView.views.solutionExplorer.nodes.SolutionExplorerModelNode.update(SolutionExplorerModelNode.kt:106)
    at com.intellij.ide.util.treeView.PresentableNodeDescriptor.getUpdatedPresentation(PresentableNodeDescriptor.java:78)
    at com.intellij.ide.util.treeView.PresentableNodeDescriptor.update(PresentableNodeDescriptor.java:30)
    at com.jetbrains.rider.projectView.views.impl.SolutionViewTreeModel$refresh$1.run(SolutionViewTreeModel.kt:128)
    at com.intellij.util.concurrency.Invoker$Wrapper.get(Invoker.java:338)
    at com.intellij.util.concurrency.Invoker$Wrapper.get(Invoker.java:329)
    at com.intellij.util.concurrency.Invoker$Task.run(Invoker.java:316)
    at com.intellij.openapi.application.impl.ApplicationImpl.tryRunReadAction(ApplicationImpl.java:1084)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.lambda$runInReadActionWithWriteActionPriority$0(ProgressIndicatorUtils.java:75)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.runActionAndCancelBeforeWrite(ProgressIndicatorUtils.java:158)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.lambda$runWithWriteActionPriority$1(ProgressIndicatorUtils.java:115)
    at com.intellij.openapi.progress.ProgressManager.lambda$runProcess$0(ProgressManager.java:57)
    at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$runProcess$2(CoreProgressManager.java:188)
    at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$executeProcessUnderProgress$12(CoreProgressManager.java:624)
    at com.intellij.openapi.progress.impl.CoreProgressManager.registerIndicatorAndRun(CoreProgressManager.java:698)
    at com.intellij.openapi.progress.impl.CoreProgressManager.computeUnderProgress(CoreProgressManager.java:646)
    at com.intellij.openapi.progress.impl.CoreProgressManager.executeProcessUnderProgress(CoreProgressManager.java:623)
    at com.intellij.openapi.progress.impl.ProgressManagerImpl.executeProcessUnderProgress(ProgressManagerImpl.java:66)
    at com.intellij.openapi.progress.impl.CoreProgressManager.runProcess(CoreProgressManager.java:175)
    at com.intellij.openapi.progress.ProgressManager.runProcess(ProgressManager.java:57)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.runWithWriteActionPriority(ProgressIndicatorUtils.java:112)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.runInReadActionWithWriteActionPriority(ProgressIndicatorUtils.java:75)
    at com.intellij.util.concurrency.Invoker.invokeSafely(Invoker.java:205)
    at com.intellij.util.concurrency.Invoker.lambda$offerSafely$0(Invoker.java:183)
    at com.intellij.util.concurrency.Invoker$Background.lambda$offer$0(Invoker.java:486)
    at com.intellij.util.concurrency.BoundedTaskExecutor.doRun(BoundedTaskExecutor.java:246)
    at com.intellij.util.concurrency.BoundedTaskExecutor.access$200(BoundedTaskExecutor.java:32)
    at com.intellij.util.concurrency.BoundedTaskExecutor$1.execute(BoundedTaskExecutor.java:225)
    at com.intellij.util.ConcurrencyUtil.runUnderThreadName(ConcurrencyUtil.java:213)
    at com.intellij.util.concurrency.BoundedTaskExecutor$1.run(BoundedTaskExecutor.java:214)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665)
    at java.base/java.security.AccessController.doPrivileged(Native Method)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665)
    at java.base/java.lang.Thread.run(Thread.java:829)
Saloed commented 2 years ago

Which plugin version do you use? I can't reproduce it with plugin version 0.11 and idea version IU-213.6777.52.

Columpio commented 2 years ago

JetBrains Rider 2021.3.3 Build #RD-213.6775.4, built on January 26, 2022 Runtime version: 11.0.13+7-b1751.25 amd64 VM: Dynamic Code Evolution 64-Bit Server VM by JetBrains s.r.o. .NET 6.0.1

Plugin has v. 0.11

Maybe I am wrong with this particular smt2 file, but the bug seems to reproduce regularly while normal working with smt2 files. Actually, I have no way on how to diagnose a problem. Could you please add more logging in your plugin or something? Maybe registering it as an official JetBrains plugin will help?

This also seems relevant.

Saloed commented 2 years ago

This issue should be fixed now. Could you try latest plugin version 0.11.1?

Ps: default file extension changed from .smtlib to .smt2.

Columpio commented 2 years ago

Thanks, I'll try it

Columpio commented 2 years ago

Now I get the following:

Error during async editor loading

com.intellij.diagnostic.PluginException: Discontinuous sequence of tokens is generated by lexer: org.antlr.intellij.adaptor.lexer.ANTLRLexerAdaptor [Plugin: org.jetbrains.research.smtlib]
    at com.intellij.ide.plugins.PluginManagerCore.createPluginException(PluginManagerCore.java:290)
    at com.intellij.diagnostic.PluginProblemReporterImpl.createPluginExceptionByClass(PluginProblemReporterImpl.java:12)
    at com.intellij.diagnostic.PluginException.createByClass(PluginException.java:83)
    at com.intellij.openapi.editor.ex.util.ValidatingLexerWrapper.throwException(ValidatingLexerWrapper.java:126)
    at com.intellij.openapi.editor.ex.util.ValidatingLexerWrapper.advance(ValidatingLexerWrapper.java:94)
    at com.intellij.openapi.editor.ex.util.LexerEditorHighlighter.doSetText(LexerEditorHighlighter.java:453)
    at com.intellij.openapi.editor.ex.util.LexerEditorHighlighter.setText(LexerEditorHighlighter.java:420)
    at com.intellij.openapi.fileEditor.impl.text.TextEditorImpl.loadEditorInBackground(TextEditorImpl.java:74)
    at com.intellij.openapi.fileEditor.impl.text.PsiAwareTextEditorImpl.loadEditorInBackground(PsiAwareTextEditorImpl.java:42)
    at com.intellij.openapi.fileEditor.impl.text.AsyncEditorLoader.lambda$scheduleLoading$0(AsyncEditorLoader.java:95)
    at com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:818)
    at com.intellij.openapi.fileEditor.impl.text.AsyncEditorLoader.lambda$scheduleLoading$1(AsyncEditorLoader.java:93)
    at com.intellij.openapi.application.impl.NonBlockingReadActionImpl$Submission.insideReadAction(NonBlockingReadActionImpl.java:521)
    at com.intellij.openapi.application.impl.NonBlockingReadActionImpl$Submission.lambda$attemptComputation$3(NonBlockingReadActionImpl.java:486)
    at com.intellij.openapi.application.impl.ApplicationImpl.tryRunReadAction(ApplicationImpl.java:1084)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.lambda$runInReadActionWithWriteActionPriority$0(ProgressIndicatorUtils.java:75)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.runActionAndCancelBeforeWrite(ProgressIndicatorUtils.java:158)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.lambda$runWithWriteActionPriority$1(ProgressIndicatorUtils.java:115)
    at com.intellij.openapi.progress.ProgressManager.lambda$runProcess$0(ProgressManager.java:57)
    at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$runProcess$2(CoreProgressManager.java:188)
    at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$executeProcessUnderProgress$12(CoreProgressManager.java:624)
    at com.intellij.openapi.progress.impl.CoreProgressManager.registerIndicatorAndRun(CoreProgressManager.java:698)
    at com.intellij.openapi.progress.impl.CoreProgressManager.computeUnderProgress(CoreProgressManager.java:646)
    at com.intellij.openapi.progress.impl.CoreProgressManager.executeProcessUnderProgress(CoreProgressManager.java:623)
    at com.intellij.openapi.progress.impl.ProgressManagerImpl.executeProcessUnderProgress(ProgressManagerImpl.java:66)
    at com.intellij.openapi.progress.impl.CoreProgressManager.runProcess(CoreProgressManager.java:175)
    at com.intellij.openapi.progress.ProgressManager.runProcess(ProgressManager.java:57)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.runWithWriteActionPriority(ProgressIndicatorUtils.java:112)
    at com.intellij.openapi.progress.util.ProgressIndicatorUtils.runInReadActionWithWriteActionPriority(ProgressIndicatorUtils.java:75)
    at com.intellij.openapi.application.impl.NonBlockingReadActionImpl$Submission.attemptComputation(NonBlockingReadActionImpl.java:486)
    at com.intellij.openapi.application.impl.NonBlockingReadActionImpl$Submission.lambda$transferToBgThread$1(NonBlockingReadActionImpl.java:407)
    at com.intellij.codeWithMe.ClientId$Companion$decorateRunnable$1.run(ClientId.kt:223)
    at com.intellij.util.concurrency.BoundedTaskExecutor.doRun(BoundedTaskExecutor.java:246)
    at com.intellij.util.concurrency.BoundedTaskExecutor.access$200(BoundedTaskExecutor.java:32)
    at com.intellij.util.concurrency.BoundedTaskExecutor$1.execute(BoundedTaskExecutor.java:225)
    at com.intellij.util.ConcurrencyUtil.runUnderThreadName(ConcurrencyUtil.java:213)
    at com.intellij.util.concurrency.BoundedTaskExecutor$1.run(BoundedTaskExecutor.java:214)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665)
    at java.base/java.security.AccessController.doPrivileged(Native Method)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665)
    at java.base/java.lang.Thread.run(Thread.java:829)
Saloed commented 2 years ago

This issue connected with current lexer implementation. Your file contains some symbols which are not recognized by the lexer. Can you provide a file on which you received this error?

Saloed commented 2 years ago

My implementation is already based on this grammar. But sometimes some symbols are not recognized properly.