9768013261

Committed 02 Jul 2024 09:09PM UTC coverage: 91.744% (+0.02%) from 91.723%

Build # 9768013261

Build Type

Pull #1061

github

Committed by

web-flow

Commit Message

Merge 709c9073e into 9c191fe57

Pull Request Pull Request #1061: feat: add support for container literals and in operator in ExprWrapper

Run Details

9 of 12 new or added lines in 1 file covered. (75.0%)

1 existing line in 1 file now uncovered.

2878 of 3137 relevant lines covered (91.74%)

9.04 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

86.79

/python_ta/transforms/ExprWrapper.py

from typing import Dict, List, Optional, Set, Tuple, Union

import astroid
import z3
from astroid import nodes


class Z3ParseException(Exception):
    """
    Raised when a case is not considered when translating an astroid expression node
    into a z3 expression.
    """

    pass


class ExprWrapper:
    """
    Wrapper class to convert 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.
    """

    node: astroid.NodeNG
    types: Dict[str, str]

    def __init__(self, expr: nodes.Expr, types=None):
        self.node = expr.value
        if types is None:
            types = {}
        self.types = types

    def reduce(self, node: astroid.NodeNG = None) -> 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):
            node = self.parse_unary_op(node)
        elif isinstance(node, nodes.Compare):
            node = self.parse_compare(node)
        elif isinstance(node, nodes.BinOp):
            node = self.parse_bin_op(node)
        elif isinstance(node, nodes.Const):
            node = node.value
        elif isinstance(node, nodes.Name):
            node = self.apply_name(node.name)
        elif isinstance(node, (nodes.List, nodes.Tuple, nodes.Set)):
            node = self.parse_container_op(node)
        else:
            raise Z3ParseException(f"Unhandled node type {type(node)}.")

        return node

    def apply_name(self, name: str) -> z3.ExprRef:
        """
        Set up the appropriate variable representation in Z3 based on name and type.
        If an error is encountered or a case is unconsidered, return None.
        """
        typ = self.types[name]
        type_to_z3 = {
            "int": z3.Int,
            "float": z3.Real,
            "bool": z3.Bool,
        }
        if typ in type_to_z3:
            x = type_to_z3[typ](name)
        else:
            raise Z3ParseException(f"Unhandled type {typ}.")

        return x

    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)
        for item in ops:
            op, right = item
            right = self.reduce(right)
            left = self.apply_bin_op(left, op, right)
        return left

    def apply_unary_op(self, left: z3.ExprRef, op: str) -> z3.ExprRef:
        """Apply z3 unary operation indicated by op."""
        op_to_z3 = {
            "not": z3.Not,
        }
        if op in op_to_z3:
            left = op_to_z3[op](left)
        else:
            raise Z3ParseException(f"Unhandled unary operation {op}.")

        return left

    def apply_bin_op(
        self, left: z3.ExprRef, op: str, right: Union[z3.ExprRef, List[z3.ExprRef]]
    ) -> z3.ExprRef:
        """Given left, right, op, apply the binary operation."""
        try:
            if op == "+":
                return left + right
            elif op == "-":
                return left - right
            elif op == "*":
                return left * right
            elif op == "/":
                return left / right
            elif op == "**":
                return left**right
            elif op == "==":
                return left == right
            elif op == "<=":
                return left <= right
            elif op == ">=":
                return left >= right
            elif op == "<":
                return left < right
            elif op == ">":
                return left > right
            elif op == "in":
                return z3.Or(*[left == element for element in right])
            elif op == "not in":
                return z3.And(*[left != element for element in right])
            else:
                raise Z3ParseException(f"Unhandled binary operation {op}.")
        except TypeError:
            raise Z3ParseException(f"Operation {op} incompatible with types {left} and {right}.")

    def apply_bool_op(self, op: str, values: Union[z3.ExprRef, List[z3.ExprRef]]) -> z3.ExprRef:
        """Apply boolean operation given by op to values."""
        op_to_z3 = {
            "and": z3.And,
            "or": z3.Or,
            "not": z3.Not,
        }
        if op in op_to_z3:
            value = op_to_z3[op](values)
        else:
            raise Z3ParseException(f"Unhandled boolean operation {op}.")

        return value

    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)

        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)

        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]

        return self.apply_bool_op(op, values)

    def parse_container_op(
        self, node: Union[nodes.List, nodes.Set, nodes.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]

1	from typing import Dict, List, Optional, Set, Tuple, Union	10✔
2
3	import astroid	10✔
4	import z3	10✔
5	from astroid import nodes	10✔
6
7
8	class Z3ParseException(Exception):	10✔
9	"""	5✔
10	Raised when a case is not considered when translating an astroid expression node
11	into a z3 expression.
12	"""
13
14	pass	10✔
15
16
17	class ExprWrapper:	10✔
18	"""	5✔
19	Wrapper class to convert an astroid expression node into a z3 expression.
20
21	Instance attributes:
22	- node: astroid node obtained given by the value attribute of astroid expression.
23	- types: dictionary mapping variable names in astroid expression to their type name.
24	"""
25
26	node: astroid.NodeNG	10✔
27	types: Dict[str, str]	10✔
28
29	def __init__(self, expr: nodes.Expr, types=None):	10✔
30	self.node = expr.value	10✔
31	if types is None:	10✔
32	types = {}	×
33	self.types = types	10✔
34
35	def reduce(self, node: astroid.NodeNG = None) -> z3.ExprRef:	10✔
36	"""
37	Convert astroid node to z3 expression and return it.
38	If an error is encountered or a case is not considered, return None.
39	"""
40	if node is None:	10✔
41	node = self.node	10✔
42
43	if isinstance(node, nodes.BoolOp):	10✔
44	node = self.parse_bool_op(node)	10✔
45	elif isinstance(node, nodes.UnaryOp):	10✔
46	node = self.parse_unary_op(node)	10✔
47	elif isinstance(node, nodes.Compare):	10✔
48	node = self.parse_compare(node)	10✔
49	elif isinstance(node, nodes.BinOp):	10✔
50	node = self.parse_bin_op(node)	10✔
51	elif isinstance(node, nodes.Const):	10✔
52	node = node.value	10✔
53	elif isinstance(node, nodes.Name):	10✔
54	node = self.apply_name(node.name)	10✔
55	elif isinstance(node, (nodes.List, nodes.Tuple, nodes.Set)):	10✔
56	node = self.parse_container_op(node)	10✔
57	else:
58	raise Z3ParseException(f"Unhandled node type {type(node)}.")	×
59
60	return node	10✔
61
62	def apply_name(self, name: str) -> z3.ExprRef:	10✔
63	"""
64	Set up the appropriate variable representation in Z3 based on name and type.
65	If an error is encountered or a case is unconsidered, return None.
66	"""
67	typ = self.types[name]	10✔
68	type_to_z3 = {	10✔
69	"int": z3.Int,
70	"float": z3.Real,
71	"bool": z3.Bool,
72	}
73	if typ in type_to_z3:	10✔
74	x = type_to_z3[typ](name)	10✔
75	else:
76	raise Z3ParseException(f"Unhandled type {typ}.")	×
77
78	return x	10✔
79
80	def parse_compare(self, node: astroid.Compare) -> z3.ExprRef:	10✔
81	"""Convert an astroid Compare node to z3 expression."""
82	left, ops = node.left, node.ops	10✔
83	left = self.reduce(left)	10✔
84	for item in ops:	10✔
85	op, right = item	10✔
86	right = self.reduce(right)	10✔
87	left = self.apply_bin_op(left, op, right)	10✔
88	return left	10✔
89
90	def apply_unary_op(self, left: z3.ExprRef, op: str) -> z3.ExprRef:	10✔
91	"""Apply z3 unary operation indicated by op."""
92	op_to_z3 = {	10✔
93	"not": z3.Not,
94	}
95	if op in op_to_z3:	10✔
96	left = op_to_z3[op](left)	10✔
97	else:
98	raise Z3ParseException(f"Unhandled unary operation {op}.")	×
99
100	return left	10✔
101
102	def apply_bin_op(	10✔
103	self, left: z3.ExprRef, op: str, right: Union[z3.ExprRef, List[z3.ExprRef]]
104	) -> z3.ExprRef:
105	"""Given left, right, op, apply the binary operation."""
106	try:	10✔
107	if op == "+":	10✔
108	return left + right	10✔
109	elif op == "-":	10✔
110	return left - right	×
111	elif op == "*":	10✔
112	return left * right	×
113	elif op == "/":	10✔
114	return left / right	×
115	elif op == "**":	10✔
116	return left**right	10✔
117	elif op == "==":	10✔
118	return left == right	10✔
119	elif op == "<=":	10✔
120	return left <= right	×
121	elif op == ">=":	10✔
122	return left >= right	×
123	elif op == "<":	10✔
124	return left < right	×
125	elif op == ">":	10✔
126	return left > right	10✔
127	elif op == "in":	10✔
128	return z3.Or(*[left == element for element in right])	10✔
129	elif op == "not in":	10✔
130	return z3.And(*[left != element for element in right])	10✔
131	else:
NEW 132	raise Z3ParseException(f"Unhandled binary operation {op}.")	×
NEW 133	except TypeError:	×
NEW 134	raise Z3ParseException(f"Operation {op} incompatible with types {left} and {right}.")	×
135
136	def apply_bool_op(self, op: str, values: Union[z3.ExprRef, List[z3.ExprRef]]) -> z3.ExprRef:	10✔
137	"""Apply boolean operation given by op to values."""
138	op_to_z3 = {	10✔
139	"and": z3.And,
140	"or": z3.Or,
141	"not": z3.Not,
142	}
143	if op in op_to_z3:	10✔
144	value = op_to_z3[op](values)	10✔
145	else:
UNCOV 146	raise Z3ParseException(f"Unhandled boolean operation {op}.")	×
147
148	return value	10✔
149
150	def parse_unary_op(self, node: astroid.UnaryOp) -> z3.ExprRef:	10✔
151	"""Convert an astroid UnaryOp node to a z3 expression."""
152	left, op = node.operand, node.op	10✔
153	left = self.reduce(left)	10✔
154
155	return self.apply_unary_op(left, op)	10✔
156
157	def parse_bin_op(self, node: astroid.BinOp) -> z3.ExprRef:	10✔
158	"""Convert an astroid BinOp node to a z3 expression."""
159	left, op, right = node.left, node.op, node.right	10✔
160	left = self.reduce(left)	10✔
161	right = self.reduce(right)	10✔
162
163	return self.apply_bin_op(left, op, right)	10✔
164
165	def parse_bool_op(self, node: astroid.BoolOp) -> z3.ExprRef:	10✔
166	"""Convert an astroid BoolOp node to a z3 expression."""
167	op, values = node.op, node.values	10✔
168	values = [self.reduce(x) for x in values]	10✔
169
170	return self.apply_bool_op(op, values)	10✔
171
172	def parse_container_op(	10✔
173	self, node: Union[nodes.List, nodes.Set, nodes.Tuple]
174	) -> List[z3.ExprRef]:
175	"""Convert an astroid List, Set, Tuple node to a list of z3 expressions."""
176	return [self.reduce(element) for element in node.elts]	10✔

pyta-uoft / pyta / 9768013261

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous