Fix some issues and regenerate the HashmapMain example for Lean

3 files changed, 18 insertions, 7 deletions

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 363955bf..2dbacce3 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -381,6 +381,7 @@ let builtin_fun_effects =
   let int_funs = List.concat int_funs in
   let no_fail_no_state_funs =
     [
+      (* TODO: redundancy with the funs information below *)
       "alloc::vec::Vec::new";
       "alloc::vec::Vec::len";
       "alloc::boxed::Box::deref";
@@ -395,7 +396,15 @@ let builtin_fun_effects =
       (fun n -> (n, { can_fail = false; stateful = false }))
       no_fail_no_state_funs
   in
-  let no_state_funs = [ "alloc::vec::Vec::push" ] in
+  let no_state_funs =
+    [
+      (* TODO: redundancy with the funs information below *)
+      "alloc::vec::Vec::push";
+      "alloc::vec::Vec::index";
+      "alloc::vec::Vec::index_mut";
+      "alloc::vec::Vec::index_mut_back";
+    ]
+  in
   let no_state_funs =
     List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs
   in
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 9eac3e6f..69c0df71 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -76,6 +76,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
         object (self)
           inherit [_] iter_statement as super
           method may_fail b = can_fail := !can_fail || b
+          method maybe_stateful b = stateful := !stateful || b
 
           method! visit_Assert env a =
             self#may_fail true;
@@ -126,14 +127,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
       | None ->
           let info_can_fail, info_stateful =
             match builtin_info with
-            | None -> (true, false)
+            | None -> (true, use_state)
             | Some { can_fail; stateful } -> (can_fail, stateful)
           in
           obj#may_fail info_can_fail;
-          stateful :=
-            (not f.is_global_decl_body)
-            && use_state
-            && not (has_builtin_info && not info_stateful)
+          obj#maybe_stateful
+            (if f.is_global_decl_body then false
+             else if not use_state then false
+             else info_stateful)
       | Some body -> obj#visit_statement () body.body
     in
     List.iter visit_fun d;
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 341e97eb..245f3b77 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -144,7 +144,8 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
       (match v.V.ty with
       | T.Adt (T.Assumed T.Box, _) ->
           raise (Failure "Can't copy an assumed value other than Option")
-      | T.Adt (T.AdtId _, _) -> assert allow_adt_copy
+      | T.Adt (T.AdtId _, _) as ty ->
+          assert (allow_adt_copy || ty_is_primitively_copyable ty)
       | T.Adt (T.Tuple, _) -> () (* Ok *)
       | T.Adt
           ( T.Assumed (Slice | T.Array),