pyk.kore_exec_covr.kore_exec_covr module

class HaskellLogEntry(value)[source]

Bases: Enum

An enumeration.

DEBUG_APPLIED_REWRITE_RULES = 'DebugAppliedRewriteRules'
DEBUG_APPLY_EQUATION = 'DebugApplyEquation'
build_rule_dict(definition: KDefinition, *, skip_projections: bool = True, skip_initializers: bool = True) dict[str, KRule][source]

Traverse the kompiled definition and build a dictionary mapping str(file:location) to KRule.

parse_rule_applications(haskell_backend_oneline_log_file: Path) dict[HaskellLogEntry, dict[str, int]][source]

Process a one-line log file produced by K’s Haskell backend.

Extracts information about:

  • Applied rewrites (DebugAppliedRewriteRules).

  • Applied simplifications (DEBUG_APPLY_EQUATION).

Note

Haskell backend logs often contain rule applications with empty locations. It seems likely that those are generated projection rules. We report their applications in bulk with UNKNOWN location.