# VSU_stackVSU verification of the Stack module

## 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.
Require Import VST.floyd.proofauto.

Require Import VST.floyd.VSU.

Require Import VST.floyd.VSU.

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:

Require Import VC.stack2.

*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

#### Exercise: 2 stars, standard (STACK)

Fixpoint listrep (il: list Z) (p: val) : mpred :=

match il with

| i::il' ⇒ EX y: val,

malloc_token M Ews (Tstruct _cons noattr) p ×

data_at Ews (Tstruct _cons noattr) (Vint (Int.repr i),y) p ×

listrep il' y

| nil ⇒ !! (p = nullval) && emp

end.

Lemma listrep_local_prop: ∀ il p, listrep il p |--

!! (is_pointer_or_null p ∧ (p=nullval ↔ il=nil)).

(* FILL IN HERE *) Admitted.

Local Hint Resolve listrep_local_prop : saturate_local.

Lemma listrep_valid_pointer:

∀ il p,

listrep il p |-- valid_pointer p.

(* FILL IN HERE *) Admitted.

Local Hint Resolve listrep_valid_pointer : valid_pointer.

Definition stack (il: list Z) (p: val) :=

EX q: val,

malloc_token M Ews (Tstruct _stack noattr) p ×

data_at Ews (Tstruct _stack noattr) q p ×

listrep il q.

Arguments stack il p : simpl never.

Lemma stack_local_prop: ∀ il p, stack il p |-- !! (isptr p).

(* FILL IN HERE *) Admitted.

Local Hint Resolve stack_local_prop : saturate_local.

Lemma stack_valid_pointer:

∀ il p,

stack il p |-- valid_pointer p.

(* FILL IN HERE *) Admitted.

Local Hint Resolve stack_valid_pointer : valid_pointer.

☐

match il with

| i::il' ⇒ EX y: val,

malloc_token M Ews (Tstruct _cons noattr) p ×

data_at Ews (Tstruct _cons noattr) (Vint (Int.repr i),y) p ×

listrep il' y

| nil ⇒ !! (p = nullval) && emp

end.

Lemma listrep_local_prop: ∀ il p, listrep il p |--

!! (is_pointer_or_null p ∧ (p=nullval ↔ il=nil)).

(* FILL IN HERE *) Admitted.

Local Hint Resolve listrep_local_prop : saturate_local.

Lemma listrep_valid_pointer:

∀ il p,

listrep il p |-- valid_pointer p.

(* FILL IN HERE *) Admitted.

Local Hint Resolve listrep_valid_pointer : valid_pointer.

Definition stack (il: list Z) (p: val) :=

EX q: val,

malloc_token M Ews (Tstruct _stack noattr) p ×

data_at Ews (Tstruct _stack noattr) q p ×

listrep il q.

Arguments stack il p : simpl never.

Lemma stack_local_prop: ∀ il p, stack il p |-- !! (isptr p).

(* FILL IN HERE *) Admitted.

Local Hint Resolve stack_local_prop : saturate_local.

Lemma stack_valid_pointer:

∀ il p,

stack il p |-- valid_pointer p.

(* FILL IN HERE *) Admitted.

Local Hint Resolve stack_valid_pointer : valid_pointer.

☐

# Internal functions

Definition surely_malloc_spec :=

DECLARE _surely_malloc

WITH t:type, gv: globals

PRE [ size_t ]

PROP (0 ≤ sizeof t ≤ Ptrofs.max_unsigned;

complete_legal_cosu_type t = true;

natural_aligned natural_alignment t = true)

PARAMS (Vptrofs (Ptrofs.repr (sizeof t))) GLOBALS (gv)

SEP (mem_mgr M gv)

POST [ tptr tvoid ] EX p:_,

PROP ()

RETURN (p)

SEP (mem_mgr M gv; malloc_token M Ews t p × data_at_ Ews t p).

DECLARE _surely_malloc

WITH t:type, gv: globals

PRE [ size_t ]

PROP (0 ≤ sizeof t ≤ Ptrofs.max_unsigned;

complete_legal_cosu_type t = true;

natural_aligned natural_alignment t = true)

PARAMS (Vptrofs (Ptrofs.repr (sizeof t))) GLOBALS (gv)

SEP (mem_mgr M gv)

POST [ tptr tvoid ] EX p:_,

PROP ()

RETURN (p)

SEP (mem_mgr M gv; malloc_token M Ews t p × data_at_ Ews t p).

## Constructing Vprog and Gprog

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.
Lemma body_pop: semax_body Stack_Vprog Stack_Gprog f_pop (pop_spec M STACK).

Proof.

start_function.

simpl stackrep.

(* FILL IN HERE *) Admitted.

Lemma body_push: semax_body Stack_Vprog Stack_Gprog f_push (push_spec M STACK).

Proof.

start_function.

simpl stackrep.

forward_call (Tstruct _cons noattr, gv).

(* FILL IN HERE *) Admitted.

Lemma body_newstack: semax_body Stack_Vprog Stack_Gprog f_newstack (newstack_spec M STACK).

Proof.

start_function.

(* FILL IN HERE *) Admitted.

Lemma body_surely_malloc: semax_body Stack_Vprog Stack_Gprog f_surely_malloc surely_malloc_spec.

Proof.

start_function.

forward_call (malloc_spec_sub M t) gv.

(* FILL IN HERE *) Admitted.

☐

Proof.

start_function.

simpl stackrep.

(* FILL IN HERE *) Admitted.

Lemma body_push: semax_body Stack_Vprog Stack_Gprog f_push (push_spec M STACK).

Proof.

start_function.

simpl stackrep.

forward_call (Tstruct _cons noattr, gv).

(* FILL IN HERE *) Admitted.

Lemma body_newstack: semax_body Stack_Vprog Stack_Gprog f_newstack (newstack_spec M STACK).

Proof.

start_function.

(* FILL IN HERE *) Admitted.

Lemma body_surely_malloc: semax_body Stack_Vprog Stack_Gprog f_surely_malloc surely_malloc_spec.

Proof.

start_function.

forward_call (malloc_spec_sub M t) gv.

(* FILL IN HERE *) Admitted.

☐

# Construction of the VSU

Existing Instance NullExtension.Espec.

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,
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

- 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.

*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.
Proof.

mkVSU prog Stack_internals.

+ solve_SF_internal body_surely_malloc.

+ solve_SF_internal body_newstack.

+

mkVSU prog Stack_internals.

+ solve_SF_internal body_surely_malloc.

+ solve_SF_internal body_newstack.

+

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

(* 2021-08-11 15:21 *)