Skip to content
This repository was archived by the owner on Feb 1, 2020. It is now read-only.
This repository was archived by the owner on Feb 1, 2020. It is now read-only.

Unimplemented Exception #2390

Open
Open
Unimplemented Exception#2390
@tawaren

Description

@tawaren
tawaren
opened on Jan 4, 2018

I had some rules that had the same identifier at least twice on the left hand side, with the intention that the positions where they appear need to have the same value (I assume that is how it should). It seemed to work for a long time (but this may be because of the lack of rigorous testing). Then one day I got a strange exception (see later). I only could get rid of it by replacing all of the mentioned rules by ones that capture the value with different names and then use a when V1 ==K V2 clause to ensure identity.

java.lang.AssertionError: unimplemented
at org.kframework.utils.OneIntegerGenericBitSet.clear(OneIntegerGenericBitSet.java:183)
at org.kframework.backend.java.symbolic.FastRuleMatcher.addSubstitution(FastRuleMatcher.java:476)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:241)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:247)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:159)
at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:100)
at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:81)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
at org.kframework.krun.KRun.run(KRun.java:86)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:110)
at org.kframework.main.Main.runApplication(Main.java:100)
at org.kframework.main.Main.main(Main.java:52)
java.lang.AssertionError: unimplemented
at org.kframework.utils.OneIntegerGenericBitSet.clear(OneIntegerGenericBitSet.java:183)
at org.kframework.backend.java.symbolic.FastRuleMatcher.addSubstitution(FastRuleMatcher.java:476)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:241)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:247)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchInside(FastRuleMatcher.java:350)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:252)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:423)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:159)
at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:100)
at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:81)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:137)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
at org.kframework.krun.KRun.run(KRun.java:86)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:110)
at org.kframework.main.Main.runApplication(Main.java:100)
at org.kframework.main.Main.main(Main.java:52)
[Error] Internal: Uncaught exception thrown of type AssertionError.
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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions