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

Traverse a one-line log file produced by K’s Haskell backend and extract 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.