diff --git a/Pystan/config/sign_analysis.py b/Pystan/config/sign_analysis.py index 61bd064cf6d836b3edcbf068f5b739187194d229..043f5b1351cfccb192fcff24f88fcc1200a90214 100644 --- a/Pystan/config/sign_analysis.py +++ b/Pystan/config/sign_analysis.py @@ -2,12 +2,16 @@ """ implements a sign analysis """ -from enum import Enum +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() @@ -172,27 +176,87 @@ def eval_aexp(env: abstract_env, e: ArithExpr) -> sign | Top | None: """ match e: case AECst(value): - raise NotImplementedError + if value == 0: + return sign.Z + elif value > 0: + return sign.POS + else: + return sign.NEG + case AEVar(var): - raise NotImplementedError - case AEUop(uop,expr): - raise NotImplementedError - case AEBop(bop,left_expr,right_expr): - raise NotImplementedError - case _: pass + return env.get(var, None) + + case AEUop(uop, expr): + val = eval_aexp(env, expr) + if val is None or isinstance(val, Top): + return val + if uop == Uop.OPP: + return sign_opp(val) + + case AEBop(bop, left_expr, right_expr): + l = eval_aexp(env, left_expr) + r = eval_aexp(env, right_expr) + if l is None or r is None: + return None + if isinstance(l, Top) or isinstance(r, Top): + return Top() + match bop: + case Bop.ADD: + return sign_add(l, r) + case Bop.MUL: + return sign_mul(l, r) + case Bop.DIV: + return sign_div(l, r) + + return None 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 + val = eval_aexp(env, aexpr) + if val is None: + return None + if isinstance(val, Top): + return BTop(True) + return val != sign.Z + + case BEEq(left_expr, right_expr): + l = eval_aexp(env, left_expr) + r = eval_aexp(env, right_expr) + if l is None or r is None: + return None + if isinstance(l, Top) or isinstance(r, Top): + return BTop(True) + return l == r + + case BELeq(left_expr, right_expr): + l = eval_aexp(env, left_expr) + r = eval_aexp(env, right_expr) + if l is None or r is None: + return None + if isinstance(l, Top) or isinstance(r, Top): + return BTop(True) + match l, r: + case sign.SNEG | sign.NEG, sign.Z | sign.POS | sign.SPOS: + return True + case sign.Z, sign.POS | sign.SPOS: + return True + case sign.POS, sign.SNEG | sign.NEG: + return False + case _: + return BTop(False) + case BENeg(expr): - raise NotImplementedError - case _: pass + b = eval_bexp(env, expr) + if b is None: + return None + if isinstance(b, BTop): + return b + return not b + + 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"""