Commit 5552a911 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Refactoring and renaming in [lang.v] (mostly).

- Put stuff in sections in [lang.v].
- Renamed [mk_layout] into [Layout] (for uniformity).
- Renamed [it_min] and [it_max] into [max_int] and [min_int].
- Some other renamings on [int_type]-related stuff.
- Changed [max_int] to be the last representable integer.
- Turned [in_it_range] into an instance of [ElemOf].
parent ea5c3527
Pipeline #36125 passed with stage
in 16 minutes and 44 seconds
......@@ -13,3 +13,4 @@ _opam
/theories/examples/tutorial/tutorial
*.timing
*.gen
.lia.cache
......@@ -261,10 +261,10 @@ btree_t insert_br(btree_t* node, int k, void* v, btree_t b,
[[rc::parameters("k : Z", "v : loc", "ty : type")]]
[[rc::args("rl @ btree_t", "rr @ btree_t", "k @ int<i32>", "v @ &own<ty>")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::requires("{br_height rl + 1 < it_max i32}")]]
[[rc::requires("{br_height rl + 1 ≤ max_int i32}")]]
[[rc::requires("{br_height rl = br_height rr}")]]
[[rc::requires("{br_max rl = (k - 1)%Z}", "{br_min rr = (k + 1)%Z}")]]
[[rc::requires("{br_min rl = it_min i32}", "{br_max rr = (it_max i32 - 1)%Z}")]]
[[rc::requires("{br_min rl = min_int i32}", "{br_max rr = max_int i32}")]]
[[rc::returns("{BR true (br_height rl + 1)%nat (br_min rl) (br_max rr) "
"({[k:=ty]} ∪ (br_map (non_root rl) ∪ br_map (non_root rr)))} "
"@ btree_t")]]
......
......@@ -25,7 +25,7 @@ flags {
[[rc::parameters("fs : Flags", "n1 : nat", "n2 : nat")]]
[[rc::args("fs @ flags", "n1 @ int<u32>", "n2 @ int<u32>")]]
[[rc::requires("{n1 + n2 < it_max u32}")]]
[[rc::requires("{n1 + n2 ≤ max_int u32}")]]
[[rc::returns("{(if flag1 fs then n1 else 0) + (if flag2 fs then n2 else 0)} @ int<u32>")]]
[[rc::trust_me]] // FIXME automation
unsigned int sum(flags_t f, unsigned int arg1, unsigned int arg2){
......
......@@ -5,25 +5,25 @@
[[rc::parameters("size : nat")]]
[[rc::args("size @ int<size_t>")]]
[[rc::requires("{size + 16 < it_max size_t}", "{(8 | size)}",
[[rc::requires("{size + 16 ≤ max_int size_t}", "{(8 | size)}",
"[alloc_initialized]")]]
[[rc::returns("&own<uninit<{mk_layout size 3}>>")]]
[[rc::returns("&own<uninit<{Layout size 3}>>")]]
void *alloc(size_t size);
[[rc::parameters("size : nat")]]
[[rc::requires("[alloc_initialized]", "{(8 | size)}")]]
[[rc::args("size @ int<size_t>", "&own<uninit<{mk_layout size 3}>>")]]
[[rc::args("size @ int<size_t>", "&own<uninit<{Layout size 3}>>")]]
void free(size_t size, void *ptr);
[[rc::parameters("size : nat", "n : nat")]]
[[rc::args("size @ int<size_t>", "n @ int<size_t>")]]
[[rc::requires("{size * n + 16 < it_max size_t}", "{(8 | size)}", "[alloc_initialized]")]]
[[rc::returns("&own<array<{mk_layout size 3}, {replicate n (uninit (mk_layout size 3))}>>")]]
[[rc::requires("{size * n + 16 ≤ max_int size_t}", "{(8 | size)}", "[alloc_initialized]")]]
[[rc::returns("&own<array<{Layout size 3}, {replicate n (uninit (Layout size 3))}>>")]]
void *alloc_array(size_t size, size_t n);
[[rc::parameters("size : nat", "n : nat")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::requires("{size * n < it_max size_t}", "{(8 | size)}")]]
[[rc::args("size @ int<size_t>", "n @ int<size_t>", "&own<array<{mk_layout size 3}, {replicate n (uninit (mk_layout size 3))}>>")]]
[[rc::requires("{size * n ≤ max_int size_t}", "{(8 | size)}")]]
[[rc::args("size @ int<size_t>", "n @ int<size_t>", "&own<array<{Layout size 3}, {replicate n (uninit (Layout size 3))}>>")]]
void free_array(size_t size, size_t n, void *ptr);
#define ALLOC(sz) alloc(sz)
......
......@@ -16,7 +16,7 @@ struct [[rc::refined_by("n1 : Z", "n2 : Z", "n3 : Z")]]
[[rc::field("spinlocked_ex<l, {\"locked_struct\"}, n3, λ n3. ...>")]]
struct [[rc::exists("a : Z", "b : Z")]]
[[rc::constraints("{n3 = (a + b)%Z}", "{it_in_range size_t n3}")]] lock_test_inner {
[[rc::constraints("{n3 = (a + b)%Z}", "{n3 ∈ size_t}")]] lock_test_inner {
[[rc::field("a @ int<size_t>")]]
size_t a;
......
......@@ -348,7 +348,7 @@ void mpool_free(struct mpool *p, void *ptr) {
*/
[[rc::parameters("p : loc", "q : own_state", "n : nat", "entry_size : nat", "count : nat", "align : nat")]]
[[rc::args("p @ &frac<q, n @ mpool<entry_size>>", "count @ int<size_t>", "align @ int<size_t>")]]
[[rc::requires("{it_in_range size_t (align * entry_size + count * entry_size)}", "{is_power_of_two align}")]]
[[rc::requires("{(align * entry_size + count * entry_size)%Z ∈ size_t}", "{is_power_of_two align}")]]
[[rc::exists("n2 : nat")]]
[[rc::returns("optional<&own<uninit<{ly_with_align (count * entry_size) (align * entry_size)}>>>")]]
[[rc::ensures("p @ &frac<q, n2 @ mpool<entry_size>>", "{q = Own → n2 <= n}")]]
......@@ -447,7 +447,7 @@ void *mpool_alloc_contiguous_no_fallback(struct mpool *p, size_t count, size_t a
*/
[[rc::parameters("p : loc", "q : own_state", "n : nat", "entry_size : nat", "count : nat", "align : nat")]]
[[rc::args("p @ &frac<q, n @ mpool<entry_size>>", "count @ int<size_t>", "align @ int<size_t>")]]
[[rc::requires("{it_in_range size_t (align * entry_size + count * entry_size)}", "{is_power_of_two align}")]]
[[rc::requires("{(align * entry_size + count * entry_size)%Z ∈ size_t}", "{is_power_of_two align}")]]
[[rc::exists("n2 : nat")]]
[[rc::returns("optional<&own<uninit<{ly_with_align (count * entry_size) (align * entry_size)}>>>")]]
[[rc::ensures("p @ &frac<q, n2 @ mpool<entry_size>>", "{q = Own → n2 <= n}")]]
......
......@@ -66,7 +66,7 @@ void fsm_realloc_if_necessary(struct fixed_size_map *m);
[[rc::parameters("m : loc", "len : nat")]]
[[rc::args("m @ &own<uninit<struct_fixed_size_map>>")]]
[[rc::args("len @ int<size_t>")]]
[[rc::requires("{1 < len}", "{struct_item.(ly_size) * len + 16 < it_max size_t}")]]
[[rc::requires("{1 < len}", "{struct_item.(ly_size) * len + 16 ≤ max_int size_t}")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::ensures("m @ &own<{∅, replicate len Empty, len} @ fixed_size_map> ")]]
[[rc::lemmas("fsm_invariant_init")]]
......@@ -236,7 +236,7 @@ void fsm_realloc_if_necessary(struct fixed_size_map *m) {
[[rc::inv_vars("m2 : {fsm_copy_entries items i, items2, count2} @ fixed_size_map")]]
[[rc::constraints("{count + length items - i < count2}", "{i <= length items}", "{0 < count}",
"{length items * 2 <= length items2}", "{fsm_invariant mp items}",
"{struct_item.(ly_size) * length items < it_max size_t}")]]
"{struct_item.(ly_size) * length items ≤ max_int size_t}")]]
for(size_t i = 0; i < m->length; i += 1) {
if((*m->items)[i].tag == ITEM_ENTRY) {
fsm_insert(&m2, (*m->items)[i].u.entry.key, (*m->items)[i].u.entry.value);
......
......@@ -454,8 +454,8 @@ Section defs.
Definition BRroot (h : nat) (m : gmap Z type) : btree_rfmt := {|
br_root := true;
br_height := h;
br_min := it_min i32;
br_max := it_max i32 - 1;
br_min := min_int i32;
br_max := max_int i32;
br_map := m;
|}.
......
......@@ -1563,11 +1563,11 @@ Section code.
sl_members := [
(Some "nb_keys", it_layout i32);
(Some "keys", mk_array_layout (it_layout i32) 4);
(None, mk_layout 4%nat 0%nat);
(None, Layout 4%nat 0%nat);
(Some "vals", mk_array_layout LPtr 4);
(Some "children", mk_array_layout LPtr 5);
(Some "height", it_layout i32);
(None, mk_layout 4%nat 0%nat)
(None, Layout 4%nat 0%nat)
];
|}.
Solve Obligations with solve_struct_obligations.
......
......@@ -90,22 +90,22 @@ Section spec.
(* Specifications for function [alloc]. *)
Definition type_of_alloc :=
fn( size : nat; (size @ (int (size_t))); size + 16 < it_max size_t (8 | size) (alloc_initialized))
() : (), (&own (uninit (mk_layout size 3))); True.
fn( size : nat; (size @ (int (size_t))); size + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (uninit (Layout size 3))); True.
(* Specifications for function [free]. *)
Definition type_of_free :=
fn( size : nat; (size @ (int (size_t))), (&own (uninit (mk_layout size 3))); (alloc_initialized) (8 | size))
fn( size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) (8 | size))
() : (), (void); True.
(* Specifications for function [alloc_array]. *)
Definition type_of_alloc_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16 < it_max size_t (8 | size) (alloc_initialized))
() : (), (&own (array (mk_layout size 3) (replicate n (uninit (mk_layout size 3))))); True.
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
(* Specifications for function [free_array]. *)
Definition type_of_free_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (mk_layout size 3) (replicate n (uninit (mk_layout size 3))))); size * n < it_max size_t (8 | size) (alloc_initialized))
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); size * n max_int size_t (8 | size) (alloc_initialized))
() : (), (void); True.
(* Specifications for function [new_btree]. *)
......@@ -148,7 +148,7 @@ Section spec.
(* Specifications for function [btree_make_root]. *)
Definition type_of_btree_make_root :=
fn( (rl, rr, k, v, ty) : btree_rfmt * btree_rfmt * Z * loc * type; (rl @ (btree_t)), (rr @ (btree_t)), (k @ (int (i32))), (v @ (&own (ty))); (alloc_initialized) br_height rl + 1 < it_max i32 br_height rl = br_height rr br_max rl = (k - 1)%Z br_min rr = (k + 1)%Z br_min rl = it_min i32 br_max rr = (it_max i32 - 1)%Z)
fn( (rl, rr, k, v, ty) : btree_rfmt * btree_rfmt * Z * loc * type; (rl @ (btree_t)), (rr @ (btree_t)), (k @ (int (i32))), (v @ (&own (ty))); (alloc_initialized) br_height rl + 1 max_int i32 br_height rl = br_height rr br_max rl = (k - 1)%Z br_min rr = (k + 1)%Z br_min rl = min_int i32 br_max rr = max_int i32)
() : (), ((BR true (br_height rl + 1)%nat (br_min rl) (br_max rr) ({[k:=ty]} (br_map (non_root rl) br_map (non_root rr)))) @ (btree_t)); True.
End spec.
......
......@@ -73,7 +73,7 @@ Section spec.
(* Specifications for function [sum]. *)
Definition type_of_sum :=
fn( (fs, n1, n2) : Flags * nat * nat; (fs @ (flags)), (n1 @ (int (u32))), (n2 @ (int (u32))); n1 + n2 < it_max u32)
fn( (fs, n1, n2) : Flags * nat * nat; (fs @ (flags)), (n1 @ (int (u32))), (n2 @ (int (u32))); n1 + n2 max_int u32)
() : (), (((if flag1 fs then n1 else 0) + (if flag2 fs then n2 else 0)) @ (int (u32))); True.
End spec.
......
......@@ -195,7 +195,7 @@ Section code.
sl_members := [
(Some "outside", it_layout size_t);
(Some "lock", layout_of struct_spinlock);
(None, mk_layout 7%nat 0%nat);
(None, Layout 7%nat 0%nat);
(Some "locked_int", it_layout size_t);
(Some "locked_struct", layout_of struct_lock_test_inner)
];
......
......@@ -28,7 +28,7 @@ Section spec.
(b @ (int (size_t)))
]) (
n3 = (a + b)%Z
it_in_range size_t n3
n3 size_t
)))
)))
])
......@@ -60,7 +60,7 @@ Section spec.
(b @ (int (size_t)))
]) (
n3 = (a + b)%Z
it_in_range size_t n3
n3 size_t
)))
)))
])
......
......@@ -859,7 +859,7 @@ Section code.
sl_members := [
(Some "entry_size", it_layout size_t);
(Some "lock", layout_of struct_spinlock);
(None, mk_layout 7%nat 0%nat);
(None, Layout 7%nat 0%nat);
(Some "locked", layout_of struct_mpool_locked_inner);
(Some "fallback", LPtr)
];
......
......@@ -279,14 +279,14 @@ Section spec.
(* Specifications for function [mpool_alloc_contiguous_no_fallback]. *)
Definition type_of_mpool_alloc_contiguous_no_fallback :=
fn( (p, q, n, entry_size, count, align) : loc * own_state * nat * nat * nat * nat; (p @ (&frac{q} (n @ (mpool (entry_size))))), (count @ (int (size_t))), (align @ (int (size_t))); it_in_range size_t (align * entry_size + count * entry_size) is_power_of_two align)
fn( (p, q, n, entry_size, count, align) : loc * own_state * nat * nat * nat * nat; (p @ (&frac{q} (n @ (mpool (entry_size))))), (count @ (int (size_t))), (align @ (int (size_t))); (align * entry_size + count * entry_size)%Z size_t is_power_of_two align)
n2 : nat, (optionalO (λ _ : unit,
&own (uninit (ly_with_align (count * entry_size) (align * entry_size)))
) null); (p ◁ₗ{q} (n2 @ (mpool (entry_size)))) q = Own n2 <= n.
(* Specifications for function [mpool_alloc_contiguous]. *)
Definition type_of_mpool_alloc_contiguous :=
fn( (p, q, n, entry_size, count, align) : loc * own_state * nat * nat * nat * nat; (p @ (&frac{q} (n @ (mpool (entry_size))))), (count @ (int (size_t))), (align @ (int (size_t))); it_in_range size_t (align * entry_size + count * entry_size) is_power_of_two align)
fn( (p, q, n, entry_size, count, align) : loc * own_state * nat * nat * nat * nat; (p @ (&frac{q} (n @ (mpool (entry_size))))), (count @ (int (size_t))), (align @ (int (size_t))); (align * entry_size + count * entry_size)%Z size_t is_power_of_two align)
n2 : nat, (optionalO (λ _ : unit,
&own (uninit (ly_with_align (count * entry_size) (align * entry_size)))
) null); (p ◁ₗ{q} (n2 @ (mpool (entry_size)))) q = Own n2 <= n.
......
......@@ -619,7 +619,7 @@ Section code.
]> $
<[ "#1" :=
locinfo: loc_123 ;
if: LocInfoE loc_123 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_123 ((LocInfoE loc_124 (use{it_layout size_t} (LocInfoE loc_125 ((LocInfoE loc_126 (!{LPtr} (LocInfoE loc_127 ("m")))) at{struct_fixed_size_map} "length")))) <{IntOp size_t, IntOp size_t} (LocInfoE loc_128 ((LocInfoE loc_129 ((LocInfoE loc_130 ((LocInfoE loc_131 (i2v (it_max size_t - 1) size_t)) /{IntOp size_t, IntOp size_t} (LocInfoE loc_132 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_132 (i2v 2 i32)))))) /{IntOp size_t, IntOp size_t} (LocInfoE loc_133 (i2v (layout_of struct_item).(ly_size) size_t)))) -{IntOp size_t, IntOp size_t} (LocInfoE loc_134 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_134 (i2v 16 i32)))))))))
if: LocInfoE loc_123 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_123 ((LocInfoE loc_124 (use{it_layout size_t} (LocInfoE loc_125 ((LocInfoE loc_126 (!{LPtr} (LocInfoE loc_127 ("m")))) at{struct_fixed_size_map} "length")))) <{IntOp size_t, IntOp size_t} (LocInfoE loc_128 ((LocInfoE loc_129 ((LocInfoE loc_130 ((LocInfoE loc_131 (i2v (max_int size_t) size_t)) /{IntOp size_t, IntOp size_t} (LocInfoE loc_132 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_132 (i2v 2 i32)))))) /{IntOp size_t, IntOp size_t} (LocInfoE loc_133 (i2v (layout_of struct_item).(ly_size) size_t)))) -{IntOp size_t, IntOp size_t} (LocInfoE loc_134 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_134 (i2v 16 i32)))))))))
then
Goto "#9"
else
......
......@@ -31,7 +31,7 @@ Section proof_fsm_realloc_if_necessary.
0 < count
length items * 2 <= length items2
fsm_invariant mp items
struct_item.(ly_size) * length items < it_max size_t
struct_item.(ly_size) * length items max_int size_t
]> $
<[ "#11" :=
arg_m ◁ₗ (m @ (&own ((mp, items, count) @ (fixed_size_map))))
......
......@@ -129,22 +129,22 @@ Section spec.
(* Specifications for function [alloc]. *)
Definition type_of_alloc :=
fn( size : nat; (size @ (int (size_t))); size + 16 < it_max size_t (8 | size) (alloc_initialized))
() : (), (&own (uninit (mk_layout size 3))); True.
fn( size : nat; (size @ (int (size_t))); size + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (uninit (Layout size 3))); True.
(* Specifications for function [free]. *)
Definition type_of_free :=
fn( size : nat; (size @ (int (size_t))), (&own (uninit (mk_layout size 3))); (alloc_initialized) (8 | size))
fn( size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) (8 | size))
() : (), (void); True.
(* Specifications for function [alloc_array]. *)
Definition type_of_alloc_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16 < it_max size_t (8 | size) (alloc_initialized))
() : (), (&own (array (mk_layout size 3) (replicate n (uninit (mk_layout size 3))))); True.
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
(* Specifications for function [free_array]. *)
Definition type_of_free_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (mk_layout size 3) (replicate n (uninit (mk_layout size 3))))); size * n < it_max size_t (8 | size) (alloc_initialized))
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); size * n max_int size_t (8 | size) (alloc_initialized))
() : (), (void); True.
(* Specifications for function [fsm_realloc_if_necessary]. *)
......@@ -154,7 +154,7 @@ Section spec.
(* Specifications for function [fsm_init]. *)
Definition type_of_fsm_init :=
fn( (m, len) : loc * nat; (m @ (&own (uninit (struct_fixed_size_map)))), (len @ (int (size_t))); 1 < len struct_item.(ly_size) * len + 16 < it_max size_t (alloc_initialized))
fn( (m, len) : loc * nat; (m @ (&own (uninit (struct_fixed_size_map)))), (len @ (int (size_t))); 1 < len struct_item.(ly_size) * len + 16 max_int size_t (alloc_initialized))
() : (), (void); (m ◁ₗ ((, replicate len Empty, len) @ (fixed_size_map))).
(* Specifications for function [fsm_slot_for_key]. *)
......
......@@ -120,22 +120,22 @@ Section spec.
(* Specifications for function [alloc]. *)
Definition type_of_alloc :=
fn( size : nat; (size @ (int (size_t))); size + 16 < it_max size_t (8 | size) (alloc_initialized))
() : (), (&own (uninit (mk_layout size 3))); True.
fn( size : nat; (size @ (int (size_t))); size + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (uninit (Layout size 3))); True.
(* Specifications for function [free]. *)
Definition type_of_free :=
fn( size : nat; (size @ (int (size_t))), (&own (uninit (mk_layout size 3))); (alloc_initialized) (8 | size))
fn( size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) (8 | size))
() : (), (void); True.
(* Specifications for function [alloc_array]. *)
Definition type_of_alloc_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16 < it_max size_t (8 | size) (alloc_initialized))
() : (), (&own (array (mk_layout size 3) (replicate n (uninit (mk_layout size 3))))); True.
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
(* Specifications for function [free_array]. *)
Definition type_of_free_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (mk_layout size 3) (replicate n (uninit (mk_layout size 3))))); size * n < it_max size_t (8 | size) (alloc_initialized))
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); size * n max_int size_t (8 | size) (alloc_initialized))
() : (), (void); True.
(* Specifications for function [init_queue]. *)
......
......@@ -10,7 +10,7 @@ Section spec.
(* Specifications for function [times_two]. *)
Definition type_of_times_two :=
fn( x : nat; (x @ (int (u32))); 2 * x < it_max u32)
fn( x : nat; (x @ (int (u32))); 2 * x max_int u32)
() : (), ((2 * x) @ (int (u32))); True.
(* Specifications for function [div_two]. *)
......
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