TP3: évaluation des expressions

Pystan/config/sign_analysis.py

@@ -2,12 +2,16 @@
 """
 implements a sign analysis
 """
-from enum import Enum
+from enum import Enum, auto
 from dataclasses import dataclass
 from cfg import Cfg
 from iteration import Transfer, fixpoint_iteration
 from syntax import *
 
+
+
+
+
 class sign(Enum):
     SNEG = auto()
     SPOS = auto()
@@ -172,27 +176,87 @@ def eval_aexp(env: abstract_env, e: ArithExpr) -> sign | Top | None:
     """
     match e:
         case AECst(value):
-            raise NotImplementedError
+            if value == 0:
+                return sign.Z
+            elif value > 0:
+                return sign.POS
+            else:
+                return sign.NEG
+
         case AEVar(var):
-            raise NotImplementedError
-        case AEUop(uop,expr):
-            raise NotImplementedError
-        case AEBop(bop,left_expr,right_expr):
-            raise NotImplementedError
-        case _: pass
+            return env.get(var, None)
+
+        case AEUop(uop, expr):
+            val = eval_aexp(env, expr)
+            if val is None or isinstance(val, Top):
+                return val
+            if uop == Uop.OPP:
+                return sign_opp(val)
+
+        case AEBop(bop, left_expr, right_expr):
+            l = eval_aexp(env, left_expr)
+            r = eval_aexp(env, right_expr)
+            if l is None or r is None:
+                return None
+            if isinstance(l, Top) or isinstance(r, Top):
+                return Top()
+            match bop:
+                case Bop.ADD:
+                    return sign_add(l, r)
+                case Bop.MUL:
+                    return sign_mul(l, r)
+                case Bop.DIV:
+                    return sign_div(l, r)
+
+    return None
 
 def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None:
     """abstract evaluation of a boolean expression"""
     match e:
         case BEPlain(aexpr):
-            raise NotImplementedError
-        case BEEq(left_expr,right_expr):
-            raise NotImplementedError
-        case BELeq(left_expr,right_expr):
-            raise NotImplementedError
+            val = eval_aexp(env, aexpr)
+            if val is None:
+                return None
+            if isinstance(val, Top):
+                return BTop(True)
+            return val != sign.Z
+
+        case BEEq(left_expr, right_expr):
+            l = eval_aexp(env, left_expr)
+            r = eval_aexp(env, right_expr)
+            if l is None or r is None:
+                return None
+            if isinstance(l, Top) or isinstance(r, Top):
+                return BTop(True)
+            return l == r
+
+        case BELeq(left_expr, right_expr):
+            l = eval_aexp(env, left_expr)
+            r = eval_aexp(env, right_expr)
+            if l is None or r is None:
+                return None
+            if isinstance(l, Top) or isinstance(r, Top):
+                return BTop(True)
+            match l, r:
+                case sign.SNEG | sign.NEG, sign.Z | sign.POS | sign.SPOS:
+                    return True
+                case sign.Z, sign.POS | sign.SPOS:
+                    return True
+                case sign.POS, sign.SNEG | sign.NEG:
+                    return False
+                case _:
+                    return BTop(False)
+
         case BENeg(expr):
-            raise NotImplementedError
-        case _: pass
+            b = eval_bexp(env, expr)
+            if b is None:
+                return None
+            if isinstance(b, BTop):
+                return b
+            return not b
+
+    return None
+
 
 def reduce_eq_sign(s: state, x: str, expr: ArithExpr) -> state:
     """reduce the value associated to x in s under the hypothesis that x == expr"""