9331718888

Committed 01 Jun 2024 04:36PM UTC coverage: 89.501% (-3.6%) from 93.12%

Build # 9331718888

Build Type

Pull #1046

github

Committed by

web-flow

Commit Message

Merge c10a81ea8 into b702c5d9d

Pull Request Pull Request #1046: Fix GitHub Action Tests

Run Details

2745 of 3067 relevant lines covered (89.5%)

8.81 hits per line

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

21.43

/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	×
31	if types is None:	×
32	types = {}	×
33	self.types = types	×
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:	×
41	node = self.node	×
42
43	if isinstance(node, nodes.BoolOp):	×
44	node = self.parse_bool_op(node)	×
45	elif isinstance(node, nodes.UnaryOp):	×
46	node = self.parse_unary_op(node)	×
47	elif isinstance(node, nodes.Compare):	×
48	node = self.parse_compare(node)	×
49	elif isinstance(node, nodes.BinOp):	×
50	node = self.parse_bin_op(node)	×
51	elif isinstance(node, nodes.Const):	×
52	node = node.value	×
53	elif isinstance(node, nodes.Name):	×
54	node = self.apply_name(node.name)	×
55	else:
56	raise Z3ParseException(f"Unhandled node type {type(node)}.")	×
57
58	return node	×
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]	×
66	type_to_z3 = {	×
67	"int": z3.Int,
68	"float": z3.Real,
69	"bool": z3.Bool,
70	}
71	if typ in type_to_z3:	×
72	x = type_to_z3[typ](name)	×
73	else:
74	raise Z3ParseException(f"Unhandled type {typ}.")	×
75
76	return x	×
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	×
81	left = self.reduce(left)	×
82	for item in ops:	×
83	op, right = item	×
84	right = self.reduce(right)	×
85	left = self.apply_bin_op(left, op, right)	×
86	return left	×
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 = {	×
91	"not": z3.Not,
92	}
93	if op in op_to_z3:	×
94	left = op_to_z3[op](left)	×
95	else:
96	raise Z3ParseException(f"Unhandled unary operation {op}.")	×
97
98	return left	×
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:	×
103	if op == "+":	×
104	return left + right	×
105	elif op == "-":	×
106	return left - right	×
107	elif op == "*":	×
108	return left * right	×
109	elif op == "/":	×
110	return left / right	×
111	elif op == "**":	×
112	return left**right	×
113	elif op == "==":	×
114	return left == right	×
115	elif op == "<=":	×
116	return left <= right	×
117	elif op == ">=":	×
118	return left >= right	×
119	elif op == "<":	×
120	return left < right	×
121	elif op == ">":	×
122	return left > right	×
123	else:
124	raise Z3ParseException(f"Unhandled binary operation {op}.")	×
125	except TypeError:	×
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 = {	×
131	"and": z3.And,
132	"or": z3.Or,
133	"not": z3.Not,
134	}
135	if op in op_to_z3:	×
136	value = op_to_z3[op](values)	×
137	else:
138	raise Z3ParseException(f"Unhandled boolean operation {op}.")	×
139
140	return value	×
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	×
145	left = self.reduce(left)	×
146
147	return self.apply_unary_op(left, op)	×
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	×
152	left = self.reduce(left)	×
153	right = self.reduce(right)	×
154
155	return self.apply_bin_op(left, op, right)	×
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	×
160	values = [self.reduce(x) for x in values]	×
161
162	return self.apply_bool_op(op, values)	×

pyta-uoft / pyta / 9331718888

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