|
| | | Syntax and informal semantics | Contents |
| <program> | ::= | [typedef <type_def>+] | enumerated types definition |
| <procedure_def>* | definition of procedures | ||
| [var <vars_decl> ;] | local variables of the main procedure | ||
| begin <statement>+ end | body of the main procedure | ||
| <type_def> | ::= | id = enum { id (, id)* } ; | |
| <procedure_def> | ::= | proc id ( <vars_decl> ) returns ( <vars_decl> ) | signature, with names of |
| input and output formal parameters | |||
| [var <vars_decl> ;] | (other) local variables | ||
| begin <statement>+ end | body |
A procedure definition first declares a list of formal input parameters, then a list of formal output parameters (which are local variables that defines the tuple of returned values), then a list of local variables, and then a body. A procedure ends with its last statement.
| <vars_decl> | ::= | eps | id : <type> (, id : <type>)* | |
| <type> | ::= | bool | Boolean type |
| | | uint[<integer>] | unsigned integers encoded with <integer> bits | |
| | | sint[<integer>] | signed integers encoded with <integer> bits | |
| | | id | Name of an enumerated type | |
| | | int | real | numerical types | |
Variables are either of finite-type, or unbounded integer or real type. Finite types includes Boolean, bounded integers encoded with the given numbe rof bits, and enumerated types. Real variables can behave as floating-point variables by modifying the exact semantics of arithmetic operations (see below).
| <statement> | ::= | skip ; |
| | | halt ; | |
| | | fail ; | |
| | | assume <expr> ; | |
| | | id = random ; | |
| | | id = <expr> ; | |
| | | id = id ( <var_list> ) ; | |
| | | ( <var_list> ) = id ( <var_list> ) ; | |
| | | if <bexpr> then <statement>+ [else <statement>+ ] endif ; | |
| | | while <bexpr> do <statement>+ done ; | |
| <var_list> | ::= | eps | id (, id)* |
The skip operation does nothing. The halt operation halts the program execution. The fail has exactly the same operational semantics, but, in addition, indicates a final control point for backward analysis (see below).
The assume expr instruction is equivalent to if expr then skip; else halt; . It may be used to abstract non-deterministic assignements. For instance, the non-deterministic assignement of a value between 0 and 2 to a variable x can be written as
x = random; assume x>=0 and x<=2;
A call to a procedure with a single return value can be written either as x = P(...) or (x)=P(...). A call to a procedure with multiple return values is written as (x,y) = P(a,b). Input parameters are passed by value. Formal input parameters in a procedure are assumed immutable.
Conditional and iteration constructions have the usual semantics.
| <expr> | ::= | random | random value (type deduced from the context) |
| | | <bexpr> | Boolean expression | |
| | | <iexpr> | bounded integer expression | |
| | | <eexpr> | enumerated type expression | |
| | | <nexpr> | numerical expression |
| <bexpr> | ::= | true | false | |
| | | id | variable | |
| | | <constraint> | ||
| | | not <bexpr> | ||
| | | <bexpr> (or | and) <bexpr> | ||
| | | ( <bexpr> ) | ||
| | | if <bexpr> then <bexpr> else <bexpr> | ||
| <constraint> | ::= | id == <expr> | |
| <iexpr> (>= | > | <= | <) <iexpr> | |||
| <nexpr> (>= | > | <= | <) <nexpr> |
Atoms of Boolean expressions are Boolean constants or equality constraints (on any type) or inequality constraints over bounded integer or numerical variables.
| <iexpr> | ::= | uint[<integer>](<integer>) | constant (second integer) of given type |
| | | sint[<integer>](<integer>) | constant (second integer) of given type | |
| | | id | variable | |
| | | <iexpr> (+|-|*) <iexpr> | ||
| | | ( <iexpr> ) | ||
| | | if <bexpr> then <iexpr> else <iexpr> | ||
| <eexpr> | ::= | id | variable or constant (label) |
| | | ( <eexpr> ) | ||
| | | if <bexpr> then <eexpr> else <eexpr> |
Example:
/* Illustrate enumerated and bounded integer types */
typedef t = enum a,b,c,d,e ;
var x:sint[4],y:sint[4], z:t;
begin
x = sint[4](2);
y = random;
z = a;
if x==y then
x = x + x;
x = x-sint[4](3)*y;
z = b;
endif;
if x<=y then
z = e;
endif;
if z==d then z=c; endif;
end
| <nexpr> | ::= | <coeff> | |
| | | id | variable | |
| | | <unop> <nexpr> | <nexpr> <binop> <nexpr> | ||
| | | ( <nexpr> ) | ||
| | | if <bexpr> then <nexpr> else nexpr | ||
| <binop> | ::= | (+|-|*|/|%)[_(i|f|d|l|q)[,(n|0|+oo|-oo)]] | |
| <unop> | ::= | - | |
| | | (cast|sqrt)[_(i|f|d|l|q)[,(n|0|+oo|-oo)]] | ||
| <coeff> | ::= | <float> | <rational> | |
| <float> | ::= | C/OCaml floating-point number syntax | |
| <rational> | ::= | <integer> | <integer>/<integer> |
The syntax of numerical expressions is the same as the one used in the APRON interactive toplevel (in OCaml language).
The priorities between (Boolean and arithmetic) operators is { *,/ } > { +,- } > { <, <=, =, >=,> } > { not } > { and } > { or }
By default, numerical expressions are evaluated using exact arithmetic on real numbers (even if some involved variables are integer), and when assigned to a variable, filtered by the variable domain (when it is integers). For instance, the assignement
x = 3/4;
is equivalent to the halt instruction if x is declared as integer, because the rational 3/4 is not an integer value. The problem here is that the instruction is not well-typed (even if this is not checked). If one want to emulate the semantics of the integer division operation, with rounding to zero, one should write
x = 3 /_i,0 4;
Indeed, most arithmetic operators have optional qualifiers that allows to modify their semantics. The first qualifier indicates a numerical type, the second one the rounding mode.
| i | integer semantics |
| f | IEEE754 32 bits floating-point semantics |
| d | IEEE754 64 bits floating-point semantics |
| l | IEEE754 80 bits extended floating-point semantics |
| q | IEEE754 128 bits floating-point semantics |
| n | nearest |
| 0 | towards zero |
| +oo | towards infinity |
| -oo | towards minus infinity |
We illustrate the syntax and (approximated) semantics of numerival expressions with the following program, annotated by InterprocStack using the command
interprocstack.opt -domain polka -colorize false examples/numerical.spl
proc integer () returns () var a : int, b : int, c : int;
begin
/* (L5 C5) top */
a = 5; /* (L6 C8) [|a-5=0|] */
b = 2; /* (L7 C8) [|b-2=0; a-5=0|] */
if brandom then
/* (L8 C17) [|b-2=0; a-5=0|] */
c = a / b; /* (L9 C14) bottom */
else
/* (L10 C6) [|b-2=0; a-5=0|] */
c = a /_i,? b; /* (L11 C16) [|b-2=0; a-5=0; -c+3>=0; c-2>=0|] */
c = a /_i,0 b; /* (L12 C18) [|c-2=0; b-2=0; a-5=0|] */
c = a /_i,-oo b; /* (L13 C20) [|c-2=0; b-2=0; a-5=0|] */
c = a /_i,+oo b; /* (L14 C20) [|c-3=0; b-2=0; a-5=0|] */
c = a /_i,n b; /* (L15 C18) [|b-2=0; a-5=0; -c+3>=0; c-2>=0|] */
c = a %_i,? b; /* (L16 C16) [|c-1=0; b-2=0; a-5=0|] */
endif; /* (L17 C8) [|c-1=0; b-2=0; a-5=0|] */
end
proc exact () returns (z : real) var x : real, y : real;
begin
/* (L22 C5) top */
x = 5; /* (L23 C8) [|x-5=0|] */
y = 2; /* (L24 C8) [|y-2=0; x-5=0|] */
z = x / y; /* (L25 C10) [|2z-5=0; y-2=0; x-5=0|] */
y = 0.1; /* (L26 C10)
[|2z-5=0; 36028797018963968y-3602879701896397=0; x-5=0|] */
z = x + y; /* (L27 C10)
[|36028797018963968z-183746864796716237=0;
36028797018963968y-3602879701896397=0; x-5=0|] */
z = z - y; /* (L28 C10)
[|z-5=0; 36028797018963968y-3602879701896397=0; x-5=0|] */
end
proc floating () returns (z : real) var x : real, y : real;
begin
/* (L33 C5) top */
x = 5; /* (L34 C8) [|x-5=0|] */
y = 2; /* (L35 C8) [|y-2=0; x-5=0|] */
z = x /_f,? y; /* (L36 C13)
[|y-2=0; x-5=0;
-713623846352979940529142984724747568191373312z
+1784059828558929176909397126420998565333565441>=0;
713623846352979940529142984724747568191373312z
-1784059403205970525736317797202739275623301119>=0|] */
y = 0.1; /* (L37 C10)
[|36028797018963968y-3602879701896397=0; x-5=0;
-713623846352979940529142984724747568191373312z
+1784059828558929176909397126420998565333565441>=0;
713623846352979940529142984724747568191373312z
-1784059403205970525736317797202739275623301119>=0|] */
z = x +_f,? y; /* (L38 C14)
[|36028797018963968y-3602879701896397=0; x-5=0;
-713623846352979940529142984724747568191373312z
+3639482050260215524856578735848702239922192385>=0;
713623846352979940529142984724747568191373312z
-3639481182540179876463495959770156714984210431>=0|] */
z = z -_f,? y; /* (L39 C14)
[|36028797018963968y-3602879701896397=0; x-5=0;
-5986310706507378352962293074805895248510699696029696z
+29931560882862943060522688904967984086376852368654337>=0;
5986310706507378352962293074805895248510699696029696z
-29931546182211708189135890236173744477275669529624577>=0|] */
end
var z : real
begin
/* (L43 C5) top */
() = integer(); /* (L44 C17) top */
z = exact(); /* (L45 C14) [z-5=0|] */
z = floating(); /* (L46 C17)
[|-5986310706507378352962293074805895248510699696029696z
+29931560882862943060522688904967984086376852368654337>=0;
5986310706507378352962293074805895248510699696029696z
-29931546182211708189135890236173744477275669529624577>=0|] */
end
|
| | | Syntax and informal semantics | Contents |