From b85e78c5cbdaac533725972334c681891e254226 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Tue, 27 Aug 2024 14:32:54 +0200 Subject: [PATCH 1/8] Add another core_array_equality to eurydice_glue.h Add another `core_array_equality` function. --- include/eurydice_glue.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 0451efd..328e8fb 100644 --- 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, t, _) #define Eurydice_slice_split_at(slice, mid, element_type, ret_t) \ (CLITERAL(ret_t){ \ From 651190a9fdcce105e54aa2dc64b842dcd9fcf0bf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 28 Aug 2024 13:38:54 +0200 Subject: [PATCH 2/8] Update charon --- flake.lock | 12 ++++++------ lib/AstOfLlbc.ml | 6 +++++- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/flake.lock b/flake.lock index 0a2d4c2..5d5d834 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724768110, - "narHash": "sha256-PPjuaIQa9srw64rDeaatDf3CHPNgLbqwfE0DSdEU37Q=", + "lastModified": 1724838996, + "narHash": "sha256-N8eoK78blhH2HRGenQbTrTxwc9W1JcSe3agcl2yj1AA=", "owner": "aeneasverif", "repo": "charon", - "rev": "13502d2f3bd477ee86acafe5974016dc7707db83", + "rev": "597fe150c3952fd197e37bc7b5ae2cb2f0d07c81", "type": "github" }, "original": { @@ -246,11 +246,11 @@ ] }, "locked": { - "lastModified": 1724725307, - "narHash": "sha256-gnu8JrUFQoy7b927EPuwmWpvk8MSroFl07pplmVueYA=", + "lastModified": 1724811750, + "narHash": "sha256-PvhVgQ1rm3gfhK7ts4emprhh/KMkFwXogmgsQ3srR7g=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "f56076b216c266cd855b0811ceb86802e834cdb9", + "rev": "6a1c4915dca7149e7258d8c7f3ac634d8c65f6c6", "type": "github" }, "original": { diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 05dc39a..9f99225 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1256,7 +1256,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 = From d9e28bff6d8872232617670591e536141b788449 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Wed, 28 Aug 2024 13:54:27 +0200 Subject: [PATCH 3/8] fixup: it's a slice --- include/eurydice_glue.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 328e8fb..398d983 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -97,7 +97,7 @@ typedef struct { 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, t, _) + Eurydice_array_eq(sz, a1, ((t *)(a2)->ptr), t, _) #define Eurydice_slice_split_at(slice, mid, element_type, ret_t) \ (CLITERAL(ret_t){ \ From f5184ea619242cf9449071cb09d170b74c0ca7a5 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Wed, 28 Aug 2024 19:26:19 +0200 Subject: [PATCH 4/8] Update eurydice_glue.h --- include/eurydice_glue.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 398d983..01c3541 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -97,7 +97,7 @@ typedef struct { 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, ((t *)(a2)->ptr), t, _) + Eurydice_array_eq(sz, a1, ((a2)->ptr), t, _) #define Eurydice_slice_split_at(slice, mid, element_type, ret_t) \ (CLITERAL(ret_t){ \ From d3ca7e4ee924189b74ec699d6a447f9f8db9c622 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 29 Aug 2024 17:14:58 +0200 Subject: [PATCH 5/8] Update charon --- flake.lock | 12 ++++++------ lib/AstOfLlbc.ml | 11 ++++++----- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/flake.lock b/flake.lock index 5d5d834..904990b 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724838996, - "narHash": "sha256-N8eoK78blhH2HRGenQbTrTxwc9W1JcSe3agcl2yj1AA=", + "lastModified": 1724943885, + "narHash": "sha256-Cb1/8daD2gkpHIbif8eXsSEYK1Es2aOgDIHoBHkTUCY=", "owner": "aeneasverif", "repo": "charon", - "rev": "597fe150c3952fd197e37bc7b5ae2cb2f0d07c81", + "rev": "f1dc801340e4105927fe8f7be17b16ecaef78699", "type": "github" }, "original": { @@ -246,11 +246,11 @@ ] }, "locked": { - "lastModified": 1724811750, - "narHash": "sha256-PvhVgQ1rm3gfhK7ts4emprhh/KMkFwXogmgsQ3srR7g=", + "lastModified": 1724898214, + "narHash": "sha256-4yMO9+Lsr3zqTf4clAGGag/bfNTmc/ITOXbJQcOEok4=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "6a1c4915dca7149e7258d8c7f3ac634d8c65f6c6", + "rev": "0bc2c784e3a6ce30a2ab1b9f47325ccbed13039f", "type": "github" }, "original": { diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 9f99225..b771e05 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1346,7 +1346,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 ]; _ }; _; }; @@ -1429,15 +1429,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 @@ -1573,7 +1574,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 From 267bd6bdae8f18c797564005459eef48cd7743e3 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 29 Aug 2024 15:30:46 -0700 Subject: [PATCH 6/8] Catch up with latest upstream karamel --- lib/Cleanup1.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/Cleanup1.ml b/lib/Cleanup1.ml index 935f0dd..4114661 100644 --- a/lib/Cleanup1.ml +++ b/lib/Cleanup1.ml @@ -56,7 +56,7 @@ 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 +153,7 @@ 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 From 4e9968689823f1599522b7f8dc88e27a409c1eaa Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 29 Aug 2024 15:30:55 -0700 Subject: [PATCH 7/8] foramt --- lib/Cleanup1.ml | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/lib/Cleanup1.ml b/lib/Cleanup1.ml index 4114661..5d218bd 100644 --- 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; attempt_inline = false }; 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; attempt_inline = false }; + node = + { + atom; + name; + mut = true; + mark = ref Krml.Mark.default; + meta = None; + attempt_inline = false; + }; typ; } in From 67e4bb695bb3aa08b80d84f6dde63b84c98f92bb Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 29 Aug 2024 15:36:12 -0700 Subject: [PATCH 8/8] nix magic? --- flake.lock | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/flake.lock b/flake.lock index 904990b..2698269 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724943885, + "lastModified": 1724945475, "narHash": "sha256-Cb1/8daD2gkpHIbif8eXsSEYK1Es2aOgDIHoBHkTUCY=", - "owner": "aeneasverif", + "owner": "AeneasVerif", "repo": "charon", - "rev": "f1dc801340e4105927fe8f7be17b16ecaef78699", + "rev": "b351338f6a84c7a1afc27433eb0ffdc668b3581d", "type": "github" }, "original": { @@ -136,11 +136,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1723651234, - "narHash": "sha256-u5zHiSygZhMqoc1Z5R2bP9nRwJx3JWq5xyOlcm765wE=", + "lastModified": 1724957201, + "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=", "owner": "FStarLang", "repo": "fstar", - "rev": "608c8c2cb41cc59f5a4d07fb70677c68aae8fa8a", + "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d", "type": "github" }, "original": { @@ -155,11 +155,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1723651234, - "narHash": "sha256-u5zHiSygZhMqoc1Z5R2bP9nRwJx3JWq5xyOlcm765wE=", + "lastModified": 1724957201, + "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=", "owner": "fstarlang", "repo": "fstar", - "rev": "608c8c2cb41cc59f5a4d07fb70677c68aae8fa8a", + "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d", "type": "github" }, "original": { @@ -183,11 +183,11 @@ ] }, "locked": { - "lastModified": 1723656573, - "narHash": "sha256-sbNNlkqgBHJZwKLHbRKTKQf4tO/DhOAlC3KTzQrh92Y=", + "lastModified": 1724965512, + "narHash": "sha256-4QrNXTaIS3BxIB5XwkjC2SoOBfkqWZ66UkKPhasHIto=", "owner": "FStarLang", "repo": "karamel", - "rev": "7862fdc3899b718d39ec98568f78ec40592a622a", + "rev": "fa19d3771e6745dac67e834cd077438905ce7720", "type": "github" }, "original": { @@ -246,11 +246,11 @@ ] }, "locked": { - "lastModified": 1724898214, - "narHash": "sha256-4yMO9+Lsr3zqTf4clAGGag/bfNTmc/ITOXbJQcOEok4=", + "lastModified": 1723429325, + "narHash": "sha256-4x/32xTCd+xCwFoI/kKSiCr5LQA2ZlyTRYXKEni5HR8=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "0bc2c784e3a6ce30a2ab1b9f47325ccbed13039f", + "rev": "65e3dc0fe079fe8df087cd38f1fe6836a0373aad", "type": "github" }, "original": {