diff options
Diffstat (limited to '')
-rw-r--r-- | src/Invariants.ml | 119 |
1 files changed, 101 insertions, 18 deletions
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 |