diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | abstract/constant_domain.ml | 155 | ||||
| -rw-r--r-- | abstract/domain.ml | 7 | ||||
| -rw-r--r-- | doc/TP1.html | 185 | ||||
| -rw-r--r-- | doc/TP1_files/main.js | 126 | ||||
| -rw-r--r-- | doc/TP1_files/preferred.css | 23 | ||||
| -rw-r--r-- | doc/enonce.html | 170 | ||||
| -rw-r--r-- | doc/enonce_files/main.js | 126 | ||||
| -rw-r--r-- | doc/enonce_files/preferred.css | 23 | ||||
| -rw-r--r-- | libs/util.ml | 8 | ||||
| -rw-r--r-- | main.ml | 11 |
11 files changed, 825 insertions, 15 deletions
@@ -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>&&</tt> (and), <tt>||</tt> (or), <tt>!</tt> (negation); integer comparisons <tt><</tt>, <tt><=</tt>, <tt>></tt>, <tt>>=</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 -> expr ext -> 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 -> stat ext -> 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 -> expr ext -> 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 -> expr ext -> 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 -> 'a) -> 'a -> '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><</tt>, <tt>></tt>, <tt><=</tt>, <tt>>=</tt>) and boolean operators (<tt>&&</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 @@ -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 () = |