summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/InterpreterExpansion.ml13
-rw-r--r--src/InterpreterExpressions.ml48
-rw-r--r--src/InterpreterUtils.ml21
-rw-r--r--src/Logging.ml13
-rw-r--r--src/Print.ml8
-rw-r--r--src/main.ml8
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:13:39 +0000