From dbbb01630190d999d3932fabd8a181b4f826f64f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 11:00:05 +0100 Subject: Improve logging and introduce eval_operands_prepare --- src/InterpreterExpansion.ml | 13 ++++++++++++ src/InterpreterExpressions.ml | 48 +++++++++++++++++++++++++++++++++++++++---- src/InterpreterUtils.ml | 21 ++++++++++--------- src/Logging.ml | 13 ++++++++++++ src/Print.ml | 8 +++++++- src/main.ml | 8 ++++++++ 6 files changed, 96 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 345c3df3..aebcda3c 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -16,6 +16,9 @@ open InterpreterUtils open InterpreterProjectors open InterpreterBorrows +(** The local logger *) +let log = L.expansion_log + (** Projector kind *) type proj_kind = LoanProj | BorrowProj @@ -366,6 +369,8 @@ let expand_symbolic_value_borrow (config : C.config) let expand_symbolic_value_no_branching (config : C.config) (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = + (* Remember the initial context for printing purposes *) + let ctx0 = ctx in (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) let original_sv = sp in @@ -424,6 +429,14 @@ let expand_symbolic_value_no_branching (config : C.config) failwith ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) in + (* Debugging *) + (* Debug *) + log#ldebug + (lazy + ("expand_symbolic_value: " + ^ symbolic_value_to_string ctx0 sp + ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Sanity check: the symbolic value has disappeared *) assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); (* Return *) diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 0b4bc90f..f3b07cc2 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -14,6 +14,9 @@ open InterpreterUtils open InterpreterExpansion open InterpreterPaths +(** The local logger *) +let log = L.expressions_log + (** TODO: change the name *) type eval_error = Panic @@ -70,7 +73,37 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) | _, Unit | _, ConstantAdt _ | _, ConstantValue _ -> failwith "Improperly typed constant value" -(** Prepare the evaluation of an operand. *) +(** Prepare the evaluation of an operand. + + Evaluating an operand requires updating the context to get access to a + given place (by ending borrows, expanding symbolic values...) then + applying the operand operation (move, copy, etc.). + + Sometimes, we want to decouple the two operations. + Consider the following example: + ``` + context = { + x -> shared_borrow l0 + y -> shared_loan {l0} v + } + + dest <- f(move x, move y); + ... + ``` + Because of the way end_borrow is implemented, when giving back the borrow + `l0` upon evaluating `move y`, we won't notice that `shared_borrow l0` has + disappeared from the environment (it has been moved and not assigned yet, + and so is hanging in "thin air"). + + By first "preparing" the operands evaluation, we make sure no such thing + happens. To be more precise, we make sure all the updates to borrows triggered + by access *and* move operations have already been applied. + + As a side note: doing this is actually not completely necessary because when + generating MIR, rustc introduces intermediate assignments for all the function + parameters. Still, it is better for soundness purposes, and corresponds to + what we do in the formal semantics. + *) let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : C.eval_ctx * V.typed_value = let ctx, v = @@ -94,7 +127,7 @@ let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand) let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : C.eval_ctx * V.typed_value = (* Debug *) - L.log#ldebug + log#ldebug (lazy ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n" ^ operand_to_string ctx op ^ "\n")); @@ -108,7 +141,6 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : let access = Read in let ctx, v = prepare_rplace config access p ctx in (* Copy the value *) - L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v)); assert (not (bottom_in_value ctx.ended_regions v)); let allow_adt_copy = false in copy_value allow_adt_copy config ctx v @@ -117,16 +149,24 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : let access = Move in let ctx, v = prepare_rplace config access p ctx in (* Move the value *) - L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v)); assert (not (bottom_in_value ctx.ended_regions v)); let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in match write_place config access p bottom ctx with | Error _ -> failwith "Unreachable" | Ok ctx -> (ctx, v)) +(** Small utility. + + See [eval_operand_prepare]. + *) +let eval_operands_prepare (config : C.config) (ctx : C.eval_ctx) + (ops : E.operand list) : C.eval_ctx * V.typed_value list = + List.fold_left_map (fun ctx op -> eval_operand_prepare config ctx op) ctx ops + (** Evaluate several operands. *) let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list) : C.eval_ctx * V.typed_value list = + let ctx, _ = eval_operands_prepare config ctx ops in List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 5f86fec2..6aa3199b 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -8,28 +8,29 @@ module Subst = Substitute module A = CfimAst open Utils open TypesUtils +module PA = Print.EvalCtxCfimAst (** Some utilities *) let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string -let ety_to_string = Print.EvalCtxCfimAst.ety_to_string +let ety_to_string = PA.ety_to_string -let rty_to_string = Print.EvalCtxCfimAst.rty_to_string +let rty_to_string = PA.rty_to_string -let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string +let symbolic_value_to_string = PA.symbolic_value_to_string -let typed_avalue_to_string = Print.EvalCtxCfimAst.typed_avalue_to_string +let typed_value_to_string = PA.typed_value_to_string -let place_to_string = Print.EvalCtxCfimAst.place_to_string +let typed_avalue_to_string = PA.typed_avalue_to_string -let operand_to_string = Print.EvalCtxCfimAst.operand_to_string +let place_to_string = PA.place_to_string -let statement_to_string ctx = - Print.EvalCtxCfimAst.statement_to_string ctx "" " " +let operand_to_string = PA.operand_to_string -let statement_to_string_with_tab ctx = - Print.EvalCtxCfimAst.statement_to_string ctx " " " " +let statement_to_string ctx = PA.statement_to_string ctx "" " " + +let statement_to_string_with_tab ctx = PA.statement_to_string ctx " " " " let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool = sv0.V.sv_id = sv1.V.sv_id diff --git a/src/Logging.ml b/src/Logging.ml index a1060014..ccf63d0d 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -3,8 +3,21 @@ module L = Easy_logging.Logging let _ = L.make_logger "MainLogger" Debug [ Cli Debug ] +(** The main logger *) let log = L.get_logger "MainLogger" +(** Below, we create subgloggers for various submodules, so that we can precisely + toggle logging on/off, depending on which information we need *) + +(** Logger for InterpreterStatements *) +let statements_log = L.get_logger "MainLogger.Statements" + +(** Logger for InterpreterExpansion *) +let expansion_log = L.get_logger "MainLogger.Statements.Expansion" + +(** Logger for InterpreterExpressions *) +let expressions_log = L.get_logger "MainLogger.Statements.Expressions" + (** Terminal colors - TODO: comes from easy_logging (did not manage to reuse the module directly) *) type color = | Default diff --git a/src/Print.ml b/src/Print.ml index f714e847..ce31338d 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -390,7 +390,7 @@ module Values = struct ^ typed_avalue_to_string fmt av ^ ")" | AEndedIgnoredMutLoan ml -> - "@ended_ignored_mut_borrow{ given_back=" + "@ended_ignored_mut_loan{ given_back=" ^ typed_avalue_to_string fmt ml.given_back ^ "; child: " ^ typed_avalue_to_string fmt ml.child @@ -973,6 +973,12 @@ module EvalCtxCfimAst = struct let fmt = PC.ctx_to_rtype_formatter fmt in PT.rty_to_string fmt t + let symbolic_value_to_string (ctx : C.eval_ctx) (sv : V.symbolic_value) : + string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + let fmt = PC.ctx_to_rtype_formatter fmt in + PV.symbolic_value_to_string fmt sv + let typed_value_to_string (ctx : C.eval_ctx) (v : V.typed_value) : string = let fmt = PC.eval_ctx_to_ctx_formatter ctx in PV.typed_value_to_string fmt v diff --git a/src/main.ml b/src/main.ml index e5c3c324..326ba08e 100644 --- a/src/main.ml +++ b/src/main.ml @@ -4,6 +4,7 @@ open Print module T = Types module A = CfimAst module I = Interpreter +module EL = Easy_logging.Logging (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work *) @@ -18,6 +19,7 @@ Usage: %s [OPTIONS] FILE Sys.argv.(0) let () = + (* Read the command line arguments *) let spec = [] in let spec = Arg.align spec in let filename = ref "" in @@ -38,6 +40,12 @@ let () = if !filename = "" then ( print_string usage; exit 1); + (* Set up the logging - for now we use default values - TODO: use the + * command-line arguments *) + statements_log#set_level EL.Debug; + expansion_log#set_level EL.Debug; + expressions_log#set_level EL.Warning; + (* Load the module *) let json = Yojson.Basic.from_file !filename in match cfim_module_of_json json with | Error s -> log#error "error: %s\n" s -- cgit v1.2.3 From e41b8da810b80a3e42bd5289dedfdb7bf2f10550 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 11:06:56 +0100 Subject: Make more improvements to logging --- src/Invariants.ml | 42 +++++++++++++++++++++--------------------- src/Logging.ml | 13 ++++++++++--- src/main.ml | 1 + 3 files changed, 32 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/Invariants.ml b/src/Invariants.ml index e214e820..65a74c31 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -12,7 +12,8 @@ open TypesUtils open InterpreterUtils open InterpreterBorrowsCore -let debug_invariants : bool ref = ref false +(** The local logger *) +let log = L.invariants_log type borrow_info = { loan_kind : T.ref_kind; @@ -36,19 +37,23 @@ let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info = { outer_borrow = true; outer_shared = true } (* TODO: we need to factorize print functions for strings *) -let ids_reprs_to_string (reprs : V.BorrowId.id V.BorrowId.Map.t) : string = +let ids_reprs_to_string (indent : string) + (reprs : V.BorrowId.id V.BorrowId.Map.t) : string = let bindings = V.BorrowId.Map.bindings reprs in let bindings = List.map (fun (id, repr_id) -> - V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id) + indent ^ V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id) bindings in String.concat "\n" bindings -let borrows_infos_to_string (infos : borrow_info V.BorrowId.Map.t) : string = +let borrows_infos_to_string (indent : string) + (infos : borrow_info V.BorrowId.Map.t) : string = let bindings = V.BorrowId.Map.bindings infos in - let bindings = List.map (fun (_, info) -> show_borrow_info info) bindings in + let bindings = + List.map (fun (_, info) -> indent ^ show_borrow_info info) bindings + in String.concat "\n" bindings type borrow_kind = Mut | Shared | Inactivated @@ -67,8 +72,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = let borrows_infos : borrow_info V.BorrowId.Map.t ref = ref V.BorrowId.Map.empty in + let context_to_string () : string = + eval_ctx_to_string ctx ^ "- representants:\n" + ^ ids_reprs_to_string " " !ids_reprs + ^ "\n- info:\n" + ^ borrows_infos_to_string " " !borrows_infos + in - (* First, register all the loans *) + (* first, register all the loans *) (* Some utilities to register the loans *) let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.set_t) : unit = @@ -178,13 +189,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = | None -> let err = "find_info: could not find the representant of borrow " - ^ V.BorrowId.to_string bid ^ "\n" ^ "\n- Context:\n" - ^ eval_ctx_to_string ctx ^ "\n- representants:\n" - ^ ids_reprs_to_string !ids_reprs - ^ "\n- info:\n" - ^ borrows_infos_to_string !borrows_infos + ^ V.BorrowId.to_string bid ^ "\n" ^ context_to_string () in - L.log#serror err; + log#serror err; failwith err in @@ -259,15 +266,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = borrows_visitor#visit_eval_ctx () ctx; (* Debugging *) - if !debug_invariants then ( - L.log#ldebug - (lazy - ("\nAbout to check context invariant:\n" ^ eval_ctx_to_string ctx ^ "\n")); - L.log#ldebug - (lazy - ("\nBorrows information:\n" - ^ borrows_infos_to_string !borrows_infos - ^ "\n"))); + log#ldebug + (lazy ("\nAbout to check context invariant:\n" ^ context_to_string ())); (* Finally, check that everything is consistant *) V.BorrowId.Map.iter diff --git a/src/Logging.ml b/src/Logging.ml index ccf63d0d..b0eeadb7 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -9,14 +9,21 @@ let log = L.get_logger "MainLogger" (** Below, we create subgloggers for various submodules, so that we can precisely toggle logging on/off, depending on which information we need *) +(** Logger for Interpreter *) +let interpreter_log = L.get_logger "MainLogger.Interpreter" + (** Logger for InterpreterStatements *) -let statements_log = L.get_logger "MainLogger.Statements" +let statements_log = L.get_logger "MainLogger.Interpreter.Statements" (** Logger for InterpreterExpansion *) -let expansion_log = L.get_logger "MainLogger.Statements.Expansion" +let expansion_log = L.get_logger "MainLogger.Interpreter.Statements.Expansion" (** Logger for InterpreterExpressions *) -let expressions_log = L.get_logger "MainLogger.Statements.Expressions" +let expressions_log = + L.get_logger "MainLogger.Interpreter.Statements.Expressions" + +(** Logger for Invariants *) +let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants" (** Terminal colors - TODO: comes from easy_logging (did not manage to reuse the module directly) *) type color = diff --git a/src/main.ml b/src/main.ml index 326ba08e..b151cce7 100644 --- a/src/main.ml +++ b/src/main.ml @@ -45,6 +45,7 @@ let () = statements_log#set_level EL.Debug; expansion_log#set_level EL.Debug; expressions_log#set_level EL.Warning; + invariants_log#set_level EL.Warning; (* Load the module *) let json = Yojson.Basic.from_file !filename in match cfim_module_of_json json with -- cgit v1.2.3 From 37bcc5a38cf7d92d70c16850714b42d57846c7c2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 11:19:26 +0100 Subject: Add logging information for borrows --- src/InterpreterBorrows.ml | 29 ++++++++++++++++++++++++++++- src/InterpreterBorrowsCore.ml | 3 +++ src/Invariants.ml | 2 +- src/Logging.ml | 10 ++++++---- src/main.ml | 3 ++- 5 files changed, 40 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 1dd4d247..c9637f46 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -743,12 +743,30 @@ and end_borrows (config : C.config) (io : inner_outer) and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = + (* Remember the original context for printing purposes *) + let ctx0 = ctx in + log#ldebug + (lazy + ("end_abstraction: " + ^ V.AbstractionId.to_string abs_id + ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0)); (* Lookup the abstraction *) let abs = C.ctx_lookup_abs ctx abs_id in (* End the parent abstractions first *) let ctx = end_abstractions config abs.parents ctx in + log#ldebug + (lazy + ("end_abstraction: " + ^ V.AbstractionId.to_string abs_id + ^ "\n- context after parent abstractions ended:\n" + ^ eval_ctx_to_string ctx)); (* End the loans inside the abstraction *) let ctx = end_abstraction_loans config abs_id ctx in + log#ldebug + (lazy + ("end_abstraction: " + ^ V.AbstractionId.to_string abs_id + ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)); (* End the abstraction itself by redistributing the borrows it contains *) let ctx = end_abstraction_borrows config abs_id ctx in (* End the regions owned by the abstraction - note that we don't need to @@ -762,7 +780,16 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) in (* Remove all the references to the id of the current abstraction, and remove * the abstraction itself *) - end_abstraction_remove_from_context config abs_id ctx + let ctx = end_abstraction_remove_from_context config abs_id ctx in + (* Debugging *) + log#ldebug + (lazy + ("end_abstraction: " + ^ V.AbstractionId.to_string abs_id + ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)); + (* Return *) + ctx and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t) (ctx : C.eval_ctx) : C.eval_ctx = diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index bc2f5971..aaab18cb 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -9,6 +9,9 @@ module Subst = Substitute module L = Logging open InterpreterUtils +(** The local logger *) +let log = L.borrows_log + (** TODO: cleanup this a bit, once we have a better understanding about what we need. TODO: I'm not sure in which file this should be moved... *) diff --git a/src/Invariants.ml b/src/Invariants.ml index 65a74c31..3c5d24e3 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -36,7 +36,7 @@ let set_outer_mut (info : outer_borrow_info) : outer_borrow_info = let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info = { outer_borrow = true; outer_shared = true } -(* TODO: we need to factorize print functions for strings *) +(* TODO: we need to factorize print functions for sets *) let ids_reprs_to_string (indent : string) (reprs : V.BorrowId.id V.BorrowId.Map.t) : string = let bindings = V.BorrowId.Map.bindings reprs in diff --git a/src/Logging.ml b/src/Logging.ml index b0eeadb7..2759854c 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -15,12 +15,14 @@ let interpreter_log = L.get_logger "MainLogger.Interpreter" (** Logger for InterpreterStatements *) let statements_log = L.get_logger "MainLogger.Interpreter.Statements" +(** Logger for InterpreterExpressions *) +let expressions_log = L.get_logger "MainLogger.Interpreter.Expressions" + (** Logger for InterpreterExpansion *) -let expansion_log = L.get_logger "MainLogger.Interpreter.Statements.Expansion" +let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion" -(** Logger for InterpreterExpressions *) -let expressions_log = - L.get_logger "MainLogger.Interpreter.Statements.Expressions" +(** Logger for InterpreterBorrows *) +let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows" (** Logger for Invariants *) let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants" diff --git a/src/main.ml b/src/main.ml index b151cce7..da1b333e 100644 --- a/src/main.ml +++ b/src/main.ml @@ -43,8 +43,9 @@ let () = (* Set up the logging - for now we use default values - TODO: use the * command-line arguments *) statements_log#set_level EL.Debug; - expansion_log#set_level EL.Debug; expressions_log#set_level EL.Warning; + expansion_log#set_level EL.Debug; + borrows_log#set_level EL.Debug; invariants_log#set_level EL.Warning; (* Load the module *) let json = Yojson.Basic.from_file !filename in -- cgit v1.2.3 From 8917bf6aca4465873e7e7642719c70789d97590c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 12:39:58 +0100 Subject: Add an optional borrow identifier to AIgnoredMutBorrow, introduce the AEndedIgnoredMutBorrow variant and fix a couple of bugs --- src/Interpreter.ml | 15 ++++++- src/InterpreterBorrows.ml | 100 ++++++++++++++++++++++++++++++++++++------ src/InterpreterBorrowsCore.ml | 13 ++++-- src/InterpreterExpansion.ml | 22 +++++----- src/InterpreterProjectors.ml | 27 +++++++----- src/InterpreterStatements.ml | 17 ++++++- src/Invariants.ml | 13 ++++-- src/Print.ml | 17 ++++++- src/Values.ml | 47 +++++++++++++++++--- 9 files changed, 220 insertions(+), 51 deletions(-) (limited to 'src') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 2789517e..9ac8149b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -67,6 +67,9 @@ module Test = struct List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs in (* Create the abstractions and insert them in the context *) + let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref = + ref V.AbstractionId.Map.empty + in let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = let abs_id = rg.A.id in let parents = @@ -79,10 +82,20 @@ module Test = struct (fun s rid -> T.RegionId.Set.add rid s) T.RegionId.Set.empty rg.A.regions in + let ancestors_regions = + List.fold_left + (fun acc parent_id -> + T.RegionId.Set.union acc + (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) + regions rg.A.parents + in + abs_to_ancestors_regions := + V.AbstractionId.Map.add abs_id ancestors_regions + !abs_to_ancestors_regions; (* Project over the values - we use *loan* projectors, as explained above *) let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in (* Create the abstraction *) - let abs = { V.abs_id; parents; regions; avalues } in + let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in (* Insert the abstraction in the context *) let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index c9637f46..b52454b1 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -169,9 +169,14 @@ let end_borrow_get_borrow (io : inner_outer) * of the two cases described above *) V.ABottom) else V.ABorrow (super#visit_ASharedBorrow outer bid) - | V.AIgnoredMutBorrow av -> + | V.AIgnoredMutBorrow (opt_bid, av) -> (* Nothing special to do *) - V.ABorrow (super#visit_AIgnoredMutBorrow outer av) + V.ABorrow (super#visit_AIgnoredMutBorrow outer opt_bid av) + | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } -> + (* Nothing special to do *) + V.ABorrow + (super#visit_AEndedIgnoredMutBorrow outer given_back_loans_proj + child) | V.AProjSharedBorrow asb -> (* Check if the borrow we are looking for is in the asb *) if borrow_in_asb l asb then ( @@ -232,7 +237,18 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) object (self) inherit [_] C.map_eval_ctx as super - method! visit_Loan opt_abs lc = + method! visit_typed_value opt_abs (v : V.typed_value) : V.typed_value = + match v.V.value with + | V.Loan lc -> + let value = self#visit_typed_Loan opt_abs v.V.ty lc in + ({ v with V.value } : V.typed_value) + | _ -> super#visit_typed_value opt_abs v + (** This is a bit annoying, but as we need the type of the value we + are exploring, for sanity checks, we need to implement + [visit_typed_avalue] instead of + overriding [visit_ALoan] *) + + method visit_typed_Loan opt_abs ty lc = match lc with | V.SharedLoan (bids, v) -> (* We are giving back a value (i.e., the content of a *mutable* @@ -241,6 +257,15 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) | V.MutLoan bid' -> (* Check if this is the loan we are looking for *) if bid' = bid then ( + (* Sanity check *) + let expected_ty = ty in + if nv.V.ty <> expected_ty then ( + log#serror + ("give_back_value: improper type:\n- expected: " + ^ ety_to_string ctx ty ^ "\n- received: " + ^ ety_to_string ctx nv.V.ty); + failwith "Value given back doesn't have the proper type"); + (* Replace *) set_replaced (); nv.V.value) else V.Loan (super#visit_MutLoan opt_abs bid') @@ -257,15 +282,46 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) back, we need to reimplement [visit_typed_avalue] instead of [visit_ALoan] *) + method! visit_ABorrow (opt_abs : V.abs option) (bc : V.aborrow_content) + : V.avalue = + match bc with + | V.AIgnoredMutBorrow (bid', child) -> + if bid' = Some bid then + (* Insert a loans projector - note that if this case happens, + * it is necessarily because we ended a parent abstraction, + * and the given back value is thus a symbolic value *) + match nv.V.value with + | V.Symbolic sv -> + (* The loan projector *) + let given_back_loans_proj = + mk_aproj_loans_from_symbolic_value sv + in + (* Continue giving back in the child value *) + let child = super#visit_typed_avalue opt_abs child in + (* Return *) + V.ABorrow + (V.AEndedIgnoredMutBorrow { given_back_loans_proj; child }) + | _ -> failwith "Unreachable" + else + (* Continue exploring *) + V.ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child) + | _ -> + (* Continue exploring *) + super#visit_ABorrow opt_abs bc + (** We need to inspect ignored mutable borrows, to insert loan projectors + if necessary. + *) + method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty) (lc : V.aloan_content) : V.avalue = (* Preparing a bit *) - let regions = + let regions, ancestors_regions = match opt_abs with | None -> failwith "Unreachable" - | Some abs -> abs.V.regions + | Some abs -> (abs.V.regions, abs.V.ancestors_regions) in - (* Rk.: there is a small issue with the types of the aloan values *) + (* Rk.: there is a small issue with the types of the aloan values. + * See the comment at the level of definition of [typed_avalue] *) let borrowed_value_aty = let _, ty, _ = ty_get_ref ty in ty @@ -281,8 +337,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) (* Apply the projection *) let given_back = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions nv borrowed_value_aty + regions ancestors_regions nv borrowed_value_aty in + (* Continue giving back in the child value *) + let child = super#visit_typed_avalue opt_abs child in (* Return the new value *) V.ALoan (V.AEndedMutLoan { given_back; child })) else @@ -307,8 +365,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) * (i.e., we don't call [set_replaced]) *) let given_back = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions nv borrowed_value_aty + regions ancestors_regions nv borrowed_value_aty in + (* Continue giving back in the child value *) + let child = super#visit_typed_avalue opt_abs child in V.ALoan (V.AEndedIgnoredMutLoan { given_back; child }) else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child) | V.AEndedIgnoredMutLoan { given_back; child } -> @@ -378,13 +438,22 @@ let give_back_avalue (_config : C.config) (bid : V.BorrowId.id) match lc with | V.AMutLoan (bid', child) -> if bid' = bid then ( + (* Sanity check - about why we need to call [ty_get_ref] + * (and don't do the same thing as in [give_back_value]) + * see the comment at the level of the definition of + * [typed_avalue] *) + let _, expected_ty, _ = ty_get_ref ty in + if nv.V.ty <> expected_ty then ( + log#serror + ("give_back_avalue: improper type:\n- expected: " + ^ rty_to_string ctx ty ^ "\n- received: " + ^ rty_to_string ctx nv.V.ty); + failwith "Value given back doesn't have the proper type"); (* This is the loan we are looking for: apply the projection to * the value we give back and replaced this mutable loan with * an ended loan *) (* Register the insertion *) set_replaced (); - (* Sanity check *) - assert (nv.V.ty = ty); (* Return the new value *) V.ALoan (V.AEndedMutLoan { given_back = nv; child })) else @@ -600,7 +669,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) assert (borrow_in_asb l asb); (* Update the context *) give_back_shared config l ctx - | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable" + | Abstract (V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _) -> + failwith "Unreachable" (** Convert an [avalue] to a [value]. @@ -889,7 +959,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) asb then raise (FoundABorrowContent bc) else () - | V.AIgnoredMutBorrow _ -> + | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> (* Nothing to do for ignored borrows *) () end @@ -918,7 +988,8 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) with | V.AsbBorrow bid -> bid | _ -> failwith "Unexpected") - | V.AIgnoredMutBorrow _ -> failwith "Unexpected" + | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> + failwith "Unexpected" in let ctx = update_aborrow ek_all bid V.ABottom ctx in (* Then give back the value *) @@ -932,7 +1003,8 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) | V.AProjSharedBorrow _ -> (* Nothing to do *) ctx - | V.AIgnoredMutBorrow _ -> failwith "Unexpected" + | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> + failwith "Unexpected" in (* Reexplore *) end_abstraction_borrows config abs_id ctx diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index aaab18cb..b590eff6 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -305,7 +305,10 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.ASharedBorrow bid -> if bid = l then raise (FoundGBorrowContent (Abstract bc)) else super#visit_ASharedBorrow env bid - | V.AIgnoredMutBorrow av -> super#visit_AIgnoredMutBorrow env av + | V.AIgnoredMutBorrow (opt_bid, av) -> + super#visit_AIgnoredMutBorrow env opt_bid av + | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } -> + super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj child | V.AProjSharedBorrow asb -> if borrow_in_asb l asb then raise (FoundGBorrowContent (Abstract bc)) @@ -418,8 +421,12 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) | V.ASharedBorrow bid -> if bid = l then update () else V.ABorrow (super#visit_ASharedBorrow env bid) - | V.AIgnoredMutBorrow av -> - V.ABorrow (super#visit_AIgnoredMutBorrow env av) + | V.AIgnoredMutBorrow (opt_bid, av) -> + V.ABorrow (super#visit_AIgnoredMutBorrow env opt_bid av) + | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } -> + V.ABorrow + (super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj + child) | V.AProjSharedBorrow asb -> if borrow_in_asb l asb then update () else V.ABorrow (super#visit_AProjSharedBorrow env asb) diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index aebcda3c..e19f8bb4 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -63,15 +63,17 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) object inherit [_] C.map_eval_ctx as super - method! visit_abs proj_regions abs = - assert (Option.is_none proj_regions); - let proj_regions = Some abs.V.regions in - super#visit_abs proj_regions abs + method! visit_abs current_abs abs = + assert (Option.is_none current_abs); + let current_abs = Some abs in + super#visit_abs current_abs abs (** When visiting an abstraction, we remember the regions it owns to be able to properly reduce projectors when expanding symbolic values *) - method! visit_ASymbolic proj_regions aproj = - let proj_regions = Option.get proj_regions in + method! visit_ASymbolic current_abs aproj = + let current_abs = Option.get current_abs in + let proj_regions = current_abs.regions in + let ancestors_regions = current_abs.ancestors_regions in match (aproj, proj_kind) with | V.AProjLoans sv, LoanProj -> (* Check if this is the symbolic value we are looking for *) @@ -85,7 +87,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) projected_value.V.value else (* Not the searched symbolic value: nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj + super#visit_ASymbolic (Some current_abs) aproj | V.AProjBorrows (sv, proj_ty), BorrowProj -> (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then @@ -101,16 +103,16 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) (* Apply the projector *) let projected_value = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - proj_regions expansion proj_ty + proj_regions ancestors_regions expansion proj_ty in (* Replace *) projected_value.V.value else (* Not the searched symbolic value: nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj + super#visit_ASymbolic (Some current_abs) aproj | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj -> (* Nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj + super#visit_ASymbolic (Some current_abs) aproj end in (* Apply the expansion *) diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 036082eb..cbd07f3e 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -129,8 +129,8 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) *) let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) - (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : - V.typed_avalue = + (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t) + (v : V.typed_value) (ty : T.rty) : V.typed_avalue = (* Sanity check - TODO: move this elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) let ety = Substitute.erase_regions ty in @@ -151,7 +151,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) List.map (fun (fv, fty) -> apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions fv fty) + regions ancestors_regions fv fty) fields_types in V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } @@ -169,7 +169,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions bv ref_ty + regions ancestors_regions bv ref_ty in V.AMutBorrow (bid, bv) | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid @@ -183,13 +183,19 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (* Not in the set: ignore *) let bc = match (bc, kind) with - | V.MutBorrow (_bid, bv), T.Mut -> + | V.MutBorrow (bid, bv), T.Mut -> (* Apply the projection on the borrowed value *) let bv = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions bv ref_ty + regions ancestors_regions bv ref_ty in - V.AIgnoredMutBorrow bv + (* If the borrow id is in the ancestor's regions, we still need + * to remember it *) + let opt_bid = + if region_in_set r ancestors_regions then Some bid else None + in + (* Return *) + V.AIgnoredMutBorrow (opt_bid, bv) | V.SharedBorrow bid, T.Shared -> (* Lookup the shared value *) let ek = ek_all in @@ -493,8 +499,8 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool) : (fresh_reborrow, apply_registered_reborrows) let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) - (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : - C.eval_ctx * V.typed_avalue = + (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t) + (v : V.typed_value) (ty : T.rty) : C.eval_ctx * V.typed_avalue = let check_symbolic_no_ended = true in let allow_reborrows = true in (* Prepare the reborrows *) @@ -503,7 +509,8 @@ let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) in (* Apply the projector *) let av = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty + apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions + ancestors_regions v ty in (* Apply the reborrows *) let ctx = apply_registered_reborrows ctx in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 36d11a9e..82f95556 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -815,6 +815,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) arg.V.ty = Subst.erase_regions rty) args_with_rtypes); (* Create the abstractions from the region groups and add them to the context *) + let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref = + ref V.AbstractionId.Map.empty + in let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = let abs_id = rg.A.id in let parents = @@ -827,17 +830,27 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (fun s rid -> T.RegionId.Set.add rid s) T.RegionId.Set.empty rg.A.regions in + let ancestors_regions = + List.fold_left + (fun acc parent_id -> + T.RegionId.Set.union acc + (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) + regions rg.A.parents + in + abs_to_ancestors_regions := + V.AbstractionId.Map.add abs_id ancestors_regions !abs_to_ancestors_regions; (* Project over the input values *) let ctx, args_projs = List.fold_left_map (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config ctx regions arg arg_rty) + apply_proj_borrows_on_input_value config ctx regions ancestors_regions + arg arg_rty) ctx args_with_rtypes in (* Group the input and output values *) let avalues = List.append args_projs [ ret_av ] in (* Create the abstraction *) - let abs = { V.abs_id; parents; regions; avalues } in + let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in (* Insert the abstraction in the context *) let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) diff --git a/src/Invariants.ml b/src/Invariants.ml index 3c5d24e3..be5f3ed3 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -253,7 +253,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match bc with | V.AMutBorrow (bid, _) -> register_borrow Mut bid | V.ASharedBorrow bid -> register_borrow Shared bid - | V.AIgnoredMutBorrow _ | V.AProjSharedBorrow _ -> + | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ + | V.AProjSharedBorrow _ -> (* Do nothing *) () in @@ -347,7 +348,8 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = match bc with | V.AMutBorrow (_, _) -> set_outer_mut info | V.ASharedBorrow _ -> set_outer_shared info - | V.AIgnoredMutBorrow _ -> set_outer_mut info + | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> + set_outer_mut info | V.AProjSharedBorrow _ -> set_outer_shared info in (* Continue exploring *) @@ -526,7 +528,12 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | Abstract (V.ASharedLoan (_, sv, _)) -> assert (sv.V.ty = Subst.erase_regions ref_ty) | _ -> failwith "Inconsistent context") - | V.AIgnoredMutBorrow av, T.Mut -> assert (av.V.ty = ref_ty) + | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut -> + assert (av.V.ty = ref_ty) + | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child }, T.Mut + -> + assert (given_back_loans_proj.V.ty = ref_ty); + assert (child.V.ty = ref_ty) | V.AProjSharedBorrow _, T.Shared -> () | _ -> failwith "Inconsistent context") | V.ALoan lc, aty -> ( diff --git a/src/Print.ml b/src/Print.ml index ce31338d..5ae722b9 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -7,6 +7,9 @@ module A = CfimAst module C = Contexts module M = Modules +let option_to_string (to_string : 'a -> string) (x : 'a option) : string = + match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None" + (** Pretty-printing for types *) module Types = struct let type_var_to_string (tv : T.type_var) : string = tv.name @@ -406,8 +409,18 @@ module Values = struct ^ typed_avalue_to_string fmt av ^ ")" | ASharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋" - | AIgnoredMutBorrow av -> - "@ignored_mut_borrow(" ^ typed_avalue_to_string fmt av ^ ")" + | AIgnoredMutBorrow (opt_bid, av) -> + "@ignored_mut_borrow(" + ^ option_to_string V.BorrowId.to_string opt_bid + ^ ", " + ^ typed_avalue_to_string fmt av + ^ ")" + | AEndedIgnoredMutBorrow { given_back_loans_proj; child } -> + "@ended_ignored_mut_borrow{ given_back_loans_proj=" + ^ typed_avalue_to_string fmt given_back_loans_proj + ^ "; child=" + ^ typed_avalue_to_string fmt child + ^ ")" | AProjSharedBorrow sb -> "@ignored_shared_borrow(" ^ abstract_shared_borrows_to_string fmt sb diff --git a/src/Values.ml b/src/Values.ml index b6bb414b..c9dff56a 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -195,6 +195,8 @@ class ['self] iter_typed_avalue_base = object (_self : 'self) inherit [_] iter_typed_value + method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> () + method visit_region : 'env -> region -> unit = fun _ _ -> () method visit_aproj : 'env -> aproj -> unit = fun _ _ -> () @@ -211,6 +213,8 @@ class ['self] map_typed_avalue_base = object (_self : 'self) inherit [_] map_typed_value + method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id + method visit_region : 'env -> region -> region = fun _ r -> r method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p @@ -421,11 +425,15 @@ and aborrow_content = > abs0 { a_shared_bororw l0 } ``` *) - | AIgnoredMutBorrow of typed_avalue + | AIgnoredMutBorrow of BorrowId.id option * typed_avalue (** An ignored mutable borrow. - - This is mostly useful for typing concerns: when a borrow doesn't - belong to an abstraction, it would be weird to ignore it altogether. + + We need to keep track of ignored mut borrows because when ending such + borrows, we need to project the loans of the given back value to + insert them in the proper abstractions. + + Note that we need to do so only for borrows consumed by parent + abstractions (hence the optional borrow id). Example: ======== @@ -441,8 +449,29 @@ and aborrow_content = > x -> mut_loan l0 > px -> mut_loan l1 > ppx -> ⊥ - > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow (U32 0)) } // TODO: duplication - > abs'b { a_ignored_mut_borrow (a_mut_borrow l0 (U32 0)) } + > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication + > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) } + + ... // abs'a ends + + > x -> mut_loan l0 + > px -> @s0 + > ppx -> ⊥ + > abs'b { + > a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector + > (a_mut_borrow l0 (U32 0)) + > } + + ... // `@s0` gets expanded to `&mut l2 @s1` + + > x -> mut_loan l0 + > px -> &mut l2 @s1 + > ppx -> ⊥ + > abs'b { + > a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here + > (a_mut_borrow l0 (U32 0)) + > } + ``` TODO: this is annoying, we are duplicating information. Maybe we could introduce an "Ignored" value? We have to pay attention to @@ -460,6 +489,10 @@ and aborrow_content = abstraction so that we can properly call the backward functions when generating the pure translation. *) + | AEndedIgnoredMutBorrow of { + given_back_loans_proj : typed_avalue; + child : typed_avalue; + } (** See the explanations for [AIgnoredMutBorrow] *) | AProjSharedBorrow of abstract_shared_borrows (** A projected shared borrow. @@ -522,6 +555,8 @@ type abs = { abs_id : (AbstractionId.id[@opaque]); parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *) regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *) + ancestors_regions : (RegionId.set_t[@opaque]); + (** Union of the regions owned by this abstraction and its ancestors *) avalues : typed_avalue list; (** The values in this abstraction *) } [@@deriving -- cgit v1.2.3 From 2ee5357216cc5a620dbe6d091b0081d419951a4e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 13:55:16 +0100 Subject: Make more modifications to logging --- src/Interpreter.ml | 7 +++++-- src/InterpreterBorrows.ml | 2 +- src/InterpreterPaths.ml | 11 +++++++---- src/InterpreterStatements.ml | 15 +++++++++------ src/Logging.ml | 12 ++++++++---- src/main.ml | 7 +++++-- 6 files changed, 35 insertions(+), 19 deletions(-) (limited to 'src') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 9ac8149b..b938fe90 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -21,6 +21,9 @@ open InterpreterStatements (* TODO: remove the config parameters when they are useless *) +(** The local logger *) +let log = L.interpreter_log + module Test = struct let initialize_context (type_context : C.type_context) (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx = @@ -126,7 +129,7 @@ module Test = struct let fdef = A.FunDefId.nth fun_defs fid in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name)); (* Sanity check - *) @@ -177,7 +180,7 @@ module Test = struct let fdef = A.FunDefId.nth fun_defs fid in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name)); diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index b52454b1..c651e2f1 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1130,7 +1130,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) | None -> (* No loan to end inside the value *) (* Some sanity checks *) - L.log#ldebug + log#ldebug (lazy ("activate_inactivated_mut_borrow: resulting value:\n" ^ V.show_typed_value sv)); diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 07c615a0..491e4c21 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -12,6 +12,9 @@ open InterpreterBorrowsCore open InterpreterBorrows open InterpreterExpansion +(** The local logger *) +let log = L.paths_log + (** Paths *) (** When we fail reading from or writing to a path, it might be because we @@ -76,7 +79,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) let nv = update v in (* Type checking *) if nv.ty <> v.ty then ( - L.log#lerror + log#lerror (lazy ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: " ^ T.show_ety v.ty)); @@ -244,7 +247,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) let pe = "- pe: " ^ E.show_projection_elem pe in let v = "- v:\n" ^ V.show_value v in let ty = "- ty:\n" ^ T.show_ety ty in - L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); + log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); failwith "Inconsistent projection") (** Generic function to access (read/write) the value at a given place. @@ -314,7 +317,7 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) ^ C.show_env ctx1.env ^ "\n\nOld environment:\n" ^ C.show_env ctx.env in - L.log#serror msg; + log#serror msg; failwith "Unexpected environment update"); Ok read_value @@ -402,7 +405,7 @@ let expand_bottom_value_from_projection (config : C.config) (access : access_kind) (p : E.place) (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx = (* Debugging *) - L.log#ldebug + log#ldebug (lazy ("expand_bottom_value_from_projection:\n" ^ "pe: " ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty)); diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 82f95556..03940bb7 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -15,13 +15,16 @@ open InterpreterExpansion open InterpreterPaths open InterpreterExpressions +(** The local logger *) +let log = L.statements_log + (** Result of evaluating a statement *) type statement_eval_res = Unit | Break of int | Continue of int | Return (** Drop a value at a given place *) let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx = - L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); + log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); (* Prepare the place (by ending the loans, then the borrows) *) let ctx, v = prepare_lplace config p ctx in (* Replace the value with [Bottom] *) @@ -167,7 +170,7 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id) let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = (* Debug *) - L.log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx)); + log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx)); (* Eval *) let ret_vid = V.VarId.zero in (* List the local variables, but the return variable *) @@ -182,7 +185,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : in let locals = list_locals ctx.env in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("ctx_pop_frame: locals to drop: [" ^ String.concat "," (List.map V.VarId.to_string locals) @@ -194,7 +197,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : ctx locals in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("ctx_pop_frame: after dropping local variables:\n" ^ eval_ctx_to_string ctx)); @@ -514,7 +517,7 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) : (C.eval_ctx * statement_eval_res) eval_result list = (* Debugging *) - L.log#ldebug + log#ldebug (lazy ("\n**About to evaluate statement**: [\n" ^ statement_to_string_with_tab ctx st @@ -909,7 +912,7 @@ and eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : C.eval_ctx eval_result = (* Debug *) - L.log#ldebug + log#ldebug (lazy (let type_params = "[" diff --git a/src/Logging.ml b/src/Logging.ml index 2759854c..36ede236 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -4,7 +4,7 @@ module L = Easy_logging.Logging let _ = L.make_logger "MainLogger" Debug [ Cli Debug ] (** The main logger *) -let log = L.get_logger "MainLogger" +let main_log = L.get_logger "MainLogger" (** Below, we create subgloggers for various submodules, so that we can precisely toggle logging on/off, depending on which information we need *) @@ -18,6 +18,9 @@ let statements_log = L.get_logger "MainLogger.Interpreter.Statements" (** Logger for InterpreterExpressions *) let expressions_log = L.get_logger "MainLogger.Interpreter.Expressions" +(** Logger for InterpreterPaths *) +let paths_log = L.get_logger "MainLogger.Interpreter.Paths" + (** Logger for InterpreterExpansion *) let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion" @@ -131,7 +134,7 @@ let format_tags (tags : string list) = "[" ^ elems_str ^ "] " (* Change the formatters *) -let _ = +let main_logger_handler = (* TODO: comes from easy_logging *) let formatter (item : L.log_item) : string = let item_level_fmt = @@ -147,5 +150,6 @@ let _ = item_msg_fmt in (* There should be exactly one handler *) - let handlers = log#get_handlers in - List.map (fun h -> H.set_formatter h formatter) handlers + let handlers = main_log#get_handlers in + List.iter (fun h -> H.set_formatter h formatter) handlers; + match handlers with [ handler ] -> handler | _ -> failwith "Unexpected" diff --git a/src/main.ml b/src/main.ml index da1b333e..da0b4a0a 100644 --- a/src/main.ml +++ b/src/main.ml @@ -42,6 +42,9 @@ let () = exit 1); (* Set up the logging - for now we use default values - TODO: use the * command-line arguments *) + Easy_logging.Handlers.set_level main_logger_handler EL.Debug; + main_log#set_level EL.Debug; + interpreter_log#set_level EL.Debug; statements_log#set_level EL.Debug; expressions_log#set_level EL.Warning; expansion_log#set_level EL.Debug; @@ -50,10 +53,10 @@ let () = (* Load the module *) let json = Yojson.Basic.from_file !filename in match cfim_module_of_json json with - | Error s -> log#error "error: %s\n" s + | Error s -> main_log#error "error: %s\n" s | Ok m -> (* Print the module *) - log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); + main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); (* Test the unit functions with the concrete interpreter *) I.Test.test_unit_functions m.types m.functions; -- cgit v1.2.3 From 4e2dd5806fe41275bf8c037b9071175e51c88c62 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 13:57:47 +0100 Subject: Add a high-level comment --- src/Values.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src') diff --git a/src/Values.ml b/src/Values.ml index c9dff56a..53851cea 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -473,6 +473,14 @@ and aborrow_content = > } ``` + + Note that we could use AIgnoredMutLoan in the case the borrow id is not + None, which would allow us to simplify the rules (to not have rules + to specifically handle the case of AIgnoredMutBorrow with Some borrow + id) and also remove the AEndedIgnoredMutBorrow variant. + For now, the rules are implemented and it allows us to make the avalues + more precise and clearer, so we will keep it that way. + TODO: this is annoying, we are duplicating information. Maybe we could introduce an "Ignored" value? We have to pay attention to two things: -- cgit v1.2.3 From c16ad7c78a149d3fd62976f4eb17d07a9c03b8c6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 15:04:11 +0100 Subject: Factorize initialize_symbolic_context_for_fun and eval_function_call_symbolic_from_inst_sig and make minor modifications --- src/Interpreter.ml | 37 +++++-------------- src/InterpreterStatements.ml | 87 +++++++++++++++++++++++++++++--------------- src/Values.ml | 3 +- 3 files changed, 69 insertions(+), 58 deletions(-) (limited to 'src') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b938fe90..f38cb66e 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -69,42 +69,23 @@ module Test = struct let input_svs = List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs in - (* Create the abstractions and insert them in the context *) - let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref = - ref V.AbstractionId.Map.empty + (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) + let empty_absl = + create_empty_abstractions_from_abs_region_groups + inst_sg.A.regions_hierarchy in - let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = - let abs_id = rg.A.id in - let parents = - List.fold_left - (fun s pid -> V.AbstractionId.Set.add pid s) - V.AbstractionId.Set.empty rg.A.parents - in - let regions = - List.fold_left - (fun s rid -> T.RegionId.Set.add rid s) - T.RegionId.Set.empty rg.A.regions - in - let ancestors_regions = - List.fold_left - (fun acc parent_id -> - T.RegionId.Set.union acc - (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) - regions rg.A.parents - in - abs_to_ancestors_regions := - V.AbstractionId.Map.add abs_id ancestors_regions - !abs_to_ancestors_regions; + (* Add the avalues to the abstractions and insert them in the context *) + let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = (* Project over the values - we use *loan* projectors, as explained above *) let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in - (* Create the abstraction *) - let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in + (* Insert the avalues in the abstraction *) + let abs = { abs with avalues } in (* Insert the abstraction in the context *) let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) ctx in - let ctx = List.fold_left create_abs ctx inst_sg.regions_hierarchy in + let ctx = List.fold_left insert_abs ctx empty_absl in (* Split the variables between return var, inputs and remaining locals *) let ret_var = List.hd fdef.locals in let input_vars, local_vars = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 03940bb7..917f1265 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -513,6 +513,54 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) (* Return *) (ctx, inst_sig) +(** Helper + + Create abstractions (with no avalues, which have to be inserted afterwards) + from a list of abs region groups. + *) +let create_empty_abstractions_from_abs_region_groups + (rgl : A.abs_region_group list) : V.abs list = + (* We use a reference to progressively create a map from abstraction ids + * to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id] + * returns the union of: + * - the regions of the ancestors of abs_id + * - the regions of abs_id + *) + let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref = + ref V.AbstractionId.Map.empty + in + (* Auxiliary function to create one abstraction *) + let create_abs (rg : A.abs_region_group) : V.abs = + let abs_id = rg.A.id in + let parents = + List.fold_left + (fun s pid -> V.AbstractionId.Set.add pid s) + V.AbstractionId.Set.empty rg.A.parents + in + let regions = + List.fold_left + (fun s rid -> T.RegionId.Set.add rid s) + T.RegionId.Set.empty rg.A.regions + in + let ancestors_regions = + List.fold_left + (fun acc parent_id -> + T.RegionId.Set.union acc + (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) + T.RegionId.Set.empty rg.A.parents + in + let ancestors_regions_union_current_regions = + T.RegionId.Set.union ancestors_regions regions + in + abs_to_ancestors_regions := + V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions + !abs_to_ancestors_regions; + (* Create the abstraction *) + { V.abs_id; parents; regions; ancestors_regions; avalues = [] } + in + (* Apply *) + List.map create_abs rgl + (** Evaluate a statement *) let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) : (C.eval_ctx * statement_eval_res) eval_result list = @@ -817,49 +865,30 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (fun ((arg, rty) : V.typed_value * T.rty) -> arg.V.ty = Subst.erase_regions rty) args_with_rtypes); - (* Create the abstractions from the region groups and add them to the context *) - let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref = - ref V.AbstractionId.Map.empty + (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) + let empty_absl = + create_empty_abstractions_from_abs_region_groups inst_sg.A.regions_hierarchy in - let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = - let abs_id = rg.A.id in - let parents = - List.fold_left - (fun s pid -> V.AbstractionId.Set.add pid s) - V.AbstractionId.Set.empty rg.A.parents - in - let regions = - List.fold_left - (fun s rid -> T.RegionId.Set.add rid s) - T.RegionId.Set.empty rg.A.regions - in - let ancestors_regions = - List.fold_left - (fun acc parent_id -> - T.RegionId.Set.union acc - (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) - regions rg.A.parents - in - abs_to_ancestors_regions := - V.AbstractionId.Map.add abs_id ancestors_regions !abs_to_ancestors_regions; + (* Add the avalues to the abstractions and insert them in the context *) + let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = (* Project over the input values *) let ctx, args_projs = List.fold_left_map (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config ctx regions ancestors_regions - arg arg_rty) + apply_proj_borrows_on_input_value config ctx abs.regions + abs.ancestors_regions arg arg_rty) ctx args_with_rtypes in (* Group the input and output values *) let avalues = List.append args_projs [ ret_av ] in - (* Create the abstraction *) - let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in + (* Add the avalues to the abstraction *) + let abs = { abs with avalues } in (* Insert the abstraction in the context *) let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) ctx in - let ctx = List.fold_left create_abs ctx inst_sg.A.regions_hierarchy in + let ctx = List.fold_left insert_abs ctx empty_absl in (* Move the return value to its destination *) let ctx = assign_to_place config ctx ret_value dest in (* Synthesis *) diff --git a/src/Values.ml b/src/Values.ml index 53851cea..bcb08dc8 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -564,7 +564,8 @@ type abs = { parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *) regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *) ancestors_regions : (RegionId.set_t[@opaque]); - (** Union of the regions owned by this abstraction and its ancestors *) + (** Union of the regions owned by this abstraction's ancestors (not + including the regions of this abstraction itself) *) avalues : typed_avalue list; (** The values in this abstraction *) } [@@deriving -- cgit v1.2.3 From f2dd12e889cca6e75b03868a7d31952c8bdfa9c7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 19:15:08 +0100 Subject: Update the invariant checks to take into account ignored borrows/loans --- src/Invariants.ml | 39 +++++++++++++++++++++++++++++++++------ 1 file changed, 33 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/Invariants.ml b/src/Invariants.ml index be5f3ed3..3fc390b5 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -78,9 +78,18 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = ^ "\n- info:\n" ^ borrows_infos_to_string " " !borrows_infos in + (* Ignored loans - when we find an ignored loan while building the borrows_infos + * map, we register it in this list; once the borrows_infos map is completely + * built, we check that all the borrow ids of the ignored loans are in this + * map *) + let ignored_loans : (T.ref_kind * V.BorrowId.id) list ref = ref [] in (* first, register all the loans *) (* Some utilities to register the loans *) + let register_ignored_loan (rkind : T.ref_kind) (bid : V.BorrowId.id) : unit = + ignored_loans := (rkind, bid) :: !ignored_loans + in + let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.set_t) : unit = let reprs = !ids_reprs in @@ -161,11 +170,11 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match lc with | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids + | V.AIgnoredMutLoan (bid, _) -> register_ignored_loan T.Mut bid + | V.AIgnoredSharedLoan _ | V.AEndedMutLoan { given_back = _; child = _ } | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) (* We might want to do something here *) - | V.AEndedIgnoredMutLoan { given_back = _; child = _ } - | V.AIgnoredSharedLoan _ -> + | V.AEndedIgnoredMutLoan { given_back = _; child = _ } -> (* Do nothing *) () in @@ -208,6 +217,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = borrows_infos := infos in + let register_ignored_borrow = register_ignored_loan in + let register_borrow (kind : borrow_kind) (bid : V.BorrowId.id) : unit = (* Lookup the info *) let info = find_info bid in @@ -253,8 +264,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match bc with | V.AMutBorrow (bid, _) -> register_borrow Mut bid | V.ASharedBorrow bid -> register_borrow Shared bid - | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ - | V.AProjSharedBorrow _ -> + | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid + | V.AIgnoredMutBorrow (None, _) + | V.AEndedIgnoredMutBorrow _ | V.AProjSharedBorrow _ -> (* Do nothing *) () in @@ -271,6 +283,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (lazy ("\nAbout to check context invariant:\n" ^ context_to_string ())); (* Finally, check that everything is consistant *) + (* First, check all the ignored loans are present at the proper place *) + List.iter + (fun (rkind, bid) -> + let info = find_info bid in + assert (info.loan_kind = rkind)) + !ignored_loans; + + (* Then, check the borrow infos *) V.BorrowId.Map.iter (fun _ info -> (* Note that we can't directly compare the sets - I guess they are @@ -466,6 +486,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv + (* TODO: there is a lot of duplication with [visit_typed_value] + * which is quite annoying. There might be a way of factorizing + * that by factorizing the definitions of value and avalue, but + * the generation of visitors then doesn't work properly (TODO: + * report that). Still, it is actually not that problematic + * because this code shouldn't change a lot in the future, + * so the cost of maintenance should be pretty low. + * *) method! visit_typed_avalue info atv = (* Check the current pair (value, type) *) (match (atv.V.value, atv.V.ty) with @@ -576,7 +604,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> failwith "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv - (** TODO: there is a lot of duplication with [visit_typed_value]... *) end in visitor#visit_eval_ctx () ctx -- cgit v1.2.3