Merge branch anastat-frama-c-24-25:main into main

.gitignore

+/config/desktop-background.png
+/config/ssl
+/config/.*
+*/config/desktop-background.png
+*/config/ssl
+*/config/.*

Cours/README.md

+Ce répertoire contient les transparents des cours passés,
+ainsi que les exemples Frama-C/Eva présentés dans le cours 1,
+dans le sous-répertoire config, ce qui permet de les avoir
+automatiquement dans l'image Docker du cours
+(voir  https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl
+pour plus d'information).
+Chaque exemple contient dans un commentaire la ligne
+de commande Frama-C qui permet de faire l'analyse avec
+le niveau de précision voulue.

Cours/config/01-numeric.c

+/* frama-c -eva -main f 01-numeric.c */
+int x, y, t, m;
+double d;
+extern char z;
+char z1;
+
+void f(int c) {
+  if (c) x = 40;
+  for (int i = 0; i <= 40; i++) {
+    Frama_C_show_each_loop(i,y);
+    if (c == i) y = i;
+  }
+  z1 = z;
+  t = z;
+  m = 3;
+  for (int i = 3; i <= 40; i += 4) {
+    if (c == i) m = i;
+  }
+  if (c) {
+    d = 0.25;
+  } else {
+    d = 3.125;
+  }
+}

Cours/config/02-address.c

+/* frama-c -eva -main f 02-address.c */
+#include <stdlib.h>
+extern int* a;
+int *x;
+const char *y;
+int *z;
+int *t;
+int *u;
+
+int p[3];
+const char *string = "foobar";
+
+void f(int c) {
+  if (c) {
+    x = &p[1];
+  } else {
+    x = &p[2];
+  }
+
+  y = string;
+
+  z = (int *)1024;
+
+  t = (int *)((unsigned long)a | 4096);
+
+  u = malloc(sizeof(*u));
+}

Cours/config/03-address_written.c

+/* frama-c -eva 03-address_written.c */
+int X, Y;
+
+int *p;
+
+void f(int c) {
+  int x, y;
+  if (c <= 0) x = 2;
+L:
+  if (c <= 0) y = x + 1;
+  p = c ? &X : &x;
+}
+
+int main(int c) {
+  f(c);
+}

Cours/config/04-cast.c

+/* frama-c -eva -main f 04-cast.c */
+typedef struct {
+  int *monpointeur;
+  short monshort;
+} t;
+void f(int c) {
+  int x = 3;
+  if (c) x = 24;
+  t S = {&x, 12};
+  char *p = (char *)&S;
+  p[2] = 4;
+}

Cours/config/05-domains.c

+/* frama-c -eva 05-domains.c
+   frama-c -eva -eva-domains symbolic-locations,octagon 05-domains.c
+*/
+#include "__fc_builtin.h"
+
+int main () {
+  int x, y;
+  int *p = Frama_C_nondet_ptr(&x,&y);
+  *p = 3;
+  int z = (*p)++;
+  y = Frama_C_interval(0,10);
+  x = y;
+  z = x - y;
+}

Cours/config/06-simple.c

+/* frama-c -eva 06-simple.c */
+int S = 0;
+int T[5];
+int main(void) {
+  int i;
+  int *p = &T[0];
+  /*@ loop unroll 6; */
+  for (i = 0; i < 5; i++) {
+    S = S + i;
+    *p++ = S;
+  }
+  return S;
+}

Cours/config/07-slevel.c

+/* frama-c -eva -eva-slevel 3 07-slevel.c */
+int x, y;
+
+void main(int c) {
+  //@ assert c<=0 || c > 0;
+  if (c) {
+    x = 10;
+  } else {
+    x = 33;
+  }
+  Frama_C_show_each(c);
+  if (!c) {
+    x++;
+  } else {
+    x--;
+  }
+
+  if (c <= 0) {
+    y = 42;
+  } else {
+    y = 36;
+  }
+  if (c > 0) {
+    y++;
+  } else {
+    y--;
+  }
+}

Cours/config/08-split.c

+/* frama-c -eva -eva-slevel 2 -eva-split-return-function f:0 08-split.c */
+extern int c;
+
+int f(int *p) {
+  //@ split c <= 0;
+  if (c <= 0) {
+    *p = 10;
+    return 0;
+  }
+  return -1;
+}
+
+int main() {
+  int x;
+  int res = f(&x);
+  if (!res)
+    x++;
+  else
+    x = 0;
+}

Cours/config/09-context.c

+/* frama-c -eva -eva-context-width 4 -main search 09-context.c */
+int search(char *a, char key) {
+  char *orig = a;
+  while (*a) {
+    if (*a == key) return a - orig;
+    a++;
+  }
+  return -1;
+}

Cours/config/10-context-driver.c

+/* frama-c -eva -eva-precision 3 09-context.c 10-context-driver.c -main driver */
+#include "__fc_builtin.h"
+#include "limits.h"
+
+int search(char *a, char key);
+
+extern char buffer[1024];
+
+int driver() {
+  buffer[1023] = 0;
+  char key = Frama_C_interval(CHAR_MIN, CHAR_MAX);
+  return search(buffer, key);
+}

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_id: 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:
+        ...
+    def init_state(self) -> state:
+        ...
+    def join(self,s1:state,s2:state) -> state:
+        ...
+
+    def included(self,s1: state,s2: state) -> bool:
+        ...
+
+    def tr_skip(self,s: state) -> state:
+        ...
+
+    def tr_set(self,s: state,v: str,e: ArithExpr) -> state:
+        ...
+
+    def tr_test(self,s: state,c: BoolExpr) -> state:
+        ...
+
+    def tr_err(self,s: state,e: Expr) -> state:
+        ...

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_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/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
+ 
+   output maps each node to the computed state
+    """
+    raise NotImplementedError