From 413a083f8e10babfe0cc7ecf49a0cf8a470ab16b Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 9 Sep 2024 11:48:42 +0200
Subject: [PATCH] [kernel] Allow plugins to register importers with the same
name
---
src/kernel_internals/parsing/logic_lexer.mll | 43 ++++++++++---
src/kernel_internals/parsing/logic_parser.mly | 26 ++++++--
src/kernel_services/ast_data/cil_types.ml | 4 +-
.../ast_printing/cil_printer.ml | 15 ++++-
.../ast_printing/cil_types_debug.ml | 7 +-
.../ast_printing/logic_print.ml | 10 ++-
.../ast_queries/acsl_extension.ml | 64 +++++++++++++------
.../ast_queries/acsl_extension.mli | 13 ++--
src/kernel_services/ast_queries/logic_env.ml | 11 +++-
src/kernel_services/ast_queries/logic_env.mli | 10 ++-
.../ast_queries/logic_typing.ml | 21 +++---
.../ast_queries/logic_typing.mli | 7 +-
src/kernel_services/parsetree/logic_ptree.ml | 2 +-
13 files changed, 174 insertions(+), 59 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 8d36a9ae06..994df65e39 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -190,22 +190,25 @@
with Not_found ->
let res =
match Logic_env.extension_category ~plugin s with
- | exception Not_found -> None
- | Cil_types.Ext_contract -> Some (EXT_CONTRACT (s, plugin))
- | Cil_types.Ext_global ->
+ | exception Not_found ->
begin
- match Logic_env.is_extension_block ~plugin s with
- | false -> Some (EXT_GLOBAL (s, plugin))
- | true -> Some (EXT_GLOBAL_BLOCK (s, plugin))
+ match Logic_env.is_importer ~plugin s, plugin with
+ | false, _ -> None
+ | true, None -> Some (EXT_IMPORTER s)
+ | true, Some _ -> Some (EXT_IMPORTER_PLUGIN (s, plugin))
end
+ | Cil_types.Ext_contract -> Some (EXT_CONTRACT (s, plugin))
+ | Cil_types.Ext_global ->
+ if Logic_env.is_extension_block ~plugin s
+ then Some (EXT_GLOBAL_BLOCK (s, plugin))
+ else Some (EXT_GLOBAL (s, plugin))
| Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT (s, plugin))
in
match res with
| None ->
if Logic_env.typename_status s then TYPENAME s
else
- (try
- Hashtbl.find type_kw s
+ (try Hashtbl.find type_kw s
with Not_found -> IDENTIFIER s)
| Some lex -> lex
),
@@ -325,6 +328,24 @@
syntax \\kernel::%s" s s;
tok
| _ -> raise Parsing.Parse_error
+
+ let check_ext_importer source plugin tok =
+ match tok with
+ | IDENTIFIER s ->
+ if Plugin.is_present plugin then
+ Kernel.warning ~once:true ~wkey:Kernel.wkey_extension_unknown ~source
+ "Ignoring unregistered importer extension '%s' of plug-in %s" s plugin
+ else
+ Kernel.warning ~once:true ~wkey:Kernel.wkey_plugin_not_loaded ~source
+ "Ignoring importer extension '%s' for unloaded plug-in %s" s plugin;
+ IDENTIFIER_IMPORTER s
+ | EXT_IMPORTER_PLUGIN (s, _) ->
+ if String.equal plugin "kernel" then
+ Kernel.abort ~source
+ "Extension importer '%s' from frama-c's kernel should not be used \
+ with the syntax \\kernel::%s" s s;
+ tok
+ | _ -> raise Parsing.Parse_error
}
let space = [' ' '\t' '\012' '\r' '@' ]
@@ -372,6 +393,12 @@ rule token = parse
then comment lexbuf
else lex_error lexbuf "unexpected block-comment opening"
}
+ | '\\' (rIdentifier as plugin) "::" (rIdentifier as name) ":" {
+ let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
+ let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
+ let tok = identifier ~plugin:(Some plugin) name cabsloc in
+ check_ext_importer (fst cabsloc) plugin tok
+ }
| '\\' (rIdentifier as plugin) "::" (rIdentifier as name) {
let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 6c6b4e299c..d7671bfea0 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -269,7 +269,7 @@
%token EXT_SPEC_MODULE EXT_SPEC_FUNCTION EXT_SPEC_CONTRACT EXT_SPEC_INCLUDE
%token EXT_SPEC_AT EXT_SPEC_LET
-%token <string> LONGIDENT IDENTIFIER TYPENAME IDENTIFIER_EXT
+%token <string> LONGIDENT IDENTIFIER TYPENAME IDENTIFIER_EXT IDENTIFIER_IMPORTER
%token <bool*string> STRING_LITERAL
%token <string> INT_CONSTANT
%token <string> FLOAT_CONSTANT
@@ -290,7 +290,8 @@
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
%token ADMIT_REQUIRES ADMIT_LOOP ADMIT_INVARIANT ADMIT_LEMMA
%token ADMIT_ENSURES ADMIT_EXITS ADMIT_CONTINUES ADMIT_BREAKS ADMIT_RETURNS
-%token <string * string option> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
+%token <string> EXT_IMPORTER
+%token <string * string option> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT EXT_IMPORTER_PLUGIN
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
%token LOGIC PREDICATE INDUCTIVE AXIOM LEMMA LBRACE RBRACE
@@ -952,7 +953,10 @@ full_identifier:
| id = EXT_CONTRACT { fst id }
| id = EXT_GLOBAL { fst id }
| id = EXT_GLOBAL_BLOCK { fst id }
+| id = EXT_IMPORTER { id }
+| id = EXT_IMPORTER_PLUGIN { fst id }
| id = IDENTIFIER_EXT { id }
+| id = IDENTIFIER_IMPORTER { id }
;
%inline unknown_extension:
@@ -1695,9 +1699,9 @@ logic_def:
{ LDimport(None,mId,None) }
| IMPORT mId = module_name AS id = IDENTIFIER SEMICOLON
{ LDimport(None,mId,Some id) }
-| IMPORT drv = IDENTIFIER COLON mId = module_name SEMICOLON
+| IMPORT drv = ext_importer mId = module_name SEMICOLON
{ LDimport(Some drv,mId,None) }
-| IMPORT drv = IDENTIFIER COLON mId = module_name AS id = IDENTIFIER SEMICOLON
+| IMPORT drv = ext_importer mId = module_name AS id = IDENTIFIER SEMICOLON
{ LDimport(Some drv,mId,Some id) }
| TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
{ let (id,tvars) = $2 in
@@ -1715,6 +1719,17 @@ push_module_name:
| module_name { push_module_types () ; $1 }
;
+ext_importer:
+| IDENTIFIER COLON {
+ Kernel.warning ~once:true ~wkey:Kernel.wkey_extension_unknown
+ ~source:(fst (loc $sloc))
+ "Ignoring unregistered importer extension '%s'" $1;
+ raise Unknown_ext
+ }
+| EXT_IMPORTER COLON { $1, None }
+| EXT_IMPORTER_PLUGIN { $1 }
+| IDENTIFIER_IMPORTER { raise Unknown_ext }
+
deprecated_logic_decl:
/* OBSOLETE: logic function declaration */
| LOGIC logic_rt_type poly_id opt_parameters SEMICOLON
@@ -1982,7 +1997,10 @@ is_acsl_decl_or_code_annot:
| EXT_CODE_ANNOT { fst $1 }
| EXT_GLOBAL { fst $1 }
| EXT_GLOBAL_BLOCK { fst $1 }
+| EXT_IMPORTER { $1 }
+| EXT_IMPORTER_PLUGIN { fst $1 }
| IDENTIFIER_EXT { $1 }
+| IDENTIFIER_IMPORTER { $1 }
| ASSUMES { "assumes" }
| ASSERT { "assert" }
| CHECK { "check" }
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 7b9f5506e3..4949133967 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1801,8 +1801,8 @@ and global_annotation =
* attributes * location
(** associated terms, reading function, writing function *)
| Daxiomatic of string * global_annotation list * attributes * location
- (** last string option is the external importer responsible for the module *)
- | Dmodule of string * global_annotation list * attributes * string option * location
+ (** last option is the external importer responsible for the module *)
+ | Dmodule of string * global_annotation list * attributes * (string * string option) option * location
| Dtype of logic_type_info * location (** declaration of a logic type. *)
| Dlemma of
string * logic_label list * string list *
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6692b16309..dd224e225f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3284,6 +3284,14 @@ class cil_printer () = object (self)
(self#typ None) mfi.mi_base_type
(self#logic_type (Some print_decl)) mfi.mi_field_type
+ method private pp_driver fmt (name, plugin) =
+ match plugin with
+ | None -> pp_print_string fmt name
+ | Some plugin ->
+ if Datatype.String.equal plugin "kernel"
+ then pp_print_string fmt name
+ else fprintf fmt "\\%s::%s" plugin name
+
method global_annotation fmt = function
| Dtype_annot (a,_) ->
let old_label = current_label in
@@ -3415,15 +3423,16 @@ class cil_printer () = object (self)
decls
| Dmodule(id, _, _, Some drv, _)
when not Kernel.(is_debug_key_enabled dkey_print_imported_modules) ->
- fprintf fmt "@[<hov 2>%a %s: %s %a _ ;@]@\n"
- self#pp_acsl_keyword "import" drv id
+ fprintf fmt "@[<hov 2>%a %a: %s %a _ ;@]@\n"
+ self#pp_acsl_keyword "import"
+ self#pp_driver drv id
self#pp_acsl_keyword "\\as"
| Dmodule(id, decls, _attr, driver, _) ->
begin
(* attributes are meant to be purely internal for now. *)
fprintf fmt "@[<v 2>@[" ;
if Kernel.(is_debug_key_enabled dkey_print_imported_modules) then
- Option.iter (fprintf fmt "// import %s:@\n") driver ;
+ Option.iter (fprintf fmt "// import %a:@\n" self#pp_driver) driver ;
fprintf fmt "%a %a {@]"
self#pp_acsl_keyword "module" self#logic_name id ;
try
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 28e5f94489..7a6e715c92 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -972,9 +972,14 @@ and pp_global_annotation fmt = function
(pp_list pp_global_annotation) global_annotation_list
pp_attributes attributes pp_location location
| Dmodule(string,global_annotation_list,attributes,driver,location) ->
+ let pp_driver fmt (name, plugin) =
+ Format.fprintf fmt "(%s, %a)" name (pp_option pp_string) plugin
+ in
Format.fprintf fmt "Dmodule(%a,%a,%a,%a,%a)" pp_string string
(pp_list pp_global_annotation) global_annotation_list
- pp_attributes attributes (pp_option pp_string) driver pp_location location
+ pp_attributes attributes
+ (pp_option pp_driver) driver
+ pp_location location
| Dtype(logic_type_info,location) ->
Format.fprintf fmt "Dtype(%a,%a)" pp_logic_type_info logic_type_info pp_location location
| Dlemma(string,logic_label_list,string_list,predicate,attributes,location) ->
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index d38113e347..b0a6758cb0 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -376,8 +376,16 @@ let rec print_decl fmt d =
fprintf fmt "@[<2>module@ %s@ {@\n%a@]@\n}" name
(pp_list ~sep:"@\n" print_decl) ds
| LDimport (drv,mId,asId) ->
+ let pp_driver fmt (name, plugin) =
+ match plugin with
+ | None -> pp_print_string fmt name
+ | Some plugin ->
+ if Datatype.String.equal plugin "kernel"
+ then pp_print_string fmt name
+ else fprintf fmt "\\%s::%s" plugin name
+ in
fprintf fmt "@[<2>import" ;
- Option.iter (fprintf fmt "@ %s:") drv ;
+ Option.iter (fprintf fmt "%a:" pp_driver) drv ;
fprintf fmt "@ %s" mId ;
Option.iter (fprintf fmt "@ \\as %s") asId ;
fprintf fmt ";@]@\n}"
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index f5c221bc25..df980b11d6 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -39,6 +39,8 @@ type extension_printer =
acsl_extension_kind -> unit
type extension_same =
acsl_extension_kind -> acsl_extension_kind -> Ast_diff.is_same_env -> bool
+type extension_module_importer =
+ module_builder -> location -> string list -> unit
type register_extension =
plugin:string -> string ->
@@ -75,8 +77,10 @@ type extension_common = {
plugin: string;
is_same_ext: extension_same;
}
-type extension_module_importer =
- module_builder -> location -> string list -> unit
+type extension_importer = {
+ plugin: string;
+ importer: extension_module_importer;
+}
let default_printer printer fmt = function
| Ext_id i -> Format.pp_print_int fmt i
@@ -128,6 +132,9 @@ let make_block
{ preprocessor; typer; status; plugin},
{ category; visitor; printer; short_printer; plugin; is_same_ext }
+let make_importer ~plugin importer : extension_importer =
+ { plugin; importer }
+
module Extensions = struct
(* Hash table for extension_common. A name can be use by different plugins to
register an extension so we keep a list. *)
@@ -144,8 +151,10 @@ module Extensions = struct
let ext_block_tbl : (string, extension_block list) Hashtbl.t =
Hashtbl.create 5
- (* Hash table for module importers. *)
- let ext_module_importer = Hashtbl.create 5
+ (* Hash table for extension_importer. A name can be use by different plugins
+ to register an extension so we keep a list. *)
+ let ext_importer_tbl : (string, extension_importer list) Hashtbl.t =
+ Hashtbl.create 5
let add_to_list tbl key value =
match Hashtbl.find_opt tbl key with
@@ -200,10 +209,11 @@ module Extensions = struct
(* Generic function for find functions, catch Not_found and throw a fatal
instead. *)
- let find_gen ~get_plugin tbl ~plugin name =
+ let find_gen ~get_plugin data tbl ~plugin name =
try find ~get_plugin ~plugin tbl name
with Not_found ->
- Kernel.fatal ~current:true "Unsupported clause extension named '%a%s'"
+ Kernel.fatal ~current:true "Unsupported %s extension named '%a%s'"
+ data
(Pretty_utils.pp_opt ~pre:"\\" ~suf:"::" Format.pp_print_string) plugin
name
@@ -213,25 +223,33 @@ module Extensions = struct
let get_plugin_block (e : extension_block) = e.plugin
- let find_single = find_gen ~get_plugin:get_plugin_single ext_single_tbl
+ let get_plugin_importer (e : extension_importer) = e.plugin
+
+ let find_single =
+ find_gen ~get_plugin:get_plugin_single "clause" ext_single_tbl
- let find_common = find_gen ~get_plugin:get_plugin_common ext_tbl
+ let find_common =
+ find_gen ~get_plugin:get_plugin_common "clause" ext_tbl
- let find_block = find_gen ~get_plugin:get_plugin_block ext_block_tbl
+ let find_block =
+ find_gen ~get_plugin:get_plugin_block "clause" ext_block_tbl
- let find_importer name : extension_module_importer =
- try Hashtbl.find ext_module_importer name with Not_found ->
- Kernel.fatal ~current:true "Unsupported module importer '%s'" name
+ let find_importer =
+ find_gen ~get_plugin:get_plugin_importer "importer" ext_importer_tbl
(* [Logic_lexer] can ask for something that is not a category, which is not
a fatal error so we do not caught the Not_found exception. *)
let category ~plugin name =
(find ~get_plugin:get_plugin_common ext_tbl ~plugin name).category
+ let importer ~plugin name = (find_importer ~plugin name).importer
+
let is_extension = mem ~get_plugin:get_plugin_common ext_tbl
let is_extension_block = mem ~get_plugin:get_plugin_block ext_block_tbl
+ let is_importer = mem ~get_plugin:get_plugin_importer ext_importer_tbl
+
let register_gen ~make ~tbl cat ~plugin name
?preprocessor typer ?visitor ?printer ?short_printer ?is_same_ext status =
let info1,info2 =
@@ -259,13 +277,20 @@ module Extensions = struct
let register_block = register_gen ~make:make_block ~tbl:ext_block_tbl
- let register_module_importer name loader =
- if Hashtbl.mem ext_module_importer name then
+ let register_module_importer ~plugin name loader =
+ if is_importer ~plugin:(Some "kernel") name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
- "Trying to register module importer %s twice. Ignoring second importer"
- name
+ "Trying to register importer extension %s reserved by frama-c. \
+ Rename to avoid conflict with the kernel. Ignored module importer" name
else
- Hashtbl.add ext_module_importer name loader
+ begin
+ if is_importer ~plugin:(Some plugin) name then
+ Kernel.warning ~wkey:Kernel.wkey_acsl_extension
+ "Trying to register importer extension %s twice with plugin %s. \
+ Ignoring the second extension" name plugin
+ else
+ add_to_list ext_importer_tbl name (make_importer ~plugin loader)
+ end
let preprocess ~plugin name = (find_single ~plugin name).preprocessor
@@ -300,7 +325,7 @@ module Extensions = struct
let print ~plugin name printer fmt kind =
let ext_common = find_common ~plugin name in
- let plugin = ext_common.plugin in
+ let plugin = get_plugin_common ext_common in
let full_name =
if Datatype.String.equal plugin "kernel"
then name
@@ -347,6 +372,7 @@ let () =
Logic_env.set_extension_handler
~category:Extensions.category
~is_extension: Extensions.is_extension
+ ~is_importer:Extensions.is_importer
~preprocess: Extensions.preprocess
~is_extension_block: Extensions.is_extension_block
~preprocess_block: Extensions.preprocess_block;
@@ -354,7 +380,7 @@ let () =
~is_extension: Extensions.is_extension
~typer: Extensions.typing
~typer_block: Extensions.typing_block
- ~importer: Extensions.find_importer;
+ ~importer: Extensions.importer;
Cil.set_extension_handler
~visit: Extensions.visit ;
Cil_printer.set_extension_handler
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 937f8c65cb..ba981fb9e2 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -46,6 +46,9 @@ type extension_preprocessor_block =
type extension_typer_block =
typing_context -> location -> string * extended_decl list -> acsl_extension_kind
+type extension_module_importer =
+ module_builder -> location -> string list -> unit
+
(** Pretty printers for ACSL extensions *)
type extension_printer =
Printer_api.extensible_printer_type -> Format.formatter ->
@@ -58,9 +61,6 @@ type extension_printer =
type extension_same =
acsl_extension_kind -> acsl_extension_kind -> Ast_diff.is_same_env -> bool
-type extension_module_importer =
- module_builder -> location -> string list -> unit
-
(** type of functions that register new ACSL extensions to be used in place of
various kinds of ACSL annotations.
@@ -161,11 +161,11 @@ val register_code_annot_next_both: register_extension
Module importer extensions allow extending the import clause with external
loaders. For instance, consider the following declaration:
{[
- //@ import A: foo::bar;
+ //@ import \myplugin::A: foo::bar;
]}
This import clause will invoke an external module importer named ["A"]
- provided it has been properly registered.
+ provided it has been properly registered by plugin [myplugin].
A module importer extension is a function that receives a [module_builder]
parameter to be populated with contents of the module. The module name is
@@ -180,4 +180,5 @@ val register_code_annot_next_both: register_extension
external module importers might use memoization internally, the provided
module builder shall be populated on every call.
*)
-val register_module_importer : string -> extension_module_importer -> unit
+val register_module_importer :
+ plugin:string -> string -> extension_module_importer -> unit
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 0f46da80c6..58795159bc 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -27,15 +27,17 @@ open Cil_types
module Extensions = struct
let initialized = ref false
let ref_is_extension = ref (fun ~plugin:_ _ -> assert false)
+ let ref_is_importer = ref (fun ~plugin:_ _ -> assert false)
let ref_category = ref (fun ~plugin:_ _ -> assert false)
let ref_preprocess = ref (fun ~plugin:_ _ -> assert false)
let ref_is_extension_block = ref (fun ~plugin:_ _ -> assert false)
let ref_preprocess_block = ref (fun ~plugin:_ _ -> assert false)
- let set_extension_handler ~category ~is_extension ~preprocess
+ let set_extension_handler ~category ~is_extension ~is_importer ~preprocess
~is_extension_block ~preprocess_block =
assert (not !initialized) ;
ref_is_extension := is_extension ;
+ ref_is_importer := is_importer ;
ref_category := category ;
ref_preprocess := preprocess ;
ref_is_extension_block := is_extension_block;
@@ -45,6 +47,7 @@ module Extensions = struct
let is_extension ~plugin name = !ref_is_extension ~plugin name
let is_extension_block ~plugin name = !ref_is_extension_block ~plugin name
+ let is_importer ~plugin name = !ref_is_importer ~plugin name
let category ~plugin name = !ref_category ~plugin name
let preprocess ~plugin name = !ref_preprocess ~plugin name
let preprocess_block ~plugin name = !ref_preprocess_block ~plugin name
@@ -52,6 +55,7 @@ end
let set_extension_handler = Extensions.set_extension_handler
let is_extension = Extensions.is_extension
let is_extension_block = Extensions.is_extension_block
+let is_importer = Extensions.is_importer
let extension_category = Extensions.category
let preprocess_extension = Extensions.preprocess
let preprocess_extension_block = Extensions.preprocess_block
@@ -154,7 +158,10 @@ module Axiomatics =
module ModuleOccurence =
Datatype.Pair
- (Datatype.Option(Datatype.String)) (* external driver *)
+ (Datatype.Option
+ (Datatype.Pair
+ (Datatype.String) (* external driver name *)
+ (Datatype.Option(Datatype.String)))) (* external driver plugin *)
(Cil_datatype.Location)
module Modules =
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index 3f9907cc2d..9bbc0a67a1 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -40,6 +40,11 @@ val is_extension: plugin:string option -> string -> bool
*)
val is_extension_block: plugin:string option -> string -> bool
+(** Return [true] if a module importer is registered for the given plugin.
+ @since Frama-C+dev
+*)
+val is_importer: plugin:string option -> string -> bool
+
(** Return the extension category.
@raise Not_Found if the extension is not registered
@before Frama-C+def the function took one less argument, [plugin], which is
@@ -87,7 +92,8 @@ module Axiomatics: State_builder.Hashtbl
(** @since Frama-C+dev *)
module Modules: State_builder.Hashtbl
with type key = string
- and type data = string option * Cil_types.location (* driver, loc *)
+ (* driver (name, plugin), location *)
+ and type data = (string * string option) option * Cil_types.location
val builtin_states: State.t list
@@ -257,7 +263,7 @@ val set_extension_handler:
If your name is not [Acsl_extension], do not call this.
@since 21.0-Scandium
@before Frama-C+dev functions did not take a [plugin] parameter.
- [get_plugins] did not exist
+ [get_plugins] and [is_importer] did not exist
*)
val init_dependencies: State.t -> unit
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 0ae28b248b..be1aba8f1e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -538,7 +538,7 @@ module Extensions = struct
let ref_is_extension = ref (fun ~plugin:_ _ -> assert false)
let ref_typer = ref (fun ~plugin:_ _ _ _ _ -> assert false)
let ref_typer_block = ref (fun ~plugin:_ _ _ _ _ -> assert false)
- let ref_importer = ref (fun _ _ _ _ -> assert false)
+ let ref_importer = ref (fun ~plugin:_ _ _ _ _ -> assert false)
let set_handler ~is_extension ~typer ~typer_block ~importer =
assert (not !initialized) ;
@@ -556,8 +556,8 @@ module Extensions = struct
let typer_block ~plugin name ~typing_context:typing_context ~loc =
!ref_typer_block ~plugin name typing_context loc
- let importer name ~builder ~loc (moduleId: string list) : unit =
- !ref_importer name builder loc moduleId
+ let importer ~plugin name ~builder ~loc (moduleId: string list) : unit =
+ !ref_importer ~plugin name builder loc moduleId
end
let set_extension_handler = Extensions.set_handler
@@ -4330,24 +4330,27 @@ struct
| LDimport(None,name,alias) ->
add_import ?alias name ; None
- | LDimport(Some driver as drv,name,alias) ->
+ | LDimport(Some (driver, plugin) as drv,name,alias) ->
let annot =
match Logic_env.Modules.find name with
| None, oldloc ->
C.error loc
"Module %s already defined (at %a)"
name Cil_printer.pp_location oldloc
- | Some odrv, oldloc ->
- if odrv <> driver then
+ | Some (driver', plugin'), oldloc ->
+ if plugin <> plugin' || driver <> driver' then
C.error loc
- "Module %s already imported with driver %s (at %a)"
- name odrv Cil_printer.pp_location oldloc
+ "Module %s already imported with driver %a%s (at %a)"
+ name
+ (Pretty_utils.pp_opt ~pre:"\\" ~suf:"::" Format.pp_print_string) plugin'
+ driver'
+ Cil_printer.pp_location oldloc
else None
| exception Not_found ->
let decls = ref [] in
let builder = make_module_builder decls name in
let path = Logic_utils.longident name in
- Extensions.importer driver ~builder ~loc path ;
+ Extensions.importer ~plugin driver ~builder ~loc path ;
Logic_env.Modules.add name (drv,loc) ;
Some (Dmodule(name,List.rev !decls,[],drv,loc))
in add_import ?alias name ; annot
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index ecb26959fa..930fc3f881 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -318,7 +318,8 @@ val set_extension_handler:
typer_block:(plugin:string option -> string -> typing_context -> location ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind) ->
- importer:(string -> module_builder -> location -> string list -> unit) ->
+ importer: (plugin:string option -> string -> module_builder -> location ->
+ string list -> unit) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this
@@ -349,7 +350,11 @@ val get_typer_block:
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind
+(** Load the given extension importer.
+ @since Frama-C+dev
+*)
val get_importer:
+ plugin:string option ->
string ->
builder:module_builder ->
loc:Logic_ptree.location ->
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 7fbcc3cde0..5c8c065d59 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -250,7 +250,7 @@ and decl_node =
| LDmodule of string * decl list
(** [LDmodule(id,decls)]
represents a module of axiomatic definitions.*)
- | LDimport of string option * string * string option
+ | LDimport of (string * string option) option * string * string option
(** [LDimport(driver,module,alias)]
imports symbols from module using the specified driver,
with optional alias.*)
--
GitLab