stack2.c

The module stack2.c is slightly adjusted from stack.c; it uses an internal function surely_malloc, just to illustrate how to handle local functions that are not exported in the ASI module interface.

    #include <stddef.h>
    #include "stdlib.h"
    #include "stack2.h"

    struct cons { int value; struct cons *next; };

    struct stack { struct cons *top; };

    void *surely_malloc (size_t n) {
      void *p = malloc(n);
      if (!p) exit(1);
      return p;
    }

    struct stack *newstack(void) {
      struct stack *p;
      p = (struct stack * ) surely_malloc(sizeof (struct stack));
      p->top = NULL;
      return p;
    }

    void push (struct stack *p, int i) {
      struct cons *q;
      q = (struct cons * ) surely_malloc(sizeof (struct cons));
      q->value = i;
      q->next = p->top;
      p->top = q;
    }

    int pop (struct stack *p) {
      struct cons *q;
      int i;
      q = p->top;
      p->top = q->next;
      i = q->value;
      free(q);
      return i;
    }

Building the VSU

Now we can verify the implementations of the individual modules. That is, for each module, we produce a VSU, a Verified Software Unit. Each of these verifications imports only ASIs (abstract specification interfaces), not other VSUs; that is, the verification of a module depends only on interfaces, not on the implementations (or verifications) of other modules. We start by importing floyd.proofauto, as usual, but also the floyd.VSU support.

Next, we import the ASIs of the imported modules, and of this module. Since stack2.c uses the malloc/free library (exported from our stdlib module), we import Spec_stdlib as well as Spec_stack.

Next, as usual we import a C program file (as parsed by clightgen). But we can import just this module:

CompSpecs stands for "composite specifications", that is, CompCert's description of the struct and union types defined in this module. The different modules of a program, that is, the different .c files that will be linked together, may have different structs and unions. Here we process the compspecs of this module. Here, prog is really VC.stack2.prog.

Recall that our ASIs are parameterized by the APDs they use; and we used a Section for that purpose in Spec_stack. The StackASI was parameterized by (M: MallocFreeAPD) and (STACK: StackAPD). The Stack VSU will use the same two APDs. As before, M will be a parameter. But STACK will not be a parameter: we will build and instantiate that APD in this verification. So our Section Stack_VSU is only for the purpose of parameterizing by M.

First, instantiate the APD

Now it's time to build an instance of StackAPD. To do that, we need to construct the same stack mpred that we constructed in Verif_stack. In this exercise, you will paste in your solutions to the corresponding exercises in Verif_stack, leading up to the definition of a StackAPD.

Exercise: 2 stars, standard (STACK)

Now we can construct STACK, an instance of StackAPD, by gluing together the stack predicate with the two lemmas about it.

Internal functions

Each internal function needs a funspec. Unlike the exported functions, whose funspecs go in the ASI (such as Spec_stack), funspecs for internal functions go here in the VSU.

Constructing Vprog and Gprog

Imports of a VSU is just the concatenation of all the ASIs of the modules that it's importing:

Privates of a module are the funspecs of locally defined functions that are not to be exported for client use

Internals are just the Privates and the other internal funspecs. IF the module does not re-export any imported functions, then that's just the same as the Privates plus the Exports, as shown here:

Gprog is the basis on which to prove each semax_body; it is always the Imports plus the Internals

For every module except Main, the Vprog is computed as,

Proofs of the function bodies

Exercise: 2 stars, standard (stack_bodies)

Copy and adapt these proofs from Verif_stack.

Construction of the VSU

Programs that do input/output need an "External Specification" (or Espec) that characterizes the interaction. All the VSUs of the program must use the same Espec. Since this program doesn't do any I/O, it can use the standard trivial Espec, as follows:

Notice that all the semax_body proofs above didn't depend at all on which Espec we use, so they're portable to any Espec. That wouldn't be true if some of them did I/O. To construct the StackVSU, we first define its type, as follows:

That is,

• nil, the Externs of this module;
• Stack_imports, the Imports of this module;
• prog, the program of this module, but transformed into a QP.program by the QPprog tactic;
• StackASI, the Exports of this module;
• emp is the global-variable specifier, since this implementation of the stack module has no global variables of its own.

Having specified the StackVSU lemma, we now prove it. The mkVSU line has two arguments: The C program (stack2.prog), and the Internals (that were not mentioned in the type of the VSU). Then, there is one subgoal for each function-body defined in the .c file. In each subgoal, solve_SF_internal solves the goal, using the appropriate semax_body lemma that you have proved.

How do you know which semax_body proof to supply for each subgoal? It's easy -- the subgoal has the form, SF Gprog name fundef funspec, where in this case name is _surely_malloc and fundef is Internal f_surely_malloc, so it's pretty clear that body_surely_malloc is what we want to provide here.

Next Chapter: VSU_triang