Check CFGEdge constraint feasibility using Z3 (#1084)

Implement update_edge_feasibility function that traverses through CFG and checks for logically impossible edges.

* feat: implement rendering of infeasible CFG edges in light grey

CHANGELOG.md

@@ -26,8 +26,10 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 - Removed `node` attribute for `Z3Parser`
 - Renamed `reduce` method of `Z3Parser` to `parse`
 - Renamed `test_expr_wrapper` to `test_z3_parser`
+- Added `is_feasible` attribute for `CFGEdge` and implemented update to edge feasibility based on lists of Z3 constraints
 - Refactored codebase to use modern type annotations. Replaced `List` with `list`, `Dict` with `dict`, `Set` with `set`, and `Tuple` with `tuple`
 - Checked for variable reassignment in `AugAssign` and `AnnAssign` node in parsing edge Z3 constraints
+- Rendered logically infeasible control flow graph edges in light grey
 - Modified `test_snapshot_to_json_sets_primitive` for Python 3.8 compatibility
 
 ## [2.8.1] - 2024-08-19

python_ta/cfg/cfg_generator.py

@@ -13,6 +13,14 @@
 from astroid import nodes
 from astroid.builder import AstroidBuilder
 
+try:
+    from ..transforms.z3_visitor import Z3Visitor
+
+    z3_dependency_available = True
+except ImportError:
+    Z3Visitor = Any
+    z3_dependency_available = False
+
 from .graph import CFGBlock, ControlFlowGraph
 from .visitor import CFGVisitor
 
@@ -61,6 +69,12 @@ def _generate(
 
     file_name = os.path.splitext(os.path.basename(abs_path))[0]
     module = AstroidBuilder().file_build(abs_path)
+
+    # invoke Z3Visitor if z3 dependency is available
+    if z3_dependency_available:
+        z3v = Z3Visitor()
+        module = z3v.visitor.visit(module)
+
     visitor = CFGVisitor(options=visitor_options)
     module.accept(visitor)
 
@@ -140,8 +154,11 @@ def _visit(block: CFGBlock, graph: graphviz.Digraph, visited: set[int], end: CFG
     visited.add(node_id)
 
     for edge in block.successors:
+        color = "black" if edge.is_feasible else "lightgrey"
         if edge.get_label() is not None:
-            graph.edge(node_id, f"{graph.name}_{edge.target.id}", edge.get_label())
+            graph.edge(
+                node_id, f"{graph.name}_{edge.target.id}", label=edge.get_label(), color=color
+            )
         else:
-            graph.edge(node_id, f"{graph.name}_{edge.target.id}")
+            graph.edge(node_id, f"{graph.name}_{edge.target.id}", color=color)
         _visit(edge.target, graph, visited, end)

python_ta/cfg/graph.py

@@ -3,7 +3,15 @@
 from typing import Any, Dict, Generator, List, Optional, Set
 
 try:
-    from z3 import Z3_OP_UNINTERPRETED, ExprRef, Not, Z3Exception, is_const
+    from z3 import (
+        Z3_OP_UNINTERPRETED,
+        ExprRef,
+        Not,
+        Solver,
+        Z3Exception,
+        is_const,
+        unsat,
+    )
 
     from ..z3.z3_parser import Z3ParseException, Z3Parser
 
@@ -16,6 +24,8 @@
     is_const = Any
     Z3_OP_UNINTERPRETED = Any
     Z3ParseException = Any
+    Solver = Any
+    unsat = Any
     z3_dependency_available = False
 
 from astroid import (
@@ -288,6 +298,25 @@ def _handle_variable_reassignment(self, node: NodeNG, env: Z3Environment) -> Non
         elif isinstance(node, (AugAssign, AnnAssign)):
             env.assign(node.target.name)
 
+    def update_edge_feasibility(self) -> None:
+        """Traverse through edges in DFS order and update is_feasible
+        attribute of each edge. Edges that are unreachable with the given
+        set of Z3 constraints will have is_feasible set to False
+        """
+        if not z3_dependency_available:
+            return
+
+        def _check_unsat(constraints: List[ExprRef]) -> bool:
+            solver = Solver()
+            solver.add(constraints)
+            return solver.check() == unsat
+
+        for edge in self.get_edges():
+            if len(edge.z3_constraints) > 0:
+                edge.is_feasible = not all(
+                    _check_unsat(constraints) for constraints in edge.z3_constraints.values()
+                )
+
 
 class CFGBlock:
     """A node in a control flow graph.
@@ -346,6 +375,7 @@ class CFGEdge:
     condition: Optional[NodeNG]
     negate: Optional[bool]
     z3_constraints: Dict[int, List[ExprRef]]
+    is_feasible: bool
 
     def __init__(
         self,
@@ -363,6 +393,7 @@ def __init__(
         self.source.successors.append(self)
         self.target.predecessors.append(self)
         self.z3_constraints = {}
+        self.is_feasible = True
 
     def get_label(self) -> Optional[str]:
         """Return the edge label if specified.

python_ta/cfg/visitor.py

@@ -146,6 +146,7 @@ def visit_functiondef(self, func: nodes.FunctionDef) -> None:
         if hasattr(func, "z3_constraints"):
             self._current_cfg.precondition_constraints = func.z3_constraints
             self._current_cfg.update_edge_z3_constraints()
+            self._current_cfg.update_edge_feasibility()
 
         self._current_block = previous_block
         self._current_cfg = previous_cfg

tests/test_cfg/snapshots/funcs_only.gv

@@ -2,29 +2,29 @@ digraph funcs_only {
 	node [fontname="Courier New" shape=box]
 	subgraph cluster_0 {
 		cluster_0_0 [label="self\l" fillcolor=white style=filled]
-		cluster_0_0 -> cluster_0_2
+		cluster_0_0 -> cluster_0_2 [color=black]
 		cluster_0_2 [label="print('method')\l" fillcolor=white style=filled]
-		cluster_0_2 -> cluster_0_1
+		cluster_0_2 -> cluster_0_1 [color=black]
 		cluster_0_1 [label="\l" fillcolor=black style=filled]
 		fontname="Courier New" label="MyClass.foo"
 	}
 	subgraph cluster_1 {
 		cluster_1_0 [label="\l" fillcolor=white style=filled]
-		cluster_1_0 -> cluster_1_2
+		cluster_1_0 -> cluster_1_2 [color=black]
 		cluster_1_2 [label="a = 5\l" fillcolor=white style=filled]
-		cluster_1_2 -> cluster_1_1
+		cluster_1_2 -> cluster_1_1 [color=black]
 		cluster_1_1 [label="\l" fillcolor=black style=filled]
 		fontname="Courier New" label=foo
 	}
 	subgraph cluster_2 {
 		cluster_2_0 [label="\l" fillcolor=white style=filled]
-		cluster_2_0 -> cluster_2_2
+		cluster_2_0 -> cluster_2_2 [color=black]
 		cluster_2_2 [label="a > 0\l" fillcolor=white style=filled]
-		cluster_2_2 -> cluster_2_3 [label=True]
+		cluster_2_2 -> cluster_2_3 [label=True color=black]
 		cluster_2_3 [label="owl = 'hoo'\l" fillcolor=white style=filled]
-		cluster_2_3 -> cluster_2_1
+		cluster_2_3 -> cluster_2_1 [color=black]
 		cluster_2_1 [label="\l" fillcolor=black style=filled]
-		cluster_2_2 -> cluster_2_1 [label=False]
+		cluster_2_2 -> cluster_2_1 [label=False color=black]
 		fontname="Courier New" label=hoo
 	}
 }

tests/test_cfg/snapshots/my_file.gv

@@ -2,23 +2,23 @@ digraph my_file {
 	node [fontname="Courier New" shape=box]
 	subgraph cluster_0 {
 		cluster_0_0 [label="\ldef foo() -> None:\l    for i in range(1, 10):\l        if i < 5:\l            print('hi')\l" fillcolor=white style=filled]
-		cluster_0_0 -> cluster_0_1
+		cluster_0_0 -> cluster_0_1 [color=black]
 		cluster_0_1 [label="\l" fillcolor=black style=filled]
 		fontname="Courier New" label=__main__
 	}
 	subgraph cluster_1 {
 		cluster_1_0 [label="\l" fillcolor=white style=filled]
-		cluster_1_0 -> cluster_1_2
+		cluster_1_0 -> cluster_1_2 [color=black]
 		cluster_1_2 [label="range(1, 10)\l" fillcolor=white style=filled]
-		cluster_1_2 -> cluster_1_3
+		cluster_1_2 -> cluster_1_3 [color=black]
 		cluster_1_3 [label="i\l" fillcolor=white style=filled]
-		cluster_1_3 -> cluster_1_5
+		cluster_1_3 -> cluster_1_5 [color=black]
 		cluster_1_5 [label="i < 5\l" fillcolor=white style=filled]
-		cluster_1_5 -> cluster_1_6 [label=True]
+		cluster_1_5 -> cluster_1_6 [label=True color=black]
 		cluster_1_6 [label="print('hi')\l" fillcolor=white style=filled]
-		cluster_1_6 -> cluster_1_3
-		cluster_1_5 -> cluster_1_3 [label=False]
-		cluster_1_3 -> cluster_1_1
+		cluster_1_6 -> cluster_1_3 [color=black]
+		cluster_1_5 -> cluster_1_3 [label=False color=black]
+		cluster_1_3 -> cluster_1_1 [color=black]
 		cluster_1_1 [label="\l" fillcolor=black style=filled]
 		fontname="Courier New" label=foo
 	}

tests/test_cfg/test_cfg_generator.py

@@ -3,6 +3,7 @@
 """
 
 import os.path
+from unittest.mock import patch
 
 import pytest
 
@@ -141,3 +142,13 @@ def test_mod_not_str(capsys) -> None:
     captured = capsys.readouterr()
 
     assert captured.out == expected
+
+
+@patch.dict("sys.modules", {"z3": None})
+def test_z3_dependency_uninstalled(snapshot, create_cfg) -> None:
+    """Test that generate_cfg does not raise any error when z3 is not installed"""
+    _, _, gv_file_io = create_cfg
+
+    # Check that the contents match with the snapshot
+    snapshot.snapshot_dir = "snapshots"
+    snapshot.assert_match(gv_file_io.read(), "my_file.gv")