From 5461b73f97e89c9b392ad55d25bc4639adc81e62 Mon Sep 17 00:00:00 2001
From: Nicolas Descamps <nicolas.descamps@theodo.com>
Date: Tue, 1 Apr 2025 16:34:48 +0200
Subject: [PATCH] Treillis des intervalles, version finale
---
TP2/example_interval.py | 4 ++
TP2/interval_analysis.py | 124 ++++++++++++++++++++++++++++-----------
2 files changed, 95 insertions(+), 33 deletions(-)
create mode 100644 TP2/example_interval.py
diff --git a/TP2/example_interval.py b/TP2/example_interval.py
new file mode 100644
index 0000000..8aa35e0
--- /dev/null
+++ b/TP2/example_interval.py
@@ -0,0 +1,4 @@
+from interval_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)
diff --git a/TP2/interval_analysis.py b/TP2/interval_analysis.py
index 4f7b2e3..79d57e3 100644
--- a/TP2/interval_analysis.py
+++ b/TP2/interval_analysis.py
@@ -99,19 +99,29 @@ def interval_meet(i1: Interval, i2: Interval) -> Interval | None:
return Interval(l,u)
def interval_widen(i1: Interval, i2: Interval) -> Interval:
- if i1.lower_bound is None or i2.lower_bound is None:
+ """widening operator for intervals"""
+ if i1.lower_bound is None and i1.upper_bound is None:
+ return i2
+
+ if i1.lower_bound is None:
l = None
- elif i1.lower_bound <= i2.lower_bound:
- l = i1.lower_bound
- else:
+ elif i2.lower_bound is None:
l = None
- if i1.upper_bound is None or i2.upper_bound is None:
- u = None
- elif i1.upper_bound >= i2.upper_bound:
- u = i1.upper_bound
+ elif i2.lower_bound < i1.lower_bound:
+ l = None
else:
+ l = i1.lower_bound
+
+ if i1.upper_bound is None:
u = None
- return Interval(l,u)
+ elif i2.upper_bound is None:
+ u = None
+ elif i2.upper_bound > i1.upper_bound:
+ u = None
+ else:
+ u = i1.upper_bound
+
+ return Interval(l, u)
def has_strict_positive_val(i: Interval) -> bool:
return i.upper_bound is None or i.upper_bound > 0
@@ -431,50 +441,98 @@ def reduce_state(s: state,c: BoolExpr) -> state:
return reduce_leq(s,y,v.upper_bound - 1)
case _: return s
-class Interval_analysis(Transfer[state]):
+class Interval_interp(Transfer[state]):
variables: frozenset[str]
- def __init__(self,instr: Instr):
+
+ def __init__(self, instr: Instr):
self.variables = variables_of_instr(instr)
+
def bottom(self) -> state:
return None
+
def init_state(self) -> state:
- return dict.fromkeys(self.variables, Interval(None,None))
- def join(self,s1:state,s2:state) -> state:
- if s1 is None: return s2
- if s2 is None: return s1
+ return dict.fromkeys(self.variables, Interval(None, None))
+
+ def join(self, s1: state, s2: state) -> state:
+ if s1 is None:
+ return s2
+ if s2 is None:
+ return s1
res: abstract_env = {}
for var in self.variables:
- v1 = s1[var]
- v2 = s2[var]
- v = interval_join(v1,v2)
- res[var] = v
+ res[var] = interval_join(s1[var], s2[var])
return res
- def widen(self, s1:state, s2:state) -> state:
- raise NotImplementedError
+ def widen(self, s1: state, s2: state) -> state:
+ if s1 is None:
+ return s2
+ if s2 is None:
+ return s1
+ res: abstract_env = {}
+ for var in self.variables:
+ res[var] = interval_widen(s1[var], s2[var])
+ return res
- def included(self,s1: state,s2: state) -> bool:
- if s1 is None: return True
- if s2 is None: return False
+ def included(self, s1: state, s2: state) -> bool:
+ if s1 is None:
+ return True
+ if s2 is None:
+ return False
for var in self.variables:
- if not interval_leq(s1[var],s2[var]): return False
+ if not interval_leq(s1[var], s2[var]):
+ return False
return True
- def tr_skip(self,s: state) -> state:
+ def tr_skip(self, s: state) -> state:
return s
- def tr_set(self,s: state,v: str,e: ArithExpr) -> state:
- raise NotImplementedError
+ def tr_set(self, s: state, v: str, e: ArithExpr) -> state:
+ """transfer function for assignment"""
+ if s is None:
+ return None
+ res = eval_aexp(s, e)
+ if res is None:
+ return None
+ if isinstance(res, Top):
+ return s | {v: Interval(None, None)}
+ return s | {v: res}
- def tr_test(self,s: state,c: BoolExpr) -> state:
- raise NotImplementedError
+ def tr_test(self, s: state, c: BoolExpr) -> state:
+ """transfer function for test"""
+ if s is None:
+ return None
+ res = eval_bexp(s, c)
+ if res is None:
+ return None
+ if isinstance(res, BTop):
+ return s
+ if res:
+ return reduce_state(s, c)
+ return None
- def tr_err(self,s: state,e: Expr) -> state:
- raise NotImplementedError
+ def tr_err(self, s: state, e: Expr) -> state:
+ """transfer function for error"""
+ if s is None:
+ return s
+ if isinstance(e, ArithExpr):
+ res = eval_aexp(s, e)
+ if res is None:
+ return None
+ if isinstance(res, Top):
+ return s
+ return s
+ if isinstance(e, BoolExpr):
+ res = eval_bexp(s, e)
+ if res is None:
+ return None
+ if isinstance(res, BTop):
+ return s
+ return s
+ return s
def analyze(i: Instr) -> None:
cfg = Cfg(i)
- res = fixpoint_iteration(Interval_analysis(i), cfg)
+ res = fixpoint_iteration(Interval_interp(i), cfg)
for node in cfg.g.nodes:
print(f"State at {node}:")
s = res[node]
--
GitLab