Merge branch 'main' into protz_closures

AeneasVerif · Aug 29, 2024 · b74d4f8 · b74d4f8
2 parents b3bd86f + 0a1b4e9
commit b74d4f8
Show file tree

Hide file tree

Showing 4 changed files with 51 additions and 24 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h
@@ -95,6 +95,9 @@ typedef struct {
 #define core_array_equality___core__cmp__PartialEq__Array_U__N___for__Array_T__N____eq( \
     sz, a1, a2, t, _, _ret_t)                                                           \
   Eurydice_array_eq(sz, a1, a2, t, _)
+#define core_array_equality___core__cmp__PartialEq__0___Slice_U____for__Array_T__N___3__eq( \
+    sz, a1, a2, t, _, _ret_t)                                                               \
+  Eurydice_array_eq(sz, a1, ((a2)->ptr), t, _)
 
 #define Eurydice_slice_split_at(slice, mid, element_type, ret_t)               \
   (CLITERAL(ret_t){                                                            \

diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
@@ -1264,7 +1264,11 @@ let expression_of_rvalue (env : env) (p : C.rvalue) : K.expr =
   | Global { global_id; global_generics = _ } ->
       let global = env.get_nth_global global_id in
       K.with_type (typ_of_ty env global.ty) (K.EQualified (lid_of_name env global.item_meta.name))
-  | Len _ -> failwith "unsupported: Len"
+  | rvalue ->
+      failwith
+        ("unsupported rvalue: `"
+        ^ Charon.PrintExpressions.rvalue_to_string env.format_env rvalue
+        ^ "`")
 
 let expression_of_assertion (env : env) ({ cond; expected } : C.assertion) : K.expr =
   let cond =
@@ -1350,7 +1354,7 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_
         func =
           FnOpRegular
             {
-              func = FunId (FAssumed (ArrayIndexShared | ArrayIndexMut));
+              func = FunId (FAssumed (Index { is_array = true; mutability = _; is_range = false }));
               generics = { types = [ ty ]; _ };
               _;
             };
@@ -1433,15 +1437,16 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_
           | _ -> []
         in
         match fn_ptr.func, fn_ptr.generics.types @ extra_types with
-        | ( FunId (FAssumed (SliceIndexShared | SliceIndexMut)),
+        | ( FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })),
             [ TAdt (TAssumed (TArray | TSlice), _) ] ) ->
             (* Will decay. See comment above maybe_addrof *)
             rhs
-        | FunId (FAssumed (SliceIndexShared | SliceIndexMut)), [ TAdt (id, generics) ]
+        | ( FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })),
+            [ TAdt (id, generics) ] )
           when RustNames.is_vec env id generics ->
             (* Will decay. See comment above maybe_addrof *)
             rhs
-        | FunId (FAssumed (SliceIndexShared | SliceIndexMut)), _ ->
+        | FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })), _ ->
             K.(with_type (TBuf (rhs.typ, false)) (EAddrOf rhs))
         | _ -> rhs
       in
@@ -1577,7 +1582,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
       let env = push_type_binders env type_params in
 
       match kind with
-      | Opaque | Error _ -> None
+      | Union _ | Opaque | Error _ -> None
       | Struct fields ->
           let fields =
             List.map

diff --git a/lib/Cleanup1.ml b/lib/Cleanup1.ml
@@ -56,7 +56,18 @@ let remove_assignments =
           List.map
             (fun atom ->
               let name, typ = AtomMap.find atom not_yet_closed in
-              ( { node = { atom; name; mut = true; mark = ref Krml.Mark.default; meta = None }; typ },
+              ( {
+                  node =
+                    {
+                      atom;
+                      name;
+                      mut = true;
+                      mark = ref Krml.Mark.default;
+                      meta = None;
+                      attempt_inline = false;
+                    };
+                  typ;
+                },
                 if typ = TUnit then
                   Krml.Helpers.eunit
                 else
@@ -153,7 +164,15 @@ let remove_assignments =
               let name, typ = AtomMap.find atom not_yet_closed in
               let b =
                 {
-                  node = { atom; name; mut = true; mark = ref Krml.Mark.default; meta = None };
+                  node =
+                    {
+                      atom;
+                      name;
+                      mut = true;
+                      mark = ref Krml.Mark.default;
+                      meta = None;
+                      attempt_inline = false;
+                    };
                   typ;
                 }
               in