Treillis des intervalles, version finale

TP2/example_interval.py

+from interval_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)

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]