diff --git a/Makefile b/Makefile index 6e8be921..5d061025 100644 --- a/Makefile +++ b/Makefile @@ -156,6 +156,8 @@ INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) INPUTS_LIST := $(filter-out %.out,$(INPUTS_LIST)) # Remove some temporary files which are inserted by, for instance, Emacs INPUTS_LIST := $(filter-out %~,$(INPUTS_LIST)) +INPUTS_LIST := $(filter-out .%,$(INPUTS_LIST)) +INPUTS_LIST := $(filter-out #%,$(INPUTS_LIST)) # Remove the directory prefix, replace with `test-` INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) diff --git a/charon-pin b/charon-pin index 03e7a85d..9c89ba41 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -f54e30a484a373514df354cfe3fd1ba238bdee6b +3402870cbf5b49d92fd18c312831ef30a14e6a5b diff --git a/flake.lock b/flake.lock index feb1476d..b1a41158 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1732629844, - "narHash": "sha256-OnDEQUoR9/XYXiyBKFMop1/nBaTtbFYSJY3iMQdE9JE=", + "lastModified": 1732661109, + "narHash": "sha256-JNcosq05JwRUnGb/ibthiUT8BHAJSmDtFJyKV7fwIjM=", "owner": "aeneasverif", "repo": "charon", - "rev": "f54e30a484a373514df354cfe3fd1ba238bdee6b", + "rev": "3402870cbf5b49d92fd18c312831ef30a14e6a5b", "type": "github" }, "original": { diff --git a/src/Config.ml b/src/Config.ml index 2a32af67..a4784d67 100644 --- a/src/Config.ml +++ b/src/Config.ml @@ -335,6 +335,9 @@ let type_check_pure_code = ref false as far as possible while leaving "holes" in the generated code? *) let fail_hard = ref false +(** Shall we emit errors instead of warnings? *) +let warnings_as_errors = ref true + (** If true, add the type name as a prefix to the variant names. Ex.: diff --git a/src/Errors.ml b/src/Errors.ml index c92c3db8..e66876c0 100644 --- a/src/Errors.ml +++ b/src/Errors.ml @@ -49,7 +49,7 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option) if !Config.fail_hard then ( let msg = format_error_message_with_file_line file line span msg in log#serror (msg ^ "\n"); - raise (Failure (format_error_message_with_file_line file line span msg))) + raise (Failure msg)) else let () = push_error span msg in raise (CFailure (span, msg)) @@ -74,5 +74,22 @@ let sanity_check_opt_span (file : string) (line : int) b span = let internal_error (file : string) (line : int) span = craise file line span "Internal error, please file an issue" +let warn_opt_span (file : string) (line : int) (span : Meta.span option) + (msg : string) = + if !Config.warnings_as_errors then + craise_opt_span file line span + (msg ^ "\nYou can deactivate this error with the option -soft-warnings") + else + let msg = format_error_message_with_file_line file line span msg in + log#swarning (msg ^ "\n") + +let cassert_warn_opt_span (file : string) (line : int) (b : bool) + (span : Meta.span option) (msg : string) = + if not b then warn_opt_span file line span msg + +let cassert_warn (file : string) (line : int) (b : bool) (span : Meta.span) + (msg : string) = + if not b then warn_opt_span file line (Some span) msg + let exec_raise = craise let exec_assert = cassert diff --git a/src/Main.ml b/src/Main.ml index 10c7e0d3..106ca4bc 100644 --- a/src/Main.ml +++ b/src/Main.ml @@ -122,6 +122,9 @@ let () = ( "-abort-on-error", Arg.Set fail_hard, " Abort on the first encountered error" ); + ( "-soft-warnings", + Arg.Clear warnings_as_errors, + " Do not treat warnings as errors" ); ( "-tuple-nested-proj", Arg.Set use_nested_tuple_projectors, " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \ diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index cb763581..007276fa 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -646,6 +646,11 @@ and extract_adt_cons (span : Meta.span) (ctx : extraction_ctx) (generics : generic_args) (args : texpression list) : unit = let e_ty = TAdt (adt_cons.adt_id, generics) in let is_single_pat = false in + (* Sanity check: make sure the expression is not a tuple constructor + with no arguments (the properly extracted expression would be a function) *) + cassert __FILE__ __LINE__ + (not (adt_cons.adt_id = TTuple && generics.types != [] && args = [])) + span "Unreachable"; let _ = extract_adt_g_value span (fun ctx inside e -> diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml index c37675c6..6fc0d3a1 100644 --- a/src/interp/Interpreter.ml +++ b/src/interp/Interpreter.ml @@ -49,9 +49,13 @@ let compute_contexts (m : crate) : decls_ctx = *) let normalize_inst_fun_sig (span : Meta.span) (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig = - let { regions_hierarchy = _; trait_type_constraints = _; inputs; output } = - sg - in + let { regions_hierarchy = _; trait_type_constraints; inputs; output } = sg in + cassert_warn __FILE__ __LINE__ + (trait_type_constraints = []) + span + "Detected type constraints over associated traits (of the shape: `where \ + Foo::T = U`). We do not handle this properly yet: the translation may be \ + incorrect, and the generated output will likely not typecheck."; let norm = AssociatedTypes.ctx_normalize_ty (Some span) ctx in let inputs = List.map norm inputs in let output = norm output in @@ -199,17 +203,14 @@ 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. *) + let span = fdef.item_meta.span in + (* Sanity check: no nested borrows *) cassert __FILE__ __LINE__ (List.for_all - (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) + (fun ty -> + not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty)) (sg.output :: sg.inputs)) - fdef.item_meta.span "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.item_meta.span "ADTs containing borrows are not supported yet"; + span "Nested borrows are not supported yet"; (* Create the context *) let regions_hierarchy = @@ -219,25 +220,23 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : List.map (fun (g : region_var_group) -> g.id) regions_hierarchy in let ctx = - initialize_eval_ctx (Some fdef.item_meta.span) ctx region_groups - sg.generics.types sg.generics.const_generics + initialize_eval_ctx (Some span) ctx region_groups sg.generics.types + sg.generics.const_generics in (* Instantiate the signature. This updates the context because we compute at the same time the normalization map for the associated types. *) let ctx, inst_sg = - symbolic_instantiate_fun_sig fdef.item_meta.span ctx fdef.signature - regions_hierarchy fdef.kind + symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy + fdef.kind in (* Create fresh symbolic values for the inputs *) let input_svs = - List.map - (fun ty -> mk_fresh_symbolic_value fdef.item_meta.span ty) - inst_sg.inputs + List.map (fun ty -> mk_fresh_symbolic_value span ty) inst_sg.inputs in (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) let call_id = fresh_fun_call_id () in - sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.item_meta.span; + sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) span; let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : eval_ctx * typed_avalue list = (* Project over the values - we use *loan* projectors, as explained above *) @@ -259,14 +258,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : Collections.List.split_at (List.tl body.locals.vars) body.locals.arg_count in (* Push the return variable (initialized with ⊥) *) - let ctx = ctx_push_uninitialized_var fdef.item_meta.span ctx ret_var in + let ctx = ctx_push_uninitialized_var span ctx ret_var in (* Push the input variables (initialized with symbolic values) *) let input_values = List.map mk_typed_value_from_symbolic_value input_svs in - let ctx = - ctx_push_vars fdef.item_meta.span ctx (List.combine input_vars input_values) - in + let ctx = ctx_push_vars span ctx (List.combine input_vars input_values) in (* Push the remaining local variables (initialized with ⊥) *) - let ctx = ctx_push_uninitialized_vars fdef.item_meta.span ctx local_vars in + let ctx = ctx_push_uninitialized_vars span ctx local_vars in (* Return *) (ctx, input_svs, inst_sg) @@ -286,6 +283,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) (fdef : fun_decl) (inst_sg : inst_fun_sig) (back_id : RegionGroupId.id) (loop_id : LoopId.id option) (is_regular_return : bool) (inside_loop : bool) (ctx : eval_ctx) : SA.expression = + let span = fdef.item_meta.span in log#ldebug (lazy ("evaluate_function_symbolic_synthesize_backward_from_return:" @@ -300,7 +298,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) ^ "\n- inside_loop: " ^ Print.bool_to_string inside_loop ^ "\n- ctx:\n" - ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx)); + ^ Print.Contexts.eval_ctx_to_string ~span:(Some span) ctx)); (* We need to instantiate the function signature - to retrieve * the return type. Note that it is important to re-generate * an instantiation of the signature, so that we use fresh @@ -309,15 +307,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies in let _, ret_inst_sg = - symbolic_instantiate_fun_sig fdef.item_meta.span ctx fdef.signature - regions_hierarchy fdef.kind + symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy + fdef.kind in let ret_rty = ret_inst_sg.output in (* Move the return value out of the return variable *) let pop_return_value = is_regular_return in - let ret_value, ctx, cc = - pop_frame config fdef.item_meta.span pop_return_value ctx - in + let ret_value, ctx, cc = pop_frame config span pop_return_value ctx in (* We need to find the parents regions/abstractions of the region we * will end - this will allow us to, first, mark the other return @@ -344,8 +340,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : eval_ctx * typed_avalue list = let ctx, avalue = - apply_proj_borrows_on_input_value config fdef.item_meta.span ctx - abs.regions abs.ancestors_regions ret_value ret_rty + apply_proj_borrows_on_input_value config span ctx abs.regions + abs.ancestors_regions ret_value ret_rty in (ctx, [ avalue ]) in @@ -360,8 +356,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let region_can_end rid = RegionGroupId.Set.mem rid parent_and_current_rgs in - sanity_check __FILE__ __LINE__ (region_can_end back_id) - fdef.item_meta.span; + sanity_check __FILE__ __LINE__ (region_can_end back_id) span; let ctx = create_push_abstractions_from_abs_region_groups (fun rg_id -> SynthRet rg_id) @@ -374,7 +369,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) (lazy ("evaluate_function_symbolic_synthesize_backward_from_return: (after \ putting the return value in the proper abstraction)\n" ^ "\n- ctx:\n" - ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx)); + ^ Print.Contexts.eval_ctx_to_string ~span:(Some span) ctx)); (* We now need to end the proper *input* abstractions - pay attention * to the fact that we end the *input* abstractions, not the *return* @@ -477,7 +472,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) sanity_check __FILE__ __LINE__ (if Option.is_some loop_id then loop_id = Some loop_id' else true) - fdef.item_meta.span; + span; (* Loop abstractions *) let rg_id' = Option.get rg_id' in if rg_id' = back_id && inside_loop then @@ -485,8 +480,7 @@ 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.item_meta.span; + sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') span; { abs with can_end = true } | SynthInput rg_id' -> if rg_id' = back_id && end_fun_synth_input then @@ -509,7 +503,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let ctx, cc = comp cc (fold_left_apply_continuation - (fun id ctx -> end_abstraction config fdef.item_meta.span id ctx) + (fun id ctx -> end_abstraction config span id ctx) target_abs_ids ctx) in (* Generate the Return node *) @@ -535,6 +529,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (fdef : fun_decl) : symbolic_value list * SA.expression option = (* Debug *) + let span = fdef.item_meta.span in let name_to_string () = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) @@ -576,7 +571,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Pop the frame and retrieve the returned value at the same time *) let pop_return_value = true in let ret_value, ctx, cc_pop = - pop_frame config fdef.item_meta.span pop_return_value ctx + pop_frame config span pop_return_value ctx in (* Generate the Return node *) cc_pop (SA.Return (ctx, ret_value)) @@ -589,7 +584,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) match res with | Return -> None | LoopReturn loop_id -> Some loop_id - | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable" + | _ -> craise __FILE__ __LINE__ span "Unreachable" in let is_regular_return = true in let inside_loop = Option.is_some loop_id in @@ -612,7 +607,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) match res with | EndEnterLoop _ -> false | EndContinue _ -> true - | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable" + | _ -> craise __FILE__ __LINE__ span "Unreachable" in (* Forward translation *) let fwd_e = @@ -620,7 +615,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) translation we will simply call the loop function *) let pop_return_value = false in let _ret_value, _ctx, cc_pop = - pop_frame config fdef.item_meta.span pop_return_value ctx + pop_frame config span pop_return_value ctx in (* Generate the Return node *) cc_pop (SA.ReturnWithLoop (loop_id, inside_loop)) @@ -647,7 +642,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) * the executions can lead to a panic *) SA.Panic | Unit | Break _ | Continue _ -> - craise __FILE__ __LINE__ fdef.item_meta.span + craise __FILE__ __LINE__ span ("evaluate_function_symbolic failed on: " ^ name_to_string ()) in @@ -675,6 +670,7 @@ module Test = struct (* Retrieve the function declaration *) let fdef = FunDeclId.Map.find fid crate.fun_decls in let body = Option.get fdef.body in + let span = fdef.item_meta.span in (* Debug *) log#ldebug @@ -687,20 +683,14 @@ module Test = struct (* Sanity check - *) sanity_check __FILE__ __LINE__ (fdef.signature.generics = empty_generic_params) - fdef.item_meta.span; - sanity_check __FILE__ __LINE__ - (body.locals.arg_count = 0) - fdef.item_meta.span; + span; + sanity_check __FILE__ __LINE__ (body.locals.arg_count = 0) span; (* Create the evaluation context *) - let ctx = - initialize_eval_ctx (Some fdef.item_meta.span) decls_ctx [] [] [] - in + let ctx = initialize_eval_ctx (Some span) decls_ctx [] [] [] in (* Insert the (uninitialized) local variables *) - let ctx = - ctx_push_uninitialized_vars fdef.item_meta.span ctx body.locals.vars - in + let ctx = ctx_push_uninitialized_vars span ctx body.locals.vars in (* Create the continuation to check the function's result *) let config = mk_config ConcreteMode in @@ -709,9 +699,9 @@ module Test = struct | Return -> (* Ok: drop the local variables and finish *) let pop_return_value = true in - pop_frame config fdef.item_meta.span pop_return_value ctx + pop_frame config span pop_return_value ctx | _ -> - craise __FILE__ __LINE__ fdef.item_meta.span + craise __FILE__ __LINE__ span ("Unit test failed (concrete execution) on: " ^ Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env decls_ctx) diff --git a/src/interp/InterpreterBorrows.ml b/src/interp/InterpreterBorrows.ml index 09debfcf..3b0e6fa4 100644 --- a/src/interp/InterpreterBorrows.ml +++ b/src/interp/InterpreterBorrows.ml @@ -148,12 +148,12 @@ let end_borrow_get_borrow (span : Meta.span) let av = super#visit_typed_avalue outer av in (* Reconstruct *) ALoan (ASharedLoan (pm, bids, v, av)) - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | AEndedSharedLoan _ (* The loan has ended, so no need to update the outer borrows *) | AIgnoredMutLoan _ (* Nothing special to do *) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } (* Nothing special to do *) | AIgnoredSharedLoan _ -> (* Nothing special to do *) @@ -207,7 +207,7 @@ let end_borrow_get_borrow (span : Meta.span) | AIgnoredMutBorrow (_, _) | AEndedMutBorrow _ | AEndedIgnoredMutBorrow - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } | AEndedSharedBorrow -> (* Nothing special to do *) super#visit_ABorrow outer bc @@ -345,7 +345,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) (* Remember the given back value as a meta-value * TODO: it is a bit annoying to have to deconstruct * the value... Think about a more elegant way. *) - let given_back_span = as_symbolic span nv.value in + let given_back_meta = as_symbolic span nv.value in (* The loan projector *) let given_back = mk_aproj_loans_value_from_symbolic_value abs.regions sv @@ -355,7 +355,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) (* Return *) ABorrow (AEndedIgnoredMutBorrow - { given_back; child; given_back_span }) + { given_back; child; given_back_meta }) | _ -> craise __FILE__ __LINE__ span "Unreachable" else (* Continue exploring *) @@ -390,7 +390,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) (* Register the insertion *) set_replaced (); (* Remember the given back value as a meta-value *) - let given_back_span = nv in + let given_back_meta = nv in (* Apply the projection *) let given_back = apply_proj_borrows span check_symbolic_no_ended ctx @@ -399,14 +399,14 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in (* Return the new value *) - ALoan (AEndedMutLoan { child; given_back; given_back_span })) + ALoan (AEndedMutLoan { child; given_back; given_back_meta })) else (* Continue exploring *) super#visit_ALoan opt_abs lc | ASharedLoan (pm, _, _, _) -> sanity_check __FILE__ __LINE__ (pm = PNone) span; (* We are giving back a value to a *mutable* loan: nothing special to do *) super#visit_ALoan opt_abs lc - | AEndedMutLoan { child = _; given_back = _; given_back_span = _ } + | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ } | AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -415,7 +415,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) * of the value which is given back *) if opt_bid = Some bid then (* Remember the given back value as a meta-value *) - let given_back_span = nv in + let given_back_meta = nv in (* Note that we replace the ignored mut loan by an *ended* ignored * mut loan. Also, this is not the loan we are looking for *per se*: * we don't register the fact that we inserted the value somewhere @@ -427,10 +427,10 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in ALoan - (AEndedIgnoredMutLoan { given_back; child; given_back_span }) + (AEndedIgnoredMutLoan { given_back; child; given_back_meta }) else super#visit_ALoan opt_abs lc | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } | AIgnoredSharedLoan _ -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -557,12 +557,12 @@ let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span) set_replaced (); (* Return the new value *) ALoan - (AEndedMutLoan { given_back = nv; child; given_back_span = nsv })) + (AEndedMutLoan { given_back = nv; child; given_back_meta = nsv })) else (* Continue exploring *) super#visit_ALoan opt_abs lc | ASharedLoan (PNone, _, _, _) (* We are giving back a value to a *mutable* loan: nothing special to do *) - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -581,10 +581,10 @@ let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span) sanity_check __FILE__ __LINE__ (nv.ty = ty) span; ALoan (AEndedIgnoredMutLoan - { given_back = nv; child; given_back_span = nsv })) + { given_back = nv; child; given_back_meta = nsv })) else super#visit_ALoan opt_abs lc | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } | AIgnoredSharedLoan _ -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -662,14 +662,14 @@ let give_back_shared _config (span : Meta.span) (bid : BorrowId.id) else (* Not the loan we are looking for: continue exploring *) super#visit_ALoan opt_abs lc - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } (* Nothing special to do (the loan has ended) *) | AEndedSharedLoan (_, _) (* Nothing special to do (the loan has ended) *) | AIgnoredMutLoan (_, _) (* Nothing special to do (we are giving back a *shared* borrow) *) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } (* Nothing special to do *) | AIgnoredSharedLoan _ -> (* Nothing special to do *) @@ -1654,7 +1654,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (av : typed_avalue) : unit = let ty = av.ty in match av.value with - | ABottom | AIgnored -> () + | ABottom | AIgnored _ -> () | AAdt adt -> (* Simply explore the children *) List.iter (list_avalues allow_borrows push) adt.field_values @@ -1664,14 +1664,14 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) | ASharedLoan (pm, bids, sv, child_av) -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ - (not (value_has_borrows ctx sv.value)) + (not (value_has_borrows (Some span) ctx sv.value)) span "Nested borrows are not supported yet"; (* Destructure the shared value *) let avl, sv = if destructure_shared_values then list_values sv else ([], sv) in (* Push a value *) - let ignored = mk_aignored span child_av.ty in + let ignored = mk_aignored span child_av.ty None in let value = ALoan (ASharedLoan (pm, bids, sv, ignored)) in push { value; ty }; (* Explore the child *) @@ -1687,26 +1687,28 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (* Explore the child *) list_avalues false push_fail child_av; (* Explore the whole loan *) - let ignored = mk_aignored span child_av.ty in + let ignored = mk_aignored span child_av.ty None in let value = ALoan (AMutLoan (pm, bid, ignored)) in push { value; ty } | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ - (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) + (not + (ty_has_borrows (Some span) ctx.type_ctx.type_infos child_av.ty)) span "Nested borrows are not supported yet"; sanity_check __FILE__ __LINE__ (opt_bid = None) span; (* Simply explore the child *) list_avalues false push_fail child_av | AEndedMutLoan - { child = child_av; given_back = _; given_back_span = _ } + { child = child_av; given_back = _; given_back_meta = _ } | AEndedSharedLoan (_, child_av) | AEndedIgnoredMutLoan - { child = child_av; given_back = _; given_back_span = _ } + { child = child_av; given_back = _; given_back_meta = _ } | AIgnoredSharedLoan child_av -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ - (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) + (not + (ty_has_borrows (Some span) ctx.type_ctx.type_infos child_av.ty)) span "Nested borrows are not supported yet"; (* Simply explore the child *) list_avalues false push_fail child_av) @@ -1719,7 +1721,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (* Explore the child *) list_avalues false push_fail child_av; (* Explore the borrow *) - let ignored = mk_aignored span child_av.ty in + let ignored = mk_aignored span child_av.ty None in let value = ABorrow (AMutBorrow (pm, bid, ignored)) in push { value; ty } | ASharedBorrow _ -> @@ -1728,16 +1730,18 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) | AIgnoredMutBorrow (opt_bid, child_av) -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ - (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) + (not + (ty_has_borrows (Some span) ctx.type_ctx.type_infos child_av.ty)) span "Nested borrows are not supported yet"; sanity_check __FILE__ __LINE__ (opt_bid = None) span; (* Just explore the child *) list_avalues false push_fail child_av | AEndedIgnoredMutBorrow - { child = child_av; given_back = _; given_back_span = _ } -> + { child = child_av; given_back = _; given_back_meta = _ } -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ - (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) + (not + (ty_has_borrows (Some span) ctx.type_ctx.type_infos child_av.ty)) span "Nested borrows are not supported yet"; (* Just explore the child *) list_avalues false push_fail child_av @@ -1757,7 +1761,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (* 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)) + (not (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty)) span and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in @@ -1784,7 +1788,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) "Nested borrows are not supported yet"; let av : typed_avalue = sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv.value)) + (not (value_has_loans_or_borrows (Some span) ctx sv.value)) span; (* We introduce fresh ids for the symbolic values *) let mk_value_with_fresh_sids (v : typed_value) : typed_value = @@ -1801,7 +1805,8 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) let sv = mk_value_with_fresh_sids sv in (* Create the new avalue *) let value = - ALoan (ASharedLoan (PNone, bids, sv, mk_aignored span ty)) + ALoan + (ASharedLoan (PNone, bids, sv, mk_aignored span ty None)) in (* We need to update the type of the value: abstract shared loans have the type `& ...` - TODO: this is annoying and not very clean... *) @@ -1820,7 +1825,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (* 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)) + (not (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty)) span; ([], v) in @@ -1937,11 +1942,11 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) let r_id = if group then r_id else fresh_region_id () in (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ - (not (value_has_borrows ctx bv.value)) + (not (value_has_borrows (Some span) ctx bv.value)) span "Nested borrows are not supported yet"; (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *) let ty = TRef (RFVar r_id, ref_ty, kind) in - let ignored = mk_aignored span ref_ty in + let ignored = mk_aignored span ref_ty None in let av = ABorrow (AMutBorrow (PNone, bid, ignored)) in let av = { value = av; ty } in (* Continue exploring, looking for loans (and forbidding borrows, @@ -1958,13 +1963,13 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) let r_id = if group then r_id else fresh_region_id () in (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ - (not (value_has_borrows ctx sv.value)) + (not (value_has_borrows (Some span) ctx sv.value)) span "Nested borrows are not supported yet"; (* Push the avalue *) cassert __FILE__ __LINE__ (ty_no_regions ty) span "Nested borrows are not supported yet"; (* We use [AIgnore] for the inner value *) - let ignored = mk_aignored span ty in + let ignored = mk_aignored span ty None in (* For avalues, a loan has the type borrow (see the comments in [avalue]) *) let ty = mk_ref_ty (RFVar r_id) ty RShared in (* Rem.: the shared value might contain loans *) @@ -1987,14 +1992,14 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) let ignored = mk_aignored span ty in (* For avalues, a loan has the type borrow (see the comments in [avalue]) *) let ty = mk_ref_ty (RFVar r_id) ty RMut in - let av = ALoan (AMutLoan (PNone, bid, ignored)) in + let av = ALoan (AMutLoan (PNone, bid, ignored None)) in let av = { value = av; ty } in ([ av ], v)) | VSymbolic _ -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) cassert __FILE__ __LINE__ - (not (value_has_borrows ctx v.value)) + (not (value_has_borrows (Some span) ctx v.value)) span "Nested borrows are not supported yet"; (* Return nothing *) ([], v) @@ -2150,7 +2155,7 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) method! visit_symbolic_value _ sv = (* Sanity check: no borrows *) sanity_check __FILE__ __LINE__ - (not (symbolic_value_has_borrows ctx sv)) + (not (symbolic_value_has_borrows (Some span) ctx sv)) span end in @@ -2251,7 +2256,7 @@ let typed_avalue_split_marker (span : Meta.span) (ctx : eval_ctx) if pm = PNone then [ mk_value PLeft; mk_value PRight ] else [ av ] in match av.value with - | AAdt _ | ABottom | ASymbolic _ | AIgnored -> + | AAdt _ | ABottom | ASymbolic _ | AIgnored _ -> craise __FILE__ __LINE__ span "Unexpected" | ABorrow bc -> ( match bc with @@ -2278,7 +2283,7 @@ let typed_avalue_split_marker (span : Meta.span) (ctx : eval_ctx) | ASharedLoan (pm, bids, sv, child) -> sanity_check __FILE__ __LINE__ (is_aignored child.value) span; sanity_check __FILE__ __LINE__ - (not (value_has_borrows ctx sv.value)) + (not (value_has_borrows (Some span) ctx sv.value)) span; let mk_value pm = { av with value = ALoan (ASharedLoan (pm, bids, sv, child)) } @@ -2546,7 +2551,9 @@ let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span) sanity_check __FILE__ __LINE__ (is_aignored child.value) span; sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv.value)) + (not + (value_has_loans_or_borrows (Some span) ctx + sv.value)) span; let lc = ASharedLoan (pm, bids, sv, child) in set_loans_as_merged pm bids; diff --git a/src/interp/InterpreterBorrowsCore.ml b/src/interp/InterpreterBorrowsCore.ml index b0ace136..4ffa40bf 100644 --- a/src/interp/InterpreterBorrowsCore.ml +++ b/src/interp/InterpreterBorrowsCore.ml @@ -269,11 +269,11 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) if BorrowId.Set.mem l bids then raise (FoundGLoanContent (Abstract lc)) else super#visit_ASharedLoan env pm bids v av - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc method! visit_EBinding env bv v = @@ -411,11 +411,11 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) sanity_check __FILE__ __LINE__ (pm = PNone) span; if BorrowId.Set.mem l bids then update () else super#visit_ASharedLoan env pm bids v av - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc (** Note that once inside the abstractions, we don't control diving @@ -475,7 +475,7 @@ let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind) | AIgnoredMutBorrow (_, _) | AEndedMutBorrow _ | AEndedIgnoredMutBorrow - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } | AEndedSharedBorrow -> super#visit_aborrow_content env bc | AProjSharedBorrow asb -> if borrow_in_asb l asb then @@ -1213,13 +1213,13 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) : (* Sanity check: projection markers can only appear when we're doing a join *) sanity_check __FILE__ __LINE__ (pm = PNone) span; raise (FoundBorrowIds (Borrows bids)) - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | AEndedSharedLoan (_, _) -> super#visit_aloan_content env lc | AIgnoredMutLoan (_, _) -> (* Ignore *) super#visit_aloan_content env lc | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } + { given_back = _; child = _; given_back_meta = _ } | AIgnoredSharedLoan _ -> (* Ignore *) super#visit_aloan_content env lc diff --git a/src/interp/InterpreterExpansion.ml b/src/interp/InterpreterExpansion.ml index afd3235d..3758d342 100644 --- a/src/interp/InterpreterExpansion.ml +++ b/src/interp/InterpreterExpansion.ml @@ -608,7 +608,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : inherit [_] iter_eval_ctx method! visit_VSymbolic _ sv = - if ty_has_borrows ctx.type_ctx.type_infos sv.sv_ty then + if ty_has_borrows (Some span) ctx.type_ctx.type_infos sv.sv_ty then raise (FoundSymbolicValue sv) else () diff --git a/src/interp/InterpreterExpressions.ml b/src/interp/InterpreterExpressions.ml index c744c6b1..c1528741 100644 --- a/src/interp/InterpreterExpressions.ml +++ b/src/interp/InterpreterExpressions.ml @@ -32,7 +32,8 @@ let expand_primitively_copyable_at_place (config : config) (span : Meta.span) fun ctx -> let v = read_place span access p ctx in match - find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v + find_first_primitively_copyable_sv_with_borrows (Some span) + ctx.type_ctx.type_infos v with | None -> (ctx, fun e -> e) | Some sv -> @@ -345,7 +346,7 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span) span "Can not copy a value containing bottom"; sanity_check __FILE__ __LINE__ (Option.is_none - (find_first_primitively_copyable_sv_with_borrows + (find_first_primitively_copyable_sv_with_borrows (Some span) ctx.type_ctx.type_infos v)) span; (* Copy the value *) diff --git a/src/interp/InterpreterLoopsCore.ml b/src/interp/InterpreterLoopsCore.ml index 2502e700..a71cab4f 100644 --- a/src/interp/InterpreterLoopsCore.ml +++ b/src/interp/InterpreterLoopsCore.ml @@ -451,7 +451,7 @@ let typed_avalue_add_marker (span : Meta.span) (ctx : eval_ctx) method! visit_symbolic_value _ sv = sanity_check __FILE__ __LINE__ - (not (symbolic_value_has_borrows ctx sv)) + (not (symbolic_value_has_borrows (Some span) ctx sv)) span; sv diff --git a/src/interp/InterpreterLoopsFixedPoint.ml b/src/interp/InterpreterLoopsFixedPoint.ml index 3b339ef8..d69d10af 100644 --- a/src/interp/InterpreterLoopsFixedPoint.ml +++ b/src/interp/InterpreterLoopsFixedPoint.ml @@ -82,7 +82,8 @@ let rec end_useless_fresh_borrows_and_abs (config : config) (span : Meta.span) (* Explore the fresh anonymous values and replace all the values which are not borrows/loans with ⊥ *) -let cleanup_fresh_values (fixed_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = +let cleanup_fresh_values (span : Meta.span option) (fixed_ids : ids_sets) + (ctx : eval_ctx) : eval_ctx = let rec explore_env (env : env) : env = match env with | [] -> [] (* Done *) @@ -90,7 +91,7 @@ let cleanup_fresh_values (fixed_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = when not (DummyVarId.Set.mem vid fixed_ids.dids) -> let env = explore_env env in (* Eliminate the value altogether if it doesn't contain loans/borrows *) - if not (value_has_loans_or_borrows ctx v.value) then env + if not (value_has_loans_or_borrows span ctx v.value) then env else (* Explore the anonymous value - raises an exception if it finds a borrow to end *) @@ -103,7 +104,7 @@ let cleanup_fresh_values (fixed_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = VBorrow v (* Don't enter inside borrows *) method! visit_value _ v = - if not (value_has_loans_or_borrows ctx v) then VBottom + if not (value_has_loans_or_borrows span ctx v) then VBottom else super#visit_value () v end in @@ -123,7 +124,7 @@ let cleanup_fresh_values_and_abs (config : config) (span : Meta.span) (fixed_ids : ids_sets) : cm_fun = fun ctx -> let ctx, cc = end_useless_fresh_borrows_and_abs config span fixed_ids ctx in - let ctx = cleanup_fresh_values fixed_ids ctx in + let ctx = cleanup_fresh_values (Some span) fixed_ids ctx in (ctx, cc) let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : @@ -226,7 +227,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : (* Create the shared loan child *) let child_rty = rty in - let child_av = mk_aignored span child_rty in + let child_av = mk_aignored span child_rty None in (* Create the shared loan *) let loan_rty = TRef (RFVar nrid, rty, RShared) in @@ -272,7 +273,9 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : let collect_shared_values_in_abs (abs : abs) : unit = let collect_shared_value lids (sv : typed_value) = (* Sanity check: we don't support nested borrows for now *) - sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) span; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows (Some span) ctx sv.value)) + span; (* Filter the loan ids whose corresponding borrows appear in abstractions (see the documentation of the function) *) @@ -307,7 +310,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : *) method! visit_symbolic_value env sv = cassert __FILE__ __LINE__ - (not (symbolic_value_has_borrows ctx sv)) + (not (symbolic_value_has_borrows (Some span) ctx sv)) span "There should be no symbolic values with borrows inside the \ abstraction"; diff --git a/src/interp/InterpreterLoopsJoinCtxs.ml b/src/interp/InterpreterLoopsJoinCtxs.ml index 1ef857ae..7feeb2b8 100644 --- a/src/interp/InterpreterLoopsJoinCtxs.ml +++ b/src/interp/InterpreterLoopsJoinCtxs.ml @@ -580,10 +580,10 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) 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)) + (not (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty0)) span; sanity_check __FILE__ __LINE__ - (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) + (not (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty1)) span in @@ -615,10 +615,10 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) join matcher [JM] to do so. *) sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv0.value)) + (not (value_has_loans_or_borrows (Some span) ctx sv0.value)) span; sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv1.value)) + (not (value_has_loans_or_borrows (Some span) ctx sv1.value)) span; let ty = ty0 in diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml index 9a6d1a81..89ff3ad2 100644 --- a/src/interp/InterpreterLoopsMatchCtxs.ml +++ b/src/interp/InterpreterLoopsMatchCtxs.ml @@ -90,7 +90,7 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (explore : abs -> bool) (* Recurse with the old marker *) self#visit_typed_avalue (abs_id, pm) child | AIgnoredMutLoan (_, child) - | AEndedIgnoredMutLoan { child; given_back = _; given_back_span = _ } + | AEndedIgnoredMutLoan { child; given_back = _; given_back_meta = _ } | AIgnoredSharedLoan child -> sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Ignore the id of the loan, if there is *) @@ -115,7 +115,7 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (explore : abs -> bool) (* Process those normally *) super#visit_aborrow_content (abs_id, pm) bc | AIgnoredMutBorrow (_, child) - | AEndedIgnoredMutBorrow { child; given_back = _; given_back_span = _ } + | AEndedIgnoredMutBorrow { child; given_back = _; given_back_meta = _ } -> sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Ignore the id of the borrow, if there is *) @@ -217,7 +217,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct one of the two contexts (ctx0 here) to call value_has_borrows, it doesn't matter here. *) let value_has_borrows = - ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos + ValuesUtils.value_has_borrows (Some span) ctx0.type_ctx.type_infos in match (v0.value, v1.value) with | VLiteral lv0, VLiteral lv1 -> @@ -256,8 +256,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct cassert __FILE__ __LINE__ (not - (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos - bv.value)) + (ValuesUtils.value_has_borrows (Some span) + ctx0.type_ctx.type_infos bv.value)) M.span "The join of nested borrows is not supported yet"; let bid, bv = M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv @@ -344,7 +344,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct one of the two contexts (ctx0 here) to call value_has_borrows, it doesn't matter here. *) let value_has_borrows = - ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos + ValuesUtils.value_has_borrows (Some span) ctx0.type_ctx.type_infos in let match_rec = match_typed_values ctx0 ctx1 in @@ -364,7 +364,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct else (* Merge *) M.match_distinct_aadts ctx0 ctx1 v0.ty av0 v1.ty av1 ty | ABottom, ABottom -> mk_abottom M.span ty - | AIgnored, AIgnored -> mk_aignored M.span ty + | AIgnored _, AIgnored _ -> mk_aignored M.span ty None | ABorrow bc0, ABorrow bc1 -> ( log#ldebug (lazy "match_typed_avalues: borrows"); match (bc0, bc1) with @@ -469,7 +469,9 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct updates *) let check_no_borrows ctx (v : typed_value) = - sanity_check __FILE__ __LINE__ (not (value_has_borrows ctx v.value)) span + sanity_check __FILE__ __LINE__ + (not (value_has_borrows (Some span) ctx v.value)) + span in List.iter (check_no_borrows ctx0) adt0.field_values; List.iter (check_no_borrows ctx1) adt1.field_values; @@ -529,7 +531,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let loan = ASharedLoan - (PNone, BorrowId.Set.singleton bid2, sv, mk_aignored span bv_ty) + (PNone, BorrowId.Set.singleton bid2, sv, mk_aignored span bv_ty None) in (* Note that an aloan has a borrow type *) let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in @@ -615,7 +617,9 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct will update [v], while the backward loop function will return nothing. *) cassert __FILE__ __LINE__ - (not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) + (not + (ValuesUtils.value_has_borrows (Some span) ctx0.type_ctx.type_infos + bv.value)) span "Nested borrows are not supported yet"; if bv0 = bv1 then ( @@ -634,14 +638,16 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let borrow_av = let ty = borrow_ty in let value = - ABorrow (AMutBorrow (PNone, bid0, mk_aignored span bv_ty)) + ABorrow (AMutBorrow (PNone, bid0, mk_aignored span bv_ty None)) in mk_typed_avalue span ty value in let loan_av = let ty = borrow_ty in - let value = ALoan (AMutLoan (PNone, nbid, mk_aignored span bv_ty)) in + let value = + ALoan (AMutLoan (PNone, nbid, mk_aignored span bv_ty None)) + in mk_typed_avalue span ty value in @@ -687,12 +693,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let bv_ty = bv.ty in cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span "Nested borrows are not supported yet"; - let value = ABorrow (AMutBorrow (pm, bid, mk_aignored span bv_ty)) in + let value = + ABorrow (AMutBorrow (pm, bid, mk_aignored span bv_ty None)) + in { value; ty = borrow_ty } in let borrows = [ mk_aborrow PLeft bid0 bv0; mk_aborrow PRight bid1 bv1 ] in - let loan = AMutLoan (PNone, bid2, mk_aignored span bv_ty) in + let loan = AMutLoan (PNone, bid2, mk_aignored span bv_ty None) in (* Note that an aloan has a borrow type *) let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in @@ -760,7 +768,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* The caller should have checked that the symbolic values don't contain borrows *) sanity_check __FILE__ __LINE__ - (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) + (not (ty_has_borrows (Some span) ctx0.type_ctx.type_infos sv0.sv_ty)) span; (* TODO: the symbolic values may contain bottoms: we're being conservatice, and fail (for now) if part of a symbolic value contains a bottom. @@ -780,10 +788,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct *) let type_infos = ctx0.type_ctx.type_infos in sanity_check __FILE__ __LINE__ - (not (ty_has_borrows type_infos sv.sv_ty)) + (not (ty_has_borrows (Some span) type_infos sv.sv_ty)) span; sanity_check __FILE__ __LINE__ - (not (ValuesUtils.value_has_borrows type_infos v.value)) + (not (ValuesUtils.value_has_borrows (Some span) type_infos v.value)) span; let value_is_left = not left in (* If there are loans in the regular value, raise an exception. *) @@ -1227,7 +1235,7 @@ struct a continue, where the fixed point contains some bottom values. *) let value_is_left = not left in let ctx = if value_is_left then ctx0 else ctx1 in - if left && not (value_has_loans_or_borrows ctx v.value) then + if left && not (value_has_loans_or_borrows (Some span) ctx v.value) then mk_bottom span v.ty else raise diff --git a/src/interp/InterpreterProjectors.ml b/src/interp/InterpreterProjectors.ml index 0e820982..f10a4dbf 100644 --- a/src/interp/InterpreterProjectors.ml +++ b/src/interp/InterpreterProjectors.ml @@ -100,11 +100,12 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool) let ety = Substitute.erase_regions ty in sanity_check __FILE__ __LINE__ (ty_is_rty ty && ety = v.ty) span; (* Project - if there are no regions from the abstraction in the type, return [_] *) - if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty } + if not (ty_has_regions_in_set regions ty) then + { value = AIgnored (Some v); ty } else let value : avalue = match (v.value, ty) with - | VLiteral _, TLiteral _ -> AIgnored + | VLiteral _, TLiteral _ -> AIgnored (Some v) | VAdt adt, TAdt (id, generics) -> (* Retrieve the types of the fields *) let field_types = @@ -270,7 +271,9 @@ let apply_proj_loans_on_symbolic_expansion (span : Meta.span) (* Match *) let (value, ty) : avalue * ty = match (see, original_sv_ty) with - | SeLiteral _, TLiteral _ -> (AIgnored, original_sv_ty) + | SeLiteral lit, TLiteral _ -> + ( AIgnored (Some { value = VLiteral lit; ty = original_sv_ty }), + original_sv_ty ) | SeAdt (variant_id, field_values), TAdt (_id, _generics) -> (* Project over the field values *) let field_values = @@ -456,11 +459,11 @@ let apply_reborrows (span : Meta.span) super#visit_ASharedLoan env pm bids sv av | AIgnoredSharedLoan _ | AMutLoan (_, _, _) - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } -> + { given_back = _; child = _; given_back_meta = _ } -> (* Nothing particular to do *) super#visit_aloan_content env lc end diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml index f24da01c..01ad66b5 100644 --- a/src/interp/InterpreterStatements.ml +++ b/src/interp/InterpreterStatements.ml @@ -1368,12 +1368,14 @@ and eval_transparent_function_call_symbolic (config : config) (span : Meta.span) (* 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)) + (fun ty -> + not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty)) (inst_sg.output :: inst_sg.inputs)) span "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)) + (fun ty -> + not (ty_has_adt_with_borrows (Some span) ctx.type_ctx.type_infos ty)) (inst_sg.output :: inst_sg.inputs)) span "ADTs containing borrows are not supported yet"; (* Evaluate the function call *) @@ -1444,7 +1446,9 @@ and eval_function_call_symbolic_from_inst_sig (config : config) sanity_check __FILE__ __LINE__ (List.for_all (fun arg -> - not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + not + (value_has_ret_symbolic_value_with_borrow_under_mut (Some span) ctx + arg)) args) span; @@ -1548,7 +1552,7 @@ and eval_builtin_function_call_symbolic (config : config) (span : Meta.span) * this is a current limitation of our synthesis *) sanity_check __FILE__ __LINE__ (List.for_all - (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty)) + (fun ty -> not (ty_has_borrows (Some span) ctx.type_ctx.type_infos ty)) generics.types) span; diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index b08e0f43..e4fce657 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -128,7 +128,11 @@ let mk_aproj_loans_value_from_symbolic_value (regions : RegionId.Set.t) let av = ASymbolic (AProjLoans (svalue, [])) in let av : typed_avalue = { value = av; ty = svalue.sv_ty } in av - else { value = AIgnored; ty = svalue.sv_ty } + else + { + value = AIgnored (Some (mk_typed_value_from_symbolic_value svalue)); + ty = svalue.sv_ty; + } (** Create a borrows projector from a symbolic value *) let mk_aproj_borrows_from_symbolic_value (span : Meta.span) @@ -280,14 +284,14 @@ let bottom_in_adt_value (ended_regions : RegionId.Set.t) (v : adt_value) : bool false with Found -> true -let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx) +let value_has_ret_symbolic_value_with_borrow_under_mut span (ctx : eval_ctx) (v : typed_value) : bool = let obj = object inherit [_] iter_typed_value method! visit_symbolic_value _ s = - if ty_has_borrow_under_mut ctx.type_ctx.type_infos s.sv_ty then + if ty_has_borrow_under_mut span ctx.type_ctx.type_infos s.sv_ty then raise Found else () end @@ -315,16 +319,17 @@ let rvalue_get_place (rv : rvalue) : place option = | Aggregate _ -> None (** See {!ValuesUtils.symbolic_value_has_borrows} *) -let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool = - ValuesUtils.symbolic_value_has_borrows ctx.type_ctx.type_infos sv +let symbolic_value_has_borrows span (ctx : eval_ctx) (sv : symbolic_value) : + bool = + ValuesUtils.symbolic_value_has_borrows span ctx.type_ctx.type_infos sv (** See {!ValuesUtils.value_has_borrows}. *) -let value_has_borrows (ctx : eval_ctx) (v : value) : bool = - ValuesUtils.value_has_borrows ctx.type_ctx.type_infos v +let value_has_borrows span (ctx : eval_ctx) (v : value) : bool = + ValuesUtils.value_has_borrows span ctx.type_ctx.type_infos v (** See {!ValuesUtils.value_has_loans_or_borrows}. *) -let value_has_loans_or_borrows (ctx : eval_ctx) (v : value) : bool = - ValuesUtils.value_has_loans_or_borrows ctx.type_ctx.type_infos v +let value_has_loans_or_borrows span (ctx : eval_ctx) (v : value) : bool = + ValuesUtils.value_has_loans_or_borrows span ctx.type_ctx.type_infos v (** See {!ValuesUtils.value_has_loans}. *) let value_has_loans (v : value) : bool = ValuesUtils.value_has_loans v @@ -508,7 +513,7 @@ let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx) (* Generate fresh regions and their substitutions *) let _, rsubst, _ = Substitute.fresh_regions_with_substs_from_vars ~fail_if_not_found:true - sg.generics.regions + sg.generics.regions fresh_region_id in let rsubst r = Option.get (rsubst r) in (* Generate the type substitution diff --git a/src/interp/Invariants.ml b/src/interp/Invariants.ml index ea2b26c3..e9e20460 100644 --- a/src/interp/Invariants.ml +++ b/src/interp/Invariants.ml @@ -155,10 +155,10 @@ let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) : | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan RMut bid | AIgnoredMutLoan (None, _) | AIgnoredSharedLoan _ - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } | AEndedSharedLoan (_, _) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } -> + { given_back = _; child = _; given_back_meta = _ } -> (* Do nothing *) () in @@ -345,12 +345,12 @@ let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit = match lc with | AMutLoan (_, _, _) -> set_outer_mut info | ASharedLoan (_, _, _, _) -> set_outer_shared info - | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } -> + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } -> set_outer_mut info | AEndedSharedLoan (_, _) -> set_outer_shared info | AIgnoredMutLoan (_, _) -> set_outer_mut info | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_span = _ } -> + { given_back = _; child = _; given_back_meta = _ } -> set_outer_mut info | AIgnoredSharedLoan _ -> set_outer_shared info in @@ -632,7 +632,7 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | _ -> craise __FILE__ __LINE__ span "Inconsistent context") | AIgnoredMutBorrow (_opt_bid, av), RMut -> sanity_check __FILE__ __LINE__ (av.ty = ref_ty) span - | ( AEndedIgnoredMutBorrow { given_back; child; given_back_span = _ }, + | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, RMut ) -> sanity_check __FILE__ __LINE__ (given_back.ty = ref_ty) span; sanity_check __FILE__ __LINE__ (child.ty = ref_ty) span @@ -674,8 +674,8 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | ASharedLoan (_, _, _, _) -> (* We get there if the projection marker is not [PNone] *) internal_error __FILE__ __LINE__ span - | AEndedMutLoan { given_back; child; given_back_span = _ } - | AEndedIgnoredMutLoan { given_back; child; given_back_span = _ } -> + | 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) @@ -716,7 +716,7 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | _ -> craise __FILE__ __LINE__ span "Unexpected") given_back_ls | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()) - | AIgnored, _ -> () + | AIgnored _, _ -> () | _ -> log#ltrace (lazy @@ -836,7 +836,7 @@ let check_symbolic_values (span : Meta.span) (ctx : eval_ctx) : unit = span; (* 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 + if ty_has_borrows (Some span) ctx.type_ctx.type_infos info.ty then sanity_check __FILE__ __LINE__ (info.env_count <= 1) span; (* A duplicated symbolic value is necessarily copyable *) sanity_check __FILE__ __LINE__ diff --git a/src/llbc/Contexts.ml b/src/llbc/Contexts.ml index 6468a0b3..bfe9f99e 100644 --- a/src/llbc/Contexts.ml +++ b/src/llbc/Contexts.ml @@ -1,11 +1,9 @@ open Types -open TypesUtils open Expressions open Values open LlbcAst open LlbcAstUtils open ValuesUtils -open Identifiers open Errors include ContextsBase diff --git a/src/llbc/ContextsBase.ml b/src/llbc/ContextsBase.ml index ecd12199..dd7ad953 100644 --- a/src/llbc/ContextsBase.ml +++ b/src/llbc/ContextsBase.ml @@ -2,7 +2,6 @@ open Types open Expressions open Values open Identifiers -open Errors module L = Logging (** The local logger *) diff --git a/src/llbc/Print.ml b/src/llbc/Print.ml index 1d23d4b8..2a60b193 100644 --- a/src/llbc/Print.ml +++ b/src/llbc/Print.ml @@ -198,7 +198,7 @@ module Values = struct | ABorrow bc -> aborrow_content_to_string ~span env bc | ALoan lc -> aloan_content_to_string ~span env lc | ASymbolic s -> aproj_to_string env s - | AIgnored -> "_" + | AIgnored _ -> "_" and aloan_content_to_string ?(span : Meta.span option = None) (env : fmt_env) (lc : aloan_content) : string = @@ -261,7 +261,7 @@ module Values = struct ^ ")" | AEndedMutBorrow (_mv, child) -> "@ended_mut_borrow(" ^ typed_avalue_to_string ~span env child ^ ")" - | AEndedIgnoredMutBorrow { child; given_back; given_back_span = _ } -> + | AEndedIgnoredMutBorrow { child; given_back; given_back_meta = _ } -> "@ended_ignored_mut_borrow{ " ^ typed_avalue_to_string ~span env child ^ "; " diff --git a/src/llbc/RegionsHierarchy.ml b/src/llbc/RegionsHierarchy.ml index 8e750162..0f497839 100644 --- a/src/llbc/RegionsHierarchy.ml +++ b/src/llbc/RegionsHierarchy.ml @@ -87,6 +87,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) let bound_regions, bound_regions_id_subst, bound_regions_subst = Subst.fresh_regions_with_substs_from_vars ~fail_if_not_found:true sg.generics.regions + (snd (RegionId.fresh_stateful_generator ())) in let region_id_to_var_map : RegionVarId.id RegionId.Map.t = RegionId.Map.of_list diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml index cf38dde7..123baefa 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -17,7 +17,7 @@ open Errors TODO: simplify? we only need the subst [RegionVarId.id -> RegionId.id] *) let fresh_regions_with_substs ~(fail_if_not_found : bool) - (region_vars : RegionVarId.id list) : + (region_vars : RegionVarId.id list) (fresh_region_id : unit -> region_id) : RegionId.id list * (RegionVarId.id -> RegionId.id option) * (region -> region) = @@ -43,12 +43,13 @@ let fresh_regions_with_substs ~(fail_if_not_found : bool) (fresh_region_ids, rid_subst, r_subst) let fresh_regions_with_substs_from_vars ~(fail_if_not_found : bool) - (region_vars : region_var list) : + (region_vars : region_var list) (fresh_region_id : unit -> region_id) : RegionId.id list * (RegionVarId.id -> RegionId.id option) * (region -> region) = fresh_regions_with_substs ~fail_if_not_found (List.map (fun (r : region_var) -> r.index) region_vars) + fresh_region_id (** Substitute a function signature, together with the regions hierarchy associated to that signature. @@ -196,12 +197,10 @@ let env_subst_rids (r_subst : RegionId.id -> RegionId.id) (x : env) : env = in vis#visit_env () x -let generic_args_of_params_erase_regions span (generics : generic_params) : - generic_args = - let generics = - st_substitute_visitor#visit_generic_params erase_regions_subst generics - in - (* Note that from here we don't need to perform any susbtitutions actually *) +let generic_args_of_params_erase_regions (span : Meta.span option) + (generics : generic_params) : generic_args = + (* Note that put aside erasing the regions, we don't need to perform any susbtitutions + actually, and we only need to erase the regions inside the trait clauses. *) let regions = List.map (fun _ -> RErased) generics.regions in let types = List.map (fun (v : type_var) -> TVar v.index) generics.types in let const_generics = @@ -209,10 +208,18 @@ let generic_args_of_params_erase_regions span (generics : generic_params) : (fun (v : const_generic_var) -> CgVar v.index) generics.const_generics in + (* Erase the regions in the trait clauses. *) + let trait_clauses = + List.map + (st_substitute_visitor#visit_trait_clause erase_regions_subst) + generics.trait_clauses + in let trait_refs = List.map (fun (c : trait_clause) -> - sanity_check __FILE__ __LINE__ (c.trait.binder_regions = []) span; + sanity_check_opt_span __FILE__ __LINE__ + (c.trait.binder_regions = []) + span; let { trait_decl_id; decl_generics; _ } = c.trait.binder_value in let trait_decl_ref = { trait_decl_id; decl_generics } in (* Note that because we directly refer to the clause, we give it @@ -227,6 +234,6 @@ let generic_args_of_params_erase_regions span (generics : generic_params) : binder_value = trait_decl_ref; }; }) - generics.trait_clauses + trait_clauses in { regions; types; const_generics; trait_refs } diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml index 1198557c..5e317418 100644 --- a/src/llbc/TypesAnalysis.ml +++ b/src/llbc/TypesAnalysis.ml @@ -1,6 +1,7 @@ open Types open LlbcAst open Errors +open Substitute type subtype_info = { under_borrow : bool; (** Are we inside a borrow? *) @@ -17,6 +18,8 @@ type type_borrows_info = { contains_static : bool; (** Does the type (transitively) contain a static borrow? *) contains_borrow : bool; (** Does the type (transitively) contain a borrow? *) + contains_mut_borrow : bool; + (** Does the type (transitively) contain a mutable borrow? *) contains_nested_borrows : bool; (** Does the type (transitively) contain nested borrows? *) contains_borrow_under_mut : bool; @@ -31,7 +34,9 @@ type 'p g_type_info = { is_tuple_struct : bool; (** If true, it means the type is a record that we should extract as a tuple. This field is only valid for type declarations. - *) + *) + mut_regions : RegionVarId.Set.t; + (** The set of regions used in mutable borrows *) } [@@deriving show] @@ -56,6 +61,7 @@ let type_borrows_info_init : type_borrows_info = { contains_static = false; contains_borrow = false; + contains_mut_borrow = false; contains_nested_borrows = false; contains_borrow_under_mut = false; } @@ -73,7 +79,12 @@ let type_decl_is_tuple_struct (x : type_decl) : bool = let initialize_g_type_info (is_tuple_struct : bool) (param_infos : 'p) : 'p g_type_info = - { borrows_info = type_borrows_info_init; is_tuple_struct; param_infos } + { + borrows_info = type_borrows_info_init; + is_tuple_struct; + param_infos; + mut_regions = RegionVarId.Set.empty; + } let initialize_type_decl_info (is_rec : bool) (def : type_decl) : type_decl_info = @@ -90,6 +101,7 @@ let type_decl_info_to_partial_type_info (info : type_decl_info) : borrows_info = info.borrows_info; is_tuple_struct = info.is_tuple_struct; param_infos = Some info.param_infos; + mut_regions = info.mut_regions; } let partial_type_info_to_type_decl_info (info : partial_type_info) : @@ -98,13 +110,25 @@ let partial_type_info_to_type_decl_info (info : partial_type_info) : borrows_info = info.borrows_info; is_tuple_struct = info.is_tuple_struct; param_infos = Option.get info.param_infos; + mut_regions = info.mut_regions; } let partial_type_info_to_ty_info (info : partial_type_info) : ty_info = info.borrows_info -let analyze_full_ty (updated : bool ref) (infos : type_infos) - (ty_info : partial_type_info) (ty : ty) : partial_type_info = +let rec trait_instance_id_reducible (span : Meta.span option) + (id : trait_instance_id) : bool = + match id with + | BuiltinOrAuto _ | TraitImpl _ -> true + | Self | Clause _ -> false + | ParentClause (id, _, _) -> trait_instance_id_reducible span id + | FnPointer _ | Closure _ | Dyn _ -> + craise_opt_span __FILE__ __LINE__ span "Unreachable" + | Unsolved _ | UnknownTrait _ -> false + +let analyze_full_ty (span : Meta.span option) (updated : bool ref) + (infos : type_infos) (ty_info : partial_type_info) (ty : ty) : + partial_type_info = (* Small utility *) let check_update_bool (original : bool) (nv : bool) : bool = if nv && not original then ( @@ -113,9 +137,23 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) else original in let r_is_static (r : region) : bool = r = RStatic in + let update_mut_regions_with_rid mut_regions rid = + let rid = RegionVarId.of_int (RegionId.to_int rid) in + if RegionVarId.Set.mem rid mut_regions then ty_info.mut_regions + else ( + updated := true; + RegionVarId.Set.add rid mut_regions) + in + let update_mut_regions mut_regions mut_region = + match mut_region with + | RStatic | RBVar _ -> + mut_regions (* We can have bound vars because of arrows *) + | RErased -> craise_opt_span __FILE__ __LINE__ span "Unreachable" + | RFVar rid -> update_mut_regions_with_rid mut_regions rid + in (* Update a partial_type_info, while registering if we actually performed an update *) - let update_ty_info (ty_info : partial_type_info) + let update_ty_info (ty_info : partial_type_info) (mut_region : region option) (ty_b_info : type_borrows_info) : partial_type_info = let original = ty_info.borrows_info in let contains_static = @@ -124,6 +162,10 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) let contains_borrow = check_update_bool original.contains_borrow ty_b_info.contains_borrow in + let contains_mut_borrow = + check_update_bool original.contains_mut_borrow + ty_b_info.contains_mut_borrow + in let contains_nested_borrows = check_update_bool original.contains_nested_borrows ty_b_info.contains_nested_borrows @@ -136,18 +178,41 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) { contains_static; contains_borrow; + contains_mut_borrow; contains_nested_borrows; contains_borrow_under_mut; } in - { ty_info with borrows_info = updated_borrows_info } + (* Add the region *) + let updated_mut_regions = + match mut_region with + | None -> ty_info.mut_regions + | Some mut_region -> update_mut_regions ty_info.mut_regions mut_region + in + { + ty_info with + borrows_info = updated_borrows_info; + mut_regions = updated_mut_regions; + } in (* The recursive function which explores the type *) - let rec analyze (expl_info : expl_info) (ty_info : partial_type_info) - (ty : ty) : partial_type_info = + let rec analyze (span : Meta.span option) (expl_info : expl_info) + (ty_info : partial_type_info) (ty : ty) : partial_type_info = match ty with - | TLiteral _ | TNever | TTraitType _ | TDynTrait _ -> ty_info + | TLiteral _ | TNever | TDynTrait _ -> ty_info + | TTraitType (tref, _) -> + (* TODO: normalize the trait types. + For now we only emit a warning because it makes some tests fail. *) + cassert_warn_opt_span __FILE__ __LINE__ + (not (trait_instance_id_reducible span tref.trait_id)) + span + "Found an unexpected trait impl associated type which was not \ + inlined while analyzing a type. This is a case we currently do not \ + handle in all generality. As a result,the consumed/given back \ + values computed for the generated backward functions may be \ + incorrect."; + ty_info | TVar var_id -> ( (* Update the information for the proper parameter, if necessary *) match ty_info.param_infos with @@ -174,17 +239,23 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) (* Update the type info *) let contains_static = r_is_static r in let contains_borrow = true in + let contains_mut_borrow, region = + match rkind with + | RMut -> (true, Some r) + | RShared -> (false, None) + in let contains_nested_borrows = expl_info.under_borrow in let contains_borrow_under_mut = expl_info.under_mut_borrow in let ty_b_info = { contains_static; contains_borrow; + contains_mut_borrow; contains_nested_borrows; contains_borrow_under_mut; } in - let ty_info = update_ty_info ty_info ty_b_info in + let ty_info = update_ty_info ty_info region ty_b_info in (* Update the exploration info *) let expl_info = { @@ -193,20 +264,20 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) } in (* Continue exploring *) - analyze expl_info ty_info rty + analyze span expl_info ty_info rty | TRawPtr (rty, _) -> (* TODO: not sure what to do here *) - analyze expl_info ty_info rty + analyze span expl_info ty_info rty | TAdt ((TTuple | TBuiltin (TBox | TSlice | TArray | TStr)), generics) -> (* Nothing to update: just explore the type parameters *) List.fold_left - (fun ty_info ty -> analyze expl_info ty_info ty) + (fun ty_info ty -> analyze span expl_info ty_info ty) ty_info generics.types | TAdt (TAdtId adt_id, generics) -> (* Lookup the information for this type definition *) let adt_info = TypeDeclId.Map.find adt_id infos in (* Update the type info with the information from the adt *) - let ty_info = update_ty_info ty_info adt_info.borrows_info in + let ty_info = update_ty_info ty_info None adt_info.borrows_info in (* Check if 'static appears in the region parameters *) let found_static = List.exists r_is_static generics.regions in let borrows_info = ty_info.borrows_info in @@ -219,7 +290,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) in let ty_info = { ty_info with borrows_info } in (* For every instantiated type parameter: update the exploration info - * then explore the type *) + then explore the type *) let params_tys = List.combine adt_info.param_infos generics.types in let ty_info = List.fold_left @@ -229,6 +300,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) * by taking the type parameter into account. *) let contains_static = false in let contains_borrow = param_info.under_borrow in + let contains_mut_borrow = param_info.under_mut_borrow in let contains_nested_borrows = expl_info.under_borrow && param_info.under_borrow in @@ -239,11 +311,12 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) { contains_static; contains_borrow; + contains_mut_borrow; contains_nested_borrows; contains_borrow_under_mut; } in - let ty_info = update_ty_info ty_info ty_b_info in + let ty_info = update_ty_info ty_info None ty_b_info in (* Update the exploration info *) let expl_info = { @@ -254,22 +327,38 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) } in (* Continue exploring *) - analyze expl_info ty_info ty) + analyze span expl_info ty_info ty) ty_info params_tys in + (* For every region parameter: do the same *) + let mut_regions = + List.fold_left + (fun mut_regions (adt_rid, r) -> + (* Check if the region is a variable and is used for mutable borrows *) + match r with + | RStatic | RBVar _ | RErased -> mut_regions + (* We can have bound vars because of arrows, and erased regions + when analyzing types appearing in function bodies *) + | RFVar rid -> + if RegionVarId.Set.mem adt_rid adt_info.mut_regions then + update_mut_regions_with_rid mut_regions rid + else mut_regions) + ty_info.mut_regions + (RegionVarId.mapi (fun adt_rid r -> (adt_rid, r)) generics.regions) + in (* Return *) - ty_info + { ty_info with mut_regions } | TArrow (_regions, inputs, output) -> (* Just dive into the arrow *) let ty_info = List.fold_left - (fun ty_info ty -> analyze expl_info ty_info ty) + (fun ty_info ty -> analyze span expl_info ty_info ty) ty_info inputs in - analyze expl_info ty_info output + analyze span expl_info ty_info output in (* Explore *) - analyze expl_info_init ty_info ty + analyze span expl_info_init ty_info ty let type_decl_is_opaque (d : type_decl) : bool = match d.kind with @@ -299,13 +388,23 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos) | Opaque | Error _ -> craise __FILE__ __LINE__ def.item_meta.span "unreachable" in + (* Substitute the regions in the fields *) + let _, _, r_subst = + Substitute.fresh_regions_with_substs_from_vars ~fail_if_not_found:true + def.generics.regions + (snd (RegionId.fresh_stateful_generator ())) + in + let subst = { Substitute.empty_subst with r_subst } in + let fields_tys = List.map (Substitute.ty_substitute subst) fields_tys in (* Explore the types and accumulate information *) let type_decl_info = TypeDeclId.Map.find def.def_id infos in let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in + (* TODO: substitute the types *) let type_decl_info = List.fold_left (fun type_decl_info ty -> - analyze_full_ty updated infos type_decl_info ty) + analyze_full_ty (Some def.item_meta.span) updated infos type_decl_info + ty) type_decl_info fields_tys in let type_decl_info = partial_type_info_to_type_decl_info type_decl_info in @@ -363,11 +462,12 @@ let analyze_type_declarations (type_decls : type_decl TypeDeclId.Map.t) (** Analyze a type to check whether it contains borrows, etc., provided we have already analyzed the type definitions in the context. *) -let analyze_ty (infos : type_infos) (ty : ty) : ty_info = +let analyze_ty (span : Meta.span option) (infos : type_infos) (ty : ty) : + ty_info = (* We don't use [updated] but need to give it as parameter *) let updated = ref false in (* We don't need to compute whether the type contains 'static or not *) let ty_info = initialize_g_type_info false None in - let ty_info = analyze_full_ty updated infos ty_info ty in + let ty_info = analyze_full_ty span updated infos ty_info ty in (* Convert the ty_info *) partial_type_info_to_ty_info ty_info diff --git a/src/llbc/TypesUtils.ml b/src/llbc/TypesUtils.ml index 315d6f85..fcce64fd 100644 --- a/src/llbc/TypesUtils.ml +++ b/src/llbc/TypesUtils.ml @@ -8,8 +8,9 @@ include Charon.TypesUtils we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty}, and when a type uses 'static this region doesn't appear in the region parameters. *) -let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = - let info = TypesAnalysis.analyze_ty infos ty in +let ty_has_borrows (span : Meta.span option) (infos : TypesAnalysis.type_infos) + (ty : ty) : bool = + let info = TypesAnalysis.analyze_ty span infos ty in info.TypesAnalysis.contains_borrow (** Checks that a type is copyable. @@ -20,8 +21,8 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = *) let ty_is_copyable (_ty : ty) : bool = true -let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool - = +let ty_has_adt_with_borrows span (infos : TypesAnalysis.type_infos) (ty : ty) : + bool = let visitor = object inherit [_] iter_ty as super @@ -29,7 +30,7 @@ let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool method! visit_ty env ty = match ty with | TAdt (type_id, _) when type_id <> TTuple -> - let info = TypesAnalysis.analyze_ty infos ty in + let info = TypesAnalysis.analyze_ty span infos ty in if info.TypesAnalysis.contains_borrow then raise Found else super#visit_ty env ty | _ -> super#visit_ty env ty @@ -46,25 +47,64 @@ let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty}, and when a type uses 'static this region doesn't appear in the region parameters. *) -let ty_has_nested_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = - let info = TypesAnalysis.analyze_ty infos ty in +let ty_has_nested_borrows (span : Meta.span option) + (infos : TypesAnalysis.type_infos) (ty : ty) : bool = + let info = TypesAnalysis.analyze_ty span infos ty in info.TypesAnalysis.contains_nested_borrows (** Retuns true if the type decl contains nested borrows. *) -let type_decl_has_nested_borrows span (infos : TypesAnalysis.type_infos) - (type_decl : type_decl) : bool = +let type_decl_has_nested_borrows (span : Meta.span option) + (infos : TypesAnalysis.type_infos) (type_decl : type_decl) : bool = let generics = Substitute.generic_args_of_params_erase_regions span type_decl.generics in let ty = TAdt (TAdtId type_decl.def_id, generics) in - ty_has_nested_borrows infos ty + ty_has_nested_borrows span infos ty (** Retuns true if the type contains a borrow under a mutable borrow *) -let ty_has_borrow_under_mut (infos : TypesAnalysis.type_infos) (ty : ty) : bool - = - let info = TypesAnalysis.analyze_ty infos ty in +let ty_has_borrow_under_mut span (infos : TypesAnalysis.type_infos) (ty : ty) : + bool = + let info = TypesAnalysis.analyze_ty span infos ty in info.TypesAnalysis.contains_borrow_under_mut +(** Check if a {!type:Charon.Types.ty} contains a mutable borrow which uses a + region from a given set. *) +let ty_has_mut_borrow_for_region_in_pred (infos : TypesAnalysis.type_infos) + (pred : region -> bool) (ty : ty) : bool = + let obj = + object + inherit [_] iter_ty as super + + method! visit_TRef env r ty rkind = + begin + match rkind with + | RMut -> if pred r then raise Found + | RShared -> () + end; + super#visit_TRef env r ty rkind + + method! visit_TAdt env type_id generics = + (* Lookup the information for this ADT *) + begin + match type_id with + | TTuple | TBuiltin (TBox | TArray | TSlice | TStr) -> () + | TAdtId adt_id -> + let info = TypeDeclId.Map.find adt_id infos in + RegionVarId.iteri + (fun adt_rid r -> + if RegionVarId.Set.mem adt_rid info.mut_regions && pred r then + raise Found + else ()) + generics.regions + end; + super#visit_TAdt env type_id generics + end + in + try + obj#visit_ty () ty; + false + with Found -> true + (** Small helper *) let raise_if_not_rty_visitor = object diff --git a/src/llbc/Values.ml b/src/llbc/Values.ml index c32cbc6e..b9522f01 100644 --- a/src/llbc/Values.ml +++ b/src/llbc/Values.ml @@ -154,10 +154,10 @@ and typed_value = { value : value; ty : ty } (** "Meta"-value: information we store for the synthesis. Note that we never automatically visit the meta-values with the - visitors: they really are span information, and shouldn't be considered + visitors: they really are meta information, and shouldn't be considered as part of the environment during a symbolic execution. - TODO: we may want to create wrappers, to prevent accidently mixing span + TODO: we may want to create wrappers, to prevent accidently mixing meta values and regular values. *) type mvalue = typed_value [@@deriving show, ord] @@ -349,11 +349,15 @@ and avalue = | ALoan of aloan_content | ABorrow of aborrow_content | ASymbolic of aproj - | AIgnored + | AIgnored of mvalue option (** A value which doesn't contain borrows, or which borrows we don't own and thus ignore. In the comments, we display it as [_]. + + Note that we store the ignored value as a meta value. + Also note that this value is not always present (when we introduce + abstractions because of a join for instance). *) and adt_avalue = { @@ -415,7 +419,7 @@ and aloan_content = | AEndedMutLoan of { child : typed_avalue; given_back : typed_avalue; - given_back_span : mvalue; + given_back_meta : mvalue; } (** An ended mutable loan in an abstraction. We need it because abstractions must keep track of the values @@ -440,7 +444,7 @@ and aloan_content = After ending [l0]: {[ - abs0 { a_ended_mut_loan { child = _; given_back = _; given_back_span = U32 3; } + abs0 { a_ended_mut_loan { child = _; given_back = _; given_back_meta = U32 3; } x -> ⊥ ]} @@ -459,7 +463,7 @@ and aloan_content = a_ended_mut_loan { child = _; given_back = a_mut_borrow l1 _; - given_back_span = (mut_borrow l1 (U32 3)); + given_back_meta = (mut_borrow l1 (U32 3)); } } ... @@ -503,7 +507,7 @@ and aloan_content = a_ended_ignored_mut_loan { child = a_mut_loan l1 _; given_back = a_mut_borrow l1 _; - given_back_span = mut_borrow l1 @s1 + given_back_meta = mut_borrow l1 @s1 } } x -> ⊥ @@ -513,7 +517,7 @@ and aloan_content = | AEndedIgnoredMutLoan of { child : typed_avalue; given_back : typed_avalue; - given_back_span : mvalue; + given_back_meta : mvalue; } (** Similar to {!AEndedMutLoan}, for ignored loans. See the comments for {!AIgnoredMutLoan}. @@ -661,8 +665,8 @@ and aborrow_content = | AEndedIgnoredMutBorrow of { child : typed_avalue; given_back : typed_avalue; - given_back_span : msymbolic_value; - (** [given_back_span] is used to store the (symbolic) value we gave back + given_back_meta : msymbolic_value; + (** [given_back_meta] is used to store the (symbolic) value we gave back upon ending the borrow. Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan]. diff --git a/src/llbc/ValuesUtils.ml b/src/llbc/ValuesUtils.ml index e36b1aaa..147ef962 100644 --- a/src/llbc/ValuesUtils.ml +++ b/src/llbc/ValuesUtils.ml @@ -34,9 +34,10 @@ let mk_abottom (span : Meta.span) (ty : ty) : typed_avalue = sanity_check __FILE__ __LINE__ (ty_is_rty ty) span; { value = ABottom; ty } -let mk_aignored (span : Meta.span) (ty : ty) : typed_avalue = +let mk_aignored (span : Meta.span) (ty : ty) (v : typed_value option) : + typed_avalue = sanity_check __FILE__ __LINE__ (ty_is_rty ty) span; - { value = AIgnored; ty } + { value = AIgnored v; ty } let value_as_symbolic (span : Meta.span) (v : value) : symbolic_value = match v with @@ -56,7 +57,7 @@ let is_bottom (v : value) : bool = let is_aignored (v : avalue) : bool = match v with - | AIgnored -> true + | AIgnored _ -> true | _ -> false let is_symbolic (v : value) : bool = @@ -163,7 +164,7 @@ let outer_loans_in_value (v : typed_value) : bool = false with Found -> true -let find_first_primitively_copyable_sv_with_borrows +let find_first_primitively_copyable_sv_with_borrows span (type_infos : TypesAnalysis.type_infos) (v : typed_value) : symbolic_value option = (* The visitor *) @@ -173,7 +174,7 @@ let find_first_primitively_copyable_sv_with_borrows method! visit_VSymbolic _ sv = let ty = sv.sv_ty in - if ty_is_copyable ty && ty_has_borrows type_infos ty then + if ty_is_copyable ty && ty_has_borrows span type_infos ty then raise (FoundSymbolicValue sv) else () end @@ -195,9 +196,9 @@ let rec value_strip_shared_loans (v : typed_value) : typed_value = | _ -> v (** Check if a symbolic value has borrows *) -let symbolic_value_has_borrows (infos : TypesAnalysis.type_infos) +let symbolic_value_has_borrows span (infos : TypesAnalysis.type_infos) (sv : symbolic_value) : bool = - ty_has_borrows infos sv.sv_ty + ty_has_borrows span infos sv.sv_ty (** Check if a value has borrows in **a general sense**. @@ -205,14 +206,15 @@ let symbolic_value_has_borrows (infos : TypesAnalysis.type_infos) - there are concrete borrows - there are symbolic values which may contain borrows *) -let value_has_borrows (infos : TypesAnalysis.type_infos) (v : value) : bool = +let value_has_borrows span (infos : TypesAnalysis.type_infos) (v : value) : bool + = let obj = object inherit [_] iter_typed_value method! visit_borrow_content _env _ = raise Found method! visit_symbolic_value _ sv = - if symbolic_value_has_borrows infos sv then raise Found else () + if symbolic_value_has_borrows span infos sv then raise Found else () end in (* We use exceptions *) @@ -246,8 +248,8 @@ let value_has_loans (v : value) : bool = - there are symbolic values which may contain borrows (symbolic values can't contain loans). *) -let value_has_loans_or_borrows (infos : TypesAnalysis.type_infos) (v : value) : - bool = +let value_has_loans_or_borrows span (infos : TypesAnalysis.type_infos) + (v : value) : bool = let obj = object inherit [_] iter_typed_value @@ -255,7 +257,7 @@ let value_has_loans_or_borrows (infos : TypesAnalysis.type_infos) (v : value) : method! visit_loan_content _env _ = raise Found method! visit_symbolic_value _ sv = - if ty_has_borrow_under_mut infos sv.sv_ty then raise Found else () + if ty_has_borrow_under_mut span infos sv.sv_ty then raise Found else () end in (* We use exceptions *) diff --git a/src/pure/PrintPure.ml b/src/pure/PrintPure.ml index 575f2ba7..841baee8 100644 --- a/src/pure/PrintPure.ml +++ b/src/pure/PrintPure.ml @@ -16,10 +16,19 @@ type fmt_env = { trait_decls : LlbcAst.trait_decl TraitDeclId.Map.t; trait_impls : LlbcAst.trait_impl TraitImplId.Map.t; generics : generic_params; - locals : (VarId.id * string option) list; + vars : string VarId.Map.t; } -let var_id_to_pretty_string (id : var_id) : string = "v@" ^ VarId.to_string id +let fmt_env_push_var (env : fmt_env) (var : var) : fmt_env = + (* Only push the binding if the name is not [None] *) + match var.basename with + | None -> env + | Some name -> { env with vars = VarId.Map.add var.id name env.vars } + +let fmt_env_push_locals (env : fmt_env) (vars : var list) : fmt_env = + List.fold_left fmt_env_push_var env vars + +let var_id_to_pretty_string (id : var_id) : string = "^" ^ VarId.to_string id let type_var_id_to_string (env : fmt_env) (id : type_var_id) : string = (* Note that the types are not necessarily ordered following their indices *) @@ -41,12 +50,9 @@ let const_generic_var_id_to_string (env : fmt_env) (id : const_generic_var_id) : | Some x -> Print.Types.const_generic_var_to_string x let var_id_to_string (env : fmt_env) (id : VarId.id) : string = - match List.find_opt (fun (i, _) -> i = id) env.locals with + match VarId.Map.find_opt id env.vars with | None -> var_id_to_pretty_string id - | Some (_, name) -> ( - match name with - | None -> var_id_to_pretty_string id - | Some name -> name ^ "^" ^ VarId.to_string id) + | Some name -> name ^ "^" ^ VarId.to_string id let trait_clause_id_to_string = Print.Types.trait_clause_id_to_string @@ -70,7 +76,7 @@ let decls_ctx_to_fmt_env (ctx : Contexts.decls_ctx) : fmt_env = trait_decls = ctx.trait_decls_ctx.trait_decls; trait_impls = ctx.trait_impls_ctx.trait_impls; generics = empty_generic_params; - locals = []; + vars = VarId.Map.empty; } let name_to_string (env : fmt_env) = @@ -356,115 +362,125 @@ let adt_field_to_string ?(span = None) (env : fmt_env) (adt_id : type_id) (* Enumerations: we can't get there *) craise_opt_span __FILE__ __LINE__ span "Unreachable") -(** TODO: we don't need a general function anymore (it is now only used for - patterns) - *) -let adt_g_value_to_string ?(span : Meta.span option = None) (env : fmt_env) - (value_to_string : 'v -> string) (variant_id : VariantId.id option) - (field_values : 'v list) (ty : ty) : string = - let field_values = List.map value_to_string field_values in - match ty with - | TAdt (TTuple, _) -> - (* Tuple *) - "(" ^ String.concat ", " field_values ^ ")" - | TAdt (TAdtId def_id, _) -> - (* "Regular" ADT *) - let adt_ident = - match variant_id with - | Some vid -> adt_variant_from_type_decl_id_to_string env def_id vid - | None -> type_decl_id_to_string env def_id - in - if field_values <> [] then - match adt_field_names env def_id variant_id with - | None -> - let field_values = String.concat ", " field_values in - adt_ident ^ " (" ^ field_values ^ ")" - | Some field_names -> - let field_values = List.combine field_names field_values in - let field_values = - List.map - (fun (field, value) -> field ^ " = " ^ value ^ ";") - field_values - in - let field_values = String.concat " " field_values in - adt_ident ^ " { " ^ field_values ^ " }" - else adt_ident - | TAdt (TBuiltin aty, _) -> ( - (* Builtin type *) - match aty with - | TState | TRawPtr _ -> - (* This type is opaque: we can't get there *) - craise_opt_span __FILE__ __LINE__ span "Unreachable" - | TResult -> - let variant_id = Option.get variant_id in - if variant_id = result_ok_id then - match field_values with - | [ v ] -> "@Result::Return " ^ v - | _ -> - craise_opt_span __FILE__ __LINE__ span - "Result::Return takes exactly one value" - else if variant_id = result_fail_id then - match field_values with - | [ v ] -> "@Result::Fail " ^ v - | _ -> - craise_opt_span __FILE__ __LINE__ span - "Result::Fail takes exactly one value" - else - craise_opt_span __FILE__ __LINE__ span - "Unreachable: improper variant id for result type" - | TError -> - cassert_opt_span __FILE__ __LINE__ (field_values = []) span - "Ill-formed error value"; - 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" - else - craise_opt_span __FILE__ __LINE__ span - "Unreachable: improper variant id for error type" - | TFuel -> - let variant_id = Option.get variant_id in - if variant_id = fuel_zero_id then ( - cassert_opt_span __FILE__ __LINE__ (field_values = []) span - "Ill-formed full value"; - "@Fuel::Zero") - else if variant_id = fuel_succ_id then - match field_values with - | [ v ] -> "@Fuel::Succ " ^ v - | _ -> - craise_opt_span __FILE__ __LINE__ span - "@Fuel::Succ takes exactly one value" - else - craise_opt_span __FILE__ __LINE__ span - "Unreachable: improper variant id for fuel type" - | TArray | TSlice | TStr -> - cassert_opt_span __FILE__ __LINE__ (variant_id = None) span - "Ill-formed value"; - let field_values = - List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values - in - let id = builtin_ty_to_string aty in - id ^ " [" ^ String.concat "; " field_values ^ "]") - | _ -> - craise_opt_span __FILE__ __LINE__ span - ("Inconsistently typed value: expected ADT type but found:" ^ "\n- ty: " - ^ ty_to_string env false ty ^ "\n- variant_id: " - ^ Print.option_to_string VariantId.to_string variant_id) - -let rec typed_pattern_to_string ?(span : Meta.span option = None) - (env : fmt_env) (v : typed_pattern) : string = +let rec typed_pattern_to_string_aux (span : Meta.span option) (env : fmt_env) + (v : typed_pattern) : fmt_env * string = match v.value with - | PatConstant cv -> literal_to_string cv - | PatVar (v, None) -> var_to_string env v + | PatConstant cv -> (env, literal_to_string cv) + | PatVar (v, None) -> (fmt_env_push_var env v, var_to_string env v) | PatVar (v, Some mp) -> let mp = "[@mplace=" ^ mplace_to_string env mp ^ "]" in - "(" ^ var_to_varname v ^ " " ^ mp ^ " : " - ^ ty_to_string env false v.ty - ^ ")" - | PatDummy -> "_" + let env = fmt_env_push_var env v in + let s = + "(" ^ var_to_varname v ^ " " ^ mp ^ " : " + ^ ty_to_string env false v.ty + ^ ")" + in + (env, s) + | PatDummy -> (env, "_") | PatAdt av -> - adt_g_value_to_string ~span env - (typed_pattern_to_string ~span env) - av.variant_id av.field_values v.ty + adt_pattern_to_string span env av.variant_id av.field_values v.ty + +(* TODO: can't make the [span] parameter optional because OCaml infers its type + to be [span option option]?? *) +and adt_pattern_to_string (span : Meta.span option) (env : fmt_env) + (variant_id : VariantId.id option) (field_values : typed_pattern list) + (ty : ty) : fmt_env * string = + let env, field_values = + List.fold_left_map (typed_pattern_to_string_aux span) env field_values + in + let s = + match ty with + | TAdt (TTuple, _) -> + (* Tuple *) + "(" ^ String.concat ", " field_values ^ ")" + | TAdt (TAdtId def_id, _) -> + (* "Regular" ADT *) + let adt_ident = + match variant_id with + | Some vid -> adt_variant_from_type_decl_id_to_string env def_id vid + | None -> type_decl_id_to_string env def_id + in + if field_values <> [] then + match adt_field_names env def_id variant_id with + | None -> + let field_values = String.concat ", " field_values in + adt_ident ^ " (" ^ field_values ^ ")" + | Some field_names -> + let field_values = List.combine field_names field_values in + let field_values = + List.map + (fun (field, value) -> field ^ " = " ^ value ^ ";") + field_values + in + let field_values = String.concat " " field_values in + adt_ident ^ " { " ^ field_values ^ " }" + else adt_ident + | TAdt (TBuiltin aty, _) -> ( + (* Builtin type *) + match aty with + | TState | TRawPtr _ -> + (* This type is opaque: we can't get there *) + craise_opt_span __FILE__ __LINE__ span "Unreachable" + | TResult -> + let variant_id = Option.get variant_id in + if variant_id = result_ok_id then + match field_values with + | [ v ] -> "@Result::Return " ^ v + | _ -> + craise_opt_span __FILE__ __LINE__ span + "Result::Return takes exactly one value" + else if variant_id = result_fail_id then + match field_values with + | [ v ] -> "@Result::Fail " ^ v + | _ -> + craise_opt_span __FILE__ __LINE__ span + "Result::Fail takes exactly one value" + else + craise_opt_span __FILE__ __LINE__ span + "Unreachable: improper variant id for result type" + | TError -> + cassert_opt_span __FILE__ __LINE__ (field_values = []) span + "Ill-formed error value"; + 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" + else + craise_opt_span __FILE__ __LINE__ span + "Unreachable: improper variant id for error type" + | TFuel -> + let variant_id = Option.get variant_id in + if variant_id = fuel_zero_id then ( + cassert_opt_span __FILE__ __LINE__ (field_values = []) span + "Ill-formed full value"; + "@Fuel::Zero") + else if variant_id = fuel_succ_id then + match field_values with + | [ v ] -> "@Fuel::Succ " ^ v + | _ -> + craise_opt_span __FILE__ __LINE__ span + "@Fuel::Succ takes exactly one value" + else + craise_opt_span __FILE__ __LINE__ span + "Unreachable: improper variant id for fuel type" + | TArray | TSlice | TStr -> + cassert_opt_span __FILE__ __LINE__ (variant_id = None) span + "Ill-formed value"; + let field_values = + List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values + in + let id = builtin_ty_to_string aty in + id ^ " [" ^ String.concat "; " field_values ^ "]") + | _ -> + craise_opt_span __FILE__ __LINE__ span + ("Inconsistently typed value: expected ADT type but found:" + ^ "\n- ty: " ^ ty_to_string env false ty ^ "\n- variant_id: " + ^ Print.option_to_string VariantId.to_string variant_id) + in + (env, s) + +let typed_pattern_to_string ?(span : Meta.span option = None) (env : fmt_env) + (v : typed_pattern) : string = + snd (typed_pattern_to_string_aux span env v) let fun_sig_to_string (env : fmt_env) (sg : fun_sig) : string = let env = { env with generics = sg.generics } in @@ -638,7 +654,7 @@ and app_to_string ?(span : Meta.span option = None) (env : fmt_env) and lambda_to_string ?(span : Meta.span option = None) (env : fmt_env) (indent : string) (indent_incr : string) (xl : typed_pattern list) (e : texpression) : string = - let xl = List.map (typed_pattern_to_string ~span env) xl in + let env, xl = List.fold_left_map (typed_pattern_to_string_aux span) env xl in let e = texpression_to_string ~span env false indent indent_incr e in "λ " ^ String.concat " " xl ^ ". " ^ e @@ -648,8 +664,8 @@ and let_to_string ?(span : Meta.span option = None) (env : fmt_env) let indent1 = indent ^ indent_incr in let inside = false in let re = texpression_to_string ~span env inside indent1 indent_incr re in + let env, lv = typed_pattern_to_string_aux span env lv in let e = texpression_to_string ~span env inside indent indent_incr e in - let lv = typed_pattern_to_string ~span env lv in if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e @@ -663,17 +679,19 @@ and switch_to_string ?(span : Meta.span option = None) (env : fmt_env) let scrut = texpression_to_string ~span env true indent1 indent_incr scrutinee in - let e_to_string = texpression_to_string ~span env false indent1 indent_incr in + let e_to_string env = + texpression_to_string ~span env false indent1 indent_incr + in match body with | If (e_true, e_false) -> - let e_true = e_to_string e_true in - let e_false = e_to_string e_false in + let e_true = e_to_string env e_true in + let e_false = e_to_string env e_false in "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent1 ^ e_true ^ "\n" ^ indent ^ "else\n" ^ indent1 ^ e_false | Match branches -> let branch_to_string (b : match_branch) : string = - let pat = typed_pattern_to_string ~span env b.pat in - indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ e_to_string b.branch + let env, pat = typed_pattern_to_string_aux span env b.pat in + indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ e_to_string env b.branch in let branches = List.map branch_to_string branches in "match " ^ scrut ^ " with\n" ^ String.concat "\n" branches diff --git a/src/pure/PureMicroPasses.ml b/src/pure/PureMicroPasses.ml index b0a29526..2b4f92c3 100644 --- a/src/pure/PureMicroPasses.ml +++ b/src/pure/PureMicroPasses.ml @@ -606,6 +606,103 @@ let remove_span (def : fun_decl) : fun_decl = let body = { body with body = PureUtils.remove_span body.body } in { def with body = Some body } +(** Simplify the let-bindings which bind the fields of structures. + + For instance, given the following structure definition: + {[ + struct Struct { + x : u32, + y : u32, + } + ]} + + We perform the following transformation: + {[ + let StructCons x y = s in + ... + + ~~> + + let x = s.x in + let y = s.y in + ... + ]} + + Of course, this is not always possible depending on the backend. + Also, recursive structures, and more specifically structures mutually recursive + with inductives, are usually not supported. We define such recursive structures + as inductives, in which case it is not always possible to use a notation + for the field projections. + + The subsequent passes, in particular the ones which inline the useless + assignments, simplify this further. + *) +let simplify_decompose_struct (ctx : trans_ctx) (def : fun_decl) : fun_decl = + let span = def.item_meta.span in + let visitor = + object + inherit [_] map_expression as super + + method! visit_Let env (monadic : bool) (lv : typed_pattern) + (scrutinee : texpression) (next : texpression) = + match (lv.value, lv.ty) with + | PatAdt adt_pat, TAdt (TAdtId adt_id, generics) -> + (* Detect if this is an enumeration or not *) + let tdef = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in + let is_enum = TypesUtils.type_decl_is_enum tdef in + (* We deconstruct the ADT with a single let-binding in two situations: + - if the ADT is an enumeration (which must have exactly one branch) + - if we forbid using field projectors + *) + let use_let_with_cons = + is_enum + || !Config.dont_use_field_projectors + (* Also, there is a special case when the ADT is to be extracted as + a tuple, because it is a structure with unnamed fields. Some backends + like Lean have projectors for tuples (like so: `x.3`), but others + like Coq don't, in which case we have to deconstruct the whole ADT + at once (`let (a, b, c) = x in`) *) + || TypesUtils.type_decl_from_type_id_is_tuple_struct + ctx.type_ctx.type_infos (T.TAdtId adt_id) + && not !Config.use_tuple_projectors + in + if use_let_with_cons then + super#visit_Let env monadic lv scrutinee next + else + (* This is not an enumeration: introduce let-bindings for every + field. + We use the [dest] variable in order not to have to recompute + the type of the result of the projection... *) + let gen_field_proj (field_id : FieldId.id) (dest : typed_pattern) + : texpression = + let proj_kind = { adt_id = TAdtId adt_id; field_id } in + let qualif = { id = Proj proj_kind; generics } in + let proj_e = Qualif qualif in + let proj_ty = mk_arrow scrutinee.ty dest.ty in + let proj = { e = proj_e; ty = proj_ty } in + mk_app span proj scrutinee + in + let id_var_pairs = + FieldId.mapi (fun fid v -> (fid, v)) adt_pat.field_values + in + let monadic = false in + let e = + List.fold_right + (fun (fid, pat) e -> + let field_proj = gen_field_proj fid pat in + mk_let monadic pat field_proj e) + id_var_pairs next + in + (super#visit_texpression env e).e + | _ -> super#visit_Let env monadic lv scrutinee next + end + in + match def.body with + | None -> def + | Some body -> + let body = { body with body = visitor#visit_texpression () body.body } in + { def with body = Some body } + (** Introduce the special structure create/update expressions. Upon generating the pure code, we introduce structure values by using @@ -625,7 +722,7 @@ let remove_span (def : fun_decl) : fun_decl = structure is to be extracted as a tuple. *) let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = - let obj = + let visitor = object (self) inherit [_] map_expression as super @@ -691,7 +788,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = match def.body with | None -> def | Some body -> - let body = { body with body = obj#visit_texpression () body.body } in + let body = { body with body = visitor#visit_texpression () body.body } in { def with body = Some body } (** Simplify the let-bindings by performing the following rewritings: @@ -743,7 +840,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = ... ]} *) -let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl = +let simplify_let_bindings (ctx : trans_ctx) (def : fun_decl) : fun_decl = let obj = object (self) inherit [_] map_expression as super @@ -810,7 +907,20 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl = | _ -> false in if List.for_all check_pat_arg (List.combine pats args) then - self#visit_Let env monadic lv g next + (* Check if the application is a tuple constructor + or will be extracted as a projector: if + it is, keep the lambdas, otherwise simplify *) + let simplify = + match g.e with + | Qualif { id = AdtCons { adt_id; _ }; _ } -> + not + (PureUtils.type_decl_from_type_id_is_tuple_struct + ctx.type_ctx.type_infos adt_id) + | Qualif { id = Proj _; _ } -> false + | _ -> true + in + if simplify then self#visit_Let env monadic lv g next + else super#visit_Let env monadic lv rv next else super#visit_Let env monadic lv rv next else super#visit_Let env monadic lv rv next else super#visit_Let env monadic lv rv next @@ -2175,6 +2285,10 @@ let end_passes : (* Convert the unit variables to [()] if they are used as right-values or * [_] if they are used as left values. *) (None, "unit_vars_to_unit", fun _ -> unit_vars_to_unit); + (* Simplify the let-bindings which bind the fields of ADTs + which only have one variant (i.e., enumerations with one variant + and structures). *) + (None, "simplify_decompose_struct", simplify_decompose_struct); (* Introduce the special structure create/update expressions *) (None, "intro_struct_updates", intro_struct_updates); (* Simplify the let-bindings *) diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index 3d717f0d..81bac9aa 100644 --- a/src/symbolic/SymbolicToPure.ml +++ b/src/symbolic/SymbolicToPure.ml @@ -1,4 +1,3 @@ -open Utils open LlbcAstUtils open Pure open PureUtils @@ -319,7 +318,7 @@ let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env = trait_decls; trait_impls; generics; - locals = []; + vars = VarId.Map.empty; } let ctx_generic_args_to_string (ctx : bs_ctx) (args : T.generic_args) : string = @@ -377,6 +376,14 @@ let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.typed_pattern_to_string ~span:(Some ctx.span) env p +let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = + let env = bs_ctx_to_fmt_env ctx in + let verbose = false in + let indent = "" in + let indent_incr = " " in + Print.Values.abs_to_string ~span:(Some ctx.span) env verbose indent + indent_incr abs + let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) : fun_effect_info = match bid with @@ -388,15 +395,6 @@ let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) : let ctx_get_effect_info (ctx : bs_ctx) : fun_effect_info = ctx_get_effect_info_for_bid ctx ctx.bid -(* TODO: move *) -let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = - let env = bs_ctx_to_fmt_env ctx in - let verbose = false in - let indent = "" in - let indent_incr = " " in - Print.Values.abs_to_string ~span:(Some ctx.span) env verbose indent - indent_incr abs - let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = TypeDeclId.Map.find id ctx.type_ctx.llbc_type_decls @@ -664,15 +662,16 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let env = Print.Contexts.decls_ctx_to_fmt_env ctx in let def_id = def.T.def_id in let name = Print.Types.name_to_string env def.item_meta.name in - (* Can't translate types with regions for now *) + let span = def.item_meta.span in + (* Can't translate types with nested borrows for now *) cassert __FILE__ __LINE__ - (def.generics.regions = []) - def.item_meta.span "ADTs containing borrows are not supported yet"; - let generics, preds = - translate_generic_params (Some def.item_meta.span) def.generics - in + (not + (TypesUtils.type_decl_has_nested_borrows (Some span) + ctx.type_ctx.type_infos def)) + span "ADTs containing borrows are not supported yet"; + let generics, preds = translate_generic_params (Some span) def.generics in let explicit_info = compute_explicit_info generics [] in - let kind = translate_type_decl_kind def.item_meta.span def.T.kind in + let kind = translate_type_decl_kind span def.T.kind in let item_meta = def.item_meta in { def_id; @@ -731,7 +730,7 @@ let rec translate_fwd_ty (span : Meta.span option) (type_infos : type_infos) cassert_opt_span __FILE__ __LINE__ (not (List.exists - (TypesUtils.ty_has_borrows type_infos) + (TypesUtils.ty_has_borrows span type_infos) generics.types)) span "ADTs containing borrows are not supported yet"; match t_generics.types with @@ -809,24 +808,26 @@ let rec translate_back_ty (span : Meta.span option) (type_infos : type_infos) translate_fwd_generic_args span type_infos generics in Some (TAdt (type_id, generics)) - else - (* If not inside a mutable reference: check if at least one - of the generics contains a mutable reference (i.e., is not - translated to `None`. If yes, keep the whole type, and - translate all the generics as "forward" types (the backward - function will extract the proper information from the ADT value) + else if + (* If not inside a mutable reference: check if the type contains + a mutable reference (through one of its generics, inside + its definition, etc.). + If yes, keep the whole type, and translate all the generics as + "forward" types (the backward function will extract the proper + information from the ADT value). *) - let types = List.filter_map translate generics.types in - if types <> [] then - let generics = - translate_fwd_generic_args span type_infos generics - in - Some (TAdt (type_id, generics)) - else None + TypesUtils.ty_has_mut_borrow_for_region_in_pred type_infos + keep_region ty + then + let generics = + translate_fwd_generic_args span type_infos generics + in + Some (TAdt (type_id, generics)) + else None | TBuiltin TBox -> ( (* Don't accept ADTs (which are not tuples) with borrows for now *) cassert_opt_span __FILE__ __LINE__ - (not (TypesUtils.ty_has_borrows type_infos ty)) + (not (TypesUtils.ty_has_borrows span type_infos ty)) span "ADTs containing borrows are not supported yet"; (* Eliminate the box *) match generics.types with @@ -835,14 +836,21 @@ let rec translate_back_ty (span : Meta.span option) (type_infos : type_infos) craise_opt_span __FILE__ __LINE__ span "Unreachable: boxes receive exactly one type parameter") | TTuple -> ( - (* Tuples can contain borrows (which we eliminate) *) - let tys_t = List.filter_map translate generics.types in - match tys_t with - | [] -> None - | _ -> - (* Note that if there is exactly one type, [mk_simpl_tuple_ty] - * is the identity *) - Some (mk_simpl_tuple_ty tys_t))) + if inside_mut then + (* We do not filter anything *) + let tys_t = + List.map (translate_fwd_ty span type_infos) generics.types + in + Some (mk_simpl_tuple_ty tys_t) + else + (* Tuples can contain borrows (which we eliminate) *) + let tys_t = List.filter_map translate generics.types in + match tys_t with + | [] -> None + | _ -> + (* Note that if there is exactly one type, [mk_simpl_tuple_ty] + * is the identity *) + Some (mk_simpl_tuple_ty tys_t))) | TVar vid -> wrap (TVar vid) | TNever -> craise_opt_span __FILE__ __LINE__ span "Unreachable" | TLiteral lty -> wrap (TLiteral lty) @@ -1152,6 +1160,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let _, rid_subst, r_subst = Substitute.fresh_regions_with_substs_from_vars ~fail_if_not_found:true sg.generics.regions + (snd (T.RegionId.fresh_stateful_generator ())) in let subst = { Substitute.empty_subst with r_subst } in let ty = Substitute.ty_substitute subst ty in @@ -1162,7 +1171,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed in let keep_region r = match r with - | T.RStatic -> raise Unimplemented + | T.RStatic -> craise_opt_span __FILE__ __LINE__ span "Unimplemented" | RErased -> craise_opt_span __FILE__ __LINE__ span "Unexpected erased region" | RBVar _ -> @@ -1173,7 +1182,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed translate_back_ty span type_infos keep_region inside_mut ty in let translate_back_inputs_for_gid (gid : T.RegionGroupId.id) : ty list = - (* For now we don't supported nested borrows, so we check that there + (* For now we don't support nested borrows, so we check that there aren't parent regions *) let parents = list_ancestor_region_groups regions_hierarchy gid in cassert_opt_span __FILE__ __LINE__ @@ -1199,7 +1208,10 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let inputs = Print.list_to_string (PrintPure.ty_to_string pctx false) inputs in - "translate_back_inputs_for_gid:" ^ "\n- gid: " + "translate_back_inputs_for_gid:" ^ "\n- function:" + ^ Charon.PrintExpressions.fun_id_or_trait_method_ref_to_string ctx + fun_id + ^ "\n- gid: " ^ RegionGroupId.to_string gid ^ "\n- output: " ^ output ^ "\n- back inputs: " ^ inputs ^ "\n")); inputs @@ -1237,7 +1249,10 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let outputs = Print.list_to_string (PrintPure.ty_to_string pctx false) outputs in - "compute_back_outputs_for_gid:" ^ "\n- gid: " + "compute_back_outputs_for_gid:" ^ "\n- function:" + ^ Charon.PrintExpressions.fun_id_or_trait_method_ref_to_string ctx + fun_id + ^ "\n- gid: " ^ RegionGroupId.to_string gid ^ "\n- inputs: " ^ inputs ^ "\n- back outputs: " ^ outputs ^ "\n")); (names, outputs) @@ -1752,7 +1767,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) translate sv | VReservedMutBorrow bid -> (* Same as for shared borrows. However, note that we use reserved borrows - * only in *span-data*: a value *actually used* in the translation can't come + * only in *meta-data*: a value *actually used* in the translation can't come * from an unpromoted reserved borrow *) let sv = InterpreterBorrowsCore.lookup_shared_value ctx.span ectx bid @@ -1775,8 +1790,100 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (* Return *) value +type borrow_kind = BMut | BShared + +(** An avalue is either produced from a borrow projector (if it is an input + to a function) or from a loan projector (if it is an ouptput). + This means that an avalue has either: + - only borrows and borrow projections over symbolic values + - only loans and loan projections over symbolic values + - none of those + + **REMARK:** this will not be valid anymore once we have nested borrows, + as an ended proj loan can contain borrows in one of its children. + In this situation, we will need to first project the avalues at the proper + level, before translating them. + *) +type typed_avalue_kind = + | BorrowProj of borrow_kind + (** The value was produced by a borrow projector (it contains borrows + or borrow projections). + + The kind is [BMut] if we found at least one (non-ignored) mutable + borrow, [BShared] otherwise. + *) + | LoanProj of borrow_kind + (** The value was produced by a loan projector (it contains loans or + loan projections). + + The kind is [BMut] if we found at least one (non-ignored) mutable loan, + [BShared] otherwise. + *) + | UnknownProj + (** No borrows, loans or projections inside the value so we can't know for sure *) + +let compute_typed_avalue_proj_kind span (av : V.typed_avalue) : + typed_avalue_kind = + let has_borrows = ref false in + let has_mut_borrows = ref false in + let has_loans = ref false in + let has_mut_loans = ref false in + let visitor = + object + inherit [_] V.iter_typed_avalue as super + + method! visit_ALoan env lc = + has_loans := true; + begin + match lc with + | ASharedLoan _ + | AEndedSharedLoan _ + | AIgnoredMutLoan _ + | AEndedIgnoredMutLoan _ + | AIgnoredSharedLoan _ -> () + | AMutLoan _ | AEndedMutLoan _ -> has_mut_loans := true + end; + (* Continue exploring as a sanity check: we want to make sure we don't find borrows *) + super#visit_ALoan env lc + + method! visit_ABorrow env bc = + has_borrows := true; + begin + match bc with + | ASharedBorrow _ + | AEndedSharedBorrow + | AIgnoredMutBorrow _ + | AEndedIgnoredMutBorrow _ + | AProjSharedBorrow _ -> () + | AMutBorrow _ | AEndedMutBorrow _ -> has_mut_borrows := true + end; + (* Continue exploring as a sanity check: we want to make sure we don't find loans *) + super#visit_ABorrow env bc + + method! visit_ASymbolic env aproj = + match aproj with + | V.AEndedProjLoans (_, _) | AProjLoans (_, _) -> + has_loans := true; + (* Continue exploring (same reasons as above) *) + super#visit_ASymbolic env aproj + | AEndedProjBorrows _ | AIgnoredProjBorrows | AProjBorrows (_, _) -> + has_borrows := true; + (* Continue exploring (same reasons as above) *) + super#visit_ASymbolic env aproj + end + in + visitor#visit_typed_avalue () av; + cassert __FILE__ __LINE__ + ((not !has_borrows) || not !has_loans) + span "Unreachable"; + let to_borrow_kind b = if b then BMut else BShared in + if !has_borrows then BorrowProj (to_borrow_kind !has_mut_borrows) + else if !has_loans then LoanProj (to_borrow_kind !has_mut_loans) + else UnknownProj + (** Explore an abstraction value and convert it to a consumed value by collecting all the meta-values from the ended *loans*. + We assume the avalue was generated by a loan projector. Consumed values are rvalues because when an abstraction ends we introduce a call to a backward function in the synthesized program, @@ -1790,34 +1897,30 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) ^^ ]} *) -let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) - (av : V.typed_avalue) : texpression option = - let translate = typed_avalue_to_consumed ctx ectx in +let rec typed_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx) + (ectx : C.eval_ctx) (av : V.typed_avalue) : texpression option = let value = match av.value with - | AAdt adt_v -> ( - (* Translate the field values *) - let field_values = List.filter_map translate adt_v.field_values in - (* For now, only tuples can contain borrows *) - let adt_id, _ = TypesUtils.ty_as_adt av.ty in - match adt_id with - | TAdtId _ | TBuiltin (TBox | TArray | TSlice | TStr) -> - cassert __FILE__ __LINE__ (field_values = []) ctx.span - "ADTs containing borrows are not supported yet"; - None - | TTuple -> - (* Return *) - if field_values = [] then None - else - (* Note that if there is exactly one field value, - * [mk_simpl_tuple_rvalue] is the identity *) - let rv = mk_simpl_tuple_texpression ctx.span field_values in - Some rv) + | AAdt adt_v -> adt_avalue_to_consumed_aux ~filter ctx ectx av adt_v | ABottom -> craise __FILE__ __LINE__ ctx.span "Unreachable" - | ALoan lc -> aloan_content_to_consumed ctx ectx lc - | ABorrow bc -> aborrow_content_to_consumed ctx bc - | ASymbolic aproj -> aproj_to_consumed ctx aproj - | AIgnored -> None + | ALoan lc -> aloan_content_to_consumed_aux ~filter ctx ectx lc + | ABorrow _ -> + (* This value should have been generated by a loan projector: there + can't be aborrows unless there are nested borrows, which are not + supported yet. *) + craise __FILE__ __LINE__ ctx.span "Unreachable" + | ASymbolic aproj -> aproj_to_consumed_aux ctx aproj + | AIgnored mv -> ( + if filter then None + else + (* If we do not filter it means we are inside an ADT: in this case, + the meta-value was produced by a projector (and not introduced + because of a join, because when doing joins we destructure the + values): there **must** be a meta-value. The consumed value + is the meta-value. *) + match mv with + | None -> craise __FILE__ __LINE__ ctx.span "Unreachable" + | Some mv -> Some (typed_value_to_texpression ctx ectx mv)) in (* Sanity check - Rk.: we do this at every recursive call, which is a bit * expansive... *) @@ -1827,46 +1930,124 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (* Return *) value -and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) - (lc : V.aloan_content) : texpression option = +and adt_avalue_to_consumed_aux ~(filter : bool) (ctx : bs_ctx) + (ectx : C.eval_ctx) (av : V.typed_avalue) (adt_v : V.adt_avalue) : + texpression option = + (* We do not do the same thing depending on whether we visit a tuple + or a "regular" ADT *) + let adt_id, _ = TypesUtils.ty_as_adt av.ty in + (* Check if the ADT contains borrows *) + match compute_typed_avalue_proj_kind ctx.span av with + | BorrowProj _ -> craise __FILE__ __LINE__ ctx.span "Unreachable" + | UnknownProj -> + (* If we filter: ignore the value. + Otherwise, translate everything. *) + if filter then None + else + let fields = + List.map + (typed_avalue_to_consumed_aux ~filter ctx ectx) + adt_v.field_values + in + let fields = List.map Option.get fields in + begin + match adt_id with + | TAdtId _ | TBuiltin (TBox | TArray | TSlice | TStr) -> + let ty = + translate_fwd_ty (Some ctx.span) ctx.type_ctx.type_infos av.ty + in + Some (mk_adt_value ctx.span ty adt_v.variant_id fields) + | TTuple -> Some (mk_simpl_tuple_texpression ctx.span fields) + end + | LoanProj borrow_kind -> begin + (* Translate the field values *) + let field_values = + let filter = + filter + && + match adt_id with + | TTuple | TBuiltin TBox -> true + | TBuiltin _ | TAdtId _ -> borrow_kind = BShared + in + List.map + (typed_avalue_to_consumed_aux ~filter ctx ectx) + adt_v.field_values + in + match adt_id with + | TAdtId _ -> + (* We should preserve all the fields *) + let fields = List.map Option.get field_values in + let ty = + translate_fwd_ty (Some ctx.span) ctx.type_ctx.type_infos av.ty + in + let pat = mk_adt_value ctx.span ty adt_v.variant_id fields in + Some pat + | TBuiltin TBox -> begin + (* The box type becomes the identity in the translation *) + match field_values with + | [ v ] -> v + | _ -> craise __FILE__ __LINE__ ctx.span "Unreachable" + end + | TBuiltin (TArray | TSlice | TStr) -> + (* This case is unreachable: + - for array and slice: in order to access one of their elements + we need to go through an index function + - for strings: the [str] is not polymorphic. + *) + craise __FILE__ __LINE__ ctx.span "Unreachable" + | TTuple -> + (* If the filtering is activated, we ignore the fields which do not + consume values (i.e., which do not contain ended mutable borrows). *) + if filter then + let field_values = List.filter_map (fun x -> x) field_values in + if field_values = [] then None + else + (* Note that if there is exactly one field value, + * [mk_simpl_tuple_rvalue] is the identity *) + let rv = mk_simpl_tuple_texpression ctx.span field_values in + Some rv + else + (* If we do not filter the fields, all the values should be [Some ...] *) + let field_values = List.map Option.get field_values in + let v = mk_simpl_tuple_texpression ctx.span field_values in + Some v + end + +and aloan_content_to_consumed_aux ~(filter : bool) (ctx : bs_ctx) + (ectx : C.eval_ctx) (lc : V.aloan_content) : texpression option = match lc with | AMutLoan (_, _, _) | ASharedLoan (_, _, _, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable" - | AEndedMutLoan { child = _; given_back = _; given_back_span } -> + | AEndedMutLoan { child; given_back; given_back_meta } -> + cassert __FILE__ __LINE__ + (ValuesUtils.is_aignored child.value) + ctx.span "Unreachable"; + cassert __FILE__ __LINE__ + (ValuesUtils.is_aignored given_back.value) + ctx.span "Unreachable"; (* Return the meta-value *) - Some (typed_value_to_texpression ctx ectx given_back_span) - | AEndedSharedLoan (_, _) -> - (* We don't dive into shared loans: there is nothing to give back - * inside (note that there could be a mutable borrow in the shared - * value, pointing to a mutable loan in the child avalue, but this - * borrow is in practice immutable) *) - None + Some (typed_value_to_texpression ctx ectx given_back_meta) + | AEndedSharedLoan (sv, child) -> + cassert __FILE__ __LINE__ + (ValuesUtils.is_aignored child.value) + ctx.span "Unreachable"; + (* We don't diveinto shared loans: there is nothing to give back + inside (note that there could be a mutable borrow in the shared + value, pointing to a mutable loan in the child avalue, but this + borrow is in practice immutable) *) + if filter then None else Some (typed_value_to_texpression ctx ectx sv) | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) craise __FILE__ __LINE__ ctx.span "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) - raise Unimplemented + craise __FILE__ __LINE__ ctx.span "Unimplemented" | AIgnoredSharedLoan _ -> - (* Ignore *) - None - -and aborrow_content_to_consumed (ctx : bs_ctx) (bc : V.aborrow_content) : - texpression option = - match bc with - | V.AMutBorrow (_, _, _) | ASharedBorrow (_, _) | AIgnoredMutBorrow (_, _) -> - craise __FILE__ __LINE__ ctx.span "Unreachable" - | AEndedMutBorrow (_, _) -> - (* We collect consumed values: ignore *) - None - | AEndedIgnoredMutBorrow _ -> - (* This happens with nested borrows: we need to dive in *) - raise Unimplemented - | AEndedSharedBorrow | AProjSharedBorrow _ -> - (* Ignore *) - None + (* This case only happens with nested borrows *) + craise __FILE__ __LINE__ ctx.span "Unimplemented" -and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = +and aproj_to_consumed_aux (ctx : bs_ctx) (aproj : V.aproj) : texpression option + = match aproj with | V.AEndedProjLoans (msv, []) -> (* The symbolic value was left unchanged *) @@ -1878,21 +2059,45 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = (* The symbolic value was updated *) Some (symbolic_value_to_texpression ctx mnv) | V.AEndedProjLoans (_, _) -> - (* The symbolic value was updated, and the given back values come from sevearl - * abstractions *) - raise Unimplemented - | AEndedProjBorrows _ -> (* We consider consumed values *) None + (* The symbolic value was updated, and the given back values come from several + abstractions *) + craise __FILE__ __LINE__ ctx.span "Unimplemented" + | AEndedProjBorrows _ -> + (* The value should have been introduced by a loan projector, and should not + contain nested borrows, so we can't get there *) + craise __FILE__ __LINE__ ctx.span "Unreachable" | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable" +let typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) + (av : V.typed_avalue) : texpression option = + (* Check if the value was generated from a loan projector: if yes, and if + it contains mutable loans, then we generate a consumed value (because + upon ending the borrow we consumed a value). + Otherwise we ignore it. *) + match compute_typed_avalue_proj_kind ctx.span av with + | LoanProj BMut -> typed_avalue_to_consumed_aux ~filter:true ctx ectx av + | LoanProj BShared | BorrowProj _ | UnknownProj -> + (* If it is a borrow proj we ignore it. If it is an unknown projection, + it means the value doesn't contain loans nor borrows, so nothing + is consumed upon ending the abstraction: we can ignore it as well. *) + None + (** Convert the abstraction values in an abstraction to consumed values. - See [typed_avalue_to_consumed]. + See [typed_avalue_to_consumed_aux]. *) let abs_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) : texpression list = log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs)); - List.filter_map (typed_avalue_to_consumed ctx ectx) abs.avalues + let values = + List.filter_map (typed_avalue_to_consumed ctx ectx) abs.avalues + in + log#ldebug + (lazy + ("abs_to_consumed:\n- abs: " ^ abs_to_string ctx abs ^ "\n- values: " + ^ Print.list_to_string (texpression_to_string ctx) values)); + values let translate_mprojection_elem (pe : E.projection_elem) : mprojection_elem option = @@ -1916,62 +2121,45 @@ let translate_opt_mplace (p : S.mplace option) : mplace option = | None -> None | Some p -> Some (translate_mplace p) -(** Explore an abstraction value and convert it to a given back value - by collecting all the meta-values from the ended *borrows*. +(** Explore an abstraction value which we know **was generated by a borrow projection** + (this means we won't find loans or loan projectors inside it) and convert it to a + given back value by collecting all the meta-values from the ended *borrows*. - Given back values are patterns, because when an abstraction ends, we - introduce a call to a backward function in the synthesized program, - which introduces new values: + Note that given back values are patterns, because when an abstraction ends we + introduce a call to a backward function in the synthesized program, which introduces + new values: {[ let (nx, ny) = f_back ... in ^^^^^^^^ ]} - [mp]: it is possible to provide some span-place information, to guide + [mp]: it is possible to provide some meta-place information, to guide the heuristics which later find pretty names for the variables. + + - [under_mut]: if [true] it means we are below a mutable borrow. + This influences whether we filter values or not. *) -let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) - (ctx : bs_ctx) : bs_ctx * typed_pattern option = - let ctx, value = +let rec typed_avalue_to_given_back_aux ~(filter : bool) (mp : mplace option) + (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_pattern option = + let (ctx, value) : _ * typed_pattern option = match av.value with - | AAdt adt_v -> ( - (* Translate the field values *) - (* For now we forget the span-place information so that it doesn't get used - * by several fields (which would then all have the same name...), but we - * might want to do something smarter *) - let mp = None in - let ctx, field_values = - List.fold_left_map - (fun ctx fv -> typed_avalue_to_given_back mp fv ctx) - ctx adt_v.field_values - in - let field_values = List.filter_map (fun x -> x) field_values in - (* For now, only tuples can contain borrows - note that if we gave - * something like a [&mut Vec] to a function, we give back the - * vector value upon visiting the "abstraction borrow" node *) - let adt_id, _ = TypesUtils.ty_as_adt av.ty in - match adt_id with - | TAdtId _ | TBuiltin (TBox | TArray | TSlice | TStr) -> - cassert __FILE__ __LINE__ (field_values = []) ctx.span - "ADTs with borrows are not supported yet"; - (ctx, None) - | TTuple -> - (* Return *) - let variant_id = adt_v.variant_id in - sanity_check __FILE__ __LINE__ (variant_id = None) ctx.span; - if field_values = [] then (ctx, None) - else - (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern] - * is the identity *) - let lv = mk_simpl_tuple_pattern field_values in - (ctx, Some lv)) + | AAdt adt_v -> adt_avalue_to_given_back_aux ~filter av adt_v ctx | ABottom -> craise __FILE__ __LINE__ ctx.span "Unreachable" - | ALoan lc -> aloan_content_to_given_back mp lc ctx - | ABorrow bc -> aborrow_content_to_given_back mp bc ctx - | ASymbolic aproj -> aproj_to_given_back mp aproj ctx - | AIgnored -> (ctx, None) + | ALoan _ -> + (* The avalue should have been generated by a borrow projector: this case is unreachable *) + craise __FILE__ __LINE__ ctx.span "Unreachable" + | ABorrow bc -> aborrow_content_to_given_back_aux ~filter mp bc av.ty ctx + | ASymbolic aproj -> aproj_to_given_back_aux mp aproj ctx + | AIgnored _ -> + (* If we do not filter, we have to create a dummy pattern *) + if filter then (ctx, None) + else + let ty = + translate_fwd_ty (Some ctx.span) ctx.type_ctx.type_infos av.ty + in + (ctx, Some (mk_dummy_pattern ty)) in - (* Sanity check - Rk.: we do this at every recursive call, which is a bit + (* Sanity checks - Rk.: we do this at every recursive call, which is a bit * expansive... *) (match value with | None -> () @@ -1979,53 +2167,108 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) (* Return *) (ctx, value) -and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) - (ctx : bs_ctx) : bs_ctx * typed_pattern option = - match lc with - | AMutLoan (_, _, _) | ASharedLoan (_, _, _, _) -> - craise __FILE__ __LINE__ ctx.span "Unreachable" - | AEndedMutLoan { child = _; given_back = _; given_back_span = _ } - | AEndedSharedLoan (_, _) -> - (* We consider given back values, and thus ignore those *) - (ctx, None) - | AIgnoredMutLoan (_, _) -> - (* There can be *inner* not ended mutable loans, but not outer ones *) - craise __FILE__ __LINE__ ctx.span "Unreachable" - | AEndedIgnoredMutLoan _ -> - (* This happens with nested borrows: we need to dive in *) - raise Unimplemented - | AIgnoredSharedLoan _ -> - (* Ignore *) - (ctx, None) +and adt_avalue_to_given_back_aux ~(filter : bool) (av : V.typed_avalue) + (adt_v : V.adt_avalue) (ctx : bs_ctx) : bs_ctx * typed_pattern option = + (* Check if the ADT contains borrows *) + match compute_typed_avalue_proj_kind ctx.span av with + | LoanProj _ -> craise __FILE__ __LINE__ ctx.span "Unreachable" + | UnknownProj -> + (* If we filter: ignore the pattern. + Otherwise, return a dummy value. *) + if filter then (ctx, None) + else + let ty = + translate_fwd_ty (Some ctx.span) ctx.type_ctx.type_infos av.ty + in + (ctx, Some (mk_dummy_pattern ty)) + | BorrowProj borrow_kind -> begin + (* We do not do the same thing depending on whether we visit a tuple + or a "regular" ADT *) + let adt_id, _ = TypesUtils.ty_as_adt av.ty in + (* Translate the field values *) + (* For now we forget the meta-place information so that it doesn't get used + by several fields (which would then all have the same name...), but we + might want to do something smarter *) + let mp = None in + let ctx, field_values = + let filter = + filter + && + match adt_id with + | TTuple | TBuiltin TBox -> true + | TBuiltin _ | TAdtId _ -> borrow_kind = BShared + in + List.fold_left_map + (fun ctx fv -> typed_avalue_to_given_back_aux ~filter mp fv ctx) + ctx adt_v.field_values + in + match adt_id with + | TAdtId _ -> + (* None of the fields must have been ignored *) + let fields = List.map Option.get field_values in + let adt_ty = + translate_fwd_ty (Some ctx.span) ctx.type_ctx.type_infos av.ty + in + let pat = mk_adt_pattern adt_ty adt_v.variant_id fields in + (ctx, Some pat) + | TBuiltin TBox -> begin + (* The box type becomes the identity in the translation *) + match field_values with + | [ pat ] -> (ctx, pat) + | _ -> craise __FILE__ __LINE__ ctx.span "Unreachable" + end + | TBuiltin (TArray | TSlice | TStr) -> + (* This case is unreachable: + - for array and slice: in order to access one of their elements + we need to go through an index function + - for strings: the [str] is not polymorphic. + *) + craise __FILE__ __LINE__ ctx.span "Unreachable" + | TTuple -> + (* Sanity checks *) + let variant_id = adt_v.variant_id in + sanity_check __FILE__ __LINE__ (variant_id = None) ctx.span; + (* If the filtering is activated, we ignore the fields which do not + give values back (i.e., which do not contain mutable borrows). *) + if filter then + let field_values = List.filter_map (fun x -> x) field_values in + if field_values = [] then (ctx, None) + else + (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern] + * is the identity *) + let lv = mk_simpl_tuple_pattern field_values in + (ctx, Some lv) + else + (* If we do not filter the fields, all the patterns should be [Some ...] *) + let field_values = List.map Option.get field_values in + let lv = mk_simpl_tuple_pattern field_values in + (ctx, Some lv) + end -and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) - (ctx : bs_ctx) : bs_ctx * typed_pattern option = +and aborrow_content_to_given_back_aux ~(filter : bool) (mp : mplace option) + (bc : V.aborrow_content) (ty : T.ty) (ctx : bs_ctx) : + bs_ctx * typed_pattern option = match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow (_, _) | AIgnoredMutBorrow (_, _) -> + (* All the borrows should have been ended upon ending the abstraction *) craise __FILE__ __LINE__ ctx.span "Unreachable" | AEndedMutBorrow (msv, _) -> - (* Return the span-symbolic-value *) + (* Return the meta symbolic-value *) let ctx, var = fresh_var_for_symbolic_value msv ctx in (ctx, Some (mk_typed_pattern_from_var var mp)) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) - raise Unimplemented + craise __FILE__ __LINE__ ctx.span "Unimplemented" | AEndedSharedBorrow | AProjSharedBorrow _ -> - (* Ignore *) - (ctx, None) + if filter then (ctx, None) + else + let ty = translate_fwd_ty (Some ctx.span) ctx.type_ctx.type_infos ty in + (ctx, Some (mk_dummy_pattern ty)) -and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : - bs_ctx * typed_pattern option = +and aproj_to_given_back_aux (mp : mplace option) (aproj : V.aproj) + (ctx : bs_ctx) : bs_ctx * typed_pattern option = match aproj with - | V.AEndedProjLoans (_, child_projs) -> - (* There may be children borrow projections in case of nested borrows, - * in which case we need to dive in - we disallow nested borrows for now *) - cassert __FILE__ __LINE__ - (List.for_all - (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) - child_projs) - ctx.span "Nested borrows are not supported yet"; - (ctx, None) + | V.AEndedProjLoans (_, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable" | AEndedProjBorrows mv -> (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in @@ -2033,6 +2276,20 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable" +let typed_avalue_to_given_back (mp : mplace option) (v : V.typed_avalue) + (ctx : bs_ctx) : bs_ctx * typed_pattern option = + (* Check if the value was generated from a borrow projector: if yes, and if + it contains mutable borrows we generate a given back pattern (because + upon ending the borrow the abstraction gave back a value). + Otherwise we ignore it. *) + match compute_typed_avalue_proj_kind ctx.span v with + | BorrowProj BMut -> typed_avalue_to_given_back_aux mp ~filter:true v ctx + | BorrowProj BShared | LoanProj _ | UnknownProj -> + (* If it is a loan proj we ignore it. If it is an unknown projection, + it means the value doesn't contain loans nor borrows, so nothing + is given back: we can ignore it as well. *) + (ctx, None) + (** Convert the abstraction values in an abstraction to given back values. See [typed_avalue_to_given_back]. @@ -2050,6 +2307,10 @@ let abs_to_given_back (mpl : mplace option list option) (abs : V.abs) ctx avalues in let values = List.filter_map (fun x -> x) values in + log#ldebug + (lazy + ("abs_to_given_back:\n- abs: " ^ abs_to_string ctx abs ^ "\n- values: " + ^ Print.list_to_string (typed_pattern_to_string ctx) values)); (ctx, values) (** Simply calls [abs_to_given_back] *) @@ -2069,7 +2330,7 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) : let abs_ancestors = list_ancestor_abstractions ctx abs call_id in (call_info.forward, abs_ancestors) -(** Add span-information to an expression *) +(** Add meta-information to an expression *) let mk_espan_symbolic_assignments (vars : var list) (values : texpression list) (e : texpression) : texpression = let var_values = List.combine (List.map var_get_id vars) values in @@ -2624,7 +2885,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) let back_inputs = List.append back_inputs back_state in (* Retrieve the values given back by this function: those are the output * values. We rely on the fact that there are no nested borrows to use the - * span-place information from the input values given to the forward function + * meta-place information from the input values given to the forward function * (we need to add [None] for the return avalue) *) let output_mpl = List.append (List.map translate_opt_mplace call.args_places) [ None ] @@ -2686,6 +2947,8 @@ and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression = + log#ldebug + (lazy ("Translating ended synthesis abstraction: " ^ abs_to_string ctx abs)); (* If we end the abstraction which consumed the return value of the function we are synthesizing, we get back the borrows which were inside. Those borrows are actually input arguments of the backward function we are synthesizing. @@ -2717,16 +2980,24 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) (* First, retrieve the list of variables used for the inputs for the * backward function *) let inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs_no_state in + log#ldebug + (lazy + ("Consumed inputs: " + ^ Print.list_to_string (pure_var_to_string ctx) inputs)); (* Retrieve the values consumed upon ending the loans inside this * abstraction: as there are no nested borrows, there should be none. *) let consumed = abs_to_consumed ctx ectx abs in cassert __FILE__ __LINE__ (consumed = []) ctx.span "Nested borrows are not supported yet"; (* Retrieve the values given back upon ending this abstraction - note that - * we don't provide span-place information, because those assignments will + * we don't provide meta-place information, because those assignments will * be inlined anyway... *) log#ldebug (lazy ("abs: " ^ abs_to_string ctx abs)); let ctx, given_back = abs_to_given_back_no_mp abs ctx in + log#ldebug + (lazy + ("given back: " + ^ Print.list_to_string (typed_pattern_to_string ctx) given_back)); (* Link the inputs to those given back values - note that this also * checks we have the same number of values, of course *) let given_back_inputs = List.combine given_back inputs in @@ -2827,7 +3098,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) | None -> next_e | Some func -> let call = mk_apps ctx.span func args in - (* Add span-information - this is slightly hacky: we look at the + (* Add meta-information - this is slightly hacky: we look at the values consumed by the abstraction (note that those come from *before* we applied the fixed-point context) and use them to guide the naming of the output vars. @@ -3008,26 +3279,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) (* Translate and [ExpandAdt] when there is no branching (i.e., one branch). - There are several possibilities: - - if the ADT is an enumeration, we attempt to deconstruct it with a let-binding: + We generate something of the shape: {[ let Cons x0 ... xn = y in ... ]} - - - if the ADT is a structure, we attempt to introduce one let-binding per field: - {[ - let x0 = y.f0 in - ... - let xn = y.fn in - ... - ]} - - Of course, this is not always possible depending on the backend. - Also, recursive structures, and more specifically structures mutually recursive - with inductives, are usually not supported. We define such recursive structures - as inductives, in which case it is not always possible to use a notation - for the field projections. *) and translate_ExpandAdt_one_branch (sv : V.symbolic_value) (scrutinee : texpression) (scrutinee_mplace : mplace option) @@ -3039,56 +3295,13 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) let ctx, vars = fresh_vars_for_symbolic_values svl ctx in let branch = translate_expression branch ctx in match type_id with - | TAdtId adt_id -> - (* Detect if this is an enumeration or not *) - let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in - let is_enum = TypesUtils.type_decl_is_enum tdef in - (* We deconstruct the ADT with a single let-binding in two situations: - - if the ADT is an enumeration (which must have exactly one branch) - - if we forbid using field projectors. - *) - let use_let_with_cons = - is_enum - || !Config.dont_use_field_projectors - (* Also, there is a special case when the ADT is to be extracted as - a tuple, because it is a structure with unnamed fields. Some backends - like Lean have projectors for tuples (like so: `x.3`), but others - like Coq don't, in which case we have to deconstruct the whole ADT - at once (`let (a, b, c) = x in`) *) - || TypesUtils.type_decl_from_type_id_is_tuple_struct - ctx.type_ctx.type_infos type_id - && not !Config.use_tuple_projectors - in - if use_let_with_cons then - (* Introduce a let binding which expands the ADT *) - let lvars = List.map (fun v -> mk_typed_pattern_from_var v None) vars in - let lv = mk_adt_pattern scrutinee.ty variant_id lvars in - let monadic = false in - - mk_let monadic lv - (mk_opt_mplace_texpression scrutinee_mplace scrutinee) - branch - else - (* This is not an enumeration: introduce let-bindings for every - * field. - * We use the [dest] variable in order not to have to recompute - * the type of the result of the projection... *) - let adt_id, generics = ty_as_adt ctx.span scrutinee.ty in - let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression = - let proj_kind = { adt_id; field_id } in - let qualif = { id = Proj proj_kind; generics } in - let proj_e = Qualif qualif in - let proj_ty = mk_arrow scrutinee.ty dest.ty in - let proj = { e = proj_e; ty = proj_ty } in - mk_app ctx.span proj scrutinee - in - let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in - let monadic = false in - List.fold_right - (fun (fid, var) e -> - let field_proj = gen_field_proj fid var in - mk_let monadic (mk_typed_pattern_from_var var None) field_proj e) - id_var_pairs branch + | TAdtId _ -> + let lvars = List.map (fun v -> mk_typed_pattern_from_var v None) vars in + let lv = mk_adt_pattern scrutinee.ty variant_id lvars in + let monadic = false in + mk_let monadic lv + (mk_opt_mplace_texpression scrutinee_mplace scrutinee) + branch | TTuple -> let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in let monadic = false in @@ -3535,7 +3748,7 @@ and translate_forward_end (ectx : C.eval_ctx) (* Create the let expression with the loop call *) let e = mk_let effect_info.can_fail out_pat loop_call next_e in - (* Add span-information linking the loop input parameters and the + (* Add meta-information linking the loop input parameters and the loop input values - we use this to derive proper names. There is something important here: as we group the end of the function @@ -3607,7 +3820,9 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = List.map (fun ty -> cassert __FILE__ __LINE__ - (not (TypesUtils.ty_has_borrows ctx.type_ctx.type_infos ty)) + (not + (TypesUtils.ty_has_borrows (Some ctx.span) + ctx.type_ctx.type_infos ty)) ctx.span "The types shouldn't contain borrows"; ctx_translate_fwd_ty ctx ty) tys) diff --git a/tests/coq/misc/AdtBorrows.v b/tests/coq/misc/AdtBorrows.v new file mode 100644 index 00000000..f4ffe58e --- /dev/null +++ b/tests/coq/misc/AdtBorrows.v @@ -0,0 +1,159 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [adt_borrows] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module AdtBorrows. + +(** [adt_borrows::SharedWrapper] + Source: 'tests/src/adt-borrows.rs', lines 4:0-4:35 *) +Definition SharedWrapper_t (T : Type) : Type := T. + +(** [adt_borrows::{adt_borrows::SharedWrapper<'a, T>}::create]: + Source: 'tests/src/adt-borrows.rs', lines 7:4-9:5 *) +Definition sharedWrapper_create + {T : Type} (x : T) : result (SharedWrapper_t T) := + Ok x +. + +(** [adt_borrows::{adt_borrows::SharedWrapper<'a, T>}::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 11:4-13:5 *) +Definition sharedWrapper_unwrap + {T : Type} (self : SharedWrapper_t T) : result T := + Ok self +. + +(** [adt_borrows::SharedWrapper1] + Source: 'tests/src/adt-borrows.rs', lines 16:0-18:1 *) +Record SharedWrapper1_t (T : Type) := +mkSharedWrapper1_t { + sharedWrapper1_x : T; +} +. + +Arguments mkSharedWrapper1_t { _ }. +Arguments sharedWrapper1_x { _ }. + +(** [adt_borrows::{adt_borrows::SharedWrapper1<'a, T>}#1::create]: + Source: 'tests/src/adt-borrows.rs', lines 21:4-23:5 *) +Definition sharedWrapper1_create + {T : Type} (x : T) : result (SharedWrapper1_t T) := + Ok {| sharedWrapper1_x := x |} +. + +(** [adt_borrows::{adt_borrows::SharedWrapper1<'a, T>}#1::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 25:4-27:5 *) +Definition sharedWrapper1_unwrap + {T : Type} (self : SharedWrapper1_t T) : result T := + Ok self.(sharedWrapper1_x) +. + +(** [adt_borrows::SharedWrapper2] + Source: 'tests/src/adt-borrows.rs', lines 30:0-33:1 *) +Record SharedWrapper2_t (T : Type) := +mkSharedWrapper2_t { + sharedWrapper2_x : T; sharedWrapper2_y : T; +} +. + +Arguments mkSharedWrapper2_t { _ }. +Arguments sharedWrapper2_x { _ }. +Arguments sharedWrapper2_y { _ }. + +(** [adt_borrows::{adt_borrows::SharedWrapper2<'a, 'b, T>}#2::create]: + Source: 'tests/src/adt-borrows.rs', lines 36:4-38:5 *) +Definition sharedWrapper2_create + {T : Type} (x : T) (y : T) : result (SharedWrapper2_t T) := + Ok {| sharedWrapper2_x := x; sharedWrapper2_y := y |} +. + +(** [adt_borrows::{adt_borrows::SharedWrapper2<'a, 'b, T>}#2::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 40:4-42:5 *) +Definition sharedWrapper2_unwrap + {T : Type} (self : SharedWrapper2_t T) : result (T * T) := + Ok (self.(sharedWrapper2_x), self.(sharedWrapper2_y)) +. + +(** [adt_borrows::MutWrapper] + Source: 'tests/src/adt-borrows.rs', lines 45:0-45:36 *) +Definition MutWrapper_t (T : Type) : Type := T. + +(** [adt_borrows::{adt_borrows::MutWrapper<'a, T>}#3::create]: + Source: 'tests/src/adt-borrows.rs', lines 48:4-50:5 *) +Definition mutWrapper_create + {T : Type} (x : T) : result ((MutWrapper_t T) * (MutWrapper_t T -> T)) := + let back := fun (ret : MutWrapper_t T) => ret in Ok (x, back) +. + +(** [adt_borrows::{adt_borrows::MutWrapper<'a, T>}#3::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 52:4-54:5 *) +Definition mutWrapper_unwrap + {T : Type} (self : MutWrapper_t T) : result (T * (T -> MutWrapper_t T)) := + let back := fun (ret : T) => ret in Ok (self, back) +. + +(** [adt_borrows::MutWrapper1] + Source: 'tests/src/adt-borrows.rs', lines 57:0-59:1 *) +Record MutWrapper1_t (T : Type) := mkMutWrapper1_t { mutWrapper1_x : T; }. + +Arguments mkMutWrapper1_t { _ }. +Arguments mutWrapper1_x { _ }. + +(** [adt_borrows::{adt_borrows::MutWrapper1<'a, T>}#4::create]: + Source: 'tests/src/adt-borrows.rs', lines 62:4-64:5 *) +Definition mutWrapper1_create + {T : Type} (x : T) : result ((MutWrapper1_t T) * (MutWrapper1_t T -> T)) := + let back := fun (ret : MutWrapper1_t T) => ret.(mutWrapper1_x) in + Ok ({| mutWrapper1_x := x |}, back) +. + +(** [adt_borrows::{adt_borrows::MutWrapper1<'a, T>}#4::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 66:4-68:5 *) +Definition mutWrapper1_unwrap + {T : Type} (self : MutWrapper1_t T) : result (T * (T -> MutWrapper1_t T)) := + let back := fun (ret : T) => {| mutWrapper1_x := ret |} in + Ok (self.(mutWrapper1_x), back) +. + +(** [adt_borrows::MutWrapper2] + Source: 'tests/src/adt-borrows.rs', lines 71:0-74:1 *) +Record MutWrapper2_t (T : Type) := +mkMutWrapper2_t { + mutWrapper2_x : T; mutWrapper2_y : T; +} +. + +Arguments mkMutWrapper2_t { _ }. +Arguments mutWrapper2_x { _ }. +Arguments mutWrapper2_y { _ }. + +(** [adt_borrows::{adt_borrows::MutWrapper2<'a, 'b, T>}#5::create]: + Source: 'tests/src/adt-borrows.rs', lines 77:4-79:5 *) +Definition mutWrapper2_create + {T : Type} (x : T) (y : T) : + result ((MutWrapper2_t T) * (MutWrapper2_t T -> T) * (MutWrapper2_t T -> T)) + := + let back'a := fun (ret : MutWrapper2_t T) => ret.(mutWrapper2_x) in + let back'b := fun (ret : MutWrapper2_t T) => ret.(mutWrapper2_y) in + Ok ({| mutWrapper2_x := x; mutWrapper2_y := y |}, back'a, back'b) +. + +(** [adt_borrows::{adt_borrows::MutWrapper2<'a, 'b, T>}#5::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 81:4-83:5 *) +Definition mutWrapper2_unwrap + {T : Type} (self : MutWrapper2_t T) : + result ((T * T) * (T -> MutWrapper2_t T) * (T -> MutWrapper2_t T)) + := + let back'a := + fun (ret : T) => + {| mutWrapper2_x := ret; mutWrapper2_y := self.(mutWrapper2_y) |} in + let back'b := + fun (ret : T) => + {| mutWrapper2_x := self.(mutWrapper2_x); mutWrapper2_y := ret |} in + Ok ((self.(mutWrapper2_x), self.(mutWrapper2_y)), back'a, back'b) +. + +End AdtBorrows. diff --git a/tests/coq/misc/Issue270LoopList.v b/tests/coq/misc/Issue270LoopList.v index aabf65c8..0be6e80e 100644 --- a/tests/coq/misc/Issue270LoopList.v +++ b/tests/coq/misc/Issue270LoopList.v @@ -19,13 +19,13 @@ Arguments List_Cons { _ }. Arguments List_Nil { _ }. (** [issue_270_loop_list::foo]: loop 0: - Source: 'tests/src/issue-270-loop-list.rs', lines 11:8-14:9 *) + Source: 'tests/src/issue-270-loop-list.rs', lines 10:8-12:9 *) Fixpoint foo_loop (t : List_t (List_t u8)) : result unit := match t with | List_Cons _ tt1 => foo_loop tt1 | List_Nil => Ok tt end . (** [issue_270_loop_list::foo]: - Source: 'tests/src/issue-270-loop-list.rs', lines 8:0-16:1 *) + Source: 'tests/src/issue-270-loop-list.rs', lines 7:0-14:1 *) Definition foo (v : List_t (List_t u8)) : result unit := match v with | List_Cons l t => foo_loop t | List_Nil => Ok tt end . diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 6d5cae43..7c3b7a7a 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -600,19 +600,28 @@ Definition not_u32 (x : u32) : result u32 := Definition not_i32 (x : i32) : result i32 := Ok (scalar_not x). +(** [no_nested_borrows::borrow_mut_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 532:0-534:1 *) +Definition borrow_mut_tuple + {T : Type} {U : Type} (x : (T * U)) : + result ((T * U) * ((T * U) -> (T * U))) + := + let back := fun (ret : (T * U)) => ret in Ok (x, back) +. + (** [no_nested_borrows::ExpandSimpliy::Wrapper] - Source: 'tests/src/no_nested_borrows.rs', lines 534:4-534:32 *) + Source: 'tests/src/no_nested_borrows.rs', lines 538:4-538:32 *) Definition ExpandSimpliy_Wrapper_t (T : Type) : Type := T * T. (** [no_nested_borrows::ExpandSimpliy::check_expand_simplify_symb1]: - Source: 'tests/src/no_nested_borrows.rs', lines 536:4-542:5 *) + Source: 'tests/src/no_nested_borrows.rs', lines 540:4-546:5 *) Definition expandSimpliy_check_expand_simplify_symb1 (x : ExpandSimpliy_Wrapper_t bool) : result (ExpandSimpliy_Wrapper_t bool) := let (b, b1) := x in if b then Ok x else Ok x . (** [no_nested_borrows::ExpandSimpliy::Wrapper2] - Source: 'tests/src/no_nested_borrows.rs', lines 544:4-547:5 *) + Source: 'tests/src/no_nested_borrows.rs', lines 548:4-551:5 *) Record ExpandSimpliy_Wrapper2_t := mkExpandSimpliy_Wrapper2_t { expandSimpliy_Wrapper2_b : bool; expandSimpliy_Wrapper2_x : u32; @@ -620,7 +629,7 @@ mkExpandSimpliy_Wrapper2_t { . (** [no_nested_borrows::ExpandSimpliy::check_expand_simplify_symb2]: - Source: 'tests/src/no_nested_borrows.rs', lines 549:4-555:5 *) + Source: 'tests/src/no_nested_borrows.rs', lines 553:4-559:5 *) Definition expandSimpliy_check_expand_simplify_symb2 (x : ExpandSimpliy_Wrapper2_t) : result ExpandSimpliy_Wrapper2_t := if x.(expandSimpliy_Wrapper2_b) diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index d455d49c..24efb46e 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -13,6 +13,7 @@ External_TypesExternal.v External_TypesExternal_Template.v InfiniteLoop.v Issue194RecursiveStructProjector.v +Issue270LoopList.v Loops.v NoNestedBorrows.v Paper.v diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index bb2d6fff..f21420ee 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -9,7 +9,7 @@ Local Open Scope Primitives_scope. Module Traits. (** Trait declaration: [traits::BoolTrait] - Source: 'tests/src/traits.rs', lines 2:0-10:1 *) + Source: 'tests/src/traits.rs', lines 3:0-11:1 *) Record BoolTrait_t (Self : Type) := mkBoolTrait_t { BoolTrait_t_get_bool : Self -> result bool; }. @@ -18,59 +18,59 @@ Arguments mkBoolTrait_t { _ }. Arguments BoolTrait_t_get_bool { _ } _. (** [traits::{traits::BoolTrait for bool}::get_bool]: - Source: 'tests/src/traits.rs', lines 13:4-15:5 *) + Source: 'tests/src/traits.rs', lines 14:4-16:5 *) Definition boolTraitBool_get_bool (self : bool) : result bool := Ok self. (** Trait implementation: [traits::{traits::BoolTrait for bool}] - Source: 'tests/src/traits.rs', lines 12:0-16:1 *) + Source: 'tests/src/traits.rs', lines 13:0-17:1 *) Definition BoolTraitBool : BoolTrait_t bool := {| BoolTrait_t_get_bool := boolTraitBool_get_bool; |}. (** [traits::BoolTrait::ret_true]: - Source: 'tests/src/traits.rs', lines 7:4-9:5 *) + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) Definition boolTrait_ret_true {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool := Ok true . (** [traits::test_bool_trait_bool]: - Source: 'tests/src/traits.rs', lines 18:0-20:1 *) + Source: 'tests/src/traits.rs', lines 19:0-21:1 *) Definition test_bool_trait_bool (x : bool) : result bool := b <- boolTraitBool_get_bool x; if b then boolTrait_ret_true BoolTraitBool x else Ok false . (** [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: - Source: 'tests/src/traits.rs', lines 24:4-29:5 *) + Source: 'tests/src/traits.rs', lines 25:4-30:5 *) Definition boolTraitOption_get_bool {T : Type} (self : option T) : result bool := match self with | None => Ok false | Some _ => Ok true end . (** Trait implementation: [traits::{traits::BoolTrait for core::option::Option}#1] - Source: 'tests/src/traits.rs', lines 23:0-30:1 *) + Source: 'tests/src/traits.rs', lines 24:0-31:1 *) Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {| BoolTrait_t_get_bool := boolTraitOption_get_bool; |}. (** [traits::test_bool_trait_option]: - Source: 'tests/src/traits.rs', lines 32:0-34:1 *) + Source: 'tests/src/traits.rs', lines 33:0-35:1 *) Definition test_bool_trait_option {T : Type} (x : option T) : result bool := b <- boolTraitOption_get_bool x; if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false . (** [traits::test_bool_trait]: - Source: 'tests/src/traits.rs', lines 36:0-38:1 *) + Source: 'tests/src/traits.rs', lines 37:0-39:1 *) Definition test_bool_trait {T : Type} (boolTraitInst : BoolTrait_t T) (x : T) : result bool := boolTraitInst.(BoolTrait_t_get_bool) x . (** Trait declaration: [traits::ToU64] - Source: 'tests/src/traits.rs', lines 40:0-42:1 *) + Source: 'tests/src/traits.rs', lines 41:0-43:1 *) Record ToU64_t (Self : Type) := mkToU64_t { ToU64_t_to_u64 : Self -> result u64; }. @@ -79,16 +79,16 @@ Arguments mkToU64_t { _ }. Arguments ToU64_t_to_u64 { _ } _. (** [traits::{traits::ToU64 for u64}#2::to_u64]: - Source: 'tests/src/traits.rs', lines 45:4-47:5 *) + Source: 'tests/src/traits.rs', lines 46:4-48:5 *) Definition toU64U64_to_u64 (self : u64) : result u64 := Ok self. (** Trait implementation: [traits::{traits::ToU64 for u64}#2] - Source: 'tests/src/traits.rs', lines 44:0-48:1 *) + Source: 'tests/src/traits.rs', lines 45:0-49:1 *) Definition ToU64U64 : ToU64_t u64 := {| ToU64_t_to_u64 := toU64U64_to_u64; |}. (** [traits::{traits::ToU64 for (A, A)}#3::to_u64]: - Source: 'tests/src/traits.rs', lines 51:4-53:5 *) + Source: 'tests/src/traits.rs', lines 52:4-54:5 *) Definition toU64Pair_to_u64 {A : Type} (toU64Inst : ToU64_t A) (self : (A * A)) : result u64 := let (t, t1) := self in @@ -98,65 +98,65 @@ Definition toU64Pair_to_u64 . (** Trait implementation: [traits::{traits::ToU64 for (A, A)}#3] - Source: 'tests/src/traits.rs', lines 50:0-54:1 *) + Source: 'tests/src/traits.rs', lines 51:0-55:1 *) Definition ToU64Pair {A : Type} (toU64Inst : ToU64_t A) : ToU64_t (A * A) := {| ToU64_t_to_u64 := toU64Pair_to_u64 toU64Inst; |}. (** [traits::f]: - Source: 'tests/src/traits.rs', lines 56:0-58:1 *) + Source: 'tests/src/traits.rs', lines 57:0-59:1 *) Definition f {T : Type} (toU64Inst : ToU64_t T) (x : (T * T)) : result u64 := toU64Pair_to_u64 toU64Inst x . (** [traits::g]: - Source: 'tests/src/traits.rs', lines 60:0-65:1 *) + Source: 'tests/src/traits.rs', lines 61:0-66:1 *) Definition g {T : Type} (toU64PairInst : ToU64_t (T * T)) (x : (T * T)) : result u64 := toU64PairInst.(ToU64_t_to_u64) x . (** [traits::h0]: - Source: 'tests/src/traits.rs', lines 67:0-69:1 *) + Source: 'tests/src/traits.rs', lines 68:0-70:1 *) Definition h0 (x : u64) : result u64 := toU64U64_to_u64 x. (** [traits::Wrapper] - Source: 'tests/src/traits.rs', lines 71:0-73:1 *) + Source: 'tests/src/traits.rs', lines 72:0-74:1 *) Record Wrapper_t (T : Type) := mkWrapper_t { wrapper_x : T; }. Arguments mkWrapper_t { _ }. Arguments wrapper_x { _ }. (** [traits::{traits::ToU64 for traits::Wrapper}#4::to_u64]: - Source: 'tests/src/traits.rs', lines 76:4-78:5 *) + Source: 'tests/src/traits.rs', lines 77:4-79:5 *) Definition toU64traitsWrapper_to_u64 {T : Type} (toU64Inst : ToU64_t T) (self : Wrapper_t T) : result u64 := toU64Inst.(ToU64_t_to_u64) self.(wrapper_x) . (** Trait implementation: [traits::{traits::ToU64 for traits::Wrapper}#4] - Source: 'tests/src/traits.rs', lines 75:0-79:1 *) + Source: 'tests/src/traits.rs', lines 76:0-80:1 *) Definition ToU64traitsWrapper {T : Type} (toU64Inst : ToU64_t T) : ToU64_t (Wrapper_t T) := {| ToU64_t_to_u64 := toU64traitsWrapper_to_u64 toU64Inst; |}. (** [traits::h1]: - Source: 'tests/src/traits.rs', lines 81:0-83:1 *) + Source: 'tests/src/traits.rs', lines 82:0-84:1 *) Definition h1 (x : Wrapper_t u64) : result u64 := toU64traitsWrapper_to_u64 ToU64U64 x . (** [traits::h2]: - Source: 'tests/src/traits.rs', lines 85:0-87:1 *) + Source: 'tests/src/traits.rs', lines 86:0-88:1 *) Definition h2 {T : Type} (toU64Inst : ToU64_t T) (x : Wrapper_t T) : result u64 := toU64traitsWrapper_to_u64 toU64Inst x . (** Trait declaration: [traits::ToType] - Source: 'tests/src/traits.rs', lines 89:0-91:1 *) + Source: 'tests/src/traits.rs', lines 90:0-92:1 *) Record ToType_t (Self : Type) (T : Type) := mkToType_t { ToType_t_to_type : Self -> result T; }. @@ -165,19 +165,19 @@ Arguments mkToType_t { _ } { _ }. Arguments ToType_t_to_type { _ } { _ } _. (** [traits::{traits::ToType for u64}#5::to_type]: - Source: 'tests/src/traits.rs', lines 94:4-96:5 *) + Source: 'tests/src/traits.rs', lines 95:4-97:5 *) Definition toTypeU64Bool_to_type (self : u64) : result bool := Ok (self s> 0%u64) . (** Trait implementation: [traits::{traits::ToType for u64}#5] - Source: 'tests/src/traits.rs', lines 93:0-97:1 *) + Source: 'tests/src/traits.rs', lines 94:0-98:1 *) Definition ToTypeU64Bool : ToType_t u64 bool := {| ToType_t_to_type := toTypeU64Bool_to_type; |}. (** Trait declaration: [traits::OfType] - Source: 'tests/src/traits.rs', lines 99:0-103:1 *) + Source: 'tests/src/traits.rs', lines 100:0-104:1 *) Record OfType_t (Self : Type) := mkOfType_t { OfType_t_of_type : forall {T : Type} (toTypeInst : ToType_t T Self), T -> result Self; @@ -187,7 +187,7 @@ Arguments mkOfType_t { _ }. Arguments OfType_t_of_type { _ } _ { _ }. (** [traits::h3]: - Source: 'tests/src/traits.rs', lines 105:0-107:1 *) + Source: 'tests/src/traits.rs', lines 106:0-108:1 *) Definition h3 {T1 : Type} {T2 : Type} (ofTypeInst : OfType_t T1) (toTypeInst : ToType_t T2 T1) (y : T2) : @@ -197,7 +197,7 @@ Definition h3 . (** Trait declaration: [traits::OfTypeBis] - Source: 'tests/src/traits.rs', lines 110:0-117:1 *) + Source: 'tests/src/traits.rs', lines 111:0-118:1 *) Record OfTypeBis_t (Self : Type) (T : Type) := mkOfTypeBis_t { OfTypeBis_tOfTypeBis_t_ToTypeInst : ToType_t T Self; OfTypeBis_t_of_type : T -> result Self; @@ -208,7 +208,7 @@ Arguments OfTypeBis_tOfTypeBis_t_ToTypeInst { _ } { _ } _. Arguments OfTypeBis_t_of_type { _ } { _ } _. (** [traits::h4]: - Source: 'tests/src/traits.rs', lines 119:0-121:1 *) + Source: 'tests/src/traits.rs', lines 120:0-122:1 *) Definition h4 {T1 : Type} {T2 : Type} (ofTypeBisInst : OfTypeBis_t T1 T2) (toTypeInst : ToType_t T2 T1) (y : T2) : @@ -218,15 +218,15 @@ Definition h4 . (** [traits::TestType] - Source: 'tests/src/traits.rs', lines 123:0-123:26 *) + Source: 'tests/src/traits.rs', lines 124:0-124:26 *) Definition TestType_t (T : Type) : Type := T. (** [traits::{traits::TestType}#6::test::TestType1] - Source: 'tests/src/traits.rs', lines 128:8-128:30 *) + Source: 'tests/src/traits.rs', lines 129:8-129:30 *) Definition TestType_test_TestType1_t : Type := u64. (** Trait declaration: [traits::{traits::TestType}#6::test::TestTrait] - Source: 'tests/src/traits.rs', lines 129:8-131:9 *) + Source: 'tests/src/traits.rs', lines 130:8-132:9 *) Record TestType_test_TestTrait_t (Self : Type) := mkTestType_test_TestTrait_t { TestType_test_TestTrait_t_test : Self -> result bool; }. @@ -235,14 +235,14 @@ Arguments mkTestType_test_TestTrait_t { _ }. Arguments TestType_test_TestTrait_t_test { _ } _. (** [traits::{traits::TestType}#6::test::{traits::{traits::TestType}#6::test::TestTrait for traits::{traits::TestType}#6::test::TestType1}::test]: - Source: 'tests/src/traits.rs', lines 140:12-142:13 *) + Source: 'tests/src/traits.rs', lines 141:12-143:13 *) Definition testType_test_TestTraittraitsTestTypetestTestType1_test (self : TestType_test_TestType1_t) : result bool := Ok (self s> 1%u64) . (** Trait implementation: [traits::{traits::TestType}#6::test::{traits::{traits::TestType}#6::test::TestTrait for traits::{traits::TestType}#6::test::TestType1}] - Source: 'tests/src/traits.rs', lines 139:8-143:9 *) + Source: 'tests/src/traits.rs', lines 140:8-144:9 *) Definition TestType_test_TestTraittraitsTestTypetestTestType1 : TestType_test_TestTrait_t TestType_test_TestType1_t := {| TestType_test_TestTrait_t_test := @@ -250,7 +250,7 @@ Definition TestType_test_TestTraittraitsTestTypetestTestType1 : |}. (** [traits::{traits::TestType}#6::test]: - Source: 'tests/src/traits.rs', lines 127:4-148:5 *) + Source: 'tests/src/traits.rs', lines 128:4-149:5 *) Definition testType_test {T : Type} (toU64Inst : ToU64_t T) (self : TestType_t T) (x : T) : result bool @@ -262,11 +262,11 @@ Definition testType_test . (** [traits::BoolWrapper] - Source: 'tests/src/traits.rs', lines 151:0-151:33 *) + Source: 'tests/src/traits.rs', lines 152:0-152:33 *) Definition BoolWrapper_t : Type := bool. (** [traits::{traits::ToType for traits::BoolWrapper}#7::to_type]: - Source: 'tests/src/traits.rs', lines 157:4-159:5 *) + Source: 'tests/src/traits.rs', lines 158:4-160:5 *) Definition toTypetraitsBoolWrapperT_to_type {T : Type} (toTypeBoolTInst : ToType_t bool T) (self : BoolWrapper_t) : result T @@ -275,14 +275,14 @@ Definition toTypetraitsBoolWrapperT_to_type . (** Trait implementation: [traits::{traits::ToType for traits::BoolWrapper}#7] - Source: 'tests/src/traits.rs', lines 153:0-160:1 *) + Source: 'tests/src/traits.rs', lines 154:0-161:1 *) Definition ToTypetraitsBoolWrapperT {T : Type} (toTypeBoolTInst : ToType_t bool T) : ToType_t BoolWrapper_t T := {| ToType_t_to_type := toTypetraitsBoolWrapperT_to_type toTypeBoolTInst; |}. (** [traits::WithConstTy::LEN2] - Source: 'tests/src/traits.rs', lines 165:4-165:27 *) + Source: 'tests/src/traits.rs', lines 166:4-166:27 *) Definition with_const_ty_len2_default_body (Self : Type) (LEN : usize) : result usize := Ok 32%usize @@ -292,7 +292,7 @@ Definition with_const_ty_len2_default (Self : Type) (LEN : usize) : usize := . (** Trait declaration: [traits::WithConstTy] - Source: 'tests/src/traits.rs', lines 162:0-173:1 *) + Source: 'tests/src/traits.rs', lines 163:0-174:1 *) Record WithConstTy_t (Self : Type) (LEN : usize) := mkWithConstTy_t { WithConstTy_tWithConstTy_t_LEN1 : usize; WithConstTy_tWithConstTy_t_LEN2 : usize; @@ -313,21 +313,21 @@ Arguments WithConstTy_tWithConstTy_t_ToU64traitsWithConstTyWInst { _ } { _ } _. Arguments WithConstTy_t_f { _ } { _ } _. (** [traits::{traits::WithConstTy<32: usize> for bool}#8::LEN1] - Source: 'tests/src/traits.rs', lines 176:4-176:27 *) + Source: 'tests/src/traits.rs', lines 177:4-177:27 *) Definition with_const_ty_bool32_len1_body : result usize := Ok 12%usize. Definition with_const_ty_bool32_len1 : usize := with_const_ty_bool32_len1_body%global . (** [traits::{traits::WithConstTy<32: usize> for bool}#8::f]: - Source: 'tests/src/traits.rs', lines 181:4-181:42 *) + Source: 'tests/src/traits.rs', lines 182:4-182:42 *) Definition withConstTyBool32_f (i : u64) (a : array u8 32%usize) : result u64 := Ok i . (** Trait implementation: [traits::{traits::WithConstTy<32: usize> for bool}#8] - Source: 'tests/src/traits.rs', lines 175:0-182:1 *) + Source: 'tests/src/traits.rs', lines 176:0-183:1 *) Definition WithConstTyBool32 : WithConstTy_t bool 32%usize := {| WithConstTy_tWithConstTy_t_LEN1 := with_const_ty_bool32_len1; WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_default bool 32%usize; @@ -338,7 +338,7 @@ Definition WithConstTyBool32 : WithConstTy_t bool 32%usize := {| |}. (** [traits::use_with_const_ty1]: - Source: 'tests/src/traits.rs', lines 184:0-186:1 *) + Source: 'tests/src/traits.rs', lines 185:0-187:1 *) Definition use_with_const_ty1 {H : Type} {LEN : usize} (withConstTyInst : WithConstTy_t H LEN) : result usize @@ -347,7 +347,7 @@ Definition use_with_const_ty1 . (** [traits::use_with_const_ty2]: - Source: 'tests/src/traits.rs', lines 188:0-188:76 *) + Source: 'tests/src/traits.rs', lines 189:0-189:76 *) Definition use_with_const_ty2 {H : Type} {LEN : usize} (withConstTyInst : WithConstTy_t H LEN) (w : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) : @@ -357,7 +357,7 @@ Definition use_with_const_ty2 . (** [traits::use_with_const_ty3]: - Source: 'tests/src/traits.rs', lines 190:0-192:1 *) + Source: 'tests/src/traits.rs', lines 191:0-193:1 *) Definition use_with_const_ty3 {H : Type} {LEN : usize} (withConstTyInst : WithConstTy_t H LEN) (x : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) : @@ -368,12 +368,12 @@ Definition use_with_const_ty3 . (** [traits::test_where1]: - Source: 'tests/src/traits.rs', lines 194:0-194:43 *) + Source: 'tests/src/traits.rs', lines 195:0-195:43 *) Definition test_where1 {T : Type} (_x : T) : result unit := Ok tt. (** [traits::test_where2]: - Source: 'tests/src/traits.rs', lines 195:0-195:60 *) + Source: 'tests/src/traits.rs', lines 196:0-196:60 *) Definition test_where2 {T : Type} (withConstTyT32Inst : WithConstTy_t T 32%usize) (_x : u32) : result unit @@ -382,7 +382,7 @@ Definition test_where2 . (** Trait declaration: [traits::ParentTrait0] - Source: 'tests/src/traits.rs', lines 201:0-205:1 *) + Source: 'tests/src/traits.rs', lines 202:0-206:1 *) Record ParentTrait0_t (Self : Type) := mkParentTrait0_t { ParentTrait0_tParentTrait0_t_W : Type; ParentTrait0_t_get_name : Self -> result string; @@ -395,13 +395,13 @@ Arguments ParentTrait0_t_get_name { _ } _. Arguments ParentTrait0_t_get_w { _ } _. (** Trait declaration: [traits::ParentTrait1] - Source: 'tests/src/traits.rs', lines 206:0-206:25 *) + Source: 'tests/src/traits.rs', lines 207:0-207:25 *) Record ParentTrait1_t (Self : Type) := mkParentTrait1_t{}. Arguments mkParentTrait1_t { _ }. (** Trait declaration: [traits::ChildTrait] - Source: 'tests/src/traits.rs', lines 207:0-207:52 *) + Source: 'tests/src/traits.rs', lines 208:0-208:52 *) Record ChildTrait_t (Self : Type) := mkChildTrait_t { ChildTrait_tChildTrait_t_ParentTrait0Inst : ParentTrait0_t Self; ChildTrait_tChildTrait_t_ParentTrait1Inst : ParentTrait1_t Self; @@ -412,7 +412,7 @@ Arguments ChildTrait_tChildTrait_t_ParentTrait0Inst { _ } _. Arguments ChildTrait_tChildTrait_t_ParentTrait1Inst { _ } _. (** [traits::test_child_trait1]: - Source: 'tests/src/traits.rs', lines 210:0-212:1 *) + Source: 'tests/src/traits.rs', lines 211:0-213:1 *) Definition test_child_trait1 {T : Type} (childTraitInst : ChildTrait_t T) (x : T) : result string := childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_t_get_name) @@ -420,7 +420,7 @@ Definition test_child_trait1 . (** [traits::test_child_trait2]: - Source: 'tests/src/traits.rs', lines 214:0-216:1 *) + Source: 'tests/src/traits.rs', lines 215:0-217:1 *) Definition test_child_trait2 {T : Type} (childTraitInst : ChildTrait_t T) (x : T) : result @@ -431,7 +431,7 @@ Definition test_child_trait2 . (** [traits::order1]: - Source: 'tests/src/traits.rs', lines 220:0-220:62 *) + Source: 'tests/src/traits.rs', lines 221:0-221:62 *) Definition order1 {T : Type} {U : Type} (parentTrait0Inst : ParentTrait0_t T) (parentTrait0Inst1 : ParentTrait0_t U) : @@ -441,7 +441,7 @@ Definition order1 . (** Trait declaration: [traits::ChildTrait1] - Source: 'tests/src/traits.rs', lines 223:0-223:38 *) + Source: 'tests/src/traits.rs', lines 224:0-224:38 *) Record ChildTrait1_t (Self : Type) := mkChildTrait1_t { ChildTrait1_tChildTrait1_t_ParentTrait1Inst : ParentTrait1_t Self; }. @@ -450,17 +450,17 @@ Arguments mkChildTrait1_t { _ }. Arguments ChildTrait1_tChildTrait1_t_ParentTrait1Inst { _ } _. (** Trait implementation: [traits::{traits::ParentTrait1 for usize}#9] - Source: 'tests/src/traits.rs', lines 225:0-225:30 *) + Source: 'tests/src/traits.rs', lines 226:0-226:30 *) Definition ParentTrait1Usize : ParentTrait1_t usize := mkParentTrait1_t. (** Trait implementation: [traits::{traits::ChildTrait1 for usize}#10] - Source: 'tests/src/traits.rs', lines 226:0-226:29 *) + Source: 'tests/src/traits.rs', lines 227:0-227:29 *) Definition ChildTrait1Usize : ChildTrait1_t usize := {| ChildTrait1_tChildTrait1_t_ParentTrait1Inst := ParentTrait1Usize; |}. (** Trait declaration: [traits::Iterator] - Source: 'tests/src/traits.rs', lines 230:0-232:1 *) + Source: 'tests/src/traits.rs', lines 231:0-233:1 *) Record Iterator_t (Self : Type) := mkIterator_t { Iterator_tIterator_t_Item : Type; }. @@ -469,7 +469,7 @@ Arguments mkIterator_t { _ }. Arguments Iterator_tIterator_t_Item { _ } _. (** Trait declaration: [traits::IntoIterator] - Source: 'tests/src/traits.rs', lines 234:0-240:1 *) + Source: 'tests/src/traits.rs', lines 235:0-241:1 *) Record IntoIterator_t (Self : Type) := mkIntoIterator_t { IntoIterator_tIntoIterator_t_Item : Type; IntoIterator_tIntoIterator_t_IntoIter : Type; @@ -487,13 +487,13 @@ Arguments IntoIterator_tIntoIterator_t_IteratortraitsIntoIteratorIntoIterInst Arguments IntoIterator_t_into_iter { _ } _. (** Trait declaration: [traits::FromResidual] - Source: 'tests/src/traits.rs', lines 251:0-251:24 *) + Source: 'tests/src/traits.rs', lines 252:0-252:24 *) Record FromResidual_t (Self : Type) (T : Type) := mkFromResidual_t{}. Arguments mkFromResidual_t { _ } { _ }. (** Trait declaration: [traits::Try] - Source: 'tests/src/traits.rs', lines 247:0-249:1 *) + Source: 'tests/src/traits.rs', lines 248:0-250:1 *) Record Try_t (Self : Type) := mkTry_t { Try_tTry_t_Residual : Type; Try_tTry_t_FromResidualSelftraitsTryResidualInst : FromResidual_t Self @@ -505,7 +505,7 @@ Arguments Try_tTry_t_Residual { _ } _. Arguments Try_tTry_t_FromResidualSelftraitsTryResidualInst { _ } _. (** Trait declaration: [traits::WithTarget] - Source: 'tests/src/traits.rs', lines 253:0-255:1 *) + Source: 'tests/src/traits.rs', lines 254:0-256:1 *) Record WithTarget_t (Self : Type) := mkWithTarget_t { WithTarget_tWithTarget_t_Target : Type; }. @@ -514,7 +514,7 @@ Arguments mkWithTarget_t { _ }. Arguments WithTarget_tWithTarget_t_Target { _ } _. (** Trait declaration: [traits::ParentTrait2] - Source: 'tests/src/traits.rs', lines 257:0-259:1 *) + Source: 'tests/src/traits.rs', lines 258:0-260:1 *) Record ParentTrait2_t (Self : Type) := mkParentTrait2_t { ParentTrait2_tParentTrait2_t_U : Type; ParentTrait2_tParentTrait2_t_WithTargettraitsParentTrait2UInst : WithTarget_t @@ -527,7 +527,7 @@ Arguments ParentTrait2_tParentTrait2_t_WithTargettraitsParentTrait2UInst { _ } _. (** Trait declaration: [traits::ChildTrait2] - Source: 'tests/src/traits.rs', lines 261:0-263:1 *) + Source: 'tests/src/traits.rs', lines 262:0-264:1 *) Record ChildTrait2_t (Self : Type) := mkChildTrait2_t { ChildTrait2_tChildTrait2_t_ParentTrait2Inst : ParentTrait2_t Self; ChildTrait2_t_convert : @@ -541,13 +541,13 @@ Arguments ChildTrait2_tChildTrait2_t_ParentTrait2Inst { _ } _. Arguments ChildTrait2_t_convert { _ } _. (** Trait implementation: [traits::{traits::WithTarget for u32}#11] - Source: 'tests/src/traits.rs', lines 265:0-267:1 *) + Source: 'tests/src/traits.rs', lines 266:0-268:1 *) Definition WithTargetU32 : WithTarget_t u32 := {| WithTarget_tWithTarget_t_Target := u32; |}. (** Trait implementation: [traits::{traits::ParentTrait2 for u32}#12] - Source: 'tests/src/traits.rs', lines 269:0-271:1 *) + Source: 'tests/src/traits.rs', lines 270:0-272:1 *) Definition ParentTrait2U32 : ParentTrait2_t u32 := {| ParentTrait2_tParentTrait2_t_U := u32; ParentTrait2_tParentTrait2_t_WithTargettraitsParentTrait2UInst := @@ -555,19 +555,19 @@ Definition ParentTrait2U32 : ParentTrait2_t u32 := {| |}. (** [traits::{traits::ChildTrait2 for u32}#13::convert]: - Source: 'tests/src/traits.rs', lines 274:4-276:5 *) + Source: 'tests/src/traits.rs', lines 275:4-277:5 *) Definition childTrait2U32_convert (x : u32) : result u32 := Ok x. (** Trait implementation: [traits::{traits::ChildTrait2 for u32}#13] - Source: 'tests/src/traits.rs', lines 273:0-277:1 *) + Source: 'tests/src/traits.rs', lines 274:0-278:1 *) Definition ChildTrait2U32 : ChildTrait2_t u32 := {| ChildTrait2_tChildTrait2_t_ParentTrait2Inst := ParentTrait2U32; ChildTrait2_t_convert := childTrait2U32_convert; |}. (** Trait declaration: [traits::CFnOnce] - Source: 'tests/src/traits.rs', lines 287:0-291:1 *) + Source: 'tests/src/traits.rs', lines 288:0-292:1 *) Record CFnOnce_t (Self : Type) (Args : Type) := mkCFnOnce_t { CFnOnce_tCFnOnce_t_Output : Type; CFnOnce_t_call_once : Self -> Args -> result CFnOnce_tCFnOnce_t_Output; @@ -578,7 +578,7 @@ Arguments CFnOnce_tCFnOnce_t_Output { _ } { _ } _. Arguments CFnOnce_t_call_once { _ } { _ } _. (** Trait declaration: [traits::CFnMut] - Source: 'tests/src/traits.rs', lines 293:0-295:1 *) + Source: 'tests/src/traits.rs', lines 294:0-296:1 *) Record CFnMut_t (Self : Type) (Args : Type) := mkCFnMut_t { CFnMut_tCFnMut_t_CFnOnceInst : CFnOnce_t Self Args; CFnMut_t_call_mut : Self -> Args -> result @@ -590,7 +590,7 @@ Arguments CFnMut_tCFnMut_t_CFnOnceInst { _ } { _ } _. Arguments CFnMut_t_call_mut { _ } { _ } _. (** Trait declaration: [traits::CFn] - Source: 'tests/src/traits.rs', lines 297:0-299:1 *) + Source: 'tests/src/traits.rs', lines 298:0-300:1 *) Record CFn_t (Self : Type) (Args : Type) := mkCFn_t { CFn_tCFn_t_CFnMutInst : CFnMut_t Self Args; CFn_t_call : Self -> Args -> result @@ -602,7 +602,7 @@ Arguments CFn_tCFn_t_CFnMutInst { _ } { _ } _. Arguments CFn_t_call { _ } { _ } _. (** Trait declaration: [traits::GetTrait] - Source: 'tests/src/traits.rs', lines 301:0-304:1 *) + Source: 'tests/src/traits.rs', lines 302:0-305:1 *) Record GetTrait_t (Self : Type) := mkGetTrait_t { GetTrait_tGetTrait_t_W : Type; GetTrait_t_get_w : Self -> result GetTrait_tGetTrait_t_W; @@ -613,7 +613,7 @@ Arguments GetTrait_tGetTrait_t_W { _ } _. Arguments GetTrait_t_get_w { _ } _. (** [traits::test_get_trait]: - Source: 'tests/src/traits.rs', lines 306:0-308:1 *) + Source: 'tests/src/traits.rs', lines 307:0-309:1 *) Definition test_get_trait {T : Type} (getTraitInst : GetTrait_t T) (x : T) : result getTraitInst.(GetTrait_tGetTrait_t_W) @@ -622,27 +622,27 @@ Definition test_get_trait . (** Trait declaration: [traits::Trait] - Source: 'tests/src/traits.rs', lines 311:0-313:1 *) + Source: 'tests/src/traits.rs', lines 312:0-314:1 *) Record Trait_t (Self : Type) := mkTrait_t { Trait_tTrait_t_LEN : usize; }. Arguments mkTrait_t { _ }. Arguments Trait_tTrait_t_LEN { _ } _. (** [traits::{traits::Trait for @Array}#14::LEN] - Source: 'tests/src/traits.rs', lines 316:4-316:25 *) + Source: 'tests/src/traits.rs', lines 317:4-317:25 *) Definition trait_array_len_body (T : Type) (N : usize) : result usize := Ok N. Definition trait_array_len (T : Type) (N : usize) : usize := (trait_array_len_body T N)%global . (** Trait implementation: [traits::{traits::Trait for @Array}#14] - Source: 'tests/src/traits.rs', lines 315:0-317:1 *) + Source: 'tests/src/traits.rs', lines 316:0-318:1 *) Definition TraitArray (T : Type) (N : usize) : Trait_t (array T N) := {| Trait_tTrait_t_LEN := trait_array_len T N; |}. (** [traits::{traits::Trait for traits::Wrapper}#15::LEN] - Source: 'tests/src/traits.rs', lines 320:4-320:25 *) + Source: 'tests/src/traits.rs', lines 321:4-321:25 *) Definition traittraits_wrapper_len_body {T : Type} (traitInst : Trait_t T) : result usize := Ok 0%usize @@ -653,20 +653,20 @@ Definition traittraits_wrapper_len {T : Type} (traitInst : Trait_t T) . (** Trait implementation: [traits::{traits::Trait for traits::Wrapper}#15] - Source: 'tests/src/traits.rs', lines 319:0-321:1 *) + Source: 'tests/src/traits.rs', lines 320:0-322:1 *) Definition TraittraitsWrapper {T : Type} (traitInst : Trait_t T) : Trait_t (Wrapper_t T) := {| Trait_tTrait_t_LEN := traittraits_wrapper_len traitInst; |}. (** [traits::use_wrapper_len]: - Source: 'tests/src/traits.rs', lines 323:0-325:1 *) + Source: 'tests/src/traits.rs', lines 324:0-326:1 *) Definition use_wrapper_len {T : Type} (traitInst : Trait_t T) : result usize := Ok (TraittraitsWrapper traitInst).(Trait_tTrait_t_LEN) . (** [traits::Foo] - Source: 'tests/src/traits.rs', lines 327:0-330:1 *) + Source: 'tests/src/traits.rs', lines 328:0-331:1 *) Record Foo_t (T : Type) (U : Type) := mkFoo_t { foo_x : T; foo_y : U; }. Arguments mkFoo_t { _ } { _ }. @@ -685,7 +685,7 @@ Arguments Core_result_Result_Ok { _ } { _ }. Arguments Core_result_Result_Err { _ } { _ }. (** [traits::{traits::Foo}#16::FOO] - Source: 'tests/src/traits.rs', lines 333:4-333:43 *) + Source: 'tests/src/traits.rs', lines 334:4-334:43 *) Definition foo_foo_body {T : Type} (U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) := Ok (Core_result_Result_Err 0%i32) @@ -696,7 +696,7 @@ Definition foo_foo {T : Type} (U : Type) (traitInst : Trait_t T) . (** [traits::use_foo1]: - Source: 'tests/src/traits.rs', lines 336:0-338:1 *) + Source: 'tests/src/traits.rs', lines 337:0-339:1 *) Definition use_foo1 {T : Type} (U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) @@ -705,7 +705,7 @@ Definition use_foo1 . (** [traits::use_foo2]: - Source: 'tests/src/traits.rs', lines 340:0-342:1 *) + Source: 'tests/src/traits.rs', lines 341:0-343:1 *) Definition use_foo2 (T : Type) {U : Type} (traitInst : Trait_t U) : result (core_result_Result_t U i32) diff --git a/tests/fstar/misc/AdtBorrows.fst b/tests/fstar/misc/AdtBorrows.fst new file mode 100644 index 00000000..731ba0f4 --- /dev/null +++ b/tests/fstar/misc/AdtBorrows.fst @@ -0,0 +1,107 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [adt_borrows] *) +module AdtBorrows +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [adt_borrows::SharedWrapper] + Source: 'tests/src/adt-borrows.rs', lines 4:0-4:35 *) +type sharedWrapper_t (t : Type0) = t + +(** [adt_borrows::{adt_borrows::SharedWrapper<'a, T>}::create]: + Source: 'tests/src/adt-borrows.rs', lines 7:4-9:5 *) +let sharedWrapper_create (#t : Type0) (x : t) : result (sharedWrapper_t t) = + Ok x + +(** [adt_borrows::{adt_borrows::SharedWrapper<'a, T>}::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 11:4-13:5 *) +let sharedWrapper_unwrap (#t : Type0) (self : sharedWrapper_t t) : result t = + Ok self + +(** [adt_borrows::SharedWrapper1] + Source: 'tests/src/adt-borrows.rs', lines 16:0-18:1 *) +type sharedWrapper1_t (t : Type0) = { x : t; } + +(** [adt_borrows::{adt_borrows::SharedWrapper1<'a, T>}#1::create]: + Source: 'tests/src/adt-borrows.rs', lines 21:4-23:5 *) +let sharedWrapper1_create (#t : Type0) (x : t) : result (sharedWrapper1_t t) = + Ok { x = x } + +(** [adt_borrows::{adt_borrows::SharedWrapper1<'a, T>}#1::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 25:4-27:5 *) +let sharedWrapper1_unwrap (#t : Type0) (self : sharedWrapper1_t t) : result t = + Ok self.x + +(** [adt_borrows::SharedWrapper2] + Source: 'tests/src/adt-borrows.rs', lines 30:0-33:1 *) +type sharedWrapper2_t (t : Type0) = { x : t; y : t; } + +(** [adt_borrows::{adt_borrows::SharedWrapper2<'a, 'b, T>}#2::create]: + Source: 'tests/src/adt-borrows.rs', lines 36:4-38:5 *) +let sharedWrapper2_create + (#t : Type0) (x : t) (y : t) : result (sharedWrapper2_t t) = + Ok { x = x; y = y } + +(** [adt_borrows::{adt_borrows::SharedWrapper2<'a, 'b, T>}#2::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 40:4-42:5 *) +let sharedWrapper2_unwrap + (#t : Type0) (self : sharedWrapper2_t t) : result (t & t) = + Ok (self.x, self.y) + +(** [adt_borrows::MutWrapper] + Source: 'tests/src/adt-borrows.rs', lines 45:0-45:36 *) +type mutWrapper_t (t : Type0) = t + +(** [adt_borrows::{adt_borrows::MutWrapper<'a, T>}#3::create]: + Source: 'tests/src/adt-borrows.rs', lines 48:4-50:5 *) +let mutWrapper_create + (#t : Type0) (x : t) : result ((mutWrapper_t t) & (mutWrapper_t t -> t)) = + let back = fun ret -> ret in Ok (x, back) + +(** [adt_borrows::{adt_borrows::MutWrapper<'a, T>}#3::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 52:4-54:5 *) +let mutWrapper_unwrap + (#t : Type0) (self : mutWrapper_t t) : result (t & (t -> mutWrapper_t t)) = + let back = fun ret -> ret in Ok (self, back) + +(** [adt_borrows::MutWrapper1] + Source: 'tests/src/adt-borrows.rs', lines 57:0-59:1 *) +type mutWrapper1_t (t : Type0) = { x : t; } + +(** [adt_borrows::{adt_borrows::MutWrapper1<'a, T>}#4::create]: + Source: 'tests/src/adt-borrows.rs', lines 62:4-64:5 *) +let mutWrapper1_create + (#t : Type0) (x : t) : result ((mutWrapper1_t t) & (mutWrapper1_t t -> t)) = + let back = fun ret -> ret.x in Ok ({ x = x }, back) + +(** [adt_borrows::{adt_borrows::MutWrapper1<'a, T>}#4::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 66:4-68:5 *) +let mutWrapper1_unwrap + (#t : Type0) (self : mutWrapper1_t t) : result (t & (t -> mutWrapper1_t t)) = + let back = fun ret -> { x = ret } in Ok (self.x, back) + +(** [adt_borrows::MutWrapper2] + Source: 'tests/src/adt-borrows.rs', lines 71:0-74:1 *) +type mutWrapper2_t (t : Type0) = { x : t; y : t; } + +(** [adt_borrows::{adt_borrows::MutWrapper2<'a, 'b, T>}#5::create]: + Source: 'tests/src/adt-borrows.rs', lines 77:4-79:5 *) +let mutWrapper2_create + (#t : Type0) (x : t) (y : t) : + result ((mutWrapper2_t t) & (mutWrapper2_t t -> t) & (mutWrapper2_t t -> t)) + = + let back'a = fun ret -> ret.x in + let back'b = fun ret -> ret.y in + Ok ({ x = x; y = y }, back'a, back'b) + +(** [adt_borrows::{adt_borrows::MutWrapper2<'a, 'b, T>}#5::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 81:4-83:5 *) +let mutWrapper2_unwrap + (#t : Type0) (self : mutWrapper2_t t) : + result ((t & t) & (t -> mutWrapper2_t t) & (t -> mutWrapper2_t t)) + = + let back'a = fun ret -> { self with x = ret } in + let back'b = fun ret -> { self with y = ret } in + Ok ((self.x, self.y), back'a, back'b) + diff --git a/tests/fstar/misc/Issue270LoopList.fst b/tests/fstar/misc/Issue270LoopList.fst index 7b2ea351..1cfdcff5 100644 --- a/tests/fstar/misc/Issue270LoopList.fst +++ b/tests/fstar/misc/Issue270LoopList.fst @@ -12,12 +12,12 @@ type list_t (t : Type0) = | List_Nil : list_t t (** [issue_270_loop_list::foo]: loop 0: - Source: 'tests/src/issue-270-loop-list.rs', lines 11:8-14:9 *) + Source: 'tests/src/issue-270-loop-list.rs', lines 10:8-12:9 *) let rec foo_loop (t : list_t (list_t u8)) : result unit = begin match t with | List_Cons _ tt -> foo_loop tt | List_Nil -> Ok () end (** [issue_270_loop_list::foo]: - Source: 'tests/src/issue-270-loop-list.rs', lines 8:0-16:1 *) + Source: 'tests/src/issue-270-loop-list.rs', lines 7:0-14:1 *) let foo (v : list_t (list_t u8)) : result unit = begin match v with | List_Cons l t -> foo_loop t | List_Nil -> Ok () end diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index 48ce588b..76ed2b6b 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -505,22 +505,30 @@ let not_u32 (x : u32) : result u32 = let not_i32 (x : i32) : result i32 = Ok (i32_not x) +(** [no_nested_borrows::borrow_mut_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 532:0-534:1 *) +let borrow_mut_tuple + (#t : Type0) (#u : Type0) (x : (t & u)) : + result ((t & u) & ((t & u) -> (t & u))) + = + let back = fun ret -> ret in Ok (x, back) + (** [no_nested_borrows::ExpandSimpliy::Wrapper] - Source: 'tests/src/no_nested_borrows.rs', lines 534:4-534:32 *) + Source: 'tests/src/no_nested_borrows.rs', lines 538:4-538:32 *) type expandSimpliy_Wrapper_t (t : Type0) = t * t (** [no_nested_borrows::ExpandSimpliy::check_expand_simplify_symb1]: - Source: 'tests/src/no_nested_borrows.rs', lines 536:4-542:5 *) + Source: 'tests/src/no_nested_borrows.rs', lines 540:4-546:5 *) let expandSimpliy_check_expand_simplify_symb1 (x : expandSimpliy_Wrapper_t bool) : result (expandSimpliy_Wrapper_t bool) = let (b, b1) = x in if b then Ok x else Ok x (** [no_nested_borrows::ExpandSimpliy::Wrapper2] - Source: 'tests/src/no_nested_borrows.rs', lines 544:4-547:5 *) + Source: 'tests/src/no_nested_borrows.rs', lines 548:4-551:5 *) type expandSimpliy_Wrapper2_t = { b : bool; x : u32; } (** [no_nested_borrows::ExpandSimpliy::check_expand_simplify_symb2]: - Source: 'tests/src/no_nested_borrows.rs', lines 549:4-555:5 *) + Source: 'tests/src/no_nested_borrows.rs', lines 553:4-559:5 *) let expandSimpliy_check_expand_simplify_symb2 (x : expandSimpliy_Wrapper2_t) : result expandSimpliy_Wrapper2_t = if x.b then Ok x else Ok x diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 201632e9..f87b05a3 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -6,20 +6,20 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** Trait declaration: [traits::BoolTrait] - Source: 'tests/src/traits.rs', lines 2:0-10:1 *) + Source: 'tests/src/traits.rs', lines 3:0-11:1 *) noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; } (** [traits::{traits::BoolTrait for bool}::get_bool]: - Source: 'tests/src/traits.rs', lines 13:4-15:5 *) + Source: 'tests/src/traits.rs', lines 14:4-16:5 *) let boolTraitBool_get_bool (self : bool) : result bool = Ok self (** Trait implementation: [traits::{traits::BoolTrait for bool}] - Source: 'tests/src/traits.rs', lines 12:0-16:1 *) + Source: 'tests/src/traits.rs', lines 13:0-17:1 *) let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; } (** [traits::BoolTrait::ret_true]: - Source: 'tests/src/traits.rs', lines 7:4-9:5 *) + Source: 'tests/src/traits.rs', lines 8:4-10:5 *) let boolTrait_ret_true (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) : result bool @@ -27,49 +27,49 @@ let boolTrait_ret_true Ok true (** [traits::test_bool_trait_bool]: - Source: 'tests/src/traits.rs', lines 18:0-20:1 *) + Source: 'tests/src/traits.rs', lines 19:0-21:1 *) let test_bool_trait_bool (x : bool) : result bool = let* b = boolTraitBool_get_bool x in if b then boolTrait_ret_true boolTraitBool x else Ok false (** [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: - Source: 'tests/src/traits.rs', lines 24:4-29:5 *) + Source: 'tests/src/traits.rs', lines 25:4-30:5 *) let boolTraitOption_get_bool (#t : Type0) (self : option t) : result bool = begin match self with | None -> Ok false | Some _ -> Ok true end (** Trait implementation: [traits::{traits::BoolTrait for core::option::Option}#1] - Source: 'tests/src/traits.rs', lines 23:0-30:1 *) + Source: 'tests/src/traits.rs', lines 24:0-31:1 *) let boolTraitOption (t : Type0) : boolTrait_t (option t) = { get_bool = boolTraitOption_get_bool; } (** [traits::test_bool_trait_option]: - Source: 'tests/src/traits.rs', lines 32:0-34:1 *) + Source: 'tests/src/traits.rs', lines 33:0-35:1 *) let test_bool_trait_option (#t : Type0) (x : option t) : result bool = let* b = boolTraitOption_get_bool x in if b then boolTrait_ret_true (boolTraitOption t) x else Ok false (** [traits::test_bool_trait]: - Source: 'tests/src/traits.rs', lines 36:0-38:1 *) + Source: 'tests/src/traits.rs', lines 37:0-39:1 *) let test_bool_trait (#t : Type0) (boolTraitInst : boolTrait_t t) (x : t) : result bool = boolTraitInst.get_bool x (** Trait declaration: [traits::ToU64] - Source: 'tests/src/traits.rs', lines 40:0-42:1 *) + Source: 'tests/src/traits.rs', lines 41:0-43:1 *) noeq type toU64_t (self : Type0) = { to_u64 : self -> result u64; } (** [traits::{traits::ToU64 for u64}#2::to_u64]: - Source: 'tests/src/traits.rs', lines 45:4-47:5 *) + Source: 'tests/src/traits.rs', lines 46:4-48:5 *) let toU64U64_to_u64 (self : u64) : result u64 = Ok self (** Trait implementation: [traits::{traits::ToU64 for u64}#2] - Source: 'tests/src/traits.rs', lines 44:0-48:1 *) + Source: 'tests/src/traits.rs', lines 45:0-49:1 *) let toU64U64 : toU64_t u64 = { to_u64 = toU64U64_to_u64; } (** [traits::{traits::ToU64 for (A, A)}#3::to_u64]: - Source: 'tests/src/traits.rs', lines 51:4-53:5 *) + Source: 'tests/src/traits.rs', lines 52:4-54:5 *) let toU64Pair_to_u64 (#a : Type0) (toU64Inst : toU64_t a) (self : (a & a)) : result u64 = let (x, x1) = self in @@ -78,75 +78,75 @@ let toU64Pair_to_u64 u64_add i i1 (** Trait implementation: [traits::{traits::ToU64 for (A, A)}#3] - Source: 'tests/src/traits.rs', lines 50:0-54:1 *) + Source: 'tests/src/traits.rs', lines 51:0-55:1 *) let toU64Pair (#a : Type0) (toU64Inst : toU64_t a) : toU64_t (a & a) = { to_u64 = toU64Pair_to_u64 toU64Inst; } (** [traits::f]: - Source: 'tests/src/traits.rs', lines 56:0-58:1 *) + Source: 'tests/src/traits.rs', lines 57:0-59:1 *) let f (#t : Type0) (toU64Inst : toU64_t t) (x : (t & t)) : result u64 = toU64Pair_to_u64 toU64Inst x (** [traits::g]: - Source: 'tests/src/traits.rs', lines 60:0-65:1 *) + Source: 'tests/src/traits.rs', lines 61:0-66:1 *) let g (#t : Type0) (toU64PairInst : toU64_t (t & t)) (x : (t & t)) : result u64 = toU64PairInst.to_u64 x (** [traits::h0]: - Source: 'tests/src/traits.rs', lines 67:0-69:1 *) + Source: 'tests/src/traits.rs', lines 68:0-70:1 *) let h0 (x : u64) : result u64 = toU64U64_to_u64 x (** [traits::Wrapper] - Source: 'tests/src/traits.rs', lines 71:0-73:1 *) + Source: 'tests/src/traits.rs', lines 72:0-74:1 *) type wrapper_t (t : Type0) = { x : t; } (** [traits::{traits::ToU64 for traits::Wrapper}#4::to_u64]: - Source: 'tests/src/traits.rs', lines 76:4-78:5 *) + Source: 'tests/src/traits.rs', lines 77:4-79:5 *) let toU64traitsWrapper_to_u64 (#t : Type0) (toU64Inst : toU64_t t) (self : wrapper_t t) : result u64 = toU64Inst.to_u64 self.x (** Trait implementation: [traits::{traits::ToU64 for traits::Wrapper}#4] - Source: 'tests/src/traits.rs', lines 75:0-79:1 *) + Source: 'tests/src/traits.rs', lines 76:0-80:1 *) let toU64traitsWrapper (#t : Type0) (toU64Inst : toU64_t t) : toU64_t (wrapper_t t) = { to_u64 = toU64traitsWrapper_to_u64 toU64Inst; } (** [traits::h1]: - Source: 'tests/src/traits.rs', lines 81:0-83:1 *) + Source: 'tests/src/traits.rs', lines 82:0-84:1 *) let h1 (x : wrapper_t u64) : result u64 = toU64traitsWrapper_to_u64 toU64U64 x (** [traits::h2]: - Source: 'tests/src/traits.rs', lines 85:0-87:1 *) + Source: 'tests/src/traits.rs', lines 86:0-88:1 *) let h2 (#t : Type0) (toU64Inst : toU64_t t) (x : wrapper_t t) : result u64 = toU64traitsWrapper_to_u64 toU64Inst x (** Trait declaration: [traits::ToType] - Source: 'tests/src/traits.rs', lines 89:0-91:1 *) + Source: 'tests/src/traits.rs', lines 90:0-92:1 *) noeq type toType_t (self : Type0) (t : Type0) = { to_type : self -> result t; } (** [traits::{traits::ToType for u64}#5::to_type]: - Source: 'tests/src/traits.rs', lines 94:4-96:5 *) + Source: 'tests/src/traits.rs', lines 95:4-97:5 *) let toTypeU64Bool_to_type (self : u64) : result bool = Ok (self > 0) (** Trait implementation: [traits::{traits::ToType for u64}#5] - Source: 'tests/src/traits.rs', lines 93:0-97:1 *) + Source: 'tests/src/traits.rs', lines 94:0-98:1 *) let toTypeU64Bool : toType_t u64 bool = { to_type = toTypeU64Bool_to_type; } (** Trait declaration: [traits::OfType] - Source: 'tests/src/traits.rs', lines 99:0-103:1 *) + Source: 'tests/src/traits.rs', lines 100:0-104:1 *) noeq type ofType_t (self : Type0) = { of_type : (#t : Type0) -> (toTypeInst : toType_t t self) -> t -> result self; } (** [traits::h3]: - Source: 'tests/src/traits.rs', lines 105:0-107:1 *) + Source: 'tests/src/traits.rs', lines 106:0-108:1 *) let h3 (#t1 : Type0) (#t2 : Type0) (ofTypeInst : ofType_t t1) (toTypeInst : toType_t t2 t1) (y : t2) : @@ -155,14 +155,14 @@ let h3 ofTypeInst.of_type toTypeInst y (** Trait declaration: [traits::OfTypeBis] - Source: 'tests/src/traits.rs', lines 110:0-117:1 *) + Source: 'tests/src/traits.rs', lines 111:0-118:1 *) noeq type ofTypeBis_t (self : Type0) (t : Type0) = { toTypeInst : toType_t t self; of_type : t -> result self; } (** [traits::h4]: - Source: 'tests/src/traits.rs', lines 119:0-121:1 *) + Source: 'tests/src/traits.rs', lines 120:0-122:1 *) let h4 (#t1 : Type0) (#t2 : Type0) (ofTypeBisInst : ofTypeBis_t t1 t2) (toTypeInst : toType_t t2 t1) (y : t2) : @@ -171,34 +171,34 @@ let h4 ofTypeBisInst.of_type y (** [traits::TestType] - Source: 'tests/src/traits.rs', lines 123:0-123:26 *) + Source: 'tests/src/traits.rs', lines 124:0-124:26 *) type testType_t (t : Type0) = t (** [traits::{traits::TestType}#6::test::TestType1] - Source: 'tests/src/traits.rs', lines 128:8-128:30 *) + Source: 'tests/src/traits.rs', lines 129:8-129:30 *) type testType_test_TestType1_t = u64 (** Trait declaration: [traits::{traits::TestType}#6::test::TestTrait] - Source: 'tests/src/traits.rs', lines 129:8-131:9 *) + Source: 'tests/src/traits.rs', lines 130:8-132:9 *) noeq type testType_test_TestTrait_t (self : Type0) = { test : self -> result bool; } (** [traits::{traits::TestType}#6::test::{traits::{traits::TestType}#6::test::TestTrait for traits::{traits::TestType}#6::test::TestType1}::test]: - Source: 'tests/src/traits.rs', lines 140:12-142:13 *) + Source: 'tests/src/traits.rs', lines 141:12-143:13 *) let testType_test_TestTraittraitsTestTypetestTestType1_test (self : testType_test_TestType1_t) : result bool = Ok (self > 1) (** Trait implementation: [traits::{traits::TestType}#6::test::{traits::{traits::TestType}#6::test::TestTrait for traits::{traits::TestType}#6::test::TestType1}] - Source: 'tests/src/traits.rs', lines 139:8-143:9 *) + Source: 'tests/src/traits.rs', lines 140:8-144:9 *) let testType_test_TestTraittraitsTestTypetestTestType1 : testType_test_TestTrait_t testType_test_TestType1_t = { test = testType_test_TestTraittraitsTestTypetestTestType1_test; } (** [traits::{traits::TestType}#6::test]: - Source: 'tests/src/traits.rs', lines 127:4-148:5 *) + Source: 'tests/src/traits.rs', lines 128:4-149:5 *) let testType_test (#t : Type0) (toU64Inst : toU64_t t) (self : testType_t t) (x : t) : result bool @@ -209,11 +209,11 @@ let testType_test else Ok false (** [traits::BoolWrapper] - Source: 'tests/src/traits.rs', lines 151:0-151:33 *) + Source: 'tests/src/traits.rs', lines 152:0-152:33 *) type boolWrapper_t = bool (** [traits::{traits::ToType for traits::BoolWrapper}#7::to_type]: - Source: 'tests/src/traits.rs', lines 157:4-159:5 *) + Source: 'tests/src/traits.rs', lines 158:4-160:5 *) let toTypetraitsBoolWrapperT_to_type (#t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) : result t @@ -221,14 +221,14 @@ let toTypetraitsBoolWrapperT_to_type toTypeBoolTInst.to_type self (** Trait implementation: [traits::{traits::ToType for traits::BoolWrapper}#7] - Source: 'tests/src/traits.rs', lines 153:0-160:1 *) + Source: 'tests/src/traits.rs', lines 154:0-161:1 *) let toTypetraitsBoolWrapperT (#t : Type0) (toTypeBoolTInst : toType_t bool t) : toType_t boolWrapper_t t = { to_type = toTypetraitsBoolWrapperT_to_type toTypeBoolTInst; } (** [traits::WithConstTy::LEN2] - Source: 'tests/src/traits.rs', lines 165:4-165:27 *) + Source: 'tests/src/traits.rs', lines 166:4-166:27 *) let with_const_ty_len2_default_body (self : Type0) (len : usize) : result usize = Ok 32 @@ -236,7 +236,7 @@ let with_const_ty_len2_default (self : Type0) (len : usize) : usize = eval_global (with_const_ty_len2_default_body self len) (** Trait declaration: [traits::WithConstTy] - Source: 'tests/src/traits.rs', lines 162:0-173:1 *) + Source: 'tests/src/traits.rs', lines 163:0-174:1 *) noeq type withConstTy_t (self : Type0) (len : usize) = { cLEN1 : usize; cLEN2 : usize; @@ -247,18 +247,18 @@ noeq type withConstTy_t (self : Type0) (len : usize) = { } (** [traits::{traits::WithConstTy<32: usize> for bool}#8::LEN1] - Source: 'tests/src/traits.rs', lines 176:4-176:27 *) + Source: 'tests/src/traits.rs', lines 177:4-177:27 *) let with_const_ty_bool32_len1_body : result usize = Ok 12 let with_const_ty_bool32_len1 : usize = eval_global with_const_ty_bool32_len1_body (** [traits::{traits::WithConstTy<32: usize> for bool}#8::f]: - Source: 'tests/src/traits.rs', lines 181:4-181:42 *) + Source: 'tests/src/traits.rs', lines 182:4-182:42 *) let withConstTyBool32_f (i : u64) (a : array u8 32) : result u64 = Ok i (** Trait implementation: [traits::{traits::WithConstTy<32: usize> for bool}#8] - Source: 'tests/src/traits.rs', lines 175:0-182:1 *) + Source: 'tests/src/traits.rs', lines 176:0-183:1 *) let withConstTyBool32 : withConstTy_t bool 32 = { cLEN1 = with_const_ty_bool32_len1; cLEN2 = with_const_ty_len2_default bool 32; @@ -269,7 +269,7 @@ let withConstTyBool32 : withConstTy_t bool 32 = { } (** [traits::use_with_const_ty1]: - Source: 'tests/src/traits.rs', lines 184:0-186:1 *) + Source: 'tests/src/traits.rs', lines 185:0-187:1 *) let use_with_const_ty1 (#h : Type0) (#len : usize) (withConstTyInst : withConstTy_t h len) : result usize @@ -277,7 +277,7 @@ let use_with_const_ty1 Ok withConstTyInst.cLEN1 (** [traits::use_with_const_ty2]: - Source: 'tests/src/traits.rs', lines 188:0-188:76 *) + Source: 'tests/src/traits.rs', lines 189:0-189:76 *) let use_with_const_ty2 (#h : Type0) (#len : usize) (withConstTyInst : withConstTy_t h len) (w : withConstTyInst.tW) : @@ -286,7 +286,7 @@ let use_with_const_ty2 Ok () (** [traits::use_with_const_ty3]: - Source: 'tests/src/traits.rs', lines 190:0-192:1 *) + Source: 'tests/src/traits.rs', lines 191:0-193:1 *) let use_with_const_ty3 (#h : Type0) (#len : usize) (withConstTyInst : withConstTy_t h len) (x : withConstTyInst.tW) : @@ -295,12 +295,12 @@ let use_with_const_ty3 withConstTyInst.toU64traitsWithConstTyWInst.to_u64 x (** [traits::test_where1]: - Source: 'tests/src/traits.rs', lines 194:0-194:43 *) + Source: 'tests/src/traits.rs', lines 195:0-195:43 *) let test_where1 (#t : Type0) (_x : t) : result unit = Ok () (** [traits::test_where2]: - Source: 'tests/src/traits.rs', lines 195:0-195:60 *) + Source: 'tests/src/traits.rs', lines 196:0-196:60 *) let test_where2 (#t : Type0) (withConstTyT32Inst : withConstTy_t t 32) (_x : u32) : result unit @@ -308,7 +308,7 @@ let test_where2 Ok () (** Trait declaration: [traits::ParentTrait0] - Source: 'tests/src/traits.rs', lines 201:0-205:1 *) + Source: 'tests/src/traits.rs', lines 202:0-206:1 *) noeq type parentTrait0_t (self : Type0) = { tW : Type0; get_name : self -> result string; @@ -316,24 +316,24 @@ noeq type parentTrait0_t (self : Type0) = { } (** Trait declaration: [traits::ParentTrait1] - Source: 'tests/src/traits.rs', lines 206:0-206:25 *) + Source: 'tests/src/traits.rs', lines 207:0-207:25 *) type parentTrait1_t (self : Type0) = unit (** Trait declaration: [traits::ChildTrait] - Source: 'tests/src/traits.rs', lines 207:0-207:52 *) + Source: 'tests/src/traits.rs', lines 208:0-208:52 *) noeq type childTrait_t (self : Type0) = { parentTrait0Inst : parentTrait0_t self; parentTrait1Inst : parentTrait1_t self; } (** [traits::test_child_trait1]: - Source: 'tests/src/traits.rs', lines 210:0-212:1 *) + Source: 'tests/src/traits.rs', lines 211:0-213:1 *) let test_child_trait1 (#t : Type0) (childTraitInst : childTrait_t t) (x : t) : result string = childTraitInst.parentTrait0Inst.get_name x (** [traits::test_child_trait2]: - Source: 'tests/src/traits.rs', lines 214:0-216:1 *) + Source: 'tests/src/traits.rs', lines 215:0-217:1 *) let test_child_trait2 (#t : Type0) (childTraitInst : childTrait_t t) (x : t) : result childTraitInst.parentTrait0Inst.tW @@ -341,7 +341,7 @@ let test_child_trait2 childTraitInst.parentTrait0Inst.get_w x (** [traits::order1]: - Source: 'tests/src/traits.rs', lines 220:0-220:62 *) + Source: 'tests/src/traits.rs', lines 221:0-221:62 *) let order1 (#t : Type0) (#u : Type0) (parentTrait0Inst : parentTrait0_t t) (parentTrait0Inst1 : parentTrait0_t u) : @@ -350,27 +350,27 @@ let order1 Ok () (** Trait declaration: [traits::ChildTrait1] - Source: 'tests/src/traits.rs', lines 223:0-223:38 *) + Source: 'tests/src/traits.rs', lines 224:0-224:38 *) noeq type childTrait1_t (self : Type0) = { parentTrait1Inst : parentTrait1_t self; } (** Trait implementation: [traits::{traits::ParentTrait1 for usize}#9] - Source: 'tests/src/traits.rs', lines 225:0-225:30 *) + Source: 'tests/src/traits.rs', lines 226:0-226:30 *) let parentTrait1Usize : parentTrait1_t usize = () (** Trait implementation: [traits::{traits::ChildTrait1 for usize}#10] - Source: 'tests/src/traits.rs', lines 226:0-226:29 *) + Source: 'tests/src/traits.rs', lines 227:0-227:29 *) let childTrait1Usize : childTrait1_t usize = { parentTrait1Inst = parentTrait1Usize; } (** Trait declaration: [traits::Iterator] - Source: 'tests/src/traits.rs', lines 230:0-232:1 *) + Source: 'tests/src/traits.rs', lines 231:0-233:1 *) noeq type iterator_t (self : Type0) = { tItem : Type0; } (** Trait declaration: [traits::IntoIterator] - Source: 'tests/src/traits.rs', lines 234:0-240:1 *) + Source: 'tests/src/traits.rs', lines 235:0-241:1 *) noeq type intoIterator_t (self : Type0) = { tItem : Type0; tIntoIter : Type0; @@ -379,29 +379,29 @@ noeq type intoIterator_t (self : Type0) = { } (** Trait declaration: [traits::FromResidual] - Source: 'tests/src/traits.rs', lines 251:0-251:24 *) + Source: 'tests/src/traits.rs', lines 252:0-252:24 *) type fromResidual_t (self : Type0) (t : Type0) = unit (** Trait declaration: [traits::Try] - Source: 'tests/src/traits.rs', lines 247:0-249:1 *) + Source: 'tests/src/traits.rs', lines 248:0-250:1 *) noeq type try_t (self : Type0) = { tResidual : Type0; fromResidualSelftraitsTryResidualInst : fromResidual_t self tResidual; } (** Trait declaration: [traits::WithTarget] - Source: 'tests/src/traits.rs', lines 253:0-255:1 *) + Source: 'tests/src/traits.rs', lines 254:0-256:1 *) noeq type withTarget_t (self : Type0) = { tTarget : Type0; } (** Trait declaration: [traits::ParentTrait2] - Source: 'tests/src/traits.rs', lines 257:0-259:1 *) + Source: 'tests/src/traits.rs', lines 258:0-260:1 *) noeq type parentTrait2_t (self : Type0) = { tU : Type0; withTargettraitsParentTrait2UInst : withTarget_t tU; } (** Trait declaration: [traits::ChildTrait2] - Source: 'tests/src/traits.rs', lines 261:0-263:1 *) + Source: 'tests/src/traits.rs', lines 262:0-264:1 *) noeq type childTrait2_t (self : Type0) = { parentTrait2Inst : parentTrait2_t self; convert : parentTrait2Inst.tU -> result @@ -409,78 +409,78 @@ noeq type childTrait2_t (self : Type0) = { } (** Trait implementation: [traits::{traits::WithTarget for u32}#11] - Source: 'tests/src/traits.rs', lines 265:0-267:1 *) + Source: 'tests/src/traits.rs', lines 266:0-268:1 *) let withTargetU32 : withTarget_t u32 = { tTarget = u32; } (** Trait implementation: [traits::{traits::ParentTrait2 for u32}#12] - Source: 'tests/src/traits.rs', lines 269:0-271:1 *) + Source: 'tests/src/traits.rs', lines 270:0-272:1 *) let parentTrait2U32 : parentTrait2_t u32 = { tU = u32; withTargettraitsParentTrait2UInst = withTargetU32; } (** [traits::{traits::ChildTrait2 for u32}#13::convert]: - Source: 'tests/src/traits.rs', lines 274:4-276:5 *) + Source: 'tests/src/traits.rs', lines 275:4-277:5 *) let childTrait2U32_convert (x : u32) : result u32 = Ok x (** Trait implementation: [traits::{traits::ChildTrait2 for u32}#13] - Source: 'tests/src/traits.rs', lines 273:0-277:1 *) + Source: 'tests/src/traits.rs', lines 274:0-278:1 *) let childTrait2U32 : childTrait2_t u32 = { parentTrait2Inst = parentTrait2U32; convert = childTrait2U32_convert; } (** Trait declaration: [traits::CFnOnce] - Source: 'tests/src/traits.rs', lines 287:0-291:1 *) + Source: 'tests/src/traits.rs', lines 288:0-292:1 *) noeq type cFnOnce_t (self : Type0) (args : Type0) = { tOutput : Type0; call_once : self -> args -> result tOutput; } (** Trait declaration: [traits::CFnMut] - Source: 'tests/src/traits.rs', lines 293:0-295:1 *) + Source: 'tests/src/traits.rs', lines 294:0-296:1 *) noeq type cFnMut_t (self : Type0) (args : Type0) = { cFnOnceInst : cFnOnce_t self args; call_mut : self -> args -> result (cFnOnceInst.tOutput & self); } (** Trait declaration: [traits::CFn] - Source: 'tests/src/traits.rs', lines 297:0-299:1 *) + Source: 'tests/src/traits.rs', lines 298:0-300:1 *) noeq type cFn_t (self : Type0) (args : Type0) = { cFnMutInst : cFnMut_t self args; call : self -> args -> result cFnMutInst.cFnOnceInst.tOutput; } (** Trait declaration: [traits::GetTrait] - Source: 'tests/src/traits.rs', lines 301:0-304:1 *) + Source: 'tests/src/traits.rs', lines 302:0-305:1 *) noeq type getTrait_t (self : Type0) = { tW : Type0; get_w : self -> result tW; } (** [traits::test_get_trait]: - Source: 'tests/src/traits.rs', lines 306:0-308:1 *) + Source: 'tests/src/traits.rs', lines 307:0-309:1 *) let test_get_trait (#t : Type0) (getTraitInst : getTrait_t t) (x : t) : result getTraitInst.tW = getTraitInst.get_w x (** Trait declaration: [traits::Trait] - Source: 'tests/src/traits.rs', lines 311:0-313:1 *) + Source: 'tests/src/traits.rs', lines 312:0-314:1 *) noeq type trait_t (self : Type0) = { cLEN : usize; } (** [traits::{traits::Trait for @Array}#14::LEN] - Source: 'tests/src/traits.rs', lines 316:4-316:25 *) + Source: 'tests/src/traits.rs', lines 317:4-317:25 *) let trait_array_len_body (t : Type0) (n : usize) : result usize = Ok n let trait_array_len (t : Type0) (n : usize) : usize = eval_global (trait_array_len_body t n) (** Trait implementation: [traits::{traits::Trait for @Array}#14] - Source: 'tests/src/traits.rs', lines 315:0-317:1 *) + Source: 'tests/src/traits.rs', lines 316:0-318:1 *) let traitArray (t : Type0) (n : usize) : trait_t (array t n) = { cLEN = trait_array_len t n; } (** [traits::{traits::Trait for traits::Wrapper}#15::LEN] - Source: 'tests/src/traits.rs', lines 320:4-320:25 *) + Source: 'tests/src/traits.rs', lines 321:4-321:25 *) let traittraits_wrapper_len_body (#t : Type0) (traitInst : trait_t t) : result usize = Ok 0 @@ -488,19 +488,19 @@ let traittraits_wrapper_len (#t : Type0) (traitInst : trait_t t) : usize = eval_global (traittraits_wrapper_len_body traitInst) (** Trait implementation: [traits::{traits::Trait for traits::Wrapper}#15] - Source: 'tests/src/traits.rs', lines 319:0-321:1 *) + Source: 'tests/src/traits.rs', lines 320:0-322:1 *) let traittraitsWrapper (#t : Type0) (traitInst : trait_t t) : trait_t (wrapper_t t) = { cLEN = traittraits_wrapper_len traitInst; } (** [traits::use_wrapper_len]: - Source: 'tests/src/traits.rs', lines 323:0-325:1 *) + Source: 'tests/src/traits.rs', lines 324:0-326:1 *) let use_wrapper_len (#t : Type0) (traitInst : trait_t t) : result usize = Ok (traittraitsWrapper traitInst).cLEN (** [traits::Foo] - Source: 'tests/src/traits.rs', lines 327:0-330:1 *) + Source: 'tests/src/traits.rs', lines 328:0-331:1 *) type foo_t (t : Type0) (u : Type0) = { x : t; y : u; } (** [core::result::Result] @@ -511,7 +511,7 @@ type core_result_Result_t (t : Type0) (e : Type0) = | Core_result_Result_Err : e -> core_result_Result_t t e (** [traits::{traits::Foo}#16::FOO] - Source: 'tests/src/traits.rs', lines 333:4-333:43 *) + Source: 'tests/src/traits.rs', lines 334:4-334:43 *) let foo_foo_body (#t : Type0) (u : Type0) (traitInst : trait_t t) : result (core_result_Result_t t i32) = Ok (Core_result_Result_Err 0) @@ -520,7 +520,7 @@ let foo_foo (#t : Type0) (u : Type0) (traitInst : trait_t t) eval_global (foo_foo_body u traitInst) (** [traits::use_foo1]: - Source: 'tests/src/traits.rs', lines 336:0-338:1 *) + Source: 'tests/src/traits.rs', lines 337:0-339:1 *) let use_foo1 (#t : Type0) (u : Type0) (traitInst : trait_t t) : result (core_result_Result_t t i32) @@ -528,7 +528,7 @@ let use_foo1 Ok (foo_foo u traitInst) (** [traits::use_foo2]: - Source: 'tests/src/traits.rs', lines 340:0-342:1 *) + Source: 'tests/src/traits.rs', lines 341:0-343:1 *) let use_foo2 (t : Type0) (#u : Type0) (traitInst : trait_t u) : result (core_result_Result_t u i32) diff --git a/tests/lean/AdtBorrows.lean b/tests/lean/AdtBorrows.lean new file mode 100644 index 00000000..5f469a12 --- /dev/null +++ b/tests/lean/AdtBorrows.lean @@ -0,0 +1,121 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [adt_borrows] +import Base +open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false + +namespace adt_borrows + +/- [adt_borrows::SharedWrapper] + Source: 'tests/src/adt-borrows.rs', lines 4:0-4:35 -/ +@[reducible] def SharedWrapper (T : Type) := T + +/- [adt_borrows::{adt_borrows::SharedWrapper<'a, T>}::create]: + Source: 'tests/src/adt-borrows.rs', lines 7:4-9:5 -/ +def SharedWrapper.create {T : Type} (x : T) : Result (SharedWrapper T) := + Result.ok x + +/- [adt_borrows::{adt_borrows::SharedWrapper<'a, T>}::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 11:4-13:5 -/ +def SharedWrapper.unwrap {T : Type} (self : SharedWrapper T) : Result T := + Result.ok self + +/- [adt_borrows::SharedWrapper1] + Source: 'tests/src/adt-borrows.rs', lines 16:0-18:1 -/ +structure SharedWrapper1 (T : Type) where + x : T + +/- [adt_borrows::{adt_borrows::SharedWrapper1<'a, T>}#1::create]: + Source: 'tests/src/adt-borrows.rs', lines 21:4-23:5 -/ +def SharedWrapper1.create {T : Type} (x : T) : Result (SharedWrapper1 T) := + Result.ok { x := x } + +/- [adt_borrows::{adt_borrows::SharedWrapper1<'a, T>}#1::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 25:4-27:5 -/ +def SharedWrapper1.unwrap {T : Type} (self : SharedWrapper1 T) : Result T := + Result.ok self.x + +/- [adt_borrows::SharedWrapper2] + Source: 'tests/src/adt-borrows.rs', lines 30:0-33:1 -/ +structure SharedWrapper2 (T : Type) where + x : T + y : T + +/- [adt_borrows::{adt_borrows::SharedWrapper2<'a, 'b, T>}#2::create]: + Source: 'tests/src/adt-borrows.rs', lines 36:4-38:5 -/ +def SharedWrapper2.create + {T : Type} (x : T) (y : T) : Result (SharedWrapper2 T) := + Result.ok { x := x, y := y } + +/- [adt_borrows::{adt_borrows::SharedWrapper2<'a, 'b, T>}#2::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 40:4-42:5 -/ +def SharedWrapper2.unwrap + {T : Type} (self : SharedWrapper2 T) : Result (T × T) := + Result.ok (self.x, self.y) + +/- [adt_borrows::MutWrapper] + Source: 'tests/src/adt-borrows.rs', lines 45:0-45:36 -/ +@[reducible] def MutWrapper (T : Type) := T + +/- [adt_borrows::{adt_borrows::MutWrapper<'a, T>}#3::create]: + Source: 'tests/src/adt-borrows.rs', lines 48:4-50:5 -/ +def MutWrapper.create + {T : Type} (x : T) : Result ((MutWrapper T) × (MutWrapper T → T)) := + let back := fun ret => ret + Result.ok (x, back) + +/- [adt_borrows::{adt_borrows::MutWrapper<'a, T>}#3::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 52:4-54:5 -/ +def MutWrapper.unwrap + {T : Type} (self : MutWrapper T) : Result (T × (T → MutWrapper T)) := + let back := fun ret => ret + Result.ok (self, back) + +/- [adt_borrows::MutWrapper1] + Source: 'tests/src/adt-borrows.rs', lines 57:0-59:1 -/ +structure MutWrapper1 (T : Type) where + x : T + +/- [adt_borrows::{adt_borrows::MutWrapper1<'a, T>}#4::create]: + Source: 'tests/src/adt-borrows.rs', lines 62:4-64:5 -/ +def MutWrapper1.create + {T : Type} (x : T) : Result ((MutWrapper1 T) × (MutWrapper1 T → T)) := + let back := fun ret => ret.x + Result.ok ({ x := x }, back) + +/- [adt_borrows::{adt_borrows::MutWrapper1<'a, T>}#4::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 66:4-68:5 -/ +def MutWrapper1.unwrap + {T : Type} (self : MutWrapper1 T) : Result (T × (T → MutWrapper1 T)) := + let back := fun ret => { x := ret } + Result.ok (self.x, back) + +/- [adt_borrows::MutWrapper2] + Source: 'tests/src/adt-borrows.rs', lines 71:0-74:1 -/ +structure MutWrapper2 (T : Type) where + x : T + y : T + +/- [adt_borrows::{adt_borrows::MutWrapper2<'a, 'b, T>}#5::create]: + Source: 'tests/src/adt-borrows.rs', lines 77:4-79:5 -/ +def MutWrapper2.create + {T : Type} (x : T) (y : T) : + Result ((MutWrapper2 T) × (MutWrapper2 T → T) × (MutWrapper2 T → T)) + := + let back'a := fun ret => ret.x + let back'b := fun ret => ret.y + Result.ok ({ x := x, y := y }, back'a, back'b) + +/- [adt_borrows::{adt_borrows::MutWrapper2<'a, 'b, T>}#5::unwrap]: + Source: 'tests/src/adt-borrows.rs', lines 81:4-83:5 -/ +def MutWrapper2.unwrap + {T : Type} (self : MutWrapper2 T) : + Result ((T × T) × (T → MutWrapper2 T) × (T → MutWrapper2 T)) + := + let back'a := fun ret => { self with x := ret } + let back'b := fun ret => { self with y := ret } + Result.ok ((self.x, self.y), back'a, back'b) + +end adt_borrows diff --git a/tests/lean/Issue270LoopList.lean b/tests/lean/Issue270LoopList.lean index 8e9122ff..5c3d5419 100644 --- a/tests/lean/Issue270LoopList.lean +++ b/tests/lean/Issue270LoopList.lean @@ -15,14 +15,14 @@ inductive List (T : Type) := | Nil : List T /- [issue_270_loop_list::foo]: loop 0: - Source: 'tests/src/issue-270-loop-list.rs', lines 11:8-14:9 -/ + Source: 'tests/src/issue-270-loop-list.rs', lines 10:8-12:9 -/ divergent def foo_loop (t : List (List U8)) : Result Unit := match t with | List.Cons _ tt => foo_loop tt | List.Nil => Result.ok () /- [issue_270_loop_list::foo]: - Source: 'tests/src/issue-270-loop-list.rs', lines 8:0-16:1 -/ + Source: 'tests/src/issue-270-loop-list.rs', lines 7:0-14:1 -/ def foo (v : List (List U8)) : Result Unit := match v with | List.Cons l t => foo_loop t diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 6cc4f1f2..589f01b8 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -605,12 +605,21 @@ def not_u32 (x : U32) : Result U32 := def not_i32 (x : I32) : Result I32 := Result.ok (￢ x) +/- [no_nested_borrows::borrow_mut_tuple]: + Source: 'tests/src/no_nested_borrows.rs', lines 532:0-534:1 -/ +def borrow_mut_tuple + {T : Type} {U : Type} (x : (T × U)) : + Result ((T × U) × ((T × U) → (T × U))) + := + let back := fun ret => ret + Result.ok (x, back) + /- [no_nested_borrows::ExpandSimpliy::Wrapper] - Source: 'tests/src/no_nested_borrows.rs', lines 534:4-534:32 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 538:4-538:32 -/ def ExpandSimpliy.Wrapper (T : Type) := T × T /- [no_nested_borrows::ExpandSimpliy::check_expand_simplify_symb1]: - Source: 'tests/src/no_nested_borrows.rs', lines 536:4-542:5 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 540:4-546:5 -/ def ExpandSimpliy.check_expand_simplify_symb1 (x : ExpandSimpliy.Wrapper Bool) : Result (ExpandSimpliy.Wrapper Bool) := let (b, b1) := x @@ -619,13 +628,13 @@ def ExpandSimpliy.check_expand_simplify_symb1 else Result.ok x /- [no_nested_borrows::ExpandSimpliy::Wrapper2] - Source: 'tests/src/no_nested_borrows.rs', lines 544:4-547:5 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 548:4-551:5 -/ structure ExpandSimpliy.Wrapper2 where b : Bool x : U32 /- [no_nested_borrows::ExpandSimpliy::check_expand_simplify_symb2]: - Source: 'tests/src/no_nested_borrows.rs', lines 549:4-555:5 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 553:4-559:5 -/ def ExpandSimpliy.check_expand_simplify_symb2 (x : ExpandSimpliy.Wrapper2) : Result ExpandSimpliy.Wrapper2 := if x.b diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 3b997c8d..233d65ae 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -9,30 +9,30 @@ set_option linter.unusedVariables false namespace traits /- Trait declaration: [traits::BoolTrait] - Source: 'tests/src/traits.rs', lines 2:0-10:1 -/ + Source: 'tests/src/traits.rs', lines 3:0-11:1 -/ structure BoolTrait (Self : Type) where get_bool : Self → Result Bool /- [traits::{traits::BoolTrait for bool}::get_bool]: - Source: 'tests/src/traits.rs', lines 13:4-15:5 -/ + Source: 'tests/src/traits.rs', lines 14:4-16:5 -/ def BoolTraitBool.get_bool (self : Bool) : Result Bool := Result.ok self /- Trait implementation: [traits::{traits::BoolTrait for bool}] - Source: 'tests/src/traits.rs', lines 12:0-16:1 -/ + Source: 'tests/src/traits.rs', lines 13:0-17:1 -/ @[reducible] def BoolTraitBool : BoolTrait Bool := { get_bool := BoolTraitBool.get_bool } /- [traits::BoolTrait::ret_true]: - Source: 'tests/src/traits.rs', lines 7:4-9:5 -/ + Source: 'tests/src/traits.rs', lines 8:4-10:5 -/ def BoolTrait.ret_true {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := Result.ok true /- [traits::test_bool_trait_bool]: - Source: 'tests/src/traits.rs', lines 18:0-20:1 -/ + Source: 'tests/src/traits.rs', lines 19:0-21:1 -/ def test_bool_trait_bool (x : Bool) : Result Bool := do let b ← BoolTraitBool.get_bool x @@ -41,21 +41,21 @@ def test_bool_trait_bool (x : Bool) : Result Bool := else Result.ok false /- [traits::{traits::BoolTrait for core::option::Option}#1::get_bool]: - Source: 'tests/src/traits.rs', lines 24:4-29:5 -/ + Source: 'tests/src/traits.rs', lines 25:4-30:5 -/ def BoolTraitOption.get_bool {T : Type} (self : Option T) : Result Bool := match self with | none => Result.ok false | some _ => Result.ok true /- Trait implementation: [traits::{traits::BoolTrait for core::option::Option}#1] - Source: 'tests/src/traits.rs', lines 23:0-30:1 -/ + Source: 'tests/src/traits.rs', lines 24:0-31:1 -/ @[reducible] def BoolTraitOption (T : Type) : BoolTrait (Option T) := { get_bool := BoolTraitOption.get_bool } /- [traits::test_bool_trait_option]: - Source: 'tests/src/traits.rs', lines 32:0-34:1 -/ + Source: 'tests/src/traits.rs', lines 33:0-35:1 -/ def test_bool_trait_option {T : Type} (x : Option T) : Result Bool := do let b ← BoolTraitOption.get_bool x @@ -64,30 +64,30 @@ def test_bool_trait_option {T : Type} (x : Option T) : Result Bool := else Result.ok false /- [traits::test_bool_trait]: - Source: 'tests/src/traits.rs', lines 36:0-38:1 -/ + Source: 'tests/src/traits.rs', lines 37:0-39:1 -/ def test_bool_trait {T : Type} (BoolTraitInst : BoolTrait T) (x : T) : Result Bool := BoolTraitInst.get_bool x /- Trait declaration: [traits::ToU64] - Source: 'tests/src/traits.rs', lines 40:0-42:1 -/ + Source: 'tests/src/traits.rs', lines 41:0-43:1 -/ structure ToU64 (Self : Type) where to_u64 : Self → Result U64 /- [traits::{traits::ToU64 for u64}#2::to_u64]: - Source: 'tests/src/traits.rs', lines 45:4-47:5 -/ + Source: 'tests/src/traits.rs', lines 46:4-48:5 -/ def ToU64U64.to_u64 (self : U64) : Result U64 := Result.ok self /- Trait implementation: [traits::{traits::ToU64 for u64}#2] - Source: 'tests/src/traits.rs', lines 44:0-48:1 -/ + Source: 'tests/src/traits.rs', lines 45:0-49:1 -/ @[reducible] def ToU64U64 : ToU64 U64 := { to_u64 := ToU64U64.to_u64 } /- [traits::{traits::ToU64 for (A, A)}#3::to_u64]: - Source: 'tests/src/traits.rs', lines 51:4-53:5 -/ + Source: 'tests/src/traits.rs', lines 52:4-54:5 -/ def ToU64Pair.to_u64 {A : Type} (ToU64Inst : ToU64 A) (self : (A × A)) : Result U64 := do @@ -97,41 +97,41 @@ def ToU64Pair.to_u64 i + i1 /- Trait implementation: [traits::{traits::ToU64 for (A, A)}#3] - Source: 'tests/src/traits.rs', lines 50:0-54:1 -/ + Source: 'tests/src/traits.rs', lines 51:0-55:1 -/ @[reducible] def ToU64Pair {A : Type} (ToU64Inst : ToU64 A) : ToU64 (A × A) := { to_u64 := ToU64Pair.to_u64 ToU64Inst } /- [traits::f]: - Source: 'tests/src/traits.rs', lines 56:0-58:1 -/ + Source: 'tests/src/traits.rs', lines 57:0-59:1 -/ def f {T : Type} (ToU64Inst : ToU64 T) (x : (T × T)) : Result U64 := ToU64Pair.to_u64 ToU64Inst x /- [traits::g]: - Source: 'tests/src/traits.rs', lines 60:0-65:1 -/ + Source: 'tests/src/traits.rs', lines 61:0-66:1 -/ def g {T : Type} (ToU64PairInst : ToU64 (T × T)) (x : (T × T)) : Result U64 := ToU64PairInst.to_u64 x /- [traits::h0]: - Source: 'tests/src/traits.rs', lines 67:0-69:1 -/ + Source: 'tests/src/traits.rs', lines 68:0-70:1 -/ def h0 (x : U64) : Result U64 := ToU64U64.to_u64 x /- [traits::Wrapper] - Source: 'tests/src/traits.rs', lines 71:0-73:1 -/ + Source: 'tests/src/traits.rs', lines 72:0-74:1 -/ structure Wrapper (T : Type) where x : T /- [traits::{traits::ToU64 for traits::Wrapper}#4::to_u64]: - Source: 'tests/src/traits.rs', lines 76:4-78:5 -/ + Source: 'tests/src/traits.rs', lines 77:4-79:5 -/ def ToU64traitsWrapper.to_u64 {T : Type} (ToU64Inst : ToU64 T) (self : Wrapper T) : Result U64 := ToU64Inst.to_u64 self.x /- Trait implementation: [traits::{traits::ToU64 for traits::Wrapper}#4] - Source: 'tests/src/traits.rs', lines 75:0-79:1 -/ + Source: 'tests/src/traits.rs', lines 76:0-80:1 -/ @[reducible] def ToU64traitsWrapper {T : Type} (ToU64Inst : ToU64 T) : ToU64 (Wrapper T) := { @@ -139,39 +139,39 @@ def ToU64traitsWrapper {T : Type} (ToU64Inst : ToU64 T) : ToU64 (Wrapper T) } /- [traits::h1]: - Source: 'tests/src/traits.rs', lines 81:0-83:1 -/ + Source: 'tests/src/traits.rs', lines 82:0-84:1 -/ def h1 (x : Wrapper U64) : Result U64 := ToU64traitsWrapper.to_u64 ToU64U64 x /- [traits::h2]: - Source: 'tests/src/traits.rs', lines 85:0-87:1 -/ + Source: 'tests/src/traits.rs', lines 86:0-88:1 -/ def h2 {T : Type} (ToU64Inst : ToU64 T) (x : Wrapper T) : Result U64 := ToU64traitsWrapper.to_u64 ToU64Inst x /- Trait declaration: [traits::ToType] - Source: 'tests/src/traits.rs', lines 89:0-91:1 -/ + Source: 'tests/src/traits.rs', lines 90:0-92:1 -/ structure ToType (Self : Type) (T : Type) where to_type : Self → Result T /- [traits::{traits::ToType for u64}#5::to_type]: - Source: 'tests/src/traits.rs', lines 94:4-96:5 -/ + Source: 'tests/src/traits.rs', lines 95:4-97:5 -/ def ToTypeU64Bool.to_type (self : U64) : Result Bool := Result.ok (self > 0#u64) /- Trait implementation: [traits::{traits::ToType for u64}#5] - Source: 'tests/src/traits.rs', lines 93:0-97:1 -/ + Source: 'tests/src/traits.rs', lines 94:0-98:1 -/ @[reducible] def ToTypeU64Bool : ToType U64 Bool := { to_type := ToTypeU64Bool.to_type } /- Trait declaration: [traits::OfType] - Source: 'tests/src/traits.rs', lines 99:0-103:1 -/ + Source: 'tests/src/traits.rs', lines 100:0-104:1 -/ structure OfType (Self : Type) where of_type : forall {T : Type} (ToTypeInst : ToType T Self), T → Result Self /- [traits::h3]: - Source: 'tests/src/traits.rs', lines 105:0-107:1 -/ + Source: 'tests/src/traits.rs', lines 106:0-108:1 -/ def h3 {T1 : Type} {T2 : Type} (OfTypeInst : OfType T1) (ToTypeInst : ToType T2 T1) (y : T2) : @@ -180,13 +180,13 @@ def h3 OfTypeInst.of_type ToTypeInst y /- Trait declaration: [traits::OfTypeBis] - Source: 'tests/src/traits.rs', lines 110:0-117:1 -/ + Source: 'tests/src/traits.rs', lines 111:0-118:1 -/ structure OfTypeBis (Self : Type) (T : Type) where ToTypeInst : ToType T Self of_type : T → Result Self /- [traits::h4]: - Source: 'tests/src/traits.rs', lines 119:0-121:1 -/ + Source: 'tests/src/traits.rs', lines 120:0-122:1 -/ def h4 {T1 : Type} {T2 : Type} (OfTypeBisInst : OfTypeBis T1 T2) (ToTypeInst : ToType T2 T1) (y : T2) : @@ -195,26 +195,26 @@ def h4 OfTypeBisInst.of_type y /- [traits::TestType] - Source: 'tests/src/traits.rs', lines 123:0-123:26 -/ + Source: 'tests/src/traits.rs', lines 124:0-124:26 -/ @[reducible] def TestType (T : Type) := T /- [traits::{traits::TestType}#6::test::TestType1] - Source: 'tests/src/traits.rs', lines 128:8-128:30 -/ + Source: 'tests/src/traits.rs', lines 129:8-129:30 -/ @[reducible] def TestType.test.TestType1 := U64 /- Trait declaration: [traits::{traits::TestType}#6::test::TestTrait] - Source: 'tests/src/traits.rs', lines 129:8-131:9 -/ + Source: 'tests/src/traits.rs', lines 130:8-132:9 -/ structure TestType.test.TestTrait (Self : Type) where test : Self → Result Bool /- [traits::{traits::TestType}#6::test::{traits::{traits::TestType}#6::test::TestTrait for traits::{traits::TestType}#6::test::TestType1}::test]: - Source: 'tests/src/traits.rs', lines 140:12-142:13 -/ + Source: 'tests/src/traits.rs', lines 141:12-143:13 -/ def TestType.test.TestTraittraitsTestTypetestTestType1.test (self : TestType.test.TestType1) : Result Bool := Result.ok (self > 1#u64) /- Trait implementation: [traits::{traits::TestType}#6::test::{traits::{traits::TestType}#6::test::TestTrait for traits::{traits::TestType}#6::test::TestType1}] - Source: 'tests/src/traits.rs', lines 139:8-143:9 -/ + Source: 'tests/src/traits.rs', lines 140:8-144:9 -/ @[reducible] def TestType.test.TestTraittraitsTestTypetestTestType1 : TestType.test.TestTrait TestType.test.TestType1 := { @@ -222,7 +222,7 @@ def TestType.test.TestTraittraitsTestTypetestTestType1 : } /- [traits::{traits::TestType}#6::test]: - Source: 'tests/src/traits.rs', lines 127:4-148:5 -/ + Source: 'tests/src/traits.rs', lines 128:4-149:5 -/ def TestType.test {T : Type} (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := do @@ -232,11 +232,11 @@ def TestType.test else Result.ok false /- [traits::BoolWrapper] - Source: 'tests/src/traits.rs', lines 151:0-151:33 -/ + Source: 'tests/src/traits.rs', lines 152:0-152:33 -/ @[reducible] def BoolWrapper := Bool /- [traits::{traits::ToType for traits::BoolWrapper}#7::to_type]: - Source: 'tests/src/traits.rs', lines 157:4-159:5 -/ + Source: 'tests/src/traits.rs', lines 158:4-160:5 -/ def ToTypetraitsBoolWrapperT.to_type {T : Type} (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) : Result T @@ -244,7 +244,7 @@ def ToTypetraitsBoolWrapperT.to_type ToTypeBoolTInst.to_type self /- Trait implementation: [traits::{traits::ToType for traits::BoolWrapper}#7] - Source: 'tests/src/traits.rs', lines 153:0-160:1 -/ + Source: 'tests/src/traits.rs', lines 154:0-161:1 -/ @[reducible] def ToTypetraitsBoolWrapperT {T : Type} (ToTypeBoolTInst : ToType Bool T) : ToType BoolWrapper T := { @@ -252,14 +252,14 @@ def ToTypetraitsBoolWrapperT {T : Type} (ToTypeBoolTInst : ToType Bool T) : } /- [traits::WithConstTy::LEN2] - Source: 'tests/src/traits.rs', lines 165:4-165:27 -/ + Source: 'tests/src/traits.rs', lines 166:4-166:27 -/ def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize := Result.ok 32#usize def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize := eval_global (WithConstTy.LEN2_default_body Self LEN) /- Trait declaration: [traits::WithConstTy] - Source: 'tests/src/traits.rs', lines 162:0-173:1 -/ + Source: 'tests/src/traits.rs', lines 163:0-174:1 -/ structure WithConstTy (Self : Type) (LEN : Usize) where LEN1 : Usize LEN2 : Usize @@ -269,17 +269,17 @@ structure WithConstTy (Self : Type) (LEN : Usize) where f : W → Array U8 LEN → Result W /- [traits::{traits::WithConstTy<32: usize> for bool}#8::LEN1] - Source: 'tests/src/traits.rs', lines 176:4-176:27 -/ + Source: 'tests/src/traits.rs', lines 177:4-177:27 -/ def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12#usize def WithConstTyBool32.LEN1 : Usize := eval_global WithConstTyBool32.LEN1_body /- [traits::{traits::WithConstTy<32: usize> for bool}#8::f]: - Source: 'tests/src/traits.rs', lines 181:4-181:42 -/ + Source: 'tests/src/traits.rs', lines 182:4-182:42 -/ def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 := Result.ok i /- Trait implementation: [traits::{traits::WithConstTy<32: usize> for bool}#8] - Source: 'tests/src/traits.rs', lines 175:0-182:1 -/ + Source: 'tests/src/traits.rs', lines 176:0-183:1 -/ @[reducible] def WithConstTyBool32 : WithConstTy Bool 32#usize := { LEN1 := WithConstTyBool32.LEN1 @@ -291,7 +291,7 @@ def WithConstTyBool32 : WithConstTy Bool 32#usize := { } /- [traits::use_with_const_ty1]: - Source: 'tests/src/traits.rs', lines 184:0-186:1 -/ + Source: 'tests/src/traits.rs', lines 185:0-187:1 -/ def use_with_const_ty1 {H : Type} {LEN : Usize} (WithConstTyInst : WithConstTy H LEN) : Result Usize @@ -299,7 +299,7 @@ def use_with_const_ty1 Result.ok WithConstTyInst.LEN1 /- [traits::use_with_const_ty2]: - Source: 'tests/src/traits.rs', lines 188:0-188:76 -/ + Source: 'tests/src/traits.rs', lines 189:0-189:76 -/ def use_with_const_ty2 {H : Type} {LEN : Usize} (WithConstTyInst : WithConstTy H LEN) (w : WithConstTyInst.W) : @@ -308,7 +308,7 @@ def use_with_const_ty2 Result.ok () /- [traits::use_with_const_ty3]: - Source: 'tests/src/traits.rs', lines 190:0-192:1 -/ + Source: 'tests/src/traits.rs', lines 191:0-193:1 -/ def use_with_const_ty3 {H : Type} {LEN : Usize} (WithConstTyInst : WithConstTy H LEN) (x : WithConstTyInst.W) : @@ -317,12 +317,12 @@ def use_with_const_ty3 WithConstTyInst.ToU64traitsWithConstTyWInst.to_u64 x /- [traits::test_where1]: - Source: 'tests/src/traits.rs', lines 194:0-194:43 -/ + Source: 'tests/src/traits.rs', lines 195:0-195:43 -/ def test_where1 {T : Type} (_x : T) : Result Unit := Result.ok () /- [traits::test_where2]: - Source: 'tests/src/traits.rs', lines 195:0-195:60 -/ + Source: 'tests/src/traits.rs', lines 196:0-196:60 -/ def test_where2 {T : Type} (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) : Result Unit @@ -330,30 +330,30 @@ def test_where2 Result.ok () /- Trait declaration: [traits::ParentTrait0] - Source: 'tests/src/traits.rs', lines 201:0-205:1 -/ + Source: 'tests/src/traits.rs', lines 202:0-206:1 -/ structure ParentTrait0 (Self : Type) where W : Type get_name : Self → Result String get_w : Self → Result W /- Trait declaration: [traits::ParentTrait1] - Source: 'tests/src/traits.rs', lines 206:0-206:25 -/ + Source: 'tests/src/traits.rs', lines 207:0-207:25 -/ structure ParentTrait1 (Self : Type) where /- Trait declaration: [traits::ChildTrait] - Source: 'tests/src/traits.rs', lines 207:0-207:52 -/ + Source: 'tests/src/traits.rs', lines 208:0-208:52 -/ structure ChildTrait (Self : Type) where ParentTrait0Inst : ParentTrait0 Self ParentTrait1Inst : ParentTrait1 Self /- [traits::test_child_trait1]: - Source: 'tests/src/traits.rs', lines 210:0-212:1 -/ + Source: 'tests/src/traits.rs', lines 211:0-213:1 -/ def test_child_trait1 {T : Type} (ChildTraitInst : ChildTrait T) (x : T) : Result String := ChildTraitInst.ParentTrait0Inst.get_name x /- [traits::test_child_trait2]: - Source: 'tests/src/traits.rs', lines 214:0-216:1 -/ + Source: 'tests/src/traits.rs', lines 215:0-217:1 -/ def test_child_trait2 {T : Type} (ChildTraitInst : ChildTrait T) (x : T) : Result ChildTraitInst.ParentTrait0Inst.W @@ -361,7 +361,7 @@ def test_child_trait2 ChildTraitInst.ParentTrait0Inst.get_w x /- [traits::order1]: - Source: 'tests/src/traits.rs', lines 220:0-220:62 -/ + Source: 'tests/src/traits.rs', lines 221:0-221:62 -/ def order1 {T : Type} {U : Type} (ParentTrait0Inst : ParentTrait0 T) (ParentTrait0Inst1 : ParentTrait0 U) : @@ -370,30 +370,30 @@ def order1 Result.ok () /- Trait declaration: [traits::ChildTrait1] - Source: 'tests/src/traits.rs', lines 223:0-223:38 -/ + Source: 'tests/src/traits.rs', lines 224:0-224:38 -/ structure ChildTrait1 (Self : Type) where ParentTrait1Inst : ParentTrait1 Self /- Trait implementation: [traits::{traits::ParentTrait1 for usize}#9] - Source: 'tests/src/traits.rs', lines 225:0-225:30 -/ + Source: 'tests/src/traits.rs', lines 226:0-226:30 -/ @[reducible] def ParentTrait1Usize : ParentTrait1 Usize := { } /- Trait implementation: [traits::{traits::ChildTrait1 for usize}#10] - Source: 'tests/src/traits.rs', lines 226:0-226:29 -/ + Source: 'tests/src/traits.rs', lines 227:0-227:29 -/ @[reducible] def ChildTrait1Usize : ChildTrait1 Usize := { ParentTrait1Inst := ParentTrait1Usize } /- Trait declaration: [traits::Iterator] - Source: 'tests/src/traits.rs', lines 230:0-232:1 -/ + Source: 'tests/src/traits.rs', lines 231:0-233:1 -/ structure Iterator (Self : Type) where Item : Type /- Trait declaration: [traits::IntoIterator] - Source: 'tests/src/traits.rs', lines 234:0-240:1 -/ + Source: 'tests/src/traits.rs', lines 235:0-241:1 -/ structure IntoIterator (Self : Type) where Item : Type IntoIter : Type @@ -401,42 +401,42 @@ structure IntoIterator (Self : Type) where into_iter : Self → Result IntoIter /- Trait declaration: [traits::FromResidual] - Source: 'tests/src/traits.rs', lines 251:0-251:24 -/ + Source: 'tests/src/traits.rs', lines 252:0-252:24 -/ structure FromResidual (Self : Type) (T : Type) where /- Trait declaration: [traits::Try] - Source: 'tests/src/traits.rs', lines 247:0-249:1 -/ + Source: 'tests/src/traits.rs', lines 248:0-250:1 -/ structure Try (Self : Type) where Residual : Type FromResidualSelftraitsTryResidualInst : FromResidual Self Residual /- Trait declaration: [traits::WithTarget] - Source: 'tests/src/traits.rs', lines 253:0-255:1 -/ + Source: 'tests/src/traits.rs', lines 254:0-256:1 -/ structure WithTarget (Self : Type) where Target : Type /- Trait declaration: [traits::ParentTrait2] - Source: 'tests/src/traits.rs', lines 257:0-259:1 -/ + Source: 'tests/src/traits.rs', lines 258:0-260:1 -/ structure ParentTrait2 (Self : Type) where U : Type WithTargettraitsParentTrait2UInst : WithTarget U /- Trait declaration: [traits::ChildTrait2] - Source: 'tests/src/traits.rs', lines 261:0-263:1 -/ + Source: 'tests/src/traits.rs', lines 262:0-264:1 -/ structure ChildTrait2 (Self : Type) where ParentTrait2Inst : ParentTrait2 Self convert : ParentTrait2Inst.U → Result ParentTrait2Inst.WithTargettraitsParentTrait2UInst.Target /- Trait implementation: [traits::{traits::WithTarget for u32}#11] - Source: 'tests/src/traits.rs', lines 265:0-267:1 -/ + Source: 'tests/src/traits.rs', lines 266:0-268:1 -/ @[reducible] def WithTargetU32 : WithTarget U32 := { Target := U32 } /- Trait implementation: [traits::{traits::ParentTrait2 for u32}#12] - Source: 'tests/src/traits.rs', lines 269:0-271:1 -/ + Source: 'tests/src/traits.rs', lines 270:0-272:1 -/ @[reducible] def ParentTrait2U32 : ParentTrait2 U32 := { U := U32 @@ -444,12 +444,12 @@ def ParentTrait2U32 : ParentTrait2 U32 := { } /- [traits::{traits::ChildTrait2 for u32}#13::convert]: - Source: 'tests/src/traits.rs', lines 274:4-276:5 -/ + Source: 'tests/src/traits.rs', lines 275:4-277:5 -/ def ChildTrait2U32.convert (x : U32) : Result U32 := Result.ok x /- Trait implementation: [traits::{traits::ChildTrait2 for u32}#13] - Source: 'tests/src/traits.rs', lines 273:0-277:1 -/ + Source: 'tests/src/traits.rs', lines 274:0-278:1 -/ @[reducible] def ChildTrait2U32 : ChildTrait2 U32 := { ParentTrait2Inst := ParentTrait2U32 @@ -457,55 +457,55 @@ def ChildTrait2U32 : ChildTrait2 U32 := { } /- Trait declaration: [traits::CFnOnce] - Source: 'tests/src/traits.rs', lines 287:0-291:1 -/ + Source: 'tests/src/traits.rs', lines 288:0-292:1 -/ structure CFnOnce (Self : Type) (Args : Type) where Output : Type call_once : Self → Args → Result Output /- Trait declaration: [traits::CFnMut] - Source: 'tests/src/traits.rs', lines 293:0-295:1 -/ + Source: 'tests/src/traits.rs', lines 294:0-296:1 -/ structure CFnMut (Self : Type) (Args : Type) where CFnOnceInst : CFnOnce Self Args call_mut : Self → Args → Result (CFnOnceInst.Output × Self) /- Trait declaration: [traits::CFn] - Source: 'tests/src/traits.rs', lines 297:0-299:1 -/ + Source: 'tests/src/traits.rs', lines 298:0-300:1 -/ structure CFn (Self : Type) (Args : Type) where CFnMutInst : CFnMut Self Args call : Self → Args → Result CFnMutInst.CFnOnceInst.Output /- Trait declaration: [traits::GetTrait] - Source: 'tests/src/traits.rs', lines 301:0-304:1 -/ + Source: 'tests/src/traits.rs', lines 302:0-305:1 -/ structure GetTrait (Self : Type) where W : Type get_w : Self → Result W /- [traits::test_get_trait]: - Source: 'tests/src/traits.rs', lines 306:0-308:1 -/ + Source: 'tests/src/traits.rs', lines 307:0-309:1 -/ def test_get_trait {T : Type} (GetTraitInst : GetTrait T) (x : T) : Result GetTraitInst.W := GetTraitInst.get_w x /- Trait declaration: [traits::Trait] - Source: 'tests/src/traits.rs', lines 311:0-313:1 -/ + Source: 'tests/src/traits.rs', lines 312:0-314:1 -/ structure Trait (Self : Type) where LEN : Usize /- [traits::{traits::Trait for @Array}#14::LEN] - Source: 'tests/src/traits.rs', lines 316:4-316:25 -/ + Source: 'tests/src/traits.rs', lines 317:4-317:25 -/ def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N def TraitArray.LEN (T : Type) (N : Usize) : Usize := eval_global (TraitArray.LEN_body T N) /- Trait implementation: [traits::{traits::Trait for @Array}#14] - Source: 'tests/src/traits.rs', lines 315:0-317:1 -/ + Source: 'tests/src/traits.rs', lines 316:0-318:1 -/ @[reducible] def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := { LEN := TraitArray.LEN T N } /- [traits::{traits::Trait for traits::Wrapper}#15::LEN] - Source: 'tests/src/traits.rs', lines 320:4-320:25 -/ + Source: 'tests/src/traits.rs', lines 321:4-321:25 -/ def TraittraitsWrapper.LEN_body {T : Type} (TraitInst : Trait T) : Result Usize := Result.ok 0#usize @@ -513,7 +513,7 @@ def TraittraitsWrapper.LEN {T : Type} (TraitInst : Trait T) : Usize := eval_global (TraittraitsWrapper.LEN_body TraitInst) /- Trait implementation: [traits::{traits::Trait for traits::Wrapper}#15] - Source: 'tests/src/traits.rs', lines 319:0-321:1 -/ + Source: 'tests/src/traits.rs', lines 320:0-322:1 -/ @[reducible] def TraittraitsWrapper {T : Type} (TraitInst : Trait T) : Trait (Wrapper T) := { @@ -521,12 +521,12 @@ def TraittraitsWrapper {T : Type} (TraitInst : Trait T) : Trait (Wrapper T) } /- [traits::use_wrapper_len]: - Source: 'tests/src/traits.rs', lines 323:0-325:1 -/ + Source: 'tests/src/traits.rs', lines 324:0-326:1 -/ def use_wrapper_len {T : Type} (TraitInst : Trait T) : Result Usize := Result.ok (TraittraitsWrapper TraitInst).LEN /- [traits::Foo] - Source: 'tests/src/traits.rs', lines 327:0-330:1 -/ + Source: 'tests/src/traits.rs', lines 328:0-331:1 -/ structure Foo (T : Type) (U : Type) where x : T y : U @@ -539,7 +539,7 @@ inductive core.result.Result (T : Type) (E : Type) := | Err : E → core.result.Result T E /- [traits::{traits::Foo}#16::FOO] - Source: 'tests/src/traits.rs', lines 333:4-333:43 -/ + Source: 'tests/src/traits.rs', lines 334:4-334:43 -/ def Foo.FOO_body {T : Type} (U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) := Result.ok (core.result.Result.Err 0#i32) @@ -548,7 +548,7 @@ def Foo.FOO {T : Type} (U : Type) (TraitInst : Trait T) eval_global (Foo.FOO_body U TraitInst) /- [traits::use_foo1]: - Source: 'tests/src/traits.rs', lines 336:0-338:1 -/ + Source: 'tests/src/traits.rs', lines 337:0-339:1 -/ def use_foo1 {T : Type} (U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) @@ -556,7 +556,7 @@ def use_foo1 Result.ok (Foo.FOO U TraitInst) /- [traits::use_foo2]: - Source: 'tests/src/traits.rs', lines 340:0-342:1 -/ + Source: 'tests/src/traits.rs', lines 341:0-343:1 -/ def use_foo2 (T : Type) {U : Type} (TraitInst : Trait U) : Result (core.result.Result U I32) diff --git a/tests/src/adt-borrows.rs b/tests/src/adt-borrows.rs new file mode 100644 index 00000000..8e7e71f8 --- /dev/null +++ b/tests/src/adt-borrows.rs @@ -0,0 +1,84 @@ +//@ [coq,fstar] subdir=misc +//! This file contains tests with ADTs containing borrows. + +struct SharedWrapper<'a, T>(&'a T); + +impl<'a, T> SharedWrapper<'a, T> { + fn create(x: &'a T) -> Self { + SharedWrapper(x) + } + + fn unwrap(self: Self) -> &'a T { + self.0 + } +} + +struct SharedWrapper1<'a, T> { + x: &'a T, +} + +impl<'a, T> SharedWrapper1<'a, T> { + fn create(x: &'a T) -> Self { + SharedWrapper1 { x } + } + + fn unwrap(self: Self) -> &'a T { + self.x + } +} + +struct SharedWrapper2<'a, 'b, T> { + x: &'a T, + y: &'b T, +} + +impl<'a, 'b, T> SharedWrapper2<'a, 'b, T> { + fn create(x: &'a T, y: &'b T) -> Self { + SharedWrapper2 { x, y } + } + + fn unwrap(self: Self) -> (&'a T, &'b T) { + (self.x, self.y) + } +} + +struct MutWrapper<'a, T>(&'a mut T); + +impl<'a, T> MutWrapper<'a, T> { + fn create(x: &'a mut T) -> Self { + MutWrapper(x) + } + + fn unwrap(self: Self) -> &'a mut T { + self.0 + } +} + +struct MutWrapper1<'a, T> { + x: &'a mut T, +} + +impl<'a, T> MutWrapper1<'a, T> { + fn create(x: &'a mut T) -> Self { + MutWrapper1 { x } + } + + fn unwrap(self: Self) -> &'a mut T { + self.x + } +} + +struct MutWrapper2<'a, 'b, T> { + x: &'a mut T, + y: &'b mut T, +} + +impl<'a, 'b, T> MutWrapper2<'a, 'b, T> { + fn create(x: &'a mut T, y: &'b mut T) -> Self { + MutWrapper2 { x, y } + } + + fn unwrap(self: Self) -> (&'a mut T, &'b mut T) { + (self.x, self.y) + } +} diff --git a/tests/src/issue-270-loop-list.rs b/tests/src/issue-270-loop-list.rs index b92f7630..6e8347fd 100644 --- a/tests/src/issue-270-loop-list.rs +++ b/tests/src/issue-270-loop-list.rs @@ -4,12 +4,10 @@ pub enum List { Nil, } - fn foo(v: &List>) { if let List::Cons(_, t) = v { let mut t = &**t; - while let List::Cons(_, tt) = t - { + while let List::Cons(_, tt) = t { t = &**tt; } } diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 360e4c15..78bafece 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -6,12 +6,11 @@ Uncaught exception: (Failure "In file Translate.ml, line 850:\ - \nIn file Translate.ml, line 850:\ \nMutually recursive trait declarations are not supported") -Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 52, characters 4-76 +Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 52, characters 4-23 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 879, characters 2-52 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1006, characters 2-36 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1576, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 318, characters 14-66 +Called from Dune__exe__Main in file "Main.ml", line 321, characters 14-66 diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index 9d1c397f..94fa69cc 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -529,6 +529,10 @@ pub fn not_i32(x: i32) -> i32 { !x } +fn borrow_mut_tuple(x: &mut (T, U)) -> &mut (T, U) { + x +} + // Testing the simplification of the ADT aggregates in the presence of symbolic expansions mod ExpandSimpliy { pub struct Wrapper(T, T); diff --git a/tests/src/traits.rs b/tests/src/traits.rs index 36389cdf..9b593c85 100644 --- a/tests/src/traits.rs +++ b/tests/src/traits.rs @@ -1,4 +1,5 @@ //@ [fstar] aeneas-args=-decreases-clauses +//@ aeneas-args=-soft-warnings pub trait BoolTrait { // Required method fn get_bool(&self) -> bool;