From eeac69419158552ef455a4197e78567837c546ca Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 3 Mar 2022 12:22:30 +0100 Subject: Add an Opaque variant to type_decl_kind and start updating the code --- src/InterpreterExpansion.ml | 4 +++- src/Print.ml | 3 ++- src/PrintPure.ml | 1 + src/Pure.ml | 2 +- src/PureToExtract.ml | 4 ++-- src/PureUtils.ml | 6 ++--- src/Substitute.ml | 2 ++ src/SymbolicToPure.ml | 8 ++++--- src/Types.ml | 6 ++++- src/TypesAnalysis.ml | 56 ++++++++++++++++++++++++++------------------- src/TypesUtils.ml | 3 +++ 11 files changed, 60 insertions(+), 35 deletions(-) (limited to 'src') 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. -- cgit v1.2.3