diff --git a/gobview b/gobview index 3de13d7412..c8fcb09e9a 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 3de13d74124ab7bc30d8be299f02570d8f498b84 +Subproject commit c8fcb09e9a3e27de22d4803606d5784f667a542a diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py index ec0e78e440..8ae3b4b3eb 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 / "solver" / "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/analyses/wrapperFunctionAnalysis0.ml b/src/cdomain/value/analyses/wrapperFunctionAnalysis0.ml similarity index 100% rename from src/analyses/wrapperFunctionAnalysis0.ml rename to src/cdomain/value/analyses/wrapperFunctionAnalysis0.ml diff --git a/src/cdomain/value/cdomain_value.mld b/src/cdomain/value/cdomain_value.mld new file mode 100644 index 0000000000..668bbfa0ca --- /dev/null +++ b/src/cdomain/value/cdomain_value.mld @@ -0,0 +1,71 @@ +{0 Library goblint.cdomain.value} +This library is unwrapped and provides the following top-level modules. +For better context, see {!Goblint_lib} which also documents these modules. + + +{1 Domains} + +{2 Analysis-specific} + +{3 Value} + +{4 Non-relational} + +{5 Numeric} +{!modules: +IntDomain +FloatDomain +} + +{5 Addresses} +{!modules: +Mval +Offset +StringDomain +AddressDomain +} + +{5 Complex} +{!modules: +StructDomain +UnionDomain +ArrayDomain +NullByteSet +JmpBufDomain +} + +{5 Combined} +{!modules: +ValueDomain +ValueDomainQueries +} + +{3 Concurrency} +{!modules: +MutexAttrDomain +ThreadIdDomain +ConcDomain +} + +{3 Other} +{!modules: +Lval +} + + +{1 I/O} + +{2 Witnesses} +{!modules: +Invariant +InvariantCil +} + + +{1 Utilities} + +{2 Analysis-specific} +{!modules: +PrecisionUtil +WideningThresholds +} diff --git a/src/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml similarity index 100% rename from src/cdomains/addressDomain.ml rename to src/cdomain/value/cdomains/addressDomain.ml diff --git a/src/cdomains/addressDomain.mli b/src/cdomain/value/cdomains/addressDomain.mli similarity index 100% rename from src/cdomains/addressDomain.mli rename to src/cdomain/value/cdomains/addressDomain.mli diff --git a/src/cdomains/addressDomain_intf.ml b/src/cdomain/value/cdomains/addressDomain_intf.ml similarity index 100% rename from src/cdomains/addressDomain_intf.ml rename to src/cdomain/value/cdomains/addressDomain_intf.ml diff --git a/src/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml similarity index 100% rename from src/cdomains/arrayDomain.ml rename to src/cdomain/value/cdomains/arrayDomain.ml diff --git a/src/cdomains/arrayDomain.mli b/src/cdomain/value/cdomains/arrayDomain.mli similarity index 100% rename from src/cdomains/arrayDomain.mli rename to src/cdomain/value/cdomains/arrayDomain.mli diff --git a/src/cdomains/concDomain.ml b/src/cdomain/value/cdomains/concDomain.ml similarity index 100% rename from src/cdomains/concDomain.ml rename to src/cdomain/value/cdomains/concDomain.ml diff --git a/src/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml similarity index 100% rename from src/cdomains/floatDomain.ml rename to src/cdomain/value/cdomains/floatDomain.ml diff --git a/src/cdomains/floatDomain.mli b/src/cdomain/value/cdomains/floatDomain.mli similarity index 100% rename from src/cdomains/floatDomain.mli rename to src/cdomain/value/cdomains/floatDomain.mli diff --git a/src/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml similarity index 100% rename from src/cdomains/intDomain.ml rename to src/cdomain/value/cdomains/intDomain.ml diff --git a/src/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli similarity index 100% rename from src/cdomains/intDomain.mli rename to src/cdomain/value/cdomains/intDomain.mli diff --git a/src/cdomains/jmpBufDomain.ml b/src/cdomain/value/cdomains/jmpBufDomain.ml similarity index 100% rename from src/cdomains/jmpBufDomain.ml rename to src/cdomain/value/cdomains/jmpBufDomain.ml diff --git a/src/cdomains/lval.ml b/src/cdomain/value/cdomains/lval.ml similarity index 100% rename from src/cdomains/lval.ml rename to src/cdomain/value/cdomains/lval.ml diff --git a/src/cdomains/mutexAttrDomain.ml b/src/cdomain/value/cdomains/mutexAttrDomain.ml similarity index 100% rename from src/cdomains/mutexAttrDomain.ml rename to src/cdomain/value/cdomains/mutexAttrDomain.ml diff --git a/src/cdomains/mval.ml b/src/cdomain/value/cdomains/mval.ml similarity index 100% rename from src/cdomains/mval.ml rename to src/cdomain/value/cdomains/mval.ml diff --git a/src/cdomains/mval.mli b/src/cdomain/value/cdomains/mval.mli similarity index 100% rename from src/cdomains/mval.mli rename to src/cdomain/value/cdomains/mval.mli diff --git a/src/cdomains/mval_intf.ml b/src/cdomain/value/cdomains/mval_intf.ml similarity index 100% rename from src/cdomains/mval_intf.ml rename to src/cdomain/value/cdomains/mval_intf.ml diff --git a/src/cdomains/nullByteSet.ml b/src/cdomain/value/cdomains/nullByteSet.ml similarity index 100% rename from src/cdomains/nullByteSet.ml rename to src/cdomain/value/cdomains/nullByteSet.ml diff --git a/src/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml similarity index 100% rename from src/cdomains/offset.ml rename to src/cdomain/value/cdomains/offset.ml diff --git a/src/cdomains/offset.mli b/src/cdomain/value/cdomains/offset.mli similarity index 100% rename from src/cdomains/offset.mli rename to src/cdomain/value/cdomains/offset.mli diff --git a/src/cdomains/offset_intf.ml b/src/cdomain/value/cdomains/offset_intf.ml similarity index 100% rename from src/cdomains/offset_intf.ml rename to src/cdomain/value/cdomains/offset_intf.ml diff --git a/src/cdomains/preValueDomain.ml b/src/cdomain/value/cdomains/preValueDomain.ml similarity index 100% rename from src/cdomains/preValueDomain.ml rename to src/cdomain/value/cdomains/preValueDomain.ml diff --git a/src/cdomains/stringDomain.ml b/src/cdomain/value/cdomains/stringDomain.ml similarity index 100% rename from src/cdomains/stringDomain.ml rename to src/cdomain/value/cdomains/stringDomain.ml diff --git a/src/cdomains/stringDomain.mli b/src/cdomain/value/cdomains/stringDomain.mli similarity index 100% rename from src/cdomains/stringDomain.mli rename to src/cdomain/value/cdomains/stringDomain.mli diff --git a/src/cdomains/structDomain.ml b/src/cdomain/value/cdomains/structDomain.ml similarity index 100% rename from src/cdomains/structDomain.ml rename to src/cdomain/value/cdomains/structDomain.ml diff --git a/src/cdomains/structDomain.mli b/src/cdomain/value/cdomains/structDomain.mli similarity index 100% rename from src/cdomains/structDomain.mli rename to src/cdomain/value/cdomains/structDomain.mli diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml similarity index 100% rename from src/cdomains/threadIdDomain.ml rename to src/cdomain/value/cdomains/threadIdDomain.ml diff --git a/src/cdomains/unionDomain.ml b/src/cdomain/value/cdomains/unionDomain.ml similarity index 100% rename from src/cdomains/unionDomain.ml rename to src/cdomain/value/cdomains/unionDomain.ml diff --git a/src/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml similarity index 100% rename from src/cdomains/valueDomain.ml rename to src/cdomain/value/cdomains/valueDomain.ml diff --git a/src/domains/invariant.ml b/src/cdomain/value/domains/invariant.ml similarity index 100% rename from src/domains/invariant.ml rename to src/cdomain/value/domains/invariant.ml diff --git a/src/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml similarity index 100% rename from src/domains/invariantCil.ml rename to src/cdomain/value/domains/invariantCil.ml diff --git a/src/domains/valueDomainQueries.ml b/src/cdomain/value/domains/valueDomainQueries.ml similarity index 100% rename from src/domains/valueDomainQueries.ml rename to src/cdomain/value/domains/valueDomainQueries.ml diff --git a/src/cdomain/value/dune b/src/cdomain/value/dune new file mode 100644 index 0000000000..c89d5be04d --- /dev/null +++ b/src/cdomain/value/dune @@ -0,0 +1,24 @@ +(include_subdirs unqualified) + +(library + (name goblint_cdomain_value) + (public_name goblint.cdomain.value) + (wrapped false) ; TODO: wrap + (libraries + batteries.unthreaded + goblint_std + goblint_common + goblint_config + goblint_library + goblint_domain + 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/util/precisionUtil.ml b/src/cdomain/value/util/precisionUtil.ml similarity index 100% rename from src/util/precisionUtil.ml rename to src/cdomain/value/util/precisionUtil.ml diff --git a/src/util/wideningThresholds.ml b/src/cdomain/value/util/wideningThresholds.ml similarity index 100% rename from src/util/wideningThresholds.ml rename to src/cdomain/value/util/wideningThresholds.ml diff --git a/src/util/wideningThresholds.mli b/src/cdomain/value/util/wideningThresholds.mli similarity index 100% rename from src/util/wideningThresholds.mli rename to src/cdomain/value/util/wideningThresholds.mli diff --git a/src/cdomains/floatOps/floatOps.ml b/src/common/cdomains/floatOps/floatOps.ml similarity index 100% rename from src/cdomains/floatOps/floatOps.ml rename to src/common/cdomains/floatOps/floatOps.ml diff --git a/src/cdomains/floatOps/floatOps.mli b/src/common/cdomains/floatOps/floatOps.mli similarity index 100% rename from src/cdomains/floatOps/floatOps.mli rename to src/common/cdomains/floatOps/floatOps.mli diff --git a/src/cdomains/floatOps/stubs.c b/src/common/cdomains/floatOps/stubs.c similarity index 100% rename from src/cdomains/floatOps/stubs.c rename to src/common/cdomains/floatOps/stubs.c diff --git a/src/common/common.mld b/src/common/common.mld index 2ad88c3758..2176a95b8a 100644 --- a/src/common/common.mld +++ b/src/common/common.mld @@ -16,6 +16,7 @@ CfgTools {2 Specification} {!modules: AnalysisState +AnalysisStateUtil ControlSpecC } @@ -42,6 +43,7 @@ Messages {2 General} {!modules: +IntOps LazyEval ResettableLazy MessageUtil @@ -55,6 +57,11 @@ Cilfacade RichVarinfo } +{2 Analysis-specific} +{!modules: +ContextUtil +} + {1 Library extensions} diff --git a/src/common/dune b/src/common/dune index 458ef02dcb..8576970900 100644 --- a/src/common/dune +++ b/src/common/dune @@ -16,6 +16,8 @@ goblint_timing qcheck-core.runner) (flags :standard -open Goblint_std) + (foreign_stubs (language c) (names stubs)) + (ocamlopt_flags :standard -no-float-const-prop) (preprocess (pps ppx_deriving.std diff --git a/src/util/analysisStateUtil.ml b/src/common/util/analysisStateUtil.ml similarity index 100% rename from src/util/analysisStateUtil.ml rename to src/common/util/analysisStateUtil.ml diff --git a/src/util/contextUtil.ml b/src/common/util/contextUtil.ml similarity index 100% rename from src/util/contextUtil.ml rename to src/common/util/contextUtil.ml diff --git a/src/util/intOps.ml b/src/common/util/intOps.ml similarity index 100% rename from src/util/intOps.ml rename to src/common/util/intOps.ml diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml new file mode 100644 index 0000000000..1698d5f214 --- /dev/null +++ b/src/constraint/constrSys.ml @@ -0,0 +1,299 @@ +(** {{!MonSystem} constraint system} signatures. *) + +open Batteries + +module type SysVar = +sig + type t + val is_write_only: t -> bool +end + +module type VarType = +sig + include Hashtbl.HashedType + include SysVar with type t := t + val pretty_trace: unit -> t -> GoblintCil.Pretty.doc + val compare : t -> t -> int + + val printXml : 'a BatInnerIO.output -> t -> unit + val var_id : t -> string + val node : t -> MyCFG.node + val relift : t -> t (* needed only for incremental+hashcons to re-hashcons contexts after loading *) +end + +(** Abstract incremental change to constraint system. + @param 'v constrain system variable type *) +type 'v sys_change_info = { + obsolete: 'v list; (** Variables to destabilize. *) + delete: 'v list; (** Variables to delete. *) + reluctant: 'v list; (** Variables to solve reluctantly. *) + restart: 'v list; (** Variables to restart. *) +} + +(** A side-effecting system. *) +module type MonSystem = +sig + type v (* variables *) + type d (* values *) + type 'a m (* basically a monad carrier *) + + (** Variables must be hashable, comparable, etc. *) + module Var : VarType with type t = v + + (** Values must form a lattice. *) + module Dom : Lattice.S with type t = d + + (** The system in functional form. *) + val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m + + val sys_change: (v -> d) -> v sys_change_info + (** Compute incremental constraint system change from old solution. *) +end + +(** Any system of side-effecting equations over lattices. *) +module type EqConstrSys = MonSystem with type 'a m := 'a option + +(** A side-effecting system with globals. *) +module type GlobConstrSys = +sig + module LVar : VarType + module GVar : VarType + + module D : Lattice.S + module G : Lattice.S + val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option + val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit + val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info +end + +(** A solver is something that can translate a system into a solution (hash-table). + Incremental solver has data to be marshaled. *) +module type GenericEqIncrSolverBase = + functor (S:EqConstrSys) -> + functor (H:Hashtbl.S with type key=S.v) -> + sig + type marshal + + val copy_marshal: marshal -> marshal + val relift_marshal: marshal -> marshal + + (** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs], + reached from starting values [xs]. + As a second component the solver returns data structures for incremental serialization. *) + val solve : (S.v*S.d) list -> S.v list -> marshal option -> S.d H.t * marshal + end + +(** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *) +module type IncrSolverArg = +sig + val should_prune: bool + val should_verify: bool + val should_warn: bool + val should_save_run: bool +end + +(** An incremental solver takes the argument about postsolving. *) +module type GenericEqIncrSolver = + functor (Arg: IncrSolverArg) -> + GenericEqIncrSolverBase + +(** A solver is something that can translate a system into a solution (hash-table) *) +module type GenericEqSolver = + functor (S:EqConstrSys) -> + functor (H:Hashtbl.S with type key=S.v) -> + sig + (** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs], + reached from starting values [xs]. *) + val solve : (S.v*S.d) list -> S.v list -> S.d H.t + end + +(** A solver is something that can translate a system into a solution (hash-table) *) +module type GenericGlobSolver = + functor (S:GlobConstrSys) -> + functor (LH:Hashtbl.S with type key=S.LVar.t) -> + functor (GH:Hashtbl.S with type key=S.GVar.t) -> + sig + type marshal + + val copy_marshal: marshal -> marshal + val relift_marshal: marshal -> marshal + + (** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs], + reached from starting values [xs]. + As a second component the solver returns data structures for incremental serialization. *) + val solve : (S.LVar.t*S.D.t) list -> (S.GVar.t*S.G.t) list -> S.LVar.t list -> marshal option -> (S.D.t LH.t * S.G.t GH.t) * marshal + end + + +(** Combined variables so that we can also use the more common [EqConstrSys] + that uses only one kind of a variable. *) +module Var2 (LV:VarType) (GV:VarType) + : VarType + with type t = [ `L of LV.t | `G of GV.t ] += +struct + type t = [ `L of LV.t | `G of GV.t ] [@@deriving eq, ord, hash] + let relift = function + | `L x -> `L (LV.relift x) + | `G x -> `G (GV.relift x) + + let pretty_trace () = function + | `L a -> GoblintCil.Pretty.dprintf "L:%a" LV.pretty_trace a + | `G a -> GoblintCil.Pretty.dprintf "G:%a" GV.pretty_trace a + + let printXml f = function + | `L a -> LV.printXml f a + | `G a -> GV.printXml f a + + let var_id = function + | `L a -> LV.var_id a + | `G a -> GV.var_id a + + let node = function + | `L a -> LV.node a + | `G a -> GV.node a + + let is_write_only = function + | `L a -> LV.is_write_only a + | `G a -> GV.is_write_only a +end + + +(** Translate a [GlobConstrSys] into a [EqConstrSys] *) +module EqConstrSysFromGlobConstrSys (S:GlobConstrSys) + : EqConstrSys with type v = Var2(S.LVar)(S.GVar).t + and type d = Lattice.Lift2(S.G)(S.D).t + and module Var = Var2(S.LVar)(S.GVar) + and module Dom = Lattice.Lift2(S.G)(S.D) += +struct + module Var = Var2(S.LVar)(S.GVar) + module Dom = + struct + include Lattice.Lift2 (S.G) (S.D) + let printXml f = function + | `Lifted1 a -> S.G.printXml f a + | `Lifted2 a -> S.D.printXml f a + | (`Bot | `Top) as x -> printXml f x + end + type v = Var.t + type d = Dom.t + + let getG = function + | `Lifted1 x -> x + | `Bot -> S.G.bot () + | `Top -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has top value" + | `Lifted2 _ -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has local value" + + let getL = function + | `Lifted2 x -> x + | `Bot -> S.D.bot () + | `Top -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has top value" + | `Lifted1 _ -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has global value" + + let l, g = (fun x -> `L x), (fun x -> `G x) + let lD, gD = (fun x -> `Lifted2 x), (fun x -> `Lifted1 x) + + let conv f get set = + f (getL % get % l) (fun x v -> set (l x) (lD v)) + (getG % get % g) (fun x v -> set (g x) (gD v)) + |> lD + + let system = function + | `G _ -> None + | `L x -> Option.map conv (S.system x) + + let sys_change get = + S.sys_change (getL % get % l) (getG % get % g) +end + +(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *) +module GlobConstrSolFromEqConstrSolBase (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) (VH: Hashtbl.S with type key = Var2 (S.LVar) (S.GVar).t) = +struct + let split_solution hm = + let l' = LH.create 113 in + let g' = GH.create 113 in + let split_vars x d = match x with + | `L x -> + begin match d with + | `Lifted2 d -> LH.replace l' x d + (* | `Bot -> () *) + (* Since Verify2 is broken and only checks existing keys, add it with local bottom value. + This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *) + | `Bot -> LH.replace l' x (S.D.bot ()) + | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value" + | `Lifted1 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value" + end + | `G x -> + begin match d with + | `Lifted1 d -> GH.replace g' x d + | `Bot -> () + | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has top value" + | `Lifted2 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has local value" + end + in + VH.iter split_vars hm; + (l', g') +end + +(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution. *) +module GlobConstrSolFromEqConstrSol (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) = +struct + module S2 = EqConstrSysFromGlobConstrSys (S) + module VH = Hashtbl.Make (S2.Var) + + include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) +end + +(** Transforms a [GenericEqIncrSolver] into a [GenericGlobSolver]. *) +module GlobSolverFromEqSolver (Sol:GenericEqIncrSolverBase) + = functor (S:GlobConstrSys) -> + functor (LH:Hashtbl.S with type key=S.LVar.t) -> + functor (GH:Hashtbl.S with type key=S.GVar.t) -> + struct + module EqSys = EqConstrSysFromGlobConstrSys (S) + + module VH : Hashtbl.S with type key=EqSys.v = Hashtbl.Make(EqSys.Var) + module Sol' = Sol (EqSys) (VH) + + module Splitter = GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) (* reuse EqSys and VH *) + + type marshal = Sol'.marshal + + let copy_marshal = Sol'.copy_marshal + let relift_marshal = Sol'.relift_marshal + + let solve ls gs l old_data = + let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls + @ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in + let sv = List.map (fun x -> `L x) l in + let hm, solver_data = Sol'.solve vs sv old_data in + Splitter.split_solution hm, solver_data + end + + +(** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *) +module CurrentVarEqConstrSys (S: EqConstrSys) = +struct + let current_var = ref None + + module S = + struct + include S + + let system x = + match S.system x with + | None -> None + | Some f -> + let f' get set = + let old_current_var = !current_var in + current_var := Some x; + Fun.protect ~finally:(fun () -> + current_var := old_current_var + ) (fun () -> + f get set + ) + in + Some f' + end +end diff --git a/src/constraint/constraint.mld b/src/constraint/constraint.mld new file mode 100644 index 0000000000..695e7bfa0d --- /dev/null +++ b/src/constraint/constraint.mld @@ -0,0 +1,16 @@ +{0 Library goblint.constraint} +This library is unwrapped and provides the following top-level modules. +For better context, see {!Goblint_lib} which also documents these modules. + + +{1 Framework} + +{2 Specification} +{!modules: +ConstrSys +} + +{2 Results} +{!modules: +VarQuery +} diff --git a/src/constraint/dune b/src/constraint/dune new file mode 100644 index 0000000000..2d11b9010f --- /dev/null +++ b/src/constraint/dune @@ -0,0 +1,21 @@ +(include_subdirs no) + +(library + (name goblint_constraint) + (public_name goblint.constraint) + (wrapped false) ; TODO: wrap + (libraries + batteries.unthreaded + goblint_std + goblint_common + goblint_domain + 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/framework/varQuery.ml b/src/constraint/varQuery.ml similarity index 100% rename from src/framework/varQuery.ml rename to src/constraint/varQuery.ml diff --git a/src/framework/varQuery.mli b/src/constraint/varQuery.mli similarity index 100% rename from src/framework/varQuery.mli rename to src/constraint/varQuery.mli diff --git a/src/dune b/src/dune index eac6640451..d7c6d28026 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_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_cdomain_value 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. @@ -61,7 +61,6 @@ ) ) (flags :standard -open Goblint_std) - (foreign_stubs (language c) (names stubs)) (ocamlopt_flags :standard -no-float-const-prop) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson ppx_blob)) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 405df5b6a6..ca6cb9fd51 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -11,24 +11,6 @@ module M = Messages * other functions. *) type fundecs = fundec list * fundec list * fundec list -module type SysVar = -sig - type t - val is_write_only: t -> bool -end - -module type VarType = -sig - include Hashtbl.HashedType - include SysVar with type t := t - val pretty_trace: unit -> t -> doc - val compare : t -> t -> int - - val printXml : 'a BatInnerIO.output -> t -> unit - val var_id : t -> string - val node : t -> MyCFG.node - val relift : t -> t (* needed only for incremental+hashcons to re-hashcons contexts after loading *) -end module Var = struct @@ -69,7 +51,7 @@ end module type SpecSysVar = sig include Printable.S - include SysVar with type t := t + include ConstrSys.SysVar with type t := t end module GVarF (V: SpecSysVar) = @@ -162,183 +144,6 @@ struct end -module ResultNode: Printable.S with type t = MyCFG.node = -struct - include Printable.Std - - include Node - - let name () = "resultnode" - - let show a = - (* Not using Node.location here to have updated locations in incremental analysis. - See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) - let x = UpdateCil.getLoc a in - let f = Node.find_fundec a in - CilType.Location.show x ^ "(" ^ f.svar.vname ^ ")" - - include Printable.SimpleShow ( - struct - type nonrec t = t - let show = show - end - ) -end - -module type ResultConf = -sig - val result_name: string -end - -module Result (Range: Printable.S) (C: ResultConf) = -struct - include Hashtbl.Make (ResultNode) - type nonrec t = Range.t t (* specialize polymorphic type for Range values *) - - let pretty () mapping = - let f key st dok = - dok ++ dprintf "%a ->@? @[%a@]\n" ResultNode.pretty key Range.pretty st - in - let content () = fold f mapping nil in - let defline () = dprintf "OTHERS -> Not available\n" in - dprintf "@[Mapping {\n @[%t%t@]}@]" content defline - - include C - - let printXml f xs = - let print_one n v = - (* Not using Node.location here to have updated locations in incremental analysis. - See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) - let loc = UpdateCil.getLoc n in - BatPrintf.fprintf f "\n" (Node.show_id n) loc.file loc.line loc.byte loc.column; - BatPrintf.fprintf f "%a\n" Range.printXml v - in - iter print_one xs - - let printJson f xs = - let print_one n v = - (* Not using Node.location here to have updated locations in incremental analysis. - See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) - let loc = UpdateCil.getLoc n in - BatPrintf.fprintf f "{\n\"id\": \"%s\", \"file\": \"%s\", \"line\": \"%d\", \"byte\": \"%d\", \"column\": \"%d\", \"states\": %s\n},\n" (Node.show_id n) loc.file loc.line loc.byte loc.column (Yojson.Safe.to_string (Range.to_yojson v)) - in - iter print_one xs - - let printXmlWarning f () = - let one_text f Messages.Piece.{loc; text = m; _} = - match loc with - | Some loc -> - let l = Messages.Location.to_cil loc in - BatPrintf.fprintf f "\n%s" l.file l.line l.column (XmlUtil.escape m) - | None -> - () (* TODO: not outputting warning without location *) - in - let one_w f (m: Messages.Message.t) = match m.multipiece with - | Single piece -> one_text f piece - | Group {group_text = n; pieces = e; group_loc} -> - let group_loc_text = match group_loc with - | None -> "" - | Some group_loc -> GobPretty.sprintf " (%a)" CilType.Location.pretty (Messages.Location.to_cil group_loc) - in - BatPrintf.fprintf f "%a\n" n group_loc_text (BatList.print ~first:"" ~last:"" ~sep:"" one_text) e - in - let one_w f x = BatPrintf.fprintf f "\n%a" one_w x in - List.iter (one_w f) !Messages.Table.messages_list - - let output table gtable gtfxml (file: file) = - let out = Messages.get_out result_name !Messages.out in - match get_string "result" with - | "pretty" -> ignore (fprintf out "%a\n" pretty (Lazy.force table)) - | "fast_xml" -> - let module SH = BatHashtbl.Make (Basetype.RawStrings) in - let file2funs = SH.create 100 in - let funs2node = SH.create 100 in - iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table); - iterGlobals file (function - | GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname - | _ -> () - ); - let p_node f n = BatPrintf.fprintf f "%s" (Node.show_id n) in - let p_nodes f xs = - List.iter (BatPrintf.fprintf f "\n" p_node) xs - in - let p_funs f xs = - let one_fun n = - BatPrintf.fprintf f "\n%a\n" n p_nodes (SH.find_all funs2node n) - in - List.iter one_fun xs - in - let write_file f fn = - Messages.xml_file_name := fn; - BatPrintf.printf "Writing xml to temp. file: %s\n%!" fn; - BatPrintf.fprintf f ""; - BatPrintf.fprintf f "%s" GobSys.command_line; - BatPrintf.fprintf f ""; - let timing_ppf = BatFormat.formatter_of_out_channel f in - Timing.Default.print timing_ppf; - Format.pp_print_flush timing_ppf (); - BatPrintf.fprintf f ""; - BatPrintf.fprintf f "\n"; - BatEnum.iter (fun b -> BatPrintf.fprintf f "\n%a\n" (Filename.basename b) b p_funs (SH.find_all file2funs b)) (BatEnum.uniq @@ SH.keys file2funs); - BatPrintf.fprintf f "%a" printXml (Lazy.force table); - gtfxml f gtable; - printXmlWarning f (); - BatPrintf.fprintf f "\n"; - BatPrintf.fprintf f "%!" - in - if get_bool "g2html" then - BatFile.with_temporary_out ~mode:[`create;`text;`delete_on_exit] write_file - else - let f = BatIO.output_channel out in - write_file f (get_string "outfile") - | "json" -> - let open BatPrintf in - let module SH = BatHashtbl.Make (Basetype.RawStrings) in - let file2funs = SH.create 100 in - let funs2node = SH.create 100 in - iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table); - iterGlobals file (function - | GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname - | _ -> () - ); - let p_enum p f xs = BatEnum.print ~first:"[\n " ~last:"\n]" ~sep:",\n " p f xs in - let p_list p f xs = BatList.print ~first:"[\n " ~last:"\n]" ~sep:",\n " p f xs in - (*let p_kv f (k,p,v) = fprintf f "\"%s\": %a" k p v in*) - (*let p_obj f xs = BatList.print ~first:"{\n " ~last:"\n}" ~sep:",\n " p_kv xs in*) - let p_node f n = BatPrintf.fprintf f "\"%s\"" (Node.show_id n) in - let p_fun f x = fprintf f "{\n \"name\": \"%s\",\n \"nodes\": %a\n}" x (p_list p_node) (SH.find_all funs2node x) in - (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*) - let p_file f x = fprintf f "{\n \"name\": \"%s\",\n \"path\": \"%s\",\n \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in - let write_file f fn = - printf "Writing json to temp. file: %s\n%!" fn; - fprintf f "{\n \"parameters\": \"%s\",\n " GobSys.command_line; - fprintf f "\"files\": %a,\n " (p_enum p_file) (SH.keys file2funs); - fprintf f "\"results\": [\n %a\n]\n" printJson (Lazy.force table); - (*gtfxml f gtable;*) - (*printXmlWarning f ();*) - fprintf f "}\n"; - in - if get_bool "g2html" then - BatFile.with_temporary_out ~mode:[`create;`text;`delete_on_exit] write_file - else - let f = BatIO.output_channel out in - write_file f (get_string "outfile") - | "sarif" -> - let open BatPrintf in - printf "Writing Sarif to file: %s\n%!" (get_string "outfile"); - Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); - | "json-messages" -> - let json = `Assoc [ - ("files", Preprocessor.dependencies_to_yojson ()); - ("messages", Messages.Table.to_yojson ()); - ] - in - Yojson.Safe.to_channel ~std:true out json - | "none" -> () - | s -> failwith @@ "Unsupported value for option `result`: "^s -end - - (* Experiment to reduce the number of arguments on transfer functions and allow sub-analyses. The list sub contains the current local states of analyses in the same order as written in the dependencies list (in MCP). @@ -495,119 +300,6 @@ type increment_data = { restarting: VarQuery.t list; } -(** Abstract incremental change to constraint system. - @param 'v constrain system variable type *) -type 'v sys_change_info = { - obsolete: 'v list; (** Variables to destabilize. *) - delete: 'v list; (** Variables to delete. *) - reluctant: 'v list; (** Variables to solve reluctantly. *) - restart: 'v list; (** Variables to restart. *) -} - -(** A side-effecting system. *) -module type MonSystem = -sig - type v (* variables *) - type d (* values *) - type 'a m (* basically a monad carrier *) - - (** Variables must be hashable, comparable, etc. *) - module Var : VarType with type t = v - - (** Values must form a lattice. *) - module Dom : Lattice.S with type t = d - - (** The system in functional form. *) - val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m - - val sys_change: (v -> d) -> v sys_change_info - (** Compute incremental constraint system change from old solution. *) -end - -(** Any system of side-effecting equations over lattices. *) -module type EqConstrSys = MonSystem with type 'a m := 'a option - -(** A side-effecting system with globals. *) -module type GlobConstrSys = -sig - module LVar : VarType - module GVar : VarType - - module D : Lattice.S - module G : Lattice.S - val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option - val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit - val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info -end - -(** A solver is something that can translate a system into a solution (hash-table). - Incremental solver has data to be marshaled. *) -module type GenericEqIncrSolverBase = - functor (S:EqConstrSys) -> - functor (H:Hashtbl.S with type key=S.v) -> - sig - type marshal - - val copy_marshal: marshal -> marshal - val relift_marshal: marshal -> marshal - - (** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs], - reached from starting values [xs]. - As a second component the solver returns data structures for incremental serialization. *) - val solve : (S.v*S.d) list -> S.v list -> marshal option -> S.d H.t * marshal - end - -(** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *) -module type IncrSolverArg = -sig - val should_prune: bool - val should_verify: bool - val should_warn: bool - val should_save_run: bool -end - -(** An incremental solver takes the argument about postsolving. *) -module type GenericEqIncrSolver = - functor (Arg: IncrSolverArg) -> - GenericEqIncrSolverBase - -(** A solver is something that can translate a system into a solution (hash-table) *) -module type GenericEqSolver = - functor (S:EqConstrSys) -> - functor (H:Hashtbl.S with type key=S.v) -> - sig - (** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs], - reached from starting values [xs]. *) - val solve : (S.v*S.d) list -> S.v list -> S.d H.t - end - -(** A solver is something that can translate a system into a solution (hash-table) *) -module type GenericGlobSolver = - functor (S:GlobConstrSys) -> - functor (LH:Hashtbl.S with type key=S.LVar.t) -> - functor (GH:Hashtbl.S with type key=S.GVar.t) -> - sig - type marshal - - val copy_marshal: marshal -> marshal - val relift_marshal: marshal -> marshal - - (** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs], - reached from starting values [xs]. - As a second component the solver returns data structures for incremental serialization. *) - val solve : (S.LVar.t*S.D.t) list -> (S.GVar.t*S.G.t) list -> S.LVar.t list -> marshal option -> (S.D.t LH.t * S.G.t GH.t) * marshal - end - -module ResultType2 (S:Spec) = -struct - open S - include Printable.Prod3 (C) (D) (CilType.Fundec) - let show (es,x,f:t) = D.show x - let pretty () (_,x,_) = D.pretty () x - let printXml f (c,d,fd) = - BatPrintf.fprintf f "\n%a\n%a" C.printXml c D.printXml d -end - module StdV = struct let is_write_only _ = false @@ -728,7 +420,7 @@ end module type SpecSys = sig module Spec: Spec - module EQSys: GlobConstrSys with module LVar = VarF (Spec.C) + module EQSys: ConstrSys.GlobConstrSys with module LVar = VarF (Spec.C) and module GVar = GVarF (Spec.V) and module D = Spec.D and module G = GVarG (Spec.G) (Spec.C) diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml new file mode 100644 index 0000000000..09ece868c1 --- /dev/null +++ b/src/framework/analysisResult.ml @@ -0,0 +1,191 @@ +(** Analysis result output. *) + +open GoblintCil +open Pretty +open GobConfig + +module ResultNode: Printable.S with type t = MyCFG.node = +struct + include Printable.Std + + include Node + + let name () = "resultnode" + + let show a = + (* Not using Node.location here to have updated locations in incremental analysis. + See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) + let x = UpdateCil.getLoc a in + let f = Node.find_fundec a in + CilType.Location.show x ^ "(" ^ f.svar.vname ^ ")" + + include Printable.SimpleShow ( + struct + type nonrec t = t + let show = show + end + ) +end + +module type ResultConf = +sig + val result_name: string +end + +module Result (Range: Printable.S) (C: ResultConf) = +struct + include BatHashtbl.Make (ResultNode) + type nonrec t = Range.t t (* specialize polymorphic type for Range values *) + + let pretty () mapping = + let f key st dok = + dok ++ dprintf "%a ->@? @[%a@]\n" ResultNode.pretty key Range.pretty st + in + let content () = fold f mapping nil in + let defline () = dprintf "OTHERS -> Not available\n" in + dprintf "@[Mapping {\n @[%t%t@]}@]" content defline + + include C + + let printXml f xs = + let print_one n v = + (* Not using Node.location here to have updated locations in incremental analysis. + See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) + let loc = UpdateCil.getLoc n in + BatPrintf.fprintf f "\n" (Node.show_id n) loc.file loc.line loc.byte loc.column; + BatPrintf.fprintf f "%a\n" Range.printXml v + in + iter print_one xs + + let printJson f xs = + let print_one n v = + (* Not using Node.location here to have updated locations in incremental analysis. + See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) + let loc = UpdateCil.getLoc n in + BatPrintf.fprintf f "{\n\"id\": \"%s\", \"file\": \"%s\", \"line\": \"%d\", \"byte\": \"%d\", \"column\": \"%d\", \"states\": %s\n},\n" (Node.show_id n) loc.file loc.line loc.byte loc.column (Yojson.Safe.to_string (Range.to_yojson v)) + in + iter print_one xs + + let printXmlWarning f () = + let one_text f Messages.Piece.{loc; text = m; _} = + match loc with + | Some loc -> + let l = Messages.Location.to_cil loc in + BatPrintf.fprintf f "\n%s" l.file l.line l.column (XmlUtil.escape m) + | None -> + () (* TODO: not outputting warning without location *) + in + let one_w f (m: Messages.Message.t) = match m.multipiece with + | Single piece -> one_text f piece + | Group {group_text = n; pieces = e; group_loc} -> + let group_loc_text = match group_loc with + | None -> "" + | Some group_loc -> GobPretty.sprintf " (%a)" CilType.Location.pretty (Messages.Location.to_cil group_loc) + in + BatPrintf.fprintf f "%a\n" n group_loc_text (BatList.print ~first:"" ~last:"" ~sep:"" one_text) e + in + let one_w f x = BatPrintf.fprintf f "\n%a" one_w x in + List.iter (one_w f) !Messages.Table.messages_list + + let output table gtable gtfxml (file: file) = + let out = Messages.get_out result_name !Messages.out in + match get_string "result" with + | "pretty" -> ignore (fprintf out "%a\n" pretty (Lazy.force table)) + | "fast_xml" -> + let module SH = BatHashtbl.Make (Basetype.RawStrings) in + let file2funs = SH.create 100 in + let funs2node = SH.create 100 in + iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table); + iterGlobals file (function + | GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname + | _ -> () + ); + let p_node f n = BatPrintf.fprintf f "%s" (Node.show_id n) in + let p_nodes f xs = + List.iter (BatPrintf.fprintf f "\n" p_node) xs + in + let p_funs f xs = + let one_fun n = + BatPrintf.fprintf f "\n%a\n" n p_nodes (SH.find_all funs2node n) + in + List.iter one_fun xs + in + let write_file f fn = + Messages.xml_file_name := fn; + BatPrintf.printf "Writing xml to temp. file: %s\n%!" fn; + BatPrintf.fprintf f ""; + BatPrintf.fprintf f "%s" GobSys.command_line; + BatPrintf.fprintf f ""; + let timing_ppf = BatFormat.formatter_of_out_channel f in + Timing.Default.print timing_ppf; + Format.pp_print_flush timing_ppf (); + BatPrintf.fprintf f ""; + BatPrintf.fprintf f "\n"; + BatEnum.iter (fun b -> BatPrintf.fprintf f "\n%a\n" (Filename.basename b) b p_funs (SH.find_all file2funs b)) (BatEnum.uniq @@ SH.keys file2funs); + BatPrintf.fprintf f "%a" printXml (Lazy.force table); + gtfxml f gtable; + printXmlWarning f (); + BatPrintf.fprintf f "\n"; + BatPrintf.fprintf f "%!" + in + if get_bool "g2html" then + BatFile.with_temporary_out ~mode:[`create;`text;`delete_on_exit] write_file + else + let f = BatIO.output_channel out in + write_file f (get_string "outfile") + | "json" -> + let open BatPrintf in + let module SH = BatHashtbl.Make (Basetype.RawStrings) in + let file2funs = SH.create 100 in + let funs2node = SH.create 100 in + iter (fun n _ -> SH.add funs2node (Node.find_fundec n).svar.vname n) (Lazy.force table); + iterGlobals file (function + | GFun (fd,loc) -> SH.add file2funs loc.file fd.svar.vname + | _ -> () + ); + let p_enum p f xs = BatEnum.print ~first:"[\n " ~last:"\n]" ~sep:",\n " p f xs in + let p_list p f xs = BatList.print ~first:"[\n " ~last:"\n]" ~sep:",\n " p f xs in + (*let p_kv f (k,p,v) = fprintf f "\"%s\": %a" k p v in*) + (*let p_obj f xs = BatList.print ~first:"{\n " ~last:"\n}" ~sep:",\n " p_kv xs in*) + let p_node f n = BatPrintf.fprintf f "\"%s\"" (Node.show_id n) in + let p_fun f x = fprintf f "{\n \"name\": \"%s\",\n \"nodes\": %a\n}" x (p_list p_node) (SH.find_all funs2node x) in + (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*) + let p_file f x = fprintf f "{\n \"name\": \"%s\",\n \"path\": \"%s\",\n \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in + let write_file f fn = + printf "Writing json to temp. file: %s\n%!" fn; + fprintf f "{\n \"parameters\": \"%s\",\n " GobSys.command_line; + fprintf f "\"files\": %a,\n " (p_enum p_file) (SH.keys file2funs); + fprintf f "\"results\": [\n %a\n]\n" printJson (Lazy.force table); + (*gtfxml f gtable;*) + (*printXmlWarning f ();*) + fprintf f "}\n"; + in + if get_bool "g2html" then + BatFile.with_temporary_out ~mode:[`create;`text;`delete_on_exit] write_file + else + let f = BatIO.output_channel out in + write_file f (get_string "outfile") + | "sarif" -> + let open BatPrintf in + printf "Writing Sarif to file: %s\n%!" (get_string "outfile"); + Yojson.Safe.to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); + | "json-messages" -> + let json = `Assoc [ + ("files", Preprocessor.dependencies_to_yojson ()); + ("messages", Messages.Table.to_yojson ()); + ] + in + Yojson.Safe.to_channel ~std:true out json + | "none" -> () + | s -> failwith @@ "Unsupported value for option `result`: "^s +end + +module ResultType2 (S: Analyses.Spec) = +struct + open S + include Printable.Prod3 (C) (D) (CilType.Fundec) + let show (es,x,f:t) = D.show x + let pretty () (_,x,_) = D.pretty () x + let printXml f (c,d,fd) = + BatPrintf.fprintf f "\n%a\n%a" C.printXml c D.printXml d +end diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 8039a867d8..f5c024c24f 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -5,6 +5,7 @@ open Batteries open GoblintCil open MyCFG open Analyses +open ConstrSys open GobConfig module M = Messages @@ -501,38 +502,6 @@ sig val increment: increment_data option end -(** Combined variables so that we can also use the more common [EqConstrSys] - that uses only one kind of a variable. *) -module Var2 (LV:VarType) (GV:VarType) - : VarType - with type t = [ `L of LV.t | `G of GV.t ] -= -struct - type t = [ `L of LV.t | `G of GV.t ] [@@deriving eq, ord, hash] - let relift = function - | `L x -> `L (LV.relift x) - | `G x -> `G (GV.relift x) - - let pretty_trace () = function - | `L a -> Pretty.dprintf "L:%a" LV.pretty_trace a - | `G a -> Pretty.dprintf "G:%a" GV.pretty_trace a - - let printXml f = function - | `L a -> LV.printXml f a - | `G a -> GV.printXml f a - - let var_id = function - | `L a -> LV.var_id a - | `G a -> GV.var_id a - - let node = function - | `L a -> LV.node a - | `G a -> GV.node a - - let is_write_only = function - | `L a -> LV.is_write_only a - | `G a -> GV.is_write_only a -end (** The main point of this file---generating a [GlobConstrSys] from a [Spec]. *) module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment) @@ -1053,137 +1022,6 @@ struct {obsolete; delete; reluctant; restart} end -(** Convert a non-incremental solver into an "incremental" solver. - It will solve from scratch, perform standard postsolving and have no marshal data. *) -module EqIncrSolverFromEqSolver (Sol: GenericEqSolver): GenericEqIncrSolver = - functor (Arg: IncrSolverArg) (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) -> - struct - module Sol = Sol (S) (VH) - module Post = PostSolver.MakeList (PostSolver.ListArgFromStdArg (S) (VH) (Arg)) - - type marshal = unit - let copy_marshal () = () - let relift_marshal () = () - - let solve xs vs _ = - let vh = Sol.solve xs vs in - Post.post xs vs vh; - (vh, ()) - end - - -(** Translate a [GlobConstrSys] into a [EqConstrSys] *) -module EqConstrSysFromGlobConstrSys (S:GlobConstrSys) - : EqConstrSys with type v = Var2(S.LVar)(S.GVar).t - and type d = Lattice.Lift2(S.G)(S.D).t - and module Var = Var2(S.LVar)(S.GVar) - and module Dom = Lattice.Lift2(S.G)(S.D) -= -struct - module Var = Var2(S.LVar)(S.GVar) - module Dom = - struct - include Lattice.Lift2 (S.G) (S.D) - let printXml f = function - | `Lifted1 a -> S.G.printXml f a - | `Lifted2 a -> S.D.printXml f a - | (`Bot | `Top) as x -> printXml f x - end - type v = Var.t - type d = Dom.t - - let getG = function - | `Lifted1 x -> x - | `Bot -> S.G.bot () - | `Top -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has top value" - | `Lifted2 _ -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has local value" - - let getL = function - | `Lifted2 x -> x - | `Bot -> S.D.bot () - | `Top -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has top value" - | `Lifted1 _ -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has global value" - - let l, g = (fun x -> `L x), (fun x -> `G x) - let lD, gD = (fun x -> `Lifted2 x), (fun x -> `Lifted1 x) - - let conv f get set = - f (getL % get % l) (fun x v -> set (l x) (lD v)) - (getG % get % g) (fun x v -> set (g x) (gD v)) - |> lD - - let system = function - | `G _ -> None - | `L x -> Option.map conv (S.system x) - - let sys_change get = - S.sys_change (getL % get % l) (getG % get % g) -end - -(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *) -module GlobConstrSolFromEqConstrSolBase (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) (VH: Hashtbl.S with type key = Var2 (S.LVar) (S.GVar).t) = -struct - let split_solution hm = - let l' = LH.create 113 in - let g' = GH.create 113 in - let split_vars x d = match x with - | `L x -> - begin match d with - | `Lifted2 d -> LH.replace l' x d - (* | `Bot -> () *) - (* Since Verify2 is broken and only checks existing keys, add it with local bottom value. - This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *) - | `Bot -> LH.replace l' x (S.D.bot ()) - | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value" - | `Lifted1 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value" - end - | `G x -> - begin match d with - | `Lifted1 d -> GH.replace g' x d - | `Bot -> () - | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has top value" - | `Lifted2 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has local value" - end - in - VH.iter split_vars hm; - (l', g') -end - -(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution. *) -module GlobConstrSolFromEqConstrSol (S: GlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) = -struct - module S2 = EqConstrSysFromGlobConstrSys (S) - module VH = Hashtbl.Make (S2.Var) - - include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) -end - -(** Transforms a [GenericEqIncrSolver] into a [GenericGlobSolver]. *) -module GlobSolverFromEqSolver (Sol:GenericEqIncrSolverBase) - = functor (S:GlobConstrSys) -> - functor (LH:Hashtbl.S with type key=S.LVar.t) -> - functor (GH:Hashtbl.S with type key=S.GVar.t) -> - struct - module EqSys = EqConstrSysFromGlobConstrSys (S) - - module VH : Hashtbl.S with type key=EqSys.v = Hashtbl.Make(EqSys.Var) - module Sol' = Sol (EqSys) (VH) - - module Splitter = GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) (* reuse EqSys and VH *) - - type marshal = Sol'.marshal - - let copy_marshal = Sol'.copy_marshal - let relift_marshal = Sol'.relift_marshal - - let solve ls gs l old_data = - let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls - @ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in - let sv = List.map (fun x -> `L x) l in - let hm, solver_data = Sol'.solve vs sv old_data in - Splitter.split_solution hm, solver_data - end - (** Add path sensitivity to a analysis *) module PathSensitive2 (Spec:Spec) @@ -2056,29 +1894,3 @@ struct ignore (Pretty.printf "Nodes comparison summary: %t\n" (fun () -> msg)); print_newline (); end - -(** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *) -module CurrentVarEqConstrSys (S: EqConstrSys) = -struct - let current_var = ref None - - module S = - struct - include S - - let system x = - match S.system x with - | None -> None - | Some f -> - let f' get set = - let old_current_var = !current_var in - current_var := Some x; - Fun.protect ~finally:(fun () -> - current_var := old_current_var - ) (fun () -> - f get set - ) - in - Some f' - end -end diff --git a/src/framework/control.ml b/src/framework/control.ml index 00a6034e27..391c766feb 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -6,6 +6,7 @@ open Batteries open GoblintCil open MyCFG open Analyses +open ConstrSys open GobConfig open Constraints @@ -84,16 +85,16 @@ 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) (* Triple of the function, context, and the local value. *) - module RT = Analyses.ResultType2 (Spec) + module RT = AnalysisResult.ResultType2 (Spec) (* Set of triples [RT] *) module LT = SetDomain.HeadlessSet (RT) (* Analysis result structure---a hashtable from program points to [LT] *) - module Result = Analyses.Result (LT) (struct let result_name = "analysis" end) + module Result = AnalysisResult.Result (LT) (struct let result_name = "analysis" end) module Query = ResultQuery.Query (SpecSys) @@ -475,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 ( @@ -581,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 e402cc33fe..1bc70f3f52 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -21,6 +21,7 @@ module CfgTools = CfgTools A dynamic composition of analyses is combined with CFGs to produce a constraint system. *) module Analyses = Analyses +module ConstrSys = ConstrSys module Constraints = Constraints module AnalysisState = AnalysisState module AnalysisStateUtil = AnalysisStateUtil @@ -45,6 +46,7 @@ module Events = Events The following modules help query the constraint system solution using semantic information. *) +module AnalysisResult = AnalysisResult module ResultQuery = ResultQuery module VarQuery = VarQuery @@ -286,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 76b9d230dd..0f6b1c3e69 100644 --- a/src/index.mld +++ b/src/index.mld @@ -16,6 +16,15 @@ This {{!page-common}unwrapped library} contains various common modules extracted {2 Library goblint.domain} This {{!page-domain}unwrapped library} contains various domain modules extracted from {!Goblint_lib}. +{2 Library goblint.cdomain.value} +This {{!page-cdomain_value}unwrapped library} contains various value domain modules extracted from {!Goblint_lib}. + +{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/solver/dune b/src/solver/dune new file mode 100644 index 0000000000..bd6d7a4d0a --- /dev/null +++ b/src/solver/dune @@ -0,0 +1,23 @@ +(include_subdirs no) + +(library + (name goblint_solver) + (public_name goblint.solver) + (libraries + batteries.unthreaded + goblint_std + goblint_common + goblint_config + 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/effectWConEq.ml b/src/solver/effectWConEq.ml similarity index 95% rename from src/solvers/effectWConEq.ml rename to src/solver/effectWConEq.ml index c6dcf8f0e9..3cca6361b4 100644 --- a/src/solvers/effectWConEq.ml +++ b/src/solver/effectWConEq.ml @@ -1,8 +1,7 @@ (** ([effectWConEq]). *) open Batteries -open Analyses -open Constraints +open ConstrSys module Make = functor (S:EqConstrSys) -> @@ -88,4 +87,4 @@ module Make = end let _ = - Selector.add_solver ("effectWConEq", (module EqIncrSolverFromEqSolver (Make))); + Selector.add_solver ("effectWConEq", (module PostSolver.EqIncrSolverFromEqSolver (Make))); diff --git a/src/solvers/generic.ml b/src/solver/generic.ml similarity index 99% rename from src/solvers/generic.ml rename to src/solver/generic.ml index 2569341dd1..636aed8831 100644 --- a/src/solvers/generic.ml +++ b/src/solver/generic.ml @@ -2,7 +2,7 @@ open Batteries open GobConfig -open Analyses +open ConstrSys module LoadRunSolver: GenericEqSolver = functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) -> @@ -30,7 +30,7 @@ module LoadRunSolver: GenericEqSolver = end module LoadRunIncrSolver: GenericEqIncrSolver = - Constraints.EqIncrSolverFromEqSolver (LoadRunSolver) + PostSolver.EqIncrSolverFromEqSolver (LoadRunSolver) module SolverStats (S:EqConstrSys) (HM:Hashtbl.S with type key = S.v) = struct diff --git a/src/solver/goblint_solver.ml b/src/solver/goblint_solver.ml new file mode 100644 index 0000000000..0a264d7dea --- /dev/null +++ b/src/solver/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 diff --git a/src/solvers/localFixpoint.ml b/src/solver/localFixpoint.ml similarity index 100% rename from src/solvers/localFixpoint.ml rename to src/solver/localFixpoint.ml diff --git a/src/solvers/postSolver.ml b/src/solver/postSolver.ml similarity index 93% rename from src/solvers/postSolver.ml rename to src/solver/postSolver.ml index e01560c752..7f4f9c2b1f 100644 --- a/src/solvers/postSolver.ml +++ b/src/solver/postSolver.ml @@ -1,9 +1,10 @@ (** Extra constraint system evaluation pass for warning generation, verification, pruning, etc. *) open Batteries -open Analyses +open ConstrSys open GobConfig module Pretty = GoblintCil.Pretty +module M = Messages (** Postsolver with hooks. *) module type S = @@ -315,3 +316,22 @@ struct |> List.map snd |> List.map (fun (module F: F) -> (module F (S) (VH): M)) end + +(* Here to avoid module cycle between ConstrSys and PostSolver. *) +(** Convert a non-incremental solver into an "incremental" solver. + It will solve from scratch, perform standard postsolving and have no marshal data. *) +module EqIncrSolverFromEqSolver (Sol: GenericEqSolver): GenericEqIncrSolver = + functor (Arg: IncrSolverArg) (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) -> + struct + module Sol = Sol (S) (VH) + module Post = MakeList (ListArgFromStdArg (S) (VH) (Arg)) + + type marshal = unit + let copy_marshal () = () + let relift_marshal () = () + + let solve xs vs _ = + let vh = Sol.solve xs vs in + Post.post xs vs vh; + (vh, ()) + end diff --git a/src/solvers/sLR.ml b/src/solver/sLR.ml similarity index 91% rename from src/solvers/sLR.ml rename to src/solver/sLR.ml index 4904731b61..d05d87c4f3 100644 --- a/src/solvers/sLR.ml +++ b/src/solver/sLR.ml @@ -3,8 +3,7 @@ @see Apinis, K. Frameworks for analyzing multi-threaded C. *) open Batteries -open Analyses -open Constraints +open ConstrSys open Messages let narrow f = if GobConfig.get_bool "exp.no-narrow" then (fun a b -> a) else f @@ -522,29 +521,29 @@ let _ = let module W1 = JustWiden (struct let ver = 1 end) in let module W2 = JustWiden (struct let ver = 2 end) in let module W3 = JustWiden (struct let ver = 3 end) in - Selector.add_solver ("widen1", (module EqIncrSolverFromEqSolver (W1))); - Selector.add_solver ("widen2", (module EqIncrSolverFromEqSolver (W2))); - Selector.add_solver ("widen3", (module EqIncrSolverFromEqSolver (W3))); + Selector.add_solver ("widen1", (module PostSolver.EqIncrSolverFromEqSolver (W1))); + Selector.add_solver ("widen2", (module PostSolver.EqIncrSolverFromEqSolver (W2))); + Selector.add_solver ("widen3", (module PostSolver.EqIncrSolverFromEqSolver (W3))); let module S2 = TwoPhased (struct let ver = 1 end) in - Selector.add_solver ("two", (module EqIncrSolverFromEqSolver (S2))); + Selector.add_solver ("two", (module PostSolver.EqIncrSolverFromEqSolver (S2))); let module S1 = Make (struct let ver = 1 end) in - Selector.add_solver ("new", (module EqIncrSolverFromEqSolver (S1))); - Selector.add_solver ("slr+", (module EqIncrSolverFromEqSolver (S1))) + Selector.add_solver ("new", (module PostSolver.EqIncrSolverFromEqSolver (S1))); + Selector.add_solver ("slr+", (module PostSolver.EqIncrSolverFromEqSolver (S1))) let _ = let module S1 = Make (struct let ver = 1 end) in let module S2 = Make (struct let ver = 2 end) in let module S3 = SLR3 in let module S4 = Make (struct let ver = 4 end) in - Selector.add_solver ("slr1", (module EqIncrSolverFromEqSolver (S1))); (* W&N at every program point *) - Selector.add_solver ("slr2", (module EqIncrSolverFromEqSolver (S2))); (* W&N dynamic at certain points, growing number of W-points *) - Selector.add_solver ("slr3", (module EqIncrSolverFromEqSolver (S3))); (* same as S2 but number of W-points may also shrink *) - Selector.add_solver ("slr4", (module EqIncrSolverFromEqSolver (S4))); (* restarting: set influenced variables to bot and start up-iteration instead of narrowing *) + Selector.add_solver ("slr1", (module PostSolver.EqIncrSolverFromEqSolver (S1))); (* W&N at every program point *) + Selector.add_solver ("slr2", (module PostSolver.EqIncrSolverFromEqSolver (S2))); (* W&N dynamic at certain points, growing number of W-points *) + Selector.add_solver ("slr3", (module PostSolver.EqIncrSolverFromEqSolver (S3))); (* same as S2 but number of W-points may also shrink *) + Selector.add_solver ("slr4", (module PostSolver.EqIncrSolverFromEqSolver (S4))); (* restarting: set influenced variables to bot and start up-iteration instead of narrowing *) let module S1p = PrintInfluence (Make (struct let ver = 1 end)) in let module S2p = PrintInfluence (Make (struct let ver = 2 end)) in let module S3p = PrintInfluence (Make (struct let ver = 3 end)) in let module S4p = PrintInfluence (Make (struct let ver = 4 end)) in - Selector.add_solver ("slr1p", (module EqIncrSolverFromEqSolver (S1p))); (* same as S1-4 above but with side-effects *) - Selector.add_solver ("slr2p", (module EqIncrSolverFromEqSolver (S2p))); - Selector.add_solver ("slr3p", (module EqIncrSolverFromEqSolver (S3p))); - Selector.add_solver ("slr4p", (module EqIncrSolverFromEqSolver (S4p))); + Selector.add_solver ("slr1p", (module PostSolver.EqIncrSolverFromEqSolver (S1p))); (* same as S1-4 above but with side-effects *) + Selector.add_solver ("slr2p", (module PostSolver.EqIncrSolverFromEqSolver (S2p))); + Selector.add_solver ("slr3p", (module PostSolver.EqIncrSolverFromEqSolver (S3p))); + Selector.add_solver ("slr4p", (module PostSolver.EqIncrSolverFromEqSolver (S4p))); diff --git a/src/solvers/sLRphased.ml b/src/solver/sLRphased.ml similarity index 98% rename from src/solvers/sLRphased.ml rename to src/solver/sLRphased.ml index c120a7bc6c..17571f0138 100644 --- a/src/solvers/sLRphased.ml +++ b/src/solver/sLRphased.ml @@ -1,8 +1,7 @@ (** Two-phased terminating SLR3 solver ([slr3tp]). *) open Batteries -open Analyses -open Constraints +open ConstrSys open Messages open SLR @@ -205,4 +204,4 @@ module Make = end let _ = - Selector.add_solver ("slr3tp", (module EqIncrSolverFromEqSolver (Make))); (* two-phased slr3t *) + Selector.add_solver ("slr3tp", (module PostSolver.EqIncrSolverFromEqSolver (Make))); (* two-phased slr3t *) diff --git a/src/solvers/sLRterm.ml b/src/solver/sLRterm.ml similarity index 97% rename from src/solvers/sLRterm.ml rename to src/solver/sLRterm.ml index eb11447d11..8ec34c7dc2 100644 --- a/src/solvers/sLRterm.ml +++ b/src/solver/sLRterm.ml @@ -2,8 +2,7 @@ Simpler version of {!SLRphased} without phases. *) open Batteries -open Analyses -open Constraints +open ConstrSys open Messages open SLR @@ -224,4 +223,4 @@ module SLR3term = end let _ = - Selector.add_solver ("slr3t", (module EqIncrSolverFromEqSolver (SLR3term))); (* same as S2 but number of W-points may also shrink + terminating? *) + Selector.add_solver ("slr3t", (module PostSolver.EqIncrSolverFromEqSolver (SLR3term))); (* same as S2 but number of W-points may also shrink + terminating? *) diff --git a/src/solvers/selector.ml b/src/solver/selector.ml similarity index 99% rename from src/solvers/selector.ml rename to src/solver/selector.ml index 664cbe0513..854b8e1036 100644 --- a/src/solvers/selector.ml +++ b/src/solver/selector.ml @@ -1,7 +1,7 @@ (** Solver, which delegates at runtime to the configured solver. *) open Batteries -open Analyses +open ConstrSys open GobConfig (* Registered solvers. *) diff --git a/src/solvers/solverBox.ml b/src/solver/solverBox.ml similarity index 100% rename from src/solvers/solverBox.ml rename to src/solver/solverBox.ml diff --git a/src/solvers/solverStats.ml b/src/solver/solverStats.ml similarity index 100% rename from src/solvers/solverStats.ml rename to src/solver/solverStats.ml diff --git a/src/solvers/td3.ml b/src/solver/td3.ml similarity index 99% rename from src/solvers/td3.ml rename to src/solver/td3.ml index 07edc632c7..54b7520cd6 100644 --- a/src/solvers/td3.ml +++ b/src/solver/td3.ml @@ -15,9 +15,11 @@ *) open Batteries -open Analyses +open ConstrSys open Messages +module M = Messages + module type Hooks = sig module S: EqConstrSys @@ -192,7 +194,7 @@ module Base = type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) - module CurrentVarS = Constraints.CurrentVarEqConstrSys (S) + module CurrentVarS = ConstrSys.CurrentVarEqConstrSys (S) module S = CurrentVarS.S let solve st vs marshal = diff --git a/src/solvers/topDown.ml b/src/solver/topDown.ml similarity index 98% rename from src/solvers/topDown.ml rename to src/solver/topDown.ml index c6b20d28db..f7da560057 100644 --- a/src/solvers/topDown.ml +++ b/src/solver/topDown.ml @@ -2,8 +2,7 @@ Simpler version of {!Td3} without terminating, space-efficiency and incremental. *) open Batteries -open Analyses -open Constraints +open ConstrSys open Messages module WP = @@ -155,4 +154,4 @@ module WP = end let _ = - Selector.add_solver ("topdown", (module EqIncrSolverFromEqSolver (WP))); + Selector.add_solver ("topdown", (module PostSolver.EqIncrSolverFromEqSolver (WP))); diff --git a/src/solvers/topDown_deprecated.ml b/src/solver/topDown_deprecated.ml similarity index 97% rename from src/solvers/topDown_deprecated.ml rename to src/solver/topDown_deprecated.ml index 1f51244458..4e9799cf78 100644 --- a/src/solvers/topDown_deprecated.ml +++ b/src/solver/topDown_deprecated.ml @@ -1,8 +1,7 @@ (** Deprecated top-down solver ([topdown_deprecated]). *) open Batteries -open Analyses -open Constraints +open ConstrSys open Messages exception SolverCannotDoGlobals @@ -164,4 +163,4 @@ module TD3 = end let _ = - Selector.add_solver ("topdown_deprecated", (module EqIncrSolverFromEqSolver (TD3))); + Selector.add_solver ("topdown_deprecated", (module PostSolver.EqIncrSolverFromEqSolver (TD3))); diff --git a/src/solvers/topDown_space_cache_term.ml b/src/solver/topDown_space_cache_term.ml similarity index 98% rename from src/solvers/topDown_space_cache_term.ml rename to src/solver/topDown_space_cache_term.ml index a78d90559d..f6c256517c 100644 --- a/src/solvers/topDown_space_cache_term.ml +++ b/src/solver/topDown_space_cache_term.ml @@ -2,8 +2,7 @@ Simpler version of {!Td3} without incremental. *) open Batteries -open Analyses -open Constraints +open ConstrSys open Messages module WP = @@ -197,4 +196,4 @@ module WP = end let _ = - Selector.add_solver ("topdown_space_cache_term", (module EqIncrSolverFromEqSolver (WP))); + Selector.add_solver ("topdown_space_cache_term", (module PostSolver.EqIncrSolverFromEqSolver (WP))); diff --git a/src/solvers/topDown_term.ml b/src/solver/topDown_term.ml similarity index 97% rename from src/solvers/topDown_term.ml rename to src/solver/topDown_term.ml index ec07995586..d15493b5a1 100644 --- a/src/solvers/topDown_term.ml +++ b/src/solver/topDown_term.ml @@ -2,8 +2,7 @@ Simpler version of {!Td3} without space-efficiency and incremental. *) open Batteries -open Analyses -open Constraints +open ConstrSys open Messages module WP = @@ -134,4 +133,4 @@ module WP = end let _ = - Selector.add_solver ("topdown_term", (module EqIncrSolverFromEqSolver (WP))); + Selector.add_solver ("topdown_term", (module PostSolver.EqIncrSolverFromEqSolver (WP))); diff --git a/src/solvers/worklist.ml b/src/solver/worklist.ml similarity index 93% rename from src/solvers/worklist.ml rename to src/solver/worklist.ml index b525764c74..b1a5d7e834 100644 --- a/src/solvers/worklist.ml +++ b/src/solver/worklist.ml @@ -1,8 +1,7 @@ (** Worklist solver ([WL]). *) open Batteries -open Analyses -open Constraints +open ConstrSys module Make = functor (S:EqConstrSys) -> @@ -63,4 +62,4 @@ module Make = let _ = - Selector.add_solver ("WL", (module EqIncrSolverFromEqSolver (Make))); + Selector.add_solver ("WL", (module PostSolver.EqIncrSolverFromEqSolver (Make))); diff --git a/unittest/dune b/unittest/dune index a08a4b2323..036c8d8013 100644 --- a/unittest/dune +++ b/unittest/dune @@ -2,7 +2,7 @@ (test (name mainTest) - (libraries ounit2 qcheck-ounit goblint.std goblint.lib goblint.sites.dune goblint.build-info.dune) + (libraries ounit2 qcheck-ounit goblint.std goblint.lib goblint.constraint goblint.solver goblint.cdomain.value goblint.sites.dune goblint.build-info.dune) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall)) diff --git a/unittest/solver/solverTest.ml b/unittest/solver/solverTest.ml index 47ec5443ca..4e96266262 100644 --- a/unittest/solver/solverTest.ml +++ b/unittest/solver/solverTest.ml @@ -2,6 +2,8 @@ open Goblint_lib open OUnit2 open GoblintCil open Pretty +open ConstrSys +open Goblint_solver (* variables are strings *) module StringVar = @@ -43,7 +45,7 @@ module ConstrSys = struct | _ -> None let iter_vars _ _ _ _ _ = () - let sys_change _ _ = {Analyses.obsolete = []; delete = []; reluctant = []; restart = []} + let sys_change _ _ = {obsolete = []; delete = []; reluctant = []; restart = []} end module LH = BatHashtbl.Make (ConstrSys.LVar) @@ -55,7 +57,7 @@ struct let should_warn = false let should_save_run = false end -module Solver = Constraints.GlobSolverFromEqSolver (Constraints.EqIncrSolverFromEqSolver (EffectWConEq.Make) (PostSolverArg)) (ConstrSys) (LH) (GH) +module Solver = GlobSolverFromEqSolver (PostSolver.EqIncrSolverFromEqSolver (EffectWConEq.Make) (PostSolverArg)) (ConstrSys) (LH) (GH) let test1 _ = let id x = x in diff --git a/unittest/util/intOpsTest.ml b/unittest/util/intOpsTest.ml index 307d9e84b0..b0cb4dc984 100644 --- a/unittest/util/intOpsTest.ml +++ b/unittest/util/intOpsTest.ml @@ -1,6 +1,5 @@ open OUnit2 open Goblint_std -open Goblint_lib (* If the first operand of a div is negative, Zarith rounds the result away from zero. We thus always transform this into a division with a non-negative first operand. *)