Skip to content
Snippets Groups Projects
Commit fab51399 authored by Nicolas Descamps's avatar Nicolas Descamps
Browse files

TP Python

parent e04bf05d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
TP2/constant_propagation.py
+ 136
− 45
View file @ fab51399
...@@ -7,13 +7,17 @@ from cfg import Label, LSkip, LSet, LTest, LErr ...@@ -7,13 +7,17 @@ from cfg import Label, LSkip, LSet, LTest, LErr
from iteration import Transfer from iteration import Transfer
from syntax import * from syntax import *
@dataclass @dataclass
class abstract_value[T]: class abstract_value[T]:
"""None indicates that we don't know the precise value""" """None indicates that we don't know the precise value"""
value: T | None value: T | None
def __str__(self): def __str__(self):
return f"{self.value}" return f"{self.value}"
type abstract_env = dict[str, abstract_value[int]] type abstract_env = dict[str, abstract_value[int]]
"""mapping from variables to abstract values. """mapping from variables to abstract values.
...@@ -24,84 +28,171 @@ type state = abstract_env | None ...@@ -24,84 +28,171 @@ type state = abstract_env | None
"""abstract state is either an abstract env or bottom """abstract state is either an abstract env or bottom
""" """
def eval_aexp(env: abstract_env, e: ArithExpr) -> abstract_value[int] | None: def eval_aexp(env: abstract_env, e: ArithExpr) -> abstract_value[int] | None:
"""evaluate an arithmetic expression in an abstract environment """evaluate an arithmetic expression in an abstract environment
returns None in case of error returns None in case of error
""" """
match e: match e:
case AECst(value): return abstract_value(value) case AECst(value):
return abstract_value(value)
case AEVar(var): case AEVar(var):
if var in env: return env[var] if var in env:
else: return None return env[var]
case AEUop(uop,expr): else:
res = eval_aexp(env,expr) return None
if res is None: return None case AEUop(uop, expr):
if res.value is None: return abstract_value(None) res = eval_aexp(env, expr)
if uop == Uop.OPP: return abstract_value(-res.value) if res is None:
return None
if res.value is None:
return abstract_value(None)
if uop == Uop.OPP:
return abstract_value(-res.value)
return None return None
case AEBop(bop,left_expr,right_expr): case AEBop(bop, left_expr, right_expr):
v1 = eval_aexp(env,left_expr) v1 = eval_aexp(env, left_expr)
v2 = eval_aexp(env,right_expr) v2 = eval_aexp(env, right_expr)
if v1 is None or v2 is None: return None if v1 is None or v2 is None:
return None
if v1.value is None or v2.value is None: if v1.value is None or v2.value is None:
return abstract_value(None) return abstract_value(None)
match bop: match bop:
case Bop.ADD: return abstract_value(v1.value+v2.value) case Bop.ADD:
case Bop.MUL: return abstract_value(v1.value*v2.value) return abstract_value(v1.value + v2.value)
case Bop.MUL:
return abstract_value(v1.value * v2.value)
case Bop.DIV: case Bop.DIV:
if v2.value == 0: return None if v2.value == 0:
return abstract_value(v1.value//v2.value) return None
case _: assert False return abstract_value(v1.value // v2.value)
case _:
assert False
def eval_bexp(env: abstract_env, e: BoolExpr) -> abstract_value[bool] | None: def eval_bexp(env: abstract_env, e: BoolExpr) -> abstract_value[bool] | None:
"""abstract evaluation of a boolean expression""" """abstract evaluation of a boolean expression"""
match e: match e:
case BEPlain(aexpr): case BEPlain(aexpr):
res = eval_aexp(env, aexpr) res = eval_aexp(env, aexpr)
if res is None: return None if res is None:
if res.value is None: return abstract_value(None) return None
return abstract_value(res.value!=0) if res.value is None:
case BEEq(left_expr,right_expr): return abstract_value(None)
return abstract_value(res.value != 0)
case BEEq(left_expr, right_expr):
v1 = eval_aexp(env, left_expr) v1 = eval_aexp(env, left_expr)
v2 = eval_aexp(env, right_expr) v2 = eval_aexp(env, right_expr)
if v1 is None or v2 is None: return None if v1 is None or v2 is None:
if v1.value is None or v2.value is None: return abstract_value(None) return None
if v1.value is None or v2.value is None:
return abstract_value(None)
return abstract_value(v1.value == v2.value) return abstract_value(v1.value == v2.value)
case BELeq(left_expr,right_expr): case BELeq(left_expr, right_expr):
v1 = eval_aexp(env, left_expr) v1 = eval_aexp(env, left_expr)
v2 = eval_aexp(env, right_expr) v2 = eval_aexp(env, right_expr)
if v1 is None or v2 is None: return None if v1 is None or v2 is None:
if v1.value is None or v2.value is None: return abstract_value(None) return None
if v1.value is None or v2.value is None:
return abstract_value(None)
return abstract_value(v1.value <= v2.value) return abstract_value(v1.value <= v2.value)
case BENeg(expr): case BENeg(expr):
v = eval_bexp(env,expr) v = eval_bexp(env, expr)
if v is None: return None if v is None:
if v.value is None: return v return None
if v.value is None:
return v
return abstract_value(not v.value) return abstract_value(not v.value)
case _: assert False case _:
assert False
class Constant_propagation(Transfer[state]): class Constant_propagation(Transfer[state]):
variables: frozenset[str] variables: frozenset[str]
def __init__(self,instr):
def __init__(self, instr):
self.variables = variables_of_instr(instr) self.variables = variables_of_instr(instr)
def bottom(self) -> state: def bottom(self) -> state:
... return None
def init_state(self) -> state: def init_state(self) -> state:
... return {var: abstract_value(None) for var in self.variables}
def join(self,s1:state,s2:state) -> state:
...
def included(self,s1: state,s2: state) -> bool: def join(self, s1: state, s2: state) -> state:
... if s1 is None:
return s2
if s2 is None:
return s1
new_env = {}
for var in self.variables:
v1 = s1.get(var, abstract_value(None))
v2 = s2.get(var, abstract_value(None))
if v1.value == v2.value:
new_env[var] = abstract_value(v1.value)
else:
new_env[var] = abstract_value(None)
return new_env
def tr_skip(self,s: state) -> state: 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:
v1 = s1.get(var, abstract_value(None))
v2 = s2.get(var, abstract_value(None))
if v1.value is not None and v2.value != v1.value:
return False
return True
def tr_set(self,s: state,v: str,e: ArithExpr) -> state: def tr_skip(self, s: state) -> state:
... return s
def tr_test(self,s: state,c: BoolExpr) -> state: def tr_set(self, s: state, v: str, e: ArithExpr) -> state:
... if s is None:
return None
val = eval_aexp(s, e)
if val is None:
return None
new_env = s.copy()
new_env[v] = val
return new_env
def tr_test(self, s: state, c: BoolExpr) -> state:
if s is None:
return None
res = eval_bexp(s, c)
if res is None:
return s
if res.value is False:
return None
if isinstance(c, BEEq):
left, right = c.left_expr, c.right_expr
if isinstance(left, AEVar) and isinstance(right, AECst):
new_env = s.copy()
new_env[left.var] = abstract_value(right.value)
return new_env
if isinstance(right, AEVar) and isinstance(left, AECst):
new_env = s.copy()
new_env[right.var] = abstract_value(left.value)
return new_env
return s
def tr_err(self,s: state,e: Expr) -> state: def tr_err(self, s: state, e: Expr) -> state:
... if s is None:
return None
if isinstance(e, ArithExpr):
res = eval_aexp(s, e)
if res is not None and res.value is not None:
return None
else:
return s
elif isinstance(e, BoolExpr):
res = eval_bexp(s, e)
if res is not None and res.value is not None:
return None
else:
return s
else:
assert False
TP2/example_opsem.py
+ 9
− 7
View file @ fab51399
...@@ -6,16 +6,18 @@ y = AEVar("y") ...@@ -6,16 +6,18 @@ y = AEVar("y")
zero = AECst(0) zero = AECst(0)
one = AECst(1) one = AECst(1)
xneg = BELeq(x, zero) xneg = BELeq(x, zero)
bound_check = ICond(xneg,ISet("x",one),ISkip()) bound_check = ICond(xneg, ISet("x", one), ISkip())
init_y = ISet("y",one) init_y = ISet("y", one)
body = ISeq(ISet("y",AEBop(Bop.MUL,y,x)),ISet("x",AEBop(Bop.ADD,x,AEUop(Uop.OPP,one)))) body = ISeq(
loop = ILoop(BENeg(BELeq(x,zero)),body) ISet("y", AEBop(Bop.MUL, y, x)), ISet("x", AEBop(Bop.ADD, x, AEUop(Uop.OPP, one)))
factorial = ISeq(ISeq(bound_check,init_y),loop) )
loop = ILoop(BENeg(BELeq(x, zero)), body)
factorial = ISeq(ISeq(bound_check, init_y), loop)
print(f"prog is\n{factorial}") print(f"prog is\n{factorial}")
env = { "x" : 4 } env = {"x": 4}
envf = eval_instr(env,factorial) envf = eval_instr(env, factorial)
print(f"init is \n{env}") print(f"init is \n{env}")
print(f"result is\n{envf}") print(f"result is\n{envf}")
TP2/iteration.py
+ 55
− 10
View file @ fab51399
...@@ -5,42 +5,87 @@ each static analysis. ...@@ -5,42 +5,87 @@ each static analysis.
- fixpoint_iteration computes a fixpoint over a cfg for the given - fixpoint_iteration computes a fixpoint over a cfg for the given
transfer instance transfer instance
""" """
from cfg import * from cfg import *
from typing import Protocol from typing import Protocol
class Transfer[S](Protocol): class Transfer[S](Protocol):
"""lists the functions that must be implemented for a static analysis over Lattice S""" """lists the functions that must be implemented for a static analysis over Lattice S"""
def bottom(self) -> S: def bottom(self) -> S:
"""the empty state, associated to unvisited nodes""" """the empty state, associated to unvisited nodes"""
... ...
def init_state(self) -> S: def init_state(self) -> S:
"""the state associated to the initial node""" """the state associated to the initial node"""
... ...
def join(self,s1:S,s2:S) -> S:
def join(self, s1: S, s2: S) -> S:
"""join of two states when merging branches""" """join of two states when merging branches"""
... ...
def included(self,s1: S,s2: S) -> bool:
def included(self, s1: S, s2: S) -> bool:
"""return True when the first state is included in the second""" """return True when the first state is included in the second"""
... ...
def tr_skip(self,s: S) -> S:
def tr_skip(self, s: S) -> S:
"""transfer state across a Skip transition """transfer state across a Skip transition
Almost always transfer the state unchanged Almost always transfer the state unchanged
""" """
return s return s
def tr_set(self,s: S,v: str,e: ArithExpr) -> S:
def tr_set(self, s: S, v: str, e: ArithExpr) -> S:
"""transfer state across an assignment""" """transfer state across an assignment"""
... ...
def tr_test(self,s: S,c: BoolExpr) -> S:
def tr_test(self, s: S, c: BoolExpr) -> S:
"""transfer state across a test transition""" """transfer state across a test transition"""
... ...
def tr_err(self,s: S,e: Expr) -> S:
def tr_err(self, s: S, e: Expr) -> S:
"""transfer state across a transition to error state""" """transfer state across a transition to error state"""
... ...
def fixpoint_iteration[T](transfer: Transfer[T], cfg: Cfg) -> dict[Node,T]:
def fixpoint_iteration[T](transfer: Transfer, cfg: Cfg) -> dict[Node, T]:
"""computes the fixpoint for the given transfer functions over the given CfG """computes the fixpoint for the given transfer functions over the given CfG
output maps each node to the computed state output maps each node to the computed state
""" """
raise NotImplementedError mapping: dict[Node, T] = {}
for node in cfg.g.nodes:
if node == cfg.init_node:
mapping[node] = transfer.init_state()
else:
mapping[node] = transfer.bottom()
worklist = [(cfg.init_node, dest, lab) for (dest, lab) in cfg.init_node.succs]
while worklist:
src, dst, label = worklist.pop(0)
s_src = mapping[src]
if isinstance(label, LSkip):
s_new = transfer.tr_skip(s_src)
elif isinstance(label, LSet):
s_new = transfer.tr_set(s_src, label.var, label.expr)
elif isinstance(label, LTest):
s_new = transfer.tr_test(s_src, label.cond)
elif isinstance(label, LErr):
s_new = transfer.tr_err(s_src, label.err)
else:
s_new = s_src
new_state = transfer.join(mapping[dst], s_new)
if not transfer.included(mapping[dst], new_state):
mapping[dst] = new_state
for succ, lab in dst.succs:
worklist.append((dst, succ, lab))
return mapping
"""
# À quoi correspondent les nœuds indiqués comme inatteignables par l'analyse?
Les nœuds inatteignables correspondent aux branches du programme qui ne peuvent jamais être exécutées, car leur condition s’évalue toujours à False dans l’analyse.
"""
TP2/opsem.py
+ 88
− 33
View file @ fab51399
"""
Operational semantics for the Why language
Provides evaluation functions for the three syntactic classes,
based on a environment mapping variables to integer values.
These functions return None when an error occur somewhere (Big step semantics)
"""
from syntax import * from syntax import *
def eval_aexp(env: dict[str,int], exp: ArithExpr) -> int | None: def eval_aexp(env: dict[str,int], exp: ArithExpr) -> int | None:
"""evaluates an arithmetic expression""" """evaluates an arithmetic expression"""
match exp: match exp:
case AECst(value): case AECst(value):
raise NotImplementedError return value
case AEVar(var): case AEVar(var):
raise NotImplementedError return env.get(var, None)
case AEUop(uop,expr): case AEUop(uop, expr):
raise NotImplementedError v = eval_aexp(env, expr)
case AEBop(bop,left_expr,right_expr): if v is None:
raise NotImplementedError return None
case _: assert False match uop:
case Uop.OPP:
return -v
case _:
return None
case AEBop(bop, left_expr, right_expr):
left_val = eval_aexp(env, left_expr)
right_val = eval_aexp(env, right_expr)
if left_val is None or right_val is None:
return None
match bop:
case Bop.ADD:
return left_val + right_val
case Bop.MUL:
return left_val * right_val
case Bop.DIV:
if right_val == 0:
return None
return left_val // right_val
case _:
return None
case _:
assert False
def eval_bexp(env: dict[str,int], exp:BoolExpr) -> bool | None: def eval_bexp(env: dict[str,int], exp: BoolExpr) -> bool | None:
"""evaluates a boolean expression""" """evaluates a boolean expression"""
match exp: match exp:
case BEPlain(aexpr): case BEPlain(aexpr):
raise NotImplementedError val = eval_aexp(env, aexpr)
case BEEq(left_expr,right_expr): if val is None:
raise NotImplementedError return None
case BELeq(left_expr,right_expr): return val != 0
raise NotImplementedError case BEEq(left_expr, right_expr):
left_val = eval_aexp(env, left_expr)
right_val = eval_aexp(env, right_expr)
if left_val is None or right_val is None:
return None
return left_val == right_val
case BELeq(left_expr, right_expr):
left_val = eval_aexp(env, left_expr)
right_val = eval_aexp(env, right_expr)
if left_val is None or right_val is None:
return None
return left_val <= right_val
case BENeg(expr): case BENeg(expr):
raise NotImplementedError val = eval_bexp(env, expr)
case _: assert False if val is None:
return None
return not val
case _:
assert False
def eval_instr(env: dict[str,int], instr: Instr) -> dict[str,int] | None: def eval_instr(env: dict[str,int], instr: Instr) -> dict[str,int] | None:
"""evaluates an instruction""" """evaluates an instruction"""
match instr: match instr:
case ISkip(): case ISkip():
raise NotImplementedError return env
case ISet(var,expr): case ISet(var, expr):
raise NotImplementedError val = eval_aexp(env, expr)
case ISeq(first,second): if val is None:
raise NotImplementedError return None
case ICond(cond,true_branch,false_branch): new_env = env.copy()
raise NotImplementedError new_env[var] = val
case ILoop(cond,body): return new_env
raise NotImplementedError case ISeq(first, second):
case _: assert False env1 = eval_instr(env, first)
if env1 is None:
return None
return eval_instr(env1, second)
case ICond(cond, true_branch, false_branch):
b = eval_bexp(env, cond)
if b is None:
return None
if b:
return eval_instr(env, true_branch)
else:
return eval_instr(env, false_branch)
case ILoop(cond, body):
current_env = env
while True:
b = eval_bexp(current_env, cond)
if b is None:
return None
if not b:
break
new_env = eval_instr(current_env, body)
if new_env is None:
return None
current_env = new_env
return current_env
case _:
assert False
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment