Declare some types and predicates in the editor below, then click .
The correlation results for the code you entered are shown below. Hover or click on the results to obtain an explanation of what they mean.
The following example shows a simple process manager and the types of its two main entities:
thread, both defined as
structures. The first predicate shown (the equivalent of functions in our language) is
thread. It receives a process
p and an
i as inputs.
It accesses the element in the
i-th cell of the array
threads of the input
p. If the element is active, the predicate exits with the
true and outputs
ti, the thread below the
constructor. Otherwise, it exits with the label
None and produces no output.
The second predicate,
descriptor, makes a call to the
thread, thus reading the
j-th element of
threads array of its input
proc. If this element is active, the predicate
returns the value of its stack descriptor as an output.
threadpredicate distinguish between the two possible exit labels,
None. For the label,
true, the correlation summary captures the flow of the active
i-th thread of the input's
threadsarray, in the
tioutput. For the label
None, since there are no outputs, we obtain
truelabel of the predicate
descriptorcapture the flow of the stack descriptor's value of the active
j-th thread associated to the input process
procinto the output
This example is presented in the first section of our article.
stop has two possible execution
true, when the given index
i corresponds to an
thread, and inval otherwise.
In the former case,
stop copies the
i-th element of
threads array to a local variable
th, sets its state to
and leaves everything else unmodified. The new state
o of the process is then returned, with
i-th element set to
th and everything else copied from
Our analysis infers that between the input process
in and the output
values of the fields
address_space are equal.
Furthermore, it detects that all elements of the array
threads are equal, except the value of
i-th element, for which only the
The following example shows the
taking a process
i and a
len as inputs.
If the given index
i is valid and
represents an active thread having reading permissions,
the predicate changes the range of the memory segment that
i-th thread is allowed to
read. The read permission contains the
id of the thread from
i-th thread is allowed
to read, as well as the starting
start_adr and the
len of the allowed memory
range. Only the
len of the read
permission is modified and set to the given input
length. Everything else remains
unchanged. The new state of the process after the
modification is returned in the output
The correlation analysis detects that on
true label of the
predicate, only the
i-th thread associated to the input
p is modified. Furthermore, the
results capture the fact that for this thread, the only
modified field is the
perm field, inside
which only the
len is modified. The flow of
the given input
length into the value of the
len argument is detected
as well. All other labels model exceptional execution
scenarios for which no output is produced.
This example is similar to the one given
in Change permissions.
shown below makes calls to other auxiliary predicates.
The correlation results of the
are identical to the ones obtained for the example shown
in Change permissions.
In the current examples, the formal parameters of the
called predicates are correctly substituted by the
effective parameters given as arguments
The following example shows a simple process manager and its two main
set_thread returns the new state
new_p of the
given input process
p after updating the
i-th element of its
field and setting it to the given input thread
ti. Everything else is copied
The results indicate that the fields
pid of output process
new_p are equal to those of the input
p. Furthermore, it detects that every element, except the one identified
i, of the
threads array is equal between the two. The flow of the
ti into the
i-th cell of
threads array is
captured as well.
This example summarizes the statements supported by our language that are not type-specific. Each statement is wrapped inside a different predicate.
This example summarizes the structure-related statements supported by our language. Each statement is wrapped inside a different predicate.
struct_create, the values of the inputs
thsflow into the corresponding fields of the output structure
p. The computed correlation summary captures these equalities between the inputs and the output
struct_all, the value of the fields of the input structure
pflow into the corresponding outputs, i.e
ths, respectively. The computed correlation summary captures these equalities between the input
pand the generated outputs.
get_field, only the field
current_threadof the input process
pis accessed and copied into the output
set_field, all other fields, except the updated one –
current_thread– are entirely preserved between the input and the output. The input's
crtvalue used for the update flows entirely into the value of the field
current_threadof the output
struct_equals, we test that the two inputs
pare equal on the fields
address_space. This predicate makes no modifications; it only has read effects.
This example shows the variant-related statements supported by our language. Each is wrapped inside a different predicate.
variant_cons, the output thread
tois created by copying the entire value of the input
thunder the element of its
variant_possibletests which constructors of the input variant
sare possible on the label
false, respectively. This predicate does not produce any output and has only read effects.
variant_switch, the predicate matches on the constructors of the input
op. If this is an active element, i.e created with the constructor
Some, the value
tunder this constructor is entirely copied into the output thread
This example shows the array-related statements supported by our language. Each is wrapped inside a
different predicate. Both operations – array access and array update – exit with the
false when the given index is out of the array's bounds. We keep
exceptional correlations for just one element whose index must be an input. The
array_set_local consider local indices.
array_get, for the label
j-th element of the input array
ais entirely copied into the output
array_set, on the label
true, the analysis indicates that every element of the input array
a, except the
j-th one, is copied into the output array
new_a. The input
tis copied into the
j-th element of the array
array_set_local, the analysis makes an overapproximation and indicates that there is no correlation between the elements of the input array
aand the ones of the output array
new_a. Since the index
jused for updating a cell of the array is a local variable, we have to join
Equal, the relation known between elements other than the
j-th one, with
Any, the relation known between the
j-th elements of the two arrays. Since
Anyis the absorbing element for join, the result is
array_get_local, we overapproximate to
NoCorrelation. In the final correlation summaries, only input variables are allowed to appear in paths corresponding to array cells. All the others are filtered. Intraprocedurally, the only correlation computed between
tjrefers to the pair of paths (
j, ε) and since it contains
j, a local variable this is filtered, thus leading to (ε, ε) -> Any.