TP3: Treillis des intervalles, version finale

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)