19282057813

Committed 12 Nov 2025 12:11AM UTC coverage: 93.909% (-0.3%) from 94.222%

Build # 19282057813

Build Type

Pull #1251

github

Committed by

web-flow

Commit Message

Merge 7053ae2b9 into ef514f733

Pull Request Pull Request #1251: Optimizing performance for 'test_examples.py'

Run Details

8 of 8 new or added lines in 2 files covered. (100.0%)

16 existing lines in 7 files now uncovered.

3515 of 3743 relevant lines covered (93.91%)

17.81 hits per line

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

94.29

/python_ta/z3/z3_parser.py

from __future__ import annotations

from typing import Optional, Union

import astroid
import z3
from astroid import nodes
from pylint.checkers.utils import safe_infer


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

    pass


class Z3Parser:
    """
    Class that converts an astroid expression node into a z3 expression.

    Instance attributes:
        - 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, types: Optional[dict[str, Union[str, z3.ExprRef]]] = None):
        if types is None:
            types = {}
        self.types = types

    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 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.Expr, nodes.Assign)):
            node = self.parse(node.value)
        elif isinstance(node, nodes.Const):
            node = node.value
        elif isinstance(node, nodes.Name):
            node = self.apply_name(node.name)
        elif isinstance(node, nodes.AssignName):
            node = self.apply_name(node.name)
        elif isinstance(node, (nodes.List, nodes.Tuple, nodes.Set)):
            node = self.parse_container_op(node)
        elif isinstance(node, nodes.Subscript):
            node = self.parse_subscript_op(node)
        elif isinstance(node, nodes.Call):
            return self.parse_call(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.get(name)
        type_to_z3 = {
            "int": z3.Int,
            "float": z3.Real,
            "bool": z3.Bool,
            "str": z3.String,
        }
        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}.")

        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.parse(left)
        for item in ops:
            op, right = item
            right = self.parse(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 == ">":
                return left > right
            elif op == "in":
                return self.apply_in_op(left, right)
            elif op == "not in":
                return self.apply_in_op(left, right, negate=True)
            else:
                raise Z3ParseException(
                    f"Unhandled binary operation {op} with operator types {left} and {right}."
                )
        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.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.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.parse(x) for x in values]

        return self.apply_bool_op(op, values)

    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.parse(element) for element in node.elts]

    def apply_in_op(
        self,
        left: Union[z3.ExprRef, str],
        right: Union[z3.ExprRef, list[z3.ExprRef], str],
        negate: bool = False,
    ) -> z3.ExprRef:
        """
        Apply `in` or `not in` operator on a list or string and return the
        resulting z3 expression. Raise Z3ParseException if the operands
        do not support `in` operator
        """
        if isinstance(right, list):  # container type (list/set/tuple)
            return (
                z3.And(*[left != element for element in right])
                if negate
                else z3.Or(*[left == element for element in right])
            )
        elif isinstance(left, (str, z3.SeqRef)) and isinstance(
            right, (str, z3.SeqRef)
        ):  # string literal or variable
            return z3.Not(z3.Contains(right, left)) if negate else z3.Contains(right, left)
        else:
            op = "not in" if negate else "in"
            raise Z3ParseException(
                f"Unhandled binary operation {op} with operator types {left} and {right}."
            )

    def _parse_number_literal(self, node: astroid.NodeNG) -> Optional[Union[int, float]]:
        """
        If the subtree from `node` represent a number literal, return the value
        Otherwise, return None
        """
        # positive number
        if isinstance(node, nodes.Const) and isinstance(node.value, (int, float)):
            return node.value
        # negative number
        elif (
            isinstance(node, nodes.UnaryOp)
            and node.op == "-"
            and isinstance(node.operand, nodes.Const)
            and isinstance(node.operand.value, (int, float))
        ):
            return -node.operand.value
        else:
            return None

    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.parse(node.value)
        slice = node.slice

        # check for invalid node type
        if not z3.is_seq(value):
            raise Z3ParseException(f"Unhandled subscript operand type {value}")

        # handle indexing
        index = self._parse_number_literal(slice)
        if isinstance(index, int):
            return z3.SubString(value, index, 1)

        # handle slicing
        if isinstance(slice, nodes.Slice):
            lower = 0 if slice.lower is None else self._parse_number_literal(slice.lower)
            upper = (
                z3.Length(value) if slice.upper is None else self._parse_number_literal(slice.upper)
            )
            step = 1 if slice.step is None else self._parse_number_literal(slice.step)

            if not (
                isinstance(lower, int)
                and isinstance(upper, (int, z3.ArithRef))
                and isinstance(step, int)
            ):
                raise Z3ParseException(f"Invalid slicing indexes {lower}, {upper}, {step}")

            if step == 1:
                return z3.SubString(value, lower, upper - lower)

            # unhandled case: the upper bound is indeterminant
            if step != 1 and upper == z3.Length(value):
                raise Z3ParseException(
                    "Unable to convert a slicing operation with a non-unit step length and an indeterminant upper bound"
                )

            return z3.Concat(*(z3.SubString(value, i, 1) for i in range(lower, upper, step)))

        raise Z3ParseException(f"Unhandled subscript operator type {slice}")

    def parse_arguments(self, node: astroid.Arguments) -> dict[str, z3.ExprRef]:
        """Convert an astroid Arguments node's parameters to z3 variables."""
        z3_vars = {}

        annotations = node.annotations
        arguments = node.args
        for ann, arg in zip(annotations, arguments):
            if ann is None:
                continue

            inferred = safe_infer(ann)
            if inferred is None or not isinstance(inferred, astroid.ClassDef):
                continue

            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.parse(arg)

        return z3_vars

    def parse_call(self, node: nodes.Call) -> Union[z3.ExprRef, list[z3.ExprRef]]:
        """
        Convert a set(), list(), or tuple() call node into a list of z3 expressions.
        This handles both empty and non-empty calls, including nested container expressions
        """
        if not isinstance(node.func, nodes.Name):
            raise Z3ParseException(f"Unsupported call target {node.func}")
        elif node.func.name not in {"set", "list", "tuple"}:
            raise Z3ParseException(f"Unsupported call to {node.func.name}")
        elif not node.args:
            return []
        elif len(node.args) == 1:
            parsed = self.parse(node.args[0])
            if not isinstance(parsed, list):
                raise Z3ParseException(
                    f"Expected a list from parse(arg), got {type(parsed)} instead"
                )
            return parsed
        else:
            return [self.parse(arg) for arg in node.args]

1	from __future__ import annotations	10✔
2
3	from typing import Optional, Union	10✔
4
5	import astroid	10✔
6	import z3	10✔
7	from astroid import nodes	10✔
8	from pylint.checkers.utils import safe_infer	10✔
9
10
11	class Z3ParseException(Exception):	10✔
12	"""
13	Raised when a case is not considered when translating an astroid expression node
14	into a z3 expression.
15	"""
16
17	pass	10✔
18
19
20	class Z3Parser:	10✔
21	"""
22	Class that converts an astroid expression node into a z3 expression.
23
24	Instance attributes:
25	- types: dictionary mapping variable names in astroid expression to their type name or z3 variable.
26	"""
27
28	node: astroid.NodeNG	10✔
29	types: dict[str, Union[str, z3.ExprRef]]	10✔
30
31	def __init__(self, types: Optional[dict[str, Union[str, z3.ExprRef]]] = None):	10✔
32	if types is None:	10✔
33	types = {}	10✔
34	self.types = types	10✔
35
36	def parse(self, node: astroid.NodeNG) -> z3.ExprRef:	10✔
37	"""
38	Convert astroid node to z3 expression and return it.
39	If an error is encountered or a case is not considered, return None.
40	"""
41	if isinstance(node, nodes.BoolOp):	10✔
42	node = self.parse_bool_op(node)	10✔
43	elif isinstance(node, nodes.UnaryOp):	10✔
44	node = self.parse_unary_op(node)	10✔
45	elif isinstance(node, nodes.Compare):	10✔
46	node = self.parse_compare(node)	10✔
47	elif isinstance(node, nodes.BinOp):	10✔
48	node = self.parse_bin_op(node)	10✔
49	elif isinstance(node, (nodes.Expr, nodes.Assign)):	10✔
50	node = self.parse(node.value)	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.AssignName):	10✔
56	node = self.apply_name(node.name)	10✔
57	elif isinstance(node, (nodes.List, nodes.Tuple, nodes.Set)):	10✔
58	node = self.parse_container_op(node)	10✔
59	elif isinstance(node, nodes.Subscript):	10✔
60	node = self.parse_subscript_op(node)	10✔
61	elif isinstance(node, nodes.Call):	10✔
62	return self.parse_call(node)	10✔
63	else:
64	raise Z3ParseException(f"Unhandled node type {type(node)}.")	10✔
65
66	return node	10✔
67
68	def apply_name(self, name: str) -> z3.ExprRef:	10✔
69	"""
70	Set up the appropriate variable representation in Z3 based on name and type.
71	If an error is encountered or a case is unconsidered, return None.
72	"""
73	typ = self.types.get(name)	10✔
74	type_to_z3 = {	10✔
75	"int": z3.Int,
76	"float": z3.Real,
77	"bool": z3.Bool,
78	"str": z3.String,
79	}
80	if isinstance(typ, z3.ExprRef): # the value is already a z3 variable	10✔
81	x = typ	10✔
82	elif typ in type_to_z3: # convert string value to z3 variable	10✔
83	x = type_to_z3[typ](name)	10✔
84	else:
85	raise Z3ParseException(f"Unhandled type {typ}.")	10✔
86
87	return x	10✔
88
89	def parse_compare(self, node: astroid.Compare) -> z3.ExprRef:	10✔
90	"""Convert an astroid Compare node to z3 expression."""
91	left, ops = node.left, node.ops	10✔
92	left = self.parse(left)	10✔
93	for item in ops:	10✔
94	op, right = item	10✔
95	right = self.parse(right)	10✔
96	left = self.apply_bin_op(left, op, right)	10✔
97	return left	10✔
98
99	def apply_unary_op(self, left: z3.ExprRef, op: str) -> z3.ExprRef:	10✔
100	"""Apply z3 unary operation indicated by op."""
101	op_to_z3 = {	10✔
102	"not": z3.Not,
103	}
104	if op in op_to_z3:	10✔
105	left = op_to_z3[op](left)	10✔
106	else:
107	raise Z3ParseException(f"Unhandled unary operation {op}.")	10✔
108
109	return left	10✔
110
111	def apply_bin_op(	10✔
112	self, left: z3.ExprRef, op: str, right: Union[z3.ExprRef, list[z3.ExprRef]]
113	) -> z3.ExprRef:
114	"""Given left, right, op, apply the binary operation."""
115	try:	10✔
116	if op == "+":	10✔
117	return left + right	10✔
118	elif op == "-":	10✔
119	return left - right	×
120	elif op == "*":	10✔
121	return left * right	×
122	elif op == "/":	10✔
123	return left / right	×
124	elif op == "**":	10✔
125	return left**right	10✔
126	elif op == "==":	10✔
127	return left == right	10✔
128	elif op == "!=":	10✔
129	return left != right	10✔
130	elif op == "<=":	10✔
131	return left <= right	10✔
132	elif op == ">=":	10✔
133	return left >= right	10✔
134	elif op == "<":	10✔
135	return left < right	10✔
136	elif op == ">":	10✔
137	return left > right	10✔
138	elif op == "in":	10✔
139	return self.apply_in_op(left, right)	10✔
140	elif op == "not in":	10✔
141	return self.apply_in_op(left, right, negate=True)	10✔
142	else:
143	raise Z3ParseException(	×
144	f"Unhandled binary operation {op} with operator types {left} and {right}."
145	)
146	except TypeError:	10✔
147	raise Z3ParseException(f"Operation {op} incompatible with types {left} and {right}.")	×
148
149	def apply_bool_op(self, op: str, values: Union[z3.ExprRef, list[z3.ExprRef]]) -> z3.ExprRef:	10✔
150	"""Apply boolean operation given by op to values."""
151	op_to_z3 = {	10✔
152	"and": z3.And,
153	"or": z3.Or,
154	"not": z3.Not,
155	}
156	if op in op_to_z3:	10✔
157	value = op_to_z3[op](values)	10✔
158	else:
159	raise Z3ParseException(f"Unhandled boolean operation {op}.")	×
160
161	return value	10✔
162
163	def parse_unary_op(self, node: astroid.UnaryOp) -> z3.ExprRef:	10✔
164	"""Convert an astroid UnaryOp node to a z3 expression."""
165	left, op = node.operand, node.op	10✔
166	left = self.parse(left)	10✔
167	return self.apply_unary_op(left, op)	10✔
168
169	def parse_bin_op(self, node: astroid.BinOp) -> z3.ExprRef:	10✔
170	"""Convert an astroid BinOp node to a z3 expression."""
171	left, op, right = node.left, node.op, node.right	10✔
172	left = self.parse(left)	10✔
173	right = self.parse(right)	10✔
174
175	return self.apply_bin_op(left, op, right)	10✔
176
177	def parse_bool_op(self, node: astroid.BoolOp) -> z3.ExprRef:	10✔
178	"""Convert an astroid BoolOp node to a z3 expression."""
179	op, values = node.op, node.values	10✔
180	values = [self.parse(x) for x in values]	10✔
181
182	return self.apply_bool_op(op, values)	10✔
183
184	def parse_container_op(	10✔
185	self, node: Union[nodes.List, astroid.Set, astroid.Tuple]
186	) -> list[z3.ExprRef]:
187	"""Convert an astroid List, Set, Tuple node to a list of z3 expressions."""
188	return [self.parse(element) for element in node.elts]	10✔
189
190	def apply_in_op(	10✔
191	self,
192	left: Union[z3.ExprRef, str],
193	right: Union[z3.ExprRef, list[z3.ExprRef], str],
194	negate: bool = False,
195	) -> z3.ExprRef:
196	"""
197	Apply `in` or `not in` operator on a list or string and return the
198	resulting z3 expression. Raise Z3ParseException if the operands
199	do not support `in` operator
200	"""
201	if isinstance(right, list): # container type (list/set/tuple)	10✔
202	return (	10✔
203	z3.And(*[left != element for element in right])
204	if negate
205	else z3.Or(*[left == element for element in right])
206	)
207	elif isinstance(left, (str, z3.SeqRef)) and isinstance(	10✔
208	right, (str, z3.SeqRef)
209	): # string literal or variable
210	return z3.Not(z3.Contains(right, left)) if negate else z3.Contains(right, left)	10✔
211	else:
212	op = "not in" if negate else "in"	10✔
213	raise Z3ParseException(	10✔
214	f"Unhandled binary operation {op} with operator types {left} and {right}."
215	)
216
217	def _parse_number_literal(self, node: astroid.NodeNG) -> Optional[Union[int, float]]:	10✔
218	"""
219	If the subtree from `node` represent a number literal, return the value
220	Otherwise, return None
221	"""
222	# positive number
223	if isinstance(node, nodes.Const) and isinstance(node.value, (int, float)):	10✔
224	return node.value	10✔
225	# negative number
226	elif (	10✔
227	isinstance(node, nodes.UnaryOp)
228	and node.op == "-"
229	and isinstance(node.operand, nodes.Const)
230	and isinstance(node.operand.value, (int, float))
231	):
232	return -node.operand.value	10✔
233	else:
234	return None	10✔
235
236	def parse_subscript_op(self, node: astroid.Subscript) -> z3.ExprRef:	10✔
237	"""
238	Convert an astroid Subscript node to z3 expression.
239	This method only supports string values and integer literal (both positive and negative) indexes
240	"""
241	value = self.parse(node.value)	10✔
242	slice = node.slice	10✔
243
244	# check for invalid node type
245	if not z3.is_seq(value):	10✔
246	raise Z3ParseException(f"Unhandled subscript operand type {value}")	10✔
247
248	# handle indexing
249	index = self._parse_number_literal(slice)	10✔
250	if isinstance(index, int):	10✔
251	return z3.SubString(value, index, 1)	10✔
252
253	# handle slicing
254	if isinstance(slice, nodes.Slice):	10✔
255	lower = 0 if slice.lower is None else self._parse_number_literal(slice.lower)	10✔
256	upper = (	10✔
257	z3.Length(value) if slice.upper is None else self._parse_number_literal(slice.upper)
258	)
259	step = 1 if slice.step is None else self._parse_number_literal(slice.step)	10✔
260
261	if not (	10✔
262	isinstance(lower, int)
263	and isinstance(upper, (int, z3.ArithRef))
264	and isinstance(step, int)
265	):
266	raise Z3ParseException(f"Invalid slicing indexes {lower}, {upper}, {step}")	10✔
267
268	if step == 1:	10✔
269	return z3.SubString(value, lower, upper - lower)	10✔
270
271	# unhandled case: the upper bound is indeterminant
272	if step != 1 and upper == z3.Length(value):	10✔
273	raise Z3ParseException(	10✔
274	"Unable to convert a slicing operation with a non-unit step length and an indeterminant upper bound"
275	)
276
277	return z3.Concat(*(z3.SubString(value, i, 1) for i in range(lower, upper, step)))	10✔
278
279	raise Z3ParseException(f"Unhandled subscript operator type {slice}")	10✔
280
281	def parse_arguments(self, node: astroid.Arguments) -> dict[str, z3.ExprRef]:	10✔
282	"""Convert an astroid Arguments node's parameters to z3 variables."""
283	z3_vars = {}	10✔
284
285	annotations = node.annotations	10✔
286	arguments = node.args	10✔
287	for ann, arg in zip(annotations, arguments):	10✔
288	if ann is None:	10✔
289	continue	10✔
290
291	inferred = safe_infer(ann)	10✔
292	if inferred is None or not isinstance(inferred, astroid.ClassDef):	10✔
293	continue	4✔
294
295	self.types[arg.name] = inferred.name	10✔
296
297	if arg.name in self.types and self.types[arg.name] in {"int", "float", "bool", "str"}:	10✔
298	z3_vars[arg.name] = self.parse(arg)	10✔
299
300	return z3_vars	10✔
301
302	def parse_call(self, node: nodes.Call) -> Union[z3.ExprRef, list[z3.ExprRef]]:	10✔
303	"""
304	Convert a set(), list(), or tuple() call node into a list of z3 expressions.
305	This handles both empty and non-empty calls, including nested container expressions
306	"""
307	if not isinstance(node.func, nodes.Name):	10✔
308	raise Z3ParseException(f"Unsupported call target {node.func}")	×
309	elif node.func.name not in {"set", "list", "tuple"}:	10✔
UNCOV 310	raise Z3ParseException(f"Unsupported call to {node.func.name}")	×
311	elif not node.args:	10✔
312	return []	10✔
313	elif len(node.args) == 1:	10✔
314	parsed = self.parse(node.args[0])	10✔
315	if not isinstance(parsed, list):	10✔
316	raise Z3ParseException(	×
317	f"Expected a list from parse(arg), got {type(parsed)} instead"
318	)
319	return parsed	10✔
320	else:
321	return [self.parse(arg) for arg in node.args]	×

pyta-uoft / pyta / 19282057813

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