10291475238

Committed 07 Aug 2024 08:44PM UTC coverage: 92.289% (+0.3%) from 91.96%

Build # 10291475238

Build Type

Pull #1072

github

Committed by

web-flow

Commit Message

Merge 4b6069573 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%)

9 existing lines in 1 file now uncovered.

3052 of 3307 relevant lines covered (92.29%)

9.1 hits per line

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

94.51

/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 == "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:
UNCOV 73	raise Z3ParseException(f"Unhandled node type {type(node)}.")	×
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✔
UNCOV 136	return left <= right	×
137	elif op == ">=":	10✔
138	return left >= right	10✔
139	elif op == "<":	10✔
140	return left < right	10✔
141	elif op == ">":	10✔
142	return left > right	10✔
143	elif op == "in":	10✔
144	return self.apply_in_op(left, right)	10✔
145	elif op == "not in":	10✔
146	return self.apply_in_op(left, right, negate=True)	10✔
147	else:
UNCOV 148	raise Z3ParseException(	×
149	f"Unhandled binary operation {op} with operator types {left} and {right}."
150	)
151	except TypeError:	10✔
UNCOV 152	raise Z3ParseException(f"Operation {op} incompatible with types {left} and {right}.")	×
153
154	def apply_bool_op(self, op: str, values: Union[z3.ExprRef, List[z3.ExprRef]]) -> z3.ExprRef:	10✔
155	"""Apply boolean operation given by op to values."""
156	op_to_z3 = {	10✔
157	"and": z3.And,
158	"or": z3.Or,
159	"not": z3.Not,
160	}
161	if op in op_to_z3:	10✔
162	value = op_to_z3[op](values)	10✔
163	else:
UNCOV 164	raise Z3ParseException(f"Unhandled boolean operation {op}.")	×
165
166	return value	10✔
167
168	def parse_unary_op(self, node: astroid.UnaryOp) -> z3.ExprRef:	10✔
169	"""Convert an astroid UnaryOp node to a z3 expression."""
170	left, op = node.operand, node.op	10✔
171	left = self.reduce(left)	10✔
172	return self.apply_unary_op(left, op)	10✔
173
174	def parse_bin_op(self, node: astroid.BinOp) -> z3.ExprRef:	10✔
175	"""Convert an astroid BinOp node to a z3 expression."""
176	left, op, right = node.left, node.op, node.right	10✔
177	left = self.reduce(left)	10✔
178	right = self.reduce(right)	10✔
179
180	return self.apply_bin_op(left, op, right)	10✔
181
182	def parse_bool_op(self, node: astroid.BoolOp) -> z3.ExprRef:	10✔
183	"""Convert an astroid BoolOp node to a z3 expression."""
184	op, values = node.op, node.values	10✔
185	values = [self.reduce(x) for x in values]	10✔
186
187	return self.apply_bool_op(op, values)	10✔
188
189	def parse_container_op(	10✔
190	self, node: Union[nodes.List, astroid.Set, astroid.Tuple]
191	) -> List[z3.ExprRef]:
192	"""Convert an astroid List, Set, Tuple node to a list of z3 expressions."""
193	return [self.reduce(element) for element in node.elts]	10✔
194
195	def apply_in_op(	10✔
196	self,
197	left: Union[z3.ExprRef, str],
198	right: Union[z3.ExprRef, List[z3.ExprRef], str],
199	negate: bool = False,
200	) -> z3.ExprRef:
201	"""
202	Apply `in` or `not in` operator on a list or string and return the
203	resulting z3 expression. Raise Z3ParseException if the operands
204	do not support `in` operator
205	"""
206	if isinstance(right, list): # container type (list/set/tuple)	10✔
207	return (	10✔
208	z3.And(*[left != element for element in right])
209	if negate
210	else z3.Or(*[left == element for element in right])
211	)
212	elif isinstance(left, (str, z3.SeqRef)) and isinstance(	10✔
213	right, (str, z3.SeqRef)
214	): # string literal or variable
215	return z3.Not(z3.Contains(right, left)) if negate else z3.Contains(right, left)	10✔
216	else:
217	op = "not in" if negate else "in"	10✔
218	raise Z3ParseException(	10✔
219	f"Unhandled binary operation {op} with operator types {left} and {right}."
220	)
221
222	def _parse_number_literal(self, node: astroid.NodeNG) -> Optional[Union[int, float]]:	10✔
223	"""
224	If the subtree from `node` represent a number literal, return the value
225	Otherwise, return None
226	"""
227	# positive number
228	if isinstance(node, nodes.Const) and isinstance(node.value, (int, float)):	10✔
229	return node.value	10✔
230	# negative number
231	elif (	10✔
232	isinstance(node, nodes.UnaryOp)
233	and node.op == "-"
234	and isinstance(node.operand, nodes.Const)
235	and isinstance(node.operand.value, (int, float))
236	):
237	return -node.operand.value	10✔
238	else:
239	return None	10✔
240
241	def parse_subscript_op(self, node: astroid.Subscript) -> z3.ExprRef:	10✔
242	"""
243	Convert an astroid Subscript node to z3 expression.
244	This method only supports string values and integer literal (both positive and negative) indexes
245	"""
246	value = self.reduce(node.value)	10✔
247	slice = node.slice	10✔
248
249	# check for invalid node type
250	if not z3.is_seq(value):	10✔
251	raise Z3ParseException(f"Unhandled subscript operand type {value}")	10✔
252
253	# handle indexing
254	index = self._parse_number_literal(slice)	10✔
255	if isinstance(index, int):	10✔
256	return z3.SubString(value, index, 1)	10✔
257
258	# handle slicing
259	if isinstance(slice, nodes.Slice):	10✔
260	lower = 0 if slice.lower is None else self._parse_number_literal(slice.lower)	10✔
261	upper = (	10✔
262	z3.Length(value) if slice.upper is None else self._parse_number_literal(slice.upper)
263	)
264	step = 1 if slice.step is None else self._parse_number_literal(slice.step)	10✔
265
266	if not (	10✔
267	isinstance(lower, int)
268	and isinstance(upper, (int, z3.ArithRef))
269	and isinstance(step, int)
270	):
271	raise Z3ParseException(f"Invalid slicing indexes {lower}, {upper}, {step}")	10✔
272
273	if step == 1:	10✔
274	return z3.SubString(value, lower, upper - lower)	10✔
275
276	# unhandled case: the upper bound is indeterminant
277	if step != 1 and upper == z3.Length(value):	10✔
278	raise Z3ParseException(	10✔
279	"Unable to convert a slicing operation with a non-unit step length and an indeterminant upper bound"
280	)
281
282	return z3.Concat(*(z3.SubString(value, i, 1) for i in range(lower, upper, step)))	10✔
283
284	raise Z3ParseException(f"Unhandled subscript operator type {slice}")	10✔
285
286	def parse_arguments(self, node: astroid.Arguments) -> Dict[str, z3.ExprRef]:	10✔
287	"""Convert an astroid Arguments node's parameters to z3 variables."""
288	z3_vars = {}	10✔
289
290	annotations = node.annotations	10✔
291	arguments = node.args	10✔
292	for ann, arg in zip(annotations, arguments):	10✔
293	if ann is None:	10✔
294	continue	10✔
295
296	inferred = safe_infer(ann)	10✔
297	if inferred is None or not isinstance(inferred, astroid.ClassDef):	10✔
298	continue	10✔
299
300	self.types[arg.name] = inferred.name	10✔
301
302	if arg.name in self.types and self.types[arg.name] in {"int", "float", "bool", "str"}:	10✔
303	z3_vars[arg.name] = self.reduce(arg)	10✔
304
305	return z3_vars	10✔

pyta-uoft / pyta / 10291475238

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