diff --git a/TP2/example_sign.py b/TP2/example_sign.py new file mode 100644 index 0000000000000000000000000000000000000000..6aa6de3d4adb559dddcd246d9cdb3159f2f12b67 --- /dev/null +++ b/TP2/example_sign.py @@ -0,0 +1,4 @@ +from sign_analysis import analyze +from example_opsem import factorial + +analyze(factorial) diff --git a/TP2/example_sign_reduce.py b/TP2/example_sign_reduce.py new file mode 100644 index 0000000000000000000000000000000000000000..17ed63624d1e282d9f535cccecbdf5d04e169e20 --- /dev/null +++ b/TP2/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/TP2/sign_analysis.py b/TP2/sign_analysis.py index fdb2a92c06ace1ae166572722a911dd2a5abbe89..60f8d0d33dd1e5a749a98d7931222cafe6a1a246 100644 --- a/TP2/sign_analysis.py +++ b/TP2/sign_analysis.py @@ -501,7 +501,49 @@ def reduce_state(s: state, c: BoolExpr) -> state: if s is None: return s match c: - # To be completed (see course's slides) + case BEPlain(aexpr): + return reduce_eq_sign(s, "x", aexpr) + case BEEq(left_expr, right_expr): + if isinstance(left_expr, AEVar) and isinstance(right_expr, AEVar): + v1 = s[left_expr.var] + v2 = s[right_expr.var] + if (v1 == sign.SPOS and v2 == sign.SNEG) or (v1 == sign.SNEG and v2 == sign.SPOS): + return None + return reduce_eq_sign(s, left_expr.var, right_expr) + elif isinstance(left_expr, AEVar): + return reduce_eq_sign(s, left_expr.var, right_expr) + elif isinstance(right_expr, AEVar): + return reduce_eq_sign(s, right_expr.var, left_expr) + return s + case BENeg(expr): + if isinstance(expr, BEEq): + left_expr, right_expr = expr.left_expr, expr.right_expr + if isinstance(left_expr, AEVar) and isinstance(right_expr, AEVar): + return reduce_neq_sign(s, left_expr.var, right_expr) + elif isinstance(left_expr, AEVar): + return reduce_neq_sign(s, left_expr.var, right_expr) + elif isinstance(right_expr, AEVar): + return reduce_neq_sign(s, right_expr.var, left_expr) + elif isinstance(expr, BELeq): + left_expr, right_expr = expr.left_expr, expr.right_expr + if isinstance(left_expr, AEVar): + return reduce_strict_lower_bound(s, left_expr.var, right_expr) + elif isinstance(right_expr, AEVar): + return reduce_strict_upper_bound(s, right_expr.var, left_expr) + return s + case BELeq(left_expr, right_expr): + if isinstance(left_expr, AEVar) and isinstance(right_expr, AEVar): + v1 = s[left_expr.var] + v2 = s[right_expr.var] + if v1 == sign.SPOS and v2 == sign.SNEG: + return None + if v1 == sign.POS and v2 == sign.NEG: + return None + if isinstance(left_expr, AEVar): + return reduce_upper_bound(s, left_expr.var, right_expr) + elif isinstance(right_expr, AEVar): + return reduce_lower_bound(s, right_expr.var, left_expr) + return s case _: return s @@ -544,18 +586,48 @@ class Sign_interp(Transfer[state]): return s def tr_set(self, s: state, v: str, e: ArithExpr) -> state: - raise NotImplementedError + """transfer function for assignment instructions""" + if s is None: + return None + res = eval_aexp(s, e) + if res is None: + return None + if isinstance(res, Top): + return s | {v: sign.INT} + return s | {v: res} def tr_test(self, s: state, c: BoolExpr) -> state: - raise NotImplementedError + """transfer function for test instructions""" + if s is None: + return None + res = eval_bexp(s, c) + if res is None: + return None + if isinstance(res, BTop): + return s + if res: + return reduce_state(s, c) + return None def tr_err(self, s: state, e: Expr) -> state: + """transfer function for error instructions""" if s is None: return s if isinstance(e, ArithExpr): - raise NotImplementedError + res = eval_aexp(s, e) + if res is None: + return None + if isinstance(res, Top): + return s + return s if isinstance(e, BoolExpr): - raise NotImplementedError + res = eval_bexp(s, e) + if res is None: + return None + if isinstance(res, BTop): + return s + return s + return s def analyze(i: Instr) -> None: