pyfcstm.bmc.binding

Semantic binding for parser-independent FCSTM BMC queries.

The binding layer sits between the .fbmcq parser and later BMC engine or solver lowering code. It validates query-context rules that are deliberately not encoded in the grammar, optionally resolves model paths through a pyfcstm.bmc.domain.BmcDomain, and returns a stable, JSON-friendly binding snapshot.

Design contracts:

Structure-only binding does not import pyfcstm.model, pyfcstm.solver, pyfcstm.verify, or z3.
Parser errors remain pyfcstm.bmc.errors.BmcQueryParseError; semantic binding errors use pyfcstm.bmc.errors.InvalidBmcQuery with a BmcBindingDiagnostic attached.
Bound objects preserve the original parser AST and expose to_canonical() for golden tests and future engine handoff.
This binding layer keeps frame-local predicates conservative: omitted and current frame selectors are accepted, while explicit integer frame selectors are rejected outside event assumptions.

The module contains:

BmcBindingDiagnostic - Stable binding diagnostic.
BoundReference - Model reference discovered during binding.
BoundInitialSpec, BoundAssumption, BoundProperty, and BoundBmcQuery - Normalized bound query snapshots.
bind_bmc_query_structure() - Query-only semantic binding.
bind_bmc_query() - Optional model/domain-aware binding.

Example:

>>> from pyfcstm.bmc.parse import parse_bmc_query
>>> from pyfcstm.bmc.binding import bind_bmc_query_structure
>>> bound = bind_bmc_query_structure(parse_bmc_query('check reach <= 1: true;'))
>>> bound.property.kind
'reach'

all

pyfcstm.bmc.binding.__all__ = ['BmcBindingDiagnostic', 'BoundReference', 'BoundInitialSpec', 'BoundAssumption', 'BoundProperty', 'BoundBmcQuery', 'bind_bmc_query_structure', 'bind_bmc_query']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

BmcBindingDiagnostic

class pyfcstm.bmc.binding.BmcBindingDiagnostic(code: str, path: str, message: str)[source]

Stable diagnostic emitted by the BMC query binder.

Parameters:

code (str) – Stable machine-readable diagnostic code.
path (str) – Semantic node path such as "property.predicate".
message (str) – Human-readable diagnostic message.

Example:

>>> diag = BmcBindingDiagnostic('bad_context', 'property', 'not allowed')
>>> diag.to_canonical()['code']
'bad_context'

__str__() → str[source]

Return a compact diagnostic string.

Returns:: Human-readable diagnostic summary.
Return type:: str

Example:

>>> str(BmcBindingDiagnostic('code', 'path', 'message'))
'code at path: message'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable diagnostic dictionary.

Returns:: Canonical diagnostic dictionary.
Return type:: Dict[str, str]

Example:

>>> BmcBindingDiagnostic('code', 'path', 'message').to_canonical()['path']
'path'

BoundReference

class pyfcstm.bmc.binding.BoundReference(kind: str, name: str, path: str, spelling: str, resolved_id: int | None = None, declared_type: str | None = None)[source]

Reference discovered and optionally resolved during query binding.

Parameters:

kind (str) – Reference category: "state", "event", or "variable".
name (str) – Query-visible name or path.
path (str) – Semantic expression path where the reference was found.
spelling (str) – Source spelling family such as "active", "event", "bare", or "var_call".
resolved_id (int, optional) – Domain id when model/domain-aware binding is used, defaults to None.
declared_type (str, optional) – Variable declared type for resolved variable refs, defaults to None.

Example:

>>> BoundReference('variable', 'x', 'property.predicate', 'bare').to_canonical()['name']
'x'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable reference dictionary.

Returns:: Canonical reference dictionary.
Return type:: Dict[str, object]

Example:

>>> BoundReference('state', 'Root', 'initial', 'state_path').to_canonical()['kind']
'state'

BoundInitialSpec

class pyfcstm.bmc.binding.BoundInitialSpec(source: InitialSpec, resolved_state_id: int | None = None, resolved_havoc_variables: Tuple[str, ...] | None = None)[source]

Bound initial-frame query specification.

Parameters:

source (InitialSpec) – Original parser-independent initial spec.
resolved_state_id (int, optional) – Domain state id for mode="state" when resolved, defaults to None.
resolved_havoc_variables (Tuple[str, ...], optional) – Domain-order variable names whose declaration initializers are skipped, or None when no domain was supplied, defaults to None.

Example:

>>> BoundInitialSpec(InitialSpec()).to_canonical()['mode']
'cold'

havoc_names(domain: object) → Tuple[str, ...][source]

Return domain-resolved initial havoc variable names.

Parameters:: domain (object) – BMC domain used when a wildcard policy must be expanded.
Returns:: Variable names skipped by the initial variable policy.
Return type:: Tuple[str, …]

Example:

>>> BoundInitialSpec(InitialSpec()).havoc_names(())
()

property mode: str

Return the initial mode.

Returns:: Initial mode string.
Return type:: str

property predicate: BmcCondExpr | None

Return the optional initial predicate.

Returns:: Initial predicate or None.
Return type:: Optional[BmcCondExpr]

to_canonical() → Dict[str, Any][source]

Return a JSON-stable bound initial-spec dictionary.

Returns:: Canonical bound initial specification.
Return type:: Dict[str, object]

Example:

>>> BoundInitialSpec(InitialSpec()).to_canonical()['node']
'bound_initial_spec'

property variable_policy: InitialVariablePolicy

Return the source initial variable policy.

Returns:: Initial variable policy.
Return type:: pyfcstm.bmc.query.InitialVariablePolicy

BoundAssumption

class pyfcstm.bmc.binding.BoundAssumption(source: BmcAssumption, kind: str, frame: int | None = None, cycles: Tuple[int, ...] = (), resolved_event_ids: Tuple[int, ...] = ())[source]

Bound query assumption.

Parameters:

source (BmcAssumption) – Original assumption object.
kind (str) – Bound assumption category.
frame (int, optional) – Frame index for frame assumptions, defaults to None.
cycles (Tuple[int, ...], optional) – Event cycles selected by event assumptions.
resolved_event_ids (Tuple[int, ...], optional) – Resolved event ids for event assumptions, defaults to ().

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> src = FrameAssumption('always', BoolLiteral('true'))
>>> BoundAssumption(src, 'frame').to_canonical()['kind']
'frame'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable bound assumption dictionary.

Returns:: Canonical bound assumption.
Return type:: Dict[str, object]

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> src = FrameAssumption('always', BoolLiteral('true'))
>>> BoundAssumption(src, 'frame').to_canonical()['node']
'bound_assumption'

BoundProperty

class pyfcstm.bmc.binding.BoundProperty(source: BmcProperty, case_label: str | None = None)[source]

Bound BMC query property.

Parameters:

source (BmcProperty) – Original property object.
case_label (str, optional) – Cover case label when kind="cover", defaults to None.

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> prop = BmcProperty('reach', 1, predicate=BoolLiteral('true'))
>>> BoundProperty(prop).bound
1

property bound: int

Return the positive query bound.

Returns:: Query bound.
Return type:: int

property kind: str

Return the property kind.

Returns:: Property kind.
Return type:: str

to_canonical() → Dict[str, Any][source]

Return a JSON-stable bound property dictionary.

Returns:: Canonical bound property.
Return type:: Dict[str, object]

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> prop = BmcProperty('reach', 1, predicate=BoolLiteral('true'))
>>> BoundProperty(prop).to_canonical()['kind']
'reach'

BoundBmcQuery

class pyfcstm.bmc.binding.BoundBmcQuery(query: ~pyfcstm.bmc.query.BmcQuery, initial: ~pyfcstm.bmc.binding.BoundInitialSpec, assumptions: ~typing.Tuple[~pyfcstm.bmc.binding.BoundAssumption, ...], property: ~pyfcstm.bmc.binding.BoundProperty, references: ~typing.Tuple[~pyfcstm.bmc.binding.BoundReference, ...] = <factory>)[source]

Complete semantically bound BMC query snapshot.

Parameters:

query (BmcQuery) – Original parser-independent query.
initial (BoundInitialSpec) – Bound initial specification.
assumptions (Tuple[BoundAssumption, ...]) – Bound assumptions.
property (BoundProperty) – Bound property.
references (Tuple[BoundReference, ...], optional) – References found while binding, defaults to ().

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> prop = BmcProperty('reach', 1, predicate=BoolLiteral('true'))
>>> bound = BoundBmcQuery(BmcQuery(property=prop), BoundInitialSpec(InitialSpec()), (), BoundProperty(prop))
>>> bound.to_canonical()['node']
'bound_bmc_query'

to_ast_node() → BmcQuery[source]

Return the parser-independent query AST bound by this snapshot.

Binding metadata such as resolved ids and declared variable types is intentionally not represented in the returned query object. Callers can render the returned pyfcstm.bmc.query.BmcQuery back to canonical .fbmcq text, parse it again, and re-bind it with the same model or domain when binding metadata must be reproduced.

Returns:: Original parser-independent BMC query object.
Return type:: pyfcstm.bmc.query.BmcQuery

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> prop = BmcProperty('reach', 1, predicate=BoolLiteral('true'))
>>> query = BmcQuery(property=prop)
>>> bound = BoundBmcQuery(query, BoundInitialSpec(InitialSpec()), (), BoundProperty(prop))
>>> bound.to_ast_node() is query
True

to_canonical() → Dict[str, Any][source]

Return a JSON-stable bound query dictionary.

Returns:: Canonical bound query.
Return type:: Dict[str, object]

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> prop = BmcProperty('reach', 1, predicate=BoolLiteral('true'))
>>> bound = BoundBmcQuery(BmcQuery(property=prop), BoundInitialSpec(InitialSpec()), (), BoundProperty(prop))
>>> bound.to_canonical()['property']['bound']
1

bind_bmc_query_structure

pyfcstm.bmc.binding.bind_bmc_query_structure(query: BmcQuery) → BoundBmcQuery[source]

Bind a BMC query without loading or resolving a model domain.

Parameters:: query (BmcQuery) – Parser-independent BMC query object.
Returns:: Query-only bound snapshot.
Return type:: BoundBmcQuery
Raises:: pyfcstm.bmc.errors.InvalidBmcQuery – If the query violates semantic context rules.

Example:

>>> from pyfcstm.bmc.parse import parse_bmc_query
>>> bound = bind_bmc_query_structure(parse_bmc_query('check reach <= 1: true;'))
>>> bound.property.bound
1

bind_bmc_query

pyfcstm.bmc.binding.bind_bmc_query(query: BmcQuery, model: object | None = None, domain: object | None = None) → BoundBmcQuery[source]

Bind a BMC query with optional model/domain resolution.

Parameters:

query (BmcQuery) – Parser-independent BMC query object.
model (object, optional) – Optional state machine. When supplied without domain, a pyfcstm.bmc.domain.BmcDomain is built from query’s bound.
domain (object, optional) – Optional pre-built domain. Its bound must match query.property.bound.

Returns:

Bound query snapshot.

Return type:

BoundBmcQuery

Raises:

pyfcstm.bmc.errors.InvalidBmcQuery – If query binding fails, both model and domain are supplied, or the supplied domain bound does not match the query bound.

Example:

>>> from pyfcstm.bmc.parse import parse_bmc_query
>>> bind_bmc_query(parse_bmc_query('check reach <= 1: true;')).property.kind
'reach'

pyfcstm.bmc.binding

__all__

BmcBindingDiagnostic

BoundReference

BoundInitialSpec

BoundAssumption

BoundProperty

BoundBmcQuery

bind_bmc_query_structure

bind_bmc_query

all