diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index 2ba86cfddf58dda836d6fce0e768bfa3d7fe71e9..f086f25ce7631762d38032984aa5536f0499b882 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -559,6 +559,9 @@ module From : sig val find : (kinstr -> Function_Froms.t) ref end end +[@@alert db_deprecated + "Db.From is deprecated and will be removed in a future version \ + of Frama-C. Please use the From module instead."] (* ************************************************************************* *) (** {2 Properties} *) diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml index 41a49e2e0a289dd89aa561ba2584d8fb2bc09b5c..b54cae7aaf9ded22a2a52fc9323b31ac7cdac38a 100644 --- a/src/plugins/from/callwise.ml +++ b/src/plugins/from/callwise.ml @@ -183,22 +183,17 @@ let () = Eva.Cvalue_callbacks.register_call_hook call_for_individual_froms; Eva.Cvalue_callbacks.register_call_results_hook record_for_individual_froms - -let force_compute_all_calldeps ()= - if Eva.Analysis.is_computed () then - Project.clear - ~selection:(State_selection.with_dependencies Eva.Analysis.self) - (); - Eva.Analysis.compute () - -(* Registration for call-wise from *) -let () = - Db.register_guarded_compute - Tbl.is_computed - Db.From.compute_all_calldeps - force_compute_all_calldeps; - Db.From.Callwise.iter := Tbl.iter; - Db.From.Callwise.find := Tbl.find +let iter = Tbl.iter +let find = Tbl.find + +let force_compute_all_calldeps () = + if not (Tbl.is_computed ()) then begin + if Eva.Analysis.is_computed () then + Project.clear + ~selection:(State_selection.with_dependencies Eva.Analysis.self) + (); + Eva.Analysis.compute () + end (* Local Variables: diff --git a/src/plugins/from/callwise.mli b/src/plugins/from/callwise.mli index 26d419c142dccc3e30658ed11ae9fcb3b920b60e..399ea357898301a06ae1116a9b94c3d6ca1f0015 100644 --- a/src/plugins/from/callwise.mli +++ b/src/plugins/from/callwise.mli @@ -22,7 +22,8 @@ (** Computation of callwise functional dependencies. The results are computed while the value analysis runs, and the results are usually much more - precise than the functionwise results. + precise than the functionwise results. *) - Nothing is exported here, the API can be found in the - Db.From.Callwise module *) +val force_compute_all_calldeps : unit -> unit +val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit +val find : Cil_types.kinstr -> Function_Froms.froms diff --git a/src/plugins/from/from.ml b/src/plugins/from/from.ml new file mode 100644 index 0000000000000000000000000000000000000000..f193d5f22e3c566bd2c1b341428e9c986a03a3b1 --- /dev/null +++ b/src/plugins/from/from.ml @@ -0,0 +1,41 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2022 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +let self = Functionwise.self +let compute = Functionwise.compute +let compute_all = Functionwise.compute_all +let is_computed = Functionwise.is_computed +let get = Functionwise.get +let pretty = Functionwise.pretty +let find_deps_no_transitivity = Functionwise.find_deps_no_transitivity +let find_deps_no_transitivity_state = + Functionwise.find_deps_no_transitivity_state + +let access zone mem = Function_Froms.Memory.find mem zone + +let display fmt = From_register.display (Some fmt) + +let force_compute_all_calldeps = Callwise.force_compute_all_calldeps +module Callwise = struct + let iter = Callwise.iter + let find = Callwise.find +end diff --git a/src/plugins/from/from.mli b/src/plugins/from/from.mli new file mode 100644 index 0000000000000000000000000000000000000000..63747ec6d10de9735e1f05d4aa298b729b3c6611 --- /dev/null +++ b/src/plugins/from/from.mli @@ -0,0 +1,40 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2022 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +open Cil_types + +val self : State.t +val is_computed : kernel_function -> bool +val compute : kernel_function -> unit +val compute_all : unit -> unit +val force_compute_all_calldeps : unit -> unit +val get : Cil_types.kernel_function -> Function_Froms.froms +val access : Locations.Zone.t -> Function_Froms.Memory.t -> Locations.Zone.t +val pretty : Format.formatter -> kernel_function -> unit +val display : Format.formatter -> unit +val find_deps_no_transitivity : stmt -> exp -> Locations.Zone.t +val find_deps_no_transitivity_state : Cvalue.Model.t -> exp -> Locations.Zone.t + +module Callwise : sig + val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit + val find : Cil_types.kinstr -> Function_Froms.froms +end diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml index 0805d3aef48555180c59ab2099575d29c51bb89d..14f127e123d57181ee9a74c02a66775eeeecc107 100644 --- a/src/plugins/from/from_compute.ml +++ b/src/plugins/from/from_compute.ml @@ -28,6 +28,15 @@ open Locations exception Call_did_not_take_place +module Record_From_Callbacks = + Hook.Build + (struct + type t = + (Kernel_function.t Stack.t) * + Function_Froms.Memory.t Stmt.Hashtbl.t * + (Kernel_function.t * Function_Froms.Memory.t) list Stmt.Hashtbl.t + end) + module type To_Use = sig val get_from_call : kernel_function -> stmt -> Function_Froms.t @@ -363,7 +372,7 @@ struct (List.length formal_args) (List.length args_froms)) end; - if not (Db.From.Record_From_Callbacks.is_empty ()) + if not (Record_From_Callbacks.is_empty ()) then states_with_formals := (kf, !state_with_formals) :: !states_with_formals; @@ -408,7 +417,7 @@ struct | Some s -> s); with Call_did_not_take_place -> state in - if not (Db.From.Record_From_Callbacks.is_empty ()) + if not (Record_From_Callbacks.is_empty ()) then Stmt.Hashtbl.replace callwise_states_with_formals @@ -582,7 +591,7 @@ struct in let module Compute = Dataflows.Simple_forward(Fenv)(Dataflow_arg) in let ret_id = Kernel_function.find_return kf in - if not (Db.From.Record_From_Callbacks.is_empty ()) + if not (Record_From_Callbacks.is_empty ()) then begin From_parameters.feedback "Now calling From callbacks"; let states = @@ -590,7 +599,7 @@ struct in Compute.iter_on_result (fun k record -> Stmt.Hashtbl.add states k record.deps_table); - Db.From.Record_From_Callbacks.apply + Record_From_Callbacks.apply (call_stack, states, Dataflow_arg.callwise_states_with_formals) end; let _poped = Stack.pop call_stack in diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml index 61a61f23ed3bab0bf24cd21deaad33401ef4743c..8928e0c4660647a3324364fdaca33254c3c1e2f0 100644 --- a/src/plugins/from/from_register.ml +++ b/src/plugins/from/from_register.ml @@ -23,7 +23,7 @@ open Cil_types let pretty_with_indirect fmt v = - let deps = !Db.From.get v in + let deps = Functionwise.get v in Function_Froms.pretty_with_type_indirect (Kernel_function.get_type v) fmt deps let display fmtopt = @@ -37,7 +37,7 @@ let display fmtopt = let pretty = if From_parameters.ShowIndirectDeps.get () then pretty_with_indirect - else !Db.From.pretty + else Functionwise.pretty in match fmtopt with | None -> @@ -63,7 +63,7 @@ module MapStmtCalls = Map.Make(SortCalls) let iter_callwise_calls_sorted f = let hkf = Kernel_function.Hashtbl.create 17 in let kglobal = ref None in - !Db.From.Callwise.iter + Callwise.iter (fun ki d -> match ki with | Kglobal -> kglobal := Some d @@ -148,28 +148,18 @@ let main () = if From_parameters.ForceDeps.get () then From_parameters.ForceDeps.output (fun () -> - !Db.From.compute_all (); + Functionwise.compute_all (); print_deps (); ); if From_parameters.ForceCallDeps.get () then From_parameters.ForceCallDeps.output (fun () -> - !Db.From.compute_all_calldeps (); + Callwise.force_compute_all_calldeps (); if not_quiet then print_calldeps (); ) let () = Db.Main.extend main -let access_from zone mem = Function_Froms.Memory.find mem zone - -(* Registration for most Db.From functions is done at the end of the - Functionwise and Callwise modules *) -let () = - Db.From.display := (fun fmt -> display (Some fmt)); - Db.From.access := access_from; - - - (* Local Variables: compile-command: "make -C ../../.." diff --git a/src/plugins/from/from_register.mli b/src/plugins/from/from_register.mli index cc955b0d1e20900dadc0eb4fe6c187ea3f9986ed..5e563bbed1499a2cbadc36ed47c60998a990cb0a 100644 --- a/src/plugins/from/from_register.mli +++ b/src/plugins/from/from_register.mli @@ -20,5 +20,6 @@ (* *) (**************************************************************************) -(** Registration of the From plugin in Frama-C main loop. - Nothing is exported in this module *) +(** Registration of the From plugin in Frama-C main loop. *) + +val display : Format.formatter option -> unit diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml index fed913033aa883471918032861ca60a8ab72715a..13413a811f265048bfdaa2db84c5bb1cf0c03d3a 100644 --- a/src/plugins/from/functionwise.ml +++ b/src/plugins/from/functionwise.ml @@ -86,43 +86,35 @@ module To_Use = struct end module From = From_compute.Make(To_Use) +let () = force_compute := From.compute -let () = - force_compute := From.compute +let self = Tbl.self + +let compute kf = ignore (To_Use.memo kf) let force_compute_all () = - Eva.Analysis.compute (); - Callgraph.Uses.iter_in_rev_order - (fun kf -> - if Kernel_function.is_definition kf && Eva.Results.is_called kf - then !Db.From.compute kf) - -(* Db Registration for function-wise from *) -let () = - Db.From.self := Tbl.self; - Db.From.is_computed := Tbl.mem; - Db.From.compute := - (fun kf -> ignore (To_Use.memo kf)); - Db.From.get := To_Use.memo; - Db.From.pretty := - (fun fmt v -> - let deps = To_Use.memo v in - Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt deps); - Db.From.find_deps_no_transitivity := - (fun stmt expr -> - Eva.Results.(before stmt |> expr_deps expr)); - (* Once this function has been moved to Eva, remove the dependency of Inout - from From. *) - Db.From.find_deps_no_transitivity_state := - (fun s e -> Eva.Results.(in_cvalue_state s |> expr_deps e)); - - ignore ( - Db.register_compute "From.compute_all" - [Tbl.self] - Db.From.compute_all - force_compute_all); + Eva.Analysis.compute () ; + Callgraph.Uses.iter_in_rev_order @@ fun kf -> + let is_definition = Kernel_function.is_definition kf in + if is_definition && Eva.Results.is_called kf then compute kf + +let compute_all = + let name = "From.compute_all" in + State_builder.apply_once name [Tbl.self] force_compute_all |> fst + +let is_computed = Tbl.mem + +let get = To_Use.memo + +let pretty fmt v = + Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt (get v) + +let find_deps_no_transitivity stmt expr = + Eva.Results.(before stmt |> expr_deps expr) +let find_deps_no_transitivity_state state expr = + Eva.Results.(in_cvalue_state state |> expr_deps expr) (* Local Variables: diff --git a/src/plugins/from/functionwise.mli b/src/plugins/from/functionwise.mli index 5d51ae4b1af5f30c1b103f204c1d52d93546dfe0..ec01c2be2cf41f78425423d03fcec5c486f5a029 100644 --- a/src/plugins/from/functionwise.mli +++ b/src/plugins/from/functionwise.mli @@ -21,6 +21,15 @@ (**************************************************************************) (** Computation of functional dependencies. In this module, the results are - computed from the synthetic results of the value analysis. + computed from the synthetic results of the value analysis. *) - Nothing is exported here, the API can be found in the Db.From module *) +open Cil_types + +val self : State.t +val compute : kernel_function -> unit +val compute_all : unit -> unit +val is_computed : kernel_function -> bool +val get : Cil_types.kernel_function -> Function_Froms.froms +val pretty : Format.formatter -> kernel_function -> unit +val find_deps_no_transitivity : stmt -> exp -> Locations.Zone.t +val find_deps_no_transitivity_state : Cvalue.Model.t -> exp -> Locations.Zone.t diff --git a/src/plugins/from/gui/from_register_gui.ml b/src/plugins/from/gui/from_register_gui.ml index c547b6da336edc04b350a69e222ba2fdc97a37e2..75408de49df139215a4ee3df1b4d46dc4b00f24b 100644 --- a/src/plugins/from/gui/from_register_gui.ml +++ b/src/plugins/from/gui/from_register_gui.ml @@ -32,9 +32,9 @@ let main (main_ui:Design.main_window_extension_points) = begin try let kf = Globals.Functions.get v in - if !Db.From.is_computed kf then + if From.is_computed kf then main_ui#pretty_information - "@[Functional dependencies:@\n%a@]@." !Db.From.pretty kf + "@[Functional dependencies:@\n%a@]@." From.pretty kf with Not_found -> () end | _ -> (); diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml index 34dfb781a9acc918cf7bbffb2cd0f28718053bbd..ca20eff30ecbf7a017cb2d7c57f7949d78476f35 100644 --- a/src/plugins/pdg/build.ml +++ b/src/plugins/pdg/build.ml @@ -621,7 +621,7 @@ let get_lval_infos lval stmt = Use the state at ki (before assign) and returns the new state (after assign). *) let process_asgn pdg state stmt lval exp = - let r_dpds = !Db.From.find_deps_no_transitivity stmt exp in + let r_dpds = From.find_deps_no_transitivity stmt exp in let r_decl = Cil.extract_varinfos_from_exp exp in let (l_loc, exact, l_dpds, l_decl) = get_lval_infos lval stmt in let key = Key.stmt_key stmt in @@ -636,7 +636,7 @@ let process_asgn pdg state stmt lval exp = (** Add a PDG node and its dependencies for each explicit call argument. *) let process_args pdg st stmt argl = let process_one_arg arg = - let dpds = !Db.From.find_deps_no_transitivity stmt arg in + let dpds = From.find_deps_no_transitivity stmt arg in let decl_dpds = Cil.extract_varinfos_from_exp arg in (dpds, decl_dpds) in let arg_dpds = List.map process_one_arg argl in @@ -717,7 +717,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc = | _ -> assert false in let mixed_froms = - try let froms = !Db.From.Callwise.find (Kstmt stmt) in Some froms + try let froms = From.Callwise.find (Kstmt stmt) in Some froms with Not_found -> None (* don't have callwise analysis (-calldeps option) *) in let process_simple_call acc called_kf = @@ -728,7 +728,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc = match mixed_froms with | Some _ -> state_with_inputs (* process outputs later *) | None -> (* don't have callwise analysis (-calldeps option) *) - let froms = !Db.From.get called_kf in + let froms = From.get called_kf in let state_for_this_call = call_outputs pdg state_before_call state_with_inputs stmt lvaloption froms funcexp_dpds @@ -763,7 +763,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc = * and register the statements that are control-dependent on it. *) let process_condition ctrl_dpds_infos pdg state stmt condition = - let loc_cond = !Db.From.find_deps_no_transitivity stmt condition in + let loc_cond = From.find_deps_no_transitivity stmt condition in let decls_cond = Cil.extract_varinfos_from_exp condition in let controlled_stmts = CtrlDpds.get_if_controlled_stmts ctrl_dpds_infos stmt in @@ -819,7 +819,7 @@ let process_return _current_function pdg state stmt ret_exp = let last_state = match ret_exp with | Some exp -> - let loc_exp = !Db.From.find_deps_no_transitivity stmt exp in + let loc_exp = From.find_deps_no_transitivity stmt exp in let decls_exp = Cil.extract_varinfos_from_exp exp in add_retres pdg state stmt loc_exp decls_exp | None -> @@ -963,7 +963,7 @@ let compute_pdg_for_f kf = let froms = match f_stmts with | [] -> Pdg_state.store_last_state pdg.states init_state; - let froms = !Db.From.get kf in + let froms = From.get kf in Some (froms) | start :: _ -> let ctrl_dpds_infos = CtrlDpds.compute kf in diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml index 8217fb8ccc0794e95ec2b72c7178730c50fa990c..b13b6da852cfbcf7bd3c8c1aa34cc56ef3420b31 100644 --- a/src/plugins/pdg/register.ml +++ b/src/plugins/pdg/register.ml @@ -28,7 +28,7 @@ let () = (fun () -> State_dependency_graph.add_codependencies ~onto:Pdg_tbl.self - [ !Db.From.self ]) + [ From.self ]) let deps = [Pdg_tbl.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self] diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml index ba308e499fa2110d4aef18bbe2f29c18c890d9e8..b28bf52e8ecaeb618c863f6bedf6383c6c040c84 100644 --- a/src/plugins/scope/zones.ml +++ b/src/plugins/scope/zones.ml @@ -40,7 +40,7 @@ module Data = struct let diff = Locations.Zone.diff (* over-approx *) let pretty fmt z = Format.fprintf fmt "@[<h 1>%a@]" Locations.Zone.pretty z - let exp_zone stmt exp = !Db.From.find_deps_no_transitivity stmt exp + let exp_zone stmt exp = From.find_deps_no_transitivity stmt exp end module Ctx = struct @@ -160,12 +160,12 @@ let process_call data_after stmt lvaloption funcexp args _loc = in let used, data = try - let froms = !Db.From.Callwise.find (Kstmt stmt) in + let froms = From.Callwise.find (Kstmt stmt) in process_one_call data_after stmt lvaloption froms with Not_found -> (* don't have callwise (-calldeps option) *) let do_call acc kf = (* notice that we use the same old data for each possible call *) - (process_one_call data_after stmt lvaloption (!Db.From.get kf))::acc + (process_one_call data_after stmt lvaloption (From.get kf))::acc in let l = List.fold_left do_call [] called_functions in (* in l, we have one result for each possible function called *) diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml index 43be72e63ec8990bfab89552dde3857cebd463e6..520907fcaed2ed9ebb8201f4dcf2b4c0fe27dc18 100644 --- a/src/plugins/slicing/fct_slice.ml +++ b/src/plugins/slicing/fct_slice.ml @@ -957,7 +957,7 @@ let add_change_call_action ff call call_info f_to_call actions = (** This function doesn't use the PDG call dependencies on purpose ! * See explanations in [add_spare_call_inputs] *) let get_called_needed_input called_kf need_out0 needed_out_zone = - let froms = !Db.From.get called_kf in + let froms = From.get called_kf in let from_table = froms.Function_Froms.deps_table in let acc_in_zones out (default, from_out) in_zones = if Locations.Zone.valid_intersects needed_out_zone out then diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml index 65c51a49d3de59b54b75d4d0fba00e3dc7794acc..61fb2ef8ebfb811b1e337759327b1e462de9bd1a 100644 --- a/src/plugins/slicing/slicingCmds.ml +++ b/src/plugins/slicing/slicingCmds.ml @@ -86,10 +86,10 @@ struct in let call_process lv f args _loc = (* returns [Zone.t read] by [lv, f, args], [Zone.t written] by [lv] *) - let read_zone = !Db.From.find_deps_no_transitivity stmt f in + let read_zone = From.find_deps_no_transitivity stmt f in let add_args arg inputs = Locations.Zone.join inputs - (!Db.From.find_deps_no_transitivity stmt arg) in + (From.find_deps_no_transitivity stmt arg) in let read_zone = List.fold_right add_args args read_zone in let read_zone,write_zone = match lv with @@ -101,16 +101,16 @@ struct | Switch (exp,_,_,_) | If (exp,_,_,_) -> (* returns [Zone.t read] by condition [exp], [Zone.bottom] *) - !Db.From.find_deps_no_transitivity stmt exp, Locations.Zone.bottom + From.find_deps_no_transitivity stmt exp, Locations.Zone.bottom | Instr (Set (lv,exp,_)) -> (* returns [Zone.t read] by [exp, lv], [Zone.t written] by [lv] *) - let read_zone = !Db.From.find_deps_no_transitivity stmt exp in + let read_zone = From.find_deps_no_transitivity stmt exp in lval_process read_zone stmt lv | Instr (Local_init (v, AssignInit i, _)) -> let rec collect zone i = match i with | SingleInit e -> - Locations.Zone.join zone (!Db.From.find_deps_no_transitivity stmt e) + Locations.Zone.join zone (From.find_deps_no_transitivity stmt e) | CompoundInit (_,l) -> List.fold_left (fun acc (_,i) -> collect acc i) zone l diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml index 4907cf29314c0d98ef989c991d66b70567bc1493..3a99ce4a5fc95abb60cf34b06103fd0f800bdc4b 100644 --- a/tests/pdg/dyn_dpds.ml +++ b/tests/pdg/dyn_dpds.ml @@ -9,7 +9,7 @@ let get_zones str_data (stmt, kf) = let lval_term = !Db.Properties.Interp.term_lval kf str_data in let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in let loc = - !Db.From.find_deps_no_transitivity + From.find_deps_no_transitivity stmt (Cil.new_exp ~loc:Cil_datatype.Location.unknown (Cil_types.Lval lval)) in