Abstract Predicate Definition

In the first view chapters of this volume (Verif_stack, Verif_triang, etc.) we demonstrated all-in-one-file C programs, and we used a form of malloc_token with the type,

That is, malloc_token takes an implicit compspecs argument, and the interpretation of the type argument depends on the compspecs. Basically, the malloc_token needs to know how many bytes the malloc'd record is, so it needs the compspecs in order to interpret the type. But now we are doing modular C programming, in which each .c file can have its own struct and union types -- that is, its own compspecs. Our malloc_token with a compspecs parameter cannot assume that every module will have the same compspecs. For modular programming, we'll start with a more primitive form, malloc_token_sz, that just depends on the size of the object, of type Z. No compspecs required. Later in this file, we show how to recover the type-based malloc_token within each module. In the memory-manager APD we have two abstract predicates, mem_mgr and malloc_token. The predicate mem_mgr represents the state of the memory manager's free list. That is, when you call free(p) you might imagine that the memory-block at address p gets added back into a free list (or some other data structure), and when you call malloc(n) then it takes a block from the free list. Since the internal representation of the free list is private to this module (stdlib), it's an abstract predicate.

Abstract Specification Interface

As usual, build a Section to parameterize the interface by the APD:

Specification of malloc has the same issue with compspecs that we discussed above for malloc_token: That is, we need the ASI to be independent of any particular module's struct/union declarations. So we will define malloc_spec_sz which is a size-based, not type-based, specification.

Of course the exit system call is not really part of the malloc/free library, but this is a convenient place to put its specification.

And now we can construct the ASI, which (as usual) is just a list of (APD-parameterized) funspecs.

Type-based specification of malloc and free

Of course, it is much easer for the user to use a funspec for malloc whose postcondition has a data_at_ of the right type. So here we will define an alternate malloc_token and malloc_spec that uses compspecs and types.

How to use the type-based malloc_spec

Both malloc_spec_sz and malloc_spec are specifications of the same malloc function, so any given program (.c file) can be verified using either of the specs. However, since the ASI provides malloc_spec_sz, then in order to use malloc_spec in the verification of the client, one must do forward_call with the (optional) funspec_sub argument. Here we prove that (for any compspecs), malloc_spec_sz implies malloc_spec.

Now, the pattern for using malloc_spec will be as shown in VSU_stack, like this: forward_call (malloc_spec_sub M t) gv forward_call (free_spec_sub M (Tstruct _cons noattr)) (q, gv) It works like this: t (or, for example, Tstruct _cons noattr) is any type of the client's choosing, interpreted using the client's own compspecs. forward_call looks up malloc in the imported ASIs (that is, in the Gprog), and finds malloc_spec_sz as its specification. Then it uses the funspec_sub proof to adapt the spec into malloc_spec M {cs} t, where the cs argument is instantiated using the client's compspecs, as desired. And similarly for free.

Next Chapter: VSU_stack