9338502324

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

Build # 9338502324

Build Type

Pull #1046

github

Committed by

web-flow

Commit Message

Merge 8c2fede6e into d04089e06

Pull Request Pull Request #1046: Fix GitHub Action Tests

Run Details

2745 of 3067 relevant lines covered (89.5%)

14.09 hits per line

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

27.78

/python_ta/transforms/z3_visitor.py

import astroid
from astroid import Uninferable, nodes
from astroid.transforms import TransformVisitor
from z3.z3types import Z3Exception

from ..contracts import parse_assertions
from .ExprWrapper import ExprWrapper, Z3ParseException


class Z3Visitor:
    """
    The class responsible for visiting astroid nodes (currently only FunctionDef nodes),
    parsing preconditions, and converting them to z3 expressions to be appended in the
    z3_constraints attribute of the node.
    """

    def __init__(self):
        """Return a TransformVisitor that sets an environment for every node."""
        visitor = TransformVisitor()
        # Register transforms
        visitor.register_transform(nodes.FunctionDef, self.set_function_def_z3_constraints)
        self.visitor = visitor

    def set_function_def_z3_constraints(self, node: nodes.FunctionDef):
        # Parse types
        types = {}
        annotations = node.args.annotations
        arguments = node.args.args
        for ann, arg in zip(annotations, arguments):
            if ann is None:
                continue
            # TODO: what to do about subscripts ex. Set[int], List[Set[int]], ...
            inferred = ann.inferred()
            if len(inferred) > 0 and inferred[0] is not Uninferable:
                if isinstance(inferred[0], nodes.ClassDef):
                    types[arg.name] = inferred[0].name
        # Parse preconditions
        preconditions = parse_assertions(node, parse_token="Precondition")
        # Get z3 constraints
        z3_constraints = []
        for pre in preconditions:
            pre = astroid.parse(pre).body[0]
            ew = ExprWrapper(pre, types)
            try:
                transformed = ew.reduce()
            except (Z3Exception, Z3ParseException):
                transformed = None
            if transformed is not None:
                z3_constraints.append(transformed)
        # Set z3 constraints
        node.z3_constraints = z3_constraints
        return node

1	import astroid	16✔
2	from astroid import Uninferable, nodes	16✔
3	from astroid.transforms import TransformVisitor	16✔
4	from z3.z3types import Z3Exception	16✔
5
6	from ..contracts import parse_assertions	16✔
7	from .ExprWrapper import ExprWrapper, Z3ParseException	16✔
8
9
10	class Z3Visitor:	16✔
11	"""	8✔
12	The class responsible for visiting astroid nodes (currently only FunctionDef nodes),
13	parsing preconditions, and converting them to z3 expressions to be appended in the
14	z3_constraints attribute of the node.
15	"""
16
17	def __init__(self):	16✔
18	"""Return a TransformVisitor that sets an environment for every node."""
19	visitor = TransformVisitor()	×
20	# Register transforms
21	visitor.register_transform(nodes.FunctionDef, self.set_function_def_z3_constraints)	×
22	self.visitor = visitor	×
23
24	def set_function_def_z3_constraints(self, node: nodes.FunctionDef):	16✔
25	# Parse types
26	types = {}	×
27	annotations = node.args.annotations	×
28	arguments = node.args.args	×
29	for ann, arg in zip(annotations, arguments):	×
30	if ann is None:	×
31	continue	×
32	# TODO: what to do about subscripts ex. Set[int], List[Set[int]], ...
33	inferred = ann.inferred()	×
34	if len(inferred) > 0 and inferred[0] is not Uninferable:	×
35	if isinstance(inferred[0], nodes.ClassDef):	×
36	types[arg.name] = inferred[0].name	×
37	# Parse preconditions
38	preconditions = parse_assertions(node, parse_token="Precondition")	×
39	# Get z3 constraints
40	z3_constraints = []	×
41	for pre in preconditions:	×
42	pre = astroid.parse(pre).body[0]	×
43	ew = ExprWrapper(pre, types)	×
44	try:	×
45	transformed = ew.reduce()	×
46	except (Z3Exception, Z3ParseException):	×
47	transformed = None	×
48	if transformed is not None:	×
49	z3_constraints.append(transformed)	×
50	# Set z3 constraints
51	node.z3_constraints = z3_constraints	×
52	return node	×

pyta-uoft / pyta / 9338502324

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