Skip to content

Debugging

Jump to bottom
David Cox edited this page Aug 18, 2021 · 6 revisions

Function evaluation

K function rules correspond to Kore equations. There are three options available in kore-exec to debug equations:

  • --debug-apply-equation EQUATION-IDENTIFIER
    Record when an equation matching EQUATION-IDENTIFIER is successfully applied.
  • --debug-attempt-equation EQUATION-IDENTIFIER
    Record when an equation matching EQUATION-IDENTIFIER is attempted. The stages of equation evaluation are logged (argument matching, instantiation, and requirement checking), but the final result (whether the equation is applied or not) is not logged; this may be important if multiple equations could apply.
  • --debug-equation EQUATION-IDENTIFIER
    Enables both --debug-apply-equation and --debug-attempt-equation, so that every equation attempt and every applied equation is logged. This is the option used most often.

An EQUATION-IDENTIFIER is one of the following:

  • A Kore symbol name, matching all equations (rules) with the named symbol at the top of the left-hand side.
  • A K label name, matching all equations (rules) with the named label at the top of the left-hand side.
  • An equation name of the form MODULE-NAME.rule-name, matching the named equation only.

Debugging options in kore-repl

The above debugging information can be obtained via kore-repl as well, as follows:

> log [DebugApplyEquation,DebugAttemptEquation] file log.txt
> stepf 1000000000

In kore-repl, one can obtain the information for a specific step.

> step ...                                                    # go to a specific step
> log [DebugApplyEquation,DebugAttemptEquation] file log.txt  # enable logging
> step                                                        # execute a single step with logging
> log [] stderr                                               # disable logging
> step ...                                                    # execute further without logging

There are other types of logging available in kore-repl. To see available log entries, run kore-repl --help and reference the --log-entries option.

For example, to debug the SMT queries:

> log [DebugSolverSend,DebugSolverRecv,DebugEvaluateCondition] file /tmp/log.txt

The --solver-transcript flag of kore-exec will also log all queries sent to the solver.

Likewise, for kprove:

KORE_EXEC_OPTS="--solver-transcript kore-exec.smt2" kprove ...

kore-repl supports both standard and oneline log formats. For example, --log-format=oneline can help reduce log size and make the logs more palatable for quick debugging.

Clone this wiki locally