From c27c240b5f6bfb914b306ca72140e00364f86997 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 24 Jul 2024 17:03:26 +0300 Subject: [PATCH] Remove dynlink and findlib dependencies from goblint-cil library --- src/dune | 8 +-- src/feature.ml | 85 ------------------------------ src/feature.mli | 22 -------- src/main.ml | 4 +- src/mainFeature.ml | 122 ++++++++++++++++++++++++++++++++++++++++++++ src/mainFeature.mli | 57 +++++++++++++++++++++ 6 files changed, 185 insertions(+), 113 deletions(-) create mode 100644 src/mainFeature.ml create mode 100644 src/mainFeature.mli diff --git a/src/dune b/src/dune index 6b3766013..92375f31c 100644 --- a/src/dune +++ b/src/dune @@ -3,8 +3,8 @@ (library (public_name goblint-cil) (name goblintCil) - (libraries zarith findlib dynlink unix str stdlib-shims) - (modules (:standard \ main ciloptions machdepConfigure modelConfigure)) + (libraries zarith unix str stdlib-shims) + (modules (:standard \ main mainFeature ciloptions machdepConfigure modelConfigure)) ) (executable @@ -50,9 +50,9 @@ (executable (name main) - (modules main ciloptions) + (modules main mainFeature ciloptions) (modes native) - (libraries goblint-cil) + (libraries goblint-cil dynlink findlib) (flags :standard -linkall)) (env diff --git a/src/feature.ml b/src/feature.ml index 98692aa92..b5213a581 100644 --- a/src/feature.ml +++ b/src/feature.ml @@ -35,8 +35,6 @@ open Cil module E = Errormsg -module D = Dynlink -module F = Findlib type t = { mutable fd_enabled: bool; @@ -71,86 +69,3 @@ let enable s = let f = find s in f.fd_enabled <- true with Not_found -> E.s (E.error "cannot enable feature %s: not found" s) - -(** Dynamic linking *) - -let load s = - try - D.allow_unsafe_modules true; - D.loadfile s - with D.Error e -> E.s (E.error "%s" (D.error_message e)) - -(** Findlib magic *) - -let initialized = ref false -let init () = - if not !initialized then begin - F.init (); - initialized := true - end - -let adapt_filename f = try - D.adapt_filename f - with _ -> f - -let findlib_lookup pkg = - try - let preds = [ if D.is_native then "native" else "byte"; "plugin" ] in - let cil_deps = F.package_deep_ancestors preds ["goblint-cil"] in - let deps = F.package_deep_ancestors preds [pkg] in - let deps = List.filter (fun x -> not (List.mem x cil_deps)) deps in - let find_modules pkg = - let base = F.package_directory pkg in - let archives = - try F.package_property preds pkg "archive" - (* some packages have dependencies but no archive *) - with Not_found -> "" in - let modules = List.filter ((<>) "") (Str.split (Str.regexp "[ ,]+") archives) in - List.map (fun m -> F.resolve_path ~base (adapt_filename m)) modules in - let files = List.map find_modules deps in - List.flatten files - with - | F.No_such_package (pkg, msg) -> - E.s (E.error "findlib: no such package %s.\n%s" pkg msg) - | F.Package_loop pkg -> - E.s (E.error "findlib: package loop for %s." pkg) - -let find_plugin s = - if s = "" then E.s (E.error "missing module name") else - let s_resolve = adapt_filename (try F.resolve_path s with _ -> s) in - if Sys.file_exists s_resolve && not (Sys.is_directory s_resolve) then [s_resolve] - else findlib_lookup s - -(** List of loaded modules *) -let plugins = ref [] - -(** Add a single plugin, except if we have added it already *) -let add_plugin path = - if not (List.mem path !plugins) then - load path; - plugins := path :: !plugins - -(** Look for plugin and dependencies and add them *) -let loadWithDeps s = - let paths = find_plugin s in - List.iter add_plugin paths - -(** Parse only {switch} command-line option, ignoring every error raised by other, unparsed - options. Return the list of plugins to load. *) -let loadFromArgv switch = - let spec = [ - switch, Arg.String loadWithDeps, ""; - (* ignore --help at this stage *) - "--help", Arg.Unit ignore, ""; "-help", Arg.Unit ignore, "" ] in - let idx = ref 0 in - let rec aux () = - try - Arg.parse_argv ~current:idx Sys.argv spec ignore "" - with Arg.Bad _ | Arg.Help _ -> aux () - in init (); aux () - -let loadFromEnv name default = - let plugins = - try Str.split (Str.regexp "[ ,]+") (Sys.getenv name) - with Not_found -> default in - List.iter loadWithDeps plugins diff --git a/src/feature.mli b/src/feature.mli index 8e5987119..4297291e8 100644 --- a/src/feature.mli +++ b/src/feature.mli @@ -79,25 +79,3 @@ val enable : string -> unit (** Check if a given feature is enabled. Return false if the feature is not registered. *) val enabled : string -> bool - -(** {1 Internal}*) - -(** Initialize the module. This needs to be called before {!loadWithDeps} is - used. Called automatically by {!loadFromArgv}. *) -val init : unit -> unit - -(** Find and dynamically links a module. The name should be either a path to a - cmo, cma or cmxs file, or the name of a findlib package. In the latter case, - package dependencies are loaded automatically. Each file is loaded at most - one. The loaded module must call {!register} to make its features - available to CIL. *) -val loadWithDeps : string -> unit - -(** [loadFromArgv switch] searches {!Sys.argv} for the command-line option - [switch], and loads the modules passed as parameters. Ignores every other - {!Sys.argv} element. *) -val loadFromArgv : string -> unit - -(** [loadFromEnv name default] loads coma-separated module names stored in the - environment variable [name], or [default] if it is not defined. *) -val loadFromEnv : string -> string list -> unit diff --git a/src/main.ml b/src/main.ml index b257176ab..b1f2a01b6 100644 --- a/src/main.ml +++ b/src/main.ml @@ -130,8 +130,8 @@ let theMain () = (* Load plugins. This needs to be done before command-line arguments are built. *) - Feature.loadFromEnv "CIL_FEATURES" ["goblint-cil.default-features"]; - Feature.loadFromArgv "--load"; + MainFeature.loadFromEnv "CIL_FEATURES" ["goblint-cil.default-features"]; + MainFeature.loadFromArgv "--load"; (*********** COMMAND LINE ARGUMENTS *****************) diff --git a/src/mainFeature.ml b/src/mainFeature.ml new file mode 100644 index 000000000..41aab29e1 --- /dev/null +++ b/src/mainFeature.ml @@ -0,0 +1,122 @@ +(* + Copyright (c) 2013 + Gabriel Kerneis + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions are + met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + 3. The names of the contributors may not be used to endorse or promote + products derived from this software without specific prior written + permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + *) + +open GoblintCil + +module E = Errormsg +module D = Dynlink +module F = Findlib + +(** Dynamic linking *) + +let load s = + try + D.allow_unsafe_modules true; + D.loadfile s + with D.Error e -> E.s (E.error "%s" (D.error_message e)) + +(** Findlib magic *) + +let initialized = ref false +let init () = + if not !initialized then begin + F.init (); + initialized := true + end + +let adapt_filename f = try + D.adapt_filename f + with _ -> f + +let findlib_lookup pkg = + try + let preds = [ if D.is_native then "native" else "byte"; "plugin" ] in + let cil_deps = F.package_deep_ancestors preds ["goblint-cil"] in + let deps = F.package_deep_ancestors preds [pkg] in + let deps = List.filter (fun x -> not (List.mem x cil_deps)) deps in + let find_modules pkg = + let base = F.package_directory pkg in + let archives = + try F.package_property preds pkg "archive" + (* some packages have dependencies but no archive *) + with Not_found -> "" in + let modules = List.filter ((<>) "") (Str.split (Str.regexp "[ ,]+") archives) in + List.map (fun m -> F.resolve_path ~base (adapt_filename m)) modules in + let files = List.map find_modules deps in + List.flatten files + with + | F.No_such_package (pkg, msg) -> + E.s (E.error "findlib: no such package %s.\n%s" pkg msg) + | F.Package_loop pkg -> + E.s (E.error "findlib: package loop for %s." pkg) + +let find_plugin s = + if s = "" then E.s (E.error "missing module name") else + let s_resolve = adapt_filename (try F.resolve_path s with _ -> s) in + if Sys.file_exists s_resolve && not (Sys.is_directory s_resolve) then [s_resolve] + else findlib_lookup s + +(** List of loaded modules *) +let plugins = ref [] + +(** Add a single plugin, except if we have added it already *) +let add_plugin path = + if not (List.mem path !plugins) then + load path; + plugins := path :: !plugins + +(** Look for plugin and dependencies and add them *) +let loadWithDeps s = + let paths = find_plugin s in + List.iter add_plugin paths + +(** Parse only {switch} command-line option, ignoring every error raised by other, unparsed + options. Return the list of plugins to load. *) +let loadFromArgv switch = + let spec = [ + switch, Arg.String loadWithDeps, ""; + (* ignore --help at this stage *) + "--help", Arg.Unit ignore, ""; "-help", Arg.Unit ignore, "" ] in + let idx = ref 0 in + let rec aux () = + try + Arg.parse_argv ~current:idx Sys.argv spec ignore "" + with Arg.Bad _ | Arg.Help _ -> aux () + in init (); aux () + +let loadFromEnv name default = + let plugins = + try Str.split (Str.regexp "[ ,]+") (Sys.getenv name) + with Not_found -> default in + List.iter loadWithDeps plugins diff --git a/src/mainFeature.mli b/src/mainFeature.mli new file mode 100644 index 000000000..44e2e6389 --- /dev/null +++ b/src/mainFeature.mli @@ -0,0 +1,57 @@ +(* + Copyright (c) 2013 + Gabriel Kerneis + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions are + met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + 3. The names of the contributors may not be used to endorse or promote + products derived from this software without specific prior written + permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + *) + +(** Extending CIL with external features *) + +(** {1 Internal}*) + +(** Initialize the module. This needs to be called before {!loadWithDeps} is + used. Called automatically by {!loadFromArgv}. *) +val init : unit -> unit + +(** Find and dynamically links a module. The name should be either a path to a + cmo, cma or cmxs file, or the name of a findlib package. In the latter case, + package dependencies are loaded automatically. Each file is loaded at most + one. The loaded module must call {!register} to make its features + available to CIL. *) +val loadWithDeps : string -> unit + +(** [loadFromArgv switch] searches {!Sys.argv} for the command-line option + [switch], and loads the modules passed as parameters. Ignores every other + {!Sys.argv} element. *) +val loadFromArgv : string -> unit + +(** [loadFromEnv name default] loads coma-separated module names stored in the + environment variable [name], or [default] if it is not defined. *) +val loadFromEnv : string -> string list -> unit