Commit 0c5bc27d authored by Michael Sammler's avatar Michael Sammler
Browse files

update code of example

parent 3cefc49b
Pipeline #43564 canceled with stage
......@@ -16,21 +16,35 @@
//@Coercion byte_layout : nat >-> layout.
//@rc::end
struct [[rc::refined_by("a : nat")]] mem_t {
struct [[rc::refined_by("a: nat")]] mem_t {
[[rc::field("a @ int<size_t>")]] size_t len;
[[rc::field("&own<uninit<a>>")]] unsigned char *buffer;
[[rc::field("&own<uninit<a>>")]] unsigned char* buffer;
};
[[rc::parameters("a : nat", "n : nat", "p : loc")]]
[[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("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;
void* alloc(struct mem_t* d, size_t sz) {
if(sz > d->len) return NULL;
d->len -= sz;
return d->buffer + d->len;
}
// variant of alloc that allocates from the start of buffer instead of the end
[[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("own p : {n ≤ a ? a - n : a} @ mem_t")]]
void* alloc_from_start(struct mem_t* d, size_t sz) {
if(sz > d->len) return NULL;
d->len -= sz;
unsigned char *res = d->buffer;
d->buffer += sz;
return res;
}
// Thread-safe version (given in appendix).
[[rc::parameters("lid : lock_id")]]
......
......@@ -16,8 +16,9 @@
typedef struct
[[rc::refined_by("s: {gmultiset nat}")]]
[[rc::ptr_type("chunks_t : {s ≠ ∅} @ optional<&own<...>, null>")]]
[[rc::exists ("n : nat", "tail : {gmultiset nat}")]]
[[rc::ptr_type("chunks_t:"
"{s ≠ ∅} @ optional<&own<...>, null>")]]
[[rc::exists ("n: nat", "tail: {gmultiset nat}")]]
[[rc::size ("n")]]
[[rc::constraints("{s = {[n]} ⊎ tail}",
"{∀ k, k ∈ tail → n ≤ k}")]]
......@@ -26,25 +27,24 @@ chunk {
[[rc::field("tail @ chunks_t")]] struct chunk* next;
}* chunks_t;
[[rc::parameters("s : {gmultiset nat}", "p : loc", "q : loc", "n : nat")]]
[[rc::args ("p @ &own<s @ chunks_t>", "q @ &own<uninit<n>>",
[[rc::parameters("s: {gmultiset nat}", "p: loc", "n: nat")]]
[[rc::args ("p @ &own<s @ chunks_t>", "&own<uninit<n>>",
"n @ int<size_t>")]]
[[rc::requires ("{sizeof struct_chunk ≤ n}")]]
[[rc::requires ("{sizeof(struct_chunk) ≤ n}")]]
[[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;
[[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>>")]]
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>>")]]
while(*cur != NULL) {
if(size <= (*cur)->size) break;
if(sz <= (*cur)->size) break;
cur = &(*cur)->next;
}
chunks_t entry = data;
entry->size = size;
entry->next = *cur;
entry->size = sz; entry->next = *cur;
*cur = entry;
}
......@@ -14,7 +14,7 @@ Section proof_alloc.
typed_function impl_alloc type_of_alloc.
Proof.
Open Scope printing_sugar.
start_function "alloc" ([[a n] p]) => arg_d arg_size.
start_function "alloc" ([[a n] p]) => arg_d arg_sz.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
From refinedc.typing Require Import typing.
From refinedc.examples.paper_example_2_1 Require Import generated_code.
From refinedc.examples.paper_example_2_1 Require Import generated_spec.
From refinedc.examples.spinlock Require Import spinlock_def.
Set Default Proof Using "Type".
(* Generated from [examples/paper_example_2_1.c]. *)
Section proof_alloc_from_start.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
(* Typing proof for [alloc_from_start]. *)
Lemma type_alloc_from_start :
typed_function impl_alloc_from_start type_of_alloc_from_start.
Proof.
Open Scope printing_sugar.
start_function "alloc_from_start" ([[a n] p]) => arg_d arg_sz local_res.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "alloc_from_start" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "alloc_from_start".
Qed.
End proof_alloc_from_start.
......@@ -92,6 +92,11 @@ Section spec.
fn( (a, n, p) : nat * nat * loc; (p @ (&own (a @ (mem_t)))), (n @ (int (size_t))); True)
() : (), ((n a) @ (optional (&own (uninit (n))) (null))); (p ◁ₗ ((n a ? a - n : a) @ (mem_t))).
(* Specifications for function [alloc_from_start]. *)
Definition type_of_alloc_from_start :=
fn( (a, n, p) : nat * nat * loc; (p @ (&own (a @ (mem_t)))), (n @ (int (size_t))); True)
() : (), ((n a) @ (optional (&own (uninit (n))) (null))); (p ◁ₗ ((n a ? a - n : a) @ (mem_t))).
(* Specifications for function [thread_safe_alloc]. *)
Definition type_of_thread_safe_alloc :=
fn( (lid, n) : lock_id * nat; (n @ (int (size_t))); (initialized "lock" lid) (initialized "data" lid))
......
generated_proof_alloc.v
generated_proof_alloc_from_start.v
generated_proof_atomic_signal_fence.v
generated_proof_atomic_thread_fence.v
generated_proof_fork.v
......
......@@ -7,62 +7,62 @@ Set Default Proof Using "Type".
(* Generated from [examples/paper_example_2_2.c]. *)
Section code.
Definition file_0 : string := "examples/paper_example_2_2.c".
Definition loc_2 : location_info := LocationInfo file_0 36 2 36 23.
Definition loc_3 : location_info := LocationInfo file_0 42 2 45 3.
Definition loc_4 : location_info := LocationInfo file_0 46 2 46 24.
Definition loc_5 : location_info := LocationInfo file_0 47 2 47 21.
Definition loc_6 : location_info := LocationInfo file_0 48 2 48 21.
Definition loc_2 : location_info := LocationInfo file_0 37 2 37 23.
Definition loc_3 : location_info := LocationInfo file_0 43 2 46 3.
Definition loc_4 : location_info := LocationInfo file_0 47 2 47 24.
Definition loc_5 : location_info := LocationInfo file_0 48 2 48 19.
Definition loc_6 : location_info := LocationInfo file_0 48 20 48 39.
Definition loc_7 : location_info := LocationInfo file_0 49 2 49 15.
Definition loc_8 : location_info := LocationInfo file_0 49 2 49 6.
Definition loc_9 : location_info := LocationInfo file_0 49 3 49 6.
Definition loc_10 : location_info := LocationInfo file_0 49 3 49 6.
Definition loc_11 : location_info := LocationInfo file_0 49 9 49 14.
Definition loc_12 : location_info := LocationInfo file_0 49 9 49 14.
Definition loc_13 : location_info := LocationInfo file_0 48 2 48 13.
Definition loc_14 : location_info := LocationInfo file_0 48 2 48 7.
Definition loc_15 : location_info := LocationInfo file_0 48 2 48 7.
Definition loc_16 : location_info := LocationInfo file_0 48 16 48 20.
Definition loc_17 : location_info := LocationInfo file_0 48 16 48 20.
Definition loc_18 : location_info := LocationInfo file_0 48 17 48 20.
Definition loc_19 : location_info := LocationInfo file_0 48 17 48 20.
Definition loc_20 : location_info := LocationInfo file_0 47 2 47 13.
Definition loc_21 : location_info := LocationInfo file_0 47 2 47 7.
Definition loc_22 : location_info := LocationInfo file_0 47 2 47 7.
Definition loc_23 : location_info := LocationInfo file_0 47 16 47 20.
Definition loc_24 : location_info := LocationInfo file_0 47 16 47 20.
Definition loc_25 : location_info := LocationInfo file_0 46 19 46 23.
Definition loc_26 : location_info := LocationInfo file_0 46 19 46 23.
Definition loc_29 : location_info := LocationInfo file_0 42 2 45 3.
Definition loc_30 : location_info := LocationInfo file_0 42 32 45 3.
Definition loc_31 : location_info := LocationInfo file_0 43 4 43 35.
Definition loc_32 : location_info := LocationInfo file_0 44 4 44 24.
Definition loc_33 : location_info := LocationInfo file_0 42 2 45 3.
Definition loc_34 : location_info := LocationInfo file_0 42 2 45 3.
Definition loc_35 : location_info := LocationInfo file_0 44 4 44 7.
Definition loc_36 : location_info := LocationInfo file_0 44 10 44 23.
Definition loc_37 : location_info := LocationInfo file_0 44 11 44 23.
Definition loc_38 : location_info := LocationInfo file_0 44 11 44 17.
Definition loc_39 : location_info := LocationInfo file_0 44 11 44 17.
Definition loc_40 : location_info := LocationInfo file_0 44 13 44 16.
Definition loc_41 : location_info := LocationInfo file_0 44 13 44 16.
Definition loc_42 : location_info := LocationInfo file_0 43 29 43 35.
Definition loc_44 : location_info := LocationInfo file_0 43 7 43 27.
Definition loc_45 : location_info := LocationInfo file_0 43 7 43 11.
Definition loc_46 : location_info := LocationInfo file_0 43 7 43 11.
Definition loc_47 : location_info := LocationInfo file_0 43 15 43 27.
Definition loc_48 : location_info := LocationInfo file_0 43 15 43 27.
Definition loc_49 : location_info := LocationInfo file_0 43 15 43 21.
Definition loc_50 : location_info := LocationInfo file_0 43 15 43 21.
Definition loc_51 : location_info := LocationInfo file_0 43 17 43 20.
Definition loc_52 : location_info := LocationInfo file_0 43 17 43 20.
Definition loc_53 : location_info := LocationInfo file_0 42 8 42 30.
Definition loc_54 : location_info := LocationInfo file_0 42 8 42 12.
Definition loc_55 : location_info := LocationInfo file_0 42 8 42 12.
Definition loc_56 : location_info := LocationInfo file_0 42 9 42 12.
Definition loc_57 : location_info := LocationInfo file_0 42 9 42 12.
Definition loc_58 : location_info := LocationInfo file_0 42 16 42 30.
Definition loc_59 : location_info := LocationInfo file_0 36 18 36 22.
Definition loc_60 : location_info := LocationInfo file_0 36 18 36 22.
Definition loc_13 : location_info := LocationInfo file_0 48 20 48 31.
Definition loc_14 : location_info := LocationInfo file_0 48 20 48 25.
Definition loc_15 : location_info := LocationInfo file_0 48 20 48 25.
Definition loc_16 : location_info := LocationInfo file_0 48 34 48 38.
Definition loc_17 : location_info := LocationInfo file_0 48 34 48 38.
Definition loc_18 : location_info := LocationInfo file_0 48 35 48 38.
Definition loc_19 : location_info := LocationInfo file_0 48 35 48 38.
Definition loc_20 : location_info := LocationInfo file_0 48 2 48 13.
Definition loc_21 : location_info := LocationInfo file_0 48 2 48 7.
Definition loc_22 : location_info := LocationInfo file_0 48 2 48 7.
Definition loc_23 : location_info := LocationInfo file_0 48 16 48 18.
Definition loc_24 : location_info := LocationInfo file_0 48 16 48 18.
Definition loc_25 : location_info := LocationInfo file_0 47 19 47 23.
Definition loc_26 : location_info := LocationInfo file_0 47 19 47 23.
Definition loc_29 : location_info := LocationInfo file_0 43 2 46 3.
Definition loc_30 : location_info := LocationInfo file_0 43 32 46 3.
Definition loc_31 : location_info := LocationInfo file_0 44 4 44 33.
Definition loc_32 : location_info := LocationInfo file_0 45 4 45 24.
Definition loc_33 : location_info := LocationInfo file_0 43 2 46 3.
Definition loc_34 : location_info := LocationInfo file_0 43 2 46 3.
Definition loc_35 : location_info := LocationInfo file_0 45 4 45 7.
Definition loc_36 : location_info := LocationInfo file_0 45 10 45 23.
Definition loc_37 : location_info := LocationInfo file_0 45 11 45 23.
Definition loc_38 : location_info := LocationInfo file_0 45 11 45 17.
Definition loc_39 : location_info := LocationInfo file_0 45 11 45 17.
Definition loc_40 : location_info := LocationInfo file_0 45 13 45 16.
Definition loc_41 : location_info := LocationInfo file_0 45 13 45 16.
Definition loc_42 : location_info := LocationInfo file_0 44 27 44 33.
Definition loc_44 : location_info := LocationInfo file_0 44 7 44 25.
Definition loc_45 : location_info := LocationInfo file_0 44 7 44 9.
Definition loc_46 : location_info := LocationInfo file_0 44 7 44 9.
Definition loc_47 : location_info := LocationInfo file_0 44 13 44 25.
Definition loc_48 : location_info := LocationInfo file_0 44 13 44 25.
Definition loc_49 : location_info := LocationInfo file_0 44 13 44 19.
Definition loc_50 : location_info := LocationInfo file_0 44 13 44 19.
Definition loc_51 : location_info := LocationInfo file_0 44 15 44 18.
Definition loc_52 : location_info := LocationInfo file_0 44 15 44 18.
Definition loc_53 : location_info := LocationInfo file_0 43 8 43 30.
Definition loc_54 : location_info := LocationInfo file_0 43 8 43 12.
Definition loc_55 : location_info := LocationInfo file_0 43 8 43 12.
Definition loc_56 : location_info := LocationInfo file_0 43 9 43 12.
Definition loc_57 : location_info := LocationInfo file_0 43 9 43 12.
Definition loc_58 : location_info := LocationInfo file_0 43 16 43 30.
Definition loc_59 : location_info := LocationInfo file_0 37 18 37 22.
Definition loc_60 : location_info := LocationInfo file_0 37 18 37 22.
(* Definition of struct [atomic_flag]. *)
Program Definition struct_atomic_flag := {|
......@@ -94,7 +94,7 @@ Section code.
f_args := [
("list", void*);
("data", void*);
("size", it_layout size_t)
("sz", it_layout size_t)
];
f_local_vars := [
("cur", void*);
......@@ -119,7 +119,7 @@ Section code.
]> $
<[ "#2" :=
locinfo: loc_44 ;
if: LocInfoE loc_44 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_44 ((LocInfoE loc_45 (use{it_layout size_t} (LocInfoE loc_46 ("size")))) {IntOp size_t, IntOp size_t} (LocInfoE loc_47 (use{it_layout size_t} (LocInfoE loc_48 ((LocInfoE loc_49 (!{void*} (LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("cur")))))) at{struct_chunk} "size")))))))
if: LocInfoE loc_44 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_44 ((LocInfoE loc_45 (use{it_layout size_t} (LocInfoE loc_46 ("sz")))) {IntOp size_t, IntOp size_t} (LocInfoE loc_47 (use{it_layout size_t} (LocInfoE loc_48 ((LocInfoE loc_49 (!{void*} (LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("cur")))))) at{struct_chunk} "size")))))))
then
Goto "#5"
else
......@@ -131,7 +131,7 @@ Section code.
LocInfoE loc_25 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_25 (use{void*} (LocInfoE loc_26 ("data"))))) ;
locinfo: loc_5 ;
LocInfoE loc_20 ((LocInfoE loc_21 (!{void*} (LocInfoE loc_22 ("entry")))) at{struct_chunk} "size") <-{ it_layout size_t }
LocInfoE loc_23 (use{it_layout size_t} (LocInfoE loc_24 ("size"))) ;
LocInfoE loc_23 (use{it_layout size_t} (LocInfoE loc_24 ("sz"))) ;
locinfo: loc_6 ;
LocInfoE loc_13 ((LocInfoE loc_14 (!{void*} (LocInfoE loc_15 ("entry")))) at{struct_chunk} "next") <-{ void* }
LocInfoE loc_16 (use{void*} (LocInfoE loc_18 (!{void*} (LocInfoE loc_19 ("cur"))))) ;
......
......@@ -14,13 +14,13 @@ Section proof_free.
typed_function impl_free type_of_free.
Proof.
Open Scope printing_sugar.
start_function "free" ([[[s p] q] n]) => arg_list arg_data arg_size local_cur local_entry.
start_function "free" ([[s p] n]) => arg_list arg_data arg_sz local_cur local_entry.
split_blocks ((
<[ "#1" :=
cp : loc,
cs : gmultiset nat,
arg_data ◁ₗ (q @ (&own (uninit (n))))
arg_size ◁ₗ (n @ (int (size_t)))
arg_data ◁ₗ (&own (uninit (n)))
arg_sz ◁ₗ (n @ (int (size_t)))
local_entry ◁ₗ uninit void*
local_cur ◁ₗ (cp @ (&own (cs @ (chunks_t))))
arg_list ◁ₗ (p @ (&own (wand (cp ◁ₗ ({[n]} cs) @ chunks_t) (({[n]} s) @ (chunks_t)))))
......
......@@ -99,7 +99,7 @@ Section spec.
(* Specifications for function [free]. *)
Definition type_of_free :=
fn( (s, p, q, n) : (gmultiset nat) * loc * loc * nat; (p @ (&own (s @ (chunks_t)))), (q @ (&own (uninit (n)))), (n @ (int (size_t))); sizeof struct_chunk n)
fn( (s, p, n) : (gmultiset nat) * loc * nat; (p @ (&own (s @ (chunks_t)))), (&own (uninit (n))), (n @ (int (size_t))); sizeof(struct_chunk) n)
() : (), (void); (p ◁ₗ (({[n]} s) @ (chunks_t))).
End spec.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment