Extract solvers to goblint_solver dune library

Author: sim642

scripts/goblint-lib-modules.py

@@ -8,6 +8,7 @@
 
 goblint_lib_paths = [
     src_root_path / "goblint_lib.ml",
+    src_root_path / "solvers" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
 ]
 goblint_lib_modules = set()
@@ -33,6 +34,7 @@
 
     # libraries
     "Goblint_std",
+    "Goblint_solver",
     "Goblint_timing",
     "Goblint_backtrace",
     "Goblint_tracing",

src/analyses/base.ml

@@ -2871,7 +2871,7 @@ struct
         | "once" ->
           f (D.bot ())
         | "fixpoint" ->
-          let module DFP = LocalFixpoint.Make (D) in
+          let module DFP = Goblint_solver.LocalFixpoint.Make (D) in
           DFP.lfp f
         | _ ->
           assert false

src/dune

@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_library goblint_incremental goblint_tracing
+  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_incremental goblint_tracing
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.

src/framework/control.ml

@@ -85,7 +85,7 @@ struct
       let save_run = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in
       save_run <> ""
   end
-  module Slvr  = (GlobSolverFromEqSolver (Selector.Make (PostSolverArg))) (EQSys) (LHT) (GHT)
+  module Slvr  = (GlobSolverFromEqSolver (Goblint_solver.Selector.Make (PostSolverArg))) (EQSys) (LHT) (GHT)
   (* The comparator *)
   module CompareGlobSys = Constraints.CompareGlobSys (SpecSys)
 
@@ -476,7 +476,7 @@ struct
       let save_run_str = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in
 
       let lh, gh = if load_run <> "" then (
-          let module S2' = (GlobSolverFromEqSolver (Generic.LoadRunIncrSolver (PostSolverArg))) (EQSys) (LHT) (GHT) in
+          let module S2' = (GlobSolverFromEqSolver (Goblint_solver.Generic.LoadRunIncrSolver (PostSolverArg))) (EQSys) (LHT) (GHT) in
           let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *)
           r2
         ) else if compare_runs <> [] then (
@@ -582,7 +582,7 @@ struct
           let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *)
           CompareGlobSys.compare (get_string "solver", get_string "comparesolver") (lh,gh) (r2)
         in
-        compare_with (Selector.choose_solver (get_string "comparesolver"))
+        compare_with (Goblint_solver.Selector.choose_solver (get_string "comparesolver"))
       );
 
       (* Most warnings happen before during postsolver, but some happen later (e.g. in finalize), so enable this for the rest (if required by option). *)

src/goblint_lib.ml

@@ -288,41 +288,6 @@ module Serialize = Serialize
 module CilMaps = CilMaps
 
 
-(** {1 Solvers}
-
-    Generic solvers are used to solve {{!Analyses.MonSystem} (side-effecting) constraint systems}. *)
-
-(** {2 Top-down}
-
-    The top-down solver family. *)
-
-module Td3 = Td3
-module TopDown = TopDown
-module TopDown_term = TopDown_term
-module TopDown_space_cache_term = TopDown_space_cache_term
-module TopDown_deprecated = TopDown_deprecated
-
-(** {2 SLR}
-
-    The SLR solver family. *)
-
-module SLRphased = SLRphased
-module SLRterm = SLRterm
-module SLR = SLR
-
-(** {2 Other} *)
-
-module EffectWConEq = EffectWConEq
-module Worklist = Worklist
-module Generic = Generic
-module Selector = Selector
-
-module PostSolver = PostSolver
-module LocalFixpoint = LocalFixpoint
-module SolverStats = SolverStats
-module SolverBox = SolverBox
-
-
 (** {1 I/O}
 
     Various input/output interfaces and formats. *)

src/index.mld

@@ -19,6 +19,9 @@ This {{!page-domain}unwrapped library} contains various domain modules extracted
 {2 Library goblint.constraint}
 This {{!page-constraint}unwrapped library} contains various constraint system modules extracted from {!Goblint_lib}.
 
+{2 Library goblint.solver}
+{!modules:Goblint_solver}
+
 {2 Library goblint.library}
 This {{!page-library}unwrapped library} contains various library specification modules extracted from {!Goblint_lib}.
 

src/maingoblint.ml

@@ -513,15 +513,15 @@ let preprocess_parse_merge () =
 let do_stats () =
   if get_bool "dbg.timing.enabled" then (
     print_newline ();
-    SolverStats.print ();
+    Goblint_solver.SolverStats.print ();
     print_newline ();
     print_string "Timings:\n";
     Timing.Default.print (Stdlib.Format.formatter_of_out_channel @@ Messages.get_out "timing" Legacy.stderr);
     flush_all ()
   )
 
 let reset_stats () =
-  SolverStats.reset ();
+  Goblint_solver.SolverStats.reset ();
   Timing.Default.reset ();
   Timing.Program.reset ()
 

src/solvers/dune

@@ -0,0 +1,22 @@
+(include_subdirs no)
+
+(library
+ (name goblint_solver)
+ (public_name goblint.solver)
+ (libraries
+   batteries.unthreaded
+   goblint_std
+   goblint_common
+   goblint_domain
+   goblint_constraint
+   goblint_incremental
+   goblint-cil)
+ (flags :standard -open Goblint_std)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash
+    ppx_deriving_yojson))
+ (instrumentation (backend bisect_ppx)))
+
+(documentation)

src/solvers/goblint_solver.ml

@@ -0,0 +1,31 @@
+(** Generic solvers for {{!ConstrSys.MonSystem} (side-effecting) constraint systems}. *)
+
+(** {1 Top-down}
+
+    The top-down solver family. *)
+
+module Td3 = Td3
+module TopDown = TopDown
+module TopDown_term = TopDown_term
+module TopDown_space_cache_term = TopDown_space_cache_term
+module TopDown_deprecated = TopDown_deprecated
+
+(** {1 SLR}
+
+    The SLR solver family. *)
+
+module SLRphased = SLRphased
+module SLRterm = SLRterm
+module SLR = SLR
+
+(** {1 Other} *)
+
+module EffectWConEq = EffectWConEq
+module Worklist = Worklist
+module Generic = Generic
+module Selector = Selector
+
+module PostSolver = PostSolver
+module LocalFixpoint = LocalFixpoint
+module SolverStats = SolverStats
+module SolverBox = SolverBox