From ee72aad77b419fe6e80d6f4fa5f2228579debc26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 25 Apr 2023 15:46:29 +0200
Subject: [PATCH] [kernel] update hook on annotations
This reverts commit 0bd1d1f0c17fb811469aa8b57fb4bd8f4acbc83b.
---
src/kernel_services/ast_data/annotations.ml | 192 +++++++++++++-----
.../plugin_entry_points/emitter.ml | 32 ++-
.../plugin_entry_points/emitter.mli | 12 --
3 files changed, 150 insertions(+), 86 deletions(-)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index e2b814dc187..4f049e0bf0d 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -67,6 +67,9 @@ let find_englobing_kf ?kf stmt =
(** {2 Internal State} *)
(**************************************************************************)
+module Changed = Hook.Make()
+let add_hook_on_change = Changed.extend
+
module Usable_emitter = struct
include Emitter.Usable_emitter
let local_clear _ h = Hashtbl.clear h
@@ -155,19 +158,6 @@ let () =
let kf = find_englobing_kf stmt in
List.iter (fun a -> clear_linked_to_annot kf stmt e a) !l)
-let add_hook_on_change f =
- begin
- let notify _ _ _ = f () in
- Globals.add_hook_on_update notify ;
- Globals.add_hook_on_remove notify ;
- Model_fields.add_hook_on_update notify ;
- Model_fields.add_hook_on_remove notify ;
- Funspecs.add_hook_on_update notify ;
- Funspecs.add_hook_on_remove notify ;
- Code_annots.add_hook_on_update notify ;
- Code_annots.add_hook_on_remove notify ;
- end
-
(**************************************************************************)
(** {2 Getting annotations} *)
(**************************************************************************)
@@ -448,7 +438,8 @@ let pre_register_funspec ?tbl ?(emitter=Emitter.end_user) ?(force=false) kf =
tbl;
*)
List.iter Property_status.register
- (Property.ip_of_spec kf Kglobal ~active:[] spec)
+ (Property.ip_of_spec kf Kglobal ~active:[] spec);
+ Changed.apply();
end
let register_funspec ?emitter ?force kf =
@@ -780,7 +771,7 @@ let remove_code_annot_internal e ?(remove_statuses=true) ?kf stmt ca =
(**************************************************************************)
(* If this function gets exported, please turn e into an Emitter.t *)
-let remove_model_field (e:Usable_emitter.t) m =
+let do_remove_model_field (e:Usable_emitter.t) m =
try
let ty = m.mi_base_type in
let h = Model_fields.find ty in
@@ -802,7 +793,7 @@ let remove_global e a =
if Emitter.Usable_emitter.equal e e' then begin
Globals.remove a;
(match a with
- | Dmodel_annot (m,_) -> remove_model_field e m
+ | Dmodel_annot (m,_) -> do_remove_model_field e m
| _ -> ());
let file = Ast.get () in
file.globals <-
@@ -810,12 +801,14 @@ let remove_global e a =
(fun a' ->
not (Global.equal (GAnnot(a, Global_annotation.loc a)) a'))
file.globals;
- Globals.apply_hooks_on_remove e a ()
+ Globals.apply_hooks_on_remove e a ();
+ Changed.apply();
end)
h;
with Not_found ->
()
+(* internal use only *)
let remove_in_funspec e kf set_spec =
try
let tbl = Funspecs.find kf in
@@ -828,7 +821,8 @@ let remove_in_funspec e kf set_spec =
Format.printf "For emitter %a: %a@."
Emitter.Usable_emitter.pretty e
Cil_printer.pp_funspec spec) tbl; *)
- set_spec spec tbl
+ set_spec spec tbl;
+ Changed.apply()
with Not_found -> ()
with Not_found ->
assert false
@@ -858,7 +852,8 @@ let remove_behavior ?(force=false) e kf bhv =
in
remove_in_funspec e kf set_spec
-let remove_decreases e kf =
+(* internal use only *)
+let do_remove_decreases e kf =
let set_spec spec _tbl =
match spec.spec_variant with
| None -> ()
@@ -868,7 +863,12 @@ let remove_decreases e kf =
in
remove_in_funspec e kf set_spec
-let remove_terminates e kf =
+let remove_decreases e kf =
+ do_remove_decreases e kf;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_terminates e kf =
let set_spec spec _tbl =
match spec.spec_terminates with
| None -> ()
@@ -878,21 +878,36 @@ let remove_terminates e kf =
in
remove_in_funspec e kf set_spec
-let remove_complete e kf l =
+let remove_terminates e kf =
+ do_remove_terminates e kf;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_complete e kf l =
let set_spec spec _tbl =
spec.spec_complete_behaviors <- filterq l spec.spec_complete_behaviors
in
remove_in_funspec e kf set_spec;
Property_status.remove (Property.ip_of_complete kf Kglobal ~active:[] l)
-let remove_disjoint e kf l =
+let remove_complete e kf l =
+ do_remove_complete e kf l;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_disjoint e kf l =
let set_spec spec _tbl =
spec.spec_disjoint_behaviors <- filterq l spec.spec_disjoint_behaviors
in
remove_in_funspec e kf set_spec;
Property_status.remove (Property.ip_of_disjoint kf Kglobal ~active:[] l)
-let remove_requires e kf p =
+let remove_disjoint e kf l =
+ do_remove_disjoint e kf l;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_requires e kf p =
let set_spec spec _tbl =
List.iter
(fun b ->
@@ -904,7 +919,12 @@ let remove_requires e kf p =
in
remove_in_funspec e kf set_spec
-let remove_assumes e kf p =
+let remove_requires e kf p =
+ do_remove_requires e kf p;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_assumes e kf p =
let set_spec spec _tbl =
List.iter
(fun b ->
@@ -916,7 +936,12 @@ let remove_assumes e kf p =
in
remove_in_funspec e kf set_spec
-let remove_ensures e kf p =
+let remove_assumes e kf p =
+ do_remove_assumes e kf p;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_ensures e kf p =
let set_spec spec _tbl =
List.iter
(fun b ->
@@ -928,7 +953,12 @@ let remove_ensures e kf p =
in
remove_in_funspec e kf set_spec
-let remove_allocates e kf p =
+let remove_ensures e kf p =
+ do_remove_ensures e kf p;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_allocates e kf p =
let set_spec spec _tbl =
List.iter
(fun b ->
@@ -942,7 +972,12 @@ let remove_allocates e kf p =
in
remove_in_funspec e kf set_spec
-let remove_extended e kf ext =
+let remove_allocates e kf p =
+ do_remove_allocates e kf p;
+ Changed.apply()
+
+(* internal use only *)
+let do_remove_extended e kf ext =
let set_spec spec _tbl =
List.iter
(fun b ->
@@ -953,8 +988,12 @@ let remove_extended e kf ext =
in
remove_in_funspec e kf set_spec
+let remove_extended e kf ext =
+ do_remove_extended e kf ext;
+ Changed.apply()
-let remove_assigns e kf p =
+(* internal use only *)
+let do_remove_assigns e kf p =
let set_spec spec _tbl =
List.iter
(fun b ->
@@ -976,12 +1015,17 @@ let remove_assigns e kf p =
in
remove_in_funspec e kf set_spec
+let remove_assigns e kf p =
+ do_remove_assigns e kf p;
+ Changed.apply()
+
let remove_behavior_components e kf b =
- List.iter (remove_requires e kf) b.b_requires;
- List.iter (remove_assumes e kf) b.b_assumes;
- List.iter (remove_ensures e kf) b.b_post_cond;
- remove_assigns e kf b.b_assigns;
- remove_allocates e kf b.b_allocation
+ List.iter (do_remove_requires e kf) b.b_requires;
+ List.iter (do_remove_assumes e kf) b.b_assumes;
+ List.iter (do_remove_ensures e kf) b.b_post_cond;
+ do_remove_assigns e kf b.b_assigns;
+ do_remove_allocates e kf b.b_allocation;
+ Changed.apply()
(**************************************************************************)
(** {2 Adding annotations} *)
@@ -1093,7 +1137,8 @@ let mk_spec bhv variant terminates complete disjoint =
spec_complete_behaviors = complete;
spec_disjoint_behaviors = disjoint; }
-let add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
+(* internal use only *)
+let do_add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
let full_spec = get_spec_all kf ?stmt ?active () in
let emit_spec = get_spec_e e kf ?stmt ?active () in
let existing_behaviors = emit_spec.spec_behavior in
@@ -1160,10 +1205,15 @@ let add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
bhvs
end
+let add_behaviors ?register_children e kf ?stmt ?active bhvs =
+ do_add_behaviors ?register_children e kf ?stmt ?active bhvs;
+ Changed.apply()
+
exception AlreadySpecified of string list
-let add_decreases ?(force=false) e kf v =
- if force then remove_decreases e kf ;
+(* internal use only *)
+let do_add_decreases ?(force=false) e kf v =
+ if force then do_remove_decreases e kf ;
let full_spec = get_spec_all kf () in
let emit_spec = get_spec_e e kf () in
(match full_spec.spec_variant with
@@ -1172,8 +1222,14 @@ let add_decreases ?(force=false) e kf v =
| _ -> emit_spec.spec_variant <- Some v);
Property_status.register (Property.ip_of_decreases kf Kglobal v)
-let add_terminates ?(force=false) e kf ?stmt ?active t =
- if force then remove_terminates e kf ;
+(* internal use only *)
+let add_decreases ?force e kf v =
+ do_add_decreases ?force e kf v;
+ Changed.apply()
+
+(* internal use only *)
+let do_add_terminates ?(force=false) e kf ?stmt ?active t =
+ if force then do_remove_terminates e kf ;
let full_spec = get_spec_all kf ?stmt ?active () in
let emit_spec = get_spec_e e kf ?stmt ?active () in
(match full_spec.spec_terminates with
@@ -1182,6 +1238,10 @@ let add_terminates ?(force=false) e kf ?stmt ?active t =
| _ -> emit_spec.spec_terminates <- Some t);
Property_status.register (Property.ip_of_terminates kf (kinstr stmt) t)
+let add_terminates ?force e kf ?stmt ?active t =
+ do_add_terminates ?force e kf ?stmt ?active t;
+ Changed.apply()
+
let check_bhv_name spec name =
if name = Cil.default_behavior_name then begin
Kernel.fatal
@@ -1195,7 +1255,8 @@ let check_bhv_name spec name =
name
end
-let add_complete e kf ?stmt ?active l =
+(* internal use only *)
+let do_add_complete e kf ?stmt ?active l =
let full_spec = get_spec_all kf ?stmt ?active () in
let emit_spec = get_spec_e e kf ?stmt ?active () in
if List.mem l full_spec.spec_complete_behaviors then
@@ -1211,7 +1272,12 @@ let add_complete e kf ?stmt ?active l =
(Property.ip_of_complete kf (kinstr stmt) ~active l)
end
-let add_disjoint e kf ?stmt ?active l =
+let add_complete e kf ?stmt ?active l =
+ do_add_complete e kf ?stmt ?active l;
+ Changed.apply()
+
+(* internal use only *)
+let do_add_disjoint e kf ?stmt ?active l =
let full_spec = get_spec_all kf ?stmt ?active () in
let emit_spec = get_spec_e e kf ?stmt ?active () in
if List.mem l full_spec.spec_disjoint_behaviors then
@@ -1226,6 +1292,10 @@ let add_disjoint e kf ?stmt ?active l =
Property_status.register (Property.ip_of_disjoint kf (kinstr stmt) ~active l)
end
+let add_disjoint e kf ?stmt ?active l =
+ do_add_disjoint e kf ?stmt ?active l;
+ Changed.apply()
+
let add_spec ?register_children ?(force=false) e kf ?stmt ?active spec =
let full_spec = get_spec_all kf ?stmt ?active () in
let conflicts =
@@ -1241,20 +1311,22 @@ let add_spec ?register_children ?(force=false) e kf ?stmt ?active spec =
| _ -> [])
in
if not force && conflicts <> [] then raise (AlreadySpecified conflicts) ;
- add_behaviors ?register_children e kf ?stmt ?active spec.spec_behavior;
+ do_add_behaviors ?register_children e kf ?stmt ?active spec.spec_behavior;
Option.iter
- (fun variant -> add_decreases ~force e kf variant)
+ (fun variant -> do_add_decreases ~force e kf variant)
spec.spec_variant;
Option.iter
- (fun terminates -> add_terminates ~force e kf ?stmt ?active terminates)
+ (fun terminates -> do_add_terminates ~force e kf ?stmt ?active terminates)
spec.spec_terminates;
List.iter
- (fun complete -> add_complete e kf ?stmt ?active complete)
+ (fun complete -> do_add_complete e kf ?stmt ?active complete)
spec.spec_complete_behaviors;
List.iter
- (fun disjoint -> add_disjoint e kf ?stmt ?active disjoint)
- spec.spec_disjoint_behaviors
+ (fun disjoint -> do_add_disjoint e kf ?stmt ?active disjoint)
+ spec.spec_disjoint_behaviors;
+ Changed.apply()
+(* internal use only *)
let extend_behavior
e kf ?stmt ?active ?(behavior=Cil.default_behavior_name) set_bhv =
(* Kernel.feedback "Function %a, behavior %s" Kf.pretty kf bhv_name;*)
@@ -1276,7 +1348,8 @@ let extend_behavior
Property_status.remove ip;
set_bhv b b';
let ip = Property.ip_of_behavior kf (kinstr stmt) ~active b in
- Property_status.register ip
+ Property_status.register ip;
+ Changed.apply()
let add_requires e kf ?stmt ?active ?behavior l =
let set_bhv _ bhv =
@@ -1410,7 +1483,8 @@ let add_extended e kf ?stmt ?active ?behavior ext =
(** {3 Adding code annotations} *)
-let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
+(* internal use only *)
+let do_add_code_annot ~keep_empty emitter ?kf stmt ca =
(* Kernel.feedback "%a: adding code annot %a with stmt %a (%d)"
Project.pretty (Project.current ())
Code_annotation.pretty ca
@@ -1455,18 +1529,18 @@ let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
| [ { annot_content = AStmtSpec _ } ] ->
let register_children = true in
let active = bhvs in
- add_behaviors
+ do_add_behaviors
~register_children emitter kf ~stmt ~active spec.spec_behavior;
if spec.spec_variant <> None then
Kernel.fatal
"statement contract cannot have a decrease clause";
Option.iter
- (add_terminates emitter kf ~stmt ~active) spec.spec_terminates;
+ (do_add_terminates emitter kf ~stmt ~active) spec.spec_terminates;
List.iter
- (add_complete emitter kf ~stmt ~active)
+ (do_add_complete emitter kf ~stmt ~active)
spec.spec_complete_behaviors;
List.iter
- (add_disjoint emitter kf ~stmt ~active)
+ (do_add_disjoint emitter kf ~stmt ~active)
spec.spec_disjoint_behaviors;
(* By construction, we have exactly one contract
corresponding to our criterion and emitter. *)
@@ -1570,6 +1644,10 @@ let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
| APragma _ | AExtended _ ->
fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
+ do_add_code_annot ~keep_empty emitter ?kf stmt ca;
+ Changed.apply()
+
let add_assert e ?kf stmt a =
let a = Logic_const.toplevel_predicate ~kind:Assert a in
let a = Logic_const.new_code_annotation (AAssert ([],a)) in
@@ -1667,7 +1745,8 @@ let add_model_field e m =
try Emitter.Usable_emitter.Hashtbl.find h e
with Not_found -> []
in
- Emitter.Usable_emitter.Hashtbl.replace h e (m::l)
+ Emitter.Usable_emitter.Hashtbl.replace h e (m::l);
+ Changed.apply()
let unsafe_add_global e a =
(* Kernel.feedback "adding global %a in project %a"
@@ -1682,7 +1761,8 @@ let unsafe_add_global e a =
let add_global e a =
unsafe_add_global e a;
- if Ast.is_computed() then insert_global_in_ast a
+ if Ast.is_computed() then insert_global_in_ast a;
+ Changed.apply()
(**************************************************************************)
(** {2 Other useful functions} *)
@@ -1779,7 +1859,9 @@ let code_annot_of_kf kf = match kf.fundec with
(* don't export the possibility to removing an annotation without associated
statuses. This is purely internal. *)
-let remove_code_annot e ?kf stmt ca = remove_code_annot_internal e ?kf stmt ca
+let remove_code_annot e ?kf stmt ca =
+ remove_code_annot_internal e ?kf stmt ca;
+ Changed.apply()
(*
Local Variables:
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index e4938ddf54d..6f7d97ede62 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -508,8 +508,9 @@ module Make_table
(Info: sig include State_builder.Info_with_size val kinds: kind list end) =
struct
- module Update_hooks = Hook.Build(struct type t = E.t * H.key * D.t end)
module Remove_hooks = Hook.Build(struct type t = E.t * H.key * D.t end)
+ let add_hook_on_remove f = Remove_hooks.extend (fun (e, k, d) -> f e k d)
+ let apply_hooks_on_remove e k d = Remove_hooks.apply (e, k, d)
(* this list is computed after defining [self] *)
let static_dependencies = ref []
@@ -565,7 +566,7 @@ struct
H.iter
(fun k h ->
if not (Remove_hooks.is_empty ()) then
- E.Hashtbl.iter (fun e x -> Remove_hooks.apply (e,k,x)) h;
+ E.Hashtbl.iter (fun e x -> apply_hooks_on_remove e k x) h;
E.local_clear k h)
tbl;
end else begin
@@ -595,7 +596,7 @@ struct
Info.name
Project.pretty (Project.current ());
E.Hashtbl.remove h e;
- Remove_hooks.apply (e,k,x);
+ apply_hooks_on_remove e k x
with Not_found ->
assert false)
!to_be_removed
@@ -610,17 +611,6 @@ struct
let dependencies = self :: dependencies
end)
- let add_hook_on_update f = Update_hooks.extend (fun (e, k, d) -> f e k d)
- let add_hook_on_remove f = Remove_hooks.extend (fun (e, k, d) -> f e k d)
- let apply_hooks_on_update e k d = Update_hooks.apply (e, k, d)
- let apply_hooks_on_remove e k d = Remove_hooks.apply (e, k, d)
-
- let notify f k =
- try
- let tbl = H.find !state k in
- E.Hashtbl.iter (fun e v -> f e k v) tbl;
- with Not_found -> ()
-
let add_kind k =
try
let l = Hashtbl.find kinds k in
@@ -641,6 +631,7 @@ struct
Cmdline.run_after_early_stage
(fun () -> static_dependencies := get_dependencies ())
+ let add key v = H.add !state key v
let find key = H.find !state key
let mem key = H.mem !state key
let iter f = H.iter f !state
@@ -648,12 +639,15 @@ struct
let to_seq () = H.to_seq !state
let iter_sorted ~cmp f = H.iter_sorted ~cmp f !state
let fold_sorted ~cmp f acc = H.fold_sorted ~cmp f !state acc
- let add key v =
- H.add !state key v ;
- if not (Update_hooks.is_empty ()) then notify apply_hooks_on_update key
let remove key =
- if not (Remove_hooks.is_empty ()) then notify apply_hooks_on_remove key ;
- H.remove !state key
+ if not (Remove_hooks.is_empty ()) then begin
+ try
+ let tbl = find key in
+ E.Hashtbl.iter (fun e v -> apply_hooks_on_remove e key v) tbl;
+ with Not_found ->
+ ()
+ end;
+ H.remove !state key;
end
diff --git a/src/kernel_services/plugin_entry_points/emitter.mli b/src/kernel_services/plugin_entry_points/emitter.mli
index dbcd4c4fc72..6215281eb6f 100644
--- a/src/kernel_services/plugin_entry_points/emitter.mli
+++ b/src/kernel_services/plugin_entry_points/emitter.mli
@@ -143,26 +143,14 @@ sig
cmp: (H.key -> H.key -> int) ->
(H.key -> internal_tbl -> 'a -> 'a) -> 'a -> 'a
val remove: H.key -> unit
-
- val add_hook_on_update: (E.t -> H.key -> D.t -> unit) -> unit
- (** Register a hook to be applied whenever a binding is added or updated
- into the table.
- @since Frama-C+dev *)
-
val add_hook_on_remove: (E.t -> H.key -> D.t -> unit) -> unit
(** Register a hook to be applied whenever a binding is removed from the table.
@since Fluorine-20130401 *)
- val apply_hooks_on_update: E.t -> H.key -> D.t -> unit
- (** This function must be called on each binding which is updated in the
- table without directly calling the function {!remove}.
- @since Frama-C+dev *)
-
val apply_hooks_on_remove: E.t -> H.key -> D.t -> unit
(** This function must be called on each binding which is removed from the
table without directly calling the function {!remove}.
@since Fluorine-20130401 *)
-
end
(*
--
GitLab