From 0602af056a32170f090cf54c9555b7366a4c2fee Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Dec 2023 14:56:31 +0200 Subject: [PATCH] Extract constraint systems from Analyses module --- src/framework/analyses.ml | 126 +----------------------- src/framework/constrSys.ml | 125 +++++++++++++++++++++++ src/framework/constraints.ml | 1 + src/framework/control.ml | 1 + src/goblint_lib.ml | 1 + src/solvers/effectWConEq.ml | 2 +- src/solvers/generic.ml | 2 +- src/solvers/postSolver.ml | 3 +- src/solvers/sLR.ml | 2 +- src/solvers/sLRphased.ml | 2 +- src/solvers/sLRterm.ml | 2 +- src/solvers/selector.ml | 2 +- src/solvers/td3.ml | 4 +- src/solvers/topDown.ml | 2 +- src/solvers/topDown_deprecated.ml | 2 +- src/solvers/topDown_space_cache_term.ml | 2 +- src/solvers/topDown_term.ml | 2 +- src/solvers/worklist.ml | 2 +- 18 files changed, 146 insertions(+), 137 deletions(-) create mode 100644 src/framework/constrSys.ml diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 633eea1b39..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) = @@ -318,110 +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 StdV = struct let is_write_only _ = false @@ -542,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/constrSys.ml b/src/framework/constrSys.ml new file mode 100644 index 0000000000..936e03355c --- /dev/null +++ b/src/framework/constrSys.ml @@ -0,0 +1,125 @@ +(** {{!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 \ No newline at end of file diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 8039a867d8..28e6f2f287 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 diff --git a/src/framework/control.ml b/src/framework/control.ml index 54fd1d7774..26ef8bbda0 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 diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 2cbe737079..a340cb085f 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 diff --git a/src/solvers/effectWConEq.ml b/src/solvers/effectWConEq.ml index c6dcf8f0e9..2455dc10f2 100644 --- a/src/solvers/effectWConEq.ml +++ b/src/solvers/effectWConEq.ml @@ -1,7 +1,7 @@ (** ([effectWConEq]). *) open Batteries -open Analyses +open ConstrSys open Constraints module Make = diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml index 2569341dd1..025074c149 100644 --- a/src/solvers/generic.ml +++ b/src/solvers/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) -> diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index e01560c752..ebfa17063a 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/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 = diff --git a/src/solvers/sLR.ml b/src/solvers/sLR.ml index 4904731b61..d6bc2a56a5 100644 --- a/src/solvers/sLR.ml +++ b/src/solvers/sLR.ml @@ -3,7 +3,7 @@ @see Apinis, K. Frameworks for analyzing multi-threaded C. *) open Batteries -open Analyses +open ConstrSys open Constraints open Messages diff --git a/src/solvers/sLRphased.ml b/src/solvers/sLRphased.ml index c120a7bc6c..5f48669b14 100644 --- a/src/solvers/sLRphased.ml +++ b/src/solvers/sLRphased.ml @@ -1,7 +1,7 @@ (** Two-phased terminating SLR3 solver ([slr3tp]). *) open Batteries -open Analyses +open ConstrSys open Constraints open Messages open SLR diff --git a/src/solvers/sLRterm.ml b/src/solvers/sLRterm.ml index eb11447d11..b90e195ec4 100644 --- a/src/solvers/sLRterm.ml +++ b/src/solvers/sLRterm.ml @@ -2,7 +2,7 @@ Simpler version of {!SLRphased} without phases. *) open Batteries -open Analyses +open ConstrSys open Constraints open Messages open SLR diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml index 664cbe0513..854b8e1036 100644 --- a/src/solvers/selector.ml +++ b/src/solvers/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/td3.ml b/src/solvers/td3.ml index 07edc632c7..b2696787e6 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -15,9 +15,11 @@ *) open Batteries -open Analyses +open ConstrSys open Messages +module M = Messages + module type Hooks = sig module S: EqConstrSys diff --git a/src/solvers/topDown.ml b/src/solvers/topDown.ml index c6b20d28db..fe6aaf53da 100644 --- a/src/solvers/topDown.ml +++ b/src/solvers/topDown.ml @@ -2,7 +2,7 @@ Simpler version of {!Td3} without terminating, space-efficiency and incremental. *) open Batteries -open Analyses +open ConstrSys open Constraints open Messages diff --git a/src/solvers/topDown_deprecated.ml b/src/solvers/topDown_deprecated.ml index 1f51244458..3e1329aa19 100644 --- a/src/solvers/topDown_deprecated.ml +++ b/src/solvers/topDown_deprecated.ml @@ -1,7 +1,7 @@ (** Deprecated top-down solver ([topdown_deprecated]). *) open Batteries -open Analyses +open ConstrSys open Constraints open Messages diff --git a/src/solvers/topDown_space_cache_term.ml b/src/solvers/topDown_space_cache_term.ml index a78d90559d..1bf8127fb9 100644 --- a/src/solvers/topDown_space_cache_term.ml +++ b/src/solvers/topDown_space_cache_term.ml @@ -2,7 +2,7 @@ Simpler version of {!Td3} without incremental. *) open Batteries -open Analyses +open ConstrSys open Constraints open Messages diff --git a/src/solvers/topDown_term.ml b/src/solvers/topDown_term.ml index ec07995586..f62aa74a5c 100644 --- a/src/solvers/topDown_term.ml +++ b/src/solvers/topDown_term.ml @@ -2,7 +2,7 @@ Simpler version of {!Td3} without space-efficiency and incremental. *) open Batteries -open Analyses +open ConstrSys open Constraints open Messages diff --git a/src/solvers/worklist.ml b/src/solvers/worklist.ml index b525764c74..2954928a23 100644 --- a/src/solvers/worklist.ml +++ b/src/solvers/worklist.ml @@ -1,7 +1,7 @@ (** Worklist solver ([WL]). *) open Batteries -open Analyses +open ConstrSys open Constraints module Make =