diff options
30 files changed, 468 insertions, 181 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 8faaf62b..083a38d1 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -51,7 +51,9 @@ let compute_norm_trait_types_from_preds (meta : Meta.meta option) (* Sanity check: the type constraint can't make use of regions - Remark that it would be enough to only visit the field [ty] of the trait type constraint, but for safety we visit all the fields *) - sanity_check_opt_meta __FILE__ __LINE__ (trait_type_constraint_no_regions c) meta; + sanity_check_opt_meta __FILE__ __LINE__ + (trait_type_constraint_no_regions c) + meta; let { trait_ref; type_name; ty } : trait_type_constraint = c in let trait_ty = TTraitType (trait_ref, type_name) in let trait_ty_ref = get_ref trait_ty in diff --git a/compiler/Errors.ml b/compiler/Errors.ml index bfdf5796..41e841f0 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -13,43 +13,63 @@ exception CFailure of string let error_list : (Meta.meta option * string) list ref = ref [] -let push_error (file : string) (line : int) (meta : Meta.meta option) (msg : string) = - error_list := (meta, msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line) :: !error_list +let push_error (file : string) (line : int) (meta : Meta.meta option) + (msg : string) = + error_list := + (meta, msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line) + :: !error_list -let save_error (file : string) (line : int) ?(b : bool = true) (meta : Meta.meta option) (msg : string) = +let save_error (file : string) (line : int) ?(b : bool = true) + (meta : Meta.meta option) (msg : string) = push_error file line meta msg; match meta with | Some m -> - if !Config.fail_hard && b then - raise (Failure (format_error_message m (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line))) - | None -> if !Config.fail_hard && b then raise (Failure msg) + if !Config.fail_hard && not b then + raise + (Failure + (format_error_message m + (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line))) + | None -> if !Config.fail_hard && not b then raise (Failure msg) -let craise_opt_meta (file : string) (line : int) (meta : Meta.meta option) (msg : string) = +let craise_opt_meta (file : string) (line : int) (meta : Meta.meta option) + (msg : string) = match meta with | Some m -> - if !Config.fail_hard then raise (Failure (format_error_message m (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line))) + if !Config.fail_hard then + raise + (Failure + (format_error_message m + (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line))) else let () = push_error file line (Some m) msg in raise (CFailure msg) | None -> - if !Config.fail_hard then raise (Failure (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line)) + if !Config.fail_hard then + raise + (Failure (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line)) else let () = push_error file line None msg in raise (CFailure msg) -let craise (file : string) (line : int) (meta : Meta.meta) (msg : string) = craise_opt_meta file line (Some meta) msg +let craise (file : string) (line : int) (meta : Meta.meta) (msg : string) = + craise_opt_meta file line (Some meta) msg -let cassert_opt_meta (file : string) (line : int) (b : bool) (meta : Meta.meta option) (msg : string) = +let cassert_opt_meta (file : string) (line : int) (b : bool) + (meta : Meta.meta option) (msg : string) = if not b then craise_opt_meta file line meta msg -let cassert (file : string) (line : int) (b : bool) (meta : Meta.meta) (msg : string) = +let cassert (file : string) (line : int) (b : bool) (meta : Meta.meta) + (msg : string) = cassert_opt_meta file line b (Some meta) msg -let sanity_check (file : string) (line : int) b meta = cassert file line b meta "Internal error, please file an issue" +let sanity_check (file : string) (line : int) b meta = + cassert file line b meta "Internal error, please file an issue" let sanity_check_opt_meta (file : string) (line : int) b meta = cassert_opt_meta file line b meta "Internal error, please file an issue" -let internal_error (file : string) (line : int) meta = craise file line meta "Internal error, please report an issue" +let internal_error (file : string) (line : int) meta = + craise file line meta "Internal error, please report an issue" + let exec_raise = craise let exec_assert = cassert diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 4fb0e3c8..1a9b3baa 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -281,7 +281,9 @@ let lets_require_wrap_in_do (meta : Meta.meta) (* HOL4 is similar to HOL4, but we add a sanity check *) let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in if wrap_in_do then - sanity_check __FILE__ __LINE__ (List.for_all (fun (m, _, _) -> m) lets) meta; + sanity_check __FILE__ __LINE__ + (List.for_all (fun (m, _, _) -> m) lets) + meta; wrap_in_do | FStar | Coq -> false @@ -485,7 +487,9 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) F.pp_print_string fmt fun_name); (* Sanity check: HOL4 doesn't support const generics *) - sanity_check __FILE__ __LINE__ (generics.const_generics = [] || !backend <> HOL4) meta; + sanity_check __FILE__ __LINE__ + (generics.const_generics = [] || !backend <> HOL4) + meta; (* Print the generics. We might need to filter some of the type arguments, if the type @@ -1872,8 +1876,11 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (global : global_decl) (body : fun_decl) (interface : bool) : unit = let meta = body.meta in - cassert __FILE__ __LINE__ body.is_global_decl_body body.meta "TODO: Error message"; - cassert __FILE__ __LINE__ (body.signature.inputs = []) body.meta "TODO: Error message"; + cassert __FILE__ __LINE__ body.is_global_decl_body body.meta + "TODO: Error message"; + cassert __FILE__ __LINE__ + (body.signature.inputs = []) + body.meta "TODO: Error message"; (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 8809d0c3..74ac9e32 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -253,8 +253,8 @@ let empty_names_map : names_map = } (** Small helper to report name collision *) -let report_name_collision (id_to_string : id -> string) - (id1 : id) (id2 : id) (name : string) : unit = +let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id) + (name : string) : unit = let id1 = "\n- " ^ id_to_string id1 in let id2 = "\n- " ^ id_to_string id2 in let err = @@ -265,8 +265,7 @@ let report_name_collision (id_to_string : id -> string) (* If we fail hard on errors, raise an exception *) save_error __FILE__ __LINE__ None err -let names_map_get_id_from_name (name : string) (nm : names_map) : - id option = +let names_map_get_id_from_name (name : string) (nm : names_map) : id option = StringMap.find_opt name nm.name_to_id let names_map_check_collision (id_to_string : id -> string) (id : id) diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index f737f73b..6dbf528c 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -148,7 +148,8 @@ let extract_unop (meta : Meta.meta) (extract_expr : bool -> texpression -> unit) (cast_str, None, Some tgt) | TInteger _, TBool -> (* This is not allowed by rustc: the way of doing it in Rust is: [x != 0] *) - craise __FILE__ __LINE__ meta "Unexpected cast: integer to bool" + craise __FILE__ __LINE__ meta + "Unexpected cast: integer to bool" | TBool, TBool -> (* There shouldn't be any cast here. Note that if one writes [b as bool] in Rust (where [b] is a @@ -534,7 +535,8 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) extract_rec false ret_ty; if inside then F.pp_print_string fmt ")" | TTraitType (trait_ref, type_name) -> ( - if !parameterize_trait_types then craise __FILE__ __LINE__ meta "Unimplemented" + if !parameterize_trait_types then + craise __FILE__ __LINE__ meta "Unimplemented" else let type_name = ctx_get_trait_type meta trait_ref.trait_decl_ref.trait_decl_id @@ -818,7 +820,8 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : (fun variant_id (variant : variant) -> (variant_id, StringMap.find variant.variant_name variant_map)) variants - | _ -> craise __FILE__ __LINE__ def.meta "Invalid builtin information" + | _ -> + craise __FILE__ __LINE__ def.meta "Invalid builtin information" in List.fold_left (fun ctx (vid, vname) -> diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index df2a010d..cad469f9 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -145,7 +145,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - sanity_check __FILE__ __LINE__ ((not f.is_global_decl_body) || not !stateful) f.meta; + sanity_check __FILE__ __LINE__ + ((not f.is_global_decl_body) || not !stateful) + f.meta; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index ea1d5633..a65e1663 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -435,7 +435,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) else abs | Loop (loop_id', _, LoopCall) -> (* We can end all the loop call abstractions *) - sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') fdef.meta; + sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') + fdef.meta; { abs with can_end = true } | SynthInput rg_id' -> if rg_id' = back_id && end_fun_synth_input then @@ -636,7 +637,9 @@ module Test = struct fdef.name)); (* Sanity check - *) - sanity_check __FILE__ __LINE__ (fdef.signature.generics = empty_generic_params) fdef.meta; + sanity_check __FILE__ __LINE__ + (fdef.signature.generics = empty_generic_params) + fdef.meta; sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.meta; (* Create the evaluation context *) diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index cc34020a..b32261e6 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -308,7 +308,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) ("give_back_value: improper 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"); + craise __FILE__ __LINE__ meta + "Value given back doesn't have the proper type"); (* Replace *) set_replaced (); nv.value) @@ -442,7 +443,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta "Only one loan should have been given back"; + cassert __FILE__ __LINE__ !replaced meta + "Only one loan should have been given back"; (* Apply the reborrows *) apply_registered_reborrows ctx @@ -451,7 +453,9 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Sanity checks *) - sanity_check __FILE__ __LINE__ (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta; + sanity_check __FILE__ __LINE__ + (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) + meta; (* Store the given-back value as a meta-value for synthesis purposes *) let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) @@ -498,7 +502,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - cassert __FILE__ __LINE__ (not !replaced) meta "Only one loan should have been updated"; + cassert __FILE__ __LINE__ (not !replaced) meta + "Only one loan should have been updated"; replaced := true in let obj = @@ -541,7 +546,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) ("give_back_avalue_to_same_abstraction: improper 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"); + 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 *) @@ -601,7 +607,8 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - cassert __FILE__ __LINE__ (not !replaced) meta "Only one loan should be updated"; + cassert __FILE__ __LINE__ (not !replaced) meta + "Only one loan should be updated"; replaced := true in let obj = @@ -666,7 +673,8 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta "Exactly one loan should be given back"; + cassert __FILE__ __LINE__ !replaced meta + "Exactly one loan should be given back"; (* Return *) ctx @@ -773,21 +781,27 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) sanity_check __FILE__ __LINE__ (l' = l) meta; sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) meta; (* Check that the corresponding loan is somewhere - purely a sanity check *) - sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta; + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* Update the context *) give_back_value config meta l tv ctx | Concrete (VSharedBorrow l' | VReservedMutBorrow l') -> (* Sanity check *) sanity_check __FILE__ __LINE__ (l' = l) meta; (* Check that the borrow is somewhere - purely a sanity check *) - sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta; + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* Update the context *) give_back_shared config meta l ctx | Abstract (AMutBorrow (l', av)) -> (* Sanity check *) sanity_check __FILE__ __LINE__ (l' = l) meta; (* Check that the corresponding loan is somewhere - purely a sanity check *) - sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta; + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* Convert the avalue to a (fresh symbolic) value. Rem.: we shouldn't do this here. We should do this in a function @@ -802,7 +816,9 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (* Sanity check *) sanity_check __FILE__ __LINE__ (l' = l) meta; (* Check that the borrow is somewhere - purely a sanity check *) - sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta; + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* Update the context *) give_back_shared config meta l ctx | Abstract (AProjSharedBorrow asb) -> @@ -946,7 +962,9 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (* Sanity check: the borrowed value shouldn't contain loans *) (match bc with | Concrete (VMutBorrow (_, bv)) -> - sanity_check __FILE__ __LINE__ (Option.is_none (get_first_loan_in_value bv)) meta + sanity_check __FILE__ __LINE__ + (Option.is_none (get_first_loan_in_value bv)) + meta | _ -> ()); (* Give back the value *) let ctx = give_back config meta l bc ctx in @@ -1602,7 +1620,9 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) ("activate_reserved_mut_borrow: resulting value:\n" ^ typed_value_to_string ~meta:(Some meta) ctx sv)); sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta; - sanity_check __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions sv)) meta; + sanity_check __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions sv)) + meta; sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) meta; (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) @@ -1737,7 +1757,8 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) list_avalues false push_fail child_av | AProjSharedBorrow asb -> (* We don't support nested borrows *) - cassert __FILE__ __LINE__ (asb = []) meta "Nested borrows are not supported yet"; + cassert __FILE__ __LINE__ (asb = []) meta + "Nested borrows are not supported yet"; (* Nothing specific to do *) () | AEndedMutBorrow _ | AEndedSharedBorrow -> @@ -1749,7 +1770,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) | ASymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta + sanity_check __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos ty)) + meta and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in match v.value with @@ -1803,7 +1826,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta; + sanity_check __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos ty)) + meta; ([], v) in @@ -2033,7 +2058,9 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) loans := BorrowId.Set.union !loans ids; BorrowId.Set.iter (fun id -> - sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) meta; + sanity_check __FILE__ __LINE__ + (not (BorrowId.Map.mem id !loan_to_content)) + meta; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans) ids @@ -2041,14 +2068,18 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) let push_loan id (lc : g_loan_content_with_ty) : unit = sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) meta; loans := BorrowId.Set.add id !loans; - sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) meta; + sanity_check __FILE__ __LINE__ + (not (BorrowId.Map.mem id !loan_to_content)) + meta; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans in let push_borrow id (bc : g_borrow_content_with_ty) : unit = sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) meta; borrows := BorrowId.Set.add id !borrows; - sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !borrow_to_content)) meta; + sanity_check __FILE__ __LINE__ + (not (BorrowId.Map.mem id !borrow_to_content)) + meta; borrow_to_content := BorrowId.Map.add id bc !borrow_to_content; borrows_loans := BorrowId id :: !borrows_loans in @@ -2129,7 +2160,9 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) method! visit_symbolic_value _ sv = (* Sanity check: no borrows *) - sanity_check __FILE__ __LINE__ (not (symbolic_value_has_borrows ctx sv)) meta + sanity_check __FILE__ __LINE__ + (not (symbolic_value_has_borrows ctx sv)) + meta end in @@ -2240,7 +2273,9 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (* Sanity check: there is no loan/borrows which appears in both abstractions, unless we allow to merge duplicates *) if merge_funs = None then - (sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint borrows0 borrows1) meta; + (sanity_check __FILE__ __LINE__ + (BorrowId.Set.disjoint borrows0 borrows1) + meta; sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1)) meta; @@ -2358,8 +2393,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) to preserve (in practice it works because we destructure the shared values in the abstractions, and forbid nested borrows). *) - sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta; - sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta; + sanity_check __FILE__ __LINE__ + (not (value_has_loans_or_borrows ctx sv0.value)) + meta; + sanity_check __FILE__ __LINE__ + (not (value_has_loans_or_borrows ctx sv0.value)) + meta; sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta; sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta; None) @@ -2476,7 +2515,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) meta; - sanity_check __FILE__ __LINE__ (is_aignored child.value) meta; + sanity_check __FILE__ __LINE__ + (is_aignored child.value) meta; sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv.value)) meta; diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index fd656063..92d8670a 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -110,7 +110,9 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) sanity_check __FILE__ __LINE__ (id1 = id2) meta; (* There are no regions in the const generics, so we ignore them, but we still check they are the same, for sanity *) - sanity_check __FILE__ __LINE__ (generics1.const_generics = generics2.const_generics) meta; + sanity_check __FILE__ __LINE__ + (generics1.const_generics = generics2.const_generics) + meta; (* We also ignore the trait refs *) @@ -805,7 +807,9 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) let set_non_shared () = match !shared with | None -> shared := Some false - | Some _ -> craise __FILE__ __LINE__ meta "Found unexpected intersecting proj_borrows" + | Some _ -> + craise __FILE__ __LINE__ meta + "Found unexpected intersecting proj_borrows" in let check_proj_borrows is_shared abs sv' proj_ty = if @@ -825,7 +829,9 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) method! visit_abstract_shared_borrows abs asb = (* Sanity check *) - (match !shared with Some b -> sanity_check __FILE__ __LINE__ b meta | _ -> ()); + (match !shared with + | Some b -> sanity_check __FILE__ __LINE__ b meta + | _ -> ()); (* Explore *) if can_update_shared then let abs = Option.get abs in @@ -857,7 +863,8 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Check that we updated the context at least once *) - cassert __FILE__ __LINE__ (Option.is_some !shared) meta "Context was not updated at least once"; + cassert __FILE__ __LINE__ (Option.is_some !shared) meta + "Context was not updated at least once"; (* Return *) ctx @@ -1156,7 +1163,8 @@ let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value) in (* Apply *) try obj#visit_eval_ctx () ctx - with Found -> craise __FILE__ __LINE__ meta "update_aproj_loans_to_ended: failed" + with Found -> + craise __FILE__ __LINE__ meta "update_aproj_loans_to_ended: failed" (** Helper function diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 0b7c071e..e47fbfbe 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -78,7 +78,9 @@ let apply_symbolic_expansion_to_target_avalues (config : config) method! visit_aproj current_abs aproj = (match aproj with | AProjLoans (sv, _) | AProjBorrows (sv, _) -> - sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) meta + sanity_check __FILE__ __LINE__ + (not (same_symbolic_id sv original_sv)) + meta | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj current_abs aproj @@ -228,7 +230,8 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) in (* Check if there is strictly more than one variant *) if List.length variants_fields_types > 1 && not expand_enumerations then - craise __FILE__ __LINE__ meta "Not allowed to expand enumerations with several variants"; + craise __FILE__ __LINE__ meta + "Not allowed to expand enumerations with several variants"; (* Initialize the expanded value for a given variant *) let initialize ((variant_id, field_types) : VariantId.id option * rty list) : symbolic_expansion = @@ -279,7 +282,8 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta) | TAssumed TBox, [], [ boxed_ty ] -> [ compute_expanded_symbolic_box_value meta boxed_ty ] | _ -> - craise __FILE__ __LINE__ meta "compute_expanded_symbolic_adt_value: unexpected combination" + craise __FILE__ __LINE__ meta + "compute_expanded_symbolic_adt_value: unexpected combination" let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) @@ -356,7 +360,9 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) method! visit_aproj proj_regions aproj = (match aproj with | AProjLoans (sv, _) | AProjBorrows (sv, _) -> - sanity_check __FILE__ __LINE__ (not (same_symbolic_id sv original_sv)) meta + sanity_check __FILE__ __LINE__ + (not (same_symbolic_id sv original_sv)) + meta | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj proj_regions aproj @@ -402,7 +408,9 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) fun cf ctx -> sanity_check __FILE__ __LINE__ (region <> RErased) meta; (* Check that we are allowed to expand the reference *) - sanity_check __FILE__ __LINE__ (not (region_in_set region ctx.ended_regions)) meta; + sanity_check __FILE__ __LINE__ + (not (region_in_set region ctx.ended_regions)) + meta; (* Match on the reference kind *) match rkind with | RMut -> @@ -490,7 +498,9 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) match resl with | Some _ :: _ -> Some (List.map Option.get resl) | None :: _ -> - List.iter (fun res -> sanity_check __FILE__ __LINE__ (res = None) meta) resl; + List.iter + (fun res -> sanity_check __FILE__ __LINE__ (res = None) meta) + resl; None | _ -> craise __FILE__ __LINE__ meta "Unreachable" in @@ -573,7 +583,9 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* Sanity check: the symbolic value has disappeared *) - sanity_check __FILE__ __LINE__ (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta) + sanity_check __FILE__ __LINE__ + (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) + meta) in (* Continue *) cc cf ctx @@ -603,7 +615,9 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta) let seel = List.map (fun see -> (Some see, cf_branches)) seel in apply_branching_symbolic_expansions_non_borrow config meta original_sv original_sv_place seel cf_after_join ctx - | _ -> craise __FILE__ __LINE__ meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) + | _ -> + craise __FILE__ __LINE__ meta + ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) @@ -684,7 +698,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : of [config]): " ^ name_to_string ctx def.name) | Opaque -> - craise __FILE__ __LINE__ meta "Attempted to greedily expand an opaque type"); + craise __FILE__ __LINE__ meta + "Attempted to greedily expand an opaque type"); (* Also, we need to check if the definition is recursive *) if ctx_type_decl_is_rec ctx def_id then craise __FILE__ __LINE__ meta diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 59f74ad8..d61ba410 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -142,9 +142,12 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) (* Sanity check *) (match v.ty with | TAdt (TAssumed TBox, _) -> - exec_raise __FILE__ __LINE__ meta "Can't copy an assumed value other than Option" + exec_raise __FILE__ __LINE__ meta + "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) meta + sanity_check __FILE__ __LINE__ + (allow_adt_copy || ty_is_primitively_copyable ty) + meta | TAdt (TTuple, _) -> () (* Ok *) | TAdt ( TAssumed (TSlice | TArray), @@ -174,13 +177,15 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) let bid' = fresh_borrow_id () in let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in (ctx, { v with value = VBorrow (VSharedBorrow bid') }) - | VMutBorrow (_, _) -> exec_raise __FILE__ __LINE__ meta "Can't copy a mutable borrow" + | VMutBorrow (_, _) -> + exec_raise __FILE__ __LINE__ meta "Can't copy a mutable borrow" | VReservedMutBorrow _ -> exec_raise __FILE__ __LINE__ meta "Can't copy a reserved mut borrow") | VLoan lc -> ( (* We can only copy shared loans *) match lc with - | VMutLoan _ -> exec_raise __FILE__ __LINE__ meta "Can't copy a mutable loan" + | VMutLoan _ -> + exec_raise __FILE__ __LINE__ meta "Can't copy a mutable loan" | VSharedLoan (_, sv) -> (* We don't copy the shared loan: only the shared value inside *) copy_value meta allow_adt_copy config ctx sv) @@ -420,7 +425,9 @@ let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand) (op2 : operand) (cf : typed_value * typed_value -> m_fun) : m_fun = let eval_op = eval_operands config meta [ op1; op2 ] in let use_res cf res = - match res with [ v1; v2 ] -> cf (v1, v2) | _ -> craise __FILE__ __LINE__ meta "Unreachable" + match res with + | [ v1; v2 ] -> cf (v1, v2) + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in comp eval_op use_res cf @@ -463,7 +470,9 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) let b = if Z.of_int 0 = sv.value then false else if Z.of_int 1 = sv.value then true - else exec_raise __FILE__ __LINE__ meta "Conversion from int to bool: out of range" + else + exec_raise __FILE__ __LINE__ meta + "Conversion from int to bool: out of range" in let value = VLiteral (VBool b) in let ty = TLiteral TBool in @@ -793,7 +802,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) meta; (* 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__ (len = Z.of_int (List.length values)) meta; + sanity_check __FILE__ __LINE__ + (len = Z.of_int (List.length values)) + meta; let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in let ty = TAdt (TAssumed TArray, generics) in (* In order to generate a better AST, we introduce a symbolic @@ -809,7 +820,8 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (* Introduce the symbolic value in the AST *) let sv = ValuesUtils.value_as_symbolic meta saggregated.value in Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))) - | AggregatedClosure _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" + | AggregatedClosure _ -> + craise __FILE__ __LINE__ meta "Closures are not supported yet" in (* Compose and apply *) comp eval_ops compute cf diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 17487401..e4370367 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -160,7 +160,8 @@ let eval_loop_symbolic (config : config) (meta : meta) cf res ctx | Continue i -> (* We don't support nested loops for now *) - cassert __FILE__ __LINE__ (i = 0) meta "Nested loops are not supported yet"; + cassert __FILE__ __LINE__ (i = 0) meta + "Nested loops are not supported yet"; log#ldebug (lazy ("eval_loop_symbolic: about to match the fixed-point context \ diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index a8a64264..2283e842 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -380,7 +380,9 @@ let ctx_split_fixed_new (meta : Meta.meta) (fixed_ids : ids_sets) let new_absl = List.map (fun ee -> - match ee with EAbs abs -> abs | _ -> craise __FILE__ __LINE__ meta "Unreachable") + match ee with + | EAbs abs -> abs + | _ -> craise __FILE__ __LINE__ meta "Unreachable") new_absl in let new_dummyl = diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 39add08e..9ff2fe38 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -270,10 +270,13 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : (* Rem.: the below sanity checks are not really necessary *) sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) meta; sanity_check __FILE__ __LINE__ (abs.original_parents = []) meta; - sanity_check __FILE__ __LINE__ (RegionId.Set.is_empty abs.ancestors_regions) meta; + sanity_check __FILE__ __LINE__ + (RegionId.Set.is_empty abs.ancestors_regions) + meta; (* Introduce the new abstraction for the shared values *) - cassert __FILE__ __LINE__ (ty_no_regions sv.ty) meta "Nested borrows are not supported yet"; + cassert __FILE__ __LINE__ (ty_no_regions sv.ty) meta + "Nested borrows are not supported yet"; let rty = sv.ty in (* Create the shared loan child *) @@ -481,7 +484,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) craise __FILE__ __LINE__ meta "Unreachable" | Continue i -> (* For now we don't support continues to outer loops *) - cassert __FILE__ __LINE__ (i = 0) meta "Continues to outer loops not supported yet"; + cassert __FILE__ __LINE__ (i = 0) meta + "Continues to outer loops not supported yet"; register_ctx ctx; None | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> @@ -736,7 +740,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (* We also check that all the regions need to end - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating... *) - sanity_check __FILE__ __LINE__ (AbstractionId.Set.equal !aids_union !fp_aids) meta; + sanity_check __FILE__ __LINE__ + (AbstractionId.Set.equal !aids_union !fp_aids) + meta; (* Merge the abstractions which need to be merged, and compute the map from region id to abstraction id *) @@ -794,7 +800,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) fp := fp'; id0 := id0'; () - with ValueMatchFailure _ -> craise __FILE__ __LINE__ meta "Unexpected") + with ValueMatchFailure _ -> + craise __FILE__ __LINE__ meta "Unexpected") ids; (* Register the mapping *) let abs = ctx_lookup_abs !fp !id0 in @@ -957,7 +964,9 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) ids.loan_ids in (* Check that the loan and borrows are related *) - sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids.borrow_ids loan_ids) meta) + sanity_check __FILE__ __LINE__ + (BorrowId.Set.equal ids.borrow_ids loan_ids) + meta) new_absl; (* For every target abstraction (going back to the [list_nth_mut] example, diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 3b1767e8..d97b05d0 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -335,8 +335,12 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) let _ = let _, ty0, _ = ty_as_ref ty0 in let _, ty1, _ = ty_as_ref ty1 in - sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta; - sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta + sanity_check __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) + meta; + sanity_check __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) + meta in (* Same remarks as for [merge_amut_borrows] *) @@ -365,8 +369,12 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) This time we need to also merge the shared values. We rely on the join matcher [JM] to do so. *) - sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta; - sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv1.value)) meta; + sanity_check __FILE__ __LINE__ + (not (value_has_loans_or_borrows ctx sv0.value)) + meta; + sanity_check __FILE__ __LINE__ + (not (value_has_loans_or_borrows ctx sv1.value)) + meta; let ty = ty0 in let child = child0 in let sv = M.match_typed_values ctx ctx sv0 sv1 in @@ -437,7 +445,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (* Variables are necessarily in the prefix *) craise __FILE__ __LINE__ meta "Unreachable" | EBinding (BDummy did, _) -> - sanity_check __FILE__ __LINE__ (not (DummyVarId.Set.mem did fixed_ids.dids)) meta + sanity_check __FILE__ __LINE__ + (not (DummyVarId.Set.mem did fixed_ids.dids)) + meta | EAbs abs -> sanity_check __FILE__ __LINE__ (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) @@ -527,7 +537,8 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (* Same as for the dummy values: there are two cases *) if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( (* Still in the prefix: the abstractions must be the same *) - cassert __FILE__ __LINE__ (abs0 = abs1) meta "The abstractions are not the same"; + cassert __FILE__ __LINE__ (abs0 = abs1) meta + "The abstractions are not the same"; (* Continue *) abs :: join_prefixes env0' env1') else (* Not in the prefix anymore *) diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 9c017f19..6d814c5c 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -96,7 +96,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) | AIgnoredSharedLoan child -> (* Ignore the id of the loan, if there is *) self#visit_typed_avalue abs_id child - | AEndedMutLoan _ | AEndedSharedLoan _ -> craise __FILE__ __LINE__ meta "Unreachable" + | AEndedMutLoan _ | AEndedSharedLoan _ -> + craise __FILE__ __LINE__ meta "Unreachable" (** Make sure we don't register the ignored ids *) method! visit_aborrow_content abs_id bc = @@ -109,7 +110,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool) -> (* Ignore the id of the borrow, if there is *) self#visit_typed_avalue abs_id child - | AEndedMutBorrow _ | AEndedSharedBorrow -> craise __FILE__ __LINE__ meta "Unreachable" + | AEndedMutBorrow _ | AEndedSharedBorrow -> + craise __FILE__ __LINE__ meta "Unreachable" method! visit_borrow_id abs_id bid = register_borrow_id abs_id bid method! visit_loan_id abs_id lid = register_loan_id abs_id lid @@ -151,8 +153,12 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) match (ty0, ty1) with | TAdt (id0, generics0), TAdt (id1, generics1) -> sanity_check __FILE__ __LINE__ (id0 = id1) meta; - sanity_check __FILE__ __LINE__ (generics0.const_generics = generics1.const_generics) meta; - sanity_check __FILE__ __LINE__ (generics0.trait_refs = generics1.trait_refs) meta; + sanity_check __FILE__ __LINE__ + (generics0.const_generics = generics1.const_generics) + meta; + sanity_check __FILE__ __LINE__ + (generics0.trait_refs = generics1.trait_refs) + meta; let id = id0 in let const_generics = generics1.const_generics in let trait_refs = generics1.trait_refs in @@ -213,8 +219,12 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct { value; ty = v1.ty } else ( (* For now, we don't merge ADTs which contain borrows *) - sanity_check __FILE__ __LINE__ (not (value_has_borrows v0.value)) M.meta; - sanity_check __FILE__ __LINE__ (not (value_has_borrows v1.value)) M.meta; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows v0.value)) + M.meta; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows v1.value)) + M.meta; (* Merge *) M.match_distinct_adts ctx0 ctx1 ty av0 av1) | VBottom, VBottom -> v0 @@ -387,7 +397,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in - sanity_check __FILE__ __LINE__ (not (value_has_borrows sv.value)) M.meta; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows sv.value)) + M.meta; M.match_ashared_loans ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 av1 ty sv av | AMutLoan (id0, av0), AMutLoan (id1, av1) -> @@ -795,11 +807,21 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_ashared_borrows _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_borrows _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" end @@ -917,11 +939,21 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_ashared_borrows _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" - let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_borrows _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_borrows _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = + craise __FILE__ __LINE__ meta "Unreachable" + let match_avalues _ _ _ _ = craise __FILE__ __LINE__ meta "Unreachable" end @@ -1129,7 +1161,9 @@ struct sanity_check __FILE__ __LINE__ left meta; let id = sv.sv_id in (* Check: fixed values are fixed *) - sanity_check __FILE__ __LINE__ (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta; + sanity_check __FILE__ __LINE__ + (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) + meta; (* Update the binding for the target symbolic value *) S.sid_to_value_map := SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; @@ -1355,7 +1389,8 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) sanity_check __FILE__ __LINE__ (v0 = v1) meta; (* The ids present in the left value must be fixed *) let ids, _ = compute_typed_value_ids v0 in - sanity_check __FILE__ __LINE__ ((not S.check_equiv) || ids_are_fixed ids)) + sanity_check __FILE__ __LINE__ + ((not S.check_equiv) || ids_are_fixed ids)) meta; (* We still match the values - allows to compute mappings (which are the identity actually) *) @@ -1376,7 +1411,9 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) sanity_check __FILE__ __LINE__ (abs0 = abs1) meta; (* Their ids must be fixed *) let ids, _ = compute_abs_ids abs0 in - sanity_check __FILE__ __LINE__ ((not S.check_equiv) || ids_are_fixed ids) meta; + sanity_check __FILE__ __LINE__ + ((not S.check_equiv) || ids_are_fixed ids) + meta; (* Continue *) match_envs env0' env1') else ( @@ -1765,7 +1802,8 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) abstractions and in the *variable bindings* once we allow symbolic values containing borrows to not be eagerly expanded. *) - sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows meta; + sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows + meta; (* Update the borrows and loans in the abstractions of the target context. diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 26456acf..93e56106 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -101,7 +101,9 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (match (proj_kind, type_id) with | ProjAdt (def_id, opt_variant_id), TAdtId def_id' -> sanity_check __FILE__ __LINE__ (def_id = def_id') meta; - sanity_check __FILE__ __LINE__ (opt_variant_id = adt.variant_id) meta + sanity_check __FILE__ __LINE__ + (opt_variant_id = adt.variant_id) + meta | _ -> craise __FILE__ __LINE__ meta "Unreachable"); (* Actually project *) let fv = FieldId.nth adt.field_values field_id in @@ -117,7 +119,9 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) Ok (ctx, { res with updated })) (* Tuples *) | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> ( - sanity_check __FILE__ __LINE__ (arity = List.length adt.field_values) meta; + sanity_check __FILE__ __LINE__ + (arity = List.length adt.field_values) + meta; let fv = FieldId.nth adt.field_values field_id in (* Project *) match access_projection meta access ctx update p' fv with @@ -191,7 +195,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } | AIgnoredSharedLoan _ ) ) -> - craise __FILE__ __LINE__ meta "Expected a shared (abstraction) loan" + craise __FILE__ __LINE__ meta + "Expected a shared (abstraction) loan" | _, Abstract (ASharedLoan (bids, sv, _av)) -> ( (* Explore the shared value *) match access_projection meta access ctx update p' sv with @@ -327,7 +332,8 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place) let read_place (meta : Meta.meta) (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value = match try_read_place meta access p ctx with - | Error e -> craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e) + | Error e -> + craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e) | Ok v -> v (** Attempt to update the value at a given place *) @@ -345,13 +351,16 @@ let try_write_place (meta : Meta.meta) (access : access_kind) (p : place) let write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : typed_value) (ctx : eval_ctx) : eval_ctx = match try_write_place meta access p nv ctx with - | Error e -> craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e) + | Error e -> + craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e) | Ok ctx -> ctx let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option) (generics : generic_args) : typed_value = - sanity_check __FILE__ __LINE__ (TypesUtils.generic_args_only_erased_regions generics) meta; + sanity_check __FILE__ __LINE__ + (TypesUtils.generic_args_only_erased_regions generics) + meta; (* Lookup the definition and check if it is an enumeration - it should be an enumeration if and only if the projection element is a field projection with *some* variant id. Retrieve the list @@ -475,7 +484,8 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) | FailBottom (_, _, _) -> (* We can't expand {!Bottom} values while reading them *) craise __FILE__ __LINE__ meta "Found [Bottom] while reading a place" - | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not read a borrow" + | FailBorrow _ -> + craise __FILE__ __LINE__ meta "Could not read a borrow" in comp cc (update_ctx_along_read_place config meta access p) cf ctx @@ -506,7 +516,8 @@ let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) pe ty ctx in cf ctx - | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not write to a borrow" + | FailBorrow _ -> + craise __FILE__ __LINE__ meta "Could not write to a borrow" in (* Retry *) comp cc (update_ctx_along_write_place config meta access p) cf ctx diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 0421a46c..d7c20ae0 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -212,7 +212,8 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: " ^ RegionId.Set.to_string None rset2 ^ "\n")); - sanity_check __FILE__ __LINE__ (not (projections_intersect meta ty1 rset1 ty2 rset2))) + sanity_check __FILE__ __LINE__ + (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta; ASymbolic (AProjBorrows (s, ty)) | _ -> @@ -250,7 +251,8 @@ let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta) let value = VBorrow (VMutBorrow (bid, bv)) in { value; ty } | SeSharedRef (_, _) -> - craise __FILE__ __LINE__ meta "Unexpected symbolic shared reference expansion" + craise __FILE__ __LINE__ meta + "Unexpected symbolic shared reference expansion" | _ -> symbolic_expansion_non_borrow_to_value meta sv see (** Apply (and reduce) a projector over loans to a value. @@ -262,7 +264,9 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (see : symbolic_expansion) (original_sv_ty : rty) : typed_avalue = (* Sanity check: if we have a proj_loans over a symbolic value, it should * contain regions which we will project *) - sanity_check __FILE__ __LINE__ (ty_has_regions_in_set regions original_sv_ty) meta; + sanity_check __FILE__ __LINE__ + (ty_has_regions_in_set regions original_sv_ty) + meta; (* Match *) let (value, ty) : avalue * ty = match (see, original_sv_ty) with diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index ccf8a5ac..7e6236b1 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -243,7 +243,9 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) a variant with all its fields set to {!Bottom} *) match av.variant_id with - | None -> craise __FILE__ __LINE__ meta "Found a struct value while expected an enum" + | None -> + craise __FILE__ __LINE__ meta + "Found a struct value while expected an enum" | Some variant_id' -> if variant_id' = variant_id then (* Nothing to do *) cf Unit ctx @@ -276,8 +278,10 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) * setting a discriminant should only be used to initialize a value, * or reset an already initialized value, really. *) craise __FILE__ __LINE__ meta "Unexpected value" - | _, (VAdt _ | VBottom) -> craise __FILE__ __LINE__ meta "Inconsistent state" - | _, (VLiteral _ | VBorrow _ | VLoan _) -> craise __FILE__ __LINE__ meta "Unexpected value" + | _, (VAdt _ | VBottom) -> + craise __FILE__ __LINE__ meta "Inconsistent state" + | _, (VLiteral _ | VBorrow _ | VLoan _) -> + craise __FILE__ __LINE__ meta "Unexpected value" in (* Compose and apply *) comp cc update_value cf ctx @@ -434,7 +438,9 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta) :: EBinding (_ret_var, _) :: EFrame :: _ ) -> (* Required type checking *) - cassert __FILE__ __LINE__ (input_value.ty = boxed_ty) meta "TODO: Error message"; + cassert __FILE__ __LINE__ + (input_value.ty = boxed_ty) + meta "TODO: Error message"; (* Move the input value *) let cf_move = @@ -1294,7 +1300,9 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) let locals, body_st = Subst.fun_body_substitute_in_body subst body in (* Evaluate the input operands *) - sanity_check __FILE__ __LINE__ (List.length args = body.arg_count) body.meta; + sanity_check __FILE__ __LINE__ + (List.length args = body.arg_count) + body.meta; let cc = eval_operands config body.meta args in (* Push a frame delimiter - we use {!comp_transmit} to transmit the result diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 4fd7722e..4ee11cbd 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -508,8 +508,12 @@ let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (* Generate the type substitution Note that for now we don't support instantiating the type parameters with types containing regions. *) - sanity_check __FILE__ __LINE__ (List.for_all TypesUtils.ty_no_regions generics.types) meta; - sanity_check __FILE__ __LINE__ (TypesUtils.trait_instance_id_no_regions tr_self) meta; + sanity_check __FILE__ __LINE__ + (List.for_all TypesUtils.ty_no_regions generics.types) + meta; + sanity_check __FILE__ __LINE__ + (TypesUtils.trait_instance_id_no_regions tr_self) + meta; let tsubst = Substitute.make_type_subst_from_vars sg.generics.types generics.types in diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 830661d2..642d7a37 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -196,7 +196,9 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = BorrowId.Map.update repr_bid (fun x -> - match x with Some _ -> Some info | None -> craise __FILE__ __LINE__ meta "Unreachable") + match x with + | Some _ -> Some info + | None -> craise __FILE__ __LINE__ meta "Unreachable") !borrows_infos in borrows_infos := infos @@ -212,7 +214,9 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : | RShared, (BShared | BReserved) | RMut, BMut -> () | _ -> craise __FILE__ __LINE__ meta "Invariant not satisfied"); (* A reserved borrow can't point to a value inside an abstraction *) - sanity_check __FILE__ __LINE__ (kind <> BReserved || not info.loan_in_abs) meta; + sanity_check __FILE__ __LINE__ + (kind <> BReserved || not info.loan_in_abs) + meta; (* Insert the borrow id *) let borrow_ids = info.borrow_ids in sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem bid borrow_ids)) meta; @@ -283,7 +287,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : = BorrowId.Set.elements info.borrow_ids) meta; match info.loan_kind with - | RMut -> sanity_check __FILE__ __LINE__ (BorrowId.Set.cardinal info.loan_ids = 1) meta + | RMut -> + sanity_check __FILE__ __LINE__ + (BorrowId.Set.cardinal info.loan_ids = 1) + meta | RShared -> ()) !borrows_infos @@ -373,7 +380,8 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) : unit = match (cv, ty) with - | VScalar sv, TInteger int_ty -> sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta + | VScalar sv, TInteger int_ty -> + sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta | VBool _, TBool | VChar _, TChar -> () | _ -> craise __FILE__ __LINE__ meta "Erroneous typing" @@ -481,8 +489,11 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (TypesUtils.const_generic_as_literal cg)) .value in - sanity_check __FILE__ __LINE__ (Z.of_int (List.length inner_values) = len) meta - | (TSlice | TStr), _, _, _, _ -> craise __FILE__ __LINE__ meta "Unexpected" + sanity_check __FILE__ __LINE__ + (Z.of_int (List.length inner_values) = len) + meta + | (TSlice | TStr), _, _, _, _ -> + craise __FILE__ __LINE__ meta "Unexpected" | _ -> craise __FILE__ __LINE__ meta "Erroneous type") | VBottom, _ -> (* Nothing to check *) () | VBorrow bc, TRef (_, ref_ty, rkind) -> ( @@ -503,7 +514,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | _ -> craise __FILE__ __LINE__ meta "Erroneous typing") | VLoan lc, ty -> ( match lc with - | VSharedLoan (_, sv) -> sanity_check __FILE__ __LINE__ (sv.ty = ty) meta + | VSharedLoan (_, sv) -> + sanity_check __FILE__ __LINE__ (sv.ty = ty) meta | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in @@ -511,7 +523,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | Concrete (VMutBorrow (_, bv)) -> sanity_check __FILE__ __LINE__ (bv.ty = ty) meta | Abstract (AMutBorrow (_, sv)) -> - sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = ty) meta + sanity_check __FILE__ __LINE__ + (Substitute.erase_regions sv.ty = ty) + meta | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")) | VSymbolic sv, ty -> let ty' = Substitute.erase_regions sv.sv_ty in @@ -607,7 +621,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions ref_ty) meta + sanity_check __FILE__ __LINE__ + (sv.ty = Substitute.erase_regions ref_ty) + meta | _ -> craise __FILE__ __LINE__ meta "Inconsistent context") | AIgnoredMutBorrow (_opt_bid, av), RMut -> sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta @@ -649,7 +665,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AEndedMutLoan { given_back; child; given_back_meta = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in - sanity_check __FILE__ __LINE__ (given_back.ty = borrowed_aty) meta; + sanity_check __FILE__ __LINE__ + (given_back.ty = borrowed_aty) + meta; sanity_check __FILE__ __LINE__ (child.ty = borrowed_aty) meta | AIgnoredSharedLoan child_av -> sanity_check __FILE__ __LINE__ @@ -664,19 +682,24 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - sanity_check __FILE__ __LINE__ (ty_has_regions_in_set abs.regions sv.sv_ty) meta + sanity_check __FILE__ __LINE__ + (ty_has_regions_in_set abs.regions sv.sv_ty) + meta | AProjBorrows (sv, proj_ty) -> let ty2 = Substitute.erase_regions sv.sv_ty in sanity_check __FILE__ __LINE__ (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - sanity_check __FILE__ __LINE__ (ty_has_regions_in_set abs.regions proj_ty) meta + sanity_check __FILE__ __LINE__ + (ty_has_regions_in_set abs.regions proj_ty) + meta | AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with - | AProjBorrows (_sv, ty') -> sanity_check __FILE__ __LINE__ (ty' = ty) meta + | AProjBorrows (_sv, ty') -> + sanity_check __FILE__ __LINE__ (ty' = ty) meta | AEndedProjBorrows _ | AIgnoredProjBorrows -> () | _ -> craise __FILE__ __LINE__ meta "Unexpected") given_back_ls @@ -796,7 +819,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = *) (* A symbolic value can't be both in the regular environment and inside * projectors of borrows in abstractions *) - sanity_check __FILE__ __LINE__ (info.env_count = 0 || info.aproj_borrows = []) meta; + sanity_check __FILE__ __LINE__ + (info.env_count = 0 || info.aproj_borrows = []) + meta; (* A symbolic value containing borrows can't be duplicated (i.e., copied): * it must be expanded first *) if ty_has_borrows ctx.type_ctx.type_infos info.ty then @@ -806,7 +831,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta; - sanity_check __FILE__ __LINE__ (info.aproj_borrows = [] || info.aproj_loans <> []) meta; + sanity_check __FILE__ __LINE__ + (info.aproj_borrows = [] || info.aproj_loans <> []) + meta; (* At the same time: * - check that the loans don't intersect * - compute the set of regions for which we project loans @@ -818,7 +845,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = let regions = RegionId.Set.fold (fun rid regions -> - sanity_check __FILE__ __LINE__ (not (RegionId.Set.mem rid regions)) meta; + sanity_check __FILE__ __LINE__ + (not (RegionId.Set.mem rid regions)) + meta; RegionId.Set.add rid regions) regions linfo.regions in diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 5e0aa289..11cd89fc 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -238,7 +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__ (statement_has_no_loop_break_continue st2) st2.meta; + sanity_check __FILE__ __LINE__ + (statement_has_no_loop_break_continue st2) + st2.meta; (replace_breaks_with st1 st2).content | _ -> super#visit_Sequence env st1 st2 end diff --git a/compiler/Print.ml b/compiler/Print.ml index a136f87e..dad1aea3 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -87,7 +87,8 @@ module Values = struct | _ -> craise_opt_meta __FILE__ __LINE__ meta ("Inconsistent value: " ^ show_typed_value v)) - | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent typed value") + | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent typed value" + ) | VBottom -> "⊥ : " ^ ty_to_string env v.ty | VBorrow bc -> borrow_content_to_string ~meta env bc | VLoan lc -> loan_content_to_string ~meta env lc @@ -184,7 +185,8 @@ module Values = struct match (aty, field_values) with | TBox, [ bv ] -> "@Box(" ^ bv ^ ")" | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent value") - | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent typed value") + | _ -> craise_opt_meta __FILE__ __LINE__ meta "Inconsistent typed value" + ) | ABottom -> "⊥ : " ^ ty_to_string env v.ty | ABorrow bc -> aborrow_content_to_string ~meta env bc | ALoan lc -> aloan_content_to_string ~meta env lc @@ -343,7 +345,8 @@ module Contexts = struct in indent ^ bv ^ ty ^ " -> " ^ typed_value_to_string ~meta env tv ^ " ;" | EAbs abs -> abs_to_string ~meta env verbose indent indent_incr abs - | EFrame -> craise_opt_meta __FILE__ __LINE__ meta "Can't print a Frame element" + | EFrame -> + craise_opt_meta __FILE__ __LINE__ meta "Can't print a Frame element" let opt_env_elem_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (verbose : bool) (with_var_types : bool) (indent : string) diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index a1b19ea3..518d8bdd 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -397,16 +397,21 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) if variant_id = result_return_id then match field_values with | [ v ] -> "@Result::Return " ^ v - | _ -> craise_opt_meta __FILE__ __LINE__ meta "Result::Return takes exactly one value" + | _ -> + craise_opt_meta __FILE__ __LINE__ meta + "Result::Return takes exactly one value" else if variant_id = result_fail_id then match field_values with | [ v ] -> "@Result::Fail " ^ v - | _ -> craise_opt_meta __FILE__ __LINE__ meta "Result::Fail takes exactly one value" + | _ -> + craise_opt_meta __FILE__ __LINE__ meta + "Result::Fail takes exactly one value" else craise_opt_meta __FILE__ __LINE__ meta "Unreachable: improper variant id for result type" | TError -> - cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta "TODO: error message"; + cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta + "TODO: error message"; let variant_id = Option.get variant_id in if variant_id = error_failure_id then "@Error::Failure" else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel" @@ -416,17 +421,21 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) | TFuel -> let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then ( - cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta "TODO: error message"; + cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta + "TODO: error message"; "@Fuel::Zero") else if variant_id = fuel_succ_id then match field_values with | [ v ] -> "@Fuel::Succ " ^ v - | _ -> craise_opt_meta __FILE__ __LINE__ meta "@Fuel::Succ takes exactly one value" + | _ -> + craise_opt_meta __FILE__ __LINE__ meta + "@Fuel::Succ takes exactly one value" else craise_opt_meta __FILE__ __LINE__ meta "Unreachable: improper variant id for fuel type" | TArray | TSlice | TStr -> - cassert_opt_meta __FILE__ __LINE__ (variant_id = None) meta "TODO: error message"; + cassert_opt_meta __FILE__ __LINE__ (variant_id = None) meta + "TODO: error message"; let field_values = List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values in diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 95c74a7b..91ee16dc 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -222,7 +222,9 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* Register a variable for constraints propagation - used when an variable is * introduced (left-hand side of a left binding) *) let register_var (ctx : pn_ctx) (v : var) : pn_ctx = - sanity_check __FILE__ __LINE__ (not (VarId.Map.mem v.id ctx.pure_vars)) def.meta; + sanity_check __FILE__ __LINE__ + (not (VarId.Map.mem v.id ctx.pure_vars)) + def.meta; match v.basename with | None -> ctx | Some name -> @@ -1198,7 +1200,8 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = in let fields = match adt_decl.kind with - | Enum _ | Opaque -> craise __FILE__ __LINE__ def.meta "Unreachable" + | Enum _ | Opaque -> + craise __FILE__ __LINE__ def.meta "Unreachable" | Struct fields -> fields in let num_fields = List.length fields in diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index 9e144c50..53ff8983 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -34,7 +34,9 @@ let get_adt_field_types (meta : Meta.meta) let variant_id = Option.get variant_id in if variant_id = result_return_id then [ ty ] else if variant_id = result_fail_id then [ mk_error_ty ] - else craise __FILE__ __LINE__ meta "Unreachable: improper variant id for result type" + else + craise __FILE__ __LINE__ meta + "Unreachable: improper variant id for result type" | TError -> sanity_check __FILE__ __LINE__ (generics = empty_generic_args) meta; let variant_id = Option.get variant_id in @@ -46,11 +48,14 @@ let get_adt_field_types (meta : Meta.meta) let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then [] else if variant_id = fuel_succ_id then [ mk_fuel_ty ] - else craise __FILE__ __LINE__ meta "Unreachable: improper variant id for fuel type" + else + craise __FILE__ __LINE__ meta + "Unreachable: improper variant id for fuel type" | TArray | TSlice | TStr | TRawPtr _ -> (* Array: when not symbolic values (for instance, because of aggregates), the array expressions are introduced as struct updates *) - craise __FILE__ __LINE__ meta "Attempting to access the fields of an opaque type") + craise __FILE__ __LINE__ meta + "Attempting to access the fields of an opaque type") type tc_ctx = { type_decls : type_decl TypeDeclId.Map.t; (** The type declarations *) @@ -64,7 +69,8 @@ type tc_ctx = { let check_literal (meta : Meta.meta) (v : literal) (ty : literal_type) : unit = match (ty, v) with - | TInteger int_ty, VScalar sv -> sanity_check __FILE__ __LINE__ (int_ty = sv.int_ty) meta + | TInteger int_ty, VScalar sv -> + sanity_check __FILE__ __LINE__ (int_ty = sv.int_ty) meta | TBool, VBool _ | TChar, VChar _ -> () | _ -> craise __FILE__ __LINE__ meta "Inconsistent type" diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 215bebe3..c3afe1c4 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -433,11 +433,14 @@ let mk_switch (meta : Meta.meta) (scrut : texpression) (sb : switch_body) : | If (_, _) -> sanity_check __FILE__ __LINE__ (scrut.ty = TLiteral TBool) meta | Match branches -> List.iter - (fun (b : match_branch) -> sanity_check __FILE__ __LINE__ (b.pat.ty = scrut.ty) meta) + (fun (b : match_branch) -> + sanity_check __FILE__ __LINE__ (b.pat.ty = scrut.ty) meta) branches); (* Sanity check: all the branches have the same type *) let ty = get_switch_body_ty sb in - iter_switch_body_branches (fun e -> sanity_check __FILE__ __LINE__ (e.ty = ty) meta) sb; + iter_switch_body_branches + (fun e -> sanity_check __FILE__ __LINE__ (e.ty = ty) meta) + sb; (* Put together *) let e = Switch (scrut, sb) in { e; ty } @@ -529,7 +532,9 @@ let ty_as_integer (meta : Meta.meta) (t : ty) : T.integer_type = | _ -> craise __FILE__ __LINE__ meta "Unreachable" let ty_as_literal (meta : Meta.meta) (t : ty) : T.literal_type = - match t with TLiteral ty -> ty | _ -> craise __FILE__ __LINE__ meta "Unreachable" + match t with + | TLiteral ty -> ty + | _ -> craise __FILE__ __LINE__ meta "Unreachable" let mk_state_ty : ty = TAdt (TAssumed TState, empty_generic_args) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 031c29f7..aeb03c34 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -445,7 +445,8 @@ and translate_trait_instance_id (meta : Meta.meta) (translate_ty : T.ty -> ty) let inst_id = translate_trait_instance_id inst_id in ItemClause (inst_id, decl_id, item_name, clause_id) | TraitRef tr -> TraitRef (translate_trait_ref meta translate_ty tr) - | FnPointer _ | Closure _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" + | FnPointer _ | Closure _ -> + craise __FILE__ __LINE__ meta "Closures are not supported yet" | UnknownTrait s -> craise __FILE__ __LINE__ meta ("Unknown trait found: " ^ s) (** Translate a signature type - TODO: factor out the different translation functions *) @@ -457,7 +458,9 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty = match type_id with | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics) | T.TTuple -> - cassert __FILE__ __LINE__ (generics.const_generics = []) meta "TODO: error message"; + cassert __FILE__ __LINE__ + (generics.const_generics = []) + meta "TODO: error message"; mk_simpl_tuple_ty generics.types | T.TAssumed aty -> ( match aty with @@ -817,7 +820,9 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) (back_funs : texpression option RegionGroupId.Map.t option) (ctx : bs_ctx) : bs_ctx = let calls = ctx.calls in - sanity_check __FILE__ __LINE__ (not (V.FunCallId.Map.mem call_id calls)) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ + (not (V.FunCallId.Map.mem call_id calls)) + ctx.fun_decl.meta; let info = { forward; forward_inputs = args; back_funs } in let calls = V.FunCallId.Map.add call_id info calls in { ctx with calls } @@ -953,7 +958,9 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) (* This is necessarily for the current function *) match fun_id with | FunId (FRegular fid) -> ( - sanity_check __FILE__ __LINE__ (fid = ctx.fun_decl.def_id) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ + (fid = ctx.fun_decl.def_id) + ctx.fun_decl.meta; (* Lookup the loop *) let lid = V.LoopId.Map.find lid ctx.loop_ids_map in let loop_info = LoopId.Map.find lid ctx.loops in @@ -1591,7 +1598,8 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) | VLoan lc -> ( match lc with | VSharedLoan (_, v) -> translate v - | VMutLoan _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable") + | VMutLoan _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + ) | VBorrow bc -> ( match bc with | VSharedBorrow bid -> @@ -1726,7 +1734,9 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = (* The symbolic value was left unchanged *) Some (symbolic_value_to_texpression ctx msv) | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) -> - sanity_check __FILE__ __LINE__ (child_aproj = AIgnoredProjBorrows) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ + (child_aproj = AIgnoredProjBorrows) + ctx.fun_decl.meta; (* The symbolic value was updated *) Some (symbolic_value_to_texpression ctx mnv) | V.AEndedProjLoans (_, _) -> @@ -2087,9 +2097,13 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) (ctx : bs_ctx) : texpression = - sanity_check __FILE__ __LINE__ (is_continue = ctx.inside_loop) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ + (is_continue = ctx.inside_loop) + ctx.fun_decl.meta; let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in - sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ + (loop_id = Option.get ctx.loop_id) + ctx.fun_decl.meta; (* Lookup the loop information *) let loop_id = Option.get ctx.loop_id in @@ -2350,7 +2364,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest) - | CastFnPtr _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "TODO: function casts") + | CastFnPtr _ -> + craise __FILE__ __LINE__ ctx.fun_decl.meta "TODO: function casts") | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> @@ -2359,7 +2374,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (match binop with (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *) | E.Shl | E.Shr -> () - | _ -> sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1) ctx.fun_decl.meta); + | _ -> + sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1) + ctx.fun_decl.meta); let effect_info = { can_fail = ExpressionsUtils.binop_can_fail binop; @@ -2477,7 +2494,9 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) if !Config.type_check_pure_code then List.iter (fun (var, v) -> - sanity_check __FILE__ __LINE__ ((var : var).ty = (v : texpression).ty) ctx.fun_decl.meta) + sanity_check __FILE__ __LINE__ + ((var : var).ty = (v : texpression).ty) + ctx.fun_decl.meta) variables_values; (* Translate the next expression *) let next_e = translate_expression e ctx in @@ -2633,7 +2652,8 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) ^ pure_ty_to_string ctx given_back.ty ^ "\n- sig input ty: " ^ pure_ty_to_string ctx input.ty)); - sanity_check __FILE__ __LINE__ (given_back.ty = input.ty) ctx.fun_decl.meta) + sanity_check __FILE__ __LINE__ (given_back.ty = input.ty) + ctx.fun_decl.meta) given_back_inputs; (* Translate the next expression *) let next_e = translate_expression e ctx in @@ -2650,7 +2670,9 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) texpression = let vloop_id = loop_id in let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in - sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ + (loop_id = Option.get ctx.loop_id) + ctx.fun_decl.meta; let rg_id = Option.get rg_id in (* There are two cases depending on the [abs_kind] (whether this is a synth input or a regular loop call) *) @@ -3015,7 +3037,8 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) * through the functions provided by the API (note that we don't * know how to expand values like vectors or arrays, because they have a variable number * of fields!) *) - craise __FILE__ __LINE__ ctx.fun_decl.meta "Attempt to expand a non-expandable value" + craise __FILE__ __LINE__ ctx.fun_decl.meta + "Attempt to expand a non-expandable value" and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression) @@ -3542,7 +3565,9 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* Add the loop information in the context *) let ctx = - sanity_check __FILE__ __LINE__ (not (LoopId.Map.mem loop_id ctx.loops)) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ + (not (LoopId.Map.mem loop_id ctx.loops)) + ctx.fun_decl.meta; (* Note that we will retrieve the input values later in the [ForwardEnd] (and will introduce the outputs at that moment, together with the actual diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 74b333f3..576b2809 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -70,7 +70,9 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) VariantId.id option * symbolic_value list = match see with | Some (SeAdt (vid, fields)) -> (vid, fields) - | _ -> craise __FILE__ __LINE__ meta "Ill-formed branching ADT expansion" + | _ -> + craise __FILE__ __LINE__ meta + "Ill-formed branching ADT expansion" in let exp = List.map diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml index 980ebef7..91010e07 100644 --- a/compiler/ValuesUtils.ml +++ b/compiler/ValuesUtils.ml @@ -33,7 +33,9 @@ let mk_aignored (meta : Meta.meta) (ty : ty) : typed_avalue = { value = AIgnored; ty } let value_as_symbolic (meta : Meta.meta) (v : value) : symbolic_value = - match v with VSymbolic v -> v | _ -> craise __FILE__ __LINE__ meta "Unexpected" + match v with + | VSymbolic v -> v + | _ -> craise __FILE__ __LINE__ meta "Unexpected" (** Box a value *) let mk_box_value (meta : Meta.meta) (v : typed_value) : typed_value = @@ -50,7 +52,9 @@ let is_symbolic (v : value) : bool = match v with VSymbolic _ -> true | _ -> false let as_symbolic (meta : Meta.meta) (v : value) : symbolic_value = - match v with VSymbolic s -> s | _ -> craise __FILE__ __LINE__ meta "Unexpected" + match v with + | VSymbolic s -> s + | _ -> craise __FILE__ __LINE__ meta "Unexpected" let as_mut_borrow (meta : Meta.meta) (v : typed_value) : BorrowId.id * typed_value = |