From da1e2f3475eb69f668753c5499520b261e68d0a1 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 29 Jan 2020 14:06:20 +0100
Subject: [PATCH] [Kernel] Clean ACSL extensions
---
.../ast_printing/cil_printer.ml | 57 ++++++++++---------
.../ast_queries/acsl_extension.mli | 2 -
src/kernel_services/ast_queries/cil.ml | 36 +++++++-----
src/kernel_services/ast_queries/logic_env.ml | 38 +++++++------
.../ast_queries/logic_typing.ml | 31 +++++-----
5 files changed, 93 insertions(+), 71 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 431a6194222..5aa6db6a1c5 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -27,42 +27,47 @@ open Cil_datatype
open Printer_api
open Format
-let initialized_extensions = ref false
-let ref_print_extension = ref (fun _ _ _ _ -> assert false)
-let ref_print_short_extension = ref (fun _ _ _ _ -> assert false)
-
-let set_extension_handler ~print ~short_print =
- assert (not !initialized_extensions) ;
- ref_print_extension := print ;
- ref_print_short_extension := short_print ;
- initialized_extensions := true ;
- ()
-
-let ref_deprecated_extension_handler = ref (fun _ _ _ -> assert false)
-let set_deprecated_extension_handler ~handler =
- ref_deprecated_extension_handler := handler
-
-module Acsl_extensions = struct
- let deprecated_register name =
- !ref_deprecated_extension_handler name
+module Extensions = struct
+ let initialized = ref false
+ let ref_print = ref (fun _ _ _ _ -> assert false)
+ let ref_short_print = ref (fun _ _ _ _ -> assert false)
+
+ let set_handler ~print ~short_print =
+ assert (not !initialized) ;
+ ref_print := print ;
+ ref_short_print := short_print ;
+ initialized := true ;
+ ()
let pp (printer) fmt {ext_name; ext_kind} =
- !ref_print_extension ext_name printer fmt ext_kind
+ !ref_print ext_name printer fmt ext_kind
let pp_short (printer) fmt {ext_name; ext_kind} =
- !ref_print_short_extension ext_name printer fmt ext_kind
+ !ref_short_print ext_name printer fmt ext_kind
+
+ let ref_deprecated_handler = ref (fun _ _ _ -> assert false)
+ let set_deprecated_handler ~handler =
+ ref_deprecated_handler := handler
+
+ let deprecated_register name =
+ !ref_deprecated_handler name
end
+let set_extension_handler = Extensions.set_handler
+
+(* Deprecated functions *)
+let set_deprecated_extension_handler = Extensions.set_deprecated_handler
+
let register_behavior_extension name =
- Acsl_extensions.deprecated_register name Ext_contract
+ Extensions.deprecated_register name Ext_contract
let register_code_annot_extension name =
- Acsl_extensions.deprecated_register name (Ext_code_annot Ext_here)
+ Extensions.deprecated_register name (Ext_code_annot Ext_here)
let register_loop_annot_extension name =
- Acsl_extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
+ Extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
let register_global_extension name =
- Acsl_extensions.deprecated_register name Ext_global
+ Extensions.deprecated_register name Ext_global
(* Internal attributes. Won't be pretty-printed *)
let reserved_attributes = ref []
@@ -2752,10 +2757,10 @@ class cil_printer () = object (self)
self#identified_predicate p
method extended fmt ext =
- Acsl_extensions.pp (self :> extensible_printer_type) fmt ext
+ Extensions.pp (self :> extensible_printer_type) fmt ext
method short_extended fmt ext =
- Acsl_extensions.pp_short (self :> extensible_printer_type) fmt ext
+ Extensions.pp_short (self :> extensible_printer_type) fmt ext
method post_cond fmt (k,p) =
let kw = get_termination_kind_name k in
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 42e2a3b0636..08a181d4ab4 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -24,8 +24,6 @@ open Cil_types
open Logic_typing
open Logic_ptree
-type extension
-
type extension_preprocessor =
lexpr list -> lexpr list
type extension_typer =
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index dc24efcd495..2b2014430b2 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -755,21 +755,31 @@ let alphabetabeta _ x = x
let alphabetafalse _ _ = false
let alphatrue _ = true
-let initialized_extensions = ref false
-let ref_visit_extension = ref (fun _ _ _ -> assert false)
+module Extensions = struct
+ let initialized = ref false
+ let ref_visit = ref (fun _ _ _ -> assert false)
-let set_extension_handler ~visit =
- assert (not !initialized_extensions) ;
- ref_visit_extension := visit ;
- initialized_extensions := true ;
- ()
+ let set_handler ~visit =
+ assert (not !initialized) ;
+ ref_visit := visit ;
+ initialized := true ;
+ ()
+
+ let visit name = !ref_visit name
+
+ let ref_deprecated_handler = ref (fun _ _ _ -> assert false)
+ let set_deprecated_handler ~handler =
+ ref_deprecated_handler := handler
+
+ let register_behavior name ext =
+ !ref_deprecated_handler name Ext_contract ext
+end
+let set_extension_handler = Extensions.set_handler
-let ref_deprecated_extension_handler = ref (fun _ _ _ -> assert false)
-let set_deprecated_extension_handler ~handler =
- ref_deprecated_extension_handler := handler
+(* Deprecated *)
+let set_deprecated_extension_handler = Extensions.set_deprecated_handler
+let register_behavior_extension = Extensions.register_behavior
-let register_behavior_extension name ext =
- !ref_deprecated_extension_handler name Ext_contract ext
(* sm/gn: cil visitor interface for traversing Cil trees. *)
(* Use visitCilStmt and/or visitCilFile to use this. *)
@@ -1901,7 +1911,7 @@ and childrenBehavior vis b =
b
and visitCilExtended vis orig =
- let visit = !ref_visit_extension orig.ext_name in
+ let visit = Extensions.visit orig.ext_name in
let e' = doVisitCil vis id (visit vis) childrenCilExtended orig.ext_kind in
if Visitor_behavior.is_fresh vis#behavior then
Logic_const.new_acsl_extension orig.ext_name orig.ext_loc
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index fdadf34d678..6d040a71c18 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -24,22 +24,28 @@
open Cil_types
-let initialized_extensions = ref false
-let ref_is_extension = ref (fun _ -> assert false)
-let ref_extension_category = ref (fun _ -> assert false)
-let ref_preprocess_extension = ref (fun _ -> assert false)
-
-let set_extension_handler ~category ~is_extension ~preprocess =
- assert (not !initialized_extensions) ;
- ref_is_extension := is_extension ;
- ref_extension_category := category ;
- ref_preprocess_extension := preprocess ;
- initialized_extensions := true ;
- ()
-
-let is_extension s = !ref_is_extension s
-let extension_category s = !ref_extension_category s
-let preprocess_extension s = !ref_preprocess_extension s
+module Extensions = struct
+ let initialized = ref false
+ let ref_is_extension = ref (fun _ -> assert false)
+ let ref_category = ref (fun _ -> assert false)
+ let ref_preprocess = ref (fun _ -> assert false)
+
+ let set_extension_handler ~category ~is_extension ~preprocess =
+ assert (not !initialized) ;
+ ref_is_extension := is_extension ;
+ ref_category := category ;
+ ref_preprocess := preprocess ;
+ initialized := true ;
+ ()
+
+ let is_extension s = !ref_is_extension s
+ let category s = !ref_category s
+ let preprocess s = !ref_preprocess s
+end
+let set_extension_handler = Extensions.set_extension_handler
+let is_extension = Extensions.is_extension
+let extension_category = Extensions.category
+let preprocess_extension = Extensions.preprocess
module CurrentLoc = Cil_const.CurrentLoc
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index aa3797f02bf..e7f783a7582 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -525,33 +525,36 @@ type typing_context = {
}
module Extensions = struct
- let initialized_extensions = ref false
+ let initialized = ref false
let ref_is_extension = ref (fun _ -> assert false)
- let ref_type_extension = ref (fun _ _ _ _ -> assert false)
+ let ref_typer = ref (fun _ _ _ _ -> assert false)
+
+ let set_handler ~is_extension ~typer =
+ assert (not !initialized) ;
+ ref_is_extension := is_extension ;
+ ref_typer := typer ;
+ initialized := true
let is_extension name = !ref_is_extension name
let typer name ~typing_context:typing_context ~loc =
- !ref_type_extension name typing_context loc
+ !ref_typer name typing_context loc
(* For deprecated functions *)
- let ref_deprecated_extension_handler = ref (fun _ _ _ _ -> assert false)
+ let ref_deprecated_handler = ref (fun _ _ _ _ -> assert false)
+
+ let set_deprecated_handler ~handler =
+ ref_deprecated_handler := handler
let deprecated_register name category status typer =
let typer typing_context loc = typer ~typing_context ~loc in
- !ref_deprecated_extension_handler name category status typer
+ !ref_deprecated_handler name category status typer
end
-
-let set_extension_handler ~is_extension ~typer =
- assert (not !Extensions.initialized_extensions) ;
- Extensions.ref_is_extension := is_extension ;
- Extensions.ref_type_extension := typer ;
- Extensions.initialized_extensions := true ;
- ()
+let set_extension_handler = Extensions.set_handler
(* Deprecated ACSL extensions functions *)
-let set_deprecated_extension_handler ~handler =
- Extensions.ref_deprecated_extension_handler := handler
+let set_deprecated_extension_handler =
+ Extensions.set_deprecated_handler
let register_behavior_extension name f =
Extensions.deprecated_register name Ext_contract f
--
GitLab