From fab51399db25dff4efb4b0da4d468d92a5c09c31 Mon Sep 17 00:00:00 2001
From: Nicolas Descamps <nicolas.descamps@theodo.com>
Date: Fri, 28 Mar 2025 15:58:15 +0100
Subject: [PATCH] TP Python
---
TP2/constant_propagation.py | 181 +++++++++++++++++++++++++++---------
TP2/example_opsem.py | 16 ++--
TP2/iteration.py | 65 +++++++++++--
TP2/opsem.py | 121 +++++++++++++++++-------
4 files changed, 288 insertions(+), 95 deletions(-)
diff --git a/TP2/constant_propagation.py b/TP2/constant_propagation.py
index a530c34..a7afd78 100644
--- a/TP2/constant_propagation.py
+++ b/TP2/constant_propagation.py
@@ -7,13 +7,17 @@ from cfg import Label, LSkip, LSet, LTest, LErr
from iteration import Transfer
from syntax import *
+
@dataclass
class abstract_value[T]:
"""None indicates that we don't know the precise value"""
+
value: T | None
+
def __str__(self):
return f"{self.value}"
+
type abstract_env = dict[str, abstract_value[int]]
"""mapping from variables to abstract values.
@@ -24,84 +28,171 @@ type state = abstract_env | None
"""abstract state is either an abstract env or bottom
"""
+
def eval_aexp(env: abstract_env, e: ArithExpr) -> abstract_value[int] | None:
"""evaluate an arithmetic expression in an abstract environment
returns None in case of error
"""
match e:
- case AECst(value): return abstract_value(value)
+ case AECst(value):
+ return abstract_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: return None
- if res.value is None: return abstract_value(None)
- if uop == Uop.OPP: return abstract_value(-res.value)
+ if var in env:
+ return env[var]
+ else:
+ return None
+ case AEUop(uop, expr):
+ res = eval_aexp(env, expr)
+ 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
- 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
+ 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 v1.value is None or v2.value is None:
return abstract_value(None)
match bop:
- case Bop.ADD: return abstract_value(v1.value+v2.value)
- case Bop.MUL: return abstract_value(v1.value*v2.value)
+ case Bop.ADD:
+ return abstract_value(v1.value + v2.value)
+ case Bop.MUL:
+ return abstract_value(v1.value * v2.value)
case Bop.DIV:
- if v2.value == 0: return None
- return abstract_value(v1.value//v2.value)
- case _: assert False
+ if v2.value == 0:
+ return None
+ return abstract_value(v1.value // v2.value)
+ case _:
+ assert False
+
def eval_bexp(env: abstract_env, e: BoolExpr) -> abstract_value[bool] | None:
"""abstract evaluation of a boolean expression"""
match e:
case BEPlain(aexpr):
res = eval_aexp(env, aexpr)
- if res is None: return None
- if res.value is None: return abstract_value(None)
- return abstract_value(res.value!=0)
- case BEEq(left_expr,right_expr):
+ if res is None:
+ return None
+ if res.value is None:
+ return abstract_value(None)
+ return abstract_value(res.value != 0)
+ 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 v1.value is None or v2.value is None: return abstract_value(None)
+ if v1 is None or v2 is None:
+ return None
+ if v1.value is None or v2.value is None:
+ return abstract_value(None)
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)
v2 = eval_aexp(env, right_expr)
- if v1 is None or v2 is None: return None
- if v1.value is None or v2.value is None: return abstract_value(None)
+ if v1 is None or v2 is None:
+ return None
+ if v1.value is None or v2.value is None:
+ return abstract_value(None)
return abstract_value(v1.value <= v2.value)
case BENeg(expr):
- v = eval_bexp(env,expr)
- if v is None: return None
- if v.value is None: return v
+ v = eval_bexp(env, expr)
+ if v is None:
+ return None
+ if v.value is None:
+ return v
return abstract_value(not v.value)
- case _: assert False
+ case _:
+ assert False
+
class Constant_propagation(Transfer[state]):
variables: frozenset[str]
- def __init__(self,instr):
+
+ def __init__(self, instr):
self.variables = variables_of_instr(instr)
+
def bottom(self) -> state:
- ...
+ return None
+
def init_state(self) -> state:
- ...
- def join(self,s1:state,s2:state) -> state:
- ...
+ return {var: abstract_value(None) for var in self.variables}
- 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
diff --git a/TP2/example_opsem.py b/TP2/example_opsem.py
index bcc5dca..710e738 100644
--- a/TP2/example_opsem.py
+++ b/TP2/example_opsem.py
@@ -6,16 +6,18 @@ y = AEVar("y")
zero = AECst(0)
one = AECst(1)
xneg = BELeq(x, zero)
-bound_check = ICond(xneg,ISet("x",one),ISkip())
-init_y = ISet("y",one)
-body = ISeq(ISet("y",AEBop(Bop.MUL,y,x)),ISet("x",AEBop(Bop.ADD,x,AEUop(Uop.OPP,one))))
-loop = ILoop(BENeg(BELeq(x,zero)),body)
-factorial = ISeq(ISeq(bound_check,init_y),loop)
+bound_check = ICond(xneg, ISet("x", one), ISkip())
+init_y = ISet("y", one)
+body = ISeq(
+ ISet("y", AEBop(Bop.MUL, y, x)), ISet("x", AEBop(Bop.ADD, x, AEUop(Uop.OPP, one)))
+)
+loop = ILoop(BENeg(BELeq(x, zero)), body)
+factorial = ISeq(ISeq(bound_check, init_y), loop)
print(f"prog is\n{factorial}")
-env = { "x" : 4 }
-envf = eval_instr(env,factorial)
+env = {"x": 4}
+envf = eval_instr(env, factorial)
print(f"init is \n{env}")
print(f"result is\n{envf}")
diff --git a/TP2/iteration.py b/TP2/iteration.py
index f911696..9af0e5a 100644
--- a/TP2/iteration.py
+++ b/TP2/iteration.py
@@ -5,42 +5,87 @@ each static analysis.
- fixpoint_iteration computes a fixpoint over a cfg for the given
transfer instance
"""
+
from cfg import *
from typing import Protocol
+
class Transfer[S](Protocol):
"""lists the functions that must be implemented for a static analysis over Lattice S"""
+
def bottom(self) -> S:
"""the empty state, associated to unvisited nodes"""
...
+
def init_state(self) -> S:
"""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"""
...
- 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"""
...
- def tr_skip(self,s: S) -> S:
+
+ def tr_skip(self, s: S) -> S:
"""transfer state across a Skip transition
Almost always transfer the state unchanged
"""
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"""
...
- def tr_test(self,s: S,c: BoolExpr) -> S:
+
+ def tr_test(self, s: S, c: BoolExpr) -> S:
"""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"""
...
-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
-
- 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.
+"""
diff --git a/TP2/opsem.py b/TP2/opsem.py
index 1313e98..1c3507d 100644
--- a/TP2/opsem.py
+++ b/TP2/opsem.py
@@ -1,50 +1,105 @@
-"""
-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 *
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
- case AEUop(uop,expr):
- raise NotImplementedError
- case AEBop(bop,left_expr,right_expr):
- raise NotImplementedError
- case _: assert False
+ return env.get(var, None)
+ case AEUop(uop, expr):
+ v = eval_aexp(env, expr)
+ if v is None:
+ return None
+ 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"""
match exp:
case BEPlain(aexpr):
- raise NotImplementedError
- case BEEq(left_expr,right_expr):
- raise NotImplementedError
- case BELeq(left_expr,right_expr):
- raise NotImplementedError
+ val = eval_aexp(env, aexpr)
+ if val is None:
+ return None
+ return val != 0
+ 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):
- raise NotImplementedError
- case _: assert False
+ val = eval_bexp(env, expr)
+ 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:
"""evaluates an instruction"""
match instr:
case ISkip():
- raise NotImplementedError
- case ISet(var,expr):
- raise NotImplementedError
- case ISeq(first,second):
- raise NotImplementedError
- case ICond(cond,true_branch,false_branch):
- raise NotImplementedError
- case ILoop(cond,body):
- raise NotImplementedError
- case _: assert False
+ return env
+ case ISet(var, expr):
+ val = eval_aexp(env, expr)
+ if val is None:
+ return None
+ new_env = env.copy()
+ new_env[var] = val
+ return new_env
+ case ISeq(first, second):
+ 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
--
GitLab