.envrc

+use flake

.gitignore

+### 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/

Pystan/.envrc

+use flake

Pystan/config/.gitignore

+### 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/
+
+

Pystan/config/cfg.py

+"""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

Pystan/config/constant_propagation.py

+"""
+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

Pystan/config/example_constant_propagation.py

+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}")

Pystan/config/example_interval.py

+from interval_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)

Pystan/config/example_interval_eval_exp.py

+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({})

Pystan/config/example_interval_reduce.py

+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) })

Pystan/config/example_iteration.py

+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")

Pystan/config/example_opsem.py

+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}")

Pystan/config/example_sign.py

+from sign_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)

Pystan/config/example_sign_eval_exp.py

+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({})

Pystan/config/example_sign_reduce.py

+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 })
+

Pystan/config/example_widen.py

+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}')

Pystan/config/interval_analysis.py

+# 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}")

Pystan/config/iteration.py

+"""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

Pystan/config/opsem.py

+"""
+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

Pystan/config/pyrightconfig.json

+{
+	"typeCheckingMode" : "standard"
+}