Verif_stackStack ADT implemented by linked lists
#include <stddef.h> extern void * malloc (size_t n); extern void free (void *p); extern void exit(int n); struct cons { int value; struct cons *next; }; struct stack { struct cons *top; }; struct stack *newstack(void) { struct stack *p; p = (struct stack * ) malloc (sizeof (struct stack)); if (!p) exit(1); p->top = NULL; return p; } void push (struct stack *p, int i) { struct cons *q; q = (struct cons * ) malloc (sizeof (struct cons)); if (!q) exit(1); 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; }
- To create a new stack, st = newstack();
- To push integer i onto the stack, push(st,i);
- To pop from the stack, i=pop(st);
Let's verify!
Require VC.Preface. (* Check for the right version of VST *)
Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import VC.stack.
#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Require Import VC.hints. (* Import special hints for this tutorial. *)
Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import VC.stack.
#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Require Import VC.hints. (* Import special hints for this tutorial. *)
Malloc and free
+-----------+
| header |
+-----------+
p-->| zero |
+-----------+
| one |
+-----------+
| two |
+-----------+
where in this case, header=3.
- malloc_token Ews p × data_at Ews (Tstruct _mystruct noattr) (zero,one,two) p
+-----------+
| header |
+-----------+
p-->
Of course, the malloc/free library might have a different way
of "remembering" the size that p points to, so its representation
of malloc_token is not necessarily a word at offset -1.
Therefore, clients of the malloc/free library treat malloc_token
as an abstract predicate. Now, the function-specifications of malloc
and free are something like this:
Definition malloc_spec_example :=
DECLARE _malloc
WITH t:type, gv: globals
PRE [ tuint ]
PROP (0 ≤ sizeof t ≤ Int.max_unsigned;
complete_legal_cosu_type t = true;
natural_aligned natural_alignment t = true)
PARAMS (Vint (Int.repr (sizeof t)))
SEP (mem_mgr gv)
POST [ tptr tvoid ] EX p:_,
PROP ()
RETURN (p)
SEP (mem_mgr gv;
if eq_dec p nullval then emp
else (malloc_token Ews t p × data_at_ Ews t p)).
Definition free_spec_example :=
DECLARE _free
WITH t: type, p:val, gv: globals
PRE [ tptr tvoid ]
PROP ()
PARAMS (p)
SEP (mem_mgr gv; malloc_token Ews t p; data_at_ Ews t p)
POST [ Tvoid ]
PROP () RETURN () SEP (mem_mgr gv).
DECLARE _malloc
WITH t:type, gv: globals
PRE [ tuint ]
PROP (0 ≤ sizeof t ≤ Int.max_unsigned;
complete_legal_cosu_type t = true;
natural_aligned natural_alignment t = true)
PARAMS (Vint (Int.repr (sizeof t)))
SEP (mem_mgr gv)
POST [ tptr tvoid ] EX p:_,
PROP ()
RETURN (p)
SEP (mem_mgr gv;
if eq_dec p nullval then emp
else (malloc_token Ews t p × data_at_ Ews t p)).
Definition free_spec_example :=
DECLARE _free
WITH t: type, p:val, gv: globals
PRE [ tptr tvoid ]
PROP ()
PARAMS (p)
SEP (mem_mgr gv; malloc_token Ews t p; data_at_ Ews t p)
POST [ Tvoid ]
PROP () RETURN () SEP (mem_mgr gv).
If your source program says malloc(sizeof(t)), your forward_call
should supply (as a WITH-witness) the C type t.
Malloc may choose to return NULL, in which case the SEP part
of the postcondition is emp, or it may return a pointer,
in which case you get data_at_ Ews t p, and as a free bonus
you get a malloc_token Ews t p. But don't lose that malloc_token!
You will need to supply it later to the free function when
you dispose of the object.
The SEP predicate data_at_ Ews t p is an uninitialized
structure of type t. It is equivalent to,
data_at Ews t (default_val t) p. The default_val is basically
a struct or array full of Vundef values.
Specification of linked lists
This is much like the linked lists in Verif_reverse.
Fixpoint listrep (il: list Z) (p: val) : mpred :=
match il with
| i::il' ⇒ EX y: val,
malloc_token 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.
match il with
| i::il' ⇒ EX y: val,
malloc_token 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.
Proof automation for user-defined separation predicates works better
if you disable automatic simplification, as follows:
As usual, we should populate the Hint databases
saturate_local and valid_pointer
Exercise: 1 star, standard (stack_listrep_properties)
Lemma listrep_local_prop: ∀ il p, listrep il p |--
!! (is_pointer_or_null p ∧ (p=nullval ↔ il=nil)).
!! (is_pointer_or_null p ∧ (p=nullval ↔ il=nil)).
See if you can remember how to prove this; or look again
at Verif_reverse to see how it's done.
(* FILL IN HERE *) Admitted.
#[export] Hint Resolve listrep_local_prop : saturate_local.
Lemma listrep_valid_pointer:
∀ il p,
listrep il p |-- valid_pointer p.
#[export] Hint Resolve listrep_local_prop : saturate_local.
Lemma listrep_valid_pointer:
∀ il p,
listrep il p |-- valid_pointer p.
See if you can remember how to prove this; or look again
at Verif_reverse to see how it's done.
(* FILL IN HERE *) Admitted.
#[export] Hint Resolve listrep_valid_pointer : valid_pointer.
☐
#[export] Hint Resolve listrep_valid_pointer : valid_pointer.
☐
Specification of stack data structure
+-----------+ | token | +-----------+ +--------- p-->| top------+---q-->| linked list... +-----------+ +---------The stack object p points to a header node with one field top (plus a malloc token); the contents of the top field is some pointer q that points to a linked list.
Definition stack (il: list Z) (p: val) :=
EX q: val,
malloc_token Ews (Tstruct _stack noattr) p ×
data_at Ews (Tstruct _stack noattr) q p ×
listrep il q.
Arguments stack il p : simpl never.
EX q: val,
malloc_token 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.
#[export] Hint Resolve stack_local_prop : saturate_local.
Lemma stack_valid_pointer:
∀ il p,
stack il p |-- valid_pointer p.
(* FILL IN HERE *) Admitted.
#[export] Hint Resolve stack_valid_pointer : valid_pointer.
☐
(* FILL IN HERE *) Admitted.
#[export] Hint Resolve stack_local_prop : saturate_local.
Lemma stack_valid_pointer:
∀ il p,
stack il p |-- valid_pointer p.
(* FILL IN HERE *) Admitted.
#[export] Hint Resolve stack_valid_pointer : valid_pointer.
☐
Definition newstack_spec : ident × funspec :=
DECLARE _newstack
WITH gv: globals
PRE [ ]
PROP () PARAMS() GLOBALS(gv) SEP (mem_mgr gv)
POST [ tptr (Tstruct _stack noattr) ]
EX p: val, PROP ( ) RETURN (p) SEP (stack nil p; mem_mgr gv).
Definition push_spec : ident × funspec :=
DECLARE _push
WITH p: val, i: Z, il: list Z, gv: globals
PRE [ tptr (Tstruct _stack noattr), tint ]
PROP (Int.min_signed ≤ i ≤ Int.max_signed)
PARAMS (p; Vint (Int.repr i)) GLOBALS(gv)
SEP (stack il p; mem_mgr gv)
POST [ tvoid ]
PROP ( ) RETURN () SEP (stack (i::il) p; mem_mgr gv).
Definition pop_spec : ident × funspec :=
DECLARE _pop
WITH p: val, i: Z, il: list Z, gv: globals
PRE [ tptr (Tstruct _stack noattr) ]
PROP ()
PARAMS (p) GLOBALS(gv)
SEP (stack (i::il) p; mem_mgr gv)
POST [ tint ]
PROP ( ) RETURN (Vint (Int.repr i)) SEP (stack il p; mem_mgr gv).
DECLARE _newstack
WITH gv: globals
PRE [ ]
PROP () PARAMS() GLOBALS(gv) SEP (mem_mgr gv)
POST [ tptr (Tstruct _stack noattr) ]
EX p: val, PROP ( ) RETURN (p) SEP (stack nil p; mem_mgr gv).
Definition push_spec : ident × funspec :=
DECLARE _push
WITH p: val, i: Z, il: list Z, gv: globals
PRE [ tptr (Tstruct _stack noattr), tint ]
PROP (Int.min_signed ≤ i ≤ Int.max_signed)
PARAMS (p; Vint (Int.repr i)) GLOBALS(gv)
SEP (stack il p; mem_mgr gv)
POST [ tvoid ]
PROP ( ) RETURN () SEP (stack (i::il) p; mem_mgr gv).
Definition pop_spec : ident × funspec :=
DECLARE _pop
WITH p: val, i: Z, il: list Z, gv: globals
PRE [ tptr (Tstruct _stack noattr) ]
PROP ()
PARAMS (p) GLOBALS(gv)
SEP (stack (i::il) p; mem_mgr gv)
POST [ tint ]
PROP ( ) RETURN (Vint (Int.repr i)) SEP (stack il p; mem_mgr gv).
Putting all the funspecs together:
Proofs of the function bodies
Exercise: 2 stars, standard (body_pop)
Lemma body_pop: semax_body Vprog Gprog f_pop pop_spec.
Proof.
start_function.
(* FILL IN HERE *) Admitted.
☐
Proof.
start_function.
(* FILL IN HERE *) Admitted.
☐
Lemma body_push: semax_body Vprog Gprog f_push push_spec.
Proof.
start_function.
forward_call (Tstruct _cons noattr, gv).
(* FILL IN HERE *) Admitted.
☐
Proof.
start_function.
forward_call (Tstruct _cons noattr, gv).
(* FILL IN HERE *) Admitted.
☐
Lemma body_newstack: semax_body Vprog Gprog f_newstack newstack_spec.
Proof.
start_function.
(* FILL IN HERE *) Admitted.
☐
Proof.
start_function.
(* FILL IN HERE *) Admitted.
☐
(* 2023-03-25 11:30 *)