10271507760

Committed 06 Aug 2024 05:53PM UTC coverage: 92.368% (+0.4%) from 91.96%

Build # 10271507760

Build Type

Pull #1072

github

Committed by

web-flow

Commit Message

Merge c1442fb2f into 26bbbfc81

Pull Request Pull Request #1072: Add Z3 Constraints to CFG Edges

Run Details

101 of 101 new or added lines in 3 files covered. (100.0%)

14 existing lines in 2 files now uncovered.

3062 of 3315 relevant lines covered (92.37%)

9.11 hits per line

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

95.78

/python_ta/transforms/ExprWrapper.py

from typing import Dict, List, 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 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, node: astroid.NodeNG, types=None):
        if types is None:
            types = {}
        self.types = types

        if isinstance(node, astroid.Expr):
            self.node = node.value  # take node attribute to be the value of the expression
        elif isinstance(node, astroid.Assign):
            self.node = node.value  # take node attribute as expression (right side) of assignment
        elif isinstance(node, astroid.Arguments):
            self.node = node  # take node attribute to be the function declaration node itself
        else:
            raise ValueError(
                "'node' param must be an astroid expression, assignment, or arguments node."
            )

    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.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)
        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 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 == ">":
                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, 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]

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

        return z3_vars

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

pyta-uoft / pyta / 10271507760

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