diff --git a/src/plugins/callgraph/uses.ml b/src/plugins/callgraph/uses.ml index a4b6931b84b78193287ac24a94b80af2b5134273..2de6a2751886f4c4f2cdf23b51d5cb88661604ae 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 4e9df9a0ad0171673666d76f2d055acd77e1b4c8..286d3a6c8ebd0b5770ba54c788f71b536c975468 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 d36e2198c59e4b45cdb8ac8bfa790fc28b6e49e9..62d89a87c610275e8d45a97f001808f2905417f9 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 e91019d1c695d319ea934b17b08a95eb0d16c49c..c1fe3c7bf7b15766aec935947116c87a4b5c7032 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 34ed60bad552a00cac80bb75364e007797e383dc..14a5f09846d059237db46b29dcbffeb3507f3e6b 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 d79e25f77ba717488ff74f6d3fa8ad728eabbee7..fa75127301f1b44ceef3d30fb4b81acb51d9da02 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 597122b725276862638615fe66df75b9ff0dfe14..f3089bf4123faebaf4963219dc208f81fab9cbb6 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 89b11aea252993081b0e5b8c2febf1c9ff54edf7..0541972c987e0935b2a0a9803a945050d0da63c3 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 c5a16ae11951cb4fec6bec7762131939b13ab083..5040c5d25c2dec2d04504f100c89e3b169ec3504 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 d4c64ac5ad0f0992d3ca624cae53a5b64421d9df..23024a487810ebb35caf04bde6429350b3537012 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 ee80d0cc402bcdc114ff443b86b4773b55e4a4c9..2f729743dbbedbc7446714fc1767cebb5c57f644 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 c9787b60363db83ed5243c704e1b9f6ff33bea81..247f1b4f0fd016ce494b6864dbe96a5209cf31b9 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 b7ce487c06545613a0caf8f58480220e18ce2d5c..a2fc93daf04e4f9c3346384d0535689ea523558d 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 4d06b9f1a51accebc2e6c80502bc94b9cd04b7ac..6cbb7eb73b01ca63c745072b8c6bd8854bbb9cfa 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 =