"""Compile BMC query properties into solver objectives.
This module is the property layer above :mod:`pyfcstm.bmc.relation`. It
consumes a :class:`pyfcstm.bmc.relation.BmcCoreFormula`, keeps the core trace
relation unchanged, and adds the query objective for the bound ``check`` clause.
The compiler does not solve the formula, decode witnesses, replay traces, or
connect to :mod:`pyfcstm.verify`; those stages can consume the returned
:class:`BmcPropertyFormula` later.
The module contains:
* :class:`BmcPropertyFormula` - Compiled objective and diagnostic formulas.
* :func:`compile_bmc_property` - Public entry point for lowering a bound query
property against an existing core trace formula.
Example::
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula
>>> from pyfcstm.bmc.properties import compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(model).prepare('check reach <= 1: active("Root");'))
>>> compile_bmc_property(core).kind
'reach'
"""
from __future__ import annotations
from collections.abc import Iterable as IterableABC
from dataclasses import dataclass
from typing import Any, Dict, Iterable, Mapping, Optional, Tuple
import z3
from .ast import (
Active,
BmcCondExpr,
BmcNumExpr,
BoolLiteral,
CallCount,
CallFilter,
CallStepPoint,
CallStepSelector,
Called,
Case,
CondBinaryOp,
CondConditionalOp,
CondUnaryOp,
Cycle,
Event,
FloatLiteral,
FrameVar,
IntLiteral,
MathConst,
NameRef,
NumBinaryOp,
NumConditionalOp,
NumUnaryOp,
NumericComparison,
Terminated,
UFuncCall,
)
from .errors import BmcBuildError, InvalidBmcQuery, UnsupportedBmcQuery
from .query import BmcProperty
from .relation import (
BmcCoreFormula,
_lower_bmc_cond_expr,
)
_CanonicalDict = Dict[str, Any]
_COVERABLE_CASE_KINDS = {"transition", "fallback"}
_KNOWN_CASE_KINDS = {"transition", "fallback", "initial", "absorb", "delta"}
_WITNESS_KINDS = {"reach", "exists_always", "cover"}
_COUNTEREXAMPLE_KINDS = {"forbid", "invariant", "must_reach", "response"}
def _z3_text(expr: z3.ExprRef) -> str:
return expr.sexpr()
def _and(items: Iterable[z3.ExprRef]) -> z3.BoolRef:
values = tuple(items)
if not values:
return z3.BoolVal(True)
if len(values) == 1:
return values[0]
return z3.And(*values)
def _or(items: Iterable[z3.ExprRef]) -> z3.BoolRef:
values = tuple(items)
if not values:
return z3.BoolVal(False)
if len(values) == 1:
return values[0]
return z3.Or(*values)
def _require_core(core: object) -> BmcCoreFormula:
if not isinstance(core, BmcCoreFormula):
raise BmcBuildError("core must be BmcCoreFormula.")
return core
def _require_bool(expr: z3.ExprRef, label: str) -> z3.BoolRef:
if not z3.is_bool(expr): # pragma: no cover - condition lowering is bool-typed.
raise BmcBuildError("%s must lower to a Z3 Boolean expression." % label)
return expr
def _require_arith(expr: z3.ExprRef, label: str) -> z3.ArithRef:
if not z3.is_arith(expr):
raise BmcBuildError("%s must lower to a Z3 arithmetic expression." % label)
return expr
@dataclass(frozen=True)
class _PredicateFormula:
value: z3.BoolRef
definedness: z3.BoolRef
@property
def good(self) -> z3.BoolRef:
return z3.And(self.definedness, self.value)
@property
def bad_true(self) -> z3.BoolRef:
return z3.Or(z3.Not(self.definedness), self.value)
@property
def bad_false(self) -> z3.BoolRef:
return z3.Or(z3.Not(self.definedness), z3.Not(self.value))
def _validate_num_context(expr: BmcNumExpr, context: str, path: str) -> None:
if isinstance(expr, CallCount):
_validate_call_filter_context(expr.filter, context, path + ".filter")
return
if isinstance(expr, Cycle):
if context == "call_where":
raise UnsupportedBmcQuery("%s call where cannot use cycle." % path)
return
if isinstance(
expr,
(
IntLiteral,
FloatLiteral,
NameRef,
MathConst,
FrameVar,
),
):
return
if isinstance(expr, NumUnaryOp):
_validate_num_context(expr.operand, context, path + ".operand")
return
if isinstance(expr, NumBinaryOp):
_validate_num_context(expr.left, context, path + ".left")
_validate_num_context(expr.right, context, path + ".right")
return
if isinstance(expr, NumConditionalOp):
_validate_condition_context(expr.condition, context, path + ".condition")
_validate_num_context(expr.if_true, context, path + ".if_true")
_validate_num_context(expr.if_false, context, path + ".if_false")
return
if isinstance(expr, UFuncCall):
_validate_num_context(expr.operand, context, path + ".operand")
return
raise UnsupportedBmcQuery( # pragma: no cover - public AST numeric set is closed.
"%s contains unsupported numeric expression %s." % (path, type(expr).__name__)
)
def _validate_condition_context(expr: BmcCondExpr, context: str, path: str) -> None:
if isinstance(expr, BoolLiteral):
return
if isinstance(expr, NumericComparison):
_validate_num_context(expr.left, context, path + ".left")
_validate_num_context(expr.right, context, path + ".right")
return
if isinstance(expr, CondUnaryOp):
_validate_condition_context(expr.operand, context, path + ".operand")
return
if isinstance(expr, CondBinaryOp):
_validate_condition_context(expr.left, context, path + ".left")
_validate_condition_context(expr.right, context, path + ".right")
return
if isinstance(expr, CondConditionalOp):
_validate_condition_context(expr.condition, context, path + ".condition")
_validate_condition_context(expr.if_true, context, path + ".if_true")
_validate_condition_context(expr.if_false, context, path + ".if_false")
return
if isinstance(expr, Active):
if context == "call_where":
raise UnsupportedBmcQuery("%s call where cannot use active()." % path)
if expr.frame != "current":
raise UnsupportedBmcQuery(
"%s uses an explicit frame selector; property compiler "
"predicates must use the current frame." % path
)
return
if isinstance(expr, Terminated):
if context == "call_where":
raise UnsupportedBmcQuery("%s call where cannot use terminated()." % path)
if expr.frame != "current":
raise UnsupportedBmcQuery(
"%s uses an explicit frame selector; property compiler "
"predicates must use the current frame." % path
)
return
if isinstance(expr, Event):
if context == "response_trigger" and expr.selector == "current":
return
if context == "response_trigger": # pragma: no cover - binder rejects this.
raise UnsupportedBmcQuery(
"%s may use only event(..., current), not explicit event selectors."
% path
)
raise UnsupportedBmcQuery( # pragma: no cover - binder rejects this.
"%s is frame-local; event atoms are only allowed in response triggers."
% path
)
if isinstance(expr, Case):
raise UnsupportedBmcQuery( # pragma: no cover - binder rejects nested case().
"%s is not a cover predicate; case atoms are only allowed as naked cover predicates."
% path
)
if isinstance(expr, Called):
_validate_call_filter_context(expr.call_filter, context, path + ".filter")
return
raise UnsupportedBmcQuery( # pragma: no cover - public AST condition set is closed.
"%s contains unsupported condition expression %s." % (path, type(expr).__name__)
)
def _lower_predicate(
core: BmcCoreFormula,
expr: BmcCondExpr,
*,
frame_index: int,
step_index: Optional[int] = None,
context: str,
path: str,
) -> _PredicateFormula:
_validate_condition_context(expr, context, path)
lowered = _lower_bmc_cond_expr(
expr,
core.symbols,
frame_index=frame_index,
step_index=step_index,
call_count_lowerer=lambda call_expr, call_frame, call_step: _lower_call_count(
core, call_expr, call_frame, call_step
),
)
value = _require_bool(lowered.expr, path)
definedness = _and(item.constraint for item in lowered.definedness_constraints)
return _PredicateFormula(value=value, definedness=definedness)
def _property_source(core: BmcCoreFormula) -> BmcProperty:
prop = core.context.bound_query.property.source
if not isinstance(prop, BmcProperty): # pragma: no cover - binder owns this shape.
raise BmcBuildError("bound query property source must be BmcProperty.")
return prop
def _polarity(kind: str) -> str:
if kind in _WITNESS_KINDS:
return "witness"
if kind in _COUNTEREXAMPLE_KINDS:
return "counterexample"
raise BmcBuildError( # pragma: no cover - query validation owns property kinds.
"Unsupported property kind: %r." % kind
)
def _validate_call_filter_context(
filter_node: CallFilter, context: str, path: str
) -> None:
if not isinstance(filter_node, CallFilter):
raise UnsupportedBmcQuery("%s must be a call filter." % path)
if context not in {"frame", "response_trigger"}:
raise UnsupportedBmcQuery(
"%s uses an abstract-call predicate outside property context." % path
)
if filter_node.where is not None:
_validate_condition_context(filter_node.where, "call_where", path + ".where")
def _eval_call_step_point(point: CallStepPoint, anchor: int) -> int:
return point.value if point.kind == "absolute" else anchor + point.value
def _effective_call_steps(
selector: CallStepSelector, anchor: int, bound: int
) -> Tuple[int, ...]:
"""Return in-bounds symbolic steps selected around an anchor step.
Omitted selectors mean the current property anchor. ``*`` spans every
executable macro step ``0 <= i < bound``. Range endpoints are interpreted
relative to the property anchor only when an explicit relative point is
present; a missing range endpoint also defaults to the anchor rather than
to the trace boundary. For example, ``..+0`` and ``+0..`` both select only
the current anchor step.
:param selector: Call-step selector AST node.
:type selector: pyfcstm.bmc.ast.CallStepSelector
:param anchor: Current property frame anchor.
:type anchor: int
:param bound: Number of executable macro steps in the query bound.
:type bound: int
:return: Sorted selected step indexes that fall inside ``[0, bound)``.
:rtype: tuple[int, ...]
:raises pyfcstm.bmc.errors.InvalidBmcQuery: If an absolute selector is
outside the query bound.
Example::
>>> selector = CallStepSelector.point(CallStepPoint.relative(-1))
>>> _effective_call_steps(selector, anchor=2, bound=4)
(1,)
"""
valid = set(range(bound))
if selector.kind == "omitted":
raw = {anchor}
elif selector.kind == "all":
raw = valid
elif selector.kind == "point":
if selector.start is None: # pragma: no cover - AST validates this.
raise BmcBuildError("point call selector is missing its point.")
if selector.start.kind == "absolute" and not (
0 <= selector.start.value < bound
):
raise InvalidBmcQuery("absolute call step selector is out of range.")
raw = {_eval_call_step_point(selector.start, anchor)}
else:
start_point = selector.start
end_point = selector.end
start = (
anchor
if start_point is None
else _eval_call_step_point(start_point, anchor)
)
end = anchor if end_point is None else _eval_call_step_point(end_point, anchor)
for point in (start_point, end_point):
if (
point is not None
and point.kind == "absolute"
and not (0 <= point.value < bound)
):
raise InvalidBmcQuery(
"absolute call step range endpoint is out of range."
)
if start > end:
return ()
raw = set(range(start, end + 1))
return tuple(sorted(raw & valid))
@dataclass(frozen=True)
class _CallSnapshotSymbols:
"""Minimal symbol adapter for lowering call-time ``where`` predicates.
:param snapshot: Call-time persistent-variable symbols.
:type snapshot: Mapping[str, z3.ArithRef]
Example::
>>> import z3
>>> symbols = _CallSnapshotSymbols({"x": z3.Int("x")})
>>> symbols.frame_var(0, "x").sort().name()
'Int'
"""
snapshot: Mapping[str, z3.ArithRef]
def frame_var(self, frame_index: int, name: str) -> z3.ArithRef:
"""Return a call-time variable from the snapshot.
``frame_index`` is intentionally ignored: call ``where`` predicates are
evaluated against the captured abstract-call snapshot, not a trace frame.
:param frame_index: Ignored frame index supplied by the shared lowerer.
:type frame_index: int
:param name: Persistent variable name.
:type name: str
:return: Snapshot variable expression.
:rtype: z3.ArithRef
:raises pyfcstm.bmc.errors.InvalidBmcQuery: If the snapshot does not
contain ``name``.
Example::
>>> import z3
>>> _CallSnapshotSymbols({"x": z3.Int("x")}).frame_var(3, "x").decl().name()
'x'
"""
try:
return self.snapshot[name]
except KeyError as err:
# KeyError: forged query/core combinations can reference a variable
# absent from the captured call snapshot even after normal binding.
raise InvalidBmcQuery(
"call where references unknown snapshot variable %r." % name
) from err
def _snapshot_cond_expr(
expr: BmcCondExpr,
snapshot: Mapping[str, z3.ArithRef],
label: str,
step_index: int,
) -> z3.BoolRef:
lowered = _lower_bmc_cond_expr(
expr,
_CallSnapshotSymbols(snapshot),
frame_index=step_index,
step_index=step_index,
)
definedness = _and(item.constraint for item in lowered.definedness_constraints)
return z3.And(_require_bool(lowered.expr, label), definedness)
def _call_match_expr(
relation,
record,
filter_node: CallFilter,
step_index: int,
) -> z3.BoolRef:
terms = [relation.selector]
if filter_node.action is not None:
terms.append(z3.BoolVal(record.action_name == filter_node.action))
if filter_node.stage is not None:
terms.append(z3.BoolVal(record.stage == filter_node.stage))
if filter_node.role is not None:
terms.append(z3.BoolVal(record.role == filter_node.role))
if filter_node.state is not None:
terms.append(z3.BoolVal(record.state_path == filter_node.state))
if filter_node.active_leaf is not None:
terms.append(z3.BoolVal(record.active_leaf_path == filter_node.active_leaf))
if filter_node.named_ref_is_null:
terms.append(z3.BoolVal(record.named_ref is None))
elif filter_node.named_ref is not None:
terms.append(z3.BoolVal(record.named_ref == filter_node.named_ref))
if filter_node.where is not None:
terms.append(
_snapshot_cond_expr(
filter_node.where, record.snapshot, "call where", step_index
)
)
return _and(terms)
def _lower_call_count(
core: BmcCoreFormula,
expr: CallCount,
frame_index: int,
step_index: Optional[int],
) -> z3.ArithRef:
anchor = step_index if step_index is not None else frame_index
selected_steps = _effective_call_steps(
expr.filter.effective_step, anchor, core.context.bound
)
items = []
for selected_step in selected_steps:
for relation in core.steps[selected_step].case_relations:
for record in relation.call_records:
items.append(
z3.If(
_call_match_expr(relation, record, expr.filter, selected_step),
z3.IntVal(1),
z3.IntVal(0),
)
)
if not items:
return z3.IntVal(0)
return z3.Sum(*items)
def _single_predicate(prop: BmcProperty) -> BmcCondExpr:
if (
prop.predicate is None
): # pragma: no cover - query validation owns property shape.
raise BmcBuildError("single-body property has no predicate.")
return prop.predicate
def _frame_predicates(
core: BmcCoreFormula, expr: BmcCondExpr
) -> Tuple[_PredicateFormula, ...]:
return tuple(
_lower_predicate(
core,
expr,
frame_index=frame_index,
context="frame",
path="property.predicate",
)
for frame_index in range(core.context.bound + 1)
)
def _compile_reach(core: BmcCoreFormula, prop: BmcProperty) -> z3.BoolRef:
predicates = _frame_predicates(core, _single_predicate(prop))
return _or(item.good for item in predicates)
def _compile_forbid(core: BmcCoreFormula, prop: BmcProperty) -> z3.BoolRef:
predicates = _frame_predicates(core, _single_predicate(prop))
return _or(item.bad_true for item in predicates)
def _compile_invariant(core: BmcCoreFormula, prop: BmcProperty) -> z3.BoolRef:
predicates = _frame_predicates(core, _single_predicate(prop))
return _or(item.bad_false for item in predicates)
def _compile_must_reach(core: BmcCoreFormula, prop: BmcProperty) -> z3.BoolRef:
predicates = _frame_predicates(core, _single_predicate(prop))
return _and(z3.Not(item.good) for item in predicates)
def _compile_exists_always(core: BmcCoreFormula, prop: BmcProperty) -> z3.BoolRef:
predicates = _frame_predicates(core, _single_predicate(prop))
return _and(item.good for item in predicates)
def _validate_cover_label_schema(label: str) -> str:
parts = label.split("::")
if len(parts) != 4 or not all(parts):
raise InvalidBmcQuery("cover case label schema is invalid: %r." % label)
case_kind = parts[1]
if case_kind not in _KNOWN_CASE_KINDS:
raise InvalidBmcQuery("cover case label kind is invalid: %r." % label)
return case_kind
def _cover_selectors(core: BmcCoreFormula, label: str) -> Tuple[z3.BoolRef, ...]:
label_kind = _validate_cover_label_schema(label)
relations = tuple(
relation
for step in core.steps
for relation in step.case_relations
if relation.case.label == label
)
if not relations:
raise InvalidBmcQuery("cover case label is unknown: %r." % label)
kinds = {relation.case.kind for relation in relations}
if kinds != {
label_kind
}: # pragma: no cover - relation labels are internally canonical.
raise BmcBuildError("cover case label kind disagrees with relation cases.")
if not kinds <= _COVERABLE_CASE_KINDS:
raise InvalidBmcQuery(
"cover case label is not coverable: %r has kind %s."
% (label, sorted(kinds)[0])
)
return tuple(relation.selector for relation in relations)
def _compile_cover(core: BmcCoreFormula, prop: BmcProperty) -> Tuple[z3.BoolRef, str]:
predicate = prop.predicate
if (
not isinstance(predicate, Case) or predicate.frame != "current"
): # pragma: no cover - binder rejects this.
raise InvalidBmcQuery(
'cover properties require a naked case("label") predicate.'
)
selectors = _cover_selectors(core, predicate.label)
return _or(selectors), predicate.label
def _compile_response(
core: BmcCoreFormula, prop: BmcProperty
) -> Tuple[z3.BoolRef, z3.BoolRef, int]:
if (
prop.trigger is None or prop.response is None or prop.within is None
): # pragma: no cover - query validation owns response shape.
raise BmcBuildError(
"response property is missing trigger, response, or window."
)
window = prop.within
if (
isinstance(window, bool) or not isinstance(window, int) or window <= 0
): # pragma: no cover - query validation owns response window shape.
raise InvalidBmcQuery("response window must be a positive integer.")
trigger_terms = tuple(
_lower_predicate(
core,
prop.trigger,
frame_index=step_index,
step_index=step_index,
context="response_trigger",
path="property.trigger",
)
for step_index in range(core.context.bound)
)
response_terms = tuple(
_lower_predicate(
core,
prop.response,
frame_index=frame_index,
context="frame",
path="property.response",
)
for frame_index in range(core.context.bound + 1)
)
trigger_undefined = [z3.Not(item.definedness) for item in trigger_terms]
violations = []
incomplete = []
for step_index, trigger in enumerate(trigger_terms):
triggered = trigger.good
if step_index + window <= core.context.bound:
responses = [
response_terms[frame_index].good
for frame_index in range(step_index + 1, step_index + window + 1)
]
violations.append(z3.And(triggered, z3.Not(_or(responses))))
else:
responses = [
response_terms[frame_index].good
for frame_index in range(step_index + 1, core.context.bound + 1)
]
incomplete.append(z3.And(triggered, z3.Not(_or(responses))))
return _or(tuple(trigger_undefined) + tuple(violations)), _or(incomplete), window
[docs]
def compile_bmc_property(core: BmcCoreFormula) -> BmcPropertyFormula:
"""Compile the prepared query property into a solver objective.
The returned formula keeps :attr:`pyfcstm.bmc.relation.BmcCoreFormula.core`
intact and adds only the objective requested by the bound ``check`` clause.
SAT means a witness for ``reach`` / ``exists_always`` / ``cover`` and a
counterexample for ``forbid`` / ``invariant`` / ``must_reach`` /
``response``.
:param core: Core trace formula to extend with the query objective.
:type core: pyfcstm.bmc.relation.BmcCoreFormula
:return: Compiled property objective bundle.
:rtype: BmcPropertyFormula
:raises pyfcstm.bmc.errors.BmcBuildError: If ``core`` or bound property
metadata is internally inconsistent.
:raises pyfcstm.bmc.errors.InvalidBmcQuery: If a query-level cover label or
property shape is invalid for property compilation.
:raises pyfcstm.bmc.errors.UnsupportedBmcQuery: If the property uses a
parsed but unsupported expression shape or unsupported arithmetic
operation.
Example::
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(model).prepare('check reach <= 1: active("Root");'))
>>> compile_bmc_property(core).solve_formula.sort().name()
'Bool'
"""
checked_core = _require_core(core)
prop = _property_source(checked_core)
kind = prop.kind
case_label = None
response_window = None
incomplete_formula = z3.BoolVal(False)
if kind == "reach":
objective = _compile_reach(checked_core, prop)
elif kind == "forbid":
objective = _compile_forbid(checked_core, prop)
elif kind == "invariant":
objective = _compile_invariant(checked_core, prop)
elif kind == "must_reach":
objective = _compile_must_reach(checked_core, prop)
elif kind == "exists_always":
objective = _compile_exists_always(checked_core, prop)
elif kind == "cover":
objective, case_label = _compile_cover(checked_core, prop)
elif kind == "response":
objective, incomplete_formula, response_window = _compile_response(
checked_core, prop
)
else: # pragma: no cover - query validation owns property kinds.
raise BmcBuildError("Unsupported property kind: %r." % kind)
solve_formula = z3.And(checked_core.core, objective)
incomplete_solve_formula = z3.And(checked_core.core, incomplete_formula)
return BmcPropertyFormula(
core=checked_core,
kind=kind,
polarity=_polarity(kind),
objective_formula=objective,
solve_formula=solve_formula,
incomplete_formula=incomplete_formula,
incomplete_solve_formula=incomplete_solve_formula,
diagnostics=(),
case_label=case_label,
response_window=response_window,
)
__all__ = ["BmcPropertyFormula", "compile_bmc_property"]