K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

Hi,

The --debugger option in K 3.6 was never really fully implemented to the point of working correctly all the time. As such, it probably will not work and will likely not be updated to work in the near future. That said, there are a couple options you can choose from.

1. The K 4.0 beta that currently exists in the master branch on github (and which you can download here: http://kframework.org/imgs/releases/k-nightly.tar.gz) will, within the next few days, support a version of the K 4.0 release that includes a fully featured and well-tested debugger similar in style to the OCAML debugger. You can track the progress of the pull request that enables this functionality by default here: https://github.com/kframework/k/pull/1819  If you don't want to wait until this code is merged, you can also get the same functionality in the current master by passing the flag "--kore" to kompile and krun. Note however that the K 4.0 release is a breaking release that will require you to modify your definition, and is also very much still a work in progress and not ready to be a release candidate yet. So you may run into bugs and issues if you try this approach.

2. You can also achieve something similar to a low-tech debugger in krun with the "--depth" and "--statistics" flags. If you run "krun tests/fib.erl --statistics on",  it should output on the command line the total number of rewrite steps that execution takes.  You can then perform a binary search to find the exact point in the execution that you care about by using the "--depth" flag. For example, if the statistics say that 500 rewrite steps took place, you could specify --depth 250 to view the configuration halfway through execution. If that looks like it has moved farther than the step you care about, you can try again with a smaller depth, otherwise you can try again with a larger depth and iterate until you get to the spot you want. Once you have reached the step that you care about, you can examine the configuration to determine what rule has applied at that step and fix it if it is incorrect.

Does this provide you with the tools you need to solve your issue?

On Thu, Oct 29, 2015 at 2:01 PM, Hopácsiné Kőszegi Judit <koszegijudit AT caesar.elte.hu> wrote:

Hello,

I would like to look at the rewriting steps the K framework make while executing a program, and I have found "--debugger" (experimental) option of krun.

I tried to krun my test program with --debugger flag, it started to work, but after a "step" command, I got an exception. Isn't it a proper command?

Details:
$ krun --debugger --debug tests/fib.erl
After running one step of execution the result is:

<T>
    ...
    ...
</T>

Command > step
java.util.NoSuchElementException: No value present
    at java.util.Optional.get(Optional.java:135)
    at org.kframework.krun.api.ExecutorDebugger.step(ExecutorDebugger.java:112)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:266)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:124)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:131)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)
java.util.NoSuchElementException: No value present
    at java.util.Optional.get(Optional.java:135)
    at org.kframework.krun.api.ExecutorDebugger.step(ExecutorDebugger.java:112)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:266)
    at org.kframework.krun.tools.Debugger$Tool.run(Debugger.java:124)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:131)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
    at org.kframework.main.Main.runApplication(Main.java:109)
    at org.kframework.main.Main.runApplication(Main.java:99)
    at org.kframework.main.Main.main(Main.java:51)
[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
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

$ krun --version
K framework version 3.6
Git revision: 28ea17d
Git branch: UNKNOWN
Build date: Fri Aug 21 21:36:54 BST 2015

Operating system: Ubuntu 14.04 LTS

Thanks,
Judit H. Koszegi