Closed RandomActsOfGrammar closed 3 months ago
What is the stack trace with SILVERTRACE=1? Is there an example to run that reproduces the issue?
I'll be traveling this week but I'll try to look in a few days.
I was able to run it with SILVERTRACE=1
:
An error occurred. Silver stack trace follows. (To see full traces including java elements, SILVERTRACE=1)
Exception in thread "main" java.lang.RuntimeException: common.exceptions.TraceException: Error while evaluating function extensibella:composed:main
at common.Util.printStackCauses(Util.java:239)
at extensibella.composed.Main.main(Main.java:22)
Caused by: common.exceptions.TraceException: Error while evaluating function extensibella:composed:main
at extensibella.composed.Pmain.invoke(Pmain.java:146)
at extensibella.composed.Main.main(Main.java:14)
Caused by: common.exceptions.TraceException: Error while evaluating function extensibella:main:mainProcess
at extensibella.main.PmainProcess.invoke(PmainProcess.java:167)
at extensibella.composed.Pmain.invoke(Pmain.java:143)
... 1 more
Caused by: common.exceptions.TraceException: Error while evaluating function extensibella:main:run:run_interactive
at extensibella.main.run.Prun_interactive.invoke(Prun_interactive.java:157)
at extensibella.main.PmainProcess$1$2$2$4$2$2.eval(PmainProcess.java:164)
at extensibella.main.PmainProcess$1$2$2$4$2$2.eval(PmainProcess.java:163)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.PmainProcess$1$2$2$4$2.eval(PmainProcess.java:164)
at extensibella.main.PmainProcess$1$2$2$4$2.eval(PmainProcess.java:162)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.PmainProcess$1$2$2$4.eval(PmainProcess.java:164)
at extensibella.main.PmainProcess$1$2$2$4.eval(PmainProcess.java:161)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.PmainProcess$1$2$2.eval(PmainProcess.java:164)
at extensibella.main.PmainProcess$1$2.eval(PmainProcess.java:164)
at extensibella.main.PmainProcess$1$2.eval(PmainProcess.java:155)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.PmainProcess$1.eval(PmainProcess.java:164)
at extensibella.main.PmainProcess$1.eval(PmainProcess.java:154)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.PmainProcess.invoke(PmainProcess.java:164)
... 2 more
Caused by: common.exceptions.TraceException: Error while evaluating function extensibella:main:run:run
at extensibella.main.run.Prun.invoke(Prun.java:246)
at extensibella.main.run.Prun_interactive.invoke(Prun_interactive.java:154)
... 24 more
Caused by: common.exceptions.TraceException: While evaling syn 'extensibella:main:run:runResult' in 'extensibella:main:run:addRunCommands' (1b316cac)
at common.DecoratedNode.evalSyn(DecoratedNode.java:506)
at common.DecoratedNode.synthesized(DecoratedNode.java:476)
at extensibella.main.run.Prun$1$2$2$4$2.eval(Prun.java:243)
at extensibella.main.run.Prun$1$2$2$4$2.eval(Prun.java:242)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.run.Prun$1$2$2$4.eval(Prun.java:243)
at extensibella.main.run.Prun$1$2$2$4.eval(Prun.java:241)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.run.Prun$1$2$2.eval(Prun.java:243)
at extensibella.main.run.Prun$1$2.eval(Prun.java:243)
at extensibella.main.run.Prun$1$2.eval(Prun.java:235)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.run.Prun$1.eval(Prun.java:243)
at extensibella.main.run.Prun$1.eval(Prun.java:234)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at extensibella.main.run.Prun.invoke(Prun.java:243)
... 25 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:core:unsafeTrace
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:144)
at extensibella.main.run.PaddRunCommands$46.eval(PaddRunCommands.java:360)
at common.DecoratedNode.evalSyn(DecoratedNode.java:504)
... 44 more
Caused by: common.exceptions.TraceException: While evaling syn 'extensibella:main:run:runResult' in 'extensibella:main:run:addRunCommands' (1a8e209b)
at common.DecoratedNode.evalSyn(DecoratedNode.java:506)
at common.DecoratedNode.synthesized(DecoratedNode.java:476)
at common.DecoratedNode.lambda$childDecoratedSynthesizedLazy$6(DecoratedNode.java:785)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:141)
... 46 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:core:unsafeTrace
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:144)
at extensibella.main.run.PaddRunCommands$46.eval(PaddRunCommands.java:360)
at common.DecoratedNode.evalSyn(DecoratedNode.java:504)
... 52 more
Caused by: common.exceptions.TraceException: While evaling syn 'extensibella:main:run:runResult' in 'extensibella:main:run:addRunCommands' (7b80be13)
at common.DecoratedNode.evalSyn(DecoratedNode.java:506)
at common.DecoratedNode.synthesized(DecoratedNode.java:476)
at common.DecoratedNode.lambda$childDecoratedSynthesizedLazy$6(DecoratedNode.java:785)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:141)
... 54 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:core:unsafeTrace
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:144)
at extensibella.main.run.PaddRunCommands$46.eval(PaddRunCommands.java:360)
at common.DecoratedNode.evalSyn(DecoratedNode.java:504)
... 60 more
Caused by: common.exceptions.TraceException: While evaling syn 'extensibella:main:run:runResult' in 'extensibella:main:run:addRunCommands' (2cf88ae1)
at common.DecoratedNode.evalSyn(DecoratedNode.java:506)
at common.DecoratedNode.synthesized(DecoratedNode.java:476)
at common.DecoratedNode.lambda$childDecoratedSynthesizedLazy$6(DecoratedNode.java:785)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:141)
... 62 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:core:unsafeTrace
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:144)
at extensibella.main.run.PaddRunCommands$46.eval(PaddRunCommands.java:360)
at common.DecoratedNode.evalSyn(DecoratedNode.java:504)
... 68 more
Caused by: common.exceptions.TraceException: While evaling local 'extensibella:main:run:addRunCommands:local:extensibella:main:run:Run_sv:356:8:finalIO' in 'extensibella:main:run:addRunCommands' (2cf88ae1)
at common.DecoratedNode.handleLocalError(DecoratedNode.java:419)
at common.DecoratedNode.evalLocalAsIs(DecoratedNode.java:406)
at common.DecoratedNode.localAsIs(DecoratedNode.java:388)
at common.DecoratedNode.lambda$localAsIsLazy$5(DecoratedNode.java:777)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.core.PunsafeTrace.invoke(PunsafeTrace.java:141)
... 70 more
Caused by: common.exceptions.TraceException: While evaling local 'extensibella:main:run:addRunCommands:local:extensibella:main:run:Run_sv:334:8:io_action_6' in 'extensibella:main:run:addRunCommands' (2cf88ae1)
at common.DecoratedNode.handleLocalError(DecoratedNode.java:419)
at common.DecoratedNode.evalLocalAsIs(DecoratedNode.java:406)
at common.DecoratedNode.localAsIs(DecoratedNode.java:388)
at extensibella.main.run.PaddRunCommands$41$1.eval(PaddRunCommands.java:344)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at common.Util.demandIndex(Util.java:94)
at extensibella.main.run.PcombineIO$1$1$1.eval(PcombineIO.java:146)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at common.Util.demandIndex(Util.java:94)
at extensibella.main.run.PaddRunCommands$40$1.invoke(PaddRunCommands.java:329)
at extensibella.main.run.PaddRunCommands$40$1.invoke(PaddRunCommands.java:326)
at extensibella.main.run.PcombineIO$1$1.eval(PcombineIO.java:146)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at common.Util.demandIndex(Util.java:94)
at extensibella.main.run.Init$103$1.invoke(Init.java:882)
at extensibella.main.run.Init$103$1.invoke(Init.java:879)
at extensibella.main.run.PcombineIO$1.invoke(PcombineIO.java:146)
at extensibella.main.run.PcombineIO$1.invoke(PcombineIO.java:143)
at extensibella.main.run.PaddRunCommands$41.eval(PaddRunCommands.java:344)
at common.DecoratedNode.evalLocalAsIs(DecoratedNode.java:404)
... 76 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:core:printT
at silver.core.PprintT.invoke(PprintT.java:144)
at extensibella.main.run.PaddRunCommands$38.eval(PaddRunCommands.java:321)
at common.DecoratedNode.evalLocalAsIs(DecoratedNode.java:404)
... 100 more
Caused by: common.exceptions.TraceException: While evaling local 'extensibella:main:run:addRunCommands:local:extensibella:main:run:output_output' in 'extensibella:main:run:addRunCommands' (2cf88ae1)
at common.DecoratedNode.handleLocalError(DecoratedNode.java:419)
at common.DecoratedNode.evalLocalAsIs(DecoratedNode.java:406)
at common.DecoratedNode.localAsIs(DecoratedNode.java:388)
at common.DecoratedNode.lambda$localAsIsLazy$5(DecoratedNode.java:777)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.core.PprintT.invoke(PprintT.java:141)
... 102 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:core:stringAppend
at silver.core.PstringAppend.invoke(PstringAppend.java:144)
at silver.core.PstringAppend$Factory.invoke(PstringAppend.java:161)
at silver.core.PstringAppend$Factory.invoke(PstringAppend.java:152)
at extensibella.main.run.PaddRunCommands$37.eval(PaddRunCommands.java:319)
at common.DecoratedNode.evalLocalAsIs(DecoratedNode.java:404)
... 108 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:core:stringAppend
at silver.core.PstringAppend.invoke(PstringAppend.java:144)
at silver.core.PstringAppend$Factory.invoke(PstringAppend.java:161)
at silver.core.PstringAppend$Factory.invoke(PstringAppend.java:152)
at extensibella.main.run.PaddRunCommands$37$2.eval(PaddRunCommands.java:319)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.core.PstringAppend.invoke(PstringAppend.java:141)
... 112 more
Caused by: common.exceptions.TraceException: Error while evaluating function extensibella:main:run:decorateAndShow
at extensibella.main.run.PdecorateAndShow.invoke(PdecorateAndShow.java:222)
at extensibella.main.run.PaddRunCommands$37$2$1.eval(PaddRunCommands.java:319)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.core.PstringAppend.invoke(PstringAppend.java:141)
... 119 more
Caused by: common.exceptions.TraceException: Error while evaluating function silver:langutil:pp:showDoc
at silver.langutil.pp.PshowDoc.invoke(PshowDoc.java:147)
at extensibella.main.run.PdecorateAndShow.invoke(PdecorateAndShow.java:219)
... 124 more
Caused by: java.lang.ArrayIndexOutOfBoundsException: Index 3 out of bounds for length 3
at common.DecoratedNode.copyInhOverrides(DecoratedNode.java:237)
at common.DecoratedNode.decorate(DecoratedNode.java:227)
at common.DecoratedNode.createDecoratedChild(DecoratedNode.java:355)
at common.DecoratedNode.childDecorated(DecoratedNode.java:336)
at common.DecoratedNode.lambda$childDecoratedSynthesizedLazy$6(DecoratedNode.java:785)
at common.Thunk.doEval(Thunk.java:45)
at common.Thunk.eval(Thunk.java:34)
at common.Util.demand(Util.java:81)
at silver.langutil.pp.PshowDoc.getChild_d(PshowDoc.java:47)
at silver.langutil.pp.PshowDoc.getChild(PshowDoc.java:69)
at common.DecoratedNode.createDecoratedChild(DecoratedNode.java:355)
at common.DecoratedNode.childDecorated(DecoratedNode.java:336)
at silver.langutil.pp.PshowDoc.invoke(PshowDoc.java:144)
... 125 more
It occurs in Extensibella, which requires installing Abella to run, and it only happens when running it interactively. You need commit d8b113e from Extensibella, and you need to run Extensibella interactively (SILVERTRACE=1 extensibella
), then copy the first three commands from the test example into Extensibella one at a time. To do this last part, you need to have Sterling installed and have compiled the Sterling standard library (go to sterling/stdLib
and run build_extensibella
) and the module for the example (go to the extensibella/test/compositionTest
directory and run sterling --extensibella -I .. compositionTest:host
).
In summary, there is an example to run that reproduces the issue, but it is a lot of effort to get there. I might try to find a smaller, self-contained, only-Silver example later.
Also, this was not an issue before I recently updated Silver on my computer in the lab. This suggests it was a relatively recent change. I don't know when exactly was the last time I had updated it, but it is probably a change within the last two or three months, certainly no later than last December.
That's alright, I think I see what the problem is from the stack trace. copyInhOverrides is assuming that
Scratch that, not quite sure I understand the stack trace. How is state defined in the place decorateAndShow is called?
It is a production attribute within a production:
production state::ProofState = top.proverState.state;
The proverState
attribute from which it is plucked is an inherited attribute.
What happens if you replace state
with new(state)
in calling decorateAndShow
? From the stack trace, I don't understand why DecoratedNode.decorate()
is being called.
Replacing state
with new(state)
there fixes it so it doesn't crash.
Okay, so it seems there are 3 issues here:
state
, which has a possibly-decorated type. In theory, we could use the presence of the inherited occurs-on contexts to specialize it to be undecorated type. But this will be irrelevant soon with #751, as one will be required to write new
explicitly.I will take a stab at fixing 1 and 3.
If I have
it works fine. If I have the following (that should be equivalent, since none of the inherited attributes are being accessed)
where we have
it crashes with the eventual message
I looked but was unable to find a message of the form shown in the last line here in Silver or Extensibella, but this is apparently the message Java gives for array out-of-bounds.
If I instead use the function made specific to one type
it does not crash.
I am using the original function with two different types in the original code.