From 2ecb7902e590b984411b1fc940692f0cf4d757be Mon Sep 17 00:00:00 2001
From: Nicolas Descamps <nicolas.descamps@theodo.com>
Date: Tue, 1 Apr 2025 16:29:04 +0200
Subject: [PATCH] =?UTF-8?q?Treillis=20des=20intervalles,=20d=C3=A9but?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
TP2/example_interval_eval_exp.py | 32 ++
TP2/example_interval_reduce.py | 39 +++
TP2/interval_analysis.py | 483 +++++++++++++++++++++++++++++++
3 files changed, 554 insertions(+)
create mode 100644 TP2/example_interval_eval_exp.py
create mode 100644 TP2/example_interval_reduce.py
create mode 100644 TP2/interval_analysis.py
diff --git a/TP2/example_interval_eval_exp.py b/TP2/example_interval_eval_exp.py
new file mode 100644
index 0000000..1203cab
--- /dev/null
+++ b/TP2/example_interval_eval_exp.py
@@ -0,0 +1,32 @@
+from syntax import *
+from interval_analysis import eval_aexp, eval_bexp, abstract_env, Interval
+
+x: ArithExpr = AEVar("x")
+y: ArithExpr = AEVar("y")
+
+# x - y * (x / y)
+test_aexp: ArithExpr = AEBop(Bop.ADD,x, AEUop(Uop.OPP,AEBop(Bop.MUL,y,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(i) for (var,i) in env.items()} }')
+ print(f"{test_aexp} -> {res_a}")
+ print(f"{test_bexp} -> {res_b}")
+
+test({ 'x': Interval(20,20), 'y': Interval(2,2) })
+
+test({ 'x': Interval(10,20), 'y': Interval(1,2) })
+
+test({ 'x': Interval(-30,0), 'y': Interval(-10,0) })
+
+test({ 'x': Interval(-20,20), 'y': Interval(0,0) })
+
+test({ 'x': Interval(0,20), 'y': Interval(2,5) })
+
+test({ 'x': Interval(-10,20), 'y': Interval(-5,-2) })
+
+test({})
diff --git a/TP2/example_interval_reduce.py b/TP2/example_interval_reduce.py
new file mode 100644
index 0000000..2d7cdda
--- /dev/null
+++ b/TP2/example_interval_reduce.py
@@ -0,0 +1,39 @@
+from syntax import *
+from interval_analysis import state, abstract_env, Interval, 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 env_str(env: abstract_env) -> str:
+ return '{ ' + ', '.join([ f'{var}: {i}' for (var,i) in env.items()]) + ' }'
+
+def state_str(env: state) -> str:
+ if env is None: return 'None'
+ return env_str(env)
+
+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 { env_str(env) }')
+ print(f"{test_eq} -> {state_str(res_eq)}")
+ print(f"{test_neq} -> {state_str(res_neq)}")
+ print(f"{test_leq} -> {state_str(res_leq)}")
+ print(f"{test_gt} -> {state_str(res_gt)}")
+
+test({ 'x': Interval(0,5), 'y': Interval(-5,0) })
+
+test({ 'x': Interval(-5,5), 'y': Interval(3,7) })
+
+test({ 'x': Interval(0,5), 'y': Interval(-10,-5) })
+
+test({ 'x': Interval(0,0), 'y': Interval(0,4) })
diff --git a/TP2/interval_analysis.py b/TP2/interval_analysis.py
new file mode 100644
index 0000000..4f7b2e3
--- /dev/null
+++ b/TP2/interval_analysis.py
@@ -0,0 +1,483 @@
+# pyright: strict
+
+"""
+implements a constant propagation analysis
+"""
+
+from dataclasses import dataclass
+from cfg import Cfg
+from iteration import Transfer, fixpoint_iteration
+from syntax import *
+
+@dataclass
+class Interval:
+ """ potentially unbounded interval
+
+ None in either bound means that we don't have info.
+ Hence `Interval(None,None)` denotes all integers
+ """
+ lower_bound: int | None
+ upper_bound: int | None
+ def __str__(self):
+ if self.lower_bound is None:
+ l = "-∞"
+ else:
+ l = str(self.lower_bound)
+ if self.upper_bound is None:
+ u = "+∞"
+ else:
+ u = str(self.upper_bound)
+ return f"[{l}; {u}]"
+
+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, Interval]
+"""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 interval_leq(i1: Interval, i2: Interval) -> bool:
+ if i2.lower_bound is None:
+ if i2.upper_bound is None:
+ return True
+ if i1.upper_bound is None:
+ return False
+ return i1.upper_bound <= i2.upper_bound
+ if i2.upper_bound is None:
+ if i1.lower_bound is None:
+ return False
+ return i1.lower_bound >= i2.lower_bound
+ if i1.lower_bound is None or i1.upper_bound is None:
+ return False
+ return i1.lower_bound >= i2.lower_bound and i1.upper_bound <= i2.upper_bound
+
+def interval_join(i1: Interval, i2: Interval) -> Interval:
+ if i1.lower_bound is None or i2.lower_bound is None:
+ l = None
+ else:
+ l = min(i1.lower_bound,i2.lower_bound)
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ else:
+ u = max(i1.upper_bound,i2.upper_bound)
+ return Interval(l,u)
+
+def interval_meet(i1: Interval, i2: Interval) -> Interval | None:
+ if i1.lower_bound is None:
+ l = i2.lower_bound
+ elif i2.lower_bound is None:
+ l = i1.lower_bound
+ else:
+ l = max(i1.lower_bound,i2.lower_bound)
+ if i1.upper_bound is None:
+ u = i2.upper_bound
+ elif i2.upper_bound is None:
+ u = i1.upper_bound
+ else:
+ u = min(i1.upper_bound,i2.upper_bound)
+ if l is not None and u is not None and l > u: return None
+ return Interval(l,u)
+
+def interval_widen(i1: Interval, i2: Interval) -> Interval:
+ if i1.lower_bound is None or i2.lower_bound is None:
+ l = None
+ elif i1.lower_bound <= i2.lower_bound:
+ l = i1.lower_bound
+ else:
+ l = None
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ elif i1.upper_bound >= i2.upper_bound:
+ u = i1.upper_bound
+ else:
+ u = None
+ return Interval(l,u)
+
+def has_strict_positive_val(i: Interval) -> bool:
+ return i.upper_bound is None or i.upper_bound > 0
+
+def has_strict_negative_val(i: Interval) -> bool:
+ return i.lower_bound is None or i.lower_bound < 0
+
+def contains_zero(i: Interval) -> bool:
+ if i.lower_bound is None:
+ return i.upper_bound is None or i.upper_bound >= 0
+ if i.upper_bound is None:
+ return i.lower_bound <= 0
+ return i.lower_bound <= 0 and i.upper_bound >= 0
+
+def is_zero(i: Interval) -> bool:
+ return i.lower_bound == 0 and i.upper_bound == 0
+
+def interval_opp(i: Interval) -> Interval:
+ if i.lower_bound is None:
+ u = None
+ else:
+ u = -i.lower_bound
+ if i.upper_bound is None:
+ l = None
+ else:
+ l = -i.upper_bound
+ return Interval(l,u)
+
+def interval_add(i1: Interval, i2: Interval) -> Interval:
+ """addition of two intervals"""
+ if i1.lower_bound is None or i2.lower_bound is None:
+ l = None
+ else:
+ l = i1.lower_bound + i2.lower_bound
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ else:
+ u = i1.upper_bound + i2.upper_bound
+ return Interval(l, u)
+
+def interval_mul(i1: Interval, i2: Interval) -> Interval:
+ """multiplication of two intervals"""
+ if i1.lower_bound is not None and i1.upper_bound is not None and i1.lower_bound > i1.upper_bound:
+ return Interval(None, None)
+ if i2.lower_bound is not None and i2.upper_bound is not None and i2.lower_bound > i2.upper_bound:
+ return Interval(None, None)
+
+ if contains_zero(i1) or contains_zero(i2):
+ return Interval(None, None)
+
+ if i1.lower_bound is not None and i1.lower_bound >= 0 and i2.lower_bound is not None and i2.lower_bound >= 0:
+ l = i1.lower_bound * i2.lower_bound
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ else:
+ u = i1.upper_bound * i2.upper_bound
+ return Interval(l, u)
+
+ if i1.upper_bound is not None and i1.upper_bound <= 0 and i2.upper_bound is not None and i2.upper_bound <= 0:
+ l = i1.upper_bound * i2.upper_bound
+ if i1.lower_bound is None or i2.lower_bound is None:
+ u = None
+ else:
+ u = i1.lower_bound * i2.lower_bound
+ return Interval(l, u)
+
+ if (i1.lower_bound is not None and i1.lower_bound >= 0 and i2.upper_bound is not None and i2.upper_bound <= 0) or \
+ (i2.lower_bound is not None and i2.lower_bound >= 0 and i1.upper_bound is not None and i1.upper_bound <= 0):
+ l = None
+ if i1.lower_bound is not None and i2.lower_bound is not None:
+ l = min(i1.lower_bound * i2.upper_bound, i1.upper_bound * i2.lower_bound)
+ u = None
+ if i1.upper_bound is not None and i2.upper_bound is not None:
+ u = max(i1.lower_bound * i2.lower_bound, i1.upper_bound * i2.upper_bound)
+ return Interval(l, u)
+
+ return Interval(None, None)
+
+def interval_div(i1: Interval, i2: Interval) -> Interval | Top | None:
+ """division of two intervals"""
+ if is_zero(i2):
+ return None
+
+ if contains_zero(i2):
+ return Top()
+
+ if i2.lower_bound is not None and i2.lower_bound > 0:
+ if i1.lower_bound is None:
+ l = None
+ else:
+ l = i1.lower_bound // i2.lower_bound
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ else:
+ u = i1.upper_bound // i2.upper_bound
+ return Interval(l, u)
+
+ if i2.upper_bound is not None and i2.upper_bound < 0:
+ if i1.lower_bound is None:
+ l = None
+ else:
+ l = i1.lower_bound // i2.upper_bound
+ if i1.upper_bound is None or i2.lower_bound is None:
+ u = None
+ else:
+ u = i1.upper_bound // i2.lower_bound
+ return Interval(l, u)
+
+ return Top()
+
+def eval_aexp(env: abstract_env, e: ArithExpr) -> Interval | Top | None:
+ """evaluate an arithmetic expression in an abstract environment
+ returns None in case of error
+ """
+ match e:
+ case AECst(value): return Interval(value,value)
+ case AEVar(var):
+ if var in env: return env[var]
+ else: return None
+ case AEUop(uop,expr):
+ res = eval_aexp(env,expr)
+ if res is None or isinstance(res,Top): return res
+ if uop == Uop.OPP: return interval_opp(res)
+ return None
+ 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 interval_add(v1,v2)
+ case Bop.MUL: return interval_mul(v1,v2)
+ case Bop.DIV: return interval_div(v1,v2)
+ case _: pass
+
+def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None:
+ """abstract evaluation of a boolean expression"""
+ match e:
+ case BEPlain(aexpr):
+ res = eval_aexp(env, aexpr)
+ if res is None: return None
+ if isinstance(res,Top): return BTop(True)
+ if res.lower_bound == 0 and res.upper_bound == 0: return True
+ if not interval_leq(Interval(0,0), res): return False
+ return BTop(False)
+ 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.lower_bound is None or v2.lower_bound is None or v1.upper_bound is None or v2.upper_bound is None:
+ return BTop(False)
+ if v1.lower_bound > v2.upper_bound or v1.upper_bound < v2.lower_bound:
+ return False
+ if v1.lower_bound == v1.upper_bound and v2.lower_bound == v2.upper_bound and v1.lower_bound == v2.lower_bound:
+ return True
+ return BTop(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.upper_bound is None:
+ if v1.lower_bound is None:
+ return BTop(False)
+ if v2.upper_bound is None:
+ return BTop(False)
+ if v2.upper_bound < v1.lower_bound:
+ return False
+ return BTop(False)
+ if v2.lower_bound is None:
+ return BTop(False)
+ if v1.upper_bound <= v2.lower_bound:
+ return True
+ if v1.lower_bound is None:
+ return BTop(False)
+ if v2.upper_bound is None:
+ return BTop(False)
+ if v2.upper_bound < v1.lower_bound:
+ return False
+ return BTop(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 _: pass
+
+def reduce_eq(s: state, x: str, i: Interval) -> state:
+ """Reduce the value of x under the hypothesis that it equals i"""
+ if s is None:
+ return None
+ if x not in s:
+ return None
+ res = interval_meet(s[x], i)
+ if res is None:
+ return None
+ return s | {x: res}
+
+def reduce_neq(s: state, x: str, i: Interval) -> state:
+ """Reduce the value of x under the hypothesis that it differs from i"""
+ if s is None:
+ return None
+ if x not in s:
+ return None
+ if i.lower_bound == i.upper_bound and s[x].lower_bound == i.lower_bound:
+ if s[x].upper_bound is None or s[x].upper_bound > i.upper_bound:
+ return s | {x: Interval(i.upper_bound + 1, s[x].upper_bound)}
+ return None
+ if i.lower_bound == i.upper_bound and s[x].upper_bound == i.upper_bound:
+ if s[x].lower_bound is None or s[x].lower_bound < i.lower_bound:
+ return s | {x: Interval(s[x].lower_bound, i.lower_bound - 1)}
+ return None
+ return s
+
+def reduce_leq(s: state, x: str, upper_bound: int) -> state:
+ """Reduce the value of x under the hypothesis that it is less than or equal to upper_bound"""
+ if s is None:
+ return None
+ if x not in s:
+ return None
+ res = interval_meet(s[x], Interval(None, upper_bound))
+ if res is None:
+ return None
+ return s | {x: res}
+
+def reduce_geq(s: state, x: str, lower_bound: int) -> state:
+ """Reduce the value of x under the hypothesis that it is greater than or equal to lower_bound"""
+ if s is None:
+ return None
+ if x not in s:
+ return None
+ res = interval_meet(s[x], Interval(lower_bound, None))
+ 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:
+ case BEEq(AEVar(x), AEVar(y)):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vx,Top):
+ s = reduce_eq(s,y,vx)
+ if not isinstance(vy,Top):
+ s = reduce_eq(s,x,vy)
+ return s
+ case BEEq(AEVar(x), right_expr):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_eq(s,x,v)
+ case BEEq(left_expr, AEVar(y)):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_eq(s,y,v)
+ case BELeq(AEVar(x), AEVar(y)):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vy,Top) and vy.upper_bound is not None:
+ s = reduce_leq(s,x,vy.upper_bound)
+ if not isinstance(vx,Top) and vx.lower_bound is not None:
+ s = reduce_geq(s,y,vx.lower_bound)
+ return s
+ case BELeq(AEVar(x),right_expr):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.upper_bound is None: return s
+ return reduce_leq(s,x,v.upper_bound)
+ case BELeq(left_expr,AEVar(y)):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.lower_bound is None: return s
+ return reduce_geq(s,y,v.lower_bound)
+ case BENeg(BEEq(AEVar(x), AEVar(y))):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vx,Top):
+ s = reduce_neq(s,y,vx)
+ if not isinstance(vy,Top):
+ s = reduce_neq(s,x,vy)
+ return s
+ case BENeg(BEEq(AEVar(x), right_expr)):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_neq(s,x,v)
+ case BENeg(BEEq(left_expr, AEVar(y))):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_neq(s,y,v)
+ case BENeg(BELeq(AEVar(x), AEVar(y))):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vx,Top) and vx.upper_bound is not None:
+ s = reduce_leq(s,y,vx.upper_bound - 1)
+ if not isinstance(vy,Top) and vy.lower_bound is not None:
+ s = reduce_geq(s,x,vy.lower_bound + 1)
+ return s
+ case BENeg(BELeq(AEVar(x),right_expr)):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.lower_bound is None: return s
+ return reduce_geq(s,x,v.lower_bound + 1)
+ case BENeg(BELeq(left_expr,AEVar(y))):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.upper_bound is None: return s
+ return reduce_leq(s,y,v.upper_bound - 1)
+ case _: return s
+
+class Interval_analysis(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, Interval(None,None))
+ 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]
+ v = interval_join(v1,v2)
+ res[var] = v
+ return res
+
+ def widen(self, s1:state, s2:state) -> state:
+ raise NotImplementedError
+
+ 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 interval_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:
+ raise NotImplementedError
+
+def analyze(i: Instr) -> None:
+ cfg = Cfg(i)
+ res = fixpoint_iteration(Interval_analysis(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}")
--
GitLab