From e30f7fa307d532c7b5d1b81e25c281c882e0facb Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Fri, 8 Nov 2024 00:26:12 -0500 Subject: [PATCH 01/23] feat: implement basic checker feature Implement feature for redundant_condition_checker Refactor z3 constraints traverse in CFG module Create unit tests for redundant_condition_checker --- python_ta/cfg/graph.py | 62 ++++--- .../checkers/redundant_condition_checker.py | 88 ++++++++++ .../test_redundant_condition_checker.py | 152 ++++++++++++++++++ 3 files changed, 277 insertions(+), 25 deletions(-) create mode 100644 python_ta/checkers/redundant_condition_checker.py create mode 100644 tests/test_custom_checkers/test_redundant_condition_checker.py diff --git a/python_ta/cfg/graph.py b/python_ta/cfg/graph.py index f442b6bb8..f8ee79f5f 100644 --- a/python_ta/cfg/graph.py +++ b/python_ta/cfg/graph.py @@ -286,29 +286,31 @@ def update_edge_z3_constraints(self) -> None: # traverse through edge if edge.condition is not None: condition_z3_constraint = z3_environment.parse_constraint(edge.condition) - if condition_z3_constraint is not None: - if edge.negate is not None: - z3_environment.add_constraint( - Not(condition_z3_constraint) - if edge.negate - else condition_z3_constraint - ) - - edge.z3_constraints[path_id] = z3_environment.update_constraints() + if condition_z3_constraint is not None and edge.negate is not None: + z3_environment.add_constraint( + Not(condition_z3_constraint) if edge.negate else condition_z3_constraint + ) + # add z3 constraint to the CFG block of condition node + edge.source.z3_constraint = z3_environment.assign_constraint( + condition_z3_constraint + ) + + # update edge z3 constraints + edge.z3_constraints[path_id] = z3_environment.assign_current_constraints() # traverse into target node - for node in edge.target.statements: - if isinstance(node, (Assign, AugAssign, AnnAssign)): - self._handle_variable_reassignment(node, z3_environment) + for stmt in edge.target.statements: + if isinstance(stmt, (Assign, AugAssign, AnnAssign)): + self._handle_variable_reassignment(stmt, z3_environment) def _handle_variable_reassignment(self, node: NodeNG, env: Z3Environment) -> None: """Check for reassignment statements and invoke Z3 environment""" if isinstance(node, Assign): for target in node.targets: if isinstance(target, AssignName): - env.assign(target.name) + env.handle_variable_assignment(target.name) elif isinstance(node, (AugAssign, AnnAssign)): - env.assign(node.target.name) + env.handle_variable_assignment(node.target.name) def update_edge_feasibility(self) -> None: """Traverse through edges in DFS order and update is_feasible @@ -346,6 +348,8 @@ class CFGBlock: successors: List[CFGEdge] # Whether there exists a path from the start block to this block. reachable: bool + # the z3 constraint associated with a conditional statement + z3_constraint: Optional[ExprRef] def __init__(self, id_: int) -> None: """Initialize a new CFGBlock.""" @@ -447,23 +451,27 @@ def __init__(self, variables: Dict[str, ExprRef], constraints: List[ExprRef]) -> self.variables = variables self.constraints = constraints.copy() - def assign(self, name: str) -> None: + def handle_variable_assignment(self, name: str) -> None: """Handle a variable assignment statement""" if name in self.variable_unassigned: self.variable_unassigned[name] = False - def update_constraints(self) -> List[ExprRef]: - """Returns all z3 constraints in the environments + def assign_constraint(self, constraint: ExprRef) -> Optional[ExprRef]: + """Returns the given z3 constraints if it + does not contain reassigned variables + """ + if self._check_variables_unassigned(constraint): + return constraint + return None + + def assign_current_constraints(self) -> List[ExprRef]: + """Returns all z3 constraints in the current environment Removes constraints with reassigned variables """ updated_constraints = [] for constraint in self.constraints: # discard expressions with reassigned variables - variables = _get_vars(constraint) - reassigned = any( - not self.variable_unassigned.get(variable, False) for variable in variables - ) - if not reassigned: + if self._check_variables_unassigned(constraint): updated_constraints.append(constraint) self.constraints = updated_constraints @@ -474,15 +482,19 @@ def add_constraint(self, constraint: ExprRef) -> None: self.constraints.append(constraint) def parse_constraint(self, node: NodeNG) -> Optional[ExprRef]: - """Parse an Astroid node to a Z3 constraint - Return the resulting expression - """ + """Parse an Astroid node to a Z3 constraint. Return the resulting expression""" parser = Z3Parser(self.variables) try: return parser.parse(node) except (Z3Exception, Z3ParseException): return None + def _check_variables_unassigned(self, constraint: ExprRef) -> bool: + """Return True if all variables in the z3 constraint have not been reassigned""" + return all( + self.variable_unassigned.get(variable, True) for variable in _get_vars(constraint) + ) + def _get_vars(expr: ExprRef) -> Set[str]: """Retrieve all z3 variables from a z3 expression""" diff --git a/python_ta/checkers/redundant_condition_checker.py b/python_ta/checkers/redundant_condition_checker.py new file mode 100644 index 000000000..96934d664 --- /dev/null +++ b/python_ta/checkers/redundant_condition_checker.py @@ -0,0 +1,88 @@ +""" +Check for redundant If or While conditions in functions based on z3 constraints +""" + +from typing import Any + +try: + import z3 + + z3_dependency_available = True +except ImportError: + z3 = Any + z3_dependency_available = False + +from astroid import nodes +from pylint.checkers import BaseChecker +from pylint.checkers.utils import only_required_for_messages +from pylint.lint import PyLinter + + +class RedundantConditionChecker(BaseChecker): + name = "redundant-condition" + msgs = { + "R9900": ( + """Condition is already true given the preceding code; consider removing redundant check.""", + "redundant-condition", + "Used when an If and While statements is tautologically true based on preceding Z3 constraints." + " Enabled when Z3 option is on.", + ), + } + options = ( + ( + "z3", + { + "default": False, + "type": "yn", + "metavar": "", + "help": "Use Z3 to restrict control flow checks to paths that are logically feasible.", + }, + ), + ) + + def __init__(self, linter=None) -> None: + super().__init__(linter=linter) + + @only_required_for_messages("redundant-condition") + def visit_if(self, node: nodes.If) -> None: + """Visit if statement""" + if self._check_redundant_condition(node): + self.add_message("redundant-condition", node=node) + + @only_required_for_messages("redundant-condition") + def visit_while(self, node: nodes.While) -> None: + """Visit while statement""" + if self._check_redundant_condition(node): + self.add_message("redundant-condition", node=node) + + def _check_redundant_condition(self, node: nodes.If | nodes.While) -> bool: + """A condition statement is redundant if for every feasible execution path + leading to the node, the condition must be True by precedent constraints + """ + if not z3_dependency_available or not hasattr(node, "cfg_block"): + return False + + node_block = node.cfg_block + + if not node_block.is_feasible or node_block.z3_constraint is None: + return False + + solver = z3.Solver() + for pred in node_block.predecessors: + for constraints in pred.z3_constraints.values(): + solver.push() + prev_constraints = z3.And(*[c for c in constraints]) + solver.add(z3.And(node_block.z3_constraint, prev_constraints) != prev_constraints) + if solver.check() == z3.sat: + return False + solver.pop() + + return True + + +def register(linter: PyLinter) -> None: + """Required method to auto-register this checker to the linter, + Register the linter only if `z3` option is turned on. + """ + if linter.config.z3: + linter.register_checker(RedundantConditionChecker(linter)) diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py new file mode 100644 index 000000000..ce1181257 --- /dev/null +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -0,0 +1,152 @@ +import astroid +import pylint.testutils +from astroid import nodes + +from python_ta.cfg import CFGVisitor +from python_ta.checkers.redundant_condition_checker import RedundantConditionChecker +from python_ta.transforms.z3_visitor import Z3Visitor + + +class TestRedundantConditionChecker(pylint.testutils.CheckerTestCase): + CHECKER_CLASS = RedundantConditionChecker + CONFIG = {"z3": True} + + def test_redundant_by_precondition(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x > 10 + ''' + if x > 5: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_redundant_by_if_condition(self): + src = """ + def func(x: int): + if x > 5: + if x > 3: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_redundant_by_while_condition(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x > 10 + ''' + while x > 0: + if x != 0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_not_redundant_condition(self): + src = """ + def func(x: str): + ''' + Preconditions: + - x[0:2] == "ab" + ''' + if x != "abc": + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + def test_partially_redundant_condition(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x > 10 + ''' + if x > 10 and x < 15: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + def test_redundant_condition_partial_paths(self): + src = """ + def func(x: int, y: bool): + ''' + Preconditions: + - x > 10 + ''' + if not y: + x = -1 + if x > 0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + def test_not_redundant_by_reassignment(self): + src = """ + def func(x: float): + ''' + Preconditions: + - x in [1.0, 2.0] + ''' + x = None + if x == 1.0 or x == 2.0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + +# inspiration: check if the reassigned variable has the same type as previous one +# if yes, update the variable value in Z3Environment and continue using it in CFG traverse From 0f173f618f9cb525151d849928f22d0df6593551 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Thu, 14 Nov 2024 12:28:58 -0500 Subject: [PATCH 02/23] feat: implement impossible-condition-checker Implement checker for impossible condition Refactor checker for redundant condition Add more unit tests for redundant and impossible condition Create examples for redundant and impossible condition --- CHANGELOG.md | 2 + .../r9900_redundant_condition.py | 16 ++ .../r9901_impossible_condition.py | 13 + .../checkers/redundant_condition_checker.py | 88 ------ ...dundant_or_impossible_condition_checker.py | 114 ++++++++ .../test_impossible_condition_checker.py | 266 ++++++++++++++++++ .../test_redundant_condition_checker.py | 82 +++++- 7 files changed, 486 insertions(+), 95 deletions(-) create mode 100644 examples/custom_checkers/r9900_redundant_condition.py create mode 100644 examples/custom_checkers/r9901_impossible_condition.py delete mode 100644 python_ta/checkers/redundant_condition_checker.py create mode 100644 python_ta/checkers/redundant_or_impossible_condition_checker.py create mode 100644 tests/test_custom_checkers/test_impossible_condition_checker.py diff --git a/CHANGELOG.md b/CHANGELOG.md index 7615cdd54..44bf2f0dc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,8 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### 💫 New checkers - `unmentioned-parameter`: Provide error message when a function parameter is not mentioned by name in the function's docstring. By default, this checker is disabled. +- `redundant-condition`: Provide error message when a conditional statement within a function is guaranteed true given the precedent statements. This checker is enabled only when `z3` option is turned on. +- `impossible-condition`: Provide error message when a conditional statement within a function contradicts the precedent statements. This checker is enabled only when `z3` option is turned on. ### 🐛 Bug fixes diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py new file mode 100644 index 000000000..423f73e4b --- /dev/null +++ b/examples/custom_checkers/r9900_redundant_condition.py @@ -0,0 +1,16 @@ +def return_large_number(x: int) -> int: + """ + Preconditions + - x > 1000 + """ + if x > 1000: + return x + else: # the else branch is redundant given the function preconditions + return 1000 + + +def nested_condition(x: int) -> int: + if x > 10: + if x > 5: + return x + return 0 diff --git a/examples/custom_checkers/r9901_impossible_condition.py b/examples/custom_checkers/r9901_impossible_condition.py new file mode 100644 index 000000000..b56e4ba24 --- /dev/null +++ b/examples/custom_checkers/r9901_impossible_condition.py @@ -0,0 +1,13 @@ +def print_natural_number(x: int): + """ + Preconditions: + - x >= 0 + """ + if x < 0: + raise Exception("x is not an integer") + print(x) + + +def invalid_condition(x: bool): + if x and not x: + print("impossible") diff --git a/python_ta/checkers/redundant_condition_checker.py b/python_ta/checkers/redundant_condition_checker.py deleted file mode 100644 index 96934d664..000000000 --- a/python_ta/checkers/redundant_condition_checker.py +++ /dev/null @@ -1,88 +0,0 @@ -""" -Check for redundant If or While conditions in functions based on z3 constraints -""" - -from typing import Any - -try: - import z3 - - z3_dependency_available = True -except ImportError: - z3 = Any - z3_dependency_available = False - -from astroid import nodes -from pylint.checkers import BaseChecker -from pylint.checkers.utils import only_required_for_messages -from pylint.lint import PyLinter - - -class RedundantConditionChecker(BaseChecker): - name = "redundant-condition" - msgs = { - "R9900": ( - """Condition is already true given the preceding code; consider removing redundant check.""", - "redundant-condition", - "Used when an If and While statements is tautologically true based on preceding Z3 constraints." - " Enabled when Z3 option is on.", - ), - } - options = ( - ( - "z3", - { - "default": False, - "type": "yn", - "metavar": "", - "help": "Use Z3 to restrict control flow checks to paths that are logically feasible.", - }, - ), - ) - - def __init__(self, linter=None) -> None: - super().__init__(linter=linter) - - @only_required_for_messages("redundant-condition") - def visit_if(self, node: nodes.If) -> None: - """Visit if statement""" - if self._check_redundant_condition(node): - self.add_message("redundant-condition", node=node) - - @only_required_for_messages("redundant-condition") - def visit_while(self, node: nodes.While) -> None: - """Visit while statement""" - if self._check_redundant_condition(node): - self.add_message("redundant-condition", node=node) - - def _check_redundant_condition(self, node: nodes.If | nodes.While) -> bool: - """A condition statement is redundant if for every feasible execution path - leading to the node, the condition must be True by precedent constraints - """ - if not z3_dependency_available or not hasattr(node, "cfg_block"): - return False - - node_block = node.cfg_block - - if not node_block.is_feasible or node_block.z3_constraint is None: - return False - - solver = z3.Solver() - for pred in node_block.predecessors: - for constraints in pred.z3_constraints.values(): - solver.push() - prev_constraints = z3.And(*[c for c in constraints]) - solver.add(z3.And(node_block.z3_constraint, prev_constraints) != prev_constraints) - if solver.check() == z3.sat: - return False - solver.pop() - - return True - - -def register(linter: PyLinter) -> None: - """Required method to auto-register this checker to the linter, - Register the linter only if `z3` option is turned on. - """ - if linter.config.z3: - linter.register_checker(RedundantConditionChecker(linter)) diff --git a/python_ta/checkers/redundant_or_impossible_condition_checker.py b/python_ta/checkers/redundant_or_impossible_condition_checker.py new file mode 100644 index 000000000..af8932cb4 --- /dev/null +++ b/python_ta/checkers/redundant_or_impossible_condition_checker.py @@ -0,0 +1,114 @@ +""" +Check for redundant If or While conditions in functions based on z3 constraints +""" + +from typing import Any + +try: + import z3 + + z3_dependency_available = True +except ImportError: + z3 = Any + z3_dependency_available = False + +from astroid import nodes +from pylint.checkers import BaseChecker +from pylint.checkers.utils import only_required_for_messages +from pylint.lint import PyLinter + + +class RedundantOrImpossibleConditionChecker(BaseChecker): + name = "redundant-condition" + msgs = { + "R9900": ( + """This conditional statement is already true given the preceding code; + consider removing redundant check.""", + "redundant-condition", + "Used when an If or While statement is tautologically true based on preceding Z3 constraints." + " Enabled when Z3 option is on.", + ), + "R9901": ( + """This conditional statement is never true given the preceding code.""", + "impossible-condition", + "Used when an If or While statement contradicts preceding Z3 constraints. Enable when Z3 option is on.", + ), + } + options = ( + ( + "z3", + { + "default": False, + "type": "yn", + "metavar": "", + "help": "Use Z3 to perform logical feasibility analysis in program control flow.", + }, + ), + ) + + def __init__(self, linter=None) -> None: + super().__init__(linter=linter) + + @only_required_for_messages("redundant-condition", "impossible-condition") + def visit_if(self, node: nodes.If) -> None: + """Visit if statement""" + self._check_condition(node) + # handle else branch + + @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: nodes.If | nodes.While) -> None: + """A condition statement is redundant if for every feasible execution path + leading to the node, the condition must be True by precedent constraints. + """ + if not z3_dependency_available or not hasattr(node, "cfg_block"): + return + + node_block = node.cfg_block + + if not node_block.is_feasible or node_block.z3_constraint is None: + return + + for pred in node_block.predecessors: + if all( + self._check_redundant_condition( + z3.And(*[c for c in constraints]), node_block.z3_constraint + ) + for constraints in pred.z3_constraints.values() + ): + self.add_message("redundant-condition", node=node) + if all( + self._check_impossible_condition( + z3.And(*[c for c in constraints]), node_block.z3_constraint + ) + for constraints in pred.z3_constraints.values() + ): + self.add_message("impossible-condition", node=node) + + def _check_redundant_condition( + self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef + ) -> bool: + """Check if the condition is redundant.""" + solver = z3.Solver() + solver.add(z3.And(prev_constraints, node_constraint) != prev_constraints) + return solver.check() == z3.unsat + + def _check_impossible_condition( + self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef + ) -> bool: + """Check if the condition is impossible.""" + solver = z3.Solver() + solver.add(prev_constraints) + solver.add(node_constraint) + return solver.check() == z3.unsat + + +def register(linter: PyLinter) -> None: + """Required method to auto-register this checker to the linter, + Register the linter only if `z3` option is turned on. + """ + if linter.config.z3: + linter.register_checker(RedundantOrImpossibleConditionChecker(linter)) diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py new file mode 100644 index 000000000..a3c482ec6 --- /dev/null +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -0,0 +1,266 @@ +import astroid +import pylint.testutils +from astroid import nodes + +from python_ta.cfg import CFGVisitor +from python_ta.checkers.redundant_or_impossible_condition_checker import ( + RedundantOrImpossibleConditionChecker, +) +from python_ta.transforms.z3_visitor import Z3Visitor + + +class TestImpossibleConditionChecker(pylint.testutils.CheckerTestCase): + CHECKER_CLASS = RedundantOrImpossibleConditionChecker + CONFIG = {"z3": True} + + def test_impossible_by_precondition(self): + src = """ + def func(x: float): + ''' + Preconditions: + - x > 5.0 + ''' + if x < 0.0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_impossible_by_if_condition(self): + src = """ + def func(x: int): + if x > 5: + if x < 3: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_impossible_conditional_statement(self): + src = """ + def func(x: int): + if x > 0 and x < 0: + print("impossible") + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_impossible_if_else(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x > 0 + ''' + if x > 0: + return x + else: + return 0 + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_impossible_by_while_condition(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x > 10 + ''' + while x > 0: + if x < 0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_impossible_condition_multiple_if_else(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x in {1, 2, 3} + ''' + if x == 1: + print(1) + elif x == 2: + print(2) + elif x == 4: + print(2) + elif x == 3: + print(3) + else: + print(0) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + _, _, condition_node, _ = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_impossible_condition_repeat_checking_if_else(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x in {1, 2, 3} + ''' + if x == 1: + print(1) + elif x == 2: + print(2) + elif x == 2: + print(2) + elif x == 3: + print(3) + else: + print(0) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + _, _, condition_node, _ = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_possible_condition(self): + src = """ + def func(x: str): + ''' + Preconditions: + - x[0:2] == "ab" + ''' + if x == "abc": + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + def test_partially_impossible_condition(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x > 5 + ''' + if x > 10 or x < 5: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + def test_impossible_condition_variable_reassignment(self): + src = """ + def func(x: int, y: bool): + ''' + Preconditions: + - x > 10 + ''' + if not y: + x = -1 + if x < 0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + def test_impossible_condition_partial_path(self): + src = """ + def func(x: int): + if x > 5: + print(x) + else: + print(x) + if x < 0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + + def test_not_impossible_by_reassignment(self): + src = """ + def func(x: float): + ''' + Preconditions: + - x in [1.0, 2.0] + ''' + x = None + if x == 3.0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index ce1181257..3ceaad32b 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -3,12 +3,14 @@ from astroid import nodes from python_ta.cfg import CFGVisitor -from python_ta.checkers.redundant_condition_checker import RedundantConditionChecker +from python_ta.checkers.redundant_or_impossible_condition_checker import ( + RedundantOrImpossibleConditionChecker, +) from python_ta.transforms.z3_visitor import Z3Visitor class TestRedundantConditionChecker(pylint.testutils.CheckerTestCase): - CHECKER_CLASS = RedundantConditionChecker + CHECKER_CLASS = RedundantOrImpossibleConditionChecker CONFIG = {"z3": True} def test_redundant_by_precondition(self): @@ -72,6 +74,58 @@ def func(x: int): ): self.checker.visit_if(condition_node) + def test_redundant_if_else(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x > 0 + ''' + if x <= 0: + return x + else: + return 0 + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + + def test_redundant_condition_multiple_if_else(self): + src = """ + def func(x: int): + ''' + Preconditions: + - x in {1, 2, 3} + ''' + if x == 1: + print(1) + elif x == 2: + print(2) + elif x != 2: + print(2) + elif x == 3: + print(3) + else: + print(0) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + _, _, condition_node, _ = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + def test_not_redundant_condition(self): src = """ def func(x: str): @@ -108,7 +162,7 @@ def func(x: int): with self.assertNoMessages(): self.checker.visit_if(condition_node) - def test_redundant_condition_partial_paths(self): + def test_redundant_condition_variable_reassignment(self): src = """ def func(x: int, y: bool): ''' @@ -128,6 +182,24 @@ def func(x: int, y: bool): with self.assertNoMessages(): self.checker.visit_if(condition_node) + def test_redundant_condition_partial_path(self): + src = """ + def func(x: int): + if x > 5: + print(x) + else: + print(x) + if x > 0: + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + condition_node, *_ = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + def test_not_redundant_by_reassignment(self): src = """ def func(x: float): @@ -146,7 +218,3 @@ def func(x: float): with self.assertNoMessages(): self.checker.visit_if(condition_node) - - -# inspiration: check if the reassigned variable has the same type as previous one -# if yes, update the variable value in Z3Environment and continue using it in CFG traverse From a9b24f6efdb42fcbac0d03e430a4f95513d26a3e Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Fri, 15 Nov 2024 14:53:59 -0500 Subject: [PATCH 03/23] fix: register checker to linter & add documentation Fix an error that unregisters checker during initialization Add examples for redundant and impossible conditions Fix an unit test's expected behavior Update checker documentation Modify check-examplet to take z3 argument --- docs/checkers/index.md | 44 +++++++++++++++++++ .../r9900_redundant_condition.py | 2 - .../r9901_impossible_condition.py | 13 +++++- ...dundant_or_impossible_condition_checker.py | 9 ++-- .../test_impossible_condition_checker.py | 2 +- .../test_redundant_condition_checker.py | 2 +- tests/test_examples.py | 3 +- 7 files changed, 66 insertions(+), 9 deletions(-) diff --git a/docs/checkers/index.md b/docs/checkers/index.md index 0b4019085..f85000368 100644 --- a/docs/checkers/index.md +++ b/docs/checkers/index.md @@ -2699,6 +2699,50 @@ python_ta.check_all(config={ }) ``` +(R9900)= + +### Redundant Condition (R9900) + +This error occurs when an `if` or `while` condition is guaranteed to be true given the program control flow leading +to the conditional statement. + +Example: + +```{literalinclude} /../examples/custom_checkers/r9900_redundant_condition.py + +``` + +This error will only be checked if `z3` dependency is install and `z3` option of PythonTA +is turned on: + +```python +import python_ta +python_ta.check_all(config={ + "z3": True +}) +``` + +### Impossible Condition (R9901) + +This error occurs when an `if` or `while` condition is always false either due to either contradictions within the +condtional statement or program control flow leading to the conditional statement. + +Example: + +```{literalinclude} /../examples/custom_checkers/r9900_impossible_condition.py + +``` + +This error will only be checked if `z3` dependency is install and `z3` option of PythonTA +is turned on: + +```python +import python_ta +python_ta.check_all(config={ + "z3": True +}) +``` + ## Miscellaneous (E1305)= diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py index 423f73e4b..056d44d93 100644 --- a/examples/custom_checkers/r9900_redundant_condition.py +++ b/examples/custom_checkers/r9900_redundant_condition.py @@ -5,8 +5,6 @@ def return_large_number(x: int) -> int: """ if x > 1000: return x - else: # the else branch is redundant given the function preconditions - return 1000 def nested_condition(x: int) -> int: diff --git a/examples/custom_checkers/r9901_impossible_condition.py b/examples/custom_checkers/r9901_impossible_condition.py index b56e4ba24..6ec6e1a62 100644 --- a/examples/custom_checkers/r9901_impossible_condition.py +++ b/examples/custom_checkers/r9901_impossible_condition.py @@ -4,10 +4,21 @@ def print_natural_number(x: int): - x >= 0 """ if x < 0: - raise Exception("x is not an integer") + raise Exception("x is not a natural number") print(x) def invalid_condition(x: bool): if x and not x: print("impossible") + + +def spell_number(x: int) -> str: + if x == 0: + return "zero" + elif x == 1: + return "one" + elif x == 2: + return "two" + elif x == 2: # this condition is impossible + return "two again" diff --git a/python_ta/checkers/redundant_or_impossible_condition_checker.py b/python_ta/checkers/redundant_or_impossible_condition_checker.py index af8932cb4..a159cb868 100644 --- a/python_ta/checkers/redundant_or_impossible_condition_checker.py +++ b/python_ta/checkers/redundant_or_impossible_condition_checker.py @@ -64,7 +64,11 @@ def _check_condition(self, node: nodes.If | nodes.While) -> None: """A condition statement is redundant if for every feasible execution path leading to the node, the condition must be True by precedent constraints. """ - if not z3_dependency_available or not hasattr(node, "cfg_block"): + if ( + not hasattr(node, "cfg_block") + or not z3_dependency_available + or not self.linter.config.z3 + ): return node_block = node.cfg_block @@ -110,5 +114,4 @@ def register(linter: PyLinter) -> None: """Required method to auto-register this checker to the linter, Register the linter only if `z3` option is turned on. """ - if linter.config.z3: - linter.register_checker(RedundantOrImpossibleConditionChecker(linter)) + linter.register_checker(RedundantOrImpossibleConditionChecker(linter)) diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index a3c482ec6..fc664cc58 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -76,7 +76,7 @@ def func(x: int): Preconditions: - x > 0 ''' - if x > 0: + if x <= 0: return x else: return 0 diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index 3ceaad32b..5f5c206d6 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -81,7 +81,7 @@ def func(x: int): Preconditions: - x > 0 ''' - if x <= 0: + if x > 0: return x else: return 0 diff --git a/tests/test_examples.py b/tests/test_examples.py index 52d67322b..4585a7f4f 100644 --- a/tests/test_examples.py +++ b/tests/test_examples.py @@ -82,6 +82,7 @@ def _symbols_by_file_pyta(paths: list[str], include_msg: bool = False) -> dict[s config={ "output-format": "python_ta.reporters.JSONReporter", "enable": ["C9960"], + "z3": True, }, ) @@ -149,7 +150,7 @@ def test_examples_files_pyta(test_file: str, pyta_examples_symbols: dict[str, se found_pylint_message = checker_name in file_symbols assert ( found_pylint_message - ), f"Failed {test_file}. File does not add expected message {file_symbols}." + ), f"Failed {test_file}. File does not add expected message {checker_name}: {file_symbols}." @pytest.mark.parametrize("test_file", get_file_paths(_PYCODESTYLE_PATH)) From 7bc4b7ccd75c7f5298c93279298a781661a47e38 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Fri, 15 Nov 2024 16:04:28 -0500 Subject: [PATCH 04/23] fix: fix typo in documentation --- docs/checkers/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/checkers/index.md b/docs/checkers/index.md index f85000368..fe0ffacd2 100644 --- a/docs/checkers/index.md +++ b/docs/checkers/index.md @@ -2729,7 +2729,7 @@ condtional statement or program control flow leading to the conditional statemen Example: -```{literalinclude} /../examples/custom_checkers/r9900_impossible_condition.py +```{literalinclude} /../examples/custom_checkers/r9901_impossible_condition.py ``` From a43c5bfda4ed253f1acaac48d26ff5c9bdd56069 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Fri, 15 Nov 2024 16:29:11 -0500 Subject: [PATCH 05/23] fix: fix type annotation for compatibility with older Python version --- .../checkers/redundant_or_impossible_condition_checker.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/python_ta/checkers/redundant_or_impossible_condition_checker.py b/python_ta/checkers/redundant_or_impossible_condition_checker.py index a159cb868..cbe84f9cf 100644 --- a/python_ta/checkers/redundant_or_impossible_condition_checker.py +++ b/python_ta/checkers/redundant_or_impossible_condition_checker.py @@ -2,7 +2,7 @@ Check for redundant If or While conditions in functions based on z3 constraints """ -from typing import Any +from typing import Any, Union try: import z3 @@ -60,7 +60,7 @@ def visit_while(self, node: nodes.While) -> None: """Visit while statement""" self._check_condition(node) - def _check_condition(self, node: nodes.If | nodes.While) -> None: + def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: """A condition statement is redundant if for every feasible execution path leading to the node, the condition must be True by precedent constraints. """ From b53c450a378b221858a94c3025d97bef84b0108b Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Mon, 18 Nov 2024 00:24:57 -0500 Subject: [PATCH 06/23] ci: remove z3 option to rerun CI tests --- tests/test_examples.py | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/test_examples.py b/tests/test_examples.py index 4585a7f4f..68a6b7a19 100644 --- a/tests/test_examples.py +++ b/tests/test_examples.py @@ -82,7 +82,6 @@ def _symbols_by_file_pyta(paths: list[str], include_msg: bool = False) -> dict[s config={ "output-format": "python_ta.reporters.JSONReporter", "enable": ["C9960"], - "z3": True, }, ) From 613e81a9f975fbf063d514a4603df56f54ff5e23 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Mon, 18 Nov 2024 00:42:53 -0500 Subject: [PATCH 07/23] fix: add node z3_constraint only if constraint is not none modify ControlFlowGraph to append node z3_constraint only when it's not none Enable z3 option in test_examples --- python_ta/cfg/graph.py | 8 ++++---- tests/test_examples.py | 1 + 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/python_ta/cfg/graph.py b/python_ta/cfg/graph.py index f8ee79f5f..4269124a8 100644 --- a/python_ta/cfg/graph.py +++ b/python_ta/cfg/graph.py @@ -290,10 +290,10 @@ def update_edge_z3_constraints(self) -> None: z3_environment.add_constraint( Not(condition_z3_constraint) if edge.negate else condition_z3_constraint ) - # add z3 constraint to the CFG block of condition node - edge.source.z3_constraint = z3_environment.assign_constraint( - condition_z3_constraint - ) + # add z3 constraint to the CFG block of condition node + edge.source.z3_constraint = z3_environment.assign_constraint( + condition_z3_constraint + ) # update edge z3 constraints edge.z3_constraints[path_id] = z3_environment.assign_current_constraints() diff --git a/tests/test_examples.py b/tests/test_examples.py index 68a6b7a19..4585a7f4f 100644 --- a/tests/test_examples.py +++ b/tests/test_examples.py @@ -82,6 +82,7 @@ def _symbols_by_file_pyta(paths: list[str], include_msg: bool = False) -> dict[s config={ "output-format": "python_ta.reporters.JSONReporter", "enable": ["C9960"], + "z3": True, }, ) From 65be1ed610c41d99bcd4850ae76878b98c581fb2 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Mon, 18 Nov 2024 00:50:32 -0500 Subject: [PATCH 08/23] tests: add docstrings in example test cases --- examples/custom_checkers/r9900_redundant_condition.py | 2 ++ examples/custom_checkers/r9901_impossible_condition.py | 4 ++++ 2 files changed, 6 insertions(+) diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py index 056d44d93..a247801b5 100644 --- a/examples/custom_checkers/r9900_redundant_condition.py +++ b/examples/custom_checkers/r9900_redundant_condition.py @@ -1,5 +1,7 @@ def return_large_number(x: int) -> int: """ + Return number x only if it's greater than 1000 + Preconditions - x > 1000 """ diff --git a/examples/custom_checkers/r9901_impossible_condition.py b/examples/custom_checkers/r9901_impossible_condition.py index 6ec6e1a62..60ce53a1c 100644 --- a/examples/custom_checkers/r9901_impossible_condition.py +++ b/examples/custom_checkers/r9901_impossible_condition.py @@ -1,5 +1,8 @@ def print_natural_number(x: int): """ + Print number x only if it's a natural number. + In CS natural number starts with 0. + Preconditions: - x >= 0 """ @@ -14,6 +17,7 @@ def invalid_condition(x: bool): def spell_number(x: int) -> str: + """ Spell numbers 0 to 2""" if x == 0: return "zero" elif x == 1: From 4be45587c0fb084d122f2d47da7f06402f8c2b77 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Mon, 18 Nov 2024 02:09:20 -0500 Subject: [PATCH 09/23] fix: fix failing unit tests Initialize z3_constraint attribute of CFGBlock with None Turn on z3 option for test_black and test_check --- examples/custom_checkers/r9900_redundant_condition.py | 2 +- python_ta/cfg/graph.py | 1 + tests/test_black.py | 6 +++--- tests/test_check.py | 8 ++++++-- 4 files changed, 11 insertions(+), 6 deletions(-) diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py index a247801b5..f0a38043a 100644 --- a/examples/custom_checkers/r9900_redundant_condition.py +++ b/examples/custom_checkers/r9900_redundant_condition.py @@ -2,7 +2,7 @@ def return_large_number(x: int) -> int: """ Return number x only if it's greater than 1000 - Preconditions + Preconditions: - x > 1000 """ if x > 1000: diff --git a/python_ta/cfg/graph.py b/python_ta/cfg/graph.py index 4269124a8..7618e1b2a 100644 --- a/python_ta/cfg/graph.py +++ b/python_ta/cfg/graph.py @@ -358,6 +358,7 @@ def __init__(self, id_: int) -> None: self.predecessors = [] self.successors = [] self.reachable = False + self.z3_constraint = None def add_statement(self, statement: NodeNG) -> None: if not self.is_jump(): diff --git a/tests/test_black.py b/tests/test_black.py index 3da9cc7a3..235246d3c 100644 --- a/tests/test_black.py +++ b/tests/test_black.py @@ -15,19 +15,19 @@ error_params = [ ( """def foo():print("Hello, world!")\n""", - {"output-format": "python_ta.reporters.JSONReporter"}, + {"output-format": "python_ta.reporters.JSONReporter", "z3": True}, True, """def foo():\n print("Hello, world!")\n""", ), ( """def foo():print("Hello, world!" + "This line is too long and should be split by black.")""", - {"output-format": "python_ta.reporters.JSONReporter", "max-line-length": 50}, + {"output-format": "python_ta.reporters.JSONReporter", "max-line-length": 50, "z3": True}, True, """def foo():\n print(\n "Hello, world!"\n + "This line is too long and should be split by black."\n )\n""", ), ( """def foo():print("Hello, world!")\n""", - {"output-format": "python_ta.reporters.JSONReporter"}, + {"output-format": "python_ta.reporters.JSONReporter", "z3": True}, False, """def foo():print("Hello, world!")\n""", ), diff --git a/tests/test_check.py b/tests/test_check.py index 4c2ae1640..64bf4d101 100644 --- a/tests/test_check.py +++ b/tests/test_check.py @@ -16,6 +16,7 @@ def test_check_on_dir(): "output-format": "python_ta.reporters.JSONReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", + "z3": True, }, ) @@ -47,6 +48,7 @@ def test_check_on_file(): "output-format": "python_ta.reporters.PlainReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", + "z3": True, }, ) @@ -69,6 +71,7 @@ def test_check_on_bad_input(): "output-format": "python_ta.reporters.PlainReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", + "z3": True, }, ) @@ -177,6 +180,7 @@ def test_check_with_config(): "output-format": "python_ta.reporters.PlainReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", + "z3": True, } for item in _inputs: python_ta.check_all(item, config=CONFIG) @@ -187,7 +191,7 @@ def test_check_saves_file() -> None: _inputs = [["examples/nodes/name.py"]] for item in _inputs: # Note that the reporter output will be created in the main directory - python_ta.check_all(item, output="pyta_output.html") + python_ta.check_all(item, output="pyta_output.html", config={"z3": True}) file_exists = path.exists("pyta_output.html") @@ -203,7 +207,7 @@ def test_check_no_reporter_output(prevent_webbrowser_and_httpserver) -> None: _inputs = [["examples/nodes/name.py"]] for item in _inputs: # Note that the reporter output *would have been* created in the main directory - python_ta.check_all(item) + python_ta.check_all(item, config={"z3": True}) file_exists = path.exists("pyta_output.html") From 6593e8552480ee7f112eb7db62bdf8d3ce511857 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Wed, 20 Nov 2024 20:44:58 -0500 Subject: [PATCH 10/23] refactor: revert changes Revert changes to transforms, test_black, and test_examples --- python_ta/patches/transforms.py | 3 +-- tests/test_black.py | 6 +++--- tests/test_check.py | 8 ++------ tests/test_examples.py | 7 ++++--- 4 files changed, 10 insertions(+), 14 deletions(-) diff --git a/python_ta/patches/transforms.py b/python_ta/patches/transforms.py index 10a5f2607..1d70e6bbb 100644 --- a/python_ta/patches/transforms.py +++ b/python_ta/patches/transforms.py @@ -14,8 +14,7 @@ def new_get_ast(self, filepath, modname, data): ast = old_get_ast(self, filepath, modname, data) if ast is not None: try: - if z3: - ast = Z3Visitor().visitor.visit(ast) + ast = Z3Visitor().visitor.visit(ast) ast.accept(CFGVisitor()) except: pass diff --git a/tests/test_black.py b/tests/test_black.py index 235246d3c..3da9cc7a3 100644 --- a/tests/test_black.py +++ b/tests/test_black.py @@ -15,19 +15,19 @@ error_params = [ ( """def foo():print("Hello, world!")\n""", - {"output-format": "python_ta.reporters.JSONReporter", "z3": True}, + {"output-format": "python_ta.reporters.JSONReporter"}, True, """def foo():\n print("Hello, world!")\n""", ), ( """def foo():print("Hello, world!" + "This line is too long and should be split by black.")""", - {"output-format": "python_ta.reporters.JSONReporter", "max-line-length": 50, "z3": True}, + {"output-format": "python_ta.reporters.JSONReporter", "max-line-length": 50}, True, """def foo():\n print(\n "Hello, world!"\n + "This line is too long and should be split by black."\n )\n""", ), ( """def foo():print("Hello, world!")\n""", - {"output-format": "python_ta.reporters.JSONReporter", "z3": True}, + {"output-format": "python_ta.reporters.JSONReporter"}, False, """def foo():print("Hello, world!")\n""", ), diff --git a/tests/test_check.py b/tests/test_check.py index 64bf4d101..4c2ae1640 100644 --- a/tests/test_check.py +++ b/tests/test_check.py @@ -16,7 +16,6 @@ def test_check_on_dir(): "output-format": "python_ta.reporters.JSONReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", - "z3": True, }, ) @@ -48,7 +47,6 @@ def test_check_on_file(): "output-format": "python_ta.reporters.PlainReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", - "z3": True, }, ) @@ -71,7 +69,6 @@ def test_check_on_bad_input(): "output-format": "python_ta.reporters.PlainReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", - "z3": True, }, ) @@ -180,7 +177,6 @@ def test_check_with_config(): "output-format": "python_ta.reporters.PlainReporter", "pyta-error-permission": "no", "pyta-file-permission": "no", - "z3": True, } for item in _inputs: python_ta.check_all(item, config=CONFIG) @@ -191,7 +187,7 @@ def test_check_saves_file() -> None: _inputs = [["examples/nodes/name.py"]] for item in _inputs: # Note that the reporter output will be created in the main directory - python_ta.check_all(item, output="pyta_output.html", config={"z3": True}) + python_ta.check_all(item, output="pyta_output.html") file_exists = path.exists("pyta_output.html") @@ -207,7 +203,7 @@ def test_check_no_reporter_output(prevent_webbrowser_and_httpserver) -> None: _inputs = [["examples/nodes/name.py"]] for item in _inputs: # Note that the reporter output *would have been* created in the main directory - python_ta.check_all(item, config={"z3": True}) + python_ta.check_all(item) file_exists = path.exists("pyta_output.html") diff --git a/tests/test_examples.py b/tests/test_examples.py index 4585a7f4f..9bd8242a5 100644 --- a/tests/test_examples.py +++ b/tests/test_examples.py @@ -13,9 +13,9 @@ import python_ta -_EXAMPLES_PATH = "examples/pylint/" -_CUSTOM_CHECKER_PATH = "examples/custom_checkers/" -_PYCODESTYLE_PATH = "examples/custom_checkers/e9989_pycodestyle/" +_EXAMPLES_PATH = "../examples/pylint/" +_CUSTOM_CHECKER_PATH = "../examples/custom_checkers/" +_PYCODESTYLE_PATH = "../examples/custom_checkers/e9989_pycodestyle/" _EXAMPLE_PREFIX_REGEX = r"[cerfw]\d{4}" _PYCODESTYLE_PREFIX_REGEX = r"^e\d{3}_(error|no_error)\.py$" @@ -77,6 +77,7 @@ def _symbols_by_file_pyta(paths: list[str], include_msg: bool = False) -> dict[s (and descriptions if include_msg is True). """ sys.stdout = StringIO() + python_ta.PYLINT_PATCHED = False python_ta.check_all( module_name=get_file_paths(paths), config={ From 1d73c958041880472c44e4f06023a01322e202b0 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Fri, 22 Nov 2024 01:47:41 -0500 Subject: [PATCH 11/23] docs: update examples Add additional comments to checker examples Add unit test for redundant-condition-checker --- .../r9900_redundant_condition.py | 9 +++++---- .../r9901_impossible_condition.py | 16 ++++++++-------- .../test_redundant_condition_checker.py | 17 +++++++++++++++++ 3 files changed, 30 insertions(+), 12 deletions(-) diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py index f0a38043a..93fc23ed4 100644 --- a/examples/custom_checkers/r9900_redundant_condition.py +++ b/examples/custom_checkers/r9900_redundant_condition.py @@ -1,16 +1,17 @@ def return_large_number(x: int) -> int: - """ - Return number x only if it's greater than 1000 + """Return number x only if it's greater than 1000 Preconditions: - x > 1000 """ - if x > 1000: + # the if condition is already checked by function precondition + if x > 1000: # Error on this line return x def nested_condition(x: int) -> int: if x > 10: - if x > 5: + # the condition `x > 5` is already guaranteed by `x > 10` + if x > 5: # Error on this line return x return 0 diff --git a/examples/custom_checkers/r9901_impossible_condition.py b/examples/custom_checkers/r9901_impossible_condition.py index 60ce53a1c..0d468a727 100644 --- a/examples/custom_checkers/r9901_impossible_condition.py +++ b/examples/custom_checkers/r9901_impossible_condition.py @@ -1,18 +1,18 @@ -def print_natural_number(x: int): - """ - Print number x only if it's a natural number. - In CS natural number starts with 0. +def print_non_negative_number(x: int): + """Print number x only if it's greater or equal to 0 Preconditions: - x >= 0 """ - if x < 0: - raise Exception("x is not a natural number") + # the if condition is impossible given the function precondition + if x < 0: # Error on this line + raise Exception("x is smaller than zero") print(x) -def invalid_condition(x: bool): - if x and not x: +def impossible_condition(x: bool): + # the if condition is self-contradictory + if x and not x: # Error on this line print("impossible") diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index 5f5c206d6..4e0c48dce 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -97,6 +97,23 @@ def func(x: int): ): self.checker.visit_if(condition_node) + def test_redundant_condition_within_statement(self): + src = """ + def func(x: bool): + if x or not x: + return x + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertAddsMessages( + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + ignore_position=True, + ): + self.checker.visit_if(condition_node) + def test_redundant_condition_multiple_if_else(self): src = """ def func(x: int): From 10076c945e1b77bf8457ed53f73a39922aba08d4 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Fri, 22 Nov 2024 16:05:54 -0500 Subject: [PATCH 12/23] refactor: rename checker Rename checker to ConditionLogicChecker Add example case for redundant condition --- examples/custom_checkers/r9900_redundant_condition.py | 6 ++++++ .../checkers/redundant_or_impossible_condition_checker.py | 4 ++-- .../test_impossible_condition_checker.py | 4 ++-- .../test_redundant_condition_checker.py | 4 ++-- 4 files changed, 12 insertions(+), 6 deletions(-) diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py index 93fc23ed4..25b10822e 100644 --- a/examples/custom_checkers/r9900_redundant_condition.py +++ b/examples/custom_checkers/r9900_redundant_condition.py @@ -15,3 +15,9 @@ def nested_condition(x: int) -> int: if x > 5: # Error on this line return x return 0 + + +def redundant_condition(x: bool): + # the if condition is always true + if x or not x: # Error on this line + print("redundant") diff --git a/python_ta/checkers/redundant_or_impossible_condition_checker.py b/python_ta/checkers/redundant_or_impossible_condition_checker.py index cbe84f9cf..af35e4220 100644 --- a/python_ta/checkers/redundant_or_impossible_condition_checker.py +++ b/python_ta/checkers/redundant_or_impossible_condition_checker.py @@ -18,7 +18,7 @@ from pylint.lint import PyLinter -class RedundantOrImpossibleConditionChecker(BaseChecker): +class ConditionLogicChecker(BaseChecker): name = "redundant-condition" msgs = { "R9900": ( @@ -114,4 +114,4 @@ def register(linter: PyLinter) -> None: """Required method to auto-register this checker to the linter, Register the linter only if `z3` option is turned on. """ - linter.register_checker(RedundantOrImpossibleConditionChecker(linter)) + linter.register_checker(ConditionLogicChecker(linter)) diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index fc664cc58..a10c61283 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -4,13 +4,13 @@ from python_ta.cfg import CFGVisitor from python_ta.checkers.redundant_or_impossible_condition_checker import ( - RedundantOrImpossibleConditionChecker, + ConditionLogicChecker, ) from python_ta.transforms.z3_visitor import Z3Visitor class TestImpossibleConditionChecker(pylint.testutils.CheckerTestCase): - CHECKER_CLASS = RedundantOrImpossibleConditionChecker + CHECKER_CLASS = ConditionLogicChecker CONFIG = {"z3": True} def test_impossible_by_precondition(self): diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index 4e0c48dce..f901d35f5 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -4,13 +4,13 @@ from python_ta.cfg import CFGVisitor from python_ta.checkers.redundant_or_impossible_condition_checker import ( - RedundantOrImpossibleConditionChecker, + ConditionLogicChecker, ) from python_ta.transforms.z3_visitor import Z3Visitor class TestRedundantConditionChecker(pylint.testutils.CheckerTestCase): - CHECKER_CLASS = RedundantOrImpossibleConditionChecker + CHECKER_CLASS = ConditionLogicChecker CONFIG = {"z3": True} def test_redundant_by_precondition(self): From fbca50e34652e8d50ce93fad5134c734836f3e64 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Tue, 26 Nov 2024 16:46:52 -0500 Subject: [PATCH 13/23] refactor: rename checker and remove outdated comments --- ...on_checker.py => condition_logic_checker.py} | 17 +++++------------ .../test_impossible_condition_checker.py | 4 +--- .../test_redundant_condition_checker.py | 4 +--- 3 files changed, 7 insertions(+), 18 deletions(-) rename python_ta/checkers/{redundant_or_impossible_condition_checker.py => condition_logic_checker.py} (84%) diff --git a/python_ta/checkers/redundant_or_impossible_condition_checker.py b/python_ta/checkers/condition_logic_checker.py similarity index 84% rename from python_ta/checkers/redundant_or_impossible_condition_checker.py rename to python_ta/checkers/condition_logic_checker.py index af35e4220..252faa065 100644 --- a/python_ta/checkers/redundant_or_impossible_condition_checker.py +++ b/python_ta/checkers/condition_logic_checker.py @@ -22,16 +22,15 @@ class ConditionLogicChecker(BaseChecker): name = "redundant-condition" msgs = { "R9900": ( - """This conditional statement is already true given the preceding code; + """This condition will always evaluate to True; consider removing redundant check.""", "redundant-condition", - "Used when an If or While statement is tautologically true based on preceding Z3 constraints." - " Enabled when Z3 option is on.", + "Used when an If or While statement is always True. Requires the z3 configuration option to be True.", ), "R9901": ( - """This conditional statement is never true given the preceding code.""", + """This condition will always evaluate to False""", "impossible-condition", - "Used when an If or While statement contradicts preceding Z3 constraints. Enable when Z3 option is on.", + "Used when an If or While statement is always False. Requires the z3 configuration option to be True.", ), } options = ( @@ -46,14 +45,10 @@ class ConditionLogicChecker(BaseChecker): ), ) - def __init__(self, linter=None) -> None: - super().__init__(linter=linter) - @only_required_for_messages("redundant-condition", "impossible-condition") def visit_if(self, node: nodes.If) -> None: """Visit if statement""" self._check_condition(node) - # handle else branch @only_required_for_messages("redundant-condition", "impossible-condition") def visit_while(self, node: nodes.While) -> None: @@ -111,7 +106,5 @@ def _check_impossible_condition( def register(linter: PyLinter) -> None: - """Required method to auto-register this checker to the linter, - Register the linter only if `z3` option is turned on. - """ + """Required method to auto-register this checker to the linter.""" linter.register_checker(ConditionLogicChecker(linter)) diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index a10c61283..9079c7ae5 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -3,9 +3,7 @@ from astroid import nodes from python_ta.cfg import CFGVisitor -from python_ta.checkers.redundant_or_impossible_condition_checker import ( - ConditionLogicChecker, -) +from python_ta.checkers.condition_logic_checker import ConditionLogicChecker from python_ta.transforms.z3_visitor import Z3Visitor diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index f901d35f5..b728731c1 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -3,9 +3,7 @@ from astroid import nodes from python_ta.cfg import CFGVisitor -from python_ta.checkers.redundant_or_impossible_condition_checker import ( - ConditionLogicChecker, -) +from python_ta.checkers.condition_logic_checker import ConditionLogicChecker from python_ta.transforms.z3_visitor import Z3Visitor From 54ad92955cf410a6961a4e7197e823d56fa6d19e Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Tue, 26 Nov 2024 16:53:06 -0500 Subject: [PATCH 14/23] refactor: revert changes to graph.py --- python_ta/cfg/graph.py | 63 +++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 38 deletions(-) diff --git a/python_ta/cfg/graph.py b/python_ta/cfg/graph.py index 7618e1b2a..f442b6bb8 100644 --- a/python_ta/cfg/graph.py +++ b/python_ta/cfg/graph.py @@ -286,31 +286,29 @@ def update_edge_z3_constraints(self) -> None: # traverse through edge if edge.condition is not None: condition_z3_constraint = z3_environment.parse_constraint(edge.condition) - if condition_z3_constraint is not None and edge.negate is not None: - z3_environment.add_constraint( - Not(condition_z3_constraint) if edge.negate else condition_z3_constraint - ) - # add z3 constraint to the CFG block of condition node - edge.source.z3_constraint = z3_environment.assign_constraint( - condition_z3_constraint - ) - - # update edge z3 constraints - edge.z3_constraints[path_id] = z3_environment.assign_current_constraints() + if condition_z3_constraint is not None: + if edge.negate is not None: + z3_environment.add_constraint( + Not(condition_z3_constraint) + if edge.negate + else condition_z3_constraint + ) + + edge.z3_constraints[path_id] = z3_environment.update_constraints() # traverse into target node - for stmt in edge.target.statements: - if isinstance(stmt, (Assign, AugAssign, AnnAssign)): - self._handle_variable_reassignment(stmt, z3_environment) + for node in edge.target.statements: + if isinstance(node, (Assign, AugAssign, AnnAssign)): + self._handle_variable_reassignment(node, z3_environment) def _handle_variable_reassignment(self, node: NodeNG, env: Z3Environment) -> None: """Check for reassignment statements and invoke Z3 environment""" if isinstance(node, Assign): for target in node.targets: if isinstance(target, AssignName): - env.handle_variable_assignment(target.name) + env.assign(target.name) elif isinstance(node, (AugAssign, AnnAssign)): - env.handle_variable_assignment(node.target.name) + env.assign(node.target.name) def update_edge_feasibility(self) -> None: """Traverse through edges in DFS order and update is_feasible @@ -348,8 +346,6 @@ class CFGBlock: successors: List[CFGEdge] # Whether there exists a path from the start block to this block. reachable: bool - # the z3 constraint associated with a conditional statement - z3_constraint: Optional[ExprRef] def __init__(self, id_: int) -> None: """Initialize a new CFGBlock.""" @@ -358,7 +354,6 @@ def __init__(self, id_: int) -> None: self.predecessors = [] self.successors = [] self.reachable = False - self.z3_constraint = None def add_statement(self, statement: NodeNG) -> None: if not self.is_jump(): @@ -452,27 +447,23 @@ def __init__(self, variables: Dict[str, ExprRef], constraints: List[ExprRef]) -> self.variables = variables self.constraints = constraints.copy() - def handle_variable_assignment(self, name: str) -> None: + def assign(self, name: str) -> None: """Handle a variable assignment statement""" if name in self.variable_unassigned: self.variable_unassigned[name] = False - def assign_constraint(self, constraint: ExprRef) -> Optional[ExprRef]: - """Returns the given z3 constraints if it - does not contain reassigned variables - """ - if self._check_variables_unassigned(constraint): - return constraint - return None - - def assign_current_constraints(self) -> List[ExprRef]: - """Returns all z3 constraints in the current environment + def update_constraints(self) -> List[ExprRef]: + """Returns all z3 constraints in the environments Removes constraints with reassigned variables """ updated_constraints = [] for constraint in self.constraints: # discard expressions with reassigned variables - if self._check_variables_unassigned(constraint): + variables = _get_vars(constraint) + reassigned = any( + not self.variable_unassigned.get(variable, False) for variable in variables + ) + if not reassigned: updated_constraints.append(constraint) self.constraints = updated_constraints @@ -483,19 +474,15 @@ def add_constraint(self, constraint: ExprRef) -> None: self.constraints.append(constraint) def parse_constraint(self, node: NodeNG) -> Optional[ExprRef]: - """Parse an Astroid node to a Z3 constraint. Return the resulting expression""" + """Parse an Astroid node to a Z3 constraint + Return the resulting expression + """ parser = Z3Parser(self.variables) try: return parser.parse(node) except (Z3Exception, Z3ParseException): return None - def _check_variables_unassigned(self, constraint: ExprRef) -> bool: - """Return True if all variables in the z3 constraint have not been reassigned""" - return all( - self.variable_unassigned.get(variable, True) for variable in _get_vars(constraint) - ) - def _get_vars(expr: ExprRef) -> Set[str]: """Retrieve all z3 variables from a z3 expression""" From 5ab960bc0b01ebc4820f3c8eba6ff7bfcb11f24a Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Tue, 26 Nov 2024 16:59:01 -0500 Subject: [PATCH 15/23] refactor: remove redundant helper function Use single _check_unsat to handle both redundant condition and impossible condition Revert changes to transforms --- python_ta/checkers/condition_logic_checker.py | 21 +++---------------- python_ta/patches/transforms.py | 3 ++- 2 files changed, 5 insertions(+), 19 deletions(-) diff --git a/python_ta/checkers/condition_logic_checker.py b/python_ta/checkers/condition_logic_checker.py index 252faa065..a321ef2ee 100644 --- a/python_ta/checkers/condition_logic_checker.py +++ b/python_ta/checkers/condition_logic_checker.py @@ -73,37 +73,22 @@ def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: for pred in node_block.predecessors: if all( - self._check_redundant_condition( - z3.And(*[c for c in constraints]), node_block.z3_constraint - ) + self._check_unsat(z3.Not(z3.And(c for c in constraints)), node_block.z3_constraint) for constraints in pred.z3_constraints.values() ): self.add_message("redundant-condition", node=node) if all( - self._check_impossible_condition( - z3.And(*[c for c in constraints]), node_block.z3_constraint - ) + self._check_unsat(z3.And(c for c in constraints), node_block.z3_constraint) for constraints in pred.z3_constraints.values() ): self.add_message("impossible-condition", node=node) - def _check_redundant_condition( - self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef - ) -> bool: + def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool: """Check if the condition is redundant.""" solver = z3.Solver() solver.add(z3.And(prev_constraints, node_constraint) != prev_constraints) return solver.check() == z3.unsat - def _check_impossible_condition( - self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef - ) -> bool: - """Check if the condition is impossible.""" - solver = z3.Solver() - solver.add(prev_constraints) - solver.add(node_constraint) - return solver.check() == z3.unsat - def register(linter: PyLinter) -> None: """Required method to auto-register this checker to the linter.""" diff --git a/python_ta/patches/transforms.py b/python_ta/patches/transforms.py index 1d70e6bbb..10a5f2607 100644 --- a/python_ta/patches/transforms.py +++ b/python_ta/patches/transforms.py @@ -14,7 +14,8 @@ def new_get_ast(self, filepath, modname, data): ast = old_get_ast(self, filepath, modname, data) if ast is not None: try: - ast = Z3Visitor().visitor.visit(ast) + if z3: + ast = Z3Visitor().visitor.visit(ast) ast.accept(CFGVisitor()) except: pass From 76aeafcb6737af75642612a5f9c33a4d06c9de58 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Tue, 26 Nov 2024 17:05:51 -0500 Subject: [PATCH 16/23] docs: refine examples --- .../custom_checkers/r9901_impossible_condition.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/examples/custom_checkers/r9901_impossible_condition.py b/examples/custom_checkers/r9901_impossible_condition.py index 0d468a727..d5cea9c5f 100644 --- a/examples/custom_checkers/r9901_impossible_condition.py +++ b/examples/custom_checkers/r9901_impossible_condition.py @@ -1,4 +1,4 @@ -def print_non_negative_number(x: int): +def print_none_negative_number(x: int): """Print number x only if it's greater or equal to 0 Preconditions: @@ -11,18 +11,18 @@ def print_non_negative_number(x: int): def impossible_condition(x: bool): - # the if condition is self-contradictory + # the if condition is always false if x and not x: # Error on this line print("impossible") -def spell_number(x: int) -> str: - """ Spell numbers 0 to 2""" +def Display_number(x: int) -> str: + """Display numbers 0 to 2 in word""" if x == 0: - return "zero" + "zero" elif x == 1: return "one" elif x == 2: return "two" - elif x == 2: # this condition is impossible + elif x == 2: # Error on this line return "two again" From ec386e91d62fbbcebc247eb1d7b6ea5cea163bdd Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Thu, 28 Nov 2024 17:04:47 -0500 Subject: [PATCH 17/23] fix: revert file path changes to test_exampes --- tests/test_examples.py | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/test_examples.py b/tests/test_examples.py index 9bd8242a5..4585a7f4f 100644 --- a/tests/test_examples.py +++ b/tests/test_examples.py @@ -13,9 +13,9 @@ import python_ta -_EXAMPLES_PATH = "../examples/pylint/" -_CUSTOM_CHECKER_PATH = "../examples/custom_checkers/" -_PYCODESTYLE_PATH = "../examples/custom_checkers/e9989_pycodestyle/" +_EXAMPLES_PATH = "examples/pylint/" +_CUSTOM_CHECKER_PATH = "examples/custom_checkers/" +_PYCODESTYLE_PATH = "examples/custom_checkers/e9989_pycodestyle/" _EXAMPLE_PREFIX_REGEX = r"[cerfw]\d{4}" _PYCODESTYLE_PREFIX_REGEX = r"^e\d{3}_(error|no_error)\.py$" @@ -77,7 +77,6 @@ def _symbols_by_file_pyta(paths: list[str], include_msg: bool = False) -> dict[s (and descriptions if include_msg is True). """ sys.stdout = StringIO() - python_ta.PYLINT_PATCHED = False python_ta.check_all( module_name=get_file_paths(paths), config={ From 78d4d2d2e221b0d1657c4efad9a7d5bdb4986369 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Thu, 28 Nov 2024 17:41:48 -0500 Subject: [PATCH 18/23] docs: refine documentation --- CHANGELOG.md | 4 ++-- docs/checkers/index.md | 6 ++---- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7815aa55f..695f9046d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -22,8 +22,8 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### 💫 New checkers - `unmentioned-parameter`: Provide error message when a function parameter is not mentioned by name in the function's docstring. By default, this checker is disabled. -- `redundant-condition`: Provide error message when a conditional statement within a function is guaranteed true given the precedent statements. This checker is enabled only when `z3` option is turned on. -- `impossible-condition`: Provide error message when a conditional statement within a function contradicts the precedent statements. This checker is enabled only when `z3` option is turned on. +- `redundant-condition`: Provide error message when a conditional statement within a function is guaranteed true. This checker requires `z3` option to be turned on. +- `impossible-condition`: Provide error message when a conditional statement within a function is guaranteed false. This checker requires `z3` option to be turned on. ### 🐛 Bug fixes diff --git a/docs/checkers/index.md b/docs/checkers/index.md index fe0ffacd2..3f59256a7 100644 --- a/docs/checkers/index.md +++ b/docs/checkers/index.md @@ -2703,8 +2703,7 @@ python_ta.check_all(config={ ### Redundant Condition (R9900) -This error occurs when an `if` or `while` condition is guaranteed to be true given the program control flow leading -to the conditional statement. +This error occurs when an `if` or `while` condition is guaranteed to be true. Example: @@ -2724,8 +2723,7 @@ python_ta.check_all(config={ ### Impossible Condition (R9901) -This error occurs when an `if` or `while` condition is always false either due to either contradictions within the -condtional statement or program control flow leading to the conditional statement. +This error occurs when an `if` or `while` condition is guaranteed to be false. Example: From 950e18a76f3e97e3d05003d8bcee9d98ae7cf5ea Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Sun, 1 Dec 2024 11:34:52 -0500 Subject: [PATCH 19/23] refactor: use Z3Environment to parse node condition Use Z3Environment of CFG variables to parse node condition Change z3_var attribute of ControlFlowGraph to public --- python_ta/cfg/graph.py | 8 +++---- python_ta/checkers/condition_logic_checker.py | 21 ++++++++++++------- tests/test_z3_visitor.py | 10 ++++----- 3 files changed, 22 insertions(+), 17 deletions(-) diff --git a/python_ta/cfg/graph.py b/python_ta/cfg/graph.py index f442b6bb8..46f446dc2 100644 --- a/python_ta/cfg/graph.py +++ b/python_ta/cfg/graph.py @@ -56,7 +56,7 @@ class ControlFlowGraph: # z3 constraints of preconditions precondition_constraints: List[ExprRef] # map from variable names to z3 variables - _z3_vars: Dict[str, ExprRef] + z3_vars: Dict[str, ExprRef] def __init__(self, cfg_id: int = 0) -> None: self.block_count = 0 @@ -64,7 +64,7 @@ def __init__(self, cfg_id: int = 0) -> None: self.unreachable_blocks = set() self.start = self.create_block() self.end = self.create_block() - self._z3_vars = {} + self.z3_vars = {} self.precondition_constraints = [] def add_arguments(self, args: Arguments) -> None: @@ -76,7 +76,7 @@ def add_arguments(self, args: Arguments) -> None: # Parse types parser = Z3Parser() z3_vars = parser.parse_arguments(args) - self._z3_vars.update(z3_vars) + self.z3_vars.update(z3_vars) def create_block( self, @@ -281,7 +281,7 @@ def update_edge_z3_constraints(self) -> None: for path_id, path in enumerate(self.get_paths()): # starting a new path - z3_environment = Z3Environment(self._z3_vars, self.precondition_constraints) + z3_environment = Z3Environment(self.z3_vars, self.precondition_constraints) for edge in path: # traverse through edge if edge.condition is not None: diff --git a/python_ta/checkers/condition_logic_checker.py b/python_ta/checkers/condition_logic_checker.py index a321ef2ee..5058964bb 100644 --- a/python_ta/checkers/condition_logic_checker.py +++ b/python_ta/checkers/condition_logic_checker.py @@ -7,9 +7,12 @@ try: import z3 + from ..cfg.graph import Z3Environment + z3_dependency_available = True except ImportError: z3 = Any + Z3Environment = Any z3_dependency_available = False from astroid import nodes @@ -68,25 +71,27 @@ def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: node_block = node.cfg_block - if not node_block.is_feasible or node_block.z3_constraint is None: - return + # create node condition z3 constraint + condition_node = node.test + env = Z3Environment(node.frame().cfg.z3_vars, []) + z3_condition = env.parse_constraint(condition_node) - for pred in node_block.predecessors: + for edge in (pred for pred in node_block.predecessors if pred.is_feasible): if all( - self._check_unsat(z3.Not(z3.And(c for c in constraints)), node_block.z3_constraint) - for constraints in pred.z3_constraints.values() + self._check_unsat(z3.And(*constraints), z3.Not(z3_condition)) + for constraints in edge.z3_constraints.values() ): self.add_message("redundant-condition", node=node) if all( - self._check_unsat(z3.And(c for c in constraints), node_block.z3_constraint) - for constraints in pred.z3_constraints.values() + self._check_unsat(z3.And(*constraints), z3_condition) + for constraints in edge.z3_constraints.values() ): self.add_message("impossible-condition", node=node) def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool: """Check if the condition is redundant.""" solver = z3.Solver() - solver.add(z3.And(prev_constraints, node_constraint) != prev_constraints) + solver.add(z3.And(prev_constraints, node_constraint)) return solver.check() == z3.unsat diff --git a/tests/test_z3_visitor.py b/tests/test_z3_visitor.py index 3aaa7b700..b69e811c7 100644 --- a/tests/test_z3_visitor.py +++ b/tests/test_z3_visitor.py @@ -365,8 +365,8 @@ def test_cfg_z3_vars_initialization(): cfg = ControlFlowGraph() cfg.add_arguments(node.args) - assert len(cfg._z3_vars) == 4 - assert cfg._z3_vars["x"] == z3.Int("x") - assert cfg._z3_vars["y"] == z3.Real("y") - assert cfg._z3_vars["z"] == z3.Bool("z") - assert cfg._z3_vars["a"] == z3.String("a") + assert len(cfg.z3_vars) == 4 + assert cfg.z3_vars["x"] == z3.Int("x") + assert cfg.z3_vars["y"] == z3.Real("y") + assert cfg.z3_vars["z"] == z3.Bool("z") + assert cfg.z3_vars["a"] == z3.String("a") From ce10717df5b7187cc300dab9dfd7c90e1a9720cb Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Sun, 1 Dec 2024 12:48:12 -0500 Subject: [PATCH 20/23] fix: fix failing test when multiple feasible branches are present Change condition of redundant/impossible condition to to be triggered only if the z3 check fails for all branches for all paths Add test cases for multiple feasible branches --- python_ta/checkers/condition_logic_checker.py | 24 ++++++++++--------- .../test_impossible_condition_checker.py | 20 ++++++++++++++++ .../test_redundant_condition_checker.py | 20 ++++++++++++++++ 3 files changed, 53 insertions(+), 11 deletions(-) diff --git a/python_ta/checkers/condition_logic_checker.py b/python_ta/checkers/condition_logic_checker.py index 5058964bb..87fe5a04f 100644 --- a/python_ta/checkers/condition_logic_checker.py +++ b/python_ta/checkers/condition_logic_checker.py @@ -76,17 +76,19 @@ def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: env = Z3Environment(node.frame().cfg.z3_vars, []) z3_condition = env.parse_constraint(condition_node) - for edge in (pred for pred in node_block.predecessors if pred.is_feasible): - if all( - self._check_unsat(z3.And(*constraints), z3.Not(z3_condition)) - for constraints in edge.z3_constraints.values() - ): - self.add_message("redundant-condition", node=node) - if all( - self._check_unsat(z3.And(*constraints), z3_condition) - for constraints in edge.z3_constraints.values() - ): - self.add_message("impossible-condition", node=node) + 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) + + 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) def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool: """Check if the condition is redundant.""" diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index 9079c7ae5..1a35fcf8a 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -262,3 +262,23 @@ def func(x: float): with self.assertNoMessages(): self.checker.visit_if(condition_node) + + def test_not_impossible_by_reassignment_one_path(self): + src = """ + def func(x: str, y: int): + ''' + Preconditions: + - x in {"a", "b"} + ''' + if y > 0: + x = "c" + if x == "c": + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index b728731c1..dd7eba2cf 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -233,3 +233,23 @@ def func(x: float): with self.assertNoMessages(): self.checker.visit_if(condition_node) + + def test_not_redundant_by_reassignment_one_path(self): + src = """ + def func(x: str, y: int): + ''' + Preconditions: + - x in {"a", "b"} + ''' + if y > 0: + x = "c" + if x == "a" or x == "b": + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) From a33367e45fc8682aca68c82ebbd2824e88da0e0f Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Thu, 12 Dec 2024 20:38:56 -0500 Subject: [PATCH 21/23] fix: fix condition logic error not ignored during reassignment Turn on `separate-condition-block` in CFGVisitor when `z3` config applied Update unit tests --- python_ta/patches/transforms.py | 4 +- .../test_impossible_condition_checker.py | 71 +++++-------------- .../test_redundant_condition_checker.py | 67 +++++------------ 3 files changed, 41 insertions(+), 101 deletions(-) diff --git a/python_ta/patches/transforms.py b/python_ta/patches/transforms.py index 10a5f2607..236aabb68 100644 --- a/python_ta/patches/transforms.py +++ b/python_ta/patches/transforms.py @@ -16,7 +16,9 @@ def new_get_ast(self, filepath, modname, data): try: if z3: ast = Z3Visitor().visitor.visit(ast) - ast.accept(CFGVisitor()) + ast.accept(CFGVisitor(options={"separate-condition-blocks": True})) + else: + ast.accept(CFGVisitor()) except: pass return ast diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index 1a35fcf8a..47a35a89f 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -21,10 +21,7 @@ def func(x: float): if x < 0.0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), @@ -39,10 +36,7 @@ def func(x: int): if x < 3: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), @@ -56,10 +50,7 @@ def func(x: int): if x > 0 and x < 0: print("impossible") """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), @@ -79,10 +70,7 @@ def func(x: int): else: return 0 """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), @@ -101,10 +89,7 @@ def func(x: int): if x < 0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), @@ -130,10 +115,7 @@ def func(x: int): else: print(0) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - _, _, condition_node, _ = mod.nodes_of_class(nodes.If) + _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), @@ -159,10 +141,7 @@ def func(x: int): else: print(0) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - _, _, condition_node, _ = mod.nodes_of_class(nodes.If) + _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), @@ -180,10 +159,7 @@ def func(x: str): if x == "abc": print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -198,10 +174,7 @@ def func(x: int): if x > 10 or x < 5: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -218,10 +191,7 @@ def func(x: int, y: bool): if x < 0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -236,10 +206,7 @@ def func(x: int): if x < 0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -255,10 +222,7 @@ def func(x: float): if x == 3.0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -275,10 +239,13 @@ def func(x: str, y: int): if x == "c": print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) + + def _apply_cfg_visitor(self, src: str) -> nodes.NodeNG: + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor(options={"separate-condition-blocks": True})) + return mod diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index dd7eba2cf..51f5a9907 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -21,10 +21,7 @@ def func(x: int): if x > 5: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), @@ -39,10 +36,7 @@ def func(x: int): if x > 3: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), @@ -61,10 +55,7 @@ def func(x: int): if x != 0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), @@ -84,10 +75,7 @@ def func(x: int): else: return 0 """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), @@ -101,10 +89,7 @@ def func(x: bool): if x or not x: return x """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), @@ -130,10 +115,7 @@ def func(x: int): else: print(0) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - _, _, condition_node, _ = mod.nodes_of_class(nodes.If) + _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), @@ -151,10 +133,7 @@ def func(x: str): if x != "abc": print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -169,10 +148,7 @@ def func(x: int): if x > 10 and x < 15: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -189,10 +165,7 @@ def func(x: int, y: bool): if x > 0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -207,10 +180,7 @@ def func(x: int): if x > 0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -226,10 +196,7 @@ def func(x: float): if x == 1.0 or x == 2.0: print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - condition_node, *_ = mod.nodes_of_class(nodes.If) + condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) @@ -246,10 +213,14 @@ def func(x: str, y: int): if x == "a" or x == "b": print(x) """ - z3v = Z3Visitor() - mod = z3v.visitor.visit(astroid.parse(src)) - mod.accept(CFGVisitor()) - *_, condition_node = mod.nodes_of_class(nodes.If) + + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertNoMessages(): self.checker.visit_if(condition_node) + + def _apply_cfg_visitor(self, src: str) -> nodes.NodeNG: + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor(options={"separate-condition-blocks": True})) + return mod From 96aa91d5d486ce34bab86dde5c9f27d34f03c908 Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Wed, 18 Dec 2024 21:48:38 -0500 Subject: [PATCH 22/23] refactor: refine comments and documentation Modify comments and error messages Add type annotations to example code Change node.test to be the node highlighted Update unit tests --- CHANGELOG.md | 5 ++-- docs/checkers/index.md | 8 +++--- .../r9900_redundant_condition.py | 2 +- .../r9901_impossible_condition.py | 6 ++-- python_ta/checkers/condition_logic_checker.py | 28 +++++++++++++------ .../test_impossible_condition_checker.py | 14 +++++----- .../test_redundant_condition_checker.py | 12 ++++---- tests/test_examples.py | 2 +- 8 files changed, 44 insertions(+), 33 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 50f998462..bffec8c9b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,9 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### 💫 New checkers +- `redundant-condition`: Provide error message when a conditional statement within a function is guaranteed true. This checker requires `z3` option to be turned on. +- `impossible-condition`: Provide error message when a conditional statement within a function is guaranteed false. This checker requires `z3` option to be turned on. + ### 🐛 Bug fixes ### 🔧 Internal changes @@ -43,8 +46,6 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ### 💫 New checkers - `unmentioned-parameter`: Provide error message when a function parameter is not mentioned by name in the function's docstring. By default, this checker is disabled. -- `redundant-condition`: Provide error message when a conditional statement within a function is guaranteed true. This checker requires `z3` option to be turned on. -- `impossible-condition`: Provide error message when a conditional statement within a function is guaranteed false. This checker requires `z3` option to be turned on. ### 🐛 Bug fixes diff --git a/docs/checkers/index.md b/docs/checkers/index.md index 3f59256a7..ebccbd2a5 100644 --- a/docs/checkers/index.md +++ b/docs/checkers/index.md @@ -2711,8 +2711,8 @@ Example: ``` -This error will only be checked if `z3` dependency is install and `z3` option of PythonTA -is turned on: +This error will only be checked if the `z3-solver` library is installed and `z3` option of PythonTA +is enabled: ```python import python_ta @@ -2731,8 +2731,8 @@ Example: ``` -This error will only be checked if `z3` dependency is install and `z3` option of PythonTA -is turned on: +This error will only be checked if the `z3-solver` library is installed and `z3` option of PythonTA +is enabled: ```python import python_ta diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py index 25b10822e..0d745c925 100644 --- a/examples/custom_checkers/r9900_redundant_condition.py +++ b/examples/custom_checkers/r9900_redundant_condition.py @@ -17,7 +17,7 @@ def nested_condition(x: int) -> int: return 0 -def redundant_condition(x: bool): +def redundant_condition(x: bool) -> None: # the if condition is always true if x or not x: # Error on this line print("redundant") diff --git a/examples/custom_checkers/r9901_impossible_condition.py b/examples/custom_checkers/r9901_impossible_condition.py index d5cea9c5f..505846e23 100644 --- a/examples/custom_checkers/r9901_impossible_condition.py +++ b/examples/custom_checkers/r9901_impossible_condition.py @@ -1,4 +1,4 @@ -def print_none_negative_number(x: int): +def print_none_negative_number(x: int) -> None: """Print number x only if it's greater or equal to 0 Preconditions: @@ -10,13 +10,13 @@ def print_none_negative_number(x: int): print(x) -def impossible_condition(x: bool): +def impossible_condition(x: bool) -> None: # the if condition is always false if x and not x: # Error on this line print("impossible") -def Display_number(x: int) -> str: +def display_number(x: int) -> str: """Display numbers 0 to 2 in word""" if x == 0: "zero" diff --git a/python_ta/checkers/condition_logic_checker.py b/python_ta/checkers/condition_logic_checker.py index 87fe5a04f..3e58658ac 100644 --- a/python_ta/checkers/condition_logic_checker.py +++ b/python_ta/checkers/condition_logic_checker.py @@ -1,7 +1,9 @@ """ -Check for redundant If or While conditions in functions based on z3 constraints +Check for redundant/impossible If or While conditions in functions based on z3 constraints """ +from __future__ import annotations + from typing import Any, Union try: @@ -25,13 +27,12 @@ class ConditionLogicChecker(BaseChecker): name = "redundant-condition" msgs = { "R9900": ( - """This condition will always evaluate to True; - consider removing redundant check.""", + """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""", + """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.", ), @@ -59,8 +60,13 @@ def visit_while(self, node: nodes.While) -> None: self._check_condition(node) def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: - """A condition statement is redundant if for every feasible execution path - leading to the node, the condition must be True by precedent constraints. + """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") @@ -81,17 +87,21 @@ def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: 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) + 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) + self.add_message("impossible-condition", node=node.test) def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool: - """Check if the condition is redundant.""" + """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 diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index 47a35a89f..a6615e7c4 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -24,7 +24,7 @@ def func(x: float): condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -39,7 +39,7 @@ def func(x: int): *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -53,7 +53,7 @@ def func(x: int): *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -73,7 +73,7 @@ def func(x: int): *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -92,7 +92,7 @@ def func(x: int): condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -118,7 +118,7 @@ def func(x: int): _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -144,7 +144,7 @@ def func(x: int): _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index 51f5a9907..0c44d2f70 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -24,7 +24,7 @@ def func(x: int): condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -39,7 +39,7 @@ def func(x: int): *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -58,7 +58,7 @@ def func(x: int): condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -78,7 +78,7 @@ def func(x: int): *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -92,7 +92,7 @@ def func(x: bool): *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) @@ -118,7 +118,7 @@ def func(x: int): _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) with self.assertAddsMessages( - pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node), + pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test), ignore_position=True, ): self.checker.visit_if(condition_node) diff --git a/tests/test_examples.py b/tests/test_examples.py index 4585a7f4f..c38e4d8c3 100644 --- a/tests/test_examples.py +++ b/tests/test_examples.py @@ -150,7 +150,7 @@ def test_examples_files_pyta(test_file: str, pyta_examples_symbols: dict[str, se found_pylint_message = checker_name in file_symbols assert ( found_pylint_message - ), f"Failed {test_file}. File does not add expected message {checker_name}: {file_symbols}." + ), f"Failed {test_file}. File does not add expected message {checker_name}: {file_symbols}." @pytest.mark.parametrize("test_file", get_file_paths(_PYCODESTYLE_PATH)) From 1e0a29e34b2132ce3df63140c0e7d4cd531ad7ad Mon Sep 17 00:00:00 2001 From: Raine-Yang-UofT Date: Wed, 18 Dec 2024 22:14:05 -0500 Subject: [PATCH 23/23] fix: fix false error reporting when condition is None Add checking for condition z3 expression to be not-None Add test cases for None condition --- python_ta/checkers/condition_logic_checker.py | 3 +++ .../test_impossible_condition_checker.py | 12 ++++++++++++ .../test_redundant_condition_checker.py | 12 ++++++++++++ 3 files changed, 27 insertions(+) diff --git a/python_ta/checkers/condition_logic_checker.py b/python_ta/checkers/condition_logic_checker.py index 3e58658ac..c2b8731e0 100644 --- a/python_ta/checkers/condition_logic_checker.py +++ b/python_ta/checkers/condition_logic_checker.py @@ -82,6 +82,9 @@ def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: 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) diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index a6615e7c4..73fbb438e 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -244,6 +244,18 @@ def func(x: str, y: int): with self.assertNoMessages(): self.checker.visit_if(condition_node) + def test_unparsed_condition(self): + src = """ + def func(a: int): + if a > 5: + print(a) + """ + + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + def _apply_cfg_visitor(self, src: str) -> nodes.NodeNG: z3v = Z3Visitor() mod = z3v.visitor.visit(astroid.parse(src)) diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index 0c44d2f70..465553f98 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -219,6 +219,18 @@ def func(x: str, y: int): with self.assertNoMessages(): self.checker.visit_if(condition_node) + def test_unparsed_condition(self): + src = """ + def func(a: int): + if a > 5: + print(a) + """ + + *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) + def _apply_cfg_visitor(self, src: str) -> nodes.NodeNG: z3v = Z3Visitor() mod = z3v.visitor.visit(astroid.parse(src))