From 02e9adbe06d98b7dcd4dde23632f6cbc97112849 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT <147955278+Raine-Yang-UofT@users.noreply.github.com> Date: Fri, 13 Sep 2024 21:57:08 -0400 Subject: [PATCH] Refactor ExprWrapper and rename it to Z3Parser (#1080) Remove the passing of `node` argument to Z3Parser constructor. Fix error in handling Arguments and Expr nodes. Rename test_expr_wrapper to test_z3_parser. --- CHANGELOG.md | 6 +++ python_ta/cfg/graph.py | 12 ++--- python_ta/transforms/z3_visitor.py | 8 ++-- python_ta/z3/__init__.py | 0 .../ExprWrapper.py => z3/z3_parser.py} | 45 ++++++++----------- tests/test_transforms/test_expr_wrapper.py | 16 ------- tests/test_z3/test_z3_parser.py | 13 ++++++ 7 files changed, 47 insertions(+), 53 deletions(-) create mode 100644 python_ta/z3/__init__.py rename python_ta/{transforms/ExprWrapper.py => z3/z3_parser.py} (89%) delete mode 100644 tests/test_transforms/test_expr_wrapper.py create mode 100644 tests/test_z3/test_z3_parser.py diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d572db5f..9a796f7d6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,12 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### 🔧 Internal changes +- Renamed `ExprWrapper` class to `Z3Parser` +- Renamed `ExprWrapper` module to `z3_parser` and moved it to new directory `python_ta.z3` +- Removed `node` attribute for `Z3Parser` +- Renamed `reduce` method of `Z3Parser` to `parse` +- Renamed `test_expr_wrapper` to `test_z3_parser` + ## [2.8.1] - 2024-08-19 ### 🐛 Bug fixes diff --git a/python_ta/cfg/graph.py b/python_ta/cfg/graph.py index b56e2b0d5..df5bfaf5a 100644 --- a/python_ta/cfg/graph.py +++ b/python_ta/cfg/graph.py @@ -5,12 +5,12 @@ try: from z3 import Z3_OP_UNINTERPRETED, ExprRef, Not, Z3Exception, is_const - from ..transforms.ExprWrapper import ExprWrapper, Z3ParseException + from ..z3.z3_parser import Z3ParseException, Z3Parser z3_dependency_available = True except ImportError: ExprRef = Any - ExprWrapper = Any + Z3Parser = Any Not = Any Z3Exception = Any is_const = Any @@ -62,8 +62,8 @@ def add_arguments(self, args: Arguments) -> None: if ExprRef is not Any: # Parse types - expr = ExprWrapper(args) - z3_vars = expr.parse_arguments(args) + parser = Z3Parser() + z3_vars = parser.parse_arguments(args) self._z3_vars.update(z3_vars) def create_block( @@ -422,9 +422,9 @@ def parse_constraint(self, node: NodeNG) -> Optional[ExprRef]: """Parse an Astroid node to a Z3 constraint Return the resulting expression """ - ew = ExprWrapper(node, self.variables) + parser = Z3Parser(self.variables) try: - return ew.reduce() + return parser.parse(node) except (Z3Exception, Z3ParseException): return None diff --git a/python_ta/transforms/z3_visitor.py b/python_ta/transforms/z3_visitor.py index e7bc46e49..b31162687 100644 --- a/python_ta/transforms/z3_visitor.py +++ b/python_ta/transforms/z3_visitor.py @@ -1,11 +1,11 @@ import astroid -from astroid import AstroidError, Uninferable, nodes +from astroid import AstroidError, nodes from astroid.transforms import TransformVisitor from astroid.util import safe_infer from z3.z3types import Z3Exception from ..contracts import parse_assertions -from .ExprWrapper import ExprWrapper, Z3ParseException +from ..z3.z3_parser import Z3ParseException, Z3Parser class Z3Visitor: @@ -40,9 +40,9 @@ def set_function_def_z3_constraints(self, node: nodes.FunctionDef): z3_constraints = [] for pre in preconditions: pre = astroid.parse(pre).body[0] - ew = ExprWrapper(pre, types) + parser = Z3Parser(types) try: - transformed = ew.reduce() + transformed = parser.parse(pre) except (AstroidError, Z3Exception, Z3ParseException): transformed = None if transformed is not None: diff --git a/python_ta/z3/__init__.py b/python_ta/z3/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/python_ta/transforms/ExprWrapper.py b/python_ta/z3/z3_parser.py similarity index 89% rename from python_ta/transforms/ExprWrapper.py rename to python_ta/z3/z3_parser.py index d29f12ab1..07c955b85 100644 --- a/python_ta/transforms/ExprWrapper.py +++ b/python_ta/z3/z3_parser.py @@ -15,37 +15,26 @@ class Z3ParseException(Exception): pass -class ExprWrapper: +class Z3Parser: """ - Wrapper class to convert an astroid expression node into a z3 expression. + Class that converts an astroid expression node into a z3 expression. Instance attributes: - - node: astroid node obtained given by the value attribute of astroid expression. - types: dictionary mapping variable names in astroid expression to their type name or z3 variable. """ - node: astroid.NodeNG types: Dict[str, Union[str, z3.ExprRef]] - def __init__(self, node: astroid.NodeNG, types=None): + def __init__(self, types: Optional[Dict[str, Union[str, z3.ExprRef]]] = None): if types is None: types = {} self.types = types - # extract expression out of expression statement - if isinstance(node, (astroid.Expr, astroid.Assign)): - self.node = node.value - else: - self.node = node - - def reduce(self, node: astroid.NodeNG = None) -> z3.ExprRef: + def parse(self, node: astroid.NodeNG) -> z3.ExprRef: """ Convert astroid node to z3 expression and return it. If an error is encountered or a case is not considered, return None. """ - if node is None: - node = self.node - if isinstance(node, nodes.BoolOp): node = self.parse_bool_op(node) elif isinstance(node, nodes.UnaryOp): @@ -54,6 +43,8 @@ def reduce(self, node: astroid.NodeNG = None) -> z3.ExprRef: node = self.parse_compare(node) elif isinstance(node, nodes.BinOp): node = self.parse_bin_op(node) + elif isinstance(node, (nodes.Expr, nodes.Assign)): + node = self.parse(node.value) elif isinstance(node, nodes.Const): node = node.value elif isinstance(node, nodes.Name): @@ -81,10 +72,10 @@ def apply_name(self, name: str) -> z3.ExprRef: "bool": z3.Bool, "str": z3.String, } - if typ in type_to_z3: # convert string value to z3 variable - x = type_to_z3[typ](name) - elif isinstance(typ, z3.ExprRef): # the value is already a z3 variable + if isinstance(typ, z3.ExprRef): # the value is already a z3 variable x = typ + elif typ in type_to_z3: # convert string value to z3 variable + x = type_to_z3[typ](name) else: raise Z3ParseException(f"Unhandled type {typ}.") @@ -93,10 +84,10 @@ def apply_name(self, name: str) -> z3.ExprRef: def parse_compare(self, node: astroid.Compare) -> z3.ExprRef: """Convert an astroid Compare node to z3 expression.""" left, ops = node.left, node.ops - left = self.reduce(left) + left = self.parse(left) for item in ops: op, right = item - right = self.reduce(right) + right = self.parse(right) left = self.apply_bin_op(left, op, right) return left @@ -167,21 +158,21 @@ def apply_bool_op(self, op: str, values: Union[z3.ExprRef, List[z3.ExprRef]]) -> def parse_unary_op(self, node: astroid.UnaryOp) -> z3.ExprRef: """Convert an astroid UnaryOp node to a z3 expression.""" left, op = node.operand, node.op - left = self.reduce(left) + left = self.parse(left) return self.apply_unary_op(left, op) def parse_bin_op(self, node: astroid.BinOp) -> z3.ExprRef: """Convert an astroid BinOp node to a z3 expression.""" left, op, right = node.left, node.op, node.right - left = self.reduce(left) - right = self.reduce(right) + left = self.parse(left) + right = self.parse(right) return self.apply_bin_op(left, op, right) def parse_bool_op(self, node: astroid.BoolOp) -> z3.ExprRef: """Convert an astroid BoolOp node to a z3 expression.""" op, values = node.op, node.values - values = [self.reduce(x) for x in values] + values = [self.parse(x) for x in values] return self.apply_bool_op(op, values) @@ -189,7 +180,7 @@ def parse_container_op( self, node: Union[nodes.List, astroid.Set, astroid.Tuple] ) -> List[z3.ExprRef]: """Convert an astroid List, Set, Tuple node to a list of z3 expressions.""" - return [self.reduce(element) for element in node.elts] + return [self.parse(element) for element in node.elts] def apply_in_op( self, @@ -242,7 +233,7 @@ def parse_subscript_op(self, node: astroid.Subscript) -> z3.ExprRef: Convert an astroid Subscript node to z3 expression. This method only supports string values and integer literal (both positive and negative) indexes """ - value = self.reduce(node.value) + value = self.parse(node.value) slice = node.slice # check for invalid node type @@ -299,6 +290,6 @@ def parse_arguments(self, node: astroid.Arguments) -> Dict[str, z3.ExprRef]: self.types[arg.name] = inferred.name if arg.name in self.types and self.types[arg.name] in {"int", "float", "bool", "str"}: - z3_vars[arg.name] = self.reduce(arg) + z3_vars[arg.name] = self.parse(arg) return z3_vars diff --git a/tests/test_transforms/test_expr_wrapper.py b/tests/test_transforms/test_expr_wrapper.py deleted file mode 100644 index 1d44ef517..000000000 --- a/tests/test_transforms/test_expr_wrapper.py +++ /dev/null @@ -1,16 +0,0 @@ -"""Tests for ExprWrapper in python_ta.transforms.""" - -import pytest -from astroid import extract_node - -from python_ta.transforms.ExprWrapper import ExprWrapper - - -def test_expr_wrapper_assignment() -> None: - assignment = "n = 2 + 3" - - node = extract_node(assignment) - expr = ExprWrapper(node) - - assert expr.node is node.value - assert expr.reduce() == 5 diff --git a/tests/test_z3/test_z3_parser.py b/tests/test_z3/test_z3_parser.py new file mode 100644 index 000000000..ed5767d83 --- /dev/null +++ b/tests/test_z3/test_z3_parser.py @@ -0,0 +1,13 @@ +"""Tests for Z3Parser in python_ta.z3.""" + +from astroid import extract_node + +from python_ta.z3.z3_parser import Z3Parser + + +def test_z3_parser_assignment() -> None: + assignment = "n = 2 + 3" + + node = extract_node(assignment) + parser = Z3Parser() + assert parser.parse(node) == 5