From dcdc0edecaaf0b160670cbeff4c792ef4503d417 Mon Sep 17 00:00:00 2001 From: Zain K Aamer Date: Wed, 11 Sep 2024 14:42:57 -0400 Subject: [PATCH] [CN-Exec] Adding `cn_internal_to_ail.mli` (#561) * [AIL] Name `sigma` member types * [CN-Exec] Minor cleanup * [CN-Exec] Add `cn_internal_to_ail.mli` --- backend/cn/lib/cn_internal_to_ail.ml | 82 +++++++----- backend/cn/lib/cn_internal_to_ail.mli | 140 +++++++++++++++++++++ backend/cn/lib/executable_spec_internal.ml | 4 +- frontend/model/ail/ailSyntax.lem | 70 +++++++++-- 4 files changed, 249 insertions(+), 47 deletions(-) create mode 100644 backend/cn/lib/cn_internal_to_ail.mli diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index acf0b6490..1a6f3ddaf 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -13,6 +13,7 @@ open Mucore module A = CF.AilSyntax module C = CF.Ctype module BT = BaseTypes +module IT = IndexTerms module T = Terms module LRT = LogicalReturnTypes module LAT = LogicalArgumentTypes @@ -21,12 +22,6 @@ module OE = Ownership_exec let true_const = A.AilEconst (ConstantPredefined PConstantTrue) -let error_msg_info_sym = Sym.fresh_pretty "error_msg_info" - -let error_msg_struct_tag = Sym.fresh_pretty "cn_error_message_info" - -let error_msg_info_ctype = mk_ctype (C.Struct error_msg_struct_tag) - let ownership_ctypes = ref [] let rec cn_base_type_to_bt = function @@ -90,12 +85,6 @@ let members_equal ms ms' = ctypes_eq && ids_eq) -module SymKey = struct - type t = C.union_tag - - let compare (x : t) y = Sym.compare_sym x y -end - module RecordMap = Map.Make (MembersKey) let records = ref RecordMap.empty @@ -713,7 +702,9 @@ let empty_for_dest : type a. a dest -> a = | PassBack -> ([], [], mk_expr empty_ail_expr) -let generate_ownership_function with_ownership_checking ctype = +let generate_ownership_function ~with_ownership_checking ctype + : A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition + = let ctype_str = str_of_ctype ctype in (* Printf.printf ("ctype_str: %s\n") ctype_str; *) let ctype_str = String.concat "_" (String.split_on_char ' ' ctype_str) in @@ -1493,6 +1484,17 @@ let cn_to_ail_expr_internal fun dts globals cn_expr d -> cn_to_ail_expr_aux_internal None None dts globals cn_expr d +let cn_to_ail_expr + (dts : _ CF.Cn.cn_datatype list) + (globals : (C.union_tag * C.ctype) list) + (it : IT.t) + : A.bindings + * CF.GenTypes.genTypeCategory A.statement_ list + * CF.GenTypes.genTypeCategory A.expression + = + cn_to_ail_expr_internal dts globals it PassBack + + let cn_to_ail_expr_internal_with_pred_name : type a. Sym.sym option -> @@ -1606,7 +1608,9 @@ let generate_map_get sym = [ (decl, def) ] -let cn_to_ail_datatype ?(first = false) (cn_datatype : cn_datatype) = +let cn_to_ail_datatype ?(first = false) (cn_datatype : cn_datatype) + : Locations.t * A.sigma_tag_definition list + = let enum_sym = generate_sym_with_suffix cn_datatype.cn_dt_name in let constructor_syms = List.map fst cn_datatype.cn_dt_cases in let generate_enum_member sym = @@ -1679,7 +1683,9 @@ let cn_to_ail_datatype ?(first = false) (cn_datatype : cn_datatype) = (cn_datatype.cn_dt_magic_loc, enum :: structs) -let generate_datatype_equality_function (cn_datatype : cn_datatype) = +let generate_datatype_equality_function (cn_datatype : cn_datatype) + : (A.sigma_declaration * 'a A.sigma_function_definition) list + = (* type cn_datatype 'a = <| cn_dt_loc: Loc.t; @@ -1956,8 +1962,8 @@ let generate_datatype_default_function (cn_datatype : cn_datatype) = let generate_struct_equality_function ?(is_record = false) dts - ((sym, (loc, attrs, tag_def)) : - A.ail_identifier * (Cerb_location.t * CF.Annot.attributes * C.tag_definition)) + ((sym, (loc, attrs, tag_def)) : A.sigma_tag_definition) + : (A.sigma_declaration * 'a A.sigma_function_definition) list = match tag_def with | C.StructDef (members, _) -> @@ -2066,8 +2072,8 @@ let generate_struct_equality_function let generate_struct_default_function ?(is_record = false) dts - ((sym, (loc, attrs, tag_def)) : - A.ail_identifier * (Cerb_location.t * CF.Annot.attributes * C.tag_definition)) + ((sym, (loc, attrs, tag_def)) : A.sigma_tag_definition) + : (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list = match tag_def with | C.StructDef (members, _) -> @@ -2135,9 +2141,8 @@ let generate_struct_default_function | C.UnionDef _ -> [] -let generate_struct_map_get - ((sym, (loc, attrs, tag_def)) : - A.ail_identifier * (Cerb_location.t * CF.Annot.attributes * C.tag_definition)) +let generate_struct_map_get ((sym, (loc, attrs, tag_def)) : A.sigma_tag_definition) + : (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list = match tag_def with | C.StructDef _ -> @@ -2147,8 +2152,8 @@ let generate_struct_map_get let generate_struct_conversion_function - ((sym, (loc, attrs, tag_def)) : - A.ail_identifier * (Cerb_location.t * CF.Annot.attributes * C.tag_definition)) + ((sym, (loc, attrs, tag_def)) : A.sigma_tag_definition) + : (A.sigma_declaration * 'a A.sigma_function_definition) list = match tag_def with | C.StructDef (members, _) -> @@ -2210,7 +2215,9 @@ let generate_struct_conversion_function (* RECORDS *) -let generate_record_equality_function dts (sym, (members : BT.member_types)) = +let generate_record_equality_function dts (sym, (members : BT.member_types)) + : (A.sigma_declaration * 'a A.sigma_function_definition) list + = let cn_sym = sym in let cn_struct_ctype = mk_ctype C.(Struct cn_sym) in let cn_struct_ptr_ctype = mk_ctype C.(Pointer (empty_qualifiers, cn_struct_ctype)) in @@ -2300,7 +2307,9 @@ let generate_record_equality_function dts (sym, (members : BT.member_types)) = [ (decl, def) ] -let generate_record_default_function dts (sym, (members : BT.member_types)) = +let generate_record_default_function dts (sym, (members : BT.member_types)) + : (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + = let cn_sym = sym in let fn_str = "default_struct_" ^ Sym.pp_string cn_sym in let cn_struct_ctype = mk_ctype C.(Struct cn_sym) in @@ -2362,9 +2371,8 @@ let generate_record_default_function dts (sym, (members : BT.member_types)) = let generate_record_map_get (sym, _) = generate_map_get sym -let cn_to_ail_struct - ((sym, (loc, attrs, tag_def)) : - A.ail_identifier * (Cerb_location.t * CF.Annot.attributes * C.tag_definition)) +let cn_to_ail_struct ((sym, (loc, attrs, tag_def)) : A.sigma_tag_definition) + : A.sigma_tag_definition list = match tag_def with | C.StructDef (members, opt) -> @@ -2749,8 +2757,11 @@ let rec generate_record_opt pred_sym = function (* TODO: Finish with rest of function - maybe header file with A.Decl_function (cn.h?) *) let cn_to_ail_function_internal (fn_sym, (lf_def : LogicalFunctions.definition)) - cn_datatypes - cn_functions + (cn_datatypes : A.sigma_cn_datatype list) + (cn_functions : A.sigma_cn_function list) + : ((Locations.t * A.sigma_declaration) + * CF.GenTypes.genTypeCategory A.sigma_function_definition option) + * A.sigma_tag_definition option = let ret_type = bt_to_ail_ctype ~pred_sym:(Some fn_sym) lf_def.return_bt in (* let ret_type = mk_ctype C.(Pointer (empty_qualifiers, ret_type)) in *) @@ -2927,7 +2938,12 @@ let cn_to_ail_predicate_internal (((loc, decl), def), ail_record_opt) -let rec cn_to_ail_predicates_internal pred_def_list dts globals preds cn_preds = +let rec cn_to_ail_predicates_internal pred_def_list dts globals preds cn_preds + : ((Locations.t * A.sigma_declaration) + * CF.GenTypes.genTypeCategory A.sigma_function_definition) + list + * A.sigma_tag_definition option list + = match pred_def_list with | [] -> ([], []) | p :: ps -> @@ -3215,7 +3231,7 @@ let rec cn_to_ail_pre_post_aux_internal cn_to_ail_lat_internal_2 with_ownership_checking dts globals preds c_return_type lat -let cn_to_ail_pre_post_internal with_ownership_checking dts preds globals c_return_type +let cn_to_ail_pre_post_internal ~with_ownership_checking dts preds globals c_return_type = function | Some internal -> let ail_executable_spec = diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli new file mode 100644 index 000000000..389261f03 --- /dev/null +++ b/backend/cn/lib/cn_internal_to_ail.mli @@ -0,0 +1,140 @@ +module CF = Cerb_frontend +module A = CF.AilSyntax +module C = CF.Ctype +module BT = BaseTypes +module AT = ArgumentTypes +module IT = IndexTerms + +val ownership_ctypes : C.ctype list ref + +module MembersKey : sig + type t = (Id.t * Sym.t CF.Cn.cn_base_type) list + + val compare : t -> t -> int +end + +module RecordMap : module type of Map.Make (MembersKey) + +val records : Sym.t RecordMap.t ref + +val bt_to_cn_base_type : BT.t -> Sym.t CF.Cn.cn_base_type + +val bt_to_ail_ctype : ?pred_sym:Sym.t option -> BT.t -> C.ctype + +val wrap_with_convert_from_cn_bool + : CF.GenTypes.genTypeCategory A.expression -> + CF.GenTypes.genTypeCategory A.expression + +val generate_sym_with_suffix + : ?suffix:string -> + ?uppercase:bool -> + ?lowercase:bool -> + Sym.t -> + Sym.t + +type ail_bindings_and_statements = + A.bindings * CF.GenTypes.genTypeCategory A.statement_ list + +type ail_executable_spec = + { pre : ail_bindings_and_statements; + post : ail_bindings_and_statements; + in_stmt : (Locations.t * ail_bindings_and_statements) list + } + +val generate_ownership_function + : with_ownership_checking:bool -> + C.ctype -> + A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition + +val generate_datatype_equality_function + : A.sigma_cn_datatype -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_datatype_map_get + : Compile.cn_datatype -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_datatype_default_function + : Compile.cn_datatype -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_struct_conversion_function + : A.sigma_tag_definition -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_struct_equality_function + : ?is_record:bool -> + 'a -> + A.sigma_tag_definition -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_struct_map_get + : A.sigma_tag_definition -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_struct_default_function + : ?is_record:bool -> + 'a -> + A.sigma_tag_definition -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_record_equality_function + : 'a -> + Sym.t * BT.member_types -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_record_default_function + : 'a -> + Sym.t * BT.member_types -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val generate_record_map_get + : Sym.t * 'a -> + (A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list + +val cn_to_ail_expr + : A.sigma_cn_datatype list -> + (C.union_tag * C.ctype) list -> + IT.t -> + A.bindings + * CF.GenTypes.genTypeCategory A.statement_ list + * CF.GenTypes.genTypeCategory A.expression + +val cn_to_ail_struct : A.sigma_tag_definition -> A.sigma_tag_definition list + +val cn_to_ail_datatype + : ?first:bool -> + A.sigma_cn_datatype -> + Locations.t * A.sigma_tag_definition list + +val cn_to_ail_pred_records + : (MembersKey.t * A.ail_identifier) list -> + A.sigma_tag_definition list + +val cn_to_ail_function_internal + : Sym.t * LogicalFunctions.definition -> + A.sigma_cn_datatype list -> + A.sigma_cn_function list -> + ((Locations.t * A.sigma_declaration) + * CF.GenTypes.genTypeCategory A.sigma_function_definition option) + * A.sigma_tag_definition option + +val cn_to_ail_predicates_internal + : (Sym.t * ResourcePredicates.definition) list -> + A.sigma_cn_datatype list -> + (Sym.t * C.ctype) list -> + Mucore.T.resource_predicates -> + A.sigma_cn_predicate list -> + ((Locations.t * A.sigma_declaration) + * CF.GenTypes.genTypeCategory A.sigma_function_definition) + list + * A.sigma_tag_definition option list + +val cn_to_ail_pre_post_internal + : with_ownership_checking:bool -> + A.sigma_cn_datatype list -> + Mucore.T.resource_predicates -> + (Sym.t * C.ctype) list -> + C.ctype -> + Core_to_mucore.fn_spec_instrumentation option -> + ail_executable_spec diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index 5afb56c67..786ee3f4c 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -94,7 +94,7 @@ let generate_c_pres_and_posts_internal let globals = extract_global_variables prog5.mu_globs in let ail_executable_spec = Cn_internal_to_ail.cn_to_ail_pre_post_internal - with_ownership_checking + ~with_ownership_checking dts preds globals @@ -564,7 +564,7 @@ let generate_ownership_functions let ail_funs = List.map (fun ctype -> - Cn_internal_to_ail.generate_ownership_function with_ownership_checking ctype) + Cn_internal_to_ail.generate_ownership_function ~with_ownership_checking ctype) ctypes in let decls, defs = List.split ail_funs in diff --git a/frontend/model/ail/ailSyntax.lem b/frontend/model/ail/ailSyntax.lem index 1ea376198..99d5198bb 100644 --- a/frontend/model/ail/ailSyntax.lem +++ b/frontend/model/ail/ailSyntax.lem @@ -240,22 +240,68 @@ type id_kind = | IK_tentative | IK_definition +type sigma_declaration = + ail_identifier * (Loc.t * Annot.attributes * declaration) + +type sigma_object_definition 'a = + ail_identifier * (expression 'a) + +type sigma_function_definition 'a = + ail_identifier * (Loc.t * nat * Annot.attributes * list ail_identifier * statement 'a) + +type sigma_static_assertion 'a = + expression 'a * stringLiteral + +type sigma_tag_definition = + ail_identifier * (Loc.t * Annot.attributes * tag_definition) + +type sigma_extern_id = ail_identifier * id_kind + +type sigma_cn_function = Cn.cn_function Symbol.sym Ctype.ctype + +type sigma_cn_lemmata = Cn.cn_lemma Symbol.sym Ctype.ctype + +type sigma_cn_predicate = Cn.cn_predicate Symbol.sym Ctype.ctype + +type sigma_cn_datatype = Cn.cn_datatype Symbol.sym + +type sigma_cn_fun_spec = nat * Cn.cn_fun_spec Symbol.sym Ctype.ctype + +type sigma_cn_ident = Cn.cn_namespace * Symbol.identifier + type sigma 'a = <| - declarations: list (ail_identifier * (Loc.t * Annot.attributes * declaration)); - object_definitions: list (ail_identifier * (expression 'a)); + declarations: list sigma_declaration; + object_definitions: list (sigma_object_definition 'a); (* the list of identifiers are the parameter names used in the body *) - function_definitions: list (ail_identifier * (Loc.t * nat * Annot.attributes * list ail_identifier * statement 'a)); - static_assertions: list (expression 'a * stringLiteral); - tag_definitions: list (ail_identifier * (Loc.t * Annot.attributes * tag_definition)); - extern_idmap: map Symbol.identifier (ail_identifier * id_kind); + function_definitions: list (sigma_function_definition 'a); + static_assertions: list (sigma_static_assertion 'a); + tag_definitions: list sigma_tag_definition; + extern_idmap: map Symbol.identifier sigma_extern_id; typedef_attributes: map ail_identifier Annot.attributes; loop_attributes: Annot.loop_attributes; - cn_functions: list (Cn.cn_function Symbol.sym Ctype.ctype); - cn_lemmata: list (Cn.cn_lemma Symbol.sym Ctype.ctype); - cn_predicates: list (Cn.cn_predicate Symbol.sym Ctype.ctype); - cn_datatypes: list (Cn.cn_datatype Symbol.sym); - cn_fun_specs: list (nat * Cn.cn_fun_spec Symbol.sym Ctype.ctype); - cn_idents: map (Cn.cn_namespace * Symbol.identifier) Symbol.sym; + cn_functions: list sigma_cn_function; + cn_lemmata: list sigma_cn_lemmata; + cn_predicates: list sigma_cn_predicate; + cn_datatypes: list sigma_cn_datatype; + cn_fun_specs: list sigma_cn_fun_spec; + cn_idents: map sigma_cn_ident Symbol.sym; +|> + +let empty_sigma : sigma 'a = <| + declarations = []; + object_definitions = []; + function_definitions = []; + static_assertions = []; + tag_definitions = []; + extern_idmap = Map.empty; + typedef_attributes = Map.empty; + loop_attributes = Map.empty; + cn_functions = []; + cn_lemmata = []; + cn_predicates = []; + cn_datatypes = []; + cn_fun_specs = []; + cn_idents = Map.empty; |>