diff --git a/src/examples/queue.broken.c b/src/examples/queue.broken.c index 668aa923..b09c8b8a 100644 --- a/src/examples/queue.broken.c +++ b/src/examples/queue.broken.c @@ -20,13 +20,13 @@ struct int_queueCell { }; /*@ -predicate (datatype seq) IntQueue(pointer q) { +predicate (datatype seq) IntQueue (pointer q) { take H = Owned(q); take Q = IntQueue1(q,H); return Q; } -predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) { +predicate (datatype seq) IntQueue1 (pointer dummy, struct int_queue H) { if (is_null(H.head) || is_null(H.tail)) { assert (is_null(H.head) && is_null(H.tail)); return (Seq_Nil{}); @@ -81,16 +81,6 @@ extern void freeIntQueueCell (struct int_queueCell *p); // ----------------------------------------------------------------- -/*@ -function [rec] (datatype seq) push (datatype seq xs, i32 y) { - snoc (xs, y) -} - -function [rec] (i32) pop (datatype seq xs, i32 y) { - hd (xs) -} -@*/ - struct int_queue* IntQueue_empty () /*@ ensures take ret = IntQueue(return); ret == Seq_Nil{}; @@ -111,38 +101,40 @@ int IntQueue_pop (struct int_queue *q) @*/ { /*@ split_case (*q).head == NULL; @*/ - int x = q->head->first; - if (q->head->next == 0) { + /*@ split_case (*q).tail == NULL; @*/ + // This is needed to unfold IntQueueAux, I guess? + /*@ split_case (*q).head == (*q).tail; @*/ // rewrite to h==t! + struct int_queueCell* h = q->head; + struct int_queueCell* t = q->tail; + /*@ split_case (*h).next == NULL; @*/ + int x = h->first; + // This originally tested for h->next == 0, but this didn't seem to fit the structure of + // the verification; this way works better, at least for the first branch. But would + // it have been possible to verify it the other way? + if (h == t) { + // This line was missing originally -- good pedagogy to fix in stages?? + freeIntQueueCell(h); q->head = 0; q->tail = 0; + return x; } else { - q->head = q->head->next; + struct int_queueCell* n = h->next; + // Needs to deallocate here too! + q->head = n; + freeIntQueueCell(h); + return x; } - return x; + // The return was originally here -- make sure to comment on why it got moved! } -void IntQueue_push (int x, struct int_queue *q) -/*@ requires take before = IntQueue(q); - ensures take after = IntQueue(q); - after == snoc (before, x); -@*/ -{ - struct int_queueCell *c = mallocIntQueueCell(); - c->first = x; - c->next = 0; - if (q->tail == 0) { - /*@ split_case (*q).head == NULL; @*/ - /*@ apply snoc_nil(x); @*/ - // And then this?? Trying random stuff... - /*@ split_case (*q).tail == NULL; @*/ - q->head = c; - q->tail = c; - } else { - // This is needed next: - /*@ split_case (*q).head == NULL; @*/ - // And then this?? Again, random stuff - /*@ split_case (*q).tail == NULL; @*/ - q->tail->next = c; - q->tail = c; - } -} + +// Notes: +// - When I tried /*@ unfold IntQueueAux (H.head, H.tail, T.first); @*/ +// I was confused by "the specification function `IntQueueAux' is not declared". +// I guess this is, again, the distinction between functions and predicates...? +// - Seq_Cons is awkward for several reasons: +// - long / verbose (nothing to do about that, I guess) +// - Seq is capitalized, but it means seq +// - most important part is buried in the middle +// - What are the established C conventions here?? +// - lastVal can be eliminated, I think diff --git a/src/examples/temp-queue3.broken.c b/src/examples/temp-queue3.broken.c new file mode 100644 index 00000000..b5ef478d --- /dev/null +++ b/src/examples/temp-queue3.broken.c @@ -0,0 +1,134 @@ +/* queue.c */ + +#include "list.h" +#include "list_snoc_spec.h" + +/*@ +lemma snoc_nil (i32 foo) + requires true; + ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}}; +@*/ + +struct int_queue { + struct int_queueCell* head; + struct int_queueCell* tail; +}; + +struct int_queueCell { + int first; + struct int_queueCell* next; +}; + +/*@ +predicate (datatype seq) IntQueue (pointer q) { + take H = Owned(q); + take Q = IntQueue1(q,H); + return Q; +} + +predicate (datatype seq) IntQueue1 (pointer dummy, struct int_queue H) { + if (is_null(H.head) || is_null(H.tail)) { + assert (is_null(H.head) && is_null(H.tail)); + return (Seq_Nil{}); + } else { + assert (!is_null(H.head) && !is_null(H.tail)); + take T = Owned(H.tail); + assert (is_null(T.next)); + take Q = IntQueueAux (H.head, H.tail, T.first); + return Q; + } +} + +predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) { + if (h == t) { + return (Seq_Cons{head: lastVal, tail: Seq_Nil{}}); + } else { + take C = Owned(h); + take TL = IntQueueAux(C.next, t, lastVal); + return (Seq_Cons { head: C.first, tail: TL }); + } +} + +@*/ + +// --------------------------------------------------------------------- + +extern struct int_queue *mallocIntQueue(); +/*@ spec mallocIntQueue(); + requires true; + ensures take u = Block(return); + return != NULL; +@*/ // 'return != NULL' should not be needed + +extern void freeIntQueue (struct int_queue *p); +/*@ spec freeIntQueue(pointer p); + requires take u = Block(p); + ensures true; +@*/ + +extern struct int_queueCell *mallocIntQueueCell(); +/*@ spec mallocIntQueueCell(); + requires true; + ensures take u = Block(return); + return != NULL; +@*/ // 'return != NULL' should not be needed + +extern void freeIntQueueCell (struct int_queueCell *p); +/*@ spec freeIntQueueCell(pointer p); + requires take u = Block(p); + ensures true; +@*/ + +// ----------------------------------------------------------------- + +struct int_queue* IntQueue_empty () +/*@ ensures take ret = IntQueue(return); + ret == Seq_Nil{}; +@*/ +{ + struct int_queue *p = mallocIntQueue(); + p->head = 0; + p->tail = 0; + return p; +} + +int IntQueue_pop (struct int_queue *q) +/*@ requires take before = IntQueue(q); + before != Seq_Nil{}; + ensures take after = IntQueue(q); + after == tl(before); + return == hd(before); +@*/ +{ + /*@ split_case (*q).head == NULL; @*/ + /*@ split_case (*q).tail == NULL; @*/ + // This is needed to unfold IntQueueAux, I guess? + /*@ split_case (*q).head == (*q).tail; @*/ + struct int_queueCell* h = q->head; + /*@ split_case (*h).next == NULL; @*/ + int x = h->first; + if (h->next == 0) { + // This line was missing originally -- good pedagogy to fix in stages?? + freeIntQueueCell(h); + q->head = 0; + q->tail = 0; + return x; + } else { + // Needs to deallocate here too! + q->head = h->next; + return x; + } + // The return was originally here -- make sure to comment on why it got moved! +} + + +// Notes: +// - When I tried /*@ unfold IntQueueAux (H.head, H.tail, T.first); @*/ +// I was confused by "the specification function `IntQueueAux' is not declared". +// I guess this is, again, the distinction between functions and predicates...? +// - Seq_Cons is awkward for several reasons: +// - long / verbose (nothing to do about that, I guess) +// - Seq is capitalized, but it means seq +// - most important part is buried in the middle +// - What are the established C conventions here?? +// - lastVal can be eliminated, I think diff --git a/src/queue-example-notes.md b/src/queue-example-notes.md index 859a237d..6150a10b 100644 --- a/src/queue-example-notes.md +++ b/src/queue-example-notes.md @@ -1,4 +1,4 @@ -# Notes +2# Notes - Bad definition of snoc (same as rev). How to spot? Look at constraint context, specifically snoc(listQ, x) == match listQ {Seq\_Nil {} => {Seq\_Nil {}}Seq\_Cons {head: h, tail: zs} => {snoc(rev(zs), h)}}. Other big clue: applying lemma snoc_nil results in an inconsistent context. This is really nasty because snoc(Seq_Nil{}, x) ends up reducing to itself.