From a9896500fa06ab8ce40f87e6d4a3aa9b376c6103 Mon Sep 17 00:00:00 2001 From: N1ark Date: Wed, 8 Apr 2026 11:41:35 +0100 Subject: [PATCH] Bump Charon --- charon-pin | 2 +- flake.lock | 6 +- src/BorrowCheck.ml | 4 +- src/PrePasses.ml | 65 ++++++++++--------- src/Translate.ml | 12 ++-- src/interp/Interp.ml | 11 ++-- src/interp/InterpStatements.ml | 12 ++-- src/llbc/FunsAnalysis.ml | 4 +- src/llbc/LlbcAstUtils.ml | 28 ++++++-- src/symbolic/SymbolicToPureTypes.ml | 4 +- .../borrow-check-negative.borrow-check.out | 14 ++-- ...ops-borrow-check-negative.borrow-check.out | 2 +- 12 files changed, 93 insertions(+), 71 deletions(-) diff --git a/charon-pin b/charon-pin index a17c8f3a4..1168b3b0b 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. -fbd54169205bf97e3c42cbfef95ca5807d697bfb +aabfaf42d9c3c3e2ef773f70ff98b14af5b56f26 diff --git a/flake.lock b/flake.lock index c8a341fe6..3f7b655b4 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1776276343, - "narHash": "sha256-nf7FkqqdvhMQz0yyYywIJMfS+nrCdniZbiTxmrkea78=", + "lastModified": 1776706038, + "narHash": "sha256-hBaM3MOCN/OuIYlOJz/fs9zwGun5FnVZtTEsg35svxQ=", "owner": "aeneasverif", "repo": "charon", - "rev": "fbd54169205bf97e3c42cbfef95ca5807d697bfb", + "rev": "aabfaf42d9c3c3e2ef773f70ff98b14af5b56f26", "type": "github" }, "original": { diff --git a/src/BorrowCheck.ml b/src/BorrowCheck.ml index 784a3b643..a503e614b 100644 --- a/src/BorrowCheck.ml +++ b/src/BorrowCheck.ml @@ -19,12 +19,12 @@ let borrow_check_crate (crate : crate) (marked_ids : Contexts.marked_ids) : unit (* Borrow-check *) let borrow_check_fun (fdef : fun_decl) : unit = match fdef.body with - | None -> () - | Some _ -> + | Body _ -> let synthesize = false in let _ = evaluate_function_symbolic synthesize trans_ctx marked_ids fdef in () + | _ -> () in List.iter borrow_check_fun (FunDeclId.Map.values crate.fun_decls) diff --git a/src/PrePasses.ml b/src/PrePasses.ml index bf96b5327..842ac3cd6 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -62,7 +62,7 @@ let erase_body_regions (crate : crate) (f : fun_decl) : fun_decl = (* Map *) let body = match f.body with - | Some body -> + | Body body -> let body = { body with @@ -74,8 +74,8 @@ let erase_body_regions (crate : crate) (f : fun_decl) : fun_decl = }; } in - Some { body with body = erase_visitor#visit_block 0 body.body } - | None -> None + Body { body with body = erase_visitor#visit_block 0 body.body } + | other -> other in let f : fun_decl = { f with body } in @@ -135,10 +135,10 @@ let remove_unreachable (crate : crate) (f : fun_decl) : fun_decl = end in match f.body with - | None -> f - | Some body -> + | Body body -> let body = { body with body = visitor#visit_block () body.body } in - { f with body = Some body } + { f with body = Body body } + | _ -> f (** The Rust compiler generates a unique implementation of [Default] for arrays for every choice of length. For instance, if we write: @@ -642,8 +642,8 @@ let update_loops (crate : crate) (f : fun_decl) : fun_decl = (* Map *) let body = match f.body with - | Some body -> Some { body with body = visitor#visit_block 0 body.body } - | None -> None + | Body body -> Body { body with body = visitor#visit_block 0 body.body } + | other -> other in let f : fun_decl = { f with body } in @@ -726,8 +726,8 @@ let remove_useless_joins (crate : crate) (f : fun_decl) : fun_decl = let body = match f.body with - | Some body -> Some { body with body = snd (update_block [] body.body) } - | None -> None + | Body body -> Body { body with body = snd (update_block [] body.body) } + | other -> other in let f : fun_decl = { f with body } in @@ -818,8 +818,8 @@ let remove_shallow_borrows_storage_live_dead (crate : crate) (f : fun_decl) : let body = match f.body with - | None -> None - | Some body -> Some { body with body = filter_in_body body.body } + | Body body -> Body { body with body = filter_in_body body.body } + | other -> other in let f = { f with body } in [%ldebug @@ -878,7 +878,7 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl = (* Map *) let body = match f.body with - | Some body -> + | Body body -> let new_locals = ref [] in let _, gen = LocalId.mk_stateful_generator_starting_at_id @@ -1006,7 +1006,7 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl = | _ -> [ st ] in let body_body = map_statement decompose_in_statement body.body in - Some + Body { body with body = body_body; @@ -1016,7 +1016,7 @@ let decompose_str_borrows (_ : crate) (f : fun_decl) : fun_decl = locals = body.locals.locals @ List.rev !new_locals; }; } - | None -> None + | other -> other in { f with body } @@ -1025,7 +1025,7 @@ let refresh_statement_ids (_ : crate) (f : fun_decl) : fun_decl = (* Map *) let body = match f.body with - | Some body -> + | Body body -> let _, gen_id = StatementId.fresh_stateful_generator () in (* Visit the rvalue *) @@ -1036,8 +1036,8 @@ let refresh_statement_ids (_ : crate) (f : fun_decl) : fun_decl = end in - Some { body with body = visitor#visit_block () body.body } - | None -> None + Body { body with body = visitor#visit_block () body.body } + | other -> other in { f with body } @@ -1099,8 +1099,8 @@ let simplify_panics (crate : crate) (f : fun_decl) : fun_decl = let body = match f.body with - | None -> None - | Some body -> Some { body with body = visitor#visit_block () body.body } + | Body body -> Body { body with body = visitor#visit_block () body.body } + | other -> other in { f with body } @@ -1126,8 +1126,7 @@ let decompose_global_accesses (crate : crate) (f : fun_decl) : fun_decl = (* Map *) let body = match f.body with - | None -> None - | Some body -> ( + | Body body -> ( let new_locals = ref [] in let _, gen = LocalId.mk_stateful_generator_starting_at_id @@ -1230,7 +1229,7 @@ let decompose_global_accesses (crate : crate) (f : fun_decl) : fun_decl = (* Visit all the statements and decompose the operands *) try let body_body = map_statement decompose_in_statement body.body in - Some + Body { body with body = body_body; @@ -1263,7 +1262,8 @@ let decompose_global_accesses (crate : crate) (f : fun_decl) : fun_decl = [%save_error_opt_span] error.span ("Failure when pre- processing: " ^ name ^ "; ignoring its body.\nName pattern: '" ^ name_pattern ^ "'"); - None) + Opaque) + | other -> other in { f with body } @@ -1339,8 +1339,7 @@ let replace_static (crate : crate) : crate = (* Update the uses of this definition *) let update (f : fun_decl) : fun_decl = match f.body with - | None -> f - | Some body -> + | Body body -> let visitor = object inherit [_] map_statement @@ -1366,7 +1365,8 @@ let replace_static (crate : crate) : crate = in let body = { body with body = visitor#visit_block () body.body } in - { f with body = Some body } + { f with body = Body body } + | _ -> f in let fun_decls = FunDeclId.Map.map update crate.fun_decls in { crate with fun_decls } @@ -1745,8 +1745,8 @@ let simplify_trait_calls (crate : crate) : crate = (fun _ (f : fun_decl) -> if f.item_meta.is_local then visitor#visit_fun_decl_id () f.def_id; match f.body with - | None -> () - | Some body -> visitor#visit_block () body.body) + | Body body -> visitor#visit_block () body.body + | _ -> ()) crate.fun_decls; GlobalDeclId.Map.iter @@ -1889,7 +1889,7 @@ let apply_passes (crate : crate) : crate = "After applying [" ^ pass_name ^ "]:\n" ^ Print.Crate.crate_fun_decl_to_string crate f]; f - with CFailure _ -> + with CFailure e -> (* The error was already registered, we don't need to register it twice. However, we replace the body of the function, and save an error to report to the user the fact that we will ignore the function body *) @@ -1897,7 +1897,10 @@ let apply_passes (crate : crate) : crate = let name = Print.name_to_string fmt f.item_meta.name in [%save_error] f.item_meta.span ("Ignoring the body of '" ^ name ^ "' because of previous error"); - { f with body = None } + let msg = + Errors.format_error_message_with_file_line e.file e.line e.span e.msg + in + { f with body = Error { span = f.item_meta.span; msg } } in let fun_decls : fun_decl FunDeclId.Map.t = let num_decls = FunDeclId.Map.cardinal crate.fun_decls in diff --git a/src/Translate.ml b/src/Translate.ml index 4d91c8d6e..b185ee440 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -27,8 +27,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) [%ltrace name_to_string trans_ctx fdef.item_meta.name]; match fdef.body with - | None -> None - | Some _ -> + | Body _ -> (* Evaluate - note that [evaluate_function_symbolic synthesize] catches exceptions to at least generate a dummy body if we do not abort on failure. *) let synthesize = true in @@ -36,6 +35,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) evaluate_function_symbolic synthesize trans_ctx marked_ids fdef in Some (inputs, Option.get symb) + | _ -> None (** Sanity check helper. @@ -211,7 +211,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) function) *) let ctx = - match (fdef.body, symbolic_trans) with + match (LlbcAstUtils.body_as_body fdef.body, symbolic_trans) with | None, None -> ctx | Some body, Some (input_svs, _) -> let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in @@ -394,7 +394,9 @@ let translate_crate_to_pure (crate : crate) (marked_ids : marked_ids) : let funs = FunDeclId.Map.values trans_ctx.fun_ctx.to_extract in (* Split between opaque and transparent *) let opaque, transparent = - List.partition (fun (d : fun_decl) -> Option.is_none d.body) funs + List.partition + (fun (d : fun_decl) -> not (LlbcAstUtils.body_is_known d.body)) + funs in (* Reorder the transparent functions to have the biggest first: @@ -1655,7 +1657,7 @@ let extract_translated_crate (filename : string) (dest_dir : string) If the backend is Lean the module names depends on the path, so we generate names of the shape [Types.lean], [Funs.lean], etc. because those files should be placed in the proper sub-folder. - + Otherwise, we prepend the crate name to generate, e.g., [Foo_Types.fst], [Foo_Funs.fst], etc. *) diff --git a/src/interp/Interp.ml b/src/interp/Interp.ml index 978bd5a97..8a04e46dd 100644 --- a/src/interp/Interp.ml +++ b/src/interp/Interp.ml @@ -292,7 +292,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) inst_sg.abs_regions_hierarchy region_can_end compute_abs_avalues ctx in (* Split the variables between return var, inputs and remaining locals *) - let body = Option.get fdef.body in + let body = [%add_loc] body_as_body_exn fdef.body in let ret_var = List.hd body.locals.locals in let input_vars, local_vars = Collections.List.split_at (List.tl body.locals.locals) body.locals.arg_count @@ -536,9 +536,8 @@ let evaluate_function_symbolic (synthesize : bool) (decls_ctx : decls_ctx) (* Evaluate the function *) let symbolic = try - let ctx_resl, cc = - eval_function_body config (Option.get fdef.body).body ctx - in + let body = [%add_loc] body_as_body_exn fdef.body in + let ctx_resl, cc = eval_function_body config body.body ctx in let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in (* Finish synthesizing *) if synthesize then Some (cc el) else None @@ -570,7 +569,7 @@ module Test = struct (fid : FunDeclId.id) : unit = (* Retrieve the function declaration *) let fdef = FunDeclId.Map.find fid crate.fun_decls in - let body = Option.get fdef.body in + let body = [%add_loc] body_as_body_exn fdef.body in let span = fdef.item_meta.span in (* Debug *) @@ -613,7 +612,7 @@ module Test = struct (** Small helper: return true if the function is a *transparent* unit function (no parameters, no arguments) - TODO: move *) let fun_decl_is_transparent_unit (def : fun_decl) : bool = - Option.is_some def.body + body_is_known def.body && def.generics = empty_generic_params && def.signature.inputs = [] diff --git a/src/interp/InterpStatements.ml b/src/interp/InterpStatements.ml index af21e2ac1..d5f9e5d76 100644 --- a/src/interp/InterpStatements.ml +++ b/src/interp/InterpStatements.ml @@ -1386,11 +1386,13 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span) (* We can evaluate the function call only if it is not opaque *) let body = match def.body with - | None -> + | Body body -> body + | other -> [%craise] span - ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.item_meta.name) - | Some body -> body + ("Can't evaluate a call to function: " + ^ name_to_string ctx def.item_meta.name + ^ ", it is " + ^ Charon.GAst.show_body Fmt.nop other) in (* TODO: we need to normalize the types if we want to correctly support traits *) [%cassert] body.span (generics.trait_refs = []) @@ -1399,7 +1401,7 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span) [%add_loc] Subst.make_subst_from_generics (Some span) def.generics generics Self in - let locals, body_st = Subst.fun_body_substitute_in_body subst body in + let locals, body_st = Subst.expr_body_substitute subst body in (* Evaluate the input operands *) [%sanity_check] body.span (List.length args = body.locals.arg_count); diff --git a/src/llbc/FunsAnalysis.ml b/src/llbc/FunsAnalysis.ml index b06d46a70..dad4f0a83 100644 --- a/src/llbc/FunsAnalysis.ml +++ b/src/llbc/FunsAnalysis.ml @@ -176,14 +176,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) : let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; match f.body with - | None -> + | Body body -> obj#visit_block body.body.span body.body + | _ -> let info_can_fail = match builtin_info with | None -> true | Some { can_fail } -> can_fail in obj#may_fail info_can_fail - | Some body -> obj#visit_block body.body.span body.body in List.iter visit_fun d; (* We need to know if the declaration group contains a global - note that diff --git a/src/llbc/LlbcAstUtils.ml b/src/llbc/LlbcAstUtils.ml index 86b42fefb..d87ddbbca 100644 --- a/src/llbc/LlbcAstUtils.ml +++ b/src/llbc/LlbcAstUtils.ml @@ -15,6 +15,21 @@ end module FunIdMap = Collections.MakeMap (FunIdOrderedType) module FunIdSet = Collections.MakeSet (FunIdOrderedType) +let body_as_body (f : fun_body) : block gexpr_body option = + match f with + | Body body -> Some body + | _ -> None + +let body_as_body_exn file line f = + match body_as_body f with + | Some body -> body + | None -> Errors.craise_opt_span file line None "Not a LLBC body" + +let body_is_known (f : fun_body) : bool = + match f with + | Body _ -> true + | _ -> false + let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : bound_fun_sig = match fun_id with @@ -37,7 +52,7 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_builtin : bool) let open ExtractBuiltin in let ctx = Charon.NameMatcher.ctx_from_crate k in let is_opaque_fun (d : fun_decl) : bool = - d.body = None + (not (body_is_known d.body)) (* Something to pay attention to: we must ignore trait method *declarations* (which don't have a body but must not be considered as opaque) *) && (match d.src with @@ -170,12 +185,13 @@ let compute_body_size (f : fun_body) : int = super#visit_block env st end in - visitor#visit_block () f.body; + let () = + match f with + | Body body -> visitor#visit_block () body.body + | _ -> () + in !size (** Compute the size of a function - we count the number of statements and blocks *) -let compute_fun_decl_size (f : fun_decl) : int = - match f.body with - | None -> 0 - | Some body -> compute_body_size body +let compute_fun_decl_size (f : fun_decl) : int = compute_body_size f.body diff --git a/src/symbolic/SymbolicToPureTypes.ml b/src/symbolic/SymbolicToPureTypes.ml index 06934534a..1d2b5e230 100644 --- a/src/symbolic/SymbolicToPureTypes.ml +++ b/src/symbolic/SymbolicToPureTypes.ml @@ -1046,11 +1046,11 @@ and translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx) (fdef : LlbcAst.fun_decl) : decomposed_fun_sig = let input_names = match fdef.body with - | None -> List.map (fun _ -> None) fdef.signature.inputs - | Some body -> + | Body body -> List.map (fun (v : LlbcAst.local) -> v.name) (LlbcAstUtils.fun_body_get_input_vars body) + | _ -> List.map (fun _ -> None) fdef.signature.inputs in let sg = translate_fun_sig_to_decomposed decls_ctx fdef.def_id diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out index 084185b2f..8862298fd 100644 --- a/tests/src/borrow-check-negative.borrow-check.out +++ b/tests/src/borrow-check-negative.borrow-check.out @@ -5,7 +5,7 @@ Compiler source: interp/InterpPaths.ml, line 224 Name pattern: 'borrow_check_negative::choose_test' Definition span: 'tests/src/borrow-check-negative.rs', lines 16:0-26:1 Source: 'tests/src/borrow-check-negative.rs', lines 25:12-25:14 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554 [Error] Can't end abstraction 8 as it is set as non-endable Source: 'tests/src/borrow-check-negative.rs', lines 28:0-34:1 @@ -14,7 +14,7 @@ Compiler source: interp/InterpBorrows.ml, line 1203 Name pattern: 'borrow_check_negative::choose_wrong' Definition span: 'tests/src/borrow-check-negative.rs', lines 28:0-34:1 Source: 'tests/src/borrow-check-negative.rs', lines 28:0-34:1 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554 [Error] Can not apply a projection to the ⊥ value Source: 'tests/src/borrow-check-negative.rs', lines 42:4-42:11 @@ -23,7 +23,7 @@ Compiler source: interp/InterpPaths.ml, line 224 Name pattern: 'borrow_check_negative::test_mut1' Definition span: 'tests/src/borrow-check-negative.rs', lines 36:0-43:1 Source: 'tests/src/borrow-check-negative.rs', lines 42:4-42:11 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554 [Error] Can not apply a projection to the ⊥ value Source: 'tests/src/borrow-check-negative.rs', lines 51:12-51:14 @@ -32,7 +32,7 @@ Compiler source: interp/InterpPaths.ml, line 224 Name pattern: 'borrow_check_negative::test_mut2' Definition span: 'tests/src/borrow-check-negative.rs', lines 46:0-52:1 Source: 'tests/src/borrow-check-negative.rs', lines 51:12-51:14 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554 [Error] Can not apply a projection to the ⊥ value Source: 'tests/src/borrow-check-negative.rs', lines 65:12-65:17 @@ -41,7 +41,7 @@ Compiler source: interp/InterpPaths.ml, line 224 Name pattern: 'borrow_check_negative::refs_test1' Definition span: 'tests/src/borrow-check-negative.rs', lines 59:0-66:1 Source: 'tests/src/borrow-check-negative.rs', lines 65:12-65:17 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554 [Error] Can not apply a projection to the ⊥ value Source: 'tests/src/borrow-check-negative.rs', lines 80:12-80:17 @@ -50,7 +50,7 @@ Compiler source: interp/InterpPaths.ml, line 224 Name pattern: 'borrow_check_negative::refs_test2' Definition span: 'tests/src/borrow-check-negative.rs', lines 68:0-81:1 Source: 'tests/src/borrow-check-negative.rs', lines 80:12-80:17 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554 [Error] Can not apply a projection to the ⊥ value Source: 'tests/src/borrow-check-negative.rs', lines 91:12-91:15 @@ -59,5 +59,5 @@ Compiler source: interp/InterpPaths.ml, line 224 Name pattern: 'borrow_check_negative::test_box1' Definition span: 'tests/src/borrow-check-negative.rs', lines 83:0-92:1 Source: 'tests/src/borrow-check-negative.rs', lines 91:12-91:15 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554 diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out index 9ac405ae5..33e3f166c 100644 --- a/tests/src/loops-borrow-check-negative.borrow-check.out +++ b/tests/src/loops-borrow-check-negative.borrow-check.out @@ -5,5 +5,5 @@ Compiler source: interp/InterpBorrows.ml, line 1203 Name pattern: 'loops_borrow_check_negative::loop_a_b' Definition span: 'tests/src/loops-borrow-check-negative.rs', lines 20:0-30:1 Source: 'tests/src/loops-borrow-check-negative.rs', lines 20:0-30:1 -Compiler source: interp/Interp.ml, line 555 +Compiler source: interp/Interp.ml, line 554