diff --git a/TP2/example_interval.py b/TP2/example_interval.py new file mode 100644 index 0000000000000000000000000000000000000000..8aa35e01334ffe53cbe00789994a19c11f544c59 --- /dev/null +++ b/TP2/example_interval.py @@ -0,0 +1,4 @@ +from interval_analysis import analyze +from example_opsem import factorial + +analyze(factorial) diff --git a/TP2/interval_analysis.py b/TP2/interval_analysis.py index 4f7b2e37ac7e9e192b48adc6e2a5acd556df8f1c..79d57e388dd8c359cf90ecb07d84fcb4535c8379 100644 --- a/TP2/interval_analysis.py +++ b/TP2/interval_analysis.py @@ -99,19 +99,29 @@ def interval_meet(i1: Interval, i2: Interval) -> Interval | 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: + """widening operator for intervals""" + if i1.lower_bound is None and i1.upper_bound is None: + return i2 + + if i1.lower_bound is None: l = None - elif i1.lower_bound <= i2.lower_bound: - l = i1.lower_bound - else: + elif i2.lower_bound is None: 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 + elif i2.lower_bound < i1.lower_bound: + l = None else: + l = i1.lower_bound + + if i1.upper_bound is None: u = None - return Interval(l,u) + elif i2.upper_bound is None: + u = None + elif i2.upper_bound > i1.upper_bound: + u = None + else: + u = i1.upper_bound + + return Interval(l, u) def has_strict_positive_val(i: Interval) -> bool: return i.upper_bound is None or i.upper_bound > 0 @@ -431,50 +441,98 @@ def reduce_state(s: state,c: BoolExpr) -> state: return reduce_leq(s,y,v.upper_bound - 1) case _: return s -class Interval_analysis(Transfer[state]): +class Interval_interp(Transfer[state]): variables: frozenset[str] - def __init__(self,instr: Instr): + + 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 + 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 + res[var] = interval_join(s1[var], s2[var]) return res - def widen(self, s1:state, s2:state) -> state: - raise NotImplementedError + def widen(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: + res[var] = interval_widen(s1[var], s2[var]) + return res - def included(self,s1: state,s2: state) -> bool: - if s1 is None: return True - if s2 is None: return False + 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 + if not interval_leq(s1[var], s2[var]): + return False return True - def tr_skip(self,s: state) -> state: + def tr_skip(self, s: state) -> state: return s - def tr_set(self,s: state,v: str,e: ArithExpr) -> state: - raise NotImplementedError + def tr_set(self, s: state, v: str, e: ArithExpr) -> state: + """transfer function for assignment""" + if s is None: + return None + res = eval_aexp(s, e) + if res is None: + return None + if isinstance(res, Top): + return s | {v: Interval(None, None)} + return s | {v: res} - def tr_test(self,s: state,c: BoolExpr) -> state: - raise NotImplementedError + def tr_test(self, s: state, c: BoolExpr) -> state: + """transfer function for test""" + 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: - raise NotImplementedError + def tr_err(self, s: state, e: Expr) -> state: + """transfer function for error""" + if s is None: + return s + if isinstance(e, ArithExpr): + res = eval_aexp(s, e) + if res is None: + return None + if isinstance(res, Top): + return s + return s + if isinstance(e, BoolExpr): + 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: cfg = Cfg(i) - res = fixpoint_iteration(Interval_analysis(i), cfg) + res = fixpoint_iteration(Interval_interp(i), cfg) for node in cfg.g.nodes: print(f"State at {node}:") s = res[node]