From 834df31e5821a5a38c956abe7f029c4e0a4b122c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Dec 2023 15:51:06 +0200 Subject: [PATCH] Extract solvers to goblint_solver dune library --- scripts/goblint-lib-modules.py | 2 ++ src/analyses/base.ml | 2 +- src/dune | 2 +- src/framework/control.ml | 6 +++--- src/goblint_lib.ml | 35 ---------------------------------- src/index.mld | 3 +++ src/maingoblint.ml | 4 ++-- src/solvers/dune | 22 +++++++++++++++++++++ src/solvers/goblint_solver.ml | 31 ++++++++++++++++++++++++++++++ 9 files changed, 65 insertions(+), 42 deletions(-) create mode 100644 src/solvers/dune create mode 100644 src/solvers/goblint_solver.ml diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py index ec0e78e440..95ac9b268e 100755 --- a/scripts/goblint-lib-modules.py +++ b/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", diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 912d1f3bff..2b8ca4d429 100644 --- a/src/analyses/base.ml +++ b/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 diff --git a/src/dune b/src/dune index 59845b8e03..2ea9155b9b 100644 --- a/src/dune +++ b/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. diff --git a/src/framework/control.ml b/src/framework/control.ml index 26ef8bbda0..391c766feb 100644 --- a/src/framework/control.ml +++ b/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). *) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index a340cb085f..1bc70f3f52 100644 --- a/src/goblint_lib.ml +++ b/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. *) diff --git a/src/index.mld b/src/index.mld index 3ed2b8079f..0763284c15 100644 --- a/src/index.mld +++ b/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}. diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 2c7d353594..f1d2793d2e 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -513,7 +513,7 @@ 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); @@ -521,7 +521,7 @@ let do_stats () = ) let reset_stats () = - SolverStats.reset (); + Goblint_solver.SolverStats.reset (); Timing.Default.reset (); Timing.Program.reset () diff --git a/src/solvers/dune b/src/solvers/dune new file mode 100644 index 0000000000..907d082089 --- /dev/null +++ b/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) diff --git a/src/solvers/goblint_solver.ml b/src/solvers/goblint_solver.ml new file mode 100644 index 0000000000..0a264d7dea --- /dev/null +++ b/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