Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
5a7b2bf6
Commit
5a7b2bf6
authored
Oct 06, 2021
by
Lennard Gäher
Committed by
Michael Sammler
Oct 06, 2021
Browse files
dynamic alloc/free
parent
13f33068
Pipeline
#55127
passed with stage
in 31 minutes and 45 seconds
Changes
7
Pipelines
8
Hide whitespace changes
Inline
Side-by-side
theories/lang/ghost_state.v
View file @
5a7b2bf6
...
...
@@ -22,8 +22,8 @@ Definition heapUR : ucmra :=
Class
heapG
Σ
:
=
HeapG
{
heap_heap_inG
:
>
inG
Σ
(
authR
heapUR
)
;
heap_heap_name
:
gname
;
heap_alloc_
range
_map_inG
:
>
ghost_mapG
Σ
alloc_id
(
Z
*
nat
)
;
heap_alloc_
range
_map_name
:
gname
;
heap_alloc_
meta
_map_inG
:
>
ghost_mapG
Σ
alloc_id
(
Z
*
nat
*
alloc_kind
)
;
heap_alloc_
meta
_map_name
:
gname
;
heap_alloc_alive_map_inG
:
>
ghost_mapG
Σ
alloc_id
bool
;
heap_alloc_alive_map_name
:
gname
;
heap_fntbl_inG
:
>
ghost_mapG
Σ
addr
function
;
...
...
@@ -39,11 +39,11 @@ Definition to_heap_cellR (hc : heap_cell) : heap_cellR :=
Definition
to_heapUR
:
heap
→
heapUR
:
=
fmap
to_heap_cellR
.
Definition
to_alloc_
range
R
(
al
:
allocation
)
:
(
Z
*
nat
)
:
=
(
al
.(
al_start
),
al
.(
al_len
)).
Definition
to_alloc_
meta
R
(
al
:
allocation
)
:
(
Z
*
nat
*
alloc_kind
)
:
=
(
al
.(
al_start
),
al
.(
al_len
)
,
al
.(
al_kind
)
).
Definition
to_alloc_
range
_map
:
allocs
→
gmap
alloc_id
(
Z
*
nat
)
:
=
fmap
to_alloc_
range
R
.
Definition
to_alloc_
meta
_map
:
allocs
→
gmap
alloc_id
(
Z
*
nat
*
alloc_kind
)
:
=
fmap
to_alloc_
meta
R
.
Definition
to_alloc_alive_map
:
allocs
→
gmap
alloc_id
bool
:
=
fmap
al_alive
.
...
...
@@ -53,20 +53,20 @@ Section definitions.
(** * Allocation stuff. *)
(** [alloc_
range
id al] persistently records the information that allocation
(** [alloc_
meta
id al] persistently records the information that allocation
with identifier [id] has a range corresponding to that of [a]. *)
Definition
alloc_
range
_def
(
id
:
alloc_id
)
(
al
:
allocation
)
:
iProp
Σ
:
=
id
↪
[
heap_alloc_
range
_map_name
]
□
to_alloc_
range
R
al
.
Definition
alloc_
range
_aux
:
seal
(@
alloc_
range
_def
).
by
eexists
.
Qed
.
Definition
alloc_
range
:
=
unseal
alloc_
range
_aux
.
Definition
alloc_
range
_eq
:
@
alloc_
range
=
@
alloc_
range
_def
:
=
seal_eq
alloc_
range
_aux
.
Definition
alloc_
meta
_def
(
id
:
alloc_id
)
(
al
:
allocation
)
:
iProp
Σ
:
=
id
↪
[
heap_alloc_
meta
_map_name
]
□
to_alloc_
meta
R
al
.
Definition
alloc_
meta
_aux
:
seal
(@
alloc_
meta
_def
).
by
eexists
.
Qed
.
Definition
alloc_
meta
:
=
unseal
alloc_
meta
_aux
.
Definition
alloc_
meta
_eq
:
@
alloc_
meta
=
@
alloc_
meta
_def
:
=
seal_eq
alloc_
meta
_aux
.
Global
Instance
allocs_range_pers
id
al
:
Persistent
(
alloc_
range
id
al
).
Proof
.
rewrite
alloc_
range
_eq
.
by
apply
_
.
Qed
.
Global
Instance
allocs_range_pers
id
al
:
Persistent
(
alloc_
meta
id
al
).
Proof
.
rewrite
alloc_
meta
_eq
.
by
apply
_
.
Qed
.
Global
Instance
allocs_range_tl
id
al
:
Timeless
(
alloc_
range
id
al
).
Proof
.
rewrite
alloc_
range
_eq
.
by
apply
_
.
Qed
.
Global
Instance
allocs_range_tl
id
al
:
Timeless
(
alloc_
meta
id
al
).
Proof
.
rewrite
alloc_
meta
_eq
.
by
apply
_
.
Qed
.
(** [loc_in_bounds l n] persistently records the information that location
[l] and any of its positive offset up to [n] (included) are in range of the
...
...
@@ -75,7 +75,7 @@ Section definitions.
Definition
loc_in_bounds_def
(
l
:
loc
)
(
n
:
nat
)
:
iProp
Σ
:
=
∃
(
id
:
alloc_id
)
(
al
:
allocation
),
⌜
l
.
1
=
ProvAlloc
(
Some
id
)
⌝
∗
⌜
al
.(
al_start
)
≤
l
.
2
⌝
∗
⌜
l
.
2
+
n
≤
al_end
al
⌝
∗
⌜
allocation_in_range
al
⌝
∗
alloc_
range
id
al
.
⌜
allocation_in_range
al
⌝
∗
alloc_
meta
id
al
.
Definition
loc_in_bounds_aux
:
seal
(@
loc_in_bounds_def
).
by
eexists
.
Qed
.
Definition
loc_in_bounds
:
=
unseal
loc_in_bounds_aux
.
Definition
loc_in_bounds_eq
:
@
loc_in_bounds
=
@
loc_in_bounds_def
:
=
...
...
@@ -156,8 +156,8 @@ Section definitions.
(** * Freeable *)
Definition
freeable_def
(
l
:
loc
)
(
n
:
nat
)
:
iProp
Σ
:
=
∃
id
,
⌜
l
.
1
=
ProvAlloc
(
Some
id
)
⌝
∗
alloc_
range
id
{|
al_start
:
=
l
.
2
;
al_len
:
=
n
;
al_alive
:
=
true
|}
∗
Definition
freeable_def
(
l
:
loc
)
(
n
:
nat
)
(
k
:
alloc_kind
)
:
iProp
Σ
:
=
∃
id
,
⌜
l
.
1
=
ProvAlloc
(
Some
id
)
⌝
∗
alloc_
meta
id
{|
al_start
:
=
l
.
2
;
al_len
:
=
n
;
al_alive
:
=
true
;
al_kind
:
=
k
|}
∗
alloc_alive
id
(
DfracOwn
1
)
true
.
Definition
freeable_aux
:
seal
(@
freeable_def
).
by
eexists
.
Qed
.
Definition
freeable
:
=
unseal
freeable_aux
.
...
...
@@ -169,8 +169,8 @@ Section definitions.
Definition
heap_ctx
(
h
:
heap
)
:
iProp
Σ
:
=
own
heap_heap_name
(
●
to_heapUR
h
).
Definition
alloc_
range
_ctx
(
ub
:
allocs
)
:
iProp
Σ
:
=
ghost_map_auth
heap_alloc_
range
_map_name
1
(
to_alloc_
range
_map
ub
).
Definition
alloc_
meta
_ctx
(
ub
:
allocs
)
:
iProp
Σ
:
=
ghost_map_auth
heap_alloc_
meta
_map_name
1
(
to_alloc_
meta
_map
ub
).
Definition
alloc_alive_ctx
(
ub
:
allocs
)
:
iProp
Σ
:
=
ghost_map_auth
heap_alloc_alive_map_name
1
(
to_alloc_alive_map
ub
).
...
...
@@ -181,7 +181,7 @@ Section definitions.
Definition
heap_state_ctx
(
st
:
heap_state
)
:
iProp
Σ
:
=
⌜
heap_state_invariant
st
⌝
∗
heap_ctx
st
.(
hs_heap
)
∗
alloc_
range
_ctx
st
.(
hs_allocs
)
∗
alloc_
meta
_ctx
st
.(
hs_allocs
)
∗
alloc_alive_ctx
st
.(
hs_allocs
).
Definition
state_ctx
(
σ
:
state
)
:
iProp
Σ
:
=
...
...
@@ -241,68 +241,70 @@ Section fntbl.
Qed
.
End
fntbl
.
Section
alloc_
range
.
Section
alloc_
meta
.
Context
`
{!
heapG
Σ
}.
Implicit
Types
am
:
allocs
.
Lemma
alloc_
range
_mono
id
a1
a2
:
Lemma
alloc_
meta
_mono
id
a1
a2
:
alloc_same_range
a1
a2
→
alloc_range
id
a1
-
∗
alloc_range
id
a2
.
Proof
.
destruct
a1
as
[???],
a2
as
[???]
=>
-[/=
<-
<-].
by
rewrite
alloc_range_eq
.
Qed
.
a1
.(
al_kind
)
=
a2
.(
al_kind
)
→
alloc_meta
id
a1
-
∗
alloc_meta
id
a2
.
Proof
.
destruct
a1
as
[????],
a2
as
[????]
=>
-[/=
<-
<-]
<-.
by
rewrite
alloc_meta_eq
.
Qed
.
Lemma
alloc_
range
_agree
id
a1
a2
:
alloc_
range
id
a1
-
∗
alloc_
range
id
a2
-
∗
⌜
alloc_same_range
a1
a2
⌝
.
Lemma
alloc_
meta
_agree
id
a1
a2
:
alloc_
meta
id
a1
-
∗
alloc_
meta
id
a2
-
∗
⌜
alloc_same_range
a1
a2
⌝
.
Proof
.
destruct
a1
as
[???],
a2
as
[???].
rewrite
alloc_
range
_eq
/
alloc_same_range
.
destruct
a1
as
[???
?
],
a2
as
[???
?
].
rewrite
alloc_
meta
_eq
/
alloc_same_range
.
iIntros
"H1 H2"
.
by
iDestruct
(
ghost_map_elem_agree
with
"H1 H2"
)
as
%[=->->].
Qed
.
Lemma
alloc_
range
_alloc
am
id
al
:
Lemma
alloc_
meta
_alloc
am
id
al
:
am
!!
id
=
None
→
alloc_
range
_ctx
am
==
∗
alloc_
range
_ctx
(<[
id
:
=
al
]>
am
)
∗
alloc_
range
id
al
.
alloc_
meta
_ctx
am
==
∗
alloc_
meta
_ctx
(<[
id
:
=
al
]>
am
)
∗
alloc_
meta
id
al
.
Proof
.
move
=>
Hid
.
rewrite
alloc_
range
_eq
.
iIntros
"Hctx"
.
move
=>
Hid
.
rewrite
alloc_
meta
_eq
.
iIntros
"Hctx"
.
iMod
(
ghost_map_insert_persist
with
"Hctx"
)
as
"[? $]"
.
{
by
rewrite
lookup_fmap
fmap_None
.
}
by
rewrite
-
fmap_insert
.
Qed
.
Lemma
alloc_
range
_to_loc_in_bounds
l
id
(
n
:
nat
)
al
:
Lemma
alloc_
meta
_to_loc_in_bounds
l
id
(
n
:
nat
)
al
:
l
.
1
=
ProvAlloc
(
Some
id
)
→
al
.(
al_start
)
≤
l
.
2
∧
l
.
2
+
n
≤
al_end
al
→
allocation_in_range
al
→
alloc_
range
id
al
-
∗
loc_in_bounds
l
n
.
alloc_
meta
id
al
-
∗
loc_in_bounds
l
n
.
Proof
.
iIntros
(?[??]?)
"Hr"
.
rewrite
loc_in_bounds_eq
.
iExists
id
,
al
.
by
iFrame
"Hr"
.
Qed
.
Lemma
alloc_
range
_lookup
am
id
al
:
alloc_
range
_ctx
am
-
∗
alloc_
range
id
al
-
∗
⌜
∃
al'
,
am
!!
id
=
Some
al'
∧
alloc_same_range
al
al'
⌝
.
Lemma
alloc_
meta
_lookup
am
id
al
:
alloc_
meta
_ctx
am
-
∗
alloc_
meta
id
al
-
∗
⌜
∃
al'
,
am
!!
id
=
Some
al'
∧
alloc_same_range
al
al'
∧
al
.(
al_kind
)
=
al'
.(
al_kind
)
⌝
.
Proof
.
rewrite
alloc_
range
_eq
.
iIntros
"Htbl Hf"
.
rewrite
alloc_
meta
_eq
.
iIntros
"Htbl Hf"
.
iDestruct
(
ghost_map_lookup
with
"Htbl Hf"
)
as
%
Hlookup
.
iPureIntro
.
move
:
Hlookup
.
rewrite
lookup_fmap
fmap_Some
=>
-[[???][?[??]]].
iPureIntro
.
move
:
Hlookup
.
rewrite
lookup_fmap
fmap_Some
=>
-[[???
?
][?[??
?
]]].
by
eexists
_
.
Qed
.
Lemma
alloc_
range
_ctx_same_range
am
id
al1
al2
:
Lemma
alloc_
meta
_ctx_same_range
am
id
al1
al2
:
am
!!
id
=
Some
al1
→
alloc_same_range
al1
al2
→
alloc_range_ctx
am
=
alloc_range_ctx
(<[
id
:
=
al2
]>
am
).
al1
.(
al_kind
)
=
al2
.(
al_kind
)
→
alloc_meta_ctx
am
=
alloc_meta_ctx
(<[
id
:
=
al2
]>
am
).
Proof
.
move
=>
Hid
[
Heq1
Heq2
].
rewrite
/
alloc_
range
_ctx
/
to_alloc_
range
_map
fmap_insert
insert_id
;
first
done
.
move
=>
Hid
[
Heq1
Heq2
]
Heq3
.
rewrite
/
alloc_
meta
_ctx
/
to_alloc_
meta
_map
fmap_insert
insert_id
;
first
done
.
rewrite
lookup_fmap
Hid
/=.
destruct
al1
,
al2
;
naive_solver
.
Qed
.
Lemma
alloc_
range
_ctx_killed
am
id
al
:
Lemma
alloc_
meta
_ctx_killed
am
id
al
:
am
!!
id
=
Some
al
→
alloc_
range
_ctx
am
=
alloc_
range
_ctx
(<[
id
:
=
killed
al
]>
am
).
Proof
.
move
=>
?.
by
apply
:
alloc_
range
_ctx_same_range
.
Qed
.
End
alloc_
range
.
alloc_
meta
_ctx
am
=
alloc_
meta
_ctx
(<[
id
:
=
killed
al
]>
am
).
Proof
.
move
=>
?.
by
apply
:
alloc_
meta
_ctx_same_range
.
Qed
.
End
alloc_
meta
.
Section
alloc_alive
.
Context
`
{!
heapG
Σ
}.
...
...
@@ -349,7 +351,7 @@ Section loc_in_bounds.
iDestruct
"H2"
as
(??
Hl2
?
Hend
?)
"#H2"
.
move
:
Hl1
Hl2
=>
/=
Hl1
Hl2
.
iExists
id
,
al
.
destruct
l
.
unfold
al_end
in
*.
simpl
in
*.
simplify_eq
.
iDestruct
(
alloc_
range
_agree
with
"H2 H1"
)
as
%[?
<-].
iDestruct
(
alloc_
meta
_agree
with
"H2 H1"
)
as
%[?
<-].
iFrame
"H1"
.
iPureIntro
.
rewrite
/
shift_loc
/=
in
Hend
.
naive_solver
lia
.
-
iIntros
"H"
.
iDestruct
"H"
as
(
id
al
????)
"#H"
.
iSplit
;
iExists
id
,
al
;
iFrame
"H"
;
iPureIntro
;
split_and
!
=>
//=
;
lia
.
...
...
@@ -387,7 +389,7 @@ Section loc_in_bounds.
Proof
.
rewrite
loc_in_bounds_eq
.
iIntros
"Hb ((?&?&Hctx&?)&?)"
.
iDestruct
"Hb"
as
(
id
al
????)
"Hb"
.
iDestruct
(
alloc_
range
_lookup
with
"Hctx Hb"
)
as
%[
al'
[?[
?
?]]].
iDestruct
(
alloc_
meta
_lookup
with
"Hctx Hb"
)
as
%[
al'
[?[
[??]
?]]].
iExists
id
,
al'
.
iPureIntro
.
unfold
allocation_in_range
,
al_end
in
*.
naive_solver
lia
.
Qed
.
...
...
@@ -524,6 +526,10 @@ Section heap.
by
iDestruct
(
heap_mapsto_mbyte_agree
with
"[$]"
)
as
%->.
Qed
.
Lemma
heap_mapsto_layout_has_layout
l
ly
:
l
↦
|
ly
|
-
∗
⌜
l
`
has_layout_loc
`
ly
⌝
.
Proof
.
iIntros
"(% & % & % & ?)"
.
done
.
Qed
.
Lemma
heap_alloc_st
l
h
v
aid
:
l
.
1
=
ProvAlloc
(
Some
aid
)
→
heap_range_free
h
l
.
2
(
length
v
)
→
...
...
@@ -555,12 +561,12 @@ Section heap.
al
.(
al_start
)
=
l
.
2
→
al
.(
al_len
)
=
length
v
→
allocation_in_range
al
→
alloc_
range
id
al
-
∗
alloc_
meta
id
al
-
∗
alloc_alive
id
(
DfracOwn
1
)
true
-
∗
heap_ctx
h
==
∗
heap_ctx
(
heap_alloc
l
.
2
v
id
h
)
∗
l
↦
v
∗
freeable
l
(
length
v
).
freeable
l
(
length
v
)
al
.(
al_kind
)
.
Proof
.
iIntros
(
Hid
Hfree
Hstart
Hlen
Hrange
)
"#Hr Hal Hctx"
.
iMod
(
heap_alloc_st
with
"Hctx"
)
as
"[$ Hl]"
=>
//.
...
...
@@ -568,7 +574,7 @@ Section heap.
rewrite
heap_mapsto_mbyte_eq
/
heap_mapsto_mbyte_def
.
iSplitR
"Hal"
;
last
first
;
last
iSplit
.
-
rewrite
freeable_eq
.
iExists
id
.
iFrame
.
iSplit
=>
//.
by
iApply
(
alloc_
range
_mono
with
"Hr"
).
by
iApply
(
alloc_
meta
_mono
with
"Hr"
).
-
rewrite
loc_in_bounds_eq
.
iExists
id
,
al
.
iFrame
"Hr"
.
rewrite
/
al_end
.
iPureIntro
.
naive_solver
lia
.
-
iApply
(
big_sepL_impl
with
"Hl"
).
...
...
@@ -839,25 +845,25 @@ End alloc_alive.
Section
alloc_new_blocks
.
Context
`
{!
heapG
Σ
}.
Lemma
heap_alloc_new_block_upd
σ
1
l
v
σ
2
:
alloc_new_block
σ
1
l
v
σ
2
→
heap_state_ctx
σ
1
==
∗
heap_state_ctx
σ
2
∗
l
↦
v
∗
freeable
l
(
length
v
).
Lemma
heap_alloc_new_block_upd
σ
1
l
v
kind
σ
2
:
alloc_new_block
σ
1
kind
l
v
σ
2
→
heap_state_ctx
σ
1
==
∗
heap_state_ctx
σ
2
∗
l
↦
v
∗
freeable
l
(
length
v
)
kind
.
Proof
.
move
=>
[]
;
clear
.
move
=>
σ
l
aid
v
alloc
Haid
???
;
subst
alloc
.
move
=>
[]
;
clear
.
move
=>
σ
l
aid
kind
v
alloc
Haid
???
;
subst
alloc
.
iIntros
"Hctx"
.
iDestruct
"Hctx"
as
(
Hinv
)
"(Hhctx&Hrctx&Hsctx)"
.
iMod
(
alloc_
range
_alloc
with
"Hrctx"
)
as
"[$ #Hb]"
=>
//.
iMod
(
alloc_
meta
_alloc
with
"Hrctx"
)
as
"[$ #Hb]"
=>
//.
iMod
(
alloc_alive_alloc
with
"Hsctx"
)
as
"[$ Hs]"
=>
//.
iDestruct
(
alloc_
range
_to_loc_in_bounds
l
aid
(
length
v
)
with
"[Hb]"
)
iDestruct
(
alloc_
meta
_to_loc_in_bounds
l
aid
(
length
v
)
with
"[Hb]"
)
as
"#Hinb"
=>
//
;
[
done
|..].
iMod
(
heap_alloc
with
"Hb Hs Hhctx"
)
as
"[Hhctx [Hv Hal]]"
=>
//.
iModIntro
.
iFrame
.
iPureIntro
.
by
eapply
alloc_new_block_invariant
.
Qed
.
Lemma
heap_alloc_new_blocks_upd
σ
1
ls
vs
σ
2
:
alloc_new_blocks
σ
1
ls
vs
σ
2
→
Lemma
heap_alloc_new_blocks_upd
σ
1
ls
vs
kind
σ
2
:
alloc_new_blocks
σ
1
kind
ls
vs
σ
2
→
heap_state_ctx
σ
1
==
∗
heap_state_ctx
σ
2
∗
[
∗
list
]
l
;
v
∈
ls
;
vs
,
l
↦
v
∗
freeable
l
(
length
v
).
[
∗
list
]
l
;
v
∈
ls
;
vs
,
l
↦
v
∗
freeable
l
(
length
v
)
kind
.
Proof
.
move
=>
alloc
.
iInduction
alloc
as
[
σ
|]
"IH"
;
first
by
iIntros
"$ !>"
.
iIntros
"Hσ"
.
...
...
@@ -869,27 +875,27 @@ End alloc_new_blocks.
Section
free_blocks
.
Context
`
{!
heapG
Σ
}.
Lemma
heap_free_block_upd
σ
1
l
ly
:
Lemma
heap_free_block_upd
σ
1
l
ly
kind
:
l
↦
|
ly
|
-
∗
freeable
l
(
ly_size
ly
)
-
∗
heap_state_ctx
σ
1
==
∗
∃
σ
2
,
⌜
free_block
σ
1
l
ly
σ
2
⌝
∗
heap_state_ctx
σ
2
.
freeable
l
(
ly_size
ly
)
kind
-
∗
heap_state_ctx
σ
1
==
∗
∃
σ
2
,
⌜
free_block
σ
1
kind
l
ly
σ
2
⌝
∗
heap_state_ctx
σ
2
.
Proof
.
iIntros
"Hl Hfree (Hinv&Hhctx&Hrctx&Hsctx)"
.
iDestruct
"Hinv"
as
%
Hinv
.
rewrite
freeable_eq
.
iDestruct
"Hfree"
as
(
aid
Haid
)
"[#Hrange Hkill]"
.
iDestruct
"Hl"
as
(
v
Hv
?)
"Hl"
.
iDestruct
(
alloc_alive_lookup
with
"Hsctx Hkill"
)
as
%[[???]
[??]].
iDestruct
(
alloc_
range
_lookup
with
"Hrctx Hrange"
)
as
%[
al''
[?[
?
?]]].
simplify_eq
/=.
iDestruct
(
alloc_alive_lookup
with
"Hsctx Hkill"
)
as
%[[???
?k
]
[??]].
iDestruct
(
alloc_
meta
_lookup
with
"Hrctx Hrange"
)
as
%[
al''
[?[
[??]
?]]].
simplify_eq
/=.
iDestruct
(
heap_mapsto_lookup_1
(
λ
st
:
lock_state
,
st
=
RSt
0
)
with
"Hhctx Hl"
)
as
%?
=>
//.
iExists
_
.
iSplitR
.
{
iPureIntro
.
by
econstructor
.
}
iMod
(
heap_free_free
with
"Hhctx Hl"
)
as
"Hhctx"
.
rewrite
Hv
.
iFrame
=>
/=.
iMod
(
alloc_alive_kill
_
_
({|
al_start
:
=
l
.
2
;
al_len
:
=
ly_size
ly
;
al_alive
:
=
true
|})
with
"Hsctx Hkill"
)
as
"[$ Hd]"
.
erewrite
alloc_
range
_ctx_same_range
;
[
iFrame
|
done
..].
iMod
(
alloc_alive_kill
_
_
({|
al_start
:
=
l
.
2
;
al_len
:
=
ly_size
ly
;
al_alive
:
=
true
;
al_kind
:
=
k
|})
with
"Hsctx Hkill"
)
as
"[$ Hd]"
.
erewrite
alloc_
meta
_ctx_same_range
;
[
iFrame
|
done
..].
iPureIntro
.
eapply
free_block_invariant
=>
//.
by
eapply
FreeBlock
.
Qed
.
Lemma
heap_free_blocks_upd
ls
σ
1
:
([
∗
list
]
l
∈
ls
,
l
.
1
↦
|
l
.
2
|
∗
freeable
l
.
1
(
ly_size
l
.
2
))
-
∗
heap_state_ctx
σ
1
==
∗
∃
σ
2
,
⌜
free_blocks
σ
1
ls
σ
2
⌝
∗
heap_state_ctx
σ
2
.
Lemma
heap_free_blocks_upd
ls
σ
1
kind
:
([
∗
list
]
l
∈
ls
,
l
.
1
↦
|
l
.
2
|
∗
freeable
l
.
1
(
ly_size
l
.
2
)
kind
)
-
∗
heap_state_ctx
σ
1
==
∗
∃
σ
2
,
⌜
free_blocks
σ
1
kind
ls
σ
2
⌝
∗
heap_state_ctx
σ
2
.
Proof
.
iInduction
ls
as
[|[
l
ly
]
ls
]
"IH"
forall
(
σ
1
).
{
iIntros
"_ ? !>"
.
iExists
σ
1
.
iFrame
.
iPureIntro
.
by
constructor
.
}
...
...
theories/lang/heap.v
View file @
5a7b2bf6
...
...
@@ -185,11 +185,18 @@ Qed.
(** ** Representation of allocations. *)
(** An allocation can either be a stack allocation or a heap allocation. *)
Inductive
alloc_kind
:
Set
:
=
|
HeapAlloc
|
StackAlloc
|
GlobalAlloc
.
Record
allocation
:
=
Allocation
{
al_start
:
Z
;
(* First valid address. *)
al_len
:
nat
;
(* Number of allocated byte. *)
al_alive
:
bool
;
(* Is the allocation still alive. *)
al_start
:
Z
;
(* First valid address. *)
al_len
:
nat
;
(* Number of allocated byte. *)
al_alive
:
bool
;
(* Is the allocation still alive. *)
al_kind
:
alloc_kind
;
(* On the heap or on the stack? *)
}.
Definition
al_end
(
al
:
allocation
)
:
Z
:
=
...
...
@@ -201,7 +208,7 @@ Definition alloc_same_range (al1 al2 : allocation) : Prop :=
al1
.(
al_start
)
=
al2
.(
al_start
)
∧
al1
.(
al_len
)
=
al2
.(
al_len
).
Definition
killed
(
al
:
allocation
)
:
allocation
:
=
{|
al_start
:
=
al
.(
al_start
)
;
al_len
:
=
al
.(
al_len
)
;
al_alive
:
=
false
;
|}.
{|
al_start
:
=
al
.(
al_start
)
;
al_len
:
=
al
.(
al_len
)
;
al_alive
:
=
false
;
al_kind
:
=
al
.(
al_kind
)
|}.
(** Smallest allocatable address (we reserve 0 for NULL). *)
Definition
min_alloc_start
:
Z
:
=
1
.
...
...
@@ -262,6 +269,8 @@ Proof. rewrite /valid_ptr => ?. apply: heap_state_loc_in_bounds_has_alloc_id. na
Definition
addr_in_range_alloc
(
a
:
addr
)
(
aid
:
alloc_id
)
(
st
:
heap_state
)
:
Prop
:
=
∃
alloc
,
st
.(
hs_allocs
)
!!
aid
=
Some
alloc
∧
a
∈
alloc
.
Global
Instance
alloc_kind_eq_dec
:
EqDecision
alloc_kind
.
Proof
.
solve_decision
.
Qed
.
Global
Instance
allocation_eq_dec
:
EqDecision
(
allocation
).
Proof
.
solve_decision
.
Qed
.
Global
Instance
alloc_id_alive_dec
aid
st
:
Decision
(
alloc_id_alive
aid
st
).
...
...
@@ -474,57 +483,57 @@ Arguments mem_cast : simpl never.
(** ** Allocation and deallocation. *)
Inductive
alloc_new_block
:
heap_state
→
loc
→
val
→
heap_state
→
Prop
:
=
|
AllocNewBlock
σ
l
aid
v
:
let
alloc
:
=
Allocation
l
.
2
(
length
v
)
true
in
Inductive
alloc_new_block
:
heap_state
→
alloc_kind
→
loc
→
val
→
heap_state
→
Prop
:
=
|
AllocNewBlock
σ
l
aid
kind
v
:
let
alloc
:
=
Allocation
l
.
2
(
length
v
)
true
kind
in
l
.
1
=
ProvAlloc
(
Some
aid
)
→
σ
.(
hs_allocs
)
!!
aid
=
None
→
allocation_in_range
alloc
→
heap_range_free
σ
.(
hs_heap
)
l
.
2
(
length
v
)
→
alloc_new_block
σ
l
v
{|
alloc_new_block
σ
kind
l
v
{|
hs_heap
:
=
heap_alloc
l
.
2
v
aid
σ
.(
hs_heap
)
;
hs_allocs
:
=
<[
aid
:
=
alloc
]>
σ
.(
hs_allocs
)
;
|}.
Inductive
alloc_new_blocks
:
heap_state
→
list
loc
→
list
val
→
heap_state
→
Prop
:
=
|
AllocNewBlock_nil
σ
:
alloc_new_blocks
σ
[]
[]
σ
|
AllocNewBlock_cons
σ
σ
'
σ
''
l
v
ls
vs
:
alloc_new_block
σ
l
v
σ
'
→
alloc_new_blocks
σ
'
ls
vs
σ
''
→
alloc_new_blocks
σ
(
l
::
ls
)
(
v
::
vs
)
σ
''
.
Inductive
free_block
:
heap_state
→
loc
→
layout
→
heap_state
→
Prop
:
=
|
FreeBlock
σ
l
aid
ly
v
:
let
al_alive
:
=
Allocation
l
.
2
ly
.(
ly_size
)
true
in
let
al_dead
:
=
Allocation
l
.
2
ly
.(
ly_size
)
false
in
Inductive
alloc_new_blocks
:
heap_state
→
alloc_kind
→
list
loc
→
list
val
→
heap_state
→
Prop
:
=
|
AllocNewBlock_nil
σ
kind
:
alloc_new_blocks
σ
kind
[]
[]
σ
|
AllocNewBlock_cons
σ
σ
'
σ
''
l
v
ls
kind
vs
:
alloc_new_block
σ
kind
l
v
σ
'
→
alloc_new_blocks
σ
'
kind
ls
vs
σ
''
→
alloc_new_blocks
σ
kind
(
l
::
ls
)
(
v
::
vs
)
σ
''
.
Inductive
free_block
:
heap_state
→
alloc_kind
→
loc
→
layout
→
heap_state
→
Prop
:
=
|
FreeBlock
σ
l
aid
ly
kind
v
:
let
al_alive
:
=
Allocation
l
.
2
ly
.(
ly_size
)
true
kind
in
let
al_dead
:
=
Allocation
l
.
2
ly
.(
ly_size
)
false
kind
in
l
.
1
=
ProvAlloc
(
Some
aid
)
→
σ
.(
hs_allocs
)
!!
aid
=
Some
al_alive
→
length
v
=
ly
.(
ly_size
)
→
heap_lookup_loc
l
v
(
λ
st
,
st
=
RSt
0
%
nat
)
σ
.(
hs_heap
)
→
free_block
σ
l
ly
{|
free_block
σ
kind
l
ly
{|
hs_heap
:
=
heap_free
l
.
2
ly
.(
ly_size
)
σ
.(
hs_heap
)
;
hs_allocs
:
=
<[
aid
:
=
al_dead
]>
σ
.(
hs_allocs
)
;
|}.
Inductive
free_blocks
:
heap_state
→
list
(
loc
*
layout
)
→
heap_state
→
Prop
:
=
|
FreeBlocks_nil
σ
:
free_blocks
σ
[]
σ
|
FreeBlocks_cons
σ
σ
'
σ
''
l
ly
ls
:
free_block
σ
l
ly
σ
'
→
free_blocks
σ
'
ls
σ
''
→
free_blocks
σ
((
l
,
ly
)
::
ls
)
σ
''
.
Inductive
free_blocks
:
heap_state
→
alloc_kind
→
list
(
loc
*
layout
)
→
heap_state
→
Prop
:
=
|
FreeBlocks_nil
σ
kind
:
free_blocks
σ
kind
[]
σ
|
FreeBlocks_cons
σ
σ
'
σ
''
l
ly
kind
ls
:
free_block
σ
kind
l
ly
σ
'
→
free_blocks
σ
'
kind
ls
σ
''
→
free_blocks
σ
kind
((
l
,
ly
)
::
ls
)
σ
''
.
Lemma
free_block_inj
hs
l
ly
hs1
hs2
:
free_block
hs
l
ly
hs1
→
free_block
hs
l
ly
hs2
→
hs1
=
hs2
.
Lemma
free_block_inj
hs
l
ly
kind
hs1
hs2
:
free_block
hs
kind
l
ly
hs1
→
free_block
hs
kind
l
ly
hs2
→
hs1
=
hs2
.
Proof
.
destruct
l
.
inversion
1
;
simplify_eq
.
by
inversion
1
;
simplify_eq
/=.
Qed
.
Lemma
free_blocks_inj
hs1
hs2
hs
ls
:
free_blocks
hs
ls
hs1
→
free_blocks
hs
ls
hs2
→
hs1
=
hs2
.
Lemma
free_blocks_inj
hs1
hs2
hs
kind
ls
:
free_blocks
hs
kind
ls
hs1
→
free_blocks
hs
kind
ls
hs2
→
hs1
=
hs2
.
Proof
.
move
Heq
:
{
1
}(
hs
)
=>
hs'
Hb
.
elim
:
Hb
hs
Heq
.
{
move
=>
??
->.
by
inversion
1
.
}
move
=>
??????
Hb1
?
IH
??.
elim
:
Hb
hs
Heq
.
{
move
=>
??
?
->.
by
inversion
1
.
}
move
=>
??????
?
Hb1
?
IH
??.
inversion
1
;
simplify_eq
.
apply
:
IH
;
[|
done
].
by
apply
:
free_block_inj
.
Qed
.
...
...
@@ -580,25 +589,25 @@ Definition heap_state_invariant (st : heap_state) : Prop :=
(** ** Lemmas about the heap state invariant. *)
Lemma
heap_state_alloc_alive_free_disjoint
σ
id
a
n
b
alloc
:
Lemma
heap_state_alloc_alive_free_disjoint
σ
id
a
n
b
kind
alloc
:
heap_state_alloc_alive_in_heap
σ
→
alloc_id_alive
id
σ
→
heap_range_free
σ
.(
hs_heap
)
a
n
→
σ
.(
hs_allocs
)
!!
id
=
Some
alloc
→
Allocation
a
n
b
##
alloc
.
Allocation
a
n
b
kind
##
alloc
.
Proof
.
move
=>
Hin_heap
Halive
Hfree
Hal
p
Hp1
Hp2
.
apply
(
Hin_heap
_
_
Hal
Halive
)
in
Hp2
as
[?
Hp2
].
rewrite
Hfree
in
Hp2
;
first
done
.
apply
Hp1
.
Qed
.
Lemma
alloc_new_block_invariant
σ
1
σ
2
l
v
:
alloc_new_block
σ
1
l
v
σ
2
→
Lemma
alloc_new_block_invariant
σ
1
σ
2
l
v
kind
:
alloc_new_block
σ
1
kind
l
v
σ
2
→
heap_state_invariant
σ
1
→
heap_state_invariant
σ
2
.
Proof
.
move
=>
[]
;
clear
.
move
=>
σ
1
l
aid
v
alloc
Haid
Hfresh
Halloc
Hrange
H
.
move
=>
σ
1
l
aid
kind
v
alloc
Haid
Hfresh
Halloc
Hrange
H
.
destruct
H
as
(
Hi1
&
Hi2
&
Hi3
&
Hi4
&
Hi5
).
split_and
!.
-
move
=>
a
[
id
??]
/=
Ha
.
destruct
(
decide
(
aid
=
id
))
as
[->|
Hne
].
+
exists
alloc
.
split
=>
/=
;
first
by
rewrite
lookup_insert
.
...
...
@@ -650,22 +659,22 @@ Proof.
eapply
(
Hi5
_
_
Hal
)
;
[
by
eexists
|
done
|..].
Qed
.
Lemma
alloc_new_blocks_invariant
σ
1
σ
2
ls
vs
:
alloc_new_blocks
σ
1
ls
vs
σ
2
→
Lemma
alloc_new_blocks_invariant
σ
1
σ
2
ls
vs
kind
:
alloc_new_blocks
σ
1
kind
ls
vs
σ
2
→
heap_state_invariant
σ
1
→
heap_state_invariant
σ
2
.
Proof
.
elim
=>
[]
//
???????
Hb
Hbs
IH
H
.
elim
=>
[]
//
???????
?
Hb
Hbs
IH
H
.
apply
IH
.
by
eapply
alloc_new_block_invariant
.
Qed
.
Lemma
free_block_invariant
σ
1
σ
2
l
ly
:
free_block
σ
1
l
ly
σ
2
→
Lemma
free_block_invariant
σ
1
σ
2
l
ly
kind
:
free_block
σ
1
kind
l
ly
σ
2
→
heap_state_invariant
σ
1
→
heap_state_invariant
σ
2
.
Proof
.
move
=>
[]
;
clear
.
move
=>
σ
l
aid
ly
v
al_a
al_d
Haid
Hal_a
Hlen
Hlookup
H
.
move
=>
σ
l
aid
ly
kind
v
al_a
al_d
Haid
Hal_a
Hlen
Hlookup
H
.
destruct
H
as
(
Hi1
&
Hi2
&
Hi3
&
Hi4
&
Hi5
).
split_and
!.
-
move
=>
a
hc
/=
Hhc
.
assert
(
¬
(
l
.
2
≤
a
<
l
.
2
+
length
v
))
as
Hnot_in
.
...
...
@@ -712,12 +721,12 @@ Proof.
erewrite
elem_of_disjoint
in
Hdisj
.
by
eapply
Hdisj
.
Qed
.
Lemma
free_blocks_invariant
σ
1
σ
2
ls
:
free_blocks
σ
1
ls
σ
2
→
Lemma
free_blocks_invariant
σ
1
σ
2
ls
kind
:
free_blocks
σ
1
kind
ls
σ
2
→
heap_state_invariant
σ
1
→
heap_state_invariant
σ
2
.
Proof
.
elim
=>
[]
//
??????
Hb
Hbs
IH
H
.
elim
=>
[]
//
??????
?
Hb
Hbs
IH
H
.
apply
IH
.
by
eapply
free_block_invariant
.
Qed
.
...
...
theories/lang/lang.v
View file @
5a7b2bf6
...
...
@@ -37,6 +37,7 @@ Inductive expr :=
|
Call
(
f
:
expr
)
(
args
:
list
expr
)
|
Concat
(
es
:
list
expr
)
|
IfE
(
ot
:
op_type
)
(
e1
e2
e3
:
expr
)
|
Alloc
(
ly
:
layout
)
(
e
:
expr
)
|
SkipE
(
e
:
expr
)
|
StuckE
(* stuck expression *)
.
...
...
@@ -53,6 +54,7 @@ Lemma expr_ind (P : expr → Prop) :
(
∀
(
f
:
expr
)
(
args
:
list
expr
),
P
f
→
Forall
P
args
→
P
(
Call
f
args
))
→
(
∀
(
es
:
list
expr
),
Forall
P
es
→
P
(
Concat
es
))
→
(
∀
(
ot
:
op_type
)
(
e1
e2
e3
:
expr
),
P
e1
→
P
e2
→
P
e3
→
P
(
IfE
ot
e1
e2
e3
))
→
(
∀
(
ly
:
layout
)
(
e
:
expr
),
P
e
→
P
(
Alloc
ly
e
))
→
(
∀
(
e
:
expr
),
P
e
→
P
(
SkipE
e
))
→