From 8aa4852e1bd2ff18515515244ad285b2e77a81c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 24 Jan 2023 14:43:14 +0100
Subject: [PATCH] [Eva] Optimizes and moves function [accept_base] from
Callgraph to Eva.
[accept_base] is used by the Inout and From plugins, and its implementation
in callgraph is very slow on programs with many callsites.
---
src/plugins/callgraph/uses.ml | 32 ---------------------
src/plugins/callgraph/uses.mli | 11 --------
src/plugins/eva/Eva.mli | 8 ++++++
src/plugins/eva/gui/register_gui.ml | 2 +-
src/plugins/eva/legacy/logic_inout.ml | 37 +++++++++++++++++++++++++
src/plugins/eva/legacy/logic_inout.mli | 8 ++++++
src/plugins/eva/utils/eva_dynamic.ml | 5 ----
src/plugins/eva/utils/eva_dynamic.mli | 4 ---
src/plugins/eva/utils/private.ml | 1 +
src/plugins/eva/utils/private.mli | 1 +
src/plugins/from/functionwise.ml | 7 +++--
src/plugins/inout/inputs.ml | 4 +--
src/plugins/inout/operational_inputs.ml | 2 +-
src/plugins/inout/outputs.ml | 4 +--
14 files changed, 66 insertions(+), 60 deletions(-)
diff --git a/src/plugins/callgraph/uses.ml b/src/plugins/callgraph/uses.ml
index a4b6931b84b..2de6a275188 100644
--- a/src/plugins/callgraph/uses.ml
+++ b/src/plugins/callgraph/uses.ml
@@ -101,38 +101,6 @@ let iter_on_aux iter_dir f kf =
let iter_on_callers = iter_on_aux Cg.G.iter_pred
let iter_on_callees = iter_on_aux Cg.G.iter_succ
-let is_local_or_formal_of_caller v kf =
- try
- iter_on_callers
- (fun caller ->
- if Base.is_formal_or_local v (Kernel_function.get_definition caller)
- then raise Exit)
- kf;
- false
- with Exit ->
- true
-
-let accept_base ~with_formals ~with_locals kf v =
- let open Cil_types in
- Base.is_global v
- ||
- (match with_formals, with_locals, kf.fundec with
- | false, false, _ | false, _, Declaration _ -> false
- | true, false, Definition (fundec,_) -> Base.is_formal v fundec
- | false, true, Definition (fundec, _) -> Base.is_local v fundec
- | true, true, Definition (fundec, _) -> Base.is_formal_or_local v fundec
- | true , _, Declaration (_, vd, _, _) -> Base.is_formal_of_prototype v vd)
- || is_local_or_formal_of_caller v kf
-
-let _accept_base =
- Dynamic.register
- ~comment:"Returns [true] if the given base is a global, \
- or a formal or local of either [kf] or one of its callers"
- ~plugin:Options.name
- "accept_base"
- Datatype.(func2 Kernel_function.ty Base.ty bool)
- (fun kf b -> accept_base ~with_formals:true ~with_locals:true kf b)
-
let nb_calls () =
let g = Cg.get () in
(* [g] contains bidirectional edges (from caller to callee and
diff --git a/src/plugins/callgraph/uses.mli b/src/plugins/callgraph/uses.mli
index 4e9df9a0ad0..286d3a6c8eb 100644
--- a/src/plugins/callgraph/uses.mli
+++ b/src/plugins/callgraph/uses.mli
@@ -38,17 +38,6 @@ val iter_on_callees : (Kernel_function.t -> unit) -> Kernel_function.t -> unit
(** Iterate over all the callees of a given function in a (reverse) depth-first
way. Do nothing if the function is not in the callgraph. *)
-val accept_base :
- with_formals:bool ->
- with_locals:bool ->
- Kernel_function.t ->
- Base.t ->
- bool
-(** [accept_base formals locals kf b] returns [true] if and only if [b] is
- - a global
- - a formal or local of one of the callers of [kf]
- - a formal or local of [kf] and the corresponding argument is [true]. *)
-
val nb_calls: unit -> int
(** @return the number of function calls in the whole callgraph. It is not
(necessarily) equal to the number of graph edges (depending on the
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index d36e2198c59..62d89a87c61 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -708,6 +708,14 @@ module Logic_inout: sig
val verify_assigns:
Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+
+ (** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
+ - a global
+ - a formal or local of one of the callers of [kf]
+ - a formal or local of [kf] and the corresponding argument is [true]. *)
+ val accept_base:
+ formals:bool -> locals:bool -> Kernel_function.t -> Base.t -> bool
+
end
module Eva_results: sig
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index e91019d1c69..c1fe3c7bf7b 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -228,7 +228,7 @@ let gui_compute_values (main_ui:main_ui) =
let cleaned_outputs kf s =
let outs = Db.Outputs.kinstr (Kstmt s) in
- let accept = Eva_dynamic.Callgraph.accept_base kf in
+ let accept = Logic_inout.accept_base ~formals:true ~locals:true kf in
let filter = Locations.Zone.filter_base accept in
Option.map filter outs
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 34ed60bad55..14a5f09846d 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -290,3 +290,40 @@ let verify_assigns kf ~pre froms =
in
let ab = Active_behaviors.create eval_predicate funspec in
check_fct_assigns kf ab ~pre_state:pre froms
+
+(* -------------------------------------------------------------------------- *)
+(* --- Utilitary function for Inout and From plugins --- *)
+(* -------------------------------------------------------------------------- *)
+
+let compute_all_callers kf =
+ let rec add_callers kf acc =
+ List.fold_left add_kf acc (Function_calls.callers kf)
+ and add_kf acc kf =
+ if Kernel_function.Hptset.mem kf acc
+ then acc
+ else add_callers kf (Kernel_function.Hptset.add kf acc)
+ in
+ add_callers kf (Kernel_function.Hptset.empty)
+
+let is_local_or_formal_of_caller callers base =
+ match Kernel_function.find_defining_kf (Base.to_varinfo base) with
+ | Some kf -> Kernel_function.Hptset.mem kf callers
+ | None | exception Base.Not_a_C_variable -> false
+
+let is_formal kf base =
+ match kf.fundec with
+ | Definition (fundec, _) -> Base.is_formal base fundec
+ | Declaration (_, vi, _, _) -> Base.is_formal_of_prototype base vi
+
+let is_local kf base =
+ match kf.fundec with
+ | Definition (fundec, _) -> Base.is_local base fundec
+ | Declaration _ -> false
+
+let accept_base ~formals ~locals kf =
+ let all_callers = compute_all_callers kf in
+ fun base ->
+ Base.is_global base
+ || (formals && is_formal kf base)
+ || (locals && is_local kf base)
+ || is_local_or_formal_of_caller all_callers base
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index d79e25f77ba..fa75127301f 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -73,4 +73,12 @@ val assigns_tlval_to_zones:
val verify_assigns:
Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+
+(** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
+ - a global
+ - a formal or local of one of the callers of [kf]
+ - a formal or local of [kf] and the corresponding argument is [true]. *)
+val accept_base:
+ formals:bool -> locals:bool -> Kernel_function.t -> Base.t -> bool
+
[@@@ api_end]
diff --git a/src/plugins/eva/utils/eva_dynamic.ml b/src/plugins/eva/utils/eva_dynamic.ml
index 597122b7252..f3089bf4123 100644
--- a/src/plugins/eva/utils/eva_dynamic.ml
+++ b/src/plugins/eva/utils/eva_dynamic.ml
@@ -35,11 +35,6 @@ module Callgraph = struct
else
let typ = Datatype.(func (func Kernel_function.ty unit) unit) in
get ~plugin "iter_in_rev_order" typ ~fallback f
-
- let accept_base kf v =
- let fallback _ _ = true in
- let typ = Datatype.(func2 Kernel_function.ty Base.ty bool) in
- get ~plugin "accept_base" typ ~fallback kf v
end
module Scope = struct
diff --git a/src/plugins/eva/utils/eva_dynamic.mli b/src/plugins/eva/utils/eva_dynamic.mli
index 89b11aea252..0541972c987 100644
--- a/src/plugins/eva/utils/eva_dynamic.mli
+++ b/src/plugins/eva/utils/eva_dynamic.mli
@@ -27,10 +27,6 @@ module Callgraph: sig
callees to callers. If callgraph is missing or if the number of callsites
is too big, the order is unspecified. *)
val iter_in_rev_order: (Kernel_function.t -> unit) -> unit
-
- (** Returns [true] if [base] is a global, or a formal or local of either [kf]
- or one of its callers. If callgraph is missing, always returns true. *)
- val accept_base: Kernel_function.t -> Base.t -> bool
end
module Scope: sig
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index c5a16ae1195..5040c5d25c2 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -36,6 +36,7 @@ module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
module Function_calls = Function_calls
+module Logic_inout = Logic_inout
module Main_locations = Main_locations
module Main_values = Main_values
module Parameters = Parameters
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index d4c64ac5ad0..23024a48781 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -40,6 +40,7 @@ module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
module Function_calls = Function_calls
+module Logic_inout = Logic_inout
module Main_locations = Main_locations
module Main_values = Main_values
module Parameters = Parameters
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index ee80d0cc402..2f729743dbb 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -50,14 +50,17 @@ module To_Use = struct
let get_from_call kf _ = memo kf
let keep_base kf = (* Eta-expansion required *)
- Callgraph.Uses.accept_base ~with_formals:false ~with_locals:false kf
+ Eva.Logic_inout.accept_base ~formals:false ~locals:false kf
let cleanup kf froms =
if Function_Froms.Memory.is_bottom froms.Function_Froms.deps_table
then froms
else
+ let accept_base =
+ Eva.Logic_inout.accept_base ~formals:true ~locals:false kf
+ in
let f b intervs =
- if Callgraph.Uses.accept_base ~with_formals:true ~with_locals:false kf b
+ if accept_base b
then Zone.inject b intervs
else Zone.bottom
in
diff --git a/src/plugins/inout/inputs.ml b/src/plugins/inout/inputs.ml
index c9787b60363..247f1b4f0fd 100644
--- a/src/plugins/inout/inputs.ml
+++ b/src/plugins/inout/inputs.ml
@@ -155,12 +155,12 @@ let get_external =
Externals.memo
(fun kf ->
Zone.filter_base
- (Callgraph.Uses.accept_base ~with_formals:false ~with_locals:false kf)
+ (Eva.Logic_inout.accept_base ~formals:false ~locals:false kf)
(get_internal kf))
let get_with_formals kf =
Zone.filter_base
- (Callgraph.Uses.accept_base ~with_formals:true ~with_locals:false kf)
+ (Eva.Logic_inout.accept_base ~formals:true ~locals:false kf)
(get_internal kf)
let compute_external kf = ignore (get_external kf)
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index b7ce487c065..a2fc93daf04 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -94,7 +94,7 @@ let join_and_is_included smaller larger =
let externalize_zone ~with_formals kf =
Zone.filter_base
- (Callgraph.Uses.accept_base ~with_formals ~with_locals:false kf)
+ (Eva.Logic_inout.accept_base ~formals:with_formals ~locals:false kf)
(* This code evaluates an assigns, computing in particular a sound approximation
of sure outputs. For an assigns [locs_out \from locs_from], the process
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 4d06b9f1a51..6cbb7eb73b0 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -117,7 +117,7 @@ class virtual do_it_ = object(self)
method clean_kf_result kf r =
Zone.filter_base
- (Callgraph.Uses.accept_base ~with_formals:true ~with_locals:true kf)
+ (Eva.Logic_inout.accept_base ~formals:true ~locals:true kf)
r
method compute_funspec kf =
@@ -141,7 +141,7 @@ let get_internal = Analysis.kernel_function
let externalize kf x =
Zone.filter_base
- (Callgraph.Uses.accept_base ~with_formals:false ~with_locals:false kf)
+ (Eva.Logic_inout.accept_base ~formals:false ~locals:false kf)
x
module Externals =
--
GitLab