Skip to content

Debugging

Jump to bottom
Daejun Park edited this page Jul 16, 2020 · 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 we will use 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:

    DebugSolverSend: log commands sent to SMT solver
    DebugSolverRecv: log responses received from SMT solver
    DebugProofState: log proof state
    DebugAppliedRewriteRules: log applied rewrite rules
    DebugSubstitutionSimplifier: log non-\bottom results when normalizing unification solutions
    WarnBottomTotalFunction: warn when a total function is undefined
    WarnDecidePredicateUnknown: warn when the solver cannot decide satisfiability of a formula
    WarnFunctionWithoutEvaluators: warn when encountering a function with no definition
    WarnSymbolSMTRepresentation: warn when a symbol cannot be translated for the SMT solver, despite being given an explicit translation
    DebugEvaluateCondition: log every predicate evaluated by the SMT solver
    ErrorException: log internal errors
    ErrorRewriteLoop: 
    LogMessage: 
    InfoAttemptUnification: log unification attempts
    InfoReachability: log reachability proof steps
    ErrorRewritesInstantiation: log rewrite instantiation errors
    DebugAttemptEquation: log equation application attempts
    DebugApplyEquation: log equation application successes
    DebugUnification:
Clone this wiki locally