Symbolic execution states

A symbolic execution state consists of the following components:

• A symbolic store, mapping each local variable name in scope whose address is not taken to a term representing its current value, and each local variable in scope whose address is taken to a term representing a pointer to the variable.
• A symbolic heap, a multiset of heap chunks representing the resources owned by the code being verified. Note: "symbolic heap" and "heap chunk" are slightly misleading names, because ownership of non-heap resources, such as global variables or stack-allocated variables whose address is taken¹, is also represented as "heap chunks"; more accurate names would have been "symbolic multiset of owned resources" and "chunk of resource".
• A path condition, a set of formulae (terms of type bool) encoding the assumptions made about the symbols used on the current symbolic execution path.

These components are shown in the Locals pane, the Heap chunks pane, and the Assumptions pane of the VeriFast IDE, respectively.

A heap chunk consists of the following components:

• The chunk's coefficient: a term representing a real number. In case of an application of a built-in predicate representing a region of memory, the coefficient is always greater than zero and not greater than one. If the coefficient equals one, it's a full chunk denoting read/write access; otherwise, it's a fractional chunk denoting read-only access. In case of a user-defined predicate, the meaning is given by distributing the multiplication by the coefficient over the separating conjunctions in the predicate's body. If a chunk's coefficient is the literal term 1, it is not shown in the VeriFast IDE.
• The chunk's predicate: a term representing a predicate value. When processing a predicate definition, VeriFast allocates a fresh predicate symbol to represent the predicate; also, each predicate constructor is associated with a function symbol mapping a predicate constructor argument list to a predicate value.
• The chunk's type arguments, a list of types with which to instantiate the predicate's type parameters.
• The chunk's arguments, a list of terms with which to instantiate the predicate's parameters.
• Optionally, the chunk's size. This is only potentially present when verifying a lemma function whose precondition's first separating conjunct is a predicate assertion. In that context, chunks derived from the first chunk produced by the lemma function's precondition through N open operations have size -N. This component is used to verify termination of lemma functions defined by induction on the derivation of the precondition's first chunk.

A predicate is either built-in or user-defined. All built-in predicates are declared in the prelude, in bin/rust/prelude.rsspec, or are automatically generated by VeriFast when it processes certain declarations. The most important ones are the following:

• pred points_to_<T>(p: *T, v: option<T>): a chunk points_to_::<T>(p, v) denotes ownership of a variable of type T pointed to by properly aligned pointer p. If v is some(V), the variable is initialized and holds value V; otherwise, it is uninitialized. Since the points-to chunk for a variable is consumed when the variable is deallocated, ownership of a points-to chunk implies that the pointer is non-dangling.
• pred points_to<T>(p: *T, v: T): equivalent to points_to_::<T>(p, some(v)).
• pred array_<T>(p: *T, n: i32, vs: list<option<T>>): a chunk array_::<T>(p, n, vs) denotes ownership of an array of n components of type T, pointed to by properly aligned pointer p. List vs of length n holds each component's value, if it is initialized, or none if it is not.
• pred array<T>(p: *T, n: i32, vs: list<T>): denotes ownership of a fully initialized array.
• When processing a definition of a struct S with fields F1: T1 through Fn: Tn, VeriFast introduces field predicates pred S_F1_(p: *S, v: option<T1>) = points_to_::<T1>(&(*p).F1, v) and pred S_F1(p: *S, v: T1) = points_to::<T>(&(*p).F1, v) through S_Fn_ and S_Fn, as well as a padding predicate pred struct_S_padding(p: *S).