10308526715

Committed 08 Aug 2024 07:45PM UTC coverage: 92.089% (+0.1%) from 91.96%

Build # 10308526715

Build Type

Pull #1072

github

Committed by

web-flow

Commit Message

Merge 96757fab7 into 26bbbfc81

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

Run Details

96 of 102 new or added lines in 3 files covered. (94.12%)

6 existing lines in 1 file now uncovered.

3038 of 3299 relevant lines covered (92.09%)

9.08 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, Union[str, z3.ExprRef]]

    def __init__(self, node: astroid.NodeNG, types=None):
        if types is None:
            types = {}
        self.types = types
        self.node = node

        if not isinstance(node, astroid.NodeNG):
            raise ValueError("'node' must be a valid astroid node")

        # extract expression out of expression statement
        if isinstance(node, (astroid.Expr, astroid.Assign)):
            self.node = node.value

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

pyta-uoft / pyta / 10308526715

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