Ajout de l'élargissement

TP2/cfg.py

@@ -17,6 +17,7 @@ class Label:
 @dataclass
 class LSkip(Label):
     """label skip (does nothing)"""
+    is_back_edge: bool = False
     def __str__(self):
         return "skip"
 
@@ -87,7 +88,7 @@ def cfg_aux(g:Graph,e:Node,i:Node,instr:Instr) -> Node:
     match instr:
         case ISkip():
            f = g.new_node()
-           g.new_edge(i,f,LSkip())
+           g.new_edge(i,f,LSkip(False))
            return f
         case ISet(var,expr):
             f = g.new_node()
@@ -106,8 +107,8 @@ def cfg_aux(g:Graph,e:Node,i:Node,instr:Instr) -> Node:
             tf = cfg_aux(g,e,t,true_branch)
             ff = cfg_aux(g,e,f,false_branch)
             f = g.new_node()
-            g.new_edge(tf,f,LSkip())
-            g.new_edge(ff,f,LSkip())
+            g.new_edge(tf,f,LSkip(False))
+            g.new_edge(ff,f,LSkip(False))
             return f
         case ILoop(cond,body):
             ib = g.new_node()
@@ -116,7 +117,7 @@ def cfg_aux(g:Graph,e:Node,i:Node,instr:Instr) -> Node:
             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(fb,i,LSkip(True))  
             return f
         case _: assert False
 

TP2/example_widen.py

+from iteration import Transfer, fixpoint_iteration
+from syntax import *
+from cfg import Cfg
+from example_opsem import factorial
+
+@dataclass
+class Number_step:
+    bound: int | None
+    def __str__(self):
+        if self.bound is None: return "+∞"
+        else: return str(self.bound)
+
+type S = Number_step | None
+
+class Analysis(Transfer[S]):
+    def bottom(self) -> S:
+        return None
+
+    def init_state(self) -> S:
+        return Number_step(0)
+
+    def join(self,s1:S,s2:S) -> S:
+        if s1 is None: return s2
+        if s2 is None: return s1
+        if s1.bound is None: return s1
+        if s2.bound is None: return s2
+        return Number_step(max(s1.bound, s2.bound))
+
+    def widen(self, s1:S, s2:S) -> S:
+        if s1 is None: return s2
+        if s2 is None: return s1
+        if s1.bound is None: return s1
+        if s2.bound is None: return s2
+        if s1.bound < s2.bound: return Number_step(None)
+        return s1
+
+    def included(self,s1: S,s2: S) -> bool:
+        if s1 is None: return True
+        if s2 is None: return False
+        if s2.bound is None: return True
+        if s1.bound is None: return False
+        return s1.bound <= s2.bound
+
+    def tr_skip(self,s: S) -> S:
+        if s is None: return None
+        if s.bound is None: return s
+        return Number_step(s.bound + 1)
+
+    def tr_set(self,s: S,v: str,e: ArithExpr) -> S:
+        return self.tr_skip(s)
+
+    def tr_test(self,s: S,c: BoolExpr) -> S:
+        return self.tr_skip(s)
+
+    def tr_err(self,s: S,e: Expr) -> S:
+        return self.tr_skip(s)
+
+res = fixpoint_iteration(Analysis(),Cfg(factorial))
+
+for (node, nb) in res.items():
+    print(f'{node} -> {nb}')

TP2/iteration.py

@@ -25,6 +25,10 @@ class Transfer[S](Protocol):
         """join of two states when merging branches"""
         ...
 
+    def widen(self, s1: S, s2: S) -> S:
+        """widening operator for accelerating convergence"""
+        return self.join(s1, s2)
+
     def included(self, s1: S, s2: S) -> bool:
         """return True when the first state is included in the second"""
         ...
@@ -76,7 +80,12 @@ def fixpoint_iteration[T](transfer: Transfer, cfg: Cfg) -> dict[Node, T]:
             s_new = transfer.tr_err(s_src, label.err)
         else:
             s_new = s_src
-        new_state = transfer.join(mapping[dst], s_new)
+
+        if isinstance(label, LSkip) and label.is_back_edge:
+            new_state = transfer.widen(mapping[dst], s_new)
+        else:
+            new_state = transfer.join(mapping[dst], s_new)
+
         if not transfer.included(mapping[dst], new_state):
             mapping[dst] = new_state
             for succ, lab in dst.succs:
@@ -87,5 +96,5 @@ def fixpoint_iteration[T](transfer: Transfer, cfg: Cfg) -> dict[Node, T]:
 """
 # À quoi correspondent les nœuds indiqués comme inatteignables par l'analyse?
 
-Les nœuds inatteignables correspondent aux branches du programme qui ne peuvent jamais être exécutées, car leur condition s’évalue toujours à False dans l’analyse.
+Les nœuds inatteignables correspondent aux branches du programme qui ne peuvent jamais être exécutées, car leur condition s'évalue toujours à False dans l'analyse.
 """