summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--TODO.md4
-rw-r--r--src/Identifiers.ml39
-rw-r--r--src/InterpreterBorrows.ml2
-rw-r--r--src/InterpreterExpansion.ml31
-rw-r--r--src/InterpreterExpressions.ml72
-rw-r--r--src/InterpreterPaths.ml15
-rw-r--r--src/InterpreterProjectors.ml4
-rw-r--r--src/InterpreterStatements.ml7
-rw-r--r--src/InterpreterUtils.ml3
-rw-r--r--src/Invariants.ml119
-rw-r--r--src/Print.ml19
-rw-r--r--src/Types.ml5
-rw-r--r--src/TypesUtils.ml9
-rw-r--r--src/ValuesUtils.ml29
-rw-r--r--src/main.ml3
15 files changed, 263 insertions, 98 deletions
diff --git a/TODO.md b/TODO.md
index 471d230f..6c8054b3 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,5 +1,7 @@
# TODO
+0. TODO: recheck give_back_symbolic_value (use regions!)
+
1. expand symbolic values which are primitively copyable upon using them as
function arguments or putting them in the return value, in order to deduplicate
those values.
@@ -18,6 +20,8 @@
6. update the printing of mut_borrows and mut_loans ([s@0 <: ...]) and (s@0)
+7. fix the static regions (with projectors)
+
* write an interesting example to study with Jonathan
* add option for: `allow_borrow_overwrites_on_input_values`
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index c6d7ea10..56edc238 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -66,11 +66,21 @@ module type Id = sig
module Set : Set.S with type elt = id with type t = set_t
- val set_to_string : Set.t -> string
+ val set_to_string : string option -> Set.t -> string
+ (** Convert a set to a string.
+
+ Takes an indentation as parameter, in case you want to insert a breakline
+ for every binding.
+ *)
module Map : Map.S with type key = id with type 'a t = 'a map_t
- (* TODO: map_to_string *)
+ val map_to_string : string option -> ('a -> string) -> 'a map_t -> string
+ (** Convert a map to a string.
+
+ Takes an indentation as parameter, in case you want to insert a breakline
+ for every binding.
+ *)
val id_of_json : Yojson.Basic.t -> (id, string) result
end
@@ -173,9 +183,28 @@ module IdGen () : Id = struct
m;
pp_string "}"
- let set_to_string ids =
- let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in
- "{" ^ String.concat ", " (List.rev ids) ^ "}"
+ let set_to_string indent_opt ids =
+ let indent, sep =
+ match indent_opt with Some indent -> (indent, ",\n") | None -> ("", ",")
+ in
+ let ids = Set.fold (fun id ids -> (indent ^ to_string id) :: ids) ids [] in
+ match ids with
+ | [] -> "{}"
+ | _ -> "{\n" ^ String.concat sep (List.rev ids) ^ "\n}"
+
+ let map_to_string indent_opt a_to_string ids =
+ let indent, sep =
+ match indent_opt with Some indent -> (indent, ",\n") | None -> ("", ",")
+ in
+ let ids =
+ Map.fold
+ (fun id v ids ->
+ (indent ^ to_string id ^ " -> " ^ a_to_string v) :: ids)
+ ids []
+ in
+ match ids with
+ | [] -> "{}"
+ | _ -> "{\n" ^ String.concat sep (List.rev ids) ^ "\n}"
let id_of_json js =
(* TODO: check boundaries ? *)
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index d17991ea..19e5716f 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -439,6 +439,8 @@ let give_back_symbolic_value (_config : C.config) (sv : V.symbolic_value)
in
V.AEndedProjLoans child_proj
in
+ (* TODO: we need to use the regions!! *)
+ raise Errors.Unimplemented;
substitute_aproj_loans_with_id sv subst ctx
(** Auxiliary function to end borrows. See [give_back].
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 4f0ac11c..8f560083 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -12,6 +12,7 @@ module L = Logging
open TypesUtils
module Inv = Invariants
module S = Synthesis
+open ValuesUtils
open InterpreterUtils
open InterpreterProjectors
open InterpreterBorrows
@@ -482,36 +483,6 @@ let expand_symbolic_value_no_branching (config : C.config)
(* Return *)
ctx
-(** Expand a symbolic value which is not an enumeration with several variants
- (i.e., in a situation where it doesn't lead to branching).
-
- This function is used when exploring paths. It simply performs a few
- sanity checks before calling [expand_symbolic_value_no_branching].
- *)
-let expand_symbolic_value_no_branching_from_projection_elem (config : C.config)
- (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) :
- C.eval_ctx =
- (* Sanity checks *)
- let rty = sp.V.sv_ty in
- let _ =
- match (pe, rty) with
- (* "Regular" ADTs *)
- | Field (ProjAdt (def_id, _), _), T.Adt (T.AdtId def_id', _, _) ->
- assert (def_id = def_id')
- (* Tuples *)
- | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
- assert (arity = List.length tys)
- (* Boxes *)
- | DerefBox, T.Adt (T.Assumed T.Box, [], [ _ ]) -> ()
- (* Borrows *)
- | Deref, T.Ref (_, _, _) -> ()
- | _ ->
- failwith
- ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
- in
- (* Perform the expansion *)
- expand_symbolic_value_no_branching config sp ctx
-
(** Expand a symbolic enumeration value.
This might lead to branching.
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 93ec8640..f577a190 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -22,11 +22,43 @@ type eval_error = Panic
type 'a eval_result = ('a, eval_error) result
-(** Small utility *)
-let prepare_rplace (config : C.config) (access : access_kind) (p : E.place)
- (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+(** As long as there are symbolic values at a given place (potentially in subalues)
+ which contain borrows and are primitively copyable, expand them.
+
+ We use this function before copying values.
+
+ Note that the place should have been prepared so that there are no remaining
+ loans.
+*)
+let expand_primitively_copyable_at_place (config : C.config)
+ (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
+ (* Small helper *)
+ let rec expand ctx =
+ let v = read_place_unwrap config access p ctx in
+ match find_first_primitively_copyable_sv v with
+ | None -> ctx
+ | Some sv ->
+ let ctx = expand_symbolic_value_no_branching config sv ctx in
+ expand ctx
+ in
+ (* Apply *)
+ expand ctx
+
+(** Small utility.
+
+ [expand_prim_copy]: if true, expand the symbolic values which are primitively
+ copyable and contain borrows.
+ *)
+let prepare_rplace (config : C.config) (expand_prim_copy : bool)
+ (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
+ C.eval_ctx * V.typed_value =
let ctx = update_ctx_along_read_place config access p ctx in
let ctx = end_loans_at_place config access p ctx in
+ let ctx =
+ if expand_prim_copy then
+ expand_primitively_copyable_at_place config access p ctx
+ else ctx
+ in
let v = read_place_unwrap config access p ctx in
(ctx, v)
@@ -114,13 +146,14 @@ let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
| Expressions.Copy p ->
(* Access the value *)
let access = Read in
- (* TODO: expand the value if it is a symbolic value *)
- raise Unimplemented;
- prepare_rplace config access p ctx
+ (* Expand the symbolic values, if necessary *)
+ let expand_prim_copy = true in
+ prepare_rplace config expand_prim_copy access p ctx
| Expressions.Move p ->
(* Access the value *)
let access = Move in
- prepare_rplace config access p ctx
+ let expand_prim_copy = false in
+ prepare_rplace config expand_prim_copy access p ctx
in
assert (not (bottom_in_value ctx.ended_regions v));
(ctx, v)
@@ -131,8 +164,8 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
(* Debug *)
log#ldebug
(lazy
- ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n"
- ^ operand_to_string ctx op ^ "\n"));
+ ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n"
+ ^ eval_ctx_to_string ctx ^ "\n"));
(* Evaluate *)
match op with
| Expressions.Constant (ty, cv) ->
@@ -141,17 +174,18 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
| Expressions.Copy p ->
(* Access the value *)
let access = Read in
- (* TODO: expand the value if it is a symbolic value *)
- raise Unimplemented;
- let ctx, v = prepare_rplace config access p ctx in
+ let expand_prim_copy = true in
+ let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
(* Copy the value *)
assert (not (bottom_in_value ctx.ended_regions v));
+ assert (Option.is_none (find_first_primitively_copyable_sv v));
let allow_adt_copy = false in
copy_value allow_adt_copy config ctx v
| Expressions.Move p -> (
(* Access the value *)
let access = Move in
- let ctx, v = prepare_rplace config access p ctx in
+ let expand_prim_copy = false in
+ let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
(* Move the value *)
assert (not (bottom_in_value ctx.ended_regions v));
let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
@@ -345,7 +379,8 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
(* Note that discriminant values have type `isize` *)
(* Access the value *)
let access = Read in
- let ctx, v = prepare_rplace config access p ctx in
+ let expand_prim_copy = false in
+ let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
match v.V.value with
| Adt av -> (
match av.variant_id with
@@ -368,7 +403,8 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
(* Note that discriminant values have type `isize` *)
(* Access the value *)
let access = Read in
- let ctx, v = prepare_rplace config access p ctx in
+ let expand_prim_copy = false in
+ let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
match v.V.value with
| Adt _ -> [ eval_rvalue_discriminant_concrete config p ctx ]
| Symbolic sv ->
@@ -385,7 +421,8 @@ let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
| E.Shared | E.TwoPhaseMut ->
(* Access the value *)
let access = if bkind = E.Shared then Read else Write in
- let ctx, v = prepare_rplace config access p ctx in
+ let expand_prim_copy = false in
+ let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
(* Compute the rvalue - simply a shared borrow with a fresh id *)
let bid = C.fresh_borrow_id () in
(* Note that the reference is *mutable* if we do a two-phase borrow *)
@@ -416,7 +453,8 @@ let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
| E.Mut ->
(* Access the value *)
let access = Write in
- let ctx, v = prepare_rplace config access p ctx in
+ let expand_prim_copy = false in
+ let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
(* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
let bid = C.fresh_borrow_id () in
let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 6bc22af4..8cf2b747 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -467,10 +467,9 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
| FailMutLoan bid -> end_outer_borrow config bid ctx
| FailInactivatedMutBorrow bid ->
activate_inactivated_mut_borrow config bid ctx
- | FailSymbolic (pe, sp) ->
+ | FailSymbolic (_pe, sp) ->
(* Expand the symbolic value *)
- expand_symbolic_value_no_branching_from_projection_elem config pe sp
- ctx
+ expand_symbolic_value_no_branching config sp ctx
| FailBottom (_, _, _) ->
(* We can't expand [Bottom] values while reading them *)
failwith "Found [Bottom] while reading a place"
@@ -495,10 +494,9 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
| FailMutLoan bid -> end_outer_borrow config bid ctx
| FailInactivatedMutBorrow bid ->
activate_inactivated_mut_borrow config bid ctx
- | FailSymbolic (pe, sp) ->
+ | FailSymbolic (_pe, sp) ->
(* Expand the symbolic value *)
- expand_symbolic_value_no_branching_from_projection_elem config pe sp
- ctx
+ expand_symbolic_value_no_branching config sp ctx
| FailBottom (remaining_pes, pe, ty) ->
(* Expand the [Bottom] value *)
expand_bottom_value_from_projection config access p remaining_pes pe
@@ -669,6 +667,11 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
*)
let rec copy_value (allow_adt_copy : bool) (config : C.config)
(ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =
+ log#ldebug
+ (lazy
+ ("copy_value: "
+ ^ typed_value_to_string ctx v
+ ^ "\n- context:\n" ^ eval_ctx_to_string ctx));
(* Remark: at some point we rewrote this function to use iterators, but then
* we reverted the changes: the result was less clear actually. In particular,
* the fact that we have exhaustive matches below makes very obvious the cases
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index b1c61980..d2d10670 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -235,9 +235,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
(lazy
("projections_intersect:" ^ "\n- ty1: " ^ rty_to_string ctx ty1
^ "\n- rset1: "
- ^ T.RegionId.set_to_string rset1
+ ^ T.RegionId.set_to_string None rset1
^ "\n- ty2: " ^ rty_to_string ctx ty2 ^ "\n- rset2: "
- ^ T.RegionId.set_to_string rset2
+ ^ T.RegionId.set_to_string None rset2
^ "\n"));
assert (not (projections_intersect ty1 rset1 ty2 rset2)));
V.ASymbolic (V.AProjBorrows (s, ty))
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 8768461c..885d1bdc 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -602,7 +602,7 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
* checking the invariants *)
let ctx = greedy_expand_symbolic_values config ctx in
(* Sanity check *)
- if config.C.check_invariants then Inv.check_invariants ctx;
+ if config.C.check_invariants then Inv.check_invariants config ctx;
(* Evaluate *)
match st with
| A.Assign (p, rvalue) -> (
@@ -617,7 +617,8 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
in
List.map assign res)
| A.FakeRead p ->
- let ctx, _ = prepare_rplace config Read p ctx in
+ let expand_prim_copy = false in
+ let ctx, _ = prepare_rplace config expand_prim_copy Read p ctx in
[ Ok (ctx, Unit) ]
| A.SetDiscriminant (p, variant_id) ->
[ Ok (set_discriminant config ctx p variant_id) ]
@@ -1028,7 +1029,7 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx)
* checking the invariants *)
let ctx = greedy_expand_symbolic_values config ctx in
(* Sanity check *)
- if config.C.check_invariants then Inv.check_invariants ctx;
+ if config.C.check_invariants then Inv.check_invariants config ctx;
match res with
| Unit | Break _ | Continue _ -> failwith "Inconsistent state"
| Return -> Ok ctx)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index b76ae28c..fc86f1f5 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -151,9 +151,6 @@ exception FoundGBorrowContent of g_borrow_content
exception FoundGLoanContent of g_loan_content
(** Utility exception *)
-exception FoundSymbolicValue of V.symbolic_value
-(** Utility exception *)
-
exception FoundAProjBorrows of V.symbolic_value * T.rty
(** Utility exception *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 5009410e..ba069bc4 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -39,22 +39,11 @@ let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info =
(* 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) ->
- indent ^ V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id)
- bindings
- in
- String.concat "\n" bindings
+ V.BorrowId.map_to_string (Some indent) V.BorrowId.to_string reprs
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) -> indent ^ show_borrow_info info) bindings
- in
- String.concat "\n" bindings
+ V.BorrowId.map_to_string (Some indent) show_borrow_info infos
type borrow_kind = Mut | Shared | Inactivated
@@ -621,16 +610,110 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
in
visitor#visit_eval_ctx (None : V.abs option) ctx
-(** TODO:
+type proj_borrows_info = {
+ abs_id : V.AbstractionId.id;
+ regions : T.RegionId.set_t;
+ proj_ty : T.rty;
+ as_shared_value : bool; (** True if the value is below a shared borrow *)
+}
+[@@deriving show]
+
+type proj_loans_info = {
+ abs_id : V.AbstractionId.id;
+ regions : T.RegionId.set_t;
+}
+[@@deriving show]
+
+type sv_info = {
+ ty : T.rty;
+ env_count : int;
+ aproj_borrows : proj_borrows_info list;
+ aproj_loans : proj_loans_info list;
+}
+[@@deriving show]
+
+(** Check the invariants over the symbolic values.
- a symbolic value can't be both in proj_borrows and in the concrete env
(this is why we preemptively expand copyable symbolic values)
-
+ - if a symbolic value contains regions: there is at most one occurrence
+ of this value in the concrete env
*)
-let check_symbolic_values (ctx : C.eval_ctx) : unit = raise Errors.Unimplemented
+let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
+ (* Small utility *)
+ let module M = V.SymbolicValueId.Map in
+ let infos : sv_info M.t ref = ref M.empty in
+ let lookup_info (sv : V.symbolic_value) : sv_info =
+ match M.find_opt sv.V.sv_id !infos with
+ | Some info -> info
+ | None ->
+ { ty = sv.sv_ty; env_count = 0; aproj_borrows = []; aproj_loans = [] }
+ in
+ let update_info (sv : V.symbolic_value) (info : sv_info) =
+ infos := M.add sv.sv_id info !infos
+ in
+ let add_env_sv (sv : V.symbolic_value) : unit =
+ let info = lookup_info sv in
+ let info = { info with env_count = info.env_count + 1 } in
+ update_info sv info
+ in
+ let add_aproj_borrows (sv : V.symbolic_value) abs_id regions proj_ty
+ as_shared_value : unit =
+ let info = lookup_info sv in
+ let binfo = { abs_id; regions; proj_ty; as_shared_value } in
+ let info = { info with aproj_borrows = binfo :: info.aproj_borrows } in
+ update_info sv info
+ in
+ let add_aproj_loans (sv : V.symbolic_value) abs_id regions : unit =
+ let info = lookup_info sv in
+ let linfo = { abs_id; regions } in
+ let info = { info with aproj_loans = linfo :: info.aproj_loans } in
+ update_info sv info
+ in
+ (* Visitor *)
+ let obj =
+ object
+ inherit [_] C.iter_eval_ctx as super
+
+ method! visit_abs _ abs = super#visit_abs (Some abs) abs
+
+ method! visit_Symbolic _ sv = add_env_sv sv
+
+ method! visit_abstract_shared_borrows abs asb =
+ let abs = Option.get abs in
+ let visit asb =
+ match asb with
+ | V.AsbBorrow _ -> ()
+ | AsbProjReborrows (sv, proj_ty) ->
+ add_aproj_borrows sv abs.abs_id abs.regions proj_ty true
+ in
+ List.iter visit asb
+
+ method! visit_aproj abs aproj =
+ (let abs = Option.get abs in
+ match aproj with
+ | AProjLoans sv -> add_aproj_loans sv abs.abs_id abs.regions
+ | AProjBorrows (sv, proj_ty) ->
+ add_aproj_borrows sv abs.abs_id abs.regions proj_ty false
+ | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ());
+ super#visit_aproj abs aproj
+ end
+ in
+ (* Collect the information *)
+ obj#visit_eval_ctx None ctx;
+ log#ldebug
+ (lazy
+ ("check_symbolic_values: collected information:\n"
+ ^ V.SymbolicValueId.map_to_string (Some " ") show_sv_info !infos));
+ (* Check *)
+ let check_info _id info =
+ assert (info.env_count = 0 || info.aproj_borrows = []);
+ if ty_has_regions info.ty then assert (info.env_count <= 1)
+ in
+ M.iter check_info !infos
-let check_invariants (ctx : C.eval_ctx) : unit =
+let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit =
check_loans_borrows_relation_invariant ctx;
check_borrowed_values_invariant ctx;
check_typing_invariant ctx;
- check_symbolic_values ctx
+ check_symbolic_values config ctx
diff --git a/src/Print.ml b/src/Print.ml
index 1eab6714..2b681ec8 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -290,7 +290,7 @@ module Values = struct
string =
match lc with
| SharedLoan (loans, v) ->
- let loans = V.BorrowId.set_to_string loans in
+ let loans = V.BorrowId.set_to_string None loans in
"@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")"
| MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋"
@@ -377,7 +377,7 @@ module Values = struct
^ typed_avalue_to_string fmt av
^ "⌋"
| ASharedLoan (loans, v, av) ->
- let loans = V.BorrowId.set_to_string loans in
+ let loans = V.BorrowId.set_to_string None loans in
"@shared_loan(" ^ loans ^ ", "
^ typed_value_to_string fmt v
^ ", "
@@ -443,9 +443,9 @@ module Values = struct
indent ^ "abs@"
^ V.AbstractionId.to_string abs.abs_id
^ "{parents="
- ^ V.AbstractionId.set_to_string abs.parents
+ ^ V.AbstractionId.set_to_string None abs.parents
^ "}" ^ "{regions="
- ^ T.RegionId.set_to_string abs.regions
+ ^ T.RegionId.set_to_string None abs.regions
^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
end
@@ -462,11 +462,10 @@ module Contexts = struct
(indent_incr : string) (ev : C.env_elem) : string =
match ev with
| Var (var, tv) ->
- indent
- ^ option_to_string binder_to_string var
- ^ " -> "
- ^ PV.typed_value_to_string fmt tv
- ^ " ;"
+ let bv =
+ match var with Some var -> binder_to_string var | None -> "_"
+ in
+ indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
| Abs abs -> PV.abs_to_string fmt indent indent_incr abs
| Frame -> failwith "Can't print a Frame element"
@@ -555,7 +554,7 @@ module Contexts = struct
let eval_ctx_to_string (ctx : C.eval_ctx) : string =
let fmt = eval_ctx_to_ctx_formatter ctx in
- let ended_regions = T.RegionId.set_to_string ctx.ended_regions in
+ let ended_regions = T.RegionId.set_to_string None ctx.ended_regions in
let frames = split_env_according_to_frames ctx.env in
let num_frames = List.length frames in
let frames =
diff --git a/src/Types.ml b/src/Types.ml
index b33df0ac..b410c5a6 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -29,6 +29,11 @@ type region_var = (RegionVarId.id, string option) indexed_var [@@deriving show]
Regions are used in function signatures (in which case we use region variable
ids) and in symbolic variables and projections (in which case we use region
ids).
+
+ TODO: use this only in the signatures. During interpretation, we need
+ a uniform treatment of regions as variables (otherwise the projectors
+ don't work: they always ignore the static regions...). By convention,
+ use region with id 0 as the static region.
*)
type 'rid region =
| Static (** Static region *)
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index bda49608..38560894 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -91,8 +91,11 @@ let rec ety_no_regions_to_rty (ty : ety) : rty =
"Can't convert a ref with erased regions to a ref with non-erased \
regions"
-(** Check if a [ty] contains regions *)
-let ty_has_regions (ty : ety) : bool =
+(** Check if a [ty] contains regions.
+
+ TODO: rename to "has_borrows"?
+ *)
+let ty_has_regions (ty : 'r ty) : bool =
let obj =
object
inherit [_] iter_ty as super
@@ -135,7 +138,7 @@ let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool =
* require calling dedicated functions defined through the Copy trait. It
* is the case for types like integers, shared borrows, etc.
*)
-let rec type_is_primitively_copyable (ty : ety) : bool =
+let rec type_is_primitively_copyable (ty : 'r ty) : bool =
match ty with
| Adt ((AdtId _ | Assumed _), _, _) -> false
| Adt (Tuple, _, tys) -> List.for_all type_is_primitively_copyable tys
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index f90a98ef..2d380ca9 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -3,6 +3,9 @@ open TypesUtils
open Types
open Values
+exception FoundSymbolicValue of symbolic_value
+(** Utility exception *)
+
let mk_unit_value : typed_value =
{ value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
@@ -16,6 +19,12 @@ let mk_box_value (v : typed_value) : typed_value =
let box_v = Adt { variant_id = None; field_values = [ v ] } in
mk_typed_value box_ty box_v
+let is_symbolic (v : value) : bool =
+ match v with Symbolic _ -> true | _ -> false
+
+let as_symbolic (v : value) : symbolic_value =
+ match v with Symbolic s -> s | _ -> failwith "Unexpected"
+
(** Check if a value contains a borrow *)
let borrows_in_value (v : typed_value) : bool =
let obj =
@@ -78,3 +87,23 @@ let outer_loans_in_value (v : typed_value) : bool =
obj#visit_typed_value () v;
false
with Found -> true
+
+let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option
+ =
+ (* The visitor *)
+ let obj =
+ object
+ inherit [_] iter_typed_value
+
+ method! visit_Symbolic _ sv =
+ let ty = sv.sv_ty in
+ if type_is_primitively_copyable ty && ty_has_regions ty then
+ raise (FoundSymbolicValue sv)
+ else ()
+ end
+ in
+ (* Small helper *)
+ try
+ obj#visit_typed_value () v;
+ None
+ with FoundSymbolicValue sv -> Some sv
diff --git a/src/main.ml b/src/main.ml
index e8f46b99..fee51421 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -47,10 +47,11 @@ let () =
main_log#set_level EL.Debug;
interpreter_log#set_level EL.Debug;
statements_log#set_level EL.Debug;
+ paths_log#set_level EL.Debug;
expressions_log#set_level EL.Debug;
expansion_log#set_level EL.Debug;
borrows_log#set_level EL.Debug;
- invariants_log#set_level EL.Warning;
+ invariants_log#set_level EL.Debug;
(* Load the module *)
let json = Yojson.Basic.from_file !filename in
match cfim_module_of_json json with