Sufficient Condition Polyhedral Prototype Analyzer

Language Syntax

The toy language accepted by the analyzer has a C-inspired syntax.

Note that, before the analysis takes place, the program is simplified to ensure that there is at most one side-effect by statement. Implicit casts in expressions (to model integer promotion and usual arithmetic conversions) are also introduced explicitly. Finally, extra statements are generated to bind formal arguments and return values of functions.

In order to avoid straining the servers, the analysis is limited to small programs with few variables.

Types

The language features boolean and numeric types.

type ::= int-type | real-type | bool
int-type ::= int-length | unsigned int-length
int-length ::= char | short | int | long | integer
real-type ::= float | double | real

Integer types of different size are available: 8-bit char, 16-bit short, 32-bit int, and 64-bit long, and exist in signed and unsigned versions. However, bound checking is not implemented at the moment; the type only affects the initial range of variables. The type integer corresponds to unbounded integers.

Various types of reals are also available. Floating-point numbers can be 32-bit float or 64-bit double. Bound checking is not implemented at the moment, but rounding is handled. The type real corresponds to mathematical reals, with no bound and no rounding.

Statements

The language accepts a subset of C statements.

stat ::= expr;
| ;
| local-decl
| assert (expr);
| return;
| return expr;
| break;
| if (expr) stat
| if (expr) stat else stat
| while (expr) stat
| { stat ... stat }

Note that the expressions appearing in if, while, and assert constructs must be boolean and cannot be numeric.

Expressions

As in C, expressions include assignments, incrementations, and function calls.

expr ::= lvalue assign-op expr
| expr bin-op expr
| un-op expr
| expr incr-op
| incr-op expr
| (type) expr
| id(expr, ..., expr)
| (expr)
| bool-const
| num-const
| [num-const;num-const]
assign-op ::= = | += | -= | *= | /= | %=
bin-op ::= + | - | * | / | % | < | > | <= | >= | == | != | && | ||
un-op ::= + | - | !
incr-op ::= ++ | --
bool-const ::= true | false
num-const ::= int-const | float-const

Numeric constants include intervals [a;b], which model a non-deterministic choice. Each time the expression is evaluated, a new value between a and b is chosen.

Lvalues

The only lvalues allowed so-far are simple variable names.

lvalue ::= id

Declarations

Declarations include the declaration of local and global variables (with an optional initialization value), of functions (with an optional return type and arbitrary arguments), and of volatiles.

decl ::= local-decl | volatile-decl | fun-decl
local-decl ::= type var-decl, ..., var-decl;
volatile-decl ::= volatile type var-decl, ..., var-decl;
var-decl ::= id | id = expr
fun-decl ::= type-void id (type id, ..., type id) { stat ... stat }
type-void ::= type | void

Variables with no initialization expression specified are considered to have any value in the range of their type.

Volatile variables cannot be assigned. Each time they are evaluated as part of an expression, a non-deterministic value in their initialization range is returned.

Programs

A program is a list of declarations. The entry-point of the program is given as a parameter to the analysis; it can be any function with no argument and no return value.


© Antoine MinĂ© 2012.
contact: mine at di.ens.fr.