Commit f81e3fce authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Make RefinedC more user-friendly with several changes.

The first change concern the syntax of constraints in annotations. The following is now allowed:
- [own l : ty] (previously written [l @ &own<ty>]),
- [shr l : ty] (previously written [l @ &shr<ty>]),
- [frac β l : ty] (previously written [l @ &frac<β, ty>]).
- The old notations have been removed.

The second change is some renaming around singleton types and layouts:
- [singleton_val] is now called [value],
- [singleton_place] is now called [place],
- [LPtr] is now called [void_ptr] and is accessed with notation [void*],
- [LVoid] is now called [void_layout].
- The front end now accepts `void*` as an identifier.

The last change introduces a new Coq scope called [printing_sugar] that is only opened at the beginning of proofs in generated proof files. It defines printing notations intended at making the output of the tool closer to the syntax of the front end. In particular it defines the following notations:
- [own l : ty], [shr l : ty], [frac {β} l : ty],
- [uninit<ly>], [value<ly, v>], [place<l>], [&own<ty>], ...
- For each user-defined types a similar printing sugar is defined automatically.
parent 378b83c1
Pipeline #40613 passed with stage
in 32 minutes and 47 seconds
......@@ -377,7 +377,7 @@ syntactic constructs will be presented here along with their semantics.
Our syntax makes use of the following regular expressions.
```
<ident> ::= Regexp([A-Za-z_][A-Za-z_0-9]+)
<ident> ::= Regexp([A-Za-z_][A-Za-z_0-9]+) | "void*"
<integer> ::= Regexp([0-9]+)
```
They range over general-purpose identifiers (for `<ident>`), and over positive
......@@ -435,7 +435,9 @@ in annotations. They are defined as follows.
<type_expr> ::=
| <ident (as type name)> {"<" ">"}?
| <ident (as type name)> "<" <type_expr_arg> {"," <type_expr_arg>}* ">"
| <ptr_type>
| "&own<" <type_expr> ">"
| "&shr<" <type_expr> ">"
| "&frac<" <coq_expr (as fraction)> "," <type_expr> ">"
| <coq_expr (as Coq value)> "@" <type_expr>
| "∃" <ident (as variable name)> {":" <coq_expr (as Coq type)>}? "." <type_expr>
| <type_expr> "&" <constr>
......@@ -444,6 +446,12 @@ in annotations. They are defined as follows.
| "(" <tupe_expr> ")"
```
Pointer types are built-in type constructors related to ownership. There are
three forms of pointer types:
- owned pointers (of the form `&own<T>`),
- shared pointers (of the form `&shr<T>`),
- and fractional pointer (of the form `&frac<q, T>`).
### Type constuctor application
There are roughly eight different type expression constructors. The first one,
......@@ -464,21 +472,6 @@ expressions, built using a λ-abstraction.
**Remark:** there is some special support for certain type constructors. There
is some discussion on that in a further section.
### Pointer types
The third type constructor for type expressions contains a pointer type.
```
<ptr_type> ::=
| "&own<" <type_expr> ">"
| "&shr<" <type_expr> ">"
| "&frac<" <coq_expr (as fraction)> "," <type_expr> ">"
```
Pointer types are built-in type constructors related to ownership (this is why
they are treated specially). There are three forms of pointer types:
- owned pointers (of the form `&own<T>`),
- shared pointers (of the form `&shr<T>`),
- and fractional pointer (of the form `&frac<q, T>`).
### Refinements
The fourth type expression constructor, of the form `v @ T`, is central to the
......@@ -519,14 +512,21 @@ The syntax of constraints is defined below.
| <iris_term (as Iris proposition)>
| <pure_term (as Coq proposition)>
| "∃" <ident (as variable name)> {":" <coq_expr (as Coq type)>}? "." <constr>
| <ident (as variable name)> "@" <ptr_type>
| "own" <ident (as variable name)> ":" <type_expr>
| "shr" <ident (as variable name)> ":" <type_expr>
| "frac" <coq_expr (as ownstate)> <ident (as variable name)> ":" <type_expr>
| <ident (as variable name)> ":" <type_expr>
| "global" <ident (as C global variable name> ":" <type_expr>
```
A constraint can be formed using either:
- a (quoted) Iris proposition,
- a (quoted) Coq proposition,
- an existential quantifier,
- a pointer type ownership statement,
- a pointer ownership statement (translated to a location type assignment),
- a location type assignment for an owned location,
- a location type assignment for a shared location,
- a location type assignment for a frac location,
- a value type assignment,
- a typing constraint for a global variable.
**Remark:** a constraint of the form `{...}` is a short-hand for `[⌜...⌝]`, in
......@@ -546,7 +546,6 @@ There is some special support for predefined type constructors:
necessary. For example, when recursive occurences of a type appear undear
an `array` type.
# Annotations using macros
The macro `rc_unfold_int(i)` can be used to extend the context with the
......
......@@ -9,14 +9,14 @@ typedef bool (*comp_fn)(void *, void *);
[[rc::parameters("R : {Z → Z → Prop}", "ls : {list Z}", "x : Z", "p : loc", "ty : {Z → type}", "px : loc")]]
[[rc::args("function_ptr<{fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝}>",
"p @ &own<array<LPtr, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<i32>", "px @ &own<{ty x}>")]]
"p @ &own<array<void*, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<i32>", "px @ &own<{ty x}>")]]
[[rc::requires("{StronglySorted R ls}", "{Transitive R}")]]
[[rc::exists("n : nat")]]
[[rc::returns("n @ int<i32>")]]
[[rc::ensures("{∀ i y, (i < n)%nat → ls !! i = Some y → R y x}",
"{∀ i y, (n ≤ i)%nat → ls !! i = Some y → ¬ R y x}")]]
[[rc::ensures("p @ &own<array<LPtr, {(fun x => &own (ty x) : type) <$> ls}>>")]]
[[rc::ensures("px @ &own<{ty x}>")]]
[[rc::ensures("own p : array<void*, {(fun x => &own (ty x) : type) <$> ls}>")]]
[[rc::ensures("own px : ty<x>")]]
[[rc::tactics("all: try by [revert select (∀ i j, _ → _ → ¬ R _ _); apply; [| done];solve_goal].")]]
[[rc::tactics("all: try by apply: (binary_search_cond_1 y); solve_goal.")]]
[[rc::tactics("all: try by apply: (binary_search_cond_2 y); solve_goal.")]]
......@@ -42,7 +42,7 @@ int binary_search(comp_fn comp, void **xs, int n, void *x) {
[[rc::args("px @ &own<x @ int<size_t>>", "py @ &own<y @ int<size_t>>")]]
[[rc::exists("b : bool")]]
[[rc::returns("b @ boolean<bool_it>")]]
[[rc::ensures("px @ &own<x @ int<size_t>>", "py @ &own<y @ int<size_t>>", "{b ↔ Z.le x y}")]]
[[rc::ensures("own px : x @ int<size_t>", "own py : y @ int<size_t>", "{b ↔ Z.le x y}")]]
bool compare_int(void *x, void *y) {
size_t *xi = x, *yi = y;
return *xi <= *yi;
......
......@@ -13,7 +13,7 @@ btree_t* new_btree(){
[[rc::parameters("p : loc")]]
[[rc::args("p @ &own<btree_t>")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::ensures("p @ &own<null>")]]
[[rc::ensures("own p : null")]]
[[rc::trust_me]] // FIXME
void free_btree_nodes(btree_t* t){
if(*t == NULL) return;
......@@ -43,8 +43,8 @@ void free_btree(btree_t* t){
[[rc::ensures("{s ≤ n}")]]
[[rc::ensures("{k ∈ l → l !! s = Some k}")]]
[[rc::ensures("{¬ k ∈ l → StronglySorted (<) (take s l ++ k :: drop s l)}")]]
[[rc::ensures("p @ &own<array<{it_layout i32}, {(l `at_type` int i32) ++ "
"replicate (sz - n)%nat (uninit i32 : type)}>>")]]
[[rc::ensures("own p : array<{it_layout i32}, {(l `at_type` int i32) ++ "
"replicate (sz - n)%nat (uninit i32 : type)}>")]]
[[rc::tactics("destruct (decide (i = s)); by naive_solver lia.")]]
[[rc::tactics(// FIXME
"move: (elem_of_list_lookup_1 _ _ H14) => [i Hi]. "
......
......@@ -41,10 +41,10 @@ btree {
[[rc::field("array_p<i32, {ks `at_type` int i32}, {(ORDER-1-n)%nat}>")]]
int keys[ORDER - 1];
[[rc::field("array_p<LPtr, {(λ ty, (&own ty : type)) <$> vs}, {(ORDER-1-n)%nat}>")]]
[[rc::field("array_p<void*, {(λ ty, (&own ty : type)) <$> vs}, {(ORDER-1-n)%nat}>")]]
void* vals[ORDER - 1];
[[rc::field("guarded<array_p<LPtr, {cs `at_type` !{btree_t<>}}, {(ORDER-1-n)%nat}>>")]]
[[rc::field("guarded<array_p<void*, {cs `at_type` !{btree_t<>}}, {(ORDER-1-n)%nat}>>")]]
struct btree* children[ORDER];
[[rc::field("{br_height r} @ int<i32>")]]
......@@ -65,7 +65,7 @@ void free_btree(btree_t* t);
[[rc::parameters("p : loc", "h : nat", "m : {gmap Z type}", "k : Z")]]
[[rc::args("p @ &own<{BRroot h m} @ btree_t>", "k @ int<i32>")]]
[[rc::returns("{bool_decide (m !! k ≠ None)} @ boolean<bool_it>")]]
[[rc::ensures("p @ &own<{BRroot h m} @ btree_t>")]]
[[rc::ensures("own p : {BRroot h m} @ btree_t")]]
bool btree_member(btree_t* t, int k);
// Find the value associated to the key k in the B-tree t. If the key k is not
......@@ -74,7 +74,7 @@ bool btree_member(btree_t* t, int k);
[[rc::args("p @ &own<{BRroot h m} @ btree_t>", "k @ int<i32>")]]
[[rc::exists("v : loc")]]
[[rc::returns("{m !! k} @ optionalO<λ ty. v @ &own<ty>>")]]
[[rc::ensures("p @ &own<{BRroot h (make_sp v k m)} @ btree_t>")]]
[[rc::ensures("own p : {BRroot h (make_sp v k m)} @ btree_t")]]
void** btree_find(btree_t* t, int k);
// Insert the key k with value v in the B-tree t. If the key is already mapped
......@@ -85,5 +85,5 @@ void** btree_find(btree_t* t, int k);
[[rc::args("k @ int<i32>", "v @ &own<ty>")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::exists("new_h : nat")]]
[[rc::ensures("p @ &own<{BRroot new_h (<[k := ty]> m)} @ btree_t>")]]
[[rc::ensures("own p : {BRroot new_h (<[k := ty]> m)} @ btree_t")]]
void btree_insert(btree_t* t, int k, void* v);
......@@ -16,13 +16,13 @@ struct latch {
[[rc::parameters("p : loc", "beta : own_state", "P : {iProp Σ}")]]
[[rc::args("p @ &frac<beta, latch<P>>")]]
[[rc::ensures("p @ &frac<beta, latch<P>>", "[P]")]]
[[rc::ensures("frac beta p : latch<P>", "[P]")]]
void latch_wait(struct latch* latch);
[[rc::parameters("p : loc", "beta : own_state", "P : {iProp Σ}")]]
[[rc::args("p @ &frac<beta, latch<P>>")]]
[[rc::requires("[□ P]")]]
[[rc::ensures("p @ &frac<beta, latch<P>>")]]
[[rc::ensures("frac beta p : latch<P>")]]
void latch_release(struct latch* latch);
#endif
......@@ -16,20 +16,20 @@ struct spinlock {
[[rc::parameters("p : loc")]]
[[rc::args("p @ &own<uninit<struct_spinlock>>")]]
[[rc::exists("gamma : lock_id")]]
[[rc::ensures("p @ &own<spinlock<gamma>>")]]
[[rc::ensures("own p : spinlock<gamma>")]]
void sl_init(struct spinlock* lock);
[[rc::parameters("p : loc", "gamma : lock_id", "beta : own_state")]]
[[rc::args("p @ &frac<beta, spinlock<gamma>>")]]
[[rc::ensures("p @ &frac<beta, spinlock<gamma>>", "[spinlock_token gamma []]")]]
[[rc::ensures("frac beta p : spinlock<gamma>", "[spinlock_token gamma []]")]]
void sl_lock(struct spinlock* lock);
[[rc::parameters("p : loc", "gamma : lock_id", "beta : own_state")]]
[[rc::args("p @ &frac<beta, spinlock<gamma>>")]]
[[rc::requires("[spinlock_token gamma []]")]]
[[rc::ensures("p @ &frac<beta, spinlock<gamma>>")]]
[[rc::ensures("frac beta p : spinlock<gamma>")]]
[[rc::annot_args("0 : 1 LockA")]]
void sl_unlock(struct spinlock* lock);
......
......@@ -25,7 +25,7 @@ size_t min_ptr_val(int *p1, int *p2){
[[rc::parameters("p : loc")]]
[[rc::args("p @ &own<int<i32>>")]]
[[rc::returns("{(None, p.2)} @ &own<singleton_place<{(None, p.2)}>>")]]
[[rc::returns("{(None, p.2)} @ &own<place<{(None, p.2)}>>")]]
int* roundtrip1(int* p){
size_t i = (size_t) p;
void *q = (void*) i;
......@@ -41,21 +41,22 @@ int* roundtrip2(int* p){
return rc_copy_alloc_id(q, p);
}
[[rc::parameters("p : loc", "n : Z")]]
[[rc::args("p @ &own<n @ int<i32>>")]]
[[rc::parameters("l : loc", "n : Z")]]
[[rc::args("l @ &own<n @ int<i32>>")]]
[[rc::returns("n @ int<i32>")]]
[[rc::ensures("p @ &own<n @ int<i32>>")]]
[[rc::ensures("own l : n @ int<i32>")]]
int roundtrip_and_read(int* p){
size_t i = (size_t) p;
int *q = (int*) i;
int *r = rc_copy_alloc_id(q, p);
return *r;
q = rc_copy_alloc_id(q, p);
int r = *q;
return r;
}
[[rc::parameters("p : loc", "n : Z")]]
[[rc::args("p @ &own<n @ int<i32>>")]]
[[rc::returns("n @ int<i32>")]]
[[rc::ensures("p @ &own<n @ int<i32>>")]]
[[rc::ensures("own p : n @ int<i32>")]]
int roundtrip_and_read2(int* p){
uintptr_t i = (uintptr_t) p;
int *q = rc_copy_alloc_id((int*) i, p);
......@@ -65,7 +66,7 @@ int roundtrip_and_read2(int* p){
[[rc::parameters("p : loc", "n : Z")]]
[[rc::args("p @ &own<n @ int<i32>>")]]
[[rc::returns("n @ int<i32>")]]
[[rc::ensures("p @ &own<n @ int<i32>>")]]
[[rc::ensures("own p : n @ int<i32>")]]
int roundtrip_and_read3(int* p){
size_t i = (size_t) p;
int *q = (int*) i;
......
......@@ -28,7 +28,7 @@ struct [[rc::refined_by("n1 : Z", "n2 : Z", "n3 : Z")]]
[[rc::parameters("p : loc")]]
[[rc::args("p @ &own<uninit<struct_lock_test>>")]]
[[rc::ensures("p @ &own<{0, 0, 10} @ lock_test>")]]
[[rc::ensures("own p : {0, 0, 10} @ lock_test")]]
void init(struct lock_test* t) {
t->outside = 0;
t->locked_int = 0;
......@@ -39,7 +39,7 @@ void init(struct lock_test* t) {
[[rc::parameters("p : loc", "n : Z", "n1 : Z", "n2 : Z", "n3 : Z")]]
[[rc::args("p @ &own<{n1, n2, n3} @ lock_test>", "n @ int<size_t>")]]
[[rc::ensures("p @ &own<{n, n2, n3} @ lock_test>")]]
[[rc::ensures("own p : {n, n2, n3} @ lock_test")]]
void write_outside(struct lock_test* t, size_t n) {
t->outside = n;
}
......@@ -47,14 +47,14 @@ void write_outside(struct lock_test* t, size_t n) {
[[rc::parameters("p : loc", "n1 : Z", "n2 : Z", "n3 : Z")]]
[[rc::args("p @ &own<{n1, n2, n3} @ lock_test>")]]
[[rc::returns("n1 @ int<size_t>")]]
[[rc::ensures("p @ &own<{n1, n2, n3} @ lock_test>")]]
[[rc::ensures("own p : {n1, n2, n3} @ lock_test")]]
size_t read_outside(struct lock_test* t) {
return t->outside;
}
[[rc::parameters("p : loc", "n : Z", "q : own_state", "n1 : Z", "n2 : Z", "n3 : Z")]]
[[rc::args("p @ &frac<q, {n1, n2, n3} @ lock_test>", "n @ int<size_t>")]]
[[rc::ensures("p @ &frac<q, {n1, n, n3} @ lock_test>")]]
[[rc::ensures("frac q p : {n1, n, n3} @ lock_test")]]
void write_locked(struct lock_test* t, size_t n) {
sl_lock(&t->lock);
......@@ -68,7 +68,7 @@ void write_locked(struct lock_test* t, size_t n) {
[[rc::args("p @ &frac<q, {n1, n2, n3} @ lock_test>")]]
[[rc::exists("n : Z")]]
[[rc::returns("n @ int<size_t>")]]
[[rc::ensures("p @ &frac<q, {n1, n2, n3} @ lock_test>", "{q = Own → n = n2}")]]
[[rc::ensures("frac q p : {n1, n2, n3} @ lock_test", "{q = Own → n = n2}")]]
size_t read_locked(struct lock_test* t) {
sl_lock(&t->lock);
rc_unlock(t->locked_int);
......@@ -83,7 +83,7 @@ size_t read_locked(struct lock_test* t) {
[[rc::args("p @ &frac<q, {n1, n2, n3} @ lock_test>")]]
[[rc::exists("n : Z")]]
[[rc::returns("n @ int<size_t>")]]
[[rc::ensures("p @ &frac<q, {n1, n2, n3} @ lock_test>", "{q = Own → n ≤ n3}")]]
[[rc::ensures("frac q p : {n1, n2, n3} @ lock_test", "{q = Own → n ≤ n3}")]]
size_t increment(struct lock_test* t) {
sl_lock(&t->lock);
rc_unlock(t->locked_struct);
......
......@@ -39,7 +39,7 @@ struct [[rc::parameters("entry_size: nat")]]
"{n * entry_size} @ int<size_t>",
"entry_size @ int<size_t>")]]
[[rc::requires("{(layout_of struct_freelist) ⊑ ly_with_align entry_size entry_size}")]]
[[rc::ensures("p @ &own<n @ slab<entry_size>>")]]
[[rc::ensures("own p : slab<entry_size>")]]
void slab_init(struct slab *s, unsigned char *p, size_t chunksize, size_t entry_size)
{
s->chunk = p;
......@@ -51,7 +51,7 @@ void slab_init(struct slab *s, unsigned char *p, size_t chunksize, size_t entry_
[[rc::parameters("p : loc", "n : nat", "entry_size : nat")]]
[[rc::args("p @ &own<n @ slab<entry_size>>")]]
[[rc::returns("{(0 < n)%nat} @ optional<&own<uninit<{ly_with_align entry_size entry_size}>>>")]]
[[rc::ensures("p @ &own<{(n - 1)%nat} @ slab<entry_size>>")]]
[[rc::ensures("own p : {(n - 1)%nat} @ slab<entry_size>")]]
void* slab_alloc(struct slab *s)
{
struct freelist *f;
......@@ -75,7 +75,7 @@ void* slab_alloc(struct slab *s)
[[rc::parameters("p : loc", "fp : loc", "n : nat", "entry_size : nat")]]
[[rc::args("p @ &own<n @ slab<entry_size>>", "fp @ &own<uninit<{ly_with_align entry_size entry_size}>>")]]
[[rc::ensures("p @ &own<{(n + 1)%nat} @ slab<entry_size>>")]]
[[rc::ensures("own p : {(n + 1)%nat} @ slab<entry_size>")]]
void slab_free(struct slab *s, void* x)
{
struct freelist* f = x;
......
......@@ -24,7 +24,7 @@
[[rc::args("p @ ptr", "align @ int<size_t>", "size @ &own<uninit<size_t>>")]]
[[rc::exists("diff : nat")]]
[[rc::returns("{p +ₗ diff} @ ptr")]]
[[rc::ensures("size @ &own<diff @ int<size_t>>", "{(p +ₗ diff) `aligned_to` align}", "{diff < align}")]]
[[rc::ensures("own size : diff @ int<size_t>", "{(p +ₗ diff) `aligned_to` align}", "{diff < align}")]]
unsigned char * round_pointer_up(unsigned char *p, size_t align, size_t *size);
......@@ -104,7 +104,7 @@ void mpool_free(struct mpool *p, void *ptr);
[[rc::requires("{layout_of struct_mpool_entry ⊑ ly_with_align entry_size entry_size}",
"{layout_of struct_mpool_chunk ⊑ ly_with_align entry_size entry_size}",
"{is_power_of_two entry_size}")]]
[[rc::ensures("p @ &own<{0%nat} @ mpool<entry_size>>")]]
[[rc::ensures("own p : {0%nat} @ mpool<entry_size>")]]
void mpool_init(struct mpool *p, size_t entry_size)
{
p->entry_size = entry_size;
......@@ -122,7 +122,7 @@ void mpool_init(struct mpool *p, size_t entry_size)
[[rc::parameters("p : loc", "entry_size : nat", "q : own_state", "entries : nat", "from : loc")]]
[[rc::args("p @ &own<uninit<struct_mpool>>", "from @ &frac<q, entries @ mpool<entry_size>>")]]
[[rc::exists("rentries : nat")]]
[[rc::ensures("p @ &own<rentries @ mpool<entry_size>>", "from @ &frac<q, {0%nat} @ mpool<entry_size>>",
[[rc::ensures("own p : rentries @ mpool<entry_size>", "frac q from : {0%nat} @ mpool<entry_size>",
"{q = Own → rentries = entries}")]]
void mpool_init_from(struct mpool *p, struct mpool *from)
{
......@@ -148,7 +148,7 @@ void mpool_init_from(struct mpool *p, struct mpool *from)
*/
[[rc::parameters("p : loc", "entry_size : nat", "q : own_state", "entries : nat", "fallback : loc")]]
[[rc::args("p @ &own<uninit<struct_mpool>>", "fallback @ &shr<entries @ mpool<entry_size>>")]]
[[rc::ensures("p @ &own<{0%nat} @ mpool<entry_size>>")]]
[[rc::ensures("own p : {0%nat} @ mpool<entry_size>")]]
void mpool_init_with_fallback(struct mpool *p, struct mpool *fallback)
{
mpool_init(p, fallback->entry_size);
......@@ -161,7 +161,7 @@ void mpool_init_with_fallback(struct mpool *p, struct mpool *fallback)
*/
[[rc::parameters("p : loc", "n : nat", "entry_size : nat")]]
[[rc::args("p @ &own<n @ mpool<entry_size>>")]]
[[rc::ensures("p @ &own<uninit<struct_mpool>>")]]
[[rc::ensures("own p : uninit<struct_mpool>")]]
void mpool_fini(struct mpool *p) {
struct mpool_entry *entry;
struct mpool_chunk *chunk;
......@@ -214,7 +214,7 @@ void mpool_fini(struct mpool *p) {
"&own<uninit<{ly_with_align (m * entry_size) entry_size}>>",
"{m * entry_size} @ int<size_t>")]]
[[rc::returns("{Z_of_bool (bool_decide (0 < m)%nat)} @ int<bool_it>")]]
[[rc::ensures("p @ &frac<q, {(n + m)%nat} @ mpool<entry_size>>")]]
[[rc::ensures("frac q p : {(n + m)%nat} @ mpool<entry_size>")]]
[[rc::tactics("all: try by destruct m => //=; solve_goal.")]]
bool mpool_add_chunk(struct mpool *p, void *begin, size_t size)
{
......@@ -247,7 +247,7 @@ bool mpool_add_chunk(struct mpool *p, void *begin, size_t size)
[[rc::args("p @ &frac<q, n @ mpool<entry_size>>")]]
[[rc::exists("b : bool")]]
[[rc::returns("b @ optional<&own<uninit<{ly_with_align entry_size entry_size}>>>")]]
[[rc::ensures("p @ &frac<q, {(n-1)%nat} @ mpool<entry_size>>", "{q = Own → b ↔ (0 < n)%nat}")]]
[[rc::ensures("frac q p : {(n-1)%nat} @ mpool<entry_size>", "{q = Own → b ↔ (0 < n)%nat}")]]
[[rc::tactics("all: try by destruct x1 as [|[]]; try solve_goal; zify; ring_simplify; solve_goal.")]]
static void *mpool_alloc_no_fallback(struct mpool *p)
{
......@@ -299,7 +299,7 @@ exit:
[[rc::args("p @ &frac<q, n @ mpool<entry_size>>")]]
[[rc::exists("b : bool")]]
[[rc::returns("b @ optional<&own<uninit<{ly_with_align entry_size entry_size}>>>")]]
[[rc::ensures("p @ &frac<q, {(n-1)%nat} @ mpool<entry_size>>", "{q = Own → (0 < n)%nat → b}")]]
[[rc::ensures("frac q p : {(n-1)%nat} @ mpool<entry_size>", "{q = Own → (0 < n)%nat → b}")]]
void *mpool_alloc(struct mpool *p) {
void *ret = mpool_alloc_no_fallback(p);
if (ret != NULL) {
......@@ -308,7 +308,7 @@ void *mpool_alloc(struct mpool *p) {
p = p->fallback;
[[rc::inv_vars("p : optional<&shr<mpool<entry_size>>>")]]
[[rc::constraints("p @ &frac<q, {(n - 1)%nat} @ mpool<entry_size>>", "{q = Own → n = 0%nat}")]]
[[rc::constraints("frac q p : {(n - 1)%nat} @ mpool<entry_size>", "{q = Own → n = 0%nat}")]]
while (p != NULL) {
ret = mpool_alloc_no_fallback(p);
if (ret != NULL) {
......@@ -328,7 +328,7 @@ void *mpool_alloc(struct mpool *p) {
*/
[[rc::parameters("p : loc", "q : own_state", "n : nat", "entry_size : nat", "ptr : loc")]]
[[rc::args("p @ &frac<q, n @ mpool<entry_size>>", "ptr @ &own<uninit<{ly_with_align entry_size entry_size}>>")]]
[[rc::ensures("p @ &frac<q, {(n + 1)%nat} @ mpool<entry_size>>")]]
[[rc::ensures("frac q p : {(n + 1)%nat} @ mpool<entry_size>")]]
void mpool_free(struct mpool *p, void *ptr) {
struct mpool_entry *e = ptr;
......@@ -350,7 +350,7 @@ void mpool_free(struct mpool *p, void *ptr) {
[[rc::requires("{(align * entry_size + count * entry_size)%Z ∈ size_t}", "{is_power_of_two align}")]]
[[rc::exists("n2 : nat")]]
[[rc::returns("optional<&own<uninit<{ly_with_align (count * entry_size) (align * entry_size)}>>>")]]
[[rc::ensures("p @ &frac<q, n2 @ mpool<entry_size>>", "{q = Own → n2 <= n}")]]
[[rc::ensures("frac q p : n2 @ mpool<entry_size>", "{q = Own → n2 <= n}")]]
[[rc::tactics("all: try by destruct o'; solve_goal.")]]
[[rc::tactics("all: try by apply mult_le_compat_r; solve_goal.")]]
[[rc::tactics("all: try by repeat progress rewrite /ly_size/=; have : (x4 - Z.to_nat o' - count > 0)%nat; solve_goal.")]]
......@@ -374,7 +374,7 @@ void *mpool_alloc_contiguous_no_fallback(struct mpool *p, size_t count, size_t a
[[rc::exists("pc : loc",
"entries_in_chunks1 : nat", "entries_in_chunks2 : nat",
"entries_in_entry_list : nat")]]
[[rc::inv_vars("align : {align * entry_size} @ int<size_t>", "ret : null", "p : ∃ l. singleton_place<l>",
[[rc::inv_vars("align : {align * entry_size} @ int<size_t>", "ret : null", "p : ∃ l. place<l>",
"prev : pc @ &own<entries_in_chunks2 @ mpool_chunk_t<entry_size>>")]]
[[rc::constraints("[p at{struct_mpool}ₗ \"locked\" ◁ₗ struct struct_mpool_locked_inner [wand_ex (λ x, pc ◁ₗ x @ mpool_chunk_t entry_size) (λ x, (entries_in_chunks1 + x)%nat @ mpool_chunk_t entry_size) ; entries_in_entry_list @ mpool_entry_t entry_size]]",
"{shelve_hint (q = Own → n = (entries_in_chunks1 + entries_in_chunks2 + entries_in_entry_list)%nat)}")]]
......@@ -447,7 +447,7 @@ void *mpool_alloc_contiguous_no_fallback(struct mpool *p, size_t count, size_t a
[[rc::requires("{(align * entry_size + count * entry_size)%Z ∈ size_t}", "{is_power_of_two align}")]]
[[rc::exists("n2 : nat")]]
[[rc::returns("optional<&own<uninit<{ly_with_align (count * entry_size) (align * entry_size)}>>>")]]
[[rc::ensures("p @ &frac<q, n2 @ mpool<entry_size>>", "{q = Own → n2 <= n}")]]
[[rc::ensures("frac q p : n2 @ mpool<entry_size>", "{q = Own → n2 <= n}")]]
void *mpool_alloc_contiguous(struct mpool *p, size_t count, size_t align)
{
void *ret = mpool_alloc_contiguous_no_fallback(p, count, align);
......@@ -459,7 +459,7 @@ void *mpool_alloc_contiguous(struct mpool *p, size_t count, size_t align)
p = p->fallback;
[[rc::exists("n2 : nat")]]
[[rc::inv_vars("p : optional<&shr<mpool<entry_size>>>")]]
[[rc::constraints("p @ &frac<q, n2 @ mpool<entry_size>>", "{q = Own → n2 <= n}")]]
[[rc::constraints("frac q p : n2 @ mpool<entry_size>", "{q = Own → n2 <= n}")]]
while (p != NULL) {
ret = mpool_alloc_contiguous_no_fallback(p, count, align);
......
......@@ -16,7 +16,7 @@ struct [[rc::refined_by("n : nat")]] mpool {
[[rc::parameters("p : loc")]]
[[rc::args("p @ &own<uninit<struct_mpool>>")]]
[[rc::ensures("p @ &own<{0%nat} @ mpool>")]]
[[rc::ensures("own p : {0%nat} @ mpool")]]
void mpool_init(struct mpool *p) {
p->entry_list = NULL;
}
......@@ -24,7 +24,7 @@ void mpool_init(struct mpool *p) {
[[rc::parameters("p : loc", "n : nat")]]
[[rc::args("p @ &own<n @ mpool>")]]
[[rc::returns("{(0 < n)%nat} @ optional<&own<uninit<ENTRY_LAYOUT>>>")]]
[[rc::ensures("p @ &own<{(n - 1)%nat} @ mpool>")]]
[[rc::ensures("own p : {(n - 1)%nat} @ mpool")]]
void *mpool_get(struct mpool *p) {
if (p->entry_list == NULL) {
return NULL;
......@@ -36,18 +36,18 @@ void *mpool_get(struct mpool *p) {
[[rc::parameters("p : loc", "n : nat")]]
[[rc::args("p @ &own<n @ mpool>", "&own<uninit<ENTRY_LAYOUT>>")]]
[[rc::ensures("p @ &own<{(n + 1)%nat} @ mpool>")]]
[[rc::ensures("own p : {(n + 1)%nat} @ mpool")]]
void mpool_put(struct mpool *p, void *ptr) {
// ptr : &own<uninit<ENTRY_LAYOUT>>
struct mpool_entry *e = ptr;
// e: &own<uninit<ENTRY_LAYOUT>>
// e: &own<padded<uninit<struct_mpool_entry>, struct_mpool_entry, ENTRY_LAYOUT>>
// e: &own<padded<struct<struct_mpool_entry, [uninit LPtr]>, struct_mpool_entry, ENTRY_LAYOUT>>
// e: &own<padded<struct<struct_mpool_entry, uninit<void*>, struct_mpool_entry, ENTRY_LAYOUT>>
// p: &own<struct<struct_mpool, [{n > 0} @ optional<&own<{n - 1} @ mpool_entry>>]>>
e->next = p->entry_list;
// e: &own<padded<struct<struct_mpool_entry, [{n > 0} @ optional<&own<{n - 1} @ mpool_entry>>]>, struct_mpool_entry, ENTRY_LAYOUT>>
// p: &own<struct<struct_mpool, [uninit<LPtr>]>>
// p: &own<struct<struct_mpool, [uninit<void*>]>>
p->entry_list = e;
// p: &own<struct<struct_mpool, [&own<padded<struct<struct_mpool_entry, [{n > 0} @ optional<&own<{n - 1} @ mpool_entry>>]>, struct_mpool_entry, ENTRY_LAYOUT>>]>>
}
......
......@@ -58,7 +58,7 @@ fixed_size_map {
[[rc::args("m @ &own<{mp, items, count} @ fixed_size_map>")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::exists("items2 : {list item_ref}", "count2: nat")]]
[[rc::ensures("m @ &own<{mp, items2, count2} @ fixed_size_map>", "{count <= count2}", "{1 < count2}",
[[rc::ensures("own m : {mp, items2, count2} @ fixed_size_map", "{count <= count2}", "{1 < count2}",
"{length items <= length items2}")]]
void fsm_realloc_if_necessary(struct fixed_size_map *m);
......@@ -68,7 +68,7 @@ void fsm_realloc_if_necessary(struct fixed_size_map *m);
[[rc::args("len @ int<size_t>")]]
[[rc::requires("{1 < len}", "{struct_item.(ly_size) * len + 16 ≤ max_int size_t}")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::ensures("m @ &own<{∅, replicate len Empty, len} @ fixed_size_map> ")]]
[[rc::ensures("own m : {∅, replicate len Empty, len} @ fixed_size_map")]]
[[rc::lemmas("fsm_invariant_init")]]
[[rc::tactics("all: try by apply/list_subequiv_split; solve_goal.")]]
[[rc::tactics("all: try by rewrite length_filter_replicate_True; solve_goal.")]]
......@@ -107,7 +107,7 @@ size_t fsm_slot_for_key(size_t len, size_t key) {
[[rc::args("m @ &own<{mp, items, count} @ fixed_size_map>", "key @ int<size_t>")]]
[[rc::exists("n : nat")]]
[[rc::returns("n @ int<size_t>")]]
[[rc::ensures("m @ &own<{mp, items, count} @ fixed_size_map>")]]
[[rc::ensures("own m : {mp, items, count} @ fixed_size_map")]]
[[rc::ensures("{∃ x, items !! n = Some x ∧ probe_ref key items = Some (n, x)}")]]
[[rc::lemmas("lookup_lt_is_Some_2")]]
[[rc::tactics("all: try by eexists _; split => //; apply probe_ref_take_Some; naive_solver.")]]
......@@ -136,7 +136,7 @@ size_t fsm_probe(struct fixed_size_map *m, size_t key) {
[[rc::requires("[alloc_initialized]")]]
[[rc::exists("items2 : {list item_ref}", "count2 : nat")]]
[[rc::returns("{mp !! key} @ optionalO<λ ty. &own<ty>>")]]
[[rc::ensures("m @ &own<{<[key:=ty]>mp, items2, count2} @ fixed_size_map>")]]
[[rc::ensures("own m : {<[key:=ty]>mp, items2, count2} @ fixed_size_map")]]
[[rc::ensures("{count - 1 <= count2}", "{length items <= length items2}")]]
[[rc::lemmas("fsm_invariant_insert")]]
[[rc::tactics("all: try by erewrite length_filter_insert => //; solve_goal.")]]
......@@ -162,7 +162,7 @@ void *fsm_insert(struct fixed_size_map *m, size_t key, void *value) {
[[rc::args("m @ &own<{mp, items, count} @ fixed_size_map>", "key @ int<size_t>")]]
[[rc::exists("p : loc", "items2 : {list item_ref}")]]
[[rc::returns("{mp !! key} @ optionalO<λ ty. p @ &own<ty>>")]]
[[rc::ensures("m @ &own<{alter (λ _, singleton_place p) key mp, items2, count} @ fixed_size_map>")]]
[[rc::ensures("own m : {alter (λ _, place p) key mp, items2, count} @ fixed_size_map")]]
[[rc::lemmas("fsm_invariant_alter")]]
[[rc::tactics("all: try by erewrite length_filter_insert => //; solve_goal.")]]
[[rc::tactics("all: try by apply inhabitant.")]]
......@@ -181,7 +181,7 @@ void *fsm_get(struct fixed_size_map *m, size_t key) {
[[rc::args("m @ &own<{mp, items, count} @ fixed_size_map>", "key @ int<size_t>")]]
[[rc::exists("items2 : {list item_ref}")]]
[[rc::returns("{mp !! key} @ optionalO<λ ty. &own<ty>>")]]
[[rc::ensures("m @ &own<{delete key mp, items2, count} @ fixed_size_map>")]]
[[rc::ensures("own m : {delete key mp, items2, count} @ fixed_size_map")]]
[[rc::lemmas("fsm_invariant_delete")]]
[[rc::tactics("all: try by erewrite length_filter_insert => //; solve_goal.")]]
void *fsm_remove(struct fixed_size_map *m, size_t key) {
......
......@@ -24,7 +24,7 @@ struct [[rc::refined_by("a : nat")]] mem_t {
[[rc::parameters("a : nat", "n : nat", "p : loc")]]
[[rc::args ("p @ &own<a @ mem_t>", "n @ int<size_t>")]]
[[rc::returns("{n ≤ a} @ optional<&own<uninit<n>>, null>")]]
[[rc::ensures("p @ &own<{n ≤ a ? a - n : a} @ mem_t>")]]
[[rc::ensures("own p : {n ≤ a ? a - n : a} @ mem_t")]]
void *alloc(struct mem_t *d, size_t size) {
if(size > d->len) return NULL;
d->len -= size;
......
......@@ -30,7 +30,7 @@ chunk {
[[rc::args ("p @ &own<s @ chunks_t>", "q @ &own<uninit<n>>",
"n @ int<size_t>")]]
[[rc::requires ("{sizeof struct_chunk ≤ n}")]]
[[rc::ensures ("p @ &own<{{[n]} ⊎ s} @ chunks_t>")]]
[[rc::ensures ("own p : {{[n]} ⊎ s} @ chunks_t")]]
[[rc::tactics ("all: multiset_solver.")]]
void free(chunks_t* list, void *data, size_t size) {
chunks_t *cur = list;
......
......@@ -242,10 +242,10 @@ Section code.
(* Definition of function [binary_search]. *)
Definition impl_binary_search : function := {|
f_args := [
("comp", LPtr);
("xs", LPtr);
("comp", void*);
("xs", void*);
("n", it_layout i32);
("x", LPtr)
("x", void*)
];
f_local_vars := [
("r", it_layout i32);
......@@ -274,9 +274,9 @@ Section code.
"k" <-{ it_layout i32 }
LocInfoE loc_38 ((LocInfoE loc_39 (use{it_layout i32} (LocInfoE loc_40 ("l")))) +{IntOp i32, IntOp i32} (LocInfoE loc_41 ((LocInfoE loc_42 ((LocInfoE loc_43 (use{it_layout i32} (LocInfoE loc_44 ("r")))) -{IntOp i32, IntOp i32} (LocInfoE loc_45 (use{it_layout i32} (LocInfoE loc_46 ("l")))))) /{IntOp i32, IntOp i32} (LocInfoE loc_47 (i2v 2 i32))))) ;
locinfo: loc_25 ;
"$0" <- LocInfoE loc_27 (use{LPtr} (LocInfoE loc_28 ("comp"))) with
[ LocInfoE loc_29 (use{LPtr} (LocInfoE loc_31 ((LocInfoE loc_32 (!{LPtr} (LocInfoE loc_33 ("xs")))) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_34 (use{it_layout i32} (LocInfoE loc_35 ("k"))))))) ;
LocInfoE loc_36 (use{LPtr} (LocInfoE loc_37 ("x"))) ] ;
"$0" <- LocInfoE loc_27 (use{void*} (LocInfoE loc_28 ("comp"))) with
[ LocInfoE loc_29 (use{void*} (LocInfoE loc_31 ((LocInfoE loc_32 (!{void*} (LocInfoE loc_33 ("xs")))) at_offset{void*, PtrOp, IntOp i32} (LocInfoE loc_34 (use{it_layout i32} (LocInfoE loc_35 ("k"))))))) ;
LocInfoE loc_36 (use{void*} (LocInfoE loc_37 ("x"))) ] ;
locinfo: loc_25 ;
if: LocInfoE loc_25 ("$0")
then
......@@ -318,22 +318,22 @@ Section code.
(* Definition of function [compare_int]. *)
Definition impl_compare_int :