Zeroing memory

Coordinator
Aug 12, 2009 at 9:50 PM

We currently have no good solution to specify (and verify) a function "void
zero(void *addr, unsigned size);" that is meant to be called in at least the
following contexts: (i) to zero out subranges of arrays of integer-types
elements ("zero(A+i,j*sizeof(*A))", where "mutable(as_array(A+i,j))" may NOT
always be known) and (ii) to zero a struct ("zero(S,sizeof(*S))").

Currently, memory reinterpretation does not help with both use cases, since it
assumes object roots and is currently not value-preserving.  Without these
limitations, memory reinterpretation could work, but would have to be tied to
the call in order not violate any typing invariant (maybe something similar to
the marker-based solution for guaranteeing call order in custom admissibility
checks).

Without memory reinterpretation, use case (ii) can also be solved by making
"zero()" generic and adding an "extent_zero()" predicate (applicable to
non-primitive pointers), similar to ye olde "region_zero" from VCC1.  Generics
with "extent_zero" don't work so well with use case (i), though, because it
would be convenient if the subrange would not have to be an object (although,
memory reinterpretation might help but requires additional annotation effort at
the call site).  One way around this would be to specify alternative contracts
of "zero" according to type, i.e.,  ensures "extent_zero" for non-primitive
types, and ensure chunk of (properly typed) zeroes for the different integer
types.  Certainly quite elaborate.

During the phone call, Ernie sketched an alternative to generics that might be
applicable; this will probably be the topic of another discussion.

Comments? Other ideas?

Coordinator
Aug 14, 2009 at 9:13 PM

I guess verifying the implementation of zero(…) is not of crucial importance right now (it’s probably assembly anyhow).

The contract I would see is:

void zero<T>(void *p, unsigned sz)

  writes(array_range((T*)p, sz/sizeof(T)))

  maintains( forall(unsigned i; 0 <= i && i < sz/sizeof(T); extent_mutable((T*)p + i))

  ensures( forall(unsigned i; 0 <= i && i < sz/sizeof(T); extent_zero((T*)p + i));

and probably folding into a simpler version when sz==sizeof(T) (i.e., use sz==sizeof(T) ==> ... in contracts).

Note that the array_range(...) does not require as_array(...), and moreover, it should also work for sz==sizeof(T), maybe a bit less efficiently.

To express this we would only need the extent_zero(...) predicate, that would also be defined for primitive types.

Michal

Coordinator
Aug 14, 2009 at 10:27 PM

Yes, the spec issue is more important right now than the verification issue (there are C functions that need a similar thing in the ensures() clause, modulo the array thing).

A requires(sz%sizeof(T)==0) should be added to the contract.

In addition to extent_zero(), sizeof(T) doesn't work currently in writes() clauses (a left-over from CP:2363), and I stumbled on pure generic function not working. I'll make issues for those.

Thanks, Mark

 

 

Coordinator
Aug 26, 2009 at 8:43 PM

Now, the following is working:

#include "vcc.h"

#ifdef VERIFY
template<typename T>
#endif
void
zero(void *p, unsigned sz)
    requires(sz && sz%sizeof(T)==0)
    writes(array_range((T*)p, sz/sizeof(T)))
    requires(is_non_primitive_ptr((T*)p)) // Note: extent_zero() doesn't work yet for primitive types
    maintains(forall(unsigned i; i < sz/sizeof(T); extent_mutable((T*)p + i)))
    ensures(forall(unsigned i; i < sz/sizeof(T); extent_zero((T*)p + i)))
    ;

struct S { int a; };

void foo() {
    struct S s;
    generic_instance(zero,<struct S>)(&s, sizeof(s));
    //assert(extent_mutable(&s));
    assert(extent_zero(((struct S*)((void*)&s))+0)); // why's that one needed?
    assert(s.a==0);
}

void foo5() {
    struct S s[5];
    generic_instance(zero,<struct S>)(s, sizeof(s));
    assert(extent_mutable(&s));
    assert(s[1].a==0);
}

There are no folded contracts for sz==sizeof(T). Also extent_zero() is not completely implemented yet.

There is a some triggering issue (see the assert in foo()). In contrast to extent_zero(), it works fine for extent_mutable(). I guess this is due to the latter appearing in the precondition and therefore getting enough implicit triggering already. (Folding the contracts would solve that anyway).

Coordinator
Aug 27, 2009 at 8:35 AM
You may add:
ensures(sz >= sizeof(T) ==> extent_zero((T*)p))

I think it would make it work.
Coordinator
Aug 27, 2009 at 9:17 AM

Well, yes, ensures(extent_zero((T*)p) works (we have sz!=0 before). I was trying to investigate needs extra triggering compare to mutability (or writability, really). I did a test assignment after the call and cut out some stuff from the state before the call, but couldn't find anything that explains the difference yet. It's no biggie of course, it's just an instance of "you do A' to achieve goal A, but if you do B' for a seemingly similar goal B, then you also have to do B'' to make it work" :)

Developer
Oct 17, 2009 at 8:18 AM

I don't remember what I proposed over the phone, but here is another suggestion.

What bothers me here is the use of a template, because we already have a polymorphism mechanism (maps can simulate even predicate types). How about instead passing a set of pointers?

Zero would take just a memory range and a set of pointers, requiring that these pointers are mutable and that they cover all of the bytes being written.

Coordinator
Oct 17, 2009 at 9:21 AM

Can you elaborate on what the writes() clause of zero() would look like (i.e., where the conversion between writable client type and writable bytes would happen) and how / where the zeroed bytes are converted to the client type?