pyfcstm.bmc.parse

Parse .fbmcq query text into parser-independent BMC AST objects.

This module is the public parsing entry point for FCSTM BMC Query files. It is structured after pyfcstm.dsl.parse: ANTLR lexer/parser classes perform syntax recognition, pyfcstm.bmc.listener.BmcQueryParseListener builds query objects, and syntax-facing errors are reported through pyfcstm.bmc.errors.BmcQueryParseError.

The parser layer is intentionally narrow. It does not import model classes, Z3, or verify-registry code; model-aware binding and solver lowering belong to later BMC modules.

The module contains:

• parse_with_bmc_grammar_entry() - Parse text through one supported entry rule.

• build_bmc_ast_from_parse_tree() - Walk an already-created parse tree and return the mapped AST object.

• parse_bmc_query(), parse_bmc_num_expression(), and parse_bmc_cond_expression() - Convenience entry points.

Example:

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

__all__

pyfcstm.bmc.parse.__all__ = ['parse_bmc_query', 'parse_bmc_num_expression', 'parse_bmc_cond_expression', 'parse_with_bmc_grammar_entry', 'build_bmc_ast_from_parse_tree']

Built-in mutable sequence.

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

build_bmc_ast_from_parse_tree

pyfcstm.bmc.parse.build_bmc_ast_from_parse_tree(parse_tree: ParserRuleContext) → Any

Build a BMC AST object from an already-created ANTLR parse tree.

Parameters:

parse_tree (antlr4.ParserRuleContext) – Root parse-tree context to walk.

Returns:

AST or query object mapped for parse_tree.

Return type:

object

Raises:

• TypeError – If parse_tree is not an ANTLR parser context.

• pyfcstm.bmc.errors.BmcQueryParseError – If the parse tree contains ANTLR recovery markers, the listener cannot map a recovered child context, or the listener does not map the provided root context.

• pyfcstm.bmc.errors.InvalidBmcQuery – If a syntactically valid query parse tree fails structural query-model validation.

Example:

>>> from antlr4 import CommonTokenStream, InputStream
>>> lexer = BmcQueryLexer(InputStream('1'))
>>> parser = BmcQueryParser(CommonTokenStream(lexer))
>>> tree = parser.bmc_num_expression_entry()
>>> build_bmc_ast_from_parse_tree(tree).value
1

parse_with_bmc_grammar_entry

pyfcstm.bmc.parse.parse_with_bmc_grammar_entry(input_text: str, entry_name: str, force_finished: bool = True) → Any

Parse text with a supported BMC grammar entry rule.

Parameters:

• input_text (str) – Query or expression text.

• entry_name (str) – One of "query", "bmc_num_expression_entry", or "bmc_cond_expression_entry".

• force_finished (bool, optional) – Whether the token stream must be exhausted after the entry rule, defaults to True.

Returns:

AST object produced by the entry rule.

Return type:

object

Raises:

pyfcstm.bmc.errors.BmcQueryParseError – If entry_name is unsupported or parsing fails.

Example:

>>> node = parse_with_bmc_grammar_entry('cycle + 1', 'bmc_num_expression_entry')
>>> node.to_canonical()['node']
'num_binary'

Note

The currently supported text entries already end in EOF in the grammar. force_finished is kept for API parity with pyfcstm.dsl.parse and as an extra guard for future entries.

parse_bmc_query

pyfcstm.bmc.parse.parse_bmc_query(input_text: str) → BmcQuery

Parse a complete .fbmcq query.

Parameters:

input_text (str) – Complete query text.

Returns:

Parsed query object.

Return type:

pyfcstm.bmc.query.BmcQuery

Raises:

• pyfcstm.bmc.errors.BmcQueryParseError – If syntax parsing fails.

• pyfcstm.bmc.errors.InvalidBmcQuery – If the parsed query is structurally invalid, for example check ... <= 0.

Example:

>>> parse_bmc_query('check reach <= 1: true;').property.bound
1

parse_bmc_num_expression

pyfcstm.bmc.parse.parse_bmc_num_expression(input_text: str) → BmcNumExpr

Parse a standalone BMC numeric expression.

Parameters:

input_text (str) – Numeric expression text.

Returns:

Parsed numeric expression object.

Return type:

pyfcstm.bmc.ast.BmcNumExpr

Raises:

pyfcstm.bmc.errors.BmcQueryParseError – If syntax parsing fails.

Example:

>>> parse_bmc_num_expression('cycle + 1').to_canonical()['op']
'+'

parse_bmc_cond_expression

pyfcstm.bmc.parse.parse_bmc_cond_expression(input_text: str) → BmcCondExpr

Parse a standalone BMC condition expression.

Parameters:

input_text (str) – Condition expression text.

Returns:

Parsed condition expression object.

Return type:

pyfcstm.bmc.ast.BmcCondExpr

Raises:

pyfcstm.bmc.errors.BmcQueryParseError – If syntax parsing fails.

Example:

>>> parse_bmc_cond_expression('active("Root.A")').to_canonical()['node']
'active'