Condition Logic Checker

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

docs/checkers/index.md

@@ -2699,6 +2699,48 @@ python_ta.check_all(config={
 })
 ```
 
+(R9900)=
+
+### Redundant Condition (R9900)
+
+This error occurs when an `if` or `while` condition is guaranteed to be true.
+
+Example:
+
+```{literalinclude} /../examples/custom_checkers/r9900_redundant_condition.py
+
+```
+
+This error will only be checked if the `z3-solver` library is installed and `z3` option of PythonTA
+is enabled:
+
+```python
+import python_ta
+python_ta.check_all(config={
+    "z3": True
+})
+```
+
+### Impossible Condition (R9901)
+
+This error occurs when an `if` or `while` condition is guaranteed to be false.
+
+Example:
+
+```{literalinclude} /../examples/custom_checkers/r9901_impossible_condition.py
+
+```
+
+This error will only be checked if the `z3-solver` library is installed and `z3` option of PythonTA
+is enabled:
+
+```python
+import python_ta
+python_ta.check_all(config={
+    "z3": True
+})
+```
+
 ## Miscellaneous
 
 (E1305)=

examples/custom_checkers/r9900_redundant_condition.py

@@ -0,0 +1,23 @@
+def return_large_number(x: int) -> int:
+    """Return number x only if it's greater than 1000
+
+    Preconditions:
+        - 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:
+        # the condition `x > 5` is already guaranteed by `x > 10`
+        if x > 5:   # Error on this line
+            return x
+    return 0
+
+
+def redundant_condition(x: bool) -> None:
+    # the if condition is always true
+    if x or not x:     # Error on this line
+        print("redundant")

examples/custom_checkers/r9901_impossible_condition.py

@@ -0,0 +1,28 @@
+def print_none_negative_number(x: int) -> None:
+    """Print number x only if it's greater or equal to 0
+
+    Preconditions:
+        - x >= 0
+    """
+    # 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 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:
+    """Display numbers 0 to 2 in word"""
+    if x == 0:
+        "zero"
+    elif x == 1:
+        return "one"
+    elif x == 2:
+        return "two"
+    elif x == 2:    # Error on this line
+        return "two again"

python_ta/cfg/graph.py

@@ -56,15 +56,15 @@ 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
         self.cfg_id = cfg_id
         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,
@@ -276,7 +276,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:

python_ta/checkers/condition_logic_checker.py

@@ -0,0 +1,115 @@
+"""
+Check for redundant/impossible If or While conditions in functions based on z3 constraints
+"""
+
+from __future__ import annotations
+
+from typing import Any, Union
+
+try:
+    import z3
+
+    from ..cfg.graph import Z3Environment
+
+    z3_dependency_available = True
+except ImportError:
+    z3 = Any
+    Z3Environment = Any
+    z3_dependency_available = False
+
+from astroid import nodes
+from pylint.checkers import BaseChecker
+from pylint.checkers.utils import only_required_for_messages
+from pylint.lint import PyLinter
+
+
+class ConditionLogicChecker(BaseChecker):
+    name = "redundant-condition"
+    msgs = {
+        "R9900": (
+            """This condition will always evaluate to True.""",
+            "redundant-condition",
+            "Used when an If or While statement is always True. Requires the z3 configuration option to be True.",
+        ),
+        "R9901": (
+            """This condition will always evaluate to False.""",
+            "impossible-condition",
+            "Used when an If or While statement is always False. Requires the z3 configuration option to be True.",
+        ),
+    }
+    options = (
+        (
+            "z3",
+            {
+                "default": False,
+                "type": "yn",
+                "metavar": "<y or n>",
+                "help": "Use Z3 to perform logical feasibility analysis in program control flow.",
+            },
+        ),
+    )
+
+    @only_required_for_messages("redundant-condition", "impossible-condition")
+    def visit_if(self, node: nodes.If) -> None:
+        """Visit if statement"""
+        self._check_condition(node)
+
+    @only_required_for_messages("redundant-condition", "impossible-condition")
+    def visit_while(self, node: nodes.While) -> None:
+        """Visit while statement"""
+        self._check_condition(node)
+
+    def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None:
+        """Check whether a condition in an `if` or `while` statement is redundant
+        or impossible based on the feasible execution paths.
+
+        - A condition is redundant if for every feasible execution path
+        leading to the node, the condition must be True due to precedent constraints.
+        - A condition is impossible if for every feasible execution path
+        leading to the node, the condition must be False due to precedent constraints.
+        """
+        if (
+            not hasattr(node, "cfg_block")
+            or not z3_dependency_available
+            or not self.linter.config.z3
+        ):
+            return
+
+        node_block = node.cfg_block
+
+        # create node condition z3 constraint
+        condition_node = node.test
+        env = Z3Environment(node.frame().cfg.z3_vars, [])
+        z3_condition = env.parse_constraint(condition_node)
+
+        if z3_condition is None:
+            return
+
+        if all(
+            self._check_unsat(z3.And(*constraints), z3.Not(z3_condition))
+            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
+            for constraints in edge.z3_constraints.values()
+        ):
+            self.add_message("redundant-condition", node=node.test)
+
+        if all(
+            self._check_unsat(z3.And(*constraints), z3_condition)
+            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
+            for constraints in edge.z3_constraints.values()
+        ):
+            self.add_message("impossible-condition", node=node.test)
+
+    def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool:
+        """Check if the conjunction of the given constraints is unsatisfiable.
+
+        - prev_constraints (z3.ExprRef): Constraints from previous nodes.
+        - node_constraint (z3.ExprRef): The condition to check at the current node.
+        """
+        solver = z3.Solver()
+        solver.add(z3.And(prev_constraints, node_constraint))
+        return solver.check() == z3.unsat
+
+
+def register(linter: PyLinter) -> None:
+    """Required method to auto-register this checker to the linter."""
+    linter.register_checker(ConditionLogicChecker(linter))

python_ta/patches/transforms.py

@@ -27,7 +27,10 @@ def new_get_ast(self, filepath, modname, data):
 
         # Run the CFGVisitor
         try:
-            ast.accept(CFGVisitor())
+            if z3:
+                ast.accept(CFGVisitor(options={"separate-condition-blocks": True}))
+            else:
+                ast.accept(CFGVisitor())
         except Exception as e:
             logging.warning(f"Could not run Z3Visitor: {e}")