pyfcstm.bmc.listener

ANTLR listener that builds parser-independent FCSTM BMC query AST nodes.

The listener mirrors pyfcstm.dsl.listener: it walks generated ANTLR parse contexts bottom-up and stores the constructed object in nodes[ctx]. The module intentionally performs syntax-to-AST construction only. It does not resolve model paths, validate event scope, lower expressions to Z3, or touch the verify registry.

The module contains:

BmcQueryParseListener - Context-to-node listener for .fbmcq query files and expression entry rules.

Example:

>>> from antlr4 import CommonTokenStream, InputStream, ParseTreeWalker
>>> from pyfcstm.bmc.grammar.BmcQueryLexer import BmcQueryLexer
>>> from pyfcstm.bmc.grammar.BmcQueryParser import BmcQueryParser
>>> listener = BmcQueryParseListener()
>>> lexer = BmcQueryLexer(InputStream('check reach <= 1: true;'))
>>> parser = BmcQueryParser(CommonTokenStream(lexer))
>>> tree = parser.query()
>>> ParseTreeWalker().walk(listener, tree)
>>> listener.nodes[tree].property.kind
'reach'

all

pyfcstm.bmc.listener.__all__ = ['BmcQueryParseListener']

Built-in mutable sequence.

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

BmcQueryParseListener

class pyfcstm.bmc.listener.BmcQueryParseListener[source]

Build BMC query model nodes from generated ANTLR parse contexts.

Variables:: nodes (Dict[object, object]) – Mapping from parse context objects to AST/query nodes.

Example:

>>> listener = BmcQueryParseListener()
>>> listener.nodes
{}

__init__() → None[source]

Initialize the listener node mapping.

Returns:: None.
Return type:: None

Example:

>>> BmcQueryParseListener().nodes
{}

exitAssume_clause(ctx: Assume_clauseContext) → None[source]

Bind an assumption wrapper to its concrete assumption node.

Parameters:: ctx (BmcQueryParser.Assume_clauseContext) – Assumption wrapper parse context.
Returns:: None.
Return type:: None

exitAtomExprCond(ctx: AtomExprCondContext) → None[source]: Bind a condition atom expression to its atom node.

exitBinaryExprCond(ctx: BinaryExprCondContext) → None[source]: Build a logical binary condition expression.

exitBinaryExprFromCondCond(ctx: BinaryExprFromCondCondContext) → None[source]: Build a condition equality, inequality, or iff expression.

exitBinaryExprFromNumCond(ctx: BinaryExprFromNumCondContext) → None[source]: Build a numeric comparison condition expression.

exitBinaryExprNum(ctx: BinaryExprNumContext) → None[source]: Build a numeric binary expression.

exitBmc_boolean_atom(ctx: Bmc_boolean_atomContext) → None[source]: Build one BMC-only boolean atom.

exitBmc_cond_expression_entry(ctx: Bmc_cond_expression_entryContext) → None[source]

Bind a condition expression entry to its expression node.

Parameters:: ctx (BmcQueryParser.Bmc_cond_expression_entryContext) – Condition expression entry parse context.
Returns:: None.
Return type:: None

exitBmc_num_expression_entry(ctx: Bmc_num_expression_entryContext) → None[source]

Bind a numeric expression entry to its expression node.

Parameters:: ctx (BmcQueryParser.Bmc_num_expression_entryContext) – Numeric expression entry parse context.
Returns:: None.
Return type:: None

exitBool_cmp_op(ctx: Bool_cmp_opContext) → None[source]

Bind a boolean comparison operator context to its spelling.

Parameters:: ctx (BmcQueryParser.Bool_cmp_opContext) – Boolean comparison operator parse context.
Returns:: None.
Return type:: None

exitBool_literal(ctx: Bool_literalContext) → None[source]: Build a boolean literal expression node.

exitCallCountExprNum(ctx: CallCountExprNumContext) → None[source]: Build a call_count(...) numeric expression.

exitCall_argument(ctx: Call_argumentContext) → None[source]: Build one call argument pair consumed by exitCall_arguments.

exitCall_argument_value(ctx: Call_argument_valueContext) → None[source]

Build one named call-argument value without reserving key names.

Call-filter keys such as action and step intentionally remain normal identifiers at the lexer level so model variables with the same names can still be used in ordinary FCSTM-aligned expressions. The listener validates the key/value pairing after parsing the generic ID = value shape.

exitCall_arguments(ctx: Call_argumentsContext) → None[source]: Build a call filter from positional and named call arguments.

exitCall_step_point(ctx: Call_step_pointContext) → None[source]: Build a call step point.

exitCall_step_selector(ctx: Call_step_selectorContext) → None[source]: Build a call step selector.

exitCardinality_assume(ctx: Cardinality_assumeContext) → None[source]

Build an event-cardinality assumption node.

Parameters:: ctx (BmcQueryParser.Cardinality_assumeContext) – Event-cardinality assumption parse context.
Returns:: None.
Return type:: None

exitCheck_clause(ctx: Check_clauseContext) → None[source]

Build the query property from a check clause.

Parameters:: ctx (BmcQueryParser.Check_clauseContext) – Check clause parse context.
Returns:: None.
Return type:: None

exitConditionalCStyleExprCond(ctx: ConditionalCStyleExprCondContext) → None[source]: Build a condition ternary expression.

exitConditionalCStyleExprNum(ctx: ConditionalCStyleExprNumContext) → None[source]: Build a numeric ternary expression.

exitCycleExprNum(ctx: CycleExprNumContext) → None[source]: Build the built-in cycle numeric atom.

exitEvent_assume(ctx: Event_assumeContext) → None[source]

Build an event assumption and normalize != polarity.

Parameters:: ctx (BmcQueryParser.Event_assumeContext) – Event assumption parse context.
Returns:: None.
Return type:: None

exitEvent_cycle_selector(ctx: Event_cycle_selectorContext) → None[source]

Build an event atom cycle selector.

Parameters:: ctx (BmcQueryParser.Event_cycle_selectorContext) – Event cycle selector parse context.
Returns:: None.
Return type:: None

exitEvent_range_selector(ctx: Event_range_selectorContext) → None[source]

Build an event-assumption range selector.

Parameters:: ctx (BmcQueryParser.Event_range_selectorContext) – Event range selector parse context.
Returns:: None.
Return type:: None

exitFrameVarExprNum(ctx: FrameVarExprNumContext) → None[source]: Build a query-level var("...") numeric atom.

exitFrame_assume(ctx: Frame_assumeContext) → None[source]

Build a frame assumption node.

Parameters:: ctx (BmcQueryParser.Frame_assumeContext) – Frame assumption parse context.
Returns:: None.
Return type:: None

exitFrame_selector(ctx: Frame_selectorContext) → None[source]

Build an optional-frame atom selector.

Parameters:: ctx (BmcQueryParser.Frame_selectorContext) – Frame selector parse context.
Returns:: None.
Return type:: None

exitFuncExprNum(ctx: FuncExprNumContext) → None[source]: Build a unary math function expression.

exitIdExprNum(ctx: IdExprNumContext) → None[source]: Build a bare numeric name reference.

exitInit_clause(ctx: Init_clauseContext) → None[source]

Build an initial clause node.

Parameters:: ctx (BmcQueryParser.Init_clauseContext) – Initial clause parse context.
Returns:: None.
Return type:: None

exitInit_havoc_clause(ctx: Init_havoc_clauseContext) → None[source]

Build an initial variable policy from a havoc clause.

Parameters:: ctx (BmcQueryParser.Init_havoc_clauseContext) – Initial havoc clause parse context.
Returns:: None.
Return type:: None

exitInit_target(ctx: Init_targetContext) → None[source]

Build an initial-target tuple used by exitInit_clause().

Parameters:: ctx (BmcQueryParser.Init_targetContext) – Initial-target parse context.
Returns:: None.
Return type:: None

exitInit_var_ref(ctx: Init_var_refContext) → None[source]

Build a variable name used inside an initial havoc clause.

Parameters:: ctx (BmcQueryParser.Init_var_refContext) – Initial variable reference parse context.
Returns:: None.
Return type:: None

exitInteger_literal(ctx: Integer_literalContext) → None[source]

Build an integer value for query bounds and selectors.

Parameters:: ctx (BmcQueryParser.Integer_literalContext) – Integer literal parse context.
Returns:: None.
Return type:: None

exitLiteralExprCond(ctx: LiteralExprCondContext) → None[source]: Bind a boolean literal condition expression to its literal node.

exitLiteralExprNum(ctx: LiteralExprNumContext) → None[source]: Bind a numeric literal expression to its literal node.

exitMathConstExprNum(ctx: MathConstExprNumContext) → None[source]: Bind a math-constant numeric expression to its constant node.

exitMath_const(ctx: Math_constContext) → None[source]: Build a math-constant expression node.

exitNum_literal(ctx: Num_literalContext) → None[source]: Build an integer or floating-point literal expression node.

exitParenExprCond(ctx: ParenExprCondContext) → None[source]: Bind a parenthesized condition expression to its inner node.

exitParenExprNum(ctx: ParenExprNumContext) → None[source]: Bind a parenthesized numeric expression to its inner node.

exitProperty_body(ctx: Property_bodyContext) → None[source]

Bind a property body to a response tuple or condition predicate.

Parameters:: ctx (BmcQueryParser.Property_bodyContext) – Property body parse context.
Returns:: None.
Return type:: None

exitProperty_kind(ctx: Property_kindContext) → None[source]

Bind a property kind context to its text.

Parameters:: ctx (BmcQueryParser.Property_kindContext) – Property-kind parse context.
Returns:: None.
Return type:: None

exitQuery(ctx: QueryContext) → None[source]

Build the top-level pyfcstm.bmc.query.BmcQuery.

Parameters:: ctx (BmcQueryParser.QueryContext) – Query parse context.
Returns:: None.
Return type:: None

exitResponse_property_body(ctx: Response_property_bodyContext) → None[source]

Build a response body tuple (trigger, within, response).

Parameters:: ctx (BmcQueryParser.Response_property_bodyContext) – Response property body parse context.
Returns:: None.
Return type:: None

exitString_list(ctx: String_listContext) → None[source]

Build a tuple of decoded string literals.

Parameters:: ctx (BmcQueryParser.String_listContext) – String-list parse context.
Returns:: None.
Return type:: None

exitString_literal(ctx: String_literalContext) → None[source]: Decode a string literal token into a Python string.

exitUnaryExprCond(ctx: UnaryExprCondContext) → None[source]: Build a condition unary expression.

exitUnaryExprNum(ctx: UnaryExprNumContext) → None[source]: Build a numeric unary expression.

pyfcstm.bmc.listener

__all__

BmcQueryParseListener

all