diff --git a/Pystan/config/__pycache__/cfg.cpython-312.pyc b/Pystan/config/__pycache__/cfg.cpython-312.pyc new file mode 100644 index 0000000000000000000000000000000000000000..d1a918da4587190ec0ed293eb58376cf5c5ba3d9 Binary files /dev/null and b/Pystan/config/__pycache__/cfg.cpython-312.pyc differ diff --git a/Pystan/config/__pycache__/constant_propagation.cpython-312.pyc b/Pystan/config/__pycache__/constant_propagation.cpython-312.pyc new file mode 100644 index 0000000000000000000000000000000000000000..81e97440258bf50a9ef41dacea62fdda37d6c587 Binary files /dev/null and b/Pystan/config/__pycache__/constant_propagation.cpython-312.pyc differ diff --git a/Pystan/config/__pycache__/iteration.cpython-312.pyc b/Pystan/config/__pycache__/iteration.cpython-312.pyc new file mode 100644 index 0000000000000000000000000000000000000000..68239e3f063ee6b0b9390a069426261f16cd1692 Binary files /dev/null and b/Pystan/config/__pycache__/iteration.cpython-312.pyc differ diff --git a/Pystan/config/__pycache__/opsem.cpython-312.pyc b/Pystan/config/__pycache__/opsem.cpython-312.pyc new file mode 100644 index 0000000000000000000000000000000000000000..b416b2b688a0eff7fd24790cc3a7dd80c0147da9 Binary files /dev/null and b/Pystan/config/__pycache__/opsem.cpython-312.pyc differ diff --git a/Pystan/config/__pycache__/syntax.cpython-312.pyc b/Pystan/config/__pycache__/syntax.cpython-312.pyc new file mode 100644 index 0000000000000000000000000000000000000000..0e0cff17c20d02adfbd1992c523683af47651381 Binary files /dev/null and b/Pystan/config/__pycache__/syntax.cpython-312.pyc differ diff --git a/Pystan/config/example_interval.py b/Pystan/config/example_interval.py new file mode 100644 index 0000000000000000000000000000000000000000..8aa35e01334ffe53cbe00789994a19c11f544c59 --- /dev/null +++ b/Pystan/config/example_interval.py @@ -0,0 +1,4 @@ +from interval_analysis import analyze +from example_opsem import factorial + +analyze(factorial) diff --git a/Pystan/config/example_interval_eval_exp.py b/Pystan/config/example_interval_eval_exp.py new file mode 100644 index 0000000000000000000000000000000000000000..1203cab645be505a71cd14888374824eca277e68 --- /dev/null +++ b/Pystan/config/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/Pystan/config/example_interval_reduce.py b/Pystan/config/example_interval_reduce.py new file mode 100644 index 0000000000000000000000000000000000000000..2d7cdda54e9d02cfd00b41b9a65d67b63f5120b9 --- /dev/null +++ b/Pystan/config/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/Pystan/config/example_sign.py b/Pystan/config/example_sign.py new file mode 100644 index 0000000000000000000000000000000000000000..6aa6de3d4adb559dddcd246d9cdb3159f2f12b67 --- /dev/null +++ b/Pystan/config/example_sign.py @@ -0,0 +1,4 @@ +from sign_analysis import analyze +from example_opsem import factorial + +analyze(factorial) diff --git a/Pystan/config/example_sign_eval_exp.py b/Pystan/config/example_sign_eval_exp.py new file mode 100644 index 0000000000000000000000000000000000000000..c8bdd995dad92d272d407c6a2c040666e1f2ad29 --- /dev/null +++ b/Pystan/config/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/Pystan/config/example_sign_reduce.py b/Pystan/config/example_sign_reduce.py new file mode 100644 index 0000000000000000000000000000000000000000..17ed63624d1e282d9f535cccecbdf5d04e169e20 --- /dev/null +++ b/Pystan/config/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/Pystan/config/example_widen.py b/Pystan/config/example_widen.py new file mode 100644 index 0000000000000000000000000000000000000000..c9372be7b6162f6f47cd8f7ed8a5c2e240aa187d --- /dev/null +++ b/Pystan/config/example_widen.py @@ -0,0 +1,61 @@ +from iteration import Transfer, fixpoint_iteration +from syntax import * +from cfg import Cfg +from example_opsem import factorial + +@dataclass +class Number_step: + bound: int | None + def __str__(self): + if self.bound is None: return "+∞" + else: return str(self.bound) + +type S = Number_step | None + +class Analysis(Transfer[S]): + def bottom(self) -> S: + return None + + def init_state(self) -> S: + return Number_step(0) + + def join(self,s1:S,s2:S) -> S: + if s1 is None: return s2 + if s2 is None: return s1 + if s1.bound is None: return s1 + if s2.bound is None: return s2 + return Number_step(max(s1.bound, s2.bound)) + + def widen(self, s1:S, s2:S) -> S: + if s1 is None: return s2 + if s2 is None: return s1 + if s1.bound is None: return s1 + if s2.bound is None: return s2 + if s1.bound < s2.bound: return Number_step(None) + return s1 + + def included(self,s1: S,s2: S) -> bool: + if s1 is None: return True + if s2 is None: return False + if s2.bound is None: return True + if s1.bound is None: return False + return s1.bound <= s2.bound + + def tr_skip(self,s: S) -> S: + if s is None: return None + if s.bound is None: return s + return Number_step(s.bound + 1) + + def tr_set(self,s: S,v: str,e: ArithExpr) -> S: + return self.tr_skip(s) + + def tr_test(self,s: S,c: BoolExpr) -> S: + return self.tr_skip(s) + + def tr_err(self,s: S,e: Expr) -> S: + return self.tr_skip(s) + +res = fixpoint_iteration(Analysis(),Cfg(factorial)) + +for (node, nb) in res.items(): + print(f'{node} -> {nb}') diff --git a/Pystan/config/interval_analysis.py b/Pystan/config/interval_analysis.py new file mode 100644 index 0000000000000000000000000000000000000000..9186efbf8ffeedb0fe1e207381313552f1b34163 --- /dev/null +++ b/Pystan/config/interval_analysis.py @@ -0,0 +1,406 @@ +# 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: + raise NotImplementedError + +def interval_mul_pos(i1: Interval, i2: Interval) -> Interval: + assert (i1.lower_bound is not None and i1.lower_bound >= 0) + assert (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) + +def interval_opt_join(i1: Interval | None, i2: Interval) -> Interval: + if i1 is None: return i2 + return interval_join(i1,i2) + +def interval_mul(i1: Interval, i2: Interval) -> Interval: + i1_neg = interval_meet(i1,Interval(None,0)) + i2_neg = interval_meet(i2,Interval(None,0)) + i1_pos = interval_meet(i1,Interval(0,None)) + i2_pos = interval_meet(i2,Interval(0,None)) + if i1_neg is None or i2_pos is None: + res = None + else: + res = interval_opp(interval_mul_pos(interval_opp(i1_neg),i2_pos)) + if i1_pos is not None and i2_neg is not None: + res1 = interval_opp(interval_mul_pos(i1_pos,interval_opp(i2_neg))) + res = interval_opt_join(res, res1) + if i1_neg is not None and i2_neg is not None: + res1 = interval_mul_pos(interval_opp(i1_neg),interval_opp(i2_neg)) + res = interval_opt_join(res,res1) + if i1_pos is not None and i2_pos is not None: + res1 = interval_mul_pos(i1_pos, i2_pos) + res = interval_opt_join(res, res1) + # at least one of the 4 cases is not empty + assert res is not None + return res + +def interval_div(i1: Interval, i2: Interval) -> Interval | Top | None: + raise NotImplementedError + +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: + raise NotImplementedError + +def reduce_neq(s:state, x: str, i: Interval) -> state: + raise NotImplementedError + +def reduce_leq(s:state,x:str,upper_bound: int) -> state: + raise NotImplementedError + +def reduce_geq(s: state, x: str, lower_bound: int) -> state: + raise NotImplementedError + +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}") diff --git a/Pystan/config/sign_analysis.py b/Pystan/config/sign_analysis.py new file mode 100644 index 0000000000000000000000000000000000000000..61bd064cf6d836b3edcbf068f5b739187194d229 --- /dev/null +++ b/Pystan/config/sign_analysis.py @@ -0,0 +1,338 @@ +# pyright: strict +""" +implements a sign analysis +""" +from enum import Enum +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): + raise NotImplementedError + case AEVar(var): + raise NotImplementedError + case AEUop(uop,expr): + raise NotImplementedError + case AEBop(bop,left_expr,right_expr): + raise NotImplementedError + case _: pass + +def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None: + """abstract evaluation of a boolean expression""" + match e: + case BEPlain(aexpr): + raise NotImplementedError + case BEEq(left_expr,right_expr): + raise NotImplementedError + case BELeq(left_expr,right_expr): + raise NotImplementedError + case BENeg(expr): + raise NotImplementedError + case _: pass + +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}")