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(-) 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