From b521f5d723b6f46043b0ddbb95dbc36d0952ab70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 20 Jan 2022 14:02:09 +0100
Subject: [PATCH] [kernel] Visitor: adds a function to visit all function
definitions of a file.
For visitors that only need function C bodies, replaces uses of
[visitFramacFileSameGlobals], which visits all globals of a file, by
[visitFramacFileFunctions], which visits only function definitions.
Also optimizes these visitors by skipping the visit of some nodes,
especially the visit of functions specifications and code annotations.
---
src/kernel_internals/typing/allocates.ml | 10 +++++++---
src/kernel_internals/typing/asm_contracts.ml | 8 +++++++-
src/kernel_internals/typing/unroll_loops.ml | 9 ++++++++-
src/kernel_services/analysis/exn_flow.ml | 15 +++++++++++++--
src/kernel_services/ast_transformations/inline.ml | 7 ++++++-
src/kernel_services/visitors/visitor.ml | 7 +++++++
src/kernel_services/visitors/visitor.mli | 7 +++++++
src/plugins/value/legacy/eval_annots.ml | 9 +++++++--
src/plugins/value/partitioning/split_return.ml | 6 +++++-
9 files changed, 67 insertions(+), 11 deletions(-)
diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index dec3566fe21..92f755e9cbb 100644
--- a/src/kernel_internals/typing/allocates.ml
+++ b/src/kernel_internals/typing/allocates.ml
@@ -57,11 +57,15 @@ class vis_add_loop_allocates =
);
Cil.DoChildren
- method! vinst _ = Cil.SkipChildren
-
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let add_allocates_nothing () =
Globals.Functions.iter add_allocates_nothing_funspec;
let vis = new vis_add_loop_allocates in
- Visitor.visitFramacFileSameGlobals vis (Ast.get ())
+ Visitor.visitFramacFileFunctions vis (Ast.get ())
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 55c5b0fb1f4..c2c8e143093 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -221,11 +221,17 @@ class visit_assembly =
~dkey:Kernel.dkey_asm_contracts "Ignoring basic assembly instruction";
Cil.SkipChildren
| _ -> Cil.SkipChildren
+
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let transform file =
if Kernel.AsmContractsGenerate.get() then
- Visitor.visitFramacFileSameGlobals (new visit_assembly) file
+ Visitor.visitFramacFileFunctions (new visit_assembly) file
let () =
File.add_code_transformation_after_cleanup
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 89c96fbb3a5..1242f533128 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -709,6 +709,13 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
ChangeDoChildrenPost (s, fgh)
| _ -> DoChildren
+
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
(* Performs unrolling transformation without using -ulevel option.
@@ -723,7 +730,7 @@ let apply_transformation ?(force=true) nb file =
in
let visitor = new do_it global_find_init (force, nb) in
Kernel.debug ~dkey "Using -ulevel %d option and UNROLL loop pragmas@." nb;
- visitFramacFileSameGlobals (visitor:>Visitor.frama_c_visitor) file;
+ visitFramacFileFunctions (visitor:>Visitor.frama_c_visitor) file;
if !ast_has_changed then Ast.mark_as_changed ()
else begin
Kernel.debug ~dkey
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index f6dd804a26c..ad3a19d463a 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -65,11 +65,17 @@ class all_exn =
all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
SkipChildren
| _ -> DoChildren
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let compute_all_exn () =
let vis = new all_exn in
- Visitor.visitFramacFileSameGlobals (vis:>Visitor.frama_c_visitor) (Ast.get());
+ Visitor.visitFramacFileFunctions (vis:>Visitor.frama_c_visitor) (Ast.get());
vis#get_exn
let all_exn () = All_exn.memo compute_all_exn
@@ -259,6 +265,11 @@ class exn_visit =
in
DoChildrenPost after_visit
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let compute_kf kf =
@@ -857,7 +868,7 @@ let prepare_file f =
let remove_exn f =
if Kernel.RemoveExn.get() then begin
- Visitor.visitFramacFileSameGlobals (new exn_visit) f;
+ Visitor.visitFramacFileFunctions (new exn_visit) f;
let vis = new erase_exn in
Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) f;
let funs = vis#modified_funcs in
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index b8cddec6cc6..8e3d83b946f 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -342,6 +342,11 @@ let inliner functions_to_inline = object (self)
let kf = Globals.Functions.get f.svar in
already_visited <- Cil_datatype.Kf.Set.add kf functions_to_inline; f)
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
let remove_local_statics = object
@@ -379,7 +384,7 @@ end
let inline_calls ast =
if not (InlineCalls.is_empty ()) then begin
let functions = InlineCalls.get() in
- Visitor.visitFramacFileSameGlobals (inliner functions) ast;
+ Visitor.visitFramacFileFunctions (inliner functions) ast;
Cil_datatype.Kf.Set.iter
(fun kf -> ignore (Visitor.visitFramacKf remove_local_statics kf))
functions;
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 1121a89660d..fdb824e963c 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -871,6 +871,13 @@ let visitFramacFunction vis f =
Option.iter vis#set_current_kf old_current_kf;
vis#fill_global_tables; f'
+let visitFramacFileFunctions vis file =
+ let process_one_global = function
+ | GFun (fundec, _) -> ignore (visitFramacFunction vis fundec)
+ | _ -> ()
+ in
+ Cil.iterGlobals file process_one_global
+
let visitFramacKf vis kf =
let glob = Ast.def_or_last_decl (Kernel_function.get_vi kf) in
ignore (visitFramacGlobal vis glob);
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 8b0a5da0742..87ae254349d 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/src/kernel_services/visitors/visitor.mli
@@ -115,6 +115,13 @@ val visitFramacFile: frama_c_visitor -> file -> unit
@plugin development guide *)
val visitFramacFileSameGlobals: frama_c_visitor -> file -> unit
+(** Visit all function definitions of a file. Use this function instead of
+ {!Visitor.visitFramacFile} or {!Visitor.visitFramacFileSameGlobals} if your
+ visitor only needs function bodies to avoid visiting other globals,
+ including libc functions and their specifications.
+ @since Frama-c+dev *)
+val visitFramacFileFunctions: frama_c_visitor -> file -> unit
+
(** Visit a global.
{b Warning} Do not call this function during another visit using the
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 910bb4dfce7..6f8a65f402a 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -96,11 +96,16 @@ let mark_unreachable () =
end;
Cil.DoChildren
- method! vinst _ = Cil.SkipChildren
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
in
Annotations.iter_all_code_annot do_code_annot;
- Visitor.visitFramacFile unreach (Ast.get ())
+ Visitor.visitFramacFileFunctions unreach (Ast.get ())
let c_labels kf cs =
if !Db.Value.use_spec_instead_of_definition kf then
diff --git a/src/plugins/value/partitioning/split_return.ml b/src/plugins/value/partitioning/split_return.ml
index fe4ee995d77..0ecb7b4edfc 100644
--- a/src/plugins/value/partitioning/split_return.ml
+++ b/src/plugins/value/partitioning/split_return.ml
@@ -208,6 +208,10 @@ module ReturnUsage = struct
method result () =
summarize_by_lv usage
+
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
end
(* For functions returning pointers, add a split on NULL/non-NULL *)
@@ -223,7 +227,7 @@ module ReturnUsage = struct
let compute file =
let vis = new visitorVarUsage in
- Visitor.visitFramacFileSameGlobals (vis:> Visitor.frama_c_visitor) file;
+ Visitor.visitFramacFileFunctions (vis:> Visitor.frama_c_visitor) file;
let split_compared = vis#result () in
let split_null_pointers = add_null_pointers_split split_compared in
split_null_pointers
--
GitLab