Skip to content

Commit 0602af0

Browse files
sim642sim642
committed
Extract constraint systems from Analyses module
1 parent 8ac5fad commit 0602af0

18 files changed

+146
-137
lines changed

‎src/framework/analyses.ml‎

Lines changed: 2 additions & 124 deletions
Original file line numberDiff line numberDiff line change
@@ -11,24 +11,6 @@ module M = Messages
1111
* other functions. *)
1212
type fundecs = fundec list * fundec list * fundec list
1313

14-
module type SysVar =
15-
sig
16-
type t
17-
val is_write_only: t -> bool
18-
end
19-
20-
module type VarType =
21-
sig
22-
include Hashtbl.HashedType
23-
include SysVar with type t := t
24-
val pretty_trace: unit -> t -> doc
25-
val compare : t -> t -> int
26-
27-
val printXml : 'a BatInnerIO.output -> t -> unit
28-
val var_id : t -> string
29-
val node : t -> MyCFG.node
30-
val relift : t -> t (* needed only for incremental+hashcons to re-hashcons contexts after loading *)
31-
end
3214

3315
module Var =
3416
struct
@@ -69,7 +51,7 @@ end
6951
module type SpecSysVar =
7052
sig
7153
include Printable.S
72-
include SysVar with type t := t
54+
include ConstrSys.SysVar with type t := t
7355
end
7456

7557
module GVarF (V: SpecSysVar) =
@@ -318,110 +300,6 @@ type increment_data = {
318300
restarting: VarQuery.t list;
319301
}
320302

321-
(** Abstract incremental change to constraint system.
322-
@param 'v constrain system variable type *)
323-
type 'v sys_change_info = {
324-
obsolete: 'v list; (** Variables to destabilize. *)
325-
delete: 'v list; (** Variables to delete. *)
326-
reluctant: 'v list; (** Variables to solve reluctantly. *)
327-
restart: 'v list; (** Variables to restart. *)
328-
}
329-
330-
(** A side-effecting system. *)
331-
module type MonSystem =
332-
sig
333-
type v (* variables *)
334-
type d (* values *)
335-
type 'a m (* basically a monad carrier *)
336-
337-
(** Variables must be hashable, comparable, etc. *)
338-
module Var : VarType with type t = v
339-
340-
(** Values must form a lattice. *)
341-
module Dom : Lattice.S with type t = d
342-
343-
(** The system in functional form. *)
344-
val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m
345-
346-
val sys_change: (v -> d) -> v sys_change_info
347-
(** Compute incremental constraint system change from old solution. *)
348-
end
349-
350-
(** Any system of side-effecting equations over lattices. *)
351-
module type EqConstrSys = MonSystem with type 'a m := 'a option
352-
353-
(** A side-effecting system with globals. *)
354-
module type GlobConstrSys =
355-
sig
356-
module LVar : VarType
357-
module GVar : VarType
358-
359-
module D : Lattice.S
360-
module G : Lattice.S
361-
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
362-
val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
363-
val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info
364-
end
365-
366-
(** A solver is something that can translate a system into a solution (hash-table).
367-
Incremental solver has data to be marshaled. *)
368-
module type GenericEqIncrSolverBase =
369-
functor (S:EqConstrSys) ->
370-
functor (H:Hashtbl.S with type key=S.v) ->
371-
sig
372-
type marshal
373-
374-
val copy_marshal: marshal -> marshal
375-
val relift_marshal: marshal -> marshal
376-
377-
(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
378-
reached from starting values [xs].
379-
As a second component the solver returns data structures for incremental serialization. *)
380-
val solve : (S.v*S.d) list -> S.v list -> marshal option -> S.d H.t * marshal
381-
end
382-
383-
(** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *)
384-
module type IncrSolverArg =
385-
sig
386-
val should_prune: bool
387-
val should_verify: bool
388-
val should_warn: bool
389-
val should_save_run: bool
390-
end
391-
392-
(** An incremental solver takes the argument about postsolving. *)
393-
module type GenericEqIncrSolver =
394-
functor (Arg: IncrSolverArg) ->
395-
GenericEqIncrSolverBase
396-
397-
(** A solver is something that can translate a system into a solution (hash-table) *)
398-
module type GenericEqSolver =
399-
functor (S:EqConstrSys) ->
400-
functor (H:Hashtbl.S with type key=S.v) ->
401-
sig
402-
(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
403-
reached from starting values [xs]. *)
404-
val solve : (S.v*S.d) list -> S.v list -> S.d H.t
405-
end
406-
407-
(** A solver is something that can translate a system into a solution (hash-table) *)
408-
module type GenericGlobSolver =
409-
functor (S:GlobConstrSys) ->
410-
functor (LH:Hashtbl.S with type key=S.LVar.t) ->
411-
functor (GH:Hashtbl.S with type key=S.GVar.t) ->
412-
sig
413-
type marshal
414-
415-
val copy_marshal: marshal -> marshal
416-
val relift_marshal: marshal -> marshal
417-
418-
(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
419-
reached from starting values [xs].
420-
As a second component the solver returns data structures for incremental serialization. *)
421-
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
422-
end
423-
424-
425303
module StdV =
426304
struct
427305
let is_write_only _ = false
@@ -542,7 +420,7 @@ end
542420
module type SpecSys =
543421
sig
544422
module Spec: Spec
545-
module EQSys: GlobConstrSys with module LVar = VarF (Spec.C)
423+
module EQSys: ConstrSys.GlobConstrSys with module LVar = VarF (Spec.C)
546424
and module GVar = GVarF (Spec.V)
547425
and module D = Spec.D
548426
and module G = GVarG (Spec.G) (Spec.C)

‎src/framework/constrSys.ml‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
(** {{!MonSystem} constraint system} signatures. *)
2+
3+
open Batteries
4+
5+
module type SysVar =
6+
sig
7+
type t
8+
val is_write_only: t -> bool
9+
end
10+
11+
module type VarType =
12+
sig
13+
include Hashtbl.HashedType
14+
include SysVar with type t := t
15+
val pretty_trace: unit -> t -> GoblintCil.Pretty.doc
16+
val compare : t -> t -> int
17+
18+
val printXml : 'a BatInnerIO.output -> t -> unit
19+
val var_id : t -> string
20+
val node : t -> MyCFG.node
21+
val relift : t -> t (* needed only for incremental+hashcons to re-hashcons contexts after loading *)
22+
end
23+
24+
(** Abstract incremental change to constraint system.
25+
@param 'v constrain system variable type *)
26+
type 'v sys_change_info = {
27+
obsolete: 'v list; (** Variables to destabilize. *)
28+
delete: 'v list; (** Variables to delete. *)
29+
reluctant: 'v list; (** Variables to solve reluctantly. *)
30+
restart: 'v list; (** Variables to restart. *)
31+
}
32+
33+
(** A side-effecting system. *)
34+
module type MonSystem =
35+
sig
36+
type v (* variables *)
37+
type d (* values *)
38+
type 'a m (* basically a monad carrier *)
39+
40+
(** Variables must be hashable, comparable, etc. *)
41+
module Var : VarType with type t = v
42+
43+
(** Values must form a lattice. *)
44+
module Dom : Lattice.S with type t = d
45+
46+
(** The system in functional form. *)
47+
val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m
48+
49+
val sys_change: (v -> d) -> v sys_change_info
50+
(** Compute incremental constraint system change from old solution. *)
51+
end
52+
53+
(** Any system of side-effecting equations over lattices. *)
54+
module type EqConstrSys = MonSystem with type 'a m := 'a option
55+
56+
(** A side-effecting system with globals. *)
57+
module type GlobConstrSys =
58+
sig
59+
module LVar : VarType
60+
module GVar : VarType
61+
62+
module D : Lattice.S
63+
module G : Lattice.S
64+
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
65+
val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
66+
val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info
67+
end
68+
69+
(** A solver is something that can translate a system into a solution (hash-table).
70+
Incremental solver has data to be marshaled. *)
71+
module type GenericEqIncrSolverBase =
72+
functor (S:EqConstrSys) ->
73+
functor (H:Hashtbl.S with type key=S.v) ->
74+
sig
75+
type marshal
76+
77+
val copy_marshal: marshal -> marshal
78+
val relift_marshal: marshal -> marshal
79+
80+
(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
81+
reached from starting values [xs].
82+
As a second component the solver returns data structures for incremental serialization. *)
83+
val solve : (S.v*S.d) list -> S.v list -> marshal option -> S.d H.t * marshal
84+
end
85+
86+
(** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *)
87+
module type IncrSolverArg =
88+
sig
89+
val should_prune: bool
90+
val should_verify: bool
91+
val should_warn: bool
92+
val should_save_run: bool
93+
end
94+
95+
(** An incremental solver takes the argument about postsolving. *)
96+
module type GenericEqIncrSolver =
97+
functor (Arg: IncrSolverArg) ->
98+
GenericEqIncrSolverBase
99+
100+
(** A solver is something that can translate a system into a solution (hash-table) *)
101+
module type GenericEqSolver =
102+
functor (S:EqConstrSys) ->
103+
functor (H:Hashtbl.S with type key=S.v) ->
104+
sig
105+
(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
106+
reached from starting values [xs]. *)
107+
val solve : (S.v*S.d) list -> S.v list -> S.d H.t
108+
end
109+
110+
(** A solver is something that can translate a system into a solution (hash-table) *)
111+
module type GenericGlobSolver =
112+
functor (S:GlobConstrSys) ->
113+
functor (LH:Hashtbl.S with type key=S.LVar.t) ->
114+
functor (GH:Hashtbl.S with type key=S.GVar.t) ->
115+
sig
116+
type marshal
117+
118+
val copy_marshal: marshal -> marshal
119+
val relift_marshal: marshal -> marshal
120+
121+
(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
122+
reached from starting values [xs].
123+
As a second component the solver returns data structures for incremental serialization. *)
124+
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
125+
end

‎src/framework/constraints.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ open Batteries
55
open GoblintCil
66
open MyCFG
77
open Analyses
8+
open ConstrSys
89
open GobConfig
910

1011
module M = Messages

‎src/framework/control.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ open Batteries
66
open GoblintCil
77
open MyCFG
88
open Analyses
9+
open ConstrSys
910
open GobConfig
1011
open Constraints
1112

‎src/goblint_lib.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ module CfgTools = CfgTools
2121
A dynamic composition of analyses is combined with CFGs to produce a constraint system. *)
2222

2323
module Analyses = Analyses
24+
module ConstrSys = ConstrSys
2425
module Constraints = Constraints
2526
module AnalysisState = AnalysisState
2627
module AnalysisStateUtil = AnalysisStateUtil

‎src/solvers/effectWConEq.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
(** ([effectWConEq]). *)
22

33
open Batteries
4-
open Analyses
4+
open ConstrSys
55
open Constraints
66

77
module Make =

‎src/solvers/generic.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
open Batteries
44
open GobConfig
5-
open Analyses
5+
open ConstrSys
66

77
module LoadRunSolver: GenericEqSolver =
88
functor (S: EqConstrSys) (VH: Hashtbl.S with type key = S.v) ->

‎src/solvers/postSolver.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
(** Extra constraint system evaluation pass for warning generation, verification, pruning, etc. *)
22

33
open Batteries
4-
open Analyses
4+
open ConstrSys
55
open GobConfig
66
module Pretty = GoblintCil.Pretty
7+
module M = Messages
78

89
(** Postsolver with hooks. *)
910
module type S =

‎src/solvers/sLR.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
@see <http://www2.in.tum.de/bib/files/apinis14diss.pdf> Apinis, K. Frameworks for analyzing multi-threaded C. *)
44

55
open Batteries
6-
open Analyses
6+
open ConstrSys
77
open Constraints
88
open Messages
99

‎src/solvers/sLRphased.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
(** Two-phased terminating SLR3 solver ([slr3tp]). *)
22

33
open Batteries
4-
open Analyses
4+
open ConstrSys
55
open Constraints
66
open Messages
77
open SLR

0 commit comments

Comments
 (0)