Add negate Attribute to CFGEdge (#1076)

Add `negate` attribute to edge to indicate whether the edge condition is negated.
Refactor update_edge_z3_constraints to use `negate` instead of `label`.
Add get_label() method to account for both label and negate attributes.

CHANGELOG.md

@@ -82,6 +82,7 @@ Custom checkers:
 - Updated `graph.py` to augment control flow graph edges with z3 constraints
 - Added support for the `!=` operator and replaced dictionary indexing with `.get` in `ExprWrapper`.
 - Refactored `Z3Visitor` to use `safe_infer()` instead of `inferred()` and added handling of `AstroidError`.
+- Add `negate` attribute to `CFGEdge`
 
 ## [2.7.0] - 2024-12-14
 

python_ta/cfg/cfg_generator.py

@@ -138,8 +138,8 @@ def _visit(block: CFGBlock, graph: graphviz.Digraph, visited: Set[int], end: CFG
     visited.add(node_id)
 
     for edge in block.successors:
-        if edge.label is not None:
-            graph.edge(node_id, f"{graph.name}_{edge.target.id}", str(edge.label))
+        if edge.get_label() is not None:
+            graph.edge(node_id, f"{graph.name}_{edge.target.id}", edge.get_label())
         else:
             graph.edge(node_id, f"{graph.name}_{edge.target.id}")
         _visit(edge.target, graph, visited, end)

python_ta/cfg/graph.py

@@ -24,7 +24,6 @@
     AssignName,
     Break,
     Continue,
-    Expr,
     NodeNG,
     Raise,
     Return,
@@ -72,6 +71,7 @@ def create_block(
         pred: Optional[CFGBlock] = None,
         edge_label: Optional[Any] = None,
         edge_condition: Optional[NodeNG] = None,
+        edge_negate: Optional[bool] = None,
     ) -> CFGBlock:
         """Create a new CFGBlock for this graph.
 
@@ -80,13 +80,15 @@ def create_block(
         If edge_label is specified, set the corresponding edge in the CFG with that label.
 
         If edge_condition is specified, store the condition node in the corresponding edge.
+
+        edge_negate is not None only if edge_condition is specified
         """
         new_block = CFGBlock(self.block_count)
         self.unreachable_blocks.add(new_block)
 
         self.block_count += 1
         if pred:
-            self.link_or_merge(pred, new_block, edge_label, edge_condition)
+            self.link_or_merge(pred, new_block, edge_label, edge_condition, edge_negate)
         return new_block
 
     def link(self, source: CFGBlock, target: CFGBlock) -> None:
@@ -100,6 +102,7 @@ def link_or_merge(
         target: CFGBlock,
         edge_label: Optional[Any] = None,
         edge_condition: Optional[NodeNG] = None,
+        edge_negate: Optional[bool] = None,
     ) -> None:
         """Link source to target, or merge source into target if source is empty.
 
@@ -111,6 +114,8 @@ def link_or_merge(
         If edge_label is specified, set the corresponding edge in the CFG with that label.
 
         If edge_condition is specified, store the condition node in the corresponding edge.
+
+        edge_negate is not None only if edge_condition is specified
         """
         if source.is_jump():
             return
@@ -125,7 +130,7 @@ def link_or_merge(
             # represent any part of the program so it is redundant.
             self.unreachable_blocks.remove(source)
         else:
-            CFGEdge(source, target, edge_label, edge_condition)
+            CFGEdge(source, target, edge_label, edge_condition, edge_negate)
 
     def multiple_link_or_merge(self, source: CFGBlock, targets: List[CFGBlock]) -> None:
         """Link source to multiple target, or merge source into targets if source is empty.
@@ -258,10 +263,12 @@ def update_edge_z3_constraints(self) -> None:
                 if edge.condition is not None:
                     condition_z3_constraint = z3_environment.parse_constraint(edge.condition)
                     if condition_z3_constraint is not None:
-                        if edge.label == "True":
-                            z3_environment.add_constraint(condition_z3_constraint)
-                        elif edge.label == "False":
-                            z3_environment.add_constraint(Not(condition_z3_constraint))
+                        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()
 
@@ -321,29 +328,45 @@ class CFGEdge:
     Edges are directed, and in the future may be augmented with auxiliary metadata about the control flow.
 
     The condition attribute stores the AST node representing the condition tested in If and While statements.
+    The negate attribute stores the condition should be False (when `negate` is True) or condition should be true
+    (when `negate` is False)
     """
 
     source: CFGBlock
     target: CFGBlock
-    label: Optional[Any]
+    label: Optional[str]
     condition: Optional[NodeNG]
+    negate: Optional[bool]
     z3_constraints: Dict[int, List[ExprRef]]
 
     def __init__(
         self,
         source: CFGBlock,
         target: CFGBlock,
-        edge_label: Optional[Any] = None,
+        edge_label: Optional[str] = None,
         condition: Optional[NodeNG] = None,
+        negate: Optional[bool] = None,
     ) -> None:
         self.source = source
         self.target = target
         self.label = edge_label
         self.condition = condition
+        self.negate = negate
         self.source.successors.append(self)
         self.target.predecessors.append(self)
         self.z3_constraints = {}
 
+    def get_label(self) -> Optional[str]:
+        """Return the edge label if specified.
+        If `edge.label` is None, return the edge condition determined by the negation of `edge.negate`.
+        Return None if both `edge.label` and `edge.negate` are None.
+        """
+        if self.label is not None:
+            return self.label
+        elif self.negate is not None:
+            return str(not self.negate)
+        return None
+
 
 class Z3Environment:
     """Z3 Environment stores the Z3 variables and constraints in the current CFG path

python_ta/cfg/visitor.py

@@ -170,7 +170,7 @@ def visit_if(self, node: nodes.If) -> None:
 
         # Handle "then" branch and label it.
         then_block = self._current_cfg.create_block(
-            old_curr, edge_label="True", edge_condition=node.test
+            old_curr, edge_condition=node.test, edge_negate=False
         )
         self._current_block = then_block
         for child in node.body:
@@ -183,7 +183,7 @@ def visit_if(self, node: nodes.If) -> None:
         else:
             # Label the edge to the else block.
             else_block = self._current_cfg.create_block(
-                old_curr, edge_label="False", edge_condition=node.test
+                old_curr, edge_condition=node.test, edge_negate=True
             )
             self._current_block = else_block
             for child in node.orelse:
@@ -195,7 +195,10 @@ def visit_if(self, node: nodes.If) -> None:
         # Label the edge if there was no "else" branch
         if node.orelse == []:
             self._current_cfg.link_or_merge(
-                end_else, after_if_block, edge_label="False", edge_condition=node.test
+                end_else,
+                after_if_block,
+                edge_condition=node.test,
+                edge_negate=True,
             )
         else:
             self._current_cfg.link_or_merge(end_else, after_if_block)
@@ -227,7 +230,7 @@ def visit_while(self, node: nodes.While) -> None:
 
         # Handle "body" branch
         body_block = self._current_cfg.create_block(
-            test_block, edge_label="True", edge_condition=node.test
+            test_block, edge_condition=node.test, edge_negate=False
         )
         self._current_block = body_block
         for child in node.body:
@@ -240,7 +243,7 @@ def visit_while(self, node: nodes.While) -> None:
 
         # Handle "else" branch
         else_block = self._current_cfg.create_block(
-            test_block, edge_label="False", edge_condition=node.test
+            test_block, edge_condition=node.test, edge_negate=True
         )
         self._current_block = else_block
         for child in node.orelse:

tests/test_cfg/test_label_if.py

@@ -19,7 +19,7 @@ def _extract_edge_labels(cfg: ControlFlowGraph) -> Tuple[int, int]:
 
     The returned 2-tuple is of the form (# of True, # of False).
     """
-    labels = [edge.label for edge in cfg.get_edges()]
+    labels = [edge.get_label() for edge in cfg.get_edges()]
     return labels.count("True"), labels.count("False")
 
 

tests/test_cfg/test_label_while.py

@@ -16,13 +16,13 @@ def build_cfg(src: str) -> ControlFlowGraph:
 
 def _extract_labels(cfg: ControlFlowGraph) -> Set[str]:
     """Return a set of all the labels in this cfg."""
-    labels = {edge.label for edge in cfg.get_edges() if edge.label is not None}
+    labels = {edge.get_label() for edge in cfg.get_edges() if edge.get_label() is not None}
     return labels
 
 
 def _extract_num_labels(cfg: ControlFlowGraph) -> int:
     """Return the number of labelled edges in the cfg."""
-    return sum(1 for edge in cfg.get_edges() if edge.label is not None)
+    return sum(1 for edge in cfg.get_edges() if edge.get_label() is not None)
 
 
 def _extract_edge_conditions(cfg: ControlFlowGraph) -> List[str]: