Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Organize constraint system and value domain modules into dune libraries #1313

Merged
merged 12 commits into from
Dec 29, 2023
Merged
Prev Previous commit
Next Next commit
Extract constraint systems from Analyses module
  • Loading branch information
sim642 committed Dec 28, 2023
commit 0602af056a32170f090cf54c9555b7366a4c2fee
126 changes: 2 additions & 124 deletions src/framework/analyses.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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) =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
125 changes: 125 additions & 0 deletions src/framework/constrSys.ml
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions src/framework/constraints.ml
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ open Batteries
open GoblintCil
open MyCFG
open Analyses
open ConstrSys
open GobConfig

module M = Messages
Expand Down
1 change: 1 addition & 0 deletions src/framework/control.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ open Batteries
open GoblintCil
open MyCFG
open Analyses
open ConstrSys
open GobConfig
open Constraints

Expand Down
1 change: 1 addition & 0 deletions src/goblint_lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/effectWConEq.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(** ([effectWConEq]). *)

open Batteries
open Analyses
open ConstrSys
open Constraints

module Make =
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/generic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down
3 changes: 2 additions & 1 deletion src/solvers/postSolver.ml
Original file line number Diff line number Diff line change
@@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/sLR.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
@see <http://www2.in.tum.de/bib/files/apinis14diss.pdf> Apinis, K. Frameworks for analyzing multi-threaded C. *)

open Batteries
open Analyses
open ConstrSys
open Constraints
open Messages

Expand Down
2 changes: 1 addition & 1 deletion src/solvers/sLRphased.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(** Two-phased terminating SLR3 solver ([slr3tp]). *)

open Batteries
open Analyses
open ConstrSys
open Constraints
open Messages
open SLR
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/sLRterm.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
Simpler version of {!SLRphased} without phases. *)

open Batteries
open Analyses
open ConstrSys
open Constraints
open Messages
open SLR
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/selector.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(** Solver, which delegates at runtime to the configured solver. *)

open Batteries
open Analyses
open ConstrSys
open GobConfig

(* Registered solvers. *)
Expand Down
4 changes: 3 additions & 1 deletion src/solvers/td3.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,11 @@
*)

open Batteries
open Analyses
open ConstrSys
open Messages

module M = Messages

module type Hooks =
sig
module S: EqConstrSys
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/topDown.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
Simpler version of {!Td3} without terminating, space-efficiency and incremental. *)

open Batteries
open Analyses
open ConstrSys
open Constraints
open Messages

Expand Down
Loading
Loading