From 21c818478cae5d06ab446234c0984709e3dcb90b Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 21 Sep 2023 09:34:58 +0200
Subject: [PATCH] Registering a new ACSL extension requires plugin's name
---
.../ast_queries/acsl_extension.ml | 36 ++++++++++++-------
.../ast_queries/acsl_extension.mli | 21 +++++++----
src/kernel_services/ast_queries/dyncall.ml | 6 ++--
src/kernel_services/ast_queries/logic_env.ml | 8 +++--
src/kernel_services/ast_queries/logic_env.mli | 4 +++
src/plugins/eva/domains/taint_domain.ml | 4 +--
src/plugins/eva/utils/eva_annotations.ml | 2 +-
src/plugins/eva/utils/widen_hints_ext.ml | 2 +-
src/plugins/wp/Probe.ml | 2 +-
src/plugins/wp/ProofStrategy.ml | 4 +--
src/plugins/wp/RefUsage.ml | 2 +-
src/plugins/wp/RegionAnnot.ml | 2 +-
12 files changed, 61 insertions(+), 32 deletions(-)
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 9593eeb1eb7..b22e748f786 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -52,6 +52,7 @@ type extension_common = {
visitor: extension_visitor ;
printer: extension_printer ;
short_printer: extension_printer ;
+ plugin: string;
}
let default_printer printer fmt = function
@@ -64,6 +65,7 @@ let default_printer printer fmt = function
let default_short_printer name _printer fmt _ext_kind = Format.fprintf fmt "%s" name
let make
+ ~plugin
name category
?(preprocessor=Fun.id)
typer
@@ -71,9 +73,11 @@ let make
?(printer=default_printer)
?(short_printer=default_short_printer name)
status : extension_single*extension_common =
- { preprocessor; typer; status},{ category; visitor; printer; short_printer }
+ { preprocessor; typer; status},
+ { category; visitor; printer; short_printer; plugin }
let make_block
+ ~plugin
name category
?(preprocessor=Fun.id)
typer
@@ -81,7 +85,8 @@ let make_block
?(printer=default_printer)
?(short_printer=default_short_printer name)
status : extension_block*extension_common =
- { preprocessor; typer; status},{ category; visitor; printer; short_printer }
+ { preprocessor; typer; status},
+ { category; visitor; printer; short_printer; plugin }
module Extensions = struct
(*hash table for category, visitor, printer and short_printer of extensions*)
@@ -113,10 +118,11 @@ module Extensions = struct
let is_extension_block = Hashtbl.mem ext_block_tbl
- let register
- cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
+ let register cat ~plugin name
+ ?preprocessor typer ?visitor ?printer ?short_printer status =
let info1,info2 =
- make name cat ?preprocessor typer ?visitor ?printer ?short_printer status
+ make ~plugin name cat ?preprocessor typer
+ ?visitor ?printer ?short_printer status
in
if is_extension name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
@@ -128,10 +134,11 @@ module Extensions = struct
Hashtbl.add ext_tbl name info2
end
- let register_block
- cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
+ let register_block cat ~plugin name
+ ?preprocessor typer ?visitor ?printer ?short_printer status =
let info1,info2 =
- make_block name cat ?preprocessor typer ?visitor ?printer ?short_printer status
+ make_block ~plugin name cat ?preprocessor typer
+ ?visitor ?printer ?short_printer status
in
if is_extension name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
@@ -182,16 +189,20 @@ module Extensions = struct
let visit name = (find_common name).visitor
let print name printer fmt kind =
- let pp = (find_common name).printer printer in
+ let ext_common = find_common name in
+ let plugin = ext_common.plugin in
+ let pp = ext_common.printer printer in
match kind with
| Ext_annot (id,_) ->
- Format.fprintf fmt "@[<v 2>@[%s %s {@]@\n%a}@]" name id pp kind
+ Format.fprintf fmt "@[<v 2>@[\\%s::%s %s {@]@\n%a}@]" plugin name id pp kind
| _ ->
- Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
+ Format.fprintf fmt "@[<hov 2>\\%s::%s %a;@]" plugin name pp kind
let short_print name printer fmt kind =
let pp = (find_common name).short_printer in
Format.fprintf fmt "%a" (pp printer) kind
+
+ let extension_from name = (find_common name).plugin
end
(* Registration functions *)
@@ -219,7 +230,8 @@ let () =
~is_extension: Extensions.is_extension
~preprocess: Extensions.preprocess
~is_extension_block: Extensions.is_extension_block
- ~preprocess_block: Extensions.preprocess_block;
+ ~preprocess_block: Extensions.preprocess_block
+ ~extension_from:Extensions.extension_from;
Logic_typing.set_extension_handler
~is_extension: Extensions.is_extension
~typer: Extensions.typing
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 935ba239ef0..1744a487853 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -98,7 +98,8 @@ type extension_printer =
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
val register_behavior:
- string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ plugin:string -> string ->
+ ?preprocessor:extension_preprocessor -> extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
@@ -108,7 +109,8 @@ val register_behavior:
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
val register_global:
- string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ plugin:string -> string ->
+ ?preprocessor:extension_preprocessor -> extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
@@ -118,7 +120,8 @@ val register_global:
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
val register_global_block:
- string -> ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
+ plugin:string -> string ->
+ ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
@@ -129,7 +132,8 @@ val register_global_block:
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
val register_code_annot:
- string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ plugin:string -> string ->
+ ?preprocessor:extension_preprocessor -> extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
@@ -140,7 +144,8 @@ val register_code_annot:
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
val register_code_annot_next_stmt:
- string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ plugin:string -> string ->
+ ?preprocessor:extension_preprocessor -> extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
@@ -150,7 +155,8 @@ val register_code_annot_next_stmt:
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
val register_code_annot_next_loop:
- string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ plugin:string -> string ->
+ ?preprocessor:extension_preprocessor -> extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
@@ -161,7 +167,8 @@ val register_code_annot_next_loop:
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
val register_code_annot_next_both:
- string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ plugin:string -> string ->
+ ?preprocessor:extension_preprocessor -> extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
diff --git a/src/kernel_services/ast_queries/dyncall.ml b/src/kernel_services/ast_queries/dyncall.ml
index 388a233b910..dd04b7a66a2 100644
--- a/src/kernel_services/ast_queries/dyncall.ml
+++ b/src/kernel_services/ast_queries/dyncall.ml
@@ -255,8 +255,10 @@ let register =
fun () ->
if (not !once) then begin
once := true;
- Acsl_extension.register_code_annot_next_stmt "calls" typecheck true ;
- Acsl_extension.register_behavior "instanceof" typecheck true ;
+ Acsl_extension.register_code_annot_next_stmt ~plugin:"kernel"
+ "calls" typecheck true ;
+ Acsl_extension.register_behavior ~plugin:"kernel"
+ "instanceof" typecheck true ;
end
let () = Cmdline.run_after_configuring_stage register
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index cee9bf044d5..4e39e5d4304 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -31,9 +31,10 @@ module Extensions = struct
let ref_preprocess = ref (fun _ -> assert false)
let ref_is_extension_block = ref (fun _ -> assert false)
let ref_preprocess_block = ref (fun _ -> assert false)
+ let ref_extension_from = ref (fun _ -> assert false)
- let set_extension_handler
- ~category ~is_extension ~preprocess ~is_extension_block ~preprocess_block =
+ let set_extension_handler ~category ~is_extension ~preprocess
+ ~is_extension_block ~preprocess_block ~extension_from =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_category := category ;
@@ -41,6 +42,7 @@ module Extensions = struct
ref_is_extension_block := is_extension_block;
ref_preprocess_block := preprocess_block;
initialized := true ;
+ ref_extension_from := extension_from;
()
let is_extension s = !ref_is_extension s
@@ -48,6 +50,7 @@ module Extensions = struct
let category s = !ref_category s
let preprocess s = !ref_preprocess s
let preprocess_block s = !ref_preprocess_block s
+ let extension_from s = !ref_extension_from s
end
let set_extension_handler = Extensions.set_extension_handler
let is_extension = Extensions.is_extension
@@ -55,6 +58,7 @@ let is_extension_block = Extensions.is_extension_block
let extension_category = Extensions.category
let preprocess_extension = Extensions.preprocess
let preprocess_extension_block = Extensions.preprocess_block
+let extension_from = Extensions.extension_from
module CurrentLoc = Cil_const.CurrentLoc
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index efbcc9e7914..377fe8b74d8 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -39,6 +39,9 @@ val preprocess_extension:
val preprocess_extension_block:
string -> string * Logic_ptree.extended_decl list -> string * Logic_ptree.extended_decl list
+(** Return the plugin name of the extension *)
+val extension_from : string -> string
+
(** {2 Global Tables} *)
module Logic_info: State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_info list
@@ -221,6 +224,7 @@ val set_extension_handler:
preprocess_block:
(string -> string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list) ->
+ extension_from:(string -> string) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index d87271e5fc7..fb392e0cca0 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -420,8 +420,8 @@ let () =
let parse context = context.type_term context (get_state context) in
Ext_terms (List.map (parse context) args)
in
- Acsl_extension.register_behavior "taints" (typer `Post) false;
- Acsl_extension.register_code_annot_next_stmt "taint" (typer `Pre) false
+ Acsl_extension.register_behavior ~plugin:"eva" "taints" (typer `Post) false;
+ Acsl_extension.register_code_annot_next_stmt ~plugin:"eva" "taint" (typer `Pre) false
(* Interpretation of logic by the taint domain, using the cvalue domain. *)
module TaintLogic = struct
diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index 8a626416fec..ceb834c1e97 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -99,7 +99,7 @@ struct
| Stmt -> Acsl_extension.register_code_annot_next_stmt
| Loop -> Acsl_extension.register_code_annot_next_loop
in
- register name typer ~printer false
+ register ~plugin:"eva" name typer ~printer false
let get stmt =
let filter_add _emitter annot acc =
diff --git a/src/plugins/eva/utils/widen_hints_ext.ml b/src/plugins/eva/utils/widen_hints_ext.ml
index 303056a3ad1..31ceab2ccc3 100644
--- a/src/plugins/eva/utils/widen_hints_ext.ml
+++ b/src/plugins/eva/utils/widen_hints_ext.ml
@@ -161,7 +161,7 @@ let printer _pp fmt ext =
let () =
Acsl_extension.register_code_annot_next_both
- "widen_hints" typer ~printer false
+ ~plugin:"eva" "widen_hints" typer ~printer false
let get_widen_hints_annots stmt =
Annotations.fold_code_annot
diff --git a/src/plugins/wp/Probe.ml b/src/plugins/wp/Probe.ml
index 9c5aa89d7e3..4140b0ea540 100644
--- a/src/plugins/wp/Probe.ml
+++ b/src/plugins/wp/Probe.ml
@@ -99,7 +99,7 @@ let register () =
if not !registered && Wp_parameters.Probes.get () then
begin
registered := true ;
- Acsl_extension.register_code_annot "probe" parse_probe false ;
+ Acsl_extension.register_code_annot ~plugin:"wp" "probe" parse_probe false ;
end
let () = Cmdline.run_after_configuring_stage register
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index e4e46b8c140..a6552be06d3 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -319,9 +319,9 @@ let register () =
let printer hmap pp _ fmt = function
| Ext_id id -> Option.iter (pp fmt) (Hashtbl.find_opt hmap id)
| _ -> () in
- Acsl_extension.register_global "strategy"
+ Acsl_extension.register_global ~plugin:"wp" "strategy"
~printer:(printer sid pp_strategy) parse_strategy false ;
- Acsl_extension.register_global "proof"
+ Acsl_extension.register_global ~plugin:"wp" "proof"
~printer:(printer hid pp_hint) parse_proofs false ;
end
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index b6956f0222f..d34ad61347c 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -851,7 +851,7 @@ struct
end
let () =
- Acsl_extension.register_behavior
+ Acsl_extension.register_behavior ~plugin:"wp"
"wp_nullable_args" Nullable_extension.typer false
module HasNullable =
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index d32aaf7a785..e01ea2a1535 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -498,7 +498,7 @@ let register () =
then
begin
registered := true ;
- Acsl_extension.register_behavior "region"
+ Acsl_extension.register_behavior ~plugin:"wp" "region"
typecheck ~printer:pp_extension false
end
--
GitLab