From d9519b781a3a0d998f677390b75e06772c109553 Mon Sep 17 00:00:00 2001
From: Nicolas Descamps <nicolas.descamps@theodo.com>
Date: Tue, 1 Apr 2025 16:09:38 +0200
Subject: [PATCH] =?UTF-8?q?=C3=A9valuation=20des=20expressions?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
TP2/example_sign_eval_exp.py | 28 ++
TP2/sign_analysis.py | 577 +++++++++++++++++++++++++++++++++++
2 files changed, 605 insertions(+)
create mode 100644 TP2/example_sign_eval_exp.py
create mode 100644 TP2/sign_analysis.py
diff --git a/TP2/example_sign_eval_exp.py b/TP2/example_sign_eval_exp.py
new file mode 100644
index 0000000..c8bdd99
--- /dev/null
+++ b/TP2/example_sign_eval_exp.py
@@ -0,0 +1,28 @@
+from syntax import *
+from sign_analysis import eval_aexp, eval_bexp, abstract_env, sign
+
+x: ArithExpr = AEVar("x")
+y: ArithExpr = AEVar("y")
+
+# y * (x - x / y)
+test_aexp: ArithExpr = AEBop(Bop.MUL,y,AEBop(Bop.ADD,x, AEUop(Uop.OPP,AEBop(Bop.DIV,x,y))))
+
+# ! (x - y <= y * (x - x/y))
+test_bexp: BoolExpr = BENeg(BELeq(AEBop(Bop.ADD,x,AEUop(Uop.OPP,y)),test_aexp))
+
+def test(env: abstract_env) -> None:
+ res_a = eval_aexp(env,test_aexp)
+ res_b = eval_bexp(env,test_bexp)
+ print(f'In environment { {var: str(sign) for (var,sign) in env.items()} }')
+ print(f"{test_aexp} -> {res_a}")
+ print(f"{test_bexp} -> {res_b}")
+
+test({ 'x': sign.SPOS, 'y': sign.SPOS })
+
+test({ 'x': sign.NEG, 'y': sign.NEG })
+
+test({ 'x': sign.INT, 'y': sign.Z })
+
+test({ 'x': sign.POS, 'y': sign.NZ })
+
+test({})
diff --git a/TP2/sign_analysis.py b/TP2/sign_analysis.py
new file mode 100644
index 0000000..fdb2a92
--- /dev/null
+++ b/TP2/sign_analysis.py
@@ -0,0 +1,577 @@
+# pyright: strict
+"""
+implements a sign analysis
+"""
+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()
+ Z = auto()
+ NEG = auto()
+ POS = auto()
+ NZ = auto()
+ INT = auto()
+
+
+class Top:
+ def __str__(self):
+ return "TOP"
+
+
+@dataclass
+class BTop:
+ """class used for the evaluation of boolean expressions
+
+ BTop(False) indicates that we don't know if the result is True or False, but
+ that the evaluation cannot lead to an error
+ BTop(True) indicates that we neither know the result nor whether an error can occur
+ """
+
+ has_error: bool
+
+ def __str__(self):
+ if self.has_error:
+ return "TOP (maybe error)"
+ else:
+ return "TOP (no error)"
+
+
+type abstract_env = dict[str, sign]
+"""mapping from variables to abstract values.
+
+As with concrete environment, a variable not in the dictionary will
+lead to an error if we try to obtain its value
+"""
+type state = abstract_env | None
+"""abstract state is either an abstract env or bottom
+"""
+
+
+def sign_leq(v1: sign, v2: sign) -> bool:
+ """order relation on the sign lattice"""
+ if v1 == v2:
+ return True
+ match v1, v2:
+ case _, sign.INT:
+ return True
+ case sign.INT, _:
+ return False
+ case sign.SNEG, (sign.NEG | sign.NZ):
+ return True
+ case sign.SPOS, (sign.POS | sign.NZ):
+ return True
+ case sign.Z, (sign.POS | sign.NEG):
+ return True
+ case sign.NEG, sign.NZ:
+ return True
+ case sign.POS, sign.NZ:
+ return True
+ case _:
+ return False
+
+
+def sign_join(v1: sign, v2: sign) -> sign:
+ """computes least upper bound"""
+ match v1, v2:
+ case sign.INT, _:
+ return sign.INT
+ case _, sign.INT:
+ return sign.INT
+ case sign.NZ, (sign.NZ | sign.SPOS | sign.SNEG):
+ return sign.NZ
+ case sign.NZ, _:
+ return sign.INT
+ case sign.NEG, (sign.NEG | sign.SNEG | sign.Z):
+ return sign.NEG
+ case sign.NEG, _:
+ return sign.INT
+ case sign.POS, (sign.POS | sign.SPOS | sign.Z):
+ return sign.POS
+ case sign.POS, _:
+ return sign.INT
+ case sign.SNEG, sign.SNEG:
+ return sign.SNEG
+ case sign.SNEG, (sign.Z | sign.NEG):
+ return sign.NEG
+ case sign.SNEG, (sign.SPOS | sign.NZ):
+ return sign.NZ
+ case sign.SNEG, _:
+ return sign.INT
+ case sign.SPOS, sign.SPOS:
+ return sign.SPOS
+ case sign.SPOS, (sign.POS | sign.Z):
+ return sign.POS
+ case sign.SPOS, (sign.SNEG | sign.NZ):
+ return sign.NZ
+ case sign.SPOS, _:
+ return sign.INT
+ case sign.Z, sign.SNEG:
+ return sign.NEG
+ case sign.Z, sign.SPOS:
+ return sign.POS
+ case sign.Z, sign.NZ:
+ return sign.INT
+ case sign.Z, _:
+ return v2
+
+
+def sign_meet(s1: sign, s2: sign) -> sign | None:
+ """computes greatest lower bound. Can be None (i.e. bottom)"""
+ match s1, s2:
+ case sign.INT, _:
+ return s2
+ case _, sign.INT:
+ return s1
+ case sign.SNEG, (sign.NEG | sign.NZ | sign.SNEG):
+ return s1
+ case (sign.NEG | sign.NZ | sign.SNEG), sign.SNEG:
+ return s2
+ case sign.SNEG, _:
+ return None
+ case _, sign.SNEG:
+ return None
+ case sign.SPOS, (sign.POS | sign.NZ | sign.SPOS):
+ return s1
+ case (sign.POS | sign.NZ | sign.SPOS), sign.SPOS:
+ return s2
+ case sign.SPOS, _:
+ return None
+ case _, sign.SPOS:
+ return None
+ case sign.Z, (sign.NEG | sign.POS):
+ return s1
+ case (sign.NEG | sign.POS), sign.Z:
+ return s2
+ case sign.Z, sign.Z:
+ return s1
+ case sign.Z, _:
+ return None
+ case _, sign.Z:
+ return None
+ case sign.NEG, sign.NEG:
+ return s1
+ case sign.POS, sign.POS:
+ return s1
+ case sign.NEG, sign.POS:
+ return sign.Z
+ case sign.POS, sign.NEG:
+ return sign.Z
+ case sign.NZ, sign.NEG:
+ return sign.SNEG
+ case sign.NEG, sign.NZ:
+ return sign.SNEG
+ case sign.NZ, sign.POS:
+ return sign.SPOS
+ case sign.POS, sign.NZ:
+ return sign.SPOS
+ case sign.NZ, sign.NZ:
+ return sign.NZ
+
+
+def sign_opp(s: sign) -> sign:
+ """unary minus"""
+ match s:
+ case sign.SNEG:
+ return sign.SPOS
+ case sign.SPOS:
+ return sign.SNEG
+ case sign.POS:
+ return sign.NEG
+ case sign.NEG:
+ return sign.POS
+ case _:
+ return s
+
+
+def sign_add(s1: sign, s2: sign) -> sign:
+ """addition"""
+ match (s1, s2):
+ case sign.INT, _:
+ return sign.INT
+ case _, sign.INT:
+ return sign.INT
+ case sign.Z, _:
+ return s2
+ case _, sign.Z:
+ return s1
+ case sign.SNEG, (sign.SNEG | sign.NEG):
+ return sign.SNEG
+ case (sign.SNEG | sign.NEG), sign.SNEG:
+ return sign.SNEG
+ case sign.NEG, sign.NEG:
+ return sign.NEG
+ case sign.SPOS, (sign.SPOS | sign.POS):
+ return sign.SPOS
+ case (sign.SPOS | sign.POS), sign.SPOS:
+ return sign.SPOS
+ case sign.POS, sign.POS:
+ return sign.POS
+ case _:
+ return sign.INT
+
+
+def sign_mul(s1: sign, s2: sign) -> sign:
+ """multiplication"""
+ match s1, s2:
+ case sign.INT, _:
+ return sign.INT
+ case _, sign.INT:
+ return sign.INT
+ case sign.Z, _:
+ return sign.Z
+ case _, sign.Z:
+ return sign.Z
+ case sign.SPOS, _:
+ return s2
+ case _, sign.SPOS:
+ return s1
+ case sign.SNEG, _:
+ return sign_opp(s2)
+ case _, sign.SNEG:
+ return sign_opp(s1)
+ case sign.NZ, _:
+ return sign.INT
+ case _, sign.NZ:
+ return sign.INT
+ case sign.NEG, sign.NEG:
+ return sign.POS
+ case sign.NEG, sign.POS:
+ return sign.NEG
+ case sign.POS, sign.NEG:
+ return sign.NEG
+ case sign.POS, sign.POS:
+ return sign.POS
+
+
+def sign_div(s1: sign, s2: sign) -> sign | Top | None:
+ """division: can lead to errors even if operands are plain sign"""
+ match s1, s2:
+ case _, sign.Z:
+ return None
+ case _, sign.INT:
+ return Top()
+ case _, sign.POS:
+ return Top()
+ case _, sign.NEG:
+ return Top()
+ case sign.Z, _:
+ return sign.Z
+ case sign.INT, _:
+ return sign.INT
+ case sign.NZ, _:
+ return sign.INT
+ case _, sign.NZ:
+ return sign.INT
+ case (sign.POS | sign.SPOS), sign.SPOS:
+ return sign.POS
+ case (sign.NEG | sign.SNEG), sign.SPOS:
+ return sign.NEG
+ case (sign.POS | sign.SPOS), sign.SNEG:
+ return sign.NEG
+ case (sign.NEG | sign.SNEG), sign.SNEG:
+ return sign.POS
+
+
+def eval_aexp(env: abstract_env, e: ArithExpr) -> sign | Top | None:
+ """evaluate an arithmetic expression in an abstract environment
+ returns None in case of error
+ """
+ match e:
+ case AECst(value):
+ if value > 0:
+ return sign.SPOS
+ elif value < 0:
+ return sign.SNEG
+ else:
+ return sign.Z
+ case AEVar(var):
+ if var not in env:
+ return None
+ return env[var]
+ case AEUop(uop, expr):
+ v = eval_aexp(env, expr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return Top()
+ if uop == Uop.OPP:
+ return sign_opp(v)
+ case AEBop(bop, left_expr, right_expr):
+ v1 = eval_aexp(env, left_expr)
+ v2 = eval_aexp(env, right_expr)
+ if v1 is None or v2 is None:
+ return None
+ if isinstance(v1, Top) or isinstance(v2, Top):
+ return Top()
+ match bop:
+ case Bop.ADD:
+ return sign_add(v1, v2)
+ case Bop.MUL:
+ return sign_mul(v1, v2)
+ case Bop.DIV:
+ res = sign_div(v1, v2)
+ if res is None:
+ return None
+ if isinstance(res, Top):
+ return Top()
+ return res
+ case _:
+ return None
+
+
+def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None:
+ """abstract evaluation of a boolean expression"""
+ match e:
+ case BEPlain(aexpr):
+ v = eval_aexp(env, aexpr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return BTop(True)
+ return v == sign.Z
+ case BEEq(left_expr, right_expr):
+ v1 = eval_aexp(env, left_expr)
+ v2 = eval_aexp(env, right_expr)
+ if v1 is None or v2 is None:
+ return None
+ if isinstance(v1, Top) or isinstance(v2, Top):
+ return BTop(True)
+ if v1 == v2:
+ return True
+ if v1 == sign.Z and v2 == sign.Z:
+ return True
+ if v1 == sign.SPOS and v2 == sign.SPOS:
+ return True
+ if v1 == sign.SNEG and v2 == sign.SNEG:
+ return True
+ return False
+ case BELeq(left_expr, right_expr):
+ v1 = eval_aexp(env, left_expr)
+ v2 = eval_aexp(env, right_expr)
+ if v1 is None or v2 is None:
+ return None
+ if isinstance(v1, Top) or isinstance(v2, Top):
+ return BTop(True)
+ if v1 == sign.SNEG and v2 == sign.SPOS:
+ return True
+ if v1 == sign.Z and v2 in [sign.SPOS, sign.POS, sign.NZ]:
+ return True
+ if v1 == sign.SPOS and v2 == sign.SPOS:
+ return True
+ return False
+ case BENeg(expr):
+ v = eval_bexp(env, expr)
+ if v is None:
+ return None
+ if isinstance(v, BTop):
+ return v
+ return not v
+ case _:
+ 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"""
+ if s is None:
+ return None
+ v = eval_aexp(s, expr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return s
+ res = sign_meet(s[x], v)
+ if res is None:
+ return None
+ return s | {x: res}
+
+
+def reduce_neq_sign(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x != expr"""
+ if s is None:
+ return None
+ v = eval_aexp(s, expr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return s
+ match s[x], v:
+ case sign.POS, sign.Z:
+ return s | {x: sign.SPOS}
+ case sign.NEG, sign.Z:
+ return s | {x: sign.SNEG}
+ case sign.INT, sign.Z:
+ return s | {x: sign.NZ}
+ case _:
+ return s
+
+
+def reduce_upper_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x <= expr"""
+ if s is None:
+ return None
+ v = eval_aexp(s, expr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return s
+ upper = sign.INT
+ match v:
+ case sign.NEG | sign.SNEG:
+ upper = v
+ case sign.Z:
+ upper = sign.NEG
+ case _:
+ pass
+ res = sign_meet(s[x], upper)
+ if res is None:
+ return None
+ return s | {x: res}
+
+
+def reduce_strict_upper_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x < expr"""
+ if s is None:
+ return None
+ v = eval_aexp(s, expr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return s
+ match v:
+ case sign.NEG | sign.SNEG | sign.Z:
+ upper = sign.SNEG
+ case _:
+ upper = sign.INT
+ res = sign_meet(s[x], upper)
+ if res is None:
+ return None
+ return s | {x: res}
+
+
+def reduce_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x >= expr"""
+ if s is None:
+ return None
+ v = eval_aexp(s, expr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return s
+ lower = sign.INT
+ match v:
+ case sign.POS | sign.SPOS:
+ lower = v
+ case sign.Z:
+ lower = sign.POS
+ case _:
+ pass
+ res = sign_meet(s[x], lower)
+ if res is None:
+ return None
+ return s | {x: res}
+
+
+def reduce_strict_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x > expr"""
+ if s is None:
+ return s
+ v = eval_aexp(s, expr)
+ if v is None:
+ return None
+ if isinstance(v, Top):
+ return s
+ match v:
+ case sign.POS | sign.SPOS | sign.Z:
+ lower = sign.SPOS
+ case _:
+ lower = sign.INT
+ res = sign_meet(s[x], lower)
+ if res is None:
+ return None
+ return s | {x: res}
+
+
+def reduce_state(s: state, c: BoolExpr) -> state:
+ if s is None:
+ return s
+ match c:
+ # To be completed (see course's slides)
+ case _:
+ return s
+
+
+class Sign_interp(Transfer[state]):
+ variables: frozenset[str]
+
+ 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, sign.INT)
+
+ 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]
+ res[var] = sign_join(v1, v2)
+ return res
+
+ 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 sign_leq(s1[var], s2[var]):
+ return False
+ return True
+
+ def tr_skip(self, s: state) -> state:
+ return s
+
+ def tr_set(self, s: state, v: str, e: ArithExpr) -> state:
+ raise NotImplementedError
+
+ def tr_test(self, s: state, c: BoolExpr) -> state:
+ raise NotImplementedError
+
+ def tr_err(self, s: state, e: Expr) -> state:
+ if s is None:
+ return s
+ if isinstance(e, ArithExpr):
+ raise NotImplementedError
+ if isinstance(e, BoolExpr):
+ raise NotImplementedError
+
+
+def analyze(i: Instr) -> None:
+ cfg = Cfg(i)
+ res = fixpoint_iteration(Sign_interp(i), cfg)
+ for node in cfg.g.nodes:
+ print(f"State at {node}:")
+ s = res[node]
+ if s is not None:
+ for v, s in s.items():
+ print(f" {v}: {s}")
+
+
+"""
+# Évaluation des expressions
+
+L'analyse de signe montre que l'expression `y * (x - x/y)` peut être évaluée de manière sûre uniquement lorsque x et y sont strictement positifs ou lorsque x est positif et y est non-zéro, mais dans ce cas le résultat peut être n'importe quel entier. Dans tous les autres cas, soit on a une erreur certaine (division par zéro ou variables non définies), soit on a une erreur potentielle (TOP) car le résultat peut être n'importe quel signe.
+
+"""
\ No newline at end of file
--
GitLab