Skip to content
Snippets Groups Projects
Commit b88019f1 authored by Moi's avatar Moi
Browse files

suite tp

parent 0eaacf85
No related branches found
No related tags found
No related merge requests found
......@@ -141,7 +141,15 @@ def interval_opp(i: Interval) -> Interval:
return Interval(l,u)
def interval_add(i1: Interval, i2: Interval) -> Interval:
raise NotImplementedError
if i1.lower_bound is None or i2.lower_bound is None :
nlower = None
else:
nlower = min(i1.lower_bound, i2.lower_bound)
if i1.upper_bound is None or i2.upper_bound is None :
nupper = None
else:
nupper = max(i1.upper_bound, i2.upper_bound)
return Interval(nlower, nupper)
def interval_mul_pos(i1: Interval, i2: Interval) -> Interval:
assert (i1.lower_bound is not None and i1.lower_bound >= 0)
......@@ -180,7 +188,7 @@ def interval_mul(i1: Interval, i2: Interval) -> Interval:
return res
def interval_div(i1: Interval, i2: Interval) -> Interval | Top | None:
raise NotImplementedError
raise NotImplemented
def eval_aexp(env: abstract_env, e: ArithExpr) -> Interval | Top | None:
"""evaluate an arithmetic expression in an abstract environment
......
......@@ -7,6 +7,7 @@ transfer instance
"""
from cfg import *
from typing import Protocol
from collections import defaultdict
class Transfer[S](Protocol):
"""lists the functions that must be implemented for a static analysis over Lattice S"""
......@@ -43,4 +44,28 @@ def fixpoint_iteration[T](transfer: Transfer[T], cfg: Cfg) -> dict[Node,T]:
output maps each node to the computed state
"""
raise NotImplementedError
mapping = defaultdict(lambda : transfer.bottom())
worklist = []
mapping[cfg.init_node] = transfer.init_state()
worklist += [(cfg.init_node, succ, lab) for succ, lab in cfg.init_node.succs]
while worklist:
(src, dest, label) = worklist.pop()
etat_passe = mapping[dest]
if isinstance(label, LSkip) :
mapping[dest] = transfer.join(mapping[dest], transfer.tr_skip(mapping[src]))
elif isinstance(label, LSet):
mapping[dest] = transfer.join(mapping[dest], transfer.tr_set(mapping[src], label.var, label.expr))
elif isinstance(label, LTest):
mapping[dest] = transfer.join(mapping[dest], transfer.tr_test(mapping[src], label.cond))
elif isinstance(label, LErr):
mapping[dest] = transfer.join(mapping[dest], transfer.tr_err(mapping[src], label.err))
else:
assert False
if not transfer.included(mapping[dest], etat_passe):
worklist += [(dest, succ, lab) for succ, lab in dest.succs]
return mapping
......@@ -12,39 +12,85 @@ def eval_aexp(env: dict[str,int], exp: ArithExpr) -> int | None:
"""evaluates an arithmetic expression"""
match exp:
case AECst(value):
raise NotImplementedError
return value
case AEVar(var):
raise NotImplementedError
if var in env:
return env[var]
else:
return None
case AEUop(uop,expr):
raise NotImplementedError
if uop == Uop.OPP:
e = eval_aexp(env, expr)
if e is None:
return None
else:
return -eval_aexp(env, expr)
else:
return None
case AEBop(bop,left_expr,right_expr):
raise NotImplementedError
l = eval_aexp(env, left_expr)
r = eval_aexp(env, right_expr)
if l is None or r is None:
return None
match bop:
case Bop.ADD: return l + r
case Bop.MUL: return l * r
case Bop.DIV: return l // r if r != 0 else None
case _: assert False
def eval_bexp(env: dict[str,int], exp:BoolExpr) -> bool | None:
"""evaluates a boolean expression"""
match exp:
case BEPlain(aexpr):
raise NotImplementedError
e = eval_aexp(env, aexpr)
if e is None:
return None
else:
return True if e != 0 else False
case BEEq(left_expr,right_expr):
raise NotImplementedError
l = eval_aexp(env, left_expr)
r = eval_aexp(env, right_expr)
if l is None or r is None:
return None
return l == r
case BELeq(left_expr,right_expr):
raise NotImplementedError
case BENeg(expr):
raise NotImplementedError
l = eval_aexp(env, left_expr)
r = eval_aexp(env, right_expr)
if l is None or r is None:
return None
return l <= r
case BENeg(bexpr):
b = eval_bexp(env, bexpr)
if b is None:
return None
else:
return not b
case _: assert False
def eval_instr(env: dict[str,int], instr: Instr) -> dict[str,int] | None:
"""evaluates an instruction"""
match instr:
case ISkip():
raise NotImplementedError
return env.copy()
case ISet(var,expr):
raise NotImplementedError
val = eval_aexp(env, expr)
nvEnv = env.copy()
nvEnv[var] = val
return nvEnv
case ISeq(first,second):
raise NotImplementedError
nvEnv1 = eval_instr(env, first)
return eval_instr(nvEnv1, second)
case ICond(cond,true_branch,false_branch):
raise NotImplementedError
b = eval_bexp(env, cond)
if b:
return eval_instr(env, true_branch)
else:
return eval_instr(env, false_branch)
case ILoop(cond,body):
raise NotImplementedError
b = eval_bexp(env, cond)
if b:
nvEnv = eval_instr(env, body)
return eval_instr(nvEnv, ILoop(cond,body))
else:
return env.copy()
case _: assert False
......@@ -391,8 +391,8 @@ def reduce_state(s: state,c: BoolExpr) -> state:
if isinstance(right_expr, AEVar):
return reduce_strict_upper_bound(s, right_expr.var, left_expr)
return s
case BENeg(expr):
return reduce_state(s, c)
case BENeg(e):
return reduce_state(s, e)
case _: return s
case _: return s
......@@ -425,17 +425,21 @@ class Sign_interp(Transfer[state]):
return s
def tr_set(self,s: state,v: str,e: ArithExpr) -> state:
raise NotImplementedError
if s is None:
return None
return reduce_state(s, BEEq(AEVar(v), e))
def tr_test(self,s: state,c: BoolExpr) -> state:
raise NotImplementedError
if s is None:
return None
return reduce_state(s, c)
def tr_err(self,s: state,e: Expr) -> state:
if s is None: return s
if isinstance(e,ArithExpr):
raise NotImplementedError
return reduce_state(s, BEPlain(e))
if isinstance(e,BoolExpr):
raise NotImplementedError
return reduce_state(s, e)
def analyze(i: Instr) -> None:
cfg = Cfg(i)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment