From 778918ad5157da7d2651b7d47584031d6b054794 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 1 Aug 2022 23:04:13 +0200
Subject: [PATCH] [kernel] export module type S of Logic_typing.Make
application to enable first class modules usage
---
.../ast_queries/logic_parse_string.ml | 139 ++++++++----------
.../ast_queries/logic_typing.ml | 20 +++
.../ast_queries/logic_typing.mli | 94 ++++++------
3 files changed, 133 insertions(+), 120 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_parse_string.ml b/src/kernel_services/ast_queries/logic_parse_string.ml
index 1b1308c18a1..9f5340c8e6d 100644
--- a/src/kernel_services/ast_queries/logic_parse_string.ml
+++ b/src/kernel_services/ast_queries/logic_parse_string.ml
@@ -70,69 +70,67 @@ let find_var kf kinstr ?label var =
(** Create a logic typer, the interpretation being done for the given
kernel_function and stmt (the stmt is used check that loop invariants
are allowed). *)
-(* It is theoretically possible to use a first-class module instead, but the
- required signatures are not exported in Logic_typing. *)
-module DefaultLT (X:
- sig
- val kf: Kernel_function.t
- val kinstr: Cil_types.kinstr
- end) =
- Logic_typing.Make
- (struct
- let anonCompFieldName = Cabs2cil.anonCompFieldName
- let conditionalConversion = Cabs2cil.logicConditionalConversion
-
- let is_loop () =
- match X.kinstr with
- | Kglobal -> false
- | Kstmt s -> Kernel_function.stmt_in_loop X.kf s
-
- let find_macro _ = raise Not_found
-
- let find_var ?label var = find_var X.kf X.kinstr ?label var
-
- let find_enum_tag x =
- try
- Globals.Types.find_enum_tag x
- with Not_found ->
- (* The ACSL typer tries to parse a string, first as a variable,
- then as an enum. We report the "Unbound variable" message
- here, as it is nicer for the user. However, this short-circuits
- the later stages of resolution, for example global logic
- variables. *)
- raise (Unbound ("Unbound variable " ^ x))
-
- let find_comp_field info s =
- let field = Cil.getCompField info s in
- Field(field,NoOffset)
-
- let find_type = Globals.Types.find_type
-
- let find_label s = Kernel_function.find_label X.kf s
- include Logic_env
-
- let add_logic_function =
- add_logic_function_gen Logic_utils.is_same_logic_profile
-
- let remove_logic_info =
- remove_logic_info_gen Logic_utils.is_same_logic_profile
-
- let integral_cast ty t =
- raise
- (Failure
- (Format.asprintf
- "term %a has type %a, but %a is expected."
- Printer.pp_term t
- Printer.pp_logic_type Linteger
- Printer.pp_typ ty))
-
- let error loc msg =
- Pretty_utils.ksfprintf (fun e -> raise (Error (loc, e))) msg
-
- let on_error f rollback x =
- try f x with Error (loc,msg) as exn -> rollback (loc,msg); raise exn
-
- end)
+
+let default_typer kf kinstr =
+ let module LT = Logic_typing.Make
+ (struct
+ let anonCompFieldName = Cabs2cil.anonCompFieldName
+ let conditionalConversion = Cabs2cil.logicConditionalConversion
+
+ let is_loop () =
+ match kinstr with
+ | Kglobal -> false
+ | Kstmt s -> Kernel_function.stmt_in_loop kf s
+
+ let find_macro _ = raise Not_found
+
+ let find_var ?label var = find_var kf kinstr ?label var
+
+ let find_enum_tag x =
+ try
+ Globals.Types.find_enum_tag x
+ with Not_found ->
+ (* The ACSL typer tries to parse a string, first as a variable,
+ then as an enum. We report the "Unbound variable" message
+ here, as it is nicer for the user. However, this short-circuits
+ the later stages of resolution, for example global logic
+ variables. *)
+ raise (Unbound ("Unbound variable " ^ x))
+
+ let find_comp_field info s =
+ let field = Cil.getCompField info s in
+ Field(field,NoOffset)
+
+ let find_type = Globals.Types.find_type
+
+ let find_label s = Kernel_function.find_label kf s
+ include Logic_env
+
+ let add_logic_function =
+ add_logic_function_gen Logic_utils.is_same_logic_profile
+
+ let remove_logic_info =
+ remove_logic_info_gen Logic_utils.is_same_logic_profile
+
+ let integral_cast ty t =
+ raise
+ (Failure
+ (Format.asprintf
+ "term %a has type %a, but %a is expected."
+ Printer.pp_term t
+ Printer.pp_logic_type Linteger
+ Printer.pp_typ ty))
+
+ let error loc msg =
+ Pretty_utils.ksfprintf (fun e -> raise (Error (loc, e))) msg
+
+ let on_error f rollback x =
+ try f x with Error (loc,msg) as exn -> rollback (loc,msg); raise exn
+
+ end)
+ in
+ (module LT : Logic_typing.S)
+
(** Set up the parser for the infamous 'C hack' needed to parse typedefs *)
let sync_typedefs () =
@@ -148,10 +146,7 @@ let wrap f parsetree loc =
let code_annot kf stmt s =
sync_typedefs ();
- let module LT = DefaultLT(struct
- let kf = kf
- let kinstr = Kstmt stmt
- end) in
+ let module LT = (val default_typer kf (Kstmt stmt) : Logic_typing.S) in
let loc = Stmt.loc stmt in
let pa =
Option.bind
@@ -171,10 +166,7 @@ let default_term_env () =
let term kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
- let module LT = DefaultLT(struct
- let kf = kf
- let kinstr = Kglobal
- end) in
+ let module LT = (val default_typer kf Kglobal : Logic_typing.S) in
let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.term env pa_expr in
wrap parse pa_expr loc
@@ -186,10 +178,7 @@ let term_lval kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
let predicate kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
- let module LT = DefaultLT(struct
- let kf = kf
- let kinstr = Kglobal
- end) in
+ let module LT = (val default_typer kf Kglobal : Logic_typing.S) in
let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.predicate env pa_expr in
wrap parse pa_expr loc
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index cdc7e48ad02..9de89b3bbd5 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -625,6 +625,26 @@ let is_plain_pointer_type t =
let is_array_type = plain_or_set is_plain_array_type
let is_pointer_type = plain_or_set is_plain_pointer_type
+module type S =
+sig
+ val type_of_field:
+ location -> string -> Cil_types.logic_type ->
+ (term_offset * Cil_types.logic_type)
+ val mk_cast:
+ ?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
+ val term : Lenv.t -> Logic_ptree.lexpr -> term
+ val predicate : Lenv.t -> Logic_ptree.lexpr -> predicate
+ val code_annot :
+ Cil_types.location -> string list ->
+ Cil_types.logic_type -> Logic_ptree.code_annot -> code_annotation
+ val type_annot : location -> Logic_ptree.type_annot -> logic_info
+ val model_annot : location -> Logic_ptree.model_annot -> model_info
+ val annot : Logic_ptree.decl -> global_annotation
+ val funspec :
+ string list ->
+ varinfo -> (varinfo list) option -> typ -> Logic_ptree.spec -> funspec
+end
+
module Make
(C:
sig
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index ef8c2d3c9ff..a9ee8eed4a1 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -147,52 +147,8 @@ type typing_context = {
*)
}
-module Make
- (C :
- sig
- val is_loop: unit -> bool
- (** whether the annotation we want to type is contained in a loop.
- Only useful when creating objects of type [code_annotation]. *)
-
- val anonCompFieldName : string
- val conditionalConversion : typ -> typ -> typ
- val find_macro : string -> Logic_ptree.lexpr
- val find_var : ?label:string -> string -> logic_var
- (** see corresponding field in {!Logic_typing.typing_context}. *)
-
- val find_enum_tag : string -> exp * typ
- val find_type : type_namespace -> string -> typ
- val find_comp_field: compinfo -> string -> offset
- val find_label : string -> stmt ref
-
- val remove_logic_function : string -> unit
- val remove_logic_info: logic_info -> unit
- val remove_logic_type: string -> unit
- val remove_logic_ctor: string -> unit
-
- val add_logic_function: logic_info -> unit
- val add_logic_type: string -> logic_type_info -> unit
- val add_logic_ctor: string -> logic_ctor_info -> unit
-
- val find_all_logic_functions : string -> Cil_types.logic_info list
- val find_logic_type: string -> logic_type_info
- val find_logic_ctor: string -> logic_ctor_info
- (** What to do when we have a term of type Integer in a context
- expecting a C integral type.
- @raise Failure to reject such conversion
- @since Nitrogen-20111001
- *)
- val integral_cast: Cil_types.typ -> Cil_types.term -> Cil_types.term
-
- (** raises an error at the given location and with the given message.
- @since Magnesium-20151001 *)
- val error: location -> ('a,Format.formatter,unit, 'b) format4 -> 'a
-
- (** see {!Logic_typing.typing_context}. *)
- val on_error: ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
-
- end) :
+module type S =
sig
(** @since Nitrogen-20111001 *)
@@ -245,6 +201,54 @@ sig
end
+module Make
+ (C :
+ sig
+ val is_loop: unit -> bool
+ (** whether the annotation we want to type is contained in a loop.
+ Only useful when creating objects of type [code_annotation]. *)
+
+ val anonCompFieldName : string
+ val conditionalConversion : typ -> typ -> typ
+ val find_macro : string -> Logic_ptree.lexpr
+ val find_var : ?label:string -> string -> logic_var
+ (** see corresponding field in {!Logic_typing.typing_context}. *)
+
+ val find_enum_tag : string -> exp * typ
+ val find_type : type_namespace -> string -> typ
+ val find_comp_field: compinfo -> string -> offset
+ val find_label : string -> stmt ref
+
+ val remove_logic_function : string -> unit
+ val remove_logic_info: logic_info -> unit
+ val remove_logic_type: string -> unit
+ val remove_logic_ctor: string -> unit
+
+ val add_logic_function: logic_info -> unit
+ val add_logic_type: string -> logic_type_info -> unit
+ val add_logic_ctor: string -> logic_ctor_info -> unit
+
+ val find_all_logic_functions : string -> Cil_types.logic_info list
+ val find_logic_type: string -> logic_type_info
+ val find_logic_ctor: string -> logic_ctor_info
+
+ (** What to do when we have a term of type Integer in a context
+ expecting a C integral type.
+ @raise Failure to reject such conversion
+ @since Nitrogen-20111001
+ *)
+ val integral_cast: Cil_types.typ -> Cil_types.term -> Cil_types.term
+
+ (** raises an error at the given location and with the given message.
+ @since Magnesium-20151001 *)
+ val error: location -> ('a,Format.formatter,unit, 'b) format4 -> 'a
+
+ (** see {!Logic_typing.typing_context}. *)
+ val on_error: ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
+
+ end) : S
+
+
(** append the Old and Post labels in the environment *)
val append_old_and_post_labels: Lenv.t -> Lenv.t
--
GitLab