Skip to content

Commit

Permalink
Fix crash when z3 is missing and add transform error reporting
Browse files Browse the repository at this point in the history
  • Loading branch information
david-yz-liu committed Dec 7, 2024
1 parent dbca946 commit 395a2f8
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 7 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
- Added a STRICT_NUMERIC_TYPES configuration to `python_ta.contracts` allowing to enable/disable stricter type checking of numeric types
- Added integration with MemoryViz Webstepper
- Added `z3` option to `one-iteration-checker` to only check for feasible code blocks based on edge z3 constraints
- Added reporting for errors raised by custom transforms (`Z3Visitor`, `CFGVisitor`)

### 💫 New checkers

Expand All @@ -34,6 +35,7 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
- Added strict type checking support for nested and union types (e.g., `list[int]`, `dict[float, int]`, `Union[int, float]`)
- Fixed issue where CFG edges from loop body to loop condition block was ignored during augmenting edge z3 constraints
- Fixed issue in `one-iteration-checker` where the message was not correctly reported for `while` loops when `z3` option is on
- Fixed crash when z3-solver is not installed

### 🔧 Internal changes

Expand Down
26 changes: 19 additions & 7 deletions python_ta/patches/transforms.py
Original file line number Diff line number Diff line change
@@ -1,24 +1,36 @@
"""Patch to add transforms for setting type constraints and creating control flow graphs.
"""

import logging

from pylint.lint import PyLinter

from ..cfg.visitor import CFGVisitor
from ..transforms.z3_visitor import Z3Visitor


def patch_ast_transforms(z3: bool):
old_get_ast = PyLinter.get_ast

def new_get_ast(self, filepath, modname, data):
ast = old_get_ast(self, filepath, modname, data)
if ast is not None:
if ast is None:
return None

# Run the Z3Visitor
if z3:
try:
if z3:
ast = Z3Visitor().visitor.visit(ast)
ast.accept(CFGVisitor())
except:
pass
from ..transforms.z3_visitor import Z3Visitor

ast = Z3Visitor().visitor.visit(ast)
except Exception as e:
logging.warning(f"Could not run Z3Visitor: {e}")

# Run the CFGVisitor
try:
ast.accept(CFGVisitor())
except Exception as e:
logging.warning(f"Could not run Z3Visitor: {e}")

return ast

PyLinter.get_ast = new_get_ast

0 comments on commit 395a2f8

Please sign in to comment.