diff options
| -rw-r--r-- | TODO.md | 4 | ||||
| -rw-r--r-- | src/Identifiers.ml | 39 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 31 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 72 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 15 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 7 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 3 | ||||
| -rw-r--r-- | src/Invariants.ml | 119 | ||||
| -rw-r--r-- | src/Print.ml | 19 | ||||
| -rw-r--r-- | src/Types.ml | 5 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 9 | ||||
| -rw-r--r-- | src/ValuesUtils.ml | 29 | ||||
| -rw-r--r-- | src/main.ml | 3 |
15 files changed, 263 insertions, 98 deletions
@@ -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 |