Clarification on meaning of \valid

[sfsiegel]

I have a question about the meaning of \valid. The ACSL manual says "A pointer p is said to be valid if *p is guaranteed to produce a definite value according to the C standard", and "\valid{L}(s) holds if and only if dereferencing any p ∈ s is safe at label L, both for reading from *p and writing to it."

In the following code, is p valid?

int main() {
int x, *p = &x;
//@ assert \valid(p);
}

According to the C Standard, the value of x is "indeterminate" and an attempt to read *p results in undefined behavior, because x might hold a "trap representation" which does "not represent a value of the object type".

So it sounds like *p is not guaranteed to produce a definite value, and certainly dereferencing p is not safe for reading. But I'm pretty sure that the intention is that p should be valid and Frama-C+WP says the assertion holds.

---

Quotes from C Standard (2018)...

"If an object that has automatic storage duration is not initialized explicitly, its value is indeterminate." (6.7.9 (10))

"Certain object representations need not represent a value of the object type. If the stored value of an object has such a representation and is read by an lvalue expression that does not have character type, the behavior is undefined. ... Such a representation is called a trap representation". (6.2.6.1(5))

"Thus, an automatic variable can be initialized to a trap representation without causing undefined behavior, but the value of the variable cannot be used until a proper value is stored in it." (footnote 50)

[pbaudin]

Something has to be modified into the ACSL manual about the definition of \valid predicate.
From a first look at this, I would say that:

• \valid{L}(s) holds if and only if dereferencing any p ∈ s is safe at label L, for writing to *p.
• of course, the reading from *p requires both \valid_read{L)(p) and \initialized{L}(p) since the initialization condition isn't part of \valid predicate nor \valid_read.

[yakobowski]

I mostly agree with @pbaudin . I have two remarks:

• do not forget !\dangling next to \initialized
• in general, I think the high-level description of \valid should take talk about indeterminate

3.17.2
1 indeterminate value
either an unspecified value or a trap representation

With the caveat that ACSL has support for talking about (un)specified values (through \initialized and \dangling) but not about trap representations. (No predicate was ever created.)

[vprevosto]

@yakobowski I'm not sure I'm following you. if !\initialized(&x), then the value of x is indeed indeterminate, not merely unspecified. If it were, reading from x wouldn't be an undefined behavior, just unspecified.

[yakobowski]

You're right, I got confused. I remembered that we determined that indeterminate values were partitioned between non-initialized + dangling + trap representations, but this is completely unrelated to unspecified values.

This means that the fix is easier though. Just mention that reading a \valid_read pointer may lead to an indeterminate value.

[sfsiegel]

It seems to me there are at least 4 different classes of pointer values one would like to specify with predicates. These may not be the appropriate names, but here is the idea...

Valid: can be used in pointer arithmetic, equality and inequality. Cannot necessarily be used as argument of dereference operator.

Allocated: Valid + points to allocated memory. I.e., all sizeof(T) bytes are inside a live object.

Readable: Allocated + the bytes represent a valid, non-trap, value of the type. Hence *p can be read.

Writeable: Allocated + T is not const-qualified, so you can assign to *p.

Example of not valid:
int main() { int *p; }
Example of valid but not allocated:
int main() { int x=0, *p=&x+1; }
Example of allocated but not readable or writeable:
int main() { const int x, *p=&x; }
Example of writeable but not readable:
int main() { int x, *p=&x; }
Example of readable but not writeable:
int main() { const int x=0, *p=&x; }
Example of readable and writeable:
int main() { int x=0, *p=&x; }

Is there some way to express each of these in ACSL?

[yakobowski]

[Note: I corrected a typo for "Readable", I initially wrote \valid instead of \valid_read]

Let's start by the end.

Writeable: Allocated + T is not const-qualified, so you can assign to *p.

That's \valid

Readable: Allocated + the bytes represent a valid, non-trap, value of the type. Hence *p can be read.

That's supposed to be \valid_read(p) && \initialized(p) && ! \dangling(p)

ACSL has no way to talk about other trap representations because no modern architecture has them.

Allocated: Valid + points to allocated memory. I.e., all sizeof(T) bytes are inside a live object.

That's \valid_read.

Valid: can be used in pointer arithmetic, equality and inequality. Cannot necessarily be used as argument of dereference operator.

That one is trickier, and is insufficiently axiomatized in ACSL right now. (Although things like "past-one" pointers can be described using \valid_read and pointer arithmetic, the latter being always ok in ACSL's total logic.)

To give you a datapoint, the Eva plugins emits warnings on pointers such as int x; int *p = &x + 2 as soon as p is used, even if it is not dereferenced.

[sfsiegel]

Thanks, Boris.
Question: doesn't \valid(p) imply !\dangling(p) ?

[khoroshilov]

It seems to me there are at least 4 different classes of pointer values one would like to specify with predicates. These may not be the appropriate names, but here is the idea...

Valid: can be used in pointer arithmetic, equality and inequality. Cannot necessarily be used as argument of dereference operator.

Allocated: Valid + points to allocated memory. I.e., all sizeof(T) bytes are inside a live object.

Readable: Allocated + the bytes represent a valid, non-trap, value of the type. Hence *p can be read.

Writeable: Allocated + T is not const-qualified, so you can assign to *p.

And what is about alignment?

[yakobowski]

@sfsiegel Unfortunately, the current \dangling predicate is the source of endless confusion, and we just had an instance of it.

\dangling(p) means that the memory location pointed to by p, assuming it is valid, contains the bit-pattern of a pointer that is now dangling [1]. Confusingly, it does not mean that p is dangling. This notion does not exist as such as ACSL, because it is not possible to talk about indeterminate values -- only about locations containing indeterminate values.

This is why I put \initialized and \dangling at the same level. Basically, if you accept that your types do not contain trap representations, a location pointed to by p can contain indeterminate values only if !\initialized(p) || \dangling(p).

[1] And so, in practice, p very often has type pointer to pointer. This is unlike the arguments of \initialized, which can be "simple" pointers.

To give an example:

int *p;
int *q = &p;
{
  int x;
  p = &x;
}
//@ assert \dangling(q);  // Holds
//@ assert \dangling(&p); // Holds
//@ assert \valid(p); // Does not have a truth value, because p is no longer a pointer value.

@khoroshilov ACSL does not currently impose alignment requirement on pointers, which is a known defect indeed.

[claudemarche]

Please see issue #83