diff options
| -rw-r--r-- | src/Interpreter.ml | 76 | ||||
| -rw-r--r-- | src/Invariants.ml | 26 |
2 files changed, 26 insertions, 76 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index e11adcbf..b105c97b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -10,6 +10,7 @@ module L = Logging open TypesUtils open ValuesUtils module Inv = Invariants +open InterpreterUtils (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -26,81 +27,6 @@ module Inv = Invariants (* TODO: remove the config parameters when they are useless *) -(** Some utilities *) - -let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string - -let ety_to_string = Print.EvalCtxCfimAst.ety_to_string - -let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string - -let place_to_string = Print.EvalCtxCfimAst.place_to_string - -let operand_to_string = Print.EvalCtxCfimAst.operand_to_string - -let statement_to_string ctx = - Print.EvalCtxCfimAst.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 - -(* TODO: move *) -let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var - = - { A.index; name; var_ty } - -(** Small helper *) -let mk_place_from_var_id (var_id : V.VarId.id) : E.place = - { var_id; projection = [] } - -(** Deconstruct a type of the form `Box<T>` to retrieve the `T` inside *) -let ty_get_box (box_ty : T.ety) : T.ety = - match box_ty with - | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> boxed_ty - | _ -> failwith "Not a boxed type" - -(** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and - the borrow kind, etc.) - *) -let ty_get_ref (ty : T.ety) : T.erased_region * T.ety * T.ref_kind = - match ty with - | T.Ref (r, ty, ref_kind) -> (r, ty, ref_kind) - | _ -> failwith "Not a ref type" - -(** Box a value *) -let mk_box_value (v : V.typed_value) : V.typed_value = - let box_ty = T.Adt (T.Assumed T.Box, [], [ v.V.ty ]) in - let box_v = V.Adt { variant_id = None; field_values = [ v ] } in - mk_typed_value box_ty box_v - -(** Create a fresh symbolic proj comp *) -let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty) - (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp = - let ctx, sv_id = C.fresh_symbolic_value_id ctx in - let svalue = { V.sv_id; V.sv_ty = ty } in - let sv = { V.svalue; rset_ended = ended_regions } in - (ctx, sv) - -(** Create a fresh symbolic value (as a complementary projector) *) -let mk_fresh_symbolic_proj_comp_value (ended_regions : T.RegionId.set_t) - (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ty ctx in - let value : V.value = V.Symbolic sv in - let ty : T.ety = Subst.erase_regions ty in - let sv : V.typed_value = { V.value; ty } in - (ctx, sv) - -let mk_typed_value_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_value = - let ty = Subst.erase_regions sv.V.svalue.V.sv_ty in - let value = V.Symbolic sv in - { V.value; ty } - -let mk_aproj_loans_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_avalue = - let ty = sv.V.svalue.V.sv_ty in - let proj = V.AProjLoans sv.V.svalue in - let value = V.ASymbolic proj in - { V.value; ty } - (** TODO: change the name *) type eval_error = Panic diff --git a/src/Invariants.ml b/src/Invariants.ml index 5caafa79..a36cae03 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -12,12 +12,21 @@ module A = CfimAst module L = Logging open TypesUtils open ValuesUtils +open InterpreterUtils + +let debug_invariants : bool ref = ref false type borrow_info = { loan_kind : T.ref_kind; loan_ids : V.BorrowId.set_t; borrow_ids : V.BorrowId.set_t; } +[@@deriving show] + +let borrows_infos_to_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 + String.concat "\n" bindings type borrow_kind = Mut | Shared | Inactivated @@ -198,10 +207,25 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (* Visit *) 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 + ("\Borrows information:\n" + ^ borrows_infos_to_string !borrows_infos + ^ "\n"))); + (* Finally, check that everything is consistant *) V.BorrowId.Map.iter (fun _ info -> - assert (info.loan_ids = info.borrow_ids); + (* Note that we can't directly compare the sets - I guess they are + * different depending on the order in which we add the elements... *) + assert ( + V.BorrowId.Set.elements info.loan_ids + = V.BorrowId.Set.elements info.borrow_ids); match info.loan_kind with | T.Mut -> assert (V.BorrowId.Set.cardinal info.loan_ids = 1) | T.Shared -> ()) |