Skip to content
Snippets Groups Projects
Commit d9519b78 authored by Nicolas Descamps's avatar Nicolas Descamps
Browse files

évaluation des expressions

parent fab51399
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
TP2/example_sign_eval_exp.py 0 → 100644
+ 28
− 0
View file @ d9519b78
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({})
TP2/sign_analysis.py 0 → 100644
+ 577
− 0
View file @ d9519b78
# 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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment