Merge pull request #311 from Nadrieril/always-name-provided-methods

AeneasVerif · Aug 22, 2024 · 45fb761 · 45fb761
2 parents 5dd3b0f + 7bb1525
commit 45fb761
Show file tree

Hide file tree

Showing 10 changed files with 38 additions and 23 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git 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
@@ -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
@@ -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
@@ -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