diff options
28 files changed, 439 insertions, 602 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6b5aacf0..eeb92c51 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -4,13 +4,33 @@ on: pull_request: workflow_dispatch: +# Minimum permissions required by skip-duplicate-actions +permissions: + actions: write + contents: read + jobs: + # Avoid `push` and `pull_request` running the same job twice + check_if_skip_duplicate_job: + runs-on: [self-hosted, linux, nix] + steps: + - id: skip_check + uses: fkirc/skip-duplicate-actions@v5 + with: + concurrent_skipping: 'same_content_newer' + skip_after_successful_duplicate: 'true' + outputs: + should_skip: ${{ steps.skip_check.outputs.should_skip }} + nix: #runs-on: ubuntu-latest runs-on: [self-hosted, linux, nix] + needs: check_if_skip_duplicate_job + if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true' steps: #- uses: cachix/install-nix-action@v22 - uses: actions/checkout@v4 + - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness - run: nix build -L .#aeneas - run: nix build -L .#checks.x86_64-linux.aeneas-tests - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar @@ -18,8 +38,11 @@ jobs: - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4 # Lean doesn't work with Nix #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean + lean: # Lean isn't supported by Nix, so we put it in a different job runs-on: [ubuntu-latest] + needs: check_if_skip_duplicate_job + if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true' steps: # Install curl - run: sudo apt update && sudo apt install curl @@ -72,7 +72,6 @@ tests/fstar/misc/obj/ nohup.out .vscode *# -*.lock *.txt */.#* *.smt2 @@ -31,9 +31,8 @@ AENEAS_EXE ?= bin/aeneas # The user can specify additional translation options for Aeneas. # By default we activate the (expensive) sanity checks. -OPTIONS ?= -checks +OPTIONS ?= -# # The rules use (and update) the following variables # # The Charon test directory where to look for the .llbc files @@ -84,7 +83,7 @@ doc: cd compiler && dune build @doc .PHONY: clean -clean: +clean: clean-generated cd compiler && dune clean # Test the project by translating test files to F* @@ -100,6 +99,12 @@ test-all: test-no_nested_borrows test-paper \ test-loops \ test-arrays test-traits test-bitwise test-demo +.PHONY: clean-generated +clean-generated: + # We can't put this line in `tests/Makefile` otherwise it will detect itself. + # FIXME: generation of hol4 files is deactivated so we don't delete those. + grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm + # Verify the F* files generated by the translation .PHONY: verify verify: @@ -108,7 +113,8 @@ verify: # Reformat the project .PHONY: format format: - cd compiler && dune build @fmt --auto-promote + @# `|| `true` because the command returns an error if it changed anything, which we don't care about. + cd compiler && dune fmt || true # The commands to run Charon to generate the .llbc files ifeq (, $(REGEN_LLBC)) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index e30c4b36..f2686cc6 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1998,10 +1998,11 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with | Some name -> (* Yes: register the custom binding *) - ctx_add def.meta decl name ctx + ctx_add def.item_meta.meta decl name ctx | None -> (* Not the case: "standard" registration *) - let name = ctx_compute_global_name def.meta ctx def.name in + let name = ctx_compute_global_name def.item_meta.meta ctx def.name in + let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in (* If this is a provided constant (i.e., the default value for a constant in a trait declaration) we add a suffix. Otherwise there is a clash @@ -2010,8 +2011,8 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : let suffix = match def.kind with TraitItemProvided _ -> "_default" | _ -> "" in - let ctx = ctx_add def.meta decl (name ^ suffix) ctx in - let ctx = ctx_add def.meta body (name ^ suffix ^ "_body") ctx in + let ctx = ctx_add def.item_meta.meta decl (name ^ suffix) ctx in + let ctx = ctx_add def.item_meta.meta body (name ^ suffix ^ "_body") ctx in ctx let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f194d4e5..ddfbf312 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -147,7 +147,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* Sanity check: global bodies don't contain stateful calls *) cassert __FILE__ __LINE__ ((not f.is_global_decl_body) || not !stateful) - f.meta "Global definition containing a stateful call in its body"; + f.item_meta.meta + "Global definition containing a stateful call in its body"; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; @@ -171,11 +172,11 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in cassert __FILE__ __LINE__ ((not is_global_decl_body) || List.length d = 1) - (List.hd d).meta + (List.hd d).item_meta.meta "This global definition is in a group of mutually recursive definitions"; cassert __FILE__ __LINE__ ((not !group_has_builtin_info) || List.length d = 1) - (List.hd d).meta + (List.hd d).item_meta.meta "This builtin function belongs to a group of mutually recursive \ definitions"; (* We ignore on purpose functions that cannot fail and consider they *can* diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 769e3144..f10c8d3e 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -196,12 +196,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : (List.for_all (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) (sg.output :: sg.inputs)) - fdef.meta "Nested borrows are not supported yet"; + fdef.item_meta.meta "Nested borrows are not supported yet"; cassert __FILE__ __LINE__ (List.for_all (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) (sg.output :: sg.inputs)) - fdef.meta "ADTs containing borrows are not supported yet"; + fdef.item_meta.meta "ADTs containing borrows are not supported yet"; (* Create the context *) let regions_hierarchy = @@ -211,23 +211,25 @@ 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 fdef.meta ctx region_groups sg.generics.types + initialize_eval_ctx fdef.item_meta.meta 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.meta ctx fdef.signature regions_hierarchy - fdef.kind + symbolic_instantiate_fun_sig fdef.item_meta.meta 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.meta ty) inst_sg.inputs + List.map + (fun ty -> mk_fresh_symbolic_value fdef.item_meta.meta 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.meta; + sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.item_meta.meta; 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 *) @@ -249,14 +251,14 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : Collections.List.split_at (List.tl body.locals) body.arg_count in (* Push the return variable (initialized with ⊥) *) - let ctx = ctx_push_uninitialized_var fdef.meta ctx ret_var in + let ctx = ctx_push_uninitialized_var fdef.item_meta.meta 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.meta ctx (List.combine input_vars input_values) + ctx_push_vars fdef.item_meta.meta ctx (List.combine input_vars input_values) in (* Push the remaining local variables (initialized with ⊥) *) - let ctx = ctx_push_uninitialized_vars fdef.meta ctx local_vars in + let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx local_vars in (* Return *) (ctx, input_svs, inst_sg) @@ -290,7 +292,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 ~meta:(Some fdef.meta) ctx)); + ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.item_meta.meta) 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 @@ -299,13 +301,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.meta ctx fdef.signature regions_hierarchy - fdef.kind + symbolic_instantiate_fun_sig fdef.item_meta.meta 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 cf_pop_frame = pop_frame config fdef.meta pop_return_value in + let cf_pop_frame = pop_frame config fdef.item_meta.meta pop_return_value 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 @@ -333,8 +335,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.meta ctx abs.regions - abs.ancestors_regions ret_value ret_rty + apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx + abs.regions abs.ancestors_regions ret_value ret_rty in (ctx, [ avalue ]) in @@ -349,7 +351,8 @@ 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.meta; + sanity_check __FILE__ __LINE__ (region_can_end back_id) + fdef.item_meta.meta; let ctx = create_push_abstractions_from_abs_region_groups (fun rg_id -> SynthRet rg_id) @@ -439,7 +442,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.meta; + fdef.item_meta.meta; (* Loop abstractions *) let rg_id' = Option.get rg_id' in if rg_id' = back_id && inside_loop then @@ -448,7 +451,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) | Loop (loop_id', _, LoopCall) -> (* We can end all the loop call abstractions *) sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') - fdef.meta; + fdef.item_meta.meta; { abs with can_end = true } | SynthInput rg_id' -> if rg_id' = back_id && end_fun_synth_input then @@ -468,7 +471,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let target_abs_ids = List.append parent_input_abs_ids current_abs_id in let cf_end_target_abs cf = List.fold_left - (fun cf id -> end_abstraction config fdef.meta id cf) + (fun cf id -> end_abstraction config fdef.item_meta.meta id cf) cf target_abs_ids in (* Generate the Return node *) @@ -534,7 +537,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) let fwd_e = (* Pop the frame and retrieve the returned value at the same time*) let pop_return_value = true in - let cf_pop = pop_frame config fdef.meta pop_return_value in + let cf_pop = + pop_frame config fdef.item_meta.meta pop_return_value + in (* Generate the Return node *) let cf_return ret_value : m_fun = fun ctx -> Some (SA.Return (ctx, ret_value)) @@ -551,7 +556,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.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable" in let is_regular_return = true in let inside_loop = Option.is_some loop_id in @@ -577,14 +582,16 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) match res with | EndEnterLoop _ -> false | EndContinue _ -> true - | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable" in (* Forward translation *) let fwd_e = (* Pop the frame - there is no returned value to pop: in the translation we will simply call the loop function *) let pop_return_value = false in - let cf_pop = pop_frame config fdef.meta pop_return_value in + let cf_pop = + pop_frame config fdef.item_meta.meta pop_return_value + in (* Generate the Return node *) let cf_return _ret_value : m_fun = fun _ctx -> Some (SA.ReturnWithLoop (loop_id, inside_loop)) @@ -618,7 +625,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) * the executions can lead to a panic *) if synthesize then Some SA.Panic else None | Unit | Break _ | Continue _ -> - craise __FILE__ __LINE__ fdef.meta + craise __FILE__ __LINE__ fdef.item_meta.meta ("evaluate_function_symbolic failed on: " ^ name_to_string ()) in @@ -652,14 +659,14 @@ module Test = struct (* Sanity check - *) sanity_check __FILE__ __LINE__ (fdef.signature.generics = empty_generic_params) - fdef.meta; - sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.meta; + fdef.item_meta.meta; + sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.item_meta.meta; (* Create the evaluation context *) - let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in + let ctx = initialize_eval_ctx fdef.item_meta.meta decls_ctx [] [] [] in (* Insert the (uninitialized) local variables *) - let ctx = ctx_push_uninitialized_vars fdef.meta ctx body.locals in + let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx body.locals in (* Create the continuation to check the function's result *) let config = mk_config ConcreteMode in @@ -668,9 +675,11 @@ module Test = struct | Return -> (* Ok: drop the local variables and finish *) let pop_return_value = true in - pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx + pop_frame config fdef.item_meta.meta pop_return_value + (fun _ _ -> None) + ctx | _ -> - craise __FILE__ __LINE__ fdef.meta + craise __FILE__ __LINE__ fdef.item_meta.meta ("Unit test failed (concrete execution) on: " ^ Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env decls_ctx) diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index e710ed2b..3db68f5d 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -714,7 +714,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct both borrows *) raise (ValueMatchFailure (LoanInLeft id0)) - let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -729,11 +729,18 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta; - (* We simply introduce a fresh symbolic value *) + (* TODO: the symbolic values may contain bottoms: we're being conservatice, + and fail (for now) if part of a symbolic value contains a bottom. + A more general approach would be to introduce a symbolic value + with some ended regions. *) + sanity_check __FILE__ __LINE__ + ((not (symbolic_value_has_ended_regions ctx0.ended_regions sv0)) + && not (symbolic_value_has_ended_regions ctx1.ended_regions sv1)) + meta; mk_fresh_symbolic_value meta sv0.sv_ty) - let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) - (sv : symbolic_value) (v : typed_value) : typed_value = + let match_symbolic_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) + (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = (* Check that: - there are no borrows in the symbolic value - there are no borrows in the "regular" value @@ -763,8 +770,16 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct | Some (VMutLoan id) -> if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) else raise (ValueMatchFailure (LoanInRight id))); - (* Return a fresh symbolic value *) - mk_fresh_symbolic_typed_value meta sv.sv_ty + + (* There might be a bottom in the other value. We're being conservative: + if there is a bottom anywhere (it includes the case where part of the + value contains bottom) the result of the join is bottom. Otherwise, + we generate a fresh symbolic value. *) + if + symbolic_value_has_ended_regions ctx0.ended_regions sv + || bottom_in_value ctx1.ended_regions v + then mk_bottom meta sv.sv_ty + else mk_fresh_symbolic_typed_value meta sv.sv_ty let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = @@ -903,9 +918,16 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (sv1 : symbolic_value) : symbolic_value = sv1 - let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) - (sv : symbolic_value) (v : typed_value) : typed_value = - if left then v else mk_typed_value_from_symbolic_value sv + let match_symbolic_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) + (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = + (* We're being conservative for now: if any of the two values contains + a bottom, the join is bottom *) + if + symbolic_value_has_ended_regions ctx0.ended_regions sv + || bottom_in_value ctx1.ended_regions v + then mk_bottom meta sv.sv_ty + else if left then v + else mk_typed_value_from_symbolic_value sv let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (v : typed_value) : typed_value = diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index de89f316..9ad6487b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1063,13 +1063,13 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) (* Treat the evaluation of the global as a call to the global body *) let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in - (eval_transparent_function_call_concrete config global.meta global.body - call) + (eval_transparent_function_call_concrete config global.item_meta.meta + global.body call) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) - cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.meta + cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.item_meta.meta "Const globals should not contain regions"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) @@ -1082,9 +1082,9 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self global.ty in - let sval = mk_fresh_symbolic_value global.meta ty in + let sval = mk_fresh_symbolic_value global.item_meta.meta ty in let cc = - assign_to_place config global.meta + assign_to_place config global.item_meta.meta (mk_typed_value_from_symbolic_value sval) dest in @@ -1368,7 +1368,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) (* Sanity check: same number of inputs *) sanity_check __FILE__ __LINE__ (List.length call.args = List.length def.signature.inputs) - def.meta; + def.item_meta.meta; (* Sanity check: no nested borrows, borrows in ADTs, etc. *) cassert __FILE__ __LINE__ (List.for_all @@ -1381,9 +1381,9 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) (inst_sg.output :: inst_sg.inputs)) meta "ADTs containing borrows are not supported yet"; (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config def.meta func def.signature - regions_hierarchy inst_sg generics trait_method_generics call.args call.dest - cf ctx + eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func + def.signature regions_hierarchy inst_sg generics trait_method_generics + call.args call.dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index a46ef79c..c84cd39c 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -446,7 +446,7 @@ let apply_passes (crate : crate) : crate = report to the user the fact that we will ignore the function body *) let fmt = Print.Crate.crate_to_fmt_env crate in let name = Print.name_to_string fmt f.name in - save_error __FILE__ __LINE__ (Some f.meta) + save_error __FILE__ __LINE__ (Some f.item_meta.meta) ("Ignoring the body of '" ^ name ^ "' because of previous error"); { f with body = None } in diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 713cdef9..21be89ee 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -323,7 +323,8 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) List.map (fun ((fid, d) : FunDeclId.id * fun_decl) -> ( FRegular fid, - (Types.name_to_string env d.name, d.signature, Some d.meta) )) + (Types.name_to_string env d.name, d.signature, Some d.item_meta.meta) + )) (FunDeclId.Map.bindings fun_decls) in let assumed = diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 15b52237..6c925bcd 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -584,16 +584,16 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let name = Print.Types.name_to_string env def.name in let { T.regions; types; const_generics; trait_clauses } = def.generics in (* Can't translate types with regions for now *) - cassert __FILE__ __LINE__ (regions = []) def.meta + cassert __FILE__ __LINE__ (regions = []) def.item_meta.meta "ADTs containing borrows are not supported yet"; let trait_clauses = - List.map (translate_trait_clause def.meta) trait_clauses + List.map (translate_trait_clause def.item_meta.meta) trait_clauses in let generics = { types; const_generics; trait_clauses } in - let kind = translate_type_decl_kind def.meta def.T.kind in - let preds = translate_predicates def.meta def.preds in + let kind = translate_type_decl_kind def.item_meta.meta def.T.kind in + let preds = translate_predicates def.item_meta.meta def.preds in let is_local = def.is_local in - let meta = def.meta in + let meta = def.item_meta.meta in { def_id; is_local; @@ -618,7 +618,7 @@ let translate_type_id (meta : Meta.meta) (id : T.type_id) : type_id = | T.TBox -> (* Boxes have to be eliminated: this type id shouldn't be translated *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ meta "Unexpected box type" in TAssumed aty | TTuple -> TTuple @@ -1262,7 +1262,9 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx) let regions_hierarchy = FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies in - let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).meta in + let meta = + (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).item_meta.meta + in translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx (FunId (FRegular fun_id)) regions_hierarchy sg input_names @@ -1624,7 +1626,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) mk_apps ctx.meta cons field_values) - | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" + | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unexpected bottom value" | VLoan lc -> ( match lc with | VSharedLoan (_, v) -> translate v @@ -2186,7 +2188,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | PeIdent (s, _) -> s | PeImpl _ -> (* We shouldn't get there *) - craise __FILE__ __LINE__ decl.meta "Unexpected") + craise __FILE__ __LINE__ decl.item_meta.meta "Unexpected") in name ^ "_back" in @@ -3839,7 +3841,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* Add a match over the fuel, if necessary *) let body = if function_decreases_fuel effect_info then - wrap_in_match_fuel def.meta ctx.fuel0 ctx.fuel body + wrap_in_match_fuel def.item_meta.meta ctx.fuel0 ctx.fuel body else body in (* Sanity check *) @@ -3884,7 +3886,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (List.for_all (fun (var, ty) -> (var : var).ty = ty) (List.combine inputs signature.inputs)) - def.meta; + def.item_meta.meta; Some { inputs; inputs_lvs; body } in @@ -3900,7 +3902,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = { def_id; is_local = def.is_local; - meta = def.meta; + meta = def.item_meta.meta; kind = def.kind; num_loops; loop_id; @@ -3938,7 +3940,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) def_id; is_local; name = llbc_name; - meta; + item_meta; generics = llbc_generics; preds; parent_clauses = llbc_parent_clauses; @@ -3955,23 +3957,31 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params trait_decl.meta llbc_generics in - let preds = translate_predicates trait_decl.meta preds in + let generics = + translate_generic_params trait_decl.item_meta.meta llbc_generics + in + let preds = translate_predicates trait_decl.item_meta.meta preds in let parent_clauses = - List.map (translate_trait_clause trait_decl.meta) llbc_parent_clauses + List.map + (translate_trait_clause trait_decl.item_meta.meta) + llbc_parent_clauses in let consts = List.map (fun (name, (ty, id)) -> - (name, (translate_fwd_ty trait_decl.meta type_infos ty, id))) + (name, (translate_fwd_ty trait_decl.item_meta.meta type_infos ty, id))) consts in let types = List.map (fun (name, (trait_clauses, ty)) -> ( name, - ( List.map (translate_trait_clause trait_decl.meta) trait_clauses, - Option.map (translate_fwd_ty trait_decl.meta type_infos) ty ) )) + ( List.map + (translate_trait_clause trait_decl.item_meta.meta) + trait_clauses, + Option.map + (translate_fwd_ty trait_decl.item_meta.meta type_infos) + ty ) )) types in { @@ -3979,7 +3989,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) is_local; llbc_name; name; - meta; + meta = item_meta.meta; generics; llbc_generics; preds; @@ -3997,7 +4007,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) A.def_id; is_local; name = llbc_name; - meta; + item_meta; impl_trait = llbc_impl_trait; generics = llbc_generics; preds; @@ -4011,8 +4021,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) in let type_infos = ctx.type_ctx.type_infos in let impl_trait = - translate_trait_decl_ref trait_impl.meta - (translate_fwd_ty trait_impl.meta type_infos) + translate_trait_decl_ref trait_impl.item_meta.meta + (translate_fwd_ty trait_impl.item_meta.meta type_infos) llbc_impl_trait in let name = @@ -4020,15 +4030,17 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params trait_impl.meta llbc_generics in - let preds = translate_predicates trait_impl.meta preds in + let generics = + translate_generic_params trait_impl.item_meta.meta llbc_generics + in + let preds = translate_predicates trait_impl.item_meta.meta preds in let parent_trait_refs = - List.map (translate_strait_ref trait_impl.meta) parent_trait_refs + List.map (translate_strait_ref trait_impl.item_meta.meta) parent_trait_refs in let consts = List.map (fun (name, (ty, id)) -> - (name, (translate_fwd_ty trait_impl.meta type_infos ty, id))) + (name, (translate_fwd_ty trait_impl.item_meta.meta type_infos ty, id))) consts in let types = @@ -4036,9 +4048,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) (fun (name, (trait_refs, ty)) -> ( name, ( List.map - (translate_fwd_trait_ref trait_impl.meta type_infos) + (translate_fwd_trait_ref trait_impl.item_meta.meta type_infos) trait_refs, - translate_fwd_ty trait_impl.meta type_infos ty ) )) + translate_fwd_ty trait_impl.item_meta.meta type_infos ty ) )) types in { @@ -4046,7 +4058,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) is_local; llbc_name; name; - meta; + meta = item_meta.meta; impl_trait; llbc_impl_trait; generics; @@ -4062,7 +4074,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : global_decl = let { - A.meta; + A.item_meta; def_id; is_local; name = llbc_name; @@ -4079,11 +4091,11 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params decl.meta llbc_generics in - let preds = translate_predicates decl.meta preds in - let ty = translate_fwd_ty decl.meta ctx.type_ctx.type_infos ty in + let generics = translate_generic_params decl.item_meta.meta llbc_generics in + let preds = translate_predicates decl.item_meta.meta preds in + let ty = translate_fwd_ty decl.item_meta.meta ctx.type_ctx.type_infos ty in { - meta; + meta = item_meta.meta; def_id; is_local; llbc_name; diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 9460c5f4..222b3c57 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -127,7 +127,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) let ctx = { - meta = fdef.meta; + meta = fdef.item_meta.meta; decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; @@ -179,7 +179,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } - | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable" in (* Add the backward inputs *) @@ -486,7 +486,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = GlobalDeclId.Map.find id global_decls in let trans = FunDeclId.Map.find global.body ctx.trans_funs in - sanity_check __FILE__ __LINE__ (trans.loops = []) global.meta; + sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.meta; let body = trans.f in let is_opaque = Option.is_none body.Pure.body in diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index e6621c7a..987df6ca 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -289,7 +289,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos) (List.map (fun v -> List.map (fun f -> f.field_ty) v.fields) variants) - | Opaque -> craise __FILE__ __LINE__ def.meta "unreachable" + | Opaque -> craise __FILE__ __LINE__ def.item_meta.meta "unreachable" in (* Explore the types and accumulate information *) let type_decl_info = TypeDeclId.Map.find def.def_id infos in diff --git a/default.nix b/default.nix new file mode 100644 index 00000000..d7da8cd1 --- /dev/null +++ b/default.nix @@ -0,0 +1,16 @@ +# This file provides backward compatibility to nix < 2.4 clients +{ system ? builtins.currentSystem }: +let + lock = builtins.fromJSON (builtins.readFile ./flake.lock); + + inherit (lock.nodes.flake-compat.locked) owner repo rev narHash; + + flake-compat = fetchTarball { + url = "https://github.com/${owner}/${repo}/archive/${rev}.tar.gz"; + sha256 = narHash; + }; + + flake = import flake-compat { inherit system; src = ./.; }; +in +flake.defaultNix + @@ -3,16 +3,17 @@ "charon": { "inputs": { "crane": "crane", + "flake-compat": "flake-compat", "flake-utils": "flake-utils", "nixpkgs": "nixpkgs", "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1712825631, - "narHash": "sha256-YC0QArtso4Z9iBgd63FXHsSopMtWof0kC7ZrYpE6yzg=", + "lastModified": 1713433954, + "narHash": "sha256-R3Pb/Z+V5s5neAwlTIhVJ/q3hDC65nLZ8d1ICotSdkM=", "owner": "aeneasverif", "repo": "charon", - "rev": "657de2521c285401d706ec69d588bb5778b18109", + "rev": "80ceb481c90f3cda435d5a60944ea7516415b294", "type": "github" }, "original": { @@ -42,6 +43,36 @@ "type": "github" } }, + "flake-compat": { + "locked": { + "lastModified": 1688025799, + "narHash": "sha256-ktpB4dRtnksm9F5WawoIkEneh1nrEvuxb5lJFt1iOyw=", + "owner": "nix-community", + "repo": "flake-compat", + "rev": "8bf105319d44f6b9f0d764efa4fdef9f1cc9ba1c", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-compat_2": { + "locked": { + "lastModified": 1688025799, + "narHash": "sha256-ktpB4dRtnksm9F5WawoIkEneh1nrEvuxb5lJFt1iOyw=", + "owner": "nix-community", + "repo": "flake-compat", + "rev": "8bf105319d44f6b9f0d764efa4fdef9f1cc9ba1c", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "flake-compat", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" @@ -221,6 +252,7 @@ "root": { "inputs": { "charon": "charon", + "flake-compat": "flake-compat_2", "flake-utils": [ "charon", "flake-utils" @@ -8,11 +8,12 @@ flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; hacl-nix.url = "github:hacl-star/hacl-nix"; + flake-compat.url = "github:nix-community/flake-compat"; }; # Remark: keep the list of outputs in sync with the list of inputs above # (see above remark) - outputs = { self, charon, flake-utils, nixpkgs, hacl-nix }: + outputs = { self, charon, flake-utils, nixpkgs, hacl-nix, flake-compat }: flake-utils.lib.eachSystem [ "x86_64-linux" ] (system: let pkgs = import nixpkgs { inherit system; }; @@ -29,11 +30,29 @@ }; buildInputs = [ ocamlPackages.calendar ]; }; + + aeneas-check-tidiness = pkgs.stdenv.mkDerivation { + name = "aeneas-check-tidiness"; + src = ./compiler; + buildInputs = [ + ocamlPackages.dune_3 + ocamlPackages.ocaml + ocamlPackages.ocamlformat + ]; + buildPhase = '' + if ! dune build @fmt; then + echo 'ERROR: Code is not formatted. Run `make format` to format the project files'. + exit 1 + fi + ''; + installPhase = "touch $out"; + }; aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; duneVersion = "3"; src = ./compiler; + OCAMLPARAM="_,warn-error=+A"; # Turn all warnings into errors. propagatedBuildInputs = [ easy_logging charon.packages.${system}.charon-ml ] ++ (with ocamlPackages; [ @@ -74,22 +93,20 @@ export AENEAS_EXE=./aeneas # Copy the tests - mkdir tests-copy cp -r tests tests-copy - # TODO: remove the test files to make sure we regenerate exactly - # the files which are checked out (we have to be careful about - # files like lakefile.lean, and the user hand-written files) - - # Run the tests - remark: we could remove the file - make test-all -j $NIX_BUILD_CORES + # Run the tests with extra sanity checks enabled + # Remark: we could remove the file + make clean-generated + OPTIONS=-checks make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests # and the original tests - if [[ $(diff -rq tests tests-copy) ]]; then + if diff -rq tests tests-copy; then echo "Ok: the regenerated test files are the same as the checked out files" else echo "Error: the regenerated test files differ from the checked out files" + diff -ru tests tests-copy exit 1 fi ''; @@ -153,10 +170,6 @@ default = aeneas; }; devShells.default = pkgs.mkShell { - # By default, tests run some sanity checks which are pretty slow. - # This disables these checks when developping locally. - OPTIONS = ""; - packages = [ pkgs.ocamlPackages.ocaml pkgs.ocamlPackages.ocamlformat @@ -172,6 +185,7 @@ inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq - aeneas-verify-hol4; }; + aeneas-verify-hol4 + aeneas-check-tidiness; }; }); } diff --git a/shell.nix b/shell.nix new file mode 100644 index 00000000..4e0d706e --- /dev/null +++ b/shell.nix @@ -0,0 +1,16 @@ +# This file provides backward compatibility to nix < 2.4 clients +{ system ? builtins.currentSystem }: +let + lock = builtins.fromJSON (builtins.readFile ./flake.lock); + + inherit (lock.nodes.flake-compat.locked) owner repo rev narHash; + + flake-compat = fetchTarball { + url = "https://github.com/${owner}/${repo}/archive/${rev}.tar.gz"; + sha256 = narHash; + }; + + flake = import flake-compat { inherit system; src = ./.; }; +in +flake.shellNix + diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/BetreeMain_FunsExternal.v index 07dba263..2d77c4ed 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal.v +++ b/tests/coq/betree/BetreeMain_FunsExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [betree_main]: external functions. -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/BetreeMain_TypesExternal.v index 50c4a4f8..870d2601 100644 --- a/tests/coq/betree/BetreeMain_TypesExternal.v +++ b/tests/coq/betree/BetreeMain_TypesExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [betree_main]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v index a03dc407..fb5f23cd 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [hashmap_main]: external function declarations *) Require Import Primitives. Import Primitives. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v index 87568232..28651c14 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [hashmap_main]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v index 130b48a2..39f4a60e 100644 --- a/tests/coq/misc/External_FunsExternal.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [external]: external function declarations *) Require Import Primitives. Import Primitives. diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v index 3f02b839..734c66e5 100644 --- a/tests/coq/misc/External_TypesExternal.v +++ b/tests/coq/misc/External_TypesExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [external]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index ecdfb281..b19ea2df 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -54,126 +54,23 @@ Inductive Sum_t (T1 T2 : Type) := Arguments Sum_Left { _ _ }. Arguments Sum_Right { _ _ }. -(** [no_nested_borrows::neg_test]: - Source: 'src/no_nested_borrows.rs', lines 48:0-48:30 *) -Definition neg_test (x : i32) : result i32 := - i32_neg x. - -(** [no_nested_borrows::add_u32]: - Source: 'src/no_nested_borrows.rs', lines 54:0-54:37 *) -Definition add_u32 (x : u32) (y : u32) : result u32 := - u32_add x y. - -(** [no_nested_borrows::subs_u32]: - Source: 'src/no_nested_borrows.rs', lines 60:0-60:38 *) -Definition subs_u32 (x : u32) (y : u32) : result u32 := - u32_sub x y. - -(** [no_nested_borrows::div_u32]: - Source: 'src/no_nested_borrows.rs', lines 66:0-66:37 *) -Definition div_u32 (x : u32) (y : u32) : result u32 := - u32_div x y. - -(** [no_nested_borrows::div_u32_const]: - Source: 'src/no_nested_borrows.rs', lines 73:0-73:35 *) -Definition div_u32_const (x : u32) : result u32 := - u32_div x 2%u32. - -(** [no_nested_borrows::rem_u32]: - Source: 'src/no_nested_borrows.rs', lines 78:0-78:37 *) -Definition rem_u32 (x : u32) (y : u32) : result u32 := - u32_rem x y. - -(** [no_nested_borrows::mul_u32]: - Source: 'src/no_nested_borrows.rs', lines 82:0-82:37 *) -Definition mul_u32 (x : u32) (y : u32) : result u32 := - u32_mul x y. - -(** [no_nested_borrows::add_i32]: - Source: 'src/no_nested_borrows.rs', lines 88:0-88:37 *) -Definition add_i32 (x : i32) (y : i32) : result i32 := - i32_add x y. - -(** [no_nested_borrows::subs_i32]: - Source: 'src/no_nested_borrows.rs', lines 92:0-92:38 *) -Definition subs_i32 (x : i32) (y : i32) : result i32 := - i32_sub x y. - -(** [no_nested_borrows::div_i32]: - Source: 'src/no_nested_borrows.rs', lines 96:0-96:37 *) -Definition div_i32 (x : i32) (y : i32) : result i32 := - i32_div x y. - -(** [no_nested_borrows::div_i32_const]: - Source: 'src/no_nested_borrows.rs', lines 100:0-100:35 *) -Definition div_i32_const (x : i32) : result i32 := - i32_div x 2%i32. - -(** [no_nested_borrows::rem_i32]: - Source: 'src/no_nested_borrows.rs', lines 104:0-104:37 *) -Definition rem_i32 (x : i32) (y : i32) : result i32 := - i32_rem x y. - -(** [no_nested_borrows::mul_i32]: - Source: 'src/no_nested_borrows.rs', lines 108:0-108:37 *) -Definition mul_i32 (x : i32) (y : i32) : result i32 := - i32_mul x y. - -(** [no_nested_borrows::mix_arith_u32]: - Source: 'src/no_nested_borrows.rs', lines 112:0-112:51 *) -Definition mix_arith_u32 (x : u32) (y : u32) (z : u32) : result u32 := - i <- u32_add x y; - i1 <- u32_div x y; - i2 <- u32_mul i i1; - i3 <- u32_rem z y; - i4 <- u32_sub x i3; - i5 <- u32_add i2 i4; - i6 <- u32_add x y; - i7 <- u32_add i6 z; - u32_rem i5 i7 -. - -(** [no_nested_borrows::mix_arith_i32]: - Source: 'src/no_nested_borrows.rs', lines 116:0-116:51 *) -Definition mix_arith_i32 (x : i32) (y : i32) (z : i32) : result i32 := - i <- i32_add x y; - i1 <- i32_div x y; - i2 <- i32_mul i i1; - i3 <- i32_rem z y; - i4 <- i32_sub x i3; - i5 <- i32_add i2 i4; - i6 <- i32_add x y; - i7 <- i32_add i6 z; - i32_rem i5 i7 -. - -(** [no_nested_borrows::CONST0] - Source: 'src/no_nested_borrows.rs', lines 125:0-125:23 *) -Definition const0_body : result usize := usize_add 1%usize 1%usize. -Definition const0 : usize := const0_body%global. - -(** [no_nested_borrows::CONST1] - Source: 'src/no_nested_borrows.rs', lines 126:0-126:23 *) -Definition const1_body : result usize := usize_mul 2%usize 2%usize. -Definition const1 : usize := const1_body%global. - (** [no_nested_borrows::cast_u32_to_i32]: - Source: 'src/no_nested_borrows.rs', lines 128:0-128:37 *) + Source: 'src/no_nested_borrows.rs', lines 46:0-46:37 *) Definition cast_u32_to_i32 (x : u32) : result i32 := scalar_cast U32 I32 x. (** [no_nested_borrows::cast_bool_to_i32]: - Source: 'src/no_nested_borrows.rs', lines 132:0-132:39 *) + Source: 'src/no_nested_borrows.rs', lines 50:0-50:39 *) Definition cast_bool_to_i32 (x : bool) : result i32 := scalar_cast_bool I32 x. (** [no_nested_borrows::cast_bool_to_bool]: - Source: 'src/no_nested_borrows.rs', lines 137:0-137:41 *) + Source: 'src/no_nested_borrows.rs', lines 55:0-55:41 *) Definition cast_bool_to_bool (x : bool) : result bool := Ok x. (** [no_nested_borrows::test2]: - Source: 'src/no_nested_borrows.rs', lines 142:0-142:14 *) + Source: 'src/no_nested_borrows.rs', lines 60:0-60:14 *) Definition test2 : result unit := _ <- u32_add 23%u32 44%u32; Ok tt. @@ -181,13 +78,13 @@ Definition test2 : result unit := Check (test2 )%return. (** [no_nested_borrows::get_max]: - Source: 'src/no_nested_borrows.rs', lines 154:0-154:37 *) + Source: 'src/no_nested_borrows.rs', lines 72:0-72:37 *) Definition get_max (x : u32) (y : u32) : result u32 := if x s>= y then Ok x else Ok y . (** [no_nested_borrows::test3]: - Source: 'src/no_nested_borrows.rs', lines 162:0-162:14 *) + Source: 'src/no_nested_borrows.rs', lines 80:0-80:14 *) Definition test3 : result unit := x <- get_max 4%u32 3%u32; y <- get_max 10%u32 11%u32; @@ -199,7 +96,7 @@ Definition test3 : result unit := Check (test3 )%return. (** [no_nested_borrows::test_neg1]: - Source: 'src/no_nested_borrows.rs', lines 169:0-169:18 *) + Source: 'src/no_nested_borrows.rs', lines 87:0-87:18 *) Definition test_neg1 : result unit := y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Ok tt . @@ -208,7 +105,7 @@ Definition test_neg1 : result unit := Check (test_neg1 )%return. (** [no_nested_borrows::refs_test1]: - Source: 'src/no_nested_borrows.rs', lines 176:0-176:19 *) + Source: 'src/no_nested_borrows.rs', lines 94:0-94:19 *) Definition refs_test1 : result unit := if negb (1%i32 s= 1%i32) then Fail_ Failure else Ok tt . @@ -217,7 +114,7 @@ Definition refs_test1 : result unit := Check (refs_test1 )%return. (** [no_nested_borrows::refs_test2]: - Source: 'src/no_nested_borrows.rs', lines 187:0-187:19 *) + Source: 'src/no_nested_borrows.rs', lines 105:0-105:19 *) Definition refs_test2 : result unit := if negb (2%i32 s= 2%i32) then Fail_ Failure @@ -234,7 +131,7 @@ Definition refs_test2 : result unit := Check (refs_test2 )%return. (** [no_nested_borrows::test_list1]: - Source: 'src/no_nested_borrows.rs', lines 203:0-203:19 *) + Source: 'src/no_nested_borrows.rs', lines 121:0-121:19 *) Definition test_list1 : result unit := Ok tt. @@ -242,7 +139,7 @@ Definition test_list1 : result unit := Check (test_list1 )%return. (** [no_nested_borrows::test_box1]: - Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 *) + Source: 'src/no_nested_borrows.rs', lines 126:0-126:18 *) Definition test_box1 : result unit := p <- alloc_boxed_Box_deref_mut i32 0%i32; let (_, deref_mut_back) := p in @@ -255,24 +152,24 @@ Definition test_box1 : result unit := Check (test_box1 )%return. (** [no_nested_borrows::copy_int]: - Source: 'src/no_nested_borrows.rs', lines 218:0-218:30 *) + Source: 'src/no_nested_borrows.rs', lines 136:0-136:30 *) Definition copy_int (x : i32) : result i32 := Ok x. (** [no_nested_borrows::test_unreachable]: - Source: 'src/no_nested_borrows.rs', lines 224:0-224:32 *) + Source: 'src/no_nested_borrows.rs', lines 142:0-142:32 *) Definition test_unreachable (b : bool) : result unit := if b then Fail_ Failure else Ok tt . (** [no_nested_borrows::test_panic]: - Source: 'src/no_nested_borrows.rs', lines 232:0-232:26 *) + Source: 'src/no_nested_borrows.rs', lines 150:0-150:26 *) Definition test_panic (b : bool) : result unit := if b then Fail_ Failure else Ok tt . (** [no_nested_borrows::test_copy_int]: - Source: 'src/no_nested_borrows.rs', lines 239:0-239:22 *) + Source: 'src/no_nested_borrows.rs', lines 157:0-157:22 *) Definition test_copy_int : result unit := y <- copy_int 0%i32; if negb (0%i32 s= y) then Fail_ Failure else Ok tt . @@ -281,13 +178,13 @@ Definition test_copy_int : result unit := Check (test_copy_int )%return. (** [no_nested_borrows::is_cons]: - Source: 'src/no_nested_borrows.rs', lines 246:0-246:38 *) + Source: 'src/no_nested_borrows.rs', lines 164:0-164:38 *) Definition is_cons (T : Type) (l : List_t T) : result bool := match l with | List_Cons _ _ => Ok true | List_Nil => Ok false end . (** [no_nested_borrows::test_is_cons]: - Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *) + Source: 'src/no_nested_borrows.rs', lines 171:0-171:21 *) Definition test_is_cons : result unit := b <- is_cons i32 (List_Cons 0%i32 List_Nil); if negb b then Fail_ Failure else Ok tt @@ -297,13 +194,13 @@ Definition test_is_cons : result unit := Check (test_is_cons )%return. (** [no_nested_borrows::split_list]: - Source: 'src/no_nested_borrows.rs', lines 259:0-259:48 *) + Source: 'src/no_nested_borrows.rs', lines 177:0-177:48 *) Definition split_list (T : Type) (l : List_t T) : result (T * (List_t T)) := match l with | List_Cons hd tl => Ok (hd, tl) | List_Nil => Fail_ Failure end . (** [no_nested_borrows::test_split_list]: - Source: 'src/no_nested_borrows.rs', lines 267:0-267:24 *) + Source: 'src/no_nested_borrows.rs', lines 185:0-185:24 *) Definition test_split_list : result unit := p <- split_list i32 (List_Cons 0%i32 List_Nil); let (hd, _) := p in @@ -314,7 +211,7 @@ Definition test_split_list : result unit := Check (test_split_list )%return. (** [no_nested_borrows::choose]: - Source: 'src/no_nested_borrows.rs', lines 274:0-274:70 *) + Source: 'src/no_nested_borrows.rs', lines 192:0-192:70 *) Definition choose (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) := if b @@ -323,7 +220,7 @@ Definition choose . (** [no_nested_borrows::choose_test]: - Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 *) + Source: 'src/no_nested_borrows.rs', lines 200:0-200:20 *) Definition choose_test : result unit := p <- choose i32 true 0%i32 0%i32; let (z, choose_back) := p in @@ -342,18 +239,18 @@ Definition choose_test : result unit := Check (choose_test )%return. (** [no_nested_borrows::test_char]: - Source: 'src/no_nested_borrows.rs', lines 294:0-294:26 *) + Source: 'src/no_nested_borrows.rs', lines 212:0-212:26 *) Definition test_char : result char := Ok (char_of_byte Coq.Init.Byte.x61). (** [no_nested_borrows::Tree] - Source: 'src/no_nested_borrows.rs', lines 299:0-299:16 *) + Source: 'src/no_nested_borrows.rs', lines 217:0-217:16 *) Inductive Tree_t (T : Type) := | Tree_Leaf : T -> Tree_t T | Tree_Node : T -> NodeElem_t T -> Tree_t T -> Tree_t T (** [no_nested_borrows::NodeElem] - Source: 'src/no_nested_borrows.rs', lines 304:0-304:20 *) + Source: 'src/no_nested_borrows.rs', lines 222:0-222:20 *) with NodeElem_t (T : Type) := | NodeElem_Cons : Tree_t T -> NodeElem_t T -> NodeElem_t T | NodeElem_Nil : NodeElem_t T @@ -366,7 +263,7 @@ Arguments NodeElem_Cons { _ }. Arguments NodeElem_Nil { _ }. (** [no_nested_borrows::list_length]: - Source: 'src/no_nested_borrows.rs', lines 339:0-339:48 *) + Source: 'src/no_nested_borrows.rs', lines 257:0-257:48 *) Fixpoint list_length (T : Type) (l : List_t T) : result u32 := match l with | List_Cons _ l1 => i <- list_length T l1; u32_add 1%u32 i @@ -375,7 +272,7 @@ Fixpoint list_length (T : Type) (l : List_t T) : result u32 := . (** [no_nested_borrows::list_nth_shared]: - Source: 'src/no_nested_borrows.rs', lines 347:0-347:62 *) + Source: 'src/no_nested_borrows.rs', lines 265:0-265:62 *) Fixpoint list_nth_shared (T : Type) (l : List_t T) (i : u32) : result T := match l with | List_Cons x tl => @@ -387,7 +284,7 @@ Fixpoint list_nth_shared (T : Type) (l : List_t T) (i : u32) : result T := . (** [no_nested_borrows::list_nth_mut]: - Source: 'src/no_nested_borrows.rs', lines 363:0-363:67 *) + Source: 'src/no_nested_borrows.rs', lines 281:0-281:67 *) Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result (T * (T -> result (List_t T))) @@ -408,7 +305,7 @@ Fixpoint list_nth_mut . (** [no_nested_borrows::list_rev_aux]: - Source: 'src/no_nested_borrows.rs', lines 379:0-379:63 *) + Source: 'src/no_nested_borrows.rs', lines 297:0-297:63 *) Fixpoint list_rev_aux (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) := match li with @@ -418,14 +315,14 @@ Fixpoint list_rev_aux . (** [no_nested_borrows::list_rev]: - Source: 'src/no_nested_borrows.rs', lines 393:0-393:42 *) + Source: 'src/no_nested_borrows.rs', lines 311:0-311:42 *) Definition list_rev (T : Type) (l : List_t T) : result (List_t T) := let (li, _) := core_mem_replace (List_t T) l List_Nil in list_rev_aux T li List_Nil . (** [no_nested_borrows::test_list_functions]: - Source: 'src/no_nested_borrows.rs', lines 398:0-398:28 *) + Source: 'src/no_nested_borrows.rs', lines 316:0-316:28 *) Definition test_list_functions : result unit := let l := List_Cons 2%i32 List_Nil in let l1 := List_Cons 1%i32 l in @@ -464,7 +361,7 @@ Definition test_list_functions : result unit := Check (test_list_functions )%return. (** [no_nested_borrows::id_mut_pair1]: - Source: 'src/no_nested_borrows.rs', lines 414:0-414:89 *) + Source: 'src/no_nested_borrows.rs', lines 332:0-332:89 *) Definition id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) @@ -473,7 +370,7 @@ Definition id_mut_pair1 . (** [no_nested_borrows::id_mut_pair2]: - Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 *) + Source: 'src/no_nested_borrows.rs', lines 336:0-336:88 *) Definition id_mut_pair2 (T1 T2 : Type) (p : (T1 * T2)) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) @@ -482,7 +379,7 @@ Definition id_mut_pair2 . (** [no_nested_borrows::id_mut_pair3]: - Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 *) + Source: 'src/no_nested_borrows.rs', lines 340:0-340:93 *) Definition id_mut_pair3 (T1 T2 : Type) (x : T1) (y : T2) : result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2)) @@ -491,7 +388,7 @@ Definition id_mut_pair3 . (** [no_nested_borrows::id_mut_pair4]: - Source: 'src/no_nested_borrows.rs', lines 426:0-426:92 *) + Source: 'src/no_nested_borrows.rs', lines 344:0-344:92 *) Definition id_mut_pair4 (T1 T2 : Type) (p : (T1 * T2)) : result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2)) @@ -500,7 +397,7 @@ Definition id_mut_pair4 . (** [no_nested_borrows::StructWithTuple] - Source: 'src/no_nested_borrows.rs', lines 433:0-433:34 *) + Source: 'src/no_nested_borrows.rs', lines 351:0-351:34 *) Record StructWithTuple_t (T1 T2 : Type) := mkStructWithTuple_t { structWithTuple_p : (T1 * T2); @@ -511,25 +408,25 @@ Arguments mkStructWithTuple_t { _ _ }. Arguments structWithTuple_p { _ _ }. (** [no_nested_borrows::new_tuple1]: - Source: 'src/no_nested_borrows.rs', lines 437:0-437:48 *) + Source: 'src/no_nested_borrows.rs', lines 355:0-355:48 *) Definition new_tuple1 : result (StructWithTuple_t u32 u32) := Ok {| structWithTuple_p := (1%u32, 2%u32) |} . (** [no_nested_borrows::new_tuple2]: - Source: 'src/no_nested_borrows.rs', lines 441:0-441:48 *) + Source: 'src/no_nested_borrows.rs', lines 359:0-359:48 *) Definition new_tuple2 : result (StructWithTuple_t i16 i16) := Ok {| structWithTuple_p := (1%i16, 2%i16) |} . (** [no_nested_borrows::new_tuple3]: - Source: 'src/no_nested_borrows.rs', lines 445:0-445:48 *) + Source: 'src/no_nested_borrows.rs', lines 363:0-363:48 *) Definition new_tuple3 : result (StructWithTuple_t u64 i64) := Ok {| structWithTuple_p := (1%u64, 2%i64) |} . (** [no_nested_borrows::StructWithPair] - Source: 'src/no_nested_borrows.rs', lines 450:0-450:33 *) + Source: 'src/no_nested_borrows.rs', lines 368:0-368:33 *) Record StructWithPair_t (T1 T2 : Type) := mkStructWithPair_t { structWithPair_p : Pair_t T1 T2; @@ -540,13 +437,13 @@ Arguments mkStructWithPair_t { _ _ }. Arguments structWithPair_p { _ _ }. (** [no_nested_borrows::new_pair1]: - Source: 'src/no_nested_borrows.rs', lines 454:0-454:46 *) + Source: 'src/no_nested_borrows.rs', lines 372:0-372:46 *) Definition new_pair1 : result (StructWithPair_t u32 u32) := Ok {| structWithPair_p := {| pair_x := 1%u32; pair_y := 2%u32 |} |} . (** [no_nested_borrows::test_constants]: - Source: 'src/no_nested_borrows.rs', lines 462:0-462:23 *) + Source: 'src/no_nested_borrows.rs', lines 380:0-380:23 *) Definition test_constants : result unit := swt <- new_tuple1; let (i, _) := swt.(structWithTuple_p) in @@ -573,7 +470,7 @@ Definition test_constants : result unit := Check (test_constants )%return. (** [no_nested_borrows::test_weird_borrows1]: - Source: 'src/no_nested_borrows.rs', lines 471:0-471:28 *) + Source: 'src/no_nested_borrows.rs', lines 389:0-389:28 *) Definition test_weird_borrows1 : result unit := Ok tt. @@ -581,78 +478,78 @@ Definition test_weird_borrows1 : result unit := Check (test_weird_borrows1 )%return. (** [no_nested_borrows::test_mem_replace]: - Source: 'src/no_nested_borrows.rs', lines 481:0-481:37 *) + Source: 'src/no_nested_borrows.rs', lines 399:0-399:37 *) Definition test_mem_replace (px : u32) : result u32 := let (y, _) := core_mem_replace u32 px 1%u32 in if negb (y s= 0%u32) then Fail_ Failure else Ok 2%u32 . (** [no_nested_borrows::test_shared_borrow_bool1]: - Source: 'src/no_nested_borrows.rs', lines 488:0-488:47 *) + Source: 'src/no_nested_borrows.rs', lines 406:0-406:47 *) Definition test_shared_borrow_bool1 (b : bool) : result u32 := if b then Ok 0%u32 else Ok 1%u32 . (** [no_nested_borrows::test_shared_borrow_bool2]: - Source: 'src/no_nested_borrows.rs', lines 501:0-501:40 *) + Source: 'src/no_nested_borrows.rs', lines 419:0-419:40 *) Definition test_shared_borrow_bool2 : result u32 := Ok 0%u32. (** [no_nested_borrows::test_shared_borrow_enum1]: - Source: 'src/no_nested_borrows.rs', lines 516:0-516:52 *) + Source: 'src/no_nested_borrows.rs', lines 434:0-434:52 *) Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 := match l with | List_Cons _ _ => Ok 1%u32 | List_Nil => Ok 0%u32 end . (** [no_nested_borrows::test_shared_borrow_enum2]: - Source: 'src/no_nested_borrows.rs', lines 528:0-528:40 *) + Source: 'src/no_nested_borrows.rs', lines 446:0-446:40 *) Definition test_shared_borrow_enum2 : result u32 := Ok 0%u32. (** [no_nested_borrows::incr]: - Source: 'src/no_nested_borrows.rs', lines 539:0-539:24 *) + Source: 'src/no_nested_borrows.rs', lines 457:0-457:24 *) Definition incr (x : u32) : result u32 := u32_add x 1%u32. (** [no_nested_borrows::call_incr]: - Source: 'src/no_nested_borrows.rs', lines 543:0-543:35 *) + Source: 'src/no_nested_borrows.rs', lines 461:0-461:35 *) Definition call_incr (x : u32) : result u32 := incr x. (** [no_nested_borrows::read_then_incr]: - Source: 'src/no_nested_borrows.rs', lines 548:0-548:41 *) + Source: 'src/no_nested_borrows.rs', lines 466:0-466:41 *) Definition read_then_incr (x : u32) : result (u32 * u32) := x1 <- u32_add x 1%u32; Ok (x, x1) . (** [no_nested_borrows::Tuple] - Source: 'src/no_nested_borrows.rs', lines 554:0-554:24 *) + Source: 'src/no_nested_borrows.rs', lines 472:0-472:24 *) Definition Tuple_t (T1 T2 : Type) : Type := T1 * T2. (** [no_nested_borrows::use_tuple_struct]: - Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 *) + Source: 'src/no_nested_borrows.rs', lines 474:0-474:48 *) Definition use_tuple_struct (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) := let (_, i) := x in Ok (1%u32, i) . (** [no_nested_borrows::create_tuple_struct]: - Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 *) + Source: 'src/no_nested_borrows.rs', lines 478:0-478:61 *) Definition create_tuple_struct (x : u32) (y : u64) : result (Tuple_t u32 u64) := Ok (x, y) . (** [no_nested_borrows::IdType] - Source: 'src/no_nested_borrows.rs', lines 565:0-565:20 *) + Source: 'src/no_nested_borrows.rs', lines 483:0-483:20 *) Definition IdType_t (T : Type) : Type := T. (** [no_nested_borrows::use_id_type]: - Source: 'src/no_nested_borrows.rs', lines 567:0-567:40 *) + Source: 'src/no_nested_borrows.rs', lines 485:0-485:40 *) Definition use_id_type (T : Type) (x : IdType_t T) : result T := Ok x. (** [no_nested_borrows::create_id_type]: - Source: 'src/no_nested_borrows.rs', lines 571:0-571:43 *) + Source: 'src/no_nested_borrows.rs', lines 489:0-489:43 *) Definition create_id_type (T : Type) (x : T) : result (IdType_t T) := Ok x. diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index ac443a99..7d965944 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -37,124 +37,23 @@ type sum_t (t1 t2 : Type0) = | Sum_Left : t1 -> sum_t t1 t2 | Sum_Right : t2 -> sum_t t1 t2 -(** [no_nested_borrows::neg_test]: - Source: 'src/no_nested_borrows.rs', lines 48:0-48:30 *) -let neg_test (x : i32) : result i32 = - i32_neg x - -(** [no_nested_borrows::add_u32]: - Source: 'src/no_nested_borrows.rs', lines 54:0-54:37 *) -let add_u32 (x : u32) (y : u32) : result u32 = - u32_add x y - -(** [no_nested_borrows::subs_u32]: - Source: 'src/no_nested_borrows.rs', lines 60:0-60:38 *) -let subs_u32 (x : u32) (y : u32) : result u32 = - u32_sub x y - -(** [no_nested_borrows::div_u32]: - Source: 'src/no_nested_borrows.rs', lines 66:0-66:37 *) -let div_u32 (x : u32) (y : u32) : result u32 = - u32_div x y - -(** [no_nested_borrows::div_u32_const]: - Source: 'src/no_nested_borrows.rs', lines 73:0-73:35 *) -let div_u32_const (x : u32) : result u32 = - u32_div x 2 - -(** [no_nested_borrows::rem_u32]: - Source: 'src/no_nested_borrows.rs', lines 78:0-78:37 *) -let rem_u32 (x : u32) (y : u32) : result u32 = - u32_rem x y - -(** [no_nested_borrows::mul_u32]: - Source: 'src/no_nested_borrows.rs', lines 82:0-82:37 *) -let mul_u32 (x : u32) (y : u32) : result u32 = - u32_mul x y - -(** [no_nested_borrows::add_i32]: - Source: 'src/no_nested_borrows.rs', lines 88:0-88:37 *) -let add_i32 (x : i32) (y : i32) : result i32 = - i32_add x y - -(** [no_nested_borrows::subs_i32]: - Source: 'src/no_nested_borrows.rs', lines 92:0-92:38 *) -let subs_i32 (x : i32) (y : i32) : result i32 = - i32_sub x y - -(** [no_nested_borrows::div_i32]: - Source: 'src/no_nested_borrows.rs', lines 96:0-96:37 *) -let div_i32 (x : i32) (y : i32) : result i32 = - i32_div x y - -(** [no_nested_borrows::div_i32_const]: - Source: 'src/no_nested_borrows.rs', lines 100:0-100:35 *) -let div_i32_const (x : i32) : result i32 = - i32_div x 2 - -(** [no_nested_borrows::rem_i32]: - Source: 'src/no_nested_borrows.rs', lines 104:0-104:37 *) -let rem_i32 (x : i32) (y : i32) : result i32 = - i32_rem x y - -(** [no_nested_borrows::mul_i32]: - Source: 'src/no_nested_borrows.rs', lines 108:0-108:37 *) -let mul_i32 (x : i32) (y : i32) : result i32 = - i32_mul x y - -(** [no_nested_borrows::mix_arith_u32]: - Source: 'src/no_nested_borrows.rs', lines 112:0-112:51 *) -let mix_arith_u32 (x : u32) (y : u32) (z : u32) : result u32 = - let* i = u32_add x y in - let* i1 = u32_div x y in - let* i2 = u32_mul i i1 in - let* i3 = u32_rem z y in - let* i4 = u32_sub x i3 in - let* i5 = u32_add i2 i4 in - let* i6 = u32_add x y in - let* i7 = u32_add i6 z in - u32_rem i5 i7 - -(** [no_nested_borrows::mix_arith_i32]: - Source: 'src/no_nested_borrows.rs', lines 116:0-116:51 *) -let mix_arith_i32 (x : i32) (y : i32) (z : i32) : result i32 = - let* i = i32_add x y in - let* i1 = i32_div x y in - let* i2 = i32_mul i i1 in - let* i3 = i32_rem z y in - let* i4 = i32_sub x i3 in - let* i5 = i32_add i2 i4 in - let* i6 = i32_add x y in - let* i7 = i32_add i6 z in - i32_rem i5 i7 - -(** [no_nested_borrows::CONST0] - Source: 'src/no_nested_borrows.rs', lines 125:0-125:23 *) -let const0_body : result usize = usize_add 1 1 -let const0 : usize = eval_global const0_body - -(** [no_nested_borrows::CONST1] - Source: 'src/no_nested_borrows.rs', lines 126:0-126:23 *) -let const1_body : result usize = usize_mul 2 2 -let const1 : usize = eval_global const1_body - (** [no_nested_borrows::cast_u32_to_i32]: - Source: 'src/no_nested_borrows.rs', lines 128:0-128:37 *) + Source: 'src/no_nested_borrows.rs', lines 46:0-46:37 *) let cast_u32_to_i32 (x : u32) : result i32 = scalar_cast U32 I32 x (** [no_nested_borrows::cast_bool_to_i32]: - Source: 'src/no_nested_borrows.rs', lines 132:0-132:39 *) + Source: 'src/no_nested_borrows.rs', lines 50:0-50:39 *) let cast_bool_to_i32 (x : bool) : result i32 = scalar_cast_bool I32 x (** [no_nested_borrows::cast_bool_to_bool]: - Source: 'src/no_nested_borrows.rs', lines 137:0-137:41 *) + Source: 'src/no_nested_borrows.rs', lines 55:0-55:41 *) let cast_bool_to_bool (x : bool) : result bool = Ok x (** [no_nested_borrows::test2]: - Source: 'src/no_nested_borrows.rs', lines 142:0-142:14 *) + Source: 'src/no_nested_borrows.rs', lines 60:0-60:14 *) let test2 : result unit = let* _ = u32_add 23 44 in Ok () @@ -162,12 +61,12 @@ let test2 : result unit = let _ = assert_norm (test2 = Ok ()) (** [no_nested_borrows::get_max]: - Source: 'src/no_nested_borrows.rs', lines 154:0-154:37 *) + Source: 'src/no_nested_borrows.rs', lines 72:0-72:37 *) let get_max (x : u32) (y : u32) : result u32 = if x >= y then Ok x else Ok y (** [no_nested_borrows::test3]: - Source: 'src/no_nested_borrows.rs', lines 162:0-162:14 *) + Source: 'src/no_nested_borrows.rs', lines 80:0-80:14 *) let test3 : result unit = let* x = get_max 4 3 in let* y = get_max 10 11 in @@ -178,7 +77,7 @@ let test3 : result unit = let _ = assert_norm (test3 = Ok ()) (** [no_nested_borrows::test_neg1]: - Source: 'src/no_nested_borrows.rs', lines 169:0-169:18 *) + Source: 'src/no_nested_borrows.rs', lines 87:0-87:18 *) let test_neg1 : result unit = let* y = i32_neg 3 in if not (y = -3) then Fail Failure else Ok () @@ -186,7 +85,7 @@ let test_neg1 : result unit = let _ = assert_norm (test_neg1 = Ok ()) (** [no_nested_borrows::refs_test1]: - Source: 'src/no_nested_borrows.rs', lines 176:0-176:19 *) + Source: 'src/no_nested_borrows.rs', lines 94:0-94:19 *) let refs_test1 : result unit = if not (1 = 1) then Fail Failure else Ok () @@ -194,7 +93,7 @@ let refs_test1 : result unit = let _ = assert_norm (refs_test1 = Ok ()) (** [no_nested_borrows::refs_test2]: - Source: 'src/no_nested_borrows.rs', lines 187:0-187:19 *) + Source: 'src/no_nested_borrows.rs', lines 105:0-105:19 *) let refs_test2 : result unit = if not (2 = 2) then Fail Failure @@ -210,7 +109,7 @@ let refs_test2 : result unit = let _ = assert_norm (refs_test2 = Ok ()) (** [no_nested_borrows::test_list1]: - Source: 'src/no_nested_borrows.rs', lines 203:0-203:19 *) + Source: 'src/no_nested_borrows.rs', lines 121:0-121:19 *) let test_list1 : result unit = Ok () @@ -218,7 +117,7 @@ let test_list1 : result unit = let _ = assert_norm (test_list1 = Ok ()) (** [no_nested_borrows::test_box1]: - Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 *) + Source: 'src/no_nested_borrows.rs', lines 126:0-126:18 *) let test_box1 : result unit = let* (_, deref_mut_back) = alloc_boxed_Box_deref_mut i32 0 in let* b = deref_mut_back 1 in @@ -229,22 +128,22 @@ let test_box1 : result unit = let _ = assert_norm (test_box1 = Ok ()) (** [no_nested_borrows::copy_int]: - Source: 'src/no_nested_borrows.rs', lines 218:0-218:30 *) + Source: 'src/no_nested_borrows.rs', lines 136:0-136:30 *) let copy_int (x : i32) : result i32 = Ok x (** [no_nested_borrows::test_unreachable]: - Source: 'src/no_nested_borrows.rs', lines 224:0-224:32 *) + Source: 'src/no_nested_borrows.rs', lines 142:0-142:32 *) let test_unreachable (b : bool) : result unit = if b then Fail Failure else Ok () (** [no_nested_borrows::test_panic]: - Source: 'src/no_nested_borrows.rs', lines 232:0-232:26 *) + Source: 'src/no_nested_borrows.rs', lines 150:0-150:26 *) let test_panic (b : bool) : result unit = if b then Fail Failure else Ok () (** [no_nested_borrows::test_copy_int]: - Source: 'src/no_nested_borrows.rs', lines 239:0-239:22 *) + Source: 'src/no_nested_borrows.rs', lines 157:0-157:22 *) let test_copy_int : result unit = let* y = copy_int 0 in if not (0 = y) then Fail Failure else Ok () @@ -252,12 +151,12 @@ let test_copy_int : result unit = let _ = assert_norm (test_copy_int = Ok ()) (** [no_nested_borrows::is_cons]: - Source: 'src/no_nested_borrows.rs', lines 246:0-246:38 *) + Source: 'src/no_nested_borrows.rs', lines 164:0-164:38 *) let is_cons (t : Type0) (l : list_t t) : result bool = begin match l with | List_Cons _ _ -> Ok true | List_Nil -> Ok false end (** [no_nested_borrows::test_is_cons]: - Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *) + Source: 'src/no_nested_borrows.rs', lines 171:0-171:21 *) let test_is_cons : result unit = let* b = is_cons i32 (List_Cons 0 List_Nil) in if not b then Fail Failure else Ok () @@ -266,7 +165,7 @@ let test_is_cons : result unit = let _ = assert_norm (test_is_cons = Ok ()) (** [no_nested_borrows::split_list]: - Source: 'src/no_nested_borrows.rs', lines 259:0-259:48 *) + Source: 'src/no_nested_borrows.rs', lines 177:0-177:48 *) let split_list (t : Type0) (l : list_t t) : result (t & (list_t t)) = begin match l with | List_Cons hd tl -> Ok (hd, tl) @@ -274,7 +173,7 @@ let split_list (t : Type0) (l : list_t t) : result (t & (list_t t)) = end (** [no_nested_borrows::test_split_list]: - Source: 'src/no_nested_borrows.rs', lines 267:0-267:24 *) + Source: 'src/no_nested_borrows.rs', lines 185:0-185:24 *) let test_split_list : result unit = let* p = split_list i32 (List_Cons 0 List_Nil) in let (hd, _) = p in @@ -284,7 +183,7 @@ let test_split_list : result unit = let _ = assert_norm (test_split_list = Ok ()) (** [no_nested_borrows::choose]: - Source: 'src/no_nested_borrows.rs', lines 274:0-274:70 *) + Source: 'src/no_nested_borrows.rs', lines 192:0-192:70 *) let choose (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) = if b @@ -292,7 +191,7 @@ let choose else let back = fun ret -> Ok (x, ret) in Ok (y, back) (** [no_nested_borrows::choose_test]: - Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 *) + Source: 'src/no_nested_borrows.rs', lines 200:0-200:20 *) let choose_test : result unit = let* (z, choose_back) = choose i32 true 0 0 in let* z1 = i32_add z 1 in @@ -308,24 +207,24 @@ let choose_test : result unit = let _ = assert_norm (choose_test = Ok ()) (** [no_nested_borrows::test_char]: - Source: 'src/no_nested_borrows.rs', lines 294:0-294:26 *) + Source: 'src/no_nested_borrows.rs', lines 212:0-212:26 *) let test_char : result char = Ok 'a' (** [no_nested_borrows::Tree] - Source: 'src/no_nested_borrows.rs', lines 299:0-299:16 *) + Source: 'src/no_nested_borrows.rs', lines 217:0-217:16 *) type tree_t (t : Type0) = | Tree_Leaf : t -> tree_t t | Tree_Node : t -> nodeElem_t t -> tree_t t -> tree_t t (** [no_nested_borrows::NodeElem] - Source: 'src/no_nested_borrows.rs', lines 304:0-304:20 *) + Source: 'src/no_nested_borrows.rs', lines 222:0-222:20 *) and nodeElem_t (t : Type0) = | NodeElem_Cons : tree_t t -> nodeElem_t t -> nodeElem_t t | NodeElem_Nil : nodeElem_t t (** [no_nested_borrows::list_length]: - Source: 'src/no_nested_borrows.rs', lines 339:0-339:48 *) + Source: 'src/no_nested_borrows.rs', lines 257:0-257:48 *) let rec list_length (t : Type0) (l : list_t t) : result u32 = begin match l with | List_Cons _ l1 -> let* i = list_length t l1 in u32_add 1 i @@ -333,7 +232,7 @@ let rec list_length (t : Type0) (l : list_t t) : result u32 = end (** [no_nested_borrows::list_nth_shared]: - Source: 'src/no_nested_borrows.rs', lines 347:0-347:62 *) + Source: 'src/no_nested_borrows.rs', lines 265:0-265:62 *) let rec list_nth_shared (t : Type0) (l : list_t t) (i : u32) : result t = begin match l with | List_Cons x tl -> @@ -342,7 +241,7 @@ let rec list_nth_shared (t : Type0) (l : list_t t) (i : u32) : result t = end (** [no_nested_borrows::list_nth_mut]: - Source: 'src/no_nested_borrows.rs', lines 363:0-363:67 *) + Source: 'src/no_nested_borrows.rs', lines 281:0-281:67 *) let rec list_nth_mut (t : Type0) (l : list_t t) (i : u32) : result (t & (t -> result (list_t t))) @@ -361,7 +260,7 @@ let rec list_nth_mut end (** [no_nested_borrows::list_rev_aux]: - Source: 'src/no_nested_borrows.rs', lines 379:0-379:63 *) + Source: 'src/no_nested_borrows.rs', lines 297:0-297:63 *) let rec list_rev_aux (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) = begin match li with @@ -370,13 +269,13 @@ let rec list_rev_aux end (** [no_nested_borrows::list_rev]: - Source: 'src/no_nested_borrows.rs', lines 393:0-393:42 *) + Source: 'src/no_nested_borrows.rs', lines 311:0-311:42 *) let list_rev (t : Type0) (l : list_t t) : result (list_t t) = let (li, _) = core_mem_replace (list_t t) l List_Nil in list_rev_aux t li List_Nil (** [no_nested_borrows::test_list_functions]: - Source: 'src/no_nested_borrows.rs', lines 398:0-398:28 *) + Source: 'src/no_nested_borrows.rs', lines 316:0-316:28 *) let test_list_functions : result unit = let l = List_Cons 2 List_Nil in let l1 = List_Cons 1 l in @@ -413,7 +312,7 @@ let test_list_functions : result unit = let _ = assert_norm (test_list_functions = Ok ()) (** [no_nested_borrows::id_mut_pair1]: - Source: 'src/no_nested_borrows.rs', lines 414:0-414:89 *) + Source: 'src/no_nested_borrows.rs', lines 332:0-332:89 *) let id_mut_pair1 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) @@ -421,7 +320,7 @@ let id_mut_pair1 Ok ((x, y), Ok) (** [no_nested_borrows::id_mut_pair2]: - Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 *) + Source: 'src/no_nested_borrows.rs', lines 336:0-336:88 *) let id_mut_pair2 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) @@ -429,7 +328,7 @@ let id_mut_pair2 let (x, x1) = p in Ok ((x, x1), Ok) (** [no_nested_borrows::id_mut_pair3]: - Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 *) + Source: 'src/no_nested_borrows.rs', lines 340:0-340:93 *) let id_mut_pair3 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2)) @@ -437,7 +336,7 @@ let id_mut_pair3 Ok ((x, y), Ok, Ok) (** [no_nested_borrows::id_mut_pair4]: - Source: 'src/no_nested_borrows.rs', lines 426:0-426:92 *) + Source: 'src/no_nested_borrows.rs', lines 344:0-344:92 *) let id_mut_pair4 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2)) @@ -445,35 +344,35 @@ let id_mut_pair4 let (x, x1) = p in Ok ((x, x1), Ok, Ok) (** [no_nested_borrows::StructWithTuple] - Source: 'src/no_nested_borrows.rs', lines 433:0-433:34 *) + Source: 'src/no_nested_borrows.rs', lines 351:0-351:34 *) type structWithTuple_t (t1 t2 : Type0) = { p : (t1 & t2); } (** [no_nested_borrows::new_tuple1]: - Source: 'src/no_nested_borrows.rs', lines 437:0-437:48 *) + Source: 'src/no_nested_borrows.rs', lines 355:0-355:48 *) let new_tuple1 : result (structWithTuple_t u32 u32) = Ok { p = (1, 2) } (** [no_nested_borrows::new_tuple2]: - Source: 'src/no_nested_borrows.rs', lines 441:0-441:48 *) + Source: 'src/no_nested_borrows.rs', lines 359:0-359:48 *) let new_tuple2 : result (structWithTuple_t i16 i16) = Ok { p = (1, 2) } (** [no_nested_borrows::new_tuple3]: - Source: 'src/no_nested_borrows.rs', lines 445:0-445:48 *) + Source: 'src/no_nested_borrows.rs', lines 363:0-363:48 *) let new_tuple3 : result (structWithTuple_t u64 i64) = Ok { p = (1, 2) } (** [no_nested_borrows::StructWithPair] - Source: 'src/no_nested_borrows.rs', lines 450:0-450:33 *) + Source: 'src/no_nested_borrows.rs', lines 368:0-368:33 *) type structWithPair_t (t1 t2 : Type0) = { p : pair_t t1 t2; } (** [no_nested_borrows::new_pair1]: - Source: 'src/no_nested_borrows.rs', lines 454:0-454:46 *) + Source: 'src/no_nested_borrows.rs', lines 372:0-372:46 *) let new_pair1 : result (structWithPair_t u32 u32) = Ok { p = { x = 1; y = 2 } } (** [no_nested_borrows::test_constants]: - Source: 'src/no_nested_borrows.rs', lines 462:0-462:23 *) + Source: 'src/no_nested_borrows.rs', lines 380:0-380:23 *) let test_constants : result unit = let* swt = new_tuple1 in let (i, _) = swt.p in @@ -497,7 +396,7 @@ let test_constants : result unit = let _ = assert_norm (test_constants = Ok ()) (** [no_nested_borrows::test_weird_borrows1]: - Source: 'src/no_nested_borrows.rs', lines 471:0-471:28 *) + Source: 'src/no_nested_borrows.rs', lines 389:0-389:28 *) let test_weird_borrows1 : result unit = Ok () @@ -505,71 +404,71 @@ let test_weird_borrows1 : result unit = let _ = assert_norm (test_weird_borrows1 = Ok ()) (** [no_nested_borrows::test_mem_replace]: - Source: 'src/no_nested_borrows.rs', lines 481:0-481:37 *) + Source: 'src/no_nested_borrows.rs', lines 399:0-399:37 *) let test_mem_replace (px : u32) : result u32 = let (y, _) = core_mem_replace u32 px 1 in if not (y = 0) then Fail Failure else Ok 2 (** [no_nested_borrows::test_shared_borrow_bool1]: - Source: 'src/no_nested_borrows.rs', lines 488:0-488:47 *) + Source: 'src/no_nested_borrows.rs', lines 406:0-406:47 *) let test_shared_borrow_bool1 (b : bool) : result u32 = if b then Ok 0 else Ok 1 (** [no_nested_borrows::test_shared_borrow_bool2]: - Source: 'src/no_nested_borrows.rs', lines 501:0-501:40 *) + Source: 'src/no_nested_borrows.rs', lines 419:0-419:40 *) let test_shared_borrow_bool2 : result u32 = Ok 0 (** [no_nested_borrows::test_shared_borrow_enum1]: - Source: 'src/no_nested_borrows.rs', lines 516:0-516:52 *) + Source: 'src/no_nested_borrows.rs', lines 434:0-434:52 *) let test_shared_borrow_enum1 (l : list_t u32) : result u32 = begin match l with | List_Cons _ _ -> Ok 1 | List_Nil -> Ok 0 end (** [no_nested_borrows::test_shared_borrow_enum2]: - Source: 'src/no_nested_borrows.rs', lines 528:0-528:40 *) + Source: 'src/no_nested_borrows.rs', lines 446:0-446:40 *) let test_shared_borrow_enum2 : result u32 = Ok 0 (** [no_nested_borrows::incr]: - Source: 'src/no_nested_borrows.rs', lines 539:0-539:24 *) + Source: 'src/no_nested_borrows.rs', lines 457:0-457:24 *) let incr (x : u32) : result u32 = u32_add x 1 (** [no_nested_borrows::call_incr]: - Source: 'src/no_nested_borrows.rs', lines 543:0-543:35 *) + Source: 'src/no_nested_borrows.rs', lines 461:0-461:35 *) let call_incr (x : u32) : result u32 = incr x (** [no_nested_borrows::read_then_incr]: - Source: 'src/no_nested_borrows.rs', lines 548:0-548:41 *) + Source: 'src/no_nested_borrows.rs', lines 466:0-466:41 *) let read_then_incr (x : u32) : result (u32 & u32) = let* x1 = u32_add x 1 in Ok (x, x1) (** [no_nested_borrows::Tuple] - Source: 'src/no_nested_borrows.rs', lines 554:0-554:24 *) + Source: 'src/no_nested_borrows.rs', lines 472:0-472:24 *) type tuple_t (t1 t2 : Type0) = t1 * t2 (** [no_nested_borrows::use_tuple_struct]: - Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 *) + Source: 'src/no_nested_borrows.rs', lines 474:0-474:48 *) let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) = let (_, i) = x in Ok (1, i) (** [no_nested_borrows::create_tuple_struct]: - Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 *) + Source: 'src/no_nested_borrows.rs', lines 478:0-478:61 *) let create_tuple_struct (x : u32) (y : u64) : result (tuple_t u32 u64) = Ok (x, y) (** [no_nested_borrows::IdType] - Source: 'src/no_nested_borrows.rs', lines 565:0-565:20 *) + Source: 'src/no_nested_borrows.rs', lines 483:0-483:20 *) type idType_t (t : Type0) = t (** [no_nested_borrows::use_id_type]: - Source: 'src/no_nested_borrows.rs', lines 567:0-567:40 *) + Source: 'src/no_nested_borrows.rs', lines 485:0-485:40 *) let use_id_type (t : Type0) (x : idType_t t) : result t = Ok x (** [no_nested_borrows::create_id_type]: - Source: 'src/no_nested_borrows.rs', lines 571:0-571:43 *) + Source: 'src/no_nested_borrows.rs', lines 489:0-489:43 *) let create_id_type (t : Type0) (x : t) : result (idType_t t) = Ok x diff --git a/tests/lean/External/Opaque.lean b/tests/lean/External/Opaque.lean index d0297523..6cec334f 100644 --- a/tests/lean/External/Opaque.lean +++ b/tests/lean/External/Opaque.lean @@ -1,4 +1,3 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [external]: opaque function definitions import Base import External.Types diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean index abf04c94..a410b253 100644 --- a/tests/lean/HashmapMain/Opaque.lean +++ b/tests/lean/HashmapMain/Opaque.lean @@ -1,4 +1,3 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [hashmap_main]: opaque function definitions import Base import HashmapMain.Types diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 7d28f7f9..66ec917b 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -43,126 +43,23 @@ inductive Sum (T1 T2 : Type) := | Left : T1 → Sum T1 T2 | Right : T2 → Sum T1 T2 -/- [no_nested_borrows::neg_test]: - Source: 'src/no_nested_borrows.rs', lines 48:0-48:30 -/ -def neg_test (x : I32) : Result I32 := - -. x - -/- [no_nested_borrows::add_u32]: - Source: 'src/no_nested_borrows.rs', lines 54:0-54:37 -/ -def add_u32 (x : U32) (y : U32) : Result U32 := - x + y - -/- [no_nested_borrows::subs_u32]: - Source: 'src/no_nested_borrows.rs', lines 60:0-60:38 -/ -def subs_u32 (x : U32) (y : U32) : Result U32 := - x - y - -/- [no_nested_borrows::div_u32]: - Source: 'src/no_nested_borrows.rs', lines 66:0-66:37 -/ -def div_u32 (x : U32) (y : U32) : Result U32 := - x / y - -/- [no_nested_borrows::div_u32_const]: - Source: 'src/no_nested_borrows.rs', lines 73:0-73:35 -/ -def div_u32_const (x : U32) : Result U32 := - x / 2#u32 - -/- [no_nested_borrows::rem_u32]: - Source: 'src/no_nested_borrows.rs', lines 78:0-78:37 -/ -def rem_u32 (x : U32) (y : U32) : Result U32 := - x % y - -/- [no_nested_borrows::mul_u32]: - Source: 'src/no_nested_borrows.rs', lines 82:0-82:37 -/ -def mul_u32 (x : U32) (y : U32) : Result U32 := - x * y - -/- [no_nested_borrows::add_i32]: - Source: 'src/no_nested_borrows.rs', lines 88:0-88:37 -/ -def add_i32 (x : I32) (y : I32) : Result I32 := - x + y - -/- [no_nested_borrows::subs_i32]: - Source: 'src/no_nested_borrows.rs', lines 92:0-92:38 -/ -def subs_i32 (x : I32) (y : I32) : Result I32 := - x - y - -/- [no_nested_borrows::div_i32]: - Source: 'src/no_nested_borrows.rs', lines 96:0-96:37 -/ -def div_i32 (x : I32) (y : I32) : Result I32 := - x / y - -/- [no_nested_borrows::div_i32_const]: - Source: 'src/no_nested_borrows.rs', lines 100:0-100:35 -/ -def div_i32_const (x : I32) : Result I32 := - x / 2#i32 - -/- [no_nested_borrows::rem_i32]: - Source: 'src/no_nested_borrows.rs', lines 104:0-104:37 -/ -def rem_i32 (x : I32) (y : I32) : Result I32 := - x % y - -/- [no_nested_borrows::mul_i32]: - Source: 'src/no_nested_borrows.rs', lines 108:0-108:37 -/ -def mul_i32 (x : I32) (y : I32) : Result I32 := - x * y - -/- [no_nested_borrows::mix_arith_u32]: - Source: 'src/no_nested_borrows.rs', lines 112:0-112:51 -/ -def mix_arith_u32 (x : U32) (y : U32) (z : U32) : Result U32 := - do - let i ← x + y - let i1 ← x / y - let i2 ← i * i1 - let i3 ← z % y - let i4 ← x - i3 - let i5 ← i2 + i4 - let i6 ← x + y - let i7 ← i6 + z - i5 % i7 - -/- [no_nested_borrows::mix_arith_i32]: - Source: 'src/no_nested_borrows.rs', lines 116:0-116:51 -/ -def mix_arith_i32 (x : I32) (y : I32) (z : I32) : Result I32 := - do - let i ← x + y - let i1 ← x / y - let i2 ← i * i1 - let i3 ← z % y - let i4 ← x - i3 - let i5 ← i2 + i4 - let i6 ← x + y - let i7 ← i6 + z - i5 % i7 - -/- [no_nested_borrows::CONST0] - Source: 'src/no_nested_borrows.rs', lines 125:0-125:23 -/ -def CONST0_body : Result Usize := 1#usize + 1#usize -def CONST0 : Usize := eval_global CONST0_body - -/- [no_nested_borrows::CONST1] - Source: 'src/no_nested_borrows.rs', lines 126:0-126:23 -/ -def CONST1_body : Result Usize := 2#usize * 2#usize -def CONST1 : Usize := eval_global CONST1_body - /- [no_nested_borrows::cast_u32_to_i32]: - Source: 'src/no_nested_borrows.rs', lines 128:0-128:37 -/ + Source: 'src/no_nested_borrows.rs', lines 46:0-46:37 -/ def cast_u32_to_i32 (x : U32) : Result I32 := Scalar.cast .I32 x /- [no_nested_borrows::cast_bool_to_i32]: - Source: 'src/no_nested_borrows.rs', lines 132:0-132:39 -/ + Source: 'src/no_nested_borrows.rs', lines 50:0-50:39 -/ def cast_bool_to_i32 (x : Bool) : Result I32 := Scalar.cast_bool .I32 x /- [no_nested_borrows::cast_bool_to_bool]: - Source: 'src/no_nested_borrows.rs', lines 137:0-137:41 -/ + Source: 'src/no_nested_borrows.rs', lines 55:0-55:41 -/ def cast_bool_to_bool (x : Bool) : Result Bool := Result.ok x /- [no_nested_borrows::test2]: - Source: 'src/no_nested_borrows.rs', lines 142:0-142:14 -/ + Source: 'src/no_nested_borrows.rs', lines 60:0-60:14 -/ def test2 : Result Unit := do let _ ← 23#u32 + 44#u32 @@ -172,14 +69,14 @@ def test2 : Result Unit := #assert (test2 == Result.ok ()) /- [no_nested_borrows::get_max]: - Source: 'src/no_nested_borrows.rs', lines 154:0-154:37 -/ + Source: 'src/no_nested_borrows.rs', lines 72:0-72:37 -/ def get_max (x : U32) (y : U32) : Result U32 := if x >= y then Result.ok x else Result.ok y /- [no_nested_borrows::test3]: - Source: 'src/no_nested_borrows.rs', lines 162:0-162:14 -/ + Source: 'src/no_nested_borrows.rs', lines 80:0-80:14 -/ def test3 : Result Unit := do let x ← get_max 4#u32 3#u32 @@ -193,7 +90,7 @@ def test3 : Result Unit := #assert (test3 == Result.ok ()) /- [no_nested_borrows::test_neg1]: - Source: 'src/no_nested_borrows.rs', lines 169:0-169:18 -/ + Source: 'src/no_nested_borrows.rs', lines 87:0-87:18 -/ def test_neg1 : Result Unit := do let y ← -. 3#i32 @@ -205,7 +102,7 @@ def test_neg1 : Result Unit := #assert (test_neg1 == Result.ok ()) /- [no_nested_borrows::refs_test1]: - Source: 'src/no_nested_borrows.rs', lines 176:0-176:19 -/ + Source: 'src/no_nested_borrows.rs', lines 94:0-94:19 -/ def refs_test1 : Result Unit := if ¬ (1#i32 = 1#i32) then Result.fail .panic @@ -215,7 +112,7 @@ def refs_test1 : Result Unit := #assert (refs_test1 == Result.ok ()) /- [no_nested_borrows::refs_test2]: - Source: 'src/no_nested_borrows.rs', lines 187:0-187:19 -/ + Source: 'src/no_nested_borrows.rs', lines 105:0-105:19 -/ def refs_test2 : Result Unit := if ¬ (2#i32 = 2#i32) then Result.fail .panic @@ -233,7 +130,7 @@ def refs_test2 : Result Unit := #assert (refs_test2 == Result.ok ()) /- [no_nested_borrows::test_list1]: - Source: 'src/no_nested_borrows.rs', lines 203:0-203:19 -/ + Source: 'src/no_nested_borrows.rs', lines 121:0-121:19 -/ def test_list1 : Result Unit := Result.ok () @@ -241,7 +138,7 @@ def test_list1 : Result Unit := #assert (test_list1 == Result.ok ()) /- [no_nested_borrows::test_box1]: - Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 -/ + Source: 'src/no_nested_borrows.rs', lines 126:0-126:18 -/ def test_box1 : Result Unit := do let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32 @@ -255,26 +152,26 @@ def test_box1 : Result Unit := #assert (test_box1 == Result.ok ()) /- [no_nested_borrows::copy_int]: - Source: 'src/no_nested_borrows.rs', lines 218:0-218:30 -/ + Source: 'src/no_nested_borrows.rs', lines 136:0-136:30 -/ def copy_int (x : I32) : Result I32 := Result.ok x /- [no_nested_borrows::test_unreachable]: - Source: 'src/no_nested_borrows.rs', lines 224:0-224:32 -/ + Source: 'src/no_nested_borrows.rs', lines 142:0-142:32 -/ def test_unreachable (b : Bool) : Result Unit := if b then Result.fail .panic else Result.ok () /- [no_nested_borrows::test_panic]: - Source: 'src/no_nested_borrows.rs', lines 232:0-232:26 -/ + Source: 'src/no_nested_borrows.rs', lines 150:0-150:26 -/ def test_panic (b : Bool) : Result Unit := if b then Result.fail .panic else Result.ok () /- [no_nested_borrows::test_copy_int]: - Source: 'src/no_nested_borrows.rs', lines 239:0-239:22 -/ + Source: 'src/no_nested_borrows.rs', lines 157:0-157:22 -/ def test_copy_int : Result Unit := do let y ← copy_int 0#i32 @@ -286,14 +183,14 @@ def test_copy_int : Result Unit := #assert (test_copy_int == Result.ok ()) /- [no_nested_borrows::is_cons]: - Source: 'src/no_nested_borrows.rs', lines 246:0-246:38 -/ + Source: 'src/no_nested_borrows.rs', lines 164:0-164:38 -/ def is_cons (T : Type) (l : List T) : Result Bool := match l with | List.Cons _ _ => Result.ok true | List.Nil => Result.ok false /- [no_nested_borrows::test_is_cons]: - Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 -/ + Source: 'src/no_nested_borrows.rs', lines 171:0-171:21 -/ def test_is_cons : Result Unit := do let b ← is_cons I32 (List.Cons 0#i32 List.Nil) @@ -305,14 +202,14 @@ def test_is_cons : Result Unit := #assert (test_is_cons == Result.ok ()) /- [no_nested_borrows::split_list]: - Source: 'src/no_nested_borrows.rs', lines 259:0-259:48 -/ + Source: 'src/no_nested_borrows.rs', lines 177:0-177:48 -/ def split_list (T : Type) (l : List T) : Result (T × (List T)) := match l with | List.Cons hd tl => Result.ok (hd, tl) | List.Nil => Result.fail .panic /- [no_nested_borrows::test_split_list]: - Source: 'src/no_nested_borrows.rs', lines 267:0-267:24 -/ + Source: 'src/no_nested_borrows.rs', lines 185:0-185:24 -/ def test_split_list : Result Unit := do let p ← split_list I32 (List.Cons 0#i32 List.Nil) @@ -325,7 +222,7 @@ def test_split_list : Result Unit := #assert (test_split_list == Result.ok ()) /- [no_nested_borrows::choose]: - Source: 'src/no_nested_borrows.rs', lines 274:0-274:70 -/ + Source: 'src/no_nested_borrows.rs', lines 192:0-192:70 -/ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result (T × (T → Result (T × T))) @@ -337,7 +234,7 @@ def choose Result.ok (y, back) /- [no_nested_borrows::choose_test]: - Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/ + Source: 'src/no_nested_borrows.rs', lines 200:0-200:20 -/ def choose_test : Result Unit := do let (z, choose_back) ← choose I32 true 0#i32 0#i32 @@ -357,20 +254,20 @@ def choose_test : Result Unit := #assert (choose_test == Result.ok ()) /- [no_nested_borrows::test_char]: - Source: 'src/no_nested_borrows.rs', lines 294:0-294:26 -/ + Source: 'src/no_nested_borrows.rs', lines 212:0-212:26 -/ def test_char : Result Char := Result.ok 'a' mutual /- [no_nested_borrows::Tree] - Source: 'src/no_nested_borrows.rs', lines 299:0-299:16 -/ + Source: 'src/no_nested_borrows.rs', lines 217:0-217:16 -/ inductive Tree (T : Type) := | Leaf : T → Tree T | Node : T → NodeElem T → Tree T → Tree T /- [no_nested_borrows::NodeElem] - Source: 'src/no_nested_borrows.rs', lines 304:0-304:20 -/ + Source: 'src/no_nested_borrows.rs', lines 222:0-222:20 -/ inductive NodeElem (T : Type) := | Cons : Tree T → NodeElem T → NodeElem T | Nil : NodeElem T @@ -378,7 +275,7 @@ inductive NodeElem (T : Type) := end /- [no_nested_borrows::list_length]: - Source: 'src/no_nested_borrows.rs', lines 339:0-339:48 -/ + Source: 'src/no_nested_borrows.rs', lines 257:0-257:48 -/ divergent def list_length (T : Type) (l : List T) : Result U32 := match l with | List.Cons _ l1 => do @@ -387,7 +284,7 @@ divergent def list_length (T : Type) (l : List T) : Result U32 := | List.Nil => Result.ok 0#u32 /- [no_nested_borrows::list_nth_shared]: - Source: 'src/no_nested_borrows.rs', lines 347:0-347:62 -/ + Source: 'src/no_nested_borrows.rs', lines 265:0-265:62 -/ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := match l with | List.Cons x tl => @@ -399,7 +296,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := | List.Nil => Result.fail .panic /- [no_nested_borrows::list_nth_mut]: - Source: 'src/no_nested_borrows.rs', lines 363:0-363:67 -/ + Source: 'src/no_nested_borrows.rs', lines 281:0-281:67 -/ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with @@ -421,7 +318,7 @@ divergent def list_nth_mut | List.Nil => Result.fail .panic /- [no_nested_borrows::list_rev_aux]: - Source: 'src/no_nested_borrows.rs', lines 379:0-379:63 -/ + Source: 'src/no_nested_borrows.rs', lines 297:0-297:63 -/ divergent def list_rev_aux (T : Type) (li : List T) (lo : List T) : Result (List T) := match li with @@ -429,13 +326,13 @@ divergent def list_rev_aux | List.Nil => Result.ok lo /- [no_nested_borrows::list_rev]: - Source: 'src/no_nested_borrows.rs', lines 393:0-393:42 -/ + Source: 'src/no_nested_borrows.rs', lines 311:0-311:42 -/ def list_rev (T : Type) (l : List T) : Result (List T) := let (li, _) := core.mem.replace (List T) l List.Nil list_rev_aux T li List.Nil /- [no_nested_borrows::test_list_functions]: - Source: 'src/no_nested_borrows.rs', lines 398:0-398:28 -/ + Source: 'src/no_nested_borrows.rs', lines 316:0-316:28 -/ def test_list_functions : Result Unit := do let l := List.Cons 2#i32 List.Nil @@ -482,7 +379,7 @@ def test_list_functions : Result Unit := #assert (test_list_functions == Result.ok ()) /- [no_nested_borrows::id_mut_pair1]: - Source: 'src/no_nested_borrows.rs', lines 414:0-414:89 -/ + Source: 'src/no_nested_borrows.rs', lines 332:0-332:89 -/ def id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) @@ -490,7 +387,7 @@ def id_mut_pair1 Result.ok ((x, y), Result.ok) /- [no_nested_borrows::id_mut_pair2]: - Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/ + Source: 'src/no_nested_borrows.rs', lines 336:0-336:88 -/ def id_mut_pair2 (T1 T2 : Type) (p : (T1 × T2)) : Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) @@ -499,7 +396,7 @@ def id_mut_pair2 Result.ok ((t, t1), Result.ok) /- [no_nested_borrows::id_mut_pair3]: - Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/ + Source: 'src/no_nested_borrows.rs', lines 340:0-340:93 -/ def id_mut_pair3 (T1 T2 : Type) (x : T1) (y : T2) : Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2)) @@ -507,7 +404,7 @@ def id_mut_pair3 Result.ok ((x, y), Result.ok, Result.ok) /- [no_nested_borrows::id_mut_pair4]: - Source: 'src/no_nested_borrows.rs', lines 426:0-426:92 -/ + Source: 'src/no_nested_borrows.rs', lines 344:0-344:92 -/ def id_mut_pair4 (T1 T2 : Type) (p : (T1 × T2)) : Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2)) @@ -516,37 +413,37 @@ def id_mut_pair4 Result.ok ((t, t1), Result.ok, Result.ok) /- [no_nested_borrows::StructWithTuple] - Source: 'src/no_nested_borrows.rs', lines 433:0-433:34 -/ + Source: 'src/no_nested_borrows.rs', lines 351:0-351:34 -/ structure StructWithTuple (T1 T2 : Type) where p : (T1 × T2) /- [no_nested_borrows::new_tuple1]: - Source: 'src/no_nested_borrows.rs', lines 437:0-437:48 -/ + Source: 'src/no_nested_borrows.rs', lines 355:0-355:48 -/ def new_tuple1 : Result (StructWithTuple U32 U32) := Result.ok { p := (1#u32, 2#u32) } /- [no_nested_borrows::new_tuple2]: - Source: 'src/no_nested_borrows.rs', lines 441:0-441:48 -/ + Source: 'src/no_nested_borrows.rs', lines 359:0-359:48 -/ def new_tuple2 : Result (StructWithTuple I16 I16) := Result.ok { p := (1#i16, 2#i16) } /- [no_nested_borrows::new_tuple3]: - Source: 'src/no_nested_borrows.rs', lines 445:0-445:48 -/ + Source: 'src/no_nested_borrows.rs', lines 363:0-363:48 -/ def new_tuple3 : Result (StructWithTuple U64 I64) := Result.ok { p := (1#u64, 2#i64) } /- [no_nested_borrows::StructWithPair] - Source: 'src/no_nested_borrows.rs', lines 450:0-450:33 -/ + Source: 'src/no_nested_borrows.rs', lines 368:0-368:33 -/ structure StructWithPair (T1 T2 : Type) where p : Pair T1 T2 /- [no_nested_borrows::new_pair1]: - Source: 'src/no_nested_borrows.rs', lines 454:0-454:46 -/ + Source: 'src/no_nested_borrows.rs', lines 372:0-372:46 -/ def new_pair1 : Result (StructWithPair U32 U32) := Result.ok { p := { x := 1#u32, y := 2#u32 } } /- [no_nested_borrows::test_constants]: - Source: 'src/no_nested_borrows.rs', lines 462:0-462:23 -/ + Source: 'src/no_nested_borrows.rs', lines 380:0-380:23 -/ def test_constants : Result Unit := do let swt ← new_tuple1 @@ -576,7 +473,7 @@ def test_constants : Result Unit := #assert (test_constants == Result.ok ()) /- [no_nested_borrows::test_weird_borrows1]: - Source: 'src/no_nested_borrows.rs', lines 471:0-471:28 -/ + Source: 'src/no_nested_borrows.rs', lines 389:0-389:28 -/ def test_weird_borrows1 : Result Unit := Result.ok () @@ -584,7 +481,7 @@ def test_weird_borrows1 : Result Unit := #assert (test_weird_borrows1 == Result.ok ()) /- [no_nested_borrows::test_mem_replace]: - Source: 'src/no_nested_borrows.rs', lines 481:0-481:37 -/ + Source: 'src/no_nested_borrows.rs', lines 399:0-399:37 -/ def test_mem_replace (px : U32) : Result U32 := let (y, _) := core.mem.replace U32 px 1#u32 if ¬ (y = 0#u32) @@ -592,71 +489,71 @@ def test_mem_replace (px : U32) : Result U32 := else Result.ok 2#u32 /- [no_nested_borrows::test_shared_borrow_bool1]: - Source: 'src/no_nested_borrows.rs', lines 488:0-488:47 -/ + Source: 'src/no_nested_borrows.rs', lines 406:0-406:47 -/ def test_shared_borrow_bool1 (b : Bool) : Result U32 := if b then Result.ok 0#u32 else Result.ok 1#u32 /- [no_nested_borrows::test_shared_borrow_bool2]: - Source: 'src/no_nested_borrows.rs', lines 501:0-501:40 -/ + Source: 'src/no_nested_borrows.rs', lines 419:0-419:40 -/ def test_shared_borrow_bool2 : Result U32 := Result.ok 0#u32 /- [no_nested_borrows::test_shared_borrow_enum1]: - Source: 'src/no_nested_borrows.rs', lines 516:0-516:52 -/ + Source: 'src/no_nested_borrows.rs', lines 434:0-434:52 -/ def test_shared_borrow_enum1 (l : List U32) : Result U32 := match l with | List.Cons _ _ => Result.ok 1#u32 | List.Nil => Result.ok 0#u32 /- [no_nested_borrows::test_shared_borrow_enum2]: - Source: 'src/no_nested_borrows.rs', lines 528:0-528:40 -/ + Source: 'src/no_nested_borrows.rs', lines 446:0-446:40 -/ def test_shared_borrow_enum2 : Result U32 := Result.ok 0#u32 /- [no_nested_borrows::incr]: - Source: 'src/no_nested_borrows.rs', lines 539:0-539:24 -/ + Source: 'src/no_nested_borrows.rs', lines 457:0-457:24 -/ def incr (x : U32) : Result U32 := x + 1#u32 /- [no_nested_borrows::call_incr]: - Source: 'src/no_nested_borrows.rs', lines 543:0-543:35 -/ + Source: 'src/no_nested_borrows.rs', lines 461:0-461:35 -/ def call_incr (x : U32) : Result U32 := incr x /- [no_nested_borrows::read_then_incr]: - Source: 'src/no_nested_borrows.rs', lines 548:0-548:41 -/ + Source: 'src/no_nested_borrows.rs', lines 466:0-466:41 -/ def read_then_incr (x : U32) : Result (U32 × U32) := do let x1 ← x + 1#u32 Result.ok (x, x1) /- [no_nested_borrows::Tuple] - Source: 'src/no_nested_borrows.rs', lines 554:0-554:24 -/ + Source: 'src/no_nested_borrows.rs', lines 472:0-472:24 -/ def Tuple (T1 T2 : Type) := T1 × T2 /- [no_nested_borrows::use_tuple_struct]: - Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 -/ + Source: 'src/no_nested_borrows.rs', lines 474:0-474:48 -/ def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) := Result.ok (1#u32, x.#1) /- [no_nested_borrows::create_tuple_struct]: - Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 -/ + Source: 'src/no_nested_borrows.rs', lines 478:0-478:61 -/ def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) := Result.ok (x, y) /- [no_nested_borrows::IdType] - Source: 'src/no_nested_borrows.rs', lines 565:0-565:20 -/ + Source: 'src/no_nested_borrows.rs', lines 483:0-483:20 -/ @[reducible] def IdType (T : Type) := T /- [no_nested_borrows::use_id_type]: - Source: 'src/no_nested_borrows.rs', lines 567:0-567:40 -/ + Source: 'src/no_nested_borrows.rs', lines 485:0-485:40 -/ def use_id_type (T : Type) (x : IdType T) : Result T := Result.ok x /- [no_nested_borrows::create_id_type]: - Source: 'src/no_nested_borrows.rs', lines 571:0-571:43 -/ + Source: 'src/no_nested_borrows.rs', lines 489:0-489:43 -/ def create_id_type (T : Type) (x : T) : Result (IdType T) := Result.ok x |