"""Typed expression data model for FCSTM BMC queries.
This module defines the parser-independent expression objects used by
``*.fbmcq`` queries. The core expression nodes intentionally mirror the
current FCSTM numeric and condition expression split, while BMC-only nodes add
frame, cycle, active-state, event, case, and abstract-call atoms. The objects
are frozen dataclasses and expose :meth:`BmcExpr.to_canonical` so later parser
parity tests can compare FCSTM and FBMCQ expressions through a stable,
language-neutral shape.
Design contracts:
* Expression nodes are data-only; they do not bind names, inspect models, or
lower anything to Z3.
* :func:`str` on every concrete expression returns canonical ``.fbmcq`` DSL
text. This is the object-to-text half of the query round-trip contract.
* :func:`repr` stays the dataclass-generated debugging representation and must
not be rewritten into DSL text.
* Numeric and condition expression categories stay separate at construction
time, matching FCSTM ``num_expression`` and ``cond_expression``.
* FCSTM-compatible expression checks intentionally use normal Python
``ValueError`` / ``TypeError`` failures for malformed literals, operators,
and operand categories. Query-facing BMC atom fields such as quoted paths,
frames, selectors, and atom spellings raise
:class:`pyfcstm.bmc.errors.InvalidBmcQuery`, matching the top-level query
wrappers in :mod:`pyfcstm.bmc.query`. Parser and binder code should not
assume one exception family covers both layers.
* Literal canonical values are kept JSON-portable. Float literals that would
overflow Python's finite ``float`` range are rejected at construction time.
Finite Python floats, including subnormal values and underflow-to-zero raw
spellings, are accepted because they match the current FCSTM literal
conversion boundary; raw text still preserves exact spelling for parity
checks and later encoding layers may impose stricter numeric policies.
* Identifier and path shape validation is shallow here: quoted query atoms only
require non-empty strings, and later binder layers resolve model paths and
reject impossible state, event, variable, case, or call names.
* The event atom always prints its cycle selector explicitly, including
``current``. This keeps event queries visually distinct from frame-based
atoms such as ``active("Root.A")`` whose default frame may be omitted.
The module contains:
* :class:`BmcNumExpr` and :class:`BmcCondExpr` - Typed numeric and condition
expression bases.
* FCSTM-compatible nodes such as :class:`IntLiteral`, :class:`NameRef`,
:class:`NumBinaryOp`, :class:`NumericComparison`, and :class:`CondBinaryOp`.
* BMC-only extension nodes such as :class:`FrameVar`, :class:`Cycle`,
:class:`Active`, :class:`Event`, :class:`Case`, :class:`CallCount`, and
:class:`Called`.
Example::
>>> from pyfcstm.bmc.ast import Active, IntLiteral, NameRef, NumericComparison
>>> expr = NumericComparison(NameRef("x"), "<=", IntLiteral("3"))
>>> expr.to_canonical()["op"]
'<='
>>> isinstance(Active("Root.Idle"), BmcCondExpr)
True
"""
from __future__ import annotations
import json
import math
import re
from abc import ABC, abstractmethod
from dataclasses import dataclass
from typing import Any, ClassVar, Dict, Optional, Tuple, Union
from .errors import InvalidBmcQuery
try:
from typing import Literal
except ImportError: # pragma: no cover - Python < 3.8 compatibility
from typing_extensions import Literal
_FrameSelector = Union[int, Literal["current"]]
_CallStepPointKind = Literal["absolute", "relative"]
_CallStepSelectorKind = Literal["omitted", "all", "point", "range"]
_CanonicalDict = Dict[str, Any]
_DECIMAL_INT_RE = re.compile(r"^[0-9]+$")
_HEX_INT_RE = re.compile(r"^0x[0-9a-fA-F]+$")
_FLOAT_RE = re.compile(
r"^(?:[0-9]+\.[0-9]*|\.[0-9]+)(?:[eE][+-]?[0-9]+)?$"
r"|^[0-9]+[eE][+-]?[0-9]+$"
)
_ID_RE = re.compile(r"^[a-zA-Z_][a-zA-Z0-9_]*$")
_FCSTM_RESERVED_NAMES = {
"import",
"def",
"event",
"as",
"named",
"pseudo",
"state",
"enter",
"exit",
"during",
"before",
"after",
"abstract",
"ref",
"effect",
"if",
"else",
"int",
"float",
"pi",
"E",
"tau",
"and",
"or",
"not",
"xor",
"implies",
"iff",
"True",
"true",
"TRUE",
"False",
"false",
"FALSE",
}
_FBMCQ_RESERVED_NAMES = {
"init",
"cold",
"terminated",
"state",
"assume",
"always",
"at",
"event",
"events",
"cardinality",
"any",
"at_most_one",
"check",
"reach",
"forbid",
"invariant",
"must_reach",
"exists_always",
"response",
"cover",
"trigger",
"within",
"where",
"havoc",
"current",
"var",
"cycle",
"active",
"case",
"called",
"call_count",
"null",
}
_BARE_NAME_RESERVED = _FCSTM_RESERVED_NAMES | _FBMCQ_RESERVED_NAMES
_NUM_UNARY_OPS = {"+", "-"}
_NUM_BINARY_OPS = {"**", "*", "/", "%", "+", "-", "<<", ">>", "&", "^", "|"}
_NUM_COMPARISON_OPS = {"<", ">", "<=", ">=", "==", "!="}
_COND_UNARY_ALIASES = {"not": "!"}
_COND_UNARY_OPS = {"!"}
_COND_BINARY_ALIASES = {
"and": "&&",
"or": "||",
"implies": "=>",
}
_COND_BINARY_OPS = {"==", "!=", "iff", "&&", "xor", "||", "=>"}
_MATH_CONSTANTS = {"pi", "E", "tau"}
_UFUNC_NAMES = {
"sin",
"cos",
"tan",
"asin",
"acos",
"atan",
"sinh",
"cosh",
"tanh",
"asinh",
"acosh",
"atanh",
"sqrt",
"cbrt",
"exp",
"log",
"log10",
"log2",
"log1p",
"abs",
"ceil",
"floor",
"round",
"trunc",
"sign",
}
[docs]
class BmcExpr(ABC):
"""Base class for every BMC query expression node.
Concrete subclasses provide a stable canonical form for tests, parser
handoff, and later binder diagnostics. The canonical form contains only
plain dictionaries, lists, strings, booleans, integers, floats, and
``None`` so it can be serialized or compared without importing grammar
classes.
:cvar _node_name: Canonical node tag emitted by
:meth:`BmcExpr.to_canonical`.
:type _node_name: str
Example::
>>> from pyfcstm.bmc.ast import IntLiteral
>>> IntLiteral("7").to_canonical()["node"]
'int_literal'
"""
_node_name: ClassVar[str] = "expr"
[docs]
def to_canonical(self) -> _CanonicalDict:
"""Return a language-neutral canonical expression shape.
:return: Canonical dictionary for this node.
:rtype: Dict[str, object]
Example::
>>> from pyfcstm.bmc.ast import BoolLiteral
>>> BoolLiteral("true").to_canonical()["value"]
True
"""
result = {"node": self._node_name}
result.update(self._canonical_payload())
return result
[docs]
def __str__(self) -> str:
"""Return the canonical ``.fbmcq`` DSL spelling for this expression.
:return: Query DSL text that can be parsed back into the same canonical
semantic expression shape. Operator aliases and literal spelling
such as boolean casing may be normalized by this canonical text.
:rtype: str
Example::
>>> from pyfcstm.bmc.ast import IntLiteral
>>> str(IntLiteral("7"))
'7'
"""
return self._to_dsl()
@abstractmethod
def _canonical_payload(self) -> _CanonicalDict:
raise NotImplementedError # pragma: no cover
@abstractmethod
def _to_dsl(self) -> str:
raise NotImplementedError # pragma: no cover
[docs]
class BmcNumExpr(BmcExpr):
"""Base class for numeric BMC expressions.
Numeric expressions follow FCSTM ``num_expression`` shape and represent
integer, float, variable, frame-variable, cycle, and arithmetic operator
values.
Example::
>>> from pyfcstm.bmc.ast import BmcNumExpr, Cycle
>>> isinstance(Cycle(), BmcNumExpr)
True
"""
[docs]
class BmcCondExpr(BmcExpr):
"""Base class for condition BMC expressions.
Condition expressions follow FCSTM ``cond_expression`` shape and represent
boolean literals, comparisons, logical operators, active-state atoms, event
atoms, selected-case atoms, and abstract-call atoms.
Example::
>>> from pyfcstm.bmc.ast import Active, BmcCondExpr
>>> isinstance(Active("Root.A"), BmcCondExpr)
True
"""
def _canonical_expr(expr: BmcExpr) -> _CanonicalDict:
return expr.to_canonical()
def _require_instance(value: object, expected_type: type, field_name: str) -> None:
if not isinstance(value, expected_type):
raise TypeError(f"{field_name} must be {expected_type.__name__}.")
def _validate_choice(value: str, choices: set, field_name: str) -> None:
if not isinstance(value, str) or value not in choices:
raise ValueError(f"Unsupported {field_name}: {value!r}.")
def _require_non_empty_string(value: object, field_name: str) -> None:
if not isinstance(value, str) or not value:
raise ValueError(f"{field_name} must be a non-empty string.")
def _require_non_empty_query_string(value: object, field_name: str) -> None:
if not isinstance(value, str) or not value:
raise InvalidBmcQuery(f"{field_name} must be a non-empty string.")
def _normalize_frame(
frame: _FrameSelector, field_name: str = "frame"
) -> _FrameSelector:
if frame == "current":
return frame
if isinstance(frame, bool) or not isinstance(frame, int):
raise InvalidBmcQuery(
f"{field_name} must be a non-negative integer or 'current'."
)
if frame < 0:
raise InvalidBmcQuery(
f"{field_name} must be a non-negative integer or 'current'."
)
return frame
def _quote_string(value: str) -> str:
return json.dumps(value, ensure_ascii=False)
def _frame_to_dsl(frame: _FrameSelector) -> str:
return "current" if frame == "current" else str(frame)
def _call_args_to_dsl(*args: str) -> str:
return ", ".join(args)
def _optional_frame_call_to_dsl(
name: str, first_arg: str, frame: _FrameSelector
) -> str:
if frame == "current":
return "%s(%s)" % (name, first_arg)
return "%s(%s)" % (name, _call_args_to_dsl(first_arg, _frame_to_dsl(frame)))
def _optional_unit_frame_call_to_dsl(name: str, frame: _FrameSelector) -> str:
if frame == "current":
return "%s()" % name
return "%s(%s)" % (name, _frame_to_dsl(frame))
def _validate_call_arg_string(value: object, field_name: str) -> Optional[str]:
if value is None:
return None
_require_non_empty_query_string(value, field_name)
return value
def _named_arg_to_dsl(name: str, value: str) -> str:
return "%s=%s" % (name, value)
def _grouped(text: str) -> str:
return "(%s)" % text
def _num_operand_to_dsl(expr: BmcNumExpr) -> str:
if isinstance(
expr,
(
IntLiteral,
FloatLiteral,
NameRef,
MathConst,
UFuncCall,
FrameVar,
Cycle,
CallCount,
),
):
return str(expr)
return _grouped(str(expr))
def _cond_operand_to_dsl(expr: BmcCondExpr) -> str:
if isinstance(
expr,
(
BoolLiteral,
NumericComparison,
CondUnaryOp,
Active,
Terminated,
Event,
Case,
Called,
),
):
return str(expr)
return _grouped(str(expr))
def _cond_unary_operand_to_dsl(expr: BmcCondExpr) -> str:
if isinstance(expr, (BoolLiteral, Active, Terminated, Event, Case, Called)):
return str(expr)
return _grouped(str(expr))
[docs]
@dataclass(frozen=True)
class IntLiteral(BmcNumExpr):
"""Integer literal preserving raw token, numeric value, and literal kind.
:param raw: Raw integer token text such as ``"42"`` or ``"0x2A"``.
:type raw: str
:param kind: Literal kind, either ``"decimal"`` or ``"hex"``. When omitted,
the kind is inferred from ``raw``. Explicit kind values must match the
raw spelling.
:type kind: str, optional
Example::
>>> IntLiteral("0x2A").to_canonical()["kind"]
'hex'
"""
_node_name: ClassVar[str] = "int_literal"
raw: str
kind: Optional[str] = None
def __post_init__(self) -> None:
_require_non_empty_string(self.raw, "raw")
if self.raw.startswith("0X"):
raise ValueError(
"Invalid FCSTM hexadecimal integer literal: uppercase '0X' "
f"prefix is not supported; use lowercase '0x': {self.raw!r}."
)
inferred_kind = "hex" if self.raw.startswith("0x") else "decimal"
if self.kind is None:
kind = inferred_kind
else:
_validate_choice(self.kind, {"decimal", "hex"}, "integer literal kind")
if self.kind != inferred_kind:
raise ValueError(
"Integer literal kind does not match raw spelling: "
f"{self.raw!r} is {inferred_kind}, got {self.kind!r}."
)
kind = self.kind
if kind == "hex":
if not _HEX_INT_RE.fullmatch(self.raw):
raise ValueError(
f"Invalid FCSTM hexadecimal integer literal: {self.raw!r}."
)
elif not _DECIMAL_INT_RE.fullmatch(self.raw):
raise ValueError(f"Invalid FCSTM decimal integer literal: {self.raw!r}.")
object.__setattr__(self, "kind", kind)
@property
def value(self) -> int:
"""Return the integer value represented by ``raw``.
:return: Parsed integer value.
:rtype: int
Example::
>>> IntLiteral("0x10").value
16
"""
return int(self.raw, 16 if self.kind == "hex" else 10)
def _canonical_payload(self) -> _CanonicalDict:
return {"kind": self.kind, "raw": self.raw, "value": self.value}
def _to_dsl(self) -> str:
return self.raw
[docs]
@dataclass(frozen=True)
class CallStepPoint:
"""Point used by ``called`` and ``call_count`` step selectors.
A point is either absolute, such as ``3``, or relative to the predicate
anchor, such as ``+2`` or ``-1``. Relative zero canonicalizes to ``+0`` so
``+0`` and ``-0`` compare equal after parsing.
:param kind: ``"absolute"`` or ``"relative"``.
:type kind: str
:param value: Non-negative absolute index or signed relative offset.
:type value: int
Example::
>>> str(CallStepPoint.relative(0))
'+0'
>>> CallStepPoint.absolute(3).to_canonical()["value"]
3
"""
kind: _CallStepPointKind
value: int
def __post_init__(self) -> None:
if self.kind not in {"absolute", "relative"}:
raise InvalidBmcQuery("call step point kind must be absolute or relative.")
if isinstance(self.value, bool) or not isinstance(self.value, int):
raise InvalidBmcQuery("call step point value must be an integer.")
if self.kind == "absolute" and self.value < 0:
raise InvalidBmcQuery("absolute call step point must be non-negative.")
[docs]
@classmethod
def absolute(cls, value: int) -> "CallStepPoint":
"""Return an absolute step point.
:param value: Non-negative step index.
:type value: int
:return: Absolute step point.
:rtype: CallStepPoint
Example::
>>> str(CallStepPoint.absolute(2))
'2'
"""
return cls("absolute", value)
[docs]
@classmethod
def relative(cls, value: int) -> "CallStepPoint":
"""Return a relative step point.
:param value: Signed offset from the predicate anchor.
:type value: int
:return: Relative step point.
:rtype: CallStepPoint
Example::
>>> str(CallStepPoint.relative(-3))
'-3'
"""
return cls("relative", value)
[docs]
def to_canonical(self) -> _CanonicalDict:
"""Return a JSON-stable point summary.
:return: Canonical call step point.
:rtype: Dict[str, object]
Example::
>>> CallStepPoint.relative(1).to_canonical()["kind"]
'relative'
"""
return {"node": "call_step_point", "kind": self.kind, "value": self.value}
[docs]
def __str__(self) -> str:
"""Return canonical ``.fbmcq`` text for this point.
:return: Point DSL text.
:rtype: str
Example::
>>> str(CallStepPoint.relative(0))
'+0'
"""
if self.kind == "absolute":
return str(self.value)
return ("%+d" % self.value) if self.value != 0 else "+0"
[docs]
@dataclass(frozen=True)
class CallStepSelector:
"""Step set selector used by abstract-call query predicates.
:param kind: ``"omitted"``, ``"all"``, ``"point"``, or ``"range"``.
:type kind: str
:param start: Point or ``None`` for omitted/current range starts.
:type start: CallStepPoint, optional
:param end: Point or ``None`` for omitted/current range ends.
:type end: CallStepPoint, optional
Example::
>>> str(CallStepSelector.all())
'*'
>>> str(CallStepSelector.range(CallStepPoint.relative(-2), CallStepPoint.relative(0)))
'-2..+0'
"""
kind: _CallStepSelectorKind = "omitted"
start: Optional[CallStepPoint] = None
end: Optional[CallStepPoint] = None
def __post_init__(self) -> None:
if self.kind not in {"omitted", "all", "point", "range"}:
raise InvalidBmcQuery("unsupported call step selector kind.")
if self.start is not None and not isinstance(self.start, CallStepPoint):
raise InvalidBmcQuery("call step selector start must be CallStepPoint.")
if self.end is not None and not isinstance(self.end, CallStepPoint):
raise InvalidBmcQuery("call step selector end must be CallStepPoint.")
if self.kind in {"omitted", "all"} and (
self.start is not None or self.end is not None
):
raise InvalidBmcQuery(
"%s call step selector cannot have endpoints." % self.kind
)
if self.kind == "point":
if self.start is None or self.end is not None:
raise InvalidBmcQuery(
"point call step selector needs exactly one point."
)
if self.kind == "range":
if self.start is None and self.end is None:
raise InvalidBmcQuery("call step range '..' is invalid.")
if self.start is not None and self.end is not None:
start = self.start
end = self.end
if start.kind == end.kind and start.value > end.value:
raise InvalidBmcQuery("call step range start must not exceed end.")
if self.start is not None and self.end is None:
start = self.start
if start.kind == "relative" and start.value > 0:
raise InvalidBmcQuery(
"open-ended future call step range is invalid."
)
if self.start is None and self.end is not None:
end = self.end
if end.kind == "relative" and end.value < 0:
raise InvalidBmcQuery("open-start past call step range is invalid.")
[docs]
@classmethod
def omitted(cls) -> "CallStepSelector":
"""Return the implicit current-step selector.
:return: Omitted selector.
:rtype: CallStepSelector
Example::
>>> CallStepSelector.omitted().to_canonical()["kind"]
'omitted'
"""
return cls("omitted")
[docs]
@classmethod
def all(cls) -> "CallStepSelector":
"""Return the all-steps selector.
:return: All-steps selector.
:rtype: CallStepSelector
Example::
>>> str(CallStepSelector.all())
'*'
"""
return cls("all")
[docs]
@classmethod
def point(cls, point: CallStepPoint) -> "CallStepSelector":
"""Return a point selector.
:param point: Selected step point.
:type point: CallStepPoint
:return: Point selector.
:rtype: CallStepSelector
Example::
>>> str(CallStepSelector.point(CallStepPoint.absolute(3)))
'3'
"""
return cls("point", start=point)
[docs]
@classmethod
def range(
cls, start: Optional[CallStepPoint], end: Optional[CallStepPoint]
) -> "CallStepSelector":
"""Return an inclusive range or relative window selector.
:param start: Start point, or ``None`` for the current anchor.
:type start: CallStepPoint, optional
:param end: End point, or ``None`` for the current anchor.
:type end: CallStepPoint, optional
:return: Range selector.
:rtype: CallStepSelector
Example::
>>> str(CallStepSelector.range(None, CallStepPoint.relative(2)))
'..+2'
"""
return cls("range", start=start, end=end)
[docs]
def to_canonical(self) -> _CanonicalDict:
"""Return a JSON-stable selector summary.
:return: Canonical call step selector.
:rtype: Dict[str, object]
Example::
>>> CallStepSelector.all().to_canonical()["kind"]
'all'
"""
return {
"node": "call_step_selector",
"kind": self.kind,
"start": self.start.to_canonical() if self.start is not None else None,
"end": self.end.to_canonical() if self.end is not None else None,
}
[docs]
def __str__(self) -> str:
"""Return canonical selector DSL text.
:return: Selector text.
:rtype: str
Example::
>>> str(CallStepSelector.range(CallStepPoint.relative(-1), None))
'-1..'
"""
if self.kind == "omitted":
return ""
if self.kind == "all":
return "*"
if self.kind == "point":
return str(self.start)
return "%s..%s" % (
"" if self.start is None else str(self.start),
"" if self.end is None else str(self.end),
)
[docs]
@dataclass(frozen=True)
class CallFilter:
"""Shared argument model for ``called`` and ``call_count`` predicates.
Omitted filter fields mean ``true`` for that dimension. ``where`` is a
filter over the matched call-time snapshot, not a global assertion over all
calls. :func:`str` returns the canonical argument fragment without the
surrounding ``called`` or ``call_count`` function name.
:param action: Resolved abstract action path filter, defaults to ``None``.
:type action: str, optional
:param step: Step selector, defaults to omitted/current.
:type step: CallStepSelector, optional
:param stage: Lifecycle stage filter such as ``"during"``.
:type stage: str, optional
:param role: Runtime role filter such as ``"aspect_during_before"``.
:type role: str, optional
:param state: Runtime public state path filter.
:type state: str, optional
:param active_leaf: Runtime active leaf path filter.
:type active_leaf: str, optional
:param named_ref: Named-ref callsite path filter, defaults to ``None``.
:type named_ref: str, optional
:param named_ref_is_null: Whether ``named_ref=null`` was requested.
:type named_ref_is_null: bool, optional
:param where: Snapshot predicate filter, defaults to ``None``.
:type where: BmcCondExpr, optional
Example::
>>> str(CallFilter(action="Root.Hook"))
'"Root.Hook"'
"""
action: Optional[str] = None
step: Optional[CallStepSelector] = None
stage: Optional[str] = None
role: Optional[str] = None
state: Optional[str] = None
active_leaf: Optional[str] = None
named_ref: Optional[str] = None
named_ref_is_null: bool = False
where: Optional[BmcCondExpr] = None
def __post_init__(self) -> None:
for field_name in (
"action",
"stage",
"role",
"state",
"active_leaf",
"named_ref",
):
object.__setattr__(
self,
field_name,
_validate_call_arg_string(getattr(self, field_name), field_name),
)
if self.step is not None and not isinstance(self.step, CallStepSelector):
raise InvalidBmcQuery("step must be CallStepSelector.")
if self.named_ref_is_null and self.named_ref is not None:
raise InvalidBmcQuery("named_ref cannot be both a string and null.")
if not isinstance(self.named_ref_is_null, bool):
raise InvalidBmcQuery("named_ref_is_null must be bool.")
if self.where is not None and not isinstance(self.where, BmcCondExpr):
raise InvalidBmcQuery("where must be a BMC condition expression.")
@property
def effective_step(self) -> CallStepSelector:
"""Return explicit or omitted step selector.
:return: Step selector.
:rtype: CallStepSelector
Example::
>>> CallFilter().effective_step.kind
'omitted'
"""
return self.step if self.step is not None else CallStepSelector.omitted()
[docs]
def to_canonical(self) -> _CanonicalDict:
"""Return a JSON-stable call-filter shape.
:return: Canonical call filter.
:rtype: Dict[str, object]
Example::
>>> CallFilter(action="A").to_canonical()["action"]
'A'
"""
return {
"node": "call_filter",
"action": self.action,
"step": self.effective_step.to_canonical(),
"stage": self.stage,
"role": self.role,
"state": self.state,
"active_leaf": self.active_leaf,
"named_ref": self.named_ref,
"named_ref_is_null": self.named_ref_is_null,
"where": self.where.to_canonical() if self.where is not None else None,
}
def _args_to_dsl(self) -> Tuple[str, ...]:
args = []
if self.action is not None:
args.append(_quote_string(self.action))
if self.step is not None:
args.append(str(self.step))
if self.stage is not None:
args.append(_named_arg_to_dsl("stage", _quote_string(self.stage)))
if self.role is not None:
args.append(_named_arg_to_dsl("role", _quote_string(self.role)))
if self.state is not None:
args.append(_named_arg_to_dsl("state", _quote_string(self.state)))
if self.active_leaf is not None:
args.append(
_named_arg_to_dsl("active_leaf", _quote_string(self.active_leaf))
)
if self.named_ref_is_null:
args.append(_named_arg_to_dsl("named_ref", "null"))
elif self.named_ref is not None:
args.append(_named_arg_to_dsl("named_ref", _quote_string(self.named_ref)))
if self.where is not None:
args.append("where %s" % self.where)
return tuple(args)
[docs]
def __str__(self) -> str:
"""Return the comma-separated canonical argument list.
:return: Argument DSL text without surrounding function name.
:rtype: str
Example::
>>> str(CallFilter(action="A", step=CallStepSelector.all()))
'"A", *'
"""
return _call_args_to_dsl(*self._args_to_dsl())
[docs]
@dataclass(frozen=True)
class FloatLiteral(BmcNumExpr):
"""Floating-point literal preserving the raw token text.
:param raw: Raw floating-point token text.
:type raw: str
Example::
>>> FloatLiteral("1e2").to_canonical()["value"]
100.0
"""
_node_name: ClassVar[str] = "float_literal"
raw: str
def __post_init__(self) -> None:
_require_non_empty_string(self.raw, "raw")
if not _FLOAT_RE.fullmatch(self.raw):
raise ValueError(f"Invalid FCSTM floating-point literal: {self.raw!r}.")
if not math.isfinite(float(self.raw)):
raise ValueError(
f"FCSTM floating-point literal must be finite: {self.raw!r}."
)
@property
def value(self) -> float:
"""Return the floating-point value represented by ``raw``.
:return: Parsed float value.
:rtype: float
Example::
>>> FloatLiteral("3.5").value
3.5
"""
return float(self.raw)
def _canonical_payload(self) -> _CanonicalDict:
return {"kind": "float", "raw": self.raw, "value": self.value}
def _to_dsl(self) -> str:
return self.raw
[docs]
@dataclass(frozen=True)
class BoolLiteral(BmcCondExpr):
"""Boolean literal preserving raw spelling and normalized value.
Canonical DSL output uses lowercase ``true`` / ``false`` even when ``raw``
records title-case or uppercase parser input. The exact input spelling
remains available through :meth:`to_canonical`.
:param raw: Raw boolean token text such as ``"true"`` or ``"FALSE"``.
:type raw: str
Example::
>>> BoolLiteral("FALSE").to_canonical()["value"]
False
"""
_node_name: ClassVar[str] = "bool_literal"
raw: str
def __post_init__(self) -> None:
_require_non_empty_string(self.raw, "raw")
if self.raw not in {"true", "True", "TRUE", "false", "False", "FALSE"}:
raise ValueError(f"Unsupported FCSTM boolean literal: {self.raw!r}.")
@property
def value(self) -> bool:
"""Return the boolean value represented by ``raw``.
:return: Parsed boolean value.
:rtype: bool
Example::
>>> BoolLiteral("True").value
True
"""
return self.raw.lower() == "true"
def _canonical_payload(self) -> _CanonicalDict:
return {"kind": "bool", "raw": self.raw, "value": self.value}
def _to_dsl(self) -> str:
return "true" if self.value else "false"
[docs]
@dataclass(frozen=True)
class NameRef(BmcNumExpr):
"""Bare FCSTM variable reference used as a numeric expression.
Names that are reserved by FCSTM or FBMCQ syntax are rejected in bare form.
A model variable whose name collides with a FBMCQ query atom, such as
``"cycle"`` or ``"event"``, should be represented through
:class:`FrameVar` and rendered as ``var("...")`` instead.
:param name: Variable name from the query expression.
:type name: str
Example::
>>> NameRef("counter").to_canonical()
{'node': 'name', 'name': 'counter'}
"""
_node_name: ClassVar[str] = "name"
name: str
def __post_init__(self) -> None:
_require_non_empty_string(self.name, "name")
if not _ID_RE.fullmatch(self.name):
raise ValueError(f"Invalid FCSTM identifier: {self.name!r}.")
if self.name in _BARE_NAME_RESERVED or self.name in _UFUNC_NAMES:
raise ValueError(f"Reserved bare expression name: {self.name!r}.")
def _canonical_payload(self) -> _CanonicalDict:
return {"name": self.name}
def _to_dsl(self) -> str:
return self.name
[docs]
@dataclass(frozen=True)
class MathConst(BmcNumExpr):
"""FCSTM mathematical constant expression.
:param name: Constant name, one of ``"pi"``, ``"E"``, or ``"tau"``.
:type name: str
Example::
>>> MathConst("pi").to_canonical()["name"]
'pi'
"""
_node_name: ClassVar[str] = "math_const"
name: str
def __post_init__(self) -> None:
_validate_choice(self.name, _MATH_CONSTANTS, "math constant")
def _canonical_payload(self) -> _CanonicalDict:
return {"name": self.name}
def _to_dsl(self) -> str:
return self.name
[docs]
@dataclass(frozen=True)
class NumUnaryOp(BmcNumExpr):
"""Numeric unary operator expression.
:param op: Unary operator, either ``"+"`` or ``"-"``.
:type op: str
:param operand: Numeric operand.
:type operand: BmcNumExpr
Example::
>>> NumUnaryOp("-", NameRef("x")).to_canonical()["op"]
'-'
"""
_node_name: ClassVar[str] = "num_unary"
op: str
operand: BmcNumExpr
def __post_init__(self) -> None:
_validate_choice(self.op, _NUM_UNARY_OPS, "numeric unary operator")
_require_instance(self.operand, BmcNumExpr, "operand")
def _canonical_payload(self) -> _CanonicalDict:
return {"op": self.op, "operand": _canonical_expr(self.operand)}
def _to_dsl(self) -> str:
return "%s%s" % (self.op, _num_operand_to_dsl(self.operand))
[docs]
@dataclass(frozen=True)
class NumBinaryOp(BmcNumExpr):
"""Numeric binary operator expression.
:param left: Left numeric operand.
:type left: BmcNumExpr
:param op: Numeric operator following FCSTM grammar spelling.
:type op: str
:param right: Right numeric operand.
:type right: BmcNumExpr
Example::
>>> NumBinaryOp(NameRef("x"), "+", IntLiteral("1")).to_canonical()["op"]
'+'
"""
_node_name: ClassVar[str] = "num_binary"
left: BmcNumExpr
op: str
right: BmcNumExpr
def __post_init__(self) -> None:
_require_instance(self.left, BmcNumExpr, "left")
_require_instance(self.right, BmcNumExpr, "right")
_validate_choice(self.op, _NUM_BINARY_OPS, "numeric binary operator")
def _canonical_payload(self) -> _CanonicalDict:
return {
"op": self.op,
"left": _canonical_expr(self.left),
"right": _canonical_expr(self.right),
}
def _to_dsl(self) -> str:
return "%s %s %s" % (
_num_operand_to_dsl(self.left),
self.op,
_num_operand_to_dsl(self.right),
)
[docs]
@dataclass(frozen=True)
class NumConditionalOp(BmcNumExpr):
"""Numeric conditional expression with a condition selector.
:param condition: Condition deciding which branch is selected.
:type condition: BmcCondExpr
:param if_true: Numeric expression used when ``condition`` is true.
:type if_true: BmcNumExpr
:param if_false: Numeric expression used when ``condition`` is false.
:type if_false: BmcNumExpr
Example::
>>> NumConditionalOp(BoolLiteral("true"), IntLiteral("1"), IntLiteral("0")).to_canonical()["node"]
'num_conditional'
"""
_node_name: ClassVar[str] = "num_conditional"
condition: BmcCondExpr
if_true: BmcNumExpr
if_false: BmcNumExpr
def __post_init__(self) -> None:
_require_instance(self.condition, BmcCondExpr, "condition")
_require_instance(self.if_true, BmcNumExpr, "if_true")
_require_instance(self.if_false, BmcNumExpr, "if_false")
def _canonical_payload(self) -> _CanonicalDict:
return {
"condition": _canonical_expr(self.condition),
"if_true": _canonical_expr(self.if_true),
"if_false": _canonical_expr(self.if_false),
}
def _to_dsl(self) -> str:
return "(%s) ? %s : %s" % (
self.condition,
_num_operand_to_dsl(self.if_true),
_num_operand_to_dsl(self.if_false),
)
[docs]
@dataclass(frozen=True)
class UFuncCall(BmcNumExpr):
"""FCSTM unary math function call.
:param func: Function name from FCSTM ``UFUNC_NAME``.
:type func: str
:param operand: Numeric function argument.
:type operand: BmcNumExpr
Example::
>>> UFuncCall("sqrt", NameRef("x")).to_canonical()["func"]
'sqrt'
"""
_node_name: ClassVar[str] = "ufunc"
func: str
operand: BmcNumExpr
def __post_init__(self) -> None:
_validate_choice(self.func, _UFUNC_NAMES, "ufunc")
_require_instance(self.operand, BmcNumExpr, "operand")
def _canonical_payload(self) -> _CanonicalDict:
return {"func": self.func, "operand": _canonical_expr(self.operand)}
def _to_dsl(self) -> str:
return "%s(%s)" % (self.func, self.operand)
[docs]
@dataclass(frozen=True)
class CondUnaryOp(BmcCondExpr):
"""Condition unary operator expression.
:param op: Unary condition operator, ``"!"`` or alias ``"not"``.
:type op: str
:param operand: Condition operand.
:type operand: BmcCondExpr
Example::
>>> CondUnaryOp("not", BoolLiteral("true")).to_canonical()["op"]
'!'
"""
_node_name: ClassVar[str] = "cond_unary"
op: str
operand: BmcCondExpr
def __post_init__(self) -> None:
op = _COND_UNARY_ALIASES.get(self.op, self.op)
_validate_choice(op, _COND_UNARY_OPS, "condition unary operator")
_require_instance(self.operand, BmcCondExpr, "operand")
object.__setattr__(self, "op", op)
def _canonical_payload(self) -> _CanonicalDict:
return {"op": self.op, "operand": _canonical_expr(self.operand)}
def _to_dsl(self) -> str:
return "%s%s" % (self.op, _cond_unary_operand_to_dsl(self.operand))
[docs]
@dataclass(frozen=True)
class NumericComparison(BmcCondExpr):
"""Comparison between two numeric expressions.
:param left: Left numeric operand.
:type left: BmcNumExpr
:param op: Comparison operator.
:type op: str
:param right: Right numeric operand.
:type right: BmcNumExpr
Example::
>>> NumericComparison(NameRef("x"), "<", IntLiteral("2")).to_canonical()["op"]
'<'
"""
_node_name: ClassVar[str] = "numeric_comparison"
left: BmcNumExpr
op: str
right: BmcNumExpr
def __post_init__(self) -> None:
_require_instance(self.left, BmcNumExpr, "left")
_require_instance(self.right, BmcNumExpr, "right")
_validate_choice(self.op, _NUM_COMPARISON_OPS, "numeric comparison operator")
def _canonical_payload(self) -> _CanonicalDict:
return {
"op": self.op,
"left": _canonical_expr(self.left),
"right": _canonical_expr(self.right),
}
def _to_dsl(self) -> str:
return "%s %s %s" % (
_num_operand_to_dsl(self.left),
self.op,
_num_operand_to_dsl(self.right),
)
[docs]
@dataclass(frozen=True)
class CondBinaryOp(BmcCondExpr):
"""Condition binary operator expression.
:param left: Left condition operand.
:type left: BmcCondExpr
:param op: Condition operator or FCSTM alias.
:type op: str
:param right: Right condition operand.
:type right: BmcCondExpr
Example::
>>> CondBinaryOp(BoolLiteral("true"), "and", BoolLiteral("false")).to_canonical()["op"]
'&&'
"""
_node_name: ClassVar[str] = "cond_binary"
left: BmcCondExpr
op: str
right: BmcCondExpr
def __post_init__(self) -> None:
op = _COND_BINARY_ALIASES.get(self.op, self.op)
_require_instance(self.left, BmcCondExpr, "left")
_require_instance(self.right, BmcCondExpr, "right")
_validate_choice(op, _COND_BINARY_OPS, "condition binary operator")
object.__setattr__(self, "op", op)
def _canonical_payload(self) -> _CanonicalDict:
return {
"op": self.op,
"left": _canonical_expr(self.left),
"right": _canonical_expr(self.right),
}
def _to_dsl(self) -> str:
return "%s %s %s" % (
_cond_operand_to_dsl(self.left),
self.op,
_cond_operand_to_dsl(self.right),
)
[docs]
@dataclass(frozen=True)
class CondConditionalOp(BmcCondExpr):
"""Condition conditional expression.
:param condition: Condition deciding which branch is selected.
:type condition: BmcCondExpr
:param if_true: Condition expression used when ``condition`` is true.
:type if_true: BmcCondExpr
:param if_false: Condition expression used when ``condition`` is false.
:type if_false: BmcCondExpr
Example::
>>> CondConditionalOp(BoolLiteral("true"), BoolLiteral("true"), BoolLiteral("false")).to_canonical()["node"]
'cond_conditional'
"""
_node_name: ClassVar[str] = "cond_conditional"
condition: BmcCondExpr
if_true: BmcCondExpr
if_false: BmcCondExpr
def __post_init__(self) -> None:
_require_instance(self.condition, BmcCondExpr, "condition")
_require_instance(self.if_true, BmcCondExpr, "if_true")
_require_instance(self.if_false, BmcCondExpr, "if_false")
def _canonical_payload(self) -> _CanonicalDict:
return {
"condition": _canonical_expr(self.condition),
"if_true": _canonical_expr(self.if_true),
"if_false": _canonical_expr(self.if_false),
}
def _to_dsl(self) -> str:
return "(%s) ? %s : %s" % (
self.condition,
_cond_operand_to_dsl(self.if_true),
_cond_operand_to_dsl(self.if_false),
)
[docs]
@dataclass(frozen=True)
class FrameVar(BmcNumExpr):
"""Numeric reference produced by the query-level ``var("...")`` atom.
The query AST is frame-relative rather than solver-frame-indexed. Later
binder and lowering phases decide which concrete frame a ``var("x")``
expression reads from. The spelling field distinguishes this explicit
query atom from a bare :class:`NameRef` that still follows FCSTM ``ID``
lexical rules. The current data model accepts only the explicit
``var("...")`` spelling family; the field is preserved in the canonical
form so parser tests can assert that bare names and frame-variable calls do
not collapse together.
:param name: Persistent variable name carried by ``var("...")``.
:type name: str
:param spelling: Query spelling family, defaults to ``"var_call"``.
:type spelling: str, optional
Example::
>>> FrameVar("x").to_canonical()["spelling"]
'var_call'
"""
_node_name: ClassVar[str] = "frame_var"
name: str
spelling: str = "var_call"
def __post_init__(self) -> None:
_require_non_empty_query_string(self.name, "name")
if not isinstance(self.spelling, str) or self.spelling != "var_call":
raise InvalidBmcQuery(
f"Unsupported frame variable spelling: {self.spelling!r}."
)
def _canonical_payload(self) -> _CanonicalDict:
return {"name": self.name, "spelling": self.spelling}
def _to_dsl(self) -> str:
return "var(%s)" % _quote_string(self.name)
[docs]
@dataclass(frozen=True)
class Cycle(BmcNumExpr):
"""Built-in numeric cycle expression for query predicates.
``cycle`` is a reserved bare numeric atom, not a function call. This keeps
it close to FCSTM mathematical constants such as ``pi`` while BMC predicates
that require quoted model paths keep function-call spellings such as
``active("Root.A")`` and ``event("Root.E", current)``.
Example::
>>> Cycle().to_canonical()
{'node': 'cycle'}
"""
_node_name: ClassVar[str] = "cycle"
def _canonical_payload(self) -> _CanonicalDict:
return {}
def _to_dsl(self) -> str:
return "cycle"
[docs]
@dataclass(frozen=True)
class Active(BmcCondExpr):
"""Boolean atom stating that a state is active at a frame.
:param state_path: Fully qualified or query-local state path string.
:type state_path: str
:param frame: Frame index or ``"current"``, defaults to ``"current"``.
:type frame: int or str, optional
Example::
>>> Active("Root.Idle").to_canonical()["frame"]
'current'
"""
_node_name: ClassVar[str] = "active"
state_path: str
frame: _FrameSelector = "current"
def __post_init__(self) -> None:
_require_non_empty_query_string(self.state_path, "state_path")
object.__setattr__(self, "frame", _normalize_frame(self.frame))
def _canonical_payload(self) -> _CanonicalDict:
return {"state_path": self.state_path, "frame": self.frame}
def _to_dsl(self) -> str:
return _optional_frame_call_to_dsl(
"active", _quote_string(self.state_path), self.frame
)
[docs]
@dataclass(frozen=True)
class Terminated(BmcCondExpr):
"""Boolean atom stating that execution is terminated at a frame.
:param frame: Frame index or ``"current"``, defaults to ``"current"``.
:type frame: int or str, optional
Example::
>>> Terminated().to_canonical()["node"]
'terminated'
"""
_node_name: ClassVar[str] = "terminated"
frame: _FrameSelector = "current"
def __post_init__(self) -> None:
object.__setattr__(self, "frame", _normalize_frame(self.frame))
def _canonical_payload(self) -> _CanonicalDict:
return {"frame": self.frame}
def _to_dsl(self) -> str:
return _optional_unit_frame_call_to_dsl("terminated", self.frame)
[docs]
@dataclass(frozen=True)
class Event(BmcCondExpr):
"""Boolean atom stating that an event is selected for a query cycle.
Event atoms always render their selector argument explicitly, even for the
default ``"current"`` selector. The explicit spelling keeps event-cycle
selection separate from the optional frame shorthand used by state and case
atoms.
:param event_path: Fully qualified or query-local event path string.
:type event_path: str
:param selector: Concrete cycle index or ``"current"``, defaults to
``"current"``.
:type selector: int or str, optional
Example::
>>> str(Event("Root.Idle.Start"))
'event("Root.Idle.Start", current)'
>>> Event("Root.Idle.Start", selector=0).to_canonical()["event_path"]
'Root.Idle.Start'
"""
_node_name: ClassVar[str] = "event"
event_path: str
selector: _FrameSelector = "current"
def __post_init__(self) -> None:
_require_non_empty_query_string(self.event_path, "event_path")
object.__setattr__(
self, "selector", _normalize_frame(self.selector, "selector")
)
def _canonical_payload(self) -> _CanonicalDict:
return {"event_path": self.event_path, "selector": self.selector}
def _to_dsl(self) -> str:
return "event(%s)" % _call_args_to_dsl(
_quote_string(self.event_path), _frame_to_dsl(self.selector)
)
[docs]
@dataclass(frozen=True)
class Case(BmcCondExpr):
"""Boolean atom stating that a macro-step case is selected at a frame.
:param label: Canonical macro-step case label.
:type label: str
:param frame: Frame index or ``"current"``, defaults to ``"current"``.
:type frame: int or str, optional
Example::
>>> Case("Root.A::fallback::Root.A::0", frame=1).to_canonical()["frame"]
1
"""
_node_name: ClassVar[str] = "case"
label: str
frame: _FrameSelector = "current"
def __post_init__(self) -> None:
_require_non_empty_query_string(self.label, "label")
object.__setattr__(self, "frame", _normalize_frame(self.frame))
def _canonical_payload(self) -> _CanonicalDict:
return {"label": self.label, "frame": self.frame}
def _to_dsl(self) -> str:
return _optional_frame_call_to_dsl(
"case", _quote_string(self.label), self.frame
)
[docs]
@dataclass(frozen=True)
class CallCount(BmcNumExpr):
"""Numeric expression counting matching abstract-call occurrences.
:param filter: Shared abstract-call filter, defaults to an empty filter.
:type filter: CallFilter, optional
Example::
>>> str(CallCount(CallFilter(action="Root.Hook")))
'call_count("Root.Hook")'
"""
_node_name: ClassVar[str] = "call_count"
filter: CallFilter = CallFilter()
def __post_init__(self) -> None:
if not isinstance(self.filter, CallFilter):
raise InvalidBmcQuery("filter must be CallFilter.")
def _canonical_payload(self) -> _CanonicalDict:
return {"filter": self.filter.to_canonical()}
def _to_dsl(self) -> str:
return "call_count(%s)" % str(self.filter)
[docs]
@dataclass(frozen=True)
class Called(BmcCondExpr):
"""Boolean atom testing whether a matching abstract call exists.
The legacy ``Called("Hook", frame=2)`` constructor remains accepted for
compatibility with earlier query-model tests. New parser output should use
:class:`CallFilter` so ``called()`` and richer named arguments are available.
:param name: Legacy abstract action or hook name, defaults to ``None``.
:type name: str, optional
:param frame: Legacy frame/step selector, defaults to ``"current"``.
:type frame: int or str, optional
:param filter: Shared call filter for the new argument model, defaults to
``None``.
:type filter: CallFilter, optional
Example::
>>> Called("Check", frame=2).to_canonical()["name"]
'Check'
>>> str(Called(filter=CallFilter()))
'called()'
"""
_node_name: ClassVar[str] = "called"
name: Optional[str] = None
frame: _FrameSelector = "current"
filter: Optional[CallFilter] = None
def __post_init__(self) -> None:
if self.name is not None:
_require_non_empty_query_string(self.name, "name")
object.__setattr__(self, "frame", _normalize_frame(self.frame))
if self.filter is not None and not isinstance(self.filter, CallFilter):
raise InvalidBmcQuery("filter must be CallFilter.")
if self.filter is None and self.name is None:
object.__setattr__(self, "filter", CallFilter())
elif self.filter is not None and (
self.name is not None or self.frame != "current"
):
raise InvalidBmcQuery(
"Called accepts either legacy name/frame or a CallFilter, not both."
)
@property
def call_filter(self) -> CallFilter:
"""Return the normalized call filter.
:return: Call filter used by semantic lowering.
:rtype: CallFilter
Example::
>>> Called("Hook", frame=1).call_filter.action
'Hook'
"""
if self.filter is not None:
return self.filter
step = (
None
if self.frame == "current"
else CallStepSelector.point(CallStepPoint.absolute(self.frame))
)
return CallFilter(action=self.name, step=step)
def _canonical_payload(self) -> _CanonicalDict:
if self.filter is None:
return {"name": self.name, "frame": self.frame}
simple_frame = self._legacy_simple_frame()
if simple_frame is not None:
return {"name": self.filter.action, "frame": simple_frame}
return {"filter": self.filter.to_canonical()}
def _to_dsl(self) -> str:
if self.filter is None:
return _optional_frame_call_to_dsl(
"called", _quote_string(self.name or ""), self.frame
)
simple_frame = self._legacy_simple_frame()
if simple_frame is not None:
return _optional_frame_call_to_dsl(
"called", _quote_string(self.filter.action or ""), simple_frame
)
return "called(%s)" % str(self.filter)
def _legacy_simple_frame(self) -> Optional[_FrameSelector]:
if self.filter is None or self.filter.action is None:
return None
if (
any(
item is not None
for item in (
self.filter.stage,
self.filter.role,
self.filter.state,
self.filter.active_leaf,
self.filter.named_ref,
self.filter.where,
)
)
or self.filter.named_ref_is_null
):
return None
selector = self.filter.effective_step
if selector.kind == "omitted":
return "current"
if (
selector.kind == "point"
and selector.start is not None
and selector.start.kind == "absolute"
):
return selector.start.value
return None
__all__ = [
"BmcExpr",
"BmcNumExpr",
"BmcCondExpr",
"IntLiteral",
"FloatLiteral",
"BoolLiteral",
"NameRef",
"MathConst",
"NumUnaryOp",
"NumBinaryOp",
"NumConditionalOp",
"UFuncCall",
"CondUnaryOp",
"NumericComparison",
"CondBinaryOp",
"CondConditionalOp",
"FrameVar",
"Cycle",
"CallStepPoint",
"CallStepSelector",
"CallFilter",
"CallCount",
"Active",
"Terminated",
"Event",
"Case",
"Called",
]