From 9c480a7394747023cec9043fdae335c6f7dc760c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 28 Jan 2020 16:14:07 +0100
Subject: [PATCH] [ACSL ext] Hides some implementation details
---
.../ast_queries/acsl_extension.ml | 66 +++++++++----------
.../ast_queries/acsl_extension.mli | 37 ++++++-----
src/plugins/value/utils/eva_annotations.ml | 6 +-
src/plugins/value/utils/widen_hints_ext.ml | 6 +-
src/plugins/wp/RegionAnnot.ml | 6 +-
src/plugins/wp/dyncall.ml | 4 +-
tests/spec/Extend.ml | 36 +++++-----
tests/spec/Extend_preprocess.ml | 8 +--
tests/spec/extend_extern.ml | 4 +-
9 files changed, 82 insertions(+), 91 deletions(-)
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index b8b92d6f74a..93c4d883ef2 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -24,46 +24,46 @@ open Cil_types
open Logic_typing
open Logic_ptree
-type extension_info = {
- ext_status: bool ;
- ext_preprocess: extension_preprocessing ;
- ext_typing: extension_typing ;
- ext_visit: extension_visit ;
- ext_printing: extension_printing ;
+type extension = {
+ status: bool ;
+ preprocessor: extension_preprocessor ;
+ typer: extension_typer ;
+ visitor: extension_visitor ;
+ printer: extension_printer ;
}
-and extension_preprocessing =
+and extension_preprocessor =
lexpr list -> lexpr list
-and extension_typing =
+and extension_typer =
typing_context -> location -> lexpr list -> acsl_extension_kind
-and extension_visit =
+and extension_visitor =
Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
-and extension_printing =
+and extension_printer =
Printer_api.extensible_printer_type -> Format.formatter ->
acsl_extension_kind -> unit
(* Default extension *)
-let default_preprocessing = Extlib.id
+let default_preprocessor = Extlib.id
-let default_typing typing_context loc l =
+let default_typer typing_context loc l =
let _ = loc in
let typing = typing_context.type_predicate typing_context (Lenv.empty ()) in
Ext_preds (List.map typing l)
-let default_visit _ _ = Cil.DoChildren
+let default_visitor _ _ = Cil.DoChildren
-let default_printing printer fmt = function
+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
-let default = {
- ext_status = false ;
- ext_preprocess = default_preprocessing ;
- ext_typing = default_typing ;
- ext_printing = default_printing ;
- ext_visit = default_visit ;
-}
+let make
+ ?(status=false)
+ ?(preprocessor=default_preprocessor)
+ ?(typer=default_typer)
+ ?(visitor=default_visitor)
+ ?(printer=default_printer)
+ () = { status ; preprocessor ; typer ; visitor ; printer }
module Extensions = struct
let ext_tbl = Hashtbl.create 5
@@ -85,16 +85,16 @@ module Extensions = struct
name
else Hashtbl.add ext_tbl name (category, info)
- let preprocess name = (find name).ext_preprocess
+ let preprocess name = (find name).preprocessor
let typing name typing_context loc es =
let ext_info = find name in
- let status = ext_info.ext_status in
- let typer = ext_info.ext_typing in
+ let status = ext_info.status in
+ let typer = ext_info.typer in
status, (typer typing_context loc es)
- let print name = (find name).ext_printing
- let visit name = (find name).ext_visit
+ let print name = (find name).printer
+ let visit name = (find name).visitor
end
(* Registration *)
@@ -137,7 +137,7 @@ let deprecated_find ?(strong=true) name cat op_name =
match Hashtbl.find_opt Extensions.ext_tbl name with
| None ->
if strong then Hashtbl.add strong_cat name cat ;
- (cat, default)
+ (cat, make ())
| Some (found_cat, ext) ->
if strong && Hashtbl.mem strong_cat name then begin
if found_cat = cat then (cat, ext)
@@ -152,19 +152,19 @@ let deprecated_find ?(strong=true) name cat op_name =
end else
(found_cat, ext)
-let deprecated_register_typing name cat ext_status ext_typing =
+let deprecated_register_typing name cat status typer =
let cat, ext = deprecated_find name cat "typing" in
- let ext = { ext with ext_status ; ext_typing } in
+ let ext = { ext with status ; typer } in
deprecated_replace name (cat, ext)
-let deprecated_register_printing name cat ext_printing =
+let deprecated_register_printing name cat printer =
let cat, ext = deprecated_find ~strong:false name cat "printing" in
- let ext = { ext with ext_printing } in
+ let ext = { ext with printer } in
deprecated_replace name (cat, ext)
-let deprecated_register_visit name cat ext_visit =
+let deprecated_register_visit name cat visitor =
let cat, ext = deprecated_find name cat "visit" in
- let ext = { ext with ext_visit } in
+ let ext = { ext with visitor } in
deprecated_replace name (cat, ext)
let () =
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 8e9d0dae0db..d766cd9e077 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -24,28 +24,29 @@ open Cil_types
open Logic_typing
open Logic_ptree
-type extension_info = {
- ext_status: bool ;
- ext_preprocess: extension_preprocessing ;
- ext_typing: extension_typing ;
- ext_visit: extension_visit ;
- ext_printing: extension_printing ;
-}
-and extension_preprocessing =
+type extension
+
+type extension_preprocessor =
lexpr list -> lexpr list
-and extension_typing =
+type extension_typer =
typing_context -> location -> lexpr list -> acsl_extension_kind
-and extension_visit =
+type extension_visitor =
Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
-and extension_printing =
+type extension_printer =
Printer_api.extensible_printer_type -> Format.formatter ->
acsl_extension_kind -> unit
-val default: extension_info
+val make:
+ ?status:bool ->
+ ?preprocessor:extension_preprocessor ->
+ ?typer:extension_typer ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer ->
+ unit -> extension
-val register_behavior: string -> extension_info -> unit
-val register_global: string -> extension_info -> unit
-val register_code_annot: string -> extension_info -> unit
-val register_code_annot_next_stmt: string -> extension_info -> unit
-val register_code_annot_next_loop: string -> extension_info -> unit
-val register_code_annot_next_both: string -> extension_info -> unit
\ No newline at end of file
+val register_behavior: string -> extension -> unit
+val register_global: string -> extension -> unit
+val register_code_annot: string -> extension -> unit
+val register_code_annot_next_stmt: string -> extension -> unit
+val register_code_annot_next_loop: string -> extension -> unit
+val register_code_annot_next_both: string -> extension -> unit
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 7424276f091..ca5a1f0913e 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -69,16 +69,16 @@ module Register (M : Annotation) =
struct
include M
- let ext_typing typing_context loc args =
+ let typer typing_context loc args =
try export (parse ~typing_context args)
with Parse_error ->
typing_context.Logic_typing.error loc "Invalid %s directive" name
- let ext_printing _pp fmt lp =
+ let printer _pp fmt lp =
print fmt (import lp)
let () =
- let ext = { Acsl_extension.default with ext_typing ; ext_printing } in
+ let ext = Acsl_extension.make ~typer ~printer () in
if is_loop_annot then
Acsl_extension.register_code_annot_next_loop name ext
else
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index b86b353196a..90e2f8e3ada 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -137,14 +137,14 @@ let widen_hint_terms_of_terms terms =
with
Invalid_hint -> None
-let ext_typing typing_context loc args =
+let typer typing_context loc args =
let var_term, hint_terms =
terms_of_parsed_widen_hints typing_context loc args
in
let terms = var_term :: hint_terms in
Ext_terms terms
-let ext_printing _pp fmt ext =
+let printer _pp fmt ext =
match ext with
| Ext_id _ -> assert false
| Ext_preds _ -> assert false
@@ -160,7 +160,7 @@ let ext_printing _pp fmt ext =
let () =
Acsl_extension.register_code_annot_next_both "widen_hints"
- { Acsl_extension.default with ext_typing ; ext_printing }
+ (Acsl_extension.make ~typer ~printer ())
let get_widen_hints_annots stmt =
Annotations.fold_code_annot
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index 2287453b699..e3b44d751e2 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -484,10 +484,8 @@ let register () =
if Wp.Region.get () || Wp.Region_annot.get () ||
List.exists specified (Wp.Model.get ())
then
- Acsl_extension.register_behavior "region"
- { Acsl_extension.default with ext_status=true;
- ext_typing=typecheck;
- ext_printing=pp_extension}
+ Acsl_extension.(register_behavior "region"
+ (make ~status:true ~typer:typecheck ~printer:pp_extension ()))
let () = Cmdline.run_after_configuring_stage register
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index 83aeeb8578a..8ddd80fe51d 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -261,9 +261,7 @@ let register =
if (not !once) &&
Wp_parameters.DynCall.get () then begin
once := true;
- let ext =
- { Acsl_extension.default with ext_status=true; ext_typing=typecheck }
- in
+ let ext = Acsl_extension.make ~status:true ~typer:typecheck () in
Acsl_extension.register_code_annot_next_stmt "calls" ext;
Acsl_extension.register_behavior "instanceof" ext;
end
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index ce95063c1e0..d29cffbb072 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -105,26 +105,22 @@ let type_bla typing_context _loc l =
Ext_preds l
let () =
- Acsl_extension.register_behavior "foo"
- { Acsl_extension.default with ext_typing = type_foo } ;
- Acsl_extension.register_code_annot_next_loop "lfoo"
- { Acsl_extension.default with ext_typing = type_foo } ;
- Acsl_extension.register_code_annot "ca_foo"
- { Acsl_extension.default with ext_typing = type_foo } ;
- Acsl_extension.register_code_annot_next_stmt "ns_foo"
- { Acsl_extension.default with ext_typing = type_foo } ;
- Acsl_extension.register_global "global_foo"
- { Acsl_extension.default with ext_typing = type_foo } ;
- Acsl_extension.register_behavior "bar"
- { Acsl_extension.default with
- ext_typing = type_bar ;
- ext_printing = print_bar ;
- ext_visit = visit_bar
- } ;
- Acsl_extension.register_behavior "bla"
- { Acsl_extension.default with ext_typing = type_bla } ;
- Acsl_extension.register_code_annot_next_both "baz"
- { Acsl_extension.default with ext_typing = type_baz }
+ Acsl_extension.(register_behavior "foo"
+ (make ~typer:type_foo ())) ;
+ Acsl_extension.(register_code_annot_next_loop "lfoo"
+ (make ~typer:type_foo ())) ;
+ Acsl_extension.(register_code_annot "ca_foo"
+ (make ~typer:type_foo ())) ;
+ Acsl_extension.(register_code_annot_next_stmt "ns_foo"
+ (make ~typer:type_foo ())) ;
+ Acsl_extension.(register_global "global_foo"
+ (make ~typer:type_foo ())) ;
+ Acsl_extension.(register_behavior "bar"
+ (make ~typer:type_bar ~printer:print_bar ~visitor:visit_bar ())) ;
+ Acsl_extension.(register_behavior "bla"
+ (make ~typer:type_bla ())) ;
+ Acsl_extension.(register_code_annot_next_both "baz"
+ (make ~typer:type_baz ()))
let run () =
Ast.compute ();
diff --git a/tests/spec/Extend_preprocess.ml b/tests/spec/Extend_preprocess.ml
index d2905255e14..32ff035e04f 100644
--- a/tests/spec/Extend_preprocess.ml
+++ b/tests/spec/Extend_preprocess.ml
@@ -37,11 +37,9 @@ let preprocess_foo_ptree_element kind = function
let preprocess_foo_ptree kind = List.map (preprocess_foo_ptree_element kind)
let register registration kind =
- let ext = {
- Acsl_extension.default with
- ext_typing = ext_typing kind ;
- ext_preprocess = preprocess_foo_ptree kind
- } in
+ let typer = ext_typing kind in
+ let preprocessor = preprocess_foo_ptree kind in
+ let ext = Acsl_extension.make ~typer ~preprocessor () in
registration (kind ^ "_foo") ext
let () =
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index 09714efad25..c2e055f5f90 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -6,7 +6,7 @@ let load_theory = function
raise Not_found
| _ -> assert false
-let ext_typing typing_context loc lexprs =
+let typer typing_context loc lexprs =
ignore loc ;
let type_predicate =
typing_context.type_predicate typing_context (Lenv.empty ())
@@ -17,7 +17,7 @@ let ext_typing typing_context loc lexprs =
let () =
- Acsl_extension.(register_global "why3" { default with ext_typing })
+ Acsl_extension.(register_global "why3" (make ~typer ()))
let main () =
try
--
GitLab