Remove dynlink and findlib dependencies from goblint-cil library

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 machdepArchConfigure modelConfigure))
+  (libraries zarith unix str stdlib-shims)
+  (modules (:standard \ main mainFeature ciloptions machdepConfigure machdepArchConfigure modelConfigure))
 )
 
 (executable
@@ -66,9 +66,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

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

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

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 *****************)

src/mainFeature.ml

@@ -0,0 +1,122 @@
+(*
+   Copyright (c) 2013
+    Gabriel Kerneis     <[email protected]>
+   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

src/mainFeature.mli

@@ -0,0 +1,57 @@
+(*
+   Copyright (c) 2013
+    Gabriel Kerneis     <[email protected]>
+   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