9945022554

Committed 15 Jul 2024 06:55PM UTC coverage: 91.648% (-0.1%) from 91.744%

Build # 9945022554

Build Type

Pull #1066

github

Committed by

web-flow

Commit Message

Merge 1cfca13df into 2e3a25dfb

Pull Request Pull Request #1066: Parsing string variables and operators to z3 constraints in `ExprWrapper`

Run Details

36 of 42 new or added lines in 1 file covered. (85.71%)

2 existing lines in 1 file now uncovered.

2908 of 3173 relevant lines covered (91.65%)

9.03 hits per line

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

85.92

/python_ta/transforms/ExprWrapper.py

from typing import Dict, List, Optional, 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) -> Union[z3.ExprRef, List[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)
        elif isinstance(node, nodes.Subscript):
            node = self.parse_index_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,
            "str": z3.String,
        }
        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 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.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]

    def apply_in_op(
        self, left: z3.ExprRef, right: Union[z3.ExprRef, List[z3.ExprRef], str], negate=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 tyoe (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(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) -> Optional:
        """
        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_index_op(self, node: nodes.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)
        if isinstance(value, z3.SeqRef):
            slice = node.slice

            # handle indexing
            index = self._parse_number_literal(slice)
            if isinstance(index, int):
                abs_index = index if index >= 0 else z3.Length(value) - index
                return z3.SubString(value, abs_index, abs_index)

            # handle slicing
            elif 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 (
                    isinstance(lower, int)
                    and isinstance(upper, (int, z3.ArithRef))
                    and isinstance(step, int)
                ):

                    if step == 1:
                        return z3.SubString(value, lower, upper)
                    else:
                        # 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 step length greater than 1 and an indeterminant upper bound"
                            )

                        return z3.Concat(
                            *(z3.SubString(value, i, i) for i in range(lower, upper, step))
                        )
                else:
                    raise Z3ParseException(f"Invalid slice {slice}")
            else:
                raise Z3ParseException(f"Invalid index {slice}")

        else:
            raise Z3ParseException(f"Unhandled subscript operand type {value}")

1	from typing import Dict, List, Optional, 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) -> Union[z3.ExprRef, List[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	elif isinstance(node, nodes.Subscript):	10✔
58	node = self.parse_index_op(node)	10✔
59	else:
UNCOV 60	raise Z3ParseException(f"Unhandled node type {type(node)}.")	×
61
62	return node	10✔
63
64	def apply_name(self, name: str) -> z3.ExprRef:	10✔
65	"""
66	Set up the appropriate variable representation in Z3 based on name and type.
67	If an error is encountered or a case is unconsidered, return None.
68	"""
69	typ = self.types[name]	10✔
70	type_to_z3 = {	10✔
71	"int": z3.Int,
72	"float": z3.Real,
73	"bool": z3.Bool,
74	"str": z3.String,
75	}
76	if typ in type_to_z3:	10✔
77	x = type_to_z3[typ](name)	10✔
78	else:
UNCOV 79	raise Z3ParseException(f"Unhandled type {typ}.")	×
80
81	return x	10✔
82
83	def parse_compare(self, node: astroid.Compare) -> z3.ExprRef:	10✔
84	"""Convert an astroid Compare node to z3 expression."""
85	left, ops = node.left, node.ops	10✔
86	left = self.reduce(left)	10✔
87	for item in ops:	10✔
88	op, right = item	10✔
89	right = self.reduce(right)	10✔
90	left = self.apply_bin_op(left, op, right)	10✔
91	return left	10✔
92
93	def apply_unary_op(self, left: z3.ExprRef, op: str) -> z3.ExprRef:	10✔
94	"""Apply z3 unary operation indicated by op."""
95	op_to_z3 = {	10✔
96	"not": z3.Not,
97	}
98	if op in op_to_z3:	10✔
99	left = op_to_z3[op](left)	10✔
100	else:
101	raise Z3ParseException(f"Unhandled unary operation {op}.")	×
102
103	return left	10✔
104
105	def apply_bin_op(	10✔
106	self, left: z3.ExprRef, op: str, right: Union[z3.ExprRef, List[z3.ExprRef]]
107	) -> z3.ExprRef:
108	"""Given left, right, op, apply the binary operation."""
109	try:	10✔
110	if op == "+":	10✔
111	return left + right	10✔
112	elif op == "-":	10✔
113	return left - right	×
114	elif op == "*":	10✔
115	return left * right	×
116	elif op == "/":	10✔
117	return left / right	×
118	elif op == "**":	10✔
119	return left**right	10✔
120	elif op == "==":	10✔
121	return left == right	10✔
122	elif op == "<=":	10✔
123	return left <= right	×
124	elif op == ">=":	10✔
125	return left >= right	×
126	elif op == "<":	10✔
127	return left < right	×
128	elif op == ">":	10✔
129	return left > right	10✔
130	elif op == "in":	10✔
131	return self.apply_in_op(left, right)	10✔
132	elif op == "not in":	10✔
133	return self.apply_in_op(left, right, negate=True)	10✔
134	else:
135	raise Z3ParseException(	×
136	f"Unhandled binary operation {op} with operator types {left} and {right}."
137	)
138	except TypeError:	×
139	raise Z3ParseException(f"Operation {op} incompatible with types {left} and {right}.")	×
140
141	def apply_bool_op(self, op: str, values: Union[z3.ExprRef, List[z3.ExprRef]]) -> z3.ExprRef:	10✔
142	"""Apply boolean operation given by op to values."""
143	op_to_z3 = {	10✔
144	"and": z3.And,
145	"or": z3.Or,
146	"not": z3.Not,
147	}
148	if op in op_to_z3:	10✔
149	value = op_to_z3[op](values)	10✔
150	else:
151	raise Z3ParseException(f"Unhandled boolean operation {op}.")	×
152
153	return value	10✔
154
155	def parse_unary_op(self, node: astroid.UnaryOp) -> z3.ExprRef:	10✔
156	"""Convert an astroid UnaryOp node to a z3 expression."""
157	left, op = node.operand, node.op	10✔
158	left = self.reduce(left)	10✔
159
160	return self.apply_unary_op(left, op)	10✔
161
162	def parse_bin_op(self, node: astroid.BinOp) -> z3.ExprRef:	10✔
163	"""Convert an astroid BinOp node to a z3 expression."""
164	left, op, right = node.left, node.op, node.right	10✔
165	left = self.reduce(left)	10✔
166	right = self.reduce(right)	10✔
167
168	return self.apply_bin_op(left, op, right)	10✔
169
170	def parse_bool_op(self, node: astroid.BoolOp) -> z3.ExprRef:	10✔
171	"""Convert an astroid BoolOp node to a z3 expression."""
172	op, values = node.op, node.values	10✔
173	values = [self.reduce(x) for x in values]	10✔
174
175	return self.apply_bool_op(op, values)	10✔
176
177	def parse_container_op(	10✔
178	self, node: Union[nodes.List, nodes.Set, nodes.Tuple]
179	) -> List[z3.ExprRef]:
180	"""Convert an astroid List, Set, Tuple node to a list of z3 expressions."""
181	return [self.reduce(element) for element in node.elts]	10✔
182
183	def apply_in_op(	10✔
184	self, left: z3.ExprRef, right: Union[z3.ExprRef, List[z3.ExprRef], str], negate=False
185	) -> z3.ExprRef:
186	"""
187	Apply `in` or `not in` operator on a list or string and return the
188	resulting z3 expression. Raise Z3ParseException if the operands
189	do not support `in` operator
190	"""
191	if isinstance(right, list): # container tyoe (list/set/tuple)	10✔
192	return (	10✔
193	z3.And(*[left != element for element in right])
194	if negate
195	else z3.Or(*[left == element for element in right])
196	)
197	elif isinstance(right, (str, z3.SeqRef)): # string literal or variable	10✔
198	return z3.Not(z3.Contains(right, left)) if negate else z3.Contains(right, left)	10✔
199	else:
NEW 200	op = "not in" if negate else "in"	×
NEW 201	raise Z3ParseException(	×
202	f"Unhandled binary operation {op} with operator types {left} and {right}."
203	)
204
205	def _parse_number_literal(self, node) -> Optional:	10✔
206	"""
207	If the subtree from `node` represent a number literal, return the value
208	Otherwise, return None
209	"""
210	# positive number
211	if isinstance(node, nodes.Const) and isinstance(node.value, (int, float)):	10✔
212	return node.value	10✔
213	# negative number
214	elif (	10✔
215	isinstance(node, nodes.UnaryOp)
216	and node.op == "-"
217	and isinstance(node.operand, nodes.Const)
218	and isinstance(node.operand.value, (int, float))
219	):
220	return -node.operand.value	10✔
221	else:
222	return None	10✔
223
224	def parse_index_op(self, node: nodes.Subscript) -> z3.ExprRef:	10✔
225	"""
226	Convert an astroid Subscript node to z3 expression.
227	This method only supports string values and integer literal (both positive and negative) indexes
228	"""
229	value = self.reduce(node.value)	10✔
230	if isinstance(value, z3.SeqRef):	10✔
231	slice = node.slice	10✔
232
233	# handle indexing
234	index = self._parse_number_literal(slice)	10✔
235	if isinstance(index, int):	10✔
236	abs_index = index if index >= 0 else z3.Length(value) - index	10✔
237	return z3.SubString(value, abs_index, abs_index)	10✔
238
239	# handle slicing
240	elif isinstance(slice, nodes.Slice):	10✔
241	lower = 0 if slice.lower is None else self._parse_number_literal(slice.lower)	10✔
242	upper = (	10✔
243	z3.Length(value)
244	if slice.upper is None
245	else self._parse_number_literal(slice.upper)
246	)
247	step = 1 if slice.step is None else self._parse_number_literal(slice.step)	10✔
248
249	if (	10✔
250	isinstance(lower, int)
251	and isinstance(upper, (int, z3.ArithRef))
252	and isinstance(step, int)
253	):
254
255	if step == 1:	10✔
256	return z3.SubString(value, lower, upper)	10✔
257	else:
258	# unhandled case: the upper bound is indeterminant
259	if step > 1 and upper == z3.Length(value):	10✔
NEW 260	raise Z3ParseException(	×
261	"Unable to convert a slicing operation with a step length greater than 1 and an indeterminant upper bound"
262	)
263
264	return z3.Concat(	10✔
265	*(z3.SubString(value, i, i) for i in range(lower, upper, step))
266	)
267	else:
NEW 268	raise Z3ParseException(f"Invalid slice {slice}")	×
269	else:
NEW 270	raise Z3ParseException(f"Invalid index {slice}")	×
271
272	else:
NEW 273	raise Z3ParseException(f"Unhandled subscript operand type {value}")	×

pyta-uoft / pyta / 9945022554

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