diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Errors.ml | 5 | ||||
| -rw-r--r-- | compiler/Extract.ml | 18 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 5 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 8 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 15 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 26 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 19 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 21 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 13 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 9 | ||||
| -rw-r--r-- | compiler/Main.ml | 13 | ||||
| -rw-r--r-- | compiler/PrePasses.ml | 19 | ||||
| -rw-r--r-- | compiler/Print.ml | 1 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 2 | ||||
| -rw-r--r-- | compiler/Pure.ml | 8 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 4 | ||||
| -rw-r--r-- | compiler/PureTypeCheck.ml | 10 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 3 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 1 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 15 | ||||
| -rw-r--r-- | compiler/Translate.ml | 93 | ||||
| -rw-r--r-- | compiler/TypesUtils.ml | 20 | ||||
| -rw-r--r-- | compiler/ValuesUtils.ml | 2 |
25 files changed, 250 insertions, 88 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml index 53e56c44..30887593 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -1,6 +1,7 @@ let log = Logging.errors_log -let meta_to_string (span : Meta.span) = +let meta_to_string (meta : Meta.meta) = + let span = meta.span in let file = match span.file with Virtual s | Local s -> s in let loc_to_string (l : Meta.loc) : string = string_of_int l.line ^ ":" ^ string_of_int l.col @@ -10,7 +11,7 @@ let meta_to_string (span : Meta.span) = let format_error_message (meta : Meta.meta option) (msg : string) = let meta = - match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta.span + match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta in msg ^ meta diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 27e9a62c..6eeef772 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) ^ string_of_int (List.length types) ^ " type arguments" in - log#serror err; + save_error __FILE__ __LINE__ None err; Result.Error (types, err)) else let types = List.combine filter types in @@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta) - application argument: [f (exp)] - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _] *) + +let extract_texpression_errors (fmt : F.formatter) = + match !Config.backend with + | FStar | Coq -> F.pp_print_string fmt "admit" + | Lean -> F.pp_print_string fmt "sorry" + | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)" + let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = match e.e with @@ -323,6 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx) | Loop _ -> (* The loop nodes should have been eliminated in {!PureMicroPasses} *) craise __FILE__ __LINE__ meta "Unreachable" + | EError (_, _) -> extract_texpression_errors fmt (* Extract an application *or* a top-level qualif (function extraction has * to handle top-level qualifiers, so it seemed more natural to merge the @@ -1871,7 +1879,7 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl} and {!extract_fun_decl}. *) -let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) +let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) (global : global_decl) (body : fun_decl) (interface : bool) : unit = let meta = body.meta in sanity_check __FILE__ __LINE__ body.is_global_decl_body meta; @@ -1966,6 +1974,12 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break to insert lines between declarations *) F.pp_print_break fmt 0 0 +let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) + (global : global_decl option) (body : fun_decl) (interface : bool) : unit = + match global with + | Some global -> extract_global_decl_aux ctx fmt global body interface + | None -> () + (** Similar to {!extract_trait_decl_register_names} *) let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) (trait_decl : trait_decl) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 8b17591e..656d2f27 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -259,7 +259,7 @@ let report_name_collision (id_to_string : id -> string) let meta_to_string (meta : Meta.meta option) = match meta with | None -> "" - | Some meta -> "\n " ^ Errors.meta_to_string meta.span + | Some meta -> "\n " ^ Errors.meta_to_string meta in let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in @@ -1719,7 +1719,8 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) | TLiteral lty -> ( match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i") | TArrow _ -> "f" - | TTraitType (_, name) -> name_from_type_ident name) + | TTraitType (_, name) -> name_from_type_ident name + | Error -> "x") (** Generates a type variable basename. *) let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) : diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 1f0abf8a..1c3657a3 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -433,6 +433,13 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter) End ]} *) + +let extract_ty_errors (fmt : F.formatter) : unit = + match !Config.backend with + | FStar | Coq -> F.pp_print_string fmt "admit" + | Lean -> F.pp_print_string fmt "sorry" + | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)" + let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit = let extract_rec = extract_ty meta ctx fmt no_params_tys in @@ -566,6 +573,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) "Trait types are not supported yet when generating code for HOL4"; extract_trait_ref meta ctx fmt no_params_tys false trait_ref; F.pp_print_string fmt ("." ^ add_brackets type_name)) + | Error -> extract_ty_errors fmt and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index a65e1663..769e3144 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -191,6 +191,18 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : * do it, and because it gives a bit of sanity. * *) let sg = fdef.signature in + (* Sanity check: no nested borrows, borrows in ADTs, etc. *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) + (sg.output :: sg.inputs)) + fdef.meta "Nested borrows are not supported yet"; + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) + (sg.output :: sg.inputs)) + fdef.meta "ADTs containing borrows are not supported yet"; + (* Create the context *) let regions_hierarchy = FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies @@ -612,7 +624,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Evaluate the function *) let symbolic = - eval_function_body config (Option.get fdef.body).body cf_finish ctx + try eval_function_body config (Option.get fdef.body).body cf_finish ctx + with CFailure (meta, msg) -> Some (Error (meta, msg)) in (* Return *) diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index e593ae75..a158ed9a 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -303,13 +303,11 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) if bid' = bid then ( (* Sanity check *) let expected_ty = ty in - if nv.ty <> expected_ty then ( - log#serror - ("give_back_value: improper type:\n- expected: " - ^ ty_to_string ctx ty ^ "\n- received: " - ^ ty_to_string ctx nv.ty); + if nv.ty <> expected_ty then craise __FILE__ __LINE__ meta - "Value given back doesn't have the proper type"); + ("Value given back doesn't have the proper type:\n\ + - expected: " ^ ty_to_string ctx ty ^ "\n- received: " + ^ ty_to_string ctx nv.ty); (* Replace *) set_replaced (); nv.value) @@ -540,13 +538,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) * see the comment at the level of the definition of * {!typed_avalue} *) let _, expected_ty, _ = ty_get_ref ty in - if nv.ty <> expected_ty then ( - log#serror - ("give_back_avalue_to_same_abstraction: improper type:\n\ + if nv.ty <> expected_ty then + craise __FILE__ __LINE__ meta + ("Value given back doesn't have the proper type:\n\ - expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); - craise __FILE__ __LINE__ meta - "Value given back doesn't have the proper type"); (* This is the loan we are looking for: apply the projection to * the value we give back and replaced this mutable loan with * an ended loan *) @@ -836,26 +832,26 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) match lookup_borrow_opt ek_all l ctx with | None -> () (* Ok *) | Some _ -> - log#lerror + log#ltrace (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": borrow didn't disappear:\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - craise __FILE__ __LINE__ meta "Borrow not eliminated" + internal_error __FILE__ __LINE__ meta in match lookup_loan_opt meta ek_all l ctx with | None -> () (* Ok *) | Some _ -> - log#lerror + log#ltrace (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": loan didn't disappear:\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - craise __FILE__ __LINE__ meta "Loan not eliminated" + internal_error __FILE__ __LINE__ meta in unit_to_cm_fun check_disappeared diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 6e65b11d..a01be046 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -162,11 +162,11 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) sanity_check __FILE__ __LINE__ (ty1 = ty2) meta; default | _ -> - log#lerror + log#ltrace (lazy ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1 ^ "\n- ty2: " ^ show_ty ty2)); - craise __FILE__ __LINE__ meta "Unreachable" + internal_error __FILE__ __LINE__ meta (** Check if two different projections intersect. This is necessary when giving a symbolic value to an abstraction: we need to check that diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 48a1cce6..5f849230 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -146,7 +146,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) "Can't copy an assumed value other than Option" | TAdt (TAdtId _, _) as ty -> sanity_check __FILE__ __LINE__ - (allow_adt_copy || ty_is_primitively_copyable ty) + (allow_adt_copy || ty_is_copyable ty) meta | TAdt (TTuple, _) -> () (* Ok *) | TAdt @@ -157,9 +157,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) const_generics = []; trait_refs = []; } ) -> - exec_assert __FILE__ __LINE__ - (ty_is_primitively_copyable ty) - meta "The type is not primitively copyable" + exec_assert __FILE__ __LINE__ (ty_is_copyable ty) meta + "The type is not primitively copyable" | _ -> exec_raise __FILE__ __LINE__ meta "Unreachable"); let ctx, fields = List.fold_left_map @@ -195,7 +194,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) * thus requires calling the proper function. Here, we copy values * for very simple types such as integers, shared borrows, etc. *) cassert __FILE__ __LINE__ - (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty)) + (ty_is_copyable (Substitute.erase_regions sp.sv_ty)) meta "Not primitively copyable"; (* If the type is copyable, we simply return the current value. Side * remark: what is important to look at when copying symbolic values @@ -528,9 +527,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "The arguments given to the binop don't have the same type"; (* Equality/inequality check is primitive only for a subset of types *) - exec_assert __FILE__ __LINE__ - (ty_is_primitively_copyable v1.ty) - meta "Type is not primitively copyable"; + exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta + "Type is not primitively copyable"; let b = v1 = v2 in Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) else @@ -621,9 +619,8 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) (* Equality operations *) sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta; (* Equality/inequality check is primitive only for a subset of types *) - exec_assert __FILE__ __LINE__ - (ty_is_primitively_copyable v1.ty) - meta "The type is not primitively copyable"; + exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta + "The type is not primitively copyable"; TLiteral TBool) else (* Other operations: input types are integers *) diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index f2c0bcb1..ab3daa72 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -83,7 +83,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) let nv = update v in (* Type checking *) if nv.ty <> v.ty then ( - log#lerror + log#ltrace (lazy ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: " ^ show_ety v.ty)); @@ -252,8 +252,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) let pe = "- pe: " ^ show_projection_elem pe in let v = "- v:\n" ^ show_value v in let ty = "- ty:\n" ^ show_ety ty in - log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); - craise __FILE__ __LINE__ meta "Inconsistent projection") + craise __FILE__ __LINE__ meta + ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty)) (** Generic function to access (read/write) the value at a given place. @@ -319,14 +319,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place) (* Note that we ignore the new environment: it should be the same as the original one. *) - if !Config.sanity_checks then - if ctx1 <> ctx then ( - let msg = - "Unexpected environment update:\nNew environment:\n" - ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env - in - log#serror msg; - craise __FILE__ __LINE__ meta "Unexpected environment update"); + (if !Config.sanity_checks then + if ctx1 <> ctx then + let msg = + "Unexpected environment update:\nNew environment:\n" + ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env + in + craise __FILE__ __LINE__ meta msg); Ok read_value let read_place (meta : Meta.meta) (access : access_kind) (p : place) diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 6e86e6a4..3993d845 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -217,12 +217,12 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) meta); ASymbolic (AProjBorrows (s, ty)) | _ -> - log#lerror + log#ltrace (lazy ("apply_proj_borrows: unexpected inputs:\n- input value: " ^ typed_value_to_string ~meta:(Some meta) ctx v ^ "\n- proj rty: " ^ ty_to_string ctx ty)); - craise __FILE__ __LINE__ meta "Unreachable" + internal_error __FILE__ __LINE__ meta in { value; ty } diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 1cf1c5ef..de89f316 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1365,10 +1365,21 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = eval_transparent_function_call_symbolic_inst meta call ctx in - (* Sanity check *) + (* Sanity check: same number of inputs *) sanity_check __FILE__ __LINE__ (List.length call.args = List.length def.signature.inputs) def.meta; + (* Sanity check: no nested borrows, borrows in ADTs, etc. *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) + (inst_sg.output :: inst_sg.inputs)) + meta "Nested borrows are not supported yet"; + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) + (inst_sg.output :: inst_sg.inputs)) + meta "ADTs containing borrows are not supported yet"; (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config def.meta func def.signature regions_hierarchy inst_sg generics trait_method_generics call.args call.dest diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 642d7a37..689db0c4 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : "find_info: could not find the representant of borrow " ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string () in - log#serror err; craise __FILE__ __LINE__ meta err in @@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()) | AIgnored, _ -> () | _ -> - log#lerror + log#ltrace (lazy ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv ^ "\n- value: " ^ typed_avalue_to_string ~meta:(Some meta) ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); - craise __FILE__ __LINE__ meta "Erroneous typing"); + internal_error __FILE__ __LINE__ meta); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv end @@ -826,9 +825,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = * it must be expanded first *) if ty_has_borrows ctx.type_ctx.type_infos info.ty then sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta; - (* A duplicated symbolic value is necessarily primitively copyable *) + (* A duplicated symbolic value is necessarily copyable *) sanity_check __FILE__ __LINE__ - (info.env_count <= 1 || ty_is_primitively_copyable info.ty) + (info.env_count <= 1 || ty_is_copyable info.ty) meta; sanity_check __FILE__ __LINE__ diff --git a/compiler/Main.ml b/compiler/Main.ml index db200f37..6161f2f2 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -274,12 +274,19 @@ let () = (* Translate the functions *) Aeneas.Translate.translate_crate filename dest_dir m - with Errors.CFailure (meta, msg) -> + 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] *) - log#serror (Errors.format_error_message meta msg); - exit 1); + ()); + + if !Errors.error_list <> [] then ( + List.iter + (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg)) + (* Reverse the list of error messages so that we print them from the + earliest to the latest. *) + (List.rev !Errors.error_list); + exit 1); (* Print total elapsed time *) log#linfo diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 0b39f64a..a46ef79c 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -238,9 +238,9 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl = method! visit_Sequence env st1 st2 = match st1.content with | Loop _ -> - sanity_check __FILE__ __LINE__ + cassert __FILE__ __LINE__ (statement_has_no_loop_break_continue st2) - st2.meta; + st2.meta "Sequences of loops are not supported yet"; (replace_breaks_with st1 st2).content | _ -> super#visit_Sequence env st1 st2 end @@ -437,9 +437,22 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl = let apply_passes (crate : crate) : crate = let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in + (* Attempt to apply a pass: if it fails we replace the body by [None] *) + let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) = + try pass f + 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 *) + let fmt = Print.Crate.crate_to_fmt_env crate in + let name = Print.name_to_string fmt f.name in + save_error __FILE__ __LINE__ (Some f.meta) + ("Ignoring the body of '" ^ name ^ "' because of previous error"); + { f with body = None } + in let fun_decls = List.fold_left - (fun fl pass -> FunDeclId.Map.map pass fl) + (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl) crate.fun_decls passes in let crate = { crate with fun_decls } in diff --git a/compiler/Print.ml b/compiler/Print.ml index dad1aea3..51286553 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -1,4 +1,5 @@ include Charon.PrintUtils +include Charon.PrintTypes include Charon.PrintLlbcAst open Charon.PrintTypes open Charon.PrintExpressions diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 43ec083e..db9c583d 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -164,6 +164,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string = let trait_ref = trait_ref_to_string env false trait_ref in let s = trait_ref ^ "::" ^ type_name in if inside then "(" ^ s ^ ")" else s + | Error -> "@Error" and generic_args_to_strings (env : fmt_env) (inside : bool) (generics : generic_args) : string list = @@ -615,6 +616,7 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) let e = meta_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") + | EError (_, _) -> "@Error" and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bool) (indent : string) (indent_incr : string) (app : texpression) diff --git a/compiler/Pure.ml b/compiler/Pure.ml index daf213cf..451767f8 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -285,6 +285,7 @@ type ty = | TArrow of ty * ty | TTraitType of trait_ref * string (** The string is for the name of the associated type *) + | Error and trait_ref = { trait_id : trait_instance_id; @@ -621,6 +622,7 @@ class ['self] iter_expression_base = method visit_qualif : 'env -> qualif -> unit = fun _ _ -> () method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> () method visit_field_id : 'env -> field_id -> unit = fun _ _ -> () + method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> () end (** Ancestor for {!map_expression} visitor *) @@ -632,6 +634,7 @@ class ['self] map_expression_base = method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x method visit_loop_id : 'env -> loop_id -> loop_id = fun _ x -> x method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x + method visit_meta : 'env -> Meta.meta -> Meta.meta = fun _ x -> x end (** Ancestor for {!reduce_expression} visitor *) @@ -643,6 +646,7 @@ class virtual ['self] reduce_expression_base = method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero method visit_loop_id : 'env -> loop_id -> 'a = fun _ _ -> self#zero method visit_field_id : 'env -> field_id -> 'a = fun _ _ -> self#zero + method visit_meta : 'env -> Meta.meta -> 'a = fun _ _ -> self#zero end (** Ancestor for {!mapreduce_expression} visitor *) @@ -662,6 +666,9 @@ class virtual ['self] mapreduce_expression_base = method visit_field_id : 'env -> field_id -> field_id * 'a = fun _ x -> (x, self#zero) + + method visit_meta : 'env -> Meta.meta -> Meta.meta * 'a = + fun _ x -> (x, self#zero) end (** **Rk.:** here, {!expression} is not at all equivalent to the expressions @@ -726,6 +733,7 @@ type expression = | Loop of loop (** See the comments for {!loop} *) | StructUpdate of struct_update (** See the comments for {!struct_update} *) | Meta of (emeta[@opaque]) * texpression (** Meta-information *) + | EError of Meta.meta option * string and switch_body = If of texpression * texpression | Match of match_branch list and match_branch = { pat : typed_pattern; branch : texpression } diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index b1c85d61..004ecfef 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -416,6 +416,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | StructUpdate supd -> update_struct_update supd ctx | Lambda (lb, e) -> update_lambda lb e ctx | Meta (meta, e) -> update_emeta meta e ctx + | EError (meta, msg) -> (ctx, EError (meta, msg)) in (ctx, { e; ty }) (* *) @@ -1006,7 +1007,8 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl = match e with | Var _ | CVar _ | Const _ | App _ | Qualif _ | Meta (_, _) - | StructUpdate _ | Lambda _ -> + | StructUpdate _ | Lambda _ + | EError (_, _) -> super#visit_expression env e | Switch (scrut, switch) -> ( match switch with diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index 9eed76b2..c1da4019 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -93,12 +93,11 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx) get_adt_field_types meta ctx.type_decls type_id av.variant_id generics in let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx = - if ty <> v.ty then ( + if ty <> v.ty then (* TODO: we need to normalize the types *) - log#serror - ("check_typed_pattern: not the same types:" ^ "\n- ty: " - ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); - craise __FILE__ __LINE__ meta "Inconsistent types"); + craise __FILE__ __LINE__ meta + ("Inconsistent types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: " + ^ show_ty v.ty); check_typed_pattern meta ctx v in (* Check the field types: check that the field patterns have the expected @@ -238,3 +237,4 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : | Meta (_, e_next) -> sanity_check __FILE__ __LINE__ (e_next.ty = e.ty) meta; check_texpression meta ctx e_next + | EError (meta, msg) -> craise_opt_meta __FILE__ __LINE__ meta msg diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index e8f2d95e..fdd14eba 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -233,6 +233,9 @@ let rec let_group_requires_parentheses (meta : Meta.meta) (e : texpression) : | Loop _ -> (* Should have been eliminated *) craise __FILE__ __LINE__ meta "Unreachable" + | EError (meta, msg) -> + craise_opt_meta __FILE__ __LINE__ meta + msg (* TODO : check if true should'nt be returned instead ? *) let texpression_requires_parentheses meta e = match !Config.backend with diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index e164fd49..f15a2c23 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -212,6 +212,7 @@ type expression = TODO: merge this with Return. *) | Meta of emeta * expression (** Meta information *) + | Error of Meta.meta option * string and loop = { loop_id : loop_id; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 482ebf3a..cf03fddf 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1997,6 +1997,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (* Return the computed information *) !info +let translate_error (meta : Meta.meta option) (msg : string) : texpression = + { e = EError (meta, msg); ty = Error } + let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return (ectx, opt_v) -> @@ -2023,6 +2026,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = *) translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx + | Error (meta, msg) -> translate_error meta msg and translate_panic (ctx : bs_ctx) : texpression = Option.get ctx.mk_panic @@ -3916,7 +3920,16 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = def let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = - List.map (translate_type_decl ctx) + List.filter_map + (fun a -> + try Some (translate_type_decl ctx a) + with CFailure (meta, _) -> + let env = PrintPure.decls_ctx_to_fmt_env ctx in + let name = PrintPure.name_to_string env a.name in + save_error __FILE__ __LINE__ meta + ("Could not translate type decl '" ^ name + ^ "' because of previous error"); + None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 22288fe2..9460c5f4 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure (trans_ctx : trans_ctx) +let translate_function_to_pure_aux (trans_ctx : trans_ctx) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = @@ -197,6 +197,20 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | None -> SymbolicToPure.translate_fun_decl ctx None | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast) +let translate_function_to_pure (trans_ctx : trans_ctx) + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) + (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : + pure_fun_translation_no_loops option = + try + Some + (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef) + with CFailure (meta, _) -> + let name = name_to_string trans_ctx fdef.name in + save_error __FILE__ __LINE__ meta + ("Could not translate the function '" ^ name + ^ "' because of previous error"); + None + (* TODO: factor out the return type *) let translate_crate_to_pure (crate : crate) : trans_ctx @@ -222,32 +236,54 @@ let translate_crate_to_pure (crate : crate) : (* Compute the decomposed fun sigs for the whole crate *) let fun_dsigs = FunDeclId.Map.of_list - (List.map + (List.filter_map (fun (fdef : LlbcAst.fun_decl) -> - ( fdef.def_id, - SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx - fdef )) + try + Some + ( fdef.def_id, + SymbolicToPure.translate_fun_sig_from_decl_to_decomposed + trans_ctx fdef ) + with CFailure (meta, _) -> + let name = name_to_string trans_ctx fdef.name in + save_error __FILE__ __LINE__ meta + ("Could not translate the function signature of '" ^ name + ^ "' because of previous error"); + None) (FunDeclId.Map.values crate.fun_decls)) in (* Translate all the *transparent* functions *) let pure_translations = - List.map + List.filter_map (translate_function_to_pure trans_ctx type_decls_map fun_dsigs) (FunDeclId.Map.values crate.fun_decls) in (* Translate the trait declarations *) let trait_decls = - List.map - (SymbolicToPure.translate_trait_decl trans_ctx) + List.filter_map + (fun a -> + try Some (SymbolicToPure.translate_trait_decl trans_ctx a) + with CFailure (meta, _) -> + let name = name_to_string trans_ctx a.name in + save_error __FILE__ __LINE__ meta + ("Could not translate the trait declaration '" ^ name + ^ "' because of previous error"); + None) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in (* Translate the trait implementations *) let trait_impls = - List.map - (SymbolicToPure.translate_trait_impl trans_ctx) + List.filter_map + (fun a -> + try Some (SymbolicToPure.translate_trait_impl trans_ctx a) + with CFailure (meta, _) -> + let name = name_to_string trans_ctx a.name in + save_error __FILE__ __LINE__ meta + ("Could not translate the trait instance '" ^ name + ^ "' because of previous error"); + None) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in @@ -473,7 +509,15 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) groups are always singletons, so the [extract_global_decl] function takes care of generating the delimiters. *) - let global = SymbolicToPure.translate_global ctx.trans_ctx global in + let global = + try Some (SymbolicToPure.translate_global ctx.trans_ctx global) + with CFailure (meta, _) -> + let name = name_to_string ctx.trans_ctx global.name in + save_error __FILE__ __LINE__ meta + ("Could not translate the global declaration '" ^ name + ^ "' because of previous error"); + None + in Extract.extract_global_decl ctx fmt global body config.interface (** Utility. @@ -728,22 +772,28 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) | TypeGroup (RecGroup ids) -> if config.extract_types then export_types_group true ids | FunGroup (NonRecGroup id) -> ( - (* Lookup *) - let pure_fun = FunDeclId.Map.find id ctx.trans_funs in + (* Lookup - the translated function may not be in the map if we had + to ignore it because of errors *) + let pure_fun = FunDeclId.Map.find_opt id ctx.trans_funs in (* Special case: we skip trait method *declarations* (we will extract their type directly in the records we generate for the trait declarations themselves, there is no point in having separate type definitions) *) - match pure_fun.f.Pure.kind with - | TraitItemDecl _ -> () - | _ -> - (* Translate *) - export_functions_group [ pure_fun ]) + match pure_fun with + | Some pure_fun -> ( + match pure_fun.f.Pure.kind with + | TraitItemDecl _ -> () + | _ -> + (* Translate *) + export_functions_group [ pure_fun ]) + | None -> ()) | FunGroup (RecGroup ids) -> (* General case of mutually recursive functions *) (* Lookup *) let pure_funs = - List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids + List.filter_map + (fun id -> FunDeclId.Map.find_opt id ctx.trans_funs) + ids in (* Translate *) export_functions_group pure_funs @@ -901,7 +951,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) | Coq -> Printf.fprintf out "End %s.\n" fi.module_name); (* Some logging *) - log#linfo (lazy ("Generated: " ^ fi.filename)); + if !Errors.error_list <> [] then + log#linfo + (lazy ("Generated the partial file (because of errors): " ^ fi.filename)) + else log#linfo (lazy ("Generated: " ^ fi.filename)); (* Flush and close the file *) close_out out diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index f5dd7df4..b2c60cc6 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -12,6 +12,26 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = let info = TypesAnalysis.analyze_ty infos ty in info.TypesAnalysis.contains_borrow +let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool + = + let visitor = + object + inherit [_] iter_ty as super + + method! visit_ty env ty = + match ty with + | TAdt (type_id, _) when type_id <> TTuple -> + let info = TypesAnalysis.analyze_ty infos ty in + if info.TypesAnalysis.contains_borrow then raise Found + else super#visit_ty env ty + | _ -> super#visit_ty env ty + end + in + try + visitor#visit_ty () ty; + false + with Found -> true + (** Retuns true if the type contains nested borrows. Note that we can't simply explore the type and look for regions: sometimes diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml index 91010e07..b6ee66f5 100644 --- a/compiler/ValuesUtils.ml +++ b/compiler/ValuesUtils.ml @@ -160,7 +160,7 @@ let find_first_primitively_copyable_sv_with_borrows method! visit_VSymbolic _ sv = let ty = sv.sv_ty in - if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then + if ty_is_copyable ty && ty_has_borrows type_infos ty then raise (FoundSymbolicValue sv) else () end |