From d38fd0604542bd78be23dbe8880cb891f3fc6915 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Wed, 31 Jul 2024 14:38:25 -0400 Subject: [PATCH 01/25] Try new naming conventions on lists --- src/examples/list_append.h | 12 +++++------ src/examples/list_c_types.h | 16 +++++++-------- src/examples/list_cn_types.h | 23 +++++++++++++-------- src/examples/list_constructors.h | 16 +++++++-------- src/examples/list_copy.c | 14 ++++++------- src/examples/list_free.c | 8 ++++---- src/examples/list_hdtl.h | 22 ++++++++++----------- src/examples/list_length.c | 26 ++++++++++++------------ src/examples/list_rev.c | 34 ++++++++++++++++---------------- src/examples/list_rev_alt.c | 30 ++++++++++++++-------------- src/examples/list_rev_lemmas.h | 10 +++++----- src/examples/list_snoc.h | 13 ++++++------ 12 files changed, 116 insertions(+), 108 deletions(-) diff --git a/src/examples/list_append.h b/src/examples/list_append.h index d6305abb..403caf56 100644 --- a/src/examples/list_append.h +++ b/src/examples/list_append.h @@ -1,13 +1,13 @@ // append.h /*@ -function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) { - match xs { - Seq_Nil {} => { - ys +function [rec] (datatype Seq_Int) Append__Seq_Int(datatype Seq_Int Xs, datatype Seq_Int Ys) { + match Xs { + Nil__Seq_Int {} => { + Ys } - Seq_Cons {head : h, tail : zs} => { - Seq_Cons {head: h, tail: append(zs, ys)} + Cons__Seq_Int {Head : H, Tail : Zs} => { + Cons__Seq_Int {Head: H, Tail: Append__Seq_Int(Zs, Ys)} } } } diff --git a/src/examples/list_c_types.h b/src/examples/list_c_types.h index c9b6d7a0..2df81dba 100644 --- a/src/examples/list_c_types.h +++ b/src/examples/list_c_types.h @@ -1,17 +1,17 @@ -struct int_list { +struct list_int { int head; - struct int_list* tail; + struct list_int* tail; }; -extern struct int_list *mallocIntList(); -/*@ spec mallocIntList(); +extern struct list_int *malloc_list_int(); +/*@ spec malloc_list_int(); requires true; - ensures take u = Block(return); + ensures take u = Block(return); @*/ -extern void freeIntList (struct int_list *p); -/*@ spec freeIntList(pointer p); - requires take u = Block(p); +extern void free_list_int (struct list_int *p); +/*@ spec free_list_int(pointer p); + requires take u = Block(p); ensures true; @*/ diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h index d45e6537..4a856bff 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/list_cn_types.h @@ -1,16 +1,23 @@ +// TODO i32 to I32 +// TODO is_null Is_Null() or Is_null() +// TODO: show people List_Int and List_Int_At and ask +// what people like better for predicate name. +// or Linked_List_Int? + +// maybe keep seq? Since it goes with many different data structures. /*@ -datatype seq { - Seq_Nil {}, - Seq_Cons {i32 head, datatype seq tail} +datatype Seq_Int { + Nil__Seq_Int {}, + Cons__Seq_Int {i32 Head, datatype Seq_Int Tail} } -predicate (datatype seq) IntList(pointer p) { +predicate (datatype Seq_Int) Linked_List_Int(pointer p) { if (is_null(p)) { - return Seq_Nil{}; + return Nil__Seq_Int{}; } else { - take H = Owned(p); - take tl = IntList(H.tail); - return (Seq_Cons { head: H.head, tail: tl }); + take h = Owned(p); + take Tl = Linked_List_Int(h.tail); + return (Cons__Seq_Int { Head: h.head, Tail: Tl }); } } @*/ diff --git a/src/examples/list_constructors.h b/src/examples/list_constructors.h index 2108a861..db4603ef 100644 --- a/src/examples/list_constructors.h +++ b/src/examples/list_constructors.h @@ -1,18 +1,18 @@ -struct int_list* IntList_nil() -/*@ ensures take ret = IntList(return); - ret == Seq_Nil{}; +struct list_int* nil__list_int() +/*@ ensures take Ret = Linked_List_Int(return); + Ret == Nil__Seq_Int{}; @*/ { return 0; } -struct int_list* IntList_cons(int h, struct int_list* t) -/*@ requires take l = IntList(t); - ensures take ret = IntList(return); - ret == Seq_Cons{ head: h, tail: l}; +struct list_int* cons__list_int(int h, struct list_int* t) +/*@ requires take L = Linked_List_Int(t); + ensures take Ret = Linked_List_Int(return); + Ret == Cons__Seq_Int{ Head: h, Tail: L}; @*/ { - struct int_list *p = mallocIntList(); + struct list_int *p = malloc_list_int(); p->head = h; p->tail = t; return p; diff --git a/src/examples/list_copy.c b/src/examples/list_copy.c index 4a1f8ef6..c45918fb 100644 --- a/src/examples/list_copy.c +++ b/src/examples/list_copy.c @@ -1,17 +1,17 @@ #include "list.h" -struct int_list* IntList_copy (struct int_list *xs) -/*@ requires take L1 = IntList(xs); - ensures take L1_ = IntList(xs); - take L2 = IntList(return); +struct list_int* list_int_copy (struct list_int *xs) +/*@ requires take L1 = Linked_List_Int(xs); + ensures take L1_ = Linked_List_Int(xs); + take L2 = Linked_List_Int(return); L1 == L1_; L1 == L2; @*/ { if (xs == 0) { - return IntList_nil(); + return nil__list_int(); } else { - struct int_list *new_tail = IntList_copy(xs->tail); - return IntList_cons(xs->head, new_tail); + struct list_int *new_tail = list_int_copy(xs->tail); + return cons__list_int(xs->head, new_tail); } } diff --git a/src/examples/list_free.c b/src/examples/list_free.c index f1441f4b..80924762 100644 --- a/src/examples/list_free.c +++ b/src/examples/list_free.c @@ -1,14 +1,14 @@ #include "list.h" -void IntList_free_list(struct int_list* xs) +void free_rec_list_int(struct list_int* xs) // You fill in the rest... /* --BEGIN-- */ -/*@ requires take L1 = IntList(xs); @*/ +/*@ requires take L1 = Linked_List_Int(xs); @*/ { if (xs == 0) { } else { - IntList_free_list(xs->tail); - freeIntList(xs); + free_rec_list_int(xs->tail); + free_list_int(xs); } } /* --END-- */ diff --git a/src/examples/list_hdtl.h b/src/examples/list_hdtl.h index e92b51ed..cad4c1d1 100644 --- a/src/examples/list_hdtl.h +++ b/src/examples/list_hdtl.h @@ -1,22 +1,22 @@ /*@ -function (i32) hd (datatype seq xs) { - match xs { - Seq_Nil {} => { +function (i32) Hd (datatype Seq_Int Xs) { + match Xs { + Nil__Seq_Int {} => { 0i32 } - Seq_Cons {head : h, tail : _} => { - h + Cons__Seq_Int {Head : H, Tail : _} => { + H } } } -function (datatype seq) tl (datatype seq xs) { - match xs { - Seq_Nil {} => { - Seq_Nil {} +function (datatype Seq_Int) Tl (datatype Seq_Int Xs) { + match Xs { + Nil__Seq_Int {} => { + Nil__Seq_Int{} } - Seq_Cons {head : _, tail : tail} => { - tail + Cons__Seq_Int {Head : _, Tail : T} => { + T } } } diff --git a/src/examples/list_length.c b/src/examples/list_length.c index 047b2c30..d99c7ec5 100644 --- a/src/examples/list_length.c +++ b/src/examples/list_length.c @@ -1,40 +1,40 @@ /* list_length.c */ - +// TODO: u32 to U32 #include "list.h" /* --BEGIN-- */ /*@ -function [rec] (u32) length(datatype seq xs) { - match xs { - Seq_Nil {} => { +function [rec] (u32) Length__Seq_Int(datatype Seq_Int Xs) { + match Xs { + Nil__Seq_Int {} => { 0u32 } - Seq_Cons {head : h, tail : zs} => { - 1u32 + length(zs) + Cons__Seq_Int {Head : H, Tail : Zs} => { + 1u32 + Length__Seq_Int(Zs) } } } @*/ /* --END-- */ -unsigned int IntList_length (struct int_list *xs) +unsigned int length__list_int (struct list_int *xs) /* --BEGIN-- */ -/*@ requires take L1 = IntList(xs); - ensures take L1_ = IntList(xs); +/*@ requires take L1 = Linked_List_Int(xs); + ensures take L1_ = Linked_List_Int(xs); L1 == L1_; - return == length(L1); + return == Length__Seq_Int(L1); @*/ /* --END-- */ { if (xs == 0) { /* --BEGIN-- */ - /*@ unfold length(L1); @*/ + /*@ unfold Length__Seq_Int(L1); @*/ /* --END-- */ return 0; } else { /* --BEGIN-- */ - /*@ unfold length(L1); @*/ + /*@ unfold Length__Seq_Int(L1); @*/ /* --END-- */ - return 1 + IntList_length (xs->tail); + return 1 + length__list_int(xs->tail); } } diff --git a/src/examples/list_rev.c b/src/examples/list_rev.c index 653ad0af..aab5b1ad 100644 --- a/src/examples/list_rev.c +++ b/src/examples/list_rev.c @@ -3,30 +3,30 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct int_list* IntList_rev_aux(struct int_list* xs, struct int_list* ys) -/*@ requires take L1 = IntList(xs); @*/ -/*@ requires take L2 = IntList(ys); @*/ -/*@ ensures take R = IntList(return); @*/ -/*@ ensures R == append(rev(L2), L1); @*/ +struct list_int* rev_aux__list_int(struct list_int* xs, struct list_int* ys) +/*@ requires take L1 = Linked_List_Int(xs); @*/ +/*@ requires take L2 = Linked_List_Int(ys); @*/ +/*@ ensures take R = Linked_List_Int(return); @*/ +/*@ ensures R == Append__Seq_Int(Rev__Seq_Int(L2), L1); @*/ { if (ys == 0) { - /*@ unfold rev(L2); @*/ - /*@ unfold append(Seq_Nil {},L1); @*/ + /*@ unfold Rev__Seq_Int(L2); @*/ + /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, L1); @*/ return xs; } else { - /*@ unfold rev(L2); @*/ - /*@ apply append_cons_r(rev(tl(L2)), hd(L2), L1); @*/ - struct int_list *tmp = ys->tail; + /*@ unfold Rev__Seq_Int(L2); @*/ + /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(L2)), Hd(L2), L1); @*/ + struct list_int *tmp = ys->tail; ys->tail = xs; - return IntList_rev_aux(ys, tmp); + return rev_aux__list_int(ys, tmp); } } -struct int_list* IntList_rev(struct int_list* xs) -/*@ requires take L1 = IntList(xs); @*/ -/*@ ensures take L1_rev = IntList(return); @*/ -/*@ ensures L1_rev == rev(L1); @*/ +struct list_int* rev__list_int(struct list_int* xs) +/*@ requires take L1 = Linked_List_Int(xs); @*/ +/*@ ensures take L1_Rev = Linked_List_Int(return); @*/ +/*@ ensures L1_Rev == Rev__Seq_Int(L1); @*/ { - /*@ apply append_nil_r(rev(L1)); @*/ - return IntList_rev_aux (0, xs); + /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L1)); @*/ + return rev_aux__list_int (0, xs); } diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c index 7cb4eaa5..f9ff3cfc 100644 --- a/src/examples/list_rev_alt.c +++ b/src/examples/list_rev_alt.c @@ -3,31 +3,31 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct int_list* IntList_rev_loop(struct int_list *xs) -/*@ requires take L = IntList(xs); - ensures take L_ = IntList(return); - L_ == rev(L); +struct list_int* rev_loop__list_int(struct list_int *xs) +/*@ requires take L = Linked_List_Int(xs); + ensures take L_ = Linked_List_Int(return); + L_ == Rev__Seq_Int(L); @*/ { - struct int_list *last = 0; - struct int_list *cur = xs; - /*@ apply append_nil_r(rev(L)); @*/ + struct list_int *last = 0; + struct list_int *cur = xs; + /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L)); @*/ while(1) - /*@ inv take L1 = IntList(last); - take L2 = IntList(cur); - append(rev(L2), L1) == rev(L); + /*@ inv take L1 = Linked_List_Int(last); + take L2 = Linked_List_Int(cur); + Append__Seq_Int(Rev__Seq_Int(L2), L1) == Rev__Seq_Int(L); @*/ { if (cur == 0) { - /*@ unfold rev(Seq_Nil {}); @*/ - /*@ unfold append(Seq_Nil {}, L1); @*/ + /*@ unfold Rev__Seq_Int(Nil__Seq_Int{}); @*/ + /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, L1); @*/ return last; } - struct int_list *tmp = cur->tail; + struct list_int *tmp = cur->tail; cur->tail = last; last = cur; cur = tmp; - /*@ unfold rev(L2); @*/ - /*@ apply append_cons_r (rev (tl(L2)), hd(L2), L1); @*/ + /*@ unfold Rev__Seq_Int(L2); @*/ + /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(L2)), Hd(L2), L1); @*/ } } diff --git a/src/examples/list_rev_lemmas.h b/src/examples/list_rev_lemmas.h index 28f21937..20615f2d 100644 --- a/src/examples/list_rev_lemmas.h +++ b/src/examples/list_rev_lemmas.h @@ -1,10 +1,10 @@ /*@ -lemma append_nil_r (datatype seq l1) +lemma Append_Nil_R__Seq_Int (datatype Seq_Int L1) requires true; - ensures append(l1, Seq_Nil {}) == l1; + ensures Append__Seq_Int(L1, Nil__Seq_Int{}) == L1; -lemma append_cons_r (datatype seq l1, i32 x, datatype seq l2) +lemma Append_Cons_R__Seq_Int (datatype Seq_Int L1, i32 X, datatype Seq_Int L2) requires true; - ensures append(l1, Seq_Cons {head: x, tail: l2}) - == append(snoc(l1, x), l2); + ensures Append__Seq_Int(L1, Cons__Seq_Int {Head: X, Tail: L2}) + == Append__Seq_Int(Snoc__Seq_Int(L1, X), L2); @*/ diff --git a/src/examples/list_snoc.h b/src/examples/list_snoc.h index 52cbdcb4..d9143701 100644 --- a/src/examples/list_snoc.h +++ b/src/examples/list_snoc.h @@ -1,11 +1,12 @@ +// TODO: change i32 to I32 /*@ -function [rec] (datatype seq) snoc(datatype seq xs, i32 y) { - match xs { - Seq_Nil {} => { - Seq_Cons {head: y, tail: Seq_Nil{}} +function [rec] (datatype Seq_Int) Snoc__Seq_Int(datatype Seq_Int Xs, i32 Y) { + match Xs { + Nil__Seq_Int {} => { + Cons__Seq_Int {Head: Y, Tail: Nil__Seq_Int{}} } - Seq_Cons {head: x, tail: zs} => { - Seq_Cons{head: x, tail: snoc (zs, y)} + Cons__Seq_Int {Head: X, Tail: Zs} => { + Cons__Seq_Int{Head: X, Tail: Snoc__Seq_Int (Zs, Y)} } } } From 281a31c552b4e2fa23e3452ba22473c8771ab36c Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Wed, 31 Jul 2024 14:59:43 -0400 Subject: [PATCH 02/25] add rev --- src/examples/list_rev.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/examples/list_rev.h b/src/examples/list_rev.h index 7260f3eb..7f8aefc9 100644 --- a/src/examples/list_rev.h +++ b/src/examples/list_rev.h @@ -1,13 +1,13 @@ #include "list_snoc.h" /*@ -function [rec] (datatype seq) rev(datatype seq xs) { - match xs { - Seq_Nil {} => { - Seq_Nil {} +function [rec] (datatype Seq_Int) Rev__Seq_Int(datatype Seq_Int Xs) { + match Xs { + Nil__Seq_Int {} => { + Nil__Seq_Int {} } - Seq_Cons {head : h, tail : zs} => { - snoc (rev(zs), h) + Cons__Seq_Int {Head : H, Tail : Zs} => { + Snoc__Seq_Int (Rev__Seq_Int(Zs), H) } } } From 5d3a937570ad0cb918b61f1bb11010cc9e1ff805 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Wed, 31 Jul 2024 15:57:04 -0400 Subject: [PATCH 03/25] Polishing, tidying, renaming, some comments --- src/examples/list_append.h | 10 +++++----- src/examples/list_cn_types.h | 12 ++++++++---- src/examples/list_constructors.h | 4 ++-- src/examples/list_copy.c | 18 +++++++++--------- src/examples/list_free.c | 10 +++++----- src/examples/list_hdtl.h | 8 ++++---- src/examples/list_length.c | 26 +++++++++++++------------- src/examples/list_rev.c | 22 +++++++++++----------- src/examples/list_rev.h | 8 ++++---- src/examples/list_rev_alt.c | 18 +++++++++--------- 10 files changed, 70 insertions(+), 66 deletions(-) diff --git a/src/examples/list_append.h b/src/examples/list_append.h index 403caf56..2d89997c 100644 --- a/src/examples/list_append.h +++ b/src/examples/list_append.h @@ -1,13 +1,13 @@ // append.h /*@ -function [rec] (datatype Seq_Int) Append__Seq_Int(datatype Seq_Int Xs, datatype Seq_Int Ys) { - match Xs { +function [rec] (datatype Seq_Int) Append__Seq_Int(datatype Seq_Int L1, datatype Seq_Int L2) { + match L1 { Nil__Seq_Int {} => { - Ys + L2 } - Cons__Seq_Int {Head : H, Tail : Zs} => { - Cons__Seq_Int {Head: H, Tail: Append__Seq_Int(Zs, Ys)} + Cons__Seq_Int {Head : H, Tail : T} => { + Cons__Seq_Int {Head: H, Tail: Append__Seq_Int(T, L2)} } } } diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h index 4a856bff..7398a7a5 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/list_cn_types.h @@ -1,10 +1,14 @@ // TODO i32 to I32 -// TODO is_null Is_Null() or Is_null() +// TODO is_null to Is_Null() or Is_null() // TODO: show people List_Int and List_Int_At and ask -// what people like better for predicate name. -// or Linked_List_Int? +// which is better for predicate name. +// (But perhaps Linked_List_Int is clearest?) +// TODO: Rename this file Seq.h + +// We've kept Seq for the type of abstract sequences, since many +// different concrete data structures are representations of abstract +// lists. -// maybe keep seq? Since it goes with many different data structures. /*@ datatype Seq_Int { Nil__Seq_Int {}, diff --git a/src/examples/list_constructors.h b/src/examples/list_constructors.h index db4603ef..c511d08c 100644 --- a/src/examples/list_constructors.h +++ b/src/examples/list_constructors.h @@ -7,9 +7,9 @@ struct list_int* nil__list_int() } struct list_int* cons__list_int(int h, struct list_int* t) -/*@ requires take L = Linked_List_Int(t); +/*@ requires take T = Linked_List_Int(t); ensures take Ret = Linked_List_Int(return); - Ret == Cons__Seq_Int{ Head: h, Tail: L}; + Ret == Cons__Seq_Int{ Head: h, Tail: T}; @*/ { struct list_int *p = malloc_list_int(); diff --git a/src/examples/list_copy.c b/src/examples/list_copy.c index c45918fb..a6604ec0 100644 --- a/src/examples/list_copy.c +++ b/src/examples/list_copy.c @@ -1,17 +1,17 @@ #include "list.h" -struct list_int* list_int_copy (struct list_int *xs) -/*@ requires take L1 = Linked_List_Int(xs); - ensures take L1_ = Linked_List_Int(xs); - take L2 = Linked_List_Int(return); - L1 == L1_; - L1 == L2; +struct list_int* list_int_copy (struct list_int *l) +/*@ requires take L = Linked_List_Int(l); + ensures take L_ = Linked_List_Int(l); + take Ret = Linked_List_Int(return); + L == L_; + L == Ret; @*/ { - if (xs == 0) { + if (l == 0) { return nil__list_int(); } else { - struct list_int *new_tail = list_int_copy(xs->tail); - return cons__list_int(xs->head, new_tail); + struct list_int *new_tail = list_int_copy(l->tail); + return cons__list_int(l->head, new_tail); } } diff --git a/src/examples/list_free.c b/src/examples/list_free.c index 80924762..09665a9d 100644 --- a/src/examples/list_free.c +++ b/src/examples/list_free.c @@ -1,14 +1,14 @@ #include "list.h" -void free_rec_list_int(struct list_int* xs) +void free_rec_list_int(struct list_int* l) // You fill in the rest... /* --BEGIN-- */ -/*@ requires take L1 = Linked_List_Int(xs); @*/ +/*@ requires take L = Linked_List_Int(l); @*/ { - if (xs == 0) { + if (l == 0) { } else { - free_rec_list_int(xs->tail); - free_list_int(xs); + free_rec_list_int(l->tail); + free_list_int(l); } } /* --END-- */ diff --git a/src/examples/list_hdtl.h b/src/examples/list_hdtl.h index cad4c1d1..fac22546 100644 --- a/src/examples/list_hdtl.h +++ b/src/examples/list_hdtl.h @@ -1,6 +1,6 @@ /*@ -function (i32) Hd (datatype Seq_Int Xs) { - match Xs { +function (i32) Hd (datatype Seq_Int L) { + match L { Nil__Seq_Int {} => { 0i32 } @@ -10,8 +10,8 @@ function (i32) Hd (datatype Seq_Int Xs) { } } -function (datatype Seq_Int) Tl (datatype Seq_Int Xs) { - match Xs { +function (datatype Seq_Int) Tl (datatype Seq_Int L) { + match L { Nil__Seq_Int {} => { Nil__Seq_Int{} } diff --git a/src/examples/list_length.c b/src/examples/list_length.c index d99c7ec5..04a0f51d 100644 --- a/src/examples/list_length.c +++ b/src/examples/list_length.c @@ -4,37 +4,37 @@ /* --BEGIN-- */ /*@ -function [rec] (u32) Length__Seq_Int(datatype Seq_Int Xs) { - match Xs { +function [rec] (u32) Length__Seq_Int(datatype Seq_Int L) { + match L { Nil__Seq_Int {} => { 0u32 } - Cons__Seq_Int {Head : H, Tail : Zs} => { - 1u32 + Length__Seq_Int(Zs) + Cons__Seq_Int {Head : H, Tail : T} => { + 1u32 + Length__Seq_Int(T) } } } @*/ /* --END-- */ -unsigned int length__list_int (struct list_int *xs) +unsigned int length__list_int (struct list_int *l) /* --BEGIN-- */ -/*@ requires take L1 = Linked_List_Int(xs); - ensures take L1_ = Linked_List_Int(xs); - L1 == L1_; - return == Length__Seq_Int(L1); +/*@ requires take L = Linked_List_Int(l); + ensures take L_ = Linked_List_Int(l); + L == L_; + return == Length__Seq_Int(L); @*/ /* --END-- */ { - if (xs == 0) { + if (l == 0) { /* --BEGIN-- */ - /*@ unfold Length__Seq_Int(L1); @*/ + /*@ unfold Length__Seq_Int(L); @*/ /* --END-- */ return 0; } else { /* --BEGIN-- */ - /*@ unfold Length__Seq_Int(L1); @*/ + /*@ unfold Length__Seq_Int(L); @*/ /* --END-- */ - return 1 + length__list_int(xs->tail); + return 1 + length__list_int(l->tail); } } diff --git a/src/examples/list_rev.c b/src/examples/list_rev.c index aab5b1ad..1352ea6c 100644 --- a/src/examples/list_rev.c +++ b/src/examples/list_rev.c @@ -3,30 +3,30 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct list_int* rev_aux__list_int(struct list_int* xs, struct list_int* ys) -/*@ requires take L1 = Linked_List_Int(xs); @*/ -/*@ requires take L2 = Linked_List_Int(ys); @*/ +struct list_int* rev_aux__list_int(struct list_int* l1, struct list_int* l2) +/*@ requires take L1 = Linked_List_Int(l1); @*/ +/*@ requires take L2 = Linked_List_Int(l2); @*/ /*@ ensures take R = Linked_List_Int(return); @*/ /*@ ensures R == Append__Seq_Int(Rev__Seq_Int(L2), L1); @*/ { - if (ys == 0) { + if (l2 == 0) { /*@ unfold Rev__Seq_Int(L2); @*/ /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, L1); @*/ - return xs; + return l1; } else { /*@ unfold Rev__Seq_Int(L2); @*/ /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(L2)), Hd(L2), L1); @*/ - struct list_int *tmp = ys->tail; - ys->tail = xs; - return rev_aux__list_int(ys, tmp); + struct list_int *tmp = l2->tail; + l2->tail = l1; + return rev_aux__list_int(l2, tmp); } } -struct list_int* rev__list_int(struct list_int* xs) -/*@ requires take L1 = Linked_List_Int(xs); @*/ +struct list_int* rev__list_int(struct list_int* l1) +/*@ requires take L1 = Linked_List_Int(l1); @*/ /*@ ensures take L1_Rev = Linked_List_Int(return); @*/ /*@ ensures L1_Rev == Rev__Seq_Int(L1); @*/ { /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L1)); @*/ - return rev_aux__list_int (0, xs); + return rev_aux__list_int (0, l1); } diff --git a/src/examples/list_rev.h b/src/examples/list_rev.h index 7f8aefc9..67174aa9 100644 --- a/src/examples/list_rev.h +++ b/src/examples/list_rev.h @@ -1,13 +1,13 @@ #include "list_snoc.h" /*@ -function [rec] (datatype Seq_Int) Rev__Seq_Int(datatype Seq_Int Xs) { - match Xs { +function [rec] (datatype Seq_Int) Rev__Seq_Int(datatype Seq_Int L) { + match L { Nil__Seq_Int {} => { Nil__Seq_Int {} } - Cons__Seq_Int {Head : H, Tail : Zs} => { - Snoc__Seq_Int (Rev__Seq_Int(Zs), H) + Cons__Seq_Int {Head : H, Tail : T} => { + Snoc__Seq_Int (Rev__Seq_Int(T), H) } } } diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c index f9ff3cfc..fecfb481 100644 --- a/src/examples/list_rev_alt.c +++ b/src/examples/list_rev_alt.c @@ -3,31 +3,31 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct list_int* rev_loop__list_int(struct list_int *xs) -/*@ requires take L = Linked_List_Int(xs); +struct list_int* rev_loop__list_int(struct list_int *l) +/*@ requires take L = Linked_List_Int(l); ensures take L_ = Linked_List_Int(return); L_ == Rev__Seq_Int(L); @*/ { struct list_int *last = 0; - struct list_int *cur = xs; + struct list_int *cur = l; /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L)); @*/ while(1) - /*@ inv take L1 = Linked_List_Int(last); - take L2 = Linked_List_Int(cur); - Append__Seq_Int(Rev__Seq_Int(L2), L1) == Rev__Seq_Int(L); + /*@ inv take Last = Linked_List_Int(last); + take Cur = Linked_List_Int(cur); + Append__Seq_Int(Rev__Seq_Int(Cur), Last) == Rev__Seq_Int(L); @*/ { if (cur == 0) { /*@ unfold Rev__Seq_Int(Nil__Seq_Int{}); @*/ - /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, L1); @*/ + /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, Last); @*/ return last; } struct list_int *tmp = cur->tail; cur->tail = last; last = cur; cur = tmp; - /*@ unfold Rev__Seq_Int(L2); @*/ - /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(L2)), Hd(L2), L1); @*/ + /*@ unfold Rev__Seq_Int(Cur); @*/ + /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(Cur)), Hd(Cur), Last); @*/ } } From 5934f2db845bd35af7457c7896b767fab4218b73 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Wed, 31 Jul 2024 15:59:00 -0400 Subject: [PATCH 04/25] Summary of proposed naming conventions --- NAMING-CONVENTIONS.md | 83 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 NAMING-CONVENTIONS.md diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md new file mode 100644 index 00000000..62346e8b --- /dev/null +++ b/NAMING-CONVENTIONS.md @@ -0,0 +1,83 @@ +CN Naming Conventions +--------------------- + +At the moment, the way things are named in CN examples is all over the +map, leading to considerable friction and frustration. We should +agree on some conventions that we like, do one painful global rename +to change everything in the tutorial (at least) to use them, and then +stick to them for new stuff we write. + +Here's our (Benjamin and Liz's) best shot at a good set of +conventions, based on past discussions: + +## Code conventions + +Rules: + - In general, identifiers are written in `snake_case` rather than `camlCase` + - C-level identifiers are `lowercase_initial` + - CN-level identifiers are `Uppercase_initial` + - Polymorphic functions and predicates, at both C and CN levels, are + "monomorphized" by adding their type arguments at the end, + connected by `__` + - E.g., `queue__int` + - When the same concept exists at both the C and CN levels, it is + named the same except for the lowercase/uppercase distinction + - E.g., `queue__int` at the C level vs. `Queue__I32` at the + CN level + - When a single structure at the CN level is used to talk + about many different structures at the C level -- e.g., + mathematical sequences are the abstract content of many + concrete heap data structures (lists, doubly linked lists, + queues, ...), the CN structure should have a name that + distinguishes it from all the concrete realizations. In + particular, the type of mathematical lists is called + `Seq__U32`, not `List__U32`. + - Alternatively, we could rename `Seq` back to `List` + but then use `linked_list__int` instead of just + `list__int` at the C level. + - A CN identifier that represents the state of a mutable data + structure when some function returns should be named the same as + the starting state of the data structure, with an `_` at the + end. + - E.g., The list copy function takes a linked list `l` + representing a sequence `L` and leaves `l` pointing to a + final sequence `L_` such that `L == L_`. Moreover, it + returns a new sequence `Ret` with `L == Ret`. + +Questions / concerns / ideas: + - Should CN-level identifiers be `Uppercase_initial` or + `Uppercase_Consistently_Throughout`? + - Convention for naming predicates? + - One suggestion is the suffix `_at` to represent the + assertion that there is an object at that address. For + example, `Queue_U32_at(p)`. + - Convention for auxiliary predicates? + - Maybe adding `_Aux` to the original predicate name + (e.g. `Queue_U32_at_Aux`). + - Does capitalization convention apply to function names? + Ex. list_int_copy() vs List_Int_Copy(). list_int is in C so it + should be lowercase, but is that true for the name of a function + that affects it? + - (BCP: Don't understand this one?) + - The existing function `IntList_free_list` is hard to rename with + these conventions. It feels like it should be `free_int_list`, + but that’s also the new name of the free function for individual + list cells (opposite of `malloc`). Current solution is + `free_int_list_rec`. + +Notes: + - This proposal will require changing some built-ins if we really + take it seriously + - `i32` to `I32`, `u64` to `U64` + - `is_null` to `Is_null` (or `Is_Null`?) + +## Text conventions + +Rules: + - Consistently use the word "abstract" to refer to CN-level + ("mathematical") structures + - Would _specification-level_ be better than "abstract" + (i.e., clearer, even if it a bit clunkier)? + - Consistently use the word "concrete" to refer to C-level + structures on the stack/heap + - Would _implementation-level_ be better than "concrete"? From c8b4bd888a4090c32c611280f9eab120f8bb9f38 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Thu, 1 Aug 2024 10:14:58 -0400 Subject: [PATCH 05/25] rename `list_cn_types` to `Seq.h` --- src/examples/{list_cn_types.h => Seq.h} | 1 - 1 file changed, 1 deletion(-) rename src/examples/{list_cn_types.h => Seq.h} (95%) diff --git a/src/examples/list_cn_types.h b/src/examples/Seq.h similarity index 95% rename from src/examples/list_cn_types.h rename to src/examples/Seq.h index 7398a7a5..95b5dd6e 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/Seq.h @@ -3,7 +3,6 @@ // TODO: show people List_Int and List_Int_At and ask // which is better for predicate name. // (But perhaps Linked_List_Int is clearest?) -// TODO: Rename this file Seq.h // We've kept Seq for the type of abstract sequences, since many // different concrete data structures are representations of abstract From 7e65961011bdfa3f42a3d38750a2cb2348cd7ae4 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 1 Aug 2024 10:20:33 -0400 Subject: [PATCH 06/25] Tidying --- NAMING-CONVENTIONS.md | 9 +++++---- src/examples/list_cn_types.h | 2 -- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 62346e8b..251f8a9a 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -46,7 +46,8 @@ Rules: Questions / concerns / ideas: - Should CN-level identifiers be `Uppercase_initial` or - `Uppercase_Consistently_Throughout`? + `Uppercase_Consistently_Throughout`? I [BCP] find the latter a + bit lighter. - Convention for naming predicates? - One suggestion is the suffix `_at` to represent the assertion that there is an object at that address. For @@ -55,7 +56,7 @@ Questions / concerns / ideas: - Maybe adding `_Aux` to the original predicate name (e.g. `Queue_U32_at_Aux`). - Does capitalization convention apply to function names? - Ex. list_int_copy() vs List_Int_Copy(). list_int is in C so it + Ex. `list_int_copy()` vs `List_Int_Copy()`. The list_int is in C so it should be lowercase, but is that true for the name of a function that affects it? - (BCP: Don't understand this one?) @@ -66,10 +67,10 @@ Questions / concerns / ideas: `free_int_list_rec`. Notes: - - This proposal will require changing some built-ins if we really + - This proposal will also require changing some built-ins if we really take it seriously - `i32` to `I32`, `u64` to `U64` - - `is_null` to `Is_null` (or `Is_Null`?) + - `is_null` to `Is_null` (or `Is_Null`) ## Text conventions diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h index 7398a7a5..517a0c5b 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/list_cn_types.h @@ -1,5 +1,3 @@ -// TODO i32 to I32 -// TODO is_null to Is_Null() or Is_null() // TODO: show people List_Int and List_Int_At and ask // which is better for predicate name. // (But perhaps Linked_List_Int is clearest?) From fb6c311577e86d0dcdcb169a8d30f7ea02e608d3 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 1 Aug 2024 11:29:39 -0400 Subject: [PATCH 07/25] Instructions --- NAMING-CONVENTIONS.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 251f8a9a..3aa01dda 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -7,8 +7,12 @@ agree on some conventions that we like, do one painful global rename to change everything in the tutorial (at least) to use them, and then stick to them for new stuff we write. -Here's our (Benjamin and Liz's) best shot at a good set of -conventions, based on past discussions: +This document describes our (Benjamin and Liz's) best shot at a good +set of conventions, based on past discussions. + +All the list-related files in src/examples have been converted to this +convention -- do `ls src/examples/{list*,Seq*}` to check it out. + ## Code conventions From 1eeb5ef1a0d22dd41e86198b075ea5a75bcd002a Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 1 Aug 2024 17:31:40 -0400 Subject: [PATCH 08/25] Rename Seq.h back to list_cn_types.h (lighter) --- src/examples/{Seq.h => list_cn_types.h} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/examples/{Seq.h => list_cn_types.h} (100%) diff --git a/src/examples/Seq.h b/src/examples/list_cn_types.h similarity index 100% rename from src/examples/Seq.h rename to src/examples/list_cn_types.h From c3bded0e75b5669bf692e1a4c1f61a8be86f1304 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 1 Aug 2024 17:32:07 -0400 Subject: [PATCH 09/25] Better proposal for conventions --- NAMING-CONVENTIONS.md | 203 +++++++++++++++++++++++++----------------- 1 file changed, 121 insertions(+), 82 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 3aa01dda..eeb81d62 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -1,88 +1,127 @@ CN Naming Conventions --------------------- -At the moment, the way things are named in CN examples is all over the -map, leading to considerable friction and frustration. We should -agree on some conventions that we like, do one painful global rename -to change everything in the tutorial (at least) to use them, and then -stick to them for new stuff we write. - This document describes our (Benjamin and Liz's) best shot at a good -set of conventions, based on past discussions. +set of conventions for naming identifiers in CN, based on numerous +discussions. All the list-related files in src/examples have been converted to this -convention -- do `ls src/examples/{list*,Seq*}` to check it out. - - -## Code conventions - -Rules: - - In general, identifiers are written in `snake_case` rather than `camlCase` - - C-level identifiers are `lowercase_initial` - - CN-level identifiers are `Uppercase_initial` - - Polymorphic functions and predicates, at both C and CN levels, are - "monomorphized" by adding their type arguments at the end, - connected by `__` - - E.g., `queue__int` - - When the same concept exists at both the C and CN levels, it is - named the same except for the lowercase/uppercase distinction - - E.g., `queue__int` at the C level vs. `Queue__I32` at the - CN level - - When a single structure at the CN level is used to talk - about many different structures at the C level -- e.g., - mathematical sequences are the abstract content of many - concrete heap data structures (lists, doubly linked lists, - queues, ...), the CN structure should have a name that - distinguishes it from all the concrete realizations. In - particular, the type of mathematical lists is called - `Seq__U32`, not `List__U32`. - - Alternatively, we could rename `Seq` back to `List` - but then use `linked_list__int` instead of just - `list__int` at the C level. - - A CN identifier that represents the state of a mutable data - structure when some function returns should be named the same as - the starting state of the data structure, with an `_` at the - end. - - E.g., The list copy function takes a linked list `l` - representing a sequence `L` and leaves `l` pointing to a - final sequence `L_` such that `L == L_`. Moreover, it - returns a new sequence `Ret` with `L == Ret`. - -Questions / concerns / ideas: - - Should CN-level identifiers be `Uppercase_initial` or - `Uppercase_Consistently_Throughout`? I [BCP] find the latter a - bit lighter. - - Convention for naming predicates? - - One suggestion is the suffix `_at` to represent the - assertion that there is an object at that address. For - example, `Queue_U32_at(p)`. - - Convention for auxiliary predicates? - - Maybe adding `_Aux` to the original predicate name - (e.g. `Queue_U32_at_Aux`). - - Does capitalization convention apply to function names? - Ex. `list_int_copy()` vs `List_Int_Copy()`. The list_int is in C so it - should be lowercase, but is that true for the name of a function - that affects it? - - (BCP: Don't understand this one?) - - The existing function `IntList_free_list` is hard to rename with - these conventions. It feels like it should be `free_int_list`, - but that’s also the new name of the free function for individual - list cells (opposite of `malloc`). Current solution is - `free_int_list_rec`. - -Notes: - - This proposal will also require changing some built-ins if we really - take it seriously - - `i32` to `I32`, `u64` to `U64` - - `is_null` to `Is_null` (or `Is_Null`) - -## Text conventions - -Rules: - - Consistently use the word "abstract" to refer to CN-level - ("mathematical") structures - - Would _specification-level_ be better than "abstract" - (i.e., clearer, even if it a bit clunkier)? - - Consistently use the word "concrete" to refer to C-level - structures on the stack/heap - - Would _implementation-level_ be better than "concrete"? +convention -- do `ls src/examples/list*` to check it out. + +# General Conventions + +- In general, identifiers are written in `snake_case` rather than `camlCase` + +- C-level identifiers are `lowercase_initial` + +- CN-level identifiers are `Uppercase_initial` + +- A CN identifier that represents the state of a mutable data + structure after some function returns should be named the same as + the starting state of the data structure, with an `_` at the + end. + - E.g., The list copy function takes a linked list `l` + representing a sequence `L` and leaves `l` at the end pointing + to a final sequence `L_` such that `L == L_`. (Moreover, it + returns a new sequence `Ret` with `L == Ret`.) + +## Questions: + +- Should CN-level identifiers be `Uppercase_initial` or + `Uppercase_Consistently_Throughout`? + + I [BCP] find the former a bit lighter. + +- Should predicates that extract some structure from the heap be named + the same as the structure they extract. I.e., should the result + type of the `Queue` predicate also be called `Queue`? + + On one hand, there is clearly some potential for confusion. On the + other hand, types don't take an argument and predicates do, so it's + easy to disambiguate. + + On balance, I [BCP] prefer naming both the same; Liz prefers using + `Queue_at` for the predicate. + +# Built-ins + +- This proposal will also require changing some built-ins if we really + take it seriously + - `i32` should change to `I32`, `u64` to `U64` + - `is_null` to `Is_null` (or `Is_Null`) + +# Polymorphism + +How to name the "instances" of "morally polymorphic" functions (i.e., +should we write (i.e., whether to write `append__Int` or +`append__List_Int` rather than just `append`) is a tricky issue. On +one hand, `append__Int` is "more correct". On the other hand, these +extra annotations get pretty heavy. + +We propose a compromise: + +1. If a project needs to use two or more instances of some polymorphic + type, then the names of the C and CN types, the C and CN functions + operating over them, and the CN predicates describing them are all + suffixed with `__xxx`, where `xxx` is the appropriate "type + argument". E.g., if some codebase uses lists of both signed and + unsigned 32-bit ints, then we would use names like this: + - `list__int` / `list__uint` + - `append__int` / `append__uint` + - `List__I32` / `List__U32` + - `Cons__I32` / `Cons__U32` + - etc. + +2. However, if, in a given project, a set of "morally polymorphic" + type definitions and library functions is only used at one + monomorphic instance (e.g., if some codebase only ever needs lists + of 32-bit signed ints), then the `__int` or `__I32` annotations are + omitted. + + This convention should be used in the CN tutorial, for example. + + TODO: Right now, the tutorial uses option (1). It was this + exercise that convinced me [BCP] that option (2) was better. :-) + +## Discussion + +One downside of this convention is that it might sometimes require +some after-the-fact renaming: If a project starts out using just lists +of signed ints and later needs to introduce lists of unsigned ints, +the old signed operations will need to be renamed. This seems like an +acceptable cost for keeping things light. + +Another downside is that it introduces two different ways of naming +polymorphic things. But hopefully (a) the appropriate use of each is +clear and (b) most C developments will actually fall in the second, +lighter case, and programmers will never need to bother understanding +the first case. + +# Text conventions + +We need some consistent way of distinguishing "C-level" things from +"CN-level" things. Here are some possibilities: + +1. _abstract_ for CN-level ("mathematical") structures vs. _concrete_ + for C-level structures + +2. _specification-level_ vs. _implementation-level_ + +3. _CN-level_ vs. _C-level_ + +I think I [BCP] like the third best. What about you? + +# Loose ends + +TODO: Tidy them! + +- Convention for auxiliary predicates? + - Maybe adding `_Aux` to the original predicate name + (e.g. `Queue_U32_at_Aux`). + +- The existing function `IntList_free_list` is hard to rename with + these conventions. It feels like it should be `free_int_list`, + but that’s also the new name of the free function for individual + list cells (opposite of `malloc`). Current solution is + `free_int_list_rec`. + From 32e5a6b83ee28c8df50e0b920fb6846bed680eb2 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Thu, 1 Aug 2024 18:02:46 -0400 Subject: [PATCH 10/25] add Liz opinions --- NAMING-CONVENTIONS.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index eeb81d62..bb123538 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -31,6 +31,9 @@ convention -- do `ls src/examples/list*` to check it out. `Uppercase_Consistently_Throughout`? I [BCP] find the former a bit lighter. + I [Liz] find the latter to be more consistent. If `List_int` is the + identifier and `Rev_list_int` is the function, then `list_int` is + lowercase in the function even though it is usually capital. - Should predicates that extract some structure from the heap be named the same as the structure they extract. I.e., should the result @@ -110,6 +113,8 @@ We need some consistent way of distinguishing "C-level" things from 3. _CN-level_ vs. _C-level_ I think I [BCP] like the third best. What about you? +I [Liz] think all of these are good options, but think the first one +communicates reality the most. # Loose ends @@ -123,5 +128,4 @@ TODO: Tidy them! these conventions. It feels like it should be `free_int_list`, but that’s also the new name of the free function for individual list cells (opposite of `malloc`). Current solution is - `free_int_list_rec`. - + `free_int_list_rec` or `free_rec_int_list`. \ No newline at end of file From fa952aa3b1c46c252ebba945a8901abef9eac79b Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Fri, 2 Aug 2024 08:38:55 -0400 Subject: [PATCH 11/25] Responses to Liz and some more polishing --- NAMING-CONVENTIONS.md | 55 ++++++++++++++++++++++++------------------- 1 file changed, 31 insertions(+), 24 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index bb123538..fd8d9c0e 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -3,7 +3,7 @@ CN Naming Conventions This document describes our (Benjamin and Liz's) best shot at a good set of conventions for naming identifiers in CN, based on numerous -discussions. +discussions and worked examples. All the list-related files in src/examples have been converted to this convention -- do `ls src/examples/list*` to check it out. @@ -28,12 +28,13 @@ convention -- do `ls src/examples/list*` to check it out. ## Questions: - Should CN-level identifiers be `Uppercase_initial` or - `Uppercase_Consistently_Throughout`? - - I [BCP] find the former a bit lighter. - I [Liz] find the latter to be more consistent. If `List_int` is the - identifier and `Rev_list_int` is the function, then `list_int` is - lowercase in the function even though it is usually capital. + `Uppercase_Consistently_Throughout`? + + BCP find the former a bit lighter. Liz finds the latter to be more + consistent. If `List_int` is the identifier and `Rev_list_int` is + the function, then `list_int` is lowercase in the function even + though it is usually capital. (BCP admits this is a fair point.) + What do others think? - Should predicates that extract some structure from the heap be named the same as the structure they extract. I.e., should the result @@ -72,15 +73,15 @@ We propose a compromise: - `list__int` / `list__uint` - `append__int` / `append__uint` - `List__I32` / `List__U32` - - `Cons__I32` / `Cons__U32` + - `Cons__I32` / `Cons__U32` - etc. 2. However, if, in a given project, a set of "morally polymorphic" type definitions and library functions is only used at one monomorphic instance (e.g., if some codebase only ever needs lists of 32-bit signed ints), then the `__int` or `__I32` annotations are - omitted. - + omitted. + This convention should be used in the CN tutorial, for example. TODO: Right now, the tutorial uses option (1). It was this @@ -112,20 +113,26 @@ We need some consistent way of distinguishing "C-level" things from 3. _CN-level_ vs. _C-level_ -I think I [BCP] like the third best. What about you? -I [Liz] think all of these are good options, but think the first one -communicates reality the most. +BCP thinks he likes the third best. Liz thinks all of these are good +options, but the first one communicates reality the most. What about +you? # Loose ends -TODO: Tidy them! - -- Convention for auxiliary predicates? - - Maybe adding `_Aux` to the original predicate name - (e.g. `Queue_U32_at_Aux`). - -- The existing function `IntList_free_list` is hard to rename with - these conventions. It feels like it should be `free_int_list`, - but that’s also the new name of the free function for individual - list cells (opposite of `malloc`). Current solution is - `free_int_list_rec` or `free_rec_int_list`. \ No newline at end of file +- Do we need a convention for auxiliary predicates? + - E.g., maybe adding `_Aux` to the original predicate name + (e.g. `Queue_Aux` for the recursive predicate that walks down + the list of queue nodes to gather them into a list once a + top-level `Queue` or `Queue_at` predicate has dealt with the + non-recursive part of the structure). + +- The current function `IntList_free_list` is hard to rename with + these conventions. It feels like it should be `free__int_list`, but + that’s also the new name of the free function for individual list + cells (opposite of `malloc`). Current solution is + `free_rec__int_list`. + - BCP wonders if this issue is specific to malloc and free. If + so, maybe we can make some special convention like + `free__int_list_node` for the single-node operation (even though + what it returns is an `int_list`, noit an `int_list_node`), + leaving `free__int_list` for the recursive one? From d21f25f2fac17e5f0d0c608f4131637a970d4944 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 8 Aug 2024 12:16:58 -0400 Subject: [PATCH 12/25] Updated naming convention recommendations (WIP) --- Makefile | 3 + NAMING-CONVENTIONS.md | 129 +++++++++++++++++++++--------------------- 2 files changed, 68 insertions(+), 64 deletions(-) diff --git a/Makefile b/Makefile index f915ad35..c98725f9 100644 --- a/Makefile +++ b/Makefile @@ -43,6 +43,9 @@ build/solutions/%: src/examples/% build/exercises.zip: $(EXERCISES) cd build; zip -r exercises.zip exercises > /dev/null +WORKING=src/examples/list_*.c +WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING)) +temp: $(WORKING_AUX) build build/tutorial.html ############################################################################## # Check that the examples all run correctly diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index fd8d9c0e..17b78106 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -1,66 +1,85 @@ CN Naming Conventions --------------------- -This document describes our (Benjamin and Liz's) best shot at a good -set of conventions for naming identifiers in CN, based on numerous -discussions and worked examples. +This document describes our (Benjamin and Liz's) current best shot at +a good set of conventions for naming identifiers in CN, based on +numerous discussions and worked examples. All the list-related files in src/examples have been converted to this convention -- do `ls src/examples/list*` to check it out. -# General Conventions +# Principles -- In general, identifiers are written in `snake_case` rather than `camlCase` +- When similar concepts exist in both C and CN, they should be named + so that the correspondence is immediately obvious. + - In particular, the C and CN versions of a given data structure + should have very similar names. -- C-level identifiers are `lowercase_initial` +- In text, we use the modifiers _CN-level_ vs. _C-level_ to + distinguish the two worlds. -- CN-level identifiers are `Uppercase_initial` +# General conventions -- A CN identifier that represents the state of a mutable data - structure after some function returns should be named the same as - the starting state of the data structure, with an `_` at the - end. - - E.g., The list copy function takes a linked list `l` - representing a sequence `L` and leaves `l` at the end pointing - to a final sequence `L_` such that `L == L_`. (Moreover, it - returns a new sequence `Ret` with `L == Ret`.) + ## For new code -## Questions: +When we're writing both C and CN code from scratch (e.g., in the +tutorial), we aim for maximal correspondence between -- Should CN-level identifiers be `Uppercase_initial` or - `Uppercase_Consistently_Throughout`? +- In general, CN identifiers are written in `snake_case` rather than `camlCase` - BCP find the former a bit lighter. Liz finds the latter to be more - consistent. If `List_int` is the identifier and `Rev_list_int` is - the function, then `list_int` is lowercase in the function even - though it is usually capital. (BCP admits this is a fair point.) - What do others think? +- C-level identifiers are `lowercase_consistently_throughout` -- Should predicates that extract some structure from the heap be named - the same as the structure they extract. I.e., should the result - type of the `Queue` predicate also be called `Queue`? +- CN-level identifiers are `Uppercase_Consistently_Throughout` - On one hand, there is clearly some potential for confusion. On the - other hand, types don't take an argument and predicates do, so it's - easy to disambiguate. - - On balance, I [BCP] prefer naming both the same; Liz prefers using - `Queue_at` for the predicate. +- A CN identifier that represents the state of a mutable data + structure after some function returns should be named the same as + the starting state of the data structure, with an `_post` at the + end. + - E.g., The list copy function takes a linked list `l` + representing a sequence `L` and leaves `l` at the end pointing + to a final sequence `L_post` such that `L == L_post`. + (Moreover, it returns a new sequence `Ret` with `L == Ret`.) + +- Predicates that extract some structure from the heap should be named + the same as the structure they extract. E.g., the result + type of the `Queue` predicate is also called `Queue`. + + *Discussion*: There is clearly some potential for confusion, and for + this reason Liz prefers using `Queue_at` for the predicate. On the + other hand hand, types don't take an argument and predicates do, so + it's easy to disambiguate. We're going with the lighter alternative + for the moment. + +## For existing code + +In existing C codebases, uppercase-initial identifiers are often used +for typedefs, structs, and enumerations. We should choose a +recommended standard convention for such cases -- e.g., "prefix +CN-level identifiers with `CN` when needed to avoid confusion with +C-level identifiers". Some experimentation will be needed to see +which convention we like best; this is left for future discussions. # Built-ins -- This proposal will also require changing some built-ins if we really - take it seriously +This proposal may also require changing some built-ins for +consistency. + - `i32` should change to `I32`, `u64` to `U64` - `is_null` to `Is_null` (or `Is_Null`) +*Discussion*: One point against this change is that CN currently tries +to use names reminiscent of Rust (`i32`, `u64`, etc.). I (BCP) do not +personally find this argument persuasive -- internal consistency seems +more important than miscellaeous points of similarity with some other +language. One way or the other, this will require a global decision. + # Polymorphism -How to name the "instances" of "morally polymorphic" functions (i.e., -should we write (i.e., whether to write `append__Int` or -`append__List_Int` rather than just `append`) is a tricky issue. On +One particularly tricky issue is how to name the "monomorphic +instances" of "morally polymorphic" functions (i.e., whether to write +`append__Int` or `append__List_Int` rather than just `append`). On one hand, `append__Int` is "more correct". On the other hand, these -extra annotations get pretty heavy. +extra annotations can get pretty heavy. We propose a compromise: @@ -77,23 +96,21 @@ We propose a compromise: - etc. 2. However, if, in a given project, a set of "morally polymorphic" - type definitions and library functions is only used at one - monomorphic instance (e.g., if some codebase only ever needs lists + type definitions and library functions is *only used at one + monomorphic instance* (e.g., if some codebase only ever uses lists of 32-bit signed ints), then the `__int` or `__I32` annotations are omitted. - This convention should be used in the CN tutorial, for example. + This convention is used in the CN tutorial, for example. TODO: Right now, the tutorial uses option (1). It was this exercise that convinced me [BCP] that option (2) was better. :-) -## Discussion - -One downside of this convention is that it might sometimes require -some after-the-fact renaming: If a project starts out using just lists -of signed ints and later needs to introduce lists of unsigned ints, -the old signed operations will need to be renamed. This seems like an -acceptable cost for keeping things light. +*Discussion*: One downside of this convention is that it might +sometimes require some after-the-fact renaming: If a project starts +out using just lists of signed ints and later needs to introduce lists +of unsigned ints, the old signed operations will need to be renamed. +This seems like an acceptable cost for keeping things light. Another downside is that it introduces two different ways of naming polymorphic things. But hopefully (a) the appropriate use of each is @@ -101,22 +118,6 @@ clear and (b) most C developments will actually fall in the second, lighter case, and programmers will never need to bother understanding the first case. -# Text conventions - -We need some consistent way of distinguishing "C-level" things from -"CN-level" things. Here are some possibilities: - -1. _abstract_ for CN-level ("mathematical") structures vs. _concrete_ - for C-level structures - -2. _specification-level_ vs. _implementation-level_ - -3. _CN-level_ vs. _C-level_ - -BCP thinks he likes the third best. Liz thinks all of these are good -options, but the first one communicates reality the most. What about -you? - # Loose ends - Do we need a convention for auxiliary predicates? From 1f903e1ea66cd48dbe79edfca8c3382ef9a1e3d3 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Mon, 12 Aug 2024 17:35:35 -0400 Subject: [PATCH 13/25] Tiny bit of renaming in progress --- Makefile | 9 +++++++-- src/examples/list_c_types.h | 16 ++++++++-------- src/examples/list_cn_types.h | 2 +- src/examples/list_constructors.h | 6 +++--- src/examples/list_copy.c | 8 ++++---- src/examples/list_free.c | 6 +++--- src/examples/list_length.c | 4 ++-- src/examples/list_rev.c | 10 +++++----- src/examples/list_rev_alt.c | 8 ++++---- 9 files changed, 37 insertions(+), 32 deletions(-) diff --git a/Makefile b/Makefile index c98725f9..5061738d 100644 --- a/Makefile +++ b/Makefile @@ -43,9 +43,14 @@ build/solutions/%: src/examples/% build/exercises.zip: $(EXERCISES) cd build; zip -r exercises.zip exercises > /dev/null -WORKING=src/examples/list_*.c +WORKING=$(ls src/examples/list_*.c) WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING)) -temp: $(WORKING_AUX) build build/tutorial.html +temp: $(WORKING_AUX) build +# build/tutorial.html + +foo: + @echo $(WORKING) + @echo $(WORKING_AUX) ############################################################################## # Check that the examples all run correctly diff --git a/src/examples/list_c_types.h b/src/examples/list_c_types.h index 2df81dba..6b7515aa 100644 --- a/src/examples/list_c_types.h +++ b/src/examples/list_c_types.h @@ -1,17 +1,17 @@ -struct list_int { +struct sllist { int head; - struct list_int* tail; + struct sllist* tail; }; -extern struct list_int *malloc_list_int(); -/*@ spec malloc_list_int(); +extern struct sllist *malloc_sllist(); +/*@ spec malloc_sllist(); requires true; - ensures take u = Block(return); + ensures take u = Block(return); @*/ -extern void free_list_int (struct list_int *p); -/*@ spec free_list_int(pointer p); - requires take u = Block(p); +extern void free_sllist (struct sllist *p); +/*@ spec free_sllist(pointer p); + requires take u = Block(p); ensures true; @*/ diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h index a7bb9d2c..26603a7e 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/list_cn_types.h @@ -16,7 +16,7 @@ predicate (datatype Seq_Int) Linked_List_Int(pointer p) { if (is_null(p)) { return Nil__Seq_Int{}; } else { - take h = Owned(p); + take h = Owned(p); take Tl = Linked_List_Int(h.tail); return (Cons__Seq_Int { Head: h.head, Tail: Tl }); } diff --git a/src/examples/list_constructors.h b/src/examples/list_constructors.h index c511d08c..29e352bf 100644 --- a/src/examples/list_constructors.h +++ b/src/examples/list_constructors.h @@ -1,4 +1,4 @@ -struct list_int* nil__list_int() +struct sllist* nil__sllist() /*@ ensures take Ret = Linked_List_Int(return); Ret == Nil__Seq_Int{}; @*/ @@ -6,13 +6,13 @@ struct list_int* nil__list_int() return 0; } -struct list_int* cons__list_int(int h, struct list_int* t) +struct sllist* cons__sllist(int h, struct sllist* t) /*@ requires take T = Linked_List_Int(t); ensures take Ret = Linked_List_Int(return); Ret == Cons__Seq_Int{ Head: h, Tail: T}; @*/ { - struct list_int *p = malloc_list_int(); + struct sllist *p = malloc_sllist(); p->head = h; p->tail = t; return p; diff --git a/src/examples/list_copy.c b/src/examples/list_copy.c index a6604ec0..d5862bc0 100644 --- a/src/examples/list_copy.c +++ b/src/examples/list_copy.c @@ -1,6 +1,6 @@ #include "list.h" -struct list_int* list_int_copy (struct list_int *l) +struct sllist* sllist_copy (struct sllist *l) /*@ requires take L = Linked_List_Int(l); ensures take L_ = Linked_List_Int(l); take Ret = Linked_List_Int(return); @@ -9,9 +9,9 @@ struct list_int* list_int_copy (struct list_int *l) @*/ { if (l == 0) { - return nil__list_int(); + return nil__sllist(); } else { - struct list_int *new_tail = list_int_copy(l->tail); - return cons__list_int(l->head, new_tail); + struct sllist *new_tail = sllist_copy(l->tail); + return cons__sllist(l->head, new_tail); } } diff --git a/src/examples/list_free.c b/src/examples/list_free.c index 09665a9d..29131232 100644 --- a/src/examples/list_free.c +++ b/src/examples/list_free.c @@ -1,14 +1,14 @@ #include "list.h" -void free_rec_list_int(struct list_int* l) +void free_rec_sllist(struct sllist* l) // You fill in the rest... /* --BEGIN-- */ /*@ requires take L = Linked_List_Int(l); @*/ { if (l == 0) { } else { - free_rec_list_int(l->tail); - free_list_int(l); + free_rec_sllist(l->tail); + free_sllist(l); } } /* --END-- */ diff --git a/src/examples/list_length.c b/src/examples/list_length.c index 04a0f51d..5febc033 100644 --- a/src/examples/list_length.c +++ b/src/examples/list_length.c @@ -17,7 +17,7 @@ function [rec] (u32) Length__Seq_Int(datatype Seq_Int L) { @*/ /* --END-- */ -unsigned int length__list_int (struct list_int *l) +unsigned int length__sllist (struct sllist *l) /* --BEGIN-- */ /*@ requires take L = Linked_List_Int(l); ensures take L_ = Linked_List_Int(l); @@ -35,6 +35,6 @@ unsigned int length__list_int (struct list_int *l) /* --BEGIN-- */ /*@ unfold Length__Seq_Int(L); @*/ /* --END-- */ - return 1 + length__list_int(l->tail); + return 1 + length__sllist(l->tail); } } diff --git a/src/examples/list_rev.c b/src/examples/list_rev.c index 1352ea6c..236159a8 100644 --- a/src/examples/list_rev.c +++ b/src/examples/list_rev.c @@ -3,7 +3,7 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct list_int* rev_aux__list_int(struct list_int* l1, struct list_int* l2) +struct sllist* rev_aux__sllist(struct sllist* l1, struct sllist* l2) /*@ requires take L1 = Linked_List_Int(l1); @*/ /*@ requires take L2 = Linked_List_Int(l2); @*/ /*@ ensures take R = Linked_List_Int(return); @*/ @@ -16,17 +16,17 @@ struct list_int* rev_aux__list_int(struct list_int* l1, struct list_int* l2) } else { /*@ unfold Rev__Seq_Int(L2); @*/ /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(L2)), Hd(L2), L1); @*/ - struct list_int *tmp = l2->tail; + struct sllist *tmp = l2->tail; l2->tail = l1; - return rev_aux__list_int(l2, tmp); + return rev_aux__sllist(l2, tmp); } } -struct list_int* rev__list_int(struct list_int* l1) +struct sllist* rev__sllist(struct sllist* l1) /*@ requires take L1 = Linked_List_Int(l1); @*/ /*@ ensures take L1_Rev = Linked_List_Int(return); @*/ /*@ ensures L1_Rev == Rev__Seq_Int(L1); @*/ { /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L1)); @*/ - return rev_aux__list_int (0, l1); + return rev_aux__sllist (0, l1); } diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c index fecfb481..fb861c2e 100644 --- a/src/examples/list_rev_alt.c +++ b/src/examples/list_rev_alt.c @@ -3,14 +3,14 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct list_int* rev_loop__list_int(struct list_int *l) +struct sllist* rev_loop__sllist(struct sllist *l) /*@ requires take L = Linked_List_Int(l); ensures take L_ = Linked_List_Int(return); L_ == Rev__Seq_Int(L); @*/ { - struct list_int *last = 0; - struct list_int *cur = l; + struct sllist *last = 0; + struct sllist *cur = l; /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L)); @*/ while(1) /*@ inv take Last = Linked_List_Int(last); @@ -23,7 +23,7 @@ struct list_int* rev_loop__list_int(struct list_int *l) /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, Last); @*/ return last; } - struct list_int *tmp = cur->tail; + struct sllist *tmp = cur->tail; cur->tail = last; last = cur; cur = tmp; From 2dd9ed05e307992a7726c07aac9c4ce1b2774a75 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Tue, 13 Aug 2024 22:11:04 -0400 Subject: [PATCH 14/25] Checkpoint renaming in progress --- Makefile | 6 +--- NAMING-CONVENTIONS.md | 2 +- .../simple-examples/working/malloc_1.c | 6 ++-- src/examples/Dbl_Linked_List/add.c | 2 +- .../Dbl_Linked_List/add_orig.broken.c | 2 +- src/examples/Dbl_Linked_List/headers.h | 2 +- src/examples/Dbl_Linked_List/malloc_free.h | 8 ++--- src/examples/Dbl_Linked_List/node_and_int.h | 8 ++--- src/examples/Dbl_Linked_List/remove.c | 4 +-- .../Dbl_Linked_List/remove_orig.broken.c | 4 +-- src/examples/Dbl_Linked_List/singleton.c | 2 +- src/examples/list.h | 2 +- src/examples/list_append.h | 8 ++--- src/examples/list_c_types.h | 8 ++--- src/examples/list_cn_types.h | 18 ++++------- src/examples/list_constructors.h | 16 +++++----- src/examples/list_copy.c | 14 ++++---- src/examples/list_free.c | 8 ++--- src/examples/list_hdtl.h | 14 ++++---- src/examples/list_length.c | 24 +++++++------- src/examples/list_rev.c | 32 +++++++++---------- src/examples/list_rev.h | 10 +++--- src/examples/list_rev_alt.c | 24 +++++++------- src/examples/list_rev_lemmas.h | 10 +++--- src/examples/list_snoc.h | 10 +++--- src/examples/slf_sized_stack.c | 10 +++--- src/tutorial.adoc | 2 +- 27 files changed, 123 insertions(+), 133 deletions(-) diff --git a/Makefile b/Makefile index 5061738d..6732dd46 100644 --- a/Makefile +++ b/Makefile @@ -43,15 +43,11 @@ build/solutions/%: src/examples/% build/exercises.zip: $(EXERCISES) cd build; zip -r exercises.zip exercises > /dev/null -WORKING=$(ls src/examples/list_*.c) +WORKING=$(wildcard src/examples/list_*.c) WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING)) temp: $(WORKING_AUX) build # build/tutorial.html -foo: - @echo $(WORKING) - @echo $(WORKING_AUX) - ############################################################################## # Check that the examples all run correctly diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 17b78106..49bc3aae 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -127,7 +127,7 @@ the first case. top-level `Queue` or `Queue_at` predicate has dealt with the non-recursive part of the structure). -- The current function `IntList_free_list` is hard to rename with +- The current function `IntList_free__list` is hard to rename with these conventions. It feels like it should be `free__int_list`, but that’s also the new name of the free function for individual list cells (opposite of `malloc`). Current solution is diff --git a/src/example-archive/simple-examples/working/malloc_1.c b/src/example-archive/simple-examples/working/malloc_1.c index cd837ed7..9259c221 100644 --- a/src/example-archive/simple-examples/working/malloc_1.c +++ b/src/example-archive/simple-examples/working/malloc_1.c @@ -3,19 +3,19 @@ // malloc() is not defined by default in CN. We can define a fake malloc() // function that only works on ints. -int *my_malloc_int() +int *my_malloc__int() /*@ trusted; @*/ /*@ ensures take New = Block(return); @*/ {} -int *malloc_1() +int *malloc__1() /*@ ensures take New = Owned(return); New == 7i32; *return == 7i32; @*/ // <-- Alternative syntax { int *new; - new = my_malloc_int(); + new = my_malloc__int(); *new = 7; // Have to initialize the memory before it's owned return new; } diff --git a/src/examples/Dbl_Linked_List/add.c b/src/examples/Dbl_Linked_List/add.c index b988d9a4..9bafd267 100644 --- a/src/examples/Dbl_Linked_List/add.c +++ b/src/examples/Dbl_Linked_List/add.c @@ -9,7 +9,7 @@ struct node *add(int element, struct node *n) : After == Dll { left: Seq_Cons{head: Node(Before).data, tail: Left(Before)}, curr: Node(After), right: Right(Before)}; @*/ { - struct node *new_node = malloc_node(); + struct node *new_node = malloc__node(); new_node->data = element; new_node->prev = 0; new_node->next = 0; diff --git a/src/examples/Dbl_Linked_List/add_orig.broken.c b/src/examples/Dbl_Linked_List/add_orig.broken.c index f8b9b306..0d60e519 100644 --- a/src/examples/Dbl_Linked_List/add_orig.broken.c +++ b/src/examples/Dbl_Linked_List/add_orig.broken.c @@ -3,7 +3,7 @@ // Adds after the given node and returns a pointer to the new node struct node *add(int element, struct node *n) { - struct node *new_node = malloc_node(); + struct node *new_node = malloc__node(); new_node->data = element; new_node->prev = 0; new_node->next = 0; diff --git a/src/examples/Dbl_Linked_List/headers.h b/src/examples/Dbl_Linked_List/headers.h index 963902fb..c2cd3c23 100644 --- a/src/examples/Dbl_Linked_List/headers.h +++ b/src/examples/Dbl_Linked_List/headers.h @@ -5,5 +5,5 @@ #include "./c_types.h" #include "./cn_types.h" #include "./getters.h" -#include "./malloc_free.h" +#include "./malloc__free.h" #include "./predicates.h" diff --git a/src/examples/Dbl_Linked_List/malloc_free.h b/src/examples/Dbl_Linked_List/malloc_free.h index 1937a5a3..c03dc804 100644 --- a/src/examples/Dbl_Linked_List/malloc_free.h +++ b/src/examples/Dbl_Linked_List/malloc_free.h @@ -1,12 +1,12 @@ -extern struct node *malloc_node(); -/*@ spec malloc_node(); +extern struct node *malloc__node(); +/*@ spec malloc__node(); requires true; ensures take u = Block(return); !ptr_eq(return,NULL); @*/ -extern void free_node (struct node *p); -/*@ spec free_node(pointer p); +extern void free__node (struct node *p); +/*@ spec free__node(pointer p); requires take u = Block(p); ensures true; @*/ \ No newline at end of file diff --git a/src/examples/Dbl_Linked_List/node_and_int.h b/src/examples/Dbl_Linked_List/node_and_int.h index faef87c7..dd223296 100644 --- a/src/examples/Dbl_Linked_List/node_and_int.h +++ b/src/examples/Dbl_Linked_List/node_and_int.h @@ -3,15 +3,15 @@ struct node_and_int { int data; }; -extern struct node_and_int *malloc_node_and_int(); -/*@ spec malloc_node_and_int(); +extern struct node_and_int *malloc__node_and_int(); +/*@ spec malloc__node_and_int(); requires true; ensures take u = Block(return); !ptr_eq(return,NULL); @*/ -extern void free_node_and_int (struct node_and_int *p); -/*@ spec free_node_and_int(pointer p); +extern void free__node_and_int (struct node_and_int *p); +/*@ spec free__node_and_int(pointer p); requires take u = Block(p); ensures true; @*/ \ No newline at end of file diff --git a/src/examples/Dbl_Linked_List/remove.c b/src/examples/Dbl_Linked_List/remove.c index 2a610db8..2d828214 100644 --- a/src/examples/Dbl_Linked_List/remove.c +++ b/src/examples/Dbl_Linked_List/remove.c @@ -27,10 +27,10 @@ struct node_and_int *remove(struct node *n) temp = n->next; } - struct node_and_int *pair = malloc_node_and_int(); + struct node_and_int *pair = malloc__node_and_int(); pair->node = temp; pair->data = n->data; - free_node(n); + free__node(n); return pair; } diff --git a/src/examples/Dbl_Linked_List/remove_orig.broken.c b/src/examples/Dbl_Linked_List/remove_orig.broken.c index b2617c69..5a4b8b24 100644 --- a/src/examples/Dbl_Linked_List/remove_orig.broken.c +++ b/src/examples/Dbl_Linked_List/remove_orig.broken.c @@ -15,10 +15,10 @@ struct node_and_int *remove(struct node *n) temp = n->next; } - struct node_and_int *pair = malloc_node_and_int(); + struct node_and_int *pair = malloc__node_and_int(); pair->node = temp; pair->data = n->data; - free_node(n); + free__node(n); return pair; } \ No newline at end of file diff --git a/src/examples/Dbl_Linked_List/singleton.c b/src/examples/Dbl_Linked_List/singleton.c index 15c8fd8a..3966f38d 100644 --- a/src/examples/Dbl_Linked_List/singleton.c +++ b/src/examples/Dbl_Linked_List/singleton.c @@ -5,7 +5,7 @@ struct node *singleton(int element) Ret == Dll{left: Seq_Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Seq_Nil{}}; @*/ { - struct node *n = malloc_node(); + struct node *n = malloc__node(); n->data = element; n->prev = 0; n->next = 0; diff --git a/src/examples/list.h b/src/examples/list.h index d93830dc..f3a8238f 100644 --- a/src/examples/list.h +++ b/src/examples/list.h @@ -6,4 +6,4 @@ #include "list_hdtl.h" #include "list_constructors.h" -#endif //_LIST_H +#endif //_LIST_H \ No newline at end of file diff --git a/src/examples/list_append.h b/src/examples/list_append.h index 2d89997c..0a54754c 100644 --- a/src/examples/list_append.h +++ b/src/examples/list_append.h @@ -1,13 +1,13 @@ // append.h /*@ -function [rec] (datatype Seq_Int) Append__Seq_Int(datatype Seq_Int L1, datatype Seq_Int L2) { +function [rec] (datatype List) AppendList(datatype List L1, datatype List L2) { match L1 { - Nil__Seq_Int {} => { + Nil {} => { L2 } - Cons__Seq_Int {Head : H, Tail : T} => { - Cons__Seq_Int {Head: H, Tail: Append__Seq_Int(T, L2)} + Cons {Head : H, Tail : T} => { + Cons {Head: H, Tail: AppendList(T, L2)} } } } diff --git a/src/examples/list_c_types.h b/src/examples/list_c_types.h index 6b7515aa..68d326aa 100644 --- a/src/examples/list_c_types.h +++ b/src/examples/list_c_types.h @@ -3,14 +3,14 @@ struct sllist { struct sllist* tail; }; -extern struct sllist *malloc_sllist(); -/*@ spec malloc_sllist(); +extern struct sllist *malloc__sllist(); +/*@ spec malloc__sllist(); requires true; ensures take u = Block(return); @*/ -extern void free_sllist (struct sllist *p); -/*@ spec free_sllist(pointer p); +extern void free__sllist (struct sllist *p); +/*@ spec free__sllist(pointer p); requires take u = Block(p); ensures true; @*/ diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h index 26603a7e..567b7c90 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/list_cn_types.h @@ -1,24 +1,20 @@ -// TODO: show people List_Int and List_Int_At and ask -// which is better for predicate name. -// (But perhaps Linked_List_Int is clearest?) - // We've kept Seq for the type of abstract sequences, since many // different concrete data structures are representations of abstract // lists. /*@ -datatype Seq_Int { - Nil__Seq_Int {}, - Cons__Seq_Int {i32 Head, datatype Seq_Int Tail} +datatype List { + Nil {}, + Cons {i32 Head, datatype List Tail} } -predicate (datatype Seq_Int) Linked_List_Int(pointer p) { +predicate (datatype List) SLList(pointer p) { if (is_null(p)) { - return Nil__Seq_Int{}; + return Nil{}; } else { take h = Owned(p); - take Tl = Linked_List_Int(h.tail); - return (Cons__Seq_Int { Head: h.head, Tail: Tl }); + take Tl = SLList(h.tail); + return (Cons { Head: h.head, Tail: Tl }); } } @*/ diff --git a/src/examples/list_constructors.h b/src/examples/list_constructors.h index 29e352bf..178fd8f7 100644 --- a/src/examples/list_constructors.h +++ b/src/examples/list_constructors.h @@ -1,18 +1,18 @@ -struct sllist* nil__sllist() -/*@ ensures take Ret = Linked_List_Int(return); - Ret == Nil__Seq_Int{}; +struct sllist* slnil() +/*@ ensures take Ret = SLList(return); + Ret == Nil{}; @*/ { return 0; } -struct sllist* cons__sllist(int h, struct sllist* t) -/*@ requires take T = Linked_List_Int(t); - ensures take Ret = Linked_List_Int(return); - Ret == Cons__Seq_Int{ Head: h, Tail: T}; +struct sllist* slcons(int h, struct sllist* t) +/*@ requires take T = SLList(t); + ensures take Ret = SLList(return); + Ret == Cons{ Head: h, Tail: T}; @*/ { - struct sllist *p = malloc_sllist(); + struct sllist *p = malloc__sllist(); p->head = h; p->tail = t; return p; diff --git a/src/examples/list_copy.c b/src/examples/list_copy.c index d5862bc0..d45678da 100644 --- a/src/examples/list_copy.c +++ b/src/examples/list_copy.c @@ -1,17 +1,17 @@ #include "list.h" -struct sllist* sllist_copy (struct sllist *l) -/*@ requires take L = Linked_List_Int(l); - ensures take L_ = Linked_List_Int(l); - take Ret = Linked_List_Int(return); +struct sllist* slcopy (struct sllist *l) +/*@ requires take L = SLList(l); + ensures take L_ = SLList(l); + take Ret = SLList(return); L == L_; L == Ret; @*/ { if (l == 0) { - return nil__sllist(); + return slnil(); } else { - struct sllist *new_tail = sllist_copy(l->tail); - return cons__sllist(l->head, new_tail); + struct sllist *new_tail = slcopy(l->tail); + return slcons(l->head, new_tail); } } diff --git a/src/examples/list_free.c b/src/examples/list_free.c index 29131232..db3a6f06 100644 --- a/src/examples/list_free.c +++ b/src/examples/list_free.c @@ -1,14 +1,14 @@ #include "list.h" -void free_rec_sllist(struct sllist* l) +void free__rec_sllist(struct sllist* l) // You fill in the rest... /* --BEGIN-- */ -/*@ requires take L = Linked_List_Int(l); @*/ +/*@ requires take L = SLList(l); @*/ { if (l == 0) { } else { - free_rec_sllist(l->tail); - free_sllist(l); + free__rec_sllist(l->tail); + free__sllist(l); } } /* --END-- */ diff --git a/src/examples/list_hdtl.h b/src/examples/list_hdtl.h index fac22546..e36738ff 100644 --- a/src/examples/list_hdtl.h +++ b/src/examples/list_hdtl.h @@ -1,21 +1,21 @@ /*@ -function (i32) Hd (datatype Seq_Int L) { +function (i32) Hd (datatype List L) { match L { - Nil__Seq_Int {} => { + Nil {} => { 0i32 } - Cons__Seq_Int {Head : H, Tail : _} => { + Cons {Head : H, Tail : _} => { H } } } -function (datatype Seq_Int) Tl (datatype Seq_Int L) { +function (datatype List) Tl (datatype List L) { match L { - Nil__Seq_Int {} => { - Nil__Seq_Int{} + Nil {} => { + Nil{} } - Cons__Seq_Int {Head : _, Tail : T} => { + Cons {Head : _, Tail : T} => { T } } diff --git a/src/examples/list_length.c b/src/examples/list_length.c index 5febc033..34dc15a8 100644 --- a/src/examples/list_length.c +++ b/src/examples/list_length.c @@ -1,40 +1,38 @@ -/* list_length.c */ -// TODO: u32 to U32 #include "list.h" /* --BEGIN-- */ /*@ -function [rec] (u32) Length__Seq_Int(datatype Seq_Int L) { +function [rec] (u32) Length(datatype List L) { match L { - Nil__Seq_Int {} => { + Nil {} => { 0u32 } - Cons__Seq_Int {Head : H, Tail : T} => { - 1u32 + Length__Seq_Int(T) + Cons {Head: H, Tail: T} => { + 1u32 + Length(T) } } } @*/ /* --END-- */ -unsigned int length__sllist (struct sllist *l) +unsigned int length (struct sllist *l) /* --BEGIN-- */ -/*@ requires take L = Linked_List_Int(l); - ensures take L_ = Linked_List_Int(l); +/*@ requires take L = SLList(l); + ensures take L_ = SLList(l); L == L_; - return == Length__Seq_Int(L); + return == Length(L); @*/ /* --END-- */ { if (l == 0) { /* --BEGIN-- */ - /*@ unfold Length__Seq_Int(L); @*/ + /*@ unfold Length(L); @*/ /* --END-- */ return 0; } else { /* --BEGIN-- */ - /*@ unfold Length__Seq_Int(L); @*/ + /*@ unfold Length(L); @*/ /* --END-- */ - return 1 + length__sllist(l->tail); + return 1 + length(l->tail); } } diff --git a/src/examples/list_rev.c b/src/examples/list_rev.c index 236159a8..ff16ce6c 100644 --- a/src/examples/list_rev.c +++ b/src/examples/list_rev.c @@ -3,30 +3,30 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct sllist* rev_aux__sllist(struct sllist* l1, struct sllist* l2) -/*@ requires take L1 = Linked_List_Int(l1); @*/ -/*@ requires take L2 = Linked_List_Int(l2); @*/ -/*@ ensures take R = Linked_List_Int(return); @*/ -/*@ ensures R == Append__Seq_Int(Rev__Seq_Int(L2), L1); @*/ +struct sllist* rev_aux(struct sllist* l1, struct sllist* l2) +/*@ requires take L1 = SLList(l1); @*/ +/*@ requires take L2 = SLList(l2); @*/ +/*@ ensures take R = SLList(return); @*/ +/*@ ensures R == AppendList(RevList(L2), L1); @*/ { if (l2 == 0) { - /*@ unfold Rev__Seq_Int(L2); @*/ - /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, L1); @*/ + /*@ unfold RevList(L2); @*/ + /*@ unfold AppendList(Nil{}, L1); @*/ return l1; } else { - /*@ unfold Rev__Seq_Int(L2); @*/ - /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(L2)), Hd(L2), L1); @*/ + /*@ unfold RevList(L2); @*/ + /*@ apply Append_Cons_RList(RevList(Tl(L2)), Hd(L2), L1); @*/ struct sllist *tmp = l2->tail; l2->tail = l1; - return rev_aux__sllist(l2, tmp); + return rev_aux(l2, tmp); } } -struct sllist* rev__sllist(struct sllist* l1) -/*@ requires take L1 = Linked_List_Int(l1); @*/ -/*@ ensures take L1_Rev = Linked_List_Int(return); @*/ -/*@ ensures L1_Rev == Rev__Seq_Int(L1); @*/ +struct sllist* rev(struct sllist* l1) +/*@ requires take L1 = SLList(l1); @*/ +/*@ ensures take L1_Rev = SLList(return); @*/ +/*@ ensures L1_Rev == RevList(L1); @*/ { - /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L1)); @*/ - return rev_aux__sllist (0, l1); + /*@ apply Append_Nil_RList(RevList(L1)); @*/ + return rev_aux (0, l1); } diff --git a/src/examples/list_rev.h b/src/examples/list_rev.h index 67174aa9..5398c6ad 100644 --- a/src/examples/list_rev.h +++ b/src/examples/list_rev.h @@ -1,13 +1,13 @@ #include "list_snoc.h" /*@ -function [rec] (datatype Seq_Int) Rev__Seq_Int(datatype Seq_Int L) { +function [rec] (datatype List) RevList(datatype List L) { match L { - Nil__Seq_Int {} => { - Nil__Seq_Int {} + Nil {} => { + Nil {} } - Cons__Seq_Int {Head : H, Tail : T} => { - Snoc__Seq_Int (Rev__Seq_Int(T), H) + Cons {Head : H, Tail : T} => { + SnocList (RevList(T), H) } } } diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c index fb861c2e..7178450b 100644 --- a/src/examples/list_rev_alt.c +++ b/src/examples/list_rev_alt.c @@ -3,31 +3,31 @@ #include "list_rev.h" #include "list_rev_lemmas.h" -struct sllist* rev_loop__sllist(struct sllist *l) -/*@ requires take L = Linked_List_Int(l); - ensures take L_ = Linked_List_Int(return); - L_ == Rev__Seq_Int(L); +struct sllist* rev_loop(struct sllist *l) +/*@ requires take L = SLList(l); + ensures take L_ = SLList(return); + L_ == RevList(L); @*/ { struct sllist *last = 0; struct sllist *cur = l; - /*@ apply Append_Nil_R__Seq_Int(Rev__Seq_Int(L)); @*/ + /*@ apply Append_Nil_RList(RevList(L)); @*/ while(1) - /*@ inv take Last = Linked_List_Int(last); - take Cur = Linked_List_Int(cur); - Append__Seq_Int(Rev__Seq_Int(Cur), Last) == Rev__Seq_Int(L); + /*@ inv take Last = SLList(last); + take Cur = SLList(cur); + AppendList(RevList(Cur), Last) == RevList(L); @*/ { if (cur == 0) { - /*@ unfold Rev__Seq_Int(Nil__Seq_Int{}); @*/ - /*@ unfold Append__Seq_Int(Nil__Seq_Int{}, Last); @*/ + /*@ unfold RevList(Nil{}); @*/ + /*@ unfold AppendList(Nil{}, Last); @*/ return last; } struct sllist *tmp = cur->tail; cur->tail = last; last = cur; cur = tmp; - /*@ unfold Rev__Seq_Int(Cur); @*/ - /*@ apply Append_Cons_R__Seq_Int(Rev__Seq_Int(Tl(Cur)), Hd(Cur), Last); @*/ + /*@ unfold RevList(Cur); @*/ + /*@ apply Append_Cons_RList(RevList(Tl(Cur)), Hd(Cur), Last); @*/ } } diff --git a/src/examples/list_rev_lemmas.h b/src/examples/list_rev_lemmas.h index 20615f2d..b1444a32 100644 --- a/src/examples/list_rev_lemmas.h +++ b/src/examples/list_rev_lemmas.h @@ -1,10 +1,10 @@ /*@ -lemma Append_Nil_R__Seq_Int (datatype Seq_Int L1) +lemma Append_Nil_RList (datatype List L1) requires true; - ensures Append__Seq_Int(L1, Nil__Seq_Int{}) == L1; + ensures AppendList(L1, Nil{}) == L1; -lemma Append_Cons_R__Seq_Int (datatype Seq_Int L1, i32 X, datatype Seq_Int L2) +lemma Append_Cons_RList (datatype List L1, i32 X, datatype List L2) requires true; - ensures Append__Seq_Int(L1, Cons__Seq_Int {Head: X, Tail: L2}) - == Append__Seq_Int(Snoc__Seq_Int(L1, X), L2); + ensures AppendList(L1, Cons {Head: X, Tail: L2}) + == AppendList(SnocList(L1, X), L2); @*/ diff --git a/src/examples/list_snoc.h b/src/examples/list_snoc.h index d9143701..dc80eebd 100644 --- a/src/examples/list_snoc.h +++ b/src/examples/list_snoc.h @@ -1,12 +1,12 @@ // TODO: change i32 to I32 /*@ -function [rec] (datatype Seq_Int) Snoc__Seq_Int(datatype Seq_Int Xs, i32 Y) { +function [rec] (datatype List) SnocList(datatype List Xs, i32 Y) { match Xs { - Nil__Seq_Int {} => { - Cons__Seq_Int {Head: Y, Tail: Nil__Seq_Int{}} + Nil {} => { + Cons {Head: Y, Tail: Nil{}} } - Cons__Seq_Int {Head: X, Tail: Zs} => { - Cons__Seq_Int{Head: X, Tail: Snoc__Seq_Int (Zs, Y)} + Cons {Head: X, Tail: Zs} => { + Cons{Head: X, Tail: SnocList (Zs, Y)} } } } diff --git a/src/examples/slf_sized_stack.c b/src/examples/slf_sized_stack.c index a258057d..c21b750e 100644 --- a/src/examples/slf_sized_stack.c +++ b/src/examples/slf_sized_stack.c @@ -18,16 +18,16 @@ predicate (sizeAndData) SizedStack(pointer p) { } @*/ -extern struct sized_stack *malloc_sized_stack (); +extern struct sized_stack *malloc__sized_stack (); /*@ -spec malloc_sized_stack(); +spec malloc__sized_stack(); requires true; ensures take u = Block(return); @*/ -extern void *free_sized_stack (struct sized_stack *p); +extern void *free__sized_stack (struct sized_stack *p); /*@ -spec free_sized_stack(pointer p); +spec free__sized_stack(pointer p); requires take u = Block(p); ensures true; @*/ @@ -37,7 +37,7 @@ struct sized_stack* create() S.s == 0u32; @*/ { - struct sized_stack *p = malloc_sized_stack(); + struct sized_stack *p = malloc__sized_stack(); p->size = 0; p->data = 0; /*@ unfold length(Seq_Nil {}); @*/ diff --git a/src/tutorial.adoc b/src/tutorial.adoc index e4d78dc0..7eaf229b 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -1270,7 +1270,7 @@ include_example(exercises/Dbl_Linked_List/getters.h) We also must include some boilerplate code for allocation and deallocation. -include_example(exercises/Dbl_Linked_List/malloc_free.h) +include_example(exercises/Dbl_Linked_List/malloc__free.h) And we compile all of these files into a single header file. From 8861f70e092b67d3dc93d110f50fcc2542edee1c Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Tue, 13 Aug 2024 22:31:14 -0400 Subject: [PATCH 15/25] Checkpoint further progress -- not ready for review yet --- src/examples/Dbl_Linked_List/add.c | 4 +- src/examples/Dbl_Linked_List/cn_types.h | 2 +- src/examples/Dbl_Linked_List/getters.h | 8 ++-- src/examples/Dbl_Linked_List/headers.h | 2 +- src/examples/Dbl_Linked_List/predicates.h | 12 ++--- src/examples/Dbl_Linked_List/singleton.c | 2 +- src/examples/append.c | 6 +-- src/examples/append2.c | 16 +++---- src/examples/list_cn_types.h | 10 ++--- src/examples/list_length.c | 2 +- src/examples/list_rev.h | 2 +- src/examples/list_rev_lemmas.h | 2 +- src/examples/list_snoc.h | 5 +-- src/examples/liste_rev_lemmas.h | 8 ++-- src/examples/mergesort.c | 54 +++++++++++------------ src/examples/queue_cn_types_1.h | 2 +- src/examples/queue_cn_types_2.h | 6 +-- src/examples/queue_cn_types_3.h | 6 +-- src/examples/queue_empty.c | 2 +- src/examples/queue_pop.c | 4 +- src/examples/queue_pop_lemma.h | 2 +- src/examples/queue_pop_lemma_stages.c | 28 ++++++------ src/examples/queue_pop_unified.c | 26 +++++------ src/examples/slf_length_acc.c | 14 +++--- src/examples/slf_sized_stack.c | 14 +++--- src/queue-example-notes.md | 54 +++++++++++------------ src/tutorial.adoc | 22 ++++----- 27 files changed, 155 insertions(+), 160 deletions(-) diff --git a/src/examples/Dbl_Linked_List/add.c b/src/examples/Dbl_Linked_List/add.c index 9bafd267..b6efc54a 100644 --- a/src/examples/Dbl_Linked_List/add.c +++ b/src/examples/Dbl_Linked_List/add.c @@ -5,8 +5,8 @@ struct node *add(int element, struct node *n) /*@ requires take Before = Dll_at(n); ensures take After = Dll_at(return); - is_null(n) ? After == Dll { left: Seq_Nil{}, curr: Node(After), right: Seq_Nil{}} - : After == Dll { left: Seq_Cons{head: Node(Before).data, tail: Left(Before)}, curr: Node(After), right: Right(Before)}; + is_null(n) ? After == Dll { left: Nil{}, curr: Node(After), right: Nil{}} + : After == Dll { left: Cons{Head: Node(Before).data, Tail: Left(Before)}, curr: Node(After), right: Right(Before)}; @*/ { struct node *new_node = malloc__node(); diff --git a/src/examples/Dbl_Linked_List/cn_types.h b/src/examples/Dbl_Linked_List/cn_types.h index 59278fb2..e82cf9fd 100644 --- a/src/examples/Dbl_Linked_List/cn_types.h +++ b/src/examples/Dbl_Linked_List/cn_types.h @@ -1,6 +1,6 @@ /*@ datatype Dll { Empty_Dll {}, - Dll {datatype seq left, struct node curr, datatype seq right} + Dll {datatype List left, struct node curr, datatype List right} } @*/ \ No newline at end of file diff --git a/src/examples/Dbl_Linked_List/getters.h b/src/examples/Dbl_Linked_List/getters.h index 9e180623..ff54d2d7 100644 --- a/src/examples/Dbl_Linked_List/getters.h +++ b/src/examples/Dbl_Linked_List/getters.h @@ -1,14 +1,14 @@ /*@ -function (datatype seq) Right (datatype Dll L) { +function (datatype List) Right (datatype Dll L) { match L { - Empty_Dll {} => { Seq_Nil{} } + Empty_Dll {} => { Nil{} } Dll {left: _, curr: _, right: r} => { r } } } -function (datatype seq) Left (datatype Dll L) { +function (datatype List) Left (datatype Dll L) { match L { - Empty_Dll {} => { Seq_Nil {} } + Empty_Dll {} => { Nil {} } Dll {left: l, curr: _, right: _} => { l } } } diff --git a/src/examples/Dbl_Linked_List/headers.h b/src/examples/Dbl_Linked_List/headers.h index c2cd3c23..963902fb 100644 --- a/src/examples/Dbl_Linked_List/headers.h +++ b/src/examples/Dbl_Linked_List/headers.h @@ -5,5 +5,5 @@ #include "./c_types.h" #include "./cn_types.h" #include "./getters.h" -#include "./malloc__free.h" +#include "./malloc_free.h" #include "./predicates.h" diff --git a/src/examples/Dbl_Linked_List/predicates.h b/src/examples/Dbl_Linked_List/predicates.h index a5353591..c5c4d54a 100644 --- a/src/examples/Dbl_Linked_List/predicates.h +++ b/src/examples/Dbl_Linked_List/predicates.h @@ -10,27 +10,27 @@ predicate (datatype Dll) Dll_at (pointer p) { } } -predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) { +predicate (datatype List) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) { if (is_null(p)) { - return Seq_Nil{}; + return Nil{}; } else { take n = Owned(p); assert (ptr_eq(n.prev, prev_pointer)); assert(ptr_eq(prev_node.next, p)); take Right = Own_Forwards(n.next, p, n); - return Seq_Cons{head: n.data, tail: Right}; + return Cons{Head: n.data, Tail: Right}; } } -predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) { +predicate (datatype List) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) { if (is_null(p)) { - return Seq_Nil{}; + return Nil{}; } else { take n = Owned(p); assert (ptr_eq(n.next, next_pointer)); assert(ptr_eq(next_node.prev, p)); take Left = Own_Backwards(n.prev, p, n); - return Seq_Cons{head: n.data, tail: Left}; + return Cons{Head: n.data, Tail: Left}; } } @*/ \ No newline at end of file diff --git a/src/examples/Dbl_Linked_List/singleton.c b/src/examples/Dbl_Linked_List/singleton.c index 3966f38d..008daadb 100644 --- a/src/examples/Dbl_Linked_List/singleton.c +++ b/src/examples/Dbl_Linked_List/singleton.c @@ -2,7 +2,7 @@ struct node *singleton(int element) /*@ ensures take Ret = Dll_at(return); - Ret == Dll{left: Seq_Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Seq_Nil{}}; + Ret == Dll{left: Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Nil{}}; @*/ { struct node *n = malloc__node(); diff --git a/src/examples/append.c b/src/examples/append.c index ff3309a0..d4214f4d 100644 --- a/src/examples/append.c +++ b/src/examples/append.c @@ -2,9 +2,9 @@ #include "list_append.h" struct int_list* IntList_append(struct int_list* xs, struct int_list* ys) -/*@ requires take L1 = IntList(xs); @*/ -/*@ requires take L2 = IntList(ys); @*/ -/*@ ensures take L3 = IntList(return); @*/ +/*@ requires take L1 = SLList(xs); @*/ +/*@ requires take L2 = SLList(ys); @*/ +/*@ ensures take L3 = SLList(return); @*/ /*@ ensures L3 == append(L1, L2); @*/ { if (xs == 0) { diff --git a/src/examples/append2.c b/src/examples/append2.c index a966e428..c91cdf78 100644 --- a/src/examples/append2.c +++ b/src/examples/append2.c @@ -2,9 +2,9 @@ #include "list_append.h" struct int_list* IntList_copy (struct int_list *xs) -/*@ requires take L1 = IntList(xs); - ensures take L1_ = IntList(xs); - take L2 = IntList(return); +/*@ requires take L1 = SLList(xs); + ensures take L1_ = SLList(xs); + take L2 = SLList(return); L1 == L1_; L1 == L2; @*/ @@ -19,11 +19,11 @@ struct int_list* IntList_copy (struct int_list *xs) struct int_list* IntList_append2 (struct int_list *xs, struct int_list *ys) /* --BEGIN-- */ -/*@ requires take L1 = IntList(xs); @*/ -/*@ requires take L2 = IntList(ys); @*/ -/*@ ensures take L1_ = IntList(xs); @*/ -/*@ ensures take L2_ = IntList(ys); @*/ -/*@ ensures take L3 = IntList(return); @*/ +/*@ requires take L1 = SLList(xs); @*/ +/*@ requires take L2 = SLList(ys); @*/ +/*@ ensures take L1_ = SLList(xs); @*/ +/*@ ensures take L2_ = SLList(ys); @*/ +/*@ ensures take L3 = SLList(return); @*/ /*@ ensures L3 == append(L1, L2); @*/ /*@ ensures L1 == L1_; @*/ /*@ ensures L2 == L2_; @*/ diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h index 567b7c90..26020bf4 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/list_cn_types.h @@ -1,7 +1,3 @@ -// We've kept Seq for the type of abstract sequences, since many -// different concrete data structures are representations of abstract -// lists. - /*@ datatype List { Nil {}, @@ -12,9 +8,9 @@ predicate (datatype List) SLList(pointer p) { if (is_null(p)) { return Nil{}; } else { - take h = Owned(p); - take Tl = SLList(h.tail); - return (Cons { Head: h.head, Tail: Tl }); + take H = Owned(p); + take Tl = SLList(H.tail); + return (Cons { Head: H.head, Tail: Tl }); } } @*/ diff --git a/src/examples/list_length.c b/src/examples/list_length.c index 34dc15a8..5167136b 100644 --- a/src/examples/list_length.c +++ b/src/examples/list_length.c @@ -7,7 +7,7 @@ function [rec] (u32) Length(datatype List L) { Nil {} => { 0u32 } - Cons {Head: H, Tail: T} => { + Cons {Head: H, Tail : T} => { 1u32 + Length(T) } } diff --git a/src/examples/list_rev.h b/src/examples/list_rev.h index 5398c6ad..eeda4df0 100644 --- a/src/examples/list_rev.h +++ b/src/examples/list_rev.h @@ -7,7 +7,7 @@ function [rec] (datatype List) RevList(datatype List L) { Nil {} } Cons {Head : H, Tail : T} => { - SnocList (RevList(T), H) + Snoc (RevList(T), H) } } } diff --git a/src/examples/list_rev_lemmas.h b/src/examples/list_rev_lemmas.h index b1444a32..f2cba579 100644 --- a/src/examples/list_rev_lemmas.h +++ b/src/examples/list_rev_lemmas.h @@ -6,5 +6,5 @@ lemma Append_Nil_RList (datatype List L1) lemma Append_Cons_RList (datatype List L1, i32 X, datatype List L2) requires true; ensures AppendList(L1, Cons {Head: X, Tail: L2}) - == AppendList(SnocList(L1, X), L2); + == AppendList(Snoc(L1, X), L2); @*/ diff --git a/src/examples/list_snoc.h b/src/examples/list_snoc.h index dc80eebd..97a27f77 100644 --- a/src/examples/list_snoc.h +++ b/src/examples/list_snoc.h @@ -1,12 +1,11 @@ -// TODO: change i32 to I32 /*@ -function [rec] (datatype List) SnocList(datatype List Xs, i32 Y) { +function [rec] (datatype List) Snoc(datatype List Xs, i32 Y) { match Xs { Nil {} => { Cons {Head: Y, Tail: Nil{}} } Cons {Head: X, Tail: Zs} => { - Cons{Head: X, Tail: SnocList (Zs, Y)} + Cons{Head: X, Tail: Snoc (Zs, Y)} } } } diff --git a/src/examples/liste_rev_lemmas.h b/src/examples/liste_rev_lemmas.h index c4554e40..d5c8976d 100644 --- a/src/examples/liste_rev_lemmas.h +++ b/src/examples/liste_rev_lemmas.h @@ -1,10 +1,10 @@ /*@ -lemma append_nil_r (datatype seq l1) +lemma append_nil_r (datatype List l1) requires true - ensures append(l1, Seq_Nil {}) == l1 + ensures append(l1, Nil {}) == l1 -lemma append_cons_r (datatype seq l1, i32 x, datatype seq l2) +lemma append_cons_r (datatype List l1, i32 x, datatype List l2) requires true - ensures append(l1, Seq_Cons {head: x, tail: l2}) + ensures append(l1, Cons {Head: x, Tail: l2}) == append(snoc(l1, x), l2) @*/ diff --git a/src/examples/mergesort.c b/src/examples/mergesort.c index 5c6c13bd..5a837d8a 100644 --- a/src/examples/mergesort.c +++ b/src/examples/mergesort.c @@ -1,44 +1,44 @@ #include "list.h" /*@ -function [rec] ({datatype seq fst, datatype seq snd}) split(datatype seq xs) +function [rec] ({datatype List fst, datatype List snd}) split(datatype List xs) { match xs { - Seq_Nil {} => { - {fst: Seq_Nil{}, snd: Seq_Nil{}} + Nil {} => { + {fst: Nil{}, snd: Nil{}} } - Seq_Cons {head: h1, tail: Seq_Nil{}} => { - {fst: Seq_Nil{}, snd: xs} + Cons {Head: h1, Tail: Nil{}} => { + {fst: Nil{}, snd: xs} } - Seq_Cons {head: h1, tail: Seq_Cons {head : h2, tail : tl2 }} => { + Cons {Head: h1, Tail: Cons {Head : h2, tail : tl2 }} => { let P = split(tl2); - {fst: Seq_Cons { head: h1, tail: P.fst}, - snd: Seq_Cons { head: h2, tail: P.snd}} + {fst: Cons { Head: h1, Tail: P.fst}, + snd: Cons { Head: h2, Tail: P.snd}} } } } -function [rec] (datatype seq) merge(datatype seq xs, datatype seq ys) { +function [rec] (datatype List) merge(datatype List xs, datatype List ys) { match xs { - Seq_Nil {} => { ys } - Seq_Cons {head: x, tail: xs1} => { + Nil {} => { ys } + Cons {Head: x, Tail: xs1} => { match ys { - Seq_Nil {} => { xs } - Seq_Cons{ head: y, tail: ys1} => { + Nil {} => { xs } + Cons{ Head: y, Tail: ys1} => { (x < y) ? - (Seq_Cons{ head: x, tail: merge(xs1, ys) }) - : (Seq_Cons{ head: y, tail: merge(xs, ys1) }) + (Cons{ Head: x, Tail: merge(xs1, ys) }) + : (Cons{ Head: y, Tail: merge(xs, ys1) }) } } } } } -function [rec] (datatype seq) mergesort(datatype seq xs) { +function [rec] (datatype List) mergesort(datatype List xs) { match xs { - Seq_Nil{} => { xs } - Seq_Cons{head: x, tail: Seq_Nil{}} => { xs } - Seq_Cons{head: x, tail: Seq_Cons{head: y, tail: zs}} => { + Nil{} => { xs } + Cons{Head: x, Tail: Nil{}} => { xs } + Cons{Head: x, Tail: Cons{Head: y, Tail: zs}} => { let P = split(xs); let L1 = mergesort(P.fst); let L2 = mergesort(P.snd); @@ -54,9 +54,9 @@ struct int_list_pair { }; struct int_list_pair split(struct int_list *xs) -/*@ requires take Xs = IntList(xs); @*/ -/*@ ensures take Ys = IntList(return.fst); @*/ -/*@ ensures take Zs = IntList(return.snd); @*/ +/*@ requires take Xs = SLList(xs); @*/ +/*@ ensures take Ys = SLList(return.fst); @*/ +/*@ ensures take Zs = SLList(return.snd); @*/ /*@ ensures {fst: Ys, snd: Zs} == split(Xs); @*/ { if (xs == 0) { @@ -81,9 +81,9 @@ struct int_list_pair split(struct int_list *xs) } struct int_list* merge(struct int_list *xs, struct int_list *ys) -/*@ requires take Xs = IntList(xs); @*/ -/*@ requires take Ys = IntList(ys); @*/ -/*@ ensures take Zs = IntList(return); @*/ +/*@ requires take Xs = SLList(xs); @*/ +/*@ requires take Ys = SLList(ys); @*/ +/*@ ensures take Zs = SLList(return); @*/ /*@ ensures Zs == merge(Xs, Ys); @*/ { if (xs == 0) { @@ -110,8 +110,8 @@ struct int_list* merge(struct int_list *xs, struct int_list *ys) } struct int_list* mergesort(struct int_list *xs) -/*@ requires take Xs = IntList(xs); @*/ -/*@ ensures take Ys = IntList(return); @*/ +/*@ requires take Xs = SLList(xs); @*/ +/*@ ensures take Ys = SLList(return); @*/ /*@ ensures Ys == mergesort(Xs); @*/ { if (xs == 0) { diff --git a/src/examples/queue_cn_types_1.h b/src/examples/queue_cn_types_1.h index 705eff65..0066a60a 100644 --- a/src/examples/queue_cn_types_1.h +++ b/src/examples/queue_cn_types_1.h @@ -1,5 +1,5 @@ /*@ -predicate (datatype seq) IntQueuePtr (pointer q) { +predicate (datatype List) IntQueuePtr (pointer q) { take Q = Owned(q); assert ( (is_null(Q.front) && is_null(Q.back)) || (!is_null(Q.front) && !is_null(Q.back))); diff --git a/src/examples/queue_cn_types_2.h b/src/examples/queue_cn_types_2.h index d8e724f3..5d1f825c 100644 --- a/src/examples/queue_cn_types_2.h +++ b/src/examples/queue_cn_types_2.h @@ -1,12 +1,12 @@ /*@ -predicate (datatype seq) IntQueueFB (pointer front, pointer back) { +predicate (datatype List) IntQueueFB (pointer front, pointer back) { if (is_null(front)) { - return Seq_Nil{}; + return Nil{}; } else { take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - return snoc(L, B.first); + return Snoc(L, B.first); } } @*/ diff --git a/src/examples/queue_cn_types_3.h b/src/examples/queue_cn_types_3.h index 99f22eb0..721930a3 100644 --- a/src/examples/queue_cn_types_3.h +++ b/src/examples/queue_cn_types_3.h @@ -1,12 +1,12 @@ /*@ -predicate (datatype seq) IntQueueAux (pointer f, pointer b) { +predicate (datatype List) IntQueueAux (pointer f, pointer b) { if (ptr_eq(f,b)) { - return Seq_Nil{}; + return Nil{}; } else { take F = Owned(f); assert (!is_null(F.next)); take B = IntQueueAux(F.next, b); - return Seq_Cons{head: F.first, tail: B}; + return Cons{Head: F.first, Tail: B}; } } @*/ diff --git a/src/examples/queue_empty.c b/src/examples/queue_empty.c index d2a8f3c7..27c0b921 100644 --- a/src/examples/queue_empty.c +++ b/src/examples/queue_empty.c @@ -3,7 +3,7 @@ struct int_queue* IntQueue_empty () /* --BEGIN-- */ /*@ ensures take ret = IntQueuePtr(return); - ret == Seq_Nil{}; + ret == Nil{}; @*/ /* --END-- */ { diff --git a/src/examples/queue_pop.c b/src/examples/queue_pop.c index d1053c25..317c0a92 100644 --- a/src/examples/queue_pop.c +++ b/src/examples/queue_pop.c @@ -3,7 +3,7 @@ int IntQueue_pop (struct int_queue *q) /*@ requires take before = IntQueuePtr(q); - before != Seq_Nil{}; + before != Nil{}; ensures take after = IntQueuePtr(q); after == tl(before); return == hd(before); @@ -16,7 +16,7 @@ int IntQueue_pop (struct int_queue *q) freeIntQueueCell(h); q->front = 0; q->back = 0; - /*@ unfold snoc(Seq_Nil{}, x); @*/ + /*@ unfold snoc(Nil{}, x); @*/ return x; } else { int x = h->first; diff --git a/src/examples/queue_pop_lemma.h b/src/examples/queue_pop_lemma.h index 80d2ab90..cf0175fc 100644 --- a/src/examples/queue_pop_lemma.h +++ b/src/examples/queue_pop_lemma.h @@ -7,7 +7,7 @@ lemma snoc_facts (pointer front, pointer back, i32 x) take NewQ = IntQueueAux(front, back); take NewB = Owned(back); Q == NewQ; B == NewB; - let L = snoc (Seq_Cons{head: x, tail: Q}, B.first); + let L = snoc (Cons{Head: x, Tail: Q}, B.first); hd(L) == x; tl(L) == snoc (Q, B.first); @*/ diff --git a/src/examples/queue_pop_lemma_stages.c b/src/examples/queue_pop_lemma_stages.c index 66043b8d..157b4053 100644 --- a/src/examples/queue_pop_lemma_stages.c +++ b/src/examples/queue_pop_lemma_stages.c @@ -5,22 +5,22 @@ /*@ -predicate (datatype seq) Pre(pointer front, pointer back, i32 popped, datatype seq before) { +predicate (datatype List) Pre(pointer front, pointer back, i32 popped, datatype List before) { if (is_null(front)) { - let after = Seq_Nil{}; - assert (before == snoc(Seq_Nil{}, popped)); + let after = Nil{}; + assert (before == snoc(Nil{}, popped)); return after; } else { take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - assert (before == snoc(Seq_Cons {head: popped, tail: L}, B.first)); + assert (before == snoc(Cons {Head: popped, Tail: L}, B.first)); let after = snoc(L, B.first); return after; } } -lemma lemma1(pointer front, pointer back, i32 popped, datatype seq before) +lemma lemma1(pointer front, pointer back, i32 popped, datatype List before) requires take Q = Pre(front, back, popped, before); ensures @@ -32,10 +32,10 @@ ensures /*@ -predicate (datatype seq) Post(pointer front, pointer back, i32 popped, datatype seq before) { +predicate (datatype List) Post(pointer front, pointer back, i32 popped, datatype List before) { if (is_null(front)) { - assert (before == snoc(Seq_Nil{}, popped)); - let after = Seq_Nil{}; + assert (before == snoc(Nil{}, popped)); + let after = Nil{}; assert (after == tl(before)); assert (popped == hd(before)); return after; @@ -43,7 +43,7 @@ predicate (datatype seq) Post(pointer front, pointer back, i32 popped, datatype take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - assert (before == snoc(Seq_Cons {head: popped, tail: L}, B.first)); + assert (before == snoc(Cons {Head: popped, Tail: L}, B.first)); let after = snoc(L, B.first); assert (after == tl(before)); assert (popped == hd(before)); @@ -51,7 +51,7 @@ predicate (datatype seq) Post(pointer front, pointer back, i32 popped, datatype } } -lemma lemma2(pointer front, pointer back, i32 popped, datatype seq before) +lemma lemma2(pointer front, pointer back, i32 popped, datatype List before) requires take Q = Pre(front, back, popped, before); ensures @@ -65,20 +65,20 @@ ensures /*@ -type_synonym result = { datatype seq after, datatype seq before } +type_synonym result = { datatype List after, datatype List before } predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) { if (is_null(front)) { - return { after: Seq_Nil{}, before: snoc(Seq_Nil{}, popped) }; + return { after: Nil{}, before: snoc(Nil{}, popped) }; } else { take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - return { after: snoc(L, B.first), before: snoc(Seq_Cons {head: popped, tail: L}, B.first) }; + return { after: snoc(L, B.first), before: snoc(Cons {Head: popped, Tail: L}, B.first) }; } } -lemma lemma3(pointer front, pointer back, i32 popped, datatype seq before) +lemma lemma3(pointer front, pointer back, i32 popped, datatype List before) requires take Q = Queue_pop_lemma(front, back, popped); before == Q.before; diff --git a/src/examples/queue_pop_unified.c b/src/examples/queue_pop_unified.c index da0b8018..f15f0136 100644 --- a/src/examples/queue_pop_unified.c +++ b/src/examples/queue_pop_unified.c @@ -1,16 +1,16 @@ #include "queue_headers.h" /*@ -type_synonym result = { datatype seq after, datatype seq before } +type_synonym result = { datatype List after, datatype List before } predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) { if (is_null(front)) { - return { after: Seq_Nil{}, before: snoc(Seq_Nil{}, popped) }; + return { after: Nil{}, before: Snoc(Nil{}, popped) }; } else { take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - return { after: snoc(L, B.first), before: snoc(Seq_Cons {head: popped, tail: L}, B.first) }; + return { after: Snoc(L, B.first), before: Snoc(Cons {Head: popped, Tail: L}, B.first) }; } } @*/ @@ -24,12 +24,12 @@ ensures take NewQ = IntQueueAux(front, back); take NewB = Owned(back); Q == NewQ; B == NewB; - let L = snoc (Seq_Cons{head: x, tail: Q}, B.first); - hd(L) == x; - tl(L) == snoc (Q, B.first); + let L = Snoc (Cons{Head: x, Tail: Q}, B.first); + Hd(L) == x; + Tl(L) == Snoc (Q, B.first); @*/ { - /*@ unfold snoc (Seq_Cons{head: x, tail: Q}, B.first); @*/ + /*@ unfold Snoc (Cons{Head: x, Tail: Q}, B.first); @*/ } void snoc_fact_unified(struct int_queueCell *front, struct int_queueCell *back, int x) @@ -39,12 +39,12 @@ requires ensures take NewAB = Queue_pop_lemma(front, back, x); AB == NewAB; - AB.after == tl(AB.before); - x == hd(AB.before); + AB.after == Tl(AB.before); + x == Hd(AB.before); @*/ { if (!front) { - /*@ unfold snoc(Seq_Nil{}, x); @*/ + /*@ unfold Snoc(Nil{}, x); @*/ } else { snoc_fact(front, back, x); } @@ -52,10 +52,10 @@ ensures int IntQueue_pop (struct int_queue *q) /*@ requires take before = IntQueuePtr(q); - before != Seq_Nil{}; + before != Nil{}; ensures take after = IntQueuePtr(q); - after == tl(before); - return == hd(before); + after == Tl(before); + return == Hd(before); @*/ { /*@ split_case is_null(q->front); @*/ diff --git a/src/examples/slf_length_acc.c b/src/examples/slf_length_acc.c index 34d85294..0b491a88 100644 --- a/src/examples/slf_length_acc.c +++ b/src/examples/slf_length_acc.c @@ -3,12 +3,12 @@ #include "free.h" /*@ -function [rec] (u32) length(datatype seq xs) { +function [rec] (u32) length(datatype List xs) { match xs { - Seq_Nil {} => { + Nil {} => { 0u32 } - Seq_Cons {head : h, tail : zs} => { + Cons {Head : h, tail : zs} => { 1u32 + length(zs) } } @@ -16,9 +16,9 @@ function [rec] (u32) length(datatype seq xs) { @*/ void IntList_length_acc_aux (struct int_list *xs, unsigned int *p) -/*@ requires take L1 = IntList(xs); +/*@ requires take L1 = SLList(xs); take n = Owned(p); - ensures take L1_ = IntList(xs); + ensures take L1_ = SLList(xs); take n_ = Owned(p); L1 == L1_; n_ == n + length(L1); @@ -33,8 +33,8 @@ void IntList_length_acc_aux (struct int_list *xs, unsigned int *p) } unsigned int IntList_length_acc (struct int_list *xs) -/*@ requires take L1 = IntList(xs); - ensures take L1_ = IntList(xs); +/*@ requires take L1 = SLList(xs); + ensures take L1_ = SLList(xs); L1 == L1_; return == length(L1); @*/ diff --git a/src/examples/slf_sized_stack.c b/src/examples/slf_sized_stack.c index c21b750e..351b5f2e 100644 --- a/src/examples/slf_sized_stack.c +++ b/src/examples/slf_sized_stack.c @@ -7,13 +7,13 @@ struct sized_stack { }; /*@ -type_synonym sizeAndData = {u32 s, datatype seq d} +type_synonym sizeAndData = {u32 s, datatype List d} predicate (sizeAndData) SizedStack(pointer p) { take S = Owned(p); let s = S.size; - take d = IntList(S.data); - assert(s == length(d)); + take d = SLList(S.data); + assert(s == Length(d)); return { s: s, d: d }; } @*/ @@ -40,7 +40,7 @@ struct sized_stack* create() struct sized_stack *p = malloc__sized_stack(); p->size = 0; p->data = 0; - /*@ unfold length(Seq_Nil {}); @*/ + /*@ unfold length(Nil {}); @*/ return p; } @@ -62,15 +62,15 @@ void push (struct sized_stack *p, int x) /* ---BEGIN--- */ /*@ requires take S = SizedStack(p); ensures take S_ = SizedStack(p); - S_.d == Seq_Cons {head:x, tail:S.d}; + S_.d == Cons {Head:x, Tail:S.d}; @*/ /* ---END--- */ { - struct int_list *data = IntList_cons(x, p->data); + struct int_list *data = slcons(x, p->data); p->size++; p->data = data; /* ---BEGIN--- */ - /*@ unfold length (Seq_Cons {head: x, tail: S.d}); @*/ + /*@ unfold length (Cons {Head: x, Tail: S.d}); @*/ /* ---END--- */ } diff --git a/src/queue-example-notes.md b/src/queue-example-notes.md index 09eb24c9..087648b3 100644 --- a/src/queue-example-notes.md +++ b/src/queue-example-notes.md @@ -1,8 +1,8 @@ 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. +- 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(Nil{}, x) ends up reducing to itself. -- Code used q->tail == 0 but predicate was testing q->head. Can adjust predicate, code, or use a split_case. +- Code used q->tail == 0 but predicate was testing q->Head. Can adjust predicate, code, or use a split_case. - Under-constrained counter-examples are something to be aware of (though the inconsitency came because of the definition of snoc here rather than l here). @@ -22,37 +22,37 @@ More notes: Here's the predicate for queues: - predicate (datatype seq) IntQueue(pointer q) { + predicate (datatype List) 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)) { + predicate (datatype List) IntQueue1(pointer dummy, struct int_queue H) { + if (is_null(H.Head)) { assert (is_null(H.tail)); - return (Seq_Nil{}); + return (Nil{}); } else { assert (!is_null(H.tail)); - take Q = IntQueueAux (H.head, H.tail); + take Q = IntQueueAux (H.Head, H.tail); return Q; } } - predicate (datatype seq) IntQueueAux(pointer h, pointer t) { + predicate (datatype List) IntQueueAux(pointer h, pointer t) { take C = Owned(h); take L = IntQueueAux1(h, C, t); return L; } - predicate (datatype seq) IntQueueAux1 + predicate (datatype List) IntQueueAux1 (pointer h, struct int_queueCell C, pointer t) { if (is_null(C.next)) { assert (h == t); - return (Seq_Cons{head: C.first, tail: Seq_Nil{}}); + return (Cons{Head: C.first, Tail: Nil{}}); } else { take TL = IntQueueAux(C.next, t); - return (Seq_Cons { head: C.first, tail: TL }); + return (Cons { Head: C.first, Tail: TL }); } } @@ -80,11 +80,11 @@ This fails because there are not enough annotations in the body of push. Confusingly, the HTML error report gives this as the unproven constraint - Seq_Cons {head: x, tail: Seq_Nil {}} == snoc(l, x) + Cons {Head: x, Tail: Nil {}} == snoc(l, x) while the list of Terms shows that - Seq_Cons {head: x, tail: Seq_Nil {}} == snoc(l, x) + Cons {Head: x, Tail: Nil {}} == snoc(l, x) has value false! @@ -111,7 +111,7 @@ not, so even to look "one level deep" we need an unfold.) Once we've unfolded, we get some more hints: - - Look at the value of l in Terms: Seq_Cons {head: 0i32, tail: Seq_Nil {}} + - Look at the value of l in Terms: Cons {Head: 0i32, Tail: Nil {}} - But we are in the empty queue case, so this seems fishy. - Now, in the constraints, we see l == unpack_IntQueue1.Q - Then look at the resources and see that unpack_IntQueue1.Q has not @@ -119,7 +119,7 @@ Once we've unfolded, we get some more hints: IntQueue1(q, unpack_IntQueue1.H)(unpack_IntQueue1.Q) - This means that CN did not have enough information to decide which way the conditional at the beginning of IntQueue1 is going to go. - - But the condition is testing H.head, while the conditional in the + - But the condition is testing H.Head, while the conditional in the code is testing the tail field! - We could get around this mismatch by adjusting the condition itself, or by adjusting the predicate. E.g., we could change the @@ -128,12 +128,12 @@ Once we've unfolded, we get some more hints: This tells us to look at snoc, which turns out to be very wrong! - function [rec] (datatype seq) snoc(datatype seq xs, i32 y) { + function [rec] (datatype List) snoc(datatype List xs, i32 y) { match xs { - Seq_Nil {} => { - Seq_Nil {} + Nil {} => { + Nil {} } - Seq_Cons {head : h, tail : zs} => { + Cons {Head : h, tail : zs} => { snoc (rev(zs), h) } } @@ -189,32 +189,32 @@ Instead, we need to rearrange IntQueue and friends so that we take ownership of the very last cell in the list at the very beginning, instead of at the very end. - predicate (datatype seq) IntQueue(pointer q) { + predicate (datatype List) 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)) { + predicate (datatype List) IntQueue1(pointer dummy, struct int_queue H) { + if (is_null(H.Head)) { assert (is_null(H.tail)); - return (Seq_Nil{}); + return (Nil{}); } else { assert (!is_null(H.tail)); take T = Owned(H.tail); assert (is_null(T.next)); - take Q = IntQueueAux (H.head, H.tail, T.first); + take Q = IntQueueAux (H.Head, H.tail, T.first); return Q; } } - predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) { + predicate (datatype List) IntQueueAux (pointer h, pointer t, i32 lastVal) { if (h == t) { - return (Seq_Cons{head: lastVal, tail: Seq_Nil{}}); + return (Cons{Head: lastVal, Tail: Nil{}}); } else { take C = Owned(h); take TL = IntQueueAux(C.next, t, lastVal); - return (Seq_Cons { head: C.first, tail: TL }); + return (Cons { Head: C.first, Tail: TL }); } } diff --git a/src/tutorial.adoc b/src/tutorial.adoc index 7eaf229b..ce64e059 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -747,7 +747,7 @@ to define a CN "predicate" that describes *mathematical* list structures, as one would do in ML, Haskell, or Coq. (We call them "sequences" here to avoid overloading the word "list".) -Intuitively, the `+IntList+` predicate walks over a pointer structure +Intuitively, the `+SLList+` predicate walks over a pointer structure in the C heap and extracts an `+Owned+` version of the mathematical list that it represents. @@ -759,7 +759,7 @@ syntax): include_example(exercises/list_hdtl.h) -We use the `+IntList+` predicate to specify functions returning the +We use the `+SLList+` predicate to specify functions returning the empty list and the cons of a number and a list. include_example(exercises/list_constructors.h) @@ -961,7 +961,7 @@ element, which is the first in a linked list of `+int_queueCell+`s, the other pointing directly to the last cell in this list. If the queue is empty, both pointers are NULL. -Abstractly, a queue just represents a list, so we can reuse the `+seq+` +Abstractly, a queue just represents a list, so we can reuse the `+List+` type from the list examples earlier in the tutorial. include_example(exercises/queue_cn_types_1.h) @@ -1135,7 +1135,7 @@ cannot.) The guard/condition for `+IntQueueFB+` is `+is_null(front)+`, which is why we need to do a `+split_case+` on this value. On one branch of the `+split_case+`, we have a contradiction: the fact that `+before == -Seq_Nil{}+` (from `+IntQueueFB+`) conflicts with `+before != Seq_Nil+` +Nil{}+` (from `+IntQueueFB+`) conflicts with `+before != Nil+` from the precondition, so that case is immediate. On the other branch, CN now knows that the queue is non-empty as required and type checking proceeds. @@ -1228,7 +1228,7 @@ track of the front or back, but rather we take any node in the list and have a sequence to the left and to the right of that node. The `left` and `right` are from the point of view of the node itself, so `left` is kept in reverse order. Additionally, similarly to in the -`Imperative Queues` example, we can reuse the `+seq+` type. +`Imperative Queues` example, we can reuse the `+List+` type. include_example(exercises/Dbl_Linked_List/cn_types.h) @@ -1301,8 +1301,8 @@ include_example(exercises/Dbl_Linked_List/add.c) First, let's look at the pre and post conditions. The `requires` clause is straightforward. We need to own the list centered around the node that `n` points to. `Before` is a `Dll` -that is either empty, or it has a seq to the left, -the current node that `n` points to, and a seq to the right. +that is either empty, or it has a List to the left, +the current node that `n` points to, and a List to the right. This corresponds to the state of the list when it is passed in. In the ensures clause, we again establish ownership of the list, but this time it is centered around the added node. This means that `After` is a `Dll` structure similar to `Before`, except that the node `curr` is @@ -1447,15 +1447,15 @@ Misc things to do: - naming issues - rename == to ptr_eq everywhere in specs - - rename list to seq in filenames. or go more radical and rename seq to cnlist - - consider renaming IntList to just List (and int_list to just list, + - rename list to List in filenames. or go more radical and rename List to cnlist + - consider renaming SLList to just List (and int_list to just list, etc.) everywhere (since we are only dealing with one kind of list in the tutorial, the extra pedantry is not getting us much; and this simplification would avoid trying to fix conventions that all CN code should use everywhere...) - - related: the name Seq_Cons is awkward for several reasons: + - related: the name Cons is awkward for several reasons: - long / verbose (nothing to do about that, I guess) - - Seq is capitalized, but it means seq + - Seq is capitalized, but it means List - most important part is buried in the middle - What are the established C conventions here?? From 3f803d4f880b27a745cfe47a7aafa73e9d14d4e6 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Tue, 13 Aug 2024 22:39:48 -0400 Subject: [PATCH 16/25] Makefile nit --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 6732dd46..46ec8f7a 100644 --- a/Makefile +++ b/Makefile @@ -3,6 +3,7 @@ MAKEFILE_DIR:=$(dir $(realpath $(lastword $(MAKEFILE_LIST)))) default: build exercises build/tutorial.html build/exercises.zip +all: default clean: rm -rf build TAGS From a76ec94d07c116586d95c789aa44966d05daf818 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Wed, 14 Aug 2024 10:07:38 -0400 Subject: [PATCH 17/25] 'nother round of renaming --- NAMING-CONVENTIONS.md | 10 ++++----- src/examples/Dbl_Linked_List/remove.c | 4 ++-- src/examples/append.c | 10 ++++----- src/examples/append2.c | 20 ++++++++--------- src/examples/list_append.h | 4 ++-- src/examples/list_rev.c | 4 ++-- src/examples/list_rev_alt.c | 4 ++-- src/examples/list_rev_lemmas.h | 6 ++--- src/examples/liste_rev_lemmas.h | 10 ++++----- src/examples/mergesort.c | 32 +++++++++++++-------------- src/examples/queue_pop.c | 6 ++--- src/examples/queue_pop_lemma.h | 6 ++--- src/examples/queue_pop_lemma_stages.c | 32 +++++++++++++-------------- src/examples/queue_push.c | 2 +- src/examples/queue_push_induction.c | 8 +++---- src/examples/queue_push_lemma.h | 2 +- src/examples/slf_length_acc.c | 6 ++--- src/examples/slf_sized_stack.c | 22 +++++++++--------- src/queue-example-notes.md | 2 +- src/tutorial.adoc | 4 ++-- 20 files changed, 97 insertions(+), 97 deletions(-) diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md index 49bc3aae..01a64f69 100644 --- a/NAMING-CONVENTIONS.md +++ b/NAMING-CONVENTIONS.md @@ -128,12 +128,12 @@ the first case. non-recursive part of the structure). - The current function `IntList_free__list` is hard to rename with - these conventions. It feels like it should be `free__int_list`, but + these conventions. It feels like it should be `free__sllist`, but that’s also the new name of the free function for individual list cells (opposite of `malloc`). Current solution is - `free_rec__int_list`. + `free_rec__sllist`. - BCP wonders if this issue is specific to malloc and free. If so, maybe we can make some special convention like - `free__int_list_node` for the single-node operation (even though - what it returns is an `int_list`, noit an `int_list_node`), - leaving `free__int_list` for the recursive one? + `free__sllist_node` for the single-node operation (even though + what it returns is an `sllist`, noit an `sllist_node`), + leaving `free__sllist` for the recursive one? diff --git a/src/examples/Dbl_Linked_List/remove.c b/src/examples/Dbl_Linked_List/remove.c index 2d828214..18a8c361 100644 --- a/src/examples/Dbl_Linked_List/remove.c +++ b/src/examples/Dbl_Linked_List/remove.c @@ -11,8 +11,8 @@ struct node_and_int *remove(struct node *n) take After = Dll_at(ret.node); ret.data == del.data; (is_null(del.prev) && is_null(del.next)) ? After == Empty_Dll{} - : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: tl(Right(Before))} - : After == Dll{left: tl(Left(Before)), curr: Node(After), right: Right(Before)}); + : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: Tl(Right(Before))} + : After == Dll{left: Tl(Left(Before)), curr: Node(After), right: Right(Before)}); @*/ { struct node *temp = 0; diff --git a/src/examples/append.c b/src/examples/append.c index d4214f4d..0fdb917d 100644 --- a/src/examples/append.c +++ b/src/examples/append.c @@ -1,18 +1,18 @@ #include "list.h" #include "list_append.h" -struct int_list* IntList_append(struct int_list* xs, struct int_list* ys) +struct sllist* IntList_append(struct sllist* xs, struct sllist* ys) /*@ requires take L1 = SLList(xs); @*/ /*@ requires take L2 = SLList(ys); @*/ /*@ ensures take L3 = SLList(return); @*/ -/*@ ensures L3 == append(L1, L2); @*/ +/*@ ensures L3 == Append(L1, L2); @*/ { if (xs == 0) { - /*@ unfold append(L1, L2); @*/ + /*@ unfold Append(L1, L2); @*/ return ys; } else { - /*@ unfold append(L1, L2); @*/ - struct int_list *new_tail = IntList_append(xs->tail, ys); + /*@ unfold Append(L1, L2); @*/ + struct sllist *new_tail = IntList_append(xs->tail, ys); xs->tail = new_tail; return xs; } diff --git a/src/examples/append2.c b/src/examples/append2.c index c91cdf78..a2fd2a48 100644 --- a/src/examples/append2.c +++ b/src/examples/append2.c @@ -1,7 +1,7 @@ #include "list.h" #include "list_append.h" -struct int_list* IntList_copy (struct int_list *xs) +struct sllist* IntList_copy (struct sllist *xs) /*@ requires take L1 = SLList(xs); ensures take L1_ = SLList(xs); take L2 = SLList(return); @@ -10,35 +10,35 @@ struct int_list* IntList_copy (struct int_list *xs) @*/ { if (xs == 0) { - return IntList_nil(); + return slnil(); } else { - struct int_list *new_tail = IntList_copy(xs->tail); - return IntList_cons(xs->head, new_tail); + struct sllist *new_tail = IntList_copy(xs->tail); + return slcons(xs->head, new_tail); } } -struct int_list* IntList_append2 (struct int_list *xs, struct int_list *ys) +struct sllist* IntList_append2 (struct sllist *xs, struct sllist *ys) /* --BEGIN-- */ /*@ requires take L1 = SLList(xs); @*/ /*@ requires take L2 = SLList(ys); @*/ /*@ ensures take L1_ = SLList(xs); @*/ /*@ ensures take L2_ = SLList(ys); @*/ /*@ ensures take L3 = SLList(return); @*/ -/*@ ensures L3 == append(L1, L2); @*/ +/*@ ensures L3 == Append(L1, L2); @*/ /*@ ensures L1 == L1_; @*/ /*@ ensures L2 == L2_; @*/ /* --END-- */ { if (xs == 0) { /* --BEGIN-- */ - /*@ unfold append(L1, L2); @*/ + /*@ unfold Append(L1, L2); @*/ /* --END-- */ return IntList_copy(ys); } else { /* --BEGIN-- */ - /*@ unfold append(L1, L2); @*/ + /*@ unfold Append(L1, L2); @*/ /* --END-- */ - struct int_list *new_tail = IntList_append2(xs->tail, ys); - return IntList_cons(xs->head, new_tail); + struct sllist *new_tail = IntList_append2(xs->tail, ys); + return slcons(xs->head, new_tail); } } diff --git a/src/examples/list_append.h b/src/examples/list_append.h index 0a54754c..38cc8a48 100644 --- a/src/examples/list_append.h +++ b/src/examples/list_append.h @@ -1,13 +1,13 @@ // append.h /*@ -function [rec] (datatype List) AppendList(datatype List L1, datatype List L2) { +function [rec] (datatype List) Append(datatype List L1, datatype List L2) { match L1 { Nil {} => { L2 } Cons {Head : H, Tail : T} => { - Cons {Head: H, Tail: AppendList(T, L2)} + Cons {Head: H, Tail: Append(T, L2)} } } } diff --git a/src/examples/list_rev.c b/src/examples/list_rev.c index ff16ce6c..584e5988 100644 --- a/src/examples/list_rev.c +++ b/src/examples/list_rev.c @@ -7,11 +7,11 @@ struct sllist* rev_aux(struct sllist* l1, struct sllist* l2) /*@ requires take L1 = SLList(l1); @*/ /*@ requires take L2 = SLList(l2); @*/ /*@ ensures take R = SLList(return); @*/ -/*@ ensures R == AppendList(RevList(L2), L1); @*/ +/*@ ensures R == Append(RevList(L2), L1); @*/ { if (l2 == 0) { /*@ unfold RevList(L2); @*/ - /*@ unfold AppendList(Nil{}, L1); @*/ + /*@ unfold Append(Nil{}, L1); @*/ return l1; } else { /*@ unfold RevList(L2); @*/ diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c index 7178450b..6e0c1fd3 100644 --- a/src/examples/list_rev_alt.c +++ b/src/examples/list_rev_alt.c @@ -15,12 +15,12 @@ struct sllist* rev_loop(struct sllist *l) while(1) /*@ inv take Last = SLList(last); take Cur = SLList(cur); - AppendList(RevList(Cur), Last) == RevList(L); + Append(RevList(Cur), Last) == RevList(L); @*/ { if (cur == 0) { /*@ unfold RevList(Nil{}); @*/ - /*@ unfold AppendList(Nil{}, Last); @*/ + /*@ unfold Append(Nil{}, Last); @*/ return last; } struct sllist *tmp = cur->tail; diff --git a/src/examples/list_rev_lemmas.h b/src/examples/list_rev_lemmas.h index f2cba579..8e6dd044 100644 --- a/src/examples/list_rev_lemmas.h +++ b/src/examples/list_rev_lemmas.h @@ -1,10 +1,10 @@ /*@ lemma Append_Nil_RList (datatype List L1) requires true; - ensures AppendList(L1, Nil{}) == L1; + ensures Append(L1, Nil{}) == L1; lemma Append_Cons_RList (datatype List L1, i32 X, datatype List L2) requires true; - ensures AppendList(L1, Cons {Head: X, Tail: L2}) - == AppendList(Snoc(L1, X), L2); + ensures Append(L1, Cons {Head: X, Tail: L2}) + == Append(Snoc(L1, X), L2); @*/ diff --git a/src/examples/liste_rev_lemmas.h b/src/examples/liste_rev_lemmas.h index d5c8976d..8bc6f870 100644 --- a/src/examples/liste_rev_lemmas.h +++ b/src/examples/liste_rev_lemmas.h @@ -1,10 +1,10 @@ /*@ -lemma append_nil_r (datatype List l1) +lemma Append_nil_r (datatype List l1) requires true - ensures append(l1, Nil {}) == l1 + ensures Append(l1, Nil {}) == l1 -lemma append_cons_r (datatype List l1, i32 x, datatype List l2) +lemma Append_cons_r (datatype List l1, i32 x, datatype List l2) requires true - ensures append(l1, Cons {Head: x, Tail: l2}) - == append(snoc(l1, x), l2) + ensures Append(l1, Cons {Head: x, Tail: l2}) + == Append(snoc(l1, x), l2) @*/ diff --git a/src/examples/mergesort.c b/src/examples/mergesort.c index 5a837d8a..c2508535 100644 --- a/src/examples/mergesort.c +++ b/src/examples/mergesort.c @@ -10,7 +10,7 @@ function [rec] ({datatype List fst, datatype List snd}) split(datatype List xs) Cons {Head: h1, Tail: Nil{}} => { {fst: Nil{}, snd: xs} } - Cons {Head: h1, Tail: Cons {Head : h2, tail : tl2 }} => { + Cons {Head: h1, Tail: Cons {Head : h2, Tail : tl2 }} => { let P = split(tl2); {fst: Cons { Head: h1, Tail: P.fst}, snd: Cons { Head: h2, Tail: P.snd}} @@ -48,12 +48,12 @@ function [rec] (datatype List) mergesort(datatype List xs) { } @*/ -struct int_list_pair { - struct int_list* fst; - struct int_list* snd; +struct sllist_pair { + struct sllist* fst; + struct sllist* snd; }; -struct int_list_pair split(struct int_list *xs) +struct sllist_pair split(struct sllist *xs) /*@ requires take Xs = SLList(xs); @*/ /*@ ensures take Ys = SLList(return.fst); @*/ /*@ ensures take Zs = SLList(return.snd); @*/ @@ -61,26 +61,26 @@ struct int_list_pair split(struct int_list *xs) { if (xs == 0) { /*@ unfold split(Xs); @*/ - struct int_list_pair r = {.fst = 0, .snd = 0}; + struct sllist_pair r = {.fst = 0, .snd = 0}; return r; } else { - struct int_list *cdr = xs -> tail; + struct sllist *cdr = xs -> tail; if (cdr == 0) { /*@ unfold split(Xs); @*/ - struct int_list_pair r = {.fst = 0, .snd = xs}; + struct sllist_pair r = {.fst = 0, .snd = xs}; return r; } else { /*@ unfold split(Xs); @*/ - struct int_list_pair p = split(cdr->tail); + struct sllist_pair p = split(cdr->tail); xs->tail = p.fst; cdr->tail = p.snd; - struct int_list_pair r = {.fst = xs, .snd = cdr}; + struct sllist_pair r = {.fst = xs, .snd = cdr}; return r; } } } -struct int_list* merge(struct int_list *xs, struct int_list *ys) +struct sllist* merge(struct sllist *xs, struct sllist *ys) /*@ requires take Xs = SLList(xs); @*/ /*@ requires take Ys = SLList(ys); @*/ /*@ ensures take Zs = SLList(return); @*/ @@ -97,11 +97,11 @@ struct int_list* merge(struct int_list *xs, struct int_list *ys) } else { /*@ unfold merge(Xs, Ys); @*/ if (xs->head < ys->head) { - struct int_list *zs = merge(xs->tail, ys); + struct sllist *zs = merge(xs->tail, ys); xs->tail = zs; return xs; } else { - struct int_list *zs = merge(xs, ys->tail); + struct sllist *zs = merge(xs, ys->tail); ys->tail = zs; return ys; } @@ -109,7 +109,7 @@ struct int_list* merge(struct int_list *xs, struct int_list *ys) } } -struct int_list* mergesort(struct int_list *xs) +struct sllist* mergesort(struct sllist *xs) /*@ requires take Xs = SLList(xs); @*/ /*@ ensures take Ys = SLList(return); @*/ /*@ ensures Ys == mergesort(Xs); @*/ @@ -118,13 +118,13 @@ struct int_list* mergesort(struct int_list *xs) /*@ unfold mergesort(Xs); @*/ return xs; } else { - struct int_list *tail = xs->tail; + struct sllist *tail = xs->tail; if (tail == 0) { /*@ unfold mergesort(Xs); @*/ return xs; } else { /*@ unfold mergesort(Xs); @*/ - struct int_list_pair p = split(xs); + struct sllist_pair p = split(xs); p.fst = mergesort(p.fst); p.snd = mergesort(p.snd); return merge(p.fst, p.snd); diff --git a/src/examples/queue_pop.c b/src/examples/queue_pop.c index 317c0a92..57798da2 100644 --- a/src/examples/queue_pop.c +++ b/src/examples/queue_pop.c @@ -5,8 +5,8 @@ int IntQueue_pop (struct int_queue *q) /*@ requires take before = IntQueuePtr(q); before != Nil{}; ensures take after = IntQueuePtr(q); - after == tl(before); - return == hd(before); + after == Tl(before); + return == Hd(before); @*/ { /*@ split_case is_null(q->front); @*/ @@ -16,7 +16,7 @@ int IntQueue_pop (struct int_queue *q) freeIntQueueCell(h); q->front = 0; q->back = 0; - /*@ unfold snoc(Nil{}, x); @*/ + /*@ unfold Snoc(Nil{}, x); @*/ return x; } else { int x = h->first; diff --git a/src/examples/queue_pop_lemma.h b/src/examples/queue_pop_lemma.h index cf0175fc..f2f46f40 100644 --- a/src/examples/queue_pop_lemma.h +++ b/src/examples/queue_pop_lemma.h @@ -7,7 +7,7 @@ lemma snoc_facts (pointer front, pointer back, i32 x) take NewQ = IntQueueAux(front, back); take NewB = Owned(back); Q == NewQ; B == NewB; - let L = snoc (Cons{Head: x, Tail: Q}, B.first); - hd(L) == x; - tl(L) == snoc (Q, B.first); + let L = Snoc (Cons{Head: x, Tail: Q}, B.first); + Hd(L) == x; + Tl(L) == Snoc (Q, B.first); @*/ diff --git a/src/examples/queue_pop_lemma_stages.c b/src/examples/queue_pop_lemma_stages.c index 157b4053..7ef87259 100644 --- a/src/examples/queue_pop_lemma_stages.c +++ b/src/examples/queue_pop_lemma_stages.c @@ -8,14 +8,14 @@ predicate (datatype List) Pre(pointer front, pointer back, i32 popped, datatype List before) { if (is_null(front)) { let after = Nil{}; - assert (before == snoc(Nil{}, popped)); + assert (before == Snoc(Nil{}, popped)); return after; } else { take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - assert (before == snoc(Cons {Head: popped, Tail: L}, B.first)); - let after = snoc(L, B.first); + assert (before == Snoc(Cons {Head: popped, Tail: L}, B.first)); + let after = Snoc(L, B.first); return after; } } @@ -34,19 +34,19 @@ ensures predicate (datatype List) Post(pointer front, pointer back, i32 popped, datatype List before) { if (is_null(front)) { - assert (before == snoc(Nil{}, popped)); + assert (before == Snoc(Nil{}, popped)); let after = Nil{}; - assert (after == tl(before)); - assert (popped == hd(before)); + assert (after == Tl(before)); + assert (popped == Hd(before)); return after; } else { take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - assert (before == snoc(Cons {Head: popped, Tail: L}, B.first)); - let after = snoc(L, B.first); - assert (after == tl(before)); - assert (popped == hd(before)); + assert (before == Snoc(Cons {Head: popped, Tail: L}, B.first)); + let after = Snoc(L, B.first); + assert (after == Tl(before)); + assert (popped == Hd(before)); return after; } } @@ -69,12 +69,12 @@ type_synonym result = { datatype List after, datatype List before } predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) { if (is_null(front)) { - return { after: Nil{}, before: snoc(Nil{}, popped) }; + return { after: Nil{}, before: Snoc(Nil{}, popped) }; } else { take B = Owned(back); assert (is_null(B.next)); take L = IntQueueAux (front, back); - return { after: snoc(L, B.first), before: snoc(Cons {Head: popped, Tail: L}, B.first) }; + return { after: Snoc(L, B.first), before: Snoc(Cons {Head: popped, Tail: L}, B.first) }; } } @@ -85,8 +85,8 @@ requires ensures take NewQ = Queue_pop_lemma(front, back, popped); Q == NewQ; - Q.after == tl(Q.before); - popped == hd(Q.before); + Q.after == Tl(Q.before); + popped == Hd(Q.before); @*/ // Step 4 (optional): Remove the sanity checking from the pre-condition. @@ -99,7 +99,7 @@ requires ensures take NewQ = Queue_pop_lemma(front, back, popped); Q == NewQ; - Q.after == tl(Q.before); - popped == hd(Q.before); + Q.after == Tl(Q.before); + popped == Hd(Q.before); @*/ diff --git a/src/examples/queue_push.c b/src/examples/queue_push.c index e22dd152..121e3cf8 100644 --- a/src/examples/queue_push.c +++ b/src/examples/queue_push.c @@ -4,7 +4,7 @@ void IntQueue_push (int x, struct int_queue *q) /*@ requires take before = IntQueuePtr(q); ensures take after = IntQueuePtr(q); - after == snoc (before, x); + after == Snoc (before, x); @*/ { struct int_queueCell *c = mallocIntQueueCell(); diff --git a/src/examples/queue_push_induction.c b/src/examples/queue_push_induction.c index 9d0f897a..d607b896 100644 --- a/src/examples/queue_push_induction.c +++ b/src/examples/queue_push_induction.c @@ -12,16 +12,16 @@ void push_induction(struct int_queueCell* front ensures take NewQ = IntQueueAux(front, last); take Last2 = Owned(last); - NewQ == snoc(Q, Second_last.first); + NewQ == Snoc(Q, Second_last.first); Last == Last2; @*/ { if (front == second_last) { - /*@ unfold snoc(Q, Second_last.first); @*/ + /*@ unfold Snoc(Q, Second_last.first); @*/ return; } else { push_induction(front->next, second_last, last); - /*@ unfold snoc(Q, Second_last.first); @*/ + /*@ unfold Snoc(Q, Second_last.first); @*/ return; } } @@ -29,7 +29,7 @@ void push_induction(struct int_queueCell* front void IntQueue_push (int x, struct int_queue *q) /*@ requires take before = IntQueuePtr(q); ensures take after = IntQueuePtr(q); - after == snoc (before, x); + after == Snoc (before, x); @*/ { struct int_queueCell *c = mallocIntQueueCell(); diff --git a/src/examples/queue_push_lemma.h b/src/examples/queue_push_lemma.h index d3052dc2..2220caf1 100644 --- a/src/examples/queue_push_lemma.h +++ b/src/examples/queue_push_lemma.h @@ -5,5 +5,5 @@ lemma push_lemma (pointer front, pointer p) take P = Owned(p); ensures take NewQ = IntQueueAux(front, P.next); - NewQ == snoc(Q, P.first); + NewQ == Snoc(Q, P.first); @*/ diff --git a/src/examples/slf_length_acc.c b/src/examples/slf_length_acc.c index 0b491a88..70139691 100644 --- a/src/examples/slf_length_acc.c +++ b/src/examples/slf_length_acc.c @@ -8,14 +8,14 @@ function [rec] (u32) length(datatype List xs) { Nil {} => { 0u32 } - Cons {Head : h, tail : zs} => { + Cons {Head: h, Tail: zs} => { 1u32 + length(zs) } } } @*/ -void IntList_length_acc_aux (struct int_list *xs, unsigned int *p) +void IntList_length_acc_aux (struct sllist *xs, unsigned int *p) /*@ requires take L1 = SLList(xs); take n = Owned(p); ensures take L1_ = SLList(xs); @@ -32,7 +32,7 @@ void IntList_length_acc_aux (struct int_list *xs, unsigned int *p) } } -unsigned int IntList_length_acc (struct int_list *xs) +unsigned int IntList_length_acc (struct sllist *xs) /*@ requires take L1 = SLList(xs); ensures take L1_ = SLList(xs); L1 == L1_; diff --git a/src/examples/slf_sized_stack.c b/src/examples/slf_sized_stack.c index 351b5f2e..4ac9d769 100644 --- a/src/examples/slf_sized_stack.c +++ b/src/examples/slf_sized_stack.c @@ -3,7 +3,7 @@ struct sized_stack { unsigned int size; - struct int_list* data; + struct sllist* data; }; /*@ @@ -40,7 +40,7 @@ struct sized_stack* create() struct sized_stack *p = malloc__sized_stack(); p->size = 0; p->data = 0; - /*@ unfold length(Nil {}); @*/ + /*@ unfold Length(Nil {}); @*/ return p; } @@ -66,11 +66,11 @@ void push (struct sized_stack *p, int x) @*/ /* ---END--- */ { - struct int_list *data = slcons(x, p->data); + struct sllist *data = slcons(x, p->data); p->size++; p->data = data; /* ---BEGIN--- */ - /*@ unfold length (Cons {Head: x, Tail: S.d}); @*/ + /*@ unfold Length (Cons {Head: x, Tail: S.d}); @*/ /* ---END--- */ } @@ -80,19 +80,19 @@ int pop (struct sized_stack *p) /*@ requires take S = SizedStack(p); S.s > 0u32; ensures take S_ = SizedStack(p); - S_.d == tl(S.d); + S_.d == Tl(S.d); @*/ /* ---END--- */ { - struct int_list *data = p->data; + struct sllist *data = p->data; if (data != 0) { int head = data->head; - struct int_list *tail = data->tail; - freeIntList(data); + struct sllist *tail = data->tail; + free__sllist(data); p->data = tail; p->size--; /* ---BEGIN--- */ - /*@ unfold length(S.d); @*/ + /*@ unfold Length(S.d); @*/ /* ---END--- */ return head; } @@ -104,10 +104,10 @@ int top (struct sized_stack *p) S.s > 0u32; ensures take S_ = SizedStack(p); S_ == S; - return == hd(S.d); + return == Hd(S.d); @*/ { - /*@ unfold length(S.d); @*/ + /*@ unfold Length(S.d); @*/ // from S.s > 0u32 it follows that the 'else' branch is impossible if (p->data != 0) { return (p->data)->head; diff --git a/src/queue-example-notes.md b/src/queue-example-notes.md index 087648b3..f2d39a56 100644 --- a/src/queue-example-notes.md +++ b/src/queue-example-notes.md @@ -133,7 +133,7 @@ This tells us to look at snoc, which turns out to be very wrong! Nil {} => { Nil {} } - Cons {Head : h, tail : zs} => { + Cons {Head : h, Tail : zs} => { snoc (rev(zs), h) } } diff --git a/src/tutorial.adoc b/src/tutorial.adoc index ce64e059..9885a15b 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -1270,7 +1270,7 @@ include_example(exercises/Dbl_Linked_List/getters.h) We also must include some boilerplate code for allocation and deallocation. -include_example(exercises/Dbl_Linked_List/malloc__free.h) +include_example(exercises/Dbl_Linked_List/malloc_free.h) And we compile all of these files into a single header file. @@ -1448,7 +1448,7 @@ Misc things to do: - naming issues - rename == to ptr_eq everywhere in specs - rename list to List in filenames. or go more radical and rename List to cnlist - - consider renaming SLList to just List (and int_list to just list, + - consider renaming SLList to just List (and sllist to just list, etc.) everywhere (since we are only dealing with one kind of list in the tutorial, the extra pedantry is not getting us much; and this simplification would avoid trying to fix conventions that all From 9094b86f23f32084332816a3ce705d6372ed33d2 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 15 Aug 2024 21:45:10 -0400 Subject: [PATCH 18/25] WIP tutorial polishing --- src/tutorial.adoc | 92 ++++++++++++++++++++++++++++------------------- 1 file changed, 56 insertions(+), 36 deletions(-) diff --git a/src/tutorial.adoc b/src/tutorial.adoc index 90c66e90..2cb5f0fe 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -10,11 +10,13 @@ By Christopher Pulte and Benjamin C. Pierce, with contributions from Elizabeth A [abstract] -- -CN is a type system for verifying C code, focusing especially on low-level systems code. Compared to the normal C type system, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes _safely_ — does not raise C undefined behaviour — and _correctly_ — according to strong user-defined specifications. -// -This tutorial introduces CN along a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures. +CN is an extension of the C programming language for verifying the correctness of C code, especially on low-level systems code. Compared to standard C, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes _safely_ — does not raise C undefined behaviour — and _correctly_ — satisfying to strong, user-defined specifications. +This tutorial introduces CN through a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures. -CN was first described in https://dl.acm.org/doi/10.1145/3571194[CN: Verifying Systems C Code with Separation-Logic Refinement Types] by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami. +This tutorial is a work in progress -- your suggestions are greatly appreciated! + +**Origins.** +CN was first described in https://dl.acm.org/doi/10.1145/3571194[CN: Verifying Systems C Code with Separation-Logic Refinement Types] by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. // To accurately handle the complex semantics of C, CN builds on the https://github.com/rems-project/cerberus/[Cerberus semantics for C]. // @@ -23,8 +25,6 @@ https://softwarefoundations.cis.upenn.edu[Separation Logic Foundations] textbook, and one of the case studies is based on an extended exercise due to Bryan Parno. -This tutorial is a work in progress -- your suggestions are greatly appreciated! - **Acknowledgment of Support and Disclaimer.** This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google. The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL). @@ -32,46 +32,42 @@ This material is based upon work supported by the Air Force Research Laboratory == Installing CN -To fetch and install CN, check the Cerberus repository at https://github.com/rems-project/cerberus and follow the instructions in https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md[backend/cn/README.md]. +To fetch and install CN, visit the Cerberus repository at https://github.com/rems-project/cerberus and follow the instructions in https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md[backend/cn/README.md]. -Once completed, type `+cn --help+` in your terminal to ensure CN is installed and found by your system. This should print the list of available options CN can be executed with. +Once the installation is completed, type `+cn --help+` in your terminal to ensure CN is installed and found by your system. This should print the list of available options CN can be executed with. -To apply CN to a C file, run `+cn CFILE+`. +To apply CN to a C file, run `+cn verify CFILE+`. -== Source files for the exercises and examples +== Source files -The source files can be downloaded from link:exercises.zip[here]. +The source files for all the exercises and examples below can be downloaded +from link:exercises.zip[here]. -== Basic usage +== Basics === First example -For a first example, let’s look at a simple arithmetic function: `+add+`, shown below, takes two `+int+` arguments, `+x+` and `+y+`, and returns their sum. +The simple arithmetic function: `+add+` shown below takes two `+int+` arguments, `+x+` and `+y+`, and returns their sum. -// TODO: BCP: We should probably adopt the convention that all the files in -// the exercises directory have a comment at the top giving their name. -// (We could actually auto-generate those header comments when we process -// /src/examples into build/exercises, to avoid having to maintain them -// and possibly get them wrong...) include_example(exercises/add_0.c) Running CN on the example produces an error message: .... -cn exercises/add_0.c +cn verify exercises/add_0.c [1/1]: add exercises/add_0.c:3:10: error: Undefined behaviour return x+y; ~^~ an exceptional condition occurs during the evaluation of an expression (§6.5#5) -Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_393431.html +Consider the state in /var/folders/_v/ndl32rvc8ph0000gn/T/state_393431.html .... -CN rejects the program because it has _C undefined behaviour_, meaning it is not safe to execute. CN points to the relevant source location, the addition `+x+y+`, and paragraph §6.5#5 of the C language standard that specifies the undefined behaviour. It also puts a link to an HTML file with more details on the error to help in diagnosing the problem. +CN rejects the program because it has _undefined behaviour_ according to the C standard, meaning it is not safe to execute. CN points to the relevant source location, the addition `+x+y+`, and paragraph §6.5#5 of the standard, which specifies the undefined behaviour. It also includes a link to an HTML file with more details on the error to help in diagnosing the problem. Inspecting this HTML report (as we do in a moment) gives us possible example values for `+x+` and `+y+` that cause the undefined behaviour and hint at the problem: for very large values for `+x+` and `+y+`, such as `+1073741825+` and `+1073741824+`, the sum of `+x+` and `+y+` can exceed the representable range of a C `+int+` value: `+1073741825 + 1073741824 = 2^31+1+`, so their sum is larger than the maximal `+int+` value, `+2^31-1+`. -Here `+x+` and `+y+` are _signed integers_, and in C, signed integer _overflow_ is undefined behaviour (UB). Hence, `+add+` is only safe to execute for smaller values. Similarly, _large negative_ values of `+x+` and `+y+` can cause signed integer _underflow_, also UB in C. We therefore need to rule out too large values for `+x+` and `+y+`, both positive and negative, which we do by writing a CN function specification. +Here `+x+` and `+y+` are _signed integers_, and in C, signed integer _overflow_ is undefined behaviour (UB). Hence, `+add+` is only safe to execute for smaller values. Similarly, _large negative_ values of `+x+` and `+y+` can cause signed integer _underflow_, also UB in C. We therefore need to rule out too-large values for `+x+` and `+y+`, both positive and negative, which we do by writing a CN function specification. === First function specification @@ -91,20 +87,25 @@ In detail: * `+let sum = (i64) x + (i64) y+` is a let-binding, which defines `+sum+` as the value `+(i64) x + (i64) y+` in the remainder of the function specification. -* Instead of C syntax, CN uses Rust-like syntax for integer types, such as `+u32+` for 32-bit unsigned integers and `+i64+` for signed 64-bit integers to make their sizes unambiguous. Here, `+x+` and `+y+`, of C-type `+int+`, have CN type `+i32+`. +* Instead of C syntax, CN uses Rust-like syntax for integer types, such as `+u32+` for 32-bit unsigned integers and `+i64+` for signed 64-bit integers, to make their sizes unambiguous. Here, `+x+` and `+y+`, of C-type `+int+`, have CN type `+i32+`. // TODO: BCP: I understand this reasoning, but I wonder whether it introduces more confusion than it avoids -- it means there are two ways of writing everything, and people have to remember whether the particular thing they are writing right now is C or CN... +// TODO: BCP: Hopefully we are moving toward unifying these notations anyway? * To define `+sum+` we cast `+x+` and `+y+` to the larger `+i64+` type, using syntax `+(i64)+`, which is large enough to hold the sum of any two `+i32+` values. -* Finally, we require this sum to be in-between the minimal and maximal `+int+` value. Integer constants, such as `+-2147483648i64+`, must specifiy their CN type (`+i64+`). +* Finally, we require this sum to be between the minimal and maximal `+int+` values. Integer constants, such as `+-2147483648i64+`, must specifiy their CN type (`+i64+`). +// TODO: BCP: We should use the new ' syntax (or whatever it turned out to be) for numeric constants -Running CN on the annotated program passes without errors. This means with our specified precondition, `+add+` is safe to execute. +Running CN on the annotated program passes without errors. This means that, with our specified precondition, `+add+` is safe to execute. -We may, however, wish to be more precise. So far the specification gives no information to callers of `+add+` about its output. To also specify the return values we add a postcondition, using the `+ensures+` keyword. +We may, however, wish to be more precise. So far, the specification gives no information to callers of `+add+` about its output. To describe its return value we add a postcondition to the specification using the `+ensures+` keyword. include_example(solutions/add_1.c) -Here we use the keyword `+return+`, only available in function postconditions, to refer to the return value, and equate it to `+sum+` as defined in the preconditions, cast back to `+i32+` type: `+add+` returns the sum of `+x+` and `+y+`. +Here we use the keyword `+return+`, which is only available in function +postconditions, to refer to the return value, and we equate it to `+sum+` +as defined in the precondition, cast back to `+i32+` type: that is, `+add+` +returns the sum of `+x+` and `+y+`. Running CN confirms that this postcondition also holds. @@ -112,24 +113,42 @@ One final refinement of this example. CN defines constant functions `MINi32`, ` include_example(solutions/add_2.c) -Two things to note: - * These are constant _functions_, so they require a following `()`. - * The type of `MINi32()` is `i32`, so if we want to use it as a 64-bit constant - we need to add the explicit coercion `(i64)`. +Two things to note: (1) These are constant _functions_, so they +require a following `()`. And (2) The type of `MINi32()` is `i32`, so +if we want to use it as a 64-bit constant we need to add the explicit +coercion `(i64)`. === Error reports -In the original example CN reported a type error due to C undefined behaviour. While that example was perhaps simple enough to guess the problem and solution, this can become quite challenging as program and specification complexity increases. Diagnosing type errors is therefore an important part of using CN. CN tries to help with that by producing detailed error information, in the form of an HTML error report. +In the original example, CN reported a type error due to C undefined +behaviour. While that example was perhaps simple enough to guess the +problem and solution, this can become quite challenging as program and +specification complexity increases. Diagnosing errors is +therefore an important part of using CN. CN tries to help with this by +producing detailed error information, in the form of an HTML error +report. -Let’s return to the type error from earlier (`+add+` without precondition) and take a closer look at this report. The report comprises two sections. +Let’s return to the type error from earlier -- `+add+` without +precondition -- and take a closer look at this report. It +comprises two sections: -// TODO: BCP: It looks different now! +// TODO: BCP: It looks quite different now! .*CN error report* image::images/0.error.png[*CN error report*] -*Path.* The first section, "`Path to error`", contains information about the control-flow path leading to the error. +*Path to error.* The first section contains information about the +control-flow path leading to the error. -When type checking a C function, CN checks each possible control-flow path through the program individually. If CN detects UB or a violation of user-defined specifications, CN reports the problematic control-flow path, as a nested structure of statements: paths are split into sections, which group together statements between high-level control-flow positions (e.g. function entry, the start of a loop, the invocation of a `+continue+`, `+break+`, or `+return+` statement, etc.); within each section, statements are listed by source code location; finally, per statement, CN lists the typechecked sub-expressions, and the memory accesses and function calls within these. +When checking a C function, CN examines each possible control-flow +path individually. If it detects UB or a violation of user-defined +specifications, CN reports the problematic control-flow path as a +nested structure of statements: the path is split into sections that +group together statements between high-level control-flow positions +(e.g. function entry, the start of a loop, the invocation of a +`+continue+`, `+break+`, or `+return+` statement, etc.); within each +section, statements are listed by source code location; finally, per +statement, CN lists the typechecked sub-expressions, and the memory +accesses and function calls within these. In our example, there is only one possible control-flow path: entering the function body (section "`function body`") and executing the block from lines 2 to 4, followed by the return statement at line 3. The entry for the latter contains the sequence of sub-expressions in the return statement, including reads of the variables `+x+` and `+y+`. @@ -354,6 +373,7 @@ include_example(exercises/add_read.c) This time we use C’s `+unsigned int+` type. In C, over- and underflow of unsigned integers is not undefined behaviour, so we do not need any special preconditions to rule this out. Instead, when an arithmetic operation at unsigned type goes outside the representable range, the value "`wraps around`". The CN variables `+m+` and `+n+` (resp. `+m2+` and `+n2+`) for the pointee values of `+p+` and `+q+` before (resp. after) the execution of `+add+` have CN basetype `+u32+`, so unsigned 32-bit integers, matching the C `+unsigned int+` type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type. +// TODO: BCP: I propose that we uniformly use i32 integers everywhere in the tutorial (just mentioning in the bullet list below that there are other integer types, and using i64 for calculations that may overflow). Forgetting which integer type I was using was a common (and silly) failure mode when I was first working through the tutorial. Hence, the postcondition `+return == m+n+` holds also when the sum of `+m+` and `+n+` is greater than the maximal `+unsigned int+` value. From a048a724aa833c98ec7eb1477ebff0df78a6cf20 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 15 Aug 2024 22:02:08 -0400 Subject: [PATCH 19/25] More WIP on tutorial --- src/examples/abs.c | 3 +-- src/tutorial.adoc | 43 ++++++++++++++++++++++++++++++++++++------- 2 files changed, 37 insertions(+), 9 deletions(-) diff --git a/src/examples/abs.c b/src/examples/abs.c index 206ee580..79da4d60 100644 --- a/src/examples/abs.c +++ b/src/examples/abs.c @@ -7,8 +7,7 @@ int abs (int x) { if (x >= 0) { return x; - } - else { + } else { return -x; } } diff --git a/src/tutorial.adoc b/src/tutorial.adoc index 2cb5f0fe..86f2fea5 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -152,30 +152,57 @@ accesses and function calls within these. In our example, there is only one possible control-flow path: entering the function body (section "`function body`") and executing the block from lines 2 to 4, followed by the return statement at line 3. The entry for the latter contains the sequence of sub-expressions in the return statement, including reads of the variables `+x+` and `+y+`. -In C, local variables in a function, including its arguments, are mutable and their address can be taken and passed as a value. CN therefore represents local variables as memory allocations that are manipulated using memory reads and writes. Here, type checking the return statement includes checking memory reads for `+x+` and `+y+`, at their locations `+&ARG0+` and `+&ARG1+`. The path report lists these reads and their return values: the read at `+&ARG0+` returns `+x+` (that is, the value of `+x+` originally passed to `+add+`); the read at `+&ARG1+` returns `+y+`. Alongside this symbolic information, CN displays concrete values: +In C, local variables in a function, including its arguments, are +mutable, their addresses can be taken and passed as values. CN +therefore represents local variables as memory allocations that are +manipulated using memory reads and writes. Here, type checking the +return statement includes checking memory reads for `+x+` and `+y+`, +at their locations `+&ARG0+` and `+&ARG1+`. The path report lists +these reads and their return values: the read at `+&ARG0+` returns +`+x+` (that is, the value of `+x+` originally passed to `+add+`); the +read at `+&ARG1+` returns `+y+`. Alongside this symbolic information, +CN displays concrete values: +// TODO: BCP: WHere do we see that ARG0 and ARG1 have something to do with x and y? * `+1073741825i32 /* 0x40000001 */+` for x (the first value is the decimal representation, the second, in `+/*...*/+` comments, the hex equivalent) and * `+1073741824i32 /* 0x40000000 */+` for `+y+`. For now, ignore the pointer values `+{@0; 4}+` for `+x+` and `+{@0; 0}+` for `+y+`. +// TODO: BCP: Where are these things discussed? Anywhere? (When) are they useful? -These concrete values are part of a _counterexample_: a concrete valuation of variables and pointers in the program that that leads to the error. (The exact values may vary on your machine, depending on the version of Z3 installed on your system.) +These concrete values are part of a _counterexample_: a concrete +valuation of variables and pointers in the program that that leads to +the error. (The exact values may vary on your machine, depending on +the SMT solver -- i.e., the particular version of Z3, CVC5, or +whatever installed on your system.) *Proof context.* The second section, below the error trace, lists the proof context CN has reached along this control-flow path. "`Available resources`" lists the owned resources, as discussed in later sections. "`Variables`" lists counterexample values for program variables and pointers. In addition to `+x+` and `+y+`, assigned the same values as above, this includes values for their memory locations `+&ARG0+` and `+&ARG1+`, function pointers in scope, and the `+__cn_alloc_history+`, all of which we ignore for now. +// TODO: BCP: Again, where are these things discussed? Should they be? -Finally, "`Constraints`" records all logical facts CN has learned along the path. This includes user-specified assumptions from preconditions or loop invariants, value ranges inferred from the C-types of variables, and facts learned during the type checking of the statements. Here (`+add+` without precondition) the only constraints are some contraints inferred from C-types in the code. +Finally, "`Constraints`" records all logical facts CN has learned along the path. This includes user-specified assumptions from preconditions or loop invariants, value ranges inferred from the C-types of variables, and facts learned during the type checking of the statements. Here -- when checking `+add+` without precondition -- the only constraints are those inferred from C-types in the code: -* For instance, `+good(x)+` says that the initial value of `+x+` is a "`good`" `+signed int+` value (i.e. in range). Here `+signed int+` is the same type as `+int+`, CN just makes the sign explicit. For integer types `+T+`, `+good+` requires the value to be in range of type `+T+`; for pointer types `+T+` it also requires the pointer to be aligned. For structs and arrays this extends in the obvious way to struct members or array cells. +* For instance, `+good(x)+` says that the initial value of +`+x+` is a "`good`" `+signed int+` value (i.e. in range). Here +`+signed int+` is the same type as `+int+`, CN just makes the sign +explicit. +// TODO: BCP: Yikes! This seems potentially cxonfusing +For an integer type `+T+`, the type `+good+` requires the value to +be in range of type `+T+`; for pointer types `+T+`, it also requires +the pointer to be aligned. For structs and arrays, this extends in the +obvious way to struct members or array cells. +// TODO: BCP: Is this information actually ever usefulful? Is it currently suppressed? * `+repr+` requires representability (not alignment) at type `+T+`, so `+repr(&ARGO)+`, for instance, records that the pointer to `+x+` is representable at C-type `+signed int*+`; * `+aligned(&ARGO, 4u64)+`, moreover, states that it is 4-byte aligned. +// TODO: BCP: Some of the above (especially the bit at the end) feels like TMI for many/most users, especially at this point in the tutorial. + === Another arithmetic example Let’s apply what we know so far to another simple arithmetic example. @@ -187,15 +214,17 @@ include_example(exercises/slf1_basic_example_let.signed.c) We would like to verify this is safe, and that `+doubled+` returns twice the value of `+n+`. Running CN on `+doubled+` leads to a type error: the increment of `+a+` has undefined behaviour. -As in the first example, we need to ensure that `+n+1+` does not overflow and `+n-1+` does not underflow. Similarly also `+a+b+` has to be representable at `+int+` type. +As in the first example, we need to ensure that `+n+1+` does not overflow and `+n-1+` does not underflow. Similarly `+a+b+` has to be representable at `+int+` type. include_example(solutions/slf1_basic_example_let.signed.c) +// TODO: BCP: WHy n_+n_ in some places and n*2i32 in others? -We can specify these using a similar style of precondition as in the first example. We first define `+n_+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+` and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+n_+` does not go below the minimal `+int+` value, that incrementing `+n_+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution. +We encode these expectations using a similar style of precondition as in the first example. We first define `+n_+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+`, and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+n_+` does not go below the minimal `+int+` value, that incrementing `+n_+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution. +// TODO: BCP: How about renaming n_ to n64? To capture the functional behaviour, the postcondition specifies that `+return+` is twice the value of `+n+`. -=== Exercise +=== Exercises *Quadruple.* Specify the precondition needed to ensure safety of the C function `+quadruple+`, and a postcondition that describes its return value. From 390750219fc8cb4b023deee591fbe96b5b4c3406 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Fri, 16 Aug 2024 07:31:14 -0400 Subject: [PATCH 20/25] More tutorial WIP --- src/tutorial.adoc | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/tutorial.adoc b/src/tutorial.adoc index 86f2fea5..4e966671 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -238,6 +238,8 @@ include_example(exercises/abs.c) So far we’ve only considered example functions manipulating integer values. Verification becomes more interesting and challenging when _pointers_ are involved, because the safety of memory accesses via pointers has to be verified. +// TODO: BCP: As a non-expert coming to CN, I was (and to some extent still am) consistently confused by the terminology of "resource TYPES" -- they do not look like types, and I just think of them as resources. I think we could save other readers some confusion by reserving the word "type" for C-types and juset talking about "resources" for CN-level things. + CN uses _separation logic resource types_ and the concept of _ownership_ to reason about memory accesses. A resource is the permission to access a region of memory. Unlike logical constraints, resource ownership is _unique_, meaning resources cannot be duplicated. Let’s look at a simple example. The function `+read+` takes an `+int+` pointer `+p+` and returns the pointee value. @@ -247,7 +249,7 @@ include_example(exercises/read.c) Running CN on this example produces the following error: .... -cn exercises/read.c +cn verify exercises/read.c [1/1]: read exercises/read.c:3:10: error: Missing resource for reading return *p; @@ -260,13 +262,15 @@ For the read `+*p+` to be safe, ownership of a resource is missing: a resource ` === The Owned resource type +// TODO: BCP: Perhaps this is a good time for one last discussion of the keyword "Owned", which I have never found very helpful: the resource itself isn't owned -- it's a description of something that *can* be owned. (It's "take" that does the owning.) Moreover, "Owned" and "Block" are badly non-parallel, both grammatically and semantically. + Given a C-type `+T+` and pointer `+p+`, the resource `+Owned(p)+` asserts ownership of a memory cell at location `+p+` of the size of C-type `+T+`. It is CN’s equivalent of a points-to assertion in separation logic (indexed by C-types `+T+`). -In this example we can ensure the safe execution of `+read+` by adding a precondition that requires ownership of `+Owned(p)+`, as shown below. For now ignore the notation `+take ... = Owned(p)+`. Since `+read+` maintains this ownership, we also add a corresponding postcondition, whereby `+read+` returns ownership of `+p+` after it is finished executing, in the form of another `+Owned(p)+` resource. +In this example we can ensure the safe execution of `+read+` by adding a precondition that requires ownership of `+Owned(p)+`, as shown below. For now ignore the notation `+take ... = Owned(p)+`. Since reading the pointer does not disturb its value, we also add a corresponding postcondition, whereby `+read+` returns ownership of `+p+` after it is finished executing, in the form of another `+Owned(p)+` resource. include_example(solutions/read.c) -This specifications means that +This specification means that: * any function calling `+read+` has to be able to provide a resource `+Owned(p)+` to pass into `+read+`, and From b0e83438350d3c6f27faf6713e788de2359d5028 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Fri, 16 Aug 2024 08:59:58 -0400 Subject: [PATCH 21/25] WIP on tutorial --- src/examples/read2.c | 2 -- src/tutorial.adoc | 31 +++++++++++++++++++------------ 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/examples/read2.c b/src/examples/read2.c index d7fb90a7..4528c534 100644 --- a/src/examples/read2.c +++ b/src/examples/read2.c @@ -1,11 +1,9 @@ int read (int *p) -/* --BEGIN-- */ /*@ requires take v1 = Owned(p); ensures take v2 = Owned(p); return == v1; v1 == v2; @*/ -/* --END-- */ { return *p; } diff --git a/src/tutorial.adoc b/src/tutorial.adoc index 4e966671..e6a44057 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -262,7 +262,7 @@ For the read `+*p+` to be safe, ownership of a resource is missing: a resource ` === The Owned resource type -// TODO: BCP: Perhaps this is a good time for one last discussion of the keyword "Owned", which I have never found very helpful: the resource itself isn't owned -- it's a description of something that *can* be owned. (It's "take" that does the owning.) Moreover, "Owned" and "Block" are badly non-parallel, both grammatically and semantically. +// TODO: BCP: Perhaps this is a good time for one last discussion of the keyword "Owned", which I have never found very helpful: the resource itself isn't owned -- it's a description of something that *can* be owned. (It's "take" that does the owning.) Moreover, "Owned" and "Block" are badly non-parallel, both grammatically and semantically. I suggest "Resource" instead of "Owned". (We can keep "Block" -- it's not too bad, IMO.) Given a C-type `+T+` and pointer `+p+`, the resource `+Owned(p)+` asserts ownership of a memory cell at location `+p+` of the size of C-type `+T+`. It is CN’s equivalent of a points-to assertion in separation logic (indexed by C-types `+T+`). @@ -278,33 +278,40 @@ This specification means that: === Resource outputs -However, a caller of `+read+` may also wish to know that `+read+` actually returns the correct value, the pointee of `+p+`, and also that it does not change memory at location `+p+`. To phrase both we need a way to refer to the pointee of `+p+`. +A caller of `+read+` may also wish to know that `+read+` actually returns the correct value, the pointee of `+p+`, and also that it does not change memory at location `+p+`. To phrase both we need a way to refer to the pointee of `+p+`. -In CN resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `+Owned(p)+` (for some C-type `+T+`) outputs the _pointee value_ of `+p+`, since that can be derived from the resource ownership: assume you have a pointer `+p+` and the associated ownership, then this uniquely determines the pointee value of `+p+`. +// TODO: BCP: The idea that "resources have outputs" is very mind-boggling to many new users, *especially* folks with some separation logic background. Needs to be explained very carefully. Also, there's some semantic muddle in the terminology: Is a resource (1) a thing in the heap, (2) a thing in the heap that one is currently holding, or (3) the act of holding a thing in the heap? These are definitely not at all the same thing, but our language at different points suggests all three! To me, (1) is the natural sense of the word "resource"; (2) is somewhat awkward, and (3) is extremely awkward. -CN uses the `+take+`-notation seen in the example above to refer to the output of a resource, introducing a new name binding for the output. The precondition `+take v1 = Owned(p)+` from the precondition does two things: (1) it assert ownership of resource `+Owned(p)+`, and (2) it binds the name `+v1+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+v2+` for the pointee value on function return. +In CN, resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `+Owned(p)+` (for some C-type `+T+`) outputs the _pointee value_ of `+p+`, since that can be derived from the resource ownership: assume you have a pointer `+p+` and the associated ownership, then this uniquely determines the pointee value of `+p+`. +// TODO: BCP: ... in a given heap! (The real problem here is that "and the associated ownership" is pretty vague.) -That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of `+read+` as planned. We add two new postconditions: we specify +CN uses the `+take+`-notation seen in the example above to bind the output of a resource to a new name. The precondition `+take v1 = Owned(p)+` does two things: (1) it assert ownership of resource `+Owned(p)+`, and (2) it binds the name `+v1+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+v2+` for the pointee value on function return. + +// TODO: BCP: But, as we've discussed, the word "take" in the postcondition is quitre confusing: What it's doing is precisely the *opposite* of "taking" the resournce, not taking it but giving it back!! It would be much better if we could choose a more neutral word that doesn't imply either taking or giving. E.g. "resource". + + +That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of `+read+` as planned. We add two new postconditions specifying . that `+read+` returns `+v1+` (the initial pointee value of `+p+`), and . that the pointee values `+v1+` and `+v2+` before and after execution of `+read+` (respectively) are the same. -include_example(solutions/read2.c) +include_example(exercises/read2.c) -*Aside.* In standard separation logic the equivalent specification for `+read+` could have been phrased as follows (where `+return+` binds the return value in the postcondition): +*Aside.* In standard separation logic, the equivalent specification for `+read+` could have been phrased as follows (where `+\return+` binds the return value in the postcondition): .... ∀p. -∀v1. { p ↦ v1 } - read(p) - { return. ∃v2. (p ↦ v2) /\ return = v1 /\ v1 = v2 } + ∀v1. + { p ↦ v1 } + read(p) + { \return. ∃v2. (p ↦ v2) /\ return = v1 /\ v1 = v2 } .... -CN’s `+take+` notation is just alternative syntax for quantification over the values of resources, but a useful one: the `+take+` notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them. +CN’s `+take+` notation is just an alternative syntax for quantification over the values of resources, but a useful one: the `+take+` notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them. === Exercises -*Quadruple*. Specify the function `+quadruple_mem+`, that is similar to the earlier `+quadruple+` function, except that the input is passed as an `+int+` pointer. Write a specification that takes ownership of this pointer on entry and returns this ownership on exit, leaving the pointee value unchanged. +*Quadruple*. Specify the function `+quadruple_mem+`, which is similar to the earlier `+quadruple+` function, except that the input is passed as an `+int+` pointer. Write a specification that takes ownership of this pointer on entry and returns this ownership on exit, leaving the pointee value unchanged. include_example(exercises/slf_quadruple_mem.c) From 17ea167c844d3cc2518814ffe4b2a945b6a5087d Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Fri, 16 Aug 2024 17:51:37 -0400 Subject: [PATCH 22/25] WIP renaming --- src/examples/add_0.c | 4 +- src/examples/add_1.c | 6 +- src/examples/add_2.c | 6 +- src/examples/slf0_basic_incr.c | 2 - src/examples/slf1_basic_example_let.signed.c | 6 +- src/examples/slf2_basic_quadruple.signed.c | 4 +- src/examples/slf3_basic_inplace_double.c | 4 +- src/examples/slf_length_acc.c | 6 +- src/examples/slf_quadruple_mem.c | 4 +- src/tutorial.adoc | 106 +++++++++++++------ 10 files changed, 96 insertions(+), 52 deletions(-) diff --git a/src/examples/add_0.c b/src/examples/add_0.c index 56a35cfd..f0f52745 100644 --- a/src/examples/add_0.c +++ b/src/examples/add_0.c @@ -1,7 +1,7 @@ int add(int x, int y) /* --BEGIN-- */ -/*@ requires let sum = (i64) x + (i64) y; - -2147483648i64 <= sum; sum <= 2147483647i64; @*/ +/*@ requires let Sum = (i64) x + (i64) y; + -2147483648i64 <= Sum; Sum <= 2147483647i64; @*/ /* --END-- */ { return x+y; diff --git a/src/examples/add_1.c b/src/examples/add_1.c index ebd141df..ac30ccc5 100644 --- a/src/examples/add_1.c +++ b/src/examples/add_1.c @@ -1,8 +1,8 @@ int add(int x, int y) /* --BEGIN-- */ -/*@ requires let sum = (i64) x + (i64) y; - -2147483648i64 <= sum; sum <= 2147483647i64; - ensures return == (i32) sum; +/*@ requires let Sum = (i64) x + (i64) y; + -2147483648i64 <= Sum; Sum <= 2147483647i64; + ensures return == (i32) Sum; @*/ /* --END-- */ { diff --git a/src/examples/add_2.c b/src/examples/add_2.c index 17339707..0afd69e0 100644 --- a/src/examples/add_2.c +++ b/src/examples/add_2.c @@ -1,8 +1,8 @@ int add(int x, int y) /* --BEGIN-- */ -/*@ requires let sum = (i64) x + (i64) y; - (i64)MINi32() <= sum; sum <= (i64)MAXi32(); - ensures return == (i32) sum; +/*@ requires let Sum = (i64) x + (i64) y; + (i64)MINi32() <= Sum; Sum <= (i64)MAXi32(); + ensures return == (i32) Sum; @*/ /* --END-- */ { diff --git a/src/examples/slf0_basic_incr.c b/src/examples/slf0_basic_incr.c index f954c842..51aa8f43 100644 --- a/src/examples/slf0_basic_incr.c +++ b/src/examples/slf0_basic_incr.c @@ -1,10 +1,8 @@ void incr (unsigned int *p) -/* --BEGIN-- */ /*@ requires take n1 = Owned(p); ensures take n2 = Owned(p); n2 == n1 + 1u32; @*/ -/* --END-- */ { unsigned int n = *p; unsigned int m = n+1; diff --git a/src/examples/slf1_basic_example_let.signed.c b/src/examples/slf1_basic_example_let.signed.c index c3102646..44064ebd 100644 --- a/src/examples/slf1_basic_example_let.signed.c +++ b/src/examples/slf1_basic_example_let.signed.c @@ -1,8 +1,8 @@ int doubled (int n) /* --BEGIN-- */ -/*@ requires let n_ = (i64) n; - (i64)MINi32() <= n_ - 1i64; n_ + 1i64 <= (i64)MAXi32(); - (i64)MINi32() <= n_ + n_; n_ + n_ <= (i64)MAXi32(); +/*@ requires let N = (i64) n; + (i64)MINi32() <= N - 1i64; N + 1i64 <= (i64)MAXi32(); + (i64)MINi32() <= N + N; N + N <= (i64)MAXi32(); ensures return == n * 2i32; @*/ /* --END-- */ diff --git a/src/examples/slf2_basic_quadruple.signed.c b/src/examples/slf2_basic_quadruple.signed.c index 23a1d495..92e71f5d 100644 --- a/src/examples/slf2_basic_quadruple.signed.c +++ b/src/examples/slf2_basic_quadruple.signed.c @@ -1,7 +1,7 @@ int quadruple (int n) /* --BEGIN-- */ -/*@ requires let n_ = (i64) n; - (i64)MINi32() <= n_ * 4i64; n_ * 4i64 <= (i64)MAXi32(); +/*@ requires let N = (i64) n; + (i64)MINi32() <= N * 4i64; N * 4i64 <= (i64)MAXi32(); ensures return == 4i32 * n; @*/ /* --END-- */ diff --git a/src/examples/slf3_basic_inplace_double.c b/src/examples/slf3_basic_inplace_double.c index 065a96f5..200697f2 100644 --- a/src/examples/slf3_basic_inplace_double.c +++ b/src/examples/slf3_basic_inplace_double.c @@ -1,7 +1,7 @@ void inplace_double (int *p) /* --BEGIN-- */ -/*@ requires take n_ = Owned(p); - let r = 2i64 * ((i64) n_); +/*@ requires take N = Owned(p); + let r = 2i64 * ((i64) N); (i64)MINi32() <= r; r <= (i64)MAXi32(); ensures take m_ = Owned(p); m_ == (i32) r; diff --git a/src/examples/slf_length_acc.c b/src/examples/slf_length_acc.c index 70139691..354d20f4 100644 --- a/src/examples/slf_length_acc.c +++ b/src/examples/slf_length_acc.c @@ -17,11 +17,11 @@ function [rec] (u32) length(datatype List xs) { void IntList_length_acc_aux (struct sllist *xs, unsigned int *p) /*@ requires take L1 = SLList(xs); - take n = Owned(p); + take P = Owned(p); ensures take L1_ = SLList(xs); - take n_ = Owned(p); + take N = Owned(p); L1 == L1_; - n_ == n + length(L1); + N == P + length(L1); @*/ { /*@ unfold length(L1); @*/ diff --git a/src/examples/slf_quadruple_mem.c b/src/examples/slf_quadruple_mem.c index 0c7e647b..b53f2daa 100644 --- a/src/examples/slf_quadruple_mem.c +++ b/src/examples/slf_quadruple_mem.c @@ -1,8 +1,8 @@ int quadruple_mem (int *p) /* --BEGIN-- */ /*@ requires take n = Owned(p); - let n_ = (i64) n; - (i64)MINi32() <= n_ * 4i64; n_ * 4i64 <= (i64)MAXi32(); + let N = (i64) n; + (i64)MINi32() <= N * 4i64; N * 4i64 <= (i64)MAXi32(); ensures take n2 = Owned(p); n2 == n; return == 4i32 * n; diff --git a/src/tutorial.adoc b/src/tutorial.adoc index e6a44057..91b27bfb 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -85,13 +85,13 @@ In detail: * In function specifications, the names of the function arguments, here `+x+` and `+y+`, refer to their _initial values_. (Function arguments are mutable in C.) -* `+let sum = (i64) x + (i64) y+` is a let-binding, which defines `+sum+` as the value `+(i64) x + (i64) y+` in the remainder of the function specification. +* `+let Sum = (i64) x + (i64) y+` is a let-binding, which defines `+Sum+` as the value `+(i64) x + (i64) y+` in the remainder of the function specification. * Instead of C syntax, CN uses Rust-like syntax for integer types, such as `+u32+` for 32-bit unsigned integers and `+i64+` for signed 64-bit integers, to make their sizes unambiguous. Here, `+x+` and `+y+`, of C-type `+int+`, have CN type `+i32+`. // TODO: BCP: I understand this reasoning, but I wonder whether it introduces more confusion than it avoids -- it means there are two ways of writing everything, and people have to remember whether the particular thing they are writing right now is C or CN... // TODO: BCP: Hopefully we are moving toward unifying these notations anyway? -* To define `+sum+` we cast `+x+` and `+y+` to the larger `+i64+` type, using syntax `+(i64)+`, which is large enough to hold the sum of any two `+i32+` values. +* To define `+Sum+` we cast `+x+` and `+y+` to the larger `+i64+` type, using syntax `+(i64)+`, which is large enough to hold the sum of any two `+i32+` values. * Finally, we require this sum to be between the minimal and maximal `+int+` values. Integer constants, such as `+-2147483648i64+`, must specifiy their CN type (`+i64+`). // TODO: BCP: We should use the new ' syntax (or whatever it turned out to be) for numeric constants @@ -103,7 +103,7 @@ We may, however, wish to be more precise. So far, the specification gives no inf include_example(solutions/add_1.c) Here we use the keyword `+return+`, which is only available in function -postconditions, to refer to the return value, and we equate it to `+sum+` +postconditions, to refer to the return value, and we equate it to `+Sum+` as defined in the precondition, cast back to `+i32+` type: that is, `+add+` returns the sum of `+x+` and `+y+`. @@ -219,8 +219,8 @@ As in the first example, we need to ensure that `+n+1+` does not overflow and `+ include_example(solutions/slf1_basic_example_let.signed.c) // TODO: BCP: WHy n_+n_ in some places and n*2i32 in others? -We encode these expectations using a similar style of precondition as in the first example. We first define `+n_+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+`, and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+n_+` does not go below the minimal `+int+` value, that incrementing `+n_+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution. -// TODO: BCP: How about renaming n_ to n64? +We encode these expectations using a similar style of precondition as in the first example. We first define `+N+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+`, and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+N+` does not go below the minimal `+int+` value, that incrementing `+N+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution. +// TODO: BCP: How about renaming N to n64? To capture the functional behaviour, the postcondition specifies that `+return+` is twice the value of `+n+`. @@ -330,7 +330,7 @@ include_example(exercises/read.broken.c) CN rejects this program with the following message: .... -cn build/exercises/read.broken.c +cn verify exercises/read.broken.c [1/1]: read build/exercises/read.broken.c:4:3: error: Left-over unused resource 'Owned(p)(v1)' return *p; @@ -338,37 +338,65 @@ build/exercises/read.broken.c:4:3: error: Left-over unused resource 'Owned(p)+`), and that the function (vacuously) satisfies its postcondition. But, following the check of the postcondition it finds that not all resources have been "`used up`". +CN has typechecked the function and verified (1) that it is safe to +execute under the precondition (given ownership `+Owned(p)+`) +and (2) that the function (vacuously) satisfies its postcondition. But +following the check of the postcondition it finds that not all +resources have been "`used up`". -Given the above specification, `+read+` leaks memory: it takes ownership, does not return it, but also does not deallocate the owned memory or otherwise dispose of it. In CN this is a type error. +Indeed, given the above specification, `+read+` leaks memory: it takes ownership, does not return it, but also does not deallocate the owned memory or otherwise dispose of it. In CN this is a type error. -CN’s resource types are _linear_ (as opposed to affine). This means not only that resources cannot be duplicated, but also that resources cannot simply be dropped or "`forgotten`". Every resource passed into a function has to either be used up by it, by returning it or passing it to another function that consumes it, or destroyed, by deallocating the owned area of memory (as we shall see later). +CN’s resource types are _linear_. This means not only that resources cannot be duplicated, but also that resources cannot simply be dropped or "`forgotten`". Every resource passed into a function has to be either _returned_ to the caller or else _destroyed_ by deallocating the owned area of memory (as we shall see later). -CN’s motivation for linear tracking of resources is its focus on low-level systems software. CN checks C programs, in which, unlike higher-level garbage-collected languages, memory is managed manually, and memory leaks are typically very undesirable. - -As a consequence, function specifications have to do precise "`book-keeping`" of their resource footprint, and, in particular, return any unused resources back to the caller. +CN’s motivation for linear tracking of resources is its focus on +low-level systems software in which memory is managed manually; in +this context, memory leaks are typically very undesirable. As a +consequence, function specifications have to do precise bookkeeping of +their resource footprint and, in particular, return any unused +resources back to the caller. === The Block resource type -Aside from the `+Owned+` resource seen so far, CN has another built-in resource type: `+Block+`. Given a C-type `+T+` and pointer `+p+`, `+Block(p)+` asserts the same ownership as `+Owned(p)+` — so ownership of a memory cell at `+p+` the size of type `+T+` — but in contrast to `+Owned+`, `+Block+` memory is not necessarily initialised. +Aside from the `+Owned+` resources seen so far, CN has another +built-in resource type called `+Block+`. Given a C-type `+T+` and +pointer `+p+`, `+Block(p)+` asserts the same ownership as +`+Owned(p)+` — ownership of a memory cell at `+p+` the size of +type `+T+` — but, in contrast to `+Owned+`, `+Block+` memory is not +assumed to be initialised. CN uses this distinction to prevent reads from uninitialised memory: -* A read at C-type `+T+` and pointer `+p+` requires a resource `+Owned(p)+`, i.e., ownership of _initialised_ memory at the right C-type. The load returns the `+Owned+` resource unchanged. - -* A write at C-type `+T+` and pointer `+p+` needs only a `+Block(p)+` (so, unlike reads, writes to uninitialised memory are fine). The write consumes ownership of the `+Block+` resource (it destroys it) and returns a new resource `+Owned(p)+` with the value written as the output. This means the resource returned from a write records the fact that this memory cell is now initialised and can be read from. - -Since `+Owned+` carries the same ownership as `+Block+`, just with the additional information that the `+Owned+` memory is initalised, a resource `+Owned(p)+` is "`at least as good`" as `+Block(p)+` — an `+Owned(p)+` resource can be used whenever `+Block(p)+` is needed. For instance CN’s type checking of a write to `+p+` requires a `+Block(p)+`, but if an `+Owned(p)+` resource is what is available, this can be used just the same. This allows an already-initialised memory cell to be over-written again. - -Unlike `+Owned+`, whose output is the pointee value, `+Block+` has no meaningful output: its output is `+void+`/`+unit+`. +* A read at C-type `+T+` and pointer `+p+` requires a resource + `+Owned(p)+`, i.e., ownership of _initialised_ memory at the + right C-type. The load returns the `+Owned+` resource unchanged. + +* A write at C-type `+T+` and pointer `+p+` needs only a + `+Block(p)+` (so, unlike reads, writes to uninitialised memory + are fine). The write consumes ownership of the `+Block+` resource + (it destroys it) and returns a new resource `+Owned(p)+` with the + value written as the output. This means the resource returned from a + write records the fact that this memory cell is now initialised and + can be read from. +// TODO: BCP: Not sure I understand "returns a new resource `+Owned(p)+` with the value written as the output" -- perhaps in part because I don't understand what the output of a resource means when the resource is not in the context o a take expression. + +Since `+Owned+` carries the same ownership as `+Block+`, just with the +additional information that the `+Owned+` memory is initalised, a +resource `+Owned(p)+` is "`at least as good`" as `+Block(p)+` — +an `+Owned(p)+` resource can be used whenever `+Block(p)+` is +needed. For instance CN’s type checking of a write to `+p+` requires a +`+Block(p)+`, but if an `+Owned(p)+` resource is what is +available, this can be used just the same. This allows an +already-initialised memory cell to be over-written again. + +Unlike `+Owned+`, whose output is the pointee value, `+Block+` has no meaningful output. === Write example -Let’s explore resources and their outputs in another example. The C function `+incr+` takes an `+int+` pointer `+p+` and increments the pointee value. +Let’s explore resources and their outputs in another example. The C function `+incr+` takes an `+int+` pointer `+p+` and increments the value in the memory cell that it poinbts to. -include_example(solutions/slf0_basic_incr.signed.c) +include_example(examples/slf0_basic_incr.signed.c) -In the precondition we assert ownership of resource `+Owned(p)+`, binding its output/pointee value to `+v1+`, and use `+v1+` to specify that `+p+` must point to a sufficiently small value at the start of the function not to overflow when incremented. The postcondition asserts ownership of `+p+` with output `+v2+`, as before, and uses this to express that the value `+p+` points to is incremented by `+incr+`: `+v2 == v1+1i32+`. +In the precondition we assert ownership of resource `+Owned(p)+`, binding its output/pointee value to `+v1+`, and use `+v1+` to specify that `+p+` must point to a sufficiently small value at the start of the function so as not to overflow when incremented. The postcondition asserts ownership of `+p+` with output `+v2+`, as before, and uses this to express that the value `+p+` points to is incremented by `+incr+`: `+v2 == v1+1i32+`. If we incorrectly tweaked this specification and used `+Block(p)+` instead of `+Owned(p)+` in the precondition, as below, then CN would reject the program. @@ -384,13 +412,22 @@ Resource needed: Owned(p) Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_5da0f3.html .... -The `+Owned(p)+` resource required for reading is missing, since, as per precondition, only `+Block(p)+` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure: +The `+Owned(p)+` resource required for reading is missing, since, per the precondition, only `+Block(p)+` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure: + +* `+Block(p)(u)+`, i.e., ownership of uninitialised memory + at location `+p+`; the output is a `+void+`/`+unit+` value `+u+` + (specified in the second pair of parentheses) -* `+Block(p)(u)+`, so ownership of uninitialised memory at location `+p+`; the output is a `+void+`/`+unit+` value `+u+` (specified in the second pair of parentheses) +* `+Owned(&ARG0)(p)+`, the ownership of (initialised) + memory at location `+&ARG0+`, i.e., the memory location where the + first function argument is stored; its output is the pointer `+p+` + (not to be confused with the pointee of `+p+`); and finally -* `+Owned(&ARG0)(p)+`, the ownership of (initialised) memory at location `+&ARG0+`, so the memory location where the first function argument is stored; its output is the pointer `+p+` (not to be confused with the pointee of `+p+`); and finally +* `+__CN_Alloc(&ARG0)(void)+` is a resource that records allocation + information for location `+&ARG0+`; this is related to CN’s + memory-object semantics, which we ignore for the moment. -* `+__CN_Alloc(&ARG0)(void)+` is a resource that records allocation information for location `+&ARG0+`; this is related to CN’s memory-object semantics, which we ignore for the moment. +// TODO: BCP: These bullet points are all a bit mysterious and maybe TMI. More generally, we should double check that this is actually the information displayed in the current HTML output... === Exercises @@ -404,9 +441,16 @@ include_example(exercises/slf3_basic_inplace_double.c) === Multiple owned pointers -When functions manipulate multiple pointers, we can assert their ownership just like before. However (as in standard separation logic) pointer ownership is unique, so simultaneous ownership of `+Owned+` or `+Block+` resources for two pointers requires these pointers to be disjoint. +When functions manipulate multiple pointers, we can assert their +ownership just like before. However (as in standard separation logic) +pointer ownership is unique -- that is, simultaneously owning +`+Owned+` or `+Block+` resources for two pointers implies that these +pointers are disjoint. -The following example shows the use of two `+Owned+` resources for accessing two different pointers: function `+add+` reads two `+int+` values in memory, at locations `+p+` and `+q+`, and returns their sum. +The following example shows the use of two `+Owned+` resources for +accessing two different pointers by a function `+add+`, which reads +two `+int+` values in memory, at locations `+p+` and `+q+`, and +returns their sum. include_example(exercises/add_read.c) @@ -550,7 +594,7 @@ On exit the array ownership is returned again. This specification, in principle, should ensure that the access `+p[i]+` is safe. However, running CN on the example produces an error: CN is unable to find the required ownership for reading `+p[i]+`. .... -cn build/solutions/array_load.broken.c +cn verify solutions/array_load.broken.c [1/1]: read build/solutions/array_load.broken.c:5:10: error: Missing resource for reading return p[i]; @@ -815,6 +859,8 @@ with allocation and deallocation functions: include_example(exercises/list_c_types.h) +// TODO: BCP: Per discussion with Christopher, Cassia, and Daniel, the word "predicate" is quite confusing for newcomers (in logic, predicates do not return things!). A more neutral word might make for significantly easier onboarding. + To write specifications for C functions that manipulate lists, we need to define a CN "predicate" that describes *mathematical* list structures, as one would do in ML, Haskell, or Coq. (We call them From 6b3f3d1898f1f97e7f56cad9f3d05551e96afff5 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Sun, 18 Aug 2024 17:21:00 -0400 Subject: [PATCH 23/25] WIP more renaming and polishing --- src/examples/abs_mem.c | 4 +- src/examples/add_read.c | 12 ++-- src/examples/init_point.c | 18 +++--- src/examples/read.c | 4 +- src/examples/read2.c | 8 +-- src/examples/slf0_basic_incr.signed.broken.c | 4 +- src/examples/slf0_basic_incr.signed.c | 10 ++- src/examples/slf3_basic_inplace_double.c | 10 +-- src/examples/slf8_basic_transfer.c | 12 ++-- src/examples/slf_quadruple_mem.c | 12 ++-- src/examples/swap.c | 10 +-- src/examples/transpose.broken.c | 8 +-- src/examples/transpose.c | 8 +-- src/examples/transpose2.c | 20 +++--- src/examples/zero.c | 6 +- src/tutorial.adoc | 67 +++++++++++++------- 16 files changed, 115 insertions(+), 98 deletions(-) diff --git a/src/examples/abs_mem.c b/src/examples/abs_mem.c index 488c2992..978fefa0 100644 --- a/src/examples/abs_mem.c +++ b/src/examples/abs_mem.c @@ -2,8 +2,8 @@ int abs_mem (int *p) /* --BEGIN-- */ /*@ requires take x = Owned(p); MINi32() < x; - ensures take x2 = Owned(p); - x == x2; + ensures take x_post = Owned(p); + x == x_post; return == ((x >= 0i32) ? x : (0i32-x)); @*/ /* --END-- */ diff --git a/src/examples/add_read.c b/src/examples/add_read.c index c15c6484..2341bd04 100644 --- a/src/examples/add_read.c +++ b/src/examples/add_read.c @@ -1,10 +1,10 @@ unsigned int add (unsigned int *p, unsigned int *q) -/*@ requires take m = Owned(p); - take n = Owned(q); - ensures take m2 = Owned(p); - take n2 = Owned(q); - m == m2 && n == n2; - return == m + n; +/*@ requires take P = Owned(p); + take Q = Owned(q); + ensures take P_post = Owned(p); + take Q_post = Owned(q); + P == P_post && Q == Q_post; + return == P + Q; @*/ { unsigned int m = *p; diff --git a/src/examples/init_point.c b/src/examples/init_point.c index b907a950..4ecb67f3 100644 --- a/src/examples/init_point.c +++ b/src/examples/init_point.c @@ -1,18 +1,18 @@ -void zero (int *p) -/*@ requires take u = Block(p); - ensures take v = Owned(p); - v == 0i32; @*/ +void zero (int *coord) +/*@ requires take Coord = Block(coord); + ensures take Coord_post = Owned(coord); + Coord_post == 0i32; @*/ { - *p = 0; + *coord = 0; } struct point { int x; int y; }; void init_point(struct point *p) -/*@ requires take s = Block(p); - ensures take s2 = Owned(p); - s2.x == 0i32; - s2.y == 0i32; +/*@ requires take P = Block(p); + ensures take P_post = Owned(p); + P_post.x == 0i32; + P_post.y == 0i32; @*/ { zero(&p->x); diff --git a/src/examples/read.c b/src/examples/read.c index 5a09f6dd..04892f56 100644 --- a/src/examples/read.c +++ b/src/examples/read.c @@ -1,7 +1,7 @@ int read (int *p) /* --BEGIN-- */ -/*@ requires take v1 = Owned(p); - ensures take v2 = Owned(p); +/*@ requires take P = Owned(p); + ensures take P_post = Owned(p); @*/ /* --END-- */ { diff --git a/src/examples/read2.c b/src/examples/read2.c index 4528c534..94ca64ea 100644 --- a/src/examples/read2.c +++ b/src/examples/read2.c @@ -1,8 +1,8 @@ int read (int *p) -/*@ requires take v1 = Owned(p); - ensures take v2 = Owned(p); - return == v1; - v1 == v2; +/*@ requires take P = Owned(p); + ensures take P_post = Owned(p); + return == P; + P_post == P; @*/ { return *p; diff --git a/src/examples/slf0_basic_incr.signed.broken.c b/src/examples/slf0_basic_incr.signed.broken.c index a4959035..3fbd627d 100644 --- a/src/examples/slf0_basic_incr.signed.broken.c +++ b/src/examples/slf0_basic_incr.signed.broken.c @@ -1,6 +1,6 @@ void incr (int *p) -/*@ requires take u = Block(p); - ensures take v = Owned(p); +/*@ requires take P = Block(p); + ensures take P_post = Owned(p); @*/ { *p = *p+1; diff --git a/src/examples/slf0_basic_incr.signed.c b/src/examples/slf0_basic_incr.signed.c index ae0656d5..2986c617 100644 --- a/src/examples/slf0_basic_incr.signed.c +++ b/src/examples/slf0_basic_incr.signed.c @@ -1,11 +1,9 @@ void incr (int *p) -/* --BEGIN-- */ -/*@ requires take v1 = Owned(p); - ((i64) v1) + 1i64 <= (i64)MAXi32(); - ensures take v2 = Owned(p); - v2 == v1+1i32; +/*@ requires take P = Owned(p); + ((i64) P) + 1i64 <= (i64) MAXi32(); + ensures take P_post = Owned(p); + P_post == P + 1i32; @*/ -/* --END-- */ { *p = *p+1; } diff --git a/src/examples/slf3_basic_inplace_double.c b/src/examples/slf3_basic_inplace_double.c index 200697f2..ca7cddde 100644 --- a/src/examples/slf3_basic_inplace_double.c +++ b/src/examples/slf3_basic_inplace_double.c @@ -1,10 +1,10 @@ void inplace_double (int *p) /* --BEGIN-- */ -/*@ requires take N = Owned(p); - let r = 2i64 * ((i64) N); - (i64)MINi32() <= r; r <= (i64)MAXi32(); - ensures take m_ = Owned(p); - m_ == (i32) r; +/*@ requires take P = Owned(p); + let M = 2i64 * ((i64) P); + (i64) MINi32() <= M; M <= (i64) MAXi32(); + ensures take P_post = Owned(p); + P_post == (i32) M; @*/ /* --END-- */ { diff --git a/src/examples/slf8_basic_transfer.c b/src/examples/slf8_basic_transfer.c index ffa37489..71a80c6a 100644 --- a/src/examples/slf8_basic_transfer.c +++ b/src/examples/slf8_basic_transfer.c @@ -1,11 +1,11 @@ void transfer (unsigned int *p, unsigned int *q) /* --BEGIN-- */ -/*@ requires take n1 = Owned(p); - take m1 = Owned(q); - ensures take n2 = Owned(p); - take m2 = Owned(q); - n2 == n1 + m1; - m2 == 0u32; +/*@ requires take P = Owned(p); + take Q = Owned(q); + ensures take P_post = Owned(p); + take Q_post = Owned(q); + P_post == P + Q; + Q_post == 0u32; @*/ /* --END-- */ { diff --git a/src/examples/slf_quadruple_mem.c b/src/examples/slf_quadruple_mem.c index b53f2daa..c7a86dc3 100644 --- a/src/examples/slf_quadruple_mem.c +++ b/src/examples/slf_quadruple_mem.c @@ -1,11 +1,11 @@ int quadruple_mem (int *p) /* --BEGIN-- */ -/*@ requires take n = Owned(p); - let N = (i64) n; - (i64)MINi32() <= N * 4i64; N * 4i64 <= (i64)MAXi32(); - ensures take n2 = Owned(p); - n2 == n; - return == 4i32 * n; +/*@ requires take P = Owned(p); + let P64 = (i64) P; + (i64)MINi32() <= P64 * 4i64; P64 * 4i64 <= (i64)MAXi32(); + ensures take P_post = Owned(p); + P_post == P; + return == 4i32 * P; @*/ /* --END-- */ { diff --git a/src/examples/swap.c b/src/examples/swap.c index 31a8c119..435ef1b0 100644 --- a/src/examples/swap.c +++ b/src/examples/swap.c @@ -1,10 +1,10 @@ void swap (unsigned int *p, unsigned int *q) /* --BEGIN-- */ -/*@ requires take v = Owned(p); - take w = Owned(q); - ensures take v2 = Owned(p); - take w2 = Owned(q); - v2 == w && w2 == v; +/*@ requires take P = Owned(p); + take Q = Owned(q); + ensures take P_post = Owned(p); + take Q_post = Owned(q); + P_post == Q && Q_post == P; @*/ /* --END-- */ { diff --git a/src/examples/transpose.broken.c b/src/examples/transpose.broken.c index 3bb2ca95..47ef9479 100644 --- a/src/examples/transpose.broken.c +++ b/src/examples/transpose.broken.c @@ -1,10 +1,10 @@ struct point { int x; int y; }; void transpose (struct point *p) -/*@ requires take s = Owned(p); - ensures take s2 = Owned(p); - s2.x == s.y; - s2.y == s.x; +/*@ requires take P = Owned(p); + ensures take P_post = Owned(p); + P_post.x == P.y; + P_post.y == P.x; @*/ { int temp_x = p->x; diff --git a/src/examples/transpose.c b/src/examples/transpose.c index 5bab82bf..03b1d9d8 100644 --- a/src/examples/transpose.c +++ b/src/examples/transpose.c @@ -1,10 +1,10 @@ struct point { int x; int y; }; void transpose (struct point *p) -/*@ requires take s = Owned(p); - ensures take s2 = Owned(p); - s2.x == s.y; - s2.y == s.x; +/*@ requires take P = Owned(p); + ensures take P_post = Owned(p); + P_post.x == P.y; + P_post.y == P.x; @*/ { int temp_x = p->x; diff --git a/src/examples/transpose2.c b/src/examples/transpose2.c index 6a903ad3..31b390fd 100644 --- a/src/examples/transpose2.c +++ b/src/examples/transpose2.c @@ -1,9 +1,9 @@ void swap (unsigned int *p, unsigned int *q) -/*@ requires take v = Owned(p); - take w = Owned(q); - ensures take v2 = Owned(p); - take w2 = Owned(q); - v2 == w && w2 == v; +/*@ requires take P = Owned(p); + take Q = Owned(q); + ensures take P_post = Owned(p); + take Q_post = Owned(q); + P_post == Q && Q_post == P; @*/ { unsigned int m = *p; @@ -16,12 +16,12 @@ struct upoint { unsigned int x; unsigned int y; }; void transpose2 (struct upoint *p) /* --BEGIN-- */ -/*@ requires take s = Owned(p); - ensures take s2 = Owned(p); - s2.x == s.y; - s2.y == s.x; +/*@ requires take P = Owned(p); + ensures take P_post = Owned(p); + P_post.x == P.y; + P_post.y == P.x; @*/ +/* --END-- */ { swap(&p->x, &p->y); } -/* --END-- */ diff --git a/src/examples/zero.c b/src/examples/zero.c index e6ac6cdd..c7fbf8c7 100644 --- a/src/examples/zero.c +++ b/src/examples/zero.c @@ -1,8 +1,8 @@ void zero (int *p) /* --BEGIN-- */ -/*@ requires take u = Block(p); - ensures take v = Owned(p); - v == 0i32; +/*@ requires take P = Block(p); + ensures take P_post = Owned(p); + P_post == 0i32; @*/ /* --END-- */ { diff --git a/src/tutorial.adoc b/src/tutorial.adoc index 91b27bfb..dc02b08e 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -285,15 +285,16 @@ A caller of `+read+` may also wish to know that `+read+` actually returns the co In CN, resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `+Owned(p)+` (for some C-type `+T+`) outputs the _pointee value_ of `+p+`, since that can be derived from the resource ownership: assume you have a pointer `+p+` and the associated ownership, then this uniquely determines the pointee value of `+p+`. // TODO: BCP: ... in a given heap! (The real problem here is that "and the associated ownership" is pretty vague.) -CN uses the `+take+`-notation seen in the example above to bind the output of a resource to a new name. The precondition `+take v1 = Owned(p)+` does two things: (1) it assert ownership of resource `+Owned(p)+`, and (2) it binds the name `+v1+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+v2+` for the pointee value on function return. +CN uses the `+take+`-notation seen in the example above to bind the output of a resource to a new name. The precondition `+take P = Owned(p)+` does two things: (1) it assert ownership of resource `+Owned(p)+`, and (2) it binds the name `+P+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+P_post+` for the pointee value on function return. // TODO: BCP: But, as we've discussed, the word "take" in the postcondition is quitre confusing: What it's doing is precisely the *opposite* of "taking" the resournce, not taking it but giving it back!! It would be much better if we could choose a more neutral word that doesn't imply either taking or giving. E.g. "resource". +// TODO: BCP: This might be a good place for a comment on naming conventions That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of `+read+` as planned. We add two new postconditions specifying -. that `+read+` returns `+v1+` (the initial pointee value of `+p+`), and -. that the pointee values `+v1+` and `+v2+` before and after execution of `+read+` (respectively) are the same. +. that `+read+` returns `+P+` (the initial pointee value of `+p+`), and +. that the pointee values `+P+` and `+P_post+` before and after execution of `+read+` (respectively) are the same. include_example(exercises/read2.c) @@ -302,9 +303,9 @@ include_example(exercises/read2.c) .... ∀p. ∀v1. - { p ↦ v1 } + { p ↦ P } read(p) - { \return. ∃v2. (p ↦ v2) /\ return = v1 /\ v1 = v2 } + { \return. ∃P_post. (p ↦ P_post) /\ return = P /\ P = P_post } .... CN’s `+take+` notation is just an alternative syntax for quantification over the values of resources, but a useful one: the `+take+` notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them. @@ -390,13 +391,19 @@ already-initialised memory cell to be over-written again. Unlike `+Owned+`, whose output is the pointee value, `+Block+` has no meaningful output. -=== Write example +=== Writing through pointers Let’s explore resources and their outputs in another example. The C function `+incr+` takes an `+int+` pointer `+p+` and increments the value in the memory cell that it poinbts to. -include_example(examples/slf0_basic_incr.signed.c) +include_example(exercises/slf0_basic_incr.signed.c) -In the precondition we assert ownership of resource `+Owned(p)+`, binding its output/pointee value to `+v1+`, and use `+v1+` to specify that `+p+` must point to a sufficiently small value at the start of the function so as not to overflow when incremented. The postcondition asserts ownership of `+p+` with output `+v2+`, as before, and uses this to express that the value `+p+` points to is incremented by `+incr+`: `+v2 == v1+1i32+`. +In the precondition we assert ownership of resource `+Owned(p)+`, +binding its output/pointee value to `+P+`, and use `+P+` to specify +that `+p+` must point to a sufficiently small value at the start of +the function so as not to overflow when incremented. The postcondition +asserts ownership of `+p+` with output `+P_post+`, as before, and uses +this to express that the value `+p+` points to is incremented by +`+incr+`: `+P_post == P + 1i32+`. If we incorrectly tweaked this specification and used `+Block(p)+` instead of `+Owned(p)+` in the precondition, as below, then CN would reject the program. @@ -442,8 +449,8 @@ include_example(exercises/slf3_basic_inplace_double.c) === Multiple owned pointers When functions manipulate multiple pointers, we can assert their -ownership just like before. However (as in standard separation logic) -pointer ownership is unique -- that is, simultaneously owning +ownership just like before. However +pointer ownership in CN is unique -- that is, simultaneously owning `+Owned+` or `+Block+` resources for two pointers implies that these pointers are disjoint. @@ -452,14 +459,17 @@ accessing two different pointers by a function `+add+`, which reads two `+int+` values in memory, at locations `+p+` and `+q+`, and returns their sum. +// TODO: BCP: Hmmm -- I'm not very sure that the way I've been naming things is actually working that well. The problem is that in examples like this we computer "thing pointed to by p" at both C and CN levels. At the C level, the thing pointed to by p obviously cannot also be called p, so it doesn't make sense for it to be called P at the CN level, right? Maybe we need to think again, but hoinestly I am not certain that it is *not* working either. So I'm going to opush on for now... + include_example(exercises/add_read.c) This time we use C’s `+unsigned int+` type. In C, over- and underflow of unsigned integers is not undefined behaviour, so we do not need any special preconditions to rule this out. Instead, when an arithmetic operation at unsigned type goes outside the representable range, the value "`wraps around`". -The CN variables `+m+` and `+n+` (resp. `+m2+` and `+n2+`) for the pointee values of `+p+` and `+q+` before (resp. after) the execution of `+add+` have CN basetype `+u32+`, so unsigned 32-bit integers, matching the C `+unsigned int+` type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type. -// TODO: BCP: I propose that we uniformly use i32 integers everywhere in the tutorial (just mentioning in the bullet list below that there are other integer types, and using i64 for calculations that may overflow). Forgetting which integer type I was using was a common (and silly) failure mode when I was first working through the tutorial. +The CN variables `+P+` and `+Q+` (resp. `+P_post+` and `+Q_post+`) for the pointee values of `+p+` and `+q+` before (resp. after) the execution of `+add+` have CN basetype `+u32+`, so unsigned 32-bit integers, matching the C `+unsigned int+` type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type. + +Hence, the postcondition `+return == P + Q+` holds also when the sum of `+P+` and `+Q+` is greater than the maximal `+unsigned int+` value. -Hence, the postcondition `+return == m+n+` holds also when the sum of `+m+` and `+n+` is greater than the maximal `+unsigned int+` value. +// TODO: BCP: I wonder whether we should uniformly use i32 integers everywhere in the tutorial (just mentioning in the bullet list below that there are other integer types, and using i64 for calculations that may overflow). Forgetting which integer type I was using was a common (and silly) failure mode when I was first working through the tutorial. In the following we will sometimes use unsigned integer types to focus on specifying memory ownership, rather than the conditions necessary to show absence of C arithmetic undefined behaviour. @@ -475,23 +485,30 @@ include_example(exercises/slf8_basic_transfer.c) == Ownership of compound objects -So far all examples have worked with just integers and pointers, but larger programs typically also manipulate compound values, often represented using C struct types. Specifying functions manipulating structs works in much the same way as with basic types. +So far, our examples have worked with just integers and pointers, but larger programs typically also manipulate compound values, often represented using C struct types. Specifying functions manipulating structs works in much the same way as with basic types. For instance, the following example uses a `+struct+` `+point+` to represent a point in two-dimensional space. The function `+transpose+` swaps a point’s `+x+` and `+y+` coordinates. include_example(exercises/transpose.c) -Here the precondition asserts ownership for `+p+`, at type `+struct point+`; the output `+s+` is a value of CN type `+struct point+`, i.e. a record with members `+i32+` `+x+` and `+i32+` `+y+`. The postcondition similarly asserts ownership of `+p+`, with output `+s2+`, and asserts the coordinates have been swapped, by referring to the members of `+s+` and `+s2+` individually. +Here the precondition asserts ownership for `+p+`, at type `+struct +point+`; the output `+P_post+` is a value of CN type `+struct point+`, +i.e. a record with members `+i32+` `+x+` and `+i32+` `+y+`. The +postcondition similarly asserts ownership of `+p+`, with output +`+P_post+`, and asserts the coordinates have been swapped, by referring to +the members of `+P+` and `+P_post+` individually. + +// TODO: BCP: This paragraph is quite confusing if read carefully: it seems to say that the "take" in the requires clause returns a different type than the "tajke" in the "ensures" clause. Moreover, even if the reader decides that this cannot be the case and they have to return the same type, they may wonder whether thius type is a C type (which is what it looks like, since there is only one struct declaration, and it is not in a magic comment) or a CN type (which might be expected, since it is the result of a "take"). I *guess* what's going on here is that every C type is automatically reflected as a CN type with the same name. But this story is also not 100% satisfying, since the basic numeric types don't work this way: each C numeric type has an *analog* in CN, but with a different name. === Compound Owned and Block resources -While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to _individual struct members_ and pass these as values, even to other functions. +While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to _individual struct members_ and manipulate these as values, including even passing them to other functions. -CN therefore cannot treat resources for compound C types, such as structs, as primitive, indivisible units. Instead, `+Owned+` and `+Block+` are defined inductively in the structure of the C-type `+T+`. +CN therefore cannot treat resources for compound C types like structs as primitive, indivisible units. Instead, `+Owned+` and `+Block+` are defined inductively on the structure of the C-type `+T+`. -For struct types `+T+`, the `+Owned+` resource is defined as the collection of `+Owned+` resources for its members (as well as `+Block+` resources for any padding bytes in-between). The resource `+Block+`, similarly, is made up of `+Block+` resources for all members (and padding bytes). +For struct types `+T+`, the `+Owned+` resource is defined as the collection of `+Owned+` resources for its members (as well as `+Block+` resources for any padding bytes in-between them). The resource `+Block+`, similarly, is made up of `+Block+` resources for all members (and padding bytes). -To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and recompose it, as needed. The following example illustrates this. +To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and it can recompose the struct later, as needed. The following example illustrates this. Recall the function `+zero+` from our earlier exercise. It takes an `+int+` pointer to uninitialised memory, with `+Block+` ownership, and initialises the value to zero, returning an `+Owned+` resource with output `+0+`. @@ -501,25 +518,27 @@ include_example(exercises/init_point.c) As stated in its precondition, `+init_point+` receives ownership `+Block(p)+`. The `+zero+` function, however, works on `+int+` pointers and requires `+Block+` ownership. -CN can prove the calls to `+zero+` with `+&p->x+` and `+&p->y+` are safe because it decomposes the `+Block(p)+` into two `+Block+`, one for member `+x+`, one for member `+y+`. Later, the reverse happens: following the two calls to `+zero+`, as per `+zero+`’s precondition, `+init_point+` has ownership of two adjacent `+Owned+` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `+init_point+` requires ownership `+Owned(p)+`, CN combines these back into a compound resource. The resulting `+Owned+` resource has for an output the struct value `+s2+` that is composed of the zeroed member values for `+x+` and `+y+`. +CN can prove the calls to `+zero+` with `+&p->x+` and `+&p->y+` are safe because it decomposes the `+Block(p)+` into a `+Block+` for member `+x+` and a `+Block+` for member `+y+`. Later, the reverse happens: following the two calls to `+zero+`, as per `+zero+`’s precondition, `+init_point+` has ownership of two adjacent `+Owned+` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `+init_point+` requires ownership `+Owned(p)+`, CN combines these back into a compound resource. The resulting `+Owned+` resource has for an output the struct value `+P_post+` that is composed of the zeroed member values for `+x+` and `+y+`. === Resource inference To handle the required resource inference, CN "`eagerly`" decomposes all `+struct+` resources into resources for the struct members, and "`lazily`" re-composes them as needed. -We can see this if, for instance, we experimentally change the `+transpose+` example from above to force a type error. Let’s insert an `+/*@ assert(false) @*/+` CN assertion in the middle of the `+transpose+` function (more on CN assertions later), so we can inspect CN’s proof context shown in the error report. +We can see this if, for instance, we experimentally change the `+transpose+` example from above to force a type error. Let’s insert an `+/*@ assert(false) @*/+` CN assertion in the middle of the `+transpose+` function, so we can inspect CN’s proof context shown in the error report. (More on CN assertions later.) include_example(exercises/transpose.broken.c) The precondition of `+transpose+` asserts ownership of an `+Owned(p)+` resource. The error report now instead lists under "`Available resources`" two resources: -* `+Owned(member_shift(p, x))+` with output `+s.x+` and +* `+Owned(member_shift(p, x))+` with output `+P.x+` and + +* `+Owned(member_shift(p, y))+` with output `+P.y+` -* `+Owned(member_shift(p, y))+` with output `+s.y+` +// TODO: BCP: We should verify that it really does say this. Here `+member_shift(p,m)+` is the CN expression that constructs, from a `+struct s+` pointer `+p+`, the "`shifted`" pointer for its member `+m+`. -When the function returns the two member resources are recombined "`on demand`" to satisfy the postcondition `+Owned(p)+`. +When the function returns, the two member resources are recombined "`on demand`" to satisfy the postcondition `+Owned(p)+`. === Exercises From b7733b990404634b3c18b9a430eb69e9cf2de0a7 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Mon, 19 Aug 2024 09:02:19 -0400 Subject: [PATCH 24/25] WIP more renaming and polishing --- src/examples/add_two_array.c | 10 ++-- src/examples/array_load.broken.c | 7 ++- src/examples/array_load.c | 11 ++-- src/examples/free.h | 4 +- src/examples/init_array.c | 12 ++-- src/examples/init_array2.c | 12 ++-- src/examples/init_array_rev.c | 14 +++-- src/examples/malloc.h | 5 +- src/examples/ref.h | 9 ++- src/examples/slf17_get_and_free.c | 5 +- src/examples/slf_incr2.c | 36 ++++++------ src/examples/slf_incr2_alias.c | 31 +++++++--- src/examples/slf_incr2_noalias.c | 12 ++-- src/examples/slf_ref_greater.c | 12 ++-- src/tutorial.adoc | 94 ++++++++++++++++++++++--------- 15 files changed, 173 insertions(+), 101 deletions(-) diff --git a/src/examples/add_two_array.c b/src/examples/add_two_array.c index 799edaf7..70a8e5fc 100644 --- a/src/examples/add_two_array.c +++ b/src/examples/add_two_array.c @@ -1,12 +1,14 @@ unsigned int array_read_two (unsigned int *p, int n, int i, int j) /* --BEGIN-- */ -/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; +/*@ requires take A = each(i32 k; 0i32 <= k && k < n) { + Owned(array_shift(p,k)) }; 0i32 <= i && i < n; 0i32 <= j && j < n; j != i; - ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned(array_shift(p,k)) }; - a1 == a2; - return == a1[i] + a1[j]; + ensures take A_post = each(i32 k; 0i32 <= k && k < n) { + Owned(array_shift(p,k)) }; + A == A_post; + return == A[i] + A[j]; @*/ /* --END-- */ { diff --git a/src/examples/array_load.broken.c b/src/examples/array_load.broken.c index 3f4b6e63..446072cf 100644 --- a/src/examples/array_load.broken.c +++ b/src/examples/array_load.broken.c @@ -1,7 +1,10 @@ int read (int *p, int n, int i) -/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; +/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { + Owned(array_shift(p,j)) }; 0i32 <= i && i < n; - ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned(array_shift(p,j)) }; @*/ + ensures take A_post = each(i32 j; 0i32 <= j && j < n) { + Owned(array_shift(p,j)) }; +@*/ { return p[i]; } diff --git a/src/examples/array_load.c b/src/examples/array_load.c index eef0dab2..6cd87216 100644 --- a/src/examples/array_load.c +++ b/src/examples/array_load.c @@ -1,9 +1,10 @@ int read (int *p, int n, int i) -/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { - Owned(array_shift(p,j)) }; - 0i32 <= i && i < n; - ensures take a2 = each(i32 j; 0i32 <= j && j < n) { - Owned(array_shift(p,j)) }; @*/ +/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { + Owned(array_shift(p,j)) }; + 0i32 <= i && i < n; + ensures take A_post = each(i32 j; 0i32 <= j && j < n) { + Owned(array_shift(p,j)) }; +@*/ { /*@ extract Owned, i; @*/ return p[i]; diff --git a/src/examples/free.h b/src/examples/free.h index 9643f4f3..b5eb5832 100644 --- a/src/examples/free.h +++ b/src/examples/free.h @@ -1,13 +1,13 @@ extern void freeInt (int *p); /*@ spec freeInt(pointer p); - requires take v = Block(p); + requires take P = Block(p); ensures true; @*/ extern void freeUnsignedInt (unsigned int *p); /*@ spec freeUnsignedInt(pointer p); - requires take v = Block(p); + requires take P = Block(p); ensures true; @*/ diff --git a/src/examples/init_array.c b/src/examples/init_array.c index 5fb3c97a..b288cb1c 100644 --- a/src/examples/init_array.c +++ b/src/examples/init_array.c @@ -1,13 +1,17 @@ void init_array (char *p, unsigned int n) -/*@ requires take a1 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; - ensures take a2 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; +/*@ requires take A = each(u32 i; i < n) { + Owned( array_shift(p, i)) }; + ensures take A_post = each(u32 i; i < n) { + Owned( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take ai = each(u32 i; i < n) { Owned( array_shift(p, i)) }; - {p} unchanged; {n} unchanged; + /*@ inv take Ai = each(u32 i; i < n) { + Owned( array_shift(p, i)) }; + {p} unchanged; + {n} unchanged; @*/ /* --END-- */ { diff --git a/src/examples/init_array2.c b/src/examples/init_array2.c index e1217845..f447f553 100644 --- a/src/examples/init_array2.c +++ b/src/examples/init_array2.c @@ -1,13 +1,17 @@ void init_array2 (char *p, unsigned int n) -/*@ requires take a1 = each(u32 i; i < n) { Block( array_shift(p, i)) }; - ensures take a2 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; +/*@ requires take A = each(u32 i; i < n) { + Block( array_shift(p, i)) }; + ensures take A_post = each(u32 i; i < n) { + Owned( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take al = each(u32 i; i < j) { Owned( array_shift(p, i)) }; - take ar = each(u32 i; j <= i && i < n) { Block( array_shift(p, i)) }; + /*@ inv take Al = each(u32 i; i < j) { + Owned( array_shift(p, i)) }; + take Ar = each(u32 i; j <= i && i < n) { + Block( array_shift(p, i)) }; {p} unchanged; {n} unchanged; j <= n; @*/ diff --git a/src/examples/init_array_rev.c b/src/examples/init_array_rev.c index dd8de2b7..e46b4f3f 100644 --- a/src/examples/init_array_rev.c +++ b/src/examples/init_array_rev.c @@ -1,14 +1,18 @@ -void init_array2 (char *p, unsigned int n) -/*@ requires take a1 = each(u32 i; i < n) { Block( array_shift(p, i)) }; +void init_array_rev (char *p, unsigned int n) +/*@ requires take A = each(u32 i; i < n) { + Block( array_shift(p, i)) }; n > 0u32; - ensures take a2 = each(u32 i; i < n) { Owned( array_shift(p, i)) }; + ensures take A_post = each(u32 i; i < n) { + Owned( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take al = each(u32 i; i < n-j) { Block( array_shift(p, i)) }; - take ar = each(u32 i; n-j <= i && i < n) { Owned( array_shift(p, i)) }; + /*@ inv take Al = each(u32 i; i < n-j) { + Block( array_shift(p, i)) }; + take Ar = each(u32 i; n-j <= i && i < n) { + Owned( array_shift(p, i)) }; {p} unchanged; {n} unchanged; 0u32 <= j && j <= n; @*/ diff --git a/src/examples/malloc.h b/src/examples/malloc.h index 7182d1a2..fe2c2fc2 100644 --- a/src/examples/malloc.h +++ b/src/examples/malloc.h @@ -1,13 +1,12 @@ extern int *mallocInt (); /*@ spec mallocInt(); requires true; - ensures take v = Block(return); + ensures take R = Block(return); @*/ - extern unsigned int *mallocUnsignedInt (); /*@ spec mallocUnsignedInt(); requires true; - ensures take v = Block(return); + ensures take R = Block(return); @*/ diff --git a/src/examples/ref.h b/src/examples/ref.h index cbd68d5f..bbb83fa0 100644 --- a/src/examples/ref.h +++ b/src/examples/ref.h @@ -1,15 +1,14 @@ extern unsigned int *refUnsignedInt (unsigned int v); /*@ spec refUnsignedInt(u32 v); requires true; - ensures take vr = Owned(return); - vr == v; + ensures take R = Owned(return); + R == v; @*/ - extern int *refInt (int v); /*@ spec refInt(i32 v); requires true; - ensures take vr = Owned(return); - vr == v; + ensures take R = Owned(return); + R == v; @*/ diff --git a/src/examples/slf17_get_and_free.c b/src/examples/slf17_get_and_free.c index 8c6e59aa..a2238315 100644 --- a/src/examples/slf17_get_and_free.c +++ b/src/examples/slf17_get_and_free.c @@ -1,8 +1,9 @@ #include "free.h" unsigned int get_and_free (unsigned int *p) -/*@ requires take v1_ = Owned(p); - ensures return == v1_; @*/ +/*@ requires take P = Owned(p); + ensures return == P; +@*/ { unsigned int v = *p; freeUnsignedInt (p); diff --git a/src/examples/slf_incr2.c b/src/examples/slf_incr2.c index 94de75c6..43e99c3f 100644 --- a/src/examples/slf_incr2.c +++ b/src/examples/slf_incr2.c @@ -1,25 +1,25 @@ /*@ -predicate { u32 pv, u32 qv } BothOwned (pointer p, pointer q) +predicate { u32 P, u32 Q } BothOwned (pointer p, pointer q) { if (ptr_eq(p,q)) { - take pv = Owned(p); - return {pv: pv, qv: pv}; + take PX = Owned(p); + return {P: PX, Q: PX}; } else { - take pv = Owned(p); - take qv = Owned(q); - return {pv: pv, qv: qv}; + take PX = Owned(p); + take QX = Owned(q); + return {P: PX, Q: QX}; } } @*/ void incr2 (unsigned int *p, unsigned int *q) -/*@ requires take vs = BothOwned(p,q); - ensures take vs_ = BothOwned(p,q); - ptr_eq (vs_.pv, - (!ptr_eq(p,q)) ? (vs.pv + 1u32) : (vs.pv + 2u32)); - ptr_eq (vs_.qv, - (!ptr_eq(p,q)) ? (vs.qv + 1u32) : vs_.pv); +/*@ requires take PQ = BothOwned(p,q); + ensures take PQ_post = BothOwned(p,q); + ptr_eq (PQ_post.P, + (!ptr_eq(p,q)) ? (PQ.P + 1u32) : (PQ.P + 2u32)); + ptr_eq (PQ_post.Q, + (!ptr_eq(p,q)) ? (PQ.Q + 1u32) : PQ_post.P); @*/ { /*@ split_case ptr_eq(p,q); @*/ @@ -32,13 +32,13 @@ void incr2 (unsigned int *p, unsigned int *q) } void call_both_better (unsigned int *p, unsigned int *q) -/*@ requires take pv = Owned(p); - take qv = Owned(q); +/*@ requires take P = Owned(p); + take Q = Owned(q); !ptr_eq(p,q); - ensures take pv_ = Owned(p); - take qv_ = Owned(q); - pv_ == pv + 3u32; - qv_ == qv + 1u32; + ensures take P_post = Owned(p); + take Q_post = Owned(q); + P_post == P + 3u32; + Q_post == Q + 1u32; @*/ { incr2(p, q); diff --git a/src/examples/slf_incr2_alias.c b/src/examples/slf_incr2_alias.c index 2eff193b..2f8cd75c 100644 --- a/src/examples/slf_incr2_alias.c +++ b/src/examples/slf_incr2_alias.c @@ -1,9 +1,28 @@ +// Increment two different pointers (same as above) +void incr2a (unsigned int *p, unsigned int *q) +/*@ requires take P = Owned(p); + take Q = Owned(q); + ensures take P_post = Owned(p); + take Q_post = Owned(q); + P_post == P + 1u32; + Q_post == Q + 1u32; +@*/ +{ + unsigned int n = *p; + unsigned int m = n+1; + *p = m; + n = *q; + m = n+1; + *q = m; +} + +// Increment the same pointer twice void incr2b (unsigned int *p, unsigned int *q) -/*@ requires take pv = Owned(p); +/*@ requires take P = Owned(p); ptr_eq(q,p); - ensures take pv_ = Owned(p); + ensures take P_post = Owned(p); ptr_eq(q,p); - pv_ == pv + 2u32; + P_post == P + 2u32; @*/ { unsigned int n = *p; @@ -14,8 +33,6 @@ void incr2b (unsigned int *p, unsigned int *q) *q = m; } -#include "slf_incr2_noalias.c" - void call_both (unsigned int *p, unsigned int *q) /*@ requires take pv = Owned(p); take qv = Owned(q); @@ -25,6 +42,6 @@ void call_both (unsigned int *p, unsigned int *q) qv_ == qv + 1u32; @*/ { - incr2a(p, q); - incr2b(p, p); + incr2a(p, q); // increment two different pointers + incr2b(p, p); // increment the same pointer twice } diff --git a/src/examples/slf_incr2_noalias.c b/src/examples/slf_incr2_noalias.c index d4966069..7c7e2369 100644 --- a/src/examples/slf_incr2_noalias.c +++ b/src/examples/slf_incr2_noalias.c @@ -1,10 +1,10 @@ void incr2a (unsigned int *p, unsigned int *q) -/*@ requires take pv = Owned(p); - take qv = Owned(q); - ensures take pv_ = Owned(p); - take qv_ = Owned(q); - pv_ == pv + 1u32; - qv_ == qv + 1u32; +/*@ requires take P = Owned(p); + take Q = Owned(q); + ensures take P_post = Owned(p); + take Q_post = Owned(q); + P_post == P + 1u32; + Q_post == Q + 1u32; @*/ { unsigned int n = *p; diff --git a/src/examples/slf_ref_greater.c b/src/examples/slf_ref_greater.c index 23c54c9c..96138e91 100644 --- a/src/examples/slf_ref_greater.c +++ b/src/examples/slf_ref_greater.c @@ -2,12 +2,12 @@ unsigned int *ref_greater_abstract (unsigned int *p) /* --BEGIN-- */ -/*@ requires take m1 = Owned(p); - m1 < 4294967295u32; - ensures take m2 = Owned(p); - take n2 = Owned(return); - m1 == m2; - m1 <= n2; +/*@ requires take P = Owned(p); + P < 4294967295u32; + ensures take P_post = Owned(p); + take R = Owned(return); + P == P_post; + P <= R; @*/ /* --END-- */ { diff --git a/src/tutorial.adoc b/src/tutorial.adoc index dc02b08e..fc004151 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -526,6 +526,8 @@ To handle the required resource inference, CN "`eagerly`" decomposes all `+struc We can see this if, for instance, we experimentally change the `+transpose+` example from above to force a type error. Let’s insert an `+/*@ assert(false) @*/+` CN assertion in the middle of the `+transpose+` function, so we can inspect CN’s proof context shown in the error report. (More on CN assertions later.) +// TODO: BCP: Recheck that what we say here matches what it actually looks like + include_example(exercises/transpose.broken.c) The precondition of `+transpose+` asserts ownership of an `+Owned(p)+` resource. The error report now instead lists under "`Available resources`" two resources: @@ -560,9 +562,11 @@ CP: Agreed. For now continuing with arrays, but will return to this later. == Arrays and loops -Another common datatype in C is arrays. Reasoning about memory ownership for arrays is more difficult than for the datatypes we have seen so far: C allows the programmer to access arrays using _computed pointers_, and the size of an array does not need to be known as a constant at compile time. +Another common datatype in C is arrays. Reasoning about memory ownership for arrays is more difficult than for the datatypes we have seen so far, for two reasons: (1) C allows the programmer to access arrays using _computed pointers_, and (2) the size of an array does not need to be known as a constant at compile time. + +To support reasoning about code manipulating arrays and computed pointers, CN has _iterated resources_. For instance, to specify ownership of an `+int+` array with 10 cells starting at pointer `+p+`, CN uses the following iterated resource: -To support reasoning about code manipulating arrays and computed pointers, CN has _iterated resources_. For instance, to specify ownership of an `+int+` array with 10 cells starting at pointer `+p+`, CN uses the iterated resource +// TODO: BCP: Another tricky naming / capitalization puzzle: The index of an "each" has CN type i32, so strictly speaking I believe it should be written with a capital "I". But insisting on this feels like insisting on a distinction that most CN programmers would never even notice, much less be confused by. I think this is another instance of the way C and CN integer types are partly but not completely squished together. [source,c] ---- @@ -599,7 +603,7 @@ comprising three parts: === First array example -Let’s see how this applies to a first example of an array-manipulating function. Function `+read+` takes three arguments: the base pointer `+p+` of an `+int+` array, the length `+n+` of the array, and an index `+i+` into the array; `+read+` then returns the value of the `+i+`-th array cell. +Let’s see how this applies to a simple array-manipulating function. Function `+read+` takes three arguments: the base pointer `+p+` of an `+int+` array, the length `+n+` of the array, and an index `+i+` into the array; `+read+` then returns the value of the `+i+`-th array cell. include_example(exercises/array_load.broken.c) @@ -621,13 +625,13 @@ build/solutions/array_load.broken.c:5:10: error: Missing resource for reading Resource needed: Owned(array_shift(p, (u64)i)) .... -The reason is that when searching for a required resource, such as the `+Owned+` resource for `+p[i]+` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user. +The reason is that, when searching for a required resource, such as the `+Owned+` resource for `+p[i]+` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user. -To make the `+Owned+` resource required for accessing `+p[i]+` available to CN’s resource inference we have to "`extract`" ownership for index `+i+` out of the iterated resource. +To make the `+Owned+` resource required for accessing `+p[i]+` available to CN’s resource inference we have to explicitly "`extract`" ownership for index `+i+` out of the iterated resource. include_example(exercises/array_load.c) -Here the CN comment `+/*@ extract Owned, i; @*/+` is a CN "`ghost statement`"/proof hint that instructs CN to instantiate any available iterated `+Owned+` resource for index `+i+`. In our example this operation splits the iterated resource into two: +Here the CN comment `+/*@ extract Owned, i; @*/+` is a proof hint in the form of a "`ghost statement`" that instructs CN to instantiate any available iterated `+Owned+` resource for index `+i+`. In our example this operation splits the iterated resource into two: [source,c] ---- @@ -652,21 +656,34 @@ each(i32 j; 0i32 <= j && j < n && j != i) After this extraction step, CN can use the (former) extracted resource to justify the access `+p[i]+`. -Following an `+extract+` statement, CN moreover remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function. +Following an `+extract+` statement, CN remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function. -So far the specification only guarantees safe execution but does not specify the behaviour of `+read+`. To address this, let’s return to the iterated resources in the function specification. When we specify `+take a1 = each ...+` here, what is `+a1+`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `+j+` has CN type `+i32+` and the iterated resource is `+Owned+`, the output `+a1+` is a map from `+i32+` indices to `+i32+` values — CN type `+map+`. (If the type of `+j+` was `+i64+` and the resource `+Owned+`, `+a1+` would have type `+map+`.) +So far the specification only guarantees safe execution but does not +specify the behaviour of `+read+`. To address this, let’s return to +the iterated resources in the function specification. When we specify +`+take A = each ...+` here, what is `+A+`? In CN, the output of an +iterated resource is a _map_ from indices to resource outputs. In this +example, where index `+j+` has CN type `+i32+` and the iterated +resource is `+Owned+`, the output `+A+` is a map from `+i32+` +indices to `+i32+` values — CN type `+map+`. If the type of +`+j+` was `+i64+` and the resource `+Owned+`, `+A+` would have +type `+map+`. We can use this to refine our specification with information about the functional behaviour of `+read+`. include_example(exercises/array_load2.c) -We specify that `+read+` does not change the array — the outputs `+a1+` and `+a2+`, taken before and after running the function, are the same — and that the value returned is `+a1[i]+`, `+a1+` at index `+i+`. +We specify that `+read+` does not change the array — the outputs of `+Owned+`, +`+A+` and `+A_post+`, taken before and after running the function, are +the same — and that the value returned is `+A[i]+`. === Exercises *Array read two.* Specify and verify the following function, `+array_read_two+`, which takes the base pointer `+p+` of an `+unsigned int+` array, the array length `+n+`, and two indices `+i+` and `+j+`. Assuming `+i+` and `+j+` are different, it returns the sum of the values at these two indices. +// TODO: BCP: When we get around to renaming files in the examples directory, we should call this one array_swap or something else beginning with "array". + include_example(exercises/add_two_array.c) //// @@ -701,15 +718,17 @@ TODO: BCP: I wrote this, which seemed natural but did not work -- I still don't === Loops -The array examples covered so far manipulate one or two individual cells of an array. Another typical pattern in code working over arrays is to *loop*, uniformly accessing all cells of an array, or sub-ranges of it. +The array examples covered so far manipulate one or two individual cells of an array. Another typical pattern in code working over arrays is to *loop*, uniformly accessing all cells of an array or a sub-range of it. In order to verify code with loops, CN requires the user to supply loop invariants -- CN specifications of all owned resources and the constraints required to verify each iteration of the loop. - Let's take a look at a simple first example. The following function, `+init_array+`, takes the base pointer `+p+` of a `+char+` array and the array length `+n+` and writes `+0+` to each array cell. + +// TODO: BCP: Rename to array_init.c + include_example(exercises/init_array.c) -If, for the moment, we focus just on proving safe execution of `+init_array+`, ignoring its functional behaviour, a specification might look as above: on entry `+init_array+` takes ownership of an iterated `+Owned+` resource -- one `+Owned+` resource for each index `+i+` of type `+u32+` (so necessarily greater or equal to `+0+`) up to `+n+`; on exit `+init_array+` returns the ownership. +If, for the moment, we focus just on proving safe execution of `+init_array+`, ignoring its functional behaviour, a specification might look as above: on entry, `+init_array+` takes ownership of an iterated `+Owned+` resource -- one `+Owned+` resource for each index `+i+` of type `+u32+` (so necessarily greater or equal to `+0+`) up to `+n+`; on exit `+init_array+` returns the ownership. To verify this, we have to supply a loop invariant that specifies all resource ownership and the necessary constraints that hold before and after each iteration of the loop. Loop invariants are specified using the keyword `inv`, followed by CN specifications using the same syntax as in function pre- and postconditions. The variables in scope for loop invariants are all in-scope C variables, as well as CN variables introduced in the function precondition. *In loop invariants, the name of a C variable refers to its current value* (more on this shortly). @@ -720,7 +739,7 @@ TODO: BCP: Concrete syntax: Why not write something like "unchanged {p,n}" or "u The main condition here is unsurprising: we specify ownership of an iterated resource for an array just like in the the pre- and postcondition. -The second thing we need to do, however, is less straightforward. Recall that, as discussed at the start of the tutorial, function arguments in C are mutable, and so CN permits this as well.While in this example it is obvious that `+p+` and `+n+` do not change, CN currently requires the loop invariant to explicitly state this, using special notation `+{p} unchanged+` (and similarly for `+n+`). +The second thing we need to do, however, is less straightforward. Recall that, as discussed at the start of the tutorial, function arguments in C are mutable. Although, in this example, it is obvious that `+p+` and `+n+` do not change, CN currently requires the loop invariant to explicitly state this, using special notation `+{p} unchanged+` (and similarly for `+n+`). **Note.** If we forget to specify `+unchanged+`, this can lead to confusing errors. In this example, for instance, CN would verify the loop against the loop invariant, but would be unable to prove a function postcondition seemingly directly implied by the loop invariant (lacking the information that the postcondition's `+p+` and `+n+` are the same as the loop invariant's). Future CN versions may handle loop invariants differently and treat variables as immutable by default. //// @@ -730,19 +749,23 @@ TODO: BCP: This seems like a good idea! The final piece needed in the verification is an `+extract+` statement, as used in the previous examples: to separate the individual `+Owned+` resource for index `+j+` out of the iterated `+Owned+` resource and make it available to the resource inference, we specify `+extract Owned, j;+`. -With the `+extract+` statements in place, CN accepts the function. +With the `+inv+` and `+extract+` statements in place, CN accepts the function. === Second loop example -However, on closer look, the specification of `+init_array+` is overly strong: it requires an iterated `+Owned+` resource for the array on entry. If, as the name suggests, the purpose of `+init_array+` is to initialise the array, then a precondition asserting only an iterated `+Block+` resource for the array should also be sufficient. The modified specification is then as follows. +The specification of `+init_array+` is overly strong: it requires an iterated `+Owned+` resource for the array on entry. If, as the name suggests, the purpose of `+init_array+` is to initialise the array, then a precondition asserting only an iterated `+Block+` resource for the array should also be sufficient. The modified specification is then as follows. include_example(exercises/init_array2.c) -This specification *should* hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `+Block+` to `+Owned+` "`state`", so that on function return the full array is initialised. (Recall that stores only require `+Block+` ownership of the written memory location, so ownership of not-necessarily-initialised memory.) +This specification *should* hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `+Block+` to `+Owned+` "`state`", so that on function return the full array is initialised. (Recall that stores only require `+Block+` ownership of the written memory location, i.e., ownership of not-necessarily-initialised memory.) -To verify this modified example we again need a loop invariant. This time, the loop invariant is more involved, however: since each iteration of the loop initialises one more array cell, the loop invariant has to do precise book-keeping of the initialisation status of the array. +To verify this modified example we again need a loop Invariant. But +this time the loop invariant is more involved: since each iteration of +the loop initialises one more array cell, the loop invariant has to do +precise book-keeping of the initialisation status of the different +sections of the array. -To do so, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `+Owned+` resource, for all other array indices we have the (unchanged) `+Block+` ownership. +To do this, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `+Owned+` resource, for all other array indices we have the (unchanged) `+Block+` ownership. include_example(solutions/init_array2.c) @@ -754,16 +777,17 @@ Let's go through this line-by-line: - As in the previous example, we assert `+p+` and `+n+` are unchanged. -- Finally, unlike in the previous example, this loop invariant involves `+j+`. We therefore also need to know that `+j+` does not exceed the array length `+n+`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `+j=n+` holds. This, in turn, is needed to show that when the function returns, ownership of the iterated `+Owned+` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource. +- Finally, unlike in the previous example, this loop invariant involves `+j+`. We therefore also need to know that `+j+` does not exceed the array length `+n+`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `+j=n+` holds. This, in turn, is needed to show that, when the function returns, ownership of the iterated `+Owned+` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource. As before, we also have to instruct CN to `+extract+` ownership of individual array cells out of the iterated resources: -- to allow CN to extract the individual `+Block+` to be written we use `+extract Block, j;+`; +- to allow CN to extract the individual `+Block+` to be written, we use `+extract Block, j;+`; - the store returns a matching `+Owned+` resource for index `+j+`; -- finally, we put `+extract Owned, j;+` to allow CN to "`attach`" this resource to the iterated `+Owned+` resource. CN issues a warning, because nothing is, in fact, extracted: we are using `+extract+` only for the "`reverse`" direction. +- finally, we add `+extract Owned, j;+` to allow CN to "`attach`" this resource to the iterated `+Owned+` resource. CN issues a warning, because nothing is, in fact, extracted: we are using `+extract+` only for the "`reverse`" direction. +// TODO: BCP: That last bit is mysterious. === Exercises @@ -771,7 +795,7 @@ As before, we also have to instruct CN to `+extract+` ownership of individual ar include_example(exercises/init_array_rev.c) - +// TODO: BCP: The transition to the next section is awkward. Needs a sentence or two to signal that we're changing topics. Some better visual indication would also be nice. //// ___________________________________________________________________________ @@ -802,17 +826,27 @@ not alias... include_example(exercises/slf_incr2_noalias.c) But what if they do alias? The clunky solution is to write a whole -different version of incr2 with a different embedded specification... +different version of `+incr2+` with a different embedded specification... include_example(exercises/slf_incr2_alias.c) -This is horrible. Much better is to define a predicate to use -in the pre- and postconditions that captures both cases together: +This version does correctly state that the final values of `+p+` and `+q+` are,m respectively, `+3+` and `+1+` more than their original values. But the way we got there -- by duplicating the whole function `+incr2+`, is horrible. + +A better way is to define a *predicate* that captures both the aliased +and the non-aliased cases together and use it in the pre- and +postconditions: include_example(exercises/slf_incr2.c) +// TODO: BCP: "BothOwned" is a pretty awkward name. +// TODO: BCP: We haven't introduced CN records. In particular, C programmers may be surprised that we don't have to pre-declare record types. +// TODO: BCP: the annotation on incr2 needs some unpacking for readers!! +// TODO: BCP: first use of the "split_case" annotation + == Allocating and Deallocating Memory +// TODO: BCP: Again, more text is needed to set up this discussion. + At the moment, CN does not understand the `+malloc+` and `+free+` functions. They are a bit tricky because they rely on a bit of polymorphism and a typecast between `+char*+` -- the result type of @@ -823,7 +857,7 @@ However, for any given type, we can define a type-specific function that allocates heap storage with exactly that type. The implementation of this function cannot be checked by CN, but we can give just the spec, together with a promise to link against an -external C library providing the implementation: +external C library providing a correct (but not verified!) implementation: include_example(exercises/malloc.h) @@ -832,9 +866,11 @@ inside a CN file by marking it with the keyword `+trusted+` at the top of its CN specification.) Similarly: + include_example(exercises/free.h) Now we can write code that allocates and frees memory: + include_example(exercises/slf17_get_and_free.c) We can also define a "safer", ML-style version of `+malloc+` that @@ -858,19 +894,21 @@ pointed to by its argument. include_example(exercises/slf_ref_greater.c) -=== Side Note +=== Side note Here is another syntax for external / unknown functions, together with an example of a loose specification: //// -TODO: BCP: This is a bit random -- it's not clear people need to know about this alternate syntax, and it's awkwardly mixed with a semi-interesting example that's not relevant to this section. +TODO: BCP: This is a bit random -- it's not clear people need to know about this alternate syntax, and it's awkwardly mixed with a semi-interesting example that's not relevant to this section. Also awkwardly placed, right here. //// include_example(exercises/slf18_two_dice.c) == Lists +// TODO: BCP: Better intro needed + Now it's time to look at some more interesting heap structures. To begin with, here is a C definition for linked list cells, together From 61033a1ac7f8e25ffd7973ec83c18a3163b491d3 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Mon, 19 Aug 2024 15:52:59 -0400 Subject: [PATCH 25/25] WIP bunch more renaming and polishing --- src/examples/append.c | 8 +-- src/examples/append2.c | 30 +++++----- src/examples/list_append.h | 2 - src/examples/list_c_types.h | 4 +- src/examples/list_cn_types.h | 4 +- src/examples/list_length.c | 4 +- src/examples/list_rev_alt.c | 4 +- src/examples/mergesort.c | 3 +- src/examples/queue_allocation.h | 8 +-- src/examples/queue_pop.c | 10 ++-- src/examples/queue_push.c | 6 +- src/examples/queue_push_lemma.h | 2 +- src/examples/slf_length_acc.c | 16 +++--- src/examples/slf_sized_stack.c | 99 ++++++++++++++++----------------- src/tutorial.adoc | 62 +++++++++++++-------- 15 files changed, 138 insertions(+), 124 deletions(-) diff --git a/src/examples/append.c b/src/examples/append.c index 0fdb917d..0b398fb9 100644 --- a/src/examples/append.c +++ b/src/examples/append.c @@ -2,10 +2,10 @@ #include "list_append.h" struct sllist* IntList_append(struct sllist* xs, struct sllist* ys) -/*@ requires take L1 = SLList(xs); @*/ -/*@ requires take L2 = SLList(ys); @*/ -/*@ ensures take L3 = SLList(return); @*/ -/*@ ensures L3 == Append(L1, L2); @*/ +/*@ requires take L1 = SLList(xs); + take L2 = SLList(ys); @*/ +/*@ ensures take L3 = SLList(return); + L3 == Append(L1, L2); @*/ { if (xs == 0) { /*@ unfold Append(L1, L2); @*/ diff --git a/src/examples/append2.c b/src/examples/append2.c index a2fd2a48..5ea0ac97 100644 --- a/src/examples/append2.c +++ b/src/examples/append2.c @@ -2,11 +2,11 @@ #include "list_append.h" struct sllist* IntList_copy (struct sllist *xs) -/*@ requires take L1 = SLList(xs); - ensures take L1_ = SLList(xs); - take L2 = SLList(return); - L1 == L1_; - L1 == L2; +/*@ requires take Xs = SLList(xs); + ensures take Xs_post = SLList(xs); + take R = SLList(return); + Xs == Xs_post; + Xs == R; @*/ { if (xs == 0) { @@ -19,24 +19,24 @@ struct sllist* IntList_copy (struct sllist *xs) struct sllist* IntList_append2 (struct sllist *xs, struct sllist *ys) /* --BEGIN-- */ -/*@ requires take L1 = SLList(xs); @*/ -/*@ requires take L2 = SLList(ys); @*/ -/*@ ensures take L1_ = SLList(xs); @*/ -/*@ ensures take L2_ = SLList(ys); @*/ -/*@ ensures take L3 = SLList(return); @*/ -/*@ ensures L3 == Append(L1, L2); @*/ -/*@ ensures L1 == L1_; @*/ -/*@ ensures L2 == L2_; @*/ +/*@ requires take Xs = SLList(xs); @*/ +/*@ requires take Ys = SLList(ys); @*/ +/*@ ensures take Xs_post = SLList(xs); @*/ +/*@ ensures take Ys_post = SLList(ys); @*/ +/*@ ensures take Ret = SLList(return); @*/ +/*@ ensures Ret == Append(Xs, Ys); @*/ +/*@ ensures Xs == Xs_post; @*/ +/*@ ensures Ys == Ys_post; @*/ /* --END-- */ { if (xs == 0) { /* --BEGIN-- */ - /*@ unfold Append(L1, L2); @*/ + /*@ unfold Append(Xs, Ys); @*/ /* --END-- */ return IntList_copy(ys); } else { /* --BEGIN-- */ - /*@ unfold Append(L1, L2); @*/ + /*@ unfold Append(Xs, Ys); @*/ /* --END-- */ struct sllist *new_tail = IntList_append2(xs->tail, ys); return slcons(xs->head, new_tail); diff --git a/src/examples/list_append.h b/src/examples/list_append.h index 38cc8a48..2c95a823 100644 --- a/src/examples/list_append.h +++ b/src/examples/list_append.h @@ -1,5 +1,3 @@ -// append.h - /*@ function [rec] (datatype List) Append(datatype List L1, datatype List L2) { match L1 { diff --git a/src/examples/list_c_types.h b/src/examples/list_c_types.h index 68d326aa..7caa03b3 100644 --- a/src/examples/list_c_types.h +++ b/src/examples/list_c_types.h @@ -6,12 +6,12 @@ struct sllist { extern struct sllist *malloc__sllist(); /*@ spec malloc__sllist(); requires true; - ensures take u = Block(return); + ensures take R = Block(return); @*/ extern void free__sllist (struct sllist *p); /*@ spec free__sllist(pointer p); - requires take u = Block(p); + requires take P = Block(p); ensures true; @*/ diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h index 26020bf4..14ef5da2 100644 --- a/src/examples/list_cn_types.h +++ b/src/examples/list_cn_types.h @@ -9,8 +9,8 @@ predicate (datatype List) SLList(pointer p) { return Nil{}; } else { take H = Owned(p); - take Tl = SLList(H.tail); - return (Cons { Head: H.head, Tail: Tl }); + take T = SLList(H.tail); + return (Cons { Head: H.head, Tail: T }); } } @*/ diff --git a/src/examples/list_length.c b/src/examples/list_length.c index 5167136b..832eb7ef 100644 --- a/src/examples/list_length.c +++ b/src/examples/list_length.c @@ -18,8 +18,8 @@ function [rec] (u32) Length(datatype List L) { unsigned int length (struct sllist *l) /* --BEGIN-- */ /*@ requires take L = SLList(l); - ensures take L_ = SLList(l); - L == L_; + ensures take L_post = SLList(l); + L == L_post; return == Length(L); @*/ /* --END-- */ diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c index 6e0c1fd3..6d3ec343 100644 --- a/src/examples/list_rev_alt.c +++ b/src/examples/list_rev_alt.c @@ -5,8 +5,8 @@ struct sllist* rev_loop(struct sllist *l) /*@ requires take L = SLList(l); - ensures take L_ = SLList(return); - L_ == RevList(L); + ensures take L_post = SLList(return); + L_post == RevList(L); @*/ { struct sllist *last = 0; diff --git a/src/examples/mergesort.c b/src/examples/mergesort.c index c2508535..5076166d 100644 --- a/src/examples/mergesort.c +++ b/src/examples/mergesort.c @@ -1,7 +1,8 @@ #include "list.h" /*@ -function [rec] ({datatype List fst, datatype List snd}) split(datatype List xs) +function [rec] ({datatype List fst, datatype List snd}) + split (datatype List xs) { match xs { Nil {} => { diff --git a/src/examples/queue_allocation.h b/src/examples/queue_allocation.h index 6415601f..430c144a 100644 --- a/src/examples/queue_allocation.h +++ b/src/examples/queue_allocation.h @@ -1,23 +1,23 @@ extern struct int_queue *mallocIntQueue(); /*@ spec mallocIntQueue(); requires true; - ensures take u = Block(return); + ensures take R = Block(return); @*/ extern void freeIntQueue (struct int_queue *p); /*@ spec freeIntQueue(pointer p); - requires take u = Block(p); + requires take P = Block(p); ensures true; @*/ extern struct int_queueCell *mallocIntQueueCell(); /*@ spec mallocIntQueueCell(); requires true; - ensures take u = Block(return); + ensures take R = Block(return); @*/ extern void freeIntQueueCell (struct int_queueCell *p); /*@ spec freeIntQueueCell(pointer p); - requires take u = Block(p); + requires take P = Block(p); ensures true; @*/ diff --git a/src/examples/queue_pop.c b/src/examples/queue_pop.c index 57798da2..d7f989a8 100644 --- a/src/examples/queue_pop.c +++ b/src/examples/queue_pop.c @@ -2,11 +2,11 @@ #include "queue_pop_lemma.h" int IntQueue_pop (struct int_queue *q) -/*@ requires take before = IntQueuePtr(q); - before != Nil{}; - ensures take after = IntQueuePtr(q); - after == Tl(before); - return == Hd(before); +/*@ requires take Q = IntQueuePtr(q); + Q != Nil{}; + ensures take Q_post = IntQueuePtr(q); + Q_post == Tl(Q); + return == Hd(Q); @*/ { /*@ split_case is_null(q->front); @*/ diff --git a/src/examples/queue_push.c b/src/examples/queue_push.c index 121e3cf8..ede31857 100644 --- a/src/examples/queue_push.c +++ b/src/examples/queue_push.c @@ -2,9 +2,9 @@ #include "queue_push_lemma.h" void IntQueue_push (int x, struct int_queue *q) -/*@ requires take before = IntQueuePtr(q); - ensures take after = IntQueuePtr(q); - after == Snoc (before, x); +/*@ requires take Q = IntQueuePtr(q); + ensures take Q_post = IntQueuePtr(q); + Q_post == Snoc (Q, x); @*/ { struct int_queueCell *c = mallocIntQueueCell(); diff --git a/src/examples/queue_push_lemma.h b/src/examples/queue_push_lemma.h index 2220caf1..740d98c0 100644 --- a/src/examples/queue_push_lemma.h +++ b/src/examples/queue_push_lemma.h @@ -4,6 +4,6 @@ lemma push_lemma (pointer front, pointer p) take Q = IntQueueAux(front, p); take P = Owned(p); ensures - take NewQ = IntQueueAux(front, P.next); + take Q_post = IntQueueAux(front, P.next); NewQ == Snoc(Q, P.first); @*/ diff --git a/src/examples/slf_length_acc.c b/src/examples/slf_length_acc.c index 354d20f4..27e919bd 100644 --- a/src/examples/slf_length_acc.c +++ b/src/examples/slf_length_acc.c @@ -18,10 +18,10 @@ function [rec] (u32) length(datatype List xs) { void IntList_length_acc_aux (struct sllist *xs, unsigned int *p) /*@ requires take L1 = SLList(xs); take P = Owned(p); - ensures take L1_ = SLList(xs); - take N = Owned(p); - L1 == L1_; - N == P + length(L1); + ensures take L1_post = SLList(xs); + take P_post = Owned(p); + L1 == L1_post; + P_post == P + length(L1); @*/ { /*@ unfold length(L1); @*/ @@ -33,10 +33,10 @@ void IntList_length_acc_aux (struct sllist *xs, unsigned int *p) } unsigned int IntList_length_acc (struct sllist *xs) -/*@ requires take L1 = SLList(xs); - ensures take L1_ = SLList(xs); - L1 == L1_; - return == length(L1); +/*@ requires take Xs = SLList(xs); + ensures take Xs_post = SLList(xs); + Xs == Xs_post; + return == length(Xs); @*/ { unsigned int *p = refUnsignedInt(0); diff --git a/src/examples/slf_sized_stack.c b/src/examples/slf_sized_stack.c index 4ac9d769..6958ca70 100644 --- a/src/examples/slf_sized_stack.c +++ b/src/examples/slf_sized_stack.c @@ -7,14 +7,13 @@ struct sized_stack { }; /*@ -type_synonym sizeAndData = {u32 s, datatype List d} +type_synonym SizedStack = {u32 Size, datatype List Data} -predicate (sizeAndData) SizedStack(pointer p) { - take S = Owned(p); - let s = S.size; - take d = SLList(S.data); - assert(s == Length(d)); - return { s: s, d: d }; +predicate (SizedStack) SizedStack (pointer p) { + take P = Owned(p); + take D = SLList(P.data); + assert(P.size == Length(D)); + return { Size: P.size, Data: D }; } @*/ @@ -22,95 +21,95 @@ extern struct sized_stack *malloc__sized_stack (); /*@ spec malloc__sized_stack(); requires true; - ensures take u = Block(return); + ensures take R = Block(return); @*/ -extern void *free__sized_stack (struct sized_stack *p); +extern void *free__sized_stack (struct sized_stack *s); /*@ -spec free__sized_stack(pointer p); - requires take u = Block(p); +spec free__sized_stack(pointer s); + requires take R = Block(s); ensures true; @*/ struct sized_stack* create() -/*@ ensures take S = SizedStack(return); - S.s == 0u32; +/*@ ensures take R = SizedStack(return); + R.Size == 0u32; @*/ { - struct sized_stack *p = malloc__sized_stack(); - p->size = 0; - p->data = 0; + struct sized_stack *s = malloc__sized_stack(); + s->size = 0; + s->data = 0; /*@ unfold Length(Nil {}); @*/ - return p; + return s; } -unsigned int sizeOf (struct sized_stack *p) +unsigned int sizeOf (struct sized_stack *s) /* FILL IN HERE */ /* ---BEGIN--- */ -/*@ requires take S = SizedStack(p); - ensures take S_ = SizedStack(p); - S_ == S; - return == S.s; +/*@ requires take S = SizedStack(s); + ensures take S_post = SizedStack(s); + S_post == S; + return == S.Size; @*/ /* ---END--- */ { - return p->size; + return s->size; } -void push (struct sized_stack *p, int x) +void push (struct sized_stack *s, int x) /* FILL IN HERE */ /* ---BEGIN--- */ -/*@ requires take S = SizedStack(p); - ensures take S_ = SizedStack(p); - S_.d == Cons {Head:x, Tail:S.d}; +/*@ requires take S = SizedStack(s); + ensures take S_post = SizedStack(s); + S_post.Data == Cons {Head:x, Tail:S.Data}; @*/ /* ---END--- */ { - struct sllist *data = slcons(x, p->data); - p->size++; - p->data = data; + struct sllist *data = slcons(x, s->data); + s->size++; + s->data = data; /* ---BEGIN--- */ - /*@ unfold Length (Cons {Head: x, Tail: S.d}); @*/ + /*@ unfold Length (Cons {Head: x, Tail: S.Data}); @*/ /* ---END--- */ } -int pop (struct sized_stack *p) +int pop (struct sized_stack *s) /* FILL IN HERE */ /* ---BEGIN--- */ -/*@ requires take S = SizedStack(p); - S.s > 0u32; - ensures take S_ = SizedStack(p); - S_.d == Tl(S.d); +/*@ requires take S = SizedStack(s); + S.Size > 0u32; + ensures take S_post = SizedStack(s); + S_post.Data == Tl(S.Data); @*/ /* ---END--- */ { - struct sllist *data = p->data; + struct sllist *data = s->data; if (data != 0) { int head = data->head; struct sllist *tail = data->tail; free__sllist(data); - p->data = tail; - p->size--; + s->data = tail; + s->size--; /* ---BEGIN--- */ - /*@ unfold Length(S.d); @*/ + /*@ unfold Length(S.Data); @*/ /* ---END--- */ return head; } return 42; } -int top (struct sized_stack *p) -/*@ requires take S = SizedStack(p); - S.s > 0u32; - ensures take S_ = SizedStack(p); - S_ == S; - return == Hd(S.d); +int top (struct sized_stack *s) +/*@ requires take S = SizedStack(s); + S.Size > 0u32; + ensures take S_post = SizedStack(s); + S_post == S; + return == Hd(S.Data); @*/ { - /*@ unfold Length(S.d); @*/ - // from S.s > 0u32 it follows that the 'else' branch is impossible - if (p->data != 0) { - return (p->data)->head; + /*@ unfold Length(S.Data); @*/ + // from S.Size > 0u32 it follows that the 'else' branch is impossible + if (s->data != 0) { + return (s->data)->head; } else { // provably dead code diff --git a/src/tutorial.adoc b/src/tutorial.adoc index fc004151..f2996ed6 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -914,23 +914,25 @@ Now it's time to look at some more interesting heap structures. To begin with, here is a C definition for linked list cells, together with allocation and deallocation functions: +// TODO: BCP: Here and in several other places, we should use the "take _ = ..." syntax when the owned value is not used. And we should explain it the first time we use it. + include_example(exercises/list_c_types.h) // TODO: BCP: Per discussion with Christopher, Cassia, and Daniel, the word "predicate" is quite confusing for newcomers (in logic, predicates do not return things!). A more neutral word might make for significantly easier onboarding. To write specifications for C functions that manipulate lists, we need -to define a CN "predicate" that describes *mathematical* list -structures, as one would do in ML, Haskell, or Coq. (We call them -"sequences" here to avoid overloading the word "list".) +to define a CN "predicate" that describes specification-level list +structures, as one would do in ML, Haskell, or Coq. We use the +datatype `+List+` for CN-level lists. -Intuitively, the `+SLList+` predicate walks over a pointer structure -in the C heap and extracts an `+Owned+` version of the mathematical -list that it represents. +Intuitively, the `+SLList+` predicate walks over a singly-linked +pointer structure in the C heap and extracts an `+Owned+` version of +the CN-level list that it represents. include_example(exercises/list_cn_types.h) -We can also write specification-level "functions" by ordinary -functional programming (in slightly strange, unholy-union-of-C-and-ML +We can also write *functions* on CN-level lists by ordinary functional +programming (in a slightly strange, unholy-union-of-C-and-Rust syntax): include_example(exercises/list_hdtl.h) @@ -940,9 +942,9 @@ empty list and the cons of a number and a list. include_example(exercises/list_constructors.h) -Finally, we can collect all this stuff into a single header file and +Finally, we can collect all this stuff into a single header file. (We add the usual C `+#ifndef+` gorp to avoid complaints from the compiler -if it happens to get included twice from the same source file later. +if it happens to get included twice from the same source file later.) include_example(exercises/list.h) @@ -986,6 +988,10 @@ avoids allocating any new list cells in the splitting step by taking alternate cells from the original list and linking them together into two new lists of roughly equal lengths. +// TODO: BCP: We've heard from more than one reader that this example is particularly hard to digest without some additional help + +// TODO: BCP: Nit: Merge multiple requires and ensures clauses into one + include_example(exercises/mergesort.c) === Exercises @@ -1017,7 +1023,7 @@ include_example(exercises/slf_length_acc.c) == Working with External Lemmas -**TODO**: This section should also show what the proof of the lemmas +// TODO: BCP: This section should also show what the proof of the lemmas looks like on the Coq side! // TODO: BCP: This needs to be filled in urgently!! @@ -1061,6 +1067,10 @@ include_example(exercises/list_rev_alt.c) **Sized stacks:** Fill in annotations where requested: +// TODO: BCP: type_synonym has not been introduced yet + +// TODO: Mention the pun here: SizedStack is both a predicate and the type that that predicate returns. There's no ambiguity because the latter takes no argument. + include_example(exercises/slf_sized_stack.c) // ====================================================================== @@ -1077,6 +1087,8 @@ include_example(exercises/slf_sized_stack.c) == CN Style +// TODO: BCP: If we are agreed on the naming conventions suggested in /NAMING-CONVENTIONS.md, we could move that material here. + This section gathers some advice on stylistic conventions and best practices in CN. @@ -1149,12 +1161,13 @@ we have to rename other things above for consistency... Given a pointer to an `+int_queue+` struct, this predicate grabs ownership of the struct, asserts that the `+front+` and `+back+` pointers must either both be NULL or both be non-NULL, and then hands off to an -auxiliary predicate `+IntQueueFB+`. (Conceptually, `+IntQueueFB+` is -part of `+IntQueuePTR+`, but CN currently allows conditional -expressions only at the beginning of predicate definitions, not after -a `+take+`.) +auxiliary predicate `+IntQueueFB+`. -`+IntQueueFB+` is where the interesting part starts: +`+IntQueueFB+` is where the interesting part starts. (Conceptually, +`+IntQueueFB+` is part of `+IntQueuePTR+`, but CN currently allows +conditional expressions only at the beginning of predicate +definitions, not after a `+take+`, so we need to make a separate +auxiliary predicate.) include_example(exercises/queue_cn_types_2.h) @@ -1174,7 +1187,7 @@ the second to last cell (or the `+front+` pointer, if there is only one cell in the list), so we need to be careful not to `+take+` this cell twice. -Accordingly, we begin by `+take+`ing the tail cell and passing it +Accordingly, we begin by `+take+`-ing the tail cell and passing it separately to the `+IntQueueAux+` predicate, which has the job of walking down the cells from the front and gathering all the rest of them into a sequence. We take the result from `+IntQueueAux+` and @@ -1232,7 +1245,7 @@ include_example(exercises/queue_push_orig.broken.c) *Exercise*: Before reading on, see if you can write down a reasonable top-level specification for this operation. -(One thing you might find odd about this code is that there's a +One thing you might find odd about this code is that there's a `+return+` statement at the end of each branch of the conditional, rather than a single `+return+` at the bottom. The reason for this is that, when CN analyzes a function body containing a conditional, it @@ -1241,7 +1254,7 @@ the branches. Then, if verification encounters an error related to this code -- e.g., "you didn't establish the `+ensures+` conditions at the point of returning -- the error message will be confusing because it will not be clear which branch of the conditional it is associated -with.) +with. Now, here is the annotated version of the `+push+` operation. @@ -1256,6 +1269,8 @@ elements, so we should expect that validating `+push+` is going to require some reasoning about this sequence. Here, in fact, is the lemma we need. +// TODO: BCP: Not sure I can explain what "pointer" means here, or why we don't need to declare more specific types for these arguments to the lemma. + include_example(exercises/queue_push_lemma.h) This says, in effect, that we have two choices for how to read out the @@ -1370,8 +1385,7 @@ telltale clues in the error report that suggest what the problem was? not `+f == b+` to find out whether we have reached the last element of the queue. Another way to get the same information would be to test whether `+f->next == 0+`. Can you verify this version? - -Note: I (BCP) have not worked out the details, so am not sure how hard +*Note*: I (BCP) have not worked out the details, so am not sure how hard this is (or if it is even not possible, though I'd be surprised). Please let me know if you get it working! @@ -1387,11 +1401,13 @@ Can you generalize the `+snoc_facts+` lemma to handle both cases? You can get past the dereference with a `+split_case+` but formulating the lemma before the `+return+` will be a bit more complicated. -Note: Again, this has not been shown to be possible, but Dhruv +*Note*: Again, this has not been shown to be possible, but Dhruv believes it should be! === Doubly Linked Lists +// TODO: BCP: The rest of the tutorial (from here to the end) needs to be checked for consistency of naming and capitalization conventions. + A doubly linked list is a linked list where each node has a pointer to both the next node and the previous node. This allows for O(1) operations for adding or removing nodes anywhere in the list. Here is @@ -1528,7 +1544,7 @@ Now, let's look at the annotations in the function body. These are similar to in // ====================================================================== -*Exercise*: There are many other functions that one might want to implement for a doubly linked list. For example, one might want to implement a function that appends one list to another, or a function that reverses a list. Try implementing these functions and writing their specifications. +*Exercise*: There are many other functions that one might want to implement for a doubly linked list. For example, one might want to implement a function that appends one list to another, or a function that reverses a list. Try implementing a few of these functions and writing their specifications. === The Runway