summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/InterpreterExpansion.ml4
-rw-r--r--src/Print.ml3
-rw-r--r--src/PrintPure.ml1
-rw-r--r--src/Pure.ml2
-rw-r--r--src/PureToExtract.ml4
-rw-r--r--src/PureUtils.ml6
-rw-r--r--src/Substitute.ml2
-rw-r--r--src/SymbolicToPure.ml8
-rw-r--r--src/Types.ml6
-rw-r--r--src/TypesAnalysis.ml56
-rw-r--r--src/TypesUtils.ml3
11 files changed, 60 insertions, 35 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 979ed780..0b65a372 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -686,7 +686,9 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
("Attempted to greedily expand a symbolic enumeration \
with > 1 variants (option \
[greedy_expand_symbolics_with_borrows] of [config]): "
- ^ Print.name_to_string def.name)));
+ ^ Print.name_to_string def.name))
+ | T.Opaque ->
+ raise (Failure "Attempted to greedily expand an opaque type"));
(* Also, we need to check if the definition is recursive *)
if C.ctx_type_decl_is_rec ctx def_id then
raise
diff --git a/src/Print.ml b/src/Print.ml
index e03efd94..c3c80da0 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -172,6 +172,7 @@ module Types = struct
in
let variants = String.concat "\n" variants in
"enum " ^ name ^ params ^ " =\n" ^ variants
+ | T.Opaque -> "opaque type " ^ name ^ params
end
module PT = Types (* local module *)
@@ -573,7 +574,7 @@ module Contexts = struct
fun def_id variant_id ->
let def = T.TypeDeclId.Map.find def_id ctx in
match def.kind with
- | Struct _ -> failwith "Unreachable"
+ | Struct _ | Opaque -> failwith "Unreachable"
| Enum variants ->
let variant = T.VariantId.nth variants variant_id in
name_to_string def.name ^ "::" ^ variant.variant_name
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index e96edeed..65b151a3 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -189,6 +189,7 @@ let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
in
let variants = String.concat "\n" variants in
"enum " ^ name ^ params ^ " =\n" ^ variants
+ | Opaque -> "opaque type " ^ name ^ params
let var_to_string (fmt : type_formatter) (v : var) : string =
let varname =
diff --git a/src/Pure.ml b/src/Pure.ml
index bbbf72a6..422292b1 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -116,7 +116,7 @@ type field = { field_name : string option; field_ty : ty } [@@deriving show]
type variant = { variant_name : string; fields : field list } [@@deriving show]
-type type_decl_kind = Struct of field list | Enum of variant list
+type type_decl_kind = Struct of field list | Enum of variant list | Opaque
[@@deriving show]
type type_var = T.type_var [@@deriving show]
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 4db5d2c5..2a00577e 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -392,7 +392,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| AdtId id -> (
let def = TypeDeclId.Map.find id type_decls in
match def.kind with
- | Struct _ -> failwith "Unreachable"
+ | Struct _ | Opaque -> failwith "Unreachable"
| Enum variants ->
let variant = VariantId.nth variants variant_id in
Print.name_to_string def.name ^ "::" ^ variant.variant_name)
@@ -409,7 +409,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| AdtId id -> (
let def = TypeDeclId.Map.find id type_decls in
match def.kind with
- | Enum _ -> failwith "Unreachable"
+ | Enum _ | Opaque -> failwith "Unreachable"
| Struct fields ->
let field = FieldId.nth fields field_id in
let field_name =
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index aa8d1f53..cfc8a270 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -102,7 +102,7 @@ let ty_as_integer (t : ty) : T.integer_type =
(* TODO: move *)
let type_decl_is_enum (def : T.type_decl) : bool =
- match def.kind with T.Struct _ -> false | Enum _ -> true
+ match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false
let mk_state_ty : ty = Adt (Assumed State, [])
@@ -186,8 +186,8 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
Raises [Invalid_argument] if the arguments are incorrect.
*)
-let type_decl_get_fields (def : type_decl) (opt_variant_id : VariantId.id option)
- : field list =
+let type_decl_get_fields (def : type_decl)
+ (opt_variant_id : VariantId.id option) : 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/Substitute.ml b/src/Substitute.ml
index 4a1f42eb..0bc612ea 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -120,6 +120,8 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
(fun i v -> (Some (T.VariantId.of_int i), v.T.fields))
variants
| T.Struct fields -> [ (None, fields) ]
+ | T.Opaque ->
+ raise (Failure "Can't retrieve the variants of an opaque type")
in
List.map
(fun (id, fields) ->
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 8f1eeb39..18b8f507 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -173,11 +173,12 @@ let get_instantiated_fun_sig (fun_id : A.fun_id)
(* Apply *)
fun_sig_substitute tsubst sg
-let bs_ctx_lookup_cfim_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl
- =
+let bs_ctx_lookup_cfim_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
+ T.type_decl =
TypeDeclId.Map.find id ctx.type_context.cfim_type_decls
-let bs_ctx_lookup_cfim_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl =
+let bs_ctx_lookup_cfim_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
+ =
FunDeclId.Map.find id ctx.fun_context.cfim_fun_decls
(* TODO: move *)
@@ -268,6 +269,7 @@ let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
match kind with
| T.Struct fields -> Struct (translate_fields fields)
| T.Enum variants -> Enum (translate_variants variants)
+ | T.Opaque -> Opaque
(** Translate a type definition from IM
diff --git a/src/Types.ml b/src/Types.ml
index 013f511d..5ff407c9 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -199,7 +199,11 @@ type field = { field_name : string option; field_ty : sty } [@@deriving show]
type variant = { variant_name : string; fields : field list } [@@deriving show]
-type type_decl_kind = Struct of field list | Enum of variant list
+type type_decl_kind =
+ | Struct of field list
+ | Enum of variant list
+ | Opaque
+ (** An opaque type: either a local type marked as opaque, or an external type *)
[@@deriving show]
type type_decl = {
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index d8895b55..e84b4f58 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -238,31 +238,41 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
(* Explore *)
analyze expl_info_init ty_info ty
+let type_decl_is_opaque (d : type_decl) : bool =
+ match d.kind with Struct _ | Enum _ -> false | Opaque -> true
+
let analyze_type_decl (updated : bool ref) (infos : type_infos)
(def : type_decl) : type_infos =
- (* Retrieve all the types of all the fields of all the variants *)
- let fields_tys : sty list =
- match def.kind with
- | Struct fields -> List.map (fun f -> f.field_ty) fields
- | Enum variants ->
- List.concat
- (List.map (fun v -> List.map (fun f -> f.field_ty) v.fields) variants)
- in
- (* Explore the types and accumulate information *)
- let r_is_static r = r = Static in
- let type_decl_info = TypeDeclId.Map.find def.def_id infos in
- let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in
- let type_decl_info =
- List.fold_left
- (fun type_decl_info ty ->
- analyze_full_ty r_is_static updated infos type_decl_info ty)
- type_decl_info fields_tys
- in
- let type_decl_info = partial_type_info_to_type_decl_info type_decl_info in
- (* Update the information for the type definition we explored *)
- let infos = TypeDeclId.Map.add def.def_id type_decl_info infos in
- (* Return *)
- infos
+ (* We analyze the type declaration only if it is not opaque (we need to explore
+ * the variants of the ADTs *)
+ if type_decl_is_opaque def then infos
+ else
+ (* Retrieve all the types of all the fields of all the variants *)
+ let fields_tys : sty list =
+ match def.kind with
+ | Struct fields -> List.map (fun f -> f.field_ty) fields
+ | Enum variants ->
+ List.concat
+ (List.map
+ (fun v -> List.map (fun f -> f.field_ty) v.fields)
+ variants)
+ | Opaque -> raise (Failure "unreachable")
+ in
+ (* Explore the types and accumulate information *)
+ let r_is_static r = r = Static in
+ let type_decl_info = TypeDeclId.Map.find def.def_id infos in
+ let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in
+ let type_decl_info =
+ List.fold_left
+ (fun type_decl_info ty ->
+ analyze_full_ty r_is_static updated infos type_decl_info ty)
+ type_decl_info fields_tys
+ in
+ let type_decl_info = partial_type_info_to_type_decl_info type_decl_info in
+ (* Update the information for the type definition we explored *)
+ let infos = TypeDeclId.Map.add def.def_id type_decl_info infos in
+ (* Return *)
+ infos
let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
(infos : type_infos) (decl : type_declaration_group) : type_infos =
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index e463fbc5..58bb4803 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -2,6 +2,9 @@ open Types
open Utils
module TA = TypesAnalysis
+let type_decl_is_opaque (d : type_decl) : bool =
+ match d.kind with Struct _ | Enum _ -> false | Opaque -> true
+
(** Retrieve the list of fields for the given variant of a [type_decl].
Raises [Invalid_argument] if the arguments are incorrect.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 18:16:16 +0000