8849617014

Committed 26 Apr 2024 02:11PM UTC coverage: 89.827% (-6.0%) from 95.841%

Build # 8849617014

Build Type

push

github

Committed by

web-flow

Commit Message

Fixed infinite recursion in representation invariants with method calls (#1031)

Run Details

15 of 17 new or added lines in 1 file covered. (88.24%)

165 existing lines in 15 files now uncovered.

2746 of 3057 relevant lines covered (89.83%)

8.85 hits per line

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

85.71

/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) -> 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)
        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,
        }
        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: 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
            else:
                raise Z3ParseException(f"Unhandled binary operation {op}.")
        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)

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) -> 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	else:
56	raise Z3ParseException(f"Unhandled node type {type(node)}.")	×
57
58	return node	10✔
59
60	def apply_name(self, name: str) -> z3.ExprRef:	10✔
61	"""
62	Set up the appropriate variable representation in Z3 based on name and type.
63	If an error is encountered or a case is unconsidered, return None.
64	"""
65	typ = self.types[name]	10✔
66	type_to_z3 = {	10✔
67	"int": z3.Int,
68	"float": z3.Real,
69	"bool": z3.Bool,
70	}
71	if typ in type_to_z3:	10✔
72	x = type_to_z3[typ](name)	10✔
73	else:
74	raise Z3ParseException(f"Unhandled type {typ}.")	×
75
76	return x	10✔
77
78	def parse_compare(self, node: astroid.Compare) -> z3.ExprRef:	10✔
79	"""Convert an astroid Compare node to z3 expression."""
80	left, ops = node.left, node.ops	10✔
81	left = self.reduce(left)	10✔
82	for item in ops:	10✔
83	op, right = item	10✔
84	right = self.reduce(right)	10✔
85	left = self.apply_bin_op(left, op, right)	10✔
86	return left	10✔
87
88	def apply_unary_op(self, left: z3.ExprRef, op: str) -> z3.ExprRef:	10✔
89	"""Apply z3 unary operation indicated by op."""
90	op_to_z3 = {	10✔
91	"not": z3.Not,
92	}
93	if op in op_to_z3:	10✔
94	left = op_to_z3[op](left)	10✔
95	else:
96	raise Z3ParseException(f"Unhandled unary operation {op}.")	×
97
98	return left	10✔
99
100	def apply_bin_op(self, left: z3.ExprRef, op: str, right: z3.ExprRef) -> z3.ExprRef:	10✔
101	"""Given left, right, op, apply the binary operation."""
102	try:	10✔
103	if op == "+":	10✔
104	return left + right	10✔
105	elif op == "-":	10✔
UNCOV 106	return left - right	×
107	elif op == "*":	10✔
UNCOV 108	return left * right	×
109	elif op == "/":	10✔
UNCOV 110	return left / right	×
111	elif op == "**":	10✔
112	return left**right	10✔
113	elif op == "==":	10✔
114	return left == right	10✔
115	elif op == "<=":	10✔
UNCOV 116	return left <= right	×
117	elif op == ">=":	10✔
UNCOV 118	return left >= right	×
119	elif op == "<":	10✔
UNCOV 120	return left < right	×
121	elif op == ">":	10✔
122	return left > right	10✔
123	else:
UNCOV 124	raise Z3ParseException(f"Unhandled binary operation {op}.")	×
UNCOV 125	except TypeError:	×
UNCOV 126	raise Z3ParseException(f"Operation {op} incompatible with types {left} and {right}.")	×
127
128	def apply_bool_op(self, op: str, values: Union[z3.ExprRef, List[z3.ExprRef]]) -> z3.ExprRef:	10✔
129	"""Apply boolean operation given by op to values."""
130	op_to_z3 = {	10✔
131	"and": z3.And,
132	"or": z3.Or,
133	"not": z3.Not,
134	}
135	if op in op_to_z3:	10✔
136	value = op_to_z3[op](values)	10✔
137	else:
138	raise Z3ParseException(f"Unhandled boolean operation {op}.")	×
139
140	return value	10✔
141
142	def parse_unary_op(self, node: astroid.UnaryOp) -> z3.ExprRef:	10✔
143	"""Convert an astroid UnaryOp node to a z3 expression."""
144	left, op = node.operand, node.op	10✔
145	left = self.reduce(left)	10✔
146
147	return self.apply_unary_op(left, op)	10✔
148
149	def parse_bin_op(self, node: astroid.BinOp) -> z3.ExprRef:	10✔
150	"""Convert an astroid BinOp node to a z3 expression."""
151	left, op, right = node.left, node.op, node.right	10✔
152	left = self.reduce(left)	10✔
153	right = self.reduce(right)	10✔
154
155	return self.apply_bin_op(left, op, right)	10✔
156
157	def parse_bool_op(self, node: astroid.BoolOp) -> z3.ExprRef:	10✔
158	"""Convert an astroid BoolOp node to a z3 expression."""
159	op, values = node.op, node.values	10✔
160	values = [self.reduce(x) for x in values]	10✔
161
162	return self.apply_bool_op(op, values)	10✔

pyta-uoft / pyta / 8849617014

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