From 7295a3eb6cc59c2f2a235cd7b39da7277ea67117 Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@kit.edu>
Date: Mon, 6 Jul 2020 16:19:48 +0200
Subject: [PATCH] Add support of recursive extended global annotations
---
src/kernel_internals/parsing/logic_lexer.mll | 7 +-
src/kernel_internals/parsing/logic_parser.mly | 34 +++-
src/kernel_internals/typing/mergecil.ml | 8 +-
src/kernel_services/ast_data/cil_types.mli | 2 +-
.../ast_printing/cil_types_debug.ml | 3 +-
.../ast_printing/logic_print.ml | 12 +-
.../ast_queries/acsl_extension.ml | 168 +++++++++++++++---
.../ast_queries/acsl_extension.mli | 14 ++
src/kernel_services/ast_queries/cil.ml | 4 +-
src/kernel_services/ast_queries/logic_env.ml | 11 +-
src/kernel_services/ast_queries/logic_env.mli | 8 +
.../ast_queries/logic_typing.ml | 18 +-
.../ast_queries/logic_typing.mli | 17 ++
.../ast_queries/logic_utils.ml | 4 +-
src/kernel_services/parsetree/logic_ptree.mli | 12 +-
15 files changed, 275 insertions(+), 47 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index b86e9200489..d31c8c679e0 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -207,7 +207,12 @@
match Logic_env.extension_category s with
| exception Not_found -> None
| Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
- | Cil_types.Ext_global -> Some (EXT_GLOBAL s)
+ | Cil_types.Ext_global ->
+ begin
+ match Logic_env.is_extension_block s with
+ | false -> Some (EXT_GLOBAL s)
+ | true -> Some (EXT_GLOBAL_BLOCK s)
+ end
| Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
end
else None
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 0bff4b69eda..121ad96facc 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -107,6 +107,8 @@
let loc_decl d = { decl_node = d; decl_loc = loc () }
+ let loc_ext d = { extended_node = d; extended_loc = loc () }
+
let concat_froms a1 a2 =
let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
(* NB: the following has an horrible complexity, but the order of
@@ -253,7 +255,7 @@
%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
%token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
-%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_CONTRACT
+%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
%token LOGIC PREDICATE INDUCTIVE AXIOMATIC AXIOM LEMMA LBRACE RBRACE
@@ -1532,13 +1534,34 @@ decl:
| type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1}
| logic_def { $1 }
-| EXT_GLOBAL grammar_extension SEMICOLON {
- let processed = Logic_env.preprocess_extension $1 $2 in
- LDextended ($1, processed)
- }
+| ext_decl { LDextended $1 }
| deprecated_logic_decl { $1 }
;
+ext_decl:
+| EXT_GLOBAL grammar_extension SEMICOLON {
+ let processed = Logic_env.preprocess_extension $1 $2 in
+ Ext_lexpr($1, processed)
+ }
+| EXT_GLOBAL_BLOCK any_identifier LBRACE ext_decls RBRACE {
+ let processed_id,processed_block =
+ Logic_env.preprocess_extension_block $1 ($2,$4)
+ in
+ Ext_extension($1,processed_id,processed_block)
+ }
+;
+
+ext_decls:
+| /* epsilon */
+ { [] }
+| ext_decl_loc ext_decls
+ { $1::$2 }
+;
+
+ext_decl_loc:
+| ext_decl { loc_ext $1 }
+;
+
volatile_opt:
| /* empty */ { None, None }
| READS any_identifier volatile_opt
@@ -1893,6 +1916,7 @@ is_acsl_spec:
is_acsl_decl_or_code_annot:
| EXT_CODE_ANNOT { $1 }
| EXT_GLOBAL { $1 }
+| EXT_GLOBAL_BLOCK { $1 }
| ASSUMES { "assumes" }
| ASSERT { "assert" }
| CHECK { "check" }
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 21989d0a2e8..ed8914b346e 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -452,7 +452,7 @@ module ExtMerging =
| Ext_id i -> Datatype.Int.hash i
| Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
| Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
- | Ext_annot annots -> 5 * (hash_list hash annots)
+ | Ext_annot (id, annots) -> Datatype.String.hash id + 5 * (hash_list hash annots)
in
Datatype.String.hash e.ext_name + 5 * hash_ext_kind e.ext_kind
let rec compare (e1 : acsl_extension) (e2 : acsl_extension) =
@@ -466,8 +466,10 @@ module ExtMerging =
| Ext_preds p1, Ext_preds p2 ->
Extlib.list_compare Logic_utils.compare_predicate p1 p2
| Ext_preds _, _ -> 1 | _, Ext_preds _ -> -1
- | Ext_annot a1 , Ext_annot a2 ->
- Extlib.list_compare compare a1 a2
+ | Ext_annot (id1, a1) , Ext_annot (id2, a2) ->
+ match String.compare id1 id2 with
+ | 0 -> Extlib.list_compare compare a1 a2
+ | n -> n
in
let res = Datatype.String.compare e1.ext_name e2.ext_name in
if res <> 0 then res
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 5f182a4a885..c13132d03e3 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1692,7 +1692,7 @@ and acsl_extension_kind =
| Ext_id of int (** id used internally by the extension itself. *)
| Ext_terms of term list
| Ext_preds of predicate list
- | Ext_annot of acsl_extension list
+ | Ext_annot of string * acsl_extension list
(** a list of predicates, the most common case of for extensions *)
(** Where are we expected to find corresponding extension keyword.
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 45e5515947e..9ce30a3dac1 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -921,7 +921,8 @@ and pp_acsl_extension_kind fmt = function
| Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)" pp_int int
| Ext_terms(term_list) -> Format.fprintf fmt "Ext_terms(%a)" (pp_list pp_term) term_list
| Ext_preds(predicate_list) -> Format.fprintf fmt "Ext_preds(%a)" (pp_list pp_predicate) predicate_list
- | Ext_annot(annotation_list ) -> Format.fprintf fmt "Ext_annots(%a)" (pp_list pp_acsl_extension) annotation_list
+ | Ext_annot(string,annotation_list) ->
+ Format.fprintf fmt "Ext_annots(%a,%a)" pp_string string (pp_list pp_acsl_extension) annotation_list
and pp_behavior fmt behavior =
Format.fprintf fmt
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 1b3c0544fc3..59f6809727d 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -311,6 +311,15 @@ let print_model_annot fmt ty =
(print_logic_type None) ty.model_type
ty.model_name
+let rec print_extended_decl fmt d =
+ let aux fmt d = print_extended_decl fmt d.extended_node in
+ match d with
+ | Ext_lexpr(name,d) ->
+ fprintf fmt "@[<2>%s@ %a@]" name (pp_list ~sep:",@ " print_lexpr) d
+ | Ext_extension(name,id,d) ->
+ fprintf fmt "@[<2>%s@ %s@ {@\n%a@]@\n}" name id
+ (pp_list ~sep:"@\n" aux) d
+
let rec print_decl fmt d =
match d.decl_node with
| LDlogic_def(name,labels,tvar,rt,prms,body) ->
@@ -374,8 +383,7 @@ let rec print_decl fmt d =
(pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" print_lexpr) tsets
(pp_opt ~pre:"@ reads@ " pp_print_string) read
(pp_opt ~pre:"@ writes@ " pp_print_string) write
- | LDextended (s,l) ->
- fprintf fmt "@[<2>%s@ %a@]" s (pp_list ~sep:",@ " print_lexpr) l
+ | LDextended d -> print_extended_decl fmt d
let print_deps fmt deps =
match deps with
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 0d3efe6680d..3fb8572e723 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -28,16 +28,36 @@ type extension_preprocessor =
lexpr list -> lexpr list
type extension_typer =
typing_context -> location -> lexpr list -> acsl_extension_kind
+type extension_preprocessor_block =
+ string * extended_decl list -> string * extended_decl list
+type extension_typer_block =
+ typing_context -> location -> string * extended_decl list -> acsl_extension_kind
type extension_visitor =
Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
type extension_printer =
Printer_api.extensible_printer_type -> Format.formatter ->
acsl_extension_kind -> unit
-type extension = {
+type extension_part1 = {
+ preprocessor: extension_preprocessor ;
+ typer: extension_typer ;
+ status: bool ;
+}
+type extension_part2 = {
category: ext_category ;
+ visitor: extension_visitor ;
+ printer: extension_printer ;
+ short_printer: extension_printer ;
+}
+type extension_part3 = {
+ preprocessor: extension_preprocessor_block ;
+ typer: extension_typer_block ;
status: bool ;
+}
+type extension = {
preprocessor: extension_preprocessor ;
typer: extension_typer ;
+ status: bool ;
+ category: ext_category ;
visitor: extension_visitor ;
printer: extension_printer ;
short_printer: extension_printer ;
@@ -47,10 +67,13 @@ let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i
| Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
| Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
- | Ext_annot an -> Pretty_utils.pp_list ~sep:",@ " printer#extended fmt an
+ | Ext_annot (id,an) -> Format.fprintf fmt "@[<v 2>@[%s@ {@]@\n%a}@]@\n"
+ id (Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
+ printer#extended) an
-let default_short_printer name _printer fmt _ext_kind =
- Format.fprintf fmt "%s" name
+let default_short_printer name printer fmt = function
+ | Ext_id _ | Ext_terms _ | Ext_preds _ -> Format.fprintf fmt "%s" name
+ | Ext_annot (id,an) -> Format.fprintf fmt "%s@ {@\n%a@]@\n}" id (Pretty_utils.pp_list ~sep:"@\n" printer#extended) an
let make
name category
@@ -59,15 +82,39 @@ let make
?(visitor=fun _ _ -> Cil.DoChildren)
?(printer=default_printer)
?(short_printer=default_short_printer name)
- status =
- { category; status; preprocessor; typer; visitor; printer; short_printer }
+ status : extension_part1*extension_part2 =
+ { preprocessor; typer; status},{ category; visitor; printer; short_printer }
+
+let make_block
+ name category
+ ?(preprocessor=Extlib.id)
+ typer
+ ?(visitor=fun _ _ -> Cil.DoChildren)
+ ?(printer=default_printer)
+ ?(short_printer=default_short_printer name)
+ status : extension_part3*extension_part2 =
+ { preprocessor; typer; status},{ category; visitor; printer; short_printer }
module Extensions = struct
+ (*hash table for category, visitor, printer and short_priner of extensions*)
let ext_tbl = Hashtbl.create 5
- let find name =
- try Hashtbl.find ext_tbl name
- with Not_found ->
+ (*hash table for status, preprocessor and typer of standard extensions*)
+ let ext_sta_tbl = Hashtbl.create 5
+
+ (*hash table for status, preprocessor and visitor of block extensions*)
+ let ext_block_tbl = Hashtbl.create 5
+
+ let find_part1 name :extension_part1 =
+ try Hashtbl.find ext_sta_tbl name with Not_found ->
+ Kernel.fatal ~current:true "unsupported clause of name '%s'" name
+
+ let find_part2 name :extension_part2 =
+ try Hashtbl.find ext_tbl name with Not_found ->
+ Kernel.fatal ~current:true "unsupported clause of name '%s'" name
+
+ let find_part3 name :extension_part3 =
+ try Hashtbl.find ext_block_tbl name with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
(* [Logic_lexer] can ask for something that is not a category, which is not
@@ -76,21 +123,60 @@ module Extensions = struct
let is_extension = Hashtbl.mem ext_tbl
+ let is_extension_block = Hashtbl.mem ext_block_tbl
+
let register
cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
- let info =
+ let info1,info2 =
make name cat ?preprocessor typer ?visitor ?printer ?short_printer status
in
if is_extension name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
"Trying to register ACSL extension %s twice. Ignoring second extension"
name
- else Hashtbl.add ext_tbl name info
+ else
+ begin
+ Hashtbl.add ext_sta_tbl name info1;
+ Hashtbl.add ext_tbl name info2
+ end
+
+ let register_block
+ cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
+ let info1,info2 =
+ make_block name cat ?preprocessor typer ?visitor ?printer ?short_printer status
+ in
+ if is_extension name then
+ Kernel.warning ~wkey:Kernel.wkey_acsl_extension
+ "Trying to register ACSL extension %s twice. Ignoring second extension"
+ name
+ else
+ begin
+ Hashtbl.add ext_block_tbl name info1;
+ Hashtbl.add ext_tbl name info2
+ end
- let preprocess name = (find name).preprocessor
+ let preprocess name = (find_part1 name).preprocessor
+
+ let preprocess_block name = (find_part3 name).preprocessor
+
+ let typing name typing_context loc es =
+ let ext_info = find_part1 name in
+ let status = ext_info.status in
+ let typer = ext_info.typer in
+ let normal_error = ref false in
+ let has_error () = normal_error := true in
+ let wrapper =
+ typing_context.on_error (typer typing_context loc) has_error
+ in
+ try status, wrapper es
+ with
+ | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
+ | exn when not !normal_error ->
+ Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
+ name (Printexc.to_string exn)
- let typing name typing_context loc es =
- let ext_info = find name in
+ let typing_block name typing_context loc es =
+ let ext_info = find_part3 name in
let status = ext_info.status in
let typer = ext_info.typer in
let normal_error = ref false in
@@ -105,14 +191,14 @@ module Extensions = struct
Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
name (Printexc.to_string exn)
- let visit name = (find name).visitor
+ let visit name = (find_part2 name).visitor
let print name printer fmt kind =
- let pp = (find name).printer printer in
+ let pp = (find_part2 name).printer printer in
Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
let short_print name printer fmt kind =
- let pp = (find name).short_printer in
+ let pp = (find_part2 name).short_printer in
Format.fprintf fmt "%a" (pp printer) kind
end
@@ -122,6 +208,8 @@ let register_behavior =
Extensions.register Ext_contract
let register_global =
Extensions.register Ext_global
+let register_global_block =
+ Extensions.register_block Ext_global
let register_code_annot =
Extensions.register (Ext_code_annot Ext_here)
let register_code_annot_next_stmt =
@@ -137,10 +225,13 @@ let () =
Logic_env.set_extension_handler
~category:Extensions.category
~is_extension: Extensions.is_extension
- ~preprocess: Extensions.preprocess ;
+ ~preprocess: Extensions.preprocess
+ ~is_extension_block: Extensions.is_extension_block
+ ~preprocess_block: Extensions.preprocess_block;
Logic_typing.set_extension_handler
~is_extension: Extensions.is_extension
- ~typer: Extensions.typing ;
+ ~typer: Extensions.typing
+ ~typer_block: Extensions.typing_block ;
Cil.set_extension_handler
~visit: Extensions.visit ;
Cil_printer.set_extension_handler
@@ -149,21 +240,45 @@ let () =
(* For Deprecation: *)
-let deprecated_replace name ext = Hashtbl.add Extensions.ext_tbl name ext
+let deprecated_replace name ext =
+ let info1:extension_part1 = {
+ preprocessor = ext.preprocessor ;
+ typer = ext.typer ;
+ status = ext.status ;
+ }
+ in
+ let info2:extension_part2 = {
+ category = ext.category ;
+ visitor = ext.visitor ;
+ printer = ext.printer ;
+ short_printer = ext.printer ;
+ }
+ in
+ Hashtbl.add Extensions.ext_sta_tbl name info1;
+ Hashtbl.add Extensions.ext_tbl name info2
let strong_cat = Hashtbl.create 5
let default_typer _typing_context _loc _l = assert false
+let merge ((info1:extension_part1),(info2:extension_part2)) :extension =
+ {preprocessor = info1.preprocessor ;
+ typer = info1.typer ;
+ status = info1.status ;
+ category = info2.category ;
+ visitor = info2.visitor ;
+ printer = info2.printer ;
+ short_printer = info2.printer}
let deprecated_find ?(strong=true) name cat op_name =
- match Hashtbl.find_opt Extensions.ext_tbl name with
+ match Hashtbl.find_opt Extensions.ext_sta_tbl name with
| None ->
if strong then Hashtbl.add strong_cat name cat ;
- (make name cat default_typer false)
- | Some ext ->
+ merge (make name cat default_typer false)
+ | Some ext1 ->
+ let ext2 = Extensions.find_part2 name in
if strong && Hashtbl.mem strong_cat name then begin
- if ext.category = cat then ext
+ if ext2.category = cat then merge (ext1,ext2)
else
Kernel.fatal
"Registring %s for %s: this extension already exists for another \
@@ -171,8 +286,9 @@ let deprecated_find ?(strong=true) name cat op_name =
op_name name
end else if strong then begin
Hashtbl.add strong_cat name cat ;
- { ext with category = cat }
- end else ext
+ let ext2 = { ext2 with category = cat } in
+ merge (ext1,ext2)
+ end else merge (ext1,ext2)
let deprecated_register_typing name cat status typer =
deprecated_replace name
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index c2778433fb9..c615564b73e 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -38,6 +38,10 @@ type extension_typer =
(** Visitor functions for ACSL extensions *)
type extension_visitor =
Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
+type extension_preprocessor_block =
+ string * extended_decl list -> string * extended_decl list
+type extension_typer_block =
+ typing_context -> location -> string * extended_decl list -> acsl_extension_kind
(** Pretty printers for ACSL extensions *)
type extension_printer =
Printer_api.extensible_printer_type -> Format.formatter ->
@@ -106,6 +110,16 @@ val register_global:
?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
unit
+(** Registers extension for global block annotation. See [register_behavior].
+
+ @plugin development guide
+*)
+val register_global_block:
+ string -> ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+ unit
+
(** Registers extension for code annotation to be evaluated at _current_
program point. See [register_behavior].
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index f99204de3a4..6f90ae11d73 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1994,9 +1994,9 @@ and childrenCilExtended vis p =
| Ext_preds preds ->
let preds' = mapNoCopy (visitCilPredicate vis) preds in
if preds == preds' then p else Ext_preds preds'
- | Ext_annot annots ->
+ | Ext_annot (id,annots) ->
let annots' = mapNoCopy (visitCilExtended vis) annots in
- if annots == annots' then p else Ext_annot annots'
+ if annots == annots' then p else Ext_annot (id,annots')
and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index dde299d846e..18381986562 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -29,23 +29,32 @@ module Extensions = struct
let ref_is_extension = ref (fun _ -> assert false)
let ref_category = ref (fun _ -> assert false)
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 set_extension_handler ~category ~is_extension ~preprocess =
+ let set_extension_handler
+ ~category ~is_extension ~preprocess ~is_extension_block ~preprocess_block =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_category := category ;
ref_preprocess := preprocess ;
+ ref_is_extension_block := is_extension_block;
+ ref_preprocess_block := preprocess_block;
initialized := true ;
()
let is_extension s = !ref_is_extension s
+ let is_extension_block s = !ref_is_extension_block s
let category s = !ref_category s
let preprocess s = !ref_preprocess s
+ let preprocess_block s = !ref_preprocess_block s
end
let set_extension_handler = Extensions.set_extension_handler
let is_extension = Extensions.is_extension
+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
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 407ac539994..954eb3645d1 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -29,12 +29,16 @@ open Cil_types
(** {2 registered ACSL extensions } *)
val is_extension: string -> bool
+val is_extension_block: string -> bool
val extension_category: string -> ext_category
val preprocess_extension:
string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list
+val preprocess_extension_block:
+ string -> string * Logic_ptree.extended_decl list -> string * Logic_ptree.extended_decl list
+
(** {2 Global Tables} *)
module Logic_info: State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_info list
@@ -208,6 +212,10 @@ val set_extension_handler:
category:(string -> ext_category) ->
is_extension:(string -> bool) ->
preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
+ is_extension_block:(string -> bool) ->
+ preprocess_block:
+ (string -> string * Logic_ptree.extended_decl list ->
+ string * Logic_ptree.extended_decl list) ->
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/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 477044c5523..fcf4ab3aed6 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -528,11 +528,13 @@ 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 set_handler ~is_extension ~typer =
+ let set_handler ~is_extension ~typer ~typer_block =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_typer := typer ;
+ ref_typer_block := typer_block;
initialized := true
let is_extension name = !ref_is_extension name
@@ -540,6 +542,9 @@ module Extensions = struct
let typer name ~typing_context:typing_context ~loc =
!ref_typer name typing_context loc
+ let typer_block name ~typing_context:typing_context ~loc =
+ !ref_typer_block name typing_context loc
+
(* For deprecated functions *)
let ref_deprecated_handler = ref (fun _ _ _ _ -> assert false)
@@ -551,6 +556,8 @@ module Extensions = struct
!ref_deprecated_handler name category status typer
end
let set_extension_handler = Extensions.set_handler
+let get_typer = Extensions.typer
+let get_typer_block = Extensions.typer_block
(* Deprecated ACSL extensions functions *)
let set_deprecated_extension_handler =
@@ -4281,11 +4288,18 @@ struct
let rvi_opt = get_volatile_fct checks_reads_fct rd_opt in
let wvi_opt = get_volatile_fct checks_writes_fct wr_opt in
Dvolatile (tsets, rvi_opt, wvi_opt, [], loc)
- | LDextended (kind, content) ->
+ | LDextended (Ext_lexpr(kind, content)) ->
let typing_context = base_ctxt (Lenv.empty ()) in
let status,tcontent = Extensions.typer kind ~typing_context ~loc content in
let textended = Logic_const.new_acsl_extension kind loc status tcontent in
Dextended (textended, [], loc)
+ | LDextended (Ext_extension (kind, name, content)) ->
+ let typing_context = base_ctxt (Lenv.empty ()) in
+ let status,tcontent =
+ Extensions.typer_block kind ~typing_context ~loc (name,content)
+ in
+ let textended = Logic_const.new_acsl_extension kind loc status tcontent in
+ Dextended (textended, [], loc)
let annot a =
start_transaction ();
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 3c4c2975d97..e1c613d9e29 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -389,12 +389,29 @@ val set_extension_handler:
is_extension:(string -> bool) ->
typer:(string -> typing_context -> location -> Logic_ptree.lexpr list ->
(bool * acsl_extension_kind)) ->
+ typer_block:(string -> typing_context ->
+ Filepath.position * Filepath.position ->
+ string * Logic_ptree.extended_decl list ->
+ bool * Cil_types.acsl_extension_kind) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this
@since 21.0-Scandium
*)
+val get_typer :
+ string ->
+ typing_context:typing_context ->
+ loc:Filepath.position * Filepath.position ->
+ Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind
+
+val get_typer_block:
+ string ->
+ typing_context:typing_context ->
+ loc:Logic_ptree.location ->
+ string * Logic_ptree.extended_decl list ->
+ bool * Cil_types.acsl_extension_kind
+
(**/**)
val set_deprecated_extension_handler:
handler:(string -> ext_category -> bool ->
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 481fc909734..acdcb97f4f8 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1195,8 +1195,8 @@ let rec is_same_extension x1 x2 =
is_same_list is_same_term t1 t2
| Ext_preds p1, Ext_preds p2 ->
is_same_list is_same_predicate p1 p2
- | Ext_annot a1, Ext_annot a2 ->
- is_same_list is_same_extension a1 a2
+ | Ext_annot (id1, a1), Ext_annot (id2, a2) ->
+ is_same_string id1 id2 && is_same_list is_same_extension a1 a2
| (Ext_id _ | Ext_preds _ | Ext_terms _ | Ext_annot _ ), _ -> false
let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index bff3332bb8d..ccc7a1d24af 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -248,7 +248,8 @@ and decl_node =
| LDmodel_annot of model_annot (** model field. *)
| LDvolatile of lexpr list * (string option * string option)
(** volatile clause read/write. *)
- | LDextended of extension (** extended global annotation. *)
+ | LDextended of global_extension (** extended global annotation. *)
+
(** dependencies of an assigned location. *)
and deps =
@@ -273,6 +274,15 @@ and allocation =
(** variant of a loop or a recursive function. *)
and variant = lexpr * string option
+and global_extension =
+ | Ext_lexpr of string * lexpr list
+ | Ext_extension of string * string * extended_decl list
+
+and extended_decl = {
+ extended_node : global_extension;
+ extended_loc : location
+}
+
(** Behavior in a specification. This type shares the name of its constructors
with {!Cil_types.behavior}. *)
type behavior = {
--
GitLab