pyk.kore_exec_covr.kore_exec_covr module

class HaskellLogEntry(value)

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]

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]]

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.