A mini ACSL tutorial for Value, part 3: indirect assigns
André Maroneze - 12th Oct 2016To conclude our 3-part series on ACSL specifications for Value, we present a feature introduced in Frama-C Aluminium that allows more precise specifications: the indirect
label in ACSL assigns clauses. The expressivity gains when writing \from
s are especially useful for plugins such as Value.
Indirect assigns
Starting in Frama-C Aluminium (20150601), assigns clauses (e.g. assigns x \from src
) accept the keyword indirect
(e.g. assigns x \from indirect:src
), stating that the dependency from src
to x
is indirect, that is, it does not include data dependencies between src
and x
. In other words, src
itself will never be directly assigned to x
.
Indirect dependencies are, most commonly, control dependencies, in which src
affects x
by controlling whether some instruction will modify the value of x
. Another kind of indirect dependency are address dependencies, related to the computation of addresses for pointer variables.
Let us once again refer to our running example, the specification and mock implementation of safe_get_random_char
. As a reminder, here’s its specification, without the ensures \subset(*out,...)
postcondition, as suggested in the previous post:
#include <stdlib.h>
typedef enum {OK, NULL_PTR, INVALID_LEN} status;
/*@
assigns \result \from out, buf, n;
assigns *out \from out, buf, buf[0 .. n-1], n;
behavior null_ptr:
assumes out == \null || buf == \null;
assigns \result \from out, buf, n;
ensures \result == NULL_PTR;
behavior invalid_len:
assumes out != \null && buf != \null;
assumes n == 0;
assigns \result \from out, buf, n;
ensures \result == INVALID_LEN;
behavior ok:
assumes out != \null && buf != \null;
assumes n > 0;
requires \valid(out);
requires \valid_read(&buf[0 .. n-1]);
ensures \result == OK;
ensures \initialized(out);
complete behaviors;
disjoint behaviors;
*/
status safe_get_random_char(char *out, char const *buf, unsigned n);
Here’s the mock implementation of the original function, in which ensures \subset(*out,...)
holds:
#include "__fc_builtin.h"
#include <stdlib.h>
typedef enum { OK, NULL_PTR, INVALID_LEN } status;
status safe_get_random_char(char *out, char const *buf, unsigned n) {
if (out == NULL || buf == NULL) return NULL_PTR;
if (n == 0) return INVALID_LEN;
*out = buf[Frama_C_interval(0,n-1)];
return OK;
}
And here’s the main
function used in our tests:
void main() {
char *msg = "abc";
int len_arr = 4;
status res;
char c;
res = safe_get_random_char(&c, msg, len_arr);
//@ assert res == OK;
res = safe_get_random_char(&c, NULL, len_arr);
//@ assert res == NULL_PTR;
res = safe_get_random_char(NULL, msg, len_arr);
//@ assert res == NULL_PTR;
res = safe_get_random_char(&c, msg, 0);
//@ assert res == INVALID_LEN;
}
In the mock implementation, we see that out
and buf
are tested to see if they are equal to NULL
, but their value itself (i.e., the address they point to) is never actually assigned to *out
; only the characters inside buf
may be assigned to it. Therefore, out
and buf
are both control dependencies (in that, they control whether *out = buf[Frama_C_interval(0,n-1)]
is executed), and thus indirect as per our definition.
n
is also a control dependency of the assignment to *out
, due to the check if (n == 0)
. n
also appears in buf[Frama_C_interval(0,n-1)]
, leading this time to an address dependency: in lval = *(buf + Frama_C_interval(0,n-1))
, lval
depends indirectly on every variable used to compute the address that will be dereferenced (buf
, n
, and every variable used by Frama_C_interval
in this case).
If we run Value using our specification, this is the result:
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
msg ∈ {{ "abc" }}
len_arr ∈ {4}
res ∈ {2}
c ∈
{{ garbled mix of &{c; "abc"}
(origin: Arithmetic {file.c:33}) }}
Note that c
has a garbled mix which includes c
itself, plus the string literal "abc"
. The culprit is this assigns
clause:
assigns *out \from out, buf, buf[0 .. n-1], n;
out
is c
and buf
is "abc"
. n
, despite also being a dependency, does not contribute to the garbled mix because it is a scalar. The garbled mix appears because, in some functions, it is the address of the pointer itself that is assigned to the lvalue in the assigns
clause. Without a means of distinguishing between direct and indirect dependencies, one (dangerous) workaround is to omit some dependencies from the clauses. This may lead to incorrect results.
Thanks to indirect \from
clauses, now we can avoid the garbled mix by specifying that out
and buf
are only indirect
dependencies. Applying the same principle to all assigns clauses, we obtain the final version of our (fixed) specification:
/*@
assigns \result \from indirect:out, indirect:buf, indirect:n;
assigns *out \from indirect:out, indirect:buf, buf[0 .. n-1], indirect:n;
behavior null_ptr:
assumes out == \null || buf == \null;
assigns \result \from indirect:out, indirect:buf, indirect:n;
ensures \result == NULL_PTR;
behavior invalid_len:
assumes out != \null && buf != \null;
assumes n == 0;
assigns \result \from indirect:out, indirect:buf, indirect:n;
ensures \result == INVALID_LEN;
behavior ok:
assumes out != \null && buf != \null;
assumes n > 0;
requires \valid(out);
requires \valid_read(&buf[0 .. n-1]);
ensures \result == OK;
ensures \initialized(out);
complete behaviors;
disjoint behaviors;
*/
status safe_get_random_char(char *out, char const *buf, unsigned n);
Note that indirect dependencies are implied by direct ones, so they never need to be added twice.
With this specification, Value will return c ∈ [--..--]
, without garbled mix. The result is still imprecise due to the lack of ensures
, but better than before. Especially when trying Value on a new code base (where most functions have no stubs, or only simple ones), the difference between garbled mix and [--..--]
(often called top int, that is, the top value of the lattice of integer ranges) is significant.
In the new specification, it is arguably easier to read the dependencies and to reason about them: users can skip the indirect dependencies when reasoning about the propagation of imprecise pointer values.
The new specification is more verbose because indirect
is not the default. And this is so in order to avoid changing the semantics of existing specifications, which might become unsound.
The From plugin has a new (experimental) option, --show-indirect-deps
, which displays the computed dependencies using the new syntax. It is considered experimental simply because it has not yet been extensively used in industrial applications, but it should work fine. Do not hesitate to tell us if you have issues with it.
Ambiguously direct dependencies
It is not always entirely obvious whether a given dependency can be safely considered as indirect
, or if it should be defined as direct. This is often the case when a function has an output argument that is related to the length (or size, cardinality, etc.) of one of its inputs. strnlen(s, n)
is an example of a libc function with that property: it returns n
itself when s
is longer than n
characters.
Let us consider the following function, which searches for a character in an array and returns its offset, or the given length if not found:
// returns the index of c in buf[0 .. n-1], or n if not found
/*@ assigns \result \from indirect:c, indirect:buf,
indirect:buf[0 .. n-1], indirect:n; */
int indexOf(char c, char const *buf, unsigned n);
Our specification seems fine: the result value is usually the number of loop iterations, and therefore it depends indirectly on the related arguments.
However, the following implementation contradicts it:
int indexOf(char c, char const *buf, unsigned n) {
unsigned i;
for (i = 0; i < n; i++) {
if (buf[i] == c) return i;
}
return n;
}
void main() {
int i1 = indexOf('a', "abc", 3);
int i2 = indexOf('z', "abc", 3);
}
If we run frama-c -calldeps -show-indirect-deps
(that is, run the From plugin with callwise dependencies, showing indirect dependencies) in this example, we will obtain this output:
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to indexOf at ambiguous.c:10 (by main):
\result FROM indirect: c; buf; n; "abc"[bits 0 to 7]
[from] call to indexOf at ambiguous.c:11 (by main):
\result FROM indirect: c; buf; n; "abc"[bits 0 to 23]; direct: n
[from] entry point:
NO EFFECTS
[from] ====== END OF CALLWISE DEPENDENCIES ======
Note that, in the second call, n
is computed as a direct dependency. Indeed, it is directly assigned to the return value in the code. This means that our specification is possibly unsound, since it states that n
is at most an indirect dependency of \result
.
However, if we modify our implementation of indexOf
to return i
instead of n
, then From will compute n
as an indirect dependency, and thus our specification could be considered correct. The conclusion is that, in some situations, both versions can be considered correct, and this not will affect the end result.
One specific case where such discussions may be relevant is the case of the memcmp
function of the C standard library (specified in string.h
): one common implementation consists in comparing each byte of both arrays, say s1[i]
and s2[i]
, and returning s1[i] - s2[i]
if they are different. One could argue that such an implementation would imply that assigns \result \from s1[0 ..], s2[0 ..]
, with direct dependencies. However, this can create undesirable garbled mix, so a better approach would be to consider them as indirect dependencies. In such situations, the best specification is not a clear-cut decision.
Frama-C libc being updated
The Frama-C stdlib has lots of specifications that still need to be updated to take indirect
into account. This is being done over time, which means that unfortunately they do not yet constitute a good example of best practices. This is improving with each release, and soon they should offer good examples for several C standard library functions. Until then, you may refer to this tutorial or ask the Frama-C community for recommendations to your specifications.
Also note that some of these recommendations may not be the most relevant ones when considering other plugins, such as WP. Still, most tips here are sufficiently general that they should help you improve your ACSL for all purposes.