fdupress Editor Aug 8, 2011 at 11:28 AM Hi all, I am currently fighting with the verification of some byte array library functions. In particular, I would like to express that these functions can read or write the contents of the arrays passed in as arguments. If specifying the writing is easy (the writes clause takes care of everything), specifying the reads in a generic way is much more of a pain. Indeed, the contents of a byte array can be readable for one of several reasons: all elements are thread local or mutable (\thread_local_array or \mutable_array), the array is a VCC array object and is known to be wrapped (\wrapped(unsigned char[length]) address), the array is contained in a VCC array object that is known to be wrapped (for example \exists size_t l; unsigned char arr; \wrapped((unsigned char[l]) arr) && \subset(\array_members(address,length),\array_members(arr,l)), which causes an OOPS at the moment), the array is (contained in) a VCC array object that is in the ownership domain of a wrapped structure (some variation of the above with an added layer of \embedding (?)), the array is (contained in) a VCC array object that is part of the non-volatile extent of a wrapped structure, possibly a bunch more situations I have not run into yet... My question is: is there any way to generically express that a given memory range can be read, allowing the body of a function to read without proving anything more, and allowing the caller to simply prove any one of the above conditions holds? In cases where the body of the function itself requires the readability to be a bit more strict (for example, if thread locality breaks), additional contracts could be added, but it would be nice to have a default case for simple functions: simple things should be easy... Using a reads clause sounds like the perfect solution from the expressivity and the specification point of view, but it doesn't do anything for non-pure functions, as far as I know. I do realize that all the previous cases can be reduced to case number 1. by unwrapping and reinterpretation, but it would be a pity to write the memory just to prove that you can read from it. I also realize that this may be very specific to arrays of primitive objects, and may not hold for arrays of structures, especially if those structure have volatile fields. I am currently using VCC 2, but am willing to move to VCC 3 is necessary to makes things a bit easier. Also, at the moment, I would be happy to have a solution for 1., 2., 3. and 4. only, as I don't really have any cases of 5. MarkHillebrand Coordinator Aug 11, 2011 at 7:57 PM Hi Francois,   indeed, this is not so easy, although some of your cases collapse. Disregarding the concurrent case, all of the above should be covered by \thread_local_array(a,n). Remember that this is in principle just an abbreviation for \forall unsigned x; x < n ==> \thread_local(&a[x])), which should be sufficient to do the read.   As you note yourself, thread locality is easy to loose, and it becomes more complicated then. The elements may be mutable, or (deep) inside an ownership domain. In the latter case, additional help, in terms of providing witnesses for domain root and embedding of the array elements is required (alternatively, existential quantification of those could work).   At the call site, you have to convince VCC that the accessed elements are indeed thread-local, which requires expanding the ownership domain far enough. (Potentially, \wrapped_with_deep_domain, added in http://vcc.codeplex.com/SourceControl/changeset/changes/096453a32c68, could help, but I haven't tried this yet).   The concurrent case is trickier, because you can't require thread-locality / mutability. Instead, a claims that guarantees the closedness of the embedding has to be passed in, which is clumsy. Also, to make a function work both for the concurrent non-volatile and sequential case, you would currently have to required the disjunction of the versions.   Below I've added some examples; they wouldn't cover all your cases (in particular not the concurrent one), but just to give you an idea. I couldn't yet make the read2() verify with "vcc /2", it verifies with "vcc /3" only. I think it might be the case, that the way that the typestate is encoded with "vcc /2" might prohibit the verification of that functions, but that needs further investigation.   Unfortunately, I don't know of a nicer version of all of that...   Hope that helps, Mark ///newsyntax #include char read1(char *x, unsigned len) _(requires 0 < len) _(requires \thread_local_array(x, len)) _(returns x[len - 1]) { return x[len - 1]; } void call1() { char x[8]; read1(x, 8); } struct S { char x[8]; }; void call2(struct S *s) _(requires \mutable(s)) { read1(&s->x, 8); } void call3(struct S *s) _(requires \wrapped(s)) { read1(&s->x, 8); } struct T { _(as_array) char x[8]; _(invariant \mine((char[8]) x)) }; void call4(struct T *s) _(requires \wrapped(s)) { read1(&s->x, 8); } struct U { struct T t; _(invariant \mine(&t)) }; void call5(struct U *s) _(requires \wrapped(s)) { _(assert &s->t \in \domain(s)) // multiple assertions like this are needed for more deeply nested ownership domains read1(&s->t.x, 8); } void call6(char *x, unsigned len) _(requires 0 < len) _(requires \wrapped((char[len])x)) { read1(x, len); } void call7(char *x, unsigned len) _(requires 0 < len) _(requires \wrapped((char[len+2])x)) { read1(x + 1, len); } struct Unrelated { int x; } Unrelated; void write_unrelated() _(writes &Unrelated); // This one requires /3 // Note: this doesn't specify the mutable alternative... char read2(char *x, unsigned len _(ghost \object embedding) _(ghost \object root)) _(requires \wrapped(root)) _(requires embedding \in \domain(root)) _(requires embedding == \embedding(x)) _(requires &Unrelated != root) _(writes &Unrelated) _(requires 0 < len) _(requires \thread_local_array(x, len)) _(returns *x) { // All of these hold: //_(assert root \in \domain(root)) //_(assert \non_primitive_ptr(root)) //_(assert \non_primitive_ptr(embedding)) write_unrelated(); return *x; } void call8(struct S *s) _(requires \wrapped(s)) _(writes &Unrelated) { read2(&s->x, 8 _(ghost s) _(ghost s)); } /* Verification of T#adm succeeded. Verification of U#adm succeeded. Verification of read1 succeeded. Verification of call1 succeeded. Verification of call2 succeeded. Verification of call3 succeeded. Verification of call4 succeeded. Verification of call5 succeeded. Verification of call6 succeeded. Verification of call7 succeeded. Verification of read2 succeeded. */ ` fdupress Editor Aug 11, 2011 at 8:38 PM Thanks Mark. I started to dive a bit in the Boogie definitions after posting and realized that my initial idea was wrong (I originally thought that thread_local required the object to be open). I didn't even want to think about the concurrent case, but I guess the least I can do in exchange for your help is explore it a bit and come back later with what I find down there :) Thanks again, Francois