diff options
| -rw-r--r-- | src/InterpreterStatements.ml | 4 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 19 | ||||
| -rw-r--r-- | src/Values.ml | 4 |
3 files changed, 12 insertions, 15 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index be0fb088..ef2c069d 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -669,7 +669,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) ref V.AbstractionId.Map.empty in (* Auxiliary function to create one abstraction *) - let create_abs (back_id : V.BackwardFunctionId.id) (rg : A.abs_region_group) : + let create_abs (back_id : T.RegionGroupId.id) (rg : A.abs_region_group) : V.abs = let abs_id = rg.T.id in let back_id = Some back_id in @@ -709,7 +709,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) } in (* Apply *) - V.BackwardFunctionId.mapi create_abs rgl + T.RegionGroupId.mapi create_abs rgl (** Evaluate a statement *) let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index be2231a3..11d7a657 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -11,7 +11,7 @@ open Pure (** TODO: move this, it is not useful for symbolic -> pure *) type name = - | FunName of A.FunDefId.id * V.BackwardFunctionId.id option + | FunName of A.FunDefId.id * T.RegionVarId.id option | TypeName of T.TypeDefId.id [@@deriving show, ord] @@ -40,8 +40,8 @@ module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType) generation with collision in mind, it is always good to have such checks. *) -let translate_fun_name (fdef : A.fun_def) (bid : V.BackwardFunctionId.id option) - : Id.name = +let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) : + Id.name = let sg = fdef.signature in (* General function to generate a suffix for a region group * (i.e., an abstraction)*) @@ -82,7 +82,7 @@ let translate_fun_name (fdef : A.fun_def) (bid : V.BackwardFunctionId.id option) (* Several backward functions - note that **we use the backward function id * as if it were a region group id** (there is a direct mapping between the * two - TODO: merge them) *) - let rg = V.BackwardFunctionId.nth sg.regions_hierarchy bid in + let rg = T.RegionGroupId.nth sg.regions_hierarchy bid in "_back" ^ rg_to_string rg) in (* Final name *) @@ -116,7 +116,7 @@ type synth_ctx = { type bs_ctx = { type_context : type_context; fun_def : A.fun_def; - bid : V.BackwardFunctionId.id option; + bid : T.RegionGroupId.id option; } (** Body synthesis context *) @@ -286,16 +286,15 @@ let list_ordered_parent_region_groups (def : A.fun_def) parents let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) - (bid : V.BackwardFunctionId.id option) : fun_sig = + (bid : T.RegionGroupId.id option) : fun_sig = let sg = def.signature in (* Retrieve the list of parent backward functions *) let gid, parents = match bid with | None -> (None, T.RegionGroupId.Set.empty) | Some bid -> - let gid = T.RegionGroupId.of_int (V.BackwardFunctionId.to_int bid) in - let parents = list_parent_region_groups def gid in - (Some gid, parents) + let parents = list_parent_region_groups def bid in + (Some bid, parents) in (* List the inputs for: * - the forward function @@ -570,7 +569,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) Switch (scrutinee, SwitchInt (int_ty, branches, otherwise)) let translate_fun_def (type_context : type_context) (def : A.fun_def) - (bid : V.BackwardFunctionId.id option) (body : S.expression) : fun_def = + (bid : T.RegionGroupId.id option) (body : S.expression) : fun_def = let bs_ctx = { type_context; fun_def = def; bid } in (* Translate the function *) let def_id = def.A.def_id in diff --git a/src/Values.ml b/src/Values.ml index a905c8d3..cc458bca 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -15,8 +15,6 @@ module AbstractionId = IdGen () module FunCallId = IdGen () -module BackwardFunctionId = IdGen () - (** A variable *) type big_int = Z.t @@ -738,7 +736,7 @@ type abs = { this is only used for pretty-printing and debugging, in the symbolic AST, generated by the symbolic execution. *) - back_id : (BackwardFunctionId.id option[@opaque]); + back_id : (RegionGroupId.id option[@opaque]); (** The id of the backward function to which this abstraction is linked. This is not used by the symbolic execution: it is a utility for the symbolic AST, generated by the symbolic execution. |