summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CfimAst.ml8
-rw-r--r--src/CfimOfJson.ml30
-rw-r--r--src/Contexts.ml6
-rw-r--r--src/Identifiers.ml65
-rw-r--r--src/Interpreter.ml208
-rw-r--r--src/Modules.ml4
-rw-r--r--src/Print.ml66
-rw-r--r--src/Substitute.ml17
-rw-r--r--src/Types.ml13
-rw-r--r--src/Values.ml8
10 files changed, 136 insertions, 289 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 7be1a4bc..36977aad 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -14,10 +14,10 @@ type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
type assertion = { cond : operand; expected : bool } [@@deriving show]
type fun_sig = {
- region_params : region_var RegionVarId.vector;
+ region_params : region_var list;
num_early_bound_regions : int;
- type_params : type_var TypeVarId.vector;
- inputs : rty VarId.vector;
+ type_params : type_var list;
+ inputs : rty list;
output : rty;
}
[@@deriving show]
@@ -75,7 +75,7 @@ type fun_def = {
signature : fun_sig;
divergent : bool;
arg_count : int;
- locals : var VarId.vector;
+ locals : var list;
body : expression;
}
[@@deriving show]
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index bb0e9b69..4f6c2e73 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -138,7 +138,7 @@ let variant_of_json (js : json) : (T.variant, string) result =
(match js with
| `Assoc [ ("name", name); ("fields", fields) ] ->
let* name = string_of_json name in
- let* fields = T.FieldId.vector_of_json field_of_json fields in
+ let* fields = list_of_json field_of_json fields in
Ok { T.variant_name = name; fields }
| _ -> Error "")
@@ -146,10 +146,10 @@ let type_def_kind_of_json (js : json) : (T.type_def_kind, string) result =
combine_error_msgs js "type_def_kind_of_json"
(match js with
| `Assoc [ ("Struct", fields) ] ->
- let* fields = T.FieldId.vector_of_json field_of_json fields in
+ let* fields = list_of_json field_of_json fields in
Ok (T.Struct fields)
| `Assoc [ ("Enum", variants) ] ->
- let* variants = T.VariantId.vector_of_json variant_of_json variants in
+ let* variants = list_of_json variant_of_json variants in
Ok (T.Enum variants)
| _ -> Error "")
@@ -166,12 +166,8 @@ let type_def_of_json (js : json) : (T.type_def, string) result =
] ->
let* def_id = T.TypeDefId.id_of_json def_id in
let* name = name_of_json name in
- let* region_params =
- T.RegionVarId.vector_of_json region_var_of_json region_params
- in
- let* type_params =
- T.TypeVarId.vector_of_json type_var_of_json type_params
- in
+ let* region_params = list_of_json region_var_of_json region_params in
+ let* type_params = list_of_json type_var_of_json type_params in
let* kind = type_def_kind_of_json kind in
Ok { T.def_id; name; region_params; type_params; kind }
| _ -> Error "")
@@ -445,14 +441,10 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
("inputs", inputs);
("output", output);
] ->
- let* region_params =
- T.RegionVarId.vector_of_json region_var_of_json region_params
- in
+ let* region_params = list_of_json region_var_of_json region_params in
let* num_early_bound_regions = int_of_json num_early_bound_regions in
- let* type_params =
- T.TypeVarId.vector_of_json type_var_of_json type_params
- in
- let* inputs = V.VarId.vector_of_json rty_of_json inputs in
+ let* type_params = list_of_json type_var_of_json type_params in
+ let* inputs = list_of_json rty_of_json inputs in
let* output = rty_of_json output in
Ok
{
@@ -572,7 +564,7 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result =
let* signature = fun_sig_of_json signature in
let* divergent = bool_of_json divergent in
let* arg_count = int_of_json arg_count in
- let* locals = V.VarId.vector_of_json var_of_json locals in
+ let* locals = list_of_json var_of_json locals in
let* body = expression_of_json body in
Ok { A.def_id; name; signature; divergent; arg_count; locals; body }
| _ -> Error "")
@@ -604,7 +596,7 @@ let cfim_module_of_json (js : json) : (M.cfim_module, string) result =
("functions", functions);
] ->
let* declarations = list_of_json declaration_of_json declarations in
- let* types = T.TypeDefId.vector_of_json type_def_of_json types in
- let* functions = A.FunDefId.vector_of_json fun_def_of_json functions in
+ let* types = list_of_json type_def_of_json types in
+ let* functions = list_of_json fun_def_of_json functions in
Ok { M.declarations; types; functions }
| _ -> Error "")
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 8a498e2e..84c88e1c 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -18,9 +18,9 @@ type config = { mode : interpreter_mode; check_invariants : bool }
[@@deriving show]
type eval_ctx = {
- type_context : type_def TypeDefId.vector;
- fun_context : fun_def FunDefId.vector;
- type_vars : type_var TypeVarId.vector;
+ type_context : type_def list;
+ fun_context : fun_def list;
+ type_vars : type_var list;
env : env;
symbolic_counter : SymbolicValueId.generator;
borrow_counter : BorrowId.generator;
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index ebe0d898..3c07b511 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -10,16 +10,13 @@ module type Id = sig
type generator
(** Id generator - simply a counter *)
- (* TODO: use list instead *)
- type 'a vector
-
type set_t
val zero : id
val generator_zero : generator
- (* TODO: this is stateful! *)
+ (* TODO: this is stateful! - but we may want to be able to duplicated contexts... *)
val fresh : generator -> id * generator
val to_string : id -> string
@@ -36,42 +33,21 @@ module type Id = sig
val of_int : id -> int
- val pp_vector :
- (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a vector -> unit
-
- val show_vector : (Format.formatter -> 'a -> unit) -> 'a vector -> string
-
- val empty_vector : 'a vector
-
- val vector_to_list : 'a vector -> 'a list
-
- val vector_of_list : 'a list -> 'a vector
-
- val length : 'a vector -> int
+ val nth : 'a list -> id -> 'a
- val nth : 'a vector -> id -> 'a
+ val nth_opt : 'a list -> id -> 'a option
- val nth_opt : 'a vector -> id -> 'a option
-
- val update_nth : 'a vector -> id -> 'a -> 'a vector
- (** Update the nth element of the vector.
+ val update_nth : 'a list -> id -> 'a -> 'a list
+ (** Update the nth element of the list.
Raises [Invalid_argument] if the identifier is out of range.
*)
- val iter : ('a -> unit) -> 'a vector -> unit
-
- val map : ('a -> 'b) -> 'a vector -> 'b vector
-
- val mapi : (id -> 'a -> 'b) -> 'a vector -> 'b vector
+ val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list
- val mapi_from1 : (id -> 'a -> 'b) -> 'a vector -> 'b vector
+ val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list
(** Same as [mapi], but where the indices start with 1 *)
- val for_all : ('a -> bool) -> 'a vector -> bool
-
- val exists : ('a -> bool) -> 'a vector -> bool
-
val pp_set_t : Format.formatter -> set_t -> unit
val show_set_t : set_t -> string
@@ -85,11 +61,6 @@ module type Id = sig
module Map : Map.S with type key = id
val id_of_json : Yojson.Basic.t -> (id, string) result
-
- val vector_of_json :
- (Yojson.Basic.t -> ('a, string) result) ->
- Yojson.Basic.t ->
- ('a vector, string) result
end
(** Generative functor for identifiers.
@@ -102,8 +73,6 @@ module IdGen () : Id = struct
type generator = id [@@deriving show]
- type 'a vector = 'a list [@@deriving show]
-
let zero = 0
let generator_zero = 0
@@ -122,14 +91,6 @@ module IdGen () : Id = struct
let of_int x = x
- let empty_vector = []
-
- let vector_to_list v = v
-
- let vector_of_list v = v
-
- let length v = List.length v
-
let nth v id = List.nth v id
let nth_opt v id = List.nth_opt v id
@@ -140,10 +101,6 @@ module IdGen () : Id = struct
| _ :: vec', 0 -> v :: vec'
| x :: vec', _ -> x :: update_nth vec' (id - 1) v
- let iter = List.iter
-
- let map = List.map
-
let mapi = List.mapi
let mapi_from1 f ls =
@@ -152,10 +109,6 @@ module IdGen () : Id = struct
in
aux 1 ls
- let for_all = List.for_all
-
- let exists = List.exists
-
module Ord = struct
type t = id
@@ -183,10 +136,6 @@ module IdGen () : Id = struct
match js with
| `Int i -> Ok i
| _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
-
- let vector_of_json a_of_json js =
- OfJsonBasic.combine_error_msgs js "vector_of_json"
- (OfJsonBasic.list_of_json a_of_json js)
end
type name = string list [@@deriving show]
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 05dc3f5a..003f5411 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -47,8 +47,7 @@ let expression_to_string ctx =
let mk_unit_ty : T.ety = T.Tuple []
(* TODO: move *)
-let mk_unit_value : V.typed_value =
- { V.value = V.Tuple (T.FieldId.vector_of_list []); V.ty = mk_unit_ty }
+let mk_unit_value : V.typed_value = { V.value = V.Tuple []; V.ty = mk_unit_ty }
let mk_typed_value (ty : T.ety) (value : V.value) : V.typed_value =
{ V.value; ty }
@@ -81,8 +80,8 @@ let rec check_borrows_in_value (check : V.borrow_content -> bool)
(v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> true
- | V.Adt av -> T.FieldId.for_all (check_borrows_in_value check) av.field_values
- | V.Tuple values -> T.FieldId.for_all (check_borrows_in_value check) values
+ | V.Adt av -> List.for_all (check_borrows_in_value check) av.field_values
+ | V.Tuple values -> List.for_all (check_borrows_in_value check) values
| V.Assumed (Box bv) -> check_borrows_in_value check bv
| V.Borrow bc -> (
check bc
@@ -100,8 +99,8 @@ let rec check_loans_in_value (check : V.loan_content -> bool)
(v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> true
- | V.Adt av -> T.FieldId.for_all (check_loans_in_value check) av.field_values
- | V.Tuple values -> T.FieldId.for_all (check_loans_in_value check) values
+ | V.Adt av -> List.for_all (check_loans_in_value check) av.field_values
+ | V.Tuple values -> List.for_all (check_loans_in_value check) values
| V.Assumed (Box bv) -> check_loans_in_value check bv
| V.Borrow bc -> (
match bc with
@@ -119,12 +118,8 @@ let rec lookup_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
(v : V.typed_value) : V.loan_content option =
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> None
- | V.Adt av ->
- let values = T.FieldId.vector_to_list av.field_values in
- List.find_map (lookup_loan_in_value ek l) values
- | V.Tuple values ->
- let values = T.FieldId.vector_to_list values in
- List.find_map (lookup_loan_in_value ek l) values
+ | V.Adt av -> List.find_map (lookup_loan_in_value ek l) av.field_values
+ | V.Tuple values -> List.find_map (lookup_loan_in_value ek l) values
| V.Assumed (Box bv) -> lookup_loan_in_value ek l bv
| V.Borrow bc -> (
match bc with
@@ -175,13 +170,11 @@ let rec update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> v
| V.Adt av ->
- let values =
- T.FieldId.map (update_loan_in_value ek l nlc) av.field_values
- in
+ let values = List.map (update_loan_in_value ek l nlc) av.field_values in
let av = { av with field_values = values } in
{ v with value = Adt av }
| V.Tuple values ->
- let values = T.FieldId.map (update_loan_in_value ek l nlc) values in
+ let values = List.map (update_loan_in_value ek l nlc) values in
{ v with value = Tuple values }
| V.Assumed (Box bv) ->
{ v with value = Assumed (Box (update_loan_in_value ek l nlc bv)) }
@@ -228,12 +221,8 @@ let rec lookup_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id)
(v : V.typed_value) : V.borrow_content option =
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> None
- | V.Adt av ->
- let values = T.FieldId.vector_to_list av.field_values in
- List.find_map (lookup_borrow_in_value ek l) values
- | V.Tuple values ->
- let values = T.FieldId.vector_to_list values in
- List.find_map (lookup_borrow_in_value ek l) values
+ | V.Adt av -> List.find_map (lookup_borrow_in_value ek l) av.field_values
+ | V.Tuple values -> List.find_map (lookup_borrow_in_value ek l) values
| V.Assumed (Box bv) -> lookup_borrow_in_value ek l bv
| V.Borrow bc -> (
match bc with
@@ -281,13 +270,11 @@ let rec update_borrow_in_value (ek : exploration_kind) (l : V.BorrowId.id)
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> v
| V.Adt av ->
- let values =
- T.FieldId.map (update_borrow_in_value ek l nbc) av.field_values
- in
+ let values = List.map (update_borrow_in_value ek l nbc) av.field_values in
let av = { av with field_values = values } in
{ v with value = Adt av }
| V.Tuple values ->
- let values = T.FieldId.map (update_borrow_in_value ek l nbc) values in
+ let values = List.map (update_borrow_in_value ek l nbc) values in
{ v with value = Tuple values }
| V.Assumed (Box bv) ->
{ v with value = Assumed (Box (update_borrow_in_value ek l nbc bv)) }
@@ -369,12 +356,8 @@ let borrows_in_value (v : V.typed_value) : bool =
let rec loans_in_value (v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ -> false
- | V.Adt av ->
- let fields = T.FieldId.vector_to_list av.field_values in
- List.exists loans_in_value fields
- | V.Tuple fields ->
- let fields = T.FieldId.vector_to_list fields in
- List.exists loans_in_value fields
+ | V.Adt av -> List.exists loans_in_value av.field_values
+ | V.Tuple fields -> List.exists loans_in_value fields
| V.Assumed (Box bv) -> loans_in_value bv
| V.Borrow bc -> (
match bc with
@@ -387,12 +370,8 @@ let rec loans_in_value (v : V.typed_value) : bool =
let rec get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
match v.V.value with
| V.Concrete _ -> None
- | V.Adt av ->
- let fields = T.FieldId.vector_to_list av.field_values in
- get_first_loan_in_values fields
- | V.Tuple fields ->
- let fields = T.FieldId.vector_to_list fields in
- get_first_loan_in_values fields
+ | V.Adt av -> get_first_loan_in_values av.field_values
+ | V.Tuple fields -> get_first_loan_in_values fields
| V.Assumed (Box bv) -> get_first_loan_in_value bv
| V.Borrow bc -> (
match bc with
@@ -413,12 +392,8 @@ and get_first_loan_in_values (vl : V.typed_value list) : V.loan_content option =
let rec bottom_in_value (v : V.typed_value) : bool =
match v.V.value with
| V.Concrete _ -> false
- | V.Adt av ->
- let fields = T.FieldId.vector_to_list av.field_values in
- List.exists bottom_in_value fields
- | V.Tuple fields ->
- let fields = T.FieldId.vector_to_list fields in
- List.exists bottom_in_value fields
+ | V.Adt av -> List.exists bottom_in_value av.field_values
+ | V.Tuple fields -> List.exists bottom_in_value fields
| V.Assumed (Box bv) -> bottom_in_value bv
| V.Borrow bc -> (
match bc with
@@ -450,19 +425,16 @@ let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer)
* boxes upon ending inner borrows *)
({ v0 with value = Assumed (Box bv') }, res)
| V.Adt adt ->
- let values = T.FieldId.vector_to_list adt.field_values in
- let values', res =
- end_borrow_get_borrow_in_values config io l outer_borrows values
+ let values, res =
+ end_borrow_get_borrow_in_values config io l outer_borrows
+ adt.field_values
in
- let values' = T.FieldId.vector_of_list values' in
- ({ v0 with value = Adt { adt with field_values = values' } }, res)
+ ({ v0 with value = Adt { adt with field_values = values } }, res)
| V.Tuple values ->
- let values = T.FieldId.vector_to_list values in
- let values', res =
+ let values, res =
end_borrow_get_borrow_in_values config io l outer_borrows values
in
- let values' = T.FieldId.vector_of_list values' in
- ({ v0 with value = Tuple values' }, res)
+ ({ v0 with value = Tuple values }, res)
| V.Loan (V.MutLoan _) -> (v0, NotFound)
| V.Loan (V.SharedLoan (borrows, v)) ->
(* Update the outer borrows, if necessary *)
@@ -543,19 +515,11 @@ let rec give_back_value_to_value config bid (v : V.typed_value)
| V.Concrete _ | V.Bottom | V.Symbolic _ -> destv
| V.Adt av ->
let field_values =
- List.map
- (give_back_value_to_value config bid v)
- (T.FieldId.vector_to_list av.field_values)
+ List.map (give_back_value_to_value config bid v) av.field_values
in
- let field_values = T.FieldId.vector_of_list field_values in
{ destv with value = Adt { av with field_values } }
| V.Tuple values ->
- let values =
- List.map
- (give_back_value_to_value config bid v)
- (T.FieldId.vector_to_list values)
- in
- let values = T.FieldId.vector_of_list values in
+ let values = List.map (give_back_value_to_value config bid v) values in
{ destv with value = Tuple values }
| V.Assumed (Box destv') ->
{
@@ -590,19 +554,11 @@ let rec give_back_shared_to_value (config : C.config) bid
| V.Concrete _ | V.Bottom | V.Symbolic _ -> destv
| V.Adt av ->
let field_values =
- List.map
- (give_back_shared_to_value config bid)
- (T.FieldId.vector_to_list av.field_values)
+ List.map (give_back_shared_to_value config bid) av.field_values
in
- let field_values = T.FieldId.vector_of_list field_values in
{ destv with value = Adt { av with field_values } }
| V.Tuple values ->
- let values =
- List.map
- (give_back_shared_to_value config bid)
- (T.FieldId.vector_to_list values)
- in
- let values = T.FieldId.vector_of_list values in
+ let values = List.map (give_back_shared_to_value config bid) values in
{ destv with value = Tuple values }
| V.Assumed (Box destv') ->
{
@@ -699,14 +655,10 @@ let reborrow_shared (config : C.config) (original_bid : V.BorrowId.id)
match v.V.value with
| V.Concrete _ | V.Bottom | V.Symbolic _ -> v
| V.Adt av ->
- let fields = T.FieldId.vector_to_list av.field_values in
- let fields = List.map reborrow_in_value fields in
- let fields = T.FieldId.vector_of_list fields in
+ let fields = List.map reborrow_in_value av.field_values in
{ v with value = Adt { av with field_values = fields } }
| V.Tuple fields ->
- let fields = T.FieldId.vector_to_list fields in
let fields = List.map reborrow_in_value fields in
- let fields = T.FieldId.vector_of_list fields in
{ v with value = Tuple fields }
| V.Assumed (Box bv) ->
{ v with value = Assumed (Box (reborrow_in_value bv)) }
@@ -1045,7 +997,7 @@ let rec access_projection (access : projection_access) (env : C.env)
Ok (env1, { res with updated }))
(* Tuples *)
| Field (ProjTuple arity, field_id), V.Tuple values -> (
- assert (arity = T.FieldId.length values);
+ assert (arity = List.length values);
let fv = T.FieldId.nth values field_id in
(* Project *)
match access_projection access env update p' fv with
@@ -1238,7 +1190,7 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
| Ok ctx -> ctx
(** Compute an expanded ADT bottom value *)
-let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.vector)
+let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
(def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
(regions : T.erased_region list) (types : T.ety list) : V.typed_value =
(* Lookup the definition and check if it is an enumeration - it
@@ -1246,15 +1198,13 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.vector)
is a field projection with *some* variant id. Retrieve the list
of fields at the same time. *)
let def = T.TypeDefId.nth tyctx def_id in
- assert (List.length regions = T.RegionVarId.length def.T.region_params);
+ assert (List.length regions = List.length def.T.region_params);
(* Compute the field types *)
let field_types =
Subst.type_def_get_instantiated_field_type def opt_variant_id types
in
(* Initialize the expanded value *)
- let field_types = T.FieldId.vector_to_list field_types in
let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in
- let fields = T.FieldId.vector_of_list fields in
let av =
V.Adt
{
@@ -1273,7 +1223,6 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
V.typed_value =
(* Generate the field values *)
let fields = List.map (fun ty -> { V.value = Bottom; ty }) field_types in
- let fields = T.FieldId.vector_of_list fields in
let v = V.Tuple fields in
let ty = T.Tuple field_types in
{ V.value = v; V.ty }
@@ -1434,8 +1383,8 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind)
(* Nothing to do for symbolic values - note that if the value needs
to be copied, etc. we perform additional checks later *)
()
- | V.Adt adt -> T.FieldId.iter inspect_update adt.field_values
- | V.Tuple values -> T.FieldId.iter inspect_update values
+ | V.Adt adt -> List.iter inspect_update adt.field_values
+ | V.Tuple values -> List.iter inspect_update values
| V.Assumed (Box v) -> inspect_update v
| V.Borrow bc -> (
match bc with
@@ -1534,9 +1483,8 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
| V.Symbolic _ ->
(* Nothing to do for symbolic values - TODO: not sure *)
raise Unimplemented
- | V.Adt adt ->
- T.FieldId.iter (inspect_update end_loans) adt.field_values
- | V.Tuple values -> T.FieldId.iter (inspect_update end_loans) values
+ | V.Adt adt -> List.iter (inspect_update end_loans) adt.field_values
+ | V.Tuple values -> List.iter (inspect_update end_loans) values
| V.Assumed (Box v) -> inspect_update end_loans v
| V.Borrow bc -> (
assert (not end_loans);
@@ -1609,15 +1557,13 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
match v.V.value with
| V.Concrete _ -> (ctx, v)
| V.Adt av ->
- let fields = T.FieldId.vector_to_list av.field_values in
- let ctx', fields = List.fold_left_map (copy_value config) ctx fields in
- let fields = T.FieldId.vector_of_list fields in
- (ctx', { v with V.value = V.Adt { av with field_values = fields } })
+ let ctx, fields =
+ List.fold_left_map (copy_value config) ctx av.field_values
+ in
+ (ctx, { v with V.value = V.Adt { av with field_values = fields } })
| V.Tuple fields ->
- let fields = T.FieldId.vector_to_list fields in
- let ctx', fields = List.fold_left_map (copy_value config) ctx fields in
- let fields = T.FieldId.vector_of_list fields in
- (ctx', { v with V.value = V.Tuple fields })
+ let ctx, fields = List.fold_left_map (copy_value config) ctx fields in
+ (ctx, { v with V.value = V.Tuple fields })
| V.Bottom -> failwith "Can't copy ⊥"
| V.Assumed _ -> failwith "Can't copy an assumed value"
| V.Borrow bc -> (
@@ -1625,6 +1571,7 @@ let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
match bc with
| SharedBorrow bid ->
let ctx', bid' = C.fresh_borrow_id ctx in
+ (* TODO: clean indices *)
let env'' = reborrow_shared config bid bid' ctx'.env in
let ctx'' = { ctx' with env = env'' } in
(ctx'', { v with V.value = V.Borrow (SharedBorrow bid') })
@@ -1646,36 +1593,30 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
(* Check the type while converting *)
match (ty, cv) with
(* Unit *)
- | T.Tuple [], Unit -> { V.value = V.Tuple (T.FieldId.vector_of_list []); ty }
+ | T.Tuple [], Unit -> { V.value = V.Tuple []; ty }
(* Adt with one variant and no fields *)
| T.Adt (def_id, [], []), ConstantAdt def_id' ->
assert (def_id = def_id');
(* Check that the adt definition only has one variant with no fields,
compute the variant id at the same time. *)
let def = T.TypeDefId.nth ctx.type_context def_id in
- assert (T.RegionVarId.length def.region_params = 0);
- assert (T.TypeVarId.length def.type_params = 0);
+ assert (List.length def.region_params = 0);
+ assert (List.length def.type_params = 0);
let variant_id =
match def.kind with
| Struct fields ->
- assert (T.FieldId.length fields = 0);
+ assert (List.length fields = 0);
None
| Enum variants ->
- assert (T.VariantId.length variants = 1);
+ assert (List.length variants = 1);
let variant_id = T.VariantId.zero in
let variant = T.VariantId.nth variants variant_id in
- assert (T.FieldId.length variant.fields = 0);
+ assert (List.length variant.fields = 0);
Some variant_id
in
let value =
V.Adt
- {
- def_id;
- variant_id;
- regions = [];
- types = [];
- field_values = T.FieldId.vector_of_list [];
- }
+ { def_id; variant_id; regions = []; types = []; field_values = [] }
in
{ value; ty }
(* Scalar, boolean... *)
@@ -1918,24 +1859,20 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
| E.Aggregate (aggregate_kind, ops) -> (
(* Evaluate the operands *)
let ctx, values = eval_operands config ctx ops in
- let values = T.FieldId.vector_of_list values in
(* Match on the aggregate kind *)
match aggregate_kind with
| E.AggregatedTuple ->
- let tys =
- List.map (fun v -> v.V.ty) (T.FieldId.vector_to_list values)
- in
+ let tys = List.map (fun v -> v.V.ty) values in
Ok (ctx, { V.value = Tuple values; ty = T.Tuple tys })
| E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
(* Sanity checks *)
let type_def = C.ctx_lookup_type_def ctx def_id in
- assert (
- T.RegionVarId.length type_def.region_params = List.length regions);
+ assert (List.length type_def.region_params = List.length regions);
let expected_field_types =
Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id
types
in
- assert (expected_field_types = T.FieldId.map (fun v -> v.V.ty) values);
+ assert (expected_field_types = List.map (fun v -> v.V.ty) values);
(* Construct the value *)
let av =
{
@@ -2312,10 +2249,7 @@ let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
(* Create and push the input variables *)
let input_vars =
- V.VarId.vector_to_list
- (V.VarId.mapi_from1
- (fun id v -> (mk_var id None v.V.ty, v))
- (V.VarId.vector_of_list args_vl))
+ V.VarId.mapi_from1 (fun id v -> (mk_var id None v.V.ty, v)) args_vl
in
let ctx = C.ctx_push_vars ctx input_vars in
@@ -2413,13 +2347,10 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx)
| ConcreteMode -> (
let tsubst =
Subst.make_type_subst
- (List.map
- (fun v -> v.T.tv_index)
- (T.TypeVarId.vector_to_list def.A.signature.type_params))
+ (List.map (fun v -> v.T.tv_index) def.A.signature.type_params)
type_params
in
let locals, body = Subst.fun_def_substitute_in_body tsubst def in
- let locals = V.VarId.vector_to_list locals in
(* Evaluate the input operands *)
let ctx1, args = eval_operands config ctx args in
@@ -2554,9 +2485,8 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) :
(** Test a unit function (taking no arguments) by evaluating it in an empty
environment
*)
-let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
- (fun_defs : A.fun_def A.FunDefId.vector) (fid : A.FunDefId.id) :
- unit eval_result =
+let test_unit_function (type_defs : T.type_def list) (fun_defs : A.fun_def list)
+ (fid : A.FunDefId.id) : unit eval_result =
(* Retrieve the function declaration *)
let fdef = A.FunDefId.nth fun_defs fid in
@@ -2565,8 +2495,8 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
(lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name));
(* Sanity check - *)
- assert (T.RegionVarId.length fdef.A.signature.region_params = 0);
- assert (T.TypeVarId.length fdef.A.signature.type_params = 0);
+ assert (List.length fdef.A.signature.region_params = 0);
+ assert (List.length fdef.A.signature.type_params = 0);
assert (fdef.A.arg_count = 0);
(* Create the evaluation context *)
@@ -2574,7 +2504,7 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
{
C.type_context = type_defs;
C.fun_context = fun_defs;
- C.type_vars = T.TypeVarId.empty_vector;
+ C.type_vars = [];
C.env = [];
C.symbolic_counter = V.SymbolicValueId.generator_zero;
C.borrow_counter = V.BorrowId.generator_zero;
@@ -2582,9 +2512,7 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
in
(* Put the (uninitialized) local variables *)
- let ctx =
- C.ctx_push_uninitialized_vars ctx (V.VarId.vector_to_list fdef.A.locals)
- in
+ let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in
(* Evaluate the function *)
let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in
@@ -2596,13 +2524,13 @@ let test_unit_function (type_defs : T.type_def T.TypeDefId.vector)
no arguments) - TODO: move *)
let fun_def_is_unit (def : A.fun_def) : bool =
def.A.arg_count = 0
- && T.RegionVarId.length def.A.signature.region_params = 0
- && T.TypeVarId.length def.A.signature.type_params = 0
- && V.VarId.length def.A.signature.inputs = 0
+ && List.length def.A.signature.region_params = 0
+ && List.length def.A.signature.type_params = 0
+ && List.length def.A.signature.inputs = 0
(** Test all the unit functions in a list of function definitions *)
-let test_all_unit_functions (type_defs : T.type_def T.TypeDefId.vector)
- (fun_defs : A.fun_def A.FunDefId.vector) : unit =
+let test_all_unit_functions (type_defs : T.type_def list)
+ (fun_defs : A.fun_def list) : unit =
let test_fun (def : A.fun_def) : unit =
if fun_def_is_unit def then
match test_unit_function type_defs fun_defs def.A.def_id with
@@ -2610,4 +2538,4 @@ let test_all_unit_functions (type_defs : T.type_def T.TypeDefId.vector)
| Ok _ -> ()
else ()
in
- A.FunDefId.iter test_fun fun_defs
+ List.iter test_fun fun_defs
diff --git a/src/Modules.ml b/src/Modules.ml
index a2b1d3bf..3be1c742 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -15,7 +15,7 @@ type declaration =
type cfim_module = {
declarations : declaration list;
- types : type_def TypeDefId.vector;
- functions : fun_def FunDefId.vector;
+ types : type_def list;
+ functions : fun_def list;
}
(** CFIM module *)
diff --git a/src/Print.ml b/src/Print.ml
index 8547d5cb..bb172d5f 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -98,18 +98,15 @@ module Types = struct
let variant_to_string fmt (v : T.variant) : string =
v.variant_name ^ "("
- ^ String.concat ", "
- (List.map (field_to_string fmt) (T.FieldId.vector_to_list v.fields))
+ ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
^ ")"
let name_to_string (name : name) : string = String.concat "::" name
let type_def_to_string (type_def_id_to_string : T.TypeDefId.id -> string)
(def : T.type_def) : string =
- let regions : T.region_var list =
- T.RegionVarId.vector_to_list def.region_params
- in
- let types : T.type_var list = T.TypeVarId.vector_to_list def.type_params in
+ let regions = def.region_params in
+ let types = def.type_params in
let rid_to_string rid =
match List.find_opt (fun rv -> rv.T.rv_index = rid) regions with
| Some rv -> region_var_to_string rv
@@ -133,7 +130,6 @@ module Types = struct
in
match def.kind with
| T.Struct fields ->
- let fields = T.FieldId.vector_to_list fields in
if List.length fields > 0 then
let fields =
String.concat ","
@@ -142,7 +138,6 @@ module Types = struct
"struct " ^ name ^ params ^ "{" ^ fields ^ "}"
else "struct " ^ name ^ params ^ "{}"
| T.Enum variants ->
- let variants = T.VariantId.vector_to_list variants in
let variants =
List.map (fun v -> "| " ^ variant_to_string fmt v) variants
in
@@ -222,8 +217,9 @@ module Values = struct
| Some vid -> fmt.adt_variant_to_string av.def_id vid
| None -> fmt.type_def_id_to_string av.def_id
in
- let field_values = T.FieldId.vector_to_list av.field_values in
- let field_values = List.map (typed_value_to_string fmt) field_values in
+ let field_values =
+ List.map (typed_value_to_string fmt) av.field_values
+ in
if List.length field_values > 0 then
match fmt.adt_field_names av.V.def_id av.V.variant_id with
| None ->
@@ -240,7 +236,6 @@ module Values = struct
adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
| Tuple values ->
- let values = T.FieldId.vector_to_list values in
let values =
String.concat ", " (List.map (typed_value_to_string fmt) values)
in
@@ -302,7 +297,7 @@ module Values = struct
| Some vid -> fmt.adt_variant_to_string av.adef_id vid
| None -> fmt.type_def_id_to_string av.adef_id
in
- let field_values = T.FieldId.vector_to_list av.afield_values in
+ let field_values = av.afield_values in
if List.length field_values > 0 then
let field_values =
String.concat " "
@@ -311,7 +306,6 @@ module Values = struct
adt_ident ^ " " ^ field_values
else adt_ident
| ATuple values ->
- let values = T.FieldId.vector_to_list values in
let values =
String.concat ", " (List.map (typed_avalue_to_string fmt) values)
in
@@ -428,8 +422,7 @@ module Contexts = struct
let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter =
PV.value_to_rtype_formatter fmt
- let type_ctx_to_adt_variant_to_string_fun
- (ctx : T.type_def T.TypeDefId.vector) :
+ let type_ctx_to_adt_variant_to_string_fun (ctx : T.type_def list) :
T.TypeDefId.id -> T.VariantId.id -> string =
fun def_id variant_id ->
let def = T.TypeDefId.nth ctx def_id in
@@ -439,14 +432,14 @@ module Contexts = struct
let variant = T.VariantId.nth variants variant_id in
PT.name_to_string def.name ^ "::" ^ variant.variant_name
- let type_ctx_to_adt_field_names_fun (ctx : T.type_def T.TypeDefId.vector) :
+ let type_ctx_to_adt_field_names_fun (ctx : T.type_def list) :
T.TypeDefId.id -> T.VariantId.id option -> string list option =
fun def_id opt_variant_id ->
let def = T.TypeDefId.nth ctx def_id in
let fields = T.type_def_get_fields def opt_variant_id in
(* TODO: the field name should be optional?? *)
- let fields = T.FieldId.map (fun f -> f.T.field_name) fields in
- Some (T.FieldId.vector_to_list fields)
+ let fields = List.map (fun f -> f.T.field_name) fields in
+ Some fields
let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
(* We shouldn't use r_to_string *)
@@ -547,8 +540,8 @@ module CfimAst = struct
PT.type_def_id_to_string = fmt.type_def_id_to_string;
}
- let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def T.TypeDefId.vector)
- : T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
+ let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def list) :
+ T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
fun def_id opt_variant_id field_id ->
let def = T.TypeDefId.nth ctx def_id in
let fields = T.type_def_get_fields def opt_variant_id in
@@ -783,8 +776,8 @@ module CfimAst = struct
let name = PT.name_to_string def.A.name in
(* Region/type parameters *)
- let regions = T.RegionVarId.vector_to_list sg.region_params in
- let types = T.TypeVarId.vector_to_list sg.type_params in
+ let regions = sg.region_params in
+ let types = sg.type_params in
let params =
if List.length regions + List.length types = 0 then ""
else
@@ -794,14 +787,14 @@ module CfimAst = struct
in
(* Arguments *)
- let inputs = V.VarId.vector_to_list def.locals in
+ let inputs = def.locals in
let ret_var, inputs =
match inputs with
| [] -> failwith "Inconsistent signature"
| ret_var :: inputs -> (ret_var, inputs)
in
let inputs, _aux_locals = Utilities.list_split_at inputs def.arg_count in
- let args = List.combine inputs (V.VarId.vector_to_list sg.inputs) in
+ let args = List.combine inputs sg.inputs in
let args =
List.map
(fun (var, rty) -> PV.var_to_string var ^ " : " ^ rty_to_string rty)
@@ -821,7 +814,7 @@ module CfimAst = struct
(fun var ->
indent ^ indent_incr ^ PV.var_to_string var ^ " : "
^ ety_to_string var.var_ty ^ ";")
- (V.VarId.vector_to_list def.locals)
+ def.locals
in
let locals = String.concat "\n" locals in
@@ -841,8 +834,8 @@ module PA = CfimAst (* local module *)
module Module = struct
(** This function pretty-prints a type definition by using a definition
context *)
- let type_def_to_string (type_context : T.type_def T.TypeDefId.vector)
- (def : T.type_def) : string =
+ let type_def_to_string (type_context : T.type_def list) (def : T.type_def) :
+ string =
let type_def_id_to_string (id : T.TypeDefId.id) : string =
let def = T.TypeDefId.nth type_context id in
PT.name_to_string def.name
@@ -851,9 +844,8 @@ module Module = struct
(** Generate an [ast_formatter] by using a definition context in combination
with the variables local to a function's definition *)
- let def_ctx_to_ast_formatter (type_context : T.type_def T.TypeDefId.vector)
- (fun_context : A.fun_def A.FunDefId.vector) (def : A.fun_def) :
- PA.ast_formatter =
+ let def_ctx_to_ast_formatter (type_context : T.type_def list)
+ (fun_context : A.fun_def list) (def : A.fun_def) : PA.ast_formatter =
let r_to_string vid =
let var = T.RegionVarId.nth def.signature.region_params vid in
PT.region_var_to_string var
@@ -894,24 +886,18 @@ module Module = struct
(** This function pretty-prints a function definition by using a definition
context *)
- let fun_def_to_string (type_context : T.type_def T.TypeDefId.vector)
- (fun_context : A.fun_def A.FunDefId.vector) (def : A.fun_def) : string =
+ let fun_def_to_string (type_context : T.type_def list)
+ (fun_context : A.fun_def list) (def : A.fun_def) : string =
let fmt = def_ctx_to_ast_formatter type_context fun_context def in
PA.fun_def_to_string fmt "" " " def
let module_to_string (m : M.cfim_module) : string =
(* The types *)
- let type_defs =
- List.map
- (type_def_to_string m.M.types)
- (T.TypeDefId.vector_to_list m.M.types)
- in
+ let type_defs = List.map (type_def_to_string m.M.types) m.M.types in
(* The functions *)
let fun_defs =
- List.map
- (fun_def_to_string m.M.types m.M.functions)
- (A.FunDefId.vector_to_list m.M.functions)
+ List.map (fun_def_to_string m.M.types m.M.functions) m.M.functions
in
(* Put everything together *)
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 452b125f..b8c3edd9 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -54,17 +54,12 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
(** Instantiate the type variables in an ADT definition, and return the list
of types of the fields for the chosen variant *)
let type_def_get_instantiated_field_type (def : T.type_def)
- (opt_variant_id : T.VariantId.id option) (types : T.ety list) :
- T.ety T.FieldId.vector =
+ (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list =
let ty_subst =
- make_type_subst
- (List.map
- (fun x -> x.T.tv_index)
- (T.TypeVarId.vector_to_list def.T.type_params))
- types
+ make_type_subst (List.map (fun x -> x.T.tv_index) def.T.type_params) types
in
let fields = T.type_def_get_fields def opt_variant_id in
- T.FieldId.map
+ List.map
(fun f -> erase_regions_substitute_types ty_subst f.T.field_ty)
fields
@@ -72,7 +67,7 @@ let type_def_get_instantiated_field_type (def : T.type_def)
context *)
let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx)
(def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
- (types : T.ety list) : T.ety T.FieldId.vector =
+ (types : T.ety list) : T.ety list =
let def = C.ctx_lookup_type_def ctx def_id in
type_def_get_instantiated_field_type def opt_variant_id types
@@ -204,10 +199,10 @@ and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety)
(** Apply a type substitution to a function body. Return the local variables
and the body. *)
let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
- (def : A.fun_def) : V.var V.VarId.vector * A.expression =
+ (def : A.fun_def) : V.var list * A.expression =
let rsubst r = r in
let locals =
- V.VarId.map
+ List.map
(fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty })
def.A.locals
in
diff --git a/src/Types.ml b/src/Types.ml
index 77296ac1..2b57e3f7 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -90,19 +90,16 @@ type ety = erased_region ty [@@deriving show]
type field = { field_name : string; field_ty : rty } [@@deriving show]
-type variant = { variant_name : string; fields : field FieldId.vector }
-[@@deriving show]
+type variant = { variant_name : string; fields : field list } [@@deriving show]
-type type_def_kind =
- | Struct of field FieldId.vector
- | Enum of variant VariantId.vector
+type type_def_kind = Struct of field list | Enum of variant list
[@@deriving show]
type type_def = {
def_id : TypeDefId.id;
name : name;
- region_params : region_var RegionVarId.vector;
- type_params : type_var TypeVarId.vector;
+ region_params : region_var list;
+ type_params : type_var list;
kind : type_def_kind;
}
[@@deriving show]
@@ -137,7 +134,7 @@ let rec erase_regions (ty : rty) : ety =
Raises [Invalid_argument] if the arguments are incorrect.
*)
let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
- : field FieldId.vector =
+ : field list =
match (def.kind, opt_variant_id) with
| Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
| Struct fields, None -> fields
diff --git a/src/Values.ml b/src/Values.ml
index 9d1cb819..330f22d3 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -79,7 +79,7 @@ type symbolic_proj_comp = {
type value =
| Concrete of constant_value (** Concrete (non-symbolic) value *)
| Adt of adt_value (** Enumerations and structures *)
- | Tuple of typed_value FieldId.vector
+ | Tuple of typed_value list
(** Tuple - note that units are encoded as 0-tuples *)
| Bottom (** No value (uninitialized or moved value) *)
| Assumed of assumed_value (** Assumed types (Box, Vec, Cell...) *)
@@ -93,7 +93,7 @@ and adt_value = {
variant_id : VariantId.id option;
regions : erased_region list;
types : ety list;
- field_values : typed_value FieldId.vector;
+ field_values : typed_value list;
}
[@@deriving show]
@@ -138,7 +138,7 @@ type abstract_shared_borrows =
type avalue =
| AConcrete of constant_value
| AAdt of aadt_value
- | ATuple of typed_avalue FieldId.vector
+ | ATuple of typed_avalue list
| ABottom
| ALoan of aloan_content
| ABorrow of aborrow_content
@@ -151,7 +151,7 @@ and aadt_value = {
avariant_id : VariantId.id option;
aregions : erased_region list;
atypes : rty list;
- afield_values : typed_avalue FieldId.vector;
+ afield_values : typed_avalue list;
}
[@@deriving show]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 02:13:17 +0000