Commit 36366a67 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Tweaks in [tagged_ptr.c].

parent 14fdc0df
Pipeline #49109 passed with stage
in 16 minutes and 20 seconds
This diff is collapsed.
......@@ -8,12 +8,11 @@ Section proof_tag.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [tag]. *)
Lemma type_tag (global_tag_of : loc) :
global_tag_of ◁ᵥ global_tag_of @ function_ptr type_of_tag_of -
typed_function (impl_tag global_tag_of) type_of_tag.
Lemma type_tag :
typed_function impl_tag type_of_tag.
Proof.
Open Scope printing_sugar.
start_function "tag" ([[r t] ty]) => arg_p arg_t local_old_t.
start_function "tag" ([[r t] ty]) => arg_p arg_t local_i local_new_i local_q.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -12,7 +12,7 @@ Section proof_tag_of.
typed_function impl_tag_of type_of_tag_of.
Proof.
Open Scope printing_sugar.
start_function "tag_of" ([[r ty] v]) => arg_p.
start_function "tag_of" ([[r ty] v]) => arg_p local_i local_t.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -6,8 +6,6 @@
#define TAG_MOD (1 << TAG_SIZE)
#define TAG_MASK (TAG_MOD - 1)
typedef unsigned char tag_t;
//@rc::inlined Notation TAG_MOD := (8%nat) (only parsing).
[[rc::parameters("r: {loc * Z}", "ty: type", "v: val")]]
......@@ -15,17 +13,21 @@ typedef unsigned char tag_t;
[[rc::requires("[type_alive_own ty]")]]
[[rc::returns("{r.2} @ int<u8>")]]
[[rc::ensures("v : r @ &tagged<TAG_MOD, ty>", "{0 ≤ r.2 < TAG_MOD}")]]
tag_t tag_of(void* p){
return ((uintptr_t) p) % TAG_MOD;
unsigned char tag_of(void* p){
uintptr_t i = (uintptr_t) p;
unsigned char t = i % TAG_MOD;
return t;
}
[[rc::parameters("r: {loc * Z}", "t: Z", "ty: type")]]
[[rc::args("r @ &tagged<TAG_MOD, ty>", "t @ int<u8>")]]
[[rc::requires("{0 ≤ t < TAG_MOD}", "[type_alive_own ty]")]]
[[rc::returns("{(r.1, t)} @ &tagged<TAG_MOD, ty>")]]
void* tag(void* p, tag_t t){
tag_t old_t = tag_of(p);
return rc_copy_alloc_id((uintptr_t) p - old_t + t, p);
void* tag(void* p, unsigned char t){
uintptr_t i = (uintptr_t) p;
uintptr_t new_i = i - i % TAG_MOD + t;
void* q = rc_copy_alloc_id(new_i, p);
return q;
}
[[rc::parameters("r: {loc * Z}", "ty: type")]]
......
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