From e7fd38878c9861cdd8fca5d97acc3115f1578a4f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2025 14:43:06 +0100 Subject: [PATCH] Update charon --- charon-pin | 2 +- flake.lock | 6 +- src/extract/Extract.ml | 10 -- src/interp/InterpreterStatements.ml | 94 ++++++------------- tests/coq/rename_attribute/RenameAttribute.v | 22 +++-- tests/coq/traits/Traits.v | 30 ++++-- .../rename_attribute/RenameAttribute.Funs.fst | 23 +++-- tests/fstar/traits/Traits.fst | 30 ++++-- tests/lean/RenameAttribute.lean | 19 ++-- tests/lean/Traits.lean | 26 +++-- 10 files changed, 130 insertions(+), 132 deletions(-) diff --git a/charon-pin b/charon-pin index 80cce8d44..6c5811cf6 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. -ab692757d7033908c89bcc0e94d5ab1380b4f856 +91f411e4de52d2fb5c7a861a374a1b9676e03dd2 diff --git a/flake.lock b/flake.lock index ea024c25c..d1092d3a7 100644 --- a/flake.lock +++ b/flake.lock @@ -12,11 +12,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1738247409, - "narHash": "sha256-T4cRt5gSW4mpOePDWu/oaBkVJYgd04Fyn93qjw33CbI=", + "lastModified": 1739281352, + "narHash": "sha256-WR6NcKcMHvjbze83pNjvsAFuB0aOO8Iat3x2wgkNeCQ=", "owner": "aeneasverif", "repo": "charon", - "rev": "ab692757d7033908c89bcc0e94d5ab1380b4f856", + "rev": "91f411e4de52d2fb5c7a861a374a1b9676e03dd2", "type": "github" }, "original": { diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 75bf91903..4a2fd0a85 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -2456,16 +2456,6 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) (ctx, Some info) in - (* For now we do not support overriding provided methods *) - cassert __FILE__ __LINE__ - (trait_impl.provided_methods = []) - trait_impl.item_meta.span - ("Overriding trait provided methods in trait implementations is not \ - supported yet (trait impl: " - ^ name_to_string ctx trait_impl.item_meta.name - ^ ", overriden methods: " - ^ String.concat ", " (List.map fst trait_impl.provided_methods) - ^ ")"); (* Everything is taken care of by {!extract_trait_decl_register_names} *but* the name of the implementation itself *) (* Compute the name *) diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml index 5db526ac7..826cd8e64 100644 --- a/src/interp/InterpreterStatements.ml +++ b/src/interp/InterpreterStatements.ml @@ -690,78 +690,40 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) depending on whethere we call a top-level trait method impl or the method from a local clause *) match trait_ref.trait_id with - | TraitImpl (impl_id, impl_generics) -> ( + | TraitImpl (impl_id, impl_generics) -> begin (* Lookup the trait impl *) let trait_impl = ctx_lookup_trait_impl ctx impl_id in log#ltrace (lazy ("trait impl: " ^ trait_impl_to_string ctx trait_impl)); - (* First look in the required methods *) + (* Lookup the method *) let fn_ref = - Substitute.lookup_and_subst_trait_impl_required_method - trait_impl method_name impl_generics func.generics + Option.get + (Substitute.lookup_and_subst_trait_impl_method trait_impl + method_name impl_generics func.generics) + in + let method_id = fn_ref.fun_id in + let generics = fn_ref.fun_generics in + let method_def = ctx_lookup_fun_decl ctx method_id in + (* Instantiate *) + let tr_self = trait_ref.trait_id in + let fid : fun_id = FRegular method_id in + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find fid ctx.fun_ctx.regions_hierarchies + in + let inst_sg = + instantiate_fun_sig span ctx generics tr_self + method_def.signature regions_hierarchy in - match fn_ref with - | Some fn_ref -> - let method_id = fn_ref.fun_id in - let generics = fn_ref.fun_generics in - (* This is a required method *) - let method_def = ctx_lookup_fun_decl ctx method_id in - (* Instantiate *) - let tr_self = trait_ref.trait_id in - let fid : fun_id = FRegular method_id in - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find fid - ctx.fun_ctx.regions_hierarchies - in - let inst_sg = - instantiate_fun_sig span ctx generics tr_self - method_def.signature regions_hierarchy - in - (* Also update the function identifier: we want to forget - the fact that we called a trait method, and treat it as - a regular function call to the top-level function - which implements the method. In order to do this properly, - we also need to update the generics. - *) - let func = FunId fid in - (* TODO: the `trait_method_generics` look fishy *) - (func, generics, Some (generics, tr_self), method_def, inst_sg) - | None -> - (* If not found, lookup the methods provided by the trait *declaration* - (remember: for now, we forbid overriding provided methods) *) - cassert __FILE__ __LINE__ - (trait_impl.provided_methods = []) - span "Overriding provided methods is currently forbidden"; - let trait_decl = - ctx_lookup_trait_decl ctx trait_decl_ref.trait_decl_id - in - let fn_ref = - Option.get - (Substitute.lookup_and_subst_trait_decl_provided_method - trait_decl method_name trait_ref func.generics) - in - let method_id = fn_ref.fun_id in - let method_def = ctx_lookup_fun_decl ctx method_id in - let all_generics = fn_ref.fun_generics in - log#ldebug - (lazy - ("provided method call:" ^ "\n- method name: " - ^ method_name ^ "\n- all_generics:\n" - ^ generic_args_to_string ctx all_generics)); - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular method_id) - ctx.fun_ctx.regions_hierarchies - in - let tr_self = trait_ref.trait_id in - let inst_sg = - instantiate_fun_sig span ctx all_generics tr_self - method_def.signature regions_hierarchy - in - ( func.func, - func.generics, - Some (all_generics, tr_self), - method_def, - inst_sg )) + (* Also update the function identifier: we want to forget + the fact that we called a trait method, and treat it as + a regular function call to the top-level function + which implements the method. In order to do this properly, + we also need to update the generics. + *) + let func = FunId fid in + (* TODO: the `trait_method_generics` look fishy *) + (func, generics, Some (generics, tr_self), method_def, inst_sg) + end | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v index 8111a9bae..937f2ad03 100644 --- a/tests/coq/rename_attribute/RenameAttribute.v +++ b/tests/coq/rename_attribute/RenameAttribute.v @@ -22,24 +22,21 @@ Arguments BoolTest_t_getTest { _ } _. Definition boolTraitBool_getTest (self : bool) : result bool := Ok self. +(** [rename_attribute::{rename_attribute::BoolTrait for bool}::ret_true]: + Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) +Definition boolTraitBool_retTest (self : bool) : result bool := + Ok true. + (** Trait implementation: [rename_attribute::{rename_attribute::BoolTrait for bool}] Source: 'tests/src/rename_attribute.rs', lines 21:0-25:1 *) Definition BoolImpl : BoolTest_t bool := {| BoolTest_t_getTest := boolTraitBool_getTest; |}. -(** [rename_attribute::BoolTrait::ret_true]: - Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) -Definition boolTrait_retTest - {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool := - Ok true -. - (** [rename_attribute::test_bool_trait]: Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 *) Definition boolFn (T : Type) (x : bool) : result bool := - b <- boolTraitBool_getTest x; - if b then boolTrait_retTest BoolImpl x else Ok false + b <- boolTraitBool_getTest x; if b then boolTraitBool_retTest x else Ok false . (** [rename_attribute::SimpleEnum] @@ -100,4 +97,11 @@ Definition no_borrows_sum (n : nat) (max : u32) : result u32 := no_borrows_sum_loop n max 0%u32 0%u32 . +(** [rename_attribute::BoolTrait::ret_true]: + Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) +Definition boolTrait_retTest + {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool := + Ok true +. + End RenameAttribute. diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index 4f9df3c9a..2e23a83d6 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -22,24 +22,22 @@ Arguments BoolTrait_t_get_bool { _ } _. Definition boolTraitBool_get_bool (self : bool) : result bool := Ok self. +(** [traits::{traits::BoolTrait for bool}::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) +Definition boolTraitBool_ret_true (self : bool) : result bool := + Ok true. + (** Trait implementation: [traits::{traits::BoolTrait for bool}] Source: 'tests/src/traits.rs', lines 13:0-17:1 *) Definition BoolTraitBool : BoolTrait_t bool := {| BoolTrait_t_get_bool := boolTraitBool_get_bool; |}. -(** [traits::BoolTrait::ret_true]: - Source: 'tests/src/traits.rs', lines 8:4-10:5 *) -Definition boolTrait_ret_true - {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool := - Ok true -. - (** [traits::test_bool_trait_bool]: Source: 'tests/src/traits.rs', lines 19:0-21:1 *) Definition test_bool_trait_bool (x : bool) : result bool := b <- boolTraitBool_get_bool x; - if b then boolTrait_ret_true BoolTraitBool x else Ok false + if b then boolTraitBool_ret_true x else Ok false . (** [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: @@ -49,6 +47,13 @@ Definition boolTraitOption_get_bool match self with | None => Ok false | Some _ => Ok true end . +(** [traits::{traits::BoolTrait for core::option::Option}#1::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) +Definition boolTraitOption_ret_true + {T : Type} (self : option T) : result bool := + Ok true +. + (** Trait implementation: [traits::{traits::BoolTrait for core::option::Option}#1] Source: 'tests/src/traits.rs', lines 24:0-31:1 *) Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {| @@ -59,7 +64,7 @@ Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {| Source: 'tests/src/traits.rs', lines 33:0-35:1 *) Definition test_bool_trait_option {T : Type} (x : option T) : result bool := b <- boolTraitOption_get_bool x; - if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false + if b then boolTraitOption_ret_true x else Ok false . (** [traits::test_bool_trait]: @@ -696,6 +701,13 @@ Definition use_foo2 Ok (foo_foo T traitInst) . +(** [traits::BoolTrait::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) +Definition boolTrait_ret_true + {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool := + Ok true +. + (** Trait declaration: [traits::{traits::TestType}#6::test::TestTrait] Source: 'tests/src/traits.rs', lines 130:8-132:9 *) Record TestType_test_TestTrait_t (Self : Type) := mkTestType_test_TestTrait_t { diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst index 1b9b63cc1..8e9a6996c 100644 --- a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst +++ b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst @@ -12,23 +12,20 @@ include RenameAttribute.Clauses let boolTraitBool_getTest (self : bool) : result bool = Ok self +(** [rename_attribute::{rename_attribute::BoolTrait for bool}::ret_true]: + Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) +let boolTraitBool_retTest (self : bool) : result bool = + Ok true + (** Trait implementation: [rename_attribute::{rename_attribute::BoolTrait for bool}] Source: 'tests/src/rename_attribute.rs', lines 21:0-25:1 *) let boolImpl : boolTest_t bool = { getTest = boolTraitBool_getTest; } -(** [rename_attribute::BoolTrait::ret_true]: - Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) -let boolTrait_retTest - (#self : Type0) (self_clause : boolTest_t self) (self1 : self) : - result bool - = - Ok true - (** [rename_attribute::test_bool_trait]: Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 *) let boolFn (t : Type0) (x : bool) : result bool = let* b = boolTraitBool_getTest x in - if b then boolTrait_retTest boolImpl x else Ok false + if b then boolTraitBool_retTest x else Ok false (** [rename_attribute::C] Source: 'tests/src/rename_attribute.rs', lines 50:0-50:28 *) @@ -65,3 +62,11 @@ let rec no_borrows_sum_loop let no_borrows_sum (max : u32) : result u32 = no_borrows_sum_loop max 0 0 +(** [rename_attribute::BoolTrait::ret_true]: + Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *) +let boolTrait_retTest + (#self : Type0) (self_clause : boolTest_t self) (self1 : self) : + result bool + = + Ok true + diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 9f6cc5e75..e19b316b0 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -14,29 +14,31 @@ noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; } let boolTraitBool_get_bool (self : bool) : result bool = Ok self +(** [traits::{traits::BoolTrait for bool}::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) +let boolTraitBool_ret_true (self : bool) : result bool = + Ok true + (** Trait implementation: [traits::{traits::BoolTrait for bool}] Source: 'tests/src/traits.rs', lines 13:0-17:1 *) let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; } -(** [traits::BoolTrait::ret_true]: - Source: 'tests/src/traits.rs', lines 8:4-10:5 *) -let boolTrait_ret_true - (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) : - result bool - = - Ok true - (** [traits::test_bool_trait_bool]: Source: 'tests/src/traits.rs', lines 19:0-21:1 *) let test_bool_trait_bool (x : bool) : result bool = let* b = boolTraitBool_get_bool x in - if b then boolTrait_ret_true boolTraitBool x else Ok false + if b then boolTraitBool_ret_true x else Ok false (** [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: Source: 'tests/src/traits.rs', lines 25:4-30:5 *) let boolTraitOption_get_bool (#t : Type0) (self : option t) : result bool = begin match self with | None -> Ok false | Some _ -> Ok true end +(** [traits::{traits::BoolTrait for core::option::Option}#1::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) +let boolTraitOption_ret_true (#t : Type0) (self : option t) : result bool = + Ok true + (** Trait implementation: [traits::{traits::BoolTrait for core::option::Option}#1] Source: 'tests/src/traits.rs', lines 24:0-31:1 *) let boolTraitOption (t : Type0) : boolTrait_t (option t) = { @@ -47,7 +49,7 @@ let boolTraitOption (t : Type0) : boolTrait_t (option t) = { Source: 'tests/src/traits.rs', lines 33:0-35:1 *) let test_bool_trait_option (#t : Type0) (x : option t) : result bool = let* b = boolTraitOption_get_bool x in - if b then boolTrait_ret_true (boolTraitOption t) x else Ok false + if b then boolTraitOption_ret_true x else Ok false (** [traits::test_bool_trait]: Source: 'tests/src/traits.rs', lines 37:0-39:1 *) @@ -522,6 +524,14 @@ let use_foo2 = Ok (foo_foo t traitInst) +(** [traits::BoolTrait::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) +let boolTrait_ret_true + (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) : + result bool + = + Ok true + (** Trait declaration: [traits::{traits::TestType}#6::test::TestTrait] Source: 'tests/src/traits.rs', lines 130:8-132:9 *) noeq type testType_test_TestTrait_t (self : Type0) = { diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean index e085f118f..5dffae3b3 100644 --- a/tests/lean/RenameAttribute.lean +++ b/tests/lean/RenameAttribute.lean @@ -18,6 +18,11 @@ structure BoolTest (Self : Type) where def BoolTraitBool.getTest (self : Bool) : Result Bool := Result.ok self +/- [rename_attribute::{rename_attribute::BoolTrait for bool}::ret_true]: + Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/ +def BoolTraitBool.retTest (self : Bool) : Result Bool := + Result.ok true + /- Trait implementation: [rename_attribute::{rename_attribute::BoolTrait for bool}] Source: 'tests/src/rename_attribute.rs', lines 21:0-25:1 -/ @[reducible] @@ -25,19 +30,13 @@ def BoolImpl : BoolTest Bool := { getTest := BoolTraitBool.getTest } -/- [rename_attribute::BoolTrait::ret_true]: - Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/ -def BoolTrait.retTest - {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool := - Result.ok true - /- [rename_attribute::test_bool_trait]: Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 -/ def BoolFn (T : Type) (x : Bool) : Result Bool := do let b ← BoolTraitBool.getTest x if b - then BoolTrait.retTest BoolImpl x + then BoolTraitBool.retTest x else Result.ok false /- [rename_attribute::SimpleEnum] @@ -90,4 +89,10 @@ divergent def No_borrows_sum_loop def No_borrows_sum (max : U32) : Result U32 := No_borrows_sum_loop max 0#u32 0#u32 +/- [rename_attribute::BoolTrait::ret_true]: + Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/ +def BoolTrait.retTest + {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool := + Result.ok true + end rename_attribute diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 1f3c6f14d..81047656b 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -18,6 +18,11 @@ structure BoolTrait (Self : Type) where def BoolTraitBool.get_bool (self : Bool) : Result Bool := Result.ok self +/- [traits::{traits::BoolTrait for bool}::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 -/ +def BoolTraitBool.ret_true (self : Bool) : Result Bool := + Result.ok true + /- Trait implementation: [traits::{traits::BoolTrait for bool}] Source: 'tests/src/traits.rs', lines 13:0-17:1 -/ @[reducible] @@ -25,19 +30,13 @@ def BoolTraitBool : BoolTrait Bool := { get_bool := BoolTraitBool.get_bool } -/- [traits::BoolTrait::ret_true]: - Source: 'tests/src/traits.rs', lines 8:4-10:5 -/ -def BoolTrait.ret_true - {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := - Result.ok true - /- [traits::test_bool_trait_bool]: Source: 'tests/src/traits.rs', lines 19:0-21:1 -/ def test_bool_trait_bool (x : Bool) : Result Bool := do let b ← BoolTraitBool.get_bool x if b - then BoolTrait.ret_true BoolTraitBool x + then BoolTraitBool.ret_true x else Result.ok false /- [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: @@ -47,6 +46,11 @@ def BoolTraitOption.get_bool {T : Type} (self : Option T) : Result Bool := | none => Result.ok false | some _ => Result.ok true +/- [traits::{traits::BoolTrait for core::option::Option}#1::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 -/ +def BoolTraitOption.ret_true {T : Type} (self : Option T) : Result Bool := + Result.ok true + /- Trait implementation: [traits::{traits::BoolTrait for core::option::Option}#1] Source: 'tests/src/traits.rs', lines 24:0-31:1 -/ @[reducible] @@ -60,7 +64,7 @@ def test_bool_trait_option {T : Type} (x : Option T) : Result Bool := do let b ← BoolTraitOption.get_bool x if b - then BoolTrait.ret_true (BoolTraitOption T) x + then BoolTraitOption.ret_true x else Result.ok false /- [traits::test_bool_trait]: @@ -543,6 +547,12 @@ def use_foo2 := Result.ok (Foo.FOO T TraitInst) +/- [traits::BoolTrait::ret_true]: + Source: 'tests/src/traits.rs', lines 8:4-10:5 -/ +def BoolTrait.ret_true + {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := + Result.ok true + /- Trait declaration: [traits::{traits::TestType}#6::test::TestTrait] Source: 'tests/src/traits.rs', lines 130:8-132:9 -/ structure TestType.test.TestTrait (Self : Type) where