From ba29d42d94ecbaa68c4966da790b4066b0bad130 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 2 Sep 2024 14:09:35 +0200 Subject: [PATCH] Update charon --- charon-pin | 2 +- compiler/Extract.ml | 9 +++++---- flake.lock | 12 ++++++------ flake.nix | 2 +- tests/test_runner/run_test.ml | 8 +++++++- 5 files changed, 20 insertions(+), 13 deletions(-) diff --git a/charon-pin b/charon-pin index f19aa722a..c08bfe738 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. -f1dc801340e4105927fe8f7be17b16ecaef78699 +cdc1dcde447a50cbc20336c79b21b42ac977b7fd diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 112a36d79..f036c8d6d 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2774,6 +2774,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) * Extract the items *) let trait_decl_id = impl.impl_trait.trait_decl_id in + let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.crate.trait_decls in (* The constants *) List.iter @@ -2810,11 +2811,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) impl.types; (* The parent clauses *) - TraitClauseId.iteri - (fun clause_id trait_ref -> + List.iter + (fun (clause, trait_ref) -> let item_name = ctx_get_trait_parent_clause impl.item_meta.span trait_decl_id - clause_id ctx + clause.T.clause_id ctx in let ty () = F.pp_print_space fmt (); @@ -2822,7 +2823,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) false trait_ref in extract_trait_impl_item ctx fmt item_name ty) - impl.parent_trait_refs; + (List.combine trait_decl.parent_clauses impl.parent_trait_refs); (* The required methods *) List.iter diff --git a/flake.lock b/flake.lock index d3e2bbdf8..de4b5a758 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724943885, - "narHash": "sha256-Cb1/8daD2gkpHIbif8eXsSEYK1Es2aOgDIHoBHkTUCY=", + "lastModified": 1725287105, + "narHash": "sha256-KUxQtYXe3/BL9XwGfiTS3tjDe0nEEF9Npp5BOHCe8ig=", "owner": "aeneasverif", "repo": "charon", - "rev": "f1dc801340e4105927fe8f7be17b16ecaef78699", + "rev": "cdc1dcde447a50cbc20336c79b21b42ac977b7fd", "type": "github" }, "original": { @@ -272,11 +272,11 @@ ] }, "locked": { - "lastModified": 1724898214, - "narHash": "sha256-4yMO9+Lsr3zqTf4clAGGag/bfNTmc/ITOXbJQcOEok4=", + "lastModified": 1725243956, + "narHash": "sha256-0A5ZP8uDCyBdYUzayZfy6JFdTefP79oZVAjyqA/yuSI=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "0bc2c784e3a6ce30a2ab1b9f47325ccbed13039f", + "rev": "a10c8092d5f82622be79ed4dd12289f72011f850", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 7fdc5c65c..87b76dbe0 100644 --- a/flake.nix +++ b/flake.nix @@ -90,7 +90,7 @@ betree-llbc = charon.extractCrateWithCharon.${system} { name = "betree"; src = ./tests/src/betree; - charonFlags = "--polonius --opaque=crate::betree_utils"; + charonFlags = "--polonius --opaque=crate::betree_utils --hide-marker-traits"; craneExtraArgs.checkPhaseCargoCommand = '' cargo rustc -- --test -Zpolonius ./target/debug/betree diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 3d4e587d7..f503d93a9 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -117,6 +117,7 @@ let run_charon (env : runner_env) (case : Input.t) = [ env.charon_path; "--no-cargo"; + "--hide-marker-traits"; "--input"; case.path; "--crate"; @@ -143,7 +144,12 @@ let run_charon (env : runner_env) (case : Input.t) = in if generate then ( let args = - [ env.charon_path; "--dest"; Filename_unix.realpath env.llbc_dir ] + [ + env.charon_path; + "--hide-marker-traits"; + "--dest"; + Filename_unix.realpath env.llbc_dir; + ] in let args = List.append args case.charon_options in (* Run Charon inside the crate *)