diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 888ebcced..f3b7777f2 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmir" -version = "0.2.14" +version = "0.2.15" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 32e1fb46b..25e198317 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -2,4 +2,4 @@ from .kmir import KMIR -VERSION: Final = '0.2.14' +VERSION: Final = '0.2.15' diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index aeade4b19..b6d072c4c 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -1,4 +1,6 @@ import logging +import sys +import traceback from collections.abc import Callable, Iterable, Iterator from contextlib import contextmanager from pathlib import Path @@ -193,15 +195,44 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_i res_lines.append('') res_lines.append(f' Node id: {str(node.id)}') - simplified_node, _ = kcfg_explore.cterm_simplify(node.cterm) - simplified_target, _ = kcfg_explore.cterm_simplify(target.cterm) + try: + simplified_node, _ = kcfg_explore.cterm_simplify(node.cterm) + except Exception as err: + process_exception( + err, + res_lines, + ' ERROR PRINTING FAILURE INFO: Could not simplify "node.cterm", see stack trace above', + ) + try: + simplified_target, _ = kcfg_explore.cterm_simplify(target.cterm) + except Exception as err: + process_exception( + err, + res_lines, + ' ERROR PRINTING FAILURE INFO: Could not simplify "target.cterm", see stack trace above', + ) res_lines.append(' Failure reason:') - _, reason = kcfg_explore.implication_failure_reason(simplified_node, simplified_target) - res_lines += [f' {line}' for line in reason.split('\n')] + try: + _, reason = kcfg_explore.implication_failure_reason(simplified_node, simplified_target) + res_lines += [f' {line}' for line in reason.split('\n')] + except Exception as err: + process_exception( + err, + res_lines, + ' ERROR PRINTING FAILURE INFO: Could not create "implication_failure_reason", see stack trace above', + ) res_lines.append(' Path condition:') - res_lines += [f' {kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id))}'] + try: + res_lines += [f' {kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id))}'] + except Exception as err: + process_exception( + err, + res_lines, + ' ERROR PRINTING FAILURE INFO: Could not pretty print "proof.path_constraints(node.id)", see stack trace above', + ) + if counterexample_info: res_lines.extend(print_model(node, kcfg_explore)) @@ -217,6 +248,12 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_i raise ValueError('Unknown proof type.') +def process_exception(err: Exception, curr_output: list[str], err_msg: str) -> None: + curr_output.append(err_msg) + print(err, flush=True, file=sys.stderr) + print(traceback.format_exc(), flush=True, file=sys.stderr) + + def print_model(node: KCFG.Node, kcfg_explore: KCFGExplore) -> list[str]: res_lines: list[str] = [] result_subst = kcfg_explore.cterm_get_model(node.cterm) diff --git a/package/version b/package/version index 769ed6ae7..b005e307c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.2.14 +0.2.15