TP3: Ajout de l'élargissement

Pystan/config/cfg.py

@@ -17,6 +17,7 @@ class Label:
 @dataclass
 class LSkip(Label):
     """label skip (does nothing)"""
+    is_back_edge: bool
     def __str__(self):
         return "skip"
 
@@ -78,47 +79,41 @@ class Graph:
             self.nodes += [n2]
         n1.succs += [(n2,l)]
 
-def cfg_aux(g:Graph,e:Node,i:Node,instr:Instr) -> Node:
-    """auxiliary function to build a CfG
-    takes as argument a graph, the error node, the node starting
-    the current instruction, and the instruction itself, returns
-    the final node of current instruction
-    """
+def cfg_aux(g: "Cfg", e: Node, i: Node, instr: Instr) -> Node:
     match instr:
         case ISkip():
-           f = g.new_node()
-           g.new_edge(i,f,LSkip())
-           return f
-        case ISet(var,expr):
             f = g.new_node()
-            g.new_edge(i,f,LSet(var,expr))
-            g.new_edge(i,e,LErr(expr))
+            g.new_edge(i, f, LSkip(is_back_edge=False))
             return f
-        case ISeq(first,second):
-            m = cfg_aux(g,e,i,first)
-            return cfg_aux(g,e,m,second)
-        case ICond(cond,true_branch,false_branch):
-            t = g.new_node()
-            f = g.new_node()
-            g.new_edge(i,t,LTest(cond))
-            g.new_edge(i,f,LTest(BENeg(cond)))
-            g.new_edge(i,e,LErr(cond))
-            tf = cfg_aux(g,e,t,true_branch)
-            ff = cfg_aux(g,e,f,false_branch)
+
+        case ISet(v, expr):
             f = g.new_node()
-            g.new_edge(tf,f,LSkip())
-            g.new_edge(ff,f,LSkip())
+            g.new_edge(i, f, LSet(v, expr))
+            g.new_edge(i, e, LErr(expr))
             return f
-        case ILoop(cond,body):
+
+        case ISeq(i1, i2):
+            m = cfg_aux(g, e, i, i1)
+            return cfg_aux(g, e, m, i2)
+
+        case ICond(cond, i1, i2):
+            f = g.new_node()
+            g.new_edge(i, f, LTest(BENeg(cond)))
+            g.new_edge(i, e, LErr(cond))
+            t = cfg_aux(g, e, f, i1)
+            g.new_edge(i, f, LTest(cond))
+            return cfg_aux(g, e, t, i2)
+
+        case ILoop(cond, body):
             ib = g.new_node()
             f = g.new_node()
-            g.new_edge(i,ib,LTest(cond))
-            g.new_edge(i,f,LTest(BENeg(cond)))
-            g.new_edge(i,e,LErr(cond))
-            fb = cfg_aux(g,e,ib,body)
-            g.new_edge(fb,i,LSkip())
+            g.new_edge(i, ib, LTest(cond))          # vers boucle si cond vrai
+            g.new_edge(i, f, LTest(BENeg(cond)))    # sortie si cond faux
+            g.new_edge(i, e, LErr(cond))            # erreur si test échoue
+            fb = cfg_aux(g, e, ib, body)
+            g.new_edge(fb, i, LSkip(is_back_edge=True))  # <-- arc de retour
             return f
-        case _: assert False
+
 
 class Cfg:
     """describes a CfG"""

Pystan/config/iteration.py

@@ -10,6 +10,11 @@ from typing import Protocol
 
 class Transfer[S](Protocol):
     """lists the functions that must be implemented for a static analysis over Lattice S"""
+
+    def widen(self, s1: S, s2: S) -> S:
+        """widening operator used on back edges (default: join)"""
+        return self.join(s1, s2)
+    
     def bottom(self) -> S:
         """the empty state, associated to unvisited nodes"""
         ...
@@ -86,7 +91,7 @@ def fixpoint_iteration[T](transfer: Transfer[T], cfg: Cfg) -> dict[Node,T]:
     output maps each node to the computed state
     """
 
-    # initialisation
+    # initialisation des états
     mapping: dict[Node, T] = {}
     for node in cfg.g.nodes:
         if node == cfg.init_node:
@@ -94,17 +99,17 @@ def fixpoint_iteration[T](transfer: Transfer[T], cfg: Cfg) -> dict[Node,T]:
         else:
             mapping[node] = transfer.bottom()
 
-    # initialisation de la worklist avec les successeurs du nœud initial
+    # initialisation de la worklist avc les successeurs du noeud initial
     worklist: list[tuple[Node, Node, Label]] = []
     for (dst, label) in cfg.init_node.succs:
         worklist.append((cfg.init_node, dst, label))
 
-    # itération principale
+    # iter principale
     while worklist:
         src, dst, label = worklist.pop(0)
         src_state = mapping[src]
 
-        # applique la fonction de transfert selon le label
+        # applique la fonction de transfert en fonction du label
         match label:
             case LSkip():
                 new_state = transfer.tr_skip(src_state)
@@ -117,13 +122,15 @@ def fixpoint_iteration[T](transfer: Transfer[T], cfg: Cfg) -> dict[Node,T]:
             case _:
                 continue  # ou raise NotImplementedError
 
-        # joindre avc l'ancien état
-        joined_state = transfer.join(mapping[dst], new_state)
+        # appliquer le widen sur un arc de retour, sinon un simple join
+        if isinstance(label, LSkip) and label.is_back_edge:
+            joined_state = transfer.widen(mapping[dst], new_state)
+        else:
+            joined_state = transfer.join(mapping[dst], new_state)
 
-        # si  nouvel état apporte de l'information, on met à jour
+        # Màj si l'état évolue
         if not transfer.included(joined_state, mapping[dst]):
             mapping[dst] = joined_state
-            # + on ajoute les successeurs à la worklist
             for (succ, lab) in dst.succs:
                 worklist.append((dst, succ, lab))