From 0225b3ccedb25a1ae13b12e0652d37cfe0d63cc1 Mon Sep 17 00:00:00 2001
From: Nicolas Descamps <nicolas.descamps@theodo.com>
Date: Tue, 1 Apr 2025 16:22:45 +0200
Subject: [PATCH] =?UTF-8?q?R=C3=A9duction=20d'un=20=C3=A9tat=20et=20Foncti?=
=?UTF-8?q?ons=20de=20transfert?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
TP2/example_sign.py | 4 ++
TP2/example_sign_reduce.py | 33 +++++++++++++++
TP2/sign_analysis.py | 82 +++++++++++++++++++++++++++++++++++---
3 files changed, 114 insertions(+), 5 deletions(-)
create mode 100644 TP2/example_sign.py
create mode 100644 TP2/example_sign_reduce.py
diff --git a/TP2/example_sign.py b/TP2/example_sign.py
new file mode 100644
index 0000000..6aa6de3
--- /dev/null
+++ b/TP2/example_sign.py
@@ -0,0 +1,4 @@
+from sign_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)
diff --git a/TP2/example_sign_reduce.py b/TP2/example_sign_reduce.py
new file mode 100644
index 0000000..17ed636
--- /dev/null
+++ b/TP2/example_sign_reduce.py
@@ -0,0 +1,33 @@
+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 })
+
diff --git a/TP2/sign_analysis.py b/TP2/sign_analysis.py
index fdb2a92..60f8d0d 100644
--- a/TP2/sign_analysis.py
+++ b/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:
--
GitLab