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
#[export] 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 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.
- 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.
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
(* 2023-03-25 11:30 *)