15791974148

Committed 21 Jun 2025 04:11AM UTC coverage: 92.849% (+0.03%) from 92.821%

Build # 15791974148

Build Type

Pull #1190

github

Committed by

web-flow

Commit Message

Merge b652ed720 into 02ddeab02

Pull Request Pull Request #1190: Simplify Combined Z3 Preconditions in z3_visitor.py Using z3.simplify

Coverage Stats

4 of 4 new or added lines in 1 file covered. (100.0%)

26 existing lines in 5 files now uncovered.

3428 of 3692 relevant lines covered (92.85%)

17.54 hits per line

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

95.45

/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

try:
    import z3

    from ..cfg.graph import Z3Environment

    z3_dependency_available = True
except ImportError:
    z3 = Any
    Z3Environment = Any
    z3_dependency_available = False

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


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

pyta-uoft / pyta / 15791974148

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