Syntax and informal semantics Contents

## Syntax and informal semantics

### Program.

 ::= [typedef +] enumerated types definition * definition of procedures [var ;] local variables of the main procedure begin + end body of the main procedure ::= id = enum { id (, id)* } ;
 ::= proc id ( ) returns ( ) signature, with names of input and output formal parameters [var ;] (other) local variables begin + 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.

 ::= eps  | id : (, id : )* ::= bool Boolean type | uint[] unsigned integers encoded with bits | sint[] signed integers encoded with 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).

### Instructions.

 ::= skip ; | halt ; | fail ; | assume ; | id = random ; | id = ; | id = id ( ) ; | ( ) = id ( ) ; | if then + [else + ] endif ; | while do + done ; ::= 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.

### Expressions.

#### Expressions.

 ::= random random value (type deduced from the context) | Boolean expression | bounded integer expression | enumerated type expression | numerical expression

#### Boolean expressions.

 ::= true  | false | id variable | | not | (or | and) | ( ) | if then else ::= id == (>= | > | <= | <) (>= | > | <= | <)

Atoms of Boolean expressions are Boolean constants or equality constraints (on any type) or inequality constraints over bounded integer or numerical variables.

#### Bounded integer and enumerated expressions.

 ::= uint[]() constant (second integer) of given type | sint[]() constant (second integer) of given type | id variable | (+|-|*) | ( ) | if then else ::= id variable or constant (label) | ( ) | if then else

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
```

#### Numerical expressions.

 ::= | id variable |  |  | ( ) | if then else nexpr ::= (+|-|*|/|%)[_(i|f|d|l|q)[,(n|0|+oo|-oo)]] ::= - | (cast|sqrt)[_(i|f|d|l|q)[,(n|0|+oo|-oo)]] ::=  |  ::= C/OCaml floating-point number syntax ::=  | /

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.

• By default, operations have an exact arithmetic semantics in the real numbers (even if involved variables are of integer). The type qualifiers modify this default semantics. Their meaning is as follows:

 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

• By default, the rounding mode is "any" (this applies only in non-real semantics), which allows to emulate all the following rounding modes:

 n nearest 0 towards zero +oo towards infinity -oo towards minus infinity

#### Examples of numerical expressions.

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