diff options
Diffstat (limited to '')
| -rw-r--r-- | src/FunsAnalysis.ml | 3 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml | 6 | ||||
| -rw-r--r-- | tests/betree/BetreeMain.Clauses.Template.fst | 24 | ||||
| -rw-r--r-- | tests/betree/BetreeMain.Funs.fst | 359 | ||||
| -rw-r--r-- | tests/betree/BetreeMain.Types.fsti | 12 | ||||
| -rw-r--r-- | tests/betree/Primitives.fst | 3 |
6 files changed, 206 insertions, 201 deletions
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index ee4f71c1..5a623450 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -74,9 +74,6 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) can_fail := EU.binop_can_fail bop || !can_fail method! visit_Call env call = - pp_fun_id Format.std_formatter call.func; - print_newline (); - (match call.func with | Regular id -> if FunDeclId.Set.mem id fun_ids then divergent := true diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 3ff45077..c157b667 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -644,13 +644,13 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ [ ("def_id", def_id); ("name", name); - ("type_", type_); + ("ty", ty); ("body", body); ] -> let* global_id = A.GlobalDeclId.id_of_json def_id in let def_id = A.global_to_fun_id gid_conv global_id in let* name = fun_name_of_json name in - let* type_ = ety_of_json type_ in + let* ty = ety_of_json ty in let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in let signature : A.fun_sig = { region_params = []; @@ -658,7 +658,7 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ regions_hierarchy = []; type_params = []; inputs = []; - output = TU.ety_no_regions_to_sty type_; + output = TU.ety_no_regions_to_sty ty; } in Ok { A.def_id; name; signature; body; is_global = true; } | _ -> Error "") diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst index eb26276c..5a9776ab 100644 --- a/tests/betree/BetreeMain.Clauses.Template.fst +++ b/tests/betree/BetreeMain.Clauses.Template.fst @@ -42,18 +42,18 @@ let betree_node_apply_upserts_decreases (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) -unfold -let betree_internal_lookup_in_children_decreases (self : betree_internal_t) - (key : u64) (st : state) : nat = - admit () - (** [betree_main::betree::Node::{5}::lookup]: decreases clause *) unfold let betree_node_lookup_decreases (self : betree_node_t) (key : u64) (st : state) : nat = admit () +(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) +unfold +let betree_internal_lookup_in_children_decreases (self : betree_internal_t) + (key : u64) (st : state) : nat = + admit () + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) unfold let betree_node_lookup_mut_in_bindings_decreases (key : u64) @@ -86,17 +86,17 @@ let betree_node_apply_messages_to_internal_decreases (new_msgs : betree_list_t (u64 & betree_message_t)) : nat = admit () -(** [betree_main::betree::Internal::{4}::flush]: decreases clause *) +(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) unfold -let betree_internal_flush_decreases (self : betree_internal_t) +let betree_node_apply_messages_decreases (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat = + (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) +(** [betree_main::betree::Internal::{4}::flush]: decreases clause *) unfold -let betree_node_apply_messages_decreases (self : betree_node_t) +let betree_internal_flush_decreases (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat = + (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat = admit () diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst index 9b960ce5..4761b6a3 100644 --- a/tests/betree/BetreeMain.Funs.fst +++ b/tests/betree/BetreeMain.Funs.fst @@ -80,6 +80,10 @@ let betree_node_id_counter_fresh_id_back | Return i -> Return (Mkbetree_node_id_counter_t i) end +(** [core::num::u64::{9}::MAX] *) +let core_num_u64_max_body : result u64 = Return 18446744073709551615 +let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body + (** [betree_main::betree::upsert_update] *) let betree_upsert_update_fwd (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 = @@ -92,16 +96,17 @@ let betree_upsert_update_fwd | Some prev0 -> begin match st with | BetreeUpsertFunStateAdd v -> - begin match u64_sub 18446744073709551615 prev0 with + let i = core_num_u64_max_c in + begin match u64_sub i prev0 with | Fail -> Fail | Return margin -> if margin >= v then begin match u64_add prev0 v with | Fail -> Fail - | Return i -> Return i + | Return i0 -> Return i0 end - else Return 18446744073709551615 + else let i0 = core_num_u64_max_c in Return i0 end | BetreeUpsertFunStateSub v -> if prev0 >= v @@ -468,48 +473,8 @@ let rec betree_node_apply_upserts_back end end -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) -let rec betree_internal_lookup_in_children_fwd - (self : betree_internal_t) (key : u64) (st : state) : - Tot (result (state & (option u64))) - (decreases (betree_internal_lookup_in_children_decreases self key st)) - = - if key < self.betree_internal_pivot - then - begin match betree_node_lookup_fwd self.betree_internal_left key st with - | Fail -> Fail - | Return (st0, opt) -> Return (st0, opt) - end - else - begin match betree_node_lookup_fwd self.betree_internal_right key st with - | Fail -> Fail - | Return (st0, opt) -> Return (st0, opt) - end - -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) -and betree_internal_lookup_in_children_back - (self : betree_internal_t) (key : u64) (st : state) : - Tot (result betree_internal_t) - (decreases (betree_internal_lookup_in_children_decreases self key st)) - = - if key < self.betree_internal_pivot - then - begin match betree_node_lookup_back self.betree_internal_left key st with - | Fail -> Fail - | Return n -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right) - end - else - begin match betree_node_lookup_back self.betree_internal_right key st with - | Fail -> Fail - | Return n -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n) - end - (** [betree_main::betree::Node::{5}::lookup] *) -and betree_node_lookup_fwd +let rec betree_node_lookup_fwd (self : betree_node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) (decreases (betree_node_lookup_decreases self key st)) @@ -723,6 +688,46 @@ and betree_node_lookup_back end end +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +and betree_internal_lookup_in_children_fwd + (self : betree_internal_t) (key : u64) (st : state) : + Tot (result (state & (option u64))) + (decreases (betree_internal_lookup_in_children_decreases self key st)) + = + if key < self.betree_internal_pivot + then + begin match betree_node_lookup_fwd self.betree_internal_left key st with + | Fail -> Fail + | Return (st0, opt) -> Return (st0, opt) + end + else + begin match betree_node_lookup_fwd self.betree_internal_right key st with + | Fail -> Fail + | Return (st0, opt) -> Return (st0, opt) + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +and betree_internal_lookup_in_children_back + (self : betree_internal_t) (key : u64) (st : state) : + Tot (result betree_internal_t) + (decreases (betree_internal_lookup_in_children_decreases self key st)) + = + if key < self.betree_internal_pivot + then + begin match betree_node_lookup_back self.betree_internal_left key st with + | Fail -> Fail + | Return n -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right) + end + else + begin match betree_node_lookup_back self.betree_internal_right key st with + | Fail -> Fail + | Return n -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n) + end + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd (key : u64) (bindings : betree_list_t (u64 & u64)) : @@ -1128,140 +1133,8 @@ let rec betree_node_apply_messages_to_internal_fwd_back | BetreeListNil -> Return msgs end -(** [betree_main::betree::Internal::{4}::flush] *) -let rec betree_internal_flush_fwd - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) : - Tot (result (state & (betree_list_t (u64 & betree_message_t)))) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) - = - begin match - betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | Fail -> Fail - | Return p -> - let (msgs_left, msgs_right) = p in - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail - | Return len_left -> - if len_left >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (st0, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (_, node_id_cnt0) -> - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right - with - | Fail -> Fail - | Return len_right -> - if len_right >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_fwd self.betree_internal_right - params node_id_cnt0 msgs_right st0 with - | Fail -> Fail - | Return (st1, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_right - params node_id_cnt0 msgs_right st0 with - | Fail -> Fail - | Return (_, _) -> Return (st1, BetreeListNil) - end - end - else Return (st0, msgs_right) - end - end - end - else - begin match - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail -> Fail - | Return (st0, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail -> Fail - | Return (_, _) -> Return (st0, msgs_left) - end - end - end - end - -(** [betree_main::betree::Internal::{4}::flush] *) -and betree_internal_flush_back - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) : - Tot (result (betree_internal_t & betree_node_id_counter_t)) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) - = - begin match - betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | Fail -> Fail - | Return p -> - let (msgs_left, msgs_right) = p in - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail - | Return len_left -> - if len_left >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (st0, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (n, node_id_cnt0) -> - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right - with - | Fail -> Fail - | Return len_right -> - if len_right >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_back self.betree_internal_right - params node_id_cnt0 msgs_right st0 with - | Fail -> Fail - | Return (n0, node_id_cnt1) -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n n0, node_id_cnt1) - end - else - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right, - node_id_cnt0) - end - end - end - else - begin match - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail -> Fail - | Return (n, node_id_cnt0) -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n, - node_id_cnt0) - end - end - end - (** [betree_main::betree::Node::{5}::apply_messages] *) -and betree_node_apply_messages_fwd +let rec betree_node_apply_messages_fwd (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : @@ -1450,6 +1323,138 @@ and betree_node_apply_messages_back end end +(** [betree_main::betree::Internal::{4}::flush] *) +and betree_internal_flush_fwd + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (u64 & betree_message_t)) (st : state) : + Tot (result (state & (betree_list_t (u64 & betree_message_t)))) + (decreases (betree_internal_flush_decreases self params node_id_cnt content + st)) + = + begin match + betree_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot with + | Fail -> Fail + | Return p -> + let (msgs_left, msgs_right) = p in + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with + | Fail -> Fail + | Return len_left -> + if len_left >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (st0, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (_, node_id_cnt0) -> + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right + with + | Fail -> Fail + | Return len_right -> + if len_right >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_fwd self.betree_internal_right + params node_id_cnt0 msgs_right st0 with + | Fail -> Fail + | Return (st1, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_right + params node_id_cnt0 msgs_right st0 with + | Fail -> Fail + | Return (_, _) -> Return (st1, BetreeListNil) + end + end + else Return (st0, msgs_right) + end + end + end + else + begin match + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st with + | Fail -> Fail + | Return (st0, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st with + | Fail -> Fail + | Return (_, _) -> Return (st0, msgs_left) + end + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +and betree_internal_flush_back + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (u64 & betree_message_t)) (st : state) : + Tot (result (betree_internal_t & betree_node_id_counter_t)) + (decreases (betree_internal_flush_decreases self params node_id_cnt content + st)) + = + begin match + betree_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot with + | Fail -> Fail + | Return p -> + let (msgs_left, msgs_right) = p in + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with + | Fail -> Fail + | Return len_left -> + if len_left >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (st0, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (n, node_id_cnt0) -> + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right + with + | Fail -> Fail + | Return len_right -> + if len_right >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_back self.betree_internal_right + params node_id_cnt0 msgs_right st0 with + | Fail -> Fail + | Return (n0, node_id_cnt1) -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n n0, node_id_cnt1) + end + else + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right, + node_id_cnt0) + end + end + end + else + begin match + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st with + | Fail -> Fail + | Return (n, node_id_cnt0) -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n, + node_id_cnt0) + end + end + end + (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd (self : betree_node_t) (params : betree_params_t) diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti index a937c726..aad9cb43 100644 --- a/tests/betree/BetreeMain.Types.fsti +++ b/tests/betree/BetreeMain.Types.fsti @@ -24,8 +24,13 @@ type betree_message_t = (** [betree_main::betree::Leaf] *) type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; } +(** [betree_main::betree::Node] *) +type betree_node_t = +| BetreeNodeInternal : betree_internal_t -> betree_node_t +| BetreeNodeLeaf : betree_leaf_t -> betree_node_t + (** [betree_main::betree::Internal] *) -type betree_internal_t = +and betree_internal_t = { betree_internal_id : u64; betree_internal_pivot : u64; @@ -33,11 +38,6 @@ type betree_internal_t = betree_internal_right : betree_node_t; } -(** [betree_main::betree::Node] *) -and betree_node_t = -| BetreeNodeInternal : betree_internal_t -> betree_node_t -| BetreeNodeLeaf : betree_leaf_t -> betree_node_t - (** [betree_main::betree::Params] *) type betree_params_t = { diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst index fe351f3a..b3da25c2 100644 --- a/tests/betree/Primitives.fst +++ b/tests/betree/Primitives.fst @@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail +// Unwrap a successful result by normalisation (used for globals). +let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x + (*** Misc *) type char = FStar.Char.char type string = string |