paper_example_2_2.c 1.54 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
// Example of Section 2.2.

#include <stddef.h>
#include <stdbool.h>
#include <refinedc.h>
#include <spinlock.h>

// NOTE: alignment constraint hidden in a coercion.

//@rc::inlined
//@Definition layout_of_nat : nat → layout := ly_set_size struct_chunk.
//@Coercion layout_of_nat : nat >-> layout.
//@
//@Close Scope Z.
//@rc::end

typedef struct
[[rc::refined_by("s: {gmultiset nat}")]]
19
20
21
[[rc::ptr_type("chunks_t:"
               "{s ≠ ∅} @ optional<&own<...>, null>")]]
[[rc::exists  ("n: nat", "tail: {gmultiset nat}")]]
22
23
24
25
26
27
28
29
[[rc::size    ("n")]]
[[rc::constraints("{s = {[n]} ⊎ tail}",
                  "{∀ k, k ∈ tail → n ≤ k}")]]
chunk {
  [[rc::field("n @ int<size_t>")]] size_t size;
  [[rc::field("tail @ chunks_t")]] struct chunk* next;
}* chunks_t;

30
31
[[rc::parameters("s: {gmultiset nat}", "p: loc", "n: nat")]]
[[rc::args      ("p @ &own<s @ chunks_t>", "&own<uninit<n>>",
32
                 "n @ int<size_t>")]]
33
[[rc::requires  ("{sizeof(struct_chunk) ≤ n}")]]
34
[[rc::ensures   ("own p : {{[n]} ⊎ s} @ chunks_t")]]
35
[[rc::tactics   ("all: multiset_solver.")]]
36
37
38
39
40
41
42
void free(chunks_t* list, void* data, size_t sz) {
  chunks_t* cur = list;
  [[rc::exists  ("cp: loc", "cs: {gmultiset nat}")]]
  [[rc::inv_vars("cur: cp @ &own<cs @ chunks_t>")]]
  [[rc::inv_vars("list:"
       "p @ &own<wand<{cp ◁ₗ ({[n]} ⊎ cs) @ chunks_t},"
                     "{{[n]} ⊎ s} @ chunks_t>>")]]
43
  while(*cur != NULL) {
44
    if(sz <= (*cur)->size) break;
45
46
47
    cur = &(*cur)->next;
  }
  chunks_t entry = data;
48
  entry->size = sz; entry->next = *cur;
49
50
  *cur = entry;
}