add TP3 files empty

Pystan/config/example_interval.py

+from interval_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)

Pystan/config/example_interval_eval_exp.py

+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({})

Pystan/config/example_interval_reduce.py

+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) })

Pystan/config/example_sign.py

+from sign_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)

Pystan/config/example_sign_eval_exp.py

+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({})

Pystan/config/example_sign_reduce.py

+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 })
+

Pystan/config/example_widen.py

+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}')

Pystan/config/interval_analysis.py

+# 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}")

Pystan/config/sign_analysis.py

+# 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}")