summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml33
-rw-r--r--src/InterpreterBorrows.ml131
-rw-r--r--src/InterpreterBorrowsCore.ml16
-rw-r--r--src/InterpreterExpansion.ml35
-rw-r--r--src/InterpreterExpressions.ml48
-rw-r--r--src/InterpreterPaths.ml11
-rw-r--r--src/InterpreterProjectors.ml27
-rw-r--r--src/InterpreterStatements.ml91
-rw-r--r--src/InterpreterUtils.ml21
-rw-r--r--src/Invariants.ml92
-rw-r--r--src/Logging.ml34
-rw-r--r--src/Print.ml25
-rw-r--r--src/Values.ml56
-rw-r--r--src/main.ml17
14 files changed, 495 insertions, 142 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2789517e..f38cb66e 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 =
@@ -66,29 +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 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
+ (* 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
+ (* 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; 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 =
@@ -113,7 +110,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 - *)
@@ -164,7 +161,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 1dd4d247..c651e2f1 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].
@@ -743,12 +813,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 +850,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 =
@@ -862,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
@@ -891,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 *)
@@ -905,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
@@ -1031,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/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index bc2f5971..b590eff6 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... *)
@@ -302,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))
@@ -415,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 345c3df3..e19f8bb4 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
@@ -60,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 *)
@@ -82,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
@@ -98,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 *)
@@ -366,6 +371,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 +431,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/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/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..917f1265 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));
@@ -510,11 +513,59 @@ 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 =
(* Debugging *)
- L.log#ldebug
+ log#ldebug
(lazy
("\n**About to evaluate statement**: [\n"
^ statement_to_string_with_tab ctx st
@@ -814,36 +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 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
+ (* 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
+ (* 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 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; 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 *)
@@ -896,7 +941,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/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 1f8e47e0..6c5d3289 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -10,28 +10,29 @@ module L = Logging
open ValuesUtils
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/Invariants.ml b/src/Invariants.ml
index e214e820..3fc390b5 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;
@@ -35,20 +36,24 @@ 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 *)
-let ids_reprs_to_string (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
+(* 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
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,9 +72,24 @@ 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
+ (* 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 *)
+ (* 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
@@ -150,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
@@ -178,13 +198,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
@@ -201,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
@@ -246,7 +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.AProjSharedBorrow _ ->
+ | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
+ | V.AIgnoredMutBorrow (None, _)
+ | V.AEndedIgnoredMutBorrow _ | V.AProjSharedBorrow _ ->
(* Do nothing *)
()
in
@@ -259,17 +279,18 @@ 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 *)
+ (* 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
@@ -347,7 +368,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 *)
@@ -464,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
@@ -526,7 +556,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 -> (
@@ -569,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
diff --git a/src/Logging.ml b/src/Logging.ml
index a1060014..36ede236 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -3,7 +3,32 @@ module L = Easy_logging.Logging
let _ = L.make_logger "MainLogger" Debug [ Cli Debug ]
-let log = L.get_logger "MainLogger"
+(** The main logger *)
+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 *)
+
+(** Logger for Interpreter *)
+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 InterpreterPaths *)
+let paths_log = L.get_logger "MainLogger.Interpreter.Paths"
+
+(** Logger for InterpreterExpansion *)
+let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion"
+
+(** Logger for InterpreterBorrows *)
+let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
+
+(** 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 =
@@ -109,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 =
@@ -125,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/Print.ml b/src/Print.ml
index f714e847..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
@@ -390,7 +393,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
@@ -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
@@ -973,6 +986,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/Values.ml b/src/Values.ml
index b6bb414b..bcb08dc8 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,9 +449,38 @@ 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))
+ > }
+
```
+
+ 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:
@@ -460,6 +497,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 +563,9 @@ 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's ancestors (not
+ including the regions of this abstraction itself) *)
avalues : typed_avalue list; (** The values in this abstraction *)
}
[@@deriving
diff --git a/src/main.ml b/src/main.ml
index ac49b782..d8e9aa40 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.
@@ -19,6 +20,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
@@ -39,12 +41,23 @@ 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 *)
+ 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;
+ borrows_log#set_level EL.Debug;
+ invariants_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
+ | 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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 22:57:29 +0000