From 32469fd62495126dbe44a44c5eef40e822fb6b73 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 18 Dec 2024 12:41:41 +0000 Subject: [PATCH 1/6] Improve error reporting --- src/Config.ml | 3 ++ src/Errors.ml | 16 ++++--- src/Main.ml | 10 +++- src/PrePasses.ml | 2 +- src/Translate.ml | 10 ++-- src/extract/Extract.ml | 4 +- src/extract/ExtractBase.ml | 8 ++-- src/extract/ExtractTypes.ml | 2 +- src/interp/Interpreter.ml | 86 +++++++++++++++++----------------- src/llbc/FunsAnalysis.ml | 2 +- src/pure/PureUtils.ml | 2 +- src/symbolic/SymbolicToPure.ml | 4 +- 12 files changed, 83 insertions(+), 66 deletions(-) diff --git a/src/Config.ml b/src/Config.ml index 7d315ca4..d990986b 100644 --- a/src/Config.ml +++ b/src/Config.ml @@ -45,6 +45,9 @@ let if_backend (f : unit -> 'a) (default : 'a) : 'a = | None -> default | Some _ -> f () +(** Print the source code span which emitted errors *) +let print_error_emitters = ref false + (** Print all the external definitions which are not listed in the builtin functions *) let print_unknown_externals = ref false diff --git a/src/Errors.ml b/src/Errors.ml index a3a5e261..68b1de13 100644 --- a/src/Errors.ml +++ b/src/Errors.ml @@ -30,20 +30,24 @@ let format_error_message_with_file_line (file : string) (line : int) exception CFailure of (Meta.span option * string) -let error_list : (Meta.span option * string) list ref = ref [] +let error_list : (string * int * Meta.span option * string) list ref = ref [] -let push_error (span : Meta.span option) (msg : string) = - error_list := (span, msg) :: !error_list +let push_error (file : string) (line : int) (span : Meta.span option) + (msg : string) = + error_list := (file, line, span, msg) :: !error_list (** Register an error, and throw an exception if [throw] is true *) -let save_error (file : string) (line : int) (span : Meta.span option) +let save_error_opt_span (file : string) (line : int) (span : Meta.span option) (msg : string) = - push_error span msg; + push_error file line span msg; if !Config.fail_hard then ( let msg = format_error_message_with_file_line file line span msg in log#serror (msg ^ "\n"); raise (Failure msg)) +let save_error (file : string) (line : int) (span : Meta.span) (msg : string) = + save_error_opt_span file line (Some span) msg + let craise_opt_span (file : string) (line : int) (span : Meta.span option) (msg : string) = if !Config.fail_hard then ( @@ -51,7 +55,7 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option) log#serror (msg ^ "\n"); raise (Failure msg)) else - let () = push_error span msg in + let () = push_error file line span msg in raise (CFailure (span, msg)) let craise (file : string) (line : int) (span : Meta.span) (msg : string) = diff --git a/src/Main.ml b/src/Main.ml index fa624b7b..370b7737 100644 --- a/src/Main.ml +++ b/src/Main.ml @@ -100,6 +100,10 @@ let () = let spec_ls = [ + ( "-print-error-emitters", + Arg.Set print_error_emitters, + " Whenever reporting an error, print the span of the source code of \ + Aeneas which emitted the error" ); ( "-borrow-check", Arg.Set borrow_check, " Only borrow-check the program and do not generate any translation" ); @@ -515,7 +519,11 @@ let () = if !Errors.error_list <> [] then ( List.iter - (fun (span, msg) -> log#serror (Errors.format_error_message span msg)) + (fun (file, line, span, msg) -> + if !print_error_emitters then + log#serror + (Errors.format_error_message_with_file_line file line span msg) + else log#serror (Errors.format_error_message span msg)) (* Reverse the list of error messages so that we print them from the earliest to the latest. *) (List.rev !Errors.error_list); diff --git a/src/PrePasses.ml b/src/PrePasses.ml index 6dd2d61c..d10ab763 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -533,7 +533,7 @@ let apply_passes (crate : crate) : crate = report to the user the fact that we will ignore the function body *) let fmt = Print.Crate.crate_to_fmt_env crate in let name = Print.name_to_string fmt f.item_meta.name in - save_error __FILE__ __LINE__ (Some f.item_meta.span) + save_error __FILE__ __LINE__ f.item_meta.span ("Ignoring the body of '" ^ name ^ "' because of previous error"); { f with body = None } in diff --git a/src/Translate.ml b/src/Translate.ml index 11296a97..eded2c5f 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -213,7 +213,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) with CFailure (span, _) -> let name = name_to_string trans_ctx fdef.item_meta.name in let name_pattern = name_to_pattern_string trans_ctx fdef.item_meta.name in - save_error __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ span ("Could not translate the function '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None @@ -252,7 +252,7 @@ let translate_crate_to_pure (crate : crate) : let name_pattern = name_to_pattern_string trans_ctx global.item_meta.name in - save_error __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ span ("Could not translate the global declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -275,7 +275,7 @@ let translate_crate_to_pure (crate : crate) : let name_pattern = name_to_pattern_string trans_ctx fdef.item_meta.name in - save_error __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ span ("Could not translate the function signature of '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); @@ -300,7 +300,7 @@ let translate_crate_to_pure (crate : crate) : let name_pattern = name_to_pattern_string trans_ctx d.item_meta.name in - save_error __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ span ("Could not translate the trait declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -318,7 +318,7 @@ let translate_crate_to_pure (crate : crate) : let name_pattern = name_to_pattern_string trans_ctx d.item_meta.name in - save_error __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ span ("Could not translate the trait instance '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 2bb39228..22a2e414 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -248,7 +248,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) ^ string_of_int (List.length types) ^ " type arguments" in - save_error __FILE__ __LINE__ None err; + save_error_opt_span __FILE__ __LINE__ None err; Result.Error (types, err)) else let filter_f = @@ -625,7 +625,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) | Error (types, err) -> extract_generic_args span ctx fmt TypeDeclId.Set.empty ~explicit { generics with types }; - save_error __FILE__ __LINE__ (Some span) err; + save_error __FILE__ __LINE__ span err; F.pp_print_string fmt "(\"ERROR: ill-formed builtin: invalid number of filtering \ arguments\")"); diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index 6729d5c2..490799c9 100644 --- a/src/extract/ExtractBase.ml +++ b/src/extract/ExtractBase.ml @@ -281,7 +281,7 @@ let report_name_collision (id_to_string : id -> string) We don't link this error to any span information because we already put the span information about the two problematic definitions in the error message above. *) - save_error __FILE__ __LINE__ None err + save_error_opt_span __FILE__ __LINE__ None err let names_map_get_id_from_name (name : string) (nm : names_map) : (id * Meta.span option) option = @@ -315,7 +315,7 @@ let names_map_add (id_to_string : id -> string) ((id, span) : id * span option) ^ ":\nThe chosen name is already in the names set: " ^ name in (* If we fail hard on errors, raise an exception *) - save_error __FILE__ __LINE__ span err); + save_error_opt_span __FILE__ __LINE__ span err); (* Insert *) names_map_add_unchecked (id, span) name nm @@ -463,7 +463,7 @@ let names_maps_get (span : Meta.span option) (id_to_string : id -> string) "Could not find: " ^ id_to_string id ^ "\nNames map:\n" ^ map_to_string m in - save_error __FILE__ __LINE__ span err; + save_error_opt_span __FILE__ __LINE__ span err; "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)") else let m = nm.names_map.id_to_name in @@ -474,7 +474,7 @@ let names_maps_get (span : Meta.span option) (id_to_string : id -> string) "Could not find: " ^ id_to_string id ^ "\nNames map:\n" ^ map_to_string m in - save_error __FILE__ __LINE__ span err; + save_error_opt_span __FILE__ __LINE__ span err; "(ERROR: \"" ^ id_to_string id ^ "\")" type names_map_init = { diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index 8af8f132..3c2f6691 100644 --- a/src/extract/ExtractTypes.ml +++ b/src/extract/ExtractTypes.ml @@ -730,7 +730,7 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx) | Self -> (* This has a specific treatment depending on the item we're extracting (associated type, etc.). We should have caught this elsewhere. *) - save_error __FILE__ __LINE__ (Some span) "Unexpected occurrence of `Self`"; + save_error __FILE__ __LINE__ span "Unexpected occurrence of `Self`"; F.pp_print_string fmt "ERROR(\"Unexpected Self\")" | TraitImpl (id, generics) -> (* Lookup the the information about the explicit/implicit parameters. *) diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml index 6c634bd2..80a5d7da 100644 --- a/src/interp/Interpreter.ml +++ b/src/interp/Interpreter.ml @@ -35,49 +35,51 @@ let compute_contexts (m : crate) : decls_ctx = } in (* Split the declaration groups between the declaration kinds (types, functions, etc.) *) - let type_decls_groups = - match split_declarations_to_group_maps m.declarations with - | Ok (type_decls_groups, _, _, _, _) -> type_decls_groups - | Error mixed_groups -> - (* We detected mixed groups: print a nice error message *) - let any_decl_id_to_string (id : any_decl_id) : string = - let kind = any_decl_id_to_kind_name id in - let meta = LlbcAstUtils.crate_get_item_meta m id in - let s = - match meta with - | None -> show_any_decl_id id - | Some meta -> - kind ^ "(" ^ span_to_string meta.span ^ "): " - ^ Print.name_to_string fmt_env meta.name - in - "- " ^ s - in - let group_to_msg (i : int) (g : mixed_declaration_group) : string = - let ids = g_declaration_group_to_list g in - let decls = List.map any_decl_id_to_string ids in - let local_requires = - LlbcAstUtils.find_local_transitive_dep m (AnyDeclIdSet.of_list ids) - in - let local_requires = List.map span_to_string local_requires in - let local_requires = - if local_requires <> [] then - "\n\n\ - The declarations in this group are (transitively) used at the \ - following location(s):\n" - ^ String.concat "\n" local_requires - else "" - in - "# Group " - ^ string_of_int (i + 1) - ^ ":\n" ^ String.concat "\n" decls ^ local_requires - in - let msgs = List.mapi group_to_msg mixed_groups in - let msgs = String.concat "\n\n" msgs in - craise_opt_span __FILE__ __LINE__ None - ("Detected groups of mixed mutually recursive definitions (such as a \ - type mutually recursive with a function, or a function mutually \ - recursive with a trait implementation):\n\n" ^ msgs) + let type_decls_groups, _, _, _, _, mixed_groups = + split_declarations_to_group_maps m.declarations in + (* Check if there are mixed groups: if there are, we report an error + and ignore those *) + (if mixed_groups <> [] then + (* We detected mixed groups: print a nice error message *) + let any_decl_id_to_string (id : any_decl_id) : string = + let kind = any_decl_id_to_kind_name id in + let meta = LlbcAstUtils.crate_get_item_meta m id in + let s = + match meta with + | None -> show_any_decl_id id + | Some meta -> + kind ^ "(" ^ span_to_string meta.span ^ "): " + ^ Print.name_to_string fmt_env meta.name + in + "- " ^ s + in + let group_to_msg (i : int) (g : mixed_declaration_group) : string = + let ids = g_declaration_group_to_list g in + let decls = List.map any_decl_id_to_string ids in + let local_requires = + LlbcAstUtils.find_local_transitive_dep m (AnyDeclIdSet.of_list ids) + in + let local_requires = List.map span_to_string local_requires in + let local_requires = + if local_requires <> [] then + "\n\n\ + The declarations in this group are (transitively) used at the \ + following location(s):\n" + ^ String.concat "\n" local_requires + else "" + in + "# Group " + ^ string_of_int (i + 1) + ^ ":\n" ^ String.concat "\n" decls ^ local_requires + in + let msgs = List.mapi group_to_msg mixed_groups in + let msgs = String.concat "\n\n" msgs in + save_error_opt_span __FILE__ __LINE__ None + ("Detected groups of mixed mutually recursive definitions (such as a \ + type mutually recursive with a function, or a function mutually \ + recursive with a trait implementation):\n\n" ^ msgs)); + let type_infos = TypesAnalysis.analyze_type_declarations type_decls type_decls_list in diff --git a/src/llbc/FunsAnalysis.ml b/src/llbc/FunsAnalysis.ml index 035782f3..4fb0551e 100644 --- a/src/llbc/FunsAnalysis.ml +++ b/src/llbc/FunsAnalysis.ml @@ -221,7 +221,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) analyze_fun_decl_group (g_declaration_group_to_list decl); analyze_decl_groups decls' | MixedGroup ids :: _ -> - craise_opt_span __FILE__ __LINE__ None + save_error_opt_span __FILE__ __LINE__ None ("Mixed declaration groups are not supported yet: [" ^ String.concat ", " (List.map Charon.PrintGAst.any_decl_id_to_string diff --git a/src/pure/PureUtils.ml b/src/pure/PureUtils.ml index 7dac890e..24a3c568 100644 --- a/src/pure/PureUtils.ml +++ b/src/pure/PureUtils.ml @@ -408,7 +408,7 @@ let mk_app (span : Meta.span) (app : texpression) (arg : texpression) : texpression = let raise_or_return msg = (* We shouldn't get there, so we save an error (and eventually raise an exception) *) - save_error __FILE__ __LINE__ (Some span) msg; + save_error __FILE__ __LINE__ span msg; let e = App (app, arg) in (* Dummy type - TODO: introduce an error type *) let ty = app.ty in diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index edc6721b..ee41e440 100644 --- a/src/symbolic/SymbolicToPure.ml +++ b/src/symbolic/SymbolicToPure.ml @@ -2709,7 +2709,7 @@ let decompose_let_match (ctx : bs_ctx) (* This is a bug, but we might want to continue generating the model: as an escape hatch, simply use the original variable (this will lead to incorrect code of course) *) - save_error __FILE__ __LINE__ (Some ctx.span) + save_error __FILE__ __LINE__ ctx.span ("Internal error: could not find variable. Please report an \ issue. Debugging information:" ^ "\n- v.id: " ^ VarId.to_string v.id ^ "\n- ctx.var_id_to_default: " @@ -4706,7 +4706,7 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = let name_pattern = TranslateCore.name_to_pattern_string ctx d.item_meta.name in - save_error __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ span ("Could not translate type decl '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None) From 9f477c75c766a5c6670e239a095c367ddb7d26d4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 18 Dec 2024 15:18:03 +0000 Subject: [PATCH 2/6] Improve the error messages and add support for arrays with borrows --- src/Errors.ml | 10 +- src/PrePasses.ml | 147 ++++++++++++++++++++++++++- src/interp/InterpreterExpressions.ml | 58 ++++++++--- src/interp/InterpreterUtils.ml | 1 + src/llbc/Print.ml | 4 + 5 files changed, 202 insertions(+), 18 deletions(-) diff --git a/src/Errors.ml b/src/Errors.ml index 68b1de13..548ec2a7 100644 --- a/src/Errors.ml +++ b/src/Errors.ml @@ -8,12 +8,18 @@ let raw_span_to_string (raw_span : Meta.raw_span) = let loc_to_string (l : Meta.loc) : string = string_of_int l.line ^ ":" ^ string_of_int l.col in - "Source: '" ^ file ^ "', lines " + "'" ^ file ^ "', lines " ^ loc_to_string raw_span.beg_loc ^ "-" ^ loc_to_string raw_span.end_loc -let span_to_string (span : Meta.span) = raw_span_to_string span.span +let span_to_string (span : Meta.span) = + let generated_from = + match span.generated_from_span with + | None -> "" + | Some span -> "; this macro is used at: " ^ raw_span_to_string span + in + "Source: " ^ raw_span_to_string span.span ^ generated_from let format_error_message (span : Meta.span option) (msg : string) = let span = diff --git a/src/PrePasses.ml b/src/PrePasses.ml index d10ab763..e8512d25 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -520,9 +520,154 @@ let filter_type_aliases (crate : crate) : crate = crate.declarations; } +(** Whenever we write a string literal in Rust, rustc actually + introduces a constant of type [&str]. + Generally speaking, because [str] is unsized, it doesn't + make sense to manipulate values of type [str] directly. + But in the context of Aeneas, it is reasonable to decompose + those literals into: a string stored in a local variable, + then a borrow of this variable. + *) +let decompose_str_borrows (f : fun_decl) : fun_decl = + (* Map *) + let body = + match f.body with + | Some body -> + let new_locals = ref [] in + let _, gen = + VarId.mk_stateful_generator_starting_at_id + (VarId.of_int (List.length body.locals.vars)) + in + let fresh_local ty = + let local = { index = gen (); var_ty = ty; name = None } in + new_locals := local :: !new_locals; + local.index + in + + (* Function to decompose a constant literal *) + let decompose_rvalue (span : Meta.span) (lv : place) (rv : rvalue) + (next : statement option) : raw_statement = + let new_statements = ref [] in + + (* Visit the rvalue *) + let visitor = + object + inherit [_] map_statement as super + + (* We have to visit all the constant operands. + As we might need to replace them with borrows, while borrows + are rvalues (i.e., not operands) we have to introduce two + intermediate statements: the string initialization, then + the borrow, that we can finally move. + *) + method! visit_Constant env cv = + match (cv.value, cv.ty) with + | ( CLiteral (VStr str), + TRef (_, (TAdt (TBuiltin TStr, _) as str_ty), ref_kind) ) -> + (* We need to introduce intermediate assignments *) + (* First the string initialization *) + let local_id = + let local_id = fresh_local str_ty in + let new_cv : constant_expr = + { value = CLiteral (VStr str); ty = str_ty } + in + let st = + { + span; + content = + Assign + ( { kind = PlaceBase local_id; ty = str_ty }, + Use (Constant new_cv) ); + comments_before = []; + } + in + new_statements := st :: !new_statements; + local_id + in + (* Then the borrow *) + let local_id = + let nlocal_id = fresh_local cv.ty in + let bkind = + match ref_kind with + | RMut -> BMut + | RShared -> BShared + in + let rv = + RvRef ({ kind = PlaceBase local_id; ty = str_ty }, bkind) + in + let lv = { kind = PlaceBase nlocal_id; ty = cv.ty } in + let st = + { + span; + content = Assign (lv, rv); + comments_before = []; + } + in + new_statements := st :: !new_statements; + nlocal_id + in + (* Finally we can move the value *) + Move { kind = PlaceBase local_id; ty = cv.ty } + | _ -> super#visit_Constant env cv + end + in + + let rv = visitor#visit_rvalue () rv in + + (* Construct the sequence *) + let assign = + { span; content = Assign (lv, rv); comments_before = [] } + in + let statements, last = + match next with + | None -> (!new_statements, assign) + | Some st -> (assign :: !new_statements, st) + in + (* Note that the new statements are in reverse order *) + (List.fold_left + (fun st nst -> + { span; content = Sequence (nst, st); comments_before = [] }) + last statements) + .content + in + + (* Visit all the statements and decompose the literals *) + let visitor = + object + inherit [_] map_statement as super + method! visit_statement _ st = super#visit_statement st.span st + + method! visit_Sequence span st1 st2 = + match st1.content with + | Assign (lv, rv) -> decompose_rvalue st1.span lv rv (Some st2) + | _ -> super#visit_Sequence span st1 st2 + + method! visit_Assign span lv rv = decompose_rvalue span lv rv None + end + in + + let body_body = visitor#visit_statement body.body.span body.body in + Some + { + body with + body = body_body; + locals = + { + body.locals with + vars = body.locals.vars @ List.rev !new_locals; + }; + } + | None -> None + in + { f with body } + let apply_passes (crate : crate) : crate = let function_passes = - [ remove_loop_breaks crate; remove_shallow_borrows crate ] + [ + remove_loop_breaks crate; + remove_shallow_borrows crate; + decompose_str_borrows; + ] in (* Attempt to apply a pass: if it fails we replace the body by [None] *) let apply_function_pass (pass : fun_decl -> fun_decl) (f : fun_decl) = diff --git a/src/interp/InterpreterExpressions.ml b/src/interp/InterpreterExpressions.ml index a1adc3f2..db1f3c04 100644 --- a/src/interp/InterpreterExpressions.ml +++ b/src/interp/InterpreterExpressions.ml @@ -278,10 +278,19 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span) match op with | Constant cv -> ( match cv.value with - | CLiteral lit -> - ( literal_to_typed_value span (ty_as_literal cv.ty) lit, - ctx, - fun e -> e ) + | CLiteral lit -> ( + (* FIXME: the str type is not in [literal_type] *) + match cv.ty with + | TAdt (TBuiltin TStr, _) -> + let v : typed_value = { value = VLiteral lit; ty = cv.ty } in + (v, ctx, fun e -> e) + | TLiteral lit_ty -> + (literal_to_typed_value span lit_ty lit, ctx, fun e -> e) + | _ -> + craise __FILE__ __LINE__ span + ("Encountered an incorrectly typed constant: " + ^ constant_expr_to_string ctx cv + ^ " : " ^ ty_to_string ctx cv.ty)) | CTraitConst (trait_ref, const_name) -> let ctx0 = ctx in (* Simply introduce a fresh symbolic value *) @@ -815,9 +824,18 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span) | TBuiltin _ -> craise __FILE__ __LINE__ span "Unreachable") | AggregatedArray (ety, cg) -> (* Sanity check: all the values have the proper type *) - sanity_check __FILE__ __LINE__ + classert __FILE__ __LINE__ (List.for_all (fun (v : typed_value) -> v.ty = ety) values) - span; + span + (lazy + ("Aggregated array: some values don't have the proper type:" + ^ "\n- expected type: " ^ ty_to_string ctx ety ^ "\n- values: [" + ^ String.concat ", " + (List.map + (fun (v : typed_value) -> + typed_value_to_string ctx v ^ " : " ^ ty_to_string ctx v.ty) + values) + ^ "]")); (* Sanity check: the number of values is consistent with the length *) let len = (literal_as_scalar (const_generic_as_literal cg)).value in sanity_check __FILE__ __LINE__ @@ -829,15 +847,25 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span) value equal to the array. The reason is that otherwise, the array we introduce here might be duplicated in the generated code: by introducing a symbolic value we introduce a let-binding - in the generated code. *) - let saggregated = mk_fresh_symbolic_typed_value span ty in - (* Update the symbolic ast *) - let cf e = - (* Introduce the symbolic value in the AST *) - let sv = ValuesUtils.value_as_symbolic span saggregated.value in - SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e) - in - (saggregated, cf) + in the generated code. + + TODO: generalize to the case where we have an array of borrows. + For now, we introduce a symbolic value only in the case the + array doesn't contain borrows. + *) + if ty_has_borrows (Some span) ctx.type_ctx.type_infos ty then + let value = VAdt { variant_id = None; field_values = values } in + let value : typed_value = { value; ty } in + (value, fun e -> e) + else + let saggregated = mk_fresh_symbolic_typed_value span ty in + (* Update the symbolic ast *) + let cf e = + (* Introduce the symbolic value in the AST *) + let sv = ValuesUtils.value_as_symbolic span saggregated.value in + SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e) + in + (saggregated, cf) | AggregatedClosure _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" in diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index 8d3111b3..3e23f9ff 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -30,6 +30,7 @@ let operand_to_string = Print.EvalCtx.operand_to_string let fun_sig_to_string = Print.EvalCtx.fun_sig_to_string let inst_fun_sig_to_string = Print.EvalCtx.inst_fun_sig_to_string let ty_to_string = Print.EvalCtx.ty_to_string +let constant_expr_to_string = Print.EvalCtx.constant_expr_to_string let generic_args_to_string = Print.EvalCtx.generic_args_to_string let trait_ref_to_string = Print.EvalCtx.trait_ref_to_string let trait_decl_ref_to_string = Print.EvalCtx.trait_decl_ref_to_string diff --git a/src/llbc/Print.ml b/src/llbc/Print.ml index 713a0d6a..3582cbc3 100644 --- a/src/llbc/Print.ml +++ b/src/llbc/Print.ml @@ -565,6 +565,10 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in ty_to_string env t + let constant_expr_to_string (ctx : eval_ctx) (c : constant_expr) : string = + let env = eval_ctx_to_fmt_env ctx in + constant_expr_to_string env c + let generic_params_to_strings (ctx : eval_ctx) (x : generic_params) : string list * string list = let env = eval_ctx_to_fmt_env ctx in From 061f32481c1b20654761d26c31774d959fbe0d7d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 18 Dec 2024 17:28:30 +0000 Subject: [PATCH 3/6] Make Aeneas a lot more resilient to errors --- src/Errors.ml | 42 ++++++- src/Main.ml | 25 ++-- src/PrePasses.ml | 2 +- src/Translate.ml | 148 ++++++++++++++++++------ src/extract/Extract.ml | 43 ++++--- src/extract/ExtractTypes.ml | 12 +- src/interp/Interpreter.ml | 9 +- src/interp/InterpreterLoopsMatchCtxs.ml | 2 +- src/interp/InterpreterStatements.ml | 5 +- src/llbc/RegionsHierarchy.ml | 20 +++- src/llbc/TypesAnalysis.ml | 5 +- src/symbolic/SymbolicToPure.ml | 21 ++-- 12 files changed, 238 insertions(+), 96 deletions(-) diff --git a/src/Errors.ml b/src/Errors.ml index 548ec2a7..4a41a4bf 100644 --- a/src/Errors.ml +++ b/src/Errors.ml @@ -17,7 +17,9 @@ let span_to_string (span : Meta.span) = let generated_from = match span.generated_from_span with | None -> "" - | Some span -> "; this macro is used at: " ^ raw_span_to_string span + | Some span -> + "; this code is generated from a macro invocation at: " + ^ raw_span_to_string span in "Source: " ^ raw_span_to_string span.span ^ generated_from @@ -34,7 +36,15 @@ let format_error_message_with_file_line (file : string) (line : int) "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n" ^ format_error_message span msg -exception CFailure of (Meta.span option * string) +type cfailure = { + span : Meta.span option; + file : string; + line : int; + msg : string; +} +[@@deriving show] + +exception CFailure of cfailure let error_list : (string * int * Meta.span option * string) list ref = ref [] @@ -62,11 +72,25 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option) raise (Failure msg)) else let () = push_error file line span msg in - raise (CFailure (span, msg)) + raise (CFailure { span; file; line; msg }) let craise (file : string) (line : int) (span : Meta.span) (msg : string) = craise_opt_span file line (Some span) msg +(** Throw an exception, but do not register an error *) +let craise_opt_span_silent (file : string) (line : int) + (span : Meta.span option) (msg : string) = + if !Config.fail_hard then + let msg = format_error_message_with_file_line file line span msg in + raise (Failure msg) + else + let () = push_error file line span msg in + raise (CFailure { span; file; line; msg }) + +let craise_silent (file : string) (line : int) (span : Meta.span) (msg : string) + = + craise_opt_span_silent file line (Some span) msg + (** Lazy assert *) let classert_opt_span (file : string) (line : int) (b : bool) (span : Meta.span option) (msg : string Lazy.t) = @@ -113,3 +137,15 @@ let cassert_warn (file : string) (line : int) (b : bool) (span : Meta.span) let exec_raise = craise let exec_assert = cassert + +let silent_unwrap_opt_span (file : string) (line : int) + (span : Meta.span option) (x : 'a option) : 'a = + match x with + | Some x -> x + | None -> + craise_opt_span_silent file line span + "Internal error: please file an issue" + +let silent_unwrap (file : string) (line : int) (span : Meta.span) + (x : 'a option) : 'a = + silent_unwrap_opt_span file line (Some span) x diff --git a/src/Main.ml b/src/Main.ml index 370b7737..445c02d8 100644 --- a/src/Main.ml +++ b/src/Main.ml @@ -500,22 +500,15 @@ let () = @ trait_impls))); ()); - (* There may be exceptions to catch *) - (try - (* Apply the pre-passes *) - let m = Aeneas.PrePasses.apply_passes m in - - (* Test the unit functions with the concrete interpreter *) - if !test_unit_functions then Test.test_unit_functions m; - - (* Translate or borrow-check the crate *) - if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m - else Aeneas.Translate.translate_crate filename dest_dir m - with Errors.CFailure (_, _) -> - (* In theory it shouldn't happen, but there may be uncaught errors - - note that we let the [Failure] exceptions go through (they are - send if we use the option [-abort-on-error] *) - ()); + (* Apply the pre-passes *) + let m = Aeneas.PrePasses.apply_passes m in + + (* Test the unit functions with the concrete interpreter *) + if !test_unit_functions then Test.test_unit_functions m; + + (* Translate or borrow-check the crate *) + if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m + else Aeneas.Translate.translate_crate filename dest_dir m; if !Errors.error_list <> [] then ( List.iter diff --git a/src/PrePasses.ml b/src/PrePasses.ml index e8512d25..245da018 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -672,7 +672,7 @@ let apply_passes (crate : crate) : crate = (* Attempt to apply a pass: if it fails we replace the body by [None] *) let apply_function_pass (pass : fun_decl -> fun_decl) (f : fun_decl) = try pass f - with CFailure (_, _) -> + with CFailure _ -> (* 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 *) diff --git a/src/Translate.ml b/src/Translate.ml index eded2c5f..1a3e2798 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -32,7 +32,8 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : match fdef.body with | None -> None | Some _ -> - (* Evaluate *) + (* 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 let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in Some (inputs, Option.get symb) @@ -210,10 +211,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx) try Some (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef) - with CFailure (span, _) -> + with CFailure error -> let name = name_to_string trans_ctx fdef.item_meta.name in let name_pattern = name_to_pattern_string trans_ctx fdef.item_meta.name in - save_error_opt_span __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ error.span ("Could not translate the function '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None @@ -247,12 +248,12 @@ let translate_crate_to_pure (crate : crate) : List.filter_map (fun (global : global_decl) -> try Some (SymbolicToPure.translate_global trans_ctx global) - with CFailure (span, _) -> + with CFailure error -> let name = name_to_string trans_ctx global.item_meta.name in let name_pattern = name_to_pattern_string trans_ctx global.item_meta.name in - save_error_opt_span __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ error.span ("Could not translate the global declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -270,12 +271,12 @@ let translate_crate_to_pure (crate : crate) : ( fdef.def_id, SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef ) - with CFailure (span, _) -> + with CFailure error -> let name = name_to_string trans_ctx fdef.item_meta.name in let name_pattern = name_to_pattern_string trans_ctx fdef.item_meta.name in - save_error_opt_span __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ error.span ("Could not translate the function signature of '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); @@ -283,7 +284,11 @@ let translate_crate_to_pure (crate : crate) : (FunDeclId.Map.values crate.fun_decls)) in - (* Translate all the *transparent* functions *) + (* Translate all the *transparent* functions. + + Remark: [translate_function_to_pure] catches errors of type [CFailure] + to allow the compilation to make progress. + *) let pure_translations = List.filter_map (translate_function_to_pure trans_ctx type_decls_map fun_dsigs) @@ -295,12 +300,12 @@ let translate_crate_to_pure (crate : crate) : List.filter_map (fun d -> try Some (SymbolicToPure.translate_trait_decl trans_ctx d) - with CFailure (span, _) -> + with CFailure error -> let name = name_to_string trans_ctx d.item_meta.name in let name_pattern = name_to_pattern_string trans_ctx d.item_meta.name in - save_error_opt_span __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ error.span ("Could not translate the trait declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -313,12 +318,12 @@ let translate_crate_to_pure (crate : crate) : List.filter_map (fun d -> try Some (SymbolicToPure.translate_trait_impl trans_ctx d) - with CFailure (span, _) -> + with CFailure error -> let name = name_to_string trans_ctx d.item_meta.name in let name_pattern = name_to_pattern_string trans_ctx d.item_meta.name in - save_error_opt_span __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ error.span ("Could not translate the trait instance '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -532,7 +537,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (id : GlobalDeclId.id) : unit = let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = GlobalDeclId.Map.find id global_decls in - let trans = FunDeclId.Map.find global.body ctx.trans_funs in + let trans = + silent_unwrap_opt_span __FILE__ __LINE__ None + (FunDeclId.Map.find_opt global.body ctx.trans_funs) + in sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.span; let body = trans.f in @@ -741,7 +749,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let export_trait_decl (fmt : Format.formatter) (_config : gen_config) (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool) (extract_extra_info : bool) : unit = - let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in + let trait_decl = + silent_unwrap_opt_span __FILE__ __LINE__ None + (TraitDeclId.Map.find_opt trait_decl_id ctx.trans_trait_decls) + in (* Check if the trait declaration is builtin, in which case we ignore it *) let open ExtractBuiltin in if @@ -878,7 +889,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if config.extract_state_type && config.extract_fun_decls then export_state_type (); - List.iter export_decl_group ctx.crate.declarations; + List.iter + (fun g -> + try export_decl_group g + with CFailure _ -> (* An exception was raised: ignore it *) + ()) + ctx.crate.declarations; if config.extract_state_type && not config.extract_fun_decls then export_state_type () @@ -1136,7 +1152,19 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : * sure there are no name clashes. *) let ctx = List.fold_left - (fun ctx def -> Extract.extract_type_decl_register_names ctx def) + (fun ctx def -> + try Extract.extract_type_decl_register_names ctx def + with CFailure error -> + (* An exception was raised: ignore it *) + let name = name_to_string trans_ctx def.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx def.item_meta.name + in + save_error_opt_span __FILE__ __LINE__ error.span + ("Could not generate names for the type declaration '" ^ name + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" + ); + ctx) ctx (Pure.TypeDeclId.Map.values trans_types) in @@ -1144,36 +1172,88 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let ctx = List.fold_left (fun ctx (trans : pure_fun_translation) -> - (* If requested by the user, register termination measures and decreases - proofs for all the recursive functions *) - let gen_decr_clause (def : Pure.fun_decl) = - !Config.extract_decreases_clauses - && PureUtils.FunLoopIdSet.mem - (def.Pure.def_id, def.Pure.loop_id) - rec_functions - in - (* Register the names, only if the function is not a global body - - * those are handled later *) - let is_global = trans.f.Pure.is_global_decl_body in - if is_global then ctx - else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans) + try + (* If requested by the user, register termination measures and decreases + proofs for all the recursive functions *) + let gen_decr_clause (def : Pure.fun_decl) = + !Config.extract_decreases_clauses + && PureUtils.FunLoopIdSet.mem + (def.Pure.def_id, def.Pure.loop_id) + rec_functions + in + (* Register the names, only if the function is not a global body - + * those are handled later *) + let is_global = trans.f.Pure.is_global_decl_body in + if is_global then ctx + else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans + with CFailure error -> + (* An exception was raised: ignore it *) + let name = name_to_string trans_ctx trans.f.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx trans.f.item_meta.name + in + save_error_opt_span __FILE__ __LINE__ error.span + ("Could not generate names for the function declaration '" ^ name + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" + ); + ctx) ctx (FunDeclId.Map.values trans_funs) in let ctx = - List.fold_left Extract.extract_global_decl_register_names ctx + List.fold_left + (fun ctx def -> + try Extract.extract_global_decl_register_names ctx def + with CFailure error -> + (* An exception was raised: ignore it *) + let name = name_to_string trans_ctx def.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx def.item_meta.name + in + save_error_opt_span __FILE__ __LINE__ error.span + ("Could not generate names for the global declaration '" ^ name + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" + ); + ctx) + ctx (GlobalDeclId.Map.values crate.global_decls) in let ctx = - List.fold_left Extract.extract_trait_decl_register_names ctx - trans_trait_decls + List.fold_left + (fun ctx def -> + try Extract.extract_trait_decl_register_names ctx def + with CFailure error -> + (* An exception was raised: ignore it *) + let name = name_to_string trans_ctx def.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx def.item_meta.name + in + save_error_opt_span __FILE__ __LINE__ error.span + ("Could not generate names for the trait declaration '" ^ name + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" + ); + ctx) + ctx trans_trait_decls in let ctx = - List.fold_left Extract.extract_trait_impl_register_names ctx - trans_trait_impls + List.fold_left + (fun ctx def -> + try Extract.extract_trait_impl_register_names ctx def + with CFailure error -> + (* An exception was raised: ignore it *) + let name = name_to_string trans_ctx def.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx def.item_meta.name + in + save_error_opt_span __FILE__ __LINE__ error.span + ("Could not generate names for the trait implementation '" ^ name + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" + ); + ctx) + ctx trans_trait_impls in (* Open the output file *) diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 22a2e414..7508a2be 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -557,7 +557,10 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) let explicit = let lookup is_trait_method fun_decl_id lp_id = (* Lookup the function to retrieve the signature information *) - let trans_fun = A.FunDeclId.Map.find fun_decl_id ctx.trans_funs in + let trans_fun = + silent_unwrap __FILE__ __LINE__ span + (A.FunDeclId.Map.find_opt fun_decl_id ctx.trans_funs) + in let trans_fun = match lp_id with | None -> trans_fun.f @@ -565,7 +568,7 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) in let explicit = trans_fun.signature.explicit_info in (* If it is a trait method, we need to remove the prefix - which account for the generics of the impl. *) + which accounts for the generics of the impl. *) let explicit = if is_trait_method then (* We simply adjust the length of the explicit information to @@ -1415,9 +1418,9 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) Some def.item_meta.name else None in - extract_comment_with_raw_span ctx fmt + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: decreases clause" ] - name def.item_meta.span.span); + name def.item_meta.span); F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1484,9 +1487,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment_with_raw_span ctx fmt + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: termination measure" ] - None def.item_meta.span.span; + None def.item_meta.span; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1543,9 +1546,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) in (* syntax term ... term : tactic *) F.pp_print_break fmt 0 0; - extract_comment_with_raw_span ctx fmt + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: decreases_by tactic" ] - None def.item_meta.span.span; + None def.item_meta.span; F.pp_print_space fmt (); F.pp_open_hvbox fmt 0; F.pp_print_string fmt "syntax \""; @@ -1590,7 +1593,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) Some def.item_meta.name else None in - extract_comment_with_raw_span ctx fmt comment name def.item_meta.span.span + extract_comment_with_span ctx fmt comment name def.item_meta.span (** Extract a function declaration. @@ -2094,9 +2097,9 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) Some global.item_meta.name else None in - extract_comment_with_raw_span ctx fmt + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx global.item_meta.name ^ "]" ] - name global.span.span; + name global.span; F.pp_print_space fmt (); let decl_name = ctx_get_global span global.def_id ctx in @@ -2528,7 +2531,10 @@ let explicit_info_drop_prefix (g1 : generic_params) (g2 : explicit_info) : let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) (decl : trait_decl) (item_name : string) (id : fun_decl_id) : unit = (* Lookup the definition *) - let trans = A.FunDeclId.Map.find id ctx.trans_funs in + let trans = + silent_unwrap_opt_span __FILE__ __LINE__ None + (A.FunDeclId.Map.find_opt id ctx.trans_funs) + in (* Extract the items *) let f = trans.f in let fun_name = @@ -2585,9 +2591,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) Some decl.item_meta.name else None in - extract_comment_with_raw_span ctx fmt + extract_comment_with_span ctx fmt [ "Trait declaration: [" ^ name_to_string ctx decl.item_meta.name ^ "]" ] - name decl.item_meta.span.span); + name decl.item_meta.span); F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on one line and indents are correct. @@ -2806,7 +2812,10 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) (impl_generics : string list * string list * string list) : unit = let trait_decl_id = impl.impl_trait.trait_decl_id in (* Lookup the definition *) - let trans = A.FunDeclId.Map.find id ctx.trans_funs in + let trans = + silent_unwrap_opt_span __FILE__ __LINE__ None + (A.FunDeclId.Map.find_opt id ctx.trans_funs) + in (* Extract the items *) let f = trans.f in let fun_name = @@ -2946,12 +2955,12 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) Some (trait_decl.llbc_generics, decl_ref.decl_generics) ) else (None, None) in - extract_comment_with_raw_span ctx fmt + extract_comment_with_span ctx fmt [ "Trait implementation: [" ^ name_to_string ctx impl.item_meta.name ^ "]"; ] (* TODO: why option option for the generics? Looks like a bug in OCaml!? *) - name ?generics:(Some generics) impl.item_meta.span.span); + name ?generics:(Some generics) impl.item_meta.span); F.pp_print_break fmt 0 0; (* If extracting for Lean, mark the definition as reducible *) diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index 3c2f6691..0669f790 100644 --- a/src/extract/ExtractTypes.ml +++ b/src/extract/ExtractTypes.ml @@ -1227,11 +1227,11 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit = F.pp_print_string fmt rd; F.pp_close_box fmt () -let extract_comment_with_raw_span (ctx : extraction_ctx) (fmt : F.formatter) +let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter) (sl : string list) (name : Types.name option) ?(generics : (Types.generic_params * Types.generic_args) option = None) - (raw_span : Meta.raw_span) : unit = - let raw_span = raw_span_to_string raw_span in + (span : Meta.span) : unit = + let span = span_to_string span in let name = match (name, generics) with | None, _ -> [] @@ -1243,7 +1243,7 @@ let extract_comment_with_raw_span (ctx : extraction_ctx) (fmt : F.formatter) ^ name_with_generics_to_pattern_string ctx.trans_ctx name params args; ] in - extract_comment fmt (sl @ [ raw_span ] @ name) + extract_comment fmt (sl @ [ span ] @ name) let extract_trait_clause_type (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) @@ -1517,9 +1517,9 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) then Some def.item_meta.name else None in - extract_comment_with_raw_span ctx fmt + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx def.item_meta.name ^ "]" ] - name def.item_meta.span.span); + name def.item_meta.span); F.pp_print_break fmt 0 0; (* Open a box for the definition, so that whenever possible it gets printed on * one line. Note however that in the case of Lean line breaks are important diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml index 80a5d7da..8a81efa8 100644 --- a/src/interp/Interpreter.ml +++ b/src/interp/Interpreter.ml @@ -191,7 +191,8 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : (* Create the context *) let regions_hierarchy = - FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies + silent_unwrap __FILE__ __LINE__ fdef.item_meta.span + (FunIdMap.find_opt (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies) in let region_groups = List.map (fun (g : region_var_group) -> g.id) regions_hierarchy @@ -310,7 +311,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) List.filter_map (fun x -> x) parent_input_abs_ids in (* TODO: need to be careful for loops *) - assert (parent_input_abs_ids = []); + sanity_check __FILE__ __LINE__ (parent_input_abs_ids = []) fdef.item_meta.span; (* Insert the return value in the return abstractions (by applying * borrow projections) *) @@ -638,8 +639,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in (* Finish synthesizing *) if synthesize then Some (cc el) else None - with CFailure (span, msg) -> - if synthesize then Some (Error (span, msg)) else None + with CFailure error -> + if synthesize then Some (Error (error.span, error.msg)) else None in (* Return *) (input_svs, symbolic) diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml index cf651285..b37365b3 100644 --- a/src/interp/InterpreterLoopsMatchCtxs.ml +++ b/src/interp/InterpreterLoopsMatchCtxs.ml @@ -1215,7 +1215,7 @@ struct S.sid_to_value_map := SymbolicValueId.Map.add_strict id0 sv1 !S.sid_to_value_map; - (* Return - the returned value is not used: we can return whatever + (* Return - the returned value is not used: we can return whatever we want *) sv0) diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml index 79275eb5..d115b5ab 100644 --- a/src/interp/InterpreterStatements.ml +++ b/src/interp/InterpreterStatements.ml @@ -662,8 +662,9 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) ^ fun_sig_to_string ctx def.signature)); let tr_self = UnknownTrait __FUNCTION__ in let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular fid) - ctx.fun_ctx.regions_hierarchies + silent_unwrap __FILE__ __LINE__ span + (LlbcAstUtils.FunIdMap.find_opt (FRegular fid) + ctx.fun_ctx.regions_hierarchies) in let inst_sg = instantiate_fun_sig span ctx func.generics tr_self def.signature diff --git a/src/llbc/RegionsHierarchy.ml b/src/llbc/RegionsHierarchy.ml index c021b5d6..3e3f2102 100644 --- a/src/llbc/RegionsHierarchy.ml +++ b/src/llbc/RegionsHierarchy.ml @@ -303,6 +303,11 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) Some { id; regions; parents }) (SccId.Map.bindings sccs.sccs) +(** Compute the region hierarchies for a set of function declarations.Aeneas + + Remark: in case we do not abort on error, this function will ignore + the signatures which trigger errors. + *) let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) (fun_decls : fun_decl FunDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) @@ -338,9 +343,16 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) (BuiltinFunIdMap.values builtin_fun_infos) in FunIdMap.of_list - (List.map + (List.filter_map (fun (fid, (name, sg, span)) -> - ( fid, - compute_regions_hierarchy_for_sig span type_decls fun_decls - global_decls trait_decls trait_impls name sg )) + try + Some + ( fid, + compute_regions_hierarchy_for_sig span type_decls fun_decls + global_decls trait_decls trait_impls name sg ) + with CFailure error -> + save_error_opt_span __FILE__ __LINE__ error.span + ("Could not compute the region hierarchies for function '" ^ name + ^ " because of previous error"); + None) (regular @ builtin)) diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml index b395f531..42e8f9df 100644 --- a/src/llbc/TypesAnalysis.ml +++ b/src/llbc/TypesAnalysis.ml @@ -278,7 +278,10 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref) ty_info generics.types | TAdt (TAdtId adt_id, generics) -> (* Lookup the information for this type definition *) - let adt_info = TypeDeclId.Map.find adt_id infos in + let adt_info = + silent_unwrap_opt_span __FILE__ __LINE__ span + (TypeDeclId.Map.find_opt adt_id infos) + in (* Update the type info with the information from the adt *) let ty_info = update_ty_info ty_info None adt_info.borrows_info in (* Check if 'static appears in the region parameters *) diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index ee41e440..3b517edc 100644 --- a/src/symbolic/SymbolicToPure.ml +++ b/src/symbolic/SymbolicToPure.ml @@ -1080,7 +1080,10 @@ let compute_raw_fun_effect_info (span : Meta.span option) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with | TraitMethod (_, _, fid) | FunId (FRegular fid) -> - let info = A.FunDeclId.Map.find fid fun_infos in + let info = + silent_unwrap_opt_span __FILE__ __LINE__ span + (A.FunDeclId.Map.find_opt fid fun_infos) + in let stateful_group = info.stateful in let stateful = stateful_group && ((not !Config.backward_no_state_update) || gid = None) @@ -1472,12 +1475,16 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : span option) let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx) (fun_id : FunDeclId.id) (sg : A.fun_sig) (input_names : string option list) : decomposed_fun_sig = + let span = + (silent_unwrap_opt_span __FILE__ __LINE__ None + (FunDeclId.Map.find_opt fun_id decls_ctx.fun_ctx.fun_decls)) + .item_meta + .span + in (* Retrieve the list of parent backward functions *) let regions_hierarchy = - FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies - in - let span = - (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).item_meta.span + silent_unwrap __FILE__ __LINE__ span + (FunIdMap.find_opt (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies) in translate_fun_sig_with_regions_hierarchy_to_decomposed (Some span) decls_ctx @@ -4700,13 +4707,13 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = List.filter_map (fun d -> try Some (translate_type_decl ctx d) - with CFailure (span, _) -> + with CFailure error -> let env = PrintPure.decls_ctx_to_fmt_env ctx in let name = PrintPure.name_to_string env d.item_meta.name in let name_pattern = TranslateCore.name_to_pattern_string ctx d.item_meta.name in - save_error_opt_span __FILE__ __LINE__ span + save_error_opt_span __FILE__ __LINE__ error.span ("Could not translate type decl '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None) From 3c1ffc3fb03efb6dc7725b8520abf731a201879e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 18 Dec 2024 17:28:42 +0000 Subject: [PATCH 4/6] Regenerate the test files --- tests/src/mutually-recursive-traits.lean.out | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 934e762f..a765efb3 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -1,16 +1,17 @@ [Info ] Imported: tests/llbc/mutually_recursive_traits.llbc -[Error] In file Translate.ml, line 852: +[Error] In file Translate.ml, line 863: Mutually recursive trait declarations are not supported Uncaught exception: (Failure - "In file Translate.ml, line 852:\ + "In file Translate.ml, line 863:\ \nMutually recursive trait declarations are not supported") -Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 52, characters 4-23 +Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 72, characters 4-23 +Called from Aeneas__Translate.extract_definitions.export_decl_group in file "Translate.ml", line 863, characters 8-114 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 -Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 881, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1008, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1578, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 509, characters 14-66 +Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 892, characters 2-177 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1024, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1658, characters 5-42 +Called from Dune__exe__Main in file "Main.ml", line 511, characters 11-63 From 4105b16716b50ffcedcf251ff6dbd35af82cd419 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 18 Dec 2024 18:19:57 +0000 Subject: [PATCH 5/6] Make the generated output cleaner in the presence of errors --- src/Errors.ml | 11 +++ src/dune | 1 + src/extract/Extract.ml | 135 ++++++++++++++++++++--------------- src/extract/ExtractBase.ml | 1 + src/extract/ExtractErrors.ml | 42 +++++++++++ src/extract/ExtractTypes.ml | 22 +++--- 6 files changed, 146 insertions(+), 66 deletions(-) create mode 100644 src/extract/ExtractErrors.ml diff --git a/src/Errors.ml b/src/Errors.ml index 4a41a4bf..416bae2d 100644 --- a/src/Errors.ml +++ b/src/Errors.ml @@ -149,3 +149,14 @@ let silent_unwrap_opt_span (file : string) (line : int) let silent_unwrap (file : string) (line : int) (span : Meta.span) (x : 'a option) : 'a = silent_unwrap_opt_span file line (Some span) x + +let opt_raise_opt_span (file : string) (line : int) (span : Meta.span option) + (msg : string) : unit = + if !Config.fail_hard then ( + let msg = format_error_message_with_file_line file line span msg in + log#serror (msg ^ "\n"); + raise (Failure msg)) + +let opt_raise (file : string) (line : int) (span : Meta.span) (msg : string) : + unit = + opt_raise_opt_span file line (Some span) msg diff --git a/src/dune b/src/dune index 784897a7..4b077025 100644 --- a/src/dune +++ b/src/dune @@ -32,6 +32,7 @@ Extract ExtractBase ExtractBuiltin + ExtractErrors ExtractName ExtractTypes FunsAnalysis diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 7508a2be..7a3f1ccb 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -205,7 +205,9 @@ let extract_adt_g_value (span : Meta.span) in if use_parentheses then F.pp_print_string fmt ")"; ctx - | _ -> craise __FILE__ __LINE__ span "Inconsistent typed value" + | _ -> + admit_raise __FILE__ __LINE__ span "Inconsistently typed value" fmt; + ctx (* Extract globals in the same way as variables *) let extract_global (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) @@ -373,7 +375,7 @@ let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx) | StructUpdate supd -> extract_StructUpdate span ctx fmt inside e.ty supd | Loop _ -> (* The loop nodes should have been eliminated in {!PureMicroPasses} *) - craise __FILE__ __LINE__ span "Unreachable" + admit_raise __FILE__ __LINE__ span "Unreachable" fmt | EError (_, _) -> extract_texpression_errors fmt (* Extract an application *or* a top-level qualif (function extraction has @@ -557,39 +559,41 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) let explicit = let lookup is_trait_method fun_decl_id lp_id = (* Lookup the function to retrieve the signature information *) - let trans_fun = - silent_unwrap __FILE__ __LINE__ span - (A.FunDeclId.Map.find_opt fun_decl_id ctx.trans_funs) - in - let trans_fun = - match lp_id with - | None -> trans_fun.f - | Some lp_id -> Pure.LoopId.nth trans_fun.loops lp_id - in - let explicit = trans_fun.signature.explicit_info in - (* If it is a trait method, we need to remove the prefix - which accounts for the generics of the impl. *) - let explicit = - if is_trait_method then - (* We simply adjust the length of the explicit information to - the number of generic arguments *) - let open Collections.List in - let { explicit_types; explicit_const_generics } = explicit in - { - explicit_types = - drop - (length explicit_types - length generics.types) - explicit_types; - explicit_const_generics = - drop - (length explicit_const_generics - - length generics.const_generics) - explicit_const_generics; - } - else explicit - in - (* *) - Some explicit + match A.FunDeclId.Map.find_opt fun_decl_id ctx.trans_funs with + | None -> + (* Error case *) + opt_raise __FILE__ __LINE__ span "Unrechable"; + None + | Some trans_fun -> + let trans_fun = + match lp_id with + | None -> trans_fun.f + | Some lp_id -> Pure.LoopId.nth trans_fun.loops lp_id + in + let explicit = trans_fun.signature.explicit_info in + (* If it is a trait method, we need to remove the prefix + which accounts for the generics of the impl. *) + let explicit = + if is_trait_method then + (* We simply adjust the length of the explicit information to + the number of generic arguments *) + let open Collections.List in + let { explicit_types; explicit_const_generics } = explicit in + { + explicit_types = + drop + (length explicit_types - length generics.types) + explicit_types; + explicit_const_generics = + drop + (length explicit_const_generics + - length generics.const_generics) + explicit_const_generics; + } + else explicit + in + (* *) + Some explicit in match fun_id with | FromLlbc (FunId (FRegular fun_decl_id), lp_id) -> @@ -643,12 +647,13 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx) (* Return *) if inside then F.pp_print_string fmt ")" | (Unop _ | Binop _), _ -> - craise __FILE__ __LINE__ span + admit_raise __FILE__ __LINE__ span ("Unreachable:\n" ^ "Function: " ^ show_fun_or_op_id fid ^ ",\nNumber of arguments: " ^ string_of_int (List.length args) ^ ",\nArguments: " ^ String.concat " " (List.map show_texpression args)) + fmt (** Subcase of the app case: ADT constructor *) and extract_adt_cons (span : Meta.span) (ctx : extraction_ctx) @@ -658,9 +663,9 @@ and extract_adt_cons (span : Meta.span) (ctx : extraction_ctx) let is_single_pat = false in (* Sanity check: make sure the expression is not a tuple constructor with no arguments (the properly extracted expression would be a function) *) - cassert __FILE__ __LINE__ + sanity_check __FILE__ __LINE__ (not (adt_cons.adt_id = TTuple && generics.types != [] && args = [])) - span "Unreachable"; + span; let _ = extract_adt_g_value span (fun ctx inside e -> @@ -772,7 +777,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx) extract_App span ctx fmt inside (mk_app span original_app arg) args | [] -> (* No argument: shouldn't happen *) - craise __FILE__ __LINE__ span "Unreachable" + admit_raise __FILE__ __LINE__ span "Unreachable" fmt and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (xl : typed_pattern list) (e : texpression) : unit = @@ -842,23 +847,23 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hovbox fmt ctx.indent_incr; let ctx = (* There are two cases: - * - do we use a notation like [x <-- y;] - * - do we use notation with let-bindings - * Note that both notations can be used for monadic let-bindings. - * For instance, in F*, you can write: - * {[ - * let* x = y in // monadic - * ... - * ]} - * TODO: cleanup - * *) + - do we use a notation like [x <-- y;] + - do we use notation with let-bindings + Note that both notations can be used for monadic let-bindings. + For instance, in F*, you can write: + {[ + let* x = y in // monadic + ... + ]} + TODO: cleanup + *) if monadic && (backend () = Coq || backend () = HOL4) then ( let ctx = extract_typed_pattern span ctx fmt true true lv in F.pp_print_space fmt (); let arrow = match backend () with | Coq | HOL4 -> "<-" - | FStar | Lean -> craise __FILE__ __LINE__ span "impossible" + | FStar | Lean -> internal_error __FILE__ __LINE__ span in F.pp_print_string fmt arrow; F.pp_print_space fmt (); @@ -1266,7 +1271,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx) F.pp_print_string fmt "]"; if need_paren then F.pp_print_string fmt ")"; F.pp_close_box fmt () - | _ -> craise __FILE__ __LINE__ span "Unreachable" + | _ -> admit_raise __FILE__ __LINE__ span "Unreachable" fmt (** A small utility to print the parameters of a function signature. @@ -2528,8 +2533,9 @@ let explicit_info_drop_prefix (g1 : generic_params) (g2 : explicit_info) : Extract the items for a method in a trait decl. *) -let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) - (decl : trait_decl) (item_name : string) (id : fun_decl_id) : unit = +let extract_trait_decl_method_items_aux (ctx : extraction_ctx) + (fmt : F.formatter) (decl : trait_decl) (item_name : string) + (id : fun_decl_id) : unit = (* Lookup the definition *) let trans = silent_unwrap_opt_span __FILE__ __LINE__ None @@ -2578,6 +2584,13 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) in extract_trait_decl_item ctx fmt fun_name ty +let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) + (decl : trait_decl) (item_name : string) (id : fun_decl_id) : unit = + try extract_trait_decl_method_items_aux ctx fmt decl item_name id + with CFailure _ -> + F.pp_print_space fmt (); + extract_admit fmt + (** Extract a trait declaration *) let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (decl : trait_decl) : unit = @@ -2807,9 +2820,10 @@ let extract_trait_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) Extract the items for a method in a trait impl. *) -let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) - (impl : trait_impl) (item_name : string) (id : fun_decl_id) - (impl_generics : string list * string list * string list) : unit = +let extract_trait_impl_method_items_aux (ctx : extraction_ctx) + (fmt : F.formatter) (impl : trait_impl) (item_name : string) + (id : fun_decl_id) (impl_generics : string list * string list * string list) + : unit = let trait_decl_id = impl.impl_trait.trait_decl_id in (* Lookup the definition *) let trans = @@ -2936,6 +2950,15 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) in extract_trait_impl_item ctx fmt fun_name ty +let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) + (impl : trait_impl) (item_name : string) (id : fun_decl_id) + (impl_generics : string list * string list * string list) : unit = + try + extract_trait_impl_method_items_aux ctx fmt impl item_name id impl_generics + with CFailure _ -> + F.pp_print_space fmt (); + extract_admit fmt + (** Extract a trait implementation *) let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (impl : trait_impl) : unit = diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index 490799c9..c77caf2b 100644 --- a/src/extract/ExtractBase.ml +++ b/src/extract/ExtractBase.ml @@ -8,6 +8,7 @@ module F = Format open ExtractBuiltin open TranslateCore open Errors +include ExtractErrors (** The local logger *) let log = Logging.extract_log diff --git a/src/extract/ExtractErrors.ml b/src/extract/ExtractErrors.ml new file mode 100644 index 00000000..c390e1cd --- /dev/null +++ b/src/extract/ExtractErrors.ml @@ -0,0 +1,42 @@ +(** Error utilities for the extraction *) + +open Errors + +let extract_raise_opt_span (file : string) (line : int) + (span : Meta.span option) (msg : string) (fmt : Format.formatter) + (extract : string) : unit = + (* Save the error *) + save_error_opt_span file line span msg; + (* If we did not raise an exception above, generate an output *) + Format.pp_print_string fmt extract + +let extract_raise (file : string) (line : int) (span : Meta.span) (msg : string) + (fmt : Format.formatter) (extract : string) : unit = + extract_raise_opt_span file line (Some span) msg fmt extract + +let admit () = + match Config.backend () with + | Coq | FStar | HOL4 -> "admit" + | Lean -> "sorry" + +let admit_raise_opt_span (file : string) (line : int) (span : Meta.span option) + (msg : string) (fmt : Format.formatter) : unit = + extract_raise_opt_span file line span msg fmt (admit ()) + +let admit_raise (file : string) (line : int) (span : Meta.span) (msg : string) + (fmt : Format.formatter) : unit = + admit_raise_opt_span file line (Some span) msg fmt + +let admit_string_opt_span (file : string) (line : int) (span : Meta.span option) + (msg : string) : string = + (* Save the error *) + save_error_opt_span file line span msg; + (* *) + admit () + +let admit_string (file : string) (line : int) (span : Meta.span) (msg : string) + : string = + admit_string_opt_span file line (Some span) msg + +let extract_admit (fmt : Format.formatter) : unit = + Format.pp_print_string fmt (admit ()) diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index 0669f790..7af7b5c3 100644 --- a/src/extract/ExtractTypes.ml +++ b/src/extract/ExtractTypes.ml @@ -31,7 +31,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool) | HOL4 -> F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty); F.pp_print_space fmt () - | _ -> craise __FILE__ __LINE__ span "Unreachable"); + | _ -> admit_raise __FILE__ __LINE__ span "Unreachable" fmt); (* We need to add parentheses if the value is negative *) if sv.value >= Z.of_int 0 then F.pp_print_string fmt (Z.to_string sv.value) @@ -47,7 +47,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool) let iname = String.lowercase_ascii (int_name sv.int_ty) in F.pp_print_string fmt ("#" ^ iname) | HOL4 -> () - | _ -> craise __FILE__ __LINE__ span "Unreachable"); + | _ -> admit_raise __FILE__ __LINE__ span "Unreachable" fmt); if print_brackets then F.pp_print_string fmt ")") | VBool b -> let b = @@ -76,8 +76,8 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool) F.pp_print_string fmt c; if inside then F.pp_print_string fmt ")") | VFloat _ | VStr _ | VByteStr _ -> - craise __FILE__ __LINE__ span - "Float, string and byte string literals are unsupported" + admit_raise __FILE__ __LINE__ span + "Float, string and byte string literals are unsupported" fmt (** Format a unary operation @@ -137,7 +137,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit) match backend () with | Coq | FStar -> "scalar_cast" | Lean -> "Scalar.cast" - | HOL4 -> craise __FILE__ __LINE__ span "Unreachable" + | HOL4 -> admit_string __FILE__ __LINE__ span "Unreachable" in let src = if backend () <> Lean then Some (integer_type_to_string src) @@ -150,7 +150,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit) match backend () with | Coq | FStar -> "scalar_cast_bool" | Lean -> "Scalar.cast_bool" - | HOL4 -> craise __FILE__ __LINE__ span "Unreachable" + | HOL4 -> admit_string __FILE__ __LINE__ span "Unreachable" in let tgt = integer_type_to_string tgt in (cast_str, None, Some tgt) @@ -221,7 +221,7 @@ let extract_binop (span : Meta.span) | Sub -> "-" | Mul -> "*" | CheckedAdd | CheckedSub | CheckedMul -> - craise __FILE__ __LINE__ span + admit_string __FILE__ __LINE__ span "Checked operations are not implemented" | Shl -> "<<<" | Shr -> ">>>" @@ -562,7 +562,9 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) match type_id with | TAdtId id -> not (TypeDeclId.Set.mem id no_params_tys) | TBuiltin _ -> true - | _ -> craise __FILE__ __LINE__ span "Unreachable" + | _ -> + save_error __FILE__ __LINE__ span "Unreachable"; + false in if types <> [] && print_tys then ( let print_paren = List.length types > 1 in @@ -592,7 +594,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter) if inside then F.pp_print_string fmt ")" | TTraitType (trait_ref, type_name) -> ( if !parameterize_trait_types then - craise __FILE__ __LINE__ span "Unimplemented" + admit_raise __FILE__ __LINE__ span "Unimplemented" fmt else let type_name = ctx_get_trait_type span trait_ref.trait_decl_ref.trait_decl_id @@ -780,7 +782,7 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx) F.pp_print_string fmt (add_brackets name) | UnknownTrait _ -> (* This is an error case *) - craise __FILE__ __LINE__ span "Unexpected" + admit_raise __FILE__ __LINE__ span "Unexpected" fmt (** Compute the names for all the top-level identifiers used in a type definition (type name, variant names, field names, etc. but not type From 8bc96d4ce83a4bb899d2ef541004621722f36ce8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 18 Dec 2024 20:55:01 +0000 Subject: [PATCH 6/6] Update the Charon pin --- charon-pin | 2 +- flake.lock | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/charon-pin b/charon-pin index 87f09071..2d18ef63 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. -2909a3c23b1abbc780aad5dca76a0f101fedc6ea +4925c99ccab9613d6af784dd52d69fccaf3f5f5d diff --git a/flake.lock b/flake.lock index 808f06ac..04e84738 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1734440782, - "narHash": "sha256-ni2DPS9/JkAmD3dMh2tIpUTo7OiZplx3f/d0ySW8G5s=", + "lastModified": 1734535109, + "narHash": "sha256-j1kKIeXg0Rl3TTujt60alOflycGyJUPpeDCw37AP15k=", "owner": "aeneasverif", "repo": "charon", - "rev": "2909a3c23b1abbc780aad5dca76a0f101fedc6ea", + "rev": "4925c99ccab9613d6af784dd52d69fccaf3f5f5d", "type": "github" }, "original": { @@ -177,11 +177,11 @@ ] }, "locked": { - "lastModified": 1734402816, - "narHash": "sha256-cgQ8mjUJz7J3fp97lnvl0dSJ6vLt8yzUSmw3B7QKw94=", + "lastModified": 1734489114, + "narHash": "sha256-dKBBZr2pw7KDI/7GeiN5qPccqqtvnK2jqAMcMo4rVvU=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "e38fbd6e56e8cd1d61c65a21bbb7785e966707b4", + "rev": "b2e385f8e5c1d7c0d9ce738d650955c2e94555ae", "type": "github" }, "original": {