From 3aaaf304f2fbdf48a63d1bb1425c52d9a999f70a Mon Sep 17 00:00:00 2001
From: Yassine Ettayeb <yassine.ettayeb@student-cs.fr>
Date: Fri, 28 Mar 2025 11:10:41 +0100
Subject: [PATCH] TP3: Treillis des intervalles, version finale
---
Pystan/config/interval_analysis.py | 77 ++++++++++++++++++------------
1 file changed, 47 insertions(+), 30 deletions(-)
diff --git a/Pystan/config/interval_analysis.py b/Pystan/config/interval_analysis.py
index b22a41c..e7ec977 100644
--- a/Pystan/config/interval_analysis.py
+++ b/Pystan/config/interval_analysis.py
@@ -405,44 +405,61 @@ def reduce_state(s: state,c: BoolExpr) -> state:
class Interval_analysis(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
- res: abstract_env = {}
- for var in self.variables:
- v1 = s1[var]
- v2 = s2[var]
- v = interval_join(v1,v2)
- res[var] = v
- return res
-
- def widen(self, s1:state, s2:state) -> state:
- raise NotImplementedError
-
- 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
- return True
-
- def tr_skip(self,s: state) -> 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 {v: interval_join(s1[v], s2[v]) for v in self.variables}
+
+ def widen(self, s1: state, s2: state) -> state:
+ if s1 is None:
+ return s2
+ if s2 is None:
+ return s1
+ return {v: interval_widen(s1[v], s2[v]) for v in self.variables}
+
+ def included(self, s1: state, s2: state) -> bool:
+ if s1 is None:
+ return True
+ if s2 is None:
+ return False
+ return all(interval_leq(s1[v], s2[v]) for v in self.variables)
+
+ 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:
+ if s is None:
+ return None
+ val = eval_aexp(s, e)
+ if val is None:
+ return None
+ s1 = s.copy()
+ s1[v] = val if not isinstance(val, Top) else Interval(None, None)
+ return s1
- def tr_test(self,s: state,c: BoolExpr) -> state:
- raise NotImplementedError
+ def tr_test(self, s: state, c: BoolExpr) -> state:
+ return reduce_state(s, c)
- def tr_err(self,s: state,e: Expr) -> state:
- raise NotImplementedError
+ def tr_err(self, s: state, e: Expr) -> state:
+ if s is None:
+ return None
+ if isinstance(e, ArithExpr):
+ return s if eval_aexp(s, e) is not None else None
+ if isinstance(e, BoolExpr):
+ return s if eval_bexp(s, e) is not None else None
+ return s
def analyze(i: Instr) -> None:
cfg = Cfg(i)
--
GitLab