diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Contexts.ml | 57 |
1 files changed, 45 insertions, 12 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 5e8ae3d0..0fe3a09a 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -3,6 +3,46 @@ open Values open CfimAst module V = Values +(** Some global counters. + * + * Note that those counters were initially stored in [eval_ctx] values, + * but it proved better to make them global and stateful: + * - when branching (and thus executing on several paths with different + * contexts) it is better to really have unique ids everywhere (and + * not have fresh ids shared by several contexts even though introduced + * after the branching) because at some point we might need to merge the + * different contexts + * - also, it is a lot more convenient to not store those counters in contexts + * objects + *) + +let symbolic_value_id_counter, fresh_symbolic_value_id = + SymbolicValueId.fresh_stateful_generator () + +let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator () + +let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator () + +let abstraction_id_counter, fresh_abstraction_id = + AbstractionId.fresh_stateful_generator () + +(** We shouldn't need to reset the global counters, but it might be good to + do it from time to time, for instance every time we start evaluating/ + synthesizing a function. + + The reasons are manifold: + - it might prevent the counters from overflowing (although this seems + extremely unlikely - as a side node: we have overflow checks to make + sure the synthesis doesn't get impacted by potential overflows) + - most importantly, it allows to always manipulate low values, which + is always a lot more readable when debugging + *) +let reset_global_counters () = + symbolic_value_id_counter := SymbolicValueId.generator_zero; + borrow_id_counter := BorrowId.generator_zero; + region_id_counter := RegionId.generator_zero; + abstraction_id_counter := AbstractionId.generator_zero + type binder = { index : VarId.id; (** Unique variable identifier *) name : string option; (** Possible name *) @@ -60,25 +100,18 @@ type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show] type config = { mode : interpreter_mode; check_invariants : bool } [@@deriving show] +type type_context = { type_defs : type_def list } [@@deriving show] + type eval_ctx = { - type_context : type_def list; + type_context : type_context; fun_context : fun_def list; type_vars : type_var list; env : env; - symbolic_counter : SymbolicValueId.generator; - borrow_counter : BorrowId.generator; + ended_regions : RegionId.set_t; } [@@deriving show] (** Evaluation context *) -let fresh_symbolic_value_id (ctx : eval_ctx) : eval_ctx * SymbolicValueId.id = - let id, counter' = SymbolicValueId.fresh ctx.symbolic_counter in - ({ ctx with symbolic_counter = counter' }, id) - -let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id = - let id, counter' = BorrowId.fresh ctx.borrow_counter in - ({ ctx with borrow_counter = counter' }, id) - let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = TypeVarId.nth ctx.type_vars vid @@ -94,7 +127,7 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder = lookup ctx.env let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def = - TypeDefId.nth ctx.type_context tid + TypeDefId.nth ctx.type_context.type_defs tid let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def = FunDefId.nth ctx.fun_context fid |