From 7bb1525ecf35bef0e947d384d43befd6f1743825 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 Aug 2024 09:29:22 +0200 Subject: [PATCH] Update charon --- charon-pin | 2 +- compiler/ExtractBase.ml | 8 +------- compiler/InterpreterStatements.ml | 12 ++---------- compiler/Pure.ml | 2 +- compiler/PureUtils.ml | 2 +- flake.lock | 6 +++--- tests/coq/misc/External_FunsExternal_Template.v | 8 ++++++++ tests/fstar/misc/External.FunsExternal.fsti | 7 +++++++ tests/lean/External/FunsExternal_Template.lean | 7 +++++++ tests/lean/Tutorial/Tutorial.lean | 7 +++++++ 10 files changed, 38 insertions(+), 23 deletions(-) diff --git a/charon-pin b/charon-pin index cb9a58633..4ec5a4ecc 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -3a56d3a39ad19db2377fa2dc712b73ebe291beb6 +9e782beeb099f447661ce91da9ba1181a94642fe diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 93001c154..197130b9a 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -2095,13 +2095,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = | None -> def.item_meta | Some trait_decl -> ( let methods = - trait_decl.required_methods - @ List.filter_map - (fun (name, opt_id) -> - match opt_id with - | None -> None - | Some id -> Some (name, id)) - trait_decl.provided_methods + trait_decl.required_methods @ trait_decl.provided_methods in match List.find_opt (fun (name, _) -> name = item_name) methods diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index b2133e346..09d654534 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -810,7 +810,6 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) (fun (s, _) -> s = method_name) trait_decl.provided_methods in - let method_id = Option.get method_id in let method_def = ctx_lookup_fun_decl ctx method_id in (* For the instantiation we have to do something peculiar because the method was defined for the trait declaration. @@ -863,17 +862,10 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) in (* Lookup the method decl in the required *and* the provided methods *) let _, method_id = - let provided = - List.filter_map - (fun (id, f) -> - match f with - | None -> None - | Some f -> Some (id, f)) - trait_decl.provided_methods - in List.find (fun (s, _) -> s = method_name) - (List.append trait_decl.required_methods provided) + (List.append trait_decl.required_methods + trait_decl.provided_methods) in let method_def = ctx_lookup_fun_decl ctx method_id in log#ldebug diff --git a/compiler/Pure.ml b/compiler/Pure.ml index a24e27cfa..ec81aedfa 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -1155,7 +1155,7 @@ type trait_decl = { consts : (trait_item_name * ty) list; types : trait_item_name list; required_methods : (trait_item_name * fun_decl_id) list; - provided_methods : (trait_item_name * fun_decl_id option) list; + provided_methods : (trait_item_name * fun_decl_id) list; } [@@deriving show] diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 818e4f8bc..2c2a4843a 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -711,7 +711,7 @@ let trait_decl_get_method (trait_decl : trait_decl) (method_name : string) : let _, id = List.find (fun (s, _) -> s = method_name) trait_decl.provided_methods in - { is_provided = true; id = Option.get id } + { is_provided = true; id } let trait_decl_is_empty (trait_decl : trait_decl) : bool = let { diff --git a/flake.lock b/flake.lock index 0d2a495fa..f51d42245 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724232574, - "narHash": "sha256-49LCpNjCW6qHUeKSTAcUh12H4UUoHGmoEKdWz5Ci2zU=", + "lastModified": 1724239793, + "narHash": "sha256-aiR5BVfWpkzZWR1WZbMhqcuDAvznV5fq2nBDCqQEczc=", "owner": "aeneasverif", "repo": "charon", - "rev": "3a56d3a39ad19db2377fa2dc712b73ebe291beb6", + "rev": "9e782beeb099f447661ce91da9ba1181a94642fe", "type": "github" }, "original": { diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v index 3d0659c4a..057012f2d 100644 --- a/tests/coq/misc/External_FunsExternal_Template.v +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -28,4 +28,12 @@ Axiom core_cell_Cell_get_mut : result (state * (core_cell_Cell_t T))))) . +(** [core::clone::Clone::clone_from]: + Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 + Name pattern: core::clone::Clone::clone_from *) +Axiom core_clone_Clone_clone_from : + forall{Self : Type} (self_clause : core_clone_Clone Self), + Self -> Self -> state -> result (state * Self) +. + End External_FunsExternal_Template. diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti index d0617f955..3d55ce054 100644 --- a/tests/fstar/misc/External.FunsExternal.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -21,3 +21,10 @@ val core_cell_Cell_get_mut core_cell_Cell_t t -> state -> result (state & (t & (t -> state -> result (state & (core_cell_Cell_t t))))) +(** [core::clone::Clone::clone_from]: + Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 + Name pattern: core::clone::Clone::clone_from *) +val core_clone_Clone_clone_from + (#self : Type0) (self_clause : core_clone_Clone self) : + self -> self -> state -> result (state & self) + diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index a8e7b90b2..9b930662e 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -24,3 +24,10 @@ axiom core.cell.Cell.get_mut core.cell.Cell T → State → Result (State × (T × (T → State → Result (State × (core.cell.Cell T))))) +/- [core::clone::Clone::clone_from]: + Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 + Name pattern: core::clone::Clone::clone_from -/ +axiom core.clone.Clone.clone_from + {Self : Type} (self_clause : core.clone.Clone Self) : + Self → Self → State → Result (State × Self) + diff --git a/tests/lean/Tutorial/Tutorial.lean b/tests/lean/Tutorial/Tutorial.lean index 153229f0f..c35550665 100644 --- a/tests/lean/Tutorial/Tutorial.lean +++ b/tests/lean/Tutorial/Tutorial.lean @@ -385,4 +385,11 @@ def add let x1 ← alloc.vec.Vec.resize U32 core.clone.CloneU32 x max1 0#u32 add_loop x1 y max1 0#u8 0#usize +/- [core::clone::Clone::clone_from]: + Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 + Name pattern: core::clone::Clone::clone_from -/ +axiom core.clone.Clone.clone_from + {Self : Type} (self_clause : core.clone.Clone Self) : + Self → Self → Result Self + end tutorial