We can view analysis and verification as two stage process
program + properties => system of equations/formulas => solution
In general, the system of equations (for a program expressed as one loop) is an approximation of the condition
where is the set of reachable states and
the code of the program.
We have seen earlier
Today we look at another constraint based analysis, which deals with non-numeric properties and is based on set constraints.
Two problems:
Set constraints can be naturally used to express
Different axes for classifying analyses:
Set constraints are suitable for non-relational analyses, whether they are flow sensitive or not and whether they are context-sensitive or not.
Type systems: context-sensitive (e.g. generics), work for higher-order programs (and callbacks and function pointers). Often flow insensitive (unless they are “typestate” or “flow sensitive type qualifiers”). Sometimes designed for purely functional programs (higher order imperative programs are difficult to reason about).
We can define the subset constraints between expressions denoting sets of terms using the following grammar :
where is a constant,
is a terminal (it can be a variable or function symbol),
is an application function and
is the projection of th
parameter of
.
Note: set difference () as it is not monotonic, so its use is restricted if we want to ensure existence of solutions.
We define the semantic of our syntax recursively by defining each of its elements over a language . We first have that :
where is the Herbrand univers, or “set of all ground terms”, or also called the “term model”. As we already saw, it's the set of all possibly constructed trees using language
:
Given that, if the meaning of is given (i.e. we have
), then we can estimate the meaning of our language as following :
Using this example we can already see how we could use set constraints to analyze procedure calls as can be viewed as a procedure call on which we apply possible parameters.
An important property we would like to have in this semantic is a very intuitive one :
This property is in fact not conserved as we can easily see using a very simple counter-example :
The correct interpretation of this property is :
A variable is said to ba alive when it's value will be reused later in the program.
Example :
x = 1; y = 5; z = 7; z = x + y;
in this example, only variables x and y are alive.
Example of use:
In order to compute the set of live variable, let's take the same example as before to use it to deduce the update rule. We can see our program as the following tree :
From this we can deduce the following set equations that define the relation between the sets of active variables at different program points :
Where as they are used in
and
as it's the newly defined variable in
.
Here we do not have a problem with the monotonicity of the \ operator as
is not a variable.
Example of the problem
In a functional language, f is a variable that pass a function. In this context, to which function (f x y) refers to ? In order to answer this question, we have to keep track of who called f.
where is a part of the program
and
is a constant.
For the case of application, the question is : Can describe the expression
?
Example
We will try to see if this is the case using .
From this we can deduce, as we defined previously, the following contraints :
Which leads to the following solutions :
Which shows that the variable can described our test expression.
Now that we know how to convert the \lambda calculus into set constraints, we need to be able to express
into set constraints too as it is not part of our gramar.
The general form of the conditional constraints is the following : .
We can transform it like this :
Which has the correct meaning as we have :
Not seen in class, have a look at the papers !
Not seen in class, have a look at the papers !
Not seen in class, have a look at the papers !