diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..f4a6e982c2bf46f9d16524dec503e8473a4e63f7
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,165 @@
+### https://raw.github.com/github/gitignore/4488915eec0b3a45b5c63ead28f286819c0917de/Python.gitignore
+
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+# Usually these files are written by a python script from a template
+# before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+cover/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+.pybuilder/
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+# For a library or package, you might want to ignore these files since the code is
+# intended to run in multiple environments; otherwise, check them in:
+# .python-version
+
+# pipenv
+# According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+# However, in case of collaboration, if having platform-specific dependencies or dependencies
+# having no cross-platform support, pipenv may install dependencies that don't work, or not
+# install all needed dependencies.
+#Pipfile.lock
+
+# poetry
+# Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control.
+# This is especially recommended for binary packages to ensure reproducibility, and is more
+# commonly ignored for libraries.
+# https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control
+#poetry.lock
+
+# pdm
+# Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control.
+#pdm.lock
+# pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it
+# in version control.
+# https://pdm.fming.dev/#use-with-ide
+.pdm.toml
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/
+
+# pytype static type analyzer
+.pytype/
+
+# Cython debug symbols
+cython_debug/
+
+# PyCharm
+# JetBrains specific template is maintained in a separate JetBrains.gitignore that can
+# be found at https://github.com/github/gitignore/blob/main/Global/JetBrains.gitignore
+# and can be added to the global gitignore or merged into this file. For a more nuclear
+# option (not recommended) you can uncomment the following to ignore the entire idea folder.
+#.idea/
+
+# Aargh nix
+Pystan/.direnv/
diff --git a/Pystan/.envrc b/Pystan/.envrc
new file mode 100644
index 0000000000000000000000000000000000000000..3550a30f2de389e537ee40ca5e64a77dc185c79b
--- /dev/null
+++ b/Pystan/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/Pystan/config/.gitignore b/Pystan/config/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..f35b094363ce2e9783e3c95ce2960898844d7da8
--- /dev/null
+++ b/Pystan/config/.gitignore
@@ -0,0 +1,164 @@
+### https://raw.github.com/github/gitignore/4488915eec0b3a45b5c63ead28f286819c0917de/Python.gitignore
+
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+# Usually these files are written by a python script from a template
+# before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+cover/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+.pybuilder/
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+# For a library or package, you might want to ignore these files since the code is
+# intended to run in multiple environments; otherwise, check them in:
+# .python-version
+
+# pipenv
+# According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+# However, in case of collaboration, if having platform-specific dependencies or dependencies
+# having no cross-platform support, pipenv may install dependencies that don't work, or not
+# install all needed dependencies.
+#Pipfile.lock
+
+# poetry
+# Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control.
+# This is especially recommended for binary packages to ensure reproducibility, and is more
+# commonly ignored for libraries.
+# https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control
+#poetry.lock
+
+# pdm
+# Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control.
+#pdm.lock
+# pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it
+# in version control.
+# https://pdm.fming.dev/#use-with-ide
+.pdm.toml
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/
+
+# pytype static type analyzer
+.pytype/
+
+# Cython debug symbols
+cython_debug/
+
+# PyCharm
+# JetBrains specific template is maintained in a separate JetBrains.gitignore that can
+# be found at https://github.com/github/gitignore/blob/main/Global/JetBrains.gitignore
+# and can be added to the global gitignore or merged into this file. For a more nuclear
+# option (not recommended) you can uncomment the following to ignore the entire idea folder.
+#.idea/
+
+
diff --git a/Pystan/config/cfg.py b/Pystan/config/cfg.py
new file mode 100644
index 0000000000000000000000000000000000000000..e8d828750d6842487b77be38a0607c6ddb0c9c6d
--- /dev/null
+++ b/Pystan/config/cfg.py
@@ -0,0 +1,144 @@
+"""Control flow graphs
+
+- Label and its subclasses describe the label on the edges of the CfGs
+- Nodes describes nodes, with an id and its successors
+- Graph describes a graph
+- Cfg describes a cfg, i.e. a graph with initial, final, and error nodes
+- function cfg creates a cfg for the given program
+"""
+from syntax import *
+from dataclasses import dataclass
+
+@dataclass
+class Label:
+ """generic class for edges' labels"""
+ pass
+
+@dataclass
+class LSkip(Label):
+ """label skip (does nothing)"""
+ def __str__(self):
+ return "skip"
+
+@dataclass
+class LSet(Label):
+ """assignment label"""
+ var: str
+ expr: ArithExpr
+ def __str__(self):
+ return f"{self.var} := {self.expr}"
+
+@dataclass
+class LTest(Label):
+ """test label"""
+ cond: BoolExpr
+ def __str__(self):
+ return f"?{self.cond}"
+
+@dataclass
+class LErr(Label):
+ """error label"""
+ err: Expr
+ def __str__(self):
+ return f"Err({self.err})"
+
+class Node:
+ """node of the graph, with its id and its successors"""
+ def __init__(self,nid):
+ self.nid = nid
+ self.succs = []
+ def __str__(self):
+ return f"Node {self.nid}"
+
+class Graph:
+ nb_nid: int
+ nodes: list[Node]
+
+ """a graph, i.e. a list of nodes"""
+ def __init__(self):
+ self.nb_nid = 0
+ self.nodes = []
+
+ def new_node(self) -> Node:
+ """creates a new node, with a fresh id and no succs"""
+ node = Node(self.nb_nid)
+ self.nb_nid += 1
+ self.nodes += [node]
+ return node
+
+ def new_edge(self,n1: Node,n2: Node,l: Label) -> None:
+ """creates a new edge.
+ If the nodes are not already in the graph, they are added.
+ In that case, no check is made that a node with the same id
+ is already present or not.
+ """
+ if n1 not in self.nodes:
+ self.nodes += [n1]
+ if n2 not in self.nodes:
+ self.nodes += [n2]
+ n1.succs += [(n2,l)]
+
+def cfg_aux(g:Graph,e:Node,i:Node,instr:Instr) -> Node:
+ """auxiliary function to build a CfG
+ takes as argument a graph, the error node, the node starting
+ the current instruction, and the instruction itself, returns
+ the final node of current instruction
+ """
+ match instr:
+ case ISkip():
+ f = g.new_node()
+ g.new_edge(i,f,LSkip())
+ return f
+ case ISet(var,expr):
+ f = g.new_node()
+ g.new_edge(i,f,LSet(var,expr))
+ g.new_edge(i,e,LErr(expr))
+ return f
+ case ISeq(first,second):
+ m = cfg_aux(g,e,i,first)
+ return cfg_aux(g,e,m,second)
+ case ICond(cond,true_branch,false_branch):
+ t = g.new_node()
+ f = g.new_node()
+ g.new_edge(i,t,LTest(cond))
+ g.new_edge(i,f,LTest(BENeg(cond)))
+ g.new_edge(i,e,LErr(cond))
+ tf = cfg_aux(g,e,t,true_branch)
+ ff = cfg_aux(g,e,f,false_branch)
+ f = g.new_node()
+ g.new_edge(tf,f,LSkip())
+ g.new_edge(ff,f,LSkip())
+ return f
+ case ILoop(cond,body):
+ ib = g.new_node()
+ f = g.new_node()
+ g.new_edge(i,ib,LTest(cond))
+ g.new_edge(i,f,LTest(BENeg(cond)))
+ g.new_edge(i,e,LErr(cond))
+ fb = cfg_aux(g,e,ib,body)
+ g.new_edge(fb,i,LSkip())
+ return f
+ case _: assert False
+
+class Cfg:
+ """describes a CfG"""
+ g: Graph
+ err_node: Node
+ init_node: Node
+ final_node: Node
+ def __init__(self,instr):
+ self.g = Graph()
+ self.err_node = self.g.new_node()
+ self.init_node = self.g.new_node()
+ self.final_node = cfg_aux(self.g,self.err_node,self.init_node,instr)
+
+ def __str__(self):
+ res = ""
+ for node in self.g.nodes:
+ res+=f"{node}:\n"
+ for (dest,lab) in node.succs:
+ res+=f" {lab} --> {dest}\n"
+ res+=f"init node is {self.init_node}\n"
+ res+=f"final node is {self.final_node}\n"
+ res+=f"err node is {self.err_node}\n"
+ return res
diff --git a/Pystan/config/constant_propagation.py b/Pystan/config/constant_propagation.py
new file mode 100644
index 0000000000000000000000000000000000000000..81bc7a20ab8fd0995277217eff73cbd5c4094e9d
--- /dev/null
+++ b/Pystan/config/constant_propagation.py
@@ -0,0 +1,154 @@
+"""
+implements a constant propagation analysis
+"""
+
+from dataclasses import dataclass
+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.
+
+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 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 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)
+ 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.DIV:
+ 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):
+ 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)
+ return abstract_value(v1.value == v2.value)
+ 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)
+ 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
+ return abstract_value(not v.value)
+ case _: assert False
+
+class Constant_propagation(Transfer[state]):
+ variables: frozenset[str]
+ def __init__(self,instr):
+ self.variables = variables_of_instr(instr)
+ def bottom(self) -> state:
+ return None
+ def init_state(self) -> state:
+ return {v : abstract_value(None) for v in self.variables}
+ def join(self,s1:state,s2:state) -> state:
+ match (s1, s2):
+ case None, s2:
+ return s2
+ case s1, None:
+ return s1
+ case s1, s2:
+ s: state = s1.copy()
+ for var in s2:
+ if not(var in s1) or s1[var] == abstract_value(None):
+ s = s | {var:s2[var]}
+ elif s2[var] == abstract_value(None):
+ pass
+ elif s1[var] != s2[var]:
+ s = s | {var: abstract_value(None)}
+ return s
+
+ def included(self,s1: state,s2: state) -> bool:
+ match (s1, s2):
+ case None, s2:
+ return True
+ case s1, None:
+ return False
+ case s1, s2:
+ for v in s1:
+ if (s1[v] != abstract_value(None) and s1[v] != s2[v]):
+ return False
+ return True
+ def tr_skip(self,s: state) -> state:
+ return s
+
+ def tr_set(self,s: state,v: str,e: ArithExpr) -> state:
+ if s == None:
+ return None
+ value = eval_aexp(s,e)
+ if value == None:
+ # Do we return None or abstract_value(None)
+ return None
+ return s | {v:value}
+
+ def tr_test(self,s: state,c: BoolExpr) -> state:
+ if s == None:
+ return None
+ # Are we sure of that ?
+ if eval_bexp(s,c) == abstract_value(False):
+ return None
+ return s
+
+ def tr_err(self,s: state,e: Expr) -> state:
+ if s == None:
+ return None
+ match e:
+ case ArithExpr():
+ if eval_aexp(s,e) == None:
+ return s
+ else:
+ return None
+ case BoolExpr():
+ if eval_bexp(s,e) == None:
+ return s
+ else:
+ return None
+ case _:
+ return None
diff --git a/Pystan/config/example_constant_propagation.py b/Pystan/config/example_constant_propagation.py
new file mode 100644
index 0000000000000000000000000000000000000000..0bf11f1a7a796124d13f8a3ea0e579835985a6d2
--- /dev/null
+++ b/Pystan/config/example_constant_propagation.py
@@ -0,0 +1,29 @@
+from syntax import *
+from cfg import Cfg
+from iteration import fixpoint_iteration
+from constant_propagation import Constant_propagation
+
+x = AEVar("x")
+y = AEVar("y")
+c = AEVar("c")
+one = AECst(1)
+zero = AECst(0)
+
+propagate_compute=ISeq(ISet("x",one),ISet("x", AEBop(Bop.ADD,x,one)))
+same_branch_if=ICond(BELeq(c,zero), ISet("y", one), ISet("y",one))
+equal_branch=ICond(BEEq(c,one),ISkip(),ISet("c",one))
+
+prog = ISeq(ISeq(propagate_compute,same_branch_if),equal_branch)
+
+cfg = Cfg(prog)
+
+cst_propagation = Constant_propagation(prog)
+
+res = fixpoint_iteration(cst_propagation,cfg)
+
+for (node, state) in res.items():
+ print(f"{node}:")
+ if state is None: print(" None")
+ else:
+ for (var, value) in state.items():
+ print(f" {var} -> {value}")
diff --git a/Pystan/config/example_interval.py b/Pystan/config/example_interval.py
new file mode 100644
index 0000000000000000000000000000000000000000..8aa35e01334ffe53cbe00789994a19c11f544c59
--- /dev/null
+++ b/Pystan/config/example_interval.py
@@ -0,0 +1,4 @@
+from interval_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)
diff --git a/Pystan/config/example_interval_eval_exp.py b/Pystan/config/example_interval_eval_exp.py
new file mode 100644
index 0000000000000000000000000000000000000000..1203cab645be505a71cd14888374824eca277e68
--- /dev/null
+++ b/Pystan/config/example_interval_eval_exp.py
@@ -0,0 +1,32 @@
+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({})
diff --git a/Pystan/config/example_interval_reduce.py b/Pystan/config/example_interval_reduce.py
new file mode 100644
index 0000000000000000000000000000000000000000..2d7cdda54e9d02cfd00b41b9a65d67b63f5120b9
--- /dev/null
+++ b/Pystan/config/example_interval_reduce.py
@@ -0,0 +1,39 @@
+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) })
diff --git a/Pystan/config/example_iteration.py b/Pystan/config/example_iteration.py
new file mode 100644
index 0000000000000000000000000000000000000000..3a9a71bb66f797cb0a6ac81b285ed1c2a8da2f75
--- /dev/null
+++ b/Pystan/config/example_iteration.py
@@ -0,0 +1,52 @@
+from syntax import *
+from cfg import Cfg
+from iteration import *
+from opsem import eval_bexp, eval_aexp
+
+one = AECst(1)
+zero = AECst(0)
+x = AEVar("x")
+dead_if=ICond(BEPlain(one),ISet("x",one),ISet("y",zero))
+infinite_loop=ILoop(BEPlain(one),ISet("x",AEBop(Bop.ADD,x,one)))
+prog_with_dead_code=ISeq(dead_if,infinite_loop)
+
+class NoInfo(Transfer[frozenset[bool]]):
+ """Almost trivial static analysis
+
+ We only have two elements in our lattice, the empty set and the singleton {True}.
+ The latter is propagated from initial state to any potentially reachable state.
+ In the end, the only nodes still at bottom are the one which are guarded by
+ always-false tests.
+ """
+ type S = frozenset[bool]
+ def bottom(self) -> S: return frozenset()
+ def init_state(self) -> S: return frozenset([True])
+ def join(self, s1:S, s2:S) -> S: return s1 | s2
+ def included(self, s1:S, s2:S) -> bool: return s1.issubset(s2)
+ def tr_skip(self,s:S): return s
+ def tr_set(self, s:S, v:str, e: ArithExpr) -> S: return s
+ def tr_test(self,s:S, c:BoolExpr) -> S:
+ if eval_bexp({},c) is False:
+ return frozenset()
+ else:
+ return s
+ def tr_err(self, s:S, e:Expr) -> S:
+ if isinstance(e,ArithExpr):
+ if eval_aexp({},e) is not None:
+ return frozenset()
+ else:
+ return s
+ else:
+ if isinstance(e,BoolExpr):
+ if eval_bexp({},e) is not None:
+ return frozenset()
+ else:
+ return s
+ else: assert False
+
+cfg = Cfg(prog_with_dead_code)
+print(f"Cfg is {cfg}")
+res = fixpoint_iteration(NoInfo(),cfg)
+unreachable = [node for node, state in res.items() if state == frozenset()]
+for node in unreachable:
+ print(f"{node} is unreachable")
diff --git a/Pystan/config/example_opsem.py b/Pystan/config/example_opsem.py
new file mode 100644
index 0000000000000000000000000000000000000000..bcc5dca4e8bbb042e3de024382c4cab6ac304b65
--- /dev/null
+++ b/Pystan/config/example_opsem.py
@@ -0,0 +1,21 @@
+from syntax import *
+from opsem import eval_instr
+
+x = AEVar("x")
+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)
+
+print(f"prog is\n{factorial}")
+
+env = { "x" : 4 }
+envf = eval_instr(env,factorial)
+
+print(f"init is \n{env}")
+print(f"result is\n{envf}")
diff --git a/Pystan/config/example_sign.py b/Pystan/config/example_sign.py
new file mode 100644
index 0000000000000000000000000000000000000000..6aa6de3d4adb559dddcd246d9cdb3159f2f12b67
--- /dev/null
+++ b/Pystan/config/example_sign.py
@@ -0,0 +1,4 @@
+from sign_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)
diff --git a/Pystan/config/example_sign_eval_exp.py b/Pystan/config/example_sign_eval_exp.py
new file mode 100644
index 0000000000000000000000000000000000000000..c8bdd995dad92d272d407c6a2c040666e1f2ad29
--- /dev/null
+++ b/Pystan/config/example_sign_eval_exp.py
@@ -0,0 +1,28 @@
+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({})
diff --git a/Pystan/config/example_sign_reduce.py b/Pystan/config/example_sign_reduce.py
new file mode 100644
index 0000000000000000000000000000000000000000..17ed63624d1e282d9f535cccecbdf5d04e169e20
--- /dev/null
+++ b/Pystan/config/example_sign_reduce.py
@@ -0,0 +1,33 @@
+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 })
+
diff --git a/Pystan/config/example_widen.py b/Pystan/config/example_widen.py
new file mode 100644
index 0000000000000000000000000000000000000000..c9372be7b6162f6f47cd8f7ed8a5c2e240aa187d
--- /dev/null
+++ b/Pystan/config/example_widen.py
@@ -0,0 +1,61 @@
+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}')
diff --git a/Pystan/config/interval_analysis.py b/Pystan/config/interval_analysis.py
new file mode 100644
index 0000000000000000000000000000000000000000..9186efbf8ffeedb0fe1e207381313552f1b34163
--- /dev/null
+++ b/Pystan/config/interval_analysis.py
@@ -0,0 +1,406 @@
+# 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}")
diff --git a/Pystan/config/iteration.py b/Pystan/config/iteration.py
new file mode 100644
index 0000000000000000000000000000000000000000..d06c222af6de8d4ed4bfa294d6ccecfff82d8584
--- /dev/null
+++ b/Pystan/config/iteration.py
@@ -0,0 +1,83 @@
+"""Fixpoint iterator over a CfG
+
+- Transfer is a base class that must be instantiated for
+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:
+ """join of two states when merging branches"""
+ ...
+ 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:
+ """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:
+ """transfer state across an assignment"""
+ ...
+ def tr_test(self,s: S,c: BoolExpr) -> S:
+ """transfer state across a test transition"""
+ ...
+ 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]:
+ """computes the fixpoint for the given transfer functions over the given CfG"""
+
+ env : dict[Node, T] = {}
+ # map bottom to all nodes
+ for node in cfg.g.nodes:
+ env = env | {node : transfer.bottom()}
+ # except map initial state to initial node
+ env = env | {cfg.init_node : transfer.init_state()}
+ # build worklist with all the nodes from the initial node
+ worklist: list[tuple[Node, Node, Label]]= []
+ for edge in cfg.init_node.succs:
+ worklist.append((cfg.init_node,) + edge)
+
+ # as long as the worklist is not empty
+ while worklist != []:
+ e = worklist.pop()
+ src = e[0]
+ dst = e[1]
+ l = e[2]
+
+ s1 = env[dst]
+ s_src = env[src]
+ s2 = s1 # to handled elegantly unmatched cases
+ match l:
+ case LSet(var, expr):
+ s2 = transfer.tr_set(s_src, var, expr)
+ case LTest(cond):
+ s2 = transfer.tr_test(s_src, cond)
+ case LErr(err):
+ s2 = transfer.tr_err(s_src, err)
+ case LSkip():
+ s2 = transfer.tr_skip(s_src)
+ case _:
+ # What should we do here ? Isn't this supposed to be unreachable ?
+ pass
+
+ env = env | {dst : transfer.join(s1, s2)}
+ if not(transfer.included(env[dst], s1)):
+ for edge in dst.succs:
+ worklist.append((dst,) + edge)
+
+ return env
diff --git a/Pystan/config/opsem.py b/Pystan/config/opsem.py
new file mode 100644
index 0000000000000000000000000000000000000000..ba9165b642f31bcdadbe4297b1ca773f4ca7afd5
--- /dev/null
+++ b/Pystan/config/opsem.py
@@ -0,0 +1,110 @@
+"""
+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):
+ return value
+ case AEVar(var):
+ if var in env:
+ return env[var]
+ else:
+ return None
+ case AEUop(uop,expr):
+ v = eval_aexp(env, expr)
+ match uop:
+ case Uop.OPP:
+ if v != None:
+ return - v
+ else:
+ return None
+ case AEBop(bop,left_expr,right_expr):
+ l = eval_aexp(env, left_expr)
+ r = eval_aexp(env, right_expr)
+ if (l == None) or (r == None):
+ return None
+ match bop:
+ case Bop.ADD:
+ return l + r
+ case Bop.MUL:
+ return l * r
+ case Bop.DIV:
+ if r!= 0:
+ return l // r
+ else:
+ return None
+ case _: assert False
+
+def eval_bexp(env: dict[str,int], exp:BoolExpr) -> bool | None:
+ """evaluates a boolean expression"""
+ match exp:
+ case BEPlain(aexpr):
+ v = eval_aexp(env, aexpr)
+ if (v == None):
+ return None
+ return v != 0
+ case BEEq(left_expr,right_expr):
+ l = eval_aexp(env, left_expr)
+ r = eval_aexp(env, right_expr)
+ if (l == None) or (r == None):
+ return None
+ return l == r
+ case BELeq(left_expr,right_expr):
+ l = eval_aexp(env, left_expr)
+ r = eval_aexp(env, right_expr)
+ if (l == None) or (r == None):
+ return None
+ return l <= r
+ case BENeg(expr):
+ v = eval_bexp(env, expr)
+ if v == None:
+ return None
+ return not(v)
+ case _: assert False
+
+def eval_instr(env: dict[str,int], instr: Instr) -> dict[str,int] | None:
+ """evaluates an instruction"""
+ match instr:
+ case ISkip():
+ return env
+ case ISet(var,expr):
+ v = eval_aexp(env, expr)
+ if v == None:
+ return None
+ return env | {var:v}
+ case ISeq(first,second):
+ rho1 = eval_instr(env, first)
+ if rho1 == None:
+ return None
+ return eval_instr(rho1, second)
+ case ICond(cond,true_branch,false_branch):
+ v = eval_bexp(env, cond)
+ t = eval_instr(env, true_branch)
+ f = eval_instr(env, false_branch)
+
+ if (v == None) or (t == None) or (f == None):
+ return None
+ if v:
+ return t
+ else:
+ return f
+ case ILoop(cond,body):
+ v = eval_bexp(env, cond)
+ if (v == None):
+ return None
+ if v:
+ new_env = eval_instr(env, body)
+ if (new_env == None):
+ return None
+ return eval_instr(new_env, ILoop(cond, body))
+ else:
+ return eval_instr(env, ISkip())
+ case _: assert False
diff --git a/Pystan/config/pyrightconfig.json b/Pystan/config/pyrightconfig.json
new file mode 100644
index 0000000000000000000000000000000000000000..80d140e60839ebbee0b542d63f517d4701ec2ae9
--- /dev/null
+++ b/Pystan/config/pyrightconfig.json
@@ -0,0 +1,3 @@
+{
+ "typeCheckingMode" : "standard"
+}
diff --git a/Pystan/config/sign_analysis.py b/Pystan/config/sign_analysis.py
new file mode 100644
index 0000000000000000000000000000000000000000..1988c81fe417dd1d8593f0f5a66546115699d04e
--- /dev/null
+++ b/Pystan/config/sign_analysis.py
@@ -0,0 +1,338 @@
+# pyright: strict
+"""
+implements a sign analysis
+"""
+from enum import Enum, auto
+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}")
diff --git a/Pystan/config/syntax.py b/Pystan/config/syntax.py
new file mode 100644
index 0000000000000000000000000000000000000000..c0938bda1f9a7554cc4db3a13763d0d68732c5bc
--- /dev/null
+++ b/Pystan/config/syntax.py
@@ -0,0 +1,185 @@
+"""Nodes of the abstract syntax tree of the program:
+
+- Uop/Bop represent unary/binary arithmetic operator
+- ArithExpr and its children describe arithmetic expressions
+- BoolExpr and its children describe boolean expressions
+- Instr and its children describe instruction
+
+"""
+from enum import Enum
+from dataclasses import dataclass
+
+class Uop(Enum):
+ """unary operators. Currently only unary minus"""
+ OPP = 1
+ def __str__(self):
+ if self is Uop.OPP:
+ return "-"
+ return ""
+
+class Bop(Enum):
+ """binary operators: addition, multiplication, and division"""
+ ADD = 1
+ MUL = 2
+ DIV = 3
+ def __str__(self):
+ match self:
+ case Bop.ADD: return "+"
+ case Bop.MUL: return "*"
+ case Bop.DIV: return "/"
+
+class Expr:
+ """generic class for expressions, either arithmetic or boolean"""
+ pass
+
+@dataclass
+class ArithExpr(Expr):
+ """generic class for arithmetic expressions"""
+ pass
+
+@dataclass
+class AECst(ArithExpr):
+ """integer constants"""
+ value: int
+ def __str__(self):
+ return f"{self.value}"
+
+@dataclass
+class AEVar(ArithExpr):
+ """variables"""
+ var: str
+ def __str__(self):
+ return self.var
+
+@dataclass
+class AEUop(ArithExpr):
+ """unary operation"""
+ uop: Uop
+ expr: ArithExpr
+ def __str__(self):
+ return f"{self.uop}{self.expr}"
+
+@dataclass
+class AEBop(ArithExpr):
+ """binary operation"""
+ bop: Bop
+ left_expr: ArithExpr
+ right_expr: ArithExpr
+ def __str__(self):
+ #TODO: only put parentheses if necessary
+ return f"({self.left_expr}) {self.bop} ({self.right_expr})"
+
+@dataclass
+class BoolExpr(Expr):
+ """generic class for boolean expressions"""
+ pass
+
+@dataclass
+class BEPlain(BoolExpr):
+ """arithmetic expression (true if not 0)"""
+ aexpr: ArithExpr
+ def __str__(self):
+ return f"{self.aexpr}"
+
+@dataclass
+class BEEq(BoolExpr):
+ """equality between two arithmetic expression"""
+ left_expr: ArithExpr
+ right_expr:ArithExpr
+ def __str__(self):
+ return f"{self.left_expr} = {self.right_expr}"
+
+@dataclass
+class BELeq(BoolExpr):
+ """less or equal"""
+ left_expr: ArithExpr
+ right_expr: ArithExpr
+ def __str__(self):
+ return f"{self.left_expr} <= {self.right_expr}"
+
+@dataclass
+class BENeg(BoolExpr):
+ """Negation"""
+ expr: BoolExpr
+ def __str__(self):
+ return f"!{self.expr}"
+
+class Instr:
+ """generic class for instruction"""
+ pass
+
+@dataclass
+class ISkip(Instr):
+ """Skip (do nothing)"""
+ def __str__(self):
+ return "skip"
+
+@dataclass
+class ISet(Instr):
+ """assignment to a variable"""
+ var: str
+ expr: ArithExpr
+ def __str__(self):
+ return f"{self.var} := {self.expr}"
+
+@dataclass
+class ISeq(Instr):
+ """sequence of two instructions"""
+ first: Instr
+ second: Instr
+ def __str__(self):
+ return f"{self.first};\n{self.second}"
+
+@dataclass
+class ICond(Instr):
+ """if then else"""
+ cond: BoolExpr
+ true_branch: Instr
+ false_branch: Instr
+ def __str__(self):
+ return f"if {self.cond} then\n{self.true_branch}\nelse\n{self.false_branch}\nfi"
+
+@dataclass
+class ILoop(Instr):
+ """while loop"""
+ cond: BoolExpr
+ body: Instr
+ def __str__(self):
+ return f"while {self.cond} do\n{self.body}\ndone"
+
+def variables_of_aexpr(e: ArithExpr) -> frozenset[str]:
+ """return the set of variables appearing in the expression"""
+ match e:
+ case AECst(_): return frozenset()
+ case AEVar(var): return frozenset(var)
+ case AEUop(expr=e): return variables_of_aexpr(e)
+ case AEBop(left_expr=le,right_expr=re):
+ return variables_of_aexpr(le) | variables_of_aexpr(re)
+ case _: assert False
+
+def variables_of_bexpr(e: BoolExpr) -> frozenset[str]:
+ """return the set of variable appearing in the expression"""
+ match e:
+ case BEPlain(expr): return variables_of_aexpr(expr)
+ case BEEq(left_expr=le,right_expr=re):
+ return variables_of_aexpr(le) | variables_of_aexpr(re)
+ case BELeq(left_expr=le,right_expr=re):
+ return variables_of_aexpr(le) | variables_of_aexpr(re)
+ case BENeg(expr):
+ return variables_of_bexpr(expr)
+ case _: assert False
+
+def variables_of_instr(instr: Instr) -> frozenset[str]:
+ """return the set of variables appearing in a program"""
+ match instr:
+ case ISkip(): return frozenset()
+ case ISet(var=v,expr=e):
+ return frozenset([v]) | variables_of_aexpr(e)
+ case ISeq(first=i1,second=i2):
+ return variables_of_instr(i1) | variables_of_instr(i2)
+ case ICond(cond=c,true_branch=tb,false_branch=fb):
+ vbranches = variables_of_instr(tb) | variables_of_instr(fb)
+ return variables_of_bexpr(c) | vbranches
+ case ILoop(cond=c,body=b):
+ return variables_of_bexpr(c) | variables_of_instr(b)
+ case _ : assert False
diff --git a/Pystan/flake.lock b/Pystan/flake.lock
new file mode 100644
index 0000000000000000000000000000000000000000..1d0fc862615d94a19522e37133ddb0d382e57af0
--- /dev/null
+++ b/Pystan/flake.lock
@@ -0,0 +1,25 @@
+{
+ "nodes": {
+ "nixpkgs": {
+ "locked": {
+ "lastModified": 1739736696,
+ "narHash": "sha256-zON2GNBkzsIyALlOCFiEBcIjI4w38GYOb+P+R4S8Jsw=",
+ "rev": "d74a2335ac9c133d6bbec9fc98d91a77f1604c1f",
+ "revCount": 754461,
+ "type": "tarball",
+ "url": "https://api.flakehub.com/f/pinned/NixOS/nixpkgs/0.1.754461%2Brev-d74a2335ac9c133d6bbec9fc98d91a77f1604c1f/01951426-5a87-7b75-8413-1a0d9ec5ff04/source.tar.gz"
+ },
+ "original": {
+ "type": "tarball",
+ "url": "https://flakehub.com/f/NixOS/nixpkgs/0.1.%2A.tar.gz"
+ }
+ },
+ "root": {
+ "inputs": {
+ "nixpkgs": "nixpkgs"
+ }
+ }
+ },
+ "root": "root",
+ "version": 7
+}
diff --git a/Pystan/flake.nix b/Pystan/flake.nix
new file mode 100644
index 0000000000000000000000000000000000000000..e4ad2916d3f801928b7621cbc12a1a99fad9c79a
--- /dev/null
+++ b/Pystan/flake.nix
@@ -0,0 +1,26 @@
+{
+ description = "A Nix-flake-based Python development environment";
+
+ inputs.nixpkgs.url = "https://flakehub.com/f/NixOS/nixpkgs/0.1.*.tar.gz";
+
+ outputs = { self, nixpkgs }:
+ let
+ supportedSystems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ];
+ forEachSupportedSystem = f: nixpkgs.lib.genAttrs supportedSystems (system: f {
+ pkgs = import nixpkgs { inherit system; };
+ });
+ in
+ {
+ devShells = forEachSupportedSystem ({ pkgs }: {
+ default = pkgs.mkShell {
+ venvDir = ".venv";
+ packages = with pkgs; [ python312 ] ++
+ (with pkgs.python312Packages; [
+ pip
+ venvShellHook
+ basedpyright
+ ]);
+ };
+ });
+ };
+}
diff --git a/Pystan/tp.md b/Pystan/tp.md
new file mode 100644
index 0000000000000000000000000000000000000000..44dac1c51d659714556557ac49fde9c553a76072
--- /dev/null
+++ b/Pystan/tp.md
@@ -0,0 +1,113 @@
+# Analyse Statique de Programmes -- TP Analyse Statique
+
+CentraleSupélec
+
+Enseignant: Virgile Prevosto
+
+## Préliminaires
+
+Ce TP utilise exclusivement Python. On pourra utiliser l'image Docker, comme
+au TP précédent, ou directement sa machine si Python y est installé.
+
+### Rappel Docker
+L'image est ici: https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl et peut être utilisée soit localement, soit depuis `MyDocker`. De plus le répertoire `config` est monté automatiquement dans le container docker si vous utilisez les scripts associé ([PowerShell](https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl/blob/main/start-3asl.ps1) pour Windows ou [sh](https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl/blob/main/start-3asl.sh) pour Linux/macOS/BSD). Ces scripts devraient automatiquement ouvrir un onglet de votre navigateur web avec une session IceWM. Si ce n'est pas le cas, vous pouvez le faire manuellement: http://localhost:3000
+
+NB: l'interpréteur Python est `python3` et non `python`.
+
+### Typage statique
+Les fichiers proposés ont des annotations de types permettant de vérifier que
+les programmes sont bien typés avant de les exécuter. On pourra utiliser
+l'outil [`pyright`](https://microsoft.github.io/pyright/#/) pour la vérification. Il n'est pas présent sur l'image
+Docker, mais peut s'installer via les commandes suivantes:
+```sh
+sudo apt update
+sudo apt install pipx
+sudo apt install pyright
+```
+
+Il dispose également d'un plugin vscode.
+
+## Introduction
+
+Le fichier [syntax.py](config/syntax.py) définit les différentes classes
+syntaxique du langage While vu en cours, soit les expressions arithmétiques,
+les expressions booléennes et les instructions.
+
+## Sémantique opérationnelle
+Le fichier [opsem.py](config/opsem.py) donne un squelette des fonctions Ã
+écrire pour définir un interpréteur concret du langage While. Les fonctions
+`eval_aexpr`, et `eval_bexpr` permettent d'évaluer respectivement une
+expression arithmétique et une expression booléenne dans un environnement
+qui associe à des noms de variable une valeur entière. En cas d'erreur
+dans l'évaluation d'une (sous-)expression, on renverra None. La fonction `eval_instr`, renvoie l'environnement final obtenu en évaluant dans un environnement initial une instruction donnée. Là encore, en cas d'erreur au cours de l'évaluation, on renvoie `None`.
+
+Compléter ces définitions, et tester le résultat à l'aide du fichier
+[example_opsem.py](config/example_opsem.py), qui définit le programme de calcul de la factorielle,
+et l'évalue pour `x = 4`.
+
+## Calcul de point fixe
+
+Le fichier [cfg.py](config/cfg.py) est donné. Il contient la définition des
+différents labels des arêtes du graphe de flot de contrôle (skip, affectation,
+test, et erreur). On a aussi une classe pour les nœuds, pour un graphe, et pour
+un CFG proprement dit, qui ajoute au graphe les informations sur le nœud
+initial, le nœud final, et le nœud d'erreur. Un CFG est construit à partir d'un
+programme, et cette construction est donnée également.
+
+Le fichier [iteration.py](config/iteration.py) contient une classe abstraite
+`Transfer` qui permet d'implémenter des analyses statiques en donnant l'élément
+`bottom` du treillis, l'état initial, le `join` de deux états, le test
+d'inclusion, et les fonctions de transfert pour chaque étiquette.
+
+Compléter la fonction `fixpoint_iteration` de ce fichier, qui prend en argument
+une instance de `Transfer` et un CFG, et calcule le point fixe associant Ã
+chaque nœud du CFG l'état correspondant. L'algorithme est le suivant (on ne se
+préoccupe pas de terminaison):
+
+1. le mapping initial associe l'état initial au nœud initial, et `bottom` à tous
+ les autres. On met toutes les arêtes qui partent du nœud initial dans la
+ worklist.
+2. tant que la worklist n'est pas vide, on prend son premier élément, une arête
+qui va du nœud `src` au nœud `dst` avec le label `l`.
+3. on associe au nœud `dst` le `join` de son état actuel avec le résultat
+de la fonction de transfert pour `l` appliqué à l'état associé à `src`
+4. si le nouvel état est inclus dans l'état associé précédemment à `dst`, on
+ne fait rien. Sinon, on ajoute les arêtes qui sortent de `dst` à la worklist
+5. on revient en 2
+
+NB: en pratique, une itération efficace sélectionne l'arête d'intérêt de manière
+beaucoup plus précise, mais cela sort du cadre de ce TP.
+
+Tester le résultat avec le fichier
+[example_iteration.py](config/example_iteration.py), qui définit une analyse
+statique minimaliste, qui propage un état non vide dans tous les nœuds sauf ceux
+qui sont gardés par une condition qui s'évalue à `False` dans un environnement
+vide. Le programme exemple a un CFG qui contient de telles arêtes. À quoi
+correspondent les nœuds indiqués comme inatteignables par l'analyse?
+
+## Propagation de constantes
+
+Le fichier [constant_propagation.py](config/constant_propagation.py) vise Ã
+implémenter la propagation de constantes dans le cadre défini précédemment.
+Pour cela, on donne un type de valeurs abstraites qui sont soit un entier (quand
+on est sûr qu'une variable est associé à cet entier), soit `None`, pour indiquer
+que plusieurs valeurs sont possibles. Un environnement abstrait associe à des
+variables des valeurs abstraites, et notre état sera un environnement abstrait
+ou `None` pour indiquer que le nœud associé n'est jamais atteint. On donne
+également les fonctions d'évaluation abstraite des expressions, dans un
+environnement abstrait et qui renvoient une valeur abstraite ou `None` si une
+erreur se produit.
+
+Implémenter les différentes méthodes de la classe `Constant_propagation`. On
+définira un état initial où toutes les variables utilisées dans le programme
+sont associées à la valeur `abstract_value(None)`, indiquant qu'elles sont
+présentes dans l'environnement mais peuvent avoir n'importe quelle valeur.
+
+On testera le résultat à l'aide du fichier
+[example_constant_propagation.py](config/example_constant_propagation.py), qui
+définit un programme dont les variables reçoivent des valeurs constantes. NB:
+pour que l'analyseur arrive à montrer que `c` est constante en fin de programme,
+il faut raffiner la fonction de transfert du `test`, en réduisant l'état propagé
+quand le test est une égalité entre une variable et une expression qui s'évalue
+Ã une constante, pour tenir compte du fait que dans la branche correspondante,
+la variable est associée à une constante. Ce raffinement est facultatif.