Improve logging and introduce eval_operands_prepare

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