Semantics and application to program verification, École normale supérieure, 2013-2014

+ +

TP1 - Denotational semantics

+ +

+The goal of this session is to program an interpreter to compute the denotational semantics of a simple language. +We will use OCaml. + + +

Language

+ +

+Start by downloading the package: codeV1.tgz. + +

+The package contains a parser for the language, programmed in OCamlLex and Menhir (lexer.mll and parser.mly). +The parser outputs an abstract syntax tree defined in abstract_syntax_tree.ml. +A pretty-printer, to print back an abstract syntax tree into the original language, is provided in abstract_syntax_printer.ml. +In main.ml, you will find a simple driver that takes a file name passed as argument, parses it, and prints it back. +Just typing make should compile the simple driver. + +

Syntax

+The language is a very simple "curly brackets" C-like language. +A program is composed of a sequence of statements of the form: +

assignment: var = expr; +
tests: if (expr) stat-1; or if (expr) stat-1; else stat-2; +
while loops: while (expr) stat; +
blocks in curly brackets { stat-1; ... stat-n; } +

+non-standard statements include: +

assertions of boolean expressions: assert (expr); +
variable printing: print (var-1,...,var-n); +
failure: halt; which stops the program immediately +

+ +

+Expressions include: integer arithmetic operators: +, -, *, /, % (modulo); boolean operators: && (and), || (or), ! (negation); integer comparisons <, <=, >, >=. +Equality == and disequality != can be used to compare either two integers or two boolean values. +Constants include integers, and the boolean constants true and false. +Finally, rand(l,h) denotes the non-deterministic interval of integers between the constant l and the constant h. +You can use /* ... */ and // comments. +You can use parentheses and the operators have their usual precedence. + +

+Unlike C, 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). + +

Semantics

+ +

+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 halt statement. + + +

Deterministic semantics

+ +

+We first consider the deterministic subset of the language, i.e., we ignore the AST_int_rand expression node for now. + +

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

+You can use the following steps: +

Define a type ival 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 ZArith OCaml library (its API is similar to that of Int32 and Int64; the module is called Z). +
Define a type env for environments. You can use the Map + functor from the standard OCaml library to represent mappings from +variables to (non-erroneous) values. In addition to such mappings, an env object can also represent an error. The initial environment is an empty map (no variable). +
Write an expression evaluation function eval_expr: env -> expr ext -> ival by induction on the syntax of expressions. +It returns an error if its env 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! +
Write a statement evaluation function eval_stat: env -> stat ext -> env. +When should the function return an error environment? +
+Test your interpreter on the programs from the examples directory. +Can you detect infinite loops in loop.c, loop2.c, and loop3.c? +Under which condition does your interpreter terminate? +

+ +

+new: correction available in interp_det.ml. +(The correction uses abstract syntax trees from the extended language in codeV1x.tgz) + +

Non-deterministic semantics

+ +

+We now consider the full language including the non-deterministic expression node rand(l,h). + +

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

+The structure of the interpreter will be similar to the one in the previous question. +You can use the following steps: +

Define a type ivalset to represent sets of values ival (including errors). +You can use OCaml's standard Set functor. +
Define a type envset to represent sets of environments (including errors). +
Program a function eval_expr: env -> expr ext -> ivalset + 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 + fold. +Binary nodes require nested fold. +
Program a filter function filter: envset -> expr ext -> envset that returns the subset of its envset 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! +
Program a generic fixpoint operator fix: ('a -> 'a) -> 'a -> 'a that iterates a function from a base element to reach a fixpoint. +Use it then in the semantics of loops. +
+Test your interpreter on the examples directory, including non-deterministic programs such as gcd_nd.c and loop4.c. +

+ +

+new: correction available in interp_ndet.ml. +(The correction uses abstract syntax trees from the extended language in codeV1x.tgz) + + + +

Extensions

+ +

+You will find in codeV1x.tgz + an extension of the language with the following additional constructs: +variable declarations (global and local), procedures and functions, break and return statements, labels and goto + 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. + +

+

+
+

+Author: Antoine Miné +

+ + +

Semantics and application to program verification

TP1 - Denotational semantics

Language

Syntax

Semantics

Deterministic semantics

Non-deterministic semantics

Extensions

Semantics and application to program verification

Project

Result

Required features

Input language

Analysis

Output

Tests

Extensions

Resources

Files

Documentation