19300648625

Committed 12 Nov 2025 02:22PM UTC coverage: 93.909% (-0.4%) from 94.325%

Build # 19300648625

Build Type

push

github

Committed by

web-flow

Commit Message

Optimized performance for 'test_examples.py' (#1251)

Run Details

8 of 8 new or added lines in 2 files covered. (100.0%)

16 existing lines in 7 files now uncovered.

3515 of 3743 relevant lines covered (93.91%)

17.81 hits per line

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

92.31

/python_ta/checkers/condition_logic_checker.py

"""
Check for redundant/impossible If or While conditions in functions based on z3 constraints
"""

from __future__ import annotations

from typing import TYPE_CHECKING, Any, Union

from pylint.checkers import BaseChecker
from pylint.checkers.utils import only_required_for_messages

if TYPE_CHECKING:
    from astroid import nodes
    from pylint.lint import PyLinter

    try:
        from z3 import ExprRef

    except ImportError:
        ExprRef = Any


class ConditionLogicChecker(BaseChecker):
    name = "redundant-condition"
    msgs = {
        "R9900": (
            """This condition will always evaluate to True.""",
            "redundant-condition",
            "Used when an If or While statement is always True. Requires the z3 configuration option to be True.",
        ),
        "R9901": (
            """This condition will always evaluate to False.""",
            "impossible-condition",
            "Used when an If or While statement is always False. Requires the z3 configuration option to be True.",
        ),
    }
    options = (
        (
            "z3",
            {
                "default": False,
                "type": "yn",
                "metavar": "<y or n>",
                "help": "Use Z3 to perform logical feasibility analysis in program control flow.",
            },
        ),
    )

    @only_required_for_messages("redundant-condition", "impossible-condition")
    def visit_if(self, node: nodes.If) -> None:
        """Visit if statement"""
        self._check_condition(node)

    @only_required_for_messages("redundant-condition", "impossible-condition")
    def visit_while(self, node: nodes.While) -> None:
        """Visit while statement"""
        self._check_condition(node)

    def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None:
        """Check whether a condition in an `if` or `while` statement is redundant
        or impossible based on the feasible execution paths.

        - A condition is redundant if for every feasible execution path
        leading to the node, the condition must be True due to precedent constraints.
        - A condition is impossible if for every feasible execution path
        leading to the node, the condition must be False due to precedent constraints.
        """
        if not hasattr(node, "cfg_block") or not self.linter.config.z3:
            return

        # Then z3 option is enabled
        try:
            import z3

            from ..cfg.graph import Z3Environment
        except ImportError:
            return

        node_block = node.cfg_block

        # create node condition z3 constraint
        condition_node = node.test
        env = Z3Environment(node.frame().cfg.z3_vars, [])
        z3_condition = env.parse_constraint(condition_node)

        if z3_condition is None:
            return

        if all(
            self._check_unsat(z3.And(*constraints), z3.Not(z3_condition))
            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
            for constraints in edge.z3_constraints.values()
        ):
            self.add_message("redundant-condition", node=node.test)

        if all(
            self._check_unsat(z3.And(*constraints), z3_condition)
            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
            for constraints in edge.z3_constraints.values()
        ):
            self.add_message("impossible-condition", node=node.test)

    def _check_unsat(self, prev_constraints: ExprRef, node_constraint: ExprRef) -> bool:
        """Check if the conjunction of the given constraints is unsatisfiable.

        - prev_constraints (z3.ExprRef): Constraints from previous nodes.
        - node_constraint (z3.ExprRef): The condition to check at the current node.
        """
        # z3 is already imported by caller (cached), no need to check for ImportError again
        import z3

        solver = z3.Solver()
        solver.add(z3.And(prev_constraints, node_constraint))
        return solver.check() == z3.unsat


def register(linter: PyLinter) -> None:
    """Required method to auto-register this checker to the linter."""
    linter.register_checker(ConditionLogicChecker(linter))

1	"""
2	Check for redundant/impossible If or While conditions in functions based on z3 constraints
3	"""
4
5	from __future__ import annotations	20✔
6
7	from typing import TYPE_CHECKING, Any, Union	20✔
8
9	from pylint.checkers import BaseChecker	20✔
10	from pylint.checkers.utils import only_required_for_messages	20✔
11
12	if TYPE_CHECKING:
13	from astroid import nodes
14	from pylint.lint import PyLinter
15
16	try:
17	from z3 import ExprRef
18
19	except ImportError:
20	ExprRef = Any
21
22
23	class ConditionLogicChecker(BaseChecker):	20✔
24	name = "redundant-condition"	20✔
25	msgs = {	20✔
26	"R9900": (
27	"""This condition will always evaluate to True.""",
28	"redundant-condition",
29	"Used when an If or While statement is always True. Requires the z3 configuration option to be True.",
30	),
31	"R9901": (
32	"""This condition will always evaluate to False.""",
33	"impossible-condition",
34	"Used when an If or While statement is always False. Requires the z3 configuration option to be True.",
35	),
36	}
37	options = (	20✔
38	(
39	"z3",
40	{
41	"default": False,
42	"type": "yn",
43	"metavar": "<y or n>",
44	"help": "Use Z3 to perform logical feasibility analysis in program control flow.",
45	},
46	),
47	)
48
49	@only_required_for_messages("redundant-condition", "impossible-condition")	20✔
50	def visit_if(self, node: nodes.If) -> None:	20✔
51	"""Visit if statement"""
52	self._check_condition(node)	20✔
53
54	@only_required_for_messages("redundant-condition", "impossible-condition")	20✔
55	def visit_while(self, node: nodes.While) -> None:	20✔
56	"""Visit while statement"""
57	self._check_condition(node)	20✔
58
59	def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None:	20✔
60	"""Check whether a condition in an `if` or `while` statement is redundant
61	or impossible based on the feasible execution paths.
62
63	- A condition is redundant if for every feasible execution path
64	leading to the node, the condition must be True due to precedent constraints.
65	- A condition is impossible if for every feasible execution path
66	leading to the node, the condition must be False due to precedent constraints.
67	"""
68	if not hasattr(node, "cfg_block") or not self.linter.config.z3:	20✔
69	return	20✔
70
71	# Then z3 option is enabled
72	try:	10✔
73	import z3	10✔
74
75	from ..cfg.graph import Z3Environment	10✔
UNCOV 76	except ImportError:	×
UNCOV 77	return	×
78
79	node_block = node.cfg_block	10✔
80
81	# create node condition z3 constraint
82	condition_node = node.test	10✔
83	env = Z3Environment(node.frame().cfg.z3_vars, [])	10✔
84	z3_condition = env.parse_constraint(condition_node)	10✔
85
86	if z3_condition is None:	10✔
UNCOV 87	return	×
88
89	if all(	10✔
90	self._check_unsat(z3.And(*constraints), z3.Not(z3_condition))
91	for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
92	for constraints in edge.z3_constraints.values()
93	):
94	self.add_message("redundant-condition", node=node.test)	10✔
95
96	if all(	10✔
97	self._check_unsat(z3.And(*constraints), z3_condition)
98	for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
99	for constraints in edge.z3_constraints.values()
100	):
101	self.add_message("impossible-condition", node=node.test)	10✔
102
103	def _check_unsat(self, prev_constraints: ExprRef, node_constraint: ExprRef) -> bool:	20✔
104	"""Check if the conjunction of the given constraints is unsatisfiable.
105
106	- prev_constraints (z3.ExprRef): Constraints from previous nodes.
107	- node_constraint (z3.ExprRef): The condition to check at the current node.
108	"""
109	# z3 is already imported by caller (cached), no need to check for ImportError again
110	import z3	10✔
111
112	solver = z3.Solver()	10✔
113	solver.add(z3.And(prev_constraints, node_constraint))	10✔
114	return solver.check() == z3.unsat	10✔
115
116
117	def register(linter: PyLinter) -> None:	20✔
118	"""Required method to auto-register this checker to the linter."""
119	linter.register_checker(ConditionLogicChecker(linter))	20✔

pyta-uoft / pyta / 19300648625

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