Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2

Complete the constants extraction by making all functions fail

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