Skip to content

GitLab

Commit f5ab0aad authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files
Options

Split paper examples in two parts.

parent 61492471
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 615 additions and 139 deletions
_CoqProject
View file @ f5ab0aad
......@@ -17,7 +17,6 @@
-Q _build/default/examples/proofs/lock refinedc.examples.lock
-Q _build/default/examples/proofs/flags refinedc.examples.flags
-Q _build/default/examples/proofs/shift refinedc.examples.shift
-Q _build/default/examples/proofs/paper_examples refinedc.examples.paper_examples
-Q _build/default/tutorial/proofs/binary_search_defs refinedc.tutorial.binary_search_defs
-Q _build/default/tutorial/proofs/t00_intro refinedc.tutorial.t00_intro
-Q _build/default/tutorial/proofs/t01_basic refinedc.tutorial.t01_basic
......@@ -35,3 +34,5 @@
-Q _build/default/tutorial/proofs/quicksort_solution refinedc.tutorial.quicksort_solution
-Q _build/default/tutorial/proofs/quicksort_exercise refinedc.tutorial.quicksort_exercise
-Q _build/default/examples/proofs/binary_search refinedc.examples.binary_search
-Q _build/default/examples/proofs/paper_example_2_1 refinedc.examples.paper_example_2_1
-Q _build/default/examples/proofs/paper_example_2_2 refinedc.examples.paper_example_2_2
examples/paper_examples.c → examples/paper_example_2_1.c
View file @ f5ab0aad
// Example of Section 2.1.
#include <stddef.h>
#include <stdbool.h>
#include <refinedc.h>
......@@ -14,8 +16,6 @@
//@Coercion byte_layout : nat >-> layout.
//@rc::end
//// Example of Section 2.1 //////////////////////////////////////////////////
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;
......@@ -31,47 +31,7 @@ void *alloc(struct mem_t *d, size_t size) {
return d->buffer + d->len;
}
//// Example of Section 2.2 //////////////////////////////////////////////////
// In the paper this example is simplified to ignore memory alignment.
// For the actual example we work on multisets of layouts, not nat.
typedef struct
[[rc::refined_by("s: {gmultiset layout}")]]
[[rc::ptr_type("chunks_t : {s ≠ ∅} @ optional<&own<...>, null>")]]
[[rc::exists ("ly : layout", "tail : {gmultiset layout}")]]
[[rc::size ("ly")]]
[[rc::constraints("{s = {[ly]} ⊎ tail}",
"{∀ k, k ∈ tail → ly.(ly_size) ≤ k.(ly_size)}")]]
chunk {
[[rc::field("{ly.(ly_size)} @ int<size_t>")]] size_t size;
[[rc::field("tail @ chunks_t")]] struct chunk* next;
}* chunks_t;
[[rc::parameters("s : {gmultiset layout}", "p : loc", "ly : layout")]]
[[rc::args ("p @ &own<s @ chunks_t>", "&own<uninit<ly>>",
"{ly.(ly_size)} @ int<size_t>")]]
[[rc::requires ("{layout_of struct_chunk ⊑ ly}")]]
[[rc::ensures ("p @ &own<{{[ly]} ⊎ 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 layout}")]]
[[rc::inv_vars("cur : cp @ &own<cs @ chunks_t>")]]
[[rc::inv_vars("list : p @ &own<"
"wand<{cp ◁ₗ ({[ly]} ⊎ cs) @ chunks_t}, "
"{{[ly]} ⊎ s} @ chunks_t>>")]]
while(*cur != NULL) {
if(size <= (*cur)->size) break;
cur = &(*cur)->next;
}
chunks_t entry = data;
entry->size = size;
entry->next = *cur;
*cur = entry;
}
//// Example given in appendix ///////////////////////////////////////////////
// Thread-safe version (given in appendix).
[[rc::parameters("lid : lock_id")]]
[[rc::global("spinlock<lid>")]]
......@@ -93,7 +53,7 @@ void *thread_safe_alloc(size_t size) {
return ret;
}
//// Testing thread-safety of thread_safe alloc //////////////////////////////
// Testing thread-safety.
// RefinedC does not have forking built-in at the moment.
// We axiomatize it using the following [fork] function.
......
examples/paper_example_2_2.c 0 → 100644
View file @ f5ab0aad
// 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}")]]
[[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}")]]
chunk {
[[rc::field("n @ int<size_t>")]] size_t size;
[[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>>",
"n @ int<size_t>")]]
[[rc::requires ("{sizeof struct_chunk ≤ n}")]]
[[rc::ensures ("p @ &own<{{[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>>")]]
while(*cur != NULL) {
if(size <= (*cur)->size) break;
cur = &(*cur)->next;
}
chunks_t entry = data;
entry->size = size;
entry->next = *cur;
*cur = entry;
}
examples/proofs/paper_examples/dune → examples/proofs/paper_example_2_1/dune
View file @ f5ab0aad
; Generated by [refinedc], do not edit.
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.paper_examples)
(name refinedc.examples.paper_example_2_1)
(theories refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
examples/proofs/paper_examples/generated_proof_alloc.v → examples/proofs/paper_example_2_1/generated_proof_alloc.v
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_examples Require Import generated_code.
From refinedc.examples.paper_examples Require Import generated_spec.
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_examples.c]. *)
(* Generated from [examples/paper_example_2_1.c]. *)
Section proof_alloc.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
......
examples/proofs/paper_examples/generated_proof_fork.v → examples/proofs/paper_example_2_1/generated_proof_fork.v
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_examples Require Import generated_code.
From refinedc.examples.paper_examples Require Import generated_spec.
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_examples.c]. *)
(* Generated from [examples/paper_example_2_1.c]. *)
Section proof_fork.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
......
examples/proofs/paper_examples/generated_proof_test_thread_safe_alloc.v → examples/proofs/paper_example_2_1/generated_proof_test_thread_safe_alloc.v
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_examples Require Import generated_code.
From refinedc.examples.paper_examples Require Import generated_spec.
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_examples.c]. *)
(* Generated from [examples/paper_example_2_1.c]. *)
Section proof_test_thread_safe_alloc.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
......
examples/proofs/paper_examples/generated_proof_test_thread_safe_alloc_fork_fn.v → examples/proofs/paper_example_2_1/generated_proof_test_thread_safe_alloc_fork_fn.v
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_examples Require Import generated_code.
From refinedc.examples.paper_examples Require Import generated_spec.
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_examples.c]. *)
(* Generated from [examples/paper_example_2_1.c]. *)
Section proof_test_thread_safe_alloc_fork_fn.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
......
examples/proofs/paper_examples/generated_proof_thread_safe_alloc.v → examples/proofs/paper_example_2_1/generated_proof_thread_safe_alloc.v
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_examples Require Import generated_code.
From refinedc.examples.paper_examples Require Import generated_spec.
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_examples.c]. *)
(* Generated from [examples/paper_example_2_1.c]. *)
Section proof_thread_safe_alloc.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
......
examples/proofs/paper_examples/generated_spec.v → examples/proofs/paper_example_2_1/generated_spec.v
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_examples Require Import generated_code.
From refinedc.examples.paper_example_2_1 Require Import generated_code.
From refinedc.examples.spinlock Require Import spinlock_def.
Set Default Proof Using "Type".
(* Generated from [examples/paper_examples.c]. *)
(* Generated from [examples/paper_example_2_1.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
......@@ -66,67 +66,6 @@ Section spec.
λ T, i2p (simplify_goal_val_eq v_ _ _ (mem_t_unfold _) T _).
Next Obligation. done. Qed.
(* Definition of type [chunks_t]. *)
Definition chunks_t_rec : ((gmultiset layout) -d> typeO) → ((gmultiset layout) -d> typeO) := (λ self s,
((s ≠ ∅) @ (optional (&own (
tyexists (λ ly : layout,
tyexists (λ tail : gmultiset layout,
constrained (padded (struct struct_chunk [@{type}
((ly.(ly_size)) @ (int (size_t))) ;
(guarded ("chunks_t_0") (apply_dfun self (tail)))
]) struct_chunk ly) (
⌜s = {[ly]} ⊎ tail⌝ ∗
⌜∀ k, k ∈ tail → ly.(ly_size) ≤ k.(ly_size)⌝
)))
)) (null)))
)%I.
Typeclasses Opaque chunks_t_rec.
Global Instance chunks_t_rec_ne : Contractive chunks_t_rec.
Proof. solve_type_proper. Qed.
Definition chunks_t : rtype := {|
rty_type := (gmultiset layout);
rty r__ := fixp chunks_t_rec r__
|}.
Lemma chunks_t_unfold (s : gmultiset layout) :
(s @ chunks_t)%I ≡@{type} (
((s ≠ ∅) @ (optional (&own (
tyexists (λ ly : layout,
tyexists (λ tail : gmultiset layout,
constrained (padded (struct struct_chunk [@{type}
((ly.(ly_size)) @ (int (size_t))) ;
(guarded "chunks_t_0" (tail @ chunks_t))
]) struct_chunk ly) (
⌜s = {[ly]} ⊎ tail⌝ ∗
⌜∀ k, k ∈ tail → ly.(ly_size) ≤ k.(ly_size)⌝
)))
)) (null)))
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
Global Program Instance chunks_t_rmovable : RMovable chunks_t :=
{| rmovable 's := movable_eq _ _ (chunks_t_unfold s) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance chunks_t_simplify_hyp_place_inst l_ β_ (s : gmultiset layout) :
SimplifyHypPlace l_ β_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (chunks_t_unfold _)).
Global Instance chunks_t_simplify_goal_place_inst l_ β_ (s : gmultiset layout) :
SimplifyGoalPlace l_ β_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (chunks_t_unfold _)).
Global Program Instance chunks_t_simplify_hyp_val_inst v_ (s : gmultiset layout) :
SimplifyHypVal v_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (chunks_t_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance chunks_t_simplify_goal_val_inst v_ (s : gmultiset layout) :
SimplifyGoalVal v_ (s @ chunks_t)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (chunks_t_unfold _) T _).
Next Obligation. done. Qed.
(* Type definitions. *)
(* Function [atomic_thread_fence] has been skipped. *)
......@@ -153,11 +92,6 @@ 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 [free]. *)
Definition type_of_free :=
fn(∀ (s, p, ly) : (gmultiset layout) * loc * layout; (p @ (&own (s @ (chunks_t)))), (&own (uninit (ly))), ((ly.(ly_size)) @ (int (size_t))); ⌜layout_of struct_chunk ⊑ ly⌝)
→ ∃ () : (), (void); (p ◁ₗ (({[ly]} ⊎ s) @ (chunks_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))
......@@ -181,4 +115,3 @@ Section spec.
End spec.
Typeclasses Opaque mem_t_rec.
Typeclasses Opaque chunks_t_rec.
examples/proofs/paper_examples/proof_files → examples/proofs/paper_example_2_1/proof_files
View file @ f5ab0aad
......@@ -2,7 +2,6 @@ generated_proof_alloc.v
generated_proof_atomic_signal_fence.v
generated_proof_atomic_thread_fence.v
generated_proof_fork.v
generated_proof_free.v
generated_proof_sl_init.v
generated_proof_sl_lock.v
generated_proof_sl_unlock.v
......
examples/proofs/paper_example_2_2/dune 0 → 100644
View file @ f5ab0aad
; Generated by [refinedc], do not edit.
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.paper_example_2_2)
(theories refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
examples/proofs/paper_example_2_2/generated_code.v 0 → 100644
View file @ f5ab0aad
From refinedc.lang Require Export notation.
From refinedc.lang Require Import tactics.
From refinedc.typing Require Import annotations.
From refinedc.examples.spinlock Require Import spinlock_annot.
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_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 of struct [atomic_flag]. *)
Program Definition struct_atomic_flag := {|
sl_members := [
(Some "_Value", it_layout bool_it)
];
|}.
Solve Obligations with solve_struct_obligations.
(* Definition of struct [spinlock]. *)
Program Definition struct_spinlock := {|
sl_members := [
(Some "lock", it_layout bool_it)
];
|}.
Solve Obligations with solve_struct_obligations.
(* Definition of struct [chunk]. *)
Program Definition struct_chunk := {|
sl_members := [
(Some "size", it_layout size_t);
(Some "next", LPtr)
];
|}.
Solve Obligations with solve_struct_obligations.
(* Definition of function [free]. *)
Definition impl_free : function := {|
f_args := [
("list", LPtr);
("data", LPtr);
("size", it_layout size_t)
];
f_local_vars := [
("cur", LPtr);
("entry", LPtr)
];
f_init := "#0";
f_code := (
<[ "#0" :=
"cur" <-{ LPtr }
LocInfoE loc_59 (use{LPtr} (LocInfoE loc_60 ("list"))) ;
locinfo: loc_3 ;
Goto "#1"
]> $
<[ "#1" :=
locinfo: loc_53 ;
if: LocInfoE loc_53 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_53 ((LocInfoE loc_54 (use{LPtr} (LocInfoE loc_56 (!{LPtr} (LocInfoE loc_57 ("cur")))))) !={PtrOp, PtrOp} (LocInfoE loc_58 (NULL)))))
then
locinfo: loc_44 ;
Goto "#2"
else
Goto "#3"
]> $
<[ "#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 (!{LPtr} (LocInfoE loc_51 (!{LPtr} (LocInfoE loc_52 ("cur")))))) at{struct_chunk} "size")))))))
then
Goto "#5"
else
locinfo: loc_32 ;
Goto "#6"
]> $
<[ "#3" :=
"entry" <-{ LPtr }
LocInfoE loc_25 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_25 (use{LPtr} (LocInfoE loc_26 ("data"))))) ;
locinfo: loc_5 ;
LocInfoE loc_20 ((LocInfoE loc_21 (!{LPtr} (LocInfoE loc_22 ("entry")))) at{struct_chunk} "size") <-{ it_layout size_t }
LocInfoE loc_23 (use{it_layout size_t} (LocInfoE loc_24 ("size"))) ;
locinfo: loc_6 ;
LocInfoE loc_13 ((LocInfoE loc_14 (!{LPtr} (LocInfoE loc_15 ("entry")))) at{struct_chunk} "next") <-{ LPtr }
LocInfoE loc_16 (use{LPtr} (LocInfoE loc_18 (!{LPtr} (LocInfoE loc_19 ("cur"))))) ;
locinfo: loc_7 ;
LocInfoE loc_9 (!{LPtr} (LocInfoE loc_10 ("cur"))) <-{ LPtr }
LocInfoE loc_11 (use{LPtr} (LocInfoE loc_12 ("entry"))) ;
Return (VOID)
]> $
<[ "#4" :=
locinfo: loc_32 ;
LocInfoE loc_35 ("cur") <-{ LPtr }
LocInfoE loc_36 (&(LocInfoE loc_37 ((LocInfoE loc_38 (!{LPtr} (LocInfoE loc_40 (!{LPtr} (LocInfoE loc_41 ("cur")))))) at{struct_chunk} "next"))) ;
locinfo: loc_33 ;
Goto "continue2"
]> $
<[ "#5" :=
Goto "#3"
]> $
<[ "#6" :=
locinfo: loc_32 ;
Goto "#4"
]> $
<[ "continue2" :=
locinfo: loc_3 ;
Goto "#1"
]> $∅
)%E
|}.
End code.
examples/proofs/paper_examples/generated_proof_free.v → examples/proofs/paper_example_2_2/generated_proof_free.v
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_examples Require Import generated_code.
From refinedc.examples.paper_examples Require Import generated_spec.
From refinedc.examples.paper_example_2_2 Require Import generated_code.
From refinedc.examples.paper_example_2_2 Require Import generated_spec.
From refinedc.examples.spinlock Require Import spinlock_def.
Set Default Proof Using "Type".
(* Generated from [examples/paper_examples.c]. *)
(* Generated from [examples/paper_example_2_2.c]. *)
Section proof_free.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
......@@ -13,16 +13,16 @@ Section proof_free.
Lemma type_free :
⊢ typed_function impl_free type_of_free.
Proof.
start_function "free" ([[s p] ly]) => arg_list arg_data arg_size local_cur local_entry.
start_function "free" ([[[s p] q] n]) => arg_list arg_data arg_size local_cur local_entry.
split_blocks ((
<[ "#1" :=
∃ cp : loc,
∃ cs : gmultiset layout,
arg_data ◁ₗ (&own (uninit (ly))) ∗
arg_size ◁ₗ ((ly.(ly_size)) @ (int (size_t))) ∗
∃ cs : gmultiset nat,
arg_data ◁ₗ (q @ (&own (uninit (n)))) ∗
arg_size ◁ₗ (n @ (int (size_t))) ∗
local_entry ◁ₗ uninit LPtr ∗
local_cur ◁ₗ (cp @ (&own (cs @ (chunks_t)))) ∗
arg_list ◁ₗ (p @ (&own (wand (cp ◁ₗ ({[ly]} ⊎ cs) @ chunks_t) (({[ly]} ⊎ s) @ (chunks_t)))))
arg_list ◁ₗ (p @ (&own (wand (cp ◁ₗ ({[n]} ⊎ cs) @ chunks_t) (({[n]} ⊎ s) @ (chunks_t)))))
]> $
∅
)%I : gmap label (iProp Σ)) ((
......
examples/proofs/paper_example_2_2/generated_spec.v 0 → 100644
View file @ f5ab0aad
From refinedc.typing Require Import typing.
From refinedc.examples.paper_example_2_2 Require Import generated_code.
From refinedc.examples.spinlock Require Import spinlock_def.
Set Default Proof Using "Type".
(* Generated from [examples/paper_example_2_2.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
Context `{!lockG Σ}.
(* Inlined code. *)
Definition layout_of_nat : nat → layout := ly_set_size struct_chunk.