Réduction d'un état et Fonctions de transfert

TP2/example_sign.py

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

TP2/example_sign_reduce.py

+from syntax import *
+from sign_analysis import state, abstract_env, sign, reduce_state
+
+x: ArithExpr = AEVar("x")
+y: ArithExpr = AEVar("y")
+
+test_eq: BoolExpr = BEEq(x,y)
+
+test_neq: BoolExpr = BENeg(test_eq)
+
+test_leq: BoolExpr = BELeq(x,y)
+
+test_gt: BoolExpr = BENeg(test_leq)
+
+def test(env: abstract_env) -> None:
+    res_eq = reduce_state(env,test_eq)
+    res_neq = reduce_state(env,test_neq)
+    res_leq = reduce_state(env,test_leq)
+    res_gt = reduce_state(env,test_gt)
+    print(f'In environment { {var: str(sign) for (var,sign) in env.items()} }')
+    print(f"{test_eq} -> {res_eq}")
+    print(f"{test_neq} -> {res_neq}")
+    print(f"{test_leq} -> {res_leq}")
+    print(f"{test_gt} -> {res_gt}")
+
+test({ 'x': sign.POS, 'y': sign.NEG })
+
+test({ 'x': sign.NZ, 'y': sign.NEG })
+
+test({ 'x': sign.POS, 'y': sign.SNEG })
+
+test({ 'x': sign.Z, 'y': sign.POS })
+

TP2/sign_analysis.py

@@ -501,7 +501,49 @@ def reduce_state(s: state, c: BoolExpr) -> state:
     if s is None:
         return s
     match c:
-        # To be completed (see course's slides)
+        case BEPlain(aexpr):
+            return reduce_eq_sign(s, "x", aexpr)
+        case BEEq(left_expr, right_expr):
+            if isinstance(left_expr, AEVar) and isinstance(right_expr, AEVar):
+                v1 = s[left_expr.var]
+                v2 = s[right_expr.var]
+                if (v1 == sign.SPOS and v2 == sign.SNEG) or (v1 == sign.SNEG and v2 == sign.SPOS):
+                    return None
+                return reduce_eq_sign(s, left_expr.var, right_expr)
+            elif isinstance(left_expr, AEVar):
+                return reduce_eq_sign(s, left_expr.var, right_expr)
+            elif isinstance(right_expr, AEVar):
+                return reduce_eq_sign(s, right_expr.var, left_expr)
+            return s
+        case BENeg(expr):
+            if isinstance(expr, BEEq):
+                left_expr, right_expr = expr.left_expr, expr.right_expr
+                if isinstance(left_expr, AEVar) and isinstance(right_expr, AEVar):
+                    return reduce_neq_sign(s, left_expr.var, right_expr)
+                elif isinstance(left_expr, AEVar):
+                    return reduce_neq_sign(s, left_expr.var, right_expr)
+                elif isinstance(right_expr, AEVar):
+                    return reduce_neq_sign(s, right_expr.var, left_expr)
+            elif isinstance(expr, BELeq):
+                left_expr, right_expr = expr.left_expr, expr.right_expr
+                if isinstance(left_expr, AEVar):
+                    return reduce_strict_lower_bound(s, left_expr.var, right_expr)
+                elif isinstance(right_expr, AEVar):
+                    return reduce_strict_upper_bound(s, right_expr.var, left_expr)
+            return s
+        case BELeq(left_expr, right_expr):
+            if isinstance(left_expr, AEVar) and isinstance(right_expr, AEVar):
+                v1 = s[left_expr.var]
+                v2 = s[right_expr.var]
+                if v1 == sign.SPOS and v2 == sign.SNEG:
+                    return None
+                if v1 == sign.POS and v2 == sign.NEG:
+                    return None
+            if isinstance(left_expr, AEVar):
+                return reduce_upper_bound(s, left_expr.var, right_expr)
+            elif isinstance(right_expr, AEVar):
+                return reduce_lower_bound(s, right_expr.var, left_expr)
+            return s
         case _:
             return s
 
@@ -544,18 +586,48 @@ class Sign_interp(Transfer[state]):
         return s
 
     def tr_set(self, s: state, v: str, e: ArithExpr) -> state:
-        raise NotImplementedError
+        """transfer function for assignment instructions"""
+        if s is None:
+            return None
+        res = eval_aexp(s, e)
+        if res is None:
+            return None
+        if isinstance(res, Top):
+            return s | {v: sign.INT}
+        return s | {v: res}
 
     def tr_test(self, s: state, c: BoolExpr) -> state:
-        raise NotImplementedError
+        """transfer function for test instructions"""
+        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:
+        """transfer function for error instructions"""
         if s is None:
             return s
         if isinstance(e, ArithExpr):
-            raise NotImplementedError
+            res = eval_aexp(s, e)
+            if res is None:
+                return None
+            if isinstance(res, Top):
+                return s
+            return s
         if isinstance(e, BoolExpr):
-            raise NotImplementedError
+            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: