| |
» Back to overview
In the TRANSFER section you specify how the exit information
for each node is computed from the entry information at that node and additional
local information (like the label of the current statement).
Each line in the TRANSFER section specifies a pattern that matches a type
of statement followed by a FULA function that
specifies the transfer function for the specified type of statement.
Variables introduced in the statement pattern are visible in the corresponding
FULA function. So each line has the form:
statement-pattern = FULA-expression where
statement-pattern is one of:
| SKIP ( ) |
skip; |
| ASSIGN ( var , exp ) |
var := exp;
var is of FULA type Var, exp has type Expression |
| WHILE ( exp ) |
while (exp) do ...
exp is of type Expression |
| IF ( exp ) |
if (exp) do ...
exp is of type Expression |
| CALL ( proc, param, exp ) |
call proc(exp);
proc is of type Proc, param has type Var and specifies the formal parameter of the procedure, exp has type Expression |
| RETURN ( proc, param, exp ) |
call proc(exp);
proc is of type Proc, param has type Var and specifies the formal parameter of the procedure, exp has type Expression
This is the information for the corresponding CALL node. |
| PROGRAM_BEGIN ( ) |
the begin node of the main program |
| PROGRAM_END ( ) |
the end node of the main program |
| BEGIN ( proc, param ) |
the begin node of procedure proc
proc is of type Proc, param has type Var and specifies the formal parameter of the procedure |
| END ( proc, param ) |
the end node of procedure proc
proc is of type Proc, param has type Var and specifies the formal parameter of the procedure
This is the information for the corresponding begin node. |
In each TRANSFER function the entry information of the node can be accessed through the variable @, which has the carrier type defined in the PROBLEM section.
Also each TRANSFER function can access two predefined local variables:
label (type: Label), which contains the while label of the current statement;
proc (type: Proc), which contains the while procedure that the current statement belongs to.
Example:
Consider an "Used Expressions" analysis, that collects all expressions in the program. Thus the carrier type is ExpressionSet (one of the built-in PAG/WWW types). The line
ASSIGN (v, e) = @ + e
will take the entry information at each assignment and set the exit information for that node to the set of all expressions in the entry information plus the expression at the actual assignment.
For certain analyses (e.g. interprocedural analyses)
it may be useful to specify different exit information for different outgoing edges,
e.g. at CALL nodes you may want to pass different information to
local and call edges.
You may do so by specifying an edge type after the statement pattern. For example
CALL(_, _, _), local_edge = bot
CALL(_, _, _), call_edge = @
will pass bot to the outgoing local edge and @ (the value of the entry information) to the outgoing call edge. If you do not specify an edge type the same exit information will be propagated to all outgoing edges.
There are six different types of edges:
normal_edge
true_edge (the edge from an IF node to the "then" block of the if statement or from a WHILE node to the body of the while loop)
false_edge (the edge from an IF node to the "else" block of the if statement or from a WHILE node to the next statement after the while loop)
call_edge (the edge from a CALL node to the BEGIN node of the procedure to call)
return_edge (the edge from a procedure END node to the RETURN node of the procedure call)
local_edge (the local edge connecting a CALL node and its corresponding RETURN node)
You can also match the edge type against "_" (which is the same as not
matching the edge at all) or against an identifer (which is then bound to
the actual edge type). So you could write:
CALL(_, _, _), edge = if (edge = local_edge) then bot else @ endif
Next step
Contents
- Overview
- Specifying datatypes in the TYPE section
- Specifying the framework of your analysis in the PROBLEM section
- The FULA language
- Global FULA variables
- Specifying the TRANSFER section
- The SUPPORT section
- Built-in PAG/WWW functions
- A formal description of the analysis specification syntax
Search
| |
