summaryrefslogtreecommitdiff
path: root/tests/hashmap_on_disk
diff options
context:
space:
mode:
authorSidney Congard2022-06-30 14:54:15 +0200
committerSidney Congard2022-06-30 14:54:15 +0200
commitfdbbb82ff89b1d5141ec63bc2385936da3de3616 (patch)
treed48e3fa933280e8a275d2cfdab8f126e920e5f13 /tests/hashmap_on_disk
parent47691de8fe3dc32a29663d4d8343eb415ce1d81e (diff)
parent4f33892c81cdaf6aefaad9b7cef1456dcfead67c (diff)
Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2
Complete the constants extraction by making all functions fail
Diffstat (limited to 'tests/hashmap_on_disk')
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst25
-rw-r--r--tests/hashmap_on_disk/Makefile48
-rw-r--r--tests/hashmap_on_disk/Primitives.fst3
3 files changed, 66 insertions, 10 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index d01046ec..1d8ee3da 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -198,6 +198,10 @@ let hashmap_hash_map_insert_no_resize_fwd_back
end
end
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
let rec hashmap_hash_map_move_elements_from_list_fwd_back
(t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
@@ -257,23 +261,24 @@ let rec hashmap_hash_map_move_elements_fwd_back
(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
let hashmap_hash_map_try_resize_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
- begin match scalar_cast U32 Usize 4294967295 with
+ let i = core_num_u32_max_c in
+ begin match scalar_cast U32 Usize i with
| Fail -> Fail
| Return max_usize ->
let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_div max_usize 2 with
| Fail -> Fail
| Return n1 ->
- let (i, i0) = self.hashmap_hash_map_max_load_factor in
- begin match usize_div n1 i with
+ let (i0, i1) = self.hashmap_hash_map_max_load_factor in
+ begin match usize_div n1 i0 with
| Fail -> Fail
- | Return i1 ->
- if capacity <= i1
+ | Return i2 ->
+ if capacity <= i2
then
begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return i2 ->
- begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
+ | Return i3 ->
+ begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 with
| Fail -> Fail
| Return ntable ->
begin match
@@ -282,14 +287,14 @@ let hashmap_hash_map_try_resize_fwd_back
| Fail -> Fail
| Return (ntable0, _) ->
Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
- (i, i0) ntable0.hashmap_hash_map_max_load
+ (i0, i1) ntable0.hashmap_hash_map_max_load
ntable0.hashmap_hash_map_slots)
end
end
end
else
- Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i,
- i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+ Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i0,
+ i1) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
end
end
end
diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile
new file mode 100644
index 00000000..ea838d2d
--- /dev/null
+++ b/tests/hashmap_on_disk/Makefile
@@ -0,0 +1,48 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+ --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+ --warn_error '+241@247+285-274' \
+ --cache_dir obj
+
+FSTAR_NO_FLAGS = fstar.exe
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+ $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst %.fsti:
+ $(FSTAR) $@
+
+# Generete the .checked files in bash mode
+%.checked:
+ $(FSTAR) $(FSTAR_FLAGS) $* && \
+ touch -c $*
+
+# Build all the files
+all: $(ALL_CHECKED_FILES)
+
+.PHONY: clean
+clean:
+ rm -f obj/*
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index fe351f3a..b3da25c2 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/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