Syntax and informal semanticsContents

Syntax and informal semantics

Program.

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

Instructions.

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

Expressions.

Expressions.

<expr> ::= random random value (type deduced from the context)
 |  <bexpr> Boolean expression
 |  <iexpr> bounded integer expression
 |  <eexpr> enumerated type expression
 |  <nexpr> numerical expression

Boolean expressions.

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

Bounded integer and enumerated expressions.

<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  

Numerical expressions.

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

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 semanticsContents