From 7d0f5785698c5325dc30740f1773e17158960367 Mon Sep 17 00:00:00 2001
From: Nicolas Descamps <nicolas.descamps@theodo.com>
Date: Tue, 1 Apr 2025 16:31:26 +0200
Subject: [PATCH] =?UTF-8?q?Ajout=20de=20l'=C3=A9largissement?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
TP2/cfg.py | 9 ++++---
TP2/example_widen.py | 61 ++++++++++++++++++++++++++++++++++++++++++++
TP2/iteration.py | 13 ++++++++--
3 files changed, 77 insertions(+), 6 deletions(-)
create mode 100644 TP2/example_widen.py
diff --git a/TP2/cfg.py b/TP2/cfg.py
index 08fa8d0..04a518f 100644
--- a/TP2/cfg.py
+++ b/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
diff --git a/TP2/example_widen.py b/TP2/example_widen.py
new file mode 100644
index 0000000..c9372be
--- /dev/null
+++ b/TP2/example_widen.py
@@ -0,0 +1,61 @@
+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}')
diff --git a/TP2/iteration.py b/TP2/iteration.py
index 9af0e5a..1d421b6 100644
--- a/TP2/iteration.py
+++ b/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.
"""
--
GitLab