PAG/WWW Logo

© 1998-2009 Saarland University and AbsInt

Please note that this service will be discontinued after December 31, 2013

 The analysis specification language
 

This document describes the FULA language in greater detail. For a general introduction to the various parts of an analysis specification and an informal description of the FULA language take a look at How to build your own analysis.

The following table presents the context free grammar of the analysis specification language. Keywords are printed in bold underlined, square brackets [] denote optional parts.

analysis ::= [typesection] problemsection transfersection [supportsection]
 
typesection ::= TYPE { identifier = typedef }*
 
typedef ::= set ( identifier )
| list ( identifier )
| lift ( identifier )
| flat ( identifier )
| identifier { * identifier }+
| identifier -> identifier
 
problemsection::= PROBLEM [ identifier ] { problemdef }*
 
problemdef ::= direction = { forward | backward }
| carrier = identifier
| init = expression
| init_start = expression
| combine = identifier
| equal = identifier
| widening = identifier
| narrowing = identifier
 
transfersection ::= TRANSFER { statementpattern [ , edgetype ] = expression }*
 
statementpattern ::= PROGRAM_BEGIN ( )
| PROGRAM_END ( )
| BEGIN ( identifier , identifier )
| END ( identifier , identifier )
| SKIP ( )
| ASSIGN ( identifier , identifier )
| IF ( identifier )
| WHILE ( identifier )
| CALL ( identifier , identifier , identifier )
| RETURN ( identifier , identifier , identifier )
 
edgetype ::= normal_edge
| true_edge
| false_edge
| call_edge
| return_edge
| local_edge
| _
| identifier
 
supportsection ::= SUPPORT { supportdefinition | supportimplementation }*
 
supportdefinition ::= identifier :: [ identifier { * identifier }* ] -> identifier
 
supportimplementation ::= identifier ( pattern { , pattern }*) = expression
 
const ::= number
| string
| true
| false
| top
| bot
| all
| { }
| [ ]
 
pattern ::= identifier
| _
| const
| ( pattern { , pattern }+ )
| pattern : pattern
| [ pattern { , pattern }* ]
| pattern as identifier
 
expression ::= identifier
| const
| @
| ( expression )
| expression ( { expression }* )
| [ expression { , expression }* ]
| { expression { , expression }* }
| + expression
| - expression
| expression + expression
| expression - expression
| expression * expression
| expression / expression
| expression % expression
| expression ^ expression
| expression : expression
| expression { < | <= | > | >= } expression
| expression = expression
| expression != expression
| ! expression
| expression && expression
| expression || expression
| expression lub expression
| expression glb expression
| expression # number
| expression ? expression
| [ -> expression ]
| expression \ [ update { , update }* ]
| zfexpression
| let letdef { , letdef }* in expression
| case expression { , expression }* of { casepattern }+ endcase
 
update ::= expression -> expression
 
letdef ::= pattern = expression
| pattern <= expression
 
casepattern ::= pattern { , pattern }* => expression ;
 
zfexpression ::= [ expression | zf { ; zf }* ]
| { expression | zf { ; zf }* }
| [ expression \ expression | zf { ; zf }* ]
 
zf ::= expression
| let letdef { , letdef }*
| pattern in expression
| pattern in expression \ expression

Additional restrictions

In the PROBLEM section of the program the direction, carrier, init, init_start and combine commands must all be present (each one exactly once). The equal, widening and narrowing commands are optional, but may not be present more than once. The order of the commands is free.

The scope of an identifier is the part of the program where it is visible. An identifier may only be used in an expression if it is visible. New identifers are introduced by static function definitions or by patterns in let and case constructs, in ZF expressions or in static function definition parameters.
A visible name may be hidden by introducing the same name again in the scope of that name, so that any reference to the name will reference the second introduction.
Apart from this hiding the scope of a name is defined by some rules:

  • Type names (e.g. snum, ExpressionSet...) are only visible in the TYPE section and in SUPPORT function definitions.
  • Names of static functions (builtin functions and SUPPORT functions) are visible in expression and in equal, widening, narrowing and combine commands.
  • Global variables are only visible in expression.
  • Names from patterns in static function definitions are visible in the body of that definition only.
  • Names from case patterns are visible only in the branch of the case where the pattern occured.
  • Names from patterns in let expressions are visible in the body of the let expression only. They are not visible in other simultaneous definitions. Thus let x=2 in let x=1, y=x in y will evaluate to 2, not 1.
  • In ZF expressions names can be introduced by patterns in generators and local definitions. The head of a ZF expression is defined to be:
    h,  if zfexp  = { h | zf1; .. ;zfn }
    head(zfexp)  =  h,  if zfexp  =  [ h | zf1; .. ;zfn ]
    a,  if zfexp  =  [ [->b]\a | zf1; .. ;zfn ]
    Names introduced in a zfi are visible in all other zfs to the right (i.e. all zfj, j>i) and in head(zfexp).
    Important: variables introduced in generators or local definitions within the ZF expression are not visible in the default value expression (called b above) when you are generating a dynamic function. This is because the default value must be unique, so it may not be dynamically generated within the ZF expression.
    a must either be a list of update or evaluate to a argument value pair (x,y) where y must have the same type as b.
  • The number of patterns in each branch of a case statement must be the same and coincide with the number of expressions after the case keyword.
  • The actual data flow value @ is only visible in TRANSFER functions.

See How to build your own analysis for a step-by-step description of the FULA semantics.

Search


 

for 

  

 

Please send any suggestions, comments or questions to Martin@cs.uni-sb.de.