Complaints by the C compiler

  • What does the error "C requires that a struct or union has at least one member" mean? - According to the C standard, struct and unions have to have at least one field. Possibly, you have tried to define a real struct that just has ghost fields - these ghost fields are not seen by the C compiler. If you actually need a structure with no real fields, make the struct a ghost struct by putting spec() around it.

Ownership

  • What does open and closed mean? - When an object o is closed, this implies that its invariant holds and that its non-volatile fields do not change. When an object is opened, its invariant can be temporarily violated. Only when the invariant has been re-established, the object can be closed again.
  • Why do I have to wrap and unwrap objects? - Non-volatile fields of an object can only be changed when the object is 'open'. unwrap(o) will move an object from the closed to the opened state, wrap(o) will move it back to the closed state.
  • How can primitive global variables be owned? - Usually, things of primitive type cannot be owned. Thus, you cannot directly own a primitive global variable, e.g., to state an invariant over it. VCC, however, implicitly embeds primitive global variable into global structs. Using the embedding of the global variable (the gemb() function), this implicit structure can be referred to. An invariant invariant(keeps(gemb(&globalvar))) can thus be stated (cf. below about invariants).
  • How can I have different owners for different fields of a struct? - Non-primitive struct fields can have separate owners because they are not part of a span of an object. If non-primitive fields of a struct are required to have separate owners, the struct needs to be split up into so-called 'groups'. Groups can be declared with the def_group() construct; individual fields can be associated with groups using the in_group() type specifier. See Groups for more information.
  • How do I refer to an object B in the invariant of an object A? - There are no inherent limitations about what objects can appear in an object invariant. However, nontrivial use of an unrelated object is likely to result in an invariant that is inadmissible. Typically, A has to either own or have a claim on the object B (or an object whose invariant guarantees that B is closed).
  • What the heck are claims? - Claims are a way to have guarantees about objects that you do not own. A claim on an object A guarantees at least its closedness, therefore it always guarantees object A's single-state invariant. Additionally, one can refer to the values of the non-volatile fields of A at the time that the claim was made and all times afterwards until it is disposed.

Invariants

  • What does the message Verification of $admissibility_TYPE failed mean? - In the sequential setting, the invariant of an object o can only depend on the sequential ownership domain of o, i.e., the objects that are (transitively) owned by o. In the (more general) concurrent setting, it should be not possible to break the invariant of o by changing some closed objects, as long as those changes preserve those objects invariants. VCC checks for this property, which is called admissibility of the invariant. When such a check fails for a type, you will get the aforementioned error message.
  • How can invariants over global variables of primitive type be stated? - Invariant can only be formulated inside a struct declaration. Therefore, to talk about invariants of global primitive variables, a ghost struct has to be created, in which the invariant is stated:
#include <vcc.h>

int global;

spec(struct vcc(claimable) _GlobalOwner {
  int dummy; // have at least one real field, cf. below
  invariant(global == 10)
  invariant(keeps(gemb(&global))) // gemb() hack, cf. above
} GlobalOwner;)
  • Why doesn't VCC verify admissibility for a struct type that I defined? - Possibly, you have defined a ghost struct without a field, e.g., stating an invariant over a global variable (cf. above). However, if a ghost structure has no field, VCC won't generate Boogie code for it and, hence, no admissibility check.
  • What is the purpose of two-state invariants? - Two-state invariants talk about two consecutive 'machine states', as caused by an atomic update. Two-state invariants need to be maintained during atomic updates on volatile fields of closed objects. The primary motivation for 2-state invariants are to define abstract automata (such as virtual machines) and to construct simulation proofs. A typical pattern is to define the abstract behavior of an object with 2-state invariants on its spec fields, to couple this abstract state to the concrete state with a (1-state) coupling invariant, and to provide with each volatile update to the concrete state a corresponding update to the abstract state (in the same atomic action); this update to the spec state "witnesses" the simulation.
  • For two-state invariants inv2(s1, s2), does inv2(s1, s1) have to hold? - Yes. This is enforced during admissibility checks with the so called stuttering conditions.
  • What does old mean in invariants? - In a two-state invariant, old(e) refers to the value of e in the first state. Expressions without old are evaluated with respect to the second state. This is only meaningful for volatile fields because non-volatile fields for closed objects do never change in two consecutive states.

Volatile fields

  • What is the meaning of the volatile specifier in VCC? - VCC treats volatile fields of a structure different from non-volatile fields. Volatile fields are intended for fields that are updated concurrently by multiple threads. In particular, volatile fields of an object can be changed while the object is closed. Yet, they can only be changed by atomic writes, which must maintain the two-state invariant of the object.
  • Why can a writes-clause on a volatile field make my state inconsistent? - A writes clause implies that the object to be written is mutable at the time of the write. Volatile fields, however, are often used inside structures that stay closed in order for the two-state-invariants to be checked by VCC. Thus, writing to a volatile field in a closed structure can make the state inconsistent when you have a writes-clause on the volatile field.
  • How can I verify updates on atomic fields? - Every update on a volatile field must be surrounded by an atomic-block. Essentially, this block tells the prover to check the invariants that may be affected by the update. An atomic-block may contain at most one update of a volatile of the 'real code'. However, you can make as many updates to volatile ghost fields as you wish.

Claims

  • Why can I invalidate the properties my claim claims? A common misunderstanding is that a claim acts like a two-state-invariant on volatile objects that are mentioned in the claim, and thus, validity of the claim would be checked whenever you modify one of the volatile objects. However, this is not the case. A claim can be a way for you to apply existing two-state-invariants in your proofs. All properties you list in your claim must actually be supported by two-state-invariants over all state transitions that can happen, the claim must be "stable". Stability of a claim is currently only checked at the time of creation of the claim, so problems with instable claims often arise when you assume the existence of claims in invariants or in preconditions of functions.

Complaints by VCC

  • What does the error "Call 'stack_free(&a)' did not verify." mean? For local variables, VCC will insert verification conditions, that the variables are mutable when the function returns. This is to make sure that the stack frame of the function (where the local variables live) can be safely destroyed when the function is left. If VCC cannot show that the variable is "free" in this sense, VCC will give the above error. In the below example, this error arises for the variable a in the function bar(), since after calling foo() variable a is not known to be mutable. This can be fixed by adding the appropriate postcondition to foo() (or using weak_out_param or out_param instead).
#include <vcc.h>

struct A {
    int a;
};

void foo(struct A *a)
    // Missing: ensures(mutable(a))
    writes(a);

void bar() { // fails stack_free check for a
    struct A a;
    foo(&a);
}

Last edited Dec 28, 2011 at 2:18 PM by erniecohen, version 13

Comments

No comments yet.