summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 16:13:31 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 16:13:31 +0200
commit73fa920959d22c084265fe847f4788564bf49700 (patch)
tree9e99d91203b475ebe74fa0b484a86ada05caacf1
parentbcde99fbe99174a094f38fdda70ad69d65a423f4 (diff)
downloadSemVerif-Projet-73fa920959d22c084265fe847f4788564bf49700.tar.gz
SemVerif-Projet-73fa920959d22c084265fe847f4788564bf49700.zip
Achieve nothing.
-rw-r--r--Makefile6
-rw-r--r--abstract/constant_domain.ml155
-rw-r--r--abstract/domain.ml7
-rw-r--r--doc/TP1.html185
-rw-r--r--doc/TP1_files/main.js126
-rw-r--r--doc/TP1_files/preferred.css23
-rw-r--r--doc/enonce.html170
-rw-r--r--doc/enonce_files/main.js126
-rw-r--r--doc/enonce_files/preferred.css23
-rw-r--r--libs/util.ml8
-rw-r--r--main.ml11
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 () =