Verifiable C: Getting the front element in a linked list based queue

Using Coq
1

Consider an efficient linked list based implementation of a FIFO queue linked_list_queue.c, achieved by keeping pointers to the both the head and last nodes (labelled front and back respectively) of the linked list so enqueueing at the back of the list can be done in O(1) time:

#include <stddef.h>

extern void *malloc(size_t);
extern void free(void *);
extern void exit(int);

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

struct queue {
  struct node *front;
  struct node *back;
};

void queue_init(struct queue *q) { q->front = q->back = NULL; }

int queue_is_empty(struct queue *q) { return !q->front; }

int queue_front(struct queue *q) { return q->front->value; }

void queue_enqueue(struct queue *q, int value) {
  struct node *t;
  t = (struct node *)malloc(sizeof(struct node));
  if (!t)
    exit(1);
  t->value = value;
  t->next = NULL;
  if (!q->back)
    q->front = q->back = t;
  else
    q->back = q->back->next = t;
}

int queue_dequeue(struct queue *q) {
  int value;
  struct node *t;
  value = q->front->value;
  if (q->front == q->back) {
    free(q->front);
    q->front = q->back = NULL;
    return value;
  }
  t = q->front->next;
  free(q->front);
  q->front = t;
  return value;
}

int main(void) { return 0; }

Here, we are only interested in int queue_front(struct queue *) which simply returns the front item of a nonempty queue.

First, we define a list representation as follows (taken from chapter Verif_stack in Software Foundations Volume 5):

Fixpoint listrep (il: list Z) (p: val) : mpred :=
 match il with
 | i::il' => EX y: val,
        malloc_token Ews (Tstruct _node noattr) p *
        data_at Ews (Tstruct _node noattr) (Vint (Int.repr i),y) p *
        listrep il' y
 | nil => !! (p = nullval) && emp
 end.

Arguments listrep il p : simpl never.

Then we define our queue ADT as follows:

Definition queue (il: list Z) (p: val) :=
  match il with
  | [] => data_at Ews (Tstruct _queue noattr) (nullval, nullval) p
  | (_ :: _) => EX front back : val,
    data_at Ews (Tstruct _queue noattr) (front, back) p *
    (listrep il front && listrep [last il 0] back)
  end.

Arguments queue il p : simpl never.

Our specification for queue_front() is as follows:

Definition queue_front_spec : ident * funspec :=
  DECLARE _queue_front
  WITH q : val, i : Z, il : list Z
  PRE [tptr (Tstruct _queue noattr)]
    PROP () PARAMS (q) SEP (queue (i :: il) q)
  POST [tint]
    PROP () RETURN (Vint (Int.repr i)) SEP (queue (i :: il) q).

And our Gprog:

Definition Gprog : funspecs :=
  ltac:(with_library prog [
    queue_front_spec
  ]).

Now consider the proof of this specification:

Lemma body_queue_front : semax_body Vprog Gprog f_queue_front queue_front_spec.
Proof.
  start_function.
  unfold queue; unfold listrep; fold listrep.
  Intros front back y y0; subst y0.
  forward.
  - autorewrite with norm.
    assert_PROP (isptr front) by (rewrite (data_at_isptr _ _ _ front);
      entailer!).
    entailer!.
  - autorewrite with norm.
    Fail forward.
    admit.
Admitted.

Before the line Fail forward, we have the following proof context:

1 subgoal
Espec : OracleKind
q : val
i : Z
il : list Z
Delta_specs : PTree.t funspec
Delta := abbreviate : tycontext
POSTCONDITION := abbreviate : ret_assert
front, back, y : val
MORE_COMMANDS := abbreviate : statement
______________________________________(1/1)
semax Delta
  (PROP ( )
   LOCAL (temp _t'1 front; temp _q q)
   SEP (data_at Ews (Tstruct _queue noattr) (front, back) q;
   malloc_token Ews (Tstruct _node noattr) front *
   data_at Ews (Tstruct _node noattr) (Vint (Int.repr i), y) front *
   listrep il y &&
   (malloc_token Ews (Tstruct _node noattr) back *
    data_at Ews (Tstruct _node noattr)
      (Vint (Int.repr (last (i :: il) 0)), nullval) back)))
  (_t'2 = (_t'1->_value);
   MORE_COMMANDS) POSTCONDITION

At the SEP clause, we have temp _t'1 front and data_at ... front where struct node has a value field so I expected to be able to go forward through the assignment _t'2 = _t'1->_value; however, on doing so, I get the following error message:

Tactic failure: 
It is not obvious how to move forward here.  One way:
Find a SEP clause of the form [data_at _ _ _ 
?p
] (or field_at, data_at_, field_at_),
then use assert_PROP to prove an equality of the form
(offset_val 0 front = field_address ?t ?gfs ?p)
or if this does not hold, prove an equality of the form
(front = field_address ?t ?gfs ?p)
, then try [forward] again. (level 990).

Some things I tried:

  • I tried assert_PROP (isptr front) (with success) but this did not help with going forward
  • I did a Search data_at and could not seem to find lemmas relating data_at with offset_val and/or field_address
  • hint only tells me to use deadvars! or try forward

I might be missing something obvious so any hint on how to proceed would be much appreciated (or if I entered a dead end due to incorrect tactics / funspec / etc.).

For reference, here is my minimal reproducible example, simplified to include only the parts relevant to queue_front(). I have not explicitly tested this so feel free to inform me of any compilation errors.

_CoqProject:

-R . Kata
Preloaded.v
Solution.v

Preloaded.v:

(* BEGIN AST *)

(* Elided - please replace with output of [clightgen -normalize linked_list_queue.c] *)

(* END AST *)

Require Import VST.floyd.proofauto VST.floyd.library Coq.Lists.List.
Import ListNotations.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Fixpoint listrep (il: list Z) (p: val) : mpred :=
 match il with
 | i::il' => EX y: val,
        malloc_token Ews (Tstruct _node noattr) p *
        data_at Ews (Tstruct _node noattr) (Vint (Int.repr i),y) p *
        listrep il' y
 | nil => !! (p = nullval) && emp
 end.

Arguments listrep il p : simpl never.

Definition queue (il: list Z) (p: val) :=
  match il with
  | [] => data_at Ews (Tstruct _queue noattr) (nullval, nullval) p
  | (_ :: _) => EX front back : val,
    data_at Ews (Tstruct _queue noattr) (front, back) p *
    (listrep il front && listrep [last il 0] back)
  end.

Arguments queue il p : simpl never.

Definition queue_front_spec : ident * funspec :=
  DECLARE _queue_front
  WITH q : val, i : Z, il : list Z
  PRE [tptr (Tstruct _queue noattr)]
    PROP () PARAMS (q) SEP (queue (i :: il) q)
  POST [tint]
    PROP () RETURN (Vint (Int.repr i)) SEP (queue (i :: il) q).

Definition Gprog : funspecs :=
  ltac:(with_library prog [
    queue_front_spec
  ]).

Solution.v:

Require Import Preloaded VST.floyd.proofauto VST.floyd.library.

Lemma listrep_local_prop: forall il p, listrep il p |--
        !! (is_pointer_or_null p  /\ (p=nullval <-> il=nil)).
Proof. (* spoilers to SF Volume 5 *) Admitted.
#[export] Hint Resolve listrep_local_prop : saturate_local.

Lemma listrep_valid_pointer:
  forall il p,
   listrep il p |-- valid_pointer p.
Proof. (* spoilers to SF Volume 5 *) Admitted.
#[export] Hint Resolve listrep_valid_pointer : valid_pointer.

Lemma queue_local_prop: forall il p, queue il p |--  !! (isptr p).
Proof.
  intros; unfold queue.
  destruct il.
  - entailer!.
  - Intros front back; entailer!.
Qed.
#[export] Hint Resolve queue_local_prop : saturate_local.

Lemma queue_valid_pointer:
  forall il p,
   queue il p |-- valid_pointer p.
Proof.
  intros; unfold queue.
  destruct il.
  - entailer!.
  - Intros front back; entailer!.
Qed.
#[export] Hint Resolve queue_valid_pointer : valid_pointer.

Lemma body_queue_front : semax_body Vprog Gprog f_queue_front queue_front_spec.
Proof.
  start_function.
  unfold queue; unfold listrep; fold listrep.
  Intros front back y y0; subst y0.
  forward.
  - autorewrite with norm.
    assert_PROP (isptr front) by (rewrite (data_at_isptr _ _ _ front);
      entailer!).
    entailer!.
  - autorewrite with norm.
    Fail forward.
    admit.
Admitted.

Using VST version 2.6 with CompCert 3.7

1 Like