From ffff36888f38932325f2042cb057f00bce7caddb Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 24 Jan 2020 11:03:25 +0100
Subject: [PATCH] [kernel] Activate Acsl_extension and deprecates old
 registration functions

---
 .../ast_printing/cil_printer.ml               | 37 +++++++--------
 .../ast_printing/cil_printer.mli              | 20 +++++++--
 .../ast_queries/acsl_extension.ml             | 45 +++++++++++++++++++
 src/kernel_services/ast_queries/cil.ml        | 14 +++---
 src/kernel_services/ast_queries/cil.mli       |  7 +++
 src/kernel_services/ast_queries/logic_env.ml  | 12 +----
 src/kernel_services/ast_queries/logic_env.mli |  3 --
 .../ast_queries/logic_typing.ml               | 44 ++++++++----------
 .../ast_queries/logic_typing.mli              | 20 +++++++++
 9 files changed, 131 insertions(+), 71 deletions(-)

diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 98b6fab58ce..ab8aea9acf1 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -36,37 +36,30 @@ let set_extension_handler ~print =
   initialized_extensions := true ;
   ()
 
-module Behavior_extensions = struct
-
-  let printer_tbl = Hashtbl.create 5
-
-  let register name printer =
-    Hashtbl.add printer_tbl name printer
+let ref_deprecated_extension_handler = ref (fun _ _ _ -> assert false)
+let set_deprecated_extension_handler ~handler =
+  ref_deprecated_extension_handler := handler
 
-  let default_pp printer fmt ext =
-    match ext with
-    | Ext_id i -> Format.pp_print_int fmt i
-    | Ext_terms terms ->
-      Pretty_utils.pp_list ~sep:",@ " printer#term fmt terms
-    | Ext_preds preds ->
-      Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt preds
+module Behavior_extensions = struct
+  let deprecated_register name =
+    !ref_deprecated_extension_handler name
 
   let pp (printer) fmt {ext_name; ext_kind} =
-    let pp =
-      try
-        Hashtbl.find printer_tbl ext_name
-      with Not_found -> default_pp
-    in
+    let pp = !ref_print_extension ext_name in
     Format.fprintf fmt "@[<hov 2>%s %a;@]" ext_name (pp printer) ext_kind
 
 end
-let register_behavior_extension = Behavior_extensions.register
+let register_behavior_extension name =
+  Behavior_extensions.deprecated_register name Ext_contract
 
-let register_code_annot_extension = Behavior_extensions.register
+let register_code_annot_extension name =
+  Behavior_extensions.deprecated_register name (Ext_code_annot Ext_here)
 
-let register_loop_annot_extension = Behavior_extensions.register
+let register_loop_annot_extension name =
+  Behavior_extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
 
-let register_global_extension = Behavior_extensions.register
+let register_global_extension name =
+  Behavior_extensions.deprecated_register name Ext_global
 
 (* Internal attributes. Won't be pretty-printed *)
 let reserved_attributes = ref []
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 04e4206ae37..3c7260976c2 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -41,31 +41,39 @@ val register_behavior_extension:
    Cil_types.acsl_extension_kind -> unit) -> unit
 (** Register a pretty-printer used for behavior extension.
     @plugin development guide
+    @deprecated Frama-C+dev
 *)
+[@@ deprecated "Use Acsl_extension.register_behavior instead"]
 
 val register_global_extension:
   string ->
   (Printer_api.extensible_printer_type -> Format.formatter ->
    Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for behavior extension.
+(** Register a pretty-printer used for global extension.
     @plugin development guide
+    @deprecated Frama-C+dev
 *)
+[@@ deprecated "Use Acsl_extension.register_global instead"]
 
 val register_code_annot_extension:
   string ->
   (Printer_api.extensible_printer_type -> Format.formatter ->
    Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for behavior extension.
+(** Register a pretty-printer used for code annotation extension.
     @plugin development guide
+    @deprecated Frama-C+dev
 *)
+[@@ deprecated "Use Acsl_extension.register_code_annot_<kind> instead"]
 
 val register_loop_annot_extension:
   string ->
   (Printer_api.extensible_printer_type -> Format.formatter ->
    Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for behavior extension.
+(** Register a pretty-printer used for loop annotation extension.
     @plugin development guide
+    @deprecated Frama-C+dev
 *)
+[@@ deprecated "Use Acsl_extension.register_loop_annot instead"]
 
 val state: Printer_api.state
 
@@ -84,6 +92,12 @@ val set_extension_handler:
     @since Frama-C+dev
 *)
 
+val set_deprecated_extension_handler:
+  handler:(string -> Cil_types.ext_category ->
+           (Printer_api.extensible_printer_type -> Format.formatter ->
+            Cil_types.acsl_extension_kind -> unit) ->
+           unit) -> unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index f59ee45bf2f..6bc74220684 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -117,3 +117,48 @@ let () =
     ~visit: Extensions.visit ;
   Cil_printer.set_extension_handler
     ~print: Extensions.print
+
+(* For Deprecation: *)
+
+let deprecated_replace name ext = Hashtbl.add Extensions.ext_tbl name ext
+
+let strong_cat = Hashtbl.create 5
+
+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)
+  | Some (found_cat, ext) ->
+    if strong && Hashtbl.mem strong_cat name then begin
+      if found_cat = cat then (cat, ext)
+      else
+        Kernel.fatal
+          "Registring %s for %s: this extension already exists for another \
+           category"
+          op_name name
+    end else if strong then begin
+      Hashtbl.add strong_cat name cat ;
+      (cat, ext)
+    end else
+      (found_cat, ext)
+
+let deprecated_register_typing name cat ext_status ext_typing =
+  let cat, ext = deprecated_find name cat "typing" in
+  let ext = { ext with ext_status ; ext_typing } in
+  deprecated_replace name (cat, ext)
+
+let deprecated_register_printing name cat ext_printing =
+  let cat, ext = deprecated_find ~strong:false name cat "printing" in
+  let ext = { ext with ext_printing } in
+  deprecated_replace name (cat, ext)
+
+let deprecated_register_visit name cat ext_visit =
+  let cat, ext = deprecated_find name cat "visit" in
+  let ext = { ext with ext_visit } in
+  deprecated_replace name (cat, ext)
+
+let () =
+  Logic_typing.set_deprecated_extension_handler deprecated_register_typing ;
+  Cil.set_deprecated_extension_handler deprecated_register_visit ;
+  Cil_printer.set_deprecated_extension_handler deprecated_register_printing
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d17d73e3598..dc24efcd495 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -755,8 +755,6 @@ let alphabetabeta _ x = x
 let alphabetafalse _ _ = false
 let alphatrue _ = true
 
-let visitor_tbl = Hashtbl.create 5
-
 let initialized_extensions = ref false
 let ref_visit_extension = ref (fun _ _ _ -> assert false)
 
@@ -766,7 +764,12 @@ let set_extension_handler ~visit =
   initialized_extensions := true ;
   ()
 
-let register_behavior_extension name ext = Hashtbl.add visitor_tbl name ext
+let ref_deprecated_extension_handler = ref (fun _ _ _ -> assert false)
+let set_deprecated_extension_handler ~handler =
+  ref_deprecated_extension_handler := handler
+
+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. *)
@@ -1898,10 +1901,7 @@ and childrenBehavior vis b =
   b
 
 and visitCilExtended vis orig =
-  let visit =
-    try Hashtbl.find visitor_tbl orig.ext_name
-    with Not_found -> (fun _ _ -> DoChildren)
-  in
+  let visit = !ref_visit_extension 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/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 61d314736e2..186a826e242 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1725,11 +1725,13 @@ end
 
     @since Sodium-20150201
     @modify Silicon-20161101
+    @deprecated Frama-C+dev
 *)
 val register_behavior_extension:
   string ->
   (cilVisitor -> acsl_extension_kind -> (acsl_extension_kind) visitAction)
   -> unit
+[@@ deprecated "Use Acsl_extension.register_behavior instead"]
 
 (**/**)
 class internal_genericCilVisitor:
@@ -2292,6 +2294,11 @@ val set_extension_handler:
     @since Frama-C+dev
 *)
 
+val set_deprecated_extension_handler:
+  handler:(string -> ext_category ->
+           (cilVisitor -> acsl_extension_kind -> acsl_extension_kind visitAction) ->
+           unit) -> unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 341ab6de574..0d7f4da3712 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -35,16 +35,8 @@ let set_extension_handler ~category ~is_extension =
   initialized_extensions := true ;
   ()
 
-
-let extensions = ref Datatype.String.Map.empty
-
-let is_extension s = Datatype.String.Map.mem s !extensions
-
-let extension_category s = Datatype.String.Map.find_opt s !extensions
-
-let register_extension s cat =
-  if not (is_extension s) then
-    extensions := Datatype.String.Map.add s cat !extensions
+let is_extension s = !ref_is_extension s
+let extension_category s = !ref_extension_category s
 
 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 2207c731d99..bc9cf490523 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -28,9 +28,6 @@ open Cil_types
 
 (** {2 registered ACSL extensions } *)
 
-(** register a given name as a clause name for extended category. *)
-val register_extension: string -> ext_category -> unit
-
 val is_extension: string -> bool
 
 val extension_category: string -> ext_category option
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 586294e2a0d..57775843694 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -535,33 +535,25 @@ let set_extension_handler ~is_extension ~typer =
   initialized_extensions := true ;
   ()
 
+let ref_deprecated_extension_handler = ref (fun _ _ _ _  -> assert false)
+let set_deprecated_extension_handler ~handler =
+  ref_deprecated_extension_handler := handler
+
 module Extensions = struct
-  let typer_tbl = Hashtbl.create 5
-  let find_typer name = Hashtbl.find typer_tbl name
-  let is_extension name = Hashtbl.mem typer_tbl name
-  let register name category status typer =
-    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
-      Logic_env.register_extension name category;
-      Hashtbl.add typer_tbl name (status,typer)
-    end
+  let is_extension name = !ref_is_extension name
+
+  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
 
   let typer name ~typing_context:typing_context ~loc p =
-    let status,typer =
-      try find_typer name
-      with Not_found ->
-        Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
-    in
+    let typer = !ref_type_extension name 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
+      typing_context.on_error (typer typing_context loc) has_error
     in
-    try
-      status, wrapper p
+    try wrapper p
     with
     | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
     | exn when not !normal_error ->
@@ -570,22 +562,22 @@ module Extensions = struct
 end
 
 let register_behavior_extension name f =
-  Extensions.register name Ext_contract f
+  Extensions.deprecated_register name Ext_contract f
 
 let register_global_extension name f =
-  Extensions.register name Ext_global f
+  Extensions.deprecated_register name Ext_global f
 
 let register_code_annot_extension name f =
-  Extensions.register name (Ext_code_annot Ext_here) f
+  Extensions.deprecated_register name (Ext_code_annot Ext_here) f
 
 let register_code_annot_next_stmt_extension name f =
-  Extensions.register name (Ext_code_annot Ext_next_stmt) f
+  Extensions.deprecated_register name (Ext_code_annot Ext_next_stmt) f
 
 let register_code_annot_next_loop_extension name f =
-  Extensions.register name (Ext_code_annot Ext_next_loop) f
+  Extensions.deprecated_register name (Ext_code_annot Ext_next_loop) f
 
 let register_code_annot_next_both_extension name f =
-  Extensions.register name (Ext_code_annot Ext_next_both) f
+  Extensions.deprecated_register name (Ext_code_annot Ext_next_both) f
 
 let rec arithmetic_conversion ty1 ty2 =
   match unroll_type ty1, unroll_type ty2 with
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 5d6bb73f7ff..f46cc6b0da8 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -177,22 +177,26 @@ type typing_context = {
     @since Carbon-20101201
     @modify Silicon-20161101 change type of the function
     @modify 19.0-Potassium add [status] argument
+    @deprecated Frama-C+dev
 *)
 val register_behavior_extension:
   string -> bool ->
   (typing_context:typing_context -> loc:location ->
    Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_behavior instead"]
 
 (** register an extension for global annotation.
 
     @plugin development guide
 
     @since 18.0-Argon
+    @deprecated Frama-C+dev
 *)
 val register_global_extension:
   string -> bool ->
   (typing_context:typing_context -> loc: location ->
    Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_global instead"]
 
 (** register an extension for code annotation to be evaluated at _current_
     program point.
@@ -200,11 +204,13 @@ val register_global_extension:
     @plugin development guide
 
     @since 18.0-Argon
+    @deprecated Frama-C+dev
 *)
 val register_code_annot_extension:
   string -> bool ->
   (typing_context: typing_context -> loc: location ->
    Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot instead"]
 
 (** register an extension for code annotation to be evaluated for the _next_
     statement.
@@ -212,22 +218,26 @@ val register_code_annot_extension:
     @plugin development guide
 
     @since 18.0-Argon
+    @deprecated Frama-C+dev
 *)
 val register_code_annot_next_stmt_extension:
   string -> bool ->
   (typing_context: typing_context -> loc: location ->
    Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot_next_stmt instead"]
 
 (** register an extension for loop annotation.
 
     @plugin development guide
 
     @since 18.0-Argon
+    @deprecated Frama-C+dev
 *)
 val register_code_annot_next_loop_extension:
   string -> bool ->
   (typing_context: typing_context -> loc: location ->
    Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot_next_loop instead"]
 
 
 (** register an extension both for code and loop annotations.
@@ -235,11 +245,13 @@ val register_code_annot_next_loop_extension:
     @plugin development guide
 
     @since 18.0-Argon
+    @deprecated Frama-C+dev
 *)
 val register_code_annot_next_both_extension:
   string -> bool ->
   (typing_context: typing_context -> loc: location ->
    Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot_next_both instead"]
 
 module Make
     (C :
@@ -383,6 +395,14 @@ val set_extension_handler:
     @since Frama-C+dev
 *)
 
+(**/**)
+val set_deprecated_extension_handler:
+  handler:(string -> ext_category -> bool ->
+           (typing_context -> location -> Logic_ptree.lexpr list ->
+            acsl_extension_kind) ->
+           unit) ->
+           unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
-- 
GitLab