Achieve nothing.

11 files changed, 825 insertions, 15 deletions

diff --git a/Makefile b/Makefile
index 640da3b..0f09d87 100644
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,12 @@
 .PHONY: clean
 
 BIN=analyze
-SRCDIRS=libs,frontend
+SRCDIRS=libs,frontend,abstract
 
 all: $(BIN)
 
-$(BIN): main.ml
-	ocamlbuild -Is $(SRCDIRS) main.native
+$(BIN): main.ml abstract/domain.ml abstract/constant_domain.ml
+	ocamlbuild -Is $(SRCDIRS) -cflags '-I /usr/lib/ocaml/zarith' -lflags '-I /usr/lib/ocaml/zarith zarith.cmxa' main.native
 	mv main.native $(BIN)
 
 clean:
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index 8444779..544d2e9 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -1,18 +1,153 @@
+open Util
+open Abstract_syntax_tree
 
-
-module Make : Domain.s =
+module CD : Domain.S =
   struct
 
+    exception DivideByZero
+    exception TypeError
+    exception Bot
+    exception NotImplemented
 
-    type tv =
-      | Bot
-      | BTrue
-      | BFalse
-      | BTop
-      | I of Z.t
-      | ITop
+    type tv =   (* type for a variable *)
       | Top
+      | I of Z.t
+
+    type ts =   (* type for an environment *)
+      | Bot
+      | Nb of tv VarMap.t
+
+    let top_ts = Nb VarMap.empty
 
-    type ts = tv VarMap.t
+    let ts_union a b =
+      begin match a, b with
+      | Bot, Bot -> Bot
+      | Nb a, Bot -> Nb a
+      | Bot, Nb b -> Nb b
+      | Nb a, Nb b ->
+        Nb
+          (VarMap.fold
+            (fun var value a ->
+              try match VarMap.find var a with
+                | Top -> a
+                | I x ->
+                  match value with
+                  | I y when y = x -> a
+                  | _ -> VarMap.add var Top a
+              with
+              | Not_found -> VarMap.add var value a)
+          b a)
+      end
+
+    (* must not raise exception *)
+    let ts_add_bool_constraint expr (s : ts) =
+      s (* TODO, not necessary... *)
+
+
+    (* only evaluates numerical statements, raises
+      TypeError when result is bool *)
+    let rec eval_abs expr (s : tv VarMap.t) =
+      match expr with
+      | AST_unary(op, (i, _)) ->
+        begin match eval_abs i s with
+        | Top -> Top
+        | I x ->
+          match op with
+          | AST_UNARY_PLUS -> I x
+          | AST_UNARY_MINUS -> I (Z.neg x)
+          | _ -> raise TypeError
+        end
+      | AST_binary(op, (a, _), (b, _)) ->
+        begin match eval_abs a s, eval_abs b s with
+        | I x, I  y ->
+          begin match op with
+          | AST_PLUS -> I (Z.add x y)
+          | AST_MINUS -> I (Z.sub x y)
+          | AST_MULTIPLY -> I (Z.mul x y)
+          | AST_DIVIDE ->
+            if y = Z.zero then raise DivideByZero;
+            I (Z.div x y)
+          | AST_MODULO ->
+            if y = Z.zero then raise DivideByZero;
+            I (Z.rem x y)
+          | _ -> raise TypeError
+          end
+        | _ -> Top
+        end
+      | AST_identifier(id, _) ->
+        begin
+          try VarMap.find id s
+          with _ -> Top
+        end 
+      | AST_int_const(s, _) ->
+        I (Z.of_string s)
+      | AST_bool_const(_) -> raise TypeError
+      | AST_int_rand _ -> Top
+      | _ -> raise NotImplemented (* extensions *)
+
+    (* returns true if the expression can evaluate to true
+      returns false if the expression always evaluates to false *)
+    let rec eval_bool_abs expr (s : tv VarMap.t) =
+      true (* TODO *)
+
+    (* must not raise exception *)
+    let rec interp_abs stat s =
+      begin match s with
+      | Bot -> Bot
+      | Nb vars ->
+        begin match stat with
+        | AST_block b ->
+          List.fold_left
+            (fun ss (st, _) -> interp_abs st ss)
+            s b
+        | AST_assign ((id, _), (exp, _)) ->
+          begin
+            try
+              let value = eval_abs exp vars in
+              Nb (VarMap.add id value vars)
+            with _ -> Bot
+          end
+        | AST_if ((cond, _), (tb, _), None) ->
+          ts_union (Nb vars)
+            (interp_abs tb
+              (ts_add_bool_constraint cond (Nb vars)))
+        | AST_if ((cond, l), (tb, _), Some (eb, _)) ->
+          ts_union
+            (interp_abs tb
+              (ts_add_bool_constraint cond (Nb vars)))
+            (interp_abs eb
+              (ts_add_bool_constraint 
+                  (AST_unary (AST_NOT, (cond, l)))
+                (Nb vars)))
+        | AST_while ((cond, _), (body, _)) ->
+          let f s =
+            ts_union
+              s
+              (ts_add_bool_constraint cond s)
+          in
+            fix f (Nb vars)
+        | AST_HALT -> Bot
+        | AST_assert (cond, _) ->
+          if eval_bool_abs cond vars
+            then Nb vars
+            else begin
+              print_string "Assert fail\n";
+              Bot
+            end
+        | AST_print items ->
+          List.iter
+            (fun (var, _) ->
+              print_string (var ^ " = ");
+              try
+                match VarMap.find var vars with
+                | Top -> print_string "T\n"
+                | I x -> print_string (Z.to_string x ^ "\n")
+              with _ -> print_string "T\n")
+            items;
+          Nb vars
+        | _ -> raise NotImplemented (* extensions *)
+        end
+      end
 
   end
+
diff --git a/abstract/domain.ml b/abstract/domain.ml
index d022e34..643a6ec 100644
--- a/abstract/domain.ml
+++ b/abstract/domain.ml
@@ -1,7 +1,14 @@
+open Abstract_syntax_tree
 
 module type S =
   sig
     type tv
     type ts
+
+    val top_ts : ts
+
+    val interp_abs : stat -> ts -> ts
     
   end
+
+
diff --git a/doc/TP1.html b/doc/TP1.html
new file mode 100644
index 0000000..dfb8def
--- /dev/null
+++ b/doc/TP1.html
@@ -0,0 +1,185 @@
+<!-- -*- ispell-local-dictionary: "english" -*- -->
+<html><head>
+<title>Semantics and application to program verification, École normale supérieure, 2013-2014</title>
+<meta name="author" content="Antoine Mine">
+<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
+<link rel="Stylesheet" title="Stylesheet" type="text/css" href="TP1_files/preferred.css">
+<script src="TP1_files/main.js" type="text/javascript"></script>
+</head>
+<body>
+
+<h1>Semantics and application to program verification</h1>
+
+<div id="main">
+
+<h2>TP1 - Denotational semantics</h2>
+
+<p>
+The goal of this session is to program an interpreter to compute the denotational semantics of a simple language.
+We will use OCaml.
+
+
+</p><h3>Language</h3>
+
+<p>
+Start by downloading the package: <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1.tgz">codeV1.tgz</a>.
+
+</p><p>
+The package contains a parser for the language, programmed in OCamlLex and Menhir (<tt>lexer.mll</tt> and <tt>parser.mly</tt>).
+The parser outputs an abstract syntax tree defined in <tt>abstract_syntax_tree.ml</tt>.
+A pretty-printer, to print back an abstract syntax tree into the original language, is provided in <tt>abstract_syntax_printer.ml</tt>.
+In <tt>main.ml</tt>, you will find a simple driver that takes a file name passed as argument, parses it, and prints it back.
+Just typing <tt>make</tt> should compile the simple driver.
+
+</p><h4><a name="syntax">Syntax</a></h4>
+<p>
+The language is a very simple "curly brackets" <tt>C</tt>-like language.
+A program is composed of a sequence of statements of the form:
+</p><ul>
+<li> assignment: <tt>var = expr;</tt>
+</li><li> tests: <tt>if (expr) stat-1;</tt> or <tt>if (expr) stat-1; else stat-2;</tt>
+</li><li> while loops: <tt>while (expr) stat;</tt>
+</li><li> blocks in curly brackets <tt>{ stat-1; ... stat-n; }</tt>
+</li></ul>
+<p>
+non-standard statements include:
+</p><ul>
+<li> assertions of boolean expressions: <tt>assert (expr);</tt>
+</li><li> variable printing: <tt>print (var-1,...,var-n);</tt>
+</li><li> failure: <tt>halt;</tt> which stops the program immediately
+</li></ul>
+
+<p>
+Expressions include: integer arithmetic operators: <tt>+</tt>, <tt>-</tt>, <tt>*</tt>, <tt>/</tt>, <tt>%</tt> (modulo); boolean operators: <tt>&amp;&amp;</tt> (and), <tt>||</tt> (or), <tt>!</tt> (negation); integer comparisons <tt>&lt;</tt>, <tt>&lt;=</tt>, <tt>&gt;</tt>, <tt>&gt;=</tt>.
+Equality <tt>==</tt> and disequality <tt>!=</tt> can be used to compare either two integers or two boolean values.
+Constants include integers, and the boolean constants <tt>true</tt> and <tt>false</tt>.
+Finally, <tt>rand(l,h)</tt> denotes the non-deterministic interval of integers between the constant <tt>l</tt> and the constant <tt>h</tt>.
+You can use <tt>/* ... */</tt> and <tt>//</tt> comments.
+You can use parentheses and the operators have their usual precedence.
+
+</p><p>
+Unlike <tt>C</tt>, variables do not need to be declared; they start existing when first assigned a value.
+There are no local variables nor functions (see the extension part).
+
+</p><h4>Semantics</h4>
+
+<p>
+Variables have no type and can hold either an integer or a boolean 
+value.
+Subsequently, we do not distinguish statically between boolean and 
+integer expressions: only values have a type.
+It is an error to use operators with values of the wrong type, such as 
+adding two boolean values.
+This is detected at run-time, when evaluating the expression in the 
+current environment.
+Other run-time errors include: divisions and modulos by zero; using a 
+non-boolean value in tests, loops and assert conditions;  using a 
+variable that has never been assigned to; asserting a condition that is 
+false; executing the <tt>halt</tt> statement.
+
+
+</p><h3>Deterministic semantics</h3>
+
+<p>
+We first consider the deterministic subset of the language, i.e., we ignore the <tt>AST_int_rand</tt> expression node for now.
+
+</p><p>
+<b>Write an interpreter that executes the program by induction on the 
+syntax of statements and expressions; it returns either an environment 
+mapping variables to values, or an error.</b>
+
+</p><p>
+You can use the following steps:
+</p><ol>
+<li> Define a type <tt>ival</tt> for values. It should contain integers,
+ booleans and errors.
+You can use a string representation for errors, which will give the user
+ some information on the location and cause of the error.
+To avoid possible overflow in arithmetic, you can use the <tt>ZArith</tt> OCaml library (its API is similar to that of <tt>Int32</tt> and <tt>Int64</tt>; the module is called <tt>Z</tt>).
+</li><li> Define a type <tt>env</tt> for environments. You can use the <tt>Map</tt>
+ functor from the standard OCaml library to represent mappings from 
+variables to (non-erroneous) values. In addition to such mappings, an <tt>env</tt> object can also represent an error. The initial environment is an empty map (no variable).
+</li><li> Write an expression evaluation function <tt>eval_expr: env -&gt; expr ext -&gt; ival</tt> by induction on the syntax of expressions.
+It returns an error if its <tt>env</tt> argument is an error 
+(strictness) or if an error is detected in the expression evaluation, 
+which then percolates to the expression root. 
+Avoid using OCaml exceptions to propagate errors in the function: it 
+will only make the construction of the non-deterministic version more 
+painful!
+</li><li> Write a statement evaluation function <tt>eval_stat: env -&gt; stat ext -&gt; env</tt>.
+When should the function return an error environment?
+</li><li>
+Test your interpreter on the programs from the <tt>examples</tt> directory.
+Can you detect infinite loops in <tt>loop.c</tt>, <tt>loop2.c</tt>, and <tt>loop3.c</tt>?
+Under which condition does your interpreter terminate?
+</li></ol>
+
+<p class="framed">
+<b>new</b>: correction available in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/correction/interp_det.ml">interp_det.ml</a>. 
+(The correction uses abstract syntax trees from the extended language in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a>)
+
+</p><h3>Non-deterministic semantics</h3>
+
+<p>
+We now consider the full language including the non-deterministic expression node <tt>rand(l,h)</tt>.
+
+</p><p>
+<b>Write an interpreter for this language that outputs the set of all 
+possible environments at the end of the program as well as the set of 
+all errors that can be encountered.</b>
+
+</p><p>
+The structure of the interpreter will be similar to the one in the previous question.
+You can use the following steps:
+</p><ol>
+<li> Define a type <tt>ivalset</tt> to represent sets of values <tt>ival</tt> (including errors). 
+You can use OCaml's standard <tt>Set</tt> functor.
+</li><li> Define a type <tt>envset</tt> to represent sets of environments (including errors).
+</li><li> Program a function <tt>eval_expr: env -&gt; expr ext -&gt; ivalset</tt>
+ to evaluate an expression in a single environment and return the set of
+ its possible values in the environment.
+When encountering a unary node, the operator must be applied to each 
+possible value of its argument expression; you can use iterators such as
+ <tt>fold</tt>.
+Binary nodes require nested <tt>fold</tt>.
+</li><li> Program a filter function <tt>filter: envset -&gt; expr ext -&gt; envset</tt> that returns the subset of its <tt>envset</tt> argument that can satisfy the expression, enriched with the errors encountered during the expression evaluation.
+This function will be useful to model loops, tests and assertions.
+Remember that an environment can satisfy both an expression and its negation!
+</li><li> Program a generic fixpoint operator <tt>fix: ('a -&gt; 'a) -&gt; 'a -&gt; 'a</tt> that iterates a function from a base element to reach a fixpoint.
+Use it then in the semantics of loops.
+</li><li>
+Test your interpreter on the <tt>examples</tt> directory, including non-deterministic programs such as <tt>gcd_nd.c</tt> and <tt>loop4.c</tt>.
+</li></ol>
+
+<p class="framed">
+<b>new</b>: correction available in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/correction/interp_ndet.ml">interp_ndet.ml</a>. 
+(The correction uses abstract syntax trees from the extended language in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a>)
+
+
+
+</p><h3>Extensions</h3>
+
+<p>
+You will find in <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a>
+ an extension of the language with the following additional constructs: 
+variable declarations (global and local), procedures and functions, <tt>break</tt> and <tt>return</tt> statements, labels and <tt>goto</tt>
+ statements.
+The language is completely backward compatible with the simpler one.
+The abstract syntax tree also enriches the previous one with new kinds 
+of nodes, so that you can simply reuse your interpreter and extend it to
+ support some or all of the new constructs.
+
+<br><br>
+</p><hr>
+<br>
+<p>
+Author: <a href="http://www.di.ens.fr/%7Emine">Antoine Miné</a>
+<br><br>
+
+
+</p></div>
+
+
+
+
+</body></html>
\ No newline at end of file
diff --git a/doc/TP1_files/main.js b/doc/TP1_files/main.js
new file mode 100644
index 0000000..a1e13a0
--- /dev/null
+++ b/doc/TP1_files/main.js
@@ -0,0 +1,126 @@
+/*
+  Scripts for my professional web-site: http://www.di.ens.fr/~mine
+  Copyright (C) Antoine Miné 2011.
+ */
+
+
+/* main menu */
+var options = [
+    ["img",  "antoine_mini.png", "80%",   "" ],
+    ["Antoine Miné", "", "", "" ],
+    ["br"],
+    ["Home",         "Accueil",      "index", "" ],
+    ["News",         "Nouvelles",    "index", "#news" ],
+    ["Research",     "Recherche",    "index", "#research" ],
+    ["Habilitation", "Habilitation", "hdr/index", "", "" ],
+    ["Ph.D",         "Thèse",        "these/index", "" ],
+    ["Projects",     "Projets",      "projects", "" ],
+    ["Conferences",  "Conférences",  "confs", "", ],
+    ["Software",     "Logiciels",    "index", "#soft", ],
+    ["Publications", "Publications", "publications", "", "important" ],
+    ["Talks",        "Exposés",      "talks", "" ],
+    ["Teaching",     "Enseignement", "index", "#teach", ],
+    ["Emulation",    "Émulation",    "emulation", "" ],
+    ["Contact",      "Contact",      "index", "#contact" ],
+    ["-"],
+/*
+    ["SAS 2012",     "",   "http://www.sas2012.ens.fr", "", "important" ],
+    ["SSCPS 2012",   "",   "http://www.sscps.net", ""],
+    ["SAS 2013",     "",  "http://research.microsoft.com/en-us/events/sas2013/", ""],
+*/
+    ["iFM 2014",   "", "http://ifm2014.cs.unibo.it/", ""],
+    ["MOVEP 2014", "", "http://movep14.irccyn.ec-nantes.fr/", ""],
+    ["TAPAS 2014", "", "http://cs.au.dk/tapas2014", ""],
+    ["TASE 2014",  "", "http://www.nudt.edu.cn/tase2014", ""],
+    ["POPL 2015",  "", "http://popl.mpi-sws.org/2015/", ""],
+    ["-"],
+
+    ["MPRI 2-6 course (M2)",         "Cours MPRI 2-6 (M2)", "http://www.di.ens.fr/~mine/enseignement/mpri/2013-2014", ""],
+    ["Semantic course (L3)",         "Cours de sémantique (L3)", "http://www.di.ens.fr/~rival/semverif-2014/", ""],
+
+    ["-"],
+    ["AstréeA",      "",    "http://www.astreea.ens.fr", "", "important" ],
+    ["Astrée",       "",    "http://www.astree.ens.fr", "" ],
+    ["Apron",        "",    "http://apron.cri.ensmp.fr/library", "" ],
+    ["-"],
+    ["br"],
+    ["img", "logo-cnrs.png",  "64",  "http://www.cnrs.fr" ],
+    ["br"],
+    ["img", "logo-ens.png",   "82",  "http://www.ens.fr" ],
+    ["br"],
+    ["img", "logo-inria.png", "128",  "http://www.inria.fr" ],
+];
+
+function print_menu(base,here)
+{
+    for (var i=0; i<options.length; i++) {
+        if (options[i][0] == "-")
+            document.write("<div class=\"menuspace\"></div>\n");
+
+        else if (options[i][0] == "br")
+            document.write("<br>\n");
+
+        else if (options[i][0] == "img") {
+            document.write("<div class=\"icon\">");
+            if (options[i][3] != "")
+                document.write("<a href=\"" + options[i][3] + "\" class=\"noborder\">");
+            document.write("<img src=\"" + base + options[i][1] + "\" alt=\"[" + 
+                           options[i][1] + "]\" width=\"" + options[i][2] + "\">");
+            if (options[i][3] != "")
+                document.write("</a>");
+            document.write("</div>\n");
+        }
+
+        else {
+            document.write("<div class=\"menuitem\">");
+            var url = options[i][2];
+            if (url != "" && url.indexOf(".") == -1) url = url + ".html." + lang + options[i][3];
+            if (url != "" && url.indexOf(":") == -1) url = base + url;
+            if (options[i][0] == here || url=="") document.write("<b>");
+            else if (4 in options[i]) document.write("<a href=\"" + url + "\" class=\"" + options[i][4] + "\">");
+            else document.write("<a href=\"" + url + "\">");
+            document.write(options[i][ options[i][1]=="" || lang!="fr" ? 0 : 1]);
+            if (options[i][0] == here || url=="") document.write("</b>");
+            else document.write("</a>");
+            document.write("</div>\n");
+        }
+    }
+}
+
+function print_ref(s) 
+{ 
+    document.write("<a href=\"publications.html." + lang + "#" + s + "\">");
+    document.write("<span class=\"pref\">[" + s + "]</span>");
+    document.write("</a>");
+}
+
+function mailchar(m,i)
+{
+    var c = "";
+    switch (i) {
+    case 0: c = 'm'; break;
+    case 1: c = 'i'; break;
+    case 2: c = 'n'; break;
+    case 3: c = 'e'; break;
+    case 4: c = '@'; break;
+    case 5: c = 'd'; break;
+    case 6: c = 'i'; break;
+    case 7: c = '.'; break;
+    case 8: c = 'e'; break;
+    case 9: c = 'n'; break;
+    case 10: c = 's'; break;
+    case 11: c = '.'; break;
+    case 12: c = 'f'; break;
+    case 13: c = 'r'; break;
+    }
+    if (c != "") m.innerHTML = m.innerHTML + "<span>" + c + "</span>";
+    if (i<13) setTimeout(function () { mailchar(m,i+1); }, 100 + 100 * Math.random());
+}
+
+function main()
+{
+    var m = document.getElementsByName("mail");
+    for (var i=0; i<m.length; i++) {
+        mailchar(m[i],0);
+    }
+}
diff --git a/doc/TP1_files/preferred.css b/doc/TP1_files/preferred.css
new file mode 100644
index 0000000..346afa6
--- /dev/null
+++ b/doc/TP1_files/preferred.css
@@ -0,0 +1,23 @@
+body { background:#eee; text-align:justify; }
+#main { margin:0 auto 5em auto; max-width:60em; 
+        border-left:1px solid #aab; border-right:2px solid #aab; border-bottom:2px solid #aab; 
+        padding:1em 4em; background:white; }
+h1   { font-size: 200%; color: #ddf; background: #23e; 
+       text-align: center; padding-top: 0.5em; padding-bottom: 0.5em; margin-bottom:0; 
+       border-right:1px solid #228; border-bottom:1px solid #228; }
+h2   { font-size: 175%; color: #248; background: #bcf; padding:0.3em; }
+h3   { font-size: 125%; color: #162; margin-top: 2em; }
+h4   { font-size: 120%; color: #128; margin-left: 0.5em; }
+p    { margin-left: 3%; margin-right: 3%; }
+.code {  border: 1px solid black; background: #eef; padding: 0.3em; margin-left: 5%; margin-right: 10%; color: #e33; font-family: monospace;font-size: 110%; }
+ul { margin-top: -0.1em; margin-bottom: 0.1em; }
+li { margin-left: 3%; margin-top: 0.1em; margin-right: 6%; }
+tt { color: #e33; }
+.com { color: #234; };
+.warn { margin-left: 4%; margin-right: 4%; color: #f11; background: #fee; 
+        padding: 0.3em; border: 1px solid; }
+.note { margin-left: 4%; margin-right: 4%; color: #000; background: #eef; 
+        padding: 0.3em; border: 1px solid; }
+.ex { border: 1px solid black; background: #eef; padding: 0.3em; margin: 1em; }
+
+.framed { background:#ffa; padding: 1ex 1ex; border: 1px dashed #fa3;   }
\ No newline at end of file
diff --git a/doc/enonce.html b/doc/enonce.html
new file mode 100644
index 0000000..f9948e6
--- /dev/null
+++ b/doc/enonce.html
@@ -0,0 +1,170 @@
+<!-- -*- ispell-local-dictionary: "english" -*- -->
+<html><head>
+<title>Semantics and application to program verification, École normale supérieure, 2013-2014</title>
+<meta name="author" content="Antoine Mine">
+<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
+<link rel="Stylesheet" title="Stylesheet" type="text/css" href="enonce_files/preferred.css">
+<script src="enonce_files/main.js" type="text/javascript"></script>
+</head>
+<body>
+
+<h1>Semantics and application to program verification</h1>
+
+<div id="main">
+
+<h2>Project</h2>
+
+<p>
+The goal of the project is to write a simple static analyzer by abstract
+ interpretation in OCaml to discover automatically numeric invariants 
+about the variables of programs written in a simple programming 
+language.
+
+</p><p>
+The project is due on the day of the exam, on <b>May the 28th</b>.
+The project should be sent by email to the teachers.
+
+</p><h3>Result</h3>
+
+<p>
+For the project, you should deliver an archive that contains the following items:
+</p><ul>
+<li> the source code of the static analyzer, well-commented and complete with a Makefile;
+</li><li> a report of 4 pages or more that describes the language 
+features supported, the choices in semantics and implementation (if 
+any), the usage of the analyzer; it must also discuss the result of a 
+few analysis tests (we provide some <a href="#testing">tests</a> that you can use).
+</li></ul>
+
+
+<h3><a name="features">Required features</a></h3>
+
+<h4>Input language</h4>
+
+<p>
+The input language can be based on the language used in the lab session,
+ or you can design your own language with similar features.
+To get started, you can download the <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a> package (see the <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/denotational.html#syntax">first practical session</a> for an explanation of the syntax of the language).
+
+</p><p>
+More precisely, the language must feature at least:
+</p><ul>
+<li> blocks (nested sequences of instructions);
+</li><li> declarations of variables of integer type, with proper scoping with respect to blocks <span class="com">(to simplify, you can assume that all variable names are distinct)</span>;
+</li><li> assignments of integer expressions, with the standard arithmetic operators: <tt>+</tt>, <tt>-</tt>, <tt>*</tt> <span class="com">(and optionally division <tt>/</tt> and modulo <tt>%</tt>)</span>;
+</li><li> if-then-else instructions, using boolean expressions containing integer comparisons (<tt>==</tt>, <tt>!=</tt>, <tt>&lt;</tt>, <tt>&gt;</tt>, <tt>&lt;=</tt>, <tt>&gt;=</tt>) and boolean operators (<tt>&amp;&amp;</tt>, <tt>||</tt>, <tt>!</tt>) <span class="com">(support for boolean variables is not required)</span>;
+</li><li> while loops;
+</li><li> a non-deterministic operation, such as <tt>rand(l,h)</tt> in integer expressions;
+</li><li> an <tt>assert</tt> instruction, that checks the validity of a boolean expression;
+</li><li> a <tt>print</tt> instruction, that takes as argument a list of variables and prints their value.
+</li></ul>
+
+<p>
+<span class="com">(You are free to reject programs using other language 
+constructions, such as functions, non-integer variable declarations, 
+gotos, etc.)</span>
+
+</p><h4>Analysis</h4>
+
+<p>
+The analyzer should contain an iterator that analyzes the program 
+forwards, by induction on the abstract syntax tree.
+Loops can be unrolled a fixed number of times (e.g., 3 times), but you 
+should ultimately use iterations with widening in order to always 
+terminate for domains with infinite increasing chains.
+To increase the precision, the first few (e.g., 3) applications of the 
+widening may be replaced with a join.
+
+</p><p>
+The analysis should be parametric in the choice of a numeric abstract domain.
+At least the <b>three</b> following domains must be provided:
+</p><ul>
+<li> the <b>constant domain</b>, that you should implement yourself;
+</li><li> the <b>interval domain</b>, that you should also implement yourself;
+</li><li> the <b>polyhedra domain</b>, which calls the <a href="http://apron.cri.ensmp.fr/library/0.9.10/mlapronidl">Apron library</a> to perform the abstract operations <span class="com">(you are not asked to implement the polyhedra operators yourself)</span>.
+</li></ul>
+
+<p>
+Depending on the domain, at least the following kinds of expressions should be handled precisely:
+</p><ul>
+<li> in assignments: all arithmetic expressions for the constant and interval domains; affine expressions for polyhedra;
+</li><li> in the conditions of if-then-else and while instructions: for 
+polyhedra, boolean formulas whose atoms are affine constraints; for 
+constants and intervals, boolean formulas whose atoms are simple 
+comparisons between two variables or between a variable and a constant.
+</li></ul>
+
+<p>
+All the expressions allowed in the program syntax must be handled (no 
+"not implemented" exception); however, any expression not belonging to 
+the above categories may be handled in a coarse way (e.g., considering 
+assignments as non-deterministic and ignoring conditions).
+
+</p><h4>Output</h4>
+
+<p>
+The analysis should at least output a textual file containing:
+</p><ul>
+<li> a list of the assertions that cannot be proved to hold, and their location;
+</li><li> for each <tt>print</tt> instruction, the invariant found for the specified variables at the location of the instruction.
+</li></ul>
+
+<p>
+For debugging, it can be useful to implement a <i>trace mode</i> that outputs the abstract element computed at each step of the analysis.
+
+</p><h4><a name="testing">Tests</a></h4>
+
+<p>
+To help you test your analyzer, we provide a <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/tests.tgz">set of small test programs</a>,
+ written in the small language used in the practical sessions.
+We also provide the output of their analysis using our reference 
+analyzer, so that you can easily check the correctness and the precision
+ of your analyzer.
+
+</p><h3><a name="extensions">Extensions</a></h3>
+
+<p>
+In addition to the mandatory features described above, you may implement one or several extensions, such as for instance:
+</p><ul>
+<li> functions and function calls <span class="com">(without recursion)</span>;
+</li><li> checks for arithmetic overflows and divisions by zero errors in expressions;
+</li><li> other numeric abstract domains <span class="com">(such as non-relational integer congruences, or linear equalities)</span>;
+</li><li> several types of numeric variables <span class="com">(such as rationals or floating-point numbers, which are supported directly by Apron)</span>;
+</li><li> boolean variables <span class="com">(you can handle them as integer variables that can only take two values: 0 for false, and 1 for true)</span>;
+</li><li> arrays <span class="com">(each array can be abstracted by a single variable, and assignments result in weak updates);
+</span></li><li> non-local control-flow instructions, such as <tt>break</tt> and <tt>continue</tt> in loops, forward <tt>goto</tt>, or even arbitrary <tt>goto</tt>;
+</li><li> a backward analysis <span class="com">(find necessary conditions on the start of the program so that all assertions are satisfied)</span>;
+</li><li> a nicer presentation for the output of the analysis, such as a graphical visualisation of numeric invariants <span class="com">(particularly useful for polyhedra in 2D or 3D)</span>;
+</li><li> any extension of your choice.
+</li></ul>
+
+<h3><a name="doc">Resources</a></h3>
+
+<h4>Files</h4>
+<ul>
+<li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a>: language parser;
+</li><li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/tests.tgz">tests.tgz</a>: some programs to test your analyzer.
+</li></ul>
+
+<h4>Documentation</h4>
+<ul>
+<li> <a href="http://caml.inria.fr/pub/docs/manual-ocaml"><b>OCaml</b></a> programming language;
+</li><li> <a href="http://gallium.inria.fr/%7Efpottier/menhir"><b>Menhir</b></a> parser generator;
+</li><li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/doc-zarith"><b>ZArith</b></a> arbitrary precision number library;
+</li><li> <a href="http://apron.cri.ensmp.fr/library/0.9.10/mlapronidl"><b>Apron</b></a> abstract domain library;
+</li><li> <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/doc-mapext/index.html"><b>Mapext</b></a> maps with some additional useful functions (the source code is included in the <a href="http://www.di.ens.fr/%7Emine/enseignement/l3/codeV1x.tgz">codeV1x.tgz</a> bundle).
+</li></ul>
+
+<p>
+</p><hr>
+<br>
+<p>
+Author: <a href="http://www.di.ens.fr/%7Emine">Antoine Miné</a>
+<br><br>
+
+</p></div>
+
+
+
+
+</body></html>
\ No newline at end of file
diff --git a/doc/enonce_files/main.js b/doc/enonce_files/main.js
new file mode 100644
index 0000000..a1e13a0
--- /dev/null
+++ b/doc/enonce_files/main.js
@@ -0,0 +1,126 @@
+/*
+  Scripts for my professional web-site: http://www.di.ens.fr/~mine
+  Copyright (C) Antoine Miné 2011.
+ */
+
+
+/* main menu */
+var options = [
+    ["img",  "antoine_mini.png", "80%",   "" ],
+    ["Antoine Miné", "", "", "" ],
+    ["br"],
+    ["Home",         "Accueil",      "index", "" ],
+    ["News",         "Nouvelles",    "index", "#news" ],
+    ["Research",     "Recherche",    "index", "#research" ],
+    ["Habilitation", "Habilitation", "hdr/index", "", "" ],
+    ["Ph.D",         "Thèse",        "these/index", "" ],
+    ["Projects",     "Projets",      "projects", "" ],
+    ["Conferences",  "Conférences",  "confs", "", ],
+    ["Software",     "Logiciels",    "index", "#soft", ],
+    ["Publications", "Publications", "publications", "", "important" ],
+    ["Talks",        "Exposés",      "talks", "" ],
+    ["Teaching",     "Enseignement", "index", "#teach", ],
+    ["Emulation",    "Émulation",    "emulation", "" ],
+    ["Contact",      "Contact",      "index", "#contact" ],
+    ["-"],
+/*
+    ["SAS 2012",     "",   "http://www.sas2012.ens.fr", "", "important" ],
+    ["SSCPS 2012",   "",   "http://www.sscps.net", ""],
+    ["SAS 2013",     "",  "http://research.microsoft.com/en-us/events/sas2013/", ""],
+*/
+    ["iFM 2014",   "", "http://ifm2014.cs.unibo.it/", ""],
+    ["MOVEP 2014", "", "http://movep14.irccyn.ec-nantes.fr/", ""],
+    ["TAPAS 2014", "", "http://cs.au.dk/tapas2014", ""],
+    ["TASE 2014",  "", "http://www.nudt.edu.cn/tase2014", ""],
+    ["POPL 2015",  "", "http://popl.mpi-sws.org/2015/", ""],
+    ["-"],
+
+    ["MPRI 2-6 course (M2)",         "Cours MPRI 2-6 (M2)", "http://www.di.ens.fr/~mine/enseignement/mpri/2013-2014", ""],
+    ["Semantic course (L3)",         "Cours de sémantique (L3)", "http://www.di.ens.fr/~rival/semverif-2014/", ""],
+
+    ["-"],
+    ["AstréeA",      "",    "http://www.astreea.ens.fr", "", "important" ],
+    ["Astrée",       "",    "http://www.astree.ens.fr", "" ],
+    ["Apron",        "",    "http://apron.cri.ensmp.fr/library", "" ],
+    ["-"],
+    ["br"],
+    ["img", "logo-cnrs.png",  "64",  "http://www.cnrs.fr" ],
+    ["br"],
+    ["img", "logo-ens.png",   "82",  "http://www.ens.fr" ],
+    ["br"],
+    ["img", "logo-inria.png", "128",  "http://www.inria.fr" ],
+];
+
+function print_menu(base,here)
+{
+    for (var i=0; i<options.length; i++) {
+        if (options[i][0] == "-")
+            document.write("<div class=\"menuspace\"></div>\n");
+
+        else if (options[i][0] == "br")
+            document.write("<br>\n");
+
+        else if (options[i][0] == "img") {
+            document.write("<div class=\"icon\">");
+            if (options[i][3] != "")
+                document.write("<a href=\"" + options[i][3] + "\" class=\"noborder\">");
+            document.write("<img src=\"" + base + options[i][1] + "\" alt=\"[" + 
+                           options[i][1] + "]\" width=\"" + options[i][2] + "\">");
+            if (options[i][3] != "")
+                document.write("</a>");
+            document.write("</div>\n");
+        }
+
+        else {
+            document.write("<div class=\"menuitem\">");
+            var url = options[i][2];
+            if (url != "" && url.indexOf(".") == -1) url = url + ".html." + lang + options[i][3];
+            if (url != "" && url.indexOf(":") == -1) url = base + url;
+            if (options[i][0] == here || url=="") document.write("<b>");
+            else if (4 in options[i]) document.write("<a href=\"" + url + "\" class=\"" + options[i][4] + "\">");
+            else document.write("<a href=\"" + url + "\">");
+            document.write(options[i][ options[i][1]=="" || lang!="fr" ? 0 : 1]);
+            if (options[i][0] == here || url=="") document.write("</b>");
+            else document.write("</a>");
+            document.write("</div>\n");
+        }
+    }
+}
+
+function print_ref(s) 
+{ 
+    document.write("<a href=\"publications.html." + lang + "#" + s + "\">");
+    document.write("<span class=\"pref\">[" + s + "]</span>");
+    document.write("</a>");
+}
+
+function mailchar(m,i)
+{
+    var c = "";
+    switch (i) {
+    case 0: c = 'm'; break;
+    case 1: c = 'i'; break;
+    case 2: c = 'n'; break;
+    case 3: c = 'e'; break;
+    case 4: c = '@'; break;
+    case 5: c = 'd'; break;
+    case 6: c = 'i'; break;
+    case 7: c = '.'; break;
+    case 8: c = 'e'; break;
+    case 9: c = 'n'; break;
+    case 10: c = 's'; break;
+    case 11: c = '.'; break;
+    case 12: c = 'f'; break;
+    case 13: c = 'r'; break;
+    }
+    if (c != "") m.innerHTML = m.innerHTML + "<span>" + c + "</span>";
+    if (i<13) setTimeout(function () { mailchar(m,i+1); }, 100 + 100 * Math.random());
+}
+
+function main()
+{
+    var m = document.getElementsByName("mail");
+    for (var i=0; i<m.length; i++) {
+        mailchar(m[i],0);
+    }
+}
diff --git a/doc/enonce_files/preferred.css b/doc/enonce_files/preferred.css
new file mode 100644
index 0000000..346afa6
--- /dev/null
+++ b/doc/enonce_files/preferred.css
@@ -0,0 +1,23 @@
+body { background:#eee; text-align:justify; }
+#main { margin:0 auto 5em auto; max-width:60em; 
+        border-left:1px solid #aab; border-right:2px solid #aab; border-bottom:2px solid #aab; 
+        padding:1em 4em; background:white; }
+h1   { font-size: 200%; color: #ddf; background: #23e; 
+       text-align: center; padding-top: 0.5em; padding-bottom: 0.5em; margin-bottom:0; 
+       border-right:1px solid #228; border-bottom:1px solid #228; }
+h2   { font-size: 175%; color: #248; background: #bcf; padding:0.3em; }
+h3   { font-size: 125%; color: #162; margin-top: 2em; }
+h4   { font-size: 120%; color: #128; margin-left: 0.5em; }
+p    { margin-left: 3%; margin-right: 3%; }
+.code {  border: 1px solid black; background: #eef; padding: 0.3em; margin-left: 5%; margin-right: 10%; color: #e33; font-family: monospace;font-size: 110%; }
+ul { margin-top: -0.1em; margin-bottom: 0.1em; }
+li { margin-left: 3%; margin-top: 0.1em; margin-right: 6%; }
+tt { color: #e33; }
+.com { color: #234; };
+.warn { margin-left: 4%; margin-right: 4%; color: #f11; background: #fee; 
+        padding: 0.3em; border: 1px solid; }
+.note { margin-left: 4%; margin-right: 4%; color: #000; background: #eef; 
+        padding: 0.3em; border: 1px solid; }
+.ex { border: 1px solid black; background: #eef; padding: 0.3em; margin: 1em; }
+
+.framed { background:#ffa; padding: 1ex 1ex; border: 1px dashed #fa3;   }
\ No newline at end of file
diff --git a/libs/util.ml b/libs/util.ml
new file mode 100644
index 0000000..b2838b6
--- /dev/null
+++ b/libs/util.ml
@@ -0,0 +1,8 @@
+
+module VarMap = Mapext.Make(String)
+
+let rec fix f s =
+  let fs = f s in
+  if fs = s
+    then fs
+    else fix f fs
diff --git a/main.ml b/main.ml
index 2db911e..91ac4b1 100644
--- a/main.ml
+++ b/main.ml
@@ -11,12 +11,19 @@
   You should modify this file to call your functions instead!
 *)
 
+open Abstract_syntax_tree
+open Constant_domain
 
 (* parse and print filename *)
 let doit filename =
   let prog = File_parser.parse_file filename in
-  Abstract_syntax_printer.print_prog Format.std_formatter prog
-
+  Abstract_syntax_printer.print_prog Format.std_formatter prog;
+  List.fold_left
+    (fun s x -> match x with
+      | AST_stat(stat, _) -> CD.interp_abs(stat) s
+      | _ -> s)
+    CD.top_ts
+    (fst prog)
 
 (* parses arguments to get filename *)
 let main () =