diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 0bbfb97d37301875456f98048c0fffb22a407893..6fe88ccaccfe1ad9155a770c8d108e31b5911148 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -73,7 +73,8 @@ type extension_common = {
plugin: string;
is_same_ext: extension_same;
}
-type module_loader = typing_context -> location -> string list -> unit
+type extension_module_importer =
+ module_builder -> location -> string list -> unit
let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i
@@ -133,8 +134,8 @@ module Extensions = struct
(*hash table for status, preprocessor and typer of block extensions*)
let ext_block_tbl = Hashtbl.create 5
- (*hash table for module loader*)
- let ext_module_loader = Hashtbl.create 5
+ (*hash table for module importers*)
+ let ext_module_importer = Hashtbl.create 5
let find_single name :extension_single =
try Hashtbl.find ext_single_tbl name with Not_found ->
@@ -148,9 +149,9 @@ module Extensions = struct
try Hashtbl.find ext_block_tbl name with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
- let find_loader name :module_loader =
- try Hashtbl.find ext_module_loader name with Not_found ->
- Kernel.fatal ~current:true "unsupported module loader '%s'" name
+ 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
(* [Logic_lexer] can ask for something that is not a category, which is not
a fatal error. *)
@@ -192,13 +193,13 @@ module Extensions = struct
Hashtbl.add ext_tbl name info2
end
- let register_loader name loader =
- if Hashtbl.mem ext_module_loader name then
+ let register_module_importer name loader =
+ if Hashtbl.mem ext_module_importer name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
- "Trying to register module loader %s twice. Ignoring second loader"
+ "Trying to register module importer %s twice. Ignoring second importer"
name
else
- Hashtbl.add ext_module_loader name loader
+ Hashtbl.add ext_module_importer name loader
let preprocess name = (find_single name).preprocessor
@@ -280,8 +281,8 @@ let register_code_annot_next_loop =
Extensions.register (Ext_code_annot Ext_next_loop)
let register_code_annot_next_both =
Extensions.register (Ext_code_annot Ext_next_both)
-let register_module_loader =
- Extensions.register_loader
+let register_module_importer =
+ Extensions.register_module_importer
(* Setup global references *)
@@ -297,7 +298,7 @@ let () =
~is_extension: Extensions.is_extension
~typer: Extensions.typing
~typer_block: Extensions.typing_block
- ~loader: Extensions.find_loader;
+ ~importer: Extensions.find_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 db0021845def0c7b50161d9c0773c2a127ecfff8..fcee9704a38fabe6317d8b77311421a9d4e4bb36 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -58,6 +58,9 @@ 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.
@@ -154,5 +157,27 @@ val register_code_annot_next_loop: register_extension
(** Registers extension both for code and loop annotations. *)
val register_code_annot_next_both: register_extension
-type module_loader = typing_context -> location -> string list -> unit
-val register_module_loader : string -> module_loader -> unit
+(**
+ Module importer extensions allow to extends the import clause with external
+ loaders. For instance, consider the following declaration:
+ [
+ //@ import A: foo::bar;
+ ]
+
+ This import clause will invoke an external module importer named ["A"]
+ provided it has been properly registered.
+
+ 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
+ provided as list (See {Logic_utils.longident} for details).
+
+ New type and function symbols shall be created with `Cil.make_xxx` functions.
+ The registered symbols {i will} be automatically prefixed with the name of
+ the imported module.
+
+ The register module importer function might be invoked several times,
+ typically when a given module is imported from several files. Although
+ 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
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index bed7d0dd72d5aa760337ed34d094d45c3a8864bd..7bde413189af3948db3d02332dda20d14105a6f5 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -186,6 +186,13 @@ let make_logic_info k x =
let make_logic_info_local = make_logic_info LVLocal
let make_logic_info = make_logic_info LVGlobal
+let make_logic_type name = {
+ lt_name = name ;
+ lt_params = [] ;
+ lt_def = None ;
+ lt_attr = [] ;
+}
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index b43e9f2456f8cb68c489b83d27c9e2bc96d0c962..1c3c1cf27bacc1952bc76db8f87a4b71cdede787 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -211,15 +211,14 @@ val make_logic_var_quant: string -> logic_type -> logic_var
val make_logic_var_local: string -> logic_type -> logic_var
(** Create a fresh logical (global) variable giving its name and type. *)
-val make_logic_info : string -> (* logic_type -> *) logic_info
+val make_logic_info : string -> logic_info
(** Create a new local logic variable given its name.
@since Fluorine-20130401
*)
-val make_logic_info_local : string -> (* logic_type -> *) logic_info
+val make_logic_info_local : string -> logic_info
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
+(** Create a logic type info given its name.
+ @since Frama-C+dev
*)
+val make_logic_type : string -> logic_type_info
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 8f13fd8082004d2106ecf633c1992393a7634d88..cd8b5c6c477e3c9976bba3a5122c2ad05d19caac 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -524,44 +524,47 @@ type typing_context = {
accept_formal:bool ->
Lenv.t ->
Logic_ptree.assigns -> Cil_types.assigns;
- add_logic_type: location -> logic_type_info -> unit;
- add_logic_ctor: location -> logic_ctor_info -> unit;
- add_logic_function: location -> logic_info -> unit;
error: 'a 'b. location -> ('a,Format.formatter,unit,'b) format4 -> 'a;
on_error: 'a 'b. ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
}
+type module_builder = {
+ add_logic_type : location -> logic_type_info -> unit ;
+ add_logic_function : location -> logic_info -> unit ;
+}
+
module Extensions = struct
let initialized = ref false
let ref_is_extension = ref (fun _ -> assert false)
let ref_typer = ref (fun _ _ _ _ -> assert false)
let ref_typer_block = ref (fun _ _ _ _ -> assert false)
- let ref_loader = ref (fun _ _ _ _ -> assert false)
+ let ref_importer = ref (fun _ _ _ _ -> assert false)
- let set_handler ~is_extension ~typer ~typer_block ~loader =
+ let set_handler ~is_extension ~typer ~typer_block ~importer =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_typer := typer ;
ref_typer_block := typer_block;
- ref_loader := loader ;
+ ref_importer := importer ;
initialized := true
let is_extension name = !ref_is_extension name
- let typer name ~typing_context:typing_context ~loc =
+ let typer name ~(typing_context:typing_context) ~(loc:location) =
!ref_typer name typing_context loc
- let typer_block name ~typing_context:typing_context ~loc mId =
+ let typer_block name ~(typing_context:typing_context) ~(loc:location) mId =
!ref_typer_block name typing_context loc mId
- let loader name ~typing_context:typing_context ~loc =
- !ref_loader name typing_context loc
+ let importer name ~(builder:module_builder) ~(loc:location)
+ (moduleId: string list) : unit =
+ !ref_importer name builder loc moduleId
end
let set_extension_handler = Extensions.set_handler
let get_typer = Extensions.typer
let get_typer_block = Extensions.typer_block
-let get_loader = Extensions.loader
+let get_importer = Extensions.importer
let rec arithmetic_conversion ty1 ty2 =
match unroll_type ty1, unroll_type ty2 with
@@ -693,6 +696,29 @@ module Make
end) =
struct
+ let make_typing_context ~pre_state ~post_state ~assigns_env
+ ~logic_type ~type_predicate ~type_term ~type_assigns = {
+ silent = false;
+ is_loop = C.is_loop;
+ pre_state=pre_state;
+ post_state=post_state;
+ assigns_env=assigns_env;
+ logic_type= logic_type;
+ type_predicate= type_predicate;
+ type_term= type_term;
+ type_assigns = type_assigns;
+ anonCompFieldName = C.anonCompFieldName;
+ conditionalConversion = C.conditionalConversion;
+ find_macro = C.find_macro;
+ find_var = C.find_var;
+ find_enum_tag = C.find_enum_tag;
+ find_comp_field = C.find_comp_field;
+ find_type = C.find_type ;
+ find_label = C.find_label;
+ error = C.error;
+ on_error = C.on_error;
+ }
+
(* Imported Scope *)
type scope = {
@@ -774,30 +800,24 @@ struct
let add_rollback_action f x = Queue.add (fun () -> f x) rollback
- let add_logic_function loc li =
+ let add_logic_info loc li =
+ let lv = li.l_var_info in
(try
- let _ = Logic_env.find_logic_ctor li.l_var_info.lv_name in
- C.error loc "constructor %s is already defined" li.l_var_info.lv_name
+ let _ = Logic_env.find_logic_ctor lv.lv_name in
+ C.error loc "constructor %s is already defined" lv.lv_name
with Not_found -> ());
- let l = Logic_env.find_all_logic_functions li.l_var_info.lv_name in
- if List.exists (Logic_utils.is_same_logic_profile li) l then begin
- C.error loc
- "%s %s is already declared with the same profile"
- (match li.l_type with None -> "predicate" | Some _ -> "logic function")
- li.l_var_info.lv_name
- end else begin
- let eq = Logic_utils.is_same_logic_profile in
- Logic_env.add_logic_function_gen eq li;
- add_rollback_action (Logic_env.remove_logic_info_gen eq) li
- end
-
- let add_logic_ctor loc ct =
- try
- ignore (Logic_env.find_logic_ctor ct.ctor_name);
- C.error loc "logic type constructor %s is already defined" ct.ctor_name
- with Not_found ->
- Logic_env.add_logic_ctor ct.ctor_name ct;
- add_rollback_action Logic_env.remove_logic_ctor ct.ctor_name
+ if Logic_utils.mem_logic_function li then
+ begin
+ C.error loc
+ "%s %s is already declared with the same profile"
+ (match li.l_type with None -> "predicate" | Some _ -> "logic function")
+ lv.lv_name
+ end
+ else
+ begin
+ Logic_utils.add_logic_function li;
+ add_rollback_action Logic_utils.remove_logic_function li
+ end
let add_logic_type loc info =
try
@@ -807,32 +827,6 @@ struct
Logic_env.add_logic_type info.lt_name info;
add_rollback_action Logic_env.remove_logic_type info.lt_name
- let make_typing_context ~pre_state ~post_state ~assigns_env
- ~logic_type ~type_predicate ~type_term ~type_assigns = {
- silent = false;
- is_loop = C.is_loop;
- pre_state=pre_state;
- post_state=post_state;
- assigns_env=assigns_env;
- logic_type= logic_type;
- type_predicate= type_predicate;
- type_term= type_term;
- type_assigns = type_assigns;
- anonCompFieldName = C.anonCompFieldName;
- conditionalConversion = C.conditionalConversion;
- find_macro = C.find_macro;
- find_var = C.find_var;
- find_enum_tag = C.find_enum_tag;
- find_comp_field = C.find_comp_field;
- find_type = C.find_type ;
- find_label = C.find_label;
- add_logic_function ;
- add_logic_type ;
- add_logic_ctor ;
- error = C.error;
- on_error = C.on_error;
- }
-
let check_non_void_ptr loc ty =
if Logic_utils.isLogicVoidPointerType ty then
C.error loc "Cannot use a pointer to void here"
@@ -3820,8 +3814,7 @@ struct
~logic_type
~type_predicate
~type_term
- ~type_assigns:type_assign
- in
+ ~type_assigns:type_assign in
let b_assumes = List.map (id_predicate env) bas in
let b_requires= List.map (id_predicate_top env) br in
let b_post_cond =
@@ -4116,7 +4109,7 @@ struct
info.l_profile <- p;
info.l_type <- t;
info.l_labels <- labels;
- add_logic_function loc info;
+ add_logic_info loc info;
env,info
let type_annot loc ti =
@@ -4288,15 +4281,8 @@ struct
ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
Some (Dmodule(name,l,[],loc))
- | LDimport(drv,name,alias) ->
- Option.iter
- begin fun drv ->
- let typing_context = base_ctxt (Lenv.empty ()) in
- Extensions.loader drv ~typing_context ~loc
- @@ List.filter (fun s -> s <> "")
- @@ String.split_on_char ':' name
- end drv ;
- open_scope ~name ?alias () ; None
+ | LDimport(_drv,moduleId,alias) ->
+ open_scope ~name:moduleId ?alias () ; None
| LDtype(name,l,def) ->
let env = init_type_variables loc l in
@@ -4347,7 +4333,7 @@ struct
in
li.l_labels <- labels;
li.l_body <- LBpred p;
- add_logic_function loc li;
+ add_logic_info loc li;
update_info_wrt_default_label li;
Some (Dinvariant (li,loc))
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e2a347f574d5f800b53b3546c4f4e89c364d646c..de61bec34f859ae64b90d64fe897e7e103919b84 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -127,11 +127,7 @@ type typing_context = {
typing_context ->
accept_formal:bool ->
Lenv.t -> Logic_ptree.assigns -> assigns;
- add_logic_type: location -> logic_type_info -> unit;
- add_logic_ctor: location -> logic_ctor_info -> unit;
- add_logic_function: location -> logic_info -> unit;
error: 'a 'b. location -> ('a,Format.formatter,unit,'b) format4 -> 'a;
-
on_error: 'a 'b. ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
(** [on_error f rollback x] will attempt to evaluate [f x]. If this triggers
an error while in [-kernel-warn-key annot-error] mode, [rollback
@@ -144,6 +140,14 @@ type typing_context = {
*)
}
+(** Functions that can be called when importing external modules into ACSL.
+ See {Acsl_extension.register_module_importer} for details.
+ @since Frama-C+dev
+*)
+type module_builder = {
+ add_logic_type : location -> logic_type_info -> unit ;
+ add_logic_function : location -> logic_info -> unit ;
+}
module type S =
sig
@@ -300,7 +304,7 @@ val set_extension_handler:
typer_block:(string -> typing_context -> location ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind) ->
- loader:(string -> typing_context -> location -> string list -> unit) ->
+ importer:(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
@@ -320,8 +324,8 @@ val get_typer_block:
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind
-val get_loader:
+val get_importer:
string ->
- typing_context:typing_context ->
+ builder:module_builder ->
loc:Logic_ptree.location ->
string list -> unit
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 3e298120913a0a4fb78a7db2f90a40e7603056e6..cf42d5119fac0683bae551966b281e9e6ced9f45 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -870,7 +870,14 @@ let is_same_builtin_profile l1 l2 =
is_same_list (fun (_,t1) (_,t2) -> is_same_type t1 t2)
l1.bl_profile l2.bl_profile
+let longident = Str.split @@ Str.regexp_string "::"
+
+let mem_logic_function f =
+ List.exists (is_same_logic_profile f) @@
+ Logic_env.find_all_logic_functions f.l_var_info.lv_name
+
let add_logic_function = Logic_env.add_logic_function_gen is_same_logic_profile
+let remove_logic_function = Logic_env.remove_logic_info_gen is_same_logic_profile
let is_same_logic_ctor_info ci1 ci2 =
ci1.ctor_name = ci2.ctor_name &&
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 9ef563d8833f901ce18594e055e4804f26f8a9ab..5d0f400732ac8882921c4b79e15e58dc9c490faa 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -34,14 +34,31 @@ exception Not_well_formed of location * string
(** exception raised when an unknown extension is called. *)
exception Unknown_ext
+(** Split a long-identifier into the list of its components.
+ eg. ["A::B::(<:)"] is split into [["A";"B";"(<:)"]].
+ Returns a singleton for regular identifiers.
+ @since Frama-C+dev *)
+val longident : string -> string list
+
(** basic utilities for logic terms and predicates. See also {! Logic_const}
to build terms and predicates.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-(** add a logic function in the environment.
- See {!Logic_env.add_logic_function_gen}*)
+(** Check if there is a logic function with same profile in the environment.
+ @since Frama-C+dev *)
+val mem_logic_function : logic_info -> bool
+
+(** Add a logic function in the environment.
+ Replaces any existing logic function with the same profile.
+ See {!Logic_env.add_logic_function_gen}
+ @since Frama-C+dev *)
val add_logic_function : logic_info -> unit
+(** remove any logic function with the same profile from the environment.
+ See {!Logic_env.remove_logic_function_gen}
+ @since Frama-C+dev *)
+val remove_logic_function : logic_info -> unit
+
(** {2 Types} *)
(** [is_instance_of poly t1 t2] returns [true] if [t1] can be derived from [t2]
diff --git a/tests/spec/import.i b/tests/spec/import.i
new file mode 100644
index 0000000000000000000000000000000000000000..5f3d679855c71653b173f6beed31380c34cf8c04
--- /dev/null
+++ b/tests/spec/import.i
@@ -0,0 +1,10 @@
+/* run.config
+MODULE: @PTEST_NAME@
+OPT: -print
+*/
+
+/*@ import foo: A::B; */
+/* predicate check1(B::t x) = B::check(x,0); */
+
+/* import foo: A::B \as C; */
+/* predicate check2(C::t x) = A::B::check(x,0); */
diff --git a/tests/spec/import.ml b/tests/spec/import.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ca99db7c9845d4dee600b58794a88ec373f6402c
--- /dev/null
+++ b/tests/spec/import.ml
@@ -0,0 +1,25 @@
+open Cil_types
+open Logic_typing
+
+let () = Format.printf "[test-import] Linking.@."
+
+let loader (ctxt: module_builder) (loc: location) (m: string list) =
+ begin
+ Format.printf "[test-import:%d] Loading %s.@."
+ (fst loc).pos_lnum (String.concat "::" m) ;
+ let t = Cil_const.make_logic_type "t" in
+ let check = Cil_const.make_logic_info "check" in
+ let x = Cil_const.make_logic_var_formal "x" (Ltype(t,[])) in
+ let k = Cil_const.make_logic_var_formal "k" Linteger in
+ check.l_profile <- [x;k] ;
+ ctxt.add_logic_type loc t ;
+ ctxt.add_logic_function loc check ;
+ end
+
+let register () =
+ begin
+ Format.printf "[test-import] Registering 'foo'.@." ;
+ Acsl_extension.register_module_importer "foo" loader ;
+ end
+
+let () = Cmdline.run_after_extended_stage register
diff --git a/tests/spec/oracle/import.res.oracle b/tests/spec/oracle/import.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..302eb64883263a23998682e34376333ddd0648ba
--- /dev/null
+++ b/tests/spec/oracle/import.res.oracle
@@ -0,0 +1,5 @@
+[test-import] Linking.
+[test-import] Registering 'foo'.
+[kernel] Parsing import.i (no preprocessing)
+/* Generated by Frama-C */
+